From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- pretyping/tacred.ml | 266 ++++++++++++++++++++++++++++------------------------ 1 file changed, 143 insertions(+), 123 deletions(-) (limited to 'pretyping/tacred.ml') 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 -- cgit v1.2.3