diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-04 14:48:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:23:49 +0100 |
| commit | d528fdaf12b74419c47698cca7c6f1ec762245a3 (patch) | |
| tree | 2edbaac4e19db595e0ec763de820cbc704897043 | |
| parent | 6bd193ff409b01948751525ce0f905916d7a64bd (diff) | |
Retyping API using EConstr.
41 files changed, 240 insertions, 229 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 2405e3c42..ca1f6e638 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -298,7 +298,7 @@ let project_hint pri l2r r = let env = Global.env() in let sigma = Evd.from_env env in let sigma, c = Evd.fresh_global env sigma gr in - let t = Retyping.get_type_of env sigma c in + let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in let t = Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in let sign,ccl = decompose_prod_assum t in @@ -655,7 +655,7 @@ let hResolve id c occ t = in let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in let sigma = Evd.merge_universe_context sigma ctx in - let t_constr_type = Retyping.get_type_of env sigma t_constr in + let t_constr_type = Retyping.get_type_of env sigma (EConstr.of_constr t_constr) in let tac = (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) in diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 7ef3ace53..80307ce8e 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -431,7 +431,7 @@ module TypeGlobal = struct end let sort_of_rel env evm rel = - Reductionops.sort_of_arity env evm (EConstr.of_constr (Retyping.get_type_of env evm rel)) + Reductionops.sort_of_arity env evm (EConstr.of_constr (Retyping.get_type_of env evm (EConstr.of_constr rel))) let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation @@ -499,20 +499,20 @@ let rec decompose_app_rel env evd t = let decompose_app_rel env evd t = let (rel, t1, t2) = decompose_app_rel env evd t in - let ty = Retyping.get_type_of env evd rel in + let ty = Retyping.get_type_of env evd (EConstr.of_constr rel) in let () = if not (Reduction.is_arity env ty) then error_no_relation () in (rel, t1, t2) let decompose_applied_relation env sigma (c,l) = let open Context.Rel.Declaration in - let ctype = Retyping.get_type_of env sigma c in + let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in let find_rel ty = let sigma, cl = Clenv.make_evar_clause env sigma ty in let sigma = Clenv.solve_evar_clause env sigma true cl l in let { Clenv.cl_holes = holes; Clenv.cl_concl = t } = cl in let (equiv, c1, c2) = decompose_app_rel env sigma t in - let ty1 = Retyping.get_type_of env sigma c1 in - let ty2 = Retyping.get_type_of env sigma c2 in + let ty1 = Retyping.get_type_of env sigma (EConstr.of_constr c1) in + let ty2 = Retyping.get_type_of env sigma (EConstr.of_constr c2) in match evd_convertible env sigma ty1 ty2 with | None -> None | Some sigma -> @@ -719,8 +719,8 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let c1 = nf c1 and c2 = nf c2 and rew_car = nf car and rel = nf rel and prf = nf prf in - let ty1 = Retyping.get_type_of env evd c1 in - let ty2 = Retyping.get_type_of env evd c2 in + let ty1 = Retyping.get_type_of env evd (EConstr.of_constr c1) in + let ty2 = Retyping.get_type_of env evd (EConstr.of_constr c2) in let () = if not (convertible env evd ty2 ty1) then raise Reduction.NotConvertible in let rew_evars = evd, cstrs in let rew_prf = RewPrf (rel, prf) in @@ -923,15 +923,15 @@ let reset_env env = let fold_match ?(force=false) env sigma c = let (ci, p, c, brs) = destCase c in - let cty = Retyping.get_type_of env sigma c in + let cty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let dep, pred, exists, (sk,eff) = let env', ctx, body = let ctx, pred = decompose_lam_assum p in let env' = Environ.push_rel_context ctx env in env', ctx, pred in - let sortp = Retyping.get_sort_family_of env' sigma body in - let sortc = Retyping.get_sort_family_of env sigma cty in + let sortp = Retyping.get_sort_family_of env' sigma (EConstr.of_constr body) in + let sortc = Retyping.get_sort_family_of env sigma (EConstr.of_constr cty) in let dep = not (noccurn 1 body) in let pred = if dep then p else it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx) @@ -985,7 +985,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = if not (Option.is_empty progress) && not all then state, (None :: acc, evars, progress) else - let argty = Retyping.get_type_of env (goalevars evars) arg in + let argty = Retyping.get_type_of env (goalevars evars) (EConstr.of_constr arg) in let state, res = s.strategy { state ; env ; unfresh ; term1 = arg ; ty1 = argty ; @@ -1033,7 +1033,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in state, res in if flags.on_morphisms then - let mty = Retyping.get_type_of env (goalevars evars) m in + let mty = Retyping.get_type_of env (goalevars evars) (EConstr.of_constr m) in let evars, cstr', m, mty, argsl, args = let argsl = Array.to_list args in let lift = if prop then PropGlobal.lift_cstr else TypeGlobal.lift_cstr in @@ -1075,8 +1075,8 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Prod (n, x, b) when noccurn 1 b -> let b = subst1 mkProp b in - let tx = Retyping.get_type_of env (goalevars evars) x - and tb = Retyping.get_type_of env (goalevars evars) b in + let tx = Retyping.get_type_of env (goalevars evars) (EConstr.of_constr x) + and tb = Retyping.get_type_of env (goalevars evars) (EConstr.of_constr b) in let arr = if prop then PropGlobal.arrow_morphism else TypeGlobal.arrow_morphism in @@ -1154,7 +1154,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in let open Context.Rel.Declaration in let env' = Environ.push_rel (LocalAssum (n', t)) env in - let bty = Retyping.get_type_of env' (goalevars evars) b in + let bty = Retyping.get_type_of env' (goalevars evars) (EConstr.of_constr b) in let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in let state, b' = s.strategy { state ; env = env' ; unfresh ; term1 = b ; ty1 = bty ; @@ -1181,7 +1181,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in state, res | Case (ci, p, c, brs) -> - let cty = Retyping.get_type_of env (goalevars evars) c in + let cty = Retyping.get_type_of env (goalevars evars) (EConstr.of_constr c) in let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in let cstr' = Some eqty in let state, c' = s.strategy { state ; env ; unfresh ; @@ -1457,7 +1457,7 @@ let rewrite_with l2r flags c occs : strategy = { strategy = } let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars = - let ty = Retyping.get_type_of env (goalevars evars) concl in + let ty = Retyping.get_type_of env (goalevars evars) (EConstr.of_constr concl) in let _, res = s.strategy { state = () ; env ; unfresh ; term1 = concl ; ty1 = ty ; cstr = (prop, Some cstr) ; evars } in @@ -1868,7 +1868,7 @@ let declare_projection n instance_id r = let env = Global.env () in let sigma = Evd.from_env env in let sigma,c = Evd.fresh_global env sigma r in - let ty = Retyping.get_type_of env sigma c in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let term = proper_projection c ty in let sigma, typ = Typing.type_of env sigma term in let ctx, typ = decompose_prod_assum typ in @@ -2060,7 +2060,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = and car = nf car and rel = nf rel in check_evar_map_of_evars_defs sigma; let prf = nf prf in - let prfty = nf (Retyping.get_type_of env sigma prf) in + let prfty = nf (Retyping.get_type_of env sigma (EConstr.of_constr prf)) in let sort = sort_of_rel env sigma but in let abs = prf, prfty in let prf = mkRel 1 in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6ca34036a..42a8cac69 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,11 +42,11 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + Retyping.get_type_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) let sort_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + Retyping.get_sort_family_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c))) (*S Generation of flags and signatures. *) @@ -595,7 +595,7 @@ let rec extract_term env mle mlt c args = | Construct (cp,_) -> extract_cons_app env mle mlt cp args | Proj (p, c) -> - let term = Retyping.expand_projection env (Evd.from_env env) p c [] in + let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in extract_term env mle mlt term args | Rel n -> (* As soon as the expected [mlt] for the head is known, *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 9fb1463db..a943ef2b0 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1199,7 +1199,7 @@ struct with e when CErrors.noncritical e -> (X(t),env,tg) in let is_prop term = - let sort = Retyping.get_sort_of (Tacmach.pf_env gl) (Tacmach.project gl) term in + let sort = Retyping.get_sort_of (Tacmach.pf_env gl) (Tacmach.project gl) (EConstr.of_constr term) in Term.is_prop_sort sort in let rec xparse_formula env tg term = diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index b129b0bb3..f88b3a700 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -94,9 +94,9 @@ let rec make_form atom_env gls term = let cciterm=special_whd gls term in match kind_of_term cciterm with Prod(_,a,b) -> - if EConstr.Vars.noccurn Evd.empty (** FIXME *) 1 (EConstr.of_constr b) && + if EConstr.Vars.noccurn (Tacmach.project gls) 1 (EConstr.of_constr b) && Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) a == InProp + (pf_env gls) (Tacmach.project gls) (EConstr.of_constr a) == InProp then let fa=make_form atom_env gls a in let fb=make_form atom_env gls b in @@ -136,7 +136,7 @@ let rec make_hyps atom_env gls lenv = function make_hyps atom_env gls (typ::lenv) rest in if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id (EConstr.of_constr c)) lenv || (Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) typ != InProp) + (pf_env gls) (Tacmach.project gls) (EConstr.of_constr typ) != InProp) then hrec else @@ -262,7 +262,7 @@ let rtauto_tac gls= let gl=pf_concl gls in let _= if Retyping.get_sort_family_of - (pf_env gls) (Tacmach.project gls) gl != InProp + (pf_env gls) (Tacmach.project gls) (EConstr.of_constr gl) != InProp then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in let glf=make_form gamma gls gl in let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index cf0f51911..e1b95ddbc 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -345,9 +345,9 @@ let ring_for_carrier r = Cmap.find r !from_carrier let find_ring_structure env sigma l = match l with | t::cl' -> - let ty = Retyping.get_type_of env sigma t in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr t) in let check c = - let ty' = Retyping.get_type_of env sigma c in + let ty' = Retyping.get_type_of env sigma (EConstr.of_constr c) in if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") @@ -540,7 +540,7 @@ let build_setoid_params env evd r add mul opp req eqth = | None -> ring_equality env evd (r,add,mul,opp,req) let dest_ring env sigma th_spec = - let th_typ = Retyping.get_type_of env sigma th_spec in + let th_typ = Retyping.get_type_of env sigma (EConstr.of_constr th_spec) in match kind_of_term th_typ with App(f,[|r;zero;one;add;mul;sub;opp;req|]) when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) -> @@ -571,7 +571,7 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])) let make_hyp env evd c = - let t = Retyping.get_type_of env !evd c in + let t = Retyping.get_type_of env !evd (EConstr.of_constr c) in plapp evd coq_mkhypo [|t;c|] let make_hyp_list env evd lH = @@ -796,7 +796,7 @@ let af_ar = my_reference"AF_AR" let f_r = my_reference"F_R" let sf_sr = my_reference"SF_SR" let dest_field env evd th_spec = - let th_typ = Retyping.get_type_of env !evd th_spec in + let th_typ = Retyping.get_type_of env !evd (EConstr.of_constr th_spec) in match kind_of_term th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) when is_global (Lazy.force afield_theory) f -> @@ -825,9 +825,9 @@ let find_field_structure env sigma l = check_required_library (cdir@["Field_tac"]); match l with | t::cl' -> - let ty = Retyping.get_type_of env sigma t in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr t) in let check c = - let ty' = Retyping.get_type_of env sigma c in + let ty' = Retyping.get_type_of env sigma (EConstr.of_constr c) in if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") diff --git a/pretyping/cases.ml b/pretyping/cases.ml index be72091a9..4dd502106 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1480,7 +1480,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = if not (Flags.is_program_mode ()) && (isRel orig || isVar orig) then (* Try to compile first using non expanded alias *) try - if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig) + if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) (EConstr.of_constr orig)) else just_pop () with e when precatchable_exception e -> (* Try then to compile using expanded alias *) @@ -1495,7 +1495,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = (* Could be needed in case of a recursive call which requires to be on a variable for size reasons *) pb.evdref := sigma; - if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig) + if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) (EConstr.of_constr orig)) else just_pop () @@ -1627,7 +1627,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = let t = whd_evar !evdref t in match kind_of_term t with | Rel n when is_local_def (lookup_rel n env) -> t | Evar ev -> - let ty = get_type_of env !evdref t in + let ty = get_type_of env !evdref (EConstr.of_constr t) in let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let inst = List.map_i @@ -1649,7 +1649,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = | (_, _, u) :: _ -> (* u is in extenv *) let vl = List.map pi1 good in let ty = - let ty = get_type_of env !evdref t in + let ty = get_type_of env !evdref (EConstr.of_constr t) in Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let ty = lift (-k) (aux x ty) in @@ -1798,7 +1798,7 @@ let build_inversion_problem loc env sigma tms t = it = None } } ] in (* [pb] is the auxiliary pattern-matching serving as skeleton for the return type of the original problem Xi *) - let s' = Retyping.get_sort_of env sigma t in + let s' = Retyping.get_sort_of env sigma (EConstr.of_constr t) in let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in let sigma = Evd.set_leq_sort env sigma s' s in let evdref = ref sigma in @@ -2067,7 +2067,7 @@ let constr_of_pat env evdref arsign pat avoid = let cstr = mkConstructU ci.cs_cstr in let app = applistc cstr (List.map (lift (List.length sign)) params) in let app = applistc app args in - let apptype = Retyping.get_type_of env ( !evdref) app in + let apptype = Retyping.get_type_of env ( !evdref) (EConstr.of_constr app) in let IndType (indf, realargs) = find_rectype env (!evdref) (EConstr.of_constr apptype) in match alias with Anonymous -> @@ -2325,7 +2325,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign = (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl -> let name = RelDecl.get_name decl in let t = RelDecl.get_type decl in - let argt = Retyping.get_type_of env !evdref arg in + let argt = Retyping.get_type_of env !evdref (EConstr.of_constr arg) in let eq, refl_arg = if Reductionops.is_conv env !evdref (EConstr.of_constr argt) (EConstr.of_constr t) then (mk_eq evdref (lift (nargeqs + slift) argt) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index fd21f5bd1..577f41a7d 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -441,7 +441,7 @@ let cache_coercion (_, c) = let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty value in + let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in let xf = { coe_value = value; coe_type = typ; diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index b062da1f4..6a7f90463 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -65,7 +65,7 @@ let apply_coercion_args env evd check isproj argl funj = | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) match kind_of_term (whd_all env evd (EConstr.of_constr typ)) with | Prod (_,c1,c2) -> - if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then + if check && not (e_cumul env evdref (Retyping.get_type_of env evd (EConstr.of_constr h)) c1) then raise NoCoercion; apply_rec (h::acc) (subst1 h c2) restl | _ -> anomaly (Pp.str "apply_coercion_args") @@ -488,7 +488,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = let v2 = Option.map (fun v -> beta_applist evd' (EConstr.of_constr (lift 1 v),[EConstr.of_constr v1])) v in let t2 = match v2 with | None -> subst_term evd' (EConstr.of_constr v1) (EConstr.of_constr t2) - | Some v2 -> Retyping.get_type_of env1 evd' v2 in + | Some v2 -> Retyping.get_type_of env1 evd' (EConstr.of_constr v2) in let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 66e690714..1261844a0 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -221,7 +221,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels else (* Might be a projection on the right *) match kind_of_term c2 with | Proj (pr, c) when not (Projection.unfolded pr) -> - (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in + (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c) (Array.map_to_list EConstr.of_constr args2) in sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) | _ -> raise PatternMatchingFailure) @@ -237,7 +237,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels with Invalid_argument _ -> raise PatternMatchingFailure else raise PatternMatchingFailure | _, Proj (pr,c) when not (Projection.unfolded pr) -> - (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in + (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c) (Array.map_to_list EConstr.of_constr arg2) in sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) | _, _ -> @@ -249,7 +249,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels raise PatternMatchingFailure | PApp (c, args), Proj (pr, c2) -> - (try let term = Retyping.expand_projection env sigma pr c2 [] in + (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c2) [] in sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) @@ -440,7 +440,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in if partial_app then try - let term = Retyping.expand_projection env sigma p c' [] in + let term = Retyping.expand_projection env sigma p (EConstr.of_constr c') [] in aux env term mk_ctx next with Retyping.RetypeError _ -> next () else diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a4d943cfa..e5e778f23 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -501,7 +501,7 @@ let rec detype flags avoid env sigma t = try let pb = Environ.lookup_projection p (snd env) in let body = pb.Declarations.proj_body in - let ty = Retyping.get_type_of (snd env) sigma c in + let ty = Retyping.get_type_of (snd env) sigma (EConstr.of_constr c) in let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma (EConstr.of_constr ty) in let body' = strip_lam_assum body in let body' = subst_instance_constr u body' in @@ -512,7 +512,7 @@ let rec detype flags avoid env sigma t = else if print_primproj_params () then try - let c = Retyping.expand_projection (snd env) sigma p c [] in + let c = Retyping.expand_projection (snd env) sigma p (EConstr.of_constr c) [] in detype flags avoid env sigma c with Retyping.RetypeError _ -> noparams () else noparams () @@ -689,7 +689,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = | BLetIn -> let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) - let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in + let s = try Retyping.get_sort_family_of (snd env) sigma (EConstr.of_constr ty) with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in let c = if s != InProp then c else GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in GLetIn (dl, na', c, r) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f54a57d57..47db71cc6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -165,7 +165,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let params1, c1, extra_args1 = match arg with | Some c -> (* A primitive projection applied to c *) - let ty = Retyping.get_type_of ~lax:true env sigma c in + let ty = Retyping.get_type_of ~lax:true env sigma (EConstr.of_constr c) in let (i,u), ind_args = try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) with _ -> raise Not_found @@ -464,7 +464,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else let f = try - let termM' = Retyping.expand_projection env evd p (EConstr.Unsafe.to_constr c) [] in + let termM' = Retyping.expand_projection env evd p c [] in let apprM', cstsM' = whd_betaiota_deltazeta_for_iota_state (fst ts) env evd cstsM (EConstr.of_constr termM',skM) @@ -643,7 +643,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Catch the p.c ~= p c' cases *) | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> let res = - try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c []))) + try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p (EConstr.of_constr c) []))) with Retyping.RetypeError _ -> None in (match res with @@ -654,7 +654,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> let res = - try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' []))) + try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' (EConstr.of_constr c') []))) with Retyping.RetypeError _ -> None in (match res with @@ -888,7 +888,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) List.fold_left (fun (i,ks,m,test) b -> if match n with Some n -> Int.equal m n | None -> false then - let ty = Retyping.get_type_of env i t2 in + let ty = Retyping.get_type_of env i (EConstr.of_constr t2) in let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else @@ -1058,7 +1058,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let id = NamedDecl.get_id decl' in let t = NamedDecl.get_type decl' in let evs = ref [] in - let ty = Retyping.get_type_of env_rhs evd c in + let ty = Retyping.get_type_of env_rhs evd (EConstr.of_constr c) in let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 17bb1406e..86ef8f56f 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -141,8 +141,8 @@ let recheck_applications conv_algo env evdref t = match kind_of_term t with | App (f, args) -> let () = aux env f in - let fty = Retyping.get_type_of env !evdref f in - let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in + let fty = Retyping.get_type_of env !evdref (EConstr.of_constr f) in + let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref (EConstr.of_constr x)) args in let rec aux i ty = if i < Array.length argsty then match kind_of_term (whd_all env !evdref (EConstr.of_constr ty)) with @@ -634,7 +634,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in let id = next_name_away na avoid in let evd,t_in_sign = - let s = Retyping.get_sort_of env evd t_in_env in + let s = Retyping.get_sort_of env evd (EConstr.of_constr t_in_env) in let evd,ty_t_in_sign = refresh_universes ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src t_in_env @@ -653,7 +653,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1) in let evd,ev2ty_in_sign = - let s = Retyping.get_sort_of env evd ty_in_env in + let s = Retyping.get_sort_of env evd (EConstr.of_constr ty_in_env) in let evd,ty_t_in_sign = refresh_universes ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src ty_in_env @@ -1161,7 +1161,7 @@ let check_evar_instance evd evk1 body conv_algo = (* FIXME: The body might be ill-typed when this is called from w_merge *) (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = - try Retyping.get_type_of ~lax:true evenv evd body + try Retyping.get_type_of ~lax:true evenv evd (EConstr.of_constr body) with Retyping.RetypeError _ -> error "Ill-typed evar instance" in match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with @@ -1365,7 +1365,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | (id,p)::_::_ -> if choose then (mkVar id, p) else raise (NotUniqueInType sols) in - let ty = lazy (Retyping.get_type_of env !evdref t) in + let ty = lazy (Retyping.get_type_of env !evdref (EConstr.of_constr t)) in let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in evdref := evd; c @@ -1428,7 +1428,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = if not !progress then raise (NotEnoughInformationEvarEvar t); (* Make the virtual left evar real *) - let ty = get_type_of env' evd t in + let ty = get_type_of env' evd (EConstr.of_constr t) in let (evd,evar'',ev'') = materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) @@ -1462,7 +1462,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | _ -> None with | Some l -> - let ty = get_type_of env' !evdref t in + let ty = get_type_of env' !evdref (EConstr.of_constr t) in let candidates = try let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 70e94b4dc..ac082d1bf 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -76,4 +76,4 @@ val remove_instance_local_defs : evar_map -> existential_key -> constr array -> constr list val get_type_of_refresh : - ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types + ?polyprop:bool -> ?lax:bool -> env -> evar_map -> EConstr.constr -> evar_map * types diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index a3cca2ad8..a9184777d 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -606,7 +606,7 @@ let rec instantiate_universes env evdref scl is = function let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = match mip.mind_arity with - | RegularArity s -> sigma, subst_instance_constr u s.mind_user_arity + | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity) | TemplateArity ar -> let _,scl = splay_arity env sigma conclty in let ctx = List.rev mip.mind_arity_ctxt in @@ -614,7 +614,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = let ctx = instantiate_universes env evdref scl ar.template_level (ctx,ar.template_param_levels) in - !evdref, mkArity (List.rev ctx,scl) + !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) let type_of_projection_knowing_arg env sigma p c ty = let c = EConstr.Unsafe.to_constr c in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1cfdef6e5..e375a2c6b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -195,7 +195,7 @@ i*) (********************) val type_of_inductive_knowing_conclusion : - env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * types + env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * EConstr.types (********************) val control_only_guard : env -> types -> unit diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 9dcb5d2a5..938b6b18e 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -153,7 +153,7 @@ let pattern_of_constr env sigma t = | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> - pattern_of_constr env (Retyping.expand_projection env sigma p c []) + pattern_of_constr env (Retyping.expand_projection env sigma p (EConstr.of_constr c) []) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2f42ad395..3c48c42df 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) -> diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 353bdbb89..2efb02417 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -49,12 +49,21 @@ let anomaly_on_error f x = try f x with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e) +let local_assum (na, t) = + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let local_def (na, b, t) = + let inj = EConstr.Unsafe.to_constr in + LocalDef (na, inj b, inj t) + let get_type_from_constraints env sigma t = - if isEvar (fst (decompose_app t)) then + let open EConstr in + if isEvar sigma (EConstr.of_constr (fst (decompose_app_vect sigma t))) then match List.map_filter (fun (pbty,env,t1,t2) -> - if is_fconv Reduction.CONV env sigma (EConstr.of_constr t) (EConstr.of_constr t1) then Some t2 - else if is_fconv Reduction.CONV env sigma (EConstr.of_constr t) (EConstr.of_constr t2) then Some t1 + if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2 + else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1 else None) (snd (Evd.extract_all_conv_pbs sigma)) with @@ -65,87 +74,89 @@ let get_type_from_constraints env sigma t = let rec subst_type env sigma typ = function | [] -> typ | h::rest -> - match kind_of_term (whd_all env sigma (EConstr.of_constr typ)) with - | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest + let open EConstr in + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma typ)) with + | Prod (na,c1,c2) -> subst_type env sigma (Vars.subst1 h c2) rest | _ -> retype_error NonFunctionalConstruction (* If ft is the type of f which itself is applied to args, *) (* [sort_of_atomic_type] computes ft[args] which has to be a sort *) let sort_of_atomic_type env sigma ft args = + let open EConstr in let rec concl_of_arity env n ar args = - match kind_of_term (whd_all env sigma (EConstr.of_constr ar)), args with - | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma ar)), args with + | Prod (na, t, b), h::l -> concl_of_arity (push_rel (local_def (na, Vars.lift n h, t)) env) (n + 1) b l | Sort s, [] -> s | _ -> retype_error NotASort in concl_of_arity env 0 ft (Array.to_list args) let type_of_var env id = - try NamedDecl.get_type (lookup_named id env) + try EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) with Not_found -> retype_error (BadVariable id) let decomp_sort env sigma t = - match kind_of_term (whd_all env sigma t) with + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with | Sort s -> s | _ -> retype_error NotASort let retype ?(polyprop=true) sigma = + let open EConstr in let rec type_of env cstr = - match kind_of_term cstr with + match EConstr.kind sigma cstr with | Meta n -> - (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) + EConstr.of_constr (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) with Not_found -> retype_error (BadMeta n)) | Rel n -> - let ty = RelDecl.get_type (lookup_rel n env) in - lift n ty + let ty = EConstr.of_constr (RelDecl.get_type (lookup_rel n env)) in + Vars.lift n ty | Var id -> type_of_var env id - | Const cst -> rename_type_of_constant env cst - | Evar ev -> Evd.existential_type sigma ev - | Ind ind -> rename_type_of_inductive env ind - | Construct cstr -> rename_type_of_constructor env cstr + | Const cst -> EConstr.of_constr (rename_type_of_constant env cst) + | Evar (evk, args) -> EConstr.of_constr (Evd.existential_type sigma (evk, Array.map EConstr.Unsafe.to_constr args)) + | Ind ind -> EConstr.of_constr (rename_type_of_inductive env ind) + | Construct cstr -> EConstr.of_constr (rename_type_of_constructor env cstr) | Case (_,p,c,lf) -> let Inductiveops.IndType(indf,realargs) = let t = type_of env c in - try Inductiveops.find_rectype env sigma (EConstr.of_constr t) + try Inductiveops.find_rectype env sigma t with Not_found -> try - let t = get_type_from_constraints env sigma t in - Inductiveops.find_rectype env sigma (EConstr.of_constr t) + let t = EConstr.of_constr (get_type_from_constraints env sigma t) in + Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in - let t = betazetaevar_applist sigma n (EConstr.of_constr p) (List.map EConstr.of_constr realargs) in - (match kind_of_term (whd_all env sigma (EConstr.of_constr (type_of env t))) with - | Prod _ -> whd_beta sigma (EConstr.of_constr (applist (t, [c]))) + let t = EConstr.of_constr (betazetaevar_applist sigma n p (List.map EConstr.of_constr realargs)) in + (match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma (type_of env t))) with + | Prod _ -> EConstr.of_constr (whd_beta sigma (applist (t, [c]))) | _ -> t) | Lambda (name,c1,c2) -> - mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2) + mkProd (name, c1, type_of (push_rel (local_assum (name,c1)) env) c2) | LetIn (name,b,c1,c2) -> - subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2) + Vars.subst1 b (type_of (push_rel (local_def (name,b,c1)) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) - | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> - let f = whd_evar sigma f in + | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in - strip_outer_cast sigma (EConstr.of_constr (subst_type env sigma t (Array.to_list args))) + EConstr.of_constr (strip_outer_cast sigma (subst_type env sigma t (Array.to_list args))) | App(f,args) -> - strip_outer_cast sigma - (EConstr.of_constr (subst_type env sigma (type_of env f) (Array.to_list args))) + EConstr.of_constr (strip_outer_cast sigma + (subst_type env sigma (type_of env f) (Array.to_list args))) | Proj (p,c) -> let ty = type_of env c in - (try - Inductiveops.type_of_projection_knowing_arg env sigma p (EConstr.of_constr c) (EConstr.of_constr ty) + EConstr.of_constr (try + Inductiveops.type_of_projection_knowing_arg env sigma p c ty with Invalid_argument _ -> retype_error BadRecursiveType) | Cast (c,_, t) -> t | Sort _ | Prod _ -> mkSort (sort_of env cstr) and sort_of env t = - match kind_of_term t with - | Cast (c,_, s) when isSort s -> destSort s + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> destSort sigma s | Sort (Prop c) -> type1_sort | Sort (Type u) -> Type (Univ.super u) | Prod (name,t,c2) -> - (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with + (match (sort_of env t, sort_of (push_rel (local_assum (name,t)) env) c2) with | _, (Prop Null as s) -> s | Prop _, (Prop Pos as s) -> s | Type _, (Prop Pos as s) when is_impredicative_set env -> s @@ -153,47 +164,45 @@ let retype ?(polyprop=true) sigma = | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) - | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> - let f = whd_evar sigma f in + | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | _ -> decomp_sort env sigma (EConstr.of_constr (type_of env t)) + | _ -> decomp_sort env sigma (type_of env t) and sort_family_of env t = - match kind_of_term t with - | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> family_of_sort (destSort sigma s) | Sort (Prop c) -> InType | Sort (Type u) -> InType | Prod (name,t,c2) -> - let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in + let s2 = sort_family_of (push_rel (local_assum (name,t)) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> - let f = whd_evar sigma f in + | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in family_of_sort (sort_of_atomic_type env sigma t args) | App(f,args) -> family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType | _ -> - family_of_sort (decomp_sort env sigma (EConstr.of_constr (type_of env t))) + family_of_sort (decomp_sort env sigma (type_of env t)) and type_of_global_reference_knowing_parameters env c args = let argtyps = - Array.map (fun c -> lazy (nf_evar sigma (type_of env c))) args in - match kind_of_term c with + Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in + match EConstr.kind sigma c with | Ind ind -> let mip = lookup_mind_specif env (fst ind) in - (try Inductive.type_of_inductive_knowing_parameters + EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters ~polyprop env (mip,snd ind) argtyps with Reduction.NotArity -> retype_error NotAnArity) | Const cst -> - (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps + EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps with Reduction.NotArity -> retype_error NotAnArity) | Var id -> type_of_var env id - | Construct cstr -> type_of_constructor env cstr + | Construct cstr -> EConstr.of_constr (type_of_constructor env cstr) | _ -> assert false in type_of, sort_of, sort_family_of, @@ -204,19 +213,19 @@ let get_sort_of ?(polyprop=true) env sigma t = let get_sort_family_of ?(polyprop=true) env sigma c = let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c let type_of_global_reference_knowing_parameters env sigma c args = - let _,_,_,f = retype sigma in anomaly_on_error (f env c) args + let _,_,_,f = retype sigma in EConstr.Unsafe.to_constr (anomaly_on_error (f env c) args) let type_of_global_reference_knowing_conclusion env sigma c conclty = - match kind_of_term c with + match EConstr.kind sigma c with | Ind (ind,u) -> let spec = Inductive.lookup_mind_specif env ind in - type_of_inductive_knowing_conclusion env sigma (spec,u) (EConstr.of_constr conclty) + type_of_inductive_knowing_conclusion env sigma (spec,u) conclty | Const cst -> let t = constant_type_in env cst in (* TODO *) - sigma, Typeops.type_of_constant_type_knowing_parameters env t [||] + sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||]) | Var id -> sigma, type_of_var env id - | Construct cstr -> sigma, type_of_constructor env cstr + | Construct cstr -> sigma, EConstr.of_constr (type_of_constructor env cstr) | _ -> assert false (* Profiling *) @@ -232,10 +241,10 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = let f,_,_,_ = retype ~polyprop sigma in - if lax then f env c else anomaly_on_error (f env) c + if lax then EConstr.Unsafe.to_constr (f env c) else EConstr.Unsafe.to_constr (anomaly_on_error (f env) c) (* Makes an unsafe judgment from a constr *) -let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c } +let get_judgment_of env evc c = { uj_val = EConstr.Unsafe.to_constr c; uj_type = get_type_of env evc c } (* Returns sorts of a context *) let sorts_of_context env evc ctxt = @@ -243,15 +252,16 @@ let sorts_of_context env evc ctxt = | [] -> env,[] | d :: ctxt -> let env,sorts = aux ctxt in - let s = get_sort_of env evc (RelDecl.get_type d) in + let s = get_sort_of env evc (EConstr.of_constr (RelDecl.get_type d)) in (push_rel d env,s::sorts) in snd (aux ctxt) let expand_projection env sigma pr c args = + let inj = EConstr.Unsafe.to_constr in let ty = get_type_of ~lax:true env sigma c in let (i,u), ind_args = try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty) with Not_found -> retype_error BadRecursiveType in mkApp (mkConstU (Projection.constant pr,u), - Array.of_list (ind_args @ (c :: args))) + Array.of_list (ind_args @ (inj c :: List.map inj args))) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 8ca40f829..08f750287 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -26,25 +26,25 @@ type retype_error exception RetypeError of retype_error val get_type_of : - ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types + ?polyprop:bool -> ?lax:bool -> env -> evar_map -> EConstr.constr -> types val get_sort_of : - ?polyprop:bool -> env -> evar_map -> types -> sorts + ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> sorts_family + ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts_family (** Makes an unsafe judgment from a constr *) -val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment +val get_judgment_of : env -> evar_map -> EConstr.constr -> unsafe_judgment -val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> - constr array -> types +val type_of_global_reference_knowing_parameters : env -> evar_map -> EConstr.constr -> + EConstr.constr array -> types val type_of_global_reference_knowing_conclusion : - env -> evar_map -> constr -> types -> evar_map * types + env -> evar_map -> EConstr.constr -> EConstr.types -> evar_map * EConstr.types val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list -val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr +val expand_projection : env -> evar_map -> Names.projection -> EConstr.constr -> EConstr.constr list -> constr val print_retype_error : retype_error -> Pp.std_ppcmds diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 357a80f44..ac2a3bc49 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -974,7 +974,7 @@ let matches_head env sigma c t = let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = match kind_of_term c with | Proj (p, r) -> (* Treat specially for partial applications *) - let t = Retyping.expand_projection env sigma p r [] in + let t = Retyping.expand_projection env sigma p (EConstr.of_constr r) [] in let hdf, al = destApp t in let a = al.(Array.length al - 1) in let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in @@ -1150,7 +1150,7 @@ let compute = cbv_betadeltaiota * the specified occurrences. *) let abstract_scheme env (locc,a) (c, sigma) = - let ta = Retyping.get_type_of env sigma a in + let ta = Retyping.get_type_of env sigma (EConstr.of_constr a) in let na = named_hd env ta Anonymous in if occur_meta sigma (EConstr.of_constr ta) then error "Cannot find a type for the generalisation."; if occur_meta sigma (EConstr.of_constr a) then diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 50dd66ea0..8c03329e2 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -300,7 +300,7 @@ let build_subclasses ~check env sigma glob pri = | Some (Forward, pri') -> let proj = Option.get proj in let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in - if check && check_instance env sigma body then None + if check && check_instance env sigma (EConstr.of_constr body) then None else let pri = match pri, pri' with @@ -312,7 +312,7 @@ let build_subclasses ~check env sigma glob pri = in let declare_proj hints (cref, pri, body) = let path' = cref :: path in - let ty = Retyping.get_type_of env sigma body in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in let rest = aux pri body ty path' in hints @ (path', pri, body) :: rest in List.fold_left declare_proj [] projs diff --git a/pretyping/typing.ml b/pretyping/typing.ml index e3d1c1741..acfe05f24 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -138,7 +138,7 @@ let check_type_fixpoint loc env evdref lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = - let pj = Retyping.get_judgment_of env sigma p in + let pj = Retyping.get_judgment_of env sigma (EConstr.of_constr p) in let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ede2606da..848a2f4a8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -684,7 +684,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if opt.with_types && flags.check_applied_meta_types then (try let tyM = Typing.meta_type sigma k in - let tyN = get_type_of curenv ~lax:true sigma cN in + let tyN = get_type_of curenv ~lax:true sigma (EConstr.of_constr cN) in check_compatibility curenv CUMUL flags substn tyN tyM with RetypeError _ -> (* Renounce, maybe metas/evars prevents typing *) sigma) @@ -703,7 +703,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let sigma = if opt.with_types && flags.check_applied_meta_types then (try - let tyM = get_type_of curenv ~lax:true sigma cM in + let tyM = get_type_of curenv ~lax:true sigma (EConstr.of_constr cM) in let tyN = Typing.meta_type sigma k in check_compatibility curenv CUMUL flags substn tyM tyN with RetypeError _ -> @@ -863,7 +863,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let expand_proj c c' l = match kind_of_term c with | Proj (p, t) when not (Projection.unfolded p) && needs_expansion p c' -> - (try destApp (Retyping.expand_projection curenv sigma p t (Array.to_list l)) + (try destApp (Retyping.expand_projection curenv sigma p (EConstr.of_constr t) (Array.map_to_list EConstr.of_constr l)) with RetypeError _ -> (** Unification can be called on ill-typed terms, due to FO and eta in particular, fail gracefully in that case *) (c, l)) @@ -888,8 +888,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb and unify_same_proj (curenv, nb as curenvnb) cv_pb opt substn c1 c2 = let substn = unirec_rec curenvnb CONV opt substn c1 c2 in try (* Force unification of the types to fill in parameters *) - let ty1 = get_type_of curenv ~lax:true sigma c1 in - let ty2 = get_type_of curenv ~lax:true sigma c2 in + let ty1 = get_type_of curenv ~lax:true sigma (EConstr.of_constr c1) in + let ty2 = get_type_of curenv ~lax:true sigma (EConstr.of_constr c2) in unify_0_with_initial_metas substn true curenv cv_pb { flags with modulo_conv_on_closed_terms = Some full_transparent_state; modulo_delta = full_transparent_state; @@ -953,8 +953,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let sigma = if opt.with_types then try (* Ensure we call conversion on terms of the same type *) - let tyM = get_type_of curenv ~lax:true sigma m1 in - let tyN = get_type_of curenv ~lax:true sigma n1 in + let tyM = get_type_of curenv ~lax:true sigma (EConstr.of_constr m1) in + let tyN = get_type_of curenv ~lax:true sigma (EConstr.of_constr n1) in check_compatibility curenv CUMUL flags substn tyM tyN with RetypeError _ -> (* Renounce, maybe metas/evars prevents typing *) sigma @@ -1240,13 +1240,13 @@ let w_coerce_to_type env evd c cty mvty = try_to_coerce env evd c cty tycon let w_coerce env evd mv c = - let cty = get_type_of env evd c in + let cty = get_type_of env evd (EConstr.of_constr c) in let mvty = Typing.meta_type evd mv in w_coerce_to_type env evd c cty mvty let unify_to_type env sigma flags c status u = let sigma, c = refresh_universes (Some false) env sigma c in - let t = get_type_of env sigma (nf_meta sigma c) in + let t = get_type_of env sigma (EConstr.of_constr (nf_meta sigma c)) in let t = nf_betaiota sigma (EConstr.of_constr (nf_meta sigma t)) in unify_0 env sigma CUMUL flags t u @@ -1379,7 +1379,7 @@ let w_merge env with_types flags (evd,metas,evars) = let evd' = Sigma.to_evar_map evd' in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags - (get_type_of sp_env evd' c) ev.evar_concl in + (get_type_of sp_env evd' (EConstr.of_constr c)) ev.evar_concl in let evd''' = w_merge_rec evd'' mc ec [] in if evd' == evd''' then Evd.define sp c evd''' @@ -1422,13 +1422,13 @@ let check_types env flags (sigma,_,_ as subst) m n = if isEvar_or_Meta (head_app sigma m) then unify_0_with_initial_metas subst true env CUMUL flags - (get_type_of env sigma n) - (get_type_of env sigma m) + (get_type_of env sigma (EConstr.of_constr n)) + (get_type_of env sigma (EConstr.of_constr m)) else if isEvar_or_Meta (head_app sigma n) then unify_0_with_initial_metas subst true env CUMUL flags - (get_type_of env sigma m) - (get_type_of env sigma n) + (get_type_of env sigma (EConstr.of_constr m)) + (get_type_of env sigma (EConstr.of_constr n)) else subst let try_resolve_typeclasses env evd flag m n = @@ -1557,7 +1557,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = applist (t,l1), l2 else t, [] in let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in - let ty = Retyping.get_type_of env sigma t in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr t) in if not (is_correct_type ty) then raise (NotUnifiable None); Some(sigma, t, l2) with @@ -1590,7 +1590,7 @@ let make_eq_test env evd c = let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let id = - let t = match ty with Some t -> t | None -> get_type_of env sigma c in + let t = match ty with Some t -> t | None -> get_type_of env sigma (EConstr.of_constr c) in let x = id_of_name_using_hdchar (Global.env()) t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d64cd9fff..f4ac094b8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -67,7 +67,7 @@ let refresh_undefined_univs clenv = let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t -let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c +let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) (EConstr.of_constr c) exception NotExtensibleClause @@ -667,8 +667,8 @@ let evar_of_binder holes = function user_err (str "No such binder.") let define_with_type sigma env ev c = - let t = Retyping.get_type_of env sigma ev in - let ty = Retyping.get_type_of env sigma c in + let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in let (ev, _) = destEvar ev in diff --git a/proofs/logic.ml b/proofs/logic.ml index 0fa193065..2df626e1c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -319,18 +319,19 @@ let check_conv_leq_goal env sigma arg ty conclty = else raise (RefinerError (BadType (arg,ty,conclty))) else sigma -exception Stop of constr list +exception Stop of EConstr.t list let meta_free_prefix sigma a = try + let a = Array.map EConstr.of_constr a in let _ = Array.fold_left (fun acc a -> - if occur_meta sigma (EConstr.of_constr a) then raise (Stop acc) + if occur_meta sigma a then raise (Stop acc) else a :: acc) [] a in a with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = if !check then unsafe_type_of env sigma c - else Retyping.get_type_of env sigma c + else Retyping.get_type_of env sigma (EConstr.of_constr c) let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in @@ -339,7 +340,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then - let t'ty = Retyping.get_type_of env sigma trm in + let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) else @@ -372,7 +373,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = (* Template sort-polymorphism of definition and inductive types *) let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in - type_of_global_reference_knowing_parameters env sigma f args + type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) in goalacc, ty, sigma, f else @@ -386,7 +387,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Proj (p,c) -> let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in - let ty = get_type_of env sigma c in + let ty = get_type_of env sigma (EConstr.of_constr c) in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> @@ -435,7 +436,7 @@ and mk_hdgoals sigma goal goalacc trm = if is_template_polymorphic env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in - (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) + (goalacc,type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l',sigma,f) else mk_hdgoals sigma goal goalacc f in let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in @@ -460,7 +461,7 @@ and mk_hdgoals sigma goal goalacc trm = | Proj (p,c) -> let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in - let ty = get_type_of env sigma c in + let ty = get_type_of env sigma (EConstr.of_constr c) in (acc',ty,sigma,c) | _ -> diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 62fe2c17c..19e72e697 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,7 +24,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) let warn_native_compute_disabled = @@ -37,7 +37,7 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) let whd_cbn flags env sigma t = diff --git a/proofs/refine.ml b/proofs/refine.ml index d4920e505..e6e3ef47d 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -133,7 +133,7 @@ let refine ?(unsafe = true) f = (** Useful definitions *) let with_type env evd c t = - let my_type = Retyping.get_type_of env evd c in + let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in let j = Environ.make_judge c my_type in let (evd,j') = Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 09f5246ab..b63b2ce28 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -104,7 +104,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls +let pf_hnf_type_of gls = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv @@ -230,7 +230,7 @@ module New = struct let pf_hnf_constr gl t = pf_reduce hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_all gl (pf_get_type_of gl t) + pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t)) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index fe7a09f77..6fb90e7af 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -280,7 +280,7 @@ let clenv_of_prods poly nprods (c, clenv) gl = if poly || Int.equal nprods 0 then Some (None, clenv) else let sigma = Tacmach.New.project gl in - let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in + let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma (EConstr.of_constr c) in let diff = nb_prod sigma (EConstr.of_constr ty) - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) @@ -473,7 +473,7 @@ let catchable = function let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l) let is_Prop env sigma concl = - let ty = Retyping.get_type_of env sigma concl in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr concl) in match kind_of_term ty with | Sort (Prop Null) -> true | _ -> false diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index b9704b846..789028ac1 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -28,7 +28,7 @@ let absurd c = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map sigma in - let j = Retyping.get_judgment_of env sigma c in + let j = Retyping.get_judgment_of env sigma (EConstr.of_constr c) in let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in let t = j.Environ.utj_val in let tac = diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index aea3ca17e..92480e253 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -596,7 +596,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = (**********************************************************************) let fix_r2l_forward_rew_scheme (c, ctx') = - let t = Retyping.get_type_of (Global.env()) Evd.empty c in + let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in let ctx,_ = decompose_prod_assum t in match ctx with | hp :: p :: ind :: indargs -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 48f46b36b..e87746a28 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -440,7 +440,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in - let ctype = get_type_of env sigma c in + let ctype = get_type_of env sigma (EConstr.of_constr c) in let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr ctype)) in match match_with_equality_type sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) @@ -621,8 +621,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = in Proofview.Goal.enter { enter = begin fun gl -> let get_type_of = pf_apply get_type_of gl in - let t1 = get_type_of c1 - and t2 = get_type_of c2 in + let t1 = get_type_of (EConstr.of_constr c1) + and t2 = get_type_of (EConstr.of_constr c2) in let evd = if unsafe then Some (Tacmach.New.project gl) else @@ -719,8 +719,8 @@ let find_positions env sigma t1 t2 = let project env sorts posn t1 t2 = let t1 = EConstr.Unsafe.to_constr t1 in let t2 = EConstr.Unsafe.to_constr t2 in - let ty1 = get_type_of env sigma t1 in - let s = get_sort_family_of env sigma ty1 in + let ty1 = get_type_of env sigma (EConstr.of_constr t1) in + let s = get_sort_family_of env sigma (EConstr.of_constr ty1) in if Sorts.List.mem s sorts then [(List.rev posn,t1,t2)] else [] in @@ -842,7 +842,7 @@ let injectable env sigma t1 t2 = let descend_then env sigma head dirn = let IndType (indf,_) = - try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma head)) + try find_rectype env sigma (EConstr.of_constr (get_type_of env sigma (EConstr.of_constr head))) with Not_found -> error "Cannot project on an inductive type derived from a dependency." in let indp,_ = (dest_ind_family indf) in @@ -897,7 +897,7 @@ let build_selector env sigma dirn c ind special default = dependent types.") in let (indp,_) = dest_ind_family indf in let ind, _ = check_privacy env indp in - let typ = Retyping.get_type_of env sigma default in + let typ = Retyping.get_type_of env sigma (EConstr.of_constr default) in let (mib,mip) = lookup_mind_specif env ind in let deparsign = make_arity_signature env true indf in let p = it_mkLambda_or_LetIn typ deparsign in @@ -912,7 +912,7 @@ let build_selector env sigma dirn c ind special default = let rec build_discriminator env sigma dirn c = function | [] -> - let ind = get_type_of env sigma c in + let ind = get_type_of env sigma (EConstr.of_constr c) in let true_0,false_0 = build_coq_True(),build_coq_False() in build_selector env sigma dirn c ind true_0 false_0 @@ -1084,7 +1084,7 @@ let find_sigma_data env s = build_sigma_type () let make_tuple env sigma (rterm,rty) lind = assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty))); - let sigdata = find_sigma_data env (get_sort_of env sigma rty) in + let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) @@ -1262,7 +1262,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let make_iterated_tuple env sigma dflt (z,zty) = let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in - let sort_of_zty = get_sort_of env sigma zty in + let sort_of_zty = get_sort_of env sigma (EConstr.of_constr zty) in let sorted_rels = Int.Set.elements rels in let sigma, (tuple,tuplety) = List.fold_left (fun (sigma, t) -> make_tuple env sigma t) (sigma, (z,zty)) sorted_rels @@ -1533,7 +1533,7 @@ let decomp_tuple_term env sigma c t = let subst_tuple_term env sigma dep_pair1 dep_pair2 b = let sigma = Sigma.to_evar_map sigma in - let typ = get_type_of env sigma dep_pair1 in + let typ = get_type_of env sigma (EConstr.of_constr dep_pair1) in (* We find all possible decompositions *) let decomps1 = decomp_tuple_term env sigma dep_pair1 typ in let decomps2 = decomp_tuple_term env sigma dep_pair2 typ in @@ -1623,7 +1623,7 @@ let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None let substClause l2r c cls = Proofview.Goal.enter { enter = begin fun gl -> - let eq = pf_apply get_type_of gl c in + let eq = pf_apply get_type_of gl (EConstr.of_constr c) in tclTHENS (cutSubstClause l2r eq cls) [Proofview.tclUNIT (); exact_no_check c] end } diff --git a/tactics/hints.ml b/tactics/hints.ml index c41f88ab7..2aa434777 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -846,7 +846,7 @@ let fresh_global_or_constr env sigma poly cr = let make_resolves env sigma flags pri poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in - let cty = Retyping.get_type_of env sigma c in + let cty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let try_apply f = try Some (f (c, cty, ctx)) with Failure _ -> None in let ents = List.map_filter try_apply diff --git a/tactics/inv.ml b/tactics/inv.ml index 0b2d2f0b2..38f75995b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -65,7 +65,7 @@ let var_occurs_in_pf gl id = type inversion_status = Dep of constr option | NoDep let compute_eqn env sigma n i ai = - (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) + (mkRel (n-i),get_type_of env sigma (EConstr.of_constr (mkRel (n-i)))) let make_inv_predicate env evd indf realargs id status concl = let nrealargs = List.length realargs in @@ -86,7 +86,7 @@ let make_inv_predicate env evd indf realargs id status concl = match dflt_concl with | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> - let sort = get_sort_family_of env !evd concl in + let sort = get_sort_family_of env !evd (EConstr.of_constr concl) in let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in let p = make_arity env true indf sort in let evd',(p,ptyp) = Unification.abstract_list_all env diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 676b23d09..2754db010 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -248,10 +248,10 @@ let compute_constructor_signatures isrec ((_,k as ity),u) = Array.map2 analrec lc lrecargs let elimination_sort_of_goal gl = - pf_apply Retyping.get_sort_family_of gl (pf_concl gl) + pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr (pf_concl gl)) let elimination_sort_of_hyp id gl = - pf_apply Retyping.get_sort_family_of gl (pf_get_hyp_typ gl id) + pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr (pf_get_hyp_typ gl id)) let elimination_sort_of_clause = function | None -> elimination_sort_of_goal @@ -708,12 +708,12 @@ module New = struct let elimination_sort_of_goal gl = (** Retyping will expand evars anyway. *) let c = Proofview.Goal.concl (Goal.assume gl) in - pf_apply Retyping.get_sort_family_of gl c + pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr c) let elimination_sort_of_hyp id gl = (** Retyping will expand evars anyway. *) let c = pf_get_hyp_typ id (Goal.assume gl) in - pf_apply Retyping.get_sort_family_of gl c + pf_apply Retyping.get_sort_family_of gl (EConstr.of_constr c) let elimination_sort_of_clause id gl = match id with | None -> elimination_sort_of_goal gl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c96553fae..e294f928e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -412,7 +412,7 @@ let default_id env sigma decl = let open Context.Rel.Declaration in match decl with | LocalAssum (name,t) -> - let dft = default_id_of_sort (Retyping.get_sort_of env sigma t) in + let dft = default_id_of_sort (Retyping.get_sort_of env sigma (EConstr.of_constr t)) in id_of_name_with_default dft name | LocalDef (name,b,_) -> id_of_name_using_hdchar env b name @@ -784,9 +784,9 @@ let make_change_arg c pats = { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma } let check_types env sigma mayneedglobalcheck deep newc origc = - let t1 = Retyping.get_type_of env sigma newc in + let t1 = Retyping.get_type_of env sigma (EConstr.of_constr newc) in if deep then begin - let t2 = Retyping.get_type_of env sigma origc in + let t2 = Retyping.get_type_of env sigma (EConstr.of_constr origc) in let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in @@ -1341,7 +1341,7 @@ let enforce_prop_bound_names rename tac = | Prod (Name _ as na,t,t') -> let very_standard = true in let na = - if Retyping.get_sort_family_of env sigma t = InProp then + if Retyping.get_sort_family_of env sigma (EConstr.of_constr t) = InProp then (* "very_standard" says that we should have "H" names only, but this would break compatibility even more... *) let s = match Namegen.head_name t with @@ -1411,7 +1411,7 @@ let general_elim_clause_gen elimtac indclause elim = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (elimc,lbindelimc) = elim.elimbody in - let elimt = Retyping.get_type_of env sigma elimc in + let elimt = Retyping.get_type_of env sigma (EConstr.of_constr elimc) in let i = match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in elimtac elim.elimrename i (elimc, elimt, lbindelimc) indclause @@ -1421,7 +1421,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let ct = Retyping.get_type_of env sigma c in + let ct = Retyping.get_type_of env sigma (EConstr.of_constr c) in let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in @@ -1439,7 +1439,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in + let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c) in let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in let sort = Tacticals.New.elimination_sort_of_goal gl in let Sigma (elim, sigma, p) = @@ -1554,7 +1554,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) (str "The type of elimination clause is not well-formed.") in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in let hyp = mkVar id in - let hyp_typ = Retyping.get_type_of env sigma hyp in + let hyp_typ = Retyping.get_type_of env sigma (EConstr.of_constr hyp) in let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in let new_hyp_typ = clenv_type elimclause'' in @@ -1614,7 +1614,7 @@ let make_projection env sigma params cstr sign elim i n c u = [|mkApp (c, args)|]) in let app = it_mkLambda_or_LetIn proj sign in - let t = Retyping.get_type_of env sigma app in + let t = Retyping.get_type_of env sigma (EConstr.of_constr app) in Some (app, t) | None -> None in elim @@ -1624,7 +1624,7 @@ let descend_in_conjunctions avoid tac (err, info) c = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try - let t = Retyping.get_type_of env sigma c in + let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in let sign,ccl = decompose_prod_assum t in match match_with_tuple sigma ccl with @@ -1704,7 +1704,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let thm_ty0 = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma c)) in + let thm_ty0 = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) in let try_apply thm_ty nprod = try let n = nb_prod_modulo_zeta sigma (EConstr.of_constr thm_ty) - nprod in @@ -1830,7 +1830,7 @@ let progress_with_clause flags innerclause clause = with Not_found -> error "Unable to unify." let apply_in_once_main flags innerclause env sigma (d,lbind) = - let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma d)) in + let thm = nf_betaiota sigma (EConstr.of_constr (Retyping.get_type_of env sigma (EConstr.of_constr d))) in let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> @@ -2604,7 +2604,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let Sigma (t, sigma, p) = match ty with | Some t -> Sigma.here t sigma | None -> - let t = typ_of env sigma c in + let t = typ_of env sigma (EConstr.of_constr c) in let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in Sigma.Unsafe.of_pair (c, sigma) in @@ -2656,7 +2656,7 @@ let insert_before decls lasthyp env = let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let open Context.Named.Declaration in - let t = match ty with Some t -> t | _ -> typ_of env sigma c in + let t = match ty with Some t -> t | _ -> typ_of env sigma (EConstr.of_constr c) in let decl = if dep then LocalDef (id,c,t) else LocalAssum (id,t) in @@ -2903,7 +2903,7 @@ let specialize (c,lbind) ipat = let sigma = Typeclasses.resolve_typeclasses env sigma in sigma, nf_evar sigma c else - let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in + let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma (EConstr.of_constr c)) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (EConstr.of_constr (clenv_value clause)) in @@ -2919,7 +2919,7 @@ let specialize (c,lbind) ipat = pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd (EConstr.of_constr term)))) ++ str "."); clause.evd, term in - let typ = Retyping.get_type_of env sigma term in + let typ = Retyping.get_type_of env sigma (EConstr.of_constr term) in let tac = match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> @@ -3152,7 +3152,7 @@ let expand_projections env sigma c = let sigma = Sigma.to_evar_map sigma in let rec aux env c = match EConstr.kind sigma c with - | Proj (p, c) -> EConstr.of_constr (Retyping.expand_projection env sigma p (EConstr.Unsafe.to_constr (aux env c)) []) + | Proj (p, c) -> EConstr.of_constr (Retyping.expand_projection env sigma p (aux env c) []) | _ -> map_constr_with_full_binders sigma push_rel aux env c in EConstr.Unsafe.to_constr (aux env (EConstr.of_constr c)) @@ -3673,7 +3673,7 @@ let abstract_args gl generalize_vars dep id defined f args = else [] in let body, c' = - if defined then Some c', Retyping.get_type_of ctxenv !sigma c' + if defined then Some c', Retyping.get_type_of ctxenv !sigma (EConstr.of_constr c') else None, c' in let typ = Tacmach.pf_get_hyp_typ gl id in @@ -4132,7 +4132,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let dep_in_concl = Option.cata (fun id -> occur_var env sigma id (EConstr.of_constr concl)) false hyp0 in let dep = dep_in_hyps || dep_in_concl in let tmpcl = it_mkNamedProd_or_LetIn concl deps in - let s = Retyping.get_sort_family_of env sigma tmpcl in + let s = Retyping.get_sort_family_of env sigma (EConstr.of_constr tmpcl) in let deps_cstr = List.fold_left (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in @@ -4286,7 +4286,7 @@ let check_enough_applied env sigma elim = fun u -> let t,_ = decompose_app (whd_all env sigma (EConstr.of_constr u)) in isInd t | Some elimc -> - let elimt = Retyping.get_type_of env sigma (fst elimc) in + let elimt = Retyping.get_type_of env sigma (EConstr.of_constr (fst elimc)) in let scheme = compute_elim_sig ~elimc elimt in match scheme.indref with | None -> @@ -4331,7 +4331,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim Refine.refine ~unsafe:true { run = begin fun sigma -> let b = not with_evars && with_eq != None in let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in - let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in + let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c) in let Sigma (ans, sigma, q) = mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t) in Sigma (ans, sigma, p +> q) end }; @@ -4376,7 +4376,7 @@ let induction_gen clear_flag isrec with_evars elim let sigma = Proofview.Goal.sigma gl in let ccl = Proofview.Goal.raw_concl gl in let cls = Option.default allHypsAndConcl cls in - let t = typ_of env sigma c in + let t = typ_of env sigma (EConstr.of_constr c) in let is_arg_pure_hyp = isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ())) && lbind == NoBindings && not with_evars && Option.is_empty eqname diff --git a/toplevel/command.ml b/toplevel/command.ml index 249d41845..14a45f837 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -206,7 +206,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t - | None -> Retyping.get_type_of env evd c + | None -> Retyping.get_type_of env evd (EConstr.of_constr c) in Obligations.check_evars env evd; let obls, _, c, cty = @@ -459,7 +459,7 @@ let sign_level env evd sign = | LocalDef _ -> lev, push_rel d env | LocalAssum _ -> let s = destSort (Reduction.whd_all env - (nf_evar evd (Retyping.get_type_of env evd (RelDecl.get_type d)))) + (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))) in let u = univ_of_sort s in (Univ.sup u lev, push_rel d env)) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 3f818f960..fef99d8af 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -403,7 +403,7 @@ let do_mutual_induction_scheme lnamedepindsort = in let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = - let decltype = Retyping.get_type_of env0 sigma decl in + let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref diff --git a/toplevel/record.ml b/toplevel/record.ml index ffe7980ef..5f2b99f90 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -84,7 +84,7 @@ let compute_constructor_level evars env l = List.fold_right (fun d (env, univ) -> let univ = if is_local_assum d then - let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in + let s = Retyping.get_sort_of env evars (EConstr.of_constr (RelDecl.get_type d)) in Univ.sup (univ_of_sort s) univ else univ in (push_rel d env, univ)) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 593aa9578..c39b4dc25 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1579,7 +1579,7 @@ let vernac_check_may_eval redexp glopt rc = let c = nf c in let j = if Evarutil.has_undefined_evars sigma' c then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) + Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) else (* OK to call kernel which does not support evars *) Arguments_renaming.rename_typing env c in |