diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 1009 |
1 files changed, 593 insertions, 416 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b18314f7..b4e0459c 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,34 +1,34 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp +open Errors open Util open Names -open Nameops open Term +open Vars open Libnames +open Globnames open Termops +open Find_subterm open Namegen -open Declarations -open Inductive -open Libobject open Environ open Closure open Reductionops open Cbv -open Glob_term -open Pattern -open Matching +open Patternops +open Locus +open Pretype_errors (* Errors *) type reduction_tactic_error = - InvalidAbstraction of env * constr * (env * Type_errors.type_error) + InvalidAbstraction of env * Evd.evar_map * constr * (env * Type_errors.type_error) exception ReductionTacticError of reduction_tactic_error @@ -39,27 +39,28 @@ exception Redelimination let error_not_evaluable r = errorlabstrm "error_not_evaluable" - (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Idset.empty r ++ + (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ spc () ++ str "to an evaluable reference.") let is_evaluable_const env cst = - is_transparent (ConstKey cst) && evaluable_constant cst env + is_transparent env (ConstKey cst) && + (evaluable_constant cst env || is_projection cst env) let is_evaluable_var env id = - is_transparent (VarKey id) && evaluable_named id env + is_transparent env (VarKey id) && evaluable_named id env let is_evaluable env = function | EvalConstRef cst -> is_evaluable_const env cst | EvalVarRef id -> is_evaluable_var env id -let value_of_evaluable_ref env = function - | EvalConstRef con -> constant_value env con +let value_of_evaluable_ref env evref u = + match evref with + | EvalConstRef con -> + (try constant_value_in env (con,u) + with NotEvaluableConst IsProj -> + raise (Invalid_argument "value_of_evaluable_ref")) | EvalVarRef id -> Option.get (pi2 (lookup_named id env)) -let constr_of_evaluable_ref = function - | EvalConstRef con -> mkConst con - | EvalVarRef id -> mkVar id - let evaluable_of_global_reference env = function | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst | VarRef id when is_evaluable_var env id -> EvalVarRef id @@ -71,31 +72,55 @@ let global_of_evaluable_reference = function type evaluable_reference = | EvalConst of constant - | EvalVar of identifier + | EvalVar of Id.t | EvalRel of int | EvalEvar of existential -let mkEvalRef = function - | EvalConst cst -> mkConst cst +let evaluable_reference_eq r1 r2 = match r1, r2 with +| EvalConst c1, EvalConst c2 -> eq_constant 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 +| _ -> false + +let mkEvalRef ref u = + match ref with + | EvalConst cst -> mkConstU (cst,u) | EvalVar id -> mkVar id | EvalRel n -> mkRel n | EvalEvar ev -> mkEvar ev let isEvalRef env c = match kind_of_term c with - | Const sp -> is_evaluable env (EvalConstRef sp) + | Const (sp,_) -> is_evaluable env (EvalConstRef sp) | Var id -> is_evaluable env (EvalVarRef id) | Rel _ | Evar _ -> true | _ -> false -let destEvalRef c = match kind_of_term c with - | Const cst -> EvalConst cst - | Var id -> EvalVar id - | Rel n -> EvalRel n - | Evar ev -> EvalEvar ev - | _ -> anomaly "Not an unfoldable reference" +let destEvalRefU c = match kind_of_term 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") + +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) + | _ -> None) + | EvalVar id -> + let (_,v,_) = lookup_named id env in + v + | EvalRel n -> + let (_,v,_) = lookup_rel n env in + Option.map (lift n) v + | EvalEvar ev -> Evd.existential_opt_value sigma ev -let reference_opt_value sigma env = function - | EvalConst cst -> constant_opt_value env cst +let reference_opt_value env sigma eval u = + match eval with + | EvalConst cst -> constant_opt_value_in env (cst,u) | EvalVar id -> let (_,v,_) = lookup_named id env in v @@ -105,8 +130,8 @@ let reference_opt_value sigma env = function | EvalEvar ev -> Evd.existential_opt_value sigma ev exception NotEvaluable -let reference_value sigma env c = - match reference_opt_value sigma env c with +let reference_value env sigma c u = + match reference_opt_value env sigma c u with | None -> raise NotEvaluable | Some d -> d @@ -121,28 +146,14 @@ type constant_evaluation = ((int*evaluable_reference) option array * (int * (int * constr) list * int)) | EliminationCases of int + | EliminationProj of int | NotAnElimination (* We use a cache registered as a global table *) -let eval_table = ref Cmap_env.empty - -type frozen = (int * constant_evaluation) Cmap_env.t - -let init () = - eval_table := Cmap_env.empty +type frozen = constant_evaluation Cmap.t -let freeze () = - !eval_table - -let unfreeze ct = - eval_table := ct - -let _ = - Summary.declare_summary "evaluation" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init } +let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation" (* [compute_consteval] determines whether c is an "elimination constant" @@ -177,8 +188,8 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = (function d -> match kind_of_term d with | Rel k -> if - array_for_all (noccurn k) tys - && array_for_all (noccurn (k+nbfix)) bds + Array.for_all (noccurn k) tys + && Array.for_all (noccurn (k+nbfix)) bds then (k, List.nth labs (k-1)) else @@ -187,12 +198,14 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = raise Elimconst) args in let reversible_rels = List.map fst li in - if not (list_distinct reversible_rels) then + if not (List.distinct_f Int.compare reversible_rels) then raise Elimconst; - list_iter_i (fun i t_i -> - if not (List.mem_assoc (i+1) li) then - let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in - if list_intersect fvs reversible_rels <> [] then 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 + match List.intersect Int.equal fvs reversible_rels with + | [] -> () + | _ -> raise Elimconst) labs; let k = lv.(i) in if k < nargs then @@ -210,57 +223,64 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = let invert_name labs l na0 env sigma ref = function | Name id -> let minfxargs = List.length l in - if na0 <> Name id then + begin match na0 with + | Name id' when Id.equal id' id -> + Some (minfxargs,ref) + | _ -> let refi = match ref with | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - Some (EvalConst (con_with_label kn (label_of_id id))) in + Some (EvalConst (con_with_label kn (Label.of_id id))) in match refi with | None -> None | Some ref -> - try match reference_opt_value sigma env ref with + try match unsafe_reference_opt_value env sigma ref with | None -> None | Some c -> let labs',ccl = decompose_lam c in let _, l' = whd_betalet_stack sigma ccl in let labs' = List.map snd labs' in - if labs' = labs & l = l' then Some (minfxargs,ref) + (** 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) else None with Not_found (* Undefined ref *) -> None - else Some (minfxargs,ref) + end | Anonymous -> None (* Actually, should not occur *) (* [compute_consteval_direct] expand all constant in a whole, but [compute_consteval_mutual_fix] only one by one, until finding the last one before the Fix if the latter is mutually defined *) -let compute_consteval_direct sigma env ref = - let rec srec env n labs c = +let compute_consteval_direct env sigma ref = + let rec srec env n labs onlyproj c = let c',l = whd_betadelta_stack env sigma c in match kind_of_term c' with - | Lambda (id,t,g) when l=[] -> - srec (push_rel (id,None,t) env) (n+1) (t::labs) g - | Fix fix -> + | Lambda (id,t,g) when List.is_empty l && not onlyproj -> + srec (push_rel (id,None,t) env) (n+1) (t::labs) onlyproj g + | Fix fix when not onlyproj -> (try check_fix_reversibility labs l fix with Elimconst -> NotAnElimination) - | Case (_,_,d,_) when isRel d -> EliminationCases n + | Case (_,_,d,_) when isRel d && not onlyproj -> EliminationCases n + | Case (_,_,d,_) -> srec env n labs true d + | Proj (p, d) when isRel d -> EliminationProj n | _ -> NotAnElimination in - match reference_opt_value sigma env ref with + match unsafe_reference_opt_value env sigma ref with | None -> NotAnElimination - | Some c -> srec env 0 [] c + | Some c -> srec env 0 [] false c -let compute_consteval_mutual_fix sigma env 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 nargs = List.length l in match kind_of_term c' with - | Lambda (na,t,g) when l=[] -> + | Lambda (na,t,g) when List.is_empty l -> srec (push_rel (na,None,t) env) (minarg+1) (t::labs) ref g | Fix ((lv,i),(names,_,_)) -> (* Last known constant wrapping Fix is ref = [labs](Fix l) *) - (match compute_consteval_direct sigma env ref with + (match compute_consteval_direct env sigma ref with | NotAnElimination -> (*Above const was eliminable but this not!*) NotAnElimination | EliminationFix (minarg',minfxargs,infos) -> @@ -272,32 +292,32 @@ let compute_consteval_mutual_fix sigma env ref = | _ -> assert false) | _ when isEvalRef env c' -> (* Forget all \'s and args and do as if we had started with c' *) - let ref = destEvalRef c' in - (match reference_opt_value sigma env ref with - | None -> anomaly "Should have been trapped by compute_direct" + let ref,_ = destEvalRefU c' in + (match unsafe_reference_opt_value env sigma ref with + | None -> anomaly (Pp.str "Should have been trapped by compute_direct") | Some c -> srec env (minarg-nargs) [] ref c) | _ -> (* Should not occur *) NotAnElimination in - match reference_opt_value sigma env ref with + match unsafe_reference_opt_value env sigma ref with | None -> (* Should not occur *) NotAnElimination | Some c -> srec env 0 [] ref c -let compute_consteval sigma env ref = - match compute_consteval_direct sigma env ref with - | EliminationFix (_,_,(nbfix,_,_)) when nbfix <> 1 -> - compute_consteval_mutual_fix sigma env ref +let compute_consteval env sigma ref = + match compute_consteval_direct env sigma ref with + | EliminationFix (_,_,(nbfix,_,_)) when not (Int.equal nbfix 1) -> + compute_consteval_mutual_fix env sigma ref | elim -> elim -let reference_eval sigma env = function +let reference_eval env sigma = function | EvalConst cst as ref -> (try - Cmap_env.find cst !eval_table + Cmap.find cst !eval_table with Not_found -> begin - let v = compute_consteval sigma env ref in - eval_table := Cmap_env.add cst v !eval_table; + let v = compute_consteval env sigma ref in + eval_table := Cmap.add cst v !eval_table; v end) - | ref -> compute_consteval sigma env ref + | ref -> compute_consteval env sigma ref (* If f is bound to EliminationFix (n',infos), then n' is the minimal number of args for starting the reduction and infos is @@ -320,16 +340,16 @@ let reference_eval sigma env = function The type Tij' is Tij[yi(j-1)..y1 <- ai(j-1)..a1] *) -let x = Name (id_of_string "x") +let x = Name default_dependent_ident -let make_elim_fun (names,(nbfix,lv,n)) largs = - let lu = list_firstn n (list_of_stack largs) in +let make_elim_fun (names,(nbfix,lv,n)) u largs = + let lu = List.firstn n largs in let p = List.length lv in let lyi = List.map fst lv in let la = - list_map_i (fun q aq -> + List.map_i (fun q aq -> (* k from the comment is q+1 *) - try mkRel (p+1-(list_index (n-q) lyi)) + try mkRel (p+1-(List.index Int.equal (n-q) lyi)) with Not_found -> aq) 0 (List.map (lift p) lu) in @@ -337,10 +357,10 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = match names.(i) with | None -> None | Some (minargs,ref) -> - let body = applistc (mkEvalRef ref) la in + let body = applistc (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 + 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 mkLambda (x,tij',c)) 1 body (List.rev lv) in Some (minargs,g) @@ -349,37 +369,32 @@ let make_elim_fun (names,(nbfix,lv,n)) largs = do so that the reduction uses this extra information *) let dummy = mkProp -let vfx = id_of_string"_expanded_fix_" -let vfun = id_of_string"_eliminator_function_" +let vfx = Id.of_string "_expanded_fix_" +let vfun = Id.of_string "_eliminator_function_" +let venv = val_of_named_context [(vfx, None, dummy); (vfun, None, dummy)] (* Mark every occurrence of substituted vars (associated to a function) as a problem variable: an evar that can be instantiated either by vfx (expanded fixpoint) or vfun (named function). *) -let substl_with_function subst constr = - let cnt = ref 0 in - let evd = ref Evd.empty in - let minargs = ref Intmap.empty in +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 - Rel i when k<i -> - if i <= k + Array.length v then - match v.(i-k-1) with - | (fx,Some(min,ref)) -> - decr cnt; - evd := Evd.add !evd !cnt - (Evd.make_evar - (val_of_named_context - [(vfx,None,dummy);(vfun,None,dummy)]) - dummy); - minargs := Intmap.add !cnt min !minargs; - lift k (mkEvar(!cnt,[|fx;ref|])) - | (fx,None) -> lift k fx - else mkRel (i - Array.length v) - | _ -> - map_constr_with_binders succ subst_total k c in + let rec subst_total k c = match kind_of_term 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, evk) = Evarutil.new_pure_evar venv !evd dummy in + evd := sigma; + minargs := Evar.Map.add evk min !minargs; + lift k (mkEvar (evk, [|fx;ref|])) + | (fx, None) -> lift k fx + else mkRel (i - Array.length v) + | _ -> + map_constr_with_binders succ subst_total k c in let c = subst_total 0 constr in - (c,!evd,!minargs) + (c, !evd, !minargs) exception Partial @@ -392,15 +407,16 @@ let solve_arity_problem env sigma fxminargs c = let c' = whd_betaiotazeta sigma c in let (h,rcargs) = decompose_app c' in match kind_of_term h with - Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) -> - let minargs = Intmap.find i fxminargs in + 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 strict then set_fix i else raise Partial; List.iter (check strict) rcargs | (Var _|Const _) when isEvalRef env h -> - (match reference_opt_value sigma env (destEvalRef h) with - Some 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 with Partial -> @@ -411,42 +427,52 @@ let solve_arity_problem env sigma fxminargs c = check true c; !evm -let substl_checking_arity env subst c = +let substl_checking_arity env subst sigma c = (* we initialize the problem: *) - let body,sigma,minargs = substl_with_function subst c in + let body,sigma,minargs = substl_with_function subst sigma c in (* we collect arity constraints *) 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 Intmap.mem i minargs -> + 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 nf_fix body +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 + | 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') + | _ -> NotReducible) let contract_fix_use_function env sigma f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in - let lbodies = list_tabulate make_Fi nbodies in - substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum)) + let lbodies = List.init nbodies make_Fi in + substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum)) let reduce_fix_use_function env sigma f whfun fix stack = - match fix_recarg fix stack with + 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 (* The recarg cannot be a local def, no worry about the right env *) - (recarg, empty_stack) + (recarg, []) else - whfun (recarg, empty_stack) in - let stack' = stack_assign stack recargnum (app_stack recarg') in + whfun recarg in + let stack' = List.assign stack recargnum (applist recarg') in (match kind_of_term recarg'hd with | Construct _ -> Reduced (contract_fix_use_function env sigma f fix,stack') @@ -456,21 +482,21 @@ let contract_cofix_use_function env sigma f (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = (mkCoFix(j,typedbodies), f j) in - let subbodies = list_tabulate make_Fi nbodies in + let subbodies = List.init nbodies make_Fi in substl_checking_arity env (List.rev subbodies) - (nf_beta sigma bodies.(bodynum)) + sigma (nf_beta sigma bodies.(bodynum)) let reduce_mind_case_use_function func env sigma mia = match kind_of_term mia.mconstr with - | Construct(ind_sp,i) -> - let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in + | 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 let minargs = List.length mia.mcargs in fun i -> - if i = bodynum then Some (minargs,func) + if Int.equal i bodynum then Some (minargs,func) else match names.(i) with | Anonymous -> None | Name id -> @@ -478,12 +504,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 = con_with_label (destConst func) (label_of_id id) + let kn = map_puniverses (fun x -> con_with_label x (Label.of_id id)) + (destConst func) in - try match constant_opt_value env kn with + try match constant_opt_value_in env kn with | None -> None (* TODO: check kn is correct *) - | Some _ -> Some (minargs,mkConst kn) + | Some _ -> Some (minargs,mkConstU kn) with Not_found -> None else fun _ -> None in @@ -492,226 +519,277 @@ let reduce_mind_case_use_function func env sigma mia = mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false -let special_red_case env sigma whfun (ci, p, c, lf) = + +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) + | _ -> 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)) + | Var id when is_evaluable env (EvalVarRef id) -> + let (_,v,_) = lookup_named id env in v + | Rel n -> let (_,v,_) = lookup_rel n env in + Option.map (lift n) v + | Evar ev -> Evd.existential_opt_value sigma ev + | _ -> None + +let special_red_case env sigma whfun (ci, p, c, lf) = let rec redrec s = let (constr, cargs) = whfun s in - if isEvalRef env constr then - let ref = destEvalRef constr in - match reference_opt_value sigma env ref with - | None -> raise Redelimination - | Some gvalue -> - if reducible_mind_case gvalue then - reduce_mind_case_use_function constr env sigma - {mP=p; mconstr=gvalue; mcargs=list_of_stack cargs; - mci=ci; mlf=lf} - else - redrec (gvalue, cargs) - else + match match_eval_ref env 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 + 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 - {mP=p; mconstr=constr; mcargs=list_of_stack cargs; + {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf} else raise Redelimination in - redrec (c, empty_stack) - -(* data structure to hold the map kn -> rec_args for simpl *) - -type behaviour = { - b_nargs: int; - b_recargs: int list; - b_dont_expose_case: bool; -} - -let behaviour_table = ref (Refmap.empty : behaviour Refmap.t) - -let _ = - Summary.declare_summary "simplbehaviour" - { Summary.freeze_function = (fun () -> !behaviour_table); - Summary.unfreeze_function = (fun x -> behaviour_table := x); - Summary.init_function = (fun () -> behaviour_table := Refmap.empty) } - -type simpl_flag = [ `SimplDontExposeCase | `SimplNeverUnfold ] -type req = - | ReqLocal - | ReqGlobal of global_reference * (int list * int * simpl_flag list) - -let load_simpl_behaviour _ (_,(_,(r, b))) = - behaviour_table := Refmap.add r b !behaviour_table - -let cache_simpl_behaviour o = load_simpl_behaviour 1 o - -let classify_simpl_behaviour = function - | ReqLocal, _ -> Dispose - | ReqGlobal _, _ as o -> Substitute o - -let subst_simpl_behaviour (subst, (_, (r,o as orig))) = - ReqLocal, - let r' = fst (subst_global subst r) in if r==r' then orig else (r',o) - -let discharge_simpl_behaviour = function - | _,(ReqGlobal (ConstRef c, req), (_, b)) -> - let c' = pop_con c in - let vars = Lib.section_segment_of_constant c in - let extra = List.length vars in - let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in - let recargs' = List.map ((+) extra) b.b_recargs in - let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in - Some (ReqGlobal (ConstRef c', req), (ConstRef c', b')) - | _ -> None + redrec c -let rebuild_simpl_behaviour = function - | req, (ConstRef c, _ as x) -> req, x - | _ -> assert false - -let inSimplBehaviour = declare_object { (default_object "SIMPLBEHAVIOUR") with - load_function = load_simpl_behaviour; - cache_function = cache_simpl_behaviour; - classify_function = classify_simpl_behaviour; - subst_function = subst_simpl_behaviour; - discharge_function = discharge_simpl_behaviour; - rebuild_function = rebuild_simpl_behaviour; -} - -let set_simpl_behaviour local r (recargs, nargs, flags as req) = - let nargs = if List.mem `SimplNeverUnfold flags then max_int else nargs in - let behaviour = { - b_nargs = nargs; b_recargs = recargs; - b_dont_expose_case = List.mem `SimplDontExposeCase flags } in - let req = if local then ReqLocal else ReqGlobal (r, req) in - Lib.add_anonymous_leaf (inSimplBehaviour (req, (r, behaviour))) -;; - -let get_simpl_behaviour r = - try - let b = Refmap.find r !behaviour_table in - let flags = - if b.b_nargs = max_int then [`SimplNeverUnfold] - else if b.b_dont_expose_case then [`SimplDontExposeCase] else [] in - Some (b.b_recargs, (if b.b_nargs = max_int then -1 else b.b_nargs), flags) - with Not_found -> None +let recargs = function + | EvalVar _ | EvalRel _ | EvalEvar _ -> None + | EvalConst c -> ReductionBehaviour.get (ConstRef c) -let get_behaviour = function - | EvalVar _ | EvalRel _ | EvalEvar _ -> raise Not_found - | EvalConst c -> Refmap.find (ConstRef c) !behaviour_table +let reduce_projection env sigma pb (recarg'hd,stack') stack = + (match kind_of_term recarg'hd with + | Construct _ -> + let proj_narg = + pb.Declarations.proj_npars + pb.Declarations.proj_arg + in Reduced (List.nth stack' proj_narg, stack) + | _ -> NotReducible) + +let reduce_proj env sigma whfun whfun' c = + let rec redrec s = + match kind_of_term 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 + | Construct _ -> + let proj_narg = + let pb = lookup_projection proj env in + pb.Declarations.proj_npars + pb.Declarations.proj_arg + in List.nth cargs proj_narg + | _ -> raise Redelimination) + | Case (n,p,c,brs) -> + let c' = redrec c in + let p = (n,p,c',brs) in + (try special_red_case env sigma whfun' p + with Redelimination -> mkCase p) + | _ -> raise Redelimination + in redrec c -let recargs r = - try let b = get_behaviour r in Some (b.b_recargs, b.b_nargs) - with Not_found -> None -let dont_expose_case r = - try (get_behaviour r).b_dont_expose_case with Not_found -> false +let dont_expose_case = function + | EvalVar _ | EvalRel _ | EvalEvar _ -> false + | EvalConst c -> + Option.cata (fun (_,_,z) -> List.mem `ReductionDontExposeCase z) + false (ReductionBehaviour.get (ConstRef c)) + +let whd_nothing_for_iota env sigma s = + let rec whrec (x, stack as s) = + match kind_of_term x with + | Rel n -> + (match lookup_rel n env with + | (_,Some body,_) -> whrec (lift n body, stack) + | _ -> s) + | Var id -> + (match lookup_named id env with + | (_,Some body,_) -> whrec (body, stack) + | _ -> s) + | Evar ev -> + (try whrec (Evd.existential_value sigma ev, stack) + with Evd.NotInstantiatedEvar | Not_found -> s) + | Meta ev -> + (try whrec (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) + | None -> s) + | LetIn (_,b,_,c) -> stacklam whrec [b] 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 + | _ -> s) + + | x -> s + in + decompose_app (Stack.zip (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 largs = - let nargs = stack_args_size largs in - let largs, unfold_anyway, unfold_nonelim = +let rec red_elim_const env sigma ref u largs = + let nargs = List.length largs in + let largs, unfold_anyway, unfold_nonelim, nocase = match recargs ref with - | None -> largs, false, false - | Some (_,n) when nargs < n -> raise Redelimination - | Some (x::l,_) when nargs <= List.fold_left max x l -> raise Redelimination - | Some (l,n) -> - List.fold_left (fun stack i -> - let arg = stack_nth stack i in - let rarg = whd_construct_state env sigma (arg, empty_stack) in - match kind_of_term (fst rarg) with - | Construct _ -> stack_assign stack i (app_stack rarg) - | _ -> raise Redelimination) - largs l, n >= 0 && l = [] && nargs >= n, - n >= 0 && l <> [] && nargs >= n in - try match reference_eval sigma env ref with + | None -> largs, false, false, false + | Some (_,n,f) when nargs < n || List.mem `ReductionNeverUnfold f -> raise Redelimination + | Some (x::l,_,_) when nargs <= List.fold_left max x l -> raise Redelimination + | Some (l,n,f) -> + let is_empty = match l with [] -> true | _ -> false in + reduce_params env sigma largs l, + n >= 0 && is_empty && nargs >= n, + n >= 0 && not is_empty && nargs >= n, + List.mem `ReductionDontExposeCase f + in + try match reference_eval env sigma ref with | EliminationCases n when nargs >= n -> - let c = reference_value sigma env ref in - let c', lrest = whd_betadelta_state env sigma (c,largs) in - let whfun = whd_simpl_state env sigma in - (special_red_case env sigma whfun (destCase c'), lrest) + 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 + | 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 + let whfun = whd_construct_stack env sigma in + let whfun' = whd_simpl_stack env sigma in + (reduce_proj env sigma whfun whfun' c', lrest), nocase | EliminationFix (min,minfxargs,infos) when nargs >= min -> - let c = reference_value sigma env ref in - let d, lrest = whd_betadelta_state env sigma (c,largs) in - let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in - let whfun = whd_construct_state env sigma in + let c = reference_value env sigma ref u in + 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 | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta sigma c, rest)) + | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase) | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min -> - let rec descend ref args = - let c = reference_value sigma env ref in - if ref = refgoal then + let rec descend (ref,u) args = + let c = reference_value env sigma ref u in + if evaluable_reference_eq ref refgoal then (c,args) else - let c', lrest = whd_betalet_state sigma (c,args) in - descend (destEvalRef c') lrest in - let (_, midargs as s) = descend ref largs in - let d, lrest = whd_betadelta_state env sigma s in - let f = make_elim_fun refinfos midargs in - let whfun = whd_construct_state env sigma in + let c', lrest = whd_betalet_stack sigma (applist(c,args)) in + descend (destEvalRefU 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 | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta sigma c, rest)) - | NotAnElimination when unfold_nonelim -> - let c = reference_value sigma env ref in - whd_betaiotazeta sigma (app_stack (c, largs)), empty_stack + | Reduced (c,rest) -> (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 | _ -> raise Redelimination with Redelimination when unfold_anyway -> - let c = reference_value sigma env ref in - whd_betaiotazeta sigma (app_stack (c, largs)), empty_stack + let c = reference_value env sigma ref u in + (whd_betaiotazeta sigma (applist (c, largs)), []), nocase + +and reduce_params env sigma stack l = + let len = List.length stack in + List.fold_left (fun stack i -> + if len <= i then raise Redelimination + 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) + | _ -> raise Redelimination) + stack l + (* reduce to whd normal form or to an applied constant that does not hide a reducible iota/fix/cofix redex (the "simpl" tactic) *) -and whd_simpl_state env sigma s = - let rec redrec (x, stack as s) = +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 | Lambda (na,t,c) -> - (match decomp_stack stack with - | None -> s - | Some (a,rest) -> stacklam redrec [a] c rest) - | LetIn (n,b,t,c) -> stacklam redrec [b] c stack - | App (f,cl) -> redrec (f, append_stack cl stack) - | Cast (c,_,_) -> redrec (c, stack) + (match stack with + | [] -> s' + | a :: rest -> redrec (beta_applist (x,stack))) + | LetIn (n,b,t,c) -> redrec (applist (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) -> (try - redrec (special_red_case env sigma redrec (ci,p,c,lf), stack) + redrec (applist(special_red_case env sigma redrec (ci,p,c,lf), stack)) with - Redelimination -> s) + Redelimination -> s') | Fix fix -> - (try match reduce_fix (whd_construct_state env) sigma fix stack with - | Reduced s' -> redrec s' - | NotReducible -> s - with Redelimination -> s) - | _ when isEvalRef env x -> - let ref = destEvalRef x in + (try match reduce_fix (whd_construct_stack env) sigma fix stack with + | Reduced s' -> redrec (applist s') + | NotReducible -> s' + with Redelimination -> s') + + | Proj (p, c) -> + (try + let unf = Projection.unfolded p in + if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then + let pb = lookup_projection p env in + (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with + | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f -> + (* simpl never *) s' + | false, Some (l, n, f) when not (List.is_empty l) -> + let l' = List.map_filter (fun i -> + let idx = (i - (pb.Declarations.proj_npars + 1)) in + if idx < 0 then None else Some idx) l in + let stack = reduce_params env sigma stack l' in + (match reduce_projection env sigma pb + (whd_construct_stack env sigma c) stack + with + | Reduced s' -> redrec (applist s') + | NotReducible -> s') + | _ -> + match reduce_projection env sigma pb (whd_construct_stack env sigma c) stack with + | Reduced s' -> redrec (applist s') + | NotReducible -> s') + else s' + with Redelimination -> s') + + | _ -> + match match_eval_ref env x with + | Some (ref, u) -> (try - let hd, _ as s' = redrec (red_elim_const env sigma ref stack) in - let rec is_case x = match kind_of_term x with - | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x - | App (hd, _) -> is_case hd - | Case _ -> true - | _ -> false in - if dont_expose_case ref && is_case hd then raise Redelimination - else s' - with Redelimination -> - s) - | _ -> s + 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 + | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x + | App (hd, _) -> is_case hd + | Case _ -> true + | _ -> false in + if nocase && is_case hd then raise Redelimination + else s'' + with Redelimination -> s') + | None -> s' in - redrec s + redrec (* reduce until finding an applied constructor or fail *) -and whd_construct_state env sigma s = - let (constr, cargs as s') = whd_simpl_state env sigma s in +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 if isEvalRef env constr then - let ref = destEvalRef constr in - match reference_opt_value sigma env ref with - | None -> raise Redelimination - | Some gvalue -> whd_construct_state env sigma (gvalue, cargs) - else - raise Redelimination + else match match_eval_ref env 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))) + | _ -> raise Redelimination (************************************************************************) (* Special Purpose Reduction Strategies *) @@ -724,35 +802,47 @@ and whd_construct_state env sigma s = let try_red_product env sigma c = let simpfun = clos_norm_flags betaiotazeta env sigma in let rec redrec env x = + let x = whd_betaiota sigma x in match kind_of_term x with | App (f,l) -> (match kind_of_term f with | Fix fix -> - let stack = append_stack l empty_stack in + let stack = Stack.append_app l Stack.empty in (match fix_recarg fix stack with | None -> raise Redelimination | Some (recargnum,recarg) -> let recarg' = redrec env recarg in - let stack' = stack_assign stack recargnum recarg' in - simpfun (app_stack (f,stack'))) + let stack' = Stack.assign stack recargnum recarg' in + simpfun (Stack.zip (f,stack'))) | _ -> simpfun (appvect (redrec env f, l))) | Cast (c,_,_) -> redrec env c | Prod (x,a,b) -> mkProd (x, a, redrec (push_rel (x,None,a) env) b) | LetIn (x,a,b,t) -> redrec env (subst1 a t) | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf)) - | _ when isEvalRef env x -> + | Proj (p, c) -> + let c' = + match kind_of_term c with + | Construct _ -> c + | _ -> redrec env c + in + let pb = lookup_projection p env in + (match reduce_projection env sigma pb (whd_betaiotazeta_stack sigma c') [] with + | Reduced s -> simpfun (applist s) + | NotReducible -> raise Redelimination) + | _ -> + (match match_eval_ref env x with + | Some (ref, u) -> (* TO DO: re-fold fixpoints after expansion *) (* to get true one-step reductions *) - let ref = destEvalRef x in - (match reference_opt_value sigma env ref with + (match reference_opt_value env sigma ref u with | None -> raise Redelimination | Some c -> c) - | _ -> raise Redelimination + | _ -> raise Redelimination) in redrec env c let red_product env sigma c = try try_red_product env sigma c - with Redelimination -> error "Not reducible." + with Redelimination -> error "No head constant to reduce." (* (* This old version of hnf uses betadeltaiota instead of itself (resp @@ -798,7 +888,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = (try redrec (red_elim_const env sigma ref stack) with Redelimination -> - match reference_opt_value sigma env ref with + match reference_opt_value env sigma ref with | Some c -> (match kind_of_term (strip_lam c) with | CoFix _ | Fix _ -> s @@ -808,96 +898,160 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = in app_stack (redrec (c, empty_stack)) *) +let whd_simpl_stack = + if Flags.profile then + let key = Profile.declare_profile "whd_simpl_stack" in + Profile.profile3 key whd_simpl_stack + else whd_simpl_stack + (* Same as [whd_simpl] but also reduces constants that do not hide a reducible fix, but does this reduction of constants only until it immediately hides a non reducible fix or a cofix *) let whd_simpl_orelse_delta_but_fix env sigma c = let rec redrec s = - let (constr, stack as s') = whd_simpl_state env sigma s in - if isEvalRef env constr then - match reference_opt_value sigma env (destEvalRef constr) with - | Some c -> - (match kind_of_term (strip_lam c) with - | CoFix _ | Fix _ -> s' - | _ -> redrec (c, stack)) - | None -> s' - else s' - in app_stack (redrec (c, empty_stack)) + let (constr, stack as s') = whd_simpl_stack env sigma s in + match match_eval_ref_value env sigma 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 + | 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))) + | None -> s' + in + let simpfun = clos_norm_flags betaiota env sigma in + simpfun (applist (redrec c)) let hnf_constr = whd_simpl_orelse_delta_but_fix (* The "simpl" reduction tactic *) let whd_simpl env sigma c = - app_stack (whd_simpl_state env sigma (c, empty_stack)) + applist (whd_simpl_stack env sigma c) let simpl env sigma c = strong whd_simpl env sigma c (* Reduction at specific subterms *) -let matches_head c t = +let matches_head env sigma c t = match kind_of_term t with - | App (f,_) -> matches c f - | _ -> raise PatternMatchingFailure + | App (f,_) -> Constr_matching.matches env sigma c f + | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p)) + | _ -> raise Constr_matching.PatternMatchingFailure + +let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false -let contextually byhead ((nowhere_except_in,locs),c) f env sigma t = +(** FIXME: Specific function to handle projections: it ignores what happens on the + parameters. This is a temporary fix while rewrite etc... are not up to equivalence + 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 + | 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 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 + | 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 + +let e_contextually byhead (occs,c) f 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 rec traverse (env,c as envc) t = - if nowhere_except_in & (!pos > maxocc) then t + let evd = ref sigma in + let rec traverse nested (env,c as envc) t = + if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t else try - let subst = if byhead then matches_head c t else matches c t in + let subst = + if byhead then matches_head env sigma c t + else Constr_matching.matches env sigma c t in let ok = - if nowhere_except_in then List.mem !pos locs - else not (List.mem !pos locs) in + if nowhere_except_in then Int.List.mem !pos locs + else not (Int.List.mem !pos locs) in incr pos; - if ok then - f subst env sigma t - else if byhead then - (* find other occurrences of c in t; TODO: ensure left-to-right *) - let (f,l) = destApp t in - mkApp (f, array_map_left (traverse envc) l) + 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 "."); + (* Skip inner occurrences for stable counting of occurrences *) + if locs != [] then + ignore (traverse_below (Some (!pos-1)) envc t); + let evm, t = f subst env !evd t in + (evd := evm; t) + end else - t - with PatternMatchingFailure -> - map_constr_with_binders_left_to_right - (fun d (env,c) -> (push_rel d env,lift_pattern 1 c)) - traverse envc t + traverse_below nested envc t + with Constr_matching.PatternMatchingFailure -> + traverse_below nested envc 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 + | 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) + | _ -> + change_map_constr_with_binders_left_to_right + (fun d (env,c) -> (push_rel d env,lift_pattern 1 c)) + (traverse nested) envc sigma t in - let t' = traverse (env,c) t in + let t' = traverse None (env,c) t in if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; - t' + !evd, t' + +let contextually byhead occs f env sigma t = + 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 occurence of name. * ol is the occurence list to find. *) -let substlin env evalref n (nowhere_except_in,locs) c = +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 + | _, _ -> None + +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 = value_of_evaluable_ref env evalref in - let term = constr_of_evaluable_ref evalref in + let value u = value_of_evaluable_ref env evalref u in let rec substrec () c = - if nowhere_except_in & !pos > maxocc then c - else if eq_constr c term then - let ok = - if nowhere_except_in then List.mem !pos locs - else not (List.mem !pos locs) in - incr pos; - if ok then value else c - else - map_constr_with_binders_left_to_right - (fun _ () -> ()) - substrec () c + if nowhere_except_in && !pos > maxocc then c + else + match match_constr_evaluable_ref sigma c evalref with + | Some u -> + let ok = + if nowhere_except_in then Int.List.mem !pos locs + else not (Int.List.mem !pos locs) in + incr pos; + if ok then value u else c + | None -> + map_constr_with_binders_left_to_right + (fun _ () -> ()) + substrec () c in let t' = substrec () c in (!pos, t') let string_of_evaluable_ref env = function - | EvalVarRef id -> string_of_id id + | EvalVarRef id -> Id.to_string id | EvalConstRef kn -> string_of_qualid (Nametab.shortest_qualid_of_global (vars_of_env env) (ConstRef kn)) @@ -908,19 +1062,31 @@ let unfold env sigma name = else error (string_of_evaluable_ref env name^" is opaque.") +let is_projection env = function + | EvalVarRef _ -> false + | EvalConstRef c -> Environ.is_projection c env + (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. * Performs a betaiota reduction after unfolding. *) -let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c = - if locs = [] then if nowhere_except_in then c else unfold env sigma name c - else - let (nbocc,uc) = substlin env name 1 plocs c in - if nbocc = 1 then +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."); let rest = List.filter (fun o -> o >= nbocc) locs in - if rest <> [] then error_invalid_occurrence rest; - nf_betaiota sigma uc + let () = match rest with + | [] -> () + | _ -> error_invalid_occurrence rest + in + nf_betaiotazeta sigma uc + in + match occs with + | NoOccurrences -> 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 = @@ -962,25 +1128,39 @@ 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 sigma (locc,a) c = +let abstract_scheme env (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 - mkLambda (na,ta,c) + mkLambda (na,ta,c), sigma else - mkLambda (na,ta,subst_closed_term_occ locc a c) + let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in + mkLambda (na,ta,c'), sigma' let pattern_occs loccs_trm env sigma c = - let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in + let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in try let _ = Typing.type_of env sigma abstr_trm in - applist(abstr_trm, List.map snd loccs_trm) + sigma, applist(abstr_trm, List.map snd loccs_trm) with Type_errors.TypeError (env',t) -> - raise (ReductionTacticError (InvalidAbstraction (env,abstr_trm,(env',t)))) + raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) (* 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.") + 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: " ++ + str "use projections or let instead.") + else ind + (* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name return name, B and t' *) @@ -988,7 +1168,7 @@ 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 - | Ind ind-> (ind, it_mkProd_or_LetIn t l) + | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l) | Prod (n,ty,t') -> if allow_product then elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l) @@ -999,7 +1179,7 @@ let reduce_to_ind_gen allow_product env sigma t = was partially the case between V5.10 and V8.1 *) let t' = whd_betadeltaiota env sigma t in match kind_of_term (fst (decompose_app t')) with - | Ind ind-> (ind, it_mkProd_or_LetIn t' l) + | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l) | _ -> errorlabstrm "" (str"Not an inductive product.") in elimrec env t [] @@ -1007,7 +1187,7 @@ let reduce_to_ind_gen allow_product env sigma 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 rec find_hnf_rectype env sigma t = +let find_hnf_rectype env sigma t = let ind,t = reduce_to_atomic_ind env sigma t in ind, snd (decompose_app t) @@ -1020,69 +1200,66 @@ let one_step_reduce env sigma c = let rec redrec (x, stack) = match kind_of_term x with | Lambda (n,t,c) -> - (match decomp_stack stack with - | None -> raise NotStepReducible - | Some (a,rest) -> (subst1 a c, rest)) - | App (f,cl) -> redrec (f, append_stack cl stack) + (match stack with + | [] -> raise NotStepReducible + | a :: rest -> (subst1 a c, rest)) + | App (f,cl) -> redrec (f, (Array.to_list cl)@stack) | LetIn (_,f,_,cl) -> (subst1 f cl,stack) | Cast (c,_,_) -> redrec (c,stack) | Case (ci,p,c,lf) -> (try - (special_red_case env sigma (whd_simpl_state env sigma) + (special_red_case env sigma (whd_simpl_stack env sigma) (ci,p,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> - (match reduce_fix (whd_construct_state env) sigma fix stack with + (match reduce_fix (whd_construct_stack env) sigma fix stack with | Reduced s' -> s' | NotReducible -> raise NotStepReducible) | _ when isEvalRef env x -> - let ref = destEvalRef x in + let ref,u = destEvalRefU x in (try - red_elim_const env sigma ref stack + fst (red_elim_const env sigma ref u stack) with Redelimination -> - match reference_opt_value sigma env ref with - | Some d -> d, stack + match reference_opt_value env sigma ref u with + | Some d -> (d, stack) | None -> raise NotStepReducible) | _ -> raise NotStepReducible in - app_stack (redrec (c, empty_stack)) + applist (redrec (c,[])) -let isIndRef = function IndRef _ -> true | _ -> false +let error_cannot_recognize ref = + errorlabstrm "" + (str "Cannot recognize a statement based on " ++ + Nametab.pr_global_env Id.Set.empty ref ++ str".") let reduce_to_ref_gen allow_product env sigma ref t = if isIndRef ref then - let (mind,t) = reduce_to_ind_gen allow_product env sigma t in - if IndRef mind <> ref then - errorlabstrm "" (str "Cannot recognize a statement based on " ++ - Nametab.pr_global_env Idset.empty ref ++ str".") - else - t + let ((mind,u),t) = reduce_to_ind_gen allow_product env sigma t in + begin match ref with + | IndRef mind' when eq_ind mind mind' -> t + | _ -> error_cannot_recognize ref + end else (* lazily reduces to match the head of [t] with the expected [ref] *) let rec elimrec env t l = - let c, _ = Reductionops.whd_stack sigma t in + let c, _ = decompose_appvect (Reductionops.whd_nored sigma t) in match kind_of_term c with | Prod (n,ty,t') -> - if allow_product then + if allow_product then elimrec (push_rel (n,None,t) env) t' ((n,None,ty)::l) - else - errorlabstrm "" - (str "Cannot recognize an atomic statement based on " ++ - Nametab.pr_global_env Idset.empty ref ++ str".") + else + error_cannot_recognize ref | _ -> try - if global_of_constr c = ref + if eq_gr (global_of_constr 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 elimrec env t' l - with NotStepReducible -> - errorlabstrm "" - (str "Cannot recognize a statement based on " ++ - Nametab.pr_global_env Idset.empty ref ++ str".") + with NotStepReducible -> error_cannot_recognize ref in elimrec env t [] |