summaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml158
1 files changed, 81 insertions, 77 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c7db802f..ab6c1393 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,6 +28,7 @@ open CErrors
open Util
open Names
open Evd
+open Constr
open Term
open Termops
open Environ
@@ -44,7 +45,6 @@ open Pretype_errors
open Glob_term
open Glob_ops
open Evarconv
-open Misctypes
open Ltac_pretype
module NamedDecl = Context.Named.Declaration
@@ -117,7 +117,7 @@ open ExtraEnv
exception Found of int array
let nf_fix sigma (nas, cs, ts) =
- let inj c = EConstr.to_constr sigma c in
+ let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
(nas, Array.map inj cs, Array.map inj ts)
let search_guard ?loc env possible_indexes fixdefs =
@@ -169,48 +169,39 @@ let _ =
optread = is_strict_universe_declarations;
optwrite = (:=) strict_universe_declarations })
-let _ =
- Goptions.(declare_bool_option
- { optdepr = false;
- optname = "minimization to Set";
- optkey = ["Universe";"Minimization";"ToSet"];
- optread = Universes.is_set_minimization;
- optwrite = (:=) Universes.set_minimization })
-
(** Miscellaneous interpretation functions *)
-let interp_known_universe_level evd r =
- let qid = Libnames.qualid_of_reference r in
+let interp_known_universe_level evd qid =
try
- match r.CAst.v with
- | Libnames.Ident id -> Evd.universe_of_name evd id
- | Libnames.Qualid _ -> raise Not_found
+ let open Libnames in
+ if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid
+ else raise Not_found
with Not_found ->
- let univ, k = Nametab.locate_universe qid.CAst.v in
+ let univ, k = Nametab.locate_universe qid in
Univ.Level.make univ k
-let interp_universe_level_name ~anon_rigidity evd r =
- try evd, interp_known_universe_level evd r
+let interp_universe_level_name ~anon_rigidity evd qid =
+ try evd, interp_known_universe_level evd qid
with Not_found ->
- match r with (* Qualified generated name *)
- | {CAst.loc; v=Libnames.Qualid qid} ->
- let dp, i = Libnames.repr_qualid qid in
- let num =
- try int_of_string (Id.to_string i)
- with Failure _ ->
- user_err ?loc ~hdr:"interp_universe_level_name"
- (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r))
- in
- let level = Univ.Level.make dp num in
- let evd =
- try Evd.add_global_univ evd level
- with UGraph.AlreadyDeclared -> evd
- in evd, level
- | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *)
- if not (is_strict_universe_declarations ()) then
- new_univ_level_variable ?loc ~name:id univ_rigid evd
- else user_err ?loc ~hdr:"interp_universe_level_name"
- (Pp.(str "Undeclared universe: " ++ Id.print id))
+ if Libnames.qualid_is_ident qid then (* Undeclared *)
+ let id = Libnames.qualid_basename qid in
+ if not (is_strict_universe_declarations ()) then
+ new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd
+ else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+ (Pp.(str "Undeclared universe: " ++ Id.print id))
+ else
+ let dp, i = Libnames.repr_qualid qid in
+ let num =
+ try int_of_string (Id.to_string i)
+ with Failure _ ->
+ user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name"
+ (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid))
+ in
+ let level = Univ.Level.make dp num in
+ let evd =
+ try Evd.add_global_univ evd level
+ with UGraph.AlreadyDeclared -> evd
+ in evd, level
let interp_universe ?loc evd = function
| [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in
@@ -240,12 +231,12 @@ let interp_known_level_info ?loc evd = function
| UUnknown | UAnonymous ->
user_err ?loc ~hdr:"interp_known_level_info"
(str "Anonymous universes not allowed here.")
- | UNamed ref ->
- try interp_known_universe_level evd ref
+ | UNamed qid ->
+ try interp_known_universe_level evd qid
with Not_found ->
- user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
+ user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid)
-let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
+let interp_level_info ?loc evd : level_info -> _ = function
| UUnknown -> new_univ_level_variable ?loc univ_rigid evd
| UAnonymous -> new_univ_level_variable ?loc univ_flexible evd
| UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s
@@ -315,7 +306,7 @@ let apply_inference_hook hook evdref frozen = match frozen with
then
try
let sigma, c = hook sigma evk in
- Evd.define evk (EConstr.Unsafe.to_constr c) sigma
+ Evd.define evk c sigma
with Exit ->
sigma
else
@@ -390,8 +381,16 @@ let adjust_evar_source evdref na c =
| Name id, Evar (evk,args) ->
let evi = Evd.find !evdref evk in
begin match evi.evar_source with
- | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
- let src = (loc,Evar_kinds.QuestionMark (b,na)) in
+ | loc, Evar_kinds.QuestionMark {
+ Evar_kinds.qm_obligation=b;
+ Evar_kinds.qm_name=Anonymous;
+ Evar_kinds.qm_record_field=recfieldname;
+ } ->
+ let src = (loc,Evar_kinds.QuestionMark {
+ Evar_kinds.qm_obligation=b;
+ Evar_kinds.qm_name=na;
+ Evar_kinds.qm_record_field=recfieldname;
+ }) in
let (evd, evk') = restrict_evar !evdref evk (evar_filter evi) ~src None in
evdref := evd;
mkEvar (evk',args)
@@ -429,7 +428,7 @@ let ltac_interp_name_env k0 lvar env sigma =
let n = Context.Rel.length (rel_context env) - k0 in
let ctxt,_ = List.chop n (rel_context env) in
let open Context.Rel.Declaration in
- let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in
+ let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in
if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
else push_rel_context sigma ctxt' (pop_rel_context n env sigma)
@@ -445,7 +444,7 @@ let protected_get_type_of env sigma c =
try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
with Retyping.RetypeError _ ->
user_err
- (str "Cannot reinterpret " ++ quote (print_constr c) ++
+ (str "Cannot reinterpret " ++ quote (Termops.Internal.print_constr_env env.ExtraEnv.env sigma c) ++
str " in the current environment.")
let pretype_id pretype k0 loc env evdref lvar id =
@@ -499,7 +498,7 @@ let interp_known_glob_level ?loc evd = function
| GSet -> Univ.Level.set
| GType s -> interp_known_level_info ?loc evd s
-let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function
+let interp_glob_level ?loc evd : glob_level -> _ = function
| GProp -> evd, Univ.Level.prop
| GSet -> evd, Univ.Level.set
| GType s -> interp_level_info ?loc evd s
@@ -532,7 +531,7 @@ let pretype_global ?loc rigid env evd gr us =
interp_instance ?loc evd ~len l
in
let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
- (sigma, EConstr.of_constr c)
+ (sigma, c)
let pretype_ref ?loc evdref env ref us =
match ref with
@@ -674,14 +673,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
let nbfix = Array.length lar in
let names = Array.map (fun id -> Name id) names in
- let _ =
+ let () =
match tycon with
| Some t ->
let fixi = match fixkind with
| GFix (vn,i) -> i
| GCoFix i -> i
- in e_conv env.ExtraEnv.env evdref ftys.(fixi) t
- | None -> true
+ in
+ begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with
+ | None -> ()
+ | Some sigma -> evdref := sigma
+ end
+ | None -> ()
in
(* Note: bodies are not used by push_rec_types, so [||] is safe *)
let newenv = push_rec_types !evdref (names,ftys,[||]) env in
@@ -698,7 +701,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
ctxtv vdef in
- Typing.check_type_fixpoint ?loc env.ExtraEnv.env evdref names ftys vdefj;
+ evdref := Typing.check_type_fixpoint ?loc env.ExtraEnv.env !evdref names ftys vdefj;
let nf c = nf_evar !evdref c in
let ftys = Array.map nf ftys in (** FIXME *)
let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in
@@ -765,11 +768,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
in
let app_f =
match EConstr.kind !evdref fj.uj_val with
- | Const (p, u) when Environ.is_projection p env.ExtraEnv.env ->
+ | Const (p, u) when Recordops.is_primitive_projection p ->
+ let p = Option.get @@ Recordops.find_primitive_projection p in
let p = Projection.make p false in
- let pb = Environ.lookup_projection p env.ExtraEnv.env in
- let npars = pb.Declarations.proj_npars in
- fun n ->
+ let npars = Projection.npars p in
+ fun n ->
if n == npars + 1 then fun _ v -> mkProj (p, v)
else fun f v -> applist (f, [v])
| _ -> fun _ f v -> applist (f, [v])
@@ -788,9 +791,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
match candargs with
| [] -> [], j_val hj
| arg :: args ->
- if e_conv env.ExtraEnv.env evdref (j_val hj) arg then
- args, nf_evar !evdref (j_val hj)
- else [], j_val hj
+ begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with
+ | Some sigma -> evdref := sigma;
+ args, nf_evar !evdref (j_val hj)
+ | None ->
+ [], j_val hj
+ end
in
let ujval = adjust_evar_source evdref na ujval in
let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
@@ -894,6 +900,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cloc = loc_of_glob_constr c in
error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj
in
+ let ind = fst (fst (dest_ind_family indf)) in
let cstrs = get_constructors env.ExtraEnv.env indf in
if not (Int.equal (Array.length cstrs) 1) then
user_err ?loc (str "Destructing let is only for inductive types" ++
@@ -904,7 +911,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
int cs.cs_nargs ++ str " variables.");
let fsign, record =
let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in
- match get_projections env.ExtraEnv.env indf with
+ match Environ.get_projections env.ExtraEnv.env ind with
| None ->
List.map2 set_name (List.rev nal) cs.cs_args, false
| Some ps ->
@@ -920,9 +927,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| [], [] -> []
| _ -> assert false
in aux 1 1 (List.rev nal) cs.cs_args, true in
- let fsign = if Flags.version_strictly_greater Flags.V8_6
- then Context.Rel.map (whd_betaiota !evdref) fsign
- else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+ let fsign = Context.Rel.map (whd_betaiota !evdref) fsign in
let obj ind p v f =
if not record then
let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
@@ -1032,10 +1037,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
- let cs_args =
- if Flags.version_strictly_greater Flags.V8_6
- then Context.Rel.map (whd_betaiota !evdref) cs_args
- else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+ let cs_args = Context.Rel.map (whd_betaiota !evdref) cs_args in
let csgn =
List.map (set_name Anonymous) cs_args
in
@@ -1077,9 +1079,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
if not (occur_existential !evdref cty || occur_existential !evdref tval) then
- let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
- if b then (evdref := evd; cj, tval)
- else
+ match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with
+ | Some evd -> (evdref := evd; cj, tval)
+ | None ->
error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
(ConversionFailed (env.ExtraEnv.env,cty,tval))
else user_err ?loc (str "Cannot check cast with vm: " ++
@@ -1088,9 +1090,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
begin
- let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
- if b then (evdref := evd; cj, tval)
- else
+ match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with
+ | Some evd -> (evdref := evd; cj, tval)
+ | None ->
error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
(ConversionFailed (env.ExtraEnv.env,cty,tval))
end
@@ -1104,7 +1106,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
let f decl (subst,update) =
let id = NamedDecl.get_id decl in
- let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in
+ let t = replace_vars subst (NamedDecl.get_type decl) in
let c, update =
try
let c = List.assoc id update in
@@ -1145,7 +1147,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
(* Correction of bug #5315 : we need to define an evar for *all* holes *)
let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in
let ev,_ = destEvar !evdref evkt in
- evdref := Evd.define ev (to_constr !evdref v) !evdref;
+ evdref := Evd.define ev (nf_evar !evdref v) !evdref;
(* End of correction of bug #5315 *)
{ utj_val = v;
utj_type = s }
@@ -1161,10 +1163,12 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
match valcon with
| None -> tj
| Some v ->
- if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj
- else
+ begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with
+ | Some sigma -> evdref := sigma; tj
+ | None ->
error_unexpected_type
?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
+ end
let ise_pretype_gen flags env sigma lvar kind c =
let env = make_env env sigma in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 15:17:59 +0000