From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 30 Oct 2016 17:53:07 +0100 Subject: Termops API using EConstr. --- pretyping/pretyping.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8f369a811e..9b572f376d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -751,7 +751,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if is_template_polymorphic env.ExtraEnv.env f then + if is_template_polymorphic env.ExtraEnv.env !evdref (EConstr.of_constr f) then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in @@ -1009,7 +1009,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | VMcast -> 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 cty || occur_existential tval) then + if not (occur_existential !evdref (EConstr.of_constr cty) || occur_existential !evdref (EConstr.of_constr tval)) then let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else -- cgit v1.2.3 From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- pretyping/pretyping.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9b572f376d..3a6d4f36cc 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -700,7 +700,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if Int.equal npars 0 then [] else try - let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in + let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr ty) in let ((ind',u'),pars) = dest_ind_family indf in if eq_ind ind ind' then pars else (* Let the usual code throw an error *) [] @@ -723,7 +723,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | c::rest -> let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in - let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in + let resty = whd_all env.ExtraEnv.env !evdref (EConstr.of_constr resj.uj_type) in match kind_of_term resty with | Prod (na,c1,c2) -> let tycon = Some c1 in @@ -834,7 +834,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env.ExtraEnv.env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type) with Not_found -> let cloc = loc_of_glob_constr c in error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj @@ -894,7 +894,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (Array.to_list cs.cs_concl_realargs) @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in + let fty = hnf_lam_applist env.ExtraEnv.env !evdref (EConstr.of_constr lp) (List.map EConstr.of_constr inst) in let fj = pretype (mk_tycon fty) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in @@ -924,7 +924,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env.ExtraEnv.env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type) with Not_found -> let cloc = loc_of_glob_constr c in error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in @@ -948,7 +948,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in + let typ = lift (- nar) (beta_applist !evdref (EConstr.of_constr pred,[EConstr.of_constr cj.uj_val])) in pred, typ | None -> let p = match tycon with @@ -963,7 +963,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let f cs b = let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) - let pi = beta_applist (pi, [build_dependent_constructor cs]) in + let pi = beta_applist !evdref (EConstr.of_constr pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let csgn = if not !allow_anonymous_refs then List.map (set_name Anonymous) cs.cs_args @@ -1046,11 +1046,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref (EConstr.of_constr t) (EConstr.of_constr t') then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in - if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref (EConstr.of_constr t) (EConstr.of_constr t') then mkVar id, update else raise Not_found with Not_found -> user_err ~loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ @@ -1068,7 +1068,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let s = let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in - match kind_of_term (whd_all env.ExtraEnv.env sigma t) with + match kind_of_term (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t)) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev -- cgit v1.2.3 From 6bd193ff409b01948751525ce0f905916d7a64bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:38:35 +0100 Subject: Nativenorm API using EConstr. --- pretyping/pretyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3a6d4f36cc..2f42ad3954 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1021,7 +1021,7 @@ 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 + let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref (EConstr.of_constr cty) (EConstr.of_constr tval) in if b then (evdref := evd; cj, tval) else error_actual_type ~loc env.ExtraEnv.env !evdref cj tval -- cgit v1.2.3 From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:48:36 +0100 Subject: Retyping API using EConstr. --- pretyping/pretyping.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2f42ad3954..3c48c42df2 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -409,7 +409,7 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c + try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma (EConstr.of_constr c) with Retyping.RetypeError _ -> user_err (str "Cannot reinterpret " ++ quote (print_constr c) ++ @@ -563,7 +563,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in + let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref (EConstr.of_constr c)) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> @@ -757,7 +757,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in - let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in + let t = Retyping.get_type_of env.ExtraEnv.env !evdref (EConstr.of_constr c) in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj @@ -1067,7 +1067,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | Some v -> let s = let sigma = !evdref in - let t = Retyping.get_type_of env.ExtraEnv.env sigma v in + let t = Retyping.get_type_of env.ExtraEnv.env sigma (EConstr.of_constr v) in match kind_of_term (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t)) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> -- cgit v1.2.3 From 147afe827dc83602cc160a8b1357e84ecea910ff Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Nov 2016 20:13:32 +0100 Subject: Evardefine API using EConstr. --- pretyping/pretyping.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3c48c42df2..b689bb7c7f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -606,7 +606,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in + let bd' = pretype (mk_tycon (EConstr.of_constr ty'.utj_val)) env evdref lvar bd in let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in @@ -640,7 +640,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre decompose_prod_n_assum (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in let nenv = push_rel_context ctxt newenv in - let j = pretype (mk_tycon ty) nenv evdref lvar def in + let j = pretype (mk_tycon (EConstr.of_constr ty)) nenv evdref lvar def in { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in @@ -815,7 +815,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match c1 with | GCast (loc, c, CastConv t) -> let tj = pretype_type empty_valcon env evdref lvar t in - pretype (mk_tycon tj.utj_val) env evdref lvar c + pretype (mk_tycon (EConstr.of_constr tj.utj_val)) env evdref lvar c | _ -> pretype empty_tycon env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes @@ -895,7 +895,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in let fty = hnf_lam_applist env.ExtraEnv.env !evdref (EConstr.of_constr lp) (List.map EConstr.of_constr inst) in - let fj = pretype (mk_tycon fty) env_f evdref lvar d in + let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; @@ -973,7 +973,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre cs.cs_args in let env_c = push_rel_context csgn env in - let bj = pretype (mk_tycon pi) env_c evdref lvar b in + let bj = pretype (mk_tycon (EConstr.of_constr pi)) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs.cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in @@ -1028,7 +1028,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> - pretype (mk_tycon tval) env evdref lvar c, tval + pretype (mk_tycon (EConstr.of_constr tval)) env evdref lvar c, tval in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } @@ -1041,7 +1041,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let c, update = try let c = List.assoc id update in - let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in + let c = pretype k0 resolve_tc (mk_tycon (EConstr.of_constr t)) env evdref lvar c in c.uj_val, List.remove_assoc id update with Not_found -> try @@ -1068,9 +1068,9 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let s = let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma (EConstr.of_constr v) in - match kind_of_term (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t)) with + match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t))) with | Sort s -> s - | Evar ev when is_Type (existential_type sigma ev) -> + | Evar ev when is_Type (existential_type sigma (fst ev, Array.map EConstr.Unsafe.to_constr (snd ev))) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in @@ -1101,7 +1101,7 @@ let ise_pretype_gen flags env sigma lvar kind c = | WithoutTypeConstraint -> (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val | OfType exptyp -> - (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val + (pretype k0 flags.use_typeclasses (mk_tycon (EConstr.of_constr exptyp)) env evdref lvar c).uj_val | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in -- cgit v1.2.3 From b7fd585b89ac5e0b7770f52739c33fe179f2eed8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Nov 2016 21:36:40 +0100 Subject: Evarsolve API using EConstr. --- pretyping/pretyping.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b689bb7c7f..fbba682fc1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -756,7 +756,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref (EConstr.of_constr c) in let t = Retyping.get_type_of env.ExtraEnv.env !evdref (EConstr.of_constr c) in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj @@ -820,7 +820,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) - evdref j.uj_type in + evdref (EConstr.of_constr j.uj_type) in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) @@ -1003,7 +1003,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let tj = pretype_type empty_valcon env evdref lvar t in let tval = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) - evdref tj.utj_val in + evdref (EConstr.of_constr tj.utj_val) in let tval = nf_evar !evdref tval in let cj, tval = match k with | VMcast -> @@ -1014,7 +1014,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if b then (evdref := evd; cj, tval) else error_actual_type ~loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,cty,tval)) + (ConversionFailed (env.ExtraEnv.env,EConstr.of_constr cty,EConstr.of_constr tval)) else user_err ~loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> @@ -1025,7 +1025,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if b then (evdref := evd; cj, tval) else error_actual_type ~loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,cty,tval)) + (ConversionFailed (env.ExtraEnv.env,EConstr.of_constr cty,EConstr.of_constr tval)) end | _ -> pretype (mk_tycon (EConstr.of_constr tval)) env evdref lvar c, tval -- cgit v1.2.3 From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 03:23:13 +0100 Subject: Evarconv API using EConstr. --- pretyping/pretyping.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index fbba682fc1..570f95324a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -626,7 +626,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env.ExtraEnv.env evdref ftys.(fixi) t + in e_conv env.ExtraEnv.env evdref (EConstr.of_constr ftys.(fixi)) (EConstr.of_constr t) | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) @@ -732,7 +732,7 @@ 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 + if e_conv env.ExtraEnv.env evdref (EConstr.of_constr (j_val hj)) (EConstr.of_constr arg) then args, nf_evar !evdref (j_val hj) else [], j_val hj in @@ -1088,7 +1088,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function match valcon with | None -> tj | Some v -> - if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj + if e_cumul env.ExtraEnv.env evdref (EConstr.of_constr v) (EConstr.of_constr tj.utj_val) then tj else error_unexpected_type ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v -- cgit v1.2.3 From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- pretyping/pretyping.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 570f95324a..28ba60812b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -507,7 +507,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in + let ty = Typing.unsafe_type_of env.ExtraEnv.env evd (EConstr.of_constr c) in make_judge c ty let judge_of_Type loc evd s = @@ -644,7 +644,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; + Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names (Array.map EConstr.of_constr ftys) vdefj; let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with @@ -898,7 +898,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p); obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } @@ -917,7 +917,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p); obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) @@ -981,7 +981,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let ind,_ = dest_ind_family indf in let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr pred); mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in -- cgit v1.2.3 From e4f066238799a4598817dfeab8a044760ab670de Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 20:33:06 +0100 Subject: Coercion API using EConstr. --- pretyping/pretyping.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 28ba60812b..18731f1e90 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -359,7 +359,7 @@ let allow_anonymous_refs = ref false let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j (EConstr.of_constr t) let check_instance loc subst = function | [] -> () @@ -770,8 +770,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in - evd, Some ty') + let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd (EConstr.of_constr ty) in + evd, Some (EConstr.Unsafe.to_constr ty')) evdref tycon in let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in -- cgit v1.2.3 From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Nov 2016 19:02:40 +0100 Subject: Pretyping API using EConstr. --- pretyping/pretyping.ml | 285 ++++++++++++++++++++++++++++--------------------- 1 file changed, 161 insertions(+), 124 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 18731f1e90..cac31a1c57 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -27,8 +27,9 @@ open Util open Names open Evd open Term -open Vars open Termops +open EConstr +open Vars open Reductionops open Environ open Type_errors @@ -59,7 +60,7 @@ type ltac_var_map = { ltac_genargs : unbound_ltac_var_map; } type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * constr +type pure_open_constr = evar_map * Constr.constr (************************************************************************) (* This concerns Cases *) @@ -68,6 +69,16 @@ open Inductiveops (************************************************************************) +let local_assum (na, t) = + let open Context.Rel.Declaration in + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let local_def (na, b, t) = + let open Context.Rel.Declaration in + let inj = EConstr.Unsafe.to_constr in + LocalDef (na, inj b, inj t) + module ExtraEnv = struct @@ -104,7 +115,7 @@ let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in - let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in + let inst_vars = List.map (get_id %> Constr.mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in let (subst, vsubst, _, nc) = Lazy.force env.extra in let typ' = subst2 subst vsubst typ in @@ -116,7 +127,7 @@ let e_new_evar env evdref ?src ?naming typ = e let push_rec_types (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt end @@ -127,6 +138,13 @@ open ExtraEnv exception Found of int array +let nf_fix sigma (nas, cs, ts) = + let inj c = EConstr.to_constr sigma c in + (nas, Array.map inj cs, Array.map inj ts) + +let nf_evar sigma c = + EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c)) + let search_guard loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) @@ -282,7 +300,7 @@ let apply_inference_hook hook evdref pending = then try let sigma, c = hook sigma evk in - Evd.define evk c sigma + Evd.define evk (EConstr.Unsafe.to_constr c) sigma with Exit -> sigma else @@ -313,17 +331,15 @@ let check_extra_evars_are_solved env current_sigma pending = let check_evars env initial_sigma sigma c = let rec proc_rec c = - match kind_of_term c with - | Evar (evk,_ as ev) -> - (match existential_opt_value sigma ev with - | Some c -> proc_rec c - | None -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in - match k with - | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None) - | _ -> Constr.iter proc_rec c + match EConstr.kind sigma c with + | Evar (evk, _) -> + if not (Evd.mem initial_sigma evk) then + let (loc,k) = evar_source evk sigma in + begin match k with + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () + | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None + end + | _ -> EConstr.iter sigma proc_rec c in proc_rec c let check_evars_are_solved env current_sigma frozen pending = @@ -359,7 +375,7 @@ let allow_anonymous_refs = ref false let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j (EConstr.of_constr t) + evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () @@ -409,26 +425,29 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma (EConstr.of_constr 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 (print_constr (EConstr.Unsafe.to_constr c)) ++ str " in the current environment.") +let j_val j = EConstr.of_constr (j_val j) + let pretype_id pretype k0 loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in - { uj_val = mkRel n; uj_type = lift n typ } + let typ = EConstr.of_constr typ in + { uj_val = EConstr.Unsafe.to_constr (mkRel n); uj_type = EConstr.Unsafe.to_constr (lift n typ) } with Not_found -> let env = ltac_interp_name_env k0 lvar env in (* Check if [id] is an ltac variable *) try let (ids,c) = Id.Map.find id lvar.ltac_constrs in let subst = List.map (invert_ltac_bound_name lvar env id) ids in - let c = substl subst c in - { uj_val = c; uj_type = protected_get_type_of env sigma c } + let c = substl subst (EConstr.of_constr c) in + { uj_val = EConstr.Unsafe.to_constr c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in let lvar = { @@ -453,14 +472,11 @@ let pretype_id pretype k0 loc env evdref lvar id = end; (* Check if [id] is a section or goal variable *) try - { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } + { uj_val = Constr.mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found ~loc id -let evar_kind_of_term sigma c = - kind_of_term (whd_evar sigma c) - (*************************************************************************) (* Main pretyping function *) @@ -492,13 +508,17 @@ let pretype_global loc rigid env evd gr us = str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) in - Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr + let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in + (sigma, EConstr.of_constr c) + +let make_judge c t = + make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) let pretype_ref loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env)) + (try make_judge (mkVar id) (EConstr.of_constr (NamedDecl.get_type (lookup_named id env))) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -507,13 +527,14 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env.ExtraEnv.env evd (EConstr.of_constr c) in + let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in + let ty = EConstr.of_constr ty in make_judge c ty let judge_of_Type loc evd s = let evd, s = interp_universe ~loc evd s in let judge = - { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } + { uj_val = Constr.mkSort (Type s); uj_type = Constr.mkSort (Type (Univ.super s)) } in evd, judge @@ -563,32 +584,32 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref (EConstr.of_constr c)) in + let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> ty + | Some ty -> EConstr.Unsafe.to_constr ty | None -> new_type_evar env evdref loc in let k = Evar_kinds.MatchingVar (someta,n) in - { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) (EConstr.of_constr ty); uj_type = ty } | GHole (loc, k, naming, None) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> ty + | Some ty -> EConstr.Unsafe.to_constr ty | None -> new_type_evar env evdref loc in - { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming (EConstr.of_constr ty); uj_type = ty } | GHole (loc, k, _naming, Some arg) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> ty + | Some ty -> EConstr.Unsafe.to_constr ty | None -> new_type_evar env evdref loc in let ist = lvar.ltac_genargs in @@ -616,8 +637,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (fun e ar -> pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) ctxtv lar in - let lara = Array.map (fun a -> a.utj_val) larj in - let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in + let lara = Array.map (fun a -> EConstr.of_constr a.utj_val) larj in + let ftys = Array.map2 (fun e a -> EConstr.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 _ = @@ -626,7 +647,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env.ExtraEnv.env evdref (EConstr.of_constr ftys.(fixi)) (EConstr.of_constr t) + in e_conv env.ExtraEnv.env evdref ftys.(fixi) t | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) @@ -637,16 +658,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) let (ctxt,ty) = - decompose_prod_n_assum (Context.Rel.length ctxt) + decompose_prod_n_assum !evdref (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in let nenv = push_rel_context ctxt newenv in - let j = pretype (mk_tycon (EConstr.of_constr ty)) nenv evdref lvar def in - { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; - uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) + let j = pretype (mk_tycon ty) nenv evdref lvar def in + { uj_val = Termops.it_mkLambda_or_LetIn j.uj_val ctxt; + uj_type = Termops.it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names (Array.map EConstr.of_constr ftys) vdefj; - let ftys = Array.map (nf_evar !evdref) ftys in - let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in + 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 let fixj = match fixkind with | GFix (vn,i) -> (* First, let's find the guard indexes. *) @@ -665,12 +687,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - loc env.ExtraEnv.env possible_indexes fixdecls + loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls) in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> - let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env.ExtraEnv.env cofix + let fixdecls = (names,ftys,fdefs) in + let cofix = (i, fixdecls) in + (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls) with reraise -> let (e, info) = CErrors.push reraise in let info = Loc.add_loc info loc in @@ -691,24 +714,24 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* Bidirectional typechecking hint: parameters of a constructor are completely determined by a typing constraint *) - if Flags.is_program_mode () && length > 0 && isConstruct fj.uj_val then + if Flags.is_program_mode () && length > 0 && isConstruct !evdref (EConstr.of_constr fj.uj_val) then match tycon with | None -> [] | Some ty -> - let ((ind, i), u) = destConstruct fj.uj_val in + let ((ind, i), u) = destConstruct !evdref (EConstr.of_constr fj.uj_val) in let npars = inductive_nparams ind in if Int.equal npars 0 then [] else try - let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr ty) in + let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in - if eq_ind ind ind' then pars + if eq_ind ind ind' then List.map EConstr.of_constr pars else (* Let the usual code throw an error *) [] with Not_found -> [] else [] in let app_f = - match kind_of_term fj.uj_val with + match EConstr.kind !evdref (EConstr.of_constr fj.uj_val) with | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in let pb = Environ.lookup_projection p env.ExtraEnv.env in @@ -724,7 +747,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in let resty = whd_all env.ExtraEnv.env !evdref (EConstr.of_constr resj.uj_type) in - match kind_of_term resty with + let resty = EConstr.of_constr resty in + match EConstr.kind !evdref resty with | Prod (na,c1,c2) -> let tycon = Some c1 in let hj = pretype tycon env evdref lvar c in @@ -732,12 +756,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 (EConstr.of_constr (j_val hj)) (EConstr.of_constr arg) then + if e_conv env.ExtraEnv.env evdref (j_val hj) arg then args, nf_evar !evdref (j_val hj) else [], j_val hj in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = value; uj_type = typ } in + let j = { uj_val = EConstr.Unsafe.to_constr value; uj_type = EConstr.Unsafe.to_constr typ } in apply_rec env (n+1) j candargs rest | _ -> @@ -748,16 +772,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let resj = apply_rec env 1 fj candargs args in let resj = - match evar_kind_of_term !evdref resj.uj_val with + match EConstr.kind !evdref (EConstr.of_constr resj.uj_val) with | App (f,args) -> - let f = whd_evar !evdref f in - if is_template_polymorphic env.ExtraEnv.env !evdref (EConstr.of_constr f) then + if is_template_polymorphic env.ExtraEnv.env !evdref f then (* Special case for inductive type applications that must be refreshed right away. *) - let sigma = !evdref in - let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref (EConstr.of_constr c) in - let t = Retyping.get_type_of env.ExtraEnv.env !evdref (EConstr.of_constr c) in + let c = mkApp (f, args) in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in + let c = EConstr.of_constr c in + let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in + let t = EConstr.of_constr t in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj @@ -770,8 +794,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd (EConstr.of_constr ty) in - evd, Some (EConstr.Unsafe.to_constr ty')) + let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in + evd, Some ty') evdref tycon in let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in @@ -794,7 +818,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j' = match name with | Anonymous -> let j = pretype_type empty_valcon env evdref lvar c2 in - { j with utj_val = lift 1 j.utj_val } + { j with utj_val = EConstr.Unsafe.to_constr (lift 1 (EConstr.of_constr j.utj_val)) } | Name _ -> let var = LocalAssum (name, j.utj_val) in let env' = push_rel var env in @@ -825,11 +849,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre the substitution must also be applied on variables before they are looked up in the rel context. *) let var = LocalDef (name, j.uj_val, t) in + let t = EConstr.of_constr t in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in - { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; - uj_type = subst1 j.uj_val j'.uj_type } + { uj_val = EConstr.Unsafe.to_constr (mkLetIn (name, EConstr.of_constr j.uj_val, t, EConstr.of_constr j'.uj_val)) ; + uj_type = EConstr.Unsafe.to_constr (subst1 (EConstr.of_constr j.uj_val) (EConstr.of_constr j'.uj_type)) } | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in @@ -839,6 +864,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 realargs = List.map EConstr.of_constr realargs 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" ++ @@ -855,8 +881,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let rec aux n k names l = match names, l with | na :: names, (LocalAssum (_,t) :: l) -> + let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in - LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) + local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, EConstr.of_constr cj.uj_val)), t) :: aux (n+1) (k + 1) names l | na :: names, (decl :: l) -> set_name na decl :: aux (n+1) k names l @@ -870,7 +897,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) + mkCase (ci, p, EConstr.of_constr cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in let env_f = push_rel_context fsign env in @@ -887,28 +914,28 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref pj.utj_val in + let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = - (Array.to_list cs.cs_concl_realargs) - @[build_dependent_constructor cs] in + (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) + @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env.ExtraEnv.env !evdref (EConstr.of_constr lp) (List.map EConstr.of_constr inst) in + let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p); - obj ind p cj.uj_val fj.uj_val + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p; + obj ind p cj.uj_val (EConstr.of_constr fj.uj_val) in - { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } + { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr (substl (realargs@[EConstr.of_constr cj.uj_val]) ccl) } | None -> let tycon = lift_tycon cs.cs_nargs tycon in let fj = pretype tycon env_f evdref lvar d in - let ccl = nf_evar !evdref fj.uj_type in + let ccl = nf_evar !evdref (EConstr.of_constr fj.uj_type) in let ccl = - if noccur_between 1 cs.cs_nargs ccl then + if noccur_between !evdref 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else error_cant_find_case_type ~loc env.ExtraEnv.env !evdref @@ -917,9 +944,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p); - obj ind p cj.uj_val fj.uj_val - in { uj_val = v; uj_type = ccl }) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p; + obj ind p cj.uj_val (EConstr.of_constr fj.uj_val) + in { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr ccl }) | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in @@ -946,16 +973,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref pj.utj_val in + let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (beta_applist !evdref (EConstr.of_constr pred,[EConstr.of_constr cj.uj_val])) in + let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[EConstr.of_constr cj.uj_val]))) in pred, typ | None -> let p = match tycon with | Some ty -> ty | None -> let env = ltac_interp_name_env k0 lvar env in - new_type_evar env evdref loc + EConstr.of_constr (new_type_evar env evdref loc) in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in @@ -963,7 +990,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let f cs b = let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) - let pi = beta_applist !evdref (EConstr.of_constr pi, [EConstr.of_constr (build_dependent_constructor cs)]) in + let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let csgn = if not !allow_anonymous_refs then List.map (set_name Anonymous) cs.cs_args @@ -974,17 +1001,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let env_c = push_rel_context csgn env in let bj = pretype (mk_tycon (EConstr.of_constr pi)) env_c evdref lvar b in - it_mkLambda_or_LetIn bj.uj_val cs.cs_args in + it_mkLambda_or_LetIn (EConstr.of_constr bj.uj_val) cs.cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr pred); - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) pred; + mkCase (ci, pred, EConstr.of_constr cj.uj_val, [|b1;b2|]) in - let cj = { uj_val = v; uj_type = p } in + let cj = { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr p } in inh_conv_coerce_to_tycon loc env evdref cj tycon | GCases (loc,sty,po,tml,eqns) -> @@ -1004,53 +1031,56 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let tval = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref (EConstr.of_constr tj.utj_val) in + let tval = EConstr.of_constr tval in let tval = nf_evar !evdref tval in let cj, tval = match k with | VMcast -> 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 (EConstr.of_constr cty) || occur_existential !evdref (EConstr.of_constr tval)) then + let cty = nf_evar !evdref (EConstr.of_constr 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 - error_actual_type ~loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,EConstr.of_constr cty,EConstr.of_constr tval)) + error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) + (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err ~loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> 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 + let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref (EConstr.of_constr cty) (EConstr.of_constr tval) in + let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj tval - (ConversionFailed (env.ExtraEnv.env,EConstr.of_constr cty,EConstr.of_constr tval)) + error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) + (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> - pretype (mk_tycon (EConstr.of_constr tval)) env evdref lvar c, tval + pretype (mk_tycon tval) env evdref lvar c, tval in - let v = mkCast (cj.uj_val, k, tval) in - { uj_val = v; uj_type = tval } + let v = mkCast (EConstr.of_constr cj.uj_val, k, tval) in + { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon 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 (NamedDecl.get_type decl) in + let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in let c, update = try let c = List.assoc id update in - let c = pretype k0 resolve_tc (mk_tycon (EConstr.of_constr t)) env evdref lvar c in - c.uj_val, List.remove_assoc id update + let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in + EConstr.of_constr c.uj_val, List.remove_assoc id update with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env.ExtraEnv.env !evdref (EConstr.of_constr t) (EConstr.of_constr t') then mkRel n, update else raise Not_found + let t' = EConstr.of_constr t' in + if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in - if is_conv env.ExtraEnv.env !evdref (EConstr.of_constr t) (EConstr.of_constr t') then mkVar id, update else raise Not_found + let t' = EConstr.of_constr t' in + if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err ~loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ @@ -1063,18 +1093,23 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> + let rec is_Type c = match EConstr.kind !evdref c with + | Sort (Type _) -> true + | Cast (c, _, _) -> is_Type c + | _ -> false + in (match valcon with | Some v -> let s = let sigma = !evdref in - let t = Retyping.get_type_of env.ExtraEnv.env sigma (EConstr.of_constr v) in + let t = Retyping.get_type_of env.ExtraEnv.env sigma v in match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t))) with | Sort s -> s - | Evar ev when is_Type (existential_type sigma (fst ev, Array.map EConstr.Unsafe.to_constr (snd ev))) -> + | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in - { utj_val = v; + { utj_val = EConstr.Unsafe.to_constr v; utj_type = s } | None -> let env = ltac_interp_name_env k0 lvar env in @@ -1088,10 +1123,10 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function match valcon with | None -> tj | Some v -> - if e_cumul env.ExtraEnv.env evdref (EConstr.of_constr v) (EConstr.of_constr tj.utj_val) then tj + if e_cumul env.ExtraEnv.env evdref v (EConstr.of_constr tj.utj_val) then tj else error_unexpected_type - ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val (EConstr.Unsafe.to_constr v) let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env in @@ -1101,11 +1136,11 @@ let ise_pretype_gen flags env sigma lvar kind c = | WithoutTypeConstraint -> (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val | OfType exptyp -> - (pretype k0 flags.use_typeclasses (mk_tycon (EConstr.of_constr exptyp)) env evdref lvar c).uj_val + (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,EConstr.of_constr c') let default_inference_flags fail = { use_typeclasses = true; @@ -1131,17 +1166,17 @@ let empty_lvar : ltac_var_map = { ltac_genargs = Id.Map.empty; } -let on_judgment f j = - let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in - let (c,_,t) = destCast (f c) in - {uj_val = c; uj_type = t} +let on_judgment sigma f j = + let c = mkCast(EConstr.of_constr j.uj_val,DEFAULTcast, EConstr.of_constr j.uj_type) in + let (c,_,t) = destCast sigma (f c) in + {uj_val = EConstr.Unsafe.to_constr c; uj_type = EConstr.Unsafe.to_constr t} let understand_judgment env sigma c = let env = make_env env in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in - let j = on_judgment (fun c -> + let j = on_judgment sigma (fun c -> let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in evdref := evd; c) j in j, Evd.evar_universe_context !evdref @@ -1150,14 +1185,14 @@ let understand_judgment_tcc env evdref c = let env = make_env env in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in - on_judgment (fun c -> + on_judgment !evdref (fun c -> let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in evdref := evd; c) j let ise_pretype_gen_ctx flags env sigma lvar kind c = let evd, c = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in - f c, Evd.evar_universe_context evd + f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd (** Entry points of the high-level type synthesis algorithm *) @@ -1168,15 +1203,17 @@ let understand ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = - ise_pretype_gen flags env sigma empty_lvar expected_type c + let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in + (sigma, EConstr.Unsafe.to_constr c) let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c = let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in evdref := sigma; - c + EConstr.Unsafe.to_constr c let understand_ltac flags env sigma lvar kind c = - ise_pretype_gen flags env sigma lvar kind c + let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in + (sigma, EConstr.Unsafe.to_constr c) let constr_flags = { use_typeclasses = true; -- cgit v1.2.3 From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 00:29:02 +0100 Subject: Making judgment type generic over the type of inner constrs. This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. --- pretyping/pretyping.ml | 157 ++++++++++++++++++++++++------------------------- 1 file changed, 78 insertions(+), 79 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cac31a1c57..49a0bccee9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -34,6 +34,7 @@ open Reductionops open Environ open Type_errors open Typeops +open Typing open Globnames open Nameops open Evarutil @@ -124,7 +125,7 @@ let e_new_evar env evdref ?src ?naming typ = let sigma = Sigma.Unsafe.of_evar_map !evdref in let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in evdref := Sigma.to_evar_map sigma; - e + EConstr.of_constr e let push_rec_types (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in @@ -425,21 +426,19 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c + try EConstr.of_constr (Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c) with Retyping.RetypeError _ -> user_err (str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++ str " in the current environment.") -let j_val j = EConstr.of_constr (j_val j) - let pretype_id pretype k0 loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in let typ = EConstr.of_constr typ in - { uj_val = EConstr.Unsafe.to_constr (mkRel n); uj_type = EConstr.Unsafe.to_constr (lift n typ) } + { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> let env = ltac_interp_name_env k0 lvar env in (* Check if [id] is an ltac variable *) @@ -447,7 +446,7 @@ let pretype_id pretype k0 loc env evdref lvar id = let (ids,c) = Id.Map.find id lvar.ltac_constrs in let subst = List.map (invert_ltac_bound_name lvar env id) ids in let c = substl subst (EConstr.of_constr c) in - { uj_val = EConstr.Unsafe.to_constr c; uj_type = protected_get_type_of env sigma c } + { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in let lvar = { @@ -472,7 +471,7 @@ let pretype_id pretype k0 loc env evdref lvar id = end; (* Check if [id] is a section or goal variable *) try - { uj_val = Constr.mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } + { uj_val = mkVar id; uj_type = EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found ~loc id @@ -511,9 +510,6 @@ let pretype_global loc rigid env evd gr us = let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in (sigma, EConstr.of_constr c) -let make_judge c t = - make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) - let pretype_ref loc evdref env ref us = match ref with | VarRef id -> @@ -527,14 +523,14 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in + let ty = unsafe_type_of env.ExtraEnv.env evd c in let ty = EConstr.of_constr ty in make_judge c ty let judge_of_Type loc evd s = let evd, s = interp_universe ~loc evd s in let judge = - { uj_val = Constr.mkSort (Type s); uj_type = Constr.mkSort (Type (Univ.super s)) } + { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } in evd, judge @@ -550,7 +546,7 @@ let new_type_evar env evdref loc = univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) in evdref := Sigma.to_evar_map sigma; - e + EConstr.of_constr e let (f_genarg_interp, genarg_interp_hook) = Hook.make () @@ -591,25 +587,25 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> EConstr.Unsafe.to_constr ty + | Some ty -> ty | None -> new_type_evar env evdref loc in let k = Evar_kinds.MatchingVar (someta,n) in - { uj_val = e_new_evar env evdref ~src:(loc,k) (EConstr.of_constr ty); uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (loc, k, naming, None) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> EConstr.Unsafe.to_constr ty + | Some ty -> ty | None -> new_type_evar env evdref loc in - { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming (EConstr.of_constr ty); uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } | GHole (loc, k, _naming, Some arg) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> EConstr.Unsafe.to_constr ty + | Some ty -> ty | None -> new_type_evar env evdref loc in let ist = lvar.ltac_genargs in @@ -622,14 +618,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre [] -> ctxt | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let dcl = LocalAssum (na, ty'.utj_val) in - let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in + let dcl = local_assum (na, ty'.utj_val) in + let dcl' = local_assum (ltac_interp_name lvar na,ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let bd' = pretype (mk_tycon (EConstr.of_constr ty'.utj_val)) env evdref lvar bd in - let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in - let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in + let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in + let dcl = local_def (na, bd'.uj_val, ty'.utj_val) in + let dcl' = local_def (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = @@ -637,8 +633,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (fun e ar -> pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) ctxtv lar in - let lara = Array.map (fun a -> EConstr.of_constr a.utj_val) larj in - let ftys = Array.map2 (fun e a -> EConstr.it_mkProd_or_LetIn a e) ctxtv lara in + let lara = Array.map (fun a -> a.utj_val) larj in + 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 _ = @@ -662,8 +658,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (lift nbfix ftys.(i)) in let nenv = push_rel_context ctxt newenv in let j = pretype (mk_tycon ty) nenv evdref lvar def in - { uj_val = Termops.it_mkLambda_or_LetIn j.uj_val ctxt; - uj_type = Termops.it_mkProd_or_LetIn j.uj_type ctxt }) + { 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; let nf c = nf_evar !evdref c in @@ -714,11 +710,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* Bidirectional typechecking hint: parameters of a constructor are completely determined by a typing constraint *) - if Flags.is_program_mode () && length > 0 && isConstruct !evdref (EConstr.of_constr fj.uj_val) then + if Flags.is_program_mode () && length > 0 && isConstruct !evdref fj.uj_val then match tycon with | None -> [] | Some ty -> - let ((ind, i), u) = destConstruct !evdref (EConstr.of_constr fj.uj_val) in + let ((ind, i), u) = destConstruct !evdref fj.uj_val in let npars = inductive_nparams ind in if Int.equal npars 0 then [] else @@ -731,7 +727,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else [] in let app_f = - match EConstr.kind !evdref (EConstr.of_constr fj.uj_val) with + match EConstr.kind !evdref fj.uj_val with | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in let pb = Environ.lookup_projection p env.ExtraEnv.env in @@ -746,7 +742,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | c::rest -> let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in - let resty = whd_all env.ExtraEnv.env !evdref (EConstr.of_constr resj.uj_type) in + let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in let resty = EConstr.of_constr resty in match EConstr.kind !evdref resty with | Prod (na,c1,c2) -> @@ -761,18 +757,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else [], j_val hj in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = EConstr.Unsafe.to_constr value; uj_type = EConstr.Unsafe.to_constr typ } in + let j = { uj_val = value; uj_type = typ } in apply_rec env (n+1) j candargs rest | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional ~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref - resj [hj] + resj [|hj|] in let resj = apply_rec env 1 fj candargs args in let resj = - match EConstr.kind !evdref (EConstr.of_constr resj.uj_val) with + match EConstr.kind !evdref resj.uj_val with | App (f,args) -> if is_template_polymorphic env.ExtraEnv.env !evdref f then (* Special case for inductive type applications that must be @@ -804,7 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = LocalAssum (name, j.utj_val) in + let var = local_assum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in @@ -818,9 +814,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j' = match name with | Anonymous -> let j = pretype_type empty_valcon env evdref lvar c2 in - { j with utj_val = EConstr.Unsafe.to_constr (lift 1 (EConstr.of_constr j.utj_val)) } + { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = LocalAssum (name, j.utj_val) in + let var = local_assum (name, j.utj_val) in let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in @@ -839,27 +835,27 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match c1 with | GCast (loc, c, CastConv t) -> let tj = pretype_type empty_valcon env evdref lvar t in - pretype (mk_tycon (EConstr.of_constr tj.utj_val)) env evdref lvar c + pretype (mk_tycon tj.utj_val) env evdref lvar c | _ -> pretype empty_tycon env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) - evdref (EConstr.of_constr j.uj_type) in + evdref j.uj_type in + let t = EConstr.of_constr t in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = LocalDef (name, j.uj_val, t) in - let t = EConstr.of_constr t in + let var = local_def (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in - { uj_val = EConstr.Unsafe.to_constr (mkLetIn (name, EConstr.of_constr j.uj_val, t, EConstr.of_constr j'.uj_val)) ; - uj_type = EConstr.Unsafe.to_constr (subst1 (EConstr.of_constr j.uj_val) (EConstr.of_constr j'.uj_type)) } + { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; + uj_type = subst1 j.uj_val j'.uj_type } | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type) + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj @@ -883,7 +879,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | na :: names, (LocalAssum (_,t) :: l) -> let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in - local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, EConstr.of_constr cj.uj_val)), t) + local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l | na :: names, (decl :: l) -> set_name na decl :: aux (n+1) k names l @@ -897,7 +893,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in - mkCase (ci, p, EConstr.of_constr cj.uj_val,[|f|]) + mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in let env_f = push_rel_context fsign env in @@ -914,7 +910,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in + let ccl = nf_evar !evdref pj.utj_val in let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = @@ -922,18 +918,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in - let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in + let fty = EConstr.of_constr fty in + let fj = pretype (mk_tycon fty) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p; - obj ind p cj.uj_val (EConstr.of_constr fj.uj_val) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + obj ind p cj.uj_val fj.uj_val in - { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr (substl (realargs@[EConstr.of_constr cj.uj_val]) ccl) } + { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) } | None -> let tycon = lift_tycon cs.cs_nargs tycon in let fj = pretype tycon env_f evdref lvar d in - let ccl = nf_evar !evdref (EConstr.of_constr fj.uj_type) in + let ccl = nf_evar !evdref fj.uj_type in let ccl = if noccur_between !evdref 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl @@ -944,14 +941,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p; - obj ind p cj.uj_val (EConstr.of_constr fj.uj_val) - in { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr ccl }) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + obj ind p cj.uj_val fj.uj_val + in { uj_val = v; uj_type = ccl }) | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type) + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in @@ -973,16 +970,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in + let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[EConstr.of_constr cj.uj_val]))) in + let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[cj.uj_val]))) in pred, typ | None -> let p = match tycon with | Some ty -> ty | None -> let env = ltac_interp_name_env k0 lvar env in - EConstr.of_constr (new_type_evar env evdref loc) + new_type_evar env evdref loc in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in @@ -991,6 +988,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let n = Context.Rel.length cs.cs_args in 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 pi = EConstr.of_constr pi in let csgn = if not !allow_anonymous_refs then List.map (set_name Anonymous) cs.cs_args @@ -1000,18 +998,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre cs.cs_args in let env_c = push_rel_context csgn env in - let bj = pretype (mk_tycon (EConstr.of_constr pi)) env_c evdref lvar b in - it_mkLambda_or_LetIn (EConstr.of_constr bj.uj_val) cs.cs_args in + let bj = pretype (mk_tycon pi) env_c evdref lvar b in + it_mkLambda_or_LetIn bj.uj_val cs.cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) pred; - mkCase (ci, pred, EConstr.of_constr cj.uj_val, [|b1;b2|]) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; + mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in - let cj = { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr p } in + let cj = { uj_val = v; uj_type = p } in inh_conv_coerce_to_tycon loc env evdref cj tycon | GCases (loc,sty,po,tml,eqns) -> @@ -1030,36 +1028,36 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let tj = pretype_type empty_valcon env evdref lvar t in let tval = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) - evdref (EConstr.of_constr tj.utj_val) in + evdref tj.utj_val in let tval = EConstr.of_constr tval in let tval = nf_evar !evdref tval in let cj, tval = match k with | VMcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval 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 - error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) + 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: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval 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 - error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) + error_actual_type ~loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> pretype (mk_tycon tval) env evdref lvar c, tval in - let v = mkCast (EConstr.of_constr cj.uj_val, k, tval) in - { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr tval } + let v = mkCast (cj.uj_val, k, tval) in + { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = @@ -1070,7 +1068,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = try let c = List.assoc id update in let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in - EConstr.of_constr c.uj_val, List.remove_assoc id update + c.uj_val, List.remove_assoc id update with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in @@ -1103,13 +1101,14 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let s = let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in - match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t))) with + let t = EConstr.of_constr t in + match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma t)) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in - { utj_val = EConstr.Unsafe.to_constr v; + { utj_val = v; utj_type = s } | None -> let env = ltac_interp_name_env k0 lvar env in @@ -1123,10 +1122,10 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function match valcon with | None -> tj | Some v -> - if e_cumul env.ExtraEnv.env evdref v (EConstr.of_constr tj.utj_val) then tj + if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else error_unexpected_type - ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val (EConstr.Unsafe.to_constr v) + ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env in @@ -1140,7 +1139,7 @@ let ise_pretype_gen flags env sigma lvar kind c = | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,EConstr.of_constr c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') let default_inference_flags fail = { use_typeclasses = true; @@ -1167,9 +1166,9 @@ let empty_lvar : ltac_var_map = { } let on_judgment sigma f j = - let c = mkCast(EConstr.of_constr j.uj_val,DEFAULTcast, EConstr.of_constr j.uj_type) in + let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in let (c,_,t) = destCast sigma (f c) in - {uj_val = EConstr.Unsafe.to_constr c; uj_type = EConstr.Unsafe.to_constr t} + {uj_val = c; uj_type = t} let understand_judgment env sigma c = let env = make_env env in -- cgit v1.2.3 From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- pretyping/pretyping.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 49a0bccee9..7586b54ba1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -116,7 +116,7 @@ let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in - let inst_vars = List.map (get_id %> Constr.mkVar) (named_context env.env) in + let inst_vars = List.map (get_id %> EConstr.mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in let (subst, vsubst, _, nc) = Lazy.force env.extra in let typ' = subst2 subst vsubst typ in @@ -125,7 +125,7 @@ let e_new_evar env evdref ?src ?naming typ = let sigma = Sigma.Unsafe.of_evar_map !evdref in let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in evdref := Sigma.to_evar_map sigma; - EConstr.of_constr e + e let push_rec_types (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in @@ -546,7 +546,7 @@ let new_type_evar env evdref loc = univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) in evdref := Sigma.to_evar_map sigma; - EConstr.of_constr e + e let (f_genarg_interp, genarg_interp_hook) = Hook.make () -- cgit v1.2.3 From 7b43de20a4acd7c9da290f038d9a16fe67eccd59 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Nov 2016 01:59:07 +0100 Subject: Leminv API using EConstr. --- pretyping/pretyping.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7586b54ba1..11d50926f4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -860,7 +860,6 @@ 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 realargs = List.map EConstr.of_constr realargs 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" ++ -- cgit v1.2.3 From e6a8ab0f428c26fff2bd7e636126974f167101bf Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 01:35:54 +0100 Subject: Tactic_matching API using EConstr. --- pretyping/pretyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 11d50926f4..c792bf2ca9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -445,7 +445,7 @@ let pretype_id pretype k0 loc env evdref lvar id = try let (ids,c) = Id.Map.find id lvar.ltac_constrs in let subst = List.map (invert_ltac_bound_name lvar env id) ids in - let c = substl subst (EConstr.of_constr c) in + let c = substl subst c in { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in -- cgit v1.2.3 From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- pretyping/pretyping.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c792bf2ca9..f814028f98 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -971,7 +971,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[cj.uj_val]))) in + let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in pred, typ | None -> let p = match tycon with @@ -987,7 +987,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let n = Context.Rel.length cs.cs_args in 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 pi = EConstr.of_constr pi in let csgn = if not !allow_anonymous_refs then List.map (set_name Anonymous) cs.cs_args -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- pretyping/pretyping.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f814028f98..7d2c96bb90 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -743,7 +743,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in - let resty = EConstr.of_constr resty in match EConstr.kind !evdref resty with | Prod (na,c1,c2) -> let tycon = Some c1 in @@ -917,7 +916,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in - let fty = EConstr.of_constr fty in let fj = pretype (mk_tycon fty) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in @@ -1100,7 +1098,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in let t = EConstr.of_constr t in - match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma t)) with + match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev -- cgit v1.2.3 From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 17:15:15 +0100 Subject: Removing compatibility layers in Retyping --- pretyping/pretyping.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7d2c96bb90..a0d8faab44 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -426,7 +426,7 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try EConstr.of_constr (Retyping.get_type_of ~lax:true env.ExtraEnv.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 (EConstr.Unsafe.to_constr c)) ++ @@ -774,9 +774,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre refreshed right away. *) let c = mkApp (f, args) in let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in - let c = EConstr.of_constr c in let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in - let t = EConstr.of_constr t in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj @@ -840,7 +838,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in - let t = EConstr.of_constr t in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) @@ -1025,7 +1022,6 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let tval = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref tj.utj_val in - let tval = EConstr.of_constr tval in let tval = nf_evar !evdref tval in let cj, tval = match k with | VMcast -> @@ -1097,7 +1093,6 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let s = let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in - let t = EConstr.of_constr t in match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> -- cgit v1.2.3 From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 18:18:17 +0100 Subject: Ltac now uses evar-based constrs. --- pretyping/pretyping.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a0d8faab44..09b99983cc 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -429,7 +429,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 (EConstr.Unsafe.to_constr c)) ++ + (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") let pretype_id pretype k0 loc env evdref lvar id = @@ -1225,6 +1225,7 @@ let type_uconstr ?(flags = constr_flags) } in let sigma = Sigma.to_evar_map sigma in let (sigma, c) = understand_ltac flags env sigma vars expected_type term in + let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) end } -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- pretyping/pretyping.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 09b99983cc..f76f608d0d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -524,7 +524,6 @@ let pretype_ref loc evdref env ref us = let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in let ty = unsafe_type_of env.ExtraEnv.env evd c in - let ty = EConstr.of_constr ty in make_judge c ty let judge_of_Type loc evd s = @@ -1194,16 +1193,16 @@ let understand let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in - (sigma, EConstr.Unsafe.to_constr c) + (sigma, c) let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=WithoutTypeConstraint) c = let sigma, c = ise_pretype_gen flags env !evdref empty_lvar expected_type c in evdref := sigma; - EConstr.Unsafe.to_constr c + c let understand_ltac flags env sigma lvar kind c = let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in - (sigma, EConstr.Unsafe.to_constr c) + (sigma, c) let constr_flags = { use_typeclasses = true; @@ -1225,7 +1224,6 @@ let type_uconstr ?(flags = constr_flags) } in let sigma = Sigma.to_evar_map sigma in let (sigma, c) = understand_ltac flags env sigma vars expected_type term in - let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) end } -- cgit v1.2.3 From 8beca748d992cd08e2dd7448c8b28dadbcea4a16 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 01:09:11 +0100 Subject: Cleaning up interfaces. We make mli files look to what they were looking before the move to EConstr by opening this module. --- pretyping/pretyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f76f608d0d..6b6800ac6a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -61,7 +61,7 @@ type ltac_var_map = { ltac_genargs : unbound_ltac_var_map; } type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * Constr.constr +type pure_open_constr = evar_map * EConstr.constr (************************************************************************) (* This concerns Cases *) -- cgit v1.2.3 From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 02:12:40 +0100 Subject: Evar-normalizing functions now act on EConstrs. --- pretyping/pretyping.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6b6800ac6a..4660978df3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -143,9 +143,6 @@ let nf_fix sigma (nas, cs, ts) = let inj c = EConstr.to_constr sigma c in (nas, Array.map inj cs, Array.map inj ts) -let nf_evar sigma c = - EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c)) - let search_guard loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- pretyping/pretyping.ml | 52 +++++++++++++++++++++----------------------------- 1 file changed, 22 insertions(+), 30 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4660978df3..2470decdda 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,10 +28,10 @@ open Names open Evd open Term open Termops +open Environ open EConstr open Vars open Reductionops -open Environ open Type_errors open Typeops open Typing @@ -70,16 +70,6 @@ open Inductiveops (************************************************************************) -let local_assum (na, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalAssum (na, inj t) - -let local_def (na, b, t) = - let open Context.Rel.Declaration in - let inj = EConstr.Unsafe.to_constr in - LocalDef (na, inj b, inj t) - module ExtraEnv = struct @@ -94,7 +84,7 @@ let get_extra env = let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in Context.Rel.fold_outside push_rel_decl_to_named_context - (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) let make_env env = { env = env; extra = lazy (get_extra env) } let rel_context env = rel_context env.env @@ -116,7 +106,7 @@ let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in - let inst_vars = List.map (get_id %> EConstr.mkVar) (named_context env.env) in + let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in let (subst, vsubst, _, nc) = Lazy.force env.extra in let typ' = subst2 subst vsubst typ in @@ -128,7 +118,7 @@ let e_new_evar env evdref ?src ?naming typ = e let push_rec_types (lna,typarray,_) env = - let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt end @@ -434,7 +424,6 @@ let pretype_id pretype k0 loc env evdref lvar id = (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in - let typ = EConstr.of_constr typ in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> let env = ltac_interp_name_env k0 lvar env in @@ -468,7 +457,7 @@ let pretype_id pretype k0 loc env evdref lvar id = end; (* Check if [id] is a section or goal variable *) try - { uj_val = mkVar id; uj_type = EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) } + { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found ~loc id @@ -511,7 +500,7 @@ let pretype_ref loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try make_judge (mkVar id) (EConstr.of_constr (NamedDecl.get_type (lookup_named id env))) + (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env)) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -614,14 +603,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre [] -> ctxt | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let dcl = local_assum (na, ty'.utj_val) in - let dcl' = local_assum (ltac_interp_name lvar na,ty'.utj_val) in + let dcl = LocalAssum (na, ty'.utj_val) in + let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in - let dcl = local_def (na, bd'.uj_val, ty'.utj_val) in - let dcl' = local_def (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in + let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in + let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = @@ -793,7 +782,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = local_assum (name, j.utj_val) in + let var = LocalAssum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in @@ -809,7 +798,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_type empty_valcon env evdref lvar c2 in { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = local_assum (name, j.utj_val) in + let var = LocalAssum (name, j.utj_val) in let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in @@ -837,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = local_def (name, j.uj_val, t) in + let var = LocalDef (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in @@ -861,6 +850,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre user_err ~loc:loc (str "Destructing let on this type expects " ++ 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 | None -> List.map2 set_name (List.rev nal) cs.cs_args, false @@ -870,7 +860,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | na :: names, (LocalAssum (_,t) :: l) -> let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in - local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) + LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l | na :: names, (decl :: l) -> set_name na decl :: aux (n+1) k names l @@ -896,6 +886,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else arsgn in let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in + let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let nar = List.length arsgn in (match po with | Some p -> @@ -903,6 +894,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) + let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) @@ -956,6 +948,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let nar = List.length arsgn in let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in + let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let pred,p = match po with | Some p -> let env_p = push_rel_context psign env in @@ -978,17 +971,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let n = Context.Rel.length cs.cs_args in 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 csgn = if not !allow_anonymous_refs then - List.map (set_name Anonymous) cs.cs_args + List.map (set_name Anonymous) cs_args else List.map (map_name (function Name _ as n -> n | Anonymous -> Name Namegen.default_non_dependent_ident)) - cs.cs_args + cs_args in let env_c = push_rel_context csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in - it_mkLambda_or_LetIn bj.uj_val cs.cs_args in + it_mkLambda_or_LetIn bj.uj_val cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = @@ -1060,12 +1054,10 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - let t' = EConstr.of_constr t' in if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try let t' = env |> lookup_named id |> NamedDecl.get_type in - let t' = EConstr.of_constr t' in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err ~loc (str "Cannot interpret " ++ -- cgit v1.2.3 From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: Namegen primitives now apply on evar constrs. Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. --- pretyping/pretyping.ml | 75 +++++++++++++++++++++++++------------------------- 1 file changed, 37 insertions(+), 38 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2470decdda..563769df54 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -79,26 +79,26 @@ type t = { (** Delay the computation of the evar extended environment *) } -let get_extra env = +let get_extra env sigma = let open Context.Named.Declaration in let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in - Context.Rel.fold_outside push_rel_decl_to_named_context + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) -let make_env env = { env = env; extra = lazy (get_extra env) } +let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) } let rel_context env = rel_context env.env -let push_rel d env = { +let push_rel sigma d env = { env = push_rel d env.env; - extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra)); + extra = lazy (push_rel_decl_to_named_context sigma d (Lazy.force env.extra)); } -let pop_rel_context n env = make_env (pop_rel_context n env.env) +let pop_rel_context n env sigma = make_env (pop_rel_context n env.env) sigma -let push_rel_context ctx env = { +let push_rel_context sigma ctx env = { env = push_rel_context ctx env.env; - extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra)); + extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx (Lazy.force env.extra)); } let lookup_named id env = lookup_named id env.env @@ -117,9 +117,9 @@ let e_new_evar env evdref ?src ?naming typ = evdref := Sigma.to_evar_map sigma; e -let push_rec_types (lna,typarray,_) env = +let push_rec_types sigma (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in - Array.fold_left (fun e assum -> push_rel assum e) env ctxt + Array.fold_left (fun e assum -> push_rel sigma assum e) env ctxt end @@ -391,7 +391,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function str"It cannot be used in a binder.") else n -let ltac_interp_name_env k0 lvar env = +let ltac_interp_name_env k0 lvar env sigma = (* envhd is the initial part of the env when pretype was called first *) (* (in practice is is probably 0, but we have to grant the specification of pretype which accepts to start with a non empty @@ -402,7 +402,7 @@ let ltac_interp_name_env k0 lvar env = let open Context.Rel.Declaration in let ctxt' = List.smartmap (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 ctxt' (pop_rel_context n env) + else push_rel_context sigma ctxt' (pop_rel_context n env sigma) let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in @@ -426,7 +426,7 @@ let pretype_id pretype k0 loc env evdref lvar id = let (n,_,typ) = lookup_rel_id id (rel_context env) in { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in (* Check if [id] is an ltac variable *) try let (ids,c) = Id.Map.find id lvar.ltac_constrs in @@ -569,7 +569,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty @@ -578,7 +578,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (loc, k, naming, None) -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty @@ -587,7 +587,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } | GHole (loc, k, _naming, Some arg) -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty @@ -605,18 +605,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let ty' = pretype_type empty_valcon env evdref lvar ty in let dcl = LocalAssum (na, ty'.utj_val) in let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in - type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl + type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in - type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in + type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = Array.map2 (fun e ar -> - pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) + pretype_type empty_valcon (push_rel_context !evdref e env) evdref lvar ar) ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in @@ -632,7 +632,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let newenv = push_rec_types (names,ftys,[||]) env in + let newenv = push_rec_types !evdref (names,ftys,[||]) env in let vdefj = Array.map2_i (fun i ctxt def -> @@ -641,7 +641,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (ctxt,ty) = decompose_prod_n_assum !evdref (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in - let nenv = push_rel_context ctxt newenv in + let nenv = push_rel_context !evdref ctxt newenv in let j = pretype (mk_tycon ty) nenv evdref lvar def in { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) @@ -783,7 +783,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre the substitution must also be applied on variables before they are looked up in the rel context. *) let var = LocalAssum (name, j.utj_val) in - let j' = pretype rng (push_rel var env) evdref lvar c2 in + let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon @@ -799,7 +799,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { j with utj_val = lift 1 j.utj_val } | Name _ -> let var = LocalAssum (name, j.utj_val) in - let env' = push_rel var env in + let env' = push_rel !evdref var env in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in @@ -828,7 +828,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre looked up in the rel context. *) let var = LocalDef (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in - let j' = pretype tycon (push_rel var env) evdref lvar c2 in + let j' = pretype tycon (push_rel !evdref var env) evdref lvar c2 in let name = ltac_interp_name lvar name in { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } @@ -877,7 +877,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in - let env_f = push_rel_context fsign env in + let env_f = push_rel_context !evdref fsign env in (* Make dependencies from arity signature impossible *) let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in @@ -890,11 +890,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let nar = List.length arsgn in (match po with | Some p -> - let env_p = push_rel_context psign env in + let env_p = push_rel_context !evdref psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) - let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in + let psign = make_arity_signature env.ExtraEnv.env !evdref true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.map_to_list EConstr.of_constr cs.cs_concl_realargs) @@ -951,7 +950,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let pred,p = match po with | Some p -> - let env_p = push_rel_context psign env in + let env_p = push_rel_context !evdref psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in @@ -961,7 +960,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let p = match tycon with | Some ty -> ty | None -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in new_type_evar env evdref loc in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in @@ -980,7 +979,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Anonymous -> Name Namegen.default_non_dependent_ident)) cs_args in - let env_c = push_rel_context csgn env in + let env_c = push_rel_context !evdref csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in it_mkLambda_or_LetIn bj.uj_val cs_args in let b1 = f cstrs.(0) b1 in @@ -997,7 +996,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty - ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref) + ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref) tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) | GCast (loc,c,k) -> @@ -1090,7 +1089,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function { utj_val = v; utj_type = s } | None -> - let env = ltac_interp_name_env k0 lvar env in + let env = ltac_interp_name_env k0 lvar env !evdref in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) @@ -1107,7 +1106,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = - let env = make_env env in + let env = make_env env sigma in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let c' = match kind with @@ -1150,7 +1149,7 @@ let on_judgment sigma f j = {uj_val = c; uj_type = t} let understand_judgment env sigma c = - let env = make_env env in + let env = make_env env sigma in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in @@ -1160,7 +1159,7 @@ let understand_judgment env sigma c = in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = - let env = make_env env in + let env = make_env env !evdref in let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment !evdref (fun c -> @@ -1217,7 +1216,7 @@ let type_uconstr ?(flags = constr_flags) end } let pretype k0 resolve_tc typcon env evdref lvar t = - pretype k0 resolve_tc typcon (make_env env) evdref lvar t + pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t let pretype_type k0 resolve_tc valcon env evdref lvar t = - pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t + pretype_type k0 resolve_tc valcon (make_env env !evdref) evdref lvar t -- cgit v1.2.3 From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 31 Mar 2017 23:20:25 +0200 Subject: Actually exporting delayed universes in the EConstr implementation. For now we only normalize sorts, and we leave instances for the next commit. --- pretyping/pretyping.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 846d8055aa..c673851c84 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1071,7 +1071,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> let rec is_Type c = match EConstr.kind !evdref c with - | Sort (Type _) -> true + | Sort s -> + begin match ESorts.kind !evdref s with + | Type _ -> true + | Prop _ -> false + end | Cast (c, _, _) -> is_Type c | _ -> false in @@ -1081,7 +1085,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with - | Sort s -> s + | Sort s -> ESorts.kind sigma s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") -- cgit v1.2.3