diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 466 |
1 files changed, 241 insertions, 225 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 820a81b5..518d2f60 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -11,24 +13,27 @@ open CErrors open Util open Names open Term -open Vars open Libnames open Globnames open Termops +open Environ +open EConstr +open Vars open Find_subterm open Namegen -open Environ open CClosure open Reductionops open Cbv open Patternops open Locus -open Sigma.Notations + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (* Errors *) type reduction_tactic_error = - InvalidAbstraction of env * Evd.evar_map * constr * (env * Type_errors.type_error) + InvalidAbstraction of env * Evd.evar_map * EConstr.constr * (env * Type_errors.type_error) exception ReductionTacticError of reduction_tactic_error @@ -38,7 +43,7 @@ exception Elimconst exception Redelimination let error_not_evaluable r = - errorlabstrm "error_not_evaluable" + user_err ~hdr:"error_not_evaluable" (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ spc () ++ str "to an evaluable reference.") @@ -54,13 +59,11 @@ let is_evaluable env = function | EvalVarRef id -> is_evaluable_var env id let value_of_evaluable_ref env evref u = - let open Context.Named.Declaration in match evref with | EvalConstRef con -> - (try constant_value_in env (con,u) - with NotEvaluableConst IsProj -> - raise (Invalid_argument "value_of_evaluable_ref")) - | EvalVarRef id -> lookup_named id env |> get_value |> Option.get + let u = Unsafe.to_instance u in + EConstr.of_constr (constant_value_in env (con, u)) + | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst @@ -72,17 +75,17 @@ let global_of_evaluable_reference = function | EvalVarRef id -> VarRef id type evaluable_reference = - | EvalConst of constant + | EvalConst of Constant.t | EvalVar of Id.t | EvalRel of int - | EvalEvar of existential + | EvalEvar of EConstr.existential -let evaluable_reference_eq r1 r2 = match r1, r2 with -| EvalConst c1, EvalConst c2 -> eq_constant c1 c2 +let evaluable_reference_eq sigma r1 r2 = match r1, r2 with +| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) -> - Evar.equal e1 e2 && Array.equal eq_constr ctx1 ctx2 + Evar.equal e1 e2 && Array.equal (EConstr.eq_constr sigma) ctx1 ctx2 | _ -> false let mkEvalRef ref u = @@ -90,45 +93,49 @@ let mkEvalRef ref u = | EvalConst cst -> mkConstU (cst,u) | EvalVar id -> mkVar id | EvalRel n -> mkRel n - | EvalEvar ev -> mkEvar ev + | EvalEvar ev -> EConstr.mkEvar ev -let isEvalRef env c = match kind_of_term c with +let isEvalRef env sigma c = match EConstr.kind sigma c with | Const (sp,_) -> is_evaluable env (EvalConstRef sp) | Var id -> is_evaluable env (EvalVarRef id) | Rel _ | Evar _ -> true | _ -> false -let destEvalRefU c = match kind_of_term c with +let destEvalRefU sigma c = match EConstr.kind sigma c with | Const (cst,u) -> EvalConst cst, u - | Var id -> (EvalVar id, Univ.Instance.empty) - | Rel n -> (EvalRel n, Univ.Instance.empty) - | Evar ev -> (EvalEvar ev, Univ.Instance.empty) - | _ -> anomaly (Pp.str "Not an unfoldable reference") + | Var id -> (EvalVar id, EInstance.empty) + | Rel n -> (EvalRel n, EInstance.empty) + | Evar ev -> (EvalEvar ev, EInstance.empty) + | _ -> anomaly (Pp.str "Not an unfoldable reference.") let unsafe_reference_opt_value env sigma eval = match eval with | EvalConst cst -> (match (lookup_constant cst env).Declarations.const_body with - | Declarations.Def c -> Some (Mod_subst.force_constr c) + | Declarations.Def c -> Some (EConstr.of_constr (Mod_subst.force_constr c)) | _ -> None) | EvalVar id -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + env |> lookup_named id |> NamedDecl.get_value | EvalRel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value - | EvalEvar ev -> Evd.existential_opt_value sigma ev + env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) + | EvalEvar ev -> + match EConstr.kind sigma (mkEvar ev) with + | Evar _ -> None + | c -> Some (EConstr.of_kind c) let reference_opt_value env sigma eval u = match eval with - | EvalConst cst -> constant_opt_value_in env (cst,u) + | EvalConst cst -> + let u = EInstance.kind sigma u in + Option.map EConstr.of_constr (constant_opt_value_in env (cst,u)) | EvalVar id -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + env |> lookup_named id |> NamedDecl.get_value | EvalRel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value - | EvalEvar ev -> Evd.existential_opt_value sigma ev + env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) + | EvalEvar ev -> + match EConstr.kind sigma (mkEvar ev) with + | Evar _ -> None + | c -> Some (EConstr.of_kind c) exception NotEvaluable let reference_value env sigma c u = @@ -179,18 +186,18 @@ let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation" the xp..x1. *) -let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = +let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) = let n = List.length labs in let nargs = List.length args in if nargs > n then raise Elimconst; 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 - && Array.for_all (noccurn (k+nbfix)) bds + Array.for_all (Vars.noccurn sigma k) tys + && Array.for_all (Vars.noccurn sigma (k+nbfix)) bds && k <= n then (k, List.nth labs (k-1)) @@ -204,7 +211,7 @@ let check_fix_reversibility 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 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) @@ -233,17 +240,18 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - Some (EvalConst (con_with_label kn (Label.of_id id))) in + Some (EvalConst (Constant.change_label kn (Label.of_id id))) in match refi with | None -> None | Some ref -> try match unsafe_reference_opt_value env sigma ref with | None -> None | Some c -> - let labs',ccl = decompose_lam c in + let labs',ccl = decompose_lam sigma c in let _, l' = whd_betalet_stack sigma ccl in let labs' = List.map snd labs' in (** ppedrot: there used to be generic equality on terms here *) + let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in if List.equal eq_constr labs' labs && List.equal eq_constr l l' then Some (minfxargs,ref) else None @@ -258,16 +266,16 @@ 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 - match kind_of_term c' with + match EConstr.kind sigma 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 | Fix fix when not onlyproj -> - (try check_fix_reversibility labs l fix + (try check_fix_reversibility sigma labs l fix with Elimconst -> NotAnElimination) - | Case (_,_,d,_) when isRel d && not onlyproj -> EliminationCases n + | Case (_,_,d,_) when isRel sigma d && not onlyproj -> EliminationCases n | Case (_,_,d,_) -> srec env n labs true d - | Proj (p, d) when isRel d -> EliminationProj n + | Proj (p, d) when isRel sigma d -> EliminationProj n | _ -> NotAnElimination in match unsafe_reference_opt_value env sigma ref with @@ -278,7 +286,7 @@ 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 nargs = List.length l in - match kind_of_term c' with + match EConstr.kind sigma c' with | Lambda (na,t,g) when List.is_empty l -> let open Context.Rel.Declaration in srec (push_rel (LocalAssum (na,t)) env) (minarg+1) (t::labs) ref g @@ -294,11 +302,11 @@ let compute_consteval_mutual_fix env sigma ref = let new_minarg = max (minarg'+minarg-nargs) minarg' in EliminationMutualFix (new_minarg,ref,(refs,infos)) | _ -> assert false) - | _ when isEvalRef env c' -> + | _ when isEvalRef env sigma c' -> (* Forget all \'s and args and do as if we had started with c' *) - let ref,_ = destEvalRefU c' in + let ref,_ = destEvalRefU sigma c' in (match unsafe_reference_opt_value env sigma ref with - | None -> anomaly (Pp.str "Should have been trapped by compute_direct") + | None -> anomaly (Pp.str "Should have been trapped by compute_direct.") | Some c -> srec env (minarg-nargs) [] ref c) | _ -> (* Should not occur *) NotAnElimination in @@ -355,17 +363,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) @@ -385,21 +393,20 @@ let substl_with_function subst sigma constr = 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 | (fx, Some (min, ref)) -> - let sigma = Sigma.Unsafe.of_evar_map !evd in - let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in - let sigma = Sigma.to_evar_map sigma in + let sigma = !evd in + let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy 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) @@ -409,28 +416,28 @@ exception Partial reduction is solved by the expanded fix term. *) 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 set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in let rec check strict c = let c' = whd_betaiotazeta sigma c in - let (h,rcargs) = decompose_app c' in - match kind_of_term h with + let (h,rcargs) = decompose_app_vect sigma c' in + match EConstr.kind sigma 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 - | (Var _|Const _) when isEvalRef env h -> - (let ev, u = destEvalRefU h in + Array.iter (check strict) rcargs + | (Var _|Const _) when isEvalRef env sigma h -> + (let ev, u = destEvalRefU sigma 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 (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 (mkApp(h',rcargs))) + | None -> Array.iter (check strict) rcargs) + | _ -> EConstr.iter sigma (check strict) c' in check true c; !evm @@ -441,16 +448,18 @@ let substl_checking_arity env subst sigma c = let sigma' = solve_arity_problem env sigma minargs body in (* we propagate the constraints: solved problems are substituted; the other ones are replaced by the function symbol *) - let rec nf_fix c = - match kind_of_term c with - Evar(i,[|fx;f|] as ev) when Evar.Map.mem i minargs -> - (match Evd.existential_opt_value sigma' ev with - Some c' -> c' - | None -> f) - | _ -> map_constr nf_fix c in + let rec nf_fix c = match EConstr.kind sigma c with + | Evar (i,[|fx;f|]) when Evar.Map.mem i minargs -> + (** FIXME: find a less hackish way of doing this *) + begin match EConstr.kind sigma' c with + | Evar _ -> f + | c -> EConstr.of_kind c + end + | _ -> EConstr.map sigma nf_fix c + in nf_fix body -type fix_reduction_result = NotReducible | Reduced of (constr*constr list) +type fix_reduction_result = NotReducible | Reduced of (constr * constr list) let reduce_fix whdfun sigma fix stack = match fix_recarg fix (Stack.append_app_list stack Stack.empty) with @@ -458,8 +467,8 @@ let reduce_fix whdfun sigma fix stack = | 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') + (match EConstr.kind sigma recarg'hd with + | Construct _ -> Reduced (contract_fix sigma fix, stack') | _ -> NotReducible) let contract_fix_use_function env sigma f @@ -467,20 +476,20 @@ let contract_fix_use_function env sigma f 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 (nf_beta env 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 + (match EConstr.kind sigma recarg'hd with | Construct _ -> Reduced (contract_fix_use_function env sigma f fix,stack') | _ -> NotReducible) @@ -491,16 +500,16 @@ let contract_cofix_use_function env sigma f 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 (nf_beta env sigma bodies.(bodynum)) let reduce_mind_case_use_function func env sigma mia = - match kind_of_term mia.mconstr with + 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) @@ -511,13 +520,13 @@ let reduce_mind_case_use_function func env sigma mia = mutual inductive, try to reuse the global name if 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) - in - try match constant_opt_value_in env kn with + let (kn, u) = destConst sigma func in + let kn = Constant.change_label kn (Label.of_id id) in + let cst = (kn, EInstance.kind sigma u) in + try match constant_opt_value_in env cst with | None -> None (* TODO: check kn is correct *) - | Some _ -> Some (minargs,mkConstU kn) + | Some _ -> Some (minargs,mkConstU (kn, u)) with Not_found -> None else fun _ -> None in @@ -527,45 +536,56 @@ let reduce_mind_case_use_function func env sigma mia = | _ -> assert false -let match_eval_ref env constr = - match kind_of_term 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) +let match_eval_ref env sigma constr stack = + match EConstr.kind sigma constr with + | Const (sp, u) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + (lazy (EConstr.to_constr sigma (applist (constr,stack)))); + if is_evaluable env (EvalConstRef sp) then Some (EvalConst sp, u) else None + | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, EInstance.empty) + | Rel i -> Some (EvalRel i, EInstance.empty) + | Evar ev -> Some (EvalEvar ev, EInstance.empty) | _ -> None -let match_eval_ref_value env sigma constr = - match kind_of_term constr with - | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> - Some (constant_value_in env (sp, u)) +let match_eval_ref_value env sigma constr stack = + match EConstr.kind sigma constr with + | Const (sp, u) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + (lazy (EConstr.to_constr sigma (applist (constr,stack)))); + if is_evaluable env (EvalConstRef sp) then + let u = EInstance.kind sigma u in + Some (EConstr.of_constr (constant_value_in env (sp, u))) + else + None + | Proj (p, c) when not (Projection.unfolded p) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + (lazy (EConstr.to_constr sigma (applist (constr,stack)))); + if is_evaluable env (EvalConstRef (Projection.constant p)) then + Some (mkProj (Projection.unfold p, c)) + else None | Var id when is_evaluable env (EvalVarRef id) -> - let open Context.Named.Declaration in - lookup_named id env |> get_value + env |> lookup_named id |> NamedDecl.get_value | Rel n -> - let open Context.Rel.Declaration in - lookup_rel n env |> map_value (lift n) |> get_value - | Evar ev -> Evd.existential_opt_value sigma ev + env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) | _ -> None 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 cargs with | Some (ref, u) -> (match reference_opt_value env sigma ref u with | None -> raise Redelimination | Some gvalue -> - if reducible_mind_case gvalue then + 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))) | 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 @@ -578,7 +598,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 @@ -587,11 +607,11 @@ let reduce_projection env sigma pb (recarg'hd,stack') stack = let reduce_proj env sigma whfun whfun' c = 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 @@ -608,7 +628,7 @@ 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 @@ -619,27 +639,26 @@ let whd_nothing_for_iota env sigma s = (match lookup_named id env with | LocalDef (_,body,_) -> whrec (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) + | Const (const, u) when is_transparent_constant full_transparent_state const -> + let u = EInstance.kind sigma u in + (match constant_opt_value_in env (const, u) with + | 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; @@ -664,7 +683,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 @@ -676,24 +695,24 @@ 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) -> (nf_beta env 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 - if evaluable_reference_eq ref refgoal then + if evaluable_reference_eq sigma ref refgoal then (c,args) else let c', lrest = whd_betalet_stack sigma (applist(c,args)) in - descend (destEvalRefU c') lrest in + descend (destEvalRefU sigma 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) -> (nf_beta env sigma c, rest), nocase) | NotAnElimination when unfold_nonelim -> let c = reference_value env sigma ref u in (whd_betaiotazeta sigma (applist (c, largs)), []), nocase @@ -709,7 +728,7 @@ 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 + match EConstr.kind sigma (fst rarg) with | Construct _ -> List.assign stack i (applist rarg) | _ -> raise Redelimination) stack l @@ -720,13 +739,15 @@ and reduce_params env sigma stack l = and whd_simpl_stack env sigma = 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.to_list stack 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 (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) -> @@ -766,12 +787,12 @@ and whd_simpl_stack env sigma = with Redelimination -> s') | _ -> - match match_eval_ref env x with + match match_eval_ref env sigma x stack 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 @@ -787,8 +808,8 @@ and whd_simpl_stack env sigma = and whd_construct_stack env sigma s = 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 cargs with | Some (ref, u) -> (match reference_opt_value env sigma ref u with | None -> raise Redelimination @@ -804,12 +825,12 @@ 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 = clos_norm_flags betaiotazeta env sigma c in let rec redrec env x = let x = whd_betaiota sigma x in - match kind_of_term x with + 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 @@ -817,17 +838,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, 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 @@ -836,7 +857,7 @@ 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 *) @@ -848,7 +869,7 @@ let try_red_product env sigma c = let red_product env sigma c = try try_red_product env sigma c - with Redelimination -> error "No head constant to reduce." + with Redelimination -> user_err (str "No head constant to reduce.") (* (* This old version of hnf uses betadeltaiota instead of itself (resp @@ -906,8 +927,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = let whd_simpl_stack = if Flags.profile then - let key = Profile.declare_profile "whd_simpl_stack" in - Profile.profile3 key whd_simpl_stack + let key = CProfile.declare_profile "whd_simpl_stack" in + CProfile.profile3 key whd_simpl_stack else whd_simpl_stack (* Same as [whd_simpl] but also reduces constants that do not hide a @@ -917,13 +938,13 @@ let whd_simpl_stack = let whd_simpl_orelse_delta_but_fix env sigma c = 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 constr stack with | Some c -> - (match kind_of_term (strip_lam c) with + (match EConstr.kind sigma (snd (decompose_lam sigma c)) with | CoFix _ | Fix _ -> s' | Proj (p,t) when - (match kind_of_term constr with - | Const (c', _) -> eq_constant (Projection.constant p) c' + (match EConstr.kind sigma constr with + | Const (c', _) -> Constant.equal (Projection.constant p) c' | _ -> false) -> let pb = Environ.lookup_projection p env in if List.length stack <= pb.Declarations.proj_npars then @@ -948,9 +969,9 @@ let simpl env sigma c = strong whd_simpl env sigma c (* Reduction at specific subterms *) let matches_head env sigma c t = - match kind_of_term t with + match EConstr.kind sigma t with | App (f,_) -> Constr_matching.matches env sigma c f - | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p)) + | Proj (p, _) -> Constr_matching.matches env sigma c (mkConstU (Projection.constant p, EInstance.empty)) | _ -> raise Constr_matching.PatternMatchingFailure (** FIXME: Specific function to handle projections: it ignores what happens on the @@ -958,26 +979,25 @@ let matches_head env sigma c t = of the projection and its eta expanded form. *) let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = - match kind_of_term c with + match EConstr.kind sigma c with | Proj (p, r) -> (* Treat specially for partial applications *) let t = Retyping.expand_projection env sigma p r [] in - let hdf, al = destApp t in + let hdf, al = destApp sigma t in let a = al.(Array.length al - 1) in let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in let app' = f acc app in let a' = f acc a in - (match kind_of_term app' with + (match EConstr.kind sigma app' with | App (hdf', al') when hdf' == hdf -> (* Still the same projection, we ignore the change in parameters *) mkProj (p, a') | _ -> mkApp (app', [| a' |])) - | _ -> map_constr_with_binders_left_to_right g f acc c + | _ -> map_constr_with_binders_left_to_right sigma g f acc c -let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> +let e_contextually byhead (occs,c) f = begin fun env sigma t -> let (nowhere_except_in,locs) = Locusops.convert_occs occs in let maxocc = List.fold_right max locs 0 in let pos = ref 1 in - let sigma = Sigma.to_evar_map sigma in (** FIXME: we do suspicious things with this evarmap *) let evd = ref sigma in let rec traverse nested (env,c as envc) t = @@ -993,12 +1013,12 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> incr pos; if ok then begin if Option.has_some nested then - errorlabstrm "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str "."); + user_err (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str "."); (* 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 - (evd := Sigma.to_evar_map evm; t) + let (evm, t) = (f subst) env !evd t in + (evd := evm; t) end else traverse_below nested envc t @@ -1007,7 +1027,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> and traverse_below nested envc t = (* when byhead, find other occurrences without matching again partial application with same head *) - match kind_of_term t with + match EConstr.kind !evd t with | App (f,l) when byhead -> mkApp (f, Array.map_left (traverse nested envc) l) | Proj (p,c) when byhead -> mkProj (p,traverse nested envc c) | _ -> @@ -1017,24 +1037,21 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> in let t' = traverse None (env,c) t in if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; - Sigma.Unsafe.of_pair (t', !evd) - end } + (!evd, t') + end let contextually byhead occs f env sigma t = - let f' subst = { e_redfun = begin fun env sigma t -> - Sigma.here (f subst env (Sigma.to_evar_map sigma) t) sigma - end } in - let Sigma (c, _, _) = (e_contextually byhead occs f').e_redfun env (Sigma.Unsafe.of_evar_map sigma) t in - c + let f' subst env sigma t = sigma, f subst env sigma t in + snd (e_contextually byhead occs f' env sigma t) (* linear bindings (following pretty-printer) of the value of name in c. * n is the number of the next occurrence of name. * ol is the occurrence list to find. *) let match_constr_evaluable_ref sigma c evref = - match kind_of_term 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 + match EConstr.kind sigma c, evref with + | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u + | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty | _, _ -> None let substlin env sigma evalref n (nowhere_except_in,locs) c = @@ -1053,7 +1070,7 @@ 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 + map_constr_with_binders_left_to_right sigma (fun _ () -> ()) substrec () c in @@ -1066,11 +1083,11 @@ let string_of_evaluable_ref env = function string_of_qualid (Nametab.shortest_qualid_of_global (vars_of_env env) (ConstRef kn)) -let unfold env sigma name = +let unfold env sigma name c = if is_evaluable env name then - clos_norm_flags (unfold_red name) env sigma + clos_norm_flags (unfold_red name) env sigma c else - error (string_of_evaluable_ref env name^" is opaque.") + user_err Pp.(str (string_of_evaluable_ref env name^" is opaque.")) (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. @@ -1080,13 +1097,13 @@ let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in if Int.equal nbocc 1 then - error ((string_of_evaluable_ref env name)^" does not occur."); + user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur.")); let rest = List.filter (fun o -> o >= nbocc) locs in let () = match rest with | [] -> () | _ -> error_invalid_occurrence rest in - nf_betaiotazeta sigma uc + nf_betaiotazeta env sigma uc in match occs with | NoOccurrences -> c @@ -1102,21 +1119,21 @@ let unfoldn loccname env sigma c = let fold_one_com com env sigma c = let rcom = try red_product env sigma com - with Redelimination -> error "Not reducible." in + with Redelimination -> user_err Pp.(str "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 (clos_norm_flags unfold_side_red env sigma rcom) c in - if not (eq_constr a c) then - subst1 com a + let a = subst_term sigma (clos_norm_flags unfold_side_red env sigma rcom) c in + if not (EConstr.eq_constr sigma a c) then + Vars.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 rcom c in - subst1 com a + let a = subst_term sigma rcom c in + Vars.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 + List.fold_right (fun com c -> fold_one_com com env sigma c) (List.rev cl) c (* call by value reduction functions *) @@ -1134,38 +1151,37 @@ let compute = cbv_betadeltaiota (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only * the specified occurrences. *) -let abstract_scheme env (locc,a) (c, sigma) = +let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in - let na = named_hd env ta Anonymous in - if occur_meta ta then error "Cannot find a type for the generalisation."; - if occur_meta a then + let na = named_hd env sigma ta Anonymous in + if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation."); + if occur_meta sigma a then mkLambda (na,ta,c), sigma else let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in mkLambda (na,ta,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 pattern_occs loccs_trm = begin fun env sigma c -> + let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (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) + (sigma, applist(abstr_trm, List.map snd loccs_trm)) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) - end } + end (* Used in several tactics. *) let check_privacy env ind = let spec = Inductive.lookup_mind_specif env (fst ind) in if Inductive.is_private spec then - errorlabstrm "" (str "case analysis on a private type.") + user_err (str "case analysis on a private type.") else ind let check_not_primitive_record env ind = let spec = Inductive.lookup_mind_specif env (fst ind) in if Inductive.is_primitive_record spec then - errorlabstrm "" (str "case analysis on a primitive record type: " ++ + user_err (str "case analysis on a primitive record type: " ++ str "use projections or let instead.") else ind @@ -1175,30 +1191,30 @@ 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 - match kind_of_term (fst (decompose_app t)) with + match EConstr.kind sigma (fst (decompose_app_vect sigma t)) with | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l) | Prod (n,ty,t') -> let open Context.Rel.Declaration in if allow_product then elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) else - errorlabstrm "" (str"Not an inductive definition.") + user_err (str"Not an inductive definition.") | _ -> (* 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 - match kind_of_term (fst (decompose_app t')) with + match EConstr.kind sigma (fst (decompose_app_vect sigma t')) with | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l) - | _ -> errorlabstrm "" (str"Not an inductive product.") + | _ -> user_err (str"Not an inductive product.") in elimrec env t [] -let reduce_to_quantified_ind x = reduce_to_ind_gen true x -let reduce_to_atomic_ind x = reduce_to_ind_gen false x +let reduce_to_quantified_ind env sigma c = reduce_to_ind_gen true env sigma c +let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma c let find_hnf_rectype env sigma t = let ind,t = reduce_to_atomic_ind env sigma t in - ind, snd (decompose_app t) + ind, snd (decompose_app sigma t) (* Reduce the weak-head redex [beta,iota/fix/cofix[all],cast,zeta,simpl/delta] or raise [NotStepReducible] if not a weak-head redex *) @@ -1207,13 +1223,13 @@ exception NotStepReducible let one_step_reduce env sigma c = 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 @@ -1225,8 +1241,8 @@ 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 sigma x -> + let ref,u = destEvalRefU sigma x in (try fst (red_elim_const env sigma ref u stack) with Redelimination -> @@ -1239,7 +1255,7 @@ let one_step_reduce env sigma c = applist (redrec (c,[])) let error_cannot_recognize ref = - errorlabstrm "" + user_err (str "Cannot recognize a statement based on " ++ Nametab.pr_global_env Id.Set.empty ref ++ str".") @@ -1253,8 +1269,8 @@ 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 - match kind_of_term c with + let c, _ = decompose_app_vect sigma t in + match EConstr.kind sigma c with | Prod (n,ty,t') -> if allow_product then let open Context.Rel.Declaration in @@ -1263,12 +1279,12 @@ let reduce_to_ref_gen allow_product env sigma ref t = error_cannot_recognize ref | _ -> try - if eq_gr (global_of_constr c) ref + if eq_gr (fst (global_of_constr sigma c)) ref then it_mkProd_or_LetIn t l else raise Not_found with Not_found -> try - let t' = nf_betaiota sigma (one_step_reduce env sigma t) in + let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in elimrec env t' l with NotStepReducible -> error_cannot_recognize ref in |