diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 445 |
1 files changed, 245 insertions, 200 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 820974888..69d47e8e6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -156,6 +156,7 @@ end (** Machinery about stack of unfolded constants *) module Cst_stack = struct + open EConstr (** constant * params * args - constant applied to params = term in head applied to args @@ -191,8 +192,8 @@ module Cst_stack = struct | (cst,params,[])::_ -> Some(cst,params) | _ -> None - let reference t = match best_cst t with - | Some (c, _) when Term.isConst c -> Some (fst (Term.destConst c)) + let reference sigma t = match best_cst t with + | Some (c, _) when isConst sigma c -> Some (fst (destConst sigma c)) | _ -> None (** [best_replace d cst_l c] makes the best replacement for [d] @@ -201,14 +202,14 @@ module Cst_stack = struct let reconstruct_head = List.fold_left (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in List.fold_right - (fun (cst,params,args) t -> Termops.replace_term sigma - (EConstr.of_constr (reconstruct_head d args)) - (EConstr.of_constr (applist (cst, List.rev params))) - (EConstr.of_constr t)) cst_l c + (fun (cst,params,args) t -> EConstr.of_constr (Termops.replace_term sigma + (reconstruct_head d args) + (applist (cst, List.rev params)) + t)) cst_l c let pr l = let open Pp in - let p_c = Termops.print_constr in + let p_c c = Termops.print_constr (EConstr.Unsafe.to_constr c) in prlist_with_sep pr_semicolon (fun (c,params,args) -> hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++ @@ -220,6 +221,7 @@ end (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *) module Stack : sig + open EConstr type 'a app_node val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds @@ -231,7 +233,7 @@ sig | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection * Cst_stack.t - | Fix of fixpoint * 'a t * Cst_stack.t + | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t | Shift of int | Update of 'a @@ -242,10 +244,10 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) - val equal : ('a * int -> 'a * int -> bool) -> (fixpoint * int -> fixpoint * int -> bool) + val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool) -> 'a t -> 'a t -> (int * int) option val compare_shape : 'a t -> 'a t -> bool - val map : (constr -> constr) -> constr t -> constr t + val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> constr t -> constr t -> 'a * int * int val append_app_list : 'a list -> 'a t -> 'a t @@ -258,10 +260,11 @@ sig val args_size : 'a t -> int val tail : int -> 'a t -> 'a t val nth : 'a t -> int -> 'a - val best_state : constr * constr t -> Cst_stack.t -> constr * constr t - val zip : ?refold:bool -> constr * constr t -> constr + val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t + val zip : ?refold:bool -> evar_map -> constr * constr t -> constr end = struct + open EConstr type 'a app_node = int * 'a array * int (* first releavnt position, arguments, last relevant position *) @@ -286,7 +289,7 @@ struct | App of 'a app_node | Case of Term.case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection * Cst_stack.t - | Fix of fixpoint * 'a t * Cst_stack.t + | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t | Shift of int | Update of 'a @@ -305,7 +308,7 @@ struct str "ZProj(" ++ int n ++ pr_comma () ++ int m ++ pr_comma () ++ pr_con (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> - str "ZFix(" ++ Termops.pr_fix Termops.print_constr f + str "ZFix(" ++ Termops.pr_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" | Cst (mem,curr,remains,params,cst_l) -> str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr @@ -533,11 +536,11 @@ struct | None -> raise Not_found (** This function breaks the abstraction of Cst_stack ! *) - let best_state (_,sk as s) l = + let best_state sigma (_,sk as s) l = let rec aux sk def = function |(cst, params, []) -> (cst, append_app_list (List.rev params) sk) |(cst, params, (i,t)::q) -> match decomp sk with - | Some (el,sk') when Constr.equal el t.(i) -> + | Some (el,sk') when EConstr.eq_constr sigma el t.(i) -> if i = pred (Array.length t) then aux sk' def (cst, params, q) else aux sk' def (cst, params, (succ i,t)::q) @@ -552,53 +555,66 @@ struct | Some (hd, sk) -> mkProj (p, hd), sk | None -> assert false - let rec zip ?(refold=false) = function + let zip ?(refold=false) sigma s = + let rec zip = function | f, [] -> f | f, (App (i,a,j) :: s) -> let a' = if Int.equal i 0 && Int.equal j (Array.length a - 1) then a else Array.sub a i (j - i + 1) in - zip ~refold (mkApp (f, a'), s) + zip (mkApp (f, a'), s) | f, (Case (ci,rt,br,cst_l)::s) when refold -> - zip ~refold (best_state (mkCase (ci,rt,f,br), s) cst_l) - | f, (Case (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s) + zip (best_state sigma (mkCase (ci,rt,f,br), s) cst_l) + | f, (Case (ci,rt,br,_)::s) -> zip (mkCase (ci,rt,f,br), s) | f, (Fix (fix,st,cst_l)::s) when refold -> - zip ~refold (best_state (mkFix fix, st @ (append_app [|f|] s)) cst_l) - | f, (Fix (fix,st,_)::s) -> zip ~refold + zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l) + | f, (Fix (fix,st,_)::s) -> zip (mkFix fix, st @ (append_app [|f|] s)) | f, (Cst (cst,_,_,params,cst_l)::s) when refold -> - zip ~refold (best_state (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) + zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) | f, (Cst (cst,_,_,params,_)::s) -> - zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s))) - | f, (Shift n::s) -> zip ~refold (lift n f, s) + zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) + | f, (Shift n::s) -> zip (Vars.lift n f, s) | f, (Proj (n,m,p,cst_l)::s) when refold -> - zip ~refold (best_state (mkProj (p,f),s) cst_l) - | f, (Proj (n,m,p,_)::s) -> zip ~refold (mkProj (p,f),s) + zip (best_state sigma (mkProj (p,f),s) cst_l) + | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s) | _, (Update _::_) -> assert false + in + zip s + end (** The type of (machine) states (= lambda-bar-calculus' cuts) *) -type state = constr * constr Stack.t +type state = EConstr.t * EConstr.t Stack.t -type contextual_reduction_function = env -> evar_map -> constr -> constr -type reduction_function = contextual_reduction_function -type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } +type contextual_reduction_function = env -> evar_map -> EConstr.t -> constr +type reduction_function = contextual_reduction_function +type local_reduction_function = evar_map -> EConstr.t -> constr +type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> EConstr.t -> (constr, 'r) Sigma.sigma } -type contextual_stack_reduction_function = - env -> evar_map -> constr -> constr * constr list -type stack_reduction_function = contextual_stack_reduction_function +type contextual_stack_reduction_function = + env -> evar_map -> EConstr.t -> EConstr.t * EConstr.t list +type stack_reduction_function = contextual_stack_reduction_function type local_stack_reduction_function = - evar_map -> constr -> constr * constr list + evar_map -> EConstr.t -> EConstr.t * EConstr.t list -type contextual_state_reduction_function = - env -> evar_map -> state -> state -type state_reduction_function = contextual_state_reduction_function +type contextual_state_reduction_function = + env -> evar_map -> state -> state +type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state let pr_state (tm,sk) = let open Pp in - h 0 (Termops.print_constr tm ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr sk) + let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in + h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) + +let local_assum (na, t) = + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let local_def (na, b, t) = + let inj = EConstr.Unsafe.to_constr in + LocalDef (na, inj b, inj t) (*************************************) (*** Reduction Functions Operators ***) @@ -612,19 +628,19 @@ let safe_meta_value sigma ev = let strong whdfun env sigma t = let rec strongrec env t = - let t = EConstr.of_constr (whdfun env sigma (EConstr.Unsafe.to_constr t)) in + let t = EConstr.of_constr (whdfun env sigma t) in map_constr_with_full_binders sigma push_rel strongrec env t in - EConstr.Unsafe.to_constr (strongrec env (EConstr.of_constr t)) + EConstr.Unsafe.to_constr (strongrec env t) let local_strong whdfun sigma = - let rec strongrec t = Constr.map strongrec (whdfun sigma t) in - strongrec + let rec strongrec t = EConstr.map sigma strongrec (EConstr.of_constr (whdfun sigma t)) in + fun c -> EConstr.Unsafe.to_constr (strongrec c) let rec strong_prodspine redfun sigma c = - let x = redfun sigma c in - match kind_of_term x with - | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b) - | _ -> x + let x = EConstr.of_constr (redfun sigma c) in + match EConstr.kind sigma x with + | Prod (na,a,b) -> mkProd (na, EConstr.Unsafe.to_constr a,strong_prodspine redfun sigma b) + | _ -> EConstr.Unsafe.to_constr x (*************************************) (*** Reduction using bindingss ***) @@ -634,31 +650,36 @@ let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA] (* Beta Reduction tools *) -let apply_subst recfun env refold cst_l t stack = +let apply_subst recfun env sigma refold cst_l t stack = let rec aux env cst_l t stack = - match (Stack.decomp stack,kind_of_term t) with + match (Stack.decomp stack, EConstr.kind sigma t) with | Some (h,stacktl), Lambda (_,_,c) -> let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in aux (h::env) cst_l' c stacktl - | _ -> recfun cst_l (substl env t, stack) + | _ -> recfun sigma cst_l (EConstr.Vars.substl env t, stack) in aux env cst_l t stack -let stacklam recfun env t stack = - apply_subst (fun _ -> recfun) env false Cst_stack.empty t stack +let stacklam recfun env sigma t stack = + apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack + +let beta_app sigma (c,l) = + let zip s = Stack.zip sigma s in + stacklam zip [] sigma c (Stack.append_app l Stack.empty) -let beta_applist (c,l) = - stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty) +let beta_applist sigma (c,l) = + let zip s = Stack.zip sigma s in + EConstr.Unsafe.to_constr (stacklam zip [] sigma c (Stack.append_app_list l Stack.empty)) (* Iota reduction tools *) type 'a miota_args = { - mP : constr; (* the result type *) - mconstr : constr; (* the constructor *) + mP : EConstr.t; (* the result type *) + mconstr : EConstr.t; (* the constructor *) mci : case_info; (* special info to re-build pattern *) mcargs : 'a list; (* the constructor's arguments *) mlf : 'a array } (* the branch code vector *) -let reducible_mind_case c = match kind_of_term c with +let reducible_mind_case sigma c = match EConstr.kind sigma c with | Construct _ | CoFix _ -> true | _ -> false @@ -672,9 +693,10 @@ let reducible_mind_case c = match kind_of_term c with f x := t. End M. Definition f := u. and say goodbye to any hope of refolding M.f this way ... *) -let magicaly_constant_of_fixbody env reference bd = function +let magicaly_constant_of_fixbody env sigma reference bd = function | Name.Anonymous -> bd | Name.Name id -> + let open EConstr in try let (cst_mod,cst_sect,_) = Constant.repr3 reference in let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in @@ -682,7 +704,7 @@ let magicaly_constant_of_fixbody env reference bd = function match constant_opt_value_in env (cst,u) with | None -> bd | Some t -> - let csts = Universes.eq_constr_universes t bd in + let csts = EConstr.eq_constr_universes sigma (EConstr.of_constr t) bd in begin match csts with | Some csts -> let subst = Universes.Constraints.fold (fun (l,d,r) acc -> @@ -696,7 +718,8 @@ let magicaly_constant_of_fixbody env reference bd = function with | Not_found -> bd -let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) = +let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = + let open EConstr in let nbodies = Array.length bodies in let make_Fi j = let ind = nbodies-j-1 in @@ -708,37 +731,40 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) | Some e -> match reference with | None -> bd - | Some r -> magicaly_constant_of_fixbody e r bd names.(ind) in + | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in let closure = List.init nbodies make_Fi in - substl closure bodies.(bodynum) + Vars.substl closure bodies.(bodynum) (** Similar to the "fix" case below *) let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk = + let open EConstr in let raw_answer = let env = if refold then Some env else None in - contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in + contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in apply_subst - (fun x (t,sk') -> + (fun sigma x (t,sk') -> let t' = if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in recfun x (t',sk')) - [] refold Cst_stack.empty raw_answer sk + [] sigma refold Cst_stack.empty raw_answer sk -let reduce_mind_case mia = - match kind_of_term mia.mconstr with +let reduce_mind_case sigma mia = + let open EConstr in + match EConstr.kind sigma mia.mconstr with | Construct ((ind_sp,i),u) -> (* let ncargs = (fst mia.mci).(i-1) in*) let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1),real_cargs) | CoFix cofix -> - let cofix_def = contract_cofix cofix in + let cofix_def = contract_cofix sigma cofix in mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *) -let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = +let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = + let open EConstr in let nbodies = Array.length recindices in let make_Fi j = let ind = nbodies-j-1 in @@ -750,26 +776,27 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty | Some e -> match reference with | None -> bd - | Some r -> magicaly_constant_of_fixbody e r bd names.(ind) in + | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in let closure = List.init nbodies make_Fi in - substl closure bodies.(bodynum) + Vars.substl closure bodies.(bodynum) (** First we substitute the Rel bodynum by the fixpoint and then we try to replace the fixpoint by the best constant from [cst_l] Other rels are directly substituted by constants "magically found from the context" in contract_fix *) let reduce_and_refold_fix recfun env sigma refold cst_l fix sk = + let open EConstr in let raw_answer = let env = if refold then None else Some env in - contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in + contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in apply_subst - (fun x (t,sk') -> + (fun sigma x (t,sk') -> let t' = if refold then Cst_stack.best_replace sigma (mkFix fix) cst_l t else t in recfun x (t',sk')) - [] refold Cst_stack.empty raw_answer sk + [] sigma refold Cst_stack.empty raw_answer sk let fix_recarg ((recindices,bodynum),_) stack = assert (0 <= bodynum && bodynum < Array.length recindices); @@ -802,51 +829,53 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_RAKAM:=a); } -let equal_stacks (x, l) (y, l') = - let f_equal (x,lft1) (y,lft2) = Constr.equal (Vars.lift lft1 x) (Vars.lift lft2 y) in - let eq_fix (a,b) (c,d) = f_equal (Constr.mkFix a, b) (Constr.mkFix c, d) in +let equal_stacks sigma (x, l) (y, l') = + let open EConstr in + let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in + let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in match Stack.equal f_equal eq_fix l l' with | None -> false | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = + let open EConstr in let open Context.Named.Declaration in - let rec whrec cst_l (x, stack as s) = + let rec whrec cst_l (x, stack) = let () = if !debug_RAKAM then let open Pp in + let pr c = Termops.print_constr (EConstr.Unsafe.to_constr c) in Feedback.msg_notice - (h 0 (str "<<" ++ Termops.print_constr x ++ + (h 0 (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ - str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++ + str "|" ++ cut () ++ Stack.pr pr stack ++ str ">>")) in + let c0 = EConstr.kind sigma x in let fold () = let () = if !debug_RAKAM then let open Pp in Feedback.msg_notice (str "<><><><><>") in - (s,cst_l) + ((EConstr.of_kind c0, stack),cst_l) in - match kind_of_term x with + match c0 with | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA -> (match lookup_rel n env with - | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack) + | LocalDef (_,body,_) -> whrec Cst_stack.empty (EConstr.of_constr (lift n body), stack) | _ -> fold ()) | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) -> (match lookup_named id env with | LocalDef (_,body,_) -> - whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack) + whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (EConstr.of_constr body, stack) | _ -> fold ()) - | Evar ev -> - (match safe_evar_value sigma ev with - | Some body -> whrec cst_l (body, stack) - | None -> fold ()) + | Evar ev -> fold () | Meta ev -> (match safe_meta_value sigma ev with - | Some body -> whrec cst_l (body, stack) + | Some body -> whrec cst_l (EConstr.of_constr body, stack) | None -> fold ()) | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) -> (match constant_opt_value_in env const with | None -> fold () | Some body -> + let body = EConstr.of_constr body in if not tactic_mode then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) (body, stack) @@ -863,12 +892,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let (tm',sk'),cst_l' = whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) in - let rec is_case x = match kind_of_term x with + let rec is_case x = match EConstr.kind sigma x with | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x | App (hd, _) -> is_case hd | Case _ -> true | _ -> false in - if equal_stacks (x, app_sk) (tm', sk') + if equal_stacks sigma (x, app_sk) (tm', sk') || Stack.will_expose_iota sk' || is_case tm' then fold () @@ -896,7 +925,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | None -> let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in let stack'', csts = whrec Cst_stack.empty stack' in - if equal_stacks stack' stack'' then fold () + if equal_stacks sigma stack' stack'' then fold () else stack'', csts | Some (recargs, nargs, flags) -> if (List.mem `ReductionNeverUnfold flags @@ -926,7 +955,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = Stack.append_app [|c|] bef,cst_l)::s')) | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> - apply_subst whrec [b] refold cst_l c stack + apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack | Cast (c,_,_) -> whrec cst_l (c, stack) | App (f,cl) -> whrec @@ -935,20 +964,20 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Lambda (na,t,c) -> (match Stack.decomp stack with | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> - apply_subst whrec [] refold cst_l x stack + apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> - let env' = push_rel (LocalAssum (na,t)) env in + let env' = push_rel (local_assum (na, t)) env in let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in - (match kind_of_term (Stack.zip ~refold (fst (whrec' (c, Stack.empty)))) with + (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with | App (f,cl) -> let napp = Array.length cl in if napp > 0 then let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in - match kind_of_term x', l' with + match EConstr.kind sigma x', l' with | Rel 1, [] -> let lc = Array.sub cl 0 (napp-1) in - let u = if Int.equal napp 1 then f else appvect (f,lc) in - if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty),Cst_stack.empty else fold () + let u = if Int.equal napp 1 then f else mkApp (f,lc) in + if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty),Cst_stack.empty else fold () | _ -> fold () else fold () | _ -> fold ()) @@ -973,11 +1002,11 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |args, (Stack.Proj (n,m,p,_)::s') when use_match -> whrec Cst_stack.empty (Stack.nth args (n+m), s') |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> - let x' = Stack.zip(x,args) in + let x' = Stack.zip sigma (x, args) in let out_sk = s' @ (Stack.append_app [|x'|] s'') in reduce_and_refold_fix whrec env sigma refold cst_l f out_sk |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') -> - let x' = Stack.zip(x,args) in + let x' = Stack.zip sigma (x, args) in begin match remains with | [] -> (match const with @@ -985,6 +1014,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (match constant_opt_value_in env const with | None -> fold () | Some body -> + let body = EConstr.of_constr body in whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) (body, s' @ (Stack.append_app [|x'|] s''))) | Stack.Cst_proj p -> @@ -1020,31 +1050,34 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = in fun xs -> let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in - if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res + if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res (** reduction machine without global env and refold machinery *) let local_whd_state_gen flags sigma = - let rec whrec (x, stack as s) = - match kind_of_term x with + let open EConstr in + let rec whrec (x, stack) = + let c0 = EConstr.kind sigma x in + let s = (EConstr.of_kind c0, stack) in + match c0 with | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> - stacklam whrec [b] c stack + stacklam whrec [b] sigma c stack | Cast (c,_,_) -> whrec (c, stack) | App (f,cl) -> whrec (f, Stack.append_app cl stack) | Lambda (_,_,c) -> (match Stack.decomp stack with | Some (a,m) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> - stacklam whrec [a] c m + stacklam whrec [a] sigma c m | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> - (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with + (match EConstr.kind sigma (Stack.zip sigma (whrec (c, Stack.empty))) with | App (f,cl) -> let napp = Array.length cl in if napp > 0 then let x', l' = whrec (Array.last cl, Stack.empty) in - match kind_of_term x', l' with + match EConstr.kind sigma x', l' with | Rel 1, [] -> let lc = Array.sub cl 0 (napp-1) in - let u = if Int.equal napp 1 then f else appvect (f,lc) in - if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty) else s + let u = if Int.equal napp 1 then f else mkApp (f,lc) in + if Vars.noccurn sigma 1 u then (EConstr.of_constr (pop u),Stack.empty) else s | _ -> s else s | _ -> s) @@ -1064,14 +1097,10 @@ let local_whd_state_gen flags sigma = |None -> s |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef,Cst_stack.empty)::s')) - | Evar ev -> - (match safe_evar_value sigma ev with - Some c -> whrec (c,stack) - | None -> s) - + | Evar ev -> s | Meta ev -> (match safe_meta_value sigma ev with - Some c -> whrec (c,stack) + Some c -> whrec (EConstr.of_constr c,stack) | None -> s) | Construct ((ind,c),u) -> @@ -1084,8 +1113,8 @@ let local_whd_state_gen flags sigma = |args, (Stack.Proj (n,m,p,_) :: s') when use_match -> whrec (Stack.nth args (n+m), s') |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> - let x' = Stack.zip(x,args) in - whrec (contract_fix f, s' @ (Stack.append_app [|x'|] s'')) + let x' = Stack.zip sigma (x,args) in + whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s'')) |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false |_, _ -> s else s @@ -1094,7 +1123,7 @@ let local_whd_state_gen flags sigma = if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ | Stack.Proj _)::s') -> - whrec (contract_cofix cofix, stack) + whrec (contract_cofix sigma cofix, stack) |_ -> s else s @@ -1107,7 +1136,7 @@ let raw_whd_state_gen flags env = f let stack_red_of_state_red f = - let f sigma x = decompose_app (Stack.zip (f sigma (x, Stack.empty))) in + let f sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f sigma (x, Stack.empty))) in f (* Drops the Cst_stack *) @@ -1115,11 +1144,11 @@ let iterate_whd_gen refold flags env sigma s = let rec aux t = let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in let whd_sk = Stack.map aux sk in - Stack.zip ~refold (hd,whd_sk) + Stack.zip sigma ~refold (hd,whd_sk) in aux s let red_of_state_red f sigma x = - Stack.zip (f sigma (x,Stack.empty)) + EConstr.Unsafe.to_constr (Stack.zip sigma (f sigma (x,Stack.empty))) (* 0. No Reduction Functions *) @@ -1174,7 +1203,7 @@ let whd_allnolet env = (* 4. Ad-hoc eta reduction, does not subsitute evars *) -let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty)) +let shrink_eta c = EConstr.Unsafe.to_constr (Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty))) (* 5. Zeta Reduction Functions *) @@ -1198,7 +1227,7 @@ let clos_norm_flags flgs env sigma t = let evars ev = safe_evar_value sigma ev in CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) - (CClosure.inject t) + (CClosure.inject (EConstr.Unsafe.to_constr t)) with e when is_anomaly e -> error "Tried to normalize ill-typed term" let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) @@ -1239,7 +1268,15 @@ let report_anomaly _ = let e = CErrors.push e in iraise e -let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y = +let f_conv ?l2r ?reds env ?evars x y = + let inj = EConstr.Unsafe.to_constr in + Reduction.conv ?l2r ?reds env ?evars (inj x) (inj y) + +let f_conv_leq ?l2r ?reds env ?evars x y = + let inj = EConstr.Unsafe.to_constr in + Reduction.conv_leq ?l2r ?reds env ?evars (inj x) (inj y) + +let test_trans_conversion (f: EConstr.t Reduction.extended_conversion_function) reds env sigma x y = try let evars ev = safe_evar_value sigma ev in let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in @@ -1247,16 +1284,16 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv reds env sigma -let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_leq reds env sigma +let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv reds env sigma +let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv_leq reds env sigma let is_fconv ?(reds=full_transparent_state) = function | Reduction.CONV -> is_conv ~reds | Reduction.CUMUL -> is_conv_leq ~reds let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = let f = match pb with - | Reduction.CONV -> Reduction.conv - | Reduction.CUMUL -> Reduction.conv_leq + | Reduction.CONV -> f_conv + | Reduction.CUMUL -> f_conv_leq in try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true with Reduction.NotConvertible -> false @@ -1320,37 +1357,38 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = (* Special-Purpose Reduction *) (********************************************************************) -let whd_meta sigma c = match kind_of_term c with - | Meta p -> (try meta_value sigma p with Not_found -> c) - | _ -> c +let whd_meta sigma c = match EConstr.kind sigma c with + | Meta p -> (try meta_value sigma p with Not_found -> EConstr.Unsafe.to_constr c) + | _ -> EConstr.Unsafe.to_constr c let default_plain_instance_ident = Id.of_string "H" (* Try to replace all metas. Does not replace metas in the metas' values * Differs from (strong whd_meta). *) -let plain_instance s c = - let rec irec n u = match kind_of_term u with - | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) - | App (f,l) when isCast f -> - let (f,_,t) = destCast f in +let plain_instance sigma s c = + let open EConstr in + let rec irec n u = match EConstr.kind sigma u with + | Meta p -> (try Vars.lift n (Metamap.find p s) with Not_found -> u) + | App (f,l) when isCast sigma f -> + let (f,_,t) = destCast sigma f in let l' = CArray.Fun1.smartmap irec n l in - (match kind_of_term f with + (match EConstr.kind sigma f with | Meta p -> (* Don't flatten application nodes: this is used to extract a proof-term from a proof-tree and we want to keep the structure of the proof-tree *) (try let g = Metamap.find p s in - match kind_of_term g with + match EConstr.kind sigma g with | App _ -> - let l' = CArray.Fun1.smartmap lift 1 l' in + let l' = CArray.Fun1.smartmap Vars.lift 1 l' in mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) | _ -> mkApp (irec n f,l')) - | Cast (m,_,_) when isMeta m -> - (try lift n (Metamap.find (destMeta m) s) with Not_found -> u) + | Cast (m,_,_) when isMeta sigma m -> + (try Vars.lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u) | _ -> - map_constr_with_binders succ irec n u + map_with_binders sigma succ irec n u in if Metamap.is_empty s then c else irec 0 c @@ -1391,7 +1429,7 @@ let plain_instance s c = let instance sigma s c = (* if s = [] then c else *) - local_strong whd_betaiota sigma (plain_instance s c) + local_strong whd_betaiota sigma (plain_instance sigma s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -1400,34 +1438,40 @@ let instance sigma s c = * error message. *) let hnf_prod_app env sigma t n = - match kind_of_term (whd_all env sigma t) with - | Prod (_,_,b) -> subst1 n b + let open EConstr in + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with + | Prod (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b) | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") let hnf_prod_appvect env sigma t nl = - Array.fold_left (hnf_prod_app env sigma) t nl + Array.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl let hnf_prod_applist env sigma t nl = - List.fold_left (hnf_prod_app env sigma) t nl + List.fold_left (fun acc t -> hnf_prod_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl let hnf_lam_app env sigma t n = - match kind_of_term (whd_all env sigma t) with - | Lambda (_,_,b) -> subst1 n b + let open EConstr in + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with + | Lambda (_,_,b) -> EConstr.Unsafe.to_constr (Vars.subst1 n b) | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") let hnf_lam_appvect env sigma t nl = - Array.fold_left (hnf_lam_app env sigma) t nl + Array.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl let hnf_lam_applist env sigma t nl = - List.fold_left (hnf_lam_app env sigma) t nl + List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl + +let bind_assum (na, t) = + let inj = EConstr.Unsafe.to_constr in + (na, inj t) let splay_prod env sigma = let rec decrec env m c = let t = whd_all env sigma c in - match kind_of_term t with + match EConstr.kind sigma (EConstr.of_constr t) with | Prod (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - ((n,a)::m) c0 + decrec (push_rel (local_assum (n,a)) env) + (bind_assum (n,a)::m) c0 | _ -> m,t in decrec env [] @@ -1435,10 +1479,10 @@ let splay_prod env sigma = let splay_lam env sigma = let rec decrec env m c = let t = whd_all env sigma c in - match kind_of_term t with + match EConstr.kind sigma (EConstr.of_constr t) with | Lambda (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - ((n,a)::m) c0 + decrec (push_rel (local_assum (n,a)) env) + (bind_assum (n,a)::m) c0 | _ -> m,t in decrec env [] @@ -1446,51 +1490,51 @@ let splay_lam env sigma = let splay_prod_assum env sigma = let rec prodec_rec env l c = let t = whd_allnolet env sigma c in - match kind_of_term t with + match EConstr.kind sigma (EConstr.of_constr t) with | Prod (x,t,c) -> - prodec_rec (push_rel (LocalAssum (x,t)) env) - (Context.Rel.add (LocalAssum (x,t)) l) c + prodec_rec (push_rel (local_assum (x,t)) env) + (Context.Rel.add (local_assum (x,t)) l) c | LetIn (x,b,t,c) -> - prodec_rec (push_rel (LocalDef (x,b,t)) env) - (Context.Rel.add (LocalDef (x,b,t)) l) c + prodec_rec (push_rel (local_def (x,b,t)) env) + (Context.Rel.add (local_def (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> - let t' = whd_all env sigma t in + let t' = whd_all env sigma (EConstr.of_constr t) in if Term.eq_constr t t' then l,t - else prodec_rec env l t' + else prodec_rec env l (EConstr.of_constr t') in prodec_rec env Context.Rel.empty let splay_arity env sigma c = let l, c = splay_prod env sigma c in - match kind_of_term c with + match EConstr.kind sigma (EConstr.of_constr c) with | Sort s -> l,s | _ -> invalid_arg "splay_arity" let sort_of_arity env sigma c = snd (splay_arity env sigma c) let splay_prod_n env sigma n = - let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else - match kind_of_term (whd_all env sigma c) with + let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with | Prod (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 + decrec (push_rel (local_assum (n,a)) env) + (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0 | _ -> invalid_arg "splay_prod_n" in decrec env n Context.Rel.empty let splay_lam_n env sigma n = - let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else - match kind_of_term (whd_all env sigma c) with + let rec decrec env m ln c = if Int.equal m 0 then (ln, EConstr.Unsafe.to_constr c) else + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma c)) with | Lambda (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 + decrec (push_rel (local_assum (n,a)) env) + (m-1) (Context.Rel.add (local_assum (n,a)) ln) c0 | _ -> invalid_arg "splay_lam_n" in decrec env n Context.Rel.empty let is_sort env sigma t = - match kind_of_term (whd_all env sigma t) with + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with | Sort s -> true | _ -> false @@ -1498,6 +1542,7 @@ let is_sort env sigma t = of case/fix (heuristic used by evar_conv) *) let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = + let open EConstr in let refold = get_refolding_in_reduction () in let tactic_mode = false in let rec whrec csts s = @@ -1506,15 +1551,15 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = |args, (Stack.Case _ :: _ as stack') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in - if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' + if reducible_mind_case sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' |args, (Stack.Fix _ :: _ as stack') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in - if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' + if isConstruct sigma t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' |args, (Stack.Proj (n,m,p,_) :: stack'') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in - if isConstruct t_o then + if isConstruct sigma t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' @@ -1523,9 +1568,9 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = let find_conclusion env sigma = let rec decrec env c = let t = whd_all env sigma c in - match kind_of_term t with - | Prod (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 - | Lambda (x,t,c0) -> decrec (push_rel (LocalAssum (x,t)) env) c0 + match EConstr.kind sigma (EConstr.of_constr t) with + | Prod (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0 + | Lambda (x,t,c0) -> decrec (push_rel (local_assum (x,t)) env) c0 | t -> t in decrec env @@ -1539,11 +1584,12 @@ let is_arity env sigma c = (* Metas *) let meta_value evd mv = + let open EConstr in let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> let metas = Metamap.bind valrec b.freemetas in - instance evd metas b.rebus + EConstr.of_constr (instance evd metas (EConstr.of_constr b.rebus)) | None -> mkMeta mv in valrec mv @@ -1553,7 +1599,7 @@ let meta_instance sigma b = if Metaset.is_empty fm then b.rebus else let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in - instance sigma c_sigma b.rebus + instance sigma c_sigma (EConstr.of_constr b.rebus) let nf_meta sigma c = meta_instance sigma (mk_freelisted c) @@ -1569,7 +1615,7 @@ let meta_reducible_instance evd b = in let metas = Metaset.fold fold fm Metamap.empty in let rec irec u = - let u = whd_betaiota Evd.empty u (** FIXME *) in + let u = whd_betaiota Evd.empty (EConstr.of_constr u) (** FIXME *) in match kind_of_term u with | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr c))) -> let m = destMeta (strip_outer_cast evd (EConstr.of_constr c)) in @@ -1615,32 +1661,31 @@ let meta_reducible_instance evd b = else irec b.rebus -let head_unfold_under_prod ts env _ c = +let head_unfold_under_prod ts env sigma c = + let open EConstr in let unfold (cst,u as cstu) = if Cpred.mem cst (snd ts) then match constant_opt_value_in env cstu with - | Some c -> c + | Some c -> EConstr.of_constr c | None -> mkConstU cstu else mkConstU cstu in let rec aux c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (n,t,c) -> mkProd (n,aux t, aux c) | _ -> - let (h,l) = decompose_app c in - match kind_of_term h with - | Const cst -> beta_applist (unfold cst,l) + let (h,l) = decompose_app_vect sigma c in + match EConstr.kind sigma (EConstr.of_constr h) with + | Const cst -> beta_app sigma (unfold cst, Array.map EConstr.of_constr l) | _ -> c in - aux c + EConstr.Unsafe.to_constr (aux c) let betazetaevar_applist sigma n c l = + let open EConstr in let rec stacklam n env t stack = - if Int.equal n 0 then applist (substl env t, stack) else - match kind_of_term t, stack with + if Int.equal n 0 then applist (Vars.substl env t, stack) else + match EConstr.kind sigma t, stack with | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack - | Evar ev, _ -> - (match safe_evar_value sigma ev with - | Some body -> stacklam n env body stack - | None -> applist (substl env t, stack)) + | LetIn(_,b,_,c), _ -> stacklam (n-1) (Vars.substl env b::env) c stack + | Evar _, _ -> applist (Vars.substl env t, stack) | _ -> anomaly (Pp.str "Not enough lambda/let's") in - stacklam n [] c l + EConstr.Unsafe.to_constr (stacklam n [] c l) |