aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-01 20:53:32 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:21:51 +0100
commit8f6aab1f4d6d60842422abc5217daac806eb0897 (patch)
treec36f2f963064f51fe1652714f4d91677d555727b /pretyping
parent5143129baac805d3a49ac3ee9f3344c7a447634f (diff)
Reductionops API using EConstr.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml24
-rw-r--r--pretyping/classops.ml23
-rw-r--r--pretyping/coercion.ml24
-rw-r--r--pretyping/constr_matching.ml2
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/evarconv.ml177
-rw-r--r--pretyping/evarconv.mli8
-rw-r--r--pretyping/evardefine.ml10
-rw-r--r--pretyping/evarsolve.ml16
-rw-r--r--pretyping/evarsolve.mli2
-rw-r--r--pretyping/indrec.ml16
-rw-r--r--pretyping/inductiveops.ml53
-rw-r--r--pretyping/inductiveops.mli18
-rw-r--r--pretyping/nativenorm.ml95
-rw-r--r--pretyping/pretyping.ml20
-rw-r--r--pretyping/recordops.ml5
-rw-r--r--pretyping/recordops.mli2
-rw-r--r--pretyping/reductionops.ml445
-rw-r--r--pretyping/reductionops.mli100
-rw-r--r--pretyping/retyping.ml29
-rw-r--r--pretyping/tacred.ml266
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/typing.ml12
-rw-r--r--pretyping/unification.ml66
-rw-r--r--pretyping/vnorm.ml110
-rw-r--r--pretyping/vnorm.mli2
26 files changed, 815 insertions, 714 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6b480986c..be72091a9 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -292,7 +292,7 @@ let inductive_template evdref env tmloc ind =
applist (mkIndU indu,List.rev evarl)
let try_find_ind env sigma typ realnames =
- let (IndType(indf,realargs) as ind) = find_rectype env sigma typ in
+ let (IndType(indf,realargs) as ind) = find_rectype env sigma (EConstr.of_constr typ) in
let names =
match realnames with
| Some names -> names
@@ -1035,7 +1035,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
(* We need _parallel_ bindings to get gamma, x1...xn |- PI tms. ccl'' *)
(* Note: applying the substitution in tms is not important (is it sure?) *)
let ccl'' =
- whd_betaiota Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in
+ whd_betaiota Evd.empty (EConstr.of_constr (subst_predicate (realargsi, copti) ccl' tms)) in
(* We adjust ccl st: gamma, x'1..x'n, x1..xn, tms |- ccl'' *)
let ccl''' = liftn_predicate n (n+1) ccl'' tms in
(* We finally get gamma,x'1..x'n,x |- [X1;x1:I(X1)]..[Xn;xn:I(Xn)]pred'''*)
@@ -1044,7 +1044,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
let pred = abstract_predicate env !evdref indf current realargs dep tms p in
(pred, whd_betaiota !evdref
- (applist (pred, realargs@[current])))
+ (EConstr.of_constr (applist (pred, realargs@[current]))))
(* Take into account that a type has been discovered to be inductive, leading
to more dependencies in the predicate if the type has indices *)
@@ -1199,7 +1199,7 @@ let rec generalize_problem names pb = function
| LocalDef (Anonymous,_,_) -> pb', deps
| _ ->
(* for better rendering *)
- let d = RelDecl.map_type (whd_betaiota !(pb.evdref)) d in
+ let d = RelDecl.map_type (fun c -> whd_betaiota !(pb.evdref) (EConstr.of_constr c)) d in
let tomatch = lift_tomatch_stack 1 pb'.tomatch in
let tomatch = relocate_index_tomatch (i+1) 1 tomatch in
{ pb' with
@@ -1377,7 +1377,7 @@ and match_current pb (initial,tomatch) =
find_predicate pb.caseloc pb.env pb.evdref
pred current indt (names,dep) tomatch in
let ci = make_case_info pb.env (fst mind) pb.casestyle in
- let pred = nf_betaiota !(pb.evdref) pred in
+ let pred = nf_betaiota !(pb.evdref) (EConstr.of_constr pred) in
let case =
make_case_or_project pb.env indf ci pred current brvals
in
@@ -1613,7 +1613,7 @@ let rec list_assoc_in_triple x = function
*)
let abstract_tycon loc env evdref subst tycon extenv t =
- let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*)
+ let t = nf_betaiota !evdref (EConstr.of_constr t) in (* it helps in some cases to remove K-redex*)
let src = match kind_of_term t with
| Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk)
| _ -> (loc,Evar_kinds.CasesType true) in
@@ -1635,13 +1635,13 @@ let abstract_tycon loc env evdref subst tycon extenv t =
try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
1 (rel_context env) in
let ev' = e_new_evar env evdref ~src ty in
- begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
+ begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,EConstr.of_constr (substl inst ev')) with
| Success evd -> evdref := evd
| UnifFailure _ -> assert false
end;
ev'
| _ ->
- let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref t u) subst in
+ let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref (EConstr.of_constr t) (EConstr.of_constr u)) subst in
match good with
| [] ->
let self env c = EConstr.of_constr (aux env (EConstr.Unsafe.to_constr c)) in
@@ -1705,7 +1705,7 @@ let build_inversion_problem loc env sigma tms t =
let id = next_name_away (named_hd env t Anonymous) avoid in
PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in
let rec reveal_pattern t (subst,avoid as acc) =
- match kind_of_term (whd_all env sigma t) with
+ match kind_of_term (whd_all env sigma (EConstr.of_constr t)) with
| Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc
| App (f,v) when isConstruct f ->
let cstr,u = destConstruct f in
@@ -2038,7 +2038,7 @@ let constr_of_pat env evdref arsign pat avoid =
| PatCstr (l,((_, i) as cstr),args,alias) ->
let cind = inductive_of_constructor cstr in
let IndType (indf, _) =
- try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
+ try find_rectype env ( !evdref) (EConstr.of_constr (lift (-(List.length realargs)) ty))
with Not_found -> error_case_not_inductive env !evdref
{uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
in
@@ -2068,7 +2068,7 @@ let constr_of_pat env evdref arsign pat avoid =
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 IndType (indf, realargs) = find_rectype env ( !evdref) apptype in
+ let IndType (indf, realargs) = find_rectype env (!evdref) (EConstr.of_constr apptype) in
match alias with
Anonymous ->
pat', sign, app, apptype, realargs, n, avoid
@@ -2327,7 +2327,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
let t = RelDecl.get_type decl in
let argt = Retyping.get_type_of env !evdref arg in
let eq, refl_arg =
- if Reductionops.is_conv env !evdref argt t then
+ if Reductionops.is_conv env !evdref (EConstr.of_constr argt) (EConstr.of_constr t) then
(mk_eq evdref (lift (nargeqs + slift) argt)
(mkRel (nargeqs + slift))
(lift (nargeqs + nar) arg),
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 30d100af9..fd21f5bd1 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -192,13 +192,14 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab
(* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *)
let find_class_type sigma t =
- let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
- match kind_of_term t' with
- | Var id -> CL_SECVAR id, Univ.Instance.empty, args
- | Const (sp,u) -> CL_CONST sp, u, args
+ let inj = EConstr.Unsafe.to_constr in
+ let t', args = Reductionops.whd_betaiotazeta_stack sigma (EConstr.of_constr t) in
+ match EConstr.kind sigma t' with
+ | Var id -> CL_SECVAR id, Univ.Instance.empty, List.map inj args
+ | Const (sp,u) -> CL_CONST sp, u, List.map inj args
| Proj (p, c) when not (Projection.unfolded p) ->
- CL_PROJ (Projection.constant p), Univ.Instance.empty, c :: args
- | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
+ CL_PROJ (Projection.constant p), Univ.Instance.empty, List.map inj (c :: args)
+ | Ind (ind_sp,u) -> CL_IND ind_sp, u, List.map inj args
| Prod (_,_,_) -> CL_FUN, Univ.Instance.empty, []
| Sort _ -> CL_SORT, Univ.Instance.empty, []
| _ -> raise Not_found
@@ -232,7 +233,7 @@ let class_of env sigma t =
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, u, args)
with Not_found ->
- let t = Tacred.hnf_constr env sigma t in
+ let t = Tacred.hnf_constr env sigma (EConstr.of_constr t) in
let (cl, u, args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
(t, n1, i, u, args)
@@ -276,7 +277,7 @@ let apply_on_class_of env sigma t cont =
t, cont i
with Not_found ->
(* Is it worth to be more incremental on the delta steps? *)
- let t = Tacred.hnf_constr env sigma t in
+ let t = Tacred.hnf_constr env sigma (EConstr.of_constr t) in
let (cl, u, args) = find_class_type sigma t in
let (i, { cl_param = n1 } ) = class_info cl in
if not (Int.equal (List.length args) n1) then raise Not_found;
@@ -297,9 +298,9 @@ let lookup_path_to_sort_from env sigma s =
let get_coercion_constructor env coe =
let c, _ =
- Reductionops.whd_all_stack env Evd.empty coe.coe_value
+ Reductionops.whd_all_stack env Evd.empty (EConstr.of_constr coe.coe_value)
in
- match kind_of_term c with
+ match EConstr.kind Evd.empty (** FIXME *) c with
| Construct (cstr,u) ->
(cstr, Inductiveops.constructor_nrealargs cstr -1)
| _ ->
@@ -403,7 +404,7 @@ type coercion = {
let reference_arity_length ref =
let t = Universes.unsafe_type_of_global ref in
- List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty t))
+ List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
let projection_arity_length p =
let len = reference_arity_length (ConstRef p) in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index a3970fc0f..b062da1f4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -63,7 +63,7 @@ let apply_coercion_args env evd check isproj argl funj =
{ uj_val = applist (j_val funj,argl);
uj_type = typ }
| 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 typ) with
+ 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
raise NoCoercion;
@@ -95,7 +95,7 @@ let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdre
Evarutil.e_new_evar env evdref ~src c
let app_opt env evdref f t =
- whd_betaiota !evdref (app_opt f t)
+ whd_betaiota !evdref (EConstr.of_constr (app_opt f t))
let pair_of_array a = (a.(0), a.(1))
@@ -128,11 +128,11 @@ let lift_args n sign =
let mu env evdref t =
let rec aux v =
- let v' = hnf env !evdref v in
+ let v' = hnf env !evdref (EConstr.of_constr v) in
match disc_subset v' with
| Some (u, p) ->
let f, ct = aux u in
- let p = hnf_nodelta env !evdref p in
+ let p = hnf_nodelta env !evdref (EConstr.of_constr p) in
(Some (fun x ->
app_opt env evdref
f (papp evdref sig_proj1 [| u; p; x |])),
@@ -145,7 +145,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
=
let open Context.Rel.Declaration in
let rec coerce_unify env x y =
- let x = hnf env !evdref x and y = hnf env !evdref y in
+ let x = hnf env !evdref (EConstr.of_constr x) and y = hnf env !evdref (EConstr.of_constr y) in
try
evdref := the_conv_x_leq env x y !evdref;
None
@@ -153,7 +153,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env evdref x y in
let dest_prod c =
- match Reductionops.splay_prod_n env ( !evdref) 1 c with
+ match Reductionops.splay_prod_n env (!evdref) 1 (EConstr.of_constr c) with
| [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c
| _ -> raise NoSubtacCoercion
in
@@ -337,7 +337,7 @@ let app_coercion env evdref coercion v =
| None -> v
| Some f ->
let v' = Typing.e_solve_evars env evdref (f v) in
- whd_betaiota !evdref v'
+ whd_betaiota !evdref (EConstr.of_constr v')
let coerce_itf loc env evd v t c1 =
let evdref = ref evd in
@@ -373,7 +373,7 @@ let apply_coercion env sigma p hj typ_cl =
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
- let t = whd_all env evd j.uj_type in
+ let t = whd_all env evd (EConstr.of_constr j.uj_type) in
match kind_of_term t with
| Prod (_,_,_) -> (evd,j)
| Evar ev ->
@@ -414,7 +414,7 @@ let inh_tosort_force loc env evd j =
error_not_a_type ~loc env evd j
let inh_coerce_to_sort loc env evd j =
- let typ = whd_all env evd j.uj_type in
+ let typ = whd_all env evd (EConstr.of_constr j.uj_type) in
match kind_of_term typ with
| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
| Evar ev when not (is_defined evd (fst ev)) ->
@@ -466,8 +466,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
try inh_coerce_to_fail env evd rigidonly v t c1
with NoCoercion ->
match
- kind_of_term (whd_all env evd t),
- kind_of_term (whd_all env evd c1)
+ kind_of_term (whd_all env evd (EConstr.of_constr t)),
+ kind_of_term (whd_all env evd (EConstr.of_constr c1))
with
| Prod (name,t1,t2), Prod (_,u1,u2) ->
(* Conversion did not work, we may succeed with a coercion. *)
@@ -485,7 +485,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
inh_conv_coerce_to_fail loc env1 evd rigidonly
(Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
let v1 = Option.get v1 in
- let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in
+ 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
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index d7b73d333..66e690714 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -165,7 +165,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| _, _ ->
(if convert then
let sigma,c' = Evd.fresh_global env sigma ref in
- is_conv env sigma c' c
+ is_conv env sigma (EConstr.of_constr c') (EConstr.of_constr c)
else false)
in
let rec sorec ctx env subst p t =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 72cf31010..a4d943cfa 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -502,7 +502,7 @@ let rec detype flags avoid env sigma t =
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 ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty 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
substl (c :: List.rev args) body'
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 194d0b297..f54a57d57 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -78,6 +78,7 @@ type flex_kind_of_term =
| Flexible of existential
let flex_kind_of_term ts env evd c sk =
+ let c = EConstr.Unsafe.to_constr c in
match kind_of_term c with
| LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c)
@@ -88,10 +89,12 @@ let flex_kind_of_term ts env evd c sk =
| Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
| Cast _ | App _ | Case _ -> assert false
+let zip evd (c, stk) = EConstr.Unsafe.to_constr (Stack.zip evd (c, stk))
+
let apprec_nohdbeta ts env evd c =
- let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
+ let (t,sk as appr) = Reductionops.whd_nored_state evd (EConstr.of_constr c, []) in
if Stack.not_purely_applicative sk
- then Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state
+ then zip evd (fst (whd_betaiota_deltazeta_for_iota_state
ts env evd Cst_stack.empty appr))
else c
@@ -135,6 +138,8 @@ let occur_rigidly (evk,_ as ev) evd t =
projection would have been reduced) *)
let check_conv_record env sigma (t1,sk1) (t2,sk2) =
+ let t1 = EConstr.Unsafe.to_constr t1 in
+ let t2 = EConstr.Unsafe.to_constr t2 in
let (proji, u), arg = Universes.global_app_of_constr t1 in
let canon_s,sk2_effective =
try
@@ -143,7 +148,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
let _, a, b = destProd (Evarutil.nf_evar sigma t2) in
if EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) then
lookup_canonical_conversion (proji, Prod_cs),
- (Stack.append_app [|a;pop (EConstr.of_constr b)|] Stack.empty)
+ (Stack.append_app [|EConstr.of_constr a;EConstr.of_constr (pop (EConstr.of_constr b))|] Stack.empty)
else raise Not_found
| Sort s ->
lookup_canonical_conversion
@@ -162,12 +167,12 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
| Some c -> (* A primitive projection applied to c *)
let ty = Retyping.get_type_of ~lax:true env sigma c in
let (i,u), ind_args =
- try Inductiveops.find_mrectype env sigma ty
+ try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty)
with _ -> raise Not_found
- in Stack.append_app_list ind_args Stack.empty, c, sk1
+ in Stack.append_app_list (List.map EConstr.of_constr ind_args) Stack.empty, c, sk1
| None ->
match Stack.strip_n_app nparams sk1 with
- | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
+ | Some (params1, c1, extra_args1) -> params1, EConstr.Unsafe.to_constr c1, extra_args1
| _ -> raise Not_found in
let us2,extra_args2 =
let l_us = List.length us in
@@ -180,9 +185,9 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
let t' = subst_univs_level_constr subst t' in
let bs' = List.map (subst_univs_level_constr subst) bs in
let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in
- ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
- (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
- (n,Stack.zip(t2,sk2))
+ ctx',(h, t2),c',bs',(Stack.append_app_list (List.map EConstr.of_constr params) Stack.empty,params1),
+ (Stack.append_app_list (List.map EConstr.of_constr us) Stack.empty,us2),(extra_args1,extra_args2),c1,
+ (n, zip sigma (EConstr.of_constr t2,sk2))
(* Precondition: one of the terms of the pb is an uninstantiated evar,
* possibly applied to arguments. *)
@@ -212,10 +217,11 @@ let ise_exact ise x1 x2 =
| Some _, Success i -> UnifFailure (i,NotSameArgSize)
let ise_array2 evd f v1 v2 =
+ let inj c = EConstr.Unsafe.to_constr c in
let rec allrec i = function
| -1 -> Success i
| n ->
- match f i v1.(n) v2.(n) with
+ match f i (inj v1.(n)) (inj v2.(n)) with
| Success i' -> allrec i' (n-1)
| UnifFailure _ as x -> x in
let lv1 = Array.length v1 in
@@ -225,28 +231,35 @@ let ise_array2 evd f v1 v2 =
(* Applicative node of stack are read from the outermost to the innermost
but are unified the other way. *)
let rec ise_app_stack2 env f evd sk1 sk2 =
+ let inj = EConstr.Unsafe.to_constr in
match sk1,sk2 with
| Stack.App node1 :: q1, Stack.App node2 :: q2 ->
let (t1,l1) = Stack.decomp_node_last node1 q1 in
let (t2,l2) = Stack.decomp_node_last node2 q2 in
begin match ise_app_stack2 env f evd l1 l2 with
|(_,UnifFailure _) as x -> x
- |x,Success i' -> x,f env i' CONV t1 t2
+ |x,Success i' -> x,f env i' CONV (inj t1) (inj t2)
end
| _, _ -> (sk1,sk2), Success evd
+let push_rec_types pfix env =
+ let (i, c, t) = pfix in
+ let inj c = EConstr.Unsafe.to_constr c in
+ push_rec_types (i, Array.map inj c, Array.map inj t) env
+
(* This function tries to unify 2 stacks element by element. It works
from the end to the beginning. If it unifies a non empty suffix of
stacks but not the entire stacks, the first part of the answer is
Some(the remaining prefixes to tackle)) *)
let ise_stack2 no_app env evd f sk1 sk2 =
+ let inj = EConstr.Unsafe.to_constr in
let rec ise_stack2 deep i sk1 sk2 =
let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i
else None, x in
match sk1, sk2 with
| [], [] -> None, Success i
| Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 ->
- (match f env i CONV t1 t2 with
+ (match f env i CONV (inj t1) (inj t2) with
| Success i' ->
(match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
| Success i'' -> ise_stack2 true i'' q1 q2
@@ -279,6 +292,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
(* Make sure that the matching suffix is the all stack *)
let exact_ise_stack2 env evd f sk1 sk2 =
+ let inj = EConstr.Unsafe.to_constr in
let rec ise_stack2 i sk1 sk2 =
match sk1, sk2 with
| [], [] -> Success i
@@ -286,7 +300,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
ise_and i [
(fun i -> ise_stack2 i q1 q2);
(fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
- (fun i -> f env i CONV t1 t2)]
+ (fun i -> f env i CONV (inj t1) (inj t2))]
| Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -344,19 +358,19 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
let term2 = apprec_nohdbeta (fst ts) env evd term2 in
let default () =
evar_eqappr_x ts env evd pbty
- (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
- (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
+ (whd_nored_state evd (EConstr.of_constr term1,Stack.empty), Cst_stack.empty)
+ (whd_nored_state evd (EConstr.of_constr term2,Stack.empty), Cst_stack.empty)
in
begin match kind_of_term term1, kind_of_term term2 with
| Evar ev, _ when Evd.is_undefined evd (fst ev) ->
(match solve_simple_eqn (evar_conv_x ts) env evd
- (position_problem true pbty,ev,term2) with
+ (position_problem true pbty,ev, EConstr.of_constr term2) with
| UnifFailure (_,OccurCheck _) ->
(* Eta-expansion might apply *) default ()
| x -> x)
| _, Evar ev when Evd.is_undefined evd (fst ev) ->
(match solve_simple_eqn (evar_conv_x ts) env evd
- (position_problem false pbty,ev,term1) with
+ (position_problem false pbty,ev, EConstr.of_constr term1) with
| UnifFailure (_, OccurCheck _) ->
(* Eta-expansion might apply *) default ()
| x -> x)
@@ -369,23 +383,25 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
UnifFailure (i, NotSameHead)
in
let miller_pfenning on_left fallback ev lF tM evd =
+ let lF = List.map EConstr.Unsafe.to_constr lF in
match is_unification_pattern_evar env evd ev lF tM with
| None -> fallback ()
| Some l1' -> (* Miller-Pfenning's patterns unification *)
let t2 = nf_evar evd tM in
let t2 = solve_pattern_eqn env evd l1' t2 in
solve_simple_eqn (evar_conv_x ts) env evd
- (position_problem on_left pbty,ev,t2)
+ (position_problem on_left pbty,ev, EConstr.of_constr t2)
in
let consume_stack on_left (termF,skF) (termO,skO) evd =
+ let inj = EConstr.Unsafe.to_constr in
let switch f a b = if on_left then f a b else f b a in
let not_only_app = Stack.not_purely_applicative skO in
match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with
|Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
- switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
+ switch (evar_conv_x ts env i' pbty) (zip evd (termF,l)) (zip evd (termO,r))
|Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
- switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
- |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
+ switch (evar_conv_x ts env i' pbty) (zip evd (termF,l)) (zip evd (termO,r))
+ |None, Success i' -> switch (evar_conv_x ts env i' pbty) (inj termF) (inj termO)
|_, (UnifFailure _ as x) -> x
|Some _, _ -> UnifFailure (evd,NotSameArgSize) in
let eta env evd onleft sk term sk' term' =
@@ -394,15 +410,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let c = nf_evar evd c1 in
let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
let out1 = whd_betaiota_deltazeta_for_iota_state
- (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
+ (fst ts) env' evd Cst_stack.empty (EConstr.of_constr c'1, Stack.empty) in
let out2 = whd_nored_state evd
- (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty),
+ (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
Cst_stack.empty in
if onleft then evar_eqappr_x ts env' evd CONV out1 out2
else evar_eqappr_x ts env' evd CONV out2 out1
in
let rigids env evd sk term sk' term' =
- let univs = Universes.eq_constr_universes term term' in
+ let univs = EConstr.eq_constr_universes evd term term' in
match univs with
| Some univs ->
ise_and evd [(fun i ->
@@ -420,10 +436,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
match Stack.list_of_app_stack skF with
| None -> quick_fail evd
| Some lF ->
- let tM = Stack.zip apprM in
+ let tM = zip evd apprM in
miller_pfenning on_left
(fun () -> if not_only_app then (* Postpone the use of an heuristic *)
- switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM
+ switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (zip evd apprF) tM
else quick_fail i)
ev lF tM i
and consume (termF,skF as apprF) (termM,skM as apprM) i =
@@ -437,7 +453,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in
let default i = ise_try i [f1; consume apprF apprM; delta]
in
- match kind_of_term termM with
+ match EConstr.kind evd termM with
| Proj (p, c) when not (Stack.is_empty skF) ->
(* Might be ?X args = p.c args', and we have to eta-expand the
primitive projection if |args| >= |args'|+1. *)
@@ -448,10 +464,10 @@ 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 c [] in
+ let termM' = Retyping.expand_projection env evd p (EConstr.Unsafe.to_constr c) [] in
let apprM', cstsM' =
whd_betaiota_deltazeta_for_iota_state
- (fst ts) env evd cstsM (termM',skM)
+ (fst ts) env evd cstsM (EConstr.of_constr termM',skM)
in
let delta' i =
switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM')
@@ -467,9 +483,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
let switch f a b = if on_left then f a b else f b a in
let eta evd =
- match kind_of_term termR with
+ match EConstr.kind evd termR with
| Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
- eta env evd false skR termR skF termF
+ eta env evd false skR (EConstr.Unsafe.to_constr termR) skF termF
| Construct u -> eta_constructor ts env evd skR u skF termF
| _ -> UnifFailure (evd,NotSameHead)
in
@@ -477,7 +493,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| None ->
ise_try evd [consume_stack on_left apprF apprR; eta]
| Some lF ->
- let tR = Stack.zip apprR in
+ let tR = zip evd apprR in
miller_pfenning on_left
(fun () ->
ise_try evd
@@ -487,10 +503,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let i,tF =
if isRel tR || isVar tR then
(* Optimization so as to generate candidates *)
- let i,ev = evar_absorb_arguments env i ev lF in
+ let i,ev = evar_absorb_arguments env i ev (List.map EConstr.Unsafe.to_constr lF) in
i,mkEvar ev
else
- i,Stack.zip apprF in
+ i,zip evd apprF in
switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
tF tR
else
@@ -516,20 +532,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let ev1' = whd_evar i' (mkEvar ev1) in
if isEvar ev1' then
solve_simple_eqn (evar_conv_x ts) env i'
- (position_problem true pbty,destEvar ev1',term2)
+ (position_problem true pbty,destEvar ev1', term2)
else
evar_eqappr_x ts env evd pbty
- ((ev1', sk1), csts1) ((term2, sk2), csts2)
+ ((EConstr.of_constr ev1', sk1), csts1) ((term2, sk2), csts2)
| Some (r,[]), Success i' ->
(* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
(* we now unify r[?ev1] and ?ev2 *)
let ev2' = whd_evar i' (mkEvar ev2) in
if isEvar ev2' then
solve_simple_eqn (evar_conv_x ts) env i'
- (position_problem false pbty,destEvar ev2',Stack.zip(term1,r))
+ (position_problem false pbty,destEvar ev2',Stack.zip evd (term1,r))
else
evar_eqappr_x ts env evd pbty
- ((ev2', sk1), csts1) ((term2, sk2), csts2)
+ ((EConstr.of_constr ev2', sk1), csts1) ((term2, sk2), csts2)
| Some ([],r), Success i' ->
(* Symmetrically *)
(* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
@@ -537,9 +553,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let ev1' = whd_evar i' (mkEvar ev1) in
if isEvar ev1' then
solve_simple_eqn (evar_conv_x ts) env i'
- (position_problem true pbty,destEvar ev1',Stack.zip(term2,r))
+ (position_problem true pbty,destEvar ev1',Stack.zip evd (term2,r))
else evar_eqappr_x ts env evd pbty
- ((ev1', sk1), csts1) ((term2, sk2), csts2)
+ ((EConstr.of_constr ev1', sk1), csts1) ((term2, sk2), csts2)
| None, (UnifFailure _ as x) ->
(* sk1 and sk2 have no common outer part *)
if Stack.not_purely_applicative sk2 then
@@ -584,13 +600,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ise_try evd [f1; f2]
| Flexible ev1, MaybeFlexible v2 ->
- flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2
+ flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) (EConstr.of_constr v2)
| MaybeFlexible v1, Flexible ev2 ->
- flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1
+ flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) (EConstr.of_constr v1)
| MaybeFlexible v1, MaybeFlexible v2 -> begin
- match kind_of_term term1, kind_of_term term2 with
+ match kind_of_term (EConstr.Unsafe.to_constr term1), kind_of_term (EConstr.Unsafe.to_constr term2) with
| LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
let f1 i = (* FO *)
ise_and i
@@ -605,8 +621,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
and f2 i =
- let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
- and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
+ let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (EConstr.of_constr v1,sk1)
+ and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (EConstr.of_constr v2,sk2)
in evar_eqappr_x ts env i pbty out1 out2
in
ise_try evd [f1; f2]
@@ -618,8 +634,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
[(fun i -> evar_conv_x ts env i CONV c c');
(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
and f2 i =
- let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
- and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
+ let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (EConstr.of_constr v1,sk1)
+ and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (EConstr.of_constr v2,sk2)
in evar_eqappr_x ts env i pbty out1 out2
in
ise_try evd [f1; f2]
@@ -627,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 (destApp (Retyping.expand_projection env evd p c []))
+ try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p c [])))
with Retyping.RetypeError _ -> None
in
(match res with
@@ -638,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 (destApp (Retyping.expand_projection env evd p' c' []))
+ try Some (EConstr.destApp evd (EConstr.of_constr (Retyping.expand_projection env evd p' c' [])))
with Retyping.RetypeError _ -> None
in
(match res with
@@ -653,7 +669,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
allow this identification (first-order unification of universes). Otherwise
fallback to unfolding.
*)
- let univs = Universes.eq_constr_universes term1 term2 in
+ let univs = EConstr.eq_constr_universes evd term1 term2 in
match univs with
| Some univs ->
ise_and i [(fun i ->
@@ -675,7 +691,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
if the first argument is a beta-redex (expand a constant
only if necessary) or the second argument is potentially
usable as a canonical projection or canonical value *)
- let rec is_unnamed (hd, args) = match kind_of_term hd with
+ let rec is_unnamed (hd, args) = match EConstr.kind i hd with
| (Var _|Construct _|Ind _|Const _|Prod _|Sort _) ->
Stack.not_purely_applicative args
| (CoFix _|Meta _|Rel _)-> true
@@ -684,7 +700,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| Lambda _ -> assert (match args with [] -> true | _ -> false); true
| LetIn (_,b,_,c) -> is_unnamed
(fst (whd_betaiota_deltazeta_for_iota_state
- (fst ts) env i Cst_stack.empty (subst1 b c, args)))
+ (fst ts) env i Cst_stack.empty (EConstr.Vars.subst1 b c, args)))
| Fix _ -> true (* Partially applied fix can be the result of a whd call *)
| Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args
| Case _ | App _| Cast _ -> assert false in
@@ -692,34 +708,35 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let applicative_stack = fst (Stack.strip_app sk2) in
is_unnamed
(fst (whd_betaiota_deltazeta_for_iota_state
- (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in
+ (fst ts) env i Cst_stack.empty (EConstr.of_constr v2, applicative_stack))) in
let rhs_is_already_stuck =
rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
- if (isLambda term1 || rhs_is_already_stuck)
+ if (EConstr.isLambda i term1 || rhs_is_already_stuck)
&& (not (Stack.not_purely_applicative sk1)) then
evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
(whd_betaiota_deltazeta_for_iota_state
- (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+ (fst ts) env i (Cst_stack.add_cst term1 csts1) (EConstr.of_constr v1,sk1))
(appr2,csts2)
else
evar_eqappr_x ts env i pbty (appr1,csts1)
(whd_betaiota_deltazeta_for_iota_state
- (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+ (fst ts) env i (Cst_stack.add_cst term2 csts2) (EConstr.of_constr v2,sk2))
in
ise_try evd [f1; f2; f3]
end
- | Rigid, Rigid when isLambda term1 && isLambda term2 ->
- let (na1,c1,c'1) = destLambda term1 in
- let (na2,c2,c'2) = destLambda term2 in
+ | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 ->
+ let (na1,c1,c'1) = EConstr.destLambda evd term1 in
+ let (na2,c2,c'2) = EConstr.destLambda evd term2 in
+ let inj = EConstr.Unsafe.to_constr in
assert app_empty;
ise_and evd
- [(fun i -> evar_conv_x ts env i CONV c1 c2);
+ [(fun i -> evar_conv_x ts env i CONV (inj c1) (inj c2));
(fun i ->
- let c = nf_evar i c1 in
+ let c = nf_evar i (inj c1) in
let na = Nameops.name_max na1 na2 in
- evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
+ evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV (inj c'1) (inj c'2))]
| Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
| Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
@@ -733,7 +750,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
and f4 i =
evar_eqappr_x ts env i pbty
(whd_betaiota_deltazeta_for_iota_state
- (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
+ (fst ts) env i (Cst_stack.add_cst term1 csts1) (EConstr.of_constr v1,sk1))
(appr2,csts2)
in
ise_try evd [f3; f4]
@@ -747,19 +764,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
and f4 i =
evar_eqappr_x ts env i pbty (appr1,csts1)
(whd_betaiota_deltazeta_for_iota_state
- (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+ (fst ts) env i (Cst_stack.add_cst term2 csts2) (EConstr.of_constr v2,sk2))
in
ise_try evd [f3; f4]
(* Eta-expansion *)
- | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
- eta env evd true sk1 term1 sk2 term2
+ | Rigid, _ when EConstr.isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
+ eta env evd true sk1 (EConstr.Unsafe.to_constr term1) sk2 term2
- | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
- eta env evd false sk2 term2 sk1 term1
+ | _, Rigid when EConstr.isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
+ eta env evd false sk2 (EConstr.Unsafe.to_constr term2) sk1 term1
| Rigid, Rigid -> begin
- match kind_of_term term1, kind_of_term term2 with
+ let inj = EConstr.Unsafe.to_constr in
+ match EConstr.kind evd term1, EConstr.kind evd term2 with
| Sort s1, Sort s2 when app_empty ->
(try
@@ -774,11 +792,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
ise_and evd
- [(fun i -> evar_conv_x ts env i CONV c1 c2);
+ [(fun i -> evar_conv_x ts env i CONV (inj c1) (inj c2));
(fun i ->
- let c = nf_evar i c1 in
+ let c = nf_evar i (inj c1) in
let na = Nameops.name_max n1 n2 in
- evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
+ evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty (inj c'1) (inj c'2))]
| Rel x1, Rel x2 ->
if Int.equal x1 x2 then
@@ -822,10 +840,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else UnifFailure (evd,NotSameHead)
| (Meta _, _) | (_, Meta _) ->
+ let inj = EConstr.Unsafe.to_constr in
begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with
|_, (UnifFailure _ as x) -> x
- |None, Success i' -> evar_conv_x ts env i' CONV term1 term2
- |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2'))
+ |None, Success i' -> evar_conv_x ts env i' CONV (inj term1) (inj term2)
+ |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (inj (Stack.zip i' (term1,sk1'))) (inj (Stack.zip i' (term2,sk2')))
end
| (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ ->
@@ -905,8 +924,8 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
(try
let l1' = Stack.tail pars sk1 in
let l2' =
- let term = Stack.zip (term2,sk2) in
- List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs)
+ let term = Stack.zip evd (term2,sk2) in
+ List.map (fun p -> EConstr.mkProj (Projection.make p false, term)) (Array.to_list projs)
in
exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1'
(Stack.append_app_list l2' Stack.empty)
@@ -938,14 +957,14 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) =
let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in
ise_and evd
(* First compare extra args for better failure message *)
- [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
+ [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) (Array.map EConstr.of_constr rest2) (Array.map EConstr.of_constr l1));
(fun i ->
(* Then instantiate evar unless already done by unifying args *)
let t2 = mkApp(term2,deb2) in
if is_defined i (fst ev1) then
evar_conv_x ts env i CONV t2 (mkEvar ev1)
else
- solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))]
+ solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1, EConstr.of_constr t2))]
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find_undefined evd evk in
@@ -1153,7 +1172,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let reason = ProblemBeyondCapabilities in
UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
| Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
- let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
+ let f env evd pbty x y = is_fconv ~reds:ts pbty env evd (EConstr.of_constr x) (EConstr.of_constr y) in
Success (solve_refl ~can_drop:true f env evd
(position_problem true pbty) evk1 args1 args2)
| Evar ev1, Evar ev2 when app_empty ->
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 14947c892..6f736e562 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -43,11 +43,11 @@ val check_problems_are_solved : env -> evar_map -> unit
(** Check if a canonical structure is applicable *)
val check_conv_record : env -> evar_map ->
- constr * types Stack.t -> constr * types Stack.t ->
+ state -> state ->
Univ.universe_context_set * (constr * constr)
- * constr * constr list * (constr Stack.t * constr Stack.t) *
- (constr Stack.t * types Stack.t) *
- (constr Stack.t * types Stack.t) * constr *
+ * constr * constr list * (EConstr.t Stack.t * EConstr.t Stack.t) *
+ (EConstr.t Stack.t * EConstr.t Stack.t) *
+ (EConstr.t Stack.t * EConstr.t Stack.t) * constr *
(int option * constr)
(** Try to solve problems of the form ?x[args] = c by second-order
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 06f619410..3982edd1c 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -33,7 +33,7 @@ let env_nf_evar sigma env =
let env_nf_betaiotaevar sigma env =
process_rel_context
(fun d e ->
- push_rel (RelDecl.map_constr (Reductionops.nf_betaiota sigma) d) e) env
+ push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma (EConstr.of_constr c)) d) e) env
(****************************************)
(* Operations on value/type constraints *)
@@ -78,7 +78,7 @@ let define_pure_evar_as_product evd evk =
let evi = Evd.find_undefined evd evk in
let evenv = evar_env evi in
let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
- let concl = Reductionops.whd_all evenv evd evi.evar_concl in
+ let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
let s = destSort concl in
let evd1,(dom,u1) =
let evd = Sigma.Unsafe.of_evar_map evd in
@@ -131,7 +131,7 @@ let define_pure_evar_as_lambda env evd evk =
let open Context.Named.Declaration in
let evi = Evd.find_undefined evd evk in
let evenv = evar_env evi in
- let typ = Reductionops.whd_all evenv evd (evar_concl evi) in
+ let typ = Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi)) in
let evd1,(na,dom,rng) = match kind_of_term typ with
| Prod (na,dom,rng) -> (evd,(na,dom,rng))
| Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
@@ -169,7 +169,7 @@ let define_evar_as_sort env evd (ev,args) =
let evd, u = new_univ_variable univ_rigid evd in
let evi = Evd.find_undefined evd ev in
let s = Type u in
- let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in
+ let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in
let sort = destSort concl in
let evd' = Evd.define ev (mkSort s) evd in
Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
@@ -181,7 +181,7 @@ let define_evar_as_sort env evd (ev,args) =
let split_tycon loc env evd tycon =
let rec real_split evd c =
- let t = Reductionops.whd_all env evd c in
+ let t = Reductionops.whd_all env evd (EConstr.of_constr c) in
match kind_of_term t with
| Prod (na,dom,rng) -> evd, (na, dom, rng)
| Evar ev (* ev is undefined because of whd_all *) ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ea3ab17a7..17bb1406e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -145,7 +145,7 @@ let recheck_applications conv_algo env evdref t =
let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in
let rec aux i ty =
if i < Array.length argsty then
- match kind_of_term (whd_all env !evdref ty) with
+ match kind_of_term (whd_all env !evdref (EConstr.of_constr ty)) with
| Prod (na, dom, codom) ->
(match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with
| Success evd -> evdref := evd;
@@ -525,7 +525,7 @@ let solve_pattern_eqn env sigma l c =
l c in
(* Warning: we may miss some opportunity to eta-reduce more since c'
is not in normal form *)
- shrink_eta c'
+ shrink_eta (EConstr.of_constr c')
(*****************************************)
(* Refining/solving unification problems *)
@@ -683,7 +683,7 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
List.filter (fun (args',id) ->
(* is_conv is maybe too strong (and source of useless computation) *)
(* (at least expansion of aliases is needed) *)
- Array.for_all2 (is_conv env evd) args args') l in
+ Array.for_all2 (fun c1 c2 -> is_conv env evd (EConstr.of_constr c1) (EConstr.of_constr c2)) args args') l in
List.map snd l
with Not_found ->
[]
@@ -808,7 +808,7 @@ let rec do_projection_effects define_fun env ty evd = function
let evd = Evd.define evk (mkVar id) evd in
(* TODO: simplify constraints involving evk *)
let evd = do_projection_effects define_fun env ty evd p in
- let ty = whd_all env evd (Lazy.force ty) in
+ let ty = whd_all env evd (EConstr.of_constr (Lazy.force ty)) in
if not (isSort ty) then
(* Don't try to instantiate if a sort because if evar_concl is an
evar it may commit to a univ level which is not the right
@@ -1484,7 +1484,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
self envk (EConstr.of_constr t))
in
- let rhs = whd_beta evd rhs (* heuristic *) in
+ let rhs = whd_beta evd (EConstr.of_constr rhs) (* heuristic *) in
let fast rhs =
let filter_ctxt = evar_filtered_context evi in
let names = ref Idset.empty in
@@ -1566,10 +1566,10 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
raise e
| OccurCheckIn (evd,rhs) ->
(* last chance: rhs actually reduces to ev *)
- let c = whd_all env evd rhs in
+ let c = whd_all env evd (EConstr.of_constr rhs) in
match kind_of_term c with
| Evar (evk',argsv2) when Evar.equal evk evk' ->
- solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
+ solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma (EConstr.of_constr c) (EConstr.of_constr c'))
env evd pbty evk argsv argsv2
| _ ->
raise (OccurCheckIn (evd,rhs))
@@ -1638,5 +1638,5 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
| IllTypedInstance (env,t,u) ->
UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))
| IncompatibleCandidates ->
- UnifFailure (evd,ConversionFailed (env,mkEvar ev1,t2))
+ UnifFailure (evd,ConversionFailed (env,mkEvar ev1, EConstr.Unsafe.to_constr t2))
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index cf059febf..70e94b4dc 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -52,7 +52,7 @@ val solve_evar_evar : ?force:bool ->
env -> evar_map -> bool option -> existential -> existential -> evar_map
val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
- bool option * existential * constr -> unification_result
+ bool option * existential * EConstr.t -> unification_result
val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 9cf91a947..4025ca8b8 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -153,7 +153,9 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let nparams = List.length vargs in
let process_pos env depK pk =
let rec prec env i sign p =
- let p',largs = whd_allnolet_stack env sigma p in
+ let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in
+ let p' = EConstr.Unsafe.to_constr p' in
+ let largs = List.map EConstr.Unsafe.to_constr largs in
match kind_of_term p' with
| Prod (n,t,c) ->
let d = LocalAssum (n,t) in
@@ -170,7 +172,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
else
base
| _ ->
- let t' = whd_all env sigma p in
+ let t' = whd_all env sigma (EConstr.of_constr p) in
if Term.eq_constr p' t' then assert false
else prec env i sign t'
in
@@ -229,7 +231,9 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
let process_pos env fk =
let rec prec env i hyps p =
- let p',largs = whd_allnolet_stack env sigma p in
+ let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in
+ let p' = EConstr.Unsafe.to_constr p' in
+ let largs = List.map EConstr.Unsafe.to_constr largs in
match kind_of_term p' with
| Prod (n,t,c) ->
let d = LocalAssum (n,t) in
@@ -242,7 +246,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in
applist(lift i fk,realargs@[arg])
| _ ->
- let t' = whd_all env sigma p in
+ let t' = whd_all env sigma (EConstr.of_constr p) in
if Term.eq_constr t' p' then assert false
else prec env i hyps t'
in
@@ -261,7 +265,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
| None ->
mkLambda_name env
(n,t,process_constr (push_rel d env) (i+1)
- (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
+ (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)]))))
(cprest,rest))
| Some(_,f_0) ->
let nF = lift (i+1+decF) f_0 in
@@ -269,7 +273,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
let arg = process_pos env' nF (lift 1 t) in
mkLambda_name env
(n,t,process_constr env' (i+1)
- (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
+ (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg]))))
(cprest,rest)))
| (LocalDef (n,c,t) as d)::cprest, rest ->
mkLetIn
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 29f57144a..a3cca2ad8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -444,15 +444,17 @@ let build_branch_type env dep p cs =
(**************************************************)
-let extract_mrectype t =
- let (t, l) = decompose_app t in
- match kind_of_term t with
- | Ind ind -> (ind, l)
+let extract_mrectype sigma t =
+ let open EConstr in
+ let (t, l) = decompose_app sigma t in
+ match EConstr.kind sigma t with
+ | Ind ind -> (ind, List.map EConstr.Unsafe.to_constr l)
| _ -> raise Not_found
let find_mrectype_vect env sigma c =
- let (t, l) = decompose_appvect (whd_all env sigma c) in
- match kind_of_term t with
+ let open EConstr in
+ let (t, l) = Termops.decompose_app_vect sigma (EConstr.of_constr (whd_all env sigma c)) in
+ match EConstr.kind sigma (EConstr.of_constr t) with
| Ind ind -> (ind, l)
| _ -> raise Not_found
@@ -460,28 +462,34 @@ let find_mrectype env sigma c =
let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v)
let find_rectype env sigma c =
- let (t, l) = decompose_app (whd_all env sigma c) in
- match kind_of_term t with
+ let open EConstr in
+ let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+ match EConstr.kind sigma t with
| Ind (ind,u as indu) ->
let (mib,mip) = Inductive.lookup_mind_specif env ind in
if mib.mind_nparams > List.length l then raise Not_found;
+ let l = List.map EConstr.Unsafe.to_constr l in
let (par,rargs) = List.chop mib.mind_nparams l in
IndType((indu, par),rargs)
| _ -> raise Not_found
let find_inductive env sigma c =
- let (t, l) = decompose_app (whd_all env sigma c) in
- match kind_of_term t with
+ let open EConstr in
+ let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+ match EConstr.kind sigma t with
| Ind ind
when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
+ let l = List.map EConstr.Unsafe.to_constr l in
(ind, l)
| _ -> raise Not_found
let find_coinductive env sigma c =
- let (t, l) = decompose_app (whd_all env sigma c) in
- match kind_of_term t with
+ let open EConstr in
+ let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in
+ match EConstr.kind sigma t with
| Ind ind
when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
+ let l = List.map EConstr.Unsafe.to_constr l in
(ind, l)
| _ -> raise Not_found
@@ -490,12 +498,12 @@ let find_coinductive env sigma c =
(* find appropriate names for pattern variables. Useful in the Case
and Inversion (case_then_using et case_nodep_then_using) tactics. *)
-let is_predicate_explicitly_dep env pred arsign =
+let is_predicate_explicitly_dep env sigma pred arsign =
let rec srec env pval arsign =
- let pv' = whd_all env Evd.empty pval in
- match kind_of_term pv', arsign with
+ let pv' = EConstr.of_constr (whd_all env sigma pval) in
+ match EConstr.kind sigma pv', arsign with
| Lambda (na,t,b), (LocalAssum _)::arsign ->
- srec (push_rel_assum (na,t) env) b arsign
+ srec (push_rel_assum (na, EConstr.Unsafe.to_constr t) env) b arsign
| Lambda (na,_,t), _ ->
(* The following code has an impact on the introduction names
@@ -525,11 +533,11 @@ let is_predicate_explicitly_dep env pred arsign =
| _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate")
in
- srec env pred arsign
+ srec env (EConstr.of_constr pred) arsign
-let is_elim_predicate_explicitly_dependent env pred indf =
+let is_elim_predicate_explicitly_dependent env sigma pred indf =
let arsign,_ = get_arity env indf in
- is_predicate_explicitly_dep env pred arsign
+ is_predicate_explicitly_dep env sigma pred arsign
let set_names env n brty =
let (ctxt,cl) = decompose_prod_n_assum n brty in
@@ -545,7 +553,7 @@ let set_pattern_names env ind brv =
mip.mind_nf_lc in
Array.map2 (set_names env) arities brv
-let type_case_branches_with_names env indspec p c =
+let type_case_branches_with_names env sigma indspec p c =
let (ind,args) = indspec in
let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
@@ -554,7 +562,7 @@ let type_case_branches_with_names env indspec p c =
(* Build case type *)
let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
(* Adjust names *)
- if is_elim_predicate_explicitly_dependent env p (ind,params) then
+ if is_elim_predicate_explicitly_dependent env sigma p (ind,params) then
(set_pattern_names env (fst ind) lbrty, conclty)
else (lbrty, conclty)
@@ -600,7 +608,7 @@ 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
| TemplateArity ar ->
- let _,scl = Reduction.dest_arity env conclty in
+ let _,scl = splay_arity env sigma conclty in
let ctx = List.rev mip.mind_arity_ctxt in
let evdref = ref sigma in
let ctx =
@@ -609,6 +617,7 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
!evdref, mkArity (List.rev ctx,scl)
let type_of_projection_knowing_arg env sigma p c ty =
+ let c = EConstr.Unsafe.to_constr c in
let IndType(pars,realargs) =
try find_rectype env sigma ty
with Not_found ->
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7bd616591..1cfdef6e5 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -130,7 +130,7 @@ val has_dependent_elim : mutual_inductive_body -> bool
val projection_nparams : projection -> int
val projection_nparams_env : env -> projection -> int
val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
- constr -> types -> types
+ EConstr.t -> EConstr.types -> types
(** Extract information from an inductive family *)
@@ -161,12 +161,12 @@ val make_arity : env -> bool -> inductive_family -> sorts -> types
val build_branch_type : env -> bool -> constr -> constructor_summary -> types
(** Raise [Not_found] if not given a valid inductive type *)
-val extract_mrectype : constr -> pinductive * constr list
-val find_mrectype : env -> evar_map -> types -> pinductive * constr list
-val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array
-val find_rectype : env -> evar_map -> types -> inductive_type
-val find_inductive : env -> evar_map -> types -> pinductive * constr list
-val find_coinductive : env -> evar_map -> types -> pinductive * constr list
+val extract_mrectype : evar_map -> EConstr.t -> pinductive * constr list
+val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * constr list
+val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * constr array
+val find_rectype : env -> evar_map -> EConstr.types -> inductive_type
+val find_inductive : env -> evar_map -> EConstr.types -> pinductive * constr list
+val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list
(********************)
@@ -175,7 +175,7 @@ val arity_of_case_predicate :
env -> inductive_family -> bool -> sorts -> types
val type_case_branches_with_names :
- env -> pinductive * constr list -> constr -> constr -> types array * types
+ env -> evar_map -> pinductive * constr list -> constr -> constr -> types array * types
(** Annotation for cases *)
val make_case_info : env -> inductive -> case_style -> case_info
@@ -195,7 +195,7 @@ i*)
(********************)
val type_of_inductive_knowing_conclusion :
- env -> evar_map -> Inductive.mind_specif puniverses -> types -> evar_map * types
+ env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * types
(********************)
val control_only_guard : env -> types -> unit
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 1e5f12b20..e45c920a3 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -92,13 +92,13 @@ let construct_of_constr_const env tag typ =
let construct_of_constr_block = construct_of_constr false
-let build_branches_type env (mind,_ as _ind) mib mip u params dep p =
+let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
let rtbl = mip.mind_reloc_tbl in
(* [build_one_branch i cty] construit le type de la ieme branche (commence
a 0) et les lambda correspondant aux realargs *)
let build_one_branch i cty =
let typi = type_constructor mind mib u cty params in
- let decl,indapp = Reductionops.splay_prod env Evd.empty typi in
+ let decl,indapp = Reductionops.splay_prod env sigma (EConstr.of_constr typi) in
let decl_with_letin,_ = decompose_prod_assum typi in
let ind,cargs = find_rectype_a env indapp in
let nparams = Array.length params in
@@ -172,9 +172,9 @@ let branch_of_switch lvl ans bs =
bs ci in
Array.init (Array.length tbl) branch
-let rec nf_val env v typ =
+let rec nf_val env sigma v typ =
match kind_of_value v with
- | Vaccu accu -> nf_accu env accu
+ | Vaccu accu -> nf_accu env sigma accu
| Vfun f ->
let lvl = nb_rel env in
let name,dom,codom =
@@ -184,44 +184,44 @@ let rec nf_val env v typ =
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
let env = push_rel (LocalAssum (name,dom)) env in
- let body = nf_val env (f (mk_rel_accu lvl)) codom in
+ let body = nf_val env sigma (f (mk_rel_accu lvl)) codom in
mkLambda(name,dom,body)
| Vconst n -> construct_of_constr_const env n typ
| Vblock b ->
let capp,ctyp = construct_of_constr_block env (block_tag b) typ in
- let args = nf_bargs env b ctyp in
+ let args = nf_bargs env sigma b ctyp in
mkApp(capp,args)
-and nf_type env v =
+and nf_type env sigma v =
match kind_of_value v with
- | Vaccu accu -> nf_accu env accu
+ | Vaccu accu -> nf_accu env sigma accu
| _ -> assert false
-and nf_type_sort env v =
+and nf_type_sort env sigma v =
match kind_of_value v with
| Vaccu accu ->
- let t,s = nf_accu_type env accu in
+ let t,s = nf_accu_type env sigma accu in
let s = try destSort s with DestKO -> assert false in
t, s
| _ -> assert false
-and nf_accu env accu =
+and nf_accu env sigma accu =
let atom = atom_of_accu accu in
- if Int.equal (accu_nargs accu) 0 then nf_atom env atom
+ if Int.equal (accu_nargs accu) 0 then nf_atom env sigma atom
else
- let a,typ = nf_atom_type env atom in
- let _, args = nf_args env accu typ in
+ let a,typ = nf_atom_type env sigma atom in
+ let _, args = nf_args env sigma accu typ in
mkApp(a,Array.of_list args)
-and nf_accu_type env accu =
+and nf_accu_type env sigma accu =
let atom = atom_of_accu accu in
- if Int.equal (accu_nargs accu) 0 then nf_atom_type env atom
+ if Int.equal (accu_nargs accu) 0 then nf_atom_type env sigma atom
else
- let a,typ = nf_atom_type env atom in
- let t, args = nf_args env accu typ in
+ let a,typ = nf_atom_type env sigma atom in
+ let t, args = nf_args env sigma accu typ in
mkApp(a,Array.of_list args), t
-and nf_args env accu t =
+and nf_args env sigma accu t =
let aux arg (t,l) =
let _,dom,codom =
try decompose_prod env t with
@@ -229,13 +229,13 @@ and nf_args env accu t =
CErrors.anomaly
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
- let c = nf_val env arg dom in
+ let c = nf_val env sigma arg dom in
(subst1 c codom, c::l)
in
let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in
t, List.rev l
-and nf_bargs env b t =
+and nf_bargs env sigma b t =
let t = ref t in
let len = block_size b in
Array.init len
@@ -246,10 +246,10 @@ and nf_bargs env b t =
CErrors.anomaly
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
- let c = nf_val env (block_field b i) dom in
+ let c = nf_val env sigma (block_field b i) dom in
t := subst1 c codom; c)
-and nf_atom env atom =
+and nf_atom env sigma atom =
match atom with
| Arel i -> mkRel (nb_rel env - i)
| Aconstant cst -> mkConstU cst
@@ -257,19 +257,19 @@ and nf_atom env atom =
| Asort s -> mkSort s
| Avar id -> mkVar id
| Aprod(n,dom,codom) ->
- let dom = nf_type env dom in
+ let dom = nf_type env sigma dom in
let vn = mk_rel_accu (nb_rel env) in
let env = push_rel (LocalAssum (n,dom)) env in
- let codom = nf_type env (codom vn) in
+ let codom = nf_type env sigma (codom vn) in
mkProd(n,dom,codom)
| Ameta (mv,_) -> mkMeta mv
| Aevar (ev,_) -> mkEvar ev
| Aproj(p,c) ->
- let c = nf_accu env c in
+ let c = nf_accu env sigma c in
mkProj(Projection.make p true,c)
- | _ -> fst (nf_atom_type env atom)
+ | _ -> fst (nf_atom_type env sigma atom)
-and nf_atom_type env atom =
+and nf_atom_type env sigma atom =
match atom with
| Arel i ->
let n = (nb_rel env - i) in
@@ -283,7 +283,7 @@ and nf_atom_type env atom =
| Avar id ->
mkVar id, type_of_var env id
| Acase(ans,accu,p,bs) ->
- let a,ta = nf_accu_type env accu in
+ let a,ta = nf_accu_type env sigma accu in
let ((mind,_),u as ind),allargs = find_rectype_a env ta in
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
@@ -292,14 +292,14 @@ and nf_atom_type env atom =
hnf_prod_applist env
(Inductiveops.type_of_inductive env ind) (Array.to_list params) in
let pT = whd_all env pT in
- let dep, p = nf_predicate env ind mip params p pT in
+ let dep, p = nf_predicate env sigma ind mip params p pT in
(* Calcul du type des branches *)
- let btypes = build_branches_type env (fst ind) mib mip u params dep p in
+ let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in
(* calcul des branches *)
let bsw = branch_of_switch (nb_rel env) ans bs in
let mkbranch i v =
let decl,decl_with_letin,codom = btypes.(i) in
- let b = nf_val (Termops.push_rels_assum decl env) v codom in
+ let b = nf_val (Termops.push_rels_assum decl env) sigma v codom in
Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin
in
let branchs = Array.mapi mkbranch bsw in
@@ -307,7 +307,7 @@ and nf_atom_type env atom =
let ci = ans.asw_ci in
mkCase(ci, p, a, branchs), tcase
| Afix(tt,ft,rp,s) ->
- let tt = Array.map (fun t -> nf_type env t) tt in
+ let tt = Array.map (fun t -> nf_type env sigma t) tt in
let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in
let lvl = nb_rel env in
let nbfix = Array.length ft in
@@ -316,37 +316,37 @@ and nf_atom_type env atom =
let env = push_rec_types (name,tt,[||]) env in
(* We lift here because the types of arguments (in tt) will be evaluated
in an environment where the fixpoints have been pushed *)
- let norm_body i v = nf_val env (napply v fargs) (lift nbfix tt.(i)) in
+ let norm_body i v = nf_val env sigma (napply v fargs) (lift nbfix tt.(i)) in
let ft = Array.mapi norm_body ft in
mkFix((rp,s),(name,tt,ft)), tt.(s)
| Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) ->
- let tt = Array.map (nf_type env) tt in
+ let tt = Array.map (nf_type env sigma) tt in
let name = Array.map (fun _ -> (Name (id_of_string "Fcofix"))) tt in
let lvl = nb_rel env in
let fargs = mk_rels_accu lvl (Array.length ft) in
let env = push_rec_types (name,tt,[||]) env in
- let ft = Array.mapi (fun i v -> nf_val env (napply v fargs) tt.(i)) ft in
+ let ft = Array.mapi (fun i v -> nf_val env sigma (napply v fargs) tt.(i)) ft in
mkCoFix(s,(name,tt,ft)), tt.(s)
| Aprod(n,dom,codom) ->
- let dom,s1 = nf_type_sort env dom in
+ let dom,s1 = nf_type_sort env sigma dom in
let vn = mk_rel_accu (nb_rel env) in
let env = push_rel (LocalAssum (n,dom)) env in
- let codom,s2 = nf_type_sort env (codom vn) in
+ let codom,s2 = nf_type_sort env sigma (codom vn) in
mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
| Aevar(ev,ty) ->
- let ty = nf_type env ty in
+ let ty = nf_type env sigma ty in
mkEvar ev, ty
| Ameta(mv,ty) ->
- let ty = nf_type env ty in
+ let ty = nf_type env sigma ty in
mkMeta mv, ty
| Aproj(p,c) ->
- let c,tc = nf_accu_type env c in
+ let c,tc = nf_accu_type env sigma c in
let cj = make_judge c tc in
let uj = Typeops.judge_of_projection env (Projection.make p true) cj in
uj.uj_val, uj.uj_type
-and nf_predicate env ind mip params v pT =
+and nf_predicate env sigma ind mip params v pT =
match kind_of_value v, kind_of_term pT with
| Vfun f, Prod _ ->
let k = nb_rel env in
@@ -358,7 +358,7 @@ and nf_predicate env ind mip params v pT =
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
let dep,body =
- nf_predicate (push_rel (LocalAssum (name,dom)) env) ind mip params vb codom in
+ nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
dep, mkLambda(name,dom,body)
| Vfun f, _ ->
let k = nb_rel env in
@@ -368,9 +368,9 @@ and nf_predicate env ind mip params v pT =
let rargs = Array.init n (fun i -> mkRel (n-i)) in
let params = if Int.equal n 0 then params else Array.map (lift n) params in
let dom = mkApp(mkIndU ind,Array.append params rargs) in
- let body = nf_type (push_rel (LocalAssum (name,dom)) env) vb in
+ let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in
true, mkLambda(name,dom,body)
- | _, _ -> false, nf_type env v
+ | _, _ -> false, nf_type env sigma v
let evars_of_evar_map sigma =
{ Nativelambda.evars_val = Evd.existential_opt_value sigma;
@@ -382,13 +382,12 @@ let native_norm env sigma c ty =
error "Native_compute reduction has been disabled at configure time."
else
let penv = Environ.pre_env env in
- let sigma = evars_of_evar_map sigma in
(*
Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
*)
let ml_filename, prefix = Nativelib.get_ml_filename () in
- let code, upd = mk_norm_code penv sigma prefix c in
+ let code, upd = mk_norm_code penv (evars_of_evar_map sigma) prefix c in
match Nativelib.compile ml_filename code with
| true, fn ->
if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
@@ -397,7 +396,7 @@ let native_norm env sigma c ty =
let t1 = Sys.time () in
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
- let res = nf_val env !Nativelib.rt1 ty in
+ let res = nf_val env sigma !Nativelib.rt1 ty in
let t2 = Sys.time () in
let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 9b572f376..3a6d4f36c 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
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e897d5f5c..062e4a068 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -202,7 +202,7 @@ let compute_canonical_projections warn (con,ind) =
let v = (mkConstU (con,u)) in
let ctx = Univ.ContextSet.of_context ctx in
let c = Environ.constant_value_in env (con,u) in
- let lt,t = Reductionops.splay_lam env Evd.empty c in
+ let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
let lt = List.rev_map snd lt in
let args = snd (decompose_app t) in
let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
@@ -302,7 +302,7 @@ let check_and_decompose_canonical_structure ref =
let vc = match Environ.constant_opt_value_in env (sp, u) with
| Some vc -> vc
| None -> error_not_structure ref in
- let body = snd (splay_lam (Global.env()) Evd.empty vc) in
+ let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
let f,args = match kind_of_term body with
| App (f,args) -> f,args
| _ -> error_not_structure ref in
@@ -323,6 +323,7 @@ let lookup_canonical_conversion (proj,pat) =
let is_open_canonical_projection env sigma (c,args) =
try
+ let c = EConstr.Unsafe.to_constr c in
let ref = global_of_constr c in
let n = find_projection_nparams ref in
(** Check if there is some canonical projection attached to this structure *)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 4a176760c..405963a9c 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -72,6 +72,6 @@ val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
val declare_canonical_structure : global_reference -> unit
val is_open_canonical_projection :
- Environ.env -> Evd.evar_map -> (constr * constr Reductionops.Stack.t) -> bool
+ Environ.env -> Evd.evar_map -> Reductionops.state -> bool
val canonical_projections : unit ->
((global_reference * cs_pattern) * obj_typ) list
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 820974888..69d47e8e6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -156,6 +156,7 @@ end
(** Machinery about stack of unfolded constants *)
module Cst_stack = struct
+ open EConstr
(** constant * params * args
- constant applied to params = term in head applied to args
@@ -191,8 +192,8 @@ module Cst_stack = struct
| (cst,params,[])::_ -> Some(cst,params)
| _ -> None
- let reference t = match best_cst t with
- | Some (c, _) when Term.isConst c -> Some (fst (Term.destConst c))
+ let reference sigma t = match best_cst t with
+ | Some (c, _) when isConst sigma c -> Some (fst (destConst sigma c))
| _ -> None
(** [best_replace d cst_l c] makes the best replacement for [d]
@@ -201,14 +202,14 @@ module Cst_stack = struct
let reconstruct_head = List.fold_left
(fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in
List.fold_right
- (fun (cst,params,args) t -> Termops.replace_term sigma
- (EConstr.of_constr (reconstruct_head d args))
- (EConstr.of_constr (applist (cst, List.rev params)))
- (EConstr.of_constr t)) cst_l c
+ (fun (cst,params,args) t -> EConstr.of_constr (Termops.replace_term sigma
+ (reconstruct_head d args)
+ (applist (cst, List.rev params))
+ t)) cst_l c
let pr l =
let open Pp in
- let p_c = Termops.print_constr in
+ let p_c c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
prlist_with_sep pr_semicolon
(fun (c,params,args) ->
hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
@@ -220,6 +221,7 @@ end
(** The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
module Stack :
sig
+ open EConstr
type 'a app_node
val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
@@ -231,7 +233,7 @@ sig
| App of 'a app_node
| Case of case_info * 'a * 'a array * Cst_stack.t
| Proj of int * int * projection * Cst_stack.t
- | Fix of fixpoint * 'a t * Cst_stack.t
+ | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Cst of cst_member * int * int list * 'a t * Cst_stack.t
| Shift of int
| Update of 'a
@@ -242,10 +244,10 @@ sig
val append_app : 'a array -> 'a t -> 'a t
val decomp : 'a t -> ('a * 'a t) option
val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
- val equal : ('a * int -> 'a * int -> bool) -> (fixpoint * int -> fixpoint * int -> bool)
+ val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool)
-> 'a t -> 'a t -> (int * int) option
val compare_shape : 'a t -> 'a t -> bool
- val map : (constr -> constr) -> constr t -> constr t
+ val map : ('a -> 'a) -> 'a t -> 'a t
val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
constr t -> constr t -> 'a * int * int
val append_app_list : 'a list -> 'a t -> 'a t
@@ -258,10 +260,11 @@ sig
val args_size : 'a t -> int
val tail : int -> 'a t -> 'a t
val nth : 'a t -> int -> 'a
- val best_state : constr * constr t -> Cst_stack.t -> constr * constr t
- val zip : ?refold:bool -> constr * constr t -> constr
+ val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
+ val zip : ?refold:bool -> evar_map -> constr * constr t -> constr
end =
struct
+ open EConstr
type 'a app_node = int * 'a array * int
(* first releavnt position, arguments, last relevant position *)
@@ -286,7 +289,7 @@ struct
| App of 'a app_node
| Case of Term.case_info * 'a * 'a array * Cst_stack.t
| Proj of int * int * projection * Cst_stack.t
- | Fix of fixpoint * 'a t * Cst_stack.t
+ | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Cst of cst_member * int * int list * 'a t * Cst_stack.t
| Shift of int
| Update of 'a
@@ -305,7 +308,7 @@ struct
str "ZProj(" ++ int n ++ pr_comma () ++ int m ++
pr_comma () ++ pr_con (Projection.constant p) ++ str ")"
| Fix (f,args,cst) ->
- str "ZFix(" ++ Termops.pr_fix Termops.print_constr f
+ str "ZFix(" ++ Termops.pr_fix pr_c f
++ pr_comma () ++ pr pr_c args ++ str ")"
| Cst (mem,curr,remains,params,cst_l) ->
str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr
@@ -533,11 +536,11 @@ struct
| None -> raise Not_found
(** This function breaks the abstraction of Cst_stack ! *)
- let best_state (_,sk as s) l =
+ let best_state sigma (_,sk as s) l =
let rec aux sk def = function
|(cst, params, []) -> (cst, append_app_list (List.rev params) sk)
|(cst, params, (i,t)::q) -> match decomp sk with
- | Some (el,sk') when Constr.equal el t.(i) ->
+ | Some (el,sk') when EConstr.eq_constr sigma el t.(i) ->
if i = pred (Array.length t)
then aux sk' def (cst, params, q)
else aux sk' def (cst, params, (succ i,t)::q)
@@ -552,53 +555,66 @@ struct
| Some (hd, sk) -> mkProj (p, hd), sk
| None -> assert false
- let rec zip ?(refold=false) = function
+ let zip ?(refold=false) sigma s =
+ let rec zip = function
| f, [] -> f
| f, (App (i,a,j) :: s) ->
let a' = if Int.equal i 0 && Int.equal j (Array.length a - 1)
then a
else Array.sub a i (j - i + 1) in
- zip ~refold (mkApp (f, a'), s)
+ zip (mkApp (f, a'), s)
| f, (Case (ci,rt,br,cst_l)::s) when refold ->
- zip ~refold (best_state (mkCase (ci,rt,f,br), s) cst_l)
- | f, (Case (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s)
+ zip (best_state sigma (mkCase (ci,rt,f,br), s) cst_l)
+ | f, (Case (ci,rt,br,_)::s) -> zip (mkCase (ci,rt,f,br), s)
| f, (Fix (fix,st,cst_l)::s) when refold ->
- zip ~refold (best_state (mkFix fix, st @ (append_app [|f|] s)) cst_l)
- | f, (Fix (fix,st,_)::s) -> zip ~refold
+ zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
+ | f, (Fix (fix,st,_)::s) -> zip
(mkFix fix, st @ (append_app [|f|] s))
| f, (Cst (cst,_,_,params,cst_l)::s) when refold ->
- zip ~refold (best_state (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
+ zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l)
| f, (Cst (cst,_,_,params,_)::s) ->
- zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s)))
- | f, (Shift n::s) -> zip ~refold (lift n f, s)
+ zip (constr_of_cst_member cst (params @ (append_app [|f|] s)))
+ | f, (Shift n::s) -> zip (Vars.lift n f, s)
| f, (Proj (n,m,p,cst_l)::s) when refold ->
- zip ~refold (best_state (mkProj (p,f),s) cst_l)
- | f, (Proj (n,m,p,_)::s) -> zip ~refold (mkProj (p,f),s)
+ zip (best_state sigma (mkProj (p,f),s) cst_l)
+ | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s)
| _, (Update _::_) -> assert false
+ in
+ zip s
+
end
(** The type of (machine) states (= lambda-bar-calculus' cuts) *)
-type state = constr * constr Stack.t
+type state = EConstr.t * EConstr.t Stack.t
-type contextual_reduction_function = env -> evar_map -> constr -> constr
-type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> constr -> constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
+type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr
+type reduction_function = contextual_reduction_function
+type local_reduction_function = evar_map -> EConstr.t -> constr
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma }
-type contextual_stack_reduction_function =
- env -> evar_map -> constr -> constr * constr list
-type stack_reduction_function = contextual_stack_reduction_function
+type contextual_stack_reduction_function =
+ env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list
+type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
- evar_map -> constr -> constr * constr list
+ evar_map -> EConstr.t -> EConstr.t * EConstr.t list
-type contextual_state_reduction_function =
- env -> evar_map -> state -> state
-type state_reduction_function = contextual_state_reduction_function
+type contextual_state_reduction_function =
+ env -> evar_map -> state -> state
+type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
let pr_state (tm,sk) =
let open Pp in
- h 0 (Termops.print_constr tm ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr sk)
+ let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
+ h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
+
+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)
(*************************************)
(*** Reduction Functions Operators ***)
@@ -612,19 +628,19 @@ let safe_meta_value sigma ev =
let strong whdfun env sigma t =
let rec strongrec env t =
- let t = EConstr.of_constr (whdfun env sigma (EConstr.Unsafe.to_constr t)) in
+ let t = EConstr.of_constr (whdfun env sigma t) in
map_constr_with_full_binders sigma push_rel strongrec env t in
- EConstr.Unsafe.to_constr (strongrec env (EConstr.of_constr t))
+ EConstr.Unsafe.to_constr (strongrec env t)
let local_strong whdfun sigma =
- let rec strongrec t = Constr.map strongrec (whdfun sigma t) in
- strongrec
+ let rec strongrec t = EConstr.map sigma strongrec (EConstr.of_constr (whdfun sigma t)) in
+ fun c -> EConstr.Unsafe.to_constr (strongrec c)
let rec strong_prodspine redfun sigma c =
- let x = redfun sigma c in
- match kind_of_term x with
- | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
- | _ -> x
+ let x = EConstr.of_constr (redfun sigma c) in
+ match EConstr.kind sigma x with
+ | Prod (na,a,b) -> mkProd (na, EConstr.Unsafe.to_constr a,strong_prodspine redfun sigma b)
+ | _ -> EConstr.Unsafe.to_constr x
(*************************************)
(*** Reduction using bindingss ***)
@@ -634,31 +650,36 @@ let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA]
(* Beta Reduction tools *)
-let apply_subst recfun env refold cst_l t stack =
+let apply_subst recfun env sigma refold cst_l t stack =
let rec aux env cst_l t stack =
- match (Stack.decomp stack,kind_of_term t) with
+ match (Stack.decomp stack, EConstr.kind sigma t) with
| Some (h,stacktl), Lambda (_,_,c) ->
let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
aux (h::env) cst_l' c stacktl
- | _ -> recfun cst_l (substl env t, stack)
+ | _ -> recfun sigma cst_l (EConstr.Vars.substl env t, stack)
in aux env cst_l t stack
-let stacklam recfun env t stack =
- apply_subst (fun _ -> recfun) env false Cst_stack.empty t stack
+let stacklam recfun env sigma t stack =
+ apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack
+
+let beta_app sigma (c,l) =
+ let zip s = Stack.zip sigma s in
+ stacklam zip [] sigma c (Stack.append_app l Stack.empty)
-let beta_applist (c,l) =
- stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty)
+let beta_applist sigma (c,l) =
+ let zip s = Stack.zip sigma s in
+ EConstr.Unsafe.to_constr (stacklam zip [] sigma c (Stack.append_app_list l Stack.empty))
(* Iota reduction tools *)
type 'a miota_args = {
- mP : constr; (* the result type *)
- mconstr : constr; (* the constructor *)
+ mP : EConstr.t; (* the result type *)
+ mconstr : EConstr.t; (* the constructor *)
mci : case_info; (* special info to re-build pattern *)
mcargs : 'a list; (* the constructor's arguments *)
mlf : 'a array } (* the branch code vector *)
-let reducible_mind_case c = match kind_of_term c with
+let reducible_mind_case sigma c = match EConstr.kind sigma c with
| Construct _ | CoFix _ -> true
| _ -> false
@@ -672,9 +693,10 @@ let reducible_mind_case c = match kind_of_term c with
f x := t. End M. Definition f := u. and say goodbye to any hope
of refolding M.f this way ...
*)
-let magicaly_constant_of_fixbody env reference bd = function
+let magicaly_constant_of_fixbody env sigma reference bd = function
| Name.Anonymous -> bd
| Name.Name id ->
+ let open EConstr in
try
let (cst_mod,cst_sect,_) = Constant.repr3 reference in
let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in
@@ -682,7 +704,7 @@ let magicaly_constant_of_fixbody env reference bd = function
match constant_opt_value_in env (cst,u) with
| None -> bd
| Some t ->
- let csts = Universes.eq_constr_universes t bd in
+ let csts = EConstr.eq_constr_universes sigma (EConstr.of_constr t) bd in
begin match csts with
| Some csts ->
let subst = Universes.Constraints.fold (fun (l,d,r) acc ->
@@ -696,7 +718,8 @@ let magicaly_constant_of_fixbody env reference bd = function
with
| Not_found -> bd
-let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) =
+let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) =
+ let open EConstr in
let nbodies = Array.length bodies in
let make_Fi j =
let ind = nbodies-j-1 in
@@ -708,37 +731,40 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies))
| Some e ->
match reference with
| None -> bd
- | Some r -> magicaly_constant_of_fixbody e r bd names.(ind) in
+ | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in
let closure = List.init nbodies make_Fi in
- substl closure bodies.(bodynum)
+ Vars.substl closure bodies.(bodynum)
(** Similar to the "fix" case below *)
let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk =
+ let open EConstr in
let raw_answer =
let env = if refold then Some env else None in
- contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in
+ contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in
apply_subst
- (fun x (t,sk') ->
+ (fun sigma x (t,sk') ->
let t' =
if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in
recfun x (t',sk'))
- [] refold Cst_stack.empty raw_answer sk
+ [] sigma refold Cst_stack.empty raw_answer sk
-let reduce_mind_case mia =
- match kind_of_term mia.mconstr with
+let reduce_mind_case sigma mia =
+ let open EConstr in
+ match EConstr.kind sigma mia.mconstr with
| Construct ((ind_sp,i),u) ->
(* let ncargs = (fst mia.mci).(i-1) in*)
let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
applist (mia.mlf.(i-1),real_cargs)
| CoFix cofix ->
- let cofix_def = contract_cofix cofix in
+ let cofix_def = contract_cofix sigma cofix in
mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
-let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) =
+ let open EConstr in
let nbodies = Array.length recindices in
let make_Fi j =
let ind = nbodies-j-1 in
@@ -750,26 +776,27 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty
| Some e ->
match reference with
| None -> bd
- | Some r -> magicaly_constant_of_fixbody e r bd names.(ind) in
+ | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in
let closure = List.init nbodies make_Fi in
- substl closure bodies.(bodynum)
+ Vars.substl closure bodies.(bodynum)
(** First we substitute the Rel bodynum by the fixpoint and then we try to
replace the fixpoint by the best constant from [cst_l]
Other rels are directly substituted by constants "magically found from the
context" in contract_fix *)
let reduce_and_refold_fix recfun env sigma refold cst_l fix sk =
+ let open EConstr in
let raw_answer =
let env = if refold then None else Some env in
- contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in
+ contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in
apply_subst
- (fun x (t,sk') ->
+ (fun sigma x (t,sk') ->
let t' =
if refold then
Cst_stack.best_replace sigma (mkFix fix) cst_l t
else t
in recfun x (t',sk'))
- [] refold Cst_stack.empty raw_answer sk
+ [] sigma refold Cst_stack.empty raw_answer sk
let fix_recarg ((recindices,bodynum),_) stack =
assert (0 <= bodynum && bodynum < Array.length recindices);
@@ -802,51 +829,53 @@ let _ = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> debug_RAKAM:=a);
}
-let equal_stacks (x, l) (y, l') =
- let f_equal (x,lft1) (y,lft2) = Constr.equal (Vars.lift lft1 x) (Vars.lift lft2 y) in
- let eq_fix (a,b) (c,d) = f_equal (Constr.mkFix a, b) (Constr.mkFix c, d) in
+let equal_stacks sigma (x, l) (y, l') =
+ let open EConstr in
+ let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in
+ let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in
match Stack.equal f_equal eq_fix l l' with
| None -> false
| Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2)
let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
+ let open EConstr in
let open Context.Named.Declaration in
- let rec whrec cst_l (x, stack as s) =
+ let rec whrec cst_l (x, stack) =
let () = if !debug_RAKAM then
let open Pp in
+ let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in
Feedback.msg_notice
- (h 0 (str "<<" ++ Termops.print_constr x ++
+ (h 0 (str "<<" ++ pr x ++
str "|" ++ cut () ++ Cst_stack.pr cst_l ++
- str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
+ str "|" ++ cut () ++ Stack.pr pr stack ++
str ">>"))
in
+ let c0 = EConstr.kind sigma x in
let fold () =
let () = if !debug_RAKAM then
let open Pp in Feedback.msg_notice (str "<><><><><>") in
- (s,cst_l)
+ ((EConstr.of_kind c0, stack),cst_l)
in
- match kind_of_term x with
+ match c0 with
| Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
(match lookup_rel n env with
- | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
+ | LocalDef (_,body,_) -> whrec Cst_stack.empty (EConstr.of_constr (lift n body), stack)
| _ -> fold ())
| Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
(match lookup_named id env with
| LocalDef (_,body,_) ->
- whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
+ whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (EConstr.of_constr body, stack)
| _ -> fold ())
- | Evar ev ->
- (match safe_evar_value sigma ev with
- | Some body -> whrec cst_l (body, stack)
- | None -> fold ())
+ | Evar ev -> fold ()
| Meta ev ->
(match safe_meta_value sigma ev with
- | Some body -> whrec cst_l (body, stack)
+ | Some body -> whrec cst_l (EConstr.of_constr body, stack)
| None -> fold ())
| Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) ->
(match constant_opt_value_in env const with
| None -> fold ()
| Some body ->
+ let body = EConstr.of_constr body in
if not tactic_mode
then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
(body, stack)
@@ -863,12 +892,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let (tm',sk'),cst_l' =
whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk)
in
- let rec is_case x = match kind_of_term x with
+ let rec is_case x = match EConstr.kind sigma x with
| Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
| App (hd, _) -> is_case hd
| Case _ -> true
| _ -> false in
- if equal_stacks (x, app_sk) (tm', sk')
+ if equal_stacks sigma (x, app_sk) (tm', sk')
|| Stack.will_expose_iota sk'
|| is_case tm'
then fold ()
@@ -896,7 +925,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| None ->
let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in
let stack'', csts = whrec Cst_stack.empty stack' in
- if equal_stacks stack' stack'' then fold ()
+ if equal_stacks sigma stack' stack'' then fold ()
else stack'', csts
| Some (recargs, nargs, flags) ->
if (List.mem `ReductionNeverUnfold flags
@@ -926,7 +955,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
Stack.append_app [|c|] bef,cst_l)::s'))
| LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
- apply_subst whrec [b] refold cst_l c stack
+ apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack
| Cast (c,_,_) -> whrec cst_l (c, stack)
| App (f,cl) ->
whrec
@@ -935,20 +964,20 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| Lambda (na,t,c) ->
(match Stack.decomp stack with
| Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
- apply_subst whrec [] refold cst_l x stack
+ apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack
| None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
- let env' = push_rel (LocalAssum (na,t)) env in
+ let env' = push_rel (local_assum (na, t)) env in
let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
- (match kind_of_term (Stack.zip ~refold (fst (whrec' (c, Stack.empty)))) with
+ (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with
| App (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in
- match kind_of_term x', l' with
+ match EConstr.kind sigma x', l' with
| Rel 1, [] ->
let lc = Array.sub cl 0 (napp-1) in
- let u = if Int.equal napp 1 then f else appvect (f,lc) in
- if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty),Cst_stack.empty else fold ()
+ let u = if Int.equal napp 1 then f else mkApp (f,lc) in
+ if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold ()
| _ -> fold ()
else fold ()
| _ -> fold ())
@@ -973,11 +1002,11 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
|args, (Stack.Proj (n,m,p,_)::s') when use_match ->
whrec Cst_stack.empty (Stack.nth args (n+m), s')
|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
- let x' = Stack.zip(x,args) in
+ let x' = Stack.zip sigma (x, args) in
let out_sk = s' @ (Stack.append_app [|x'|] s'') in
reduce_and_refold_fix whrec env sigma refold cst_l f out_sk
|args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
- let x' = Stack.zip(x,args) in
+ let x' = Stack.zip sigma (x, args) in
begin match remains with
| [] ->
(match const with
@@ -985,6 +1014,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
(match constant_opt_value_in env const with
| None -> fold ()
| Some body ->
+ let body = EConstr.of_constr body in
whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
(body, s' @ (Stack.append_app [|x'|] s'')))
| Stack.Cst_proj p ->
@@ -1020,31 +1050,34 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
in
fun xs ->
let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
- if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res
+ if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
(** reduction machine without global env and refold machinery *)
let local_whd_state_gen flags sigma =
- let rec whrec (x, stack as s) =
- match kind_of_term x with
+ let open EConstr in
+ let rec whrec (x, stack) =
+ let c0 = EConstr.kind sigma x in
+ let s = (EConstr.of_kind c0, stack) in
+ match c0 with
| LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
- stacklam whrec [b] c stack
+ stacklam whrec [b] sigma c stack
| Cast (c,_,_) -> whrec (c, stack)
| App (f,cl) -> whrec (f, Stack.append_app cl stack)
| Lambda (_,_,c) ->
(match Stack.decomp stack with
| Some (a,m) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
- stacklam whrec [a] c m
+ stacklam whrec [a] sigma c m
| None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
- (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with
+ (match EConstr.kind sigma (Stack.zip sigma (whrec (c, Stack.empty))) with
| App (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
let x', l' = whrec (Array.last cl, Stack.empty) in
- match kind_of_term x', l' with
+ match EConstr.kind sigma x', l' with
| Rel 1, [] ->
let lc = Array.sub cl 0 (napp-1) in
- let u = if Int.equal napp 1 then f else appvect (f,lc) in
- if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty) else s
+ let u = if Int.equal napp 1 then f else mkApp (f,lc) in
+ if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s
| _ -> s
else s
| _ -> s)
@@ -1064,14 +1097,10 @@ let local_whd_state_gen flags sigma =
|None -> s
|Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef,Cst_stack.empty)::s'))
- | Evar ev ->
- (match safe_evar_value sigma ev with
- Some c -> whrec (c,stack)
- | None -> s)
-
+ | Evar ev -> s
| Meta ev ->
(match safe_meta_value sigma ev with
- Some c -> whrec (c,stack)
+ Some c -> whrec (EConstr.of_constr c,stack)
| None -> s)
| Construct ((ind,c),u) ->
@@ -1084,8 +1113,8 @@ let local_whd_state_gen flags sigma =
|args, (Stack.Proj (n,m,p,_) :: s') when use_match ->
whrec (Stack.nth args (n+m), s')
|args, (Stack.Fix (f,s',cst)::s'') when use_fix ->
- let x' = Stack.zip(x,args) in
- whrec (contract_fix f, s' @ (Stack.append_app [|x'|] s''))
+ let x' = Stack.zip sigma (x,args) in
+ whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s''))
|_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false
|_, _ -> s
else s
@@ -1094,7 +1123,7 @@ let local_whd_state_gen flags sigma =
if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
match Stack.strip_app stack with
|args, ((Stack.Case _ | Stack.Proj _)::s') ->
- whrec (contract_cofix cofix, stack)
+ whrec (contract_cofix sigma cofix, stack)
|_ -> s
else s
@@ -1107,7 +1136,7 @@ let raw_whd_state_gen flags env =
f
let stack_red_of_state_red f =
- let f sigma x = decompose_app (Stack.zip (f sigma (x, Stack.empty))) in
+ let f sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f sigma (x, Stack.empty))) in
f
(* Drops the Cst_stack *)
@@ -1115,11 +1144,11 @@ let iterate_whd_gen refold flags env sigma s =
let rec aux t =
let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in
let whd_sk = Stack.map aux sk in
- Stack.zip ~refold (hd,whd_sk)
+ Stack.zip sigma ~refold (hd,whd_sk)
in aux s
let red_of_state_red f sigma x =
- Stack.zip (f sigma (x,Stack.empty))
+ EConstr.Unsafe.to_constr (Stack.zip sigma (f sigma (x,Stack.empty)))
(* 0. No Reduction Functions *)
@@ -1174,7 +1203,7 @@ let whd_allnolet env =
(* 4. Ad-hoc eta reduction, does not subsitute evars *)
-let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty))
+let shrink_eta c = EConstr.Unsafe.to_constr (Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)))
(* 5. Zeta Reduction Functions *)
@@ -1198,7 +1227,7 @@ let clos_norm_flags flgs env sigma t =
let evars ev = safe_evar_value sigma ev in
CClosure.norm_val
(CClosure.create_clos_infos ~evars flgs env)
- (CClosure.inject t)
+ (CClosure.inject (EConstr.Unsafe.to_constr t))
with e when is_anomaly e -> error "Tried to normalize ill-typed term"
let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
@@ -1239,7 +1268,15 @@ let report_anomaly _ =
let e = CErrors.push e in
iraise e
-let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
+let f_conv ?l2r ?reds env ?evars x y =
+ let inj = EConstr.Unsafe.to_constr in
+ Reduction.conv ?l2r ?reds env ?evars (inj x) (inj y)
+
+let f_conv_leq ?l2r ?reds env ?evars x y =
+ let inj = EConstr.Unsafe.to_constr in
+ Reduction.conv_leq ?l2r ?reds env ?evars (inj x) (inj y)
+
+let test_trans_conversion (f: EConstr.t Reduction.extended_conversion_function) reds env sigma x y =
try
let evars ev = safe_evar_value sigma ev in
let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in
@@ -1247,16 +1284,16 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red
with Reduction.NotConvertible -> false
| e when is_anomaly e -> report_anomaly e
-let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv reds env sigma
-let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_leq reds env sigma
+let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv reds env sigma
+let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv_leq reds env sigma
let is_fconv ?(reds=full_transparent_state) = function
| Reduction.CONV -> is_conv ~reds
| Reduction.CUMUL -> is_conv_leq ~reds
let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y =
let f = match pb with
- | Reduction.CONV -> Reduction.conv
- | Reduction.CUMUL -> Reduction.conv_leq
+ | Reduction.CONV -> f_conv
+ | Reduction.CUMUL -> f_conv_leq
in
try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true
with Reduction.NotConvertible -> false
@@ -1320,37 +1357,38 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
(* Special-Purpose Reduction *)
(********************************************************************)
-let whd_meta sigma c = match kind_of_term c with
- | Meta p -> (try meta_value sigma p with Not_found -> c)
- | _ -> c
+let whd_meta sigma c = match EConstr.kind sigma c with
+ | Meta p -> (try meta_value sigma p with Not_found -> EConstr.Unsafe.to_constr c)
+ | _ -> EConstr.Unsafe.to_constr c
let default_plain_instance_ident = Id.of_string "H"
(* Try to replace all metas. Does not replace metas in the metas' values
* Differs from (strong whd_meta). *)
-let plain_instance s c =
- let rec irec n u = match kind_of_term u with
- | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
- | App (f,l) when isCast f ->
- let (f,_,t) = destCast f in
+let plain_instance sigma s c =
+ let open EConstr in
+ let rec irec n u = match EConstr.kind sigma u with
+ | Meta p -> (try Vars.lift n (Metamap.find p s) with Not_found -> u)
+ | App (f,l) when isCast sigma f ->
+ let (f,_,t) = destCast sigma f in
let l' = CArray.Fun1.smartmap irec n l in
- (match kind_of_term f with
+ (match EConstr.kind sigma f with
| Meta p ->
(* Don't flatten application nodes: this is used to extract a
proof-term from a proof-tree and we want to keep the structure
of the proof-tree *)
(try let g = Metamap.find p s in
- match kind_of_term g with
+ match EConstr.kind sigma g with
| App _ ->
- let l' = CArray.Fun1.smartmap lift 1 l' in
+ let l' = CArray.Fun1.smartmap Vars.lift 1 l' in
mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l'))
| _ -> mkApp (g,l')
with Not_found -> mkApp (f,l'))
| _ -> mkApp (irec n f,l'))
- | Cast (m,_,_) when isMeta m ->
- (try lift n (Metamap.find (destMeta m) s) with Not_found -> u)
+ | Cast (m,_,_) when isMeta sigma m ->
+ (try Vars.lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u)
| _ ->
- map_constr_with_binders succ irec n u
+ map_with_binders sigma succ irec n u
in
if Metamap.is_empty s then c
else irec 0 c
@@ -1391,7 +1429,7 @@ let plain_instance s c =
let instance sigma s c =
(* if s = [] then c else *)
- local_strong whd_betaiota sigma (plain_instance s c)
+ local_strong whd_betaiota sigma (plain_instance sigma s c)
(* pseudo-reduction rule:
* [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -1400,34 +1438,40 @@ let instance sigma s c =
* error message. *)
let hnf_prod_app env sigma t n =
- match kind_of_term (whd_all env sigma t) with
- | Prod (_,_,b) -> subst1 n b
+ let open EConstr in
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+ | Prod (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b)
| _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
let hnf_prod_appvect env sigma t nl =
- Array.fold_left (hnf_prod_app env sigma) t nl
+ Array.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
let hnf_prod_applist env sigma t nl =
- List.fold_left (hnf_prod_app env sigma) t nl
+ List.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
let hnf_lam_app env sigma t n =
- match kind_of_term (whd_all env sigma t) with
- | Lambda (_,_,b) -> subst1 n b
+ let open EConstr in
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with
+ | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b)
| _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction")
let hnf_lam_appvect env sigma t nl =
- Array.fold_left (hnf_lam_app env sigma) t nl
+ Array.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
let hnf_lam_applist env sigma t nl =
- List.fold_left (hnf_lam_app env sigma) t nl
+ List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
+
+let bind_assum (na, t) =
+ let inj = EConstr.Unsafe.to_constr in
+ (na, inj t)
let splay_prod env sigma =
let rec decrec env m c =
let t = whd_all env sigma c in
- match kind_of_term t with
+ match EConstr.kind sigma (EConstr.of_constr t) with
| Prod (n,a,c0) ->
- decrec (push_rel (LocalAssum (n,a)) env)
- ((n,a)::m) c0
+ decrec (push_rel (local_assum (n,a)) env)
+ (bind_assum (n,a)::m) c0
| _ -> m,t
in
decrec env []
@@ -1435,10 +1479,10 @@ let splay_prod env sigma =
let splay_lam env sigma =
let rec decrec env m c =
let t = whd_all env sigma c in
- match kind_of_term t with
+ match EConstr.kind sigma (EConstr.of_constr t) with
| Lambda (n,a,c0) ->
- decrec (push_rel (LocalAssum (n,a)) env)
- ((n,a)::m) c0
+ decrec (push_rel (local_assum (n,a)) env)
+ (bind_assum (n,a)::m) c0
| _ -> m,t
in
decrec env []
@@ -1446,51 +1490,51 @@ let splay_lam env sigma =
let splay_prod_assum env sigma =
let rec prodec_rec env l c =
let t = whd_allnolet env sigma c in
- match kind_of_term t with
+ match EConstr.kind sigma (EConstr.of_constr t) with
| Prod (x,t,c) ->
- prodec_rec (push_rel (LocalAssum (x,t)) env)
- (Context.Rel.add (LocalAssum (x,t)) l) c
+ prodec_rec (push_rel (local_assum (x,t)) env)
+ (Context.Rel.add (local_assum (x,t)) l) c
| LetIn (x,b,t,c) ->
- prodec_rec (push_rel (LocalDef (x,b,t)) env)
- (Context.Rel.add (LocalDef (x,b,t)) l) c
+ prodec_rec (push_rel (local_def (x,b,t)) env)
+ (Context.Rel.add (local_def (x,b,t)) l) c
| Cast (c,_,_) -> prodec_rec env l c
| _ ->
- let t' = whd_all env sigma t in
+ let t' = whd_all env sigma (EConstr.of_constr t) in
if Term.eq_constr t t' then l,t
- else prodec_rec env l t'
+ else prodec_rec env l (EConstr.of_constr t')
in
prodec_rec env Context.Rel.empty
let splay_arity env sigma c =
let l, c = splay_prod env sigma c in
- match kind_of_term c with
+ match EConstr.kind sigma (EConstr.of_constr c) with
| Sort s -> l,s
| _ -> invalid_arg "splay_arity"
let sort_of_arity env sigma c = snd (splay_arity env sigma c)
let splay_prod_n env sigma n =
- let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
- match kind_of_term (whd_all env sigma c) with
+ let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
| Prod (n,a,c0) ->
- decrec (push_rel (LocalAssum (n,a)) env)
- (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
+ decrec (push_rel (local_assum (n,a)) env)
+ (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
| _ -> invalid_arg "splay_prod_n"
in
decrec env n Context.Rel.empty
let splay_lam_n env sigma n =
- let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
- match kind_of_term (whd_all env sigma c) with
+ let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else
+ match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with
| Lambda (n,a,c0) ->
- decrec (push_rel (LocalAssum (n,a)) env)
- (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0
+ decrec (push_rel (local_assum (n,a)) env)
+ (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0
| _ -> invalid_arg "splay_lam_n"
in
decrec env n Context.Rel.empty
let is_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 -> true
| _ -> false
@@ -1498,6 +1542,7 @@ let is_sort env sigma t =
of case/fix (heuristic used by evar_conv) *)
let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
+ let open EConstr in
let refold = get_refolding_in_reduction () in
let tactic_mode = false in
let rec whrec csts s =
@@ -1506,15 +1551,15 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
|args, (Stack.Case _ :: _ as stack') ->
let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
(CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
- if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+ if reducible_mind_case sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
|args, (Stack.Fix _ :: _ as stack') ->
let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
(CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
- if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
+ if isConstruct sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
|args, (Stack.Proj (n,m,p,_) :: stack'') ->
let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
(CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
- if isConstruct t_o then
+ if isConstruct sigma t_o then
whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
else s,csts'
|_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts'
@@ -1523,9 +1568,9 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
let find_conclusion env sigma =
let rec decrec env c =
let t = whd_all env sigma c in
- match kind_of_term t with
- | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
- | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0
+ match EConstr.kind sigma (EConstr.of_constr t) with
+ | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
+ | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0
| t -> t
in
decrec env
@@ -1539,11 +1584,12 @@ let is_arity env sigma c =
(* Metas *)
let meta_value evd mv =
+ let open EConstr in
let rec valrec mv =
match meta_opt_fvalue evd mv with
| Some (b,_) ->
let metas = Metamap.bind valrec b.freemetas in
- instance evd metas b.rebus
+ EConstr.of_constr (instance evd metas (EConstr.of_constr b.rebus))
| None -> mkMeta mv
in
valrec mv
@@ -1553,7 +1599,7 @@ let meta_instance sigma b =
if Metaset.is_empty fm then b.rebus
else
let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
- instance sigma c_sigma b.rebus
+ instance sigma c_sigma (EConstr.of_constr b.rebus)
let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
@@ -1569,7 +1615,7 @@ let meta_reducible_instance evd b =
in
let metas = Metaset.fold fold fm Metamap.empty in
let rec irec u =
- let u = whd_betaiota Evd.empty u (** FIXME *) in
+ let u = whd_betaiota Evd.empty (EConstr.of_constr u) (** FIXME *) in
match kind_of_term u with
| Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr c))) ->
let m = destMeta (strip_outer_cast evd (EConstr.of_constr c)) in
@@ -1615,32 +1661,31 @@ let meta_reducible_instance evd b =
else irec b.rebus
-let head_unfold_under_prod ts env _ c =
+let head_unfold_under_prod ts env sigma c =
+ let open EConstr in
let unfold (cst,u as cstu) =
if Cpred.mem cst (snd ts) then
match constant_opt_value_in env cstu with
- | Some c -> c
+ | Some c -> EConstr.of_constr c
| None -> mkConstU cstu
else mkConstU cstu in
let rec aux c =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Prod (n,t,c) -> mkProd (n,aux t, aux c)
| _ ->
- let (h,l) = decompose_app c in
- match kind_of_term h with
- | Const cst -> beta_applist (unfold cst,l)
+ let (h,l) = decompose_app_vect sigma c in
+ match EConstr.kind sigma (EConstr.of_constr h) with
+ | Const cst -> beta_app sigma (unfold cst, Array.map EConstr.of_constr l)
| _ -> c in
- aux c
+ EConstr.Unsafe.to_constr (aux c)
let betazetaevar_applist sigma n c l =
+ let open EConstr in
let rec stacklam n env t stack =
- if Int.equal n 0 then applist (substl env t, stack) else
- match kind_of_term t, stack with
+ if Int.equal n 0 then applist (Vars.substl env t, stack) else
+ match EConstr.kind sigma t, stack with
| Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
- | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
- | Evar ev, _ ->
- (match safe_evar_value sigma ev with
- | Some body -> stacklam n env body stack
- | None -> applist (substl env t, stack))
+ | LetIn(_,b,_,c), _ -> stacklam (n-1) (Vars.substl env b::env) c stack
+ | Evar _, _ -> applist (Vars.substl env t, stack)
| _ -> anomaly (Pp.str "Not enough lambda/let's") in
- stacklam n [] c l
+ EConstr.Unsafe.to_constr (stacklam n [] c l)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 8dcf5c084..911dab0b6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -38,6 +38,7 @@ val set_refolding_in_reduction : bool -> unit
cst applied to params must convertible to term of the state applied to args
*)
module Cst_stack : sig
+ open EConstr
type t
val empty : t
val add_param : constr -> t -> t
@@ -45,12 +46,13 @@ module Cst_stack : sig
val add_cst : constr -> t -> t
val best_cst : t -> (constr * constr list) option
val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
- val reference : t -> Constant.t option
+ val reference : Evd.evar_map -> t -> Constant.t option
val pr : t -> Pp.std_ppcmds
end
module Stack : sig
+ open EConstr
type 'a app_node
val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds
@@ -63,7 +65,7 @@ module Stack : sig
| App of 'a app_node
| Case of case_info * 'a * 'a array * Cst_stack.t
| Proj of int * int * projection * Cst_stack.t
- | Fix of fixpoint * 'a t * Cst_stack.t
+ | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
* 'a t * Cst_stack.t
| Shift of int
@@ -82,9 +84,9 @@ module Stack : sig
val compare_shape : 'a t -> 'a t -> bool
(** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)].
@return the result and the lifts to apply on the terms *)
- val fold2 : ('a -> Term.constr -> Term.constr -> 'a) -> 'a ->
- Term.constr t -> Term.constr t -> 'a * int * int
- val map : (Term.constr -> Term.constr) -> Term.constr t -> Term.constr t
+ val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
+ constr t -> constr t -> 'a * int * int
+ val map : ('a -> 'a) -> 'a t -> 'a t
val append_app_list : 'a list -> 'a t -> 'a t
(** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not
@@ -101,25 +103,25 @@ module Stack : sig
val tail : int -> 'a t -> 'a t
val nth : 'a t -> int -> 'a
- val best_state : constr * constr t -> Cst_stack.t -> constr * constr t
- val zip : ?refold:bool -> constr * constr t -> constr
+ val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t
+ val zip : ?refold:bool -> evar_map -> constr * constr t -> constr
end
(************************************************************************)
-type state = constr * constr Stack.t
+type state = EConstr.t * EConstr.t Stack.t
-type contextual_reduction_function = env -> evar_map -> constr -> constr
+type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr
type reduction_function = contextual_reduction_function
-type local_reduction_function = evar_map -> constr -> constr
+type local_reduction_function = evar_map -> EConstr.t -> constr
-type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma }
+type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma }
type contextual_stack_reduction_function =
- env -> evar_map -> constr -> constr * constr list
+ env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list
type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
- evar_map -> constr -> constr * constr list
+ evar_map -> EConstr.t -> EConstr.t * EConstr.t list
type contextual_state_reduction_function =
env -> evar_map -> state -> state
@@ -137,13 +139,13 @@ val strong_prodspine : local_reduction_function -> local_reduction_function
val stack_reduction_of_reduction :
'a reduction_function -> 'a state_reduction_function
i*)
-val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a
+val stacklam : (state -> 'a) -> EConstr.t list -> evar_map -> EConstr.t -> EConstr.t Stack.t -> 'a
val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool ->
CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
val iterate_whd_gen : bool -> CClosure.RedFlags.reds ->
- Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
+ Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr
(** {6 Generic Optimized Reduction Function using Closures } *)
@@ -196,46 +198,46 @@ val whd_zeta_stack : local_stack_reduction_function
val whd_zeta_state : local_state_reduction_function
val whd_zeta : local_reduction_function
-val shrink_eta : constr -> constr
+val shrink_eta : EConstr.t -> constr
(** Various reduction functions *)
val safe_evar_value : evar_map -> existential -> constr option
-val beta_applist : constr * constr list -> constr
-
-val hnf_prod_app : env -> evar_map -> constr -> constr -> constr
-val hnf_prod_appvect : env -> evar_map -> constr -> constr array -> constr
-val hnf_prod_applist : env -> evar_map -> constr -> constr list -> constr
-val hnf_lam_app : env -> evar_map -> constr -> constr -> constr
-val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr
-val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr
-
-val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr
-val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr
-val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts
-val sort_of_arity : env -> evar_map -> constr -> sorts
-val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr
-val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr
+val beta_applist : evar_map -> EConstr.t * EConstr.t list -> constr
+
+val hnf_prod_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr
+val hnf_prod_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr
+val hnf_prod_applist : env -> evar_map -> EConstr.t -> EConstr.t list -> constr
+val hnf_lam_app : env -> evar_map -> EConstr.t -> EConstr.t -> constr
+val hnf_lam_appvect : env -> evar_map -> EConstr.t -> EConstr.t array -> constr
+val hnf_lam_applist : env -> evar_map -> EConstr.t -> EConstr.t list -> constr
+
+val splay_prod : env -> evar_map -> EConstr.t -> (Name.t * constr) list * constr
+val splay_lam : env -> evar_map -> EConstr.t -> (Name.t * constr) list * constr
+val splay_arity : env -> evar_map -> EConstr.t -> (Name.t * constr) list * sorts
+val sort_of_arity : env -> evar_map -> EConstr.t -> sorts
+val splay_prod_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr
+val splay_lam_n : env -> evar_map -> int -> EConstr.t -> Context.Rel.t * constr
val splay_prod_assum :
- env -> evar_map -> constr -> Context.Rel.t * constr
+ env -> evar_map -> EConstr.t -> Context.Rel.t * constr
type 'a miota_args = {
- mP : constr; (** the result type *)
- mconstr : constr; (** the constructor *)
+ mP : EConstr.t; (** the result type *)
+ mconstr : EConstr.t; (** the constructor *)
mci : case_info; (** special info to re-build pattern *)
mcargs : 'a list; (** the constructor's arguments *)
mlf : 'a array } (** the branch code vector *)
-val reducible_mind_case : constr -> bool
-val reduce_mind_case : constr miota_args -> constr
+val reducible_mind_case : evar_map -> EConstr.t -> bool
+val reduce_mind_case : evar_map -> EConstr.t miota_args -> EConstr.t
-val find_conclusion : env -> evar_map -> constr -> (constr,constr) kind_of_term
-val is_arity : env -> evar_map -> constr -> bool
-val is_sort : env -> evar_map -> types -> bool
+val find_conclusion : env -> evar_map -> EConstr.t -> (EConstr.t,EConstr.t) kind_of_term
+val is_arity : env -> evar_map -> EConstr.t -> bool
+val is_sort : env -> evar_map -> EConstr.types -> bool
-val contract_fix : ?env:Environ.env -> ?reference:Constant.t -> fixpoint -> constr
-val fix_recarg : fixpoint -> constr Stack.t -> (int * constr) option
+val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> (EConstr.t, EConstr.t) pfixpoint -> EConstr.t
+val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option
(** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
val is_transparent : Environ.env -> constant tableKey -> bool
@@ -247,14 +249,14 @@ type conversion_test = constraints -> constraints
val pb_is_equal : conv_pb -> bool
val pb_equal : conv_pb -> conv_pb
-val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool
-val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool
-val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> constr -> constr -> bool
+val is_conv : ?reds:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool
+val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool
+val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> EConstr.t -> EConstr.t -> bool
(** [check_conv] Checks universe constraints only.
pb defaults to CUMUL and ts to a full transparent state.
*)
-val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool
+val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> EConstr.t -> EConstr.t -> bool
(** [infer_conv] Adds necessary universe constraints to the evar map.
pb defaults to CUMUL and ts to a full transparent state.
@@ -280,11 +282,11 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
(** {6 Special-Purpose Reduction Functions } *)
-val whd_meta : evar_map -> constr -> constr
-val plain_instance : constr Metamap.t -> constr -> constr
-val instance : evar_map -> constr Metamap.t -> constr -> constr
+val whd_meta : local_reduction_function
+val plain_instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> EConstr.t
+val instance : evar_map -> EConstr.t Metamap.t -> EConstr.t -> constr
val head_unfold_under_prod : transparent_state -> reduction_function
-val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
+val betazetaevar_applist : evar_map -> int -> EConstr.t -> EConstr.t list -> constr
(** {6 Heuristic for Conversion with Evar } *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index ac3b5ef63..353bdbb89 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -53,8 +53,8 @@ let get_type_from_constraints env sigma t =
if isEvar (fst (decompose_app t)) then
match
List.map_filter (fun (pbty,env,t1,t2) ->
- if is_fconv Reduction.CONV env sigma t t1 then Some t2
- else if is_fconv Reduction.CONV env sigma t t2 then Some t1
+ 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
else None)
(snd (Evd.extract_all_conv_pbs sigma))
with
@@ -65,7 +65,7 @@ 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 typ) with
+ 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
| _ -> retype_error NonFunctionalConstruction
@@ -74,7 +74,7 @@ let rec subst_type env sigma typ = function
let sort_of_atomic_type env sigma ft args =
let rec concl_of_arity env n ar args =
- match kind_of_term (whd_all env sigma ar), args with
+ 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
| Sort s, [] -> s
| _ -> retype_error NotASort
@@ -106,17 +106,17 @@ let retype ?(polyprop=true) sigma =
| Case (_,p,c,lf) ->
let Inductiveops.IndType(indf,realargs) =
let t = type_of env c in
- try Inductiveops.find_rectype env sigma t
+ try Inductiveops.find_rectype env sigma (EConstr.of_constr t)
with Not_found ->
try
let t = get_type_from_constraints env sigma t in
- Inductiveops.find_rectype env sigma t
+ Inductiveops.find_rectype env sigma (EConstr.of_constr 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 p realargs in
- (match kind_of_term (whd_all env sigma (type_of env t)) with
- | Prod _ -> whd_beta sigma (applist (t, [c]))
+ 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])))
| _ -> t)
| Lambda (name,c1,c2) ->
mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2)
@@ -134,7 +134,7 @@ let retype ?(polyprop=true) sigma =
| Proj (p,c) ->
let ty = type_of env c in
(try
- Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+ Inductiveops.type_of_projection_knowing_arg env sigma p (EConstr.of_constr c) (EConstr.of_constr ty)
with Invalid_argument _ -> retype_error BadRecursiveType)
| Cast (c,_, t) -> t
| Sort _ | Prod _ -> mkSort (sort_of env cstr)
@@ -159,7 +159,7 @@ let retype ?(polyprop=true) sigma =
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 (type_of env t)
+ | _ -> decomp_sort env sigma (EConstr.of_constr (type_of env t))
and sort_family_of env t =
match kind_of_term t with
@@ -178,7 +178,7 @@ let retype ?(polyprop=true) sigma =
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 (type_of env t))
+ family_of_sort (decomp_sort env sigma (EConstr.of_constr (type_of env t)))
and type_of_global_reference_knowing_parameters env c args =
let argtyps =
@@ -207,11 +207,10 @@ let type_of_global_reference_knowing_parameters env sigma c args =
let _,_,_,f = retype sigma in anomaly_on_error (f env c) args
let type_of_global_reference_knowing_conclusion env sigma c conclty =
- let conclty = nf_evar sigma conclty in
match kind_of_term c with
| Ind (ind,u) ->
let spec = Inductive.lookup_mind_specif env ind in
- type_of_inductive_knowing_conclusion env sigma (spec,u) conclty
+ type_of_inductive_knowing_conclusion env sigma (spec,u) (EConstr.of_constr conclty)
| Const cst ->
let t = constant_type_in env cst in
(* TODO *)
@@ -251,7 +250,7 @@ let sorts_of_context env evc ctxt =
let expand_projection env sigma pr c args =
let ty = get_type_of ~lax:true env sigma c in
let (i,u), ind_args =
- try Inductiveops.find_mrectype env sigma ty
+ try Inductiveops.find_mrectype env sigma (EConstr.of_constr ty)
with Not_found -> retype_error BadRecursiveType
in
mkApp (mkConstU (Projection.constant pr,u),
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ff76abe37..357a80f44 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -88,11 +88,12 @@ let evaluable_reference_eq r1 r2 = match r1, r2 with
| _ -> false
let mkEvalRef ref u =
+ let open EConstr in
match ref with
| EvalConst cst -> mkConstU (cst,u)
| EvalVar id -> mkVar id
| EvalRel n -> mkRel n
- | EvalEvar ev -> mkEvar ev
+ | EvalEvar ev -> EConstr.of_constr (Constr.mkEvar ev)
let isEvalRef env c = match kind_of_term c with
| Const (sp,_) -> is_evaluable env (EvalConstRef sp)
@@ -132,18 +133,18 @@ exception NotEvaluable
let reference_value env sigma c u =
match reference_opt_value env sigma c u with
| None -> raise NotEvaluable
- | Some d -> d
+ | Some d -> EConstr.of_constr d
(************************************************************************)
(* Reduction of constants hiding a fixpoint (e.g. for "simpl" tactic). *)
(* One reuses the name of the function after reduction of the fixpoint *)
type constant_evaluation =
- | EliminationFix of int * int * (int * (int * constr) list * int)
+ | EliminationFix of int * int * (int * (int * EConstr.t) list * int)
| EliminationMutualFix of
int * evaluable_reference *
((int*evaluable_reference) option array *
- (int * (int * constr) list * int))
+ (int * (int * EConstr.t) list * int))
| EliminationCases of int
| EliminationProj of int
| NotAnElimination
@@ -184,7 +185,7 @@ let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) =
let nbfix = Array.length bds in
let li =
List.map
- (function d -> match kind_of_term d with
+ (function d -> match EConstr.kind sigma d with
| Rel k ->
if
Array.for_all (noccurn k) tys
@@ -202,7 +203,7 @@ let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) =
raise Elimconst;
List.iteri (fun i t_i ->
if not (Int.List.mem_assoc (i+1) li) then
- let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels sigma (EConstr.of_constr t_i))) in
+ let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels sigma t_i)) in
match List.intersect Int.equal fvs reversible_rels with
| [] -> ()
| _ -> raise Elimconst)
@@ -239,11 +240,11 @@ let invert_name labs l na0 env sigma ref = function
| None -> None
| Some c ->
let labs',ccl = decompose_lam c in
- let _, l' = whd_betalet_stack sigma ccl in
+ let _, l' = whd_betalet_stack sigma (EConstr.of_constr ccl) in
let labs' = List.map snd labs' in
(** ppedrot: there used to be generic equality on terms here *)
if List.equal eq_constr labs' labs &&
- List.equal eq_constr l l' then Some (minfxargs,ref)
+ List.equal (fun c1 c2 -> EConstr.eq_constr sigma c1 c2) l l' then Some (minfxargs,ref)
else None
with Not_found (* Undefined ref *) -> None
end
@@ -255,11 +256,12 @@ let invert_name labs l na0 env sigma ref = function
let compute_consteval_direct env sigma ref =
let rec srec env n labs onlyproj c =
- let c',l = whd_betadeltazeta_stack env sigma c in
+ let c',l = whd_betadeltazeta_stack env sigma (EConstr.of_constr c) in
+ let c' = EConstr.Unsafe.to_constr c' in
match kind_of_term c' with
| Lambda (id,t,g) when List.is_empty l && not onlyproj ->
let open Context.Rel.Declaration in
- srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g
+ srec (push_rel (LocalAssum (id,t)) env) (n+1) (EConstr.of_constr t::labs) onlyproj g
| Fix fix when not onlyproj ->
(try check_fix_reversibility sigma labs l fix
with Elimconst -> NotAnElimination)
@@ -274,8 +276,9 @@ let compute_consteval_direct env sigma ref =
let compute_consteval_mutual_fix env sigma ref =
let rec srec env minarg labs ref c =
- let c',l = whd_betalet_stack sigma c in
+ let c',l = whd_betalet_stack sigma (EConstr.of_constr c) in
let nargs = List.length l in
+ let c' = EConstr.Unsafe.to_constr c' in
match kind_of_term c' with
| Lambda (na,t,g) when List.is_empty l ->
let open Context.Rel.Declaration in
@@ -345,6 +348,7 @@ let reference_eval env sigma = function
let x = Name default_dependent_ident
let make_elim_fun (names,(nbfix,lv,n)) u largs =
+ let open EConstr in
let lu = List.firstn n largs in
let p = List.length lv in
let lyi = List.map fst lv in
@@ -353,17 +357,17 @@ let make_elim_fun (names,(nbfix,lv,n)) u largs =
(* k from the comment is q+1 *)
try mkRel (p+1-(List.index Int.equal (n-q) lyi))
with Not_found -> aq)
- 0 (List.map (lift p) lu)
+ 0 (List.map (Vars.lift p) lu)
in
fun i ->
match names.(i) with
| None -> None
| Some (minargs,ref) ->
- let body = applistc (mkEvalRef ref u) la in
+ let body = applist (mkEvalRef ref u, la) in
let g =
List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
- let subst = List.map (lift (-q)) (List.firstn (n-ij) la) in
- let tij' = substl (List.rev subst) tij in
+ let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in
+ let tij' = Vars.substl (List.rev subst) tij in
mkLambda (x,tij',c)) 1 body (List.rev lv)
in Some (minargs,g)
@@ -380,10 +384,11 @@ let venv = let open Context.Named.Declaration in
as a problem variable: an evar that can be instantiated either by
vfx (expanded fixpoint) or vfun (named function). *)
let substl_with_function subst sigma constr =
+ let open EConstr in
let evd = ref sigma in
let minargs = ref Evar.Map.empty in
let v = Array.of_list subst in
- let rec subst_total k c = match kind_of_term c with
+ let rec subst_total k c = match EConstr.kind sigma c with
| Rel i when k < i ->
if i <= k + Array.length v then
match v.(i-k-1) with
@@ -393,11 +398,11 @@ let substl_with_function subst sigma constr =
let sigma = Sigma.to_evar_map sigma in
evd := sigma;
minargs := Evar.Map.add evk min !minargs;
- lift k (mkEvar (evk, [|fx;ref|]))
- | (fx, None) -> lift k fx
+ Vars.lift k (mkEvar (evk, [|fx;ref|]))
+ | (fx, None) -> Vars.lift k fx
else mkRel (i - Array.length v)
| _ ->
- map_constr_with_binders succ subst_total k c in
+ map_with_binders sigma succ subst_total k c in
let c = subst_total 0 constr in
(c, !evd, !minargs)
@@ -408,27 +413,28 @@ exception Partial
let solve_arity_problem env sigma fxminargs c =
let evm = ref sigma in
let set_fix i = evm := Evd.define i (mkVar vfx) !evm in
+ let open EConstr in
let rec check strict c =
- let c' = whd_betaiotazeta sigma c in
- let (h,rcargs) = decompose_app c' in
+ let c' = EConstr.of_constr (whd_betaiotazeta sigma c) in
+ let (h,rcargs) = decompose_app_vect sigma c' in
match kind_of_term h with
Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
let minargs = Evar.Map.find i fxminargs in
- if List.length rcargs < minargs then
+ if Array.length rcargs < minargs then
if strict then set_fix i
else raise Partial;
- List.iter (check strict) rcargs
+ Array.iter (EConstr.of_constr %> check strict) rcargs
| (Var _|Const _) when isEvalRef env h ->
(let ev, u = destEvalRefU h in
match reference_opt_value env sigma ev u with
| Some h' ->
let bak = !evm in
- (try List.iter (check false) rcargs
+ (try Array.iter (EConstr.of_constr %> check false) rcargs
with Partial ->
evm := bak;
- check strict (applist(h',rcargs)))
- | None -> List.iter (check strict) rcargs)
- | _ -> iter_constr (check strict) c' in
+ check strict (EConstr.of_constr (Constr.mkApp(h',rcargs))))
+ | None -> Array.iter (EConstr.of_constr %> check strict) rcargs)
+ | _ -> EConstr.iter sigma (check strict) c' in
check true c;
!evm
@@ -446,59 +452,62 @@ let substl_checking_arity env subst sigma c =
Some c' -> c'
| None -> f)
| _ -> map_constr nf_fix c in
- nf_fix body
+ EConstr.of_constr (nf_fix (EConstr.Unsafe.to_constr body))
-type fix_reduction_result = NotReducible | Reduced of (constr*constr list)
+type fix_reduction_result = NotReducible | Reduced of (EConstr.t * EConstr.t list)
let reduce_fix whdfun sigma fix stack =
match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
| None -> NotReducible
| Some (recargnum,recarg) ->
let (recarg'hd,_ as recarg') = whdfun sigma recarg in
- let stack' = List.assign stack recargnum (applist recarg') in
- (match kind_of_term recarg'hd with
- | Construct _ -> Reduced (contract_fix fix, stack')
+ let stack' = List.assign stack recargnum (EConstr.applist recarg') in
+ (match EConstr.kind sigma recarg'hd with
+ | Construct _ -> Reduced (contract_fix sigma fix, stack')
| _ -> NotReducible)
let contract_fix_use_function env sigma f
((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
+ let open EConstr in
let nbodies = Array.length recindices in
let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
let lbodies = List.init nbodies make_Fi in
- substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum))
+ substl_checking_arity env (List.rev lbodies) sigma (EConstr.of_constr (nf_beta sigma bodies.(bodynum)))
let reduce_fix_use_function env sigma f whfun fix stack =
match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
| None -> NotReducible
| Some (recargnum,recarg) ->
let (recarg'hd,_ as recarg') =
- if isRel recarg then
+ if EConstr.isRel sigma recarg then
(* The recarg cannot be a local def, no worry about the right env *)
(recarg, [])
else
whfun recarg in
- let stack' = List.assign stack recargnum (applist recarg') in
- (match kind_of_term recarg'hd with
+ let stack' = List.assign stack recargnum (EConstr.applist recarg') in
+ (match EConstr.kind sigma recarg'hd with
| Construct _ ->
Reduced (contract_fix_use_function env sigma f fix,stack')
| _ -> NotReducible)
let contract_cofix_use_function env sigma f
(bodynum,(_names,_,bodies as typedbodies)) =
+ let open EConstr in
let nbodies = Array.length bodies in
let make_Fi j = (mkCoFix(j,typedbodies), f j) in
let subbodies = List.init nbodies make_Fi in
substl_checking_arity env (List.rev subbodies)
- sigma (nf_beta sigma bodies.(bodynum))
+ sigma (EConstr.of_constr (nf_beta sigma bodies.(bodynum)))
let reduce_mind_case_use_function func env sigma mia =
- match kind_of_term mia.mconstr with
+ let open EConstr in
+ match EConstr.kind sigma mia.mconstr with
| Construct ((ind_sp,i),u) ->
let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
applist (mia.mlf.(i-1), real_cargs)
| CoFix (bodynum,(names,_,_) as cofix) ->
let build_cofix_name =
- if isConst func then
+ if isConst sigma func then
let minargs = List.length mia.mcargs in
fun i ->
if Int.equal i bodynum then Some (minargs,func)
@@ -510,7 +519,7 @@ let reduce_mind_case_use_function func env sigma mia =
the block was indeed initially built as a global
definition *)
let kn = map_puniverses (fun x -> con_with_label x (Label.of_id id))
- (destConst func)
+ (destConst sigma func)
in
try match constant_opt_value_in env kn with
| None -> None
@@ -525,13 +534,13 @@ let reduce_mind_case_use_function func env sigma mia =
| _ -> assert false
-let match_eval_ref env constr =
- match kind_of_term constr with
+let match_eval_ref env sigma constr =
+ match EConstr.kind sigma constr with
| Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
Some (EvalConst sp, u)
| Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, Univ.Instance.empty)
| Rel i -> Some (EvalRel i, Univ.Instance.empty)
- | Evar ev -> Some (EvalEvar ev, Univ.Instance.empty)
+ | Evar (evk, args) -> Some (EvalEvar (evk, Array.map EConstr.Unsafe.to_constr args), Univ.Instance.empty)
| _ -> None
let match_eval_ref_value env sigma constr =
@@ -548,20 +557,21 @@ let match_eval_ref_value env sigma constr =
let special_red_case env sigma whfun (ci, p, c, lf) =
let rec redrec s =
let (constr, cargs) = whfun s in
- match match_eval_ref env constr with
+ match match_eval_ref env sigma constr with
| Some (ref, u) ->
(match reference_opt_value env sigma ref u with
| None -> raise Redelimination
| Some gvalue ->
- if reducible_mind_case gvalue then
+ let gvalue = EConstr.of_constr gvalue in
+ if reducible_mind_case sigma gvalue then
reduce_mind_case_use_function constr env sigma
{mP=p; mconstr=gvalue; mcargs=cargs;
mci=ci; mlf=lf}
else
- redrec (applist(gvalue, cargs)))
+ redrec (EConstr.applist(gvalue, cargs)))
| None ->
- if reducible_mind_case constr then
- reduce_mind_case
+ if reducible_mind_case sigma constr then
+ reduce_mind_case sigma
{mP=p; mconstr=constr; mcargs=cargs;
mci=ci; mlf=lf}
else
@@ -574,7 +584,7 @@ let recargs = function
| EvalConst c -> ReductionBehaviour.get (ConstRef c)
let reduce_projection env sigma pb (recarg'hd,stack') stack =
- (match kind_of_term recarg'hd with
+ (match EConstr.kind sigma recarg'hd with
| Construct _ ->
let proj_narg =
pb.Declarations.proj_npars + pb.Declarations.proj_arg
@@ -582,12 +592,13 @@ let reduce_projection env sigma pb (recarg'hd,stack') stack =
| _ -> NotReducible)
let reduce_proj env sigma whfun whfun' c =
+ let open EConstr in
let rec redrec s =
- match kind_of_term s with
+ match EConstr.kind sigma s with
| Proj (proj, c) ->
let c' = try redrec c with Redelimination -> c in
let constr, cargs = whfun c' in
- (match kind_of_term constr with
+ (match EConstr.kind sigma constr with
| Construct _ ->
let proj_narg =
let pb = lookup_projection proj env in
@@ -604,44 +615,43 @@ let reduce_proj env sigma whfun whfun' c =
let whd_nothing_for_iota env sigma s =
let rec whrec (x, stack as s) =
- match kind_of_term x with
+ match EConstr.kind sigma x with
| Rel n ->
let open Context.Rel.Declaration in
(match lookup_rel n env with
- | LocalDef (_,body,_) -> whrec (lift n body, stack)
+ | LocalDef (_,body,_) -> whrec (EConstr.of_constr (lift n body), stack)
| _ -> s)
| Var id ->
let open Context.Named.Declaration in
(match lookup_named id env with
- | LocalDef (_,body,_) -> whrec (body, stack)
+ | LocalDef (_,body,_) -> whrec (EConstr.of_constr body, stack)
| _ -> s)
- | Evar ev ->
- (try whrec (Evd.existential_value sigma ev, stack)
- with Evd.NotInstantiatedEvar | Not_found -> s)
+ | Evar ev -> s
| Meta ev ->
- (try whrec (Evd.meta_value sigma ev, stack)
+ (try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack)
with Not_found -> s)
| Const const when is_transparent_constant full_transparent_state (fst const) ->
(match constant_opt_value_in env const with
- | Some body -> whrec (body, stack)
+ | Some body -> whrec (EConstr.of_constr body, stack)
| None -> s)
- | LetIn (_,b,_,c) -> stacklam whrec [b] c stack
+ | LetIn (_,b,_,c) -> stacklam whrec [b] sigma c stack
| Cast (c,_,_) -> whrec (c, stack)
| App (f,cl) -> whrec (f, Stack.append_app cl stack)
| Lambda (na,t,c) ->
(match Stack.decomp stack with
- | Some (a,m) -> stacklam whrec [a] c m
+ | Some (a,m) -> stacklam whrec [a] sigma c m
| _ -> s)
| x -> s
in
- decompose_app (Stack.zip (whrec (s,Stack.empty)))
+ EConstr.decompose_app sigma (Stack.zip sigma (whrec (s,Stack.empty)))
(* [red_elim_const] contracts iota/fix/cofix redexes hidden behind
constants by keeping the name of the constants in the recursive calls;
it fails if no redex is around *)
let rec red_elim_const env sigma ref u largs =
+ let open EConstr in
let nargs = List.length largs in
let largs, unfold_anyway, unfold_nonelim, nocase =
match recargs ref with
@@ -660,7 +670,7 @@ let rec red_elim_const env sigma ref u largs =
let c = reference_value env sigma ref u in
let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
let whfun = whd_simpl_stack env sigma in
- (special_red_case env sigma whfun (destCase c'), lrest), nocase
+ (special_red_case env sigma whfun (EConstr.destCase sigma c'), lrest), nocase
| EliminationProj n when nargs >= n ->
let c = reference_value env sigma ref u in
let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
@@ -672,9 +682,9 @@ let rec red_elim_const env sigma ref u largs =
let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) u largs in
let whfun = whd_construct_stack env sigma in
- (match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
+ (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
| NotReducible -> raise Redelimination
- | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
+ | Reduced (c,rest) -> (EConstr.of_constr (nf_beta sigma c), rest), nocase)
| EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
let rec descend (ref,u) args =
let c = reference_value env sigma ref u in
@@ -682,21 +692,21 @@ let rec red_elim_const env sigma ref u largs =
(c,args)
else
let c', lrest = whd_betalet_stack sigma (applist(c,args)) in
- descend (destEvalRefU c') lrest in
+ descend (destEvalRefU (EConstr.Unsafe.to_constr c')) lrest in
let (_, midargs as s) = descend (ref,u) largs in
let d, lrest = whd_nothing_for_iota env sigma (applist s) in
let f = make_elim_fun refinfos u midargs in
let whfun = whd_construct_stack env sigma in
- (match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
+ (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
| NotReducible -> raise Redelimination
- | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
+ | Reduced (c,rest) -> (EConstr.of_constr (nf_beta sigma c), rest), nocase)
| NotAnElimination when unfold_nonelim ->
let c = reference_value env sigma ref u in
- (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
+ (EConstr.of_constr (whd_betaiotazeta sigma (applist (c, largs))), []), nocase
| _ -> raise Redelimination
with Redelimination when unfold_anyway ->
let c = reference_value env sigma ref u in
- (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
+ (EConstr.of_constr (whd_betaiotazeta sigma (applist (c, largs))), []), nocase
and reduce_params env sigma stack l =
let len = List.length stack in
@@ -705,8 +715,8 @@ and reduce_params env sigma stack l =
else
let arg = List.nth stack i in
let rarg = whd_construct_stack env sigma arg in
- match kind_of_term (fst rarg) with
- | Construct _ -> List.assign stack i (applist rarg)
+ match EConstr.kind sigma (fst rarg) with
+ | Construct _ -> List.assign stack i (EConstr.applist rarg)
| _ -> raise Redelimination)
stack l
@@ -715,14 +725,18 @@ and reduce_params env sigma stack l =
a reducible iota/fix/cofix redex (the "simpl" tactic) *)
and whd_simpl_stack env sigma =
+ let open EConstr in
let rec redrec s =
- let (x, stack as s') = decompose_app s in
- match kind_of_term x with
+ let (x, stack) = decompose_app_vect sigma s in
+ let stack = Array.map_to_list EConstr.of_constr stack in
+ let x = EConstr.of_constr x in
+ let s' = (x, stack) in
+ match EConstr.kind sigma x with
| Lambda (na,t,c) ->
(match stack with
| [] -> s'
- | a :: rest -> redrec (beta_applist (x,stack)))
- | LetIn (n,b,t,c) -> redrec (applist (substl [b] c, stack))
+ | a :: rest -> redrec (EConstr.of_constr (beta_applist sigma (x, stack))))
+ | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack))
| App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack))
| Cast (c,_,_) -> redrec (applist(c, stack))
| Case (ci,p,c,lf) ->
@@ -762,12 +776,12 @@ and whd_simpl_stack env sigma =
with Redelimination -> s')
| _ ->
- match match_eval_ref env x with
+ match match_eval_ref env sigma x with
| Some (ref, u) ->
(try
let sapp, nocase = red_elim_const env sigma ref u stack in
let hd, _ as s'' = redrec (applist(sapp)) in
- let rec is_case x = match kind_of_term x with
+ let rec is_case x = match EConstr.kind sigma x with
| Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
| App (hd, _) -> is_case hd
| Case _ -> true
@@ -782,13 +796,14 @@ and whd_simpl_stack env sigma =
(* reduce until finding an applied constructor or fail *)
and whd_construct_stack env sigma s =
+ let open EConstr in
let (constr, cargs as s') = whd_simpl_stack env sigma s in
- if reducible_mind_case constr then s'
- else match match_eval_ref env constr with
+ if reducible_mind_case sigma constr then s'
+ else match match_eval_ref env sigma constr with
| Some (ref, u) ->
(match reference_opt_value env sigma ref u with
| None -> raise Redelimination
- | Some gvalue -> whd_construct_stack env sigma (applist(gvalue, cargs)))
+ | Some gvalue -> whd_construct_stack env sigma (applist(EConstr.of_constr gvalue, cargs)))
| _ -> raise Redelimination
(************************************************************************)
@@ -800,12 +815,14 @@ and whd_construct_stack env sigma s =
*)
let try_red_product env sigma c =
- let simpfun = clos_norm_flags betaiotazeta env sigma in
+ let simpfun c = EConstr.of_constr (clos_norm_flags betaiotazeta env sigma c) in
+ let inj = EConstr.Unsafe.to_constr in
+ let open EConstr in
let rec redrec env x =
- let x = whd_betaiota sigma x in
- match kind_of_term x with
+ let x = EConstr.of_constr (whd_betaiota sigma x) in
+ match EConstr.kind sigma x with
| App (f,l) ->
- (match kind_of_term f with
+ (match EConstr.kind sigma f with
| Fix fix ->
let stack = Stack.append_app l Stack.empty in
(match fix_recarg fix stack with
@@ -813,17 +830,17 @@ let try_red_product env sigma c =
| Some (recargnum,recarg) ->
let recarg' = redrec env recarg in
let stack' = Stack.assign stack recargnum recarg' in
- simpfun (Stack.zip (f,stack')))
- | _ -> simpfun (appvect (redrec env f, l)))
+ simpfun (Stack.zip sigma (f,stack')))
+ | _ -> simpfun (mkApp (redrec env f, l)))
| Cast (c,_,_) -> redrec env c
| Prod (x,a,b) ->
let open Context.Rel.Declaration in
- mkProd (x, a, redrec (push_rel (LocalAssum (x,a)) env) b)
- | LetIn (x,a,b,t) -> redrec env (subst1 a t)
+ mkProd (x, a, redrec (push_rel (LocalAssum (x, inj a)) env) b)
+ | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t)
| Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf))
| Proj (p, c) ->
let c' =
- match kind_of_term c with
+ match EConstr.kind sigma c with
| Construct _ -> c
| _ -> redrec env c
in
@@ -832,15 +849,15 @@ let try_red_product env sigma c =
| Reduced s -> simpfun (applist s)
| NotReducible -> raise Redelimination)
| _ ->
- (match match_eval_ref env x with
+ (match match_eval_ref env sigma x with
| Some (ref, u) ->
(* TO DO: re-fold fixpoints after expansion *)
(* to get true one-step reductions *)
(match reference_opt_value env sigma ref u with
| None -> raise Redelimination
- | Some c -> c)
+ | Some c -> EConstr.of_constr c)
| _ -> raise Redelimination)
- in redrec env c
+ in EConstr.Unsafe.to_constr (redrec env c)
let red_product env sigma c =
try try_red_product env sigma c
@@ -911,22 +928,23 @@ let whd_simpl_stack =
immediately hides a non reducible fix or a cofix *)
let whd_simpl_orelse_delta_but_fix env sigma c =
+ let open EConstr in
let rec redrec s =
let (constr, stack as s') = whd_simpl_stack env sigma s in
- match match_eval_ref_value env sigma constr with
+ match match_eval_ref_value env sigma (EConstr.Unsafe.to_constr constr) with
| Some c ->
(match kind_of_term (strip_lam c) with
| CoFix _ | Fix _ -> s'
| Proj (p,t) when
- (match kind_of_term constr with
+ (match EConstr.kind sigma constr with
| Const (c', _) -> eq_constant (Projection.constant p) c'
| _ -> false) ->
let pb = Environ.lookup_projection p env in
if List.length stack <= pb.Declarations.proj_npars then
(** Do not show the eta-expanded form *)
s'
- else redrec (applist (c, stack))
- | _ -> redrec (applist(c, stack)))
+ else redrec (applist (EConstr.of_constr c, stack))
+ | _ -> redrec (applist(EConstr.of_constr c, stack)))
| None -> s'
in
let simpfun = clos_norm_flags betaiota env sigma in
@@ -937,7 +955,7 @@ let hnf_constr = whd_simpl_orelse_delta_but_fix
(* The "simpl" reduction tactic *)
let whd_simpl env sigma c =
- applist (whd_simpl_stack env sigma c)
+ EConstr.Unsafe.to_constr (EConstr.applist (whd_simpl_stack env sigma c))
let simpl env sigma c = strong whd_simpl env sigma c
@@ -993,7 +1011,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
(* Skip inner occurrences for stable counting of occurrences *)
if locs != [] then
ignore (traverse_below (Some (!pos-1)) envc t);
- let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) t in
+ let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) (EConstr.of_constr t) in
(evd := Sigma.to_evar_map evm; t)
end
else
@@ -1011,7 +1029,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
(fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
(traverse nested) envc sigma t
in
- let t' = traverse None (env,c) t in
+ let t' = traverse None (env,c) (EConstr.Unsafe.to_constr t) in
if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
Sigma.Unsafe.of_pair (t', !evd)
end }
@@ -1028,7 +1046,7 @@ let contextually byhead occs f env sigma t =
* ol is the occurrence list to find. *)
let match_constr_evaluable_ref sigma c evref =
- match kind_of_term c, evref with
+ match EConstr.kind sigma c, evref with
| Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u
| Var id, EvalVarRef id' when id_eq id id' -> Some Univ.Instance.empty
| _, _ -> None
@@ -1037,7 +1055,7 @@ let substlin env sigma evalref n (nowhere_except_in,locs) c =
let maxocc = List.fold_right max locs 0 in
let pos = ref n in
assert (List.for_all (fun x -> x >= 0) locs);
- let value u = value_of_evaluable_ref env evalref u in
+ let value u = EConstr.of_constr (value_of_evaluable_ref env evalref u) in
let rec substrec () c =
if nowhere_except_in && !pos > maxocc then c
else
@@ -1049,9 +1067,10 @@ let substlin env sigma evalref n (nowhere_except_in,locs) c =
incr pos;
if ok then value u else c
| None ->
- map_constr_with_binders_left_to_right
+ let self () c = EConstr.Unsafe.to_constr (substrec () (EConstr.of_constr c)) in
+ EConstr.of_constr (map_constr_with_binders_left_to_right
(fun _ () -> ())
- substrec () c
+ self () (EConstr.Unsafe.to_constr c))
in
let t' = substrec () c in
(!pos, t')
@@ -1085,39 +1104,39 @@ let unfoldoccs env sigma (occs,name) c =
nf_betaiotazeta sigma uc
in
match occs with
- | NoOccurrences -> c
+ | NoOccurrences -> EConstr.Unsafe.to_constr c
| AllOccurrences -> unfold env sigma name c
| OnlyOccurrences l -> unfo true l
| AllOccurrencesBut l -> unfo false l
(* Unfold reduction tactic: *)
let unfoldn loccname env sigma c =
- List.fold_left (fun c occname -> unfoldoccs env sigma occname c) c loccname
+ EConstr.Unsafe.to_constr (List.fold_left (fun c occname -> EConstr.of_constr (unfoldoccs env sigma occname c)) c loccname)
(* Re-folding constants tactics: refold com in term c *)
let fold_one_com com env sigma c =
let rcom =
- try red_product env sigma com
+ try red_product env sigma (EConstr.of_constr com)
with Redelimination -> error "Not reducible." in
(* Reason first on the beta-iota-zeta normal form of the constant as
unfold produces it, so that the "unfold f; fold f" configuration works
to refold fix expressions *)
- let a = subst_term sigma (EConstr.of_constr (clos_norm_flags unfold_side_red env sigma rcom)) (EConstr.of_constr c) in
- if not (eq_constr a c) then
+ let a = subst_term sigma (EConstr.of_constr (clos_norm_flags unfold_side_red env sigma (EConstr.of_constr rcom))) c in
+ if not (eq_constr a (EConstr.Unsafe.to_constr c)) then
subst1 com a
else
(* Then reason on the non beta-iota-zeta form for compatibility -
even if it is probably a useless configuration *)
- let a = subst_term sigma (EConstr.of_constr rcom) (EConstr.of_constr c) in
+ let a = subst_term sigma (EConstr.of_constr rcom) c in
subst1 com a
let fold_commands cl env sigma c =
- List.fold_right (fun com -> fold_one_com com env sigma) (List.rev cl) c
+ EConstr.Unsafe.to_constr (List.fold_right (fun com c -> EConstr.of_constr (fold_one_com com env sigma c)) (List.rev cl) c)
(* call by value reduction functions *)
let cbv_norm_flags flags env sigma t =
- cbv_norm (create_cbv_infos flags env sigma) t
+ cbv_norm (create_cbv_infos flags env sigma) (EConstr.Unsafe.to_constr t)
let cbv_beta = cbv_norm_flags beta empty_env
let cbv_betaiota = cbv_norm_flags betaiota empty_env
@@ -1142,7 +1161,7 @@ let abstract_scheme env (locc,a) (c, sigma) =
let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
let sigma = Sigma.to_evar_map sigma in
- let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in
+ let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (EConstr.Unsafe.to_constr c,sigma) in
try
let _ = Typing.unsafe_type_of env sigma abstr_trm in
Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
@@ -1170,7 +1189,7 @@ let check_not_primitive_record env ind =
let reduce_to_ind_gen allow_product env sigma t =
let rec elimrec env t l =
- let t = hnf_constr env sigma t in
+ let t = hnf_constr env sigma (EConstr.of_constr t) in
match kind_of_term (fst (decompose_app t)) with
| Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l)
| Prod (n,ty,t') ->
@@ -1182,7 +1201,7 @@ let reduce_to_ind_gen allow_product env sigma t =
| _ ->
(* Last chance: we allow to bypass the Opaque flag (as it
was partially the case between V5.10 and V8.1 *)
- let t' = whd_all env sigma t in
+ let t' = whd_all env sigma (EConstr.of_constr t) in
match kind_of_term (fst (decompose_app t')) with
| Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
| _ -> user_err (str"Not an inductive product.")
@@ -1202,14 +1221,15 @@ let find_hnf_rectype env sigma t =
exception NotStepReducible
let one_step_reduce env sigma c =
+ let open EConstr in
let rec redrec (x, stack) =
- match kind_of_term x with
+ match EConstr.kind sigma x with
| Lambda (n,t,c) ->
(match stack with
| [] -> raise NotStepReducible
- | a :: rest -> (subst1 a c, rest))
+ | a :: rest -> (Vars.subst1 a c, rest))
| App (f,cl) -> redrec (f, (Array.to_list cl)@stack)
- | LetIn (_,f,_,cl) -> (subst1 f cl,stack)
+ | LetIn (_,f,_,cl) -> (Vars.subst1 f cl,stack)
| Cast (c,_,_) -> redrec (c,stack)
| Case (ci,p,c,lf) ->
(try
@@ -1221,13 +1241,13 @@ let one_step_reduce env sigma c =
| Reduced s' -> s'
| NotReducible -> raise NotStepReducible
with Redelimination -> raise NotStepReducible)
- | _ when isEvalRef env x ->
- let ref,u = destEvalRefU x in
+ | _ when isEvalRef env (EConstr.Unsafe.to_constr x) ->
+ let ref,u = destEvalRefU (EConstr.Unsafe.to_constr x) in
(try
fst (red_elim_const env sigma ref u stack)
with Redelimination ->
match reference_opt_value env sigma ref u with
- | Some d -> (d, stack)
+ | Some d -> (EConstr.of_constr d, stack)
| None -> raise NotStepReducible)
| _ -> raise NotStepReducible
@@ -1249,7 +1269,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else
(* lazily reduces to match the head of [t] with the expected [ref] *)
let rec elimrec env t l =
- let c, _ = decompose_appvect (Reductionops.whd_nored sigma t) in
+ let c, _ = decompose_app_vect sigma (EConstr.of_constr t) in
match kind_of_term c with
| Prod (n,ty,t') ->
if allow_product then
@@ -1264,7 +1284,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else raise Not_found
with Not_found ->
try
- let t' = nf_betaiota sigma (one_step_reduce env sigma t) in
+ let t' = nf_betaiota sigma (one_step_reduce env sigma (EConstr.of_constr t)) in
elimrec env t' l
with NotStepReducible -> error_cannot_recognize ref
in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4207eccb9..50dd66ea0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -289,7 +289,7 @@ let build_subclasses ~check env sigma glob pri =
| None -> []
| Some (rels, ((tc,u), args)) ->
let instapp =
- Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels))
+ Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect 0 rels)))
in
let projargs = Array.of_list (args @ [instapp]) in
let projs = List.map_filter
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e79e3d46f..e3d1c1741 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -36,7 +36,7 @@ let inductive_type_knowing_parameters env (ind,u) jl =
Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
let e_type_judgment env evdref j =
- match kind_of_term (whd_all env !evdref j.uj_type) with
+ match kind_of_term (whd_all env !evdref (EConstr.of_constr j.uj_type)) with
| Sort s -> {utj_val = j.uj_val; utj_type = s }
| Evar ev ->
let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
@@ -54,7 +54,7 @@ let e_judge_of_apply env evdref funj argjv =
{ uj_val = mkApp (j_val funj, Array.map j_val argjv);
uj_type = typ }
| hj::restjl ->
- match kind_of_term (whd_all env !evdref typ) with
+ match kind_of_term (whd_all env !evdref (EConstr.of_constr typ)) with
| Prod (_,c1,c2) ->
if Evarconv.e_cumul env evdref hj.uj_type c1 then
apply_rec (n+1) (subst1 hj.uj_val c2) restjl
@@ -87,7 +87,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
let allowed_sorts = elim_sorts specif in
let error () = error_elim_arity env ind allowed_sorts c pj None in
let rec srec env pt ar =
- let pt' = whd_all env !evdref pt in
+ let pt' = whd_all env !evdref (EConstr.of_constr pt) in
match kind_of_term pt', ar with
| Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
if not (Evarconv.e_cumul env evdref a1 a1') then error ();
@@ -113,12 +113,12 @@ let e_type_case_branches env evdref (ind,largs) pj c =
let () = e_is_correct_arity env evdref c pj ind specif params in
let lc = build_branches_type ind specif params p in
let n = (snd specif).Declarations.mind_nrealdecls in
- let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in
+ let ty = whd_betaiota !evdref (EConstr.of_constr (lambda_applist_assum (n+1) p (realargs@[c]))) in
(lc, ty)
let e_judge_of_case env evdref ci pj cj lfj =
let indspec =
- try find_mrectype env !evdref cj.uj_type
+ try find_mrectype env !evdref (EConstr.of_constr cj.uj_type)
with Not_found -> error_case_not_inductive env cj in
let _ = check_case_info env (fst indspec) ci in
let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in
@@ -139,7 +139,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 ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) 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
if not (List.exists ((==) ksort) sorts) then
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 3134dac6a..ede2606da 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -68,7 +68,7 @@ let occur_meta_or_undefined_evar evd c =
let occur_meta_evd sigma mv c =
let rec occrec c =
(* Note: evars are not instantiated by terms with metas *)
- let c = whd_evar sigma (whd_meta sigma c) in
+ let c = whd_evar sigma (whd_meta sigma (EConstr.of_constr c)) in
match kind_of_term c with
| Meta mv' when Int.equal mv mv' -> raise Occur
| _ -> Constr.iter occrec c
@@ -98,7 +98,7 @@ let abstract_scheme env evd c l lname_typ =
(* Precondition: resulting abstraction is expected to be of type [typ] *)
let abstract_list_all env evd typ c l =
- let ctxt,_ = splay_prod_n env evd (List.length l) typ in
+ let ctxt,_ = splay_prod_n env evd (List.length l) (EConstr.of_constr typ) in
let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
let evd,typp =
@@ -480,8 +480,8 @@ let unfold_projection env p stk =
let expand_key ts env sigma = function
| Some (IsKey k) -> expand_table_key env k
| Some (IsProj (p, c)) ->
- let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
- Cst_stack.empty (c, unfold_projection env p [])))
+ let red = EConstr.Unsafe.to_constr (Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
+ Cst_stack.empty (EConstr.of_constr c, unfold_projection env p []))))
in if Term.eq_constr (mkProj (p, c)) red then None else Some red
| None -> None
@@ -576,8 +576,8 @@ let constr_cmp pb sigma flags t u =
sigma, false
let do_reduce ts (env, nb) sigma c =
- Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state
- ts env sigma Cst_stack.empty (c, Stack.empty)))
+ EConstr.Unsafe.to_constr (Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
+ ts env sigma Cst_stack.empty (EConstr.of_constr c, Stack.empty))))
let use_full_betaiota flags =
flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
@@ -977,33 +977,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
(match expand_key flags.modulo_delta curenv sigma cf1 with
| Some c ->
unirec_rec curenvnb pb opt substn
- (whd_betaiotazeta sigma (mkApp(c,l1))) cN
+ (whd_betaiotazeta sigma (EConstr.of_constr (mkApp(c,l1)))) cN
| None ->
(match expand_key flags.modulo_delta curenv sigma cf2 with
| Some c ->
unirec_rec curenvnb pb opt substn cM
- (whd_betaiotazeta sigma (mkApp(c,l2)))
+ (whd_betaiotazeta sigma (EConstr.of_constr (mkApp(c,l2))))
| None ->
error_cannot_unify curenv sigma (cM,cN)))
| Some false ->
(match expand_key flags.modulo_delta curenv sigma cf2 with
| Some c ->
unirec_rec curenvnb pb opt substn cM
- (whd_betaiotazeta sigma (mkApp(c,l2)))
+ (whd_betaiotazeta sigma (EConstr.of_constr (mkApp(c,l2))))
| None ->
(match expand_key flags.modulo_delta curenv sigma cf1 with
| Some c ->
unirec_rec curenvnb pb opt substn
- (whd_betaiotazeta sigma (mkApp(c,l1))) cN
+ (whd_betaiotazeta sigma (EConstr.of_constr (mkApp(c,l1)))) cN
| None ->
error_cannot_unify curenv sigma (cM,cN)))
and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
let f1 () =
if isApp cM then
- let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
+ let f1l1 = whd_nored_state sigma (EConstr.of_constr cM,Stack.empty) in
if is_open_canonical_projection curenv sigma f1l1 then
- let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
+ let f2l2 = whd_nored_state sigma (EConstr.of_constr cN,Stack.empty) in
solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1017,9 +1017,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
else
try f1 () with e when precatchable_exception e ->
if isApp cN then
- let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
+ let f2l2 = whd_nored_state sigma (EConstr.of_constr cN, Stack.empty) in
if is_open_canonical_projection curenv sigma f2l2 then
- let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
+ let f1l1 = whd_nored_state sigma (EConstr.of_constr cM, Stack.empty) in
solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1044,13 +1044,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
in
try
let opt' = {opt with with_types = false} in
+ let inj = EConstr.Unsafe.to_constr in
let (substn,_,_) = Reductionops.Stack.fold2
- (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
+ (fun s u1 u -> unirec_rec curenvnb pb opt' s (inj u1) (substl ks (inj u)))
(evd,ms,es) us2 us in
let (substn,_,_) = Reductionops.Stack.fold2
- (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
+ (fun s u1 u -> unirec_rec curenvnb pb opt' s (inj u1) (substl ks (inj u)))
substn params1 params in
- let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb opt') substn ts ts1 in
+ let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s (inj u1) (inj u2)) substn ts ts1 in
let app = mkApp (c, Array.rev_of_list ks) in
(* let substn = unirec_rec curenvnb pb b false substn t cN in *)
unirec_rec curenvnb pb opt' substn c1 app
@@ -1206,7 +1207,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
if Int.equal n 0 then
Sigma (c, evd, p)
else
- match kind_of_term (whd_all env (Sigma.to_evar_map evd) cty) with
+ match kind_of_term (whd_all env (Sigma.to_evar_map evd) (EConstr.of_constr cty)) with
| Prod (_,c1,c2) ->
let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
@@ -1235,7 +1236,7 @@ let w_coerce_to_type env evd c cty mvty =
(* inh_conv_coerce_rigid_to should have reasoned modulo reduction
but there are cases where it though it was not rigid (like in
fst (nat,nat)) and stops while it could have seen that it is rigid *)
- let cty = Tacred.hnf_constr env evd cty in
+ let cty = Tacred.hnf_constr env evd (EConstr.of_constr cty) in
try_to_coerce env evd c cty tycon
let w_coerce env evd mv c =
@@ -1246,7 +1247,7 @@ let w_coerce env evd mv c =
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 = nf_betaiota sigma (nf_meta sigma t) in
+ let t = nf_betaiota sigma (EConstr.of_constr (nf_meta sigma t)) in
unify_0 env sigma CUMUL flags t u
let unify_type env sigma flags mv status c =
@@ -1270,7 +1271,7 @@ let order_metas metas =
(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
let solve_simple_evar_eqn ts env evd ev rhs =
- match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
+ match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,EConstr.of_constr rhs) with
| UnifFailure (evd,reason) ->
error_cannot_unify env evd ~reason (mkEvar ev,rhs);
| Success evd ->
@@ -1349,7 +1350,7 @@ let w_merge env with_types flags (evd,metas,evars) =
else
let evd' =
if occur_meta_evd evd mv c then
- if isMetaOf mv (whd_all env evd c) then evd
+ if isMetaOf mv (whd_all env evd (EConstr.of_constr c)) then evd
else error_cannot_unify env evd (mkMeta mv,c)
else
meta_assign mv (c,(status,TypeProcessed)) evd in
@@ -1415,7 +1416,7 @@ let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
types of metavars are unifiable with the types of their instances *)
let head_app sigma m =
- fst (whd_nored_state sigma (m, Stack.empty))
+ EConstr.Unsafe.to_constr (fst (whd_nored_state sigma (EConstr.of_constr m, Stack.empty)))
let check_types env flags (sigma,_,_ as subst) m n =
if isEvar_or_Meta (head_app sigma m) then
@@ -1577,7 +1578,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
(fun test -> match test.testing_state with
| None -> None
| Some (sigma,_,l) ->
- let c = applist (nf_evar sigma (local_strong whd_meta sigma c),l) in
+ let c = applist (nf_evar sigma (local_strong whd_meta sigma (EConstr.of_constr c)),l) in
let univs, subst = nf_univ_variables sigma in
Some (sigma,subst_univs_constr subst c))
@@ -1832,7 +1833,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
let w_unify_to_subterm_list env evd flags hdmeta oplist t =
List.fold_right
(fun op (evd,l) ->
- let op = whd_meta evd op in
+ let op = whd_meta evd (EConstr.of_constr op) in
if isMeta op then
if flags.allow_K_in_toplevel_higher_order_unification then (evd,op::l)
else error_abstraction_over_meta env evd hdmeta (destMeta op)
@@ -1905,15 +1906,16 @@ let secondOrderAbstractionAlgo dep =
if dep then secondOrderDependentAbstraction else secondOrderAbstraction
let w_unify2 env evd flags dep cv_pb ty1 ty2 =
- let c1, oplist1 = whd_nored_stack evd ty1 in
- let c2, oplist2 = whd_nored_stack evd ty2 in
- match kind_of_term c1, kind_of_term c2 with
+ let inj = EConstr.Unsafe.to_constr in
+ let c1, oplist1 = whd_nored_stack evd (EConstr.of_constr ty1) in
+ let c2, oplist2 = whd_nored_stack evd (EConstr.of_constr ty2) in
+ match EConstr.kind evd c1, EConstr.kind evd c2 with
| Meta p1, _ ->
(* Find the predicate *)
- secondOrderAbstractionAlgo dep env evd flags ty2 (p1,oplist1)
+ secondOrderAbstractionAlgo dep env evd flags ty2 (p1, List.map inj oplist1)
| _, Meta p2 ->
(* Find the predicate *)
- secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2)
+ secondOrderAbstractionAlgo dep env evd flags ty1 (p2, List.map inj oplist2)
| _ -> error "w_unify2"
(* The unique unification algorithm works like this: If the pattern is
@@ -1937,8 +1939,8 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
convertible and first-order otherwise. But if failed if e.g. the type of
Meta(1) had meta-variables in it. *)
let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
- let hd1,l1 = decompose_appvect (whd_nored evd ty1) in
- let hd2,l2 = decompose_appvect (whd_nored evd ty2) in
+ let hd1,l1 = decompose_appvect (whd_nored evd (EConstr.of_constr ty1)) in
+ let hd2,l2 = decompose_appvect (whd_nored evd (EConstr.of_constr ty2)) in
let is_empty1 = Array.is_empty l1 in
let is_empty2 = Array.is_empty l2 in
match kind_of_term hd1, not is_empty1, kind_of_term hd2, not is_empty2 with
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 75159bf8b..8c3de7cfd 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -99,13 +99,13 @@ let construct_of_constr_block = construct_of_constr false
let type_of_ind env (ind, u) =
type_of_inductive env (Inductive.lookup_mind_specif env ind, u)
-let build_branches_type env (mind,_ as _ind) mib mip u params dep p =
+let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
let rtbl = mip.mind_reloc_tbl in
(* [build_one_branch i cty] construit le type de la ieme branche (commence
a 0) et les lambda correspondant aux realargs *)
let build_one_branch i cty =
let typi = type_constructor mind mib u cty params in
- let decl,indapp = Reductionops.splay_prod env Evd.empty typi in
+ let decl,indapp = Reductionops.splay_prod env sigma (EConstr.of_constr typi) in
let decl_with_letin,_ = decompose_prod_assum typi in
let ((ind,u),cargs) = find_rectype_a env indapp in
let nparams = Array.length params in
@@ -131,28 +131,28 @@ let build_case_type dep p realargs c =
(* La fonction de normalisation *)
-let rec nf_val env v t = nf_whd env (whd_val v) t
+let rec nf_val env sigma v t = nf_whd env sigma (whd_val v) t
-and nf_vtype env v = nf_val env v crazy_type
+and nf_vtype env sigma v = nf_val env sigma v crazy_type
-and nf_whd env whd typ =
+and nf_whd env sigma whd typ =
match whd with
| Vsort s -> mkSort s
| Vprod p ->
- let dom = nf_vtype env (dom p) in
+ let dom = nf_vtype env sigma (dom p) in
let name = Name (Id.of_string "x") in
let vc = body_of_vfun (nb_rel env) (codom p) in
- let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) vc in
+ let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vc in
mkProd(name,dom,codom)
- | Vfun f -> nf_fun env f typ
- | Vfix(f,None) -> nf_fix env f
- | Vfix(f,Some vargs) -> fst (nf_fix_app env f vargs)
- | Vcofix(cf,_,None) -> nf_cofix env cf
+ | Vfun f -> nf_fun env sigma f typ
+ | Vfix(f,None) -> nf_fix env sigma f
+ | Vfix(f,Some vargs) -> fst (nf_fix_app env sigma f vargs)
+ | Vcofix(cf,_,None) -> nf_cofix env sigma cf
| Vcofix(cf,_,Some vargs) ->
- let cfd = nf_cofix env cf in
+ let cfd = nf_cofix env sigma cf in
let i,(_,ta,_) = destCoFix cfd in
let t = ta.(i) in
- let _, args = nf_args env vargs t in
+ let _, args = nf_args env sigma vargs t in
mkApp(cfd,args)
| Vconstr_const n ->
construct_of_constr_const env n typ
@@ -165,10 +165,10 @@ and nf_whd env whd typ =
| _ -> assert false
else (tag, 0) in
let capp,ctyp = construct_of_constr_block env tag typ in
- let args = nf_bargs env b ofs ctyp in
+ let args = nf_bargs env sigma b ofs ctyp in
mkApp(capp,args)
| Vatom_stk(Aid idkey, stk) ->
- constr_type_of_idkey env idkey stk
+ constr_type_of_idkey env sigma idkey stk
| Vatom_stk(Aind ((mi,i) as ind), stk) ->
let mib = Environ.lookup_mind mi env in
let nb_univs =
@@ -178,12 +178,12 @@ and nf_whd env whd typ =
let mk u =
let pind = (ind, u) in (mkIndU pind, type_of_ind env pind)
in
- nf_univ_args ~nb_univs mk env stk
+ nf_univ_args ~nb_univs mk env sigma stk
| Vatom_stk(Atype u, stk) -> assert false
| Vuniv_level lvl ->
assert false
-and nf_univ_args ~nb_univs mk env stk =
+and nf_univ_args ~nb_univs mk env sigma stk =
let u =
if Int.equal nb_univs 0 then Univ.Instance.empty
else match stk with
@@ -195,9 +195,9 @@ and nf_univ_args ~nb_univs mk env stk =
| _ -> assert false
in
let (t,ty) = mk u in
- nf_stk ~from:nb_univs env t ty stk
+ nf_stk ~from:nb_univs env sigma t ty stk
-and constr_type_of_idkey env (idkey : Vars.id_key) stk =
+and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
match idkey with
| ConstKey cst ->
let cbody = Environ.lookup_constant cst env in
@@ -208,30 +208,30 @@ and constr_type_of_idkey env (idkey : Vars.id_key) stk =
let mk u =
let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst)
in
- nf_univ_args ~nb_univs mk env stk
+ nf_univ_args ~nb_univs mk env sigma stk
| VarKey id ->
let ty = NamedDecl.get_type (lookup_named id env) in
- nf_stk env (mkVar id) ty stk
+ nf_stk env sigma (mkVar id) ty stk
| RelKey i ->
let n = (nb_rel env - i) in
let ty = RelDecl.get_type (lookup_rel n env) in
- nf_stk env (mkRel n) (lift n ty) stk
+ nf_stk env sigma (mkRel n) (lift n ty) stk
-and nf_stk ?from:(from=0) env c t stk =
+and nf_stk ?from:(from=0) env sigma c t stk =
match stk with
| [] -> c
| Zapp vargs :: stk ->
if nargs vargs >= from then
- let t, args = nf_args ~from:from env vargs t in
- nf_stk env (mkApp(c,args)) t stk
+ let t, args = nf_args ~from:from env sigma vargs t in
+ nf_stk env sigma (mkApp(c,args)) t stk
else
let rest = from - nargs vargs in
- nf_stk ~from:rest env c t stk
+ nf_stk ~from:rest env sigma c t stk
| Zfix (f,vargs) :: stk ->
assert (from = 0) ;
- let fa, typ = nf_fix_app env f vargs in
+ let fa, typ = nf_fix_app env sigma f vargs in
let _,_,codom = decompose_prod env typ in
- nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
+ nf_stk env sigma (mkApp(fa,[|c|])) (subst1 c codom) stk
| Zswitch sw :: stk ->
assert (from = 0) ;
let ((mind,_ as ind), u), allargs = find_rectype_a env t in
@@ -241,34 +241,34 @@ and nf_stk ?from:(from=0) env c t stk =
let pT =
hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
let pT = whd_all env pT in
- let dep, p = nf_predicate env (ind,u) mip params (type_of_switch sw) pT in
+ let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
- let btypes = build_branches_type env ind mib mip u params dep p in
+ let btypes = build_branches_type env sigma ind mib mip u params dep p in
(* calcul des branches *)
let bsw = branch_of_switch (nb_rel env) sw in
let mkbranch i (n,v) =
let decl,decl_with_letin,codom = btypes.(i) in
- let b = nf_val (Termops.push_rels_assum decl env) v codom in
+ let b = nf_val (Termops.push_rels_assum decl env) sigma v codom in
Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type dep p realargs c in
let ci = case_info sw in
- nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+ nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk
| Zproj p :: stk ->
assert (from = 0) ;
let p' = Projection.make p true in
- let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in
- nf_stk env (mkProj(p',c)) ty stk
+ let ty = Inductiveops.type_of_projection_knowing_arg env sigma p' (EConstr.of_constr c) (EConstr.of_constr t) in
+ nf_stk env sigma (mkProj(p',c)) ty stk
-and nf_predicate env ind mip params v pT =
+and nf_predicate env sigma ind mip params v pT =
match whd_val v, kind_of_term pT with
| Vfun f, Prod _ ->
let k = nb_rel env in
let vb = body_of_vfun k f in
let name,dom,codom = decompose_prod env pT in
let dep,body =
- nf_predicate (push_rel (LocalAssum (name,dom)) env) ind mip params vb codom in
+ nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
dep, mkLambda(name,dom,body)
| Vfun f, _ ->
let k = nb_rel env in
@@ -278,33 +278,33 @@ and nf_predicate env ind mip params v pT =
let rargs = Array.init n (fun i -> mkRel (n-i)) in
let params = if Int.equal n 0 then params else Array.map (lift n) params in
let dom = mkApp(mkIndU ind,Array.append params rargs) in
- let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) vb in
+ let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in
true, mkLambda(name,dom,body)
- | _, _ -> false, nf_val env v crazy_type
+ | _, _ -> false, nf_val env sigma v crazy_type
-and nf_args env vargs ?from:(f=0) t =
+and nf_args env sigma vargs ?from:(f=0) t =
let t = ref t in
let len = nargs vargs - f in
let args =
Array.init len
(fun i ->
let _,dom,codom = decompose_prod env !t in
- let c = nf_val env (arg vargs (f+i)) dom in
+ let c = nf_val env sigma (arg vargs (f+i)) dom in
t := subst1 c codom; c) in
!t,args
-and nf_bargs env b ofs t =
+and nf_bargs env sigma b ofs t =
let t = ref t in
let len = bsize b - ofs in
let args =
Array.init len
(fun i ->
let _,dom,codom = decompose_prod env !t in
- let c = nf_val env (bfield b (i+ofs)) dom in
+ let c = nf_val env sigma (bfield b (i+ofs)) dom in
t := subst1 c codom; c) in
args
-and nf_fun env f typ =
+and nf_fun env sigma f typ =
let k = nb_rel env in
let vb = body_of_vfun k f in
let name,dom,codom =
@@ -314,46 +314,46 @@ and nf_fun env f typ =
CErrors.anomaly
(Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
in
- let body = nf_val (push_rel (LocalAssum (name,dom)) env) vb codom in
+ let body = nf_val (push_rel (LocalAssum (name,dom)) env) sigma vb codom in
mkLambda(name,dom,body)
-and nf_fix env f =
+and nf_fix env sigma f =
let init = current_fix f in
let rec_args = rec_args f in
let k = nb_rel env in
let vb, vt = reduce_fix k f in
let ndef = Array.length vt in
- let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
+ let ft = Array.map (fun v -> nf_val env sigma v crazy_type) vt in
let name = Array.init ndef (fun _ -> (Name (Id.of_string "Ffix"))) in
(* Third argument of the tuple is ignored by push_rec_types *)
let env = push_rec_types (name,ft,ft) env in
(* We lift here because the types of arguments (in tt) will be evaluated
in an environment where the fixpoints have been pushed *)
- let norm_vb v t = nf_fun env v (lift ndef t) in
+ let norm_vb v t = nf_fun env sigma v (lift ndef t) in
let fb = Util.Array.map2 norm_vb vb ft in
mkFix ((rec_args,init),(name,ft,fb))
-and nf_fix_app env f vargs =
- let fd = nf_fix env f in
+and nf_fix_app env sigma f vargs =
+ let fd = nf_fix env sigma f in
let (_,i),(_,ta,_) = destFix fd in
let t = ta.(i) in
- let t, args = nf_args env vargs t in
+ let t, args = nf_args env sigma vargs t in
mkApp(fd,args),t
-and nf_cofix env cf =
+and nf_cofix env sigma cf =
let init = current_cofix cf in
let k = nb_rel env in
let vb,vt = reduce_cofix k cf in
let ndef = Array.length vt in
- let cft = Array.map (fun v -> nf_val env v crazy_type) vt in
+ let cft = Array.map (fun v -> nf_val env sigma v crazy_type) vt in
let name = Array.init ndef (fun _ -> (Name (Id.of_string "Fcofix"))) in
let env = push_rec_types (name,cft,cft) env in
- let cfb = Util.Array.map2 (fun v t -> nf_val env v t) vb cft in
+ let cfb = Util.Array.map2 (fun v t -> nf_val env sigma v t) vb cft in
mkCoFix (init,(name,cft,cfb))
-let cbv_vm env c t =
+let cbv_vm env sigma c t =
let v = Vconv.val_of_constr env c in
- nf_val env v t
+ nf_val env sigma v t
let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb)
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 58f5b14e1..bc6eec851 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -10,4 +10,4 @@ open Term
open Environ
(** {6 Reduction functions } *)
-val cbv_vm : env -> constr -> types -> constr
+val cbv_vm : env -> Evd.evar_map -> constr -> types -> constr
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 13:13:49 +0000