From 787e409e773d45da6d149fbcdf9657b0be4a5529 Mon Sep 17 00:00:00 2001 From: pboutill Date: Wed, 19 Dec 2012 22:34:35 +0000 Subject: Reductionops reduction machine can refold constant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16107 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarconv.ml | 4 +- pretyping/reductionops.ml | 200 +++++++++++++++++++++++++++------------------ pretyping/reductionops.mli | 15 +++- pretyping/tacred.ml | 2 +- 4 files changed, 136 insertions(+), 85 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8238a3c94..614f99ee8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -184,13 +184,13 @@ let ise_stack2 no_app env evd f sk1 sk2 = else None, (evd, false) in match sk1, sk2 with | [], [] -> None, (i,true) - | Zcase (_,t1,c1)::q1, Zcase (_,t2,c2)::q2 -> + | Zcase (_,t1,c1,_)::q1, Zcase (_,t2,c2,_)::q2 -> let (i',b') = f env i CONV t1 t2 in if b' then let (i'',b'') = ise_array2 i' (fun ii -> f env ii CONV) c1 c2 in if b'' then ise_stack2 true i'' q1 q2 else fal () else fal () - | Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> + | Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 -> if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then let (i',b') = ise_and i [ (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f2366ea02..0b89830ef 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -25,8 +25,8 @@ exception Elimconst type 'a stack_member = | Zapp of 'a list - | Zcase of case_info * 'a * 'a array - | Zfix of fixpoint * 'a list + | Zcase of case_info * 'a * 'a array * ('a * 'a list) option + | Zfix of fixpoint * 'a list * ('a * 'a list) option | Zshift of int | Zupdate of 'a @@ -73,15 +73,20 @@ let list_of_app_stack s = Option.init init out let array_of_app_stack s = Option.map Array.of_list (list_of_app_stack s) -let rec zip = function +let rec zip ?(refold=false) = function | f, [] -> f - | f, (Zapp [] :: s) -> zip (f, s) + | f, (Zapp [] :: s) -> zip ~refold (f, s) | f, (Zapp args :: s) -> - zip (applist (f, args), s) - | f, (Zcase (ci,rt,br)::s) -> zip (mkCase (ci,rt,f,br), s) - | f, (Zfix (fix,st)::s) -> zip + zip ~refold (applist (f, args), s) + | f, (Zcase (ci,rt,br,Some(cst, params))::s) when refold -> + zip ~refold (cst, append_stack_app_list (List.rev params) s) + | f, (Zcase (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s) + | f, (Zfix (fix,st,Some(cst, params))::s) when refold -> zip ~refold + (cst, append_stack_app_list (List.rev params) + (append_stack_app_list st (append_stack_app_list [f] s))) + | f, (Zfix (fix,st,_)::s) -> zip ~refold (mkFix fix, append_stack_app_list st (append_stack_app_list [f] s)) - | f, (Zshift n::s) -> zip (lift n f, s) + | f, (Zshift n::s) -> zip ~refold (lift n f, s) | _ -> assert false let rec stack_assign s p c = match s with | Zapp args :: s -> @@ -180,10 +185,18 @@ let betadeltaiotaeta = Closure.RedFlags.red_add betadeltaiota Closure.RedFlags.f (* Beta Reduction tools *) +let apply_subst recfun env cst_l t stack = + let rec aux env cst_l t stack = + match (decomp_stack stack,kind_of_term t) with + | Some (h,stacktl), Lambda (_,_,c) -> + let append2cst (c,params,nb_skip) = + if nb_skip <= 0 then (c, h::params, nb_skip) else (c, params, pred nb_skip) in + aux (h::env) (List.map append2cst cst_l) c stacktl + | _ -> recfun cst_l (substl env t, stack) + in aux env cst_l t stack + let rec stacklam recfun env t stack = - match (decomp_stack stack,kind_of_term t) with - | Some (h,stacktl), Lambda (_,_,c) -> stacklam recfun (h::env) c stacktl - | _ -> recfun (substl env t, stack) +apply_subst (fun _ -> recfun) env [] t stack let beta_applist (c,l) = stacklam zip [] c (append_stack_app_list l empty_stack) @@ -201,10 +214,17 @@ let reducible_mind_case c = match kind_of_term c with | Construct _ | CoFix _ -> true | _ -> false -let contract_cofix (bodynum,(types,names,bodies as typedbodies)) = +let contract_cofix (bodynum,(types,names,bodies as typedbodies)) cst = let nbodies = Array.length bodies in - let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in - substl (List.tabulate make_Fi nbodies) bodies.(bodynum) + let make_Fi j = + let ind = nbodies-j-1 in + if bodynum = ind && not (Option.is_empty cst) then + let (c,params) = Option.get cst in + applist(c, List.rev params) + else + mkCoFix (ind,typedbodies) in + let closure = List.tabulate make_Fi nbodies in + substl closure bodies.(bodynum) let reduce_mind_case mia = match kind_of_term mia.mconstr with @@ -213,17 +233,24 @@ let reduce_mind_case mia = 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 cofix None 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 ((recindices,bodynum),(types,names,bodies as typedbodies)) = - let nbodies = Array.length recindices in - let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in - substl (List.tabulate make_Fi nbodies) bodies.(bodynum) +let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) cst = + let nbodies = Array.length recindices in + let make_Fi j = + let ind = nbodies-j-1 in + if bodynum = ind && not (Option.is_empty cst) then + let (c,params) = Option.get cst in + applist(c, List.rev params) + else + mkFix ((recindices,ind),typedbodies) in + let closure = List.tabulate make_Fi nbodies in + substl closure bodies.(bodynum) let fix_recarg ((recindices,bodynum),_) stack = assert (0 <= bodynum & bodynum < Array.length recindices); @@ -242,41 +269,57 @@ let fix_recarg ((recindices,bodynum),_) stack = ------------------- qui coute cher *) -let rec whd_state_gen flags env sigma = - let rec whrec (x, stack as s) = +let rec whd_state_gen ?(refold=false) flags env sigma = + let noth = [] in + let rec whrec cst_l (x, stack as s) = + let best_cst () = List.fold_left + (fun def (c,params,nb_skip) -> if nb_skip = 0 then Some(c,params) else def) + None cst_l in + let best_state def (cst,params,nb_skip) = + let apps,s' = strip_app stack in + try + let _,aft = List.chop nb_skip apps in + (cst, append_stack_app_list (List.rev params) (append_stack_app_list aft s')) + with Failure _ -> def in + let fold () = + if refold then List.fold_left best_state s cst_l else s + in match kind_of_term x with | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA -> (match lookup_rel n env with - | (_,Some body,_) -> whrec (lift n body, stack) - | _ -> s) + | (_,Some body,_) -> whrec noth (lift n body, stack) + | _ -> fold ()) | Var id when Closure.RedFlags.red_set flags (Closure.RedFlags.fVAR id) -> (match lookup_named id env with - | (_,Some body,_) -> whrec (body, stack) - | _ -> s) + | (_,Some body,_) -> whrec ((mkVar id,[],0)::cst_l) (body, stack) + | _ -> fold ()) | Evar ev -> (match safe_evar_value sigma ev with - | Some body -> whrec (body, stack) - | None -> s) + | Some body -> whrec noth (body, stack) + | None -> fold ()) | Meta ev -> (match safe_meta_value sigma ev with - | Some body -> whrec (body, stack) - | None -> s) + | Some body -> whrec noth (body, stack) + | None -> fold ()) | Const const when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST const) -> (match constant_opt_value env const with - | Some body -> whrec (body, stack) - | None -> s) + | Some body -> whrec ((mkConst const,[],0)::cst_l) (body, stack) + | None -> fold ()) | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> - stacklam whrec [b] c stack - | Cast (c,_,_) -> whrec (c, stack) - | App (f,cl) -> whrec (f, append_stack_app cl stack) + apply_subst whrec [b] cst_l c stack + | Cast (c,_,_) -> whrec cst_l (c, stack) + | App (f,cl) -> + whrec + (List.map (fun (a,b,nb_skip) -> (a,b,nb_skip+Array.length cl)) cst_l) + (f, append_stack_app cl stack) | Lambda (na,t,c) -> (match decomp_stack stack with - | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> - stacklam whrec [a] c m + | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> + apply_subst whrec [] cst_l x stack | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> let env' = push_rel (na,None,t) env in - let whrec' = whd_state_gen flags env' sigma in - (match kind_of_term (zip (whrec' (c, empty_stack))) with + let whrec' = whd_state_gen ~refold flags env' sigma in + (match kind_of_term (zip ~refold (whrec' (c, empty_stack))) with | App (f,cl) -> let napp = Array.length cl in if napp > 0 then @@ -285,42 +328,43 @@ let rec whd_state_gen flags env sigma = | 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 u,empty_stack) else s - | _ -> s - else s - | _ -> s) - | _ -> s) + if noccurn 1 u then (pop u,empty_stack) else fold () + | _ -> fold () + else fold () + | _ -> fold ()) + | _ -> fold ()) | Case (ci,p,d,lf) -> - whrec (d, Zcase (ci,p,lf) :: stack) + whrec noth (d, Zcase (ci,p,lf,best_cst ()) :: stack) | Fix ((ri,n),_ as f) -> (match strip_n_app ri.(n) stack with - |None -> s - |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef)::s')) + |None -> fold () + |Some (bef,arg,s') -> whrec noth (arg, Zfix(f,bef,best_cst ())::s')) | Construct (ind,c) -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match strip_app stack with - |args, (Zcase(ci, _, lf)::s') -> - whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s') - |args, (Zfix (f,s')::s'') -> + |args, (Zcase(ci, _, lf,_)::s') -> + whrec noth (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s') + |args, (Zfix (f,s',cst)::s'') -> let x' = applist(x,args) in - whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s'')) - |_ -> s - else s + whrec noth (contract_fix f cst, append_stack_app_list s' (append_stack_app_list [x'] s'')) + |_ -> fold () + else fold () | CoFix cofix -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match strip_app stack with - |args, (Zcase(ci, _, lf)::s') -> - whrec (contract_cofix cofix, stack) - |_ -> s - else s + |args, (Zcase(ci, _, lf,_)::s') -> + whrec noth (contract_cofix cofix (best_cst ()), stack) + |_ -> fold () + else fold () - | x -> s + | Rel _ | Var _ | Const _ | LetIn _ -> fold () + | Sort _ | Ind _ | Prod _ -> fold () in - whrec + whrec noth let local_whd_state_gen flags sigma = let rec whrec (x, stack as s) = @@ -350,12 +394,12 @@ let local_whd_state_gen flags sigma = | _ -> s) | Case (ci,p,d,lf) -> - whrec (d, Zcase (ci,p,lf) :: stack) + whrec (d, Zcase (ci,p,lf,None) :: stack) | Fix ((ri,n),_ as f) -> (match strip_n_app ri.(n) stack with |None -> s - |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef)::s')) + |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef,None)::s')) | Evar ev -> (match safe_evar_value sigma ev with @@ -370,19 +414,19 @@ let local_whd_state_gen flags sigma = | Construct (ind,c) -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match strip_app stack with - |args, (Zcase(ci, _, lf)::s') -> + |args, (Zcase(ci, _, lf,_)::s') -> whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s') - |args, (Zfix (f,s')::s'') -> + |args, (Zfix (f,s',cst)::s'') -> let x' = applist(x,args) in - whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s'')) + whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s'')) |_ -> s else s | CoFix cofix -> if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then match strip_app stack with - |args, (Zcase(ci, _, lf)::s') -> - whrec (contract_cofix cofix, stack) + |args, (Zcase(ci, _, lf,_)::s') -> + whrec (contract_cofix cofix None, stack) |_ -> s else s @@ -548,22 +592,22 @@ let whd_betaiota_preserving_vm_cast env sigma t = | Some (a,m) -> stacklam_var [a] c m | _ -> s) | Case (ci,p,d,lf) -> - whrec (d, Zcase (ci,p,lf) :: stack) + whrec (d, Zcase (ci,p,lf,None) :: stack) | Construct (ind,c) -> begin match strip_app stack with - |args, (Zcase(ci, _, lf)::s') -> + |args, (Zcase(ci, _, lf,_)::s') -> whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s') - |args, (Zfix (f,s')::s'') -> + |args, (Zfix (f,s',cst)::s'') -> let x' = applist(x,args) in - whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s'')) + whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s'')) |_ -> s end | CoFix cofix -> begin match strip_app stack with - |args, (Zcase(ci, _, lf)::s') -> - whrec (contract_cofix cofix, stack) + |args, (Zcase(ci, _, lf,_)::s') -> + whrec (contract_cofix cofix None, stack) |_ -> s end @@ -846,24 +890,24 @@ let whd_programs_stack env sigma = if occur_existential d then s else - whrec (d, Zcase (ci,p,lf) :: stack) + whrec (d, Zcase (ci,p,lf,None) :: stack) | Fix ((ri,n),_ as f) -> (match strip_n_app ri.(n) stack with |None -> s - |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef)::s')) + |Some (bef,arg,s') -> whrec (arg, Zfix(f,bef,None)::s')) | Construct (ind,c) -> begin match strip_app stack with - |args, (Zcase(ci, _, lf)::s') -> + |args, (Zcase(ci, _, lf,_)::s') -> whrec (lf.(c-1), append_stack_app_list (List.skipn ci.ci_npar args) s') - |args, (Zfix (f,s')::s'') -> + |args, (Zfix (f,s',cst)::s'') -> let x' = applist(x,args) in - whrec (contract_fix f,append_stack_app_list s' (append_stack_app_list [x'] s'')) + whrec (contract_fix f cst,append_stack_app_list s' (append_stack_app_list [x'] s'')) |_ -> s end | CoFix cofix -> begin match strip_app stack with - |args, (Zcase(ci, _, lf)::s') -> - whrec (contract_cofix cofix, stack) + |args, (Zcase(ci, _, lf,_)::s') -> + whrec (contract_cofix cofix None, stack) |_ -> s end | _ -> s diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 60c111370..7a80f9121 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -24,8 +24,8 @@ exception Elimconst type 'a stack_member = | Zapp of 'a list - | Zcase of case_info * 'a * 'a array - | Zfix of fixpoint * 'a list + | Zcase of case_info * 'a * 'a array * ('a * 'a list) option + | Zfix of fixpoint * 'a list * ('a * 'a list) option | Zshift of int | Zupdate of 'a @@ -46,7 +46,7 @@ val list_of_app_stack : 'a stack -> 'a list option val array_of_app_stack : 'a stack -> 'a array option val stack_assign : 'a stack -> int -> 'a -> 'a stack val stack_args_size : 'a stack -> int -val zip : constr * constr stack -> constr +val zip : ?refold:bool -> constr * constr stack -> constr val stack_tail : int -> 'a stack -> 'a stack val stack_nth : 'a stack -> int -> 'a @@ -80,6 +80,13 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a +val whd_state_gen : ?refold:bool -> + Closure.RedFlags.reds -> + Environ.env -> + Evd.evar_map -> + Term.constr * Term.constr stack_member list -> + Term.constr * Term.constr stack_member list + (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : Closure.RedFlags.reds -> reduction_function @@ -180,7 +187,7 @@ val is_arity : env -> evar_map -> constr -> bool val whd_programs : reduction_function -val contract_fix : fixpoint -> Term.constr +val contract_fix : fixpoint -> (constr * constr list) option -> constr val fix_recarg : fixpoint -> constr stack -> (int * constr) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 78b01a42a..b265d636e 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -450,7 +450,7 @@ let reduce_fix whdfun sigma fix stack = 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') + | Construct _ -> Reduced (contract_fix fix None, stack') | _ -> NotReducible) let contract_fix_use_function env sigma f -- cgit v1.2.3