diff options
| -rw-r--r-- | dev/include_printers | 1 | ||||
| -rw-r--r-- | dev/top_printers.dbg | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | dev/top_printers.mli | 1 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 21 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 552 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 48 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | tactics/cbn.ml | 797 | ||||
| -rw-r--r-- | tactics/cbn.mli | 13 | ||||
| -rw-r--r-- | tactics/redexpr.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 1 |
12 files changed, 939 insertions, 505 deletions
diff --git a/dev/include_printers b/dev/include_printers index d077075eeb..30529b5fd6 100644 --- a/dev/include_printers +++ b/dev/include_printers @@ -27,7 +27,6 @@ #install_printer (* id set *) ppidset;; #install_printer (* int set *) ppintset;; -#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;; #install_printer (* Reductionops machine stack *) pp_stack_t;; (*#install_printer (* hint_db *) print_hint_db;;*) diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index 06db787488..63071bba72 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -46,7 +46,6 @@ install_printer Top_printers.pp_idpred install_printer Top_printers.pp_cpred install_printer Top_printers.pp_transparent_state install_printer Top_printers.pp_stack_t -install_printer Top_printers.pp_cst_stack_t install_printer Top_printers.pp_state_t install_printer Top_printers.ppmetas install_printer Top_printers.ppevm diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 00050a89e1..bca1eb5754 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -169,7 +169,6 @@ let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n) -let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n) let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n) (* proof printers *) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index c826391cac..65eab8daa3 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -106,7 +106,6 @@ val pp_cpred : Names.Cpred.t -> unit val pp_transparent_state : TransparentState.t -> unit val pp_stack_t : Constr.t Reductionops.Stack.t -> unit -val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit val pp_state_t : Reductionops.state -> unit val ppmetas : Evd.Metaset.t -> unit diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 36dc01e272..366203faeb 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -382,19 +382,19 @@ let ise_stack2 no_app env evd f sk1 sk2 = else None, x in match sk1, sk2 with | [], [] -> None, Success i - | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 -> + | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 -> (match f env i CONV t1 t2 with | Success i' -> (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with | Success i'' -> ise_stack2 true i'' q1 q2 | UnifFailure _ as x -> fail x) | UnifFailure _ as x -> fail x) - | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 -> + | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) then ise_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) - | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, - Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 -> + | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, + Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then match ise_and i [ (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); @@ -417,13 +417,13 @@ let exact_ise_stack2 env evd f sk1 sk2 = let rec ise_stack2 i sk1 sk2 = match sk1, sk2 with | [], [] -> Success i - | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 -> + | Stack.Case (_,t1,c1)::q1, Stack.Case (_,t2,c2)::q2 -> ise_and i [ (fun i -> ise_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2); (fun i -> f env i CONV t1 t2)] - | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, - Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 -> + | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, + Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then ise_and i [ (fun i -> ise_stack2 i q1 q2); @@ -431,7 +431,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); (fun i -> ise_stack2 i a1 a2)] else UnifFailure (i,NotSameHead) - | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 -> + | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) @@ -556,9 +556,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env' evd (c'1, Stack.empty) in - let out2, _ = whd_nored_state env' evd - (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), - Cst_stack.empty in + let out2 = whd_nored_state env' evd + (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty) in if onleft then evar_eqappr_x flags env' evd CONV out1 out2 else evar_eqappr_x flags env' evd CONV out2 out1 in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 15bf9667b3..8ab040b3b1 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -24,11 +24,7 @@ open Context.Rel.Declaration exception Elimconst (** This module implements a call by name reduction used by (at - least) evarconv unification and cbn tactic. - - It has an ability to "refold" constants by storing constants and - their parameters in its stack. -*) + least) evarconv unification. *) (** Support for reduction effects *) @@ -174,71 +170,6 @@ module ReductionBehaviour = struct 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 -- there is at most one arguments with an empty list of args, it must be the first. -- in args, the int represents the indice of the first arg to consider *) - type t = (constr * constr list * (int * constr array) list) list - - let empty = [] - let is_empty = CList.is_empty - - let drop_useless = function - | _ :: ((_,_,[])::_ as q) -> q - | l -> l - - let add_param h cst_l = - let append2cst = function - | (c,params,[]) -> (c, h::params, []) - | (c,params,((i,t)::q)) when i = pred (Array.length t) -> - (c, params, q) - | (c,params,(i,t)::q) -> - (c, params, (succ i,t)::q) - in - drop_useless (List.map append2cst cst_l) - - let add_args cl = - List.map (fun (a,b,args) -> (a,b,(0,cl)::args)) - - let add_cst cst = function - | (_,_,[]) :: q as l -> l - | l -> (cst,[],[])::l - - let best_cst = function - | (cst,params,[])::_ -> Some(cst,params) - | _ -> None - - 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] - by [cst_l] in [c] *) - let best_replace sigma d cst_l c = - 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 - (reconstruct_head d args) - (applist (cst, List.rev params)) - t) cst_l c - - let pr env sigma l = - let open Pp in - let p_c c = Termops.Internal.print_constr_env env sigma 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:" ++ - pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++ - str ")")) l -end - - (** The type of (machine) stacks (= lambda-bar-calculus' contexts) *) module Stack : sig @@ -246,17 +177,12 @@ sig type 'a app_node val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t - type cst_member = - | Cst_const of pconstant - | Cst_proj of Projection.t - type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of Projection.t * Cst_stack.t - | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t - | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t - | Cst of cst_member * int * int list * 'a t * Cst_stack.t + | Case of case_info * 'a * 'a array + | Proj of Projection.t + | Fix of ('a, 'a) pfixpoint * 'a t + | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red and 'a t = 'a member list @@ -268,8 +194,6 @@ 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 -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool) - -> 'a t -> 'a t -> bool val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> @@ -278,14 +202,12 @@ sig val strip_app : 'a t -> 'a t * 'a t val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option val not_purely_applicative : 'a t -> bool - val will_expose_iota : 'a t -> bool val list_of_app_stack : constr t -> constr list option val assign : 'a t -> int -> 'a -> 'a t val args_size : 'a t -> int val tail : int -> 'a t -> 'a t val nth : 'a t -> int -> 'a - val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t - val zip : ?refold:bool -> evar_map -> constr * constr t -> constr + val zip : evar_map -> constr * constr t -> constr val check_native_args : CPrimitives.t -> 'a t -> bool val get_next_primitive_args : CPrimitives.args_red -> 'a t -> CPrimitives.args_red * ('a t * 'a * 'a t) option end = @@ -307,17 +229,12 @@ struct ) - type cst_member = - | Cst_const of pconstant - | Cst_proj of Projection.t - type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of Projection.t * Cst_stack.t - | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t - | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t - | Cst of cst_member * int * int list * 'a t * Cst_stack.t + | Case of case_info * 'a * 'a array + | Proj of Projection.t + | Fix of ('a, 'a) pfixpoint * 'a t + | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red and 'a t = 'a member list @@ -327,37 +244,22 @@ struct let pr_c x = hov 1 (pr_c x) in match member with | App app -> str "ZApp" ++ pr_app_node pr_c app - | Case (_,_,br,cst) -> + | Case (_,_,br) -> str "ZCase(" ++ prvect_with_sep (pr_bar) pr_c br ++ str ")" - | Proj (p,cst) -> + | Proj p -> str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")" - | Fix (f,args,cst) -> + | Fix (f,args) -> str "ZFix(" ++ Constr.debug_print_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" - | Primitive (p,c,args,kargs,cst_l) -> + | Primitive (p,c,args,kargs) -> str "ZPrimitive(" ++ str (CPrimitives.to_string p) ++ 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 - ++ pr_comma () ++ - prlist_with_sep pr_semicolon int remains ++ - pr_comma () ++ pr pr_c params ++ str ")" and pr pr_c l = let open Pp in prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l - and pr_cst_member pr_c c = - let open Pp in - match c with - | Cst_const (c, u) -> - if Univ.Instance.is_empty u then Constant.debug_print c - else str"(" ++ Constant.debug_print c ++ str ", " ++ - Univ.Instance.pr Univ.Level.pr u ++ str")" - | Cst_proj p -> - str".(" ++ Constant.debug_print (Projection.constant p) ++ str")" - let empty = [] let is_empty = CList.is_empty @@ -377,54 +279,21 @@ struct if i < j then (l.(j), App (i,l,pred j) :: sk) else (l.(j), sk) - let equal f f_fix sk1 sk2 = - let equal_cst_member x y = - match x, y with - | Cst_const (c1,u1), Cst_const (c2, u2) -> - Constant.equal c1 c2 && Univ.Instance.equal u1 u2 - | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2 - | _, _ -> false - in - let rec equal_rec sk1 sk2 = - match sk1,sk2 with - | [],[] -> true - | App a1 :: s1, App a2 :: s2 -> - let t1,s1' = decomp_node_last a1 s1 in - let t2,s2' = decomp_node_last a2 s2 in - (f t1 t2) && (equal_rec s1' s2') - | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> - f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 - | (Proj (p,_)::s1, Proj(p2,_)::s2) -> - Projection.Repr.equal (Projection.repr p) (Projection.repr p2) - && equal_rec s1 s2 - | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> - f_fix f1 f2 - && equal_rec (List.rev s1) (List.rev s2) - && equal_rec s1' s2' - | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' -> - equal_cst_member c1 c2 - && equal_rec (List.rev params1) (List.rev params2) - && equal_rec s1' s2' - | ((App _|Case _|Proj _|Fix _|Cst _|Primitive _)::_|[]), _ -> false - in equal_rec (List.rev sk1) (List.rev sk2) - let compare_shape stk1 stk2 = let rec compare_rec bal stk1 stk2 = match (stk1,stk2) with ([],[]) -> Int.equal bal 0 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 - | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> + | (Case(c1,_,_)::s1, Case(c2,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 - | (Proj (p,_)::s1, Proj(p2,_)::s2) -> + | (Proj (p)::s1, Proj(p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) -> + | (Fix(_,a1)::s1, Fix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 - | (Primitive(_,_,a1,_,_)::s1, Primitive(_,_,a2,_,_)::s2) -> + | (Primitive(_,_,a1,_)::s1, Primitive(_,_,a2,_)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 - | (Cst (_,_,_,p1,_)::s1, Cst (_,_,_,p2,_)::s2) -> - Int.equal bal 0 && compare_rec 0 p1 p2 && compare_rec 0 s1 s2 - | ((Case _|Proj _|Fix _|Cst _|Primitive _) :: _ | []) ,_ -> false in + | ((Case _|Proj _|Fix _|Primitive _) :: _ | []) ,_ -> false in compare_rec 0 stk1 stk2 exception IncompatibleFold2 @@ -436,32 +305,27 @@ struct let t1,l1 = decomp_node_last n1 q1 in let t2,l2 = decomp_node_last n2 q2 in aux (f o t1 t2) l1 l2 - | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 -> + | Case (_,t1,a1) :: q1, Case (_,t2,a2) :: q2 -> aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 - | Proj (p1,_) :: q1, Proj (p2,_) :: q2 -> + | Proj (p1) :: q1, Proj (p2) :: q2 -> aux o q1 q2 - | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 -> + | Fix ((_,(_,a1,b1)),s1) :: q1, Fix ((_,(_,a2,b2)),s2) :: q2 -> let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in aux o' q1 q2 - | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 -> - let o' = aux o (List.rev params1) (List.rev params2) in - aux o' q1 q2 - | (((App _|Case _|Proj _|Fix _|Cst _|Primitive _) :: _|[]), _) -> + | (((App _|Case _|Proj _|Fix _|Primitive _) :: _|[]), _) -> raise IncompatibleFold2 in aux o (List.rev sk1) (List.rev sk2) let rec map f x = List.map (function - | (Proj (_,_)) as e -> e + | (Proj (_)) as e -> e | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) - | Case (info,ty,br,alt) -> Case (info, f ty, Array.map f br, alt) - | Fix ((r,(na,ty,bo)),arg,alt) -> - Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg,alt) - | Cst (cst,curr,remains,params,alt) -> - Cst (cst,curr,remains,map f params,alt) - | Primitive (p,c,args,kargs,cst_l) -> - Primitive(p,c, map f args, kargs, cst_l) + | Case (info,ty,br) -> Case (info, f ty, Array.map f br) + | Fix ((r,(na,ty,bo)),arg) -> + Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg) + | Primitive (p,c,args,kargs) -> + Primitive(p,c, map f args, kargs) ) x let append_app_list l s = @@ -470,7 +334,7 @@ struct let rec args_size = function | App (i,_,j)::s -> j + 1 - i + args_size s - | (Case _|Fix _|Proj _|Cst _|Primitive _)::_ | [] -> 0 + | (Case _|Fix _|Proj _|Primitive _)::_ | [] -> 0 let strip_app s = let rec aux out = function @@ -493,13 +357,8 @@ struct in aux n [] s let not_purely_applicative args = - List.exists (function (Fix _ | Case _ | Proj _ | Cst _) -> true + List.exists (function (Fix _ | Case _ | Proj _ ) -> true | App _ | Primitive _ -> false) args - let will_expose_iota args = - List.exists - (function (Fix (_,_,l) | Case (_,_,_,l) | - Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false) - args let list_of_app_stack s = let rec aux = function @@ -536,27 +395,7 @@ struct | Some (_,el,_) -> el | None -> raise Not_found - (** This function breaks the abstraction of Cst_stack ! *) - 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 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) - | _ -> def - in List.fold_left (aux sk) s l - - let constr_of_cst_member f sk = - match f with - | Cst_const (c, u) -> mkConstU (c, EInstance.make u), sk - | Cst_proj p -> - match decomp sk with - | Some (hd, sk) -> mkProj (p, hd), sk - | None -> assert false - - let zip ?(refold=false) sigma s = + let zip sigma s = let rec zip = function | f, [] -> f | f, (App (i,a,j) :: s) -> @@ -564,21 +403,11 @@ struct then a else Array.sub a i (j - i + 1) in zip (mkApp (f, a'), s) - | f, (Case (ci,rt,br,cst_l)::s) when refold -> - 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 (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l) - | f, (Fix (fix,st,_)::s) -> zip + | f, (Case (ci,rt,br)::s) -> zip (mkCase (ci,rt,f,br), s) + | f, (Fix (fix,st)::s) -> zip (mkFix fix, st @ (append_app [|f|] s)) - | f, (Cst (cst,_,_,params,cst_l)::s) when refold -> - zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) - | f, (Cst (cst,_,_,params,_)::s) -> - zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) - | f, (Proj (p,cst_l)::s) when refold -> - zip (best_state sigma (mkProj (p,f),s) cst_l) - | f, (Proj (p,_)::s) -> zip (mkProj (p,f),s) - | f, (Primitive (p,c,args,kargs,cst_l)::s) -> + | f, (Proj (p)::s) -> zip (mkProj (p,f),s) + | f, (Primitive (p,c,args,kargs)::s) -> zip (mkConstU c, args @ append_app [|f|] s) in zip s @@ -656,17 +485,16 @@ let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA] (* Beta Reduction tools *) -let apply_subst recfun env sigma refold cst_l t stack = - let rec aux env cst_l t stack = +let apply_subst recfun env sigma t stack = + let rec aux env t stack = 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 sigma cst_l (substl env t, stack) - in aux env cst_l t stack + aux (h::env) c stacktl + | _ -> recfun sigma (substl env t, stack) + in aux env t stack let stacklam recfun env sigma t stack = - apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack + apply_subst (fun _ s -> recfun s) env sigma t stack let beta_applist sigma (c,l) = let zip s = Stack.zip sigma s in @@ -685,73 +513,25 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with | Construct _ | CoFix _ -> true | _ -> false -(** @return c if there is a constant c whose body is bd - @return bd else. - - It has only a meaning because internal representation of "Fixpoint f x - := t" is Definition f := fix f x => t - - Even more fragile that we could hope because do Module M. Fixpoint - f x := t. End M. Definition f := u. and say goodbye to any hope - of refolding M.f this way ... -*) -let magically_constant_of_fixbody env sigma reference bd = function - | Name.Anonymous -> bd - | Name.Name id -> - let open UnivProblem in - let (cst_mod,_) = Constant.repr2 reference in - let cst = Constant.make2 cst_mod (Label.of_id id) in - if not (Environ.mem_constant cst env) then bd - else - let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in - match constant_opt_value_in env (cst,u) with - | None -> bd - | Some t -> - let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in - begin match csts with - | Some csts -> - let subst = Set.fold (fun cst acc -> - let l, r = match cst with - | ULub (u, v) | UWeak (u, v) -> u, v - | UEq (u, v) | ULe (u, v) -> - let get u = Option.get (Universe.level u) in - get u, get v - in - Univ.LMap.add l r acc) - csts Univ.LMap.empty - in - let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in - mkConstU (cst, EInstance.make inst) - | None -> bd - end - -let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = +let contract_cofix sigma (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = let ind = nbodies-j-1 in if Int.equal bodynum ind then mkCoFix (ind,typedbodies) else let bd = mkCoFix (ind,typedbodies) in - match env with - | None -> bd - | Some e -> - match reference with - | None -> bd - | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in + bd + in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) (** Similar to the "fix" case below *) -let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk = +let reduce_and_refold_cofix recfun env sigma cofix sk = let raw_answer = - let env = if refold then Some env else None in - contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in + contract_cofix sigma cofix in apply_subst - (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')) - [] sigma refold Cst_stack.empty raw_answer sk + (fun _ (t,sk') -> recfun (t,sk')) + [] sigma raw_answer sk let reduce_mind_case sigma mia = match EConstr.kind sigma mia.mconstr with @@ -767,19 +547,15 @@ let reduce_mind_case sigma mia = (* 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 sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = +let contract_fix sigma ((recindices,bodynum),(names,types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = let ind = nbodies-j-1 in if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies) else let bd = mkFix ((recindices,ind),typedbodies) in - match env with - | None -> bd - | Some e -> - match reference with - | None -> bd - | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in + bd + in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -787,18 +563,12 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies 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 reduce_and_refold_fix recfun env sigma fix sk = let raw_answer = - let env = if refold then Some env else None in - contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in + contract_fix sigma fix in apply_subst - (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')) - [] sigma refold Cst_stack.empty raw_answer sk + (fun _ (t,sk') -> recfun (t,sk')) + [] sigma raw_answer sk let fix_recarg ((recindices,bodynum),_) stack = assert (0 <= bodynum && bodynum < Array.length recindices); @@ -952,21 +722,14 @@ let debug_RAKAM = ~key:["Debug";"RAKAM"] ~value:false -let equal_stacks sigma (x, l) (y, l') = - let f_equal x y = eq_constr sigma x y in - let eq_fix a b = f_equal (mkFix a) (mkFix b) in - Stack.equal f_equal eq_fix l l' && f_equal x y - -let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = +let rec whd_state_gen flags env sigma = let open Context.Named.Declaration in - let open ReductionBehaviour in - let rec whrec cst_l (x, stack) = + let rec whrec (x, stack) : state = let () = if debug_RAKAM () then let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in Feedback.msg_debug (h 0 (str "<<" ++ pr x ++ - str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ str ">>")) in @@ -974,22 +737,22 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let fold () = let () = if debug_RAKAM () then let open Pp in Feedback.msg_debug (str "<><><><><>") in - ((EConstr.of_kind c0, stack),cst_l) + ((EConstr.of_kind c0, stack)) in 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 (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 (body, stack) | _ -> fold ()) | Evar ev -> fold () | Meta ev -> (match safe_meta_value sigma ev with - | Some body -> whrec cst_l (body, stack) + | Some body -> whrec (body, stack) | None -> fold ()) | Const (c,u as const) -> reduction_effect_hook env sigma c @@ -1000,175 +763,70 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | body -> begin 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) - else (* Looks for ReductionBehaviour *) - match ReductionBehaviour.get (GlobRef.ConstRef c) with - | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) - | Some behavior -> - begin match behavior with - | NeverUnfold -> fold () - | (UnfoldWhen { nargs = Some n } | - UnfoldWhenNoMatch { nargs = Some n } ) - when Stack.args_size stack < n -> - fold () - | UnfoldWhenNoMatch { recargs } -> (* maybe unfolds *) - let app_sk,sk = Stack.strip_app stack in - let (tm',sk'),cst_l' = - whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) - in - 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 sigma (x, app_sk) (tm', sk') - || Stack.will_expose_iota sk' - || is_case tm' - then fold () - else whrec cst_l' (tm', sk' @ sk) - | UnfoldWhen { recargs } -> (* maybe unfolds *) - begin match recargs with - |[] -> (* if nargs has been specified *) - (* CAUTION : the constant is NEVER refold - (even when it hides a (co)fix) *) - whrec cst_l (body, stack) - |curr::remains -> match Stack.strip_n_app curr stack with - | None -> fold () - | Some (bef,arg,s') -> - whrec Cst_stack.empty - (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') - end - end - end + whrec (body, stack) + end | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack -> let kargs = CPrimitives.kind p in let (kargs,o) = Stack.get_next_primitive_args kargs stack in (* Should not fail thanks to [check_native_args] *) let (before,a,after) = Option.get o in - whrec Cst_stack.empty (a,Stack.Primitive(p,const,before,kargs,cst_l)::after) + whrec (a,Stack.Primitive(p,const,before,kargs)::after) | exception NotEvaluableConst _ -> fold () else fold () | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> - (let npars = Projection.npars p in - if not tactic_mode then - let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in - whrec Cst_stack.empty stack' - else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with - | None -> - let stack' = (c, Stack.Proj (p, cst_l) :: stack) in - let stack'', csts = whrec Cst_stack.empty stack' in - if equal_stacks sigma stack' stack'' then fold () - else stack'', csts - | Some behavior -> - begin match behavior with - | NeverUnfold -> fold () - | (UnfoldWhen { nargs = Some n } - | UnfoldWhenNoMatch { nargs = Some n }) - when Stack.args_size stack < n - (npars + 1) -> fold () - | UnfoldWhen { recargs } - | UnfoldWhenNoMatch { recargs }-> (* maybe unfolds *) - let recargs = List.map_filter (fun x -> - let idx = x - npars in - if idx < 0 then None else Some idx) recargs - in - match recargs with - |[] -> (* if nargs has been specified *) - (* CAUTION : the constant is NEVER refold - (even when it hides a (co)fix) *) - let stack' = (c, Stack.Proj (p, cst_l) :: stack) in - whrec Cst_stack.empty(* cst_l *) stack' - | curr::remains -> - if curr == 0 then (* Try to reduce the record argument *) - whrec Cst_stack.empty - (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack) - else - match Stack.strip_n_app curr stack with - | None -> fold () - | Some (bef,arg,s') -> - whrec Cst_stack.empty - (arg,Stack.Cst(Stack.Cst_proj p,curr,remains, - Stack.append_app [|c|] bef,cst_l)::s') - end) + let stack' = (c, Stack.Proj (p) :: stack) in + whrec stack' | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> - apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack - | Cast (c,_,_) -> whrec cst_l (c, stack) + apply_subst (fun _ -> whrec) [b] sigma c stack + | Cast (c,_,_) -> whrec (c, stack) | App (f,cl) -> whrec - (if refold then Cst_stack.add_args cl cst_l else cst_l) (f, Stack.append_app cl stack) | Lambda (na,t,c) -> (match Stack.decomp stack with | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> - apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack + apply_subst (fun _ -> whrec) [] sigma x stack | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> let env' = push_rel (LocalAssum (na, t)) env in - let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in - (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with + let whrec' = whd_state_gen flags env' sigma in + (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 + let (x', l') = whrec' (Array.last cl, Stack.empty) in 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 mkApp (f,lc) in - if noccurn sigma 1 u then (pop u,Stack.empty),Cst_stack.empty else fold () + if noccurn sigma 1 u then (pop u,Stack.empty) else fold () | _ -> fold () else fold () | _ -> fold ()) | _ -> fold ()) | Case (ci,p,d,lf) -> - whrec Cst_stack.empty (d, Stack.Case (ci,p,lf,cst_l) :: stack) + whrec (d, Stack.Case (ci,p,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with |None -> fold () |Some (bef,arg,s') -> - whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s')) + whrec (arg, Stack.Fix(f,bef)::s')) | Construct ((ind,c),u) -> let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> - whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (p,_)::s') when use_match -> - whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s') - |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> + |args, (Stack.Case(ci, _, lf)::s') when use_match -> + whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') + |args, (Stack.Proj (p)::s') when use_match -> + whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') + |args, (Stack.Fix (f,s')::s'') when use_fix -> 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 sigma (x, args) in - begin match remains with - | [] -> - (match const with - | Stack.Cst_const const -> - (match constant_opt_value_in env const with - | None -> fold () - | Some body -> - let const = (fst const, EInstance.make (snd const)) in - 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 -> - let stack = s' @ (Stack.append_app [|x'|] s'') in - match Stack.strip_n_app 0 stack with - | None -> assert false - | Some (_,arg,s'') -> - whrec Cst_stack.empty (arg, Stack.Proj (p,cst_l) :: s'')) - | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with - | None -> fold () - | Some (bef,arg,s''') -> - whrec Cst_stack.empty - (arg, - Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') - end + reduce_and_refold_fix whrec env sigma f out_sk |_, (Stack.App _)::_ -> assert false |_, _ -> fold () else fold () @@ -1177,19 +835,19 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ |Stack.Proj _)::s') -> - reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack + reduce_and_refold_cofix whrec env sigma cofix stack |_ -> fold () else fold () | Int _ | Float _ -> begin match Stack.strip_app stack with - | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) -> + | (_, Stack.Primitive(p,kn,rargs,kargs)::s) -> let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in if more_to_reduce then let (kargs,o) = Stack.get_next_primitive_args kargs s in (* Should not fail because Primitive is put on the stack only if fully applied *) let (before,a,after) = Option.get o in - whrec Cst_stack.empty (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs,cst_l')::after) + whrec (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs)::after) else let n = List.length kargs in let (args,s) = Stack.strip_app s in @@ -1199,8 +857,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = in let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in begin match CredNative.red_prim env sigma p args with - | Some t -> whrec cst_l' (t,s) - | None -> ((mkApp (mkConstU kn, args), s), cst_l) + | Some t -> whrec (t,s) + | None -> ((mkApp (mkConstU kn, args), s)) end | _ -> fold () end @@ -1208,9 +866,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Rel _ | Var _ | LetIn _ | Proj _ -> fold () | Sort _ | Ind _ | Prod _ -> fold () 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 sigma s cst_l,Cst_stack.empty) else res + whrec (** reduction machine without global env and refold machinery *) let local_whd_state_gen flags _env sigma = @@ -1243,15 +899,15 @@ let local_whd_state_gen flags _env sigma = | _ -> s) | Proj (p,c) when CClosure.RedFlags.red_projection flags p -> - (whrec (c, Stack.Proj (p, Cst_stack.empty) :: stack)) + (whrec (c, Stack.Proj (p) :: stack)) | Case (ci,p,d,lf) -> - whrec (d, Stack.Case (ci,p,lf,Cst_stack.empty) :: stack) + whrec (d, Stack.Case (ci,p,lf) :: stack) | Fix ((ri,n),_ as f) -> (match Stack.strip_n_app ri.(n) stack with |None -> s - |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef,Cst_stack.empty)::s')) + |Some (bef,arg,s') -> whrec (arg, Stack.Fix(f,bef)::s')) | Evar ev -> s | Meta ev -> @@ -1264,14 +920,14 @@ let local_whd_state_gen flags _env sigma = let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in if use_match || use_fix then match Stack.strip_app stack with - |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> + |args, (Stack.Case(ci, _, lf)::s') when use_match -> whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') - |args, (Stack.Proj (p,_) :: s') when use_match -> + |args, (Stack.Proj (p) :: s') when use_match -> whrec (Stack.nth args (Projection.npars p + Projection.arg p), s') - |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> + |args, (Stack.Fix (f,s')::s'') when use_fix -> let x' = Stack.zip sigma (x,args) in whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s'')) - |_, (Stack.App _|Stack.Cst _)::_ -> assert false + |_, (Stack.App _)::_ -> assert false |_, _ -> s else s @@ -1290,9 +946,7 @@ let local_whd_state_gen flags _env sigma = whrec let raw_whd_state_gen flags env = - let f sigma s = fst (whd_state_gen ~refold:false - ~tactic_mode:false - flags env sigma s) in + let f sigma s = whd_state_gen flags env sigma s in f let stack_red_of_state_red f = @@ -1300,11 +954,11 @@ let stack_red_of_state_red f = f (* Drops the Cst_stack *) -let iterate_whd_gen refold flags env sigma s = +let iterate_whd_gen flags env sigma s = let rec aux t = - let (hd,sk),_ = whd_state_gen ~refold ~tactic_mode:false flags env sigma (t,Stack.empty) in + let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in let whd_sk = Stack.map aux sk in - Stack.zip sigma ~refold (hd,whd_sk) + Stack.zip sigma (hd,whd_sk) in aux s let red_of_state_red f env sigma x = @@ -1717,8 +1371,6 @@ let is_sort env sigma t = of case/fix (heuristic used by evar_conv) *) let whd_betaiota_deltazeta_for_iota_state ts env sigma s = - let refold = false in - let tactic_mode = false in let all' = CClosure.RedFlags.red_add_transparent CClosure.all ts in (* Unset the sharing flag to get a call-by-name reduction. This matters for the shape of the generated term. *) @@ -1738,7 +1390,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma s = | _ -> None in let rec whrec s = - let (t, stack as s), _ = whd_state_gen ~refold ~tactic_mode CClosure.betaiota env sigma s in + let (t, stack as s) = whd_state_gen CClosure.betaiota env sigma s in match Stack.strip_app stack with |args, (Stack.Case _ :: _ as stack') -> begin match whd_opt (t, args) with @@ -1750,13 +1402,13 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma s = | Some (t_o, args) when isConstruct sigma t_o -> whrec (t_o, Stack.append_app args stack') | (Some _ | None) -> s end - |args, (Stack.Proj (p,_) :: stack'') -> + |args, (Stack.Proj p :: stack'') -> begin match whd_opt (t, args) with | Some (t_o, args) when isConstruct sigma t_o -> whrec (args.(Projection.npars p + Projection.arg p), stack'') | (Some _ | None) -> s end - |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s + |_, ((Stack.App _|Stack.Primitive _) :: _|[]) -> s in whrec s diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index be91f688e7..a0cbd8ccf7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -19,6 +19,11 @@ open Environ exception Elimconst +val debug_RAKAM : unit -> bool + +module CredNative : Primred.RedNative with + type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map + (** Machinery to customize the behavior of the reduction *) module ReductionBehaviour : sig @@ -46,41 +51,17 @@ val set_reduction_effect : Constant.t -> effect_name -> unit val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constant.t -> Constr.constr Lazy.t -> unit -(** {6 Machinery about a stack of unfolded constant } - - cst applied to params must convertible to term of the state applied to args -*) -module Cst_stack : sig - type t - val empty : t - val add_param : constr -> t -> t - val add_args : constr array -> t -> t - val add_cst : constr -> t -> t - val best_cst : t -> (constr * constr list) option - val best_replace : Evd.evar_map -> constr -> t -> constr -> constr - val reference : Evd.evar_map -> t -> Constant.t option - val pr : env -> Evd.evar_map -> t -> Pp.t -end - module Stack : sig type 'a app_node val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t - type cst_member = - | Cst_const of pconstant - | Cst_proj of Projection.t - type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of Projection.t * Cst_stack.t - | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t - | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t - | Cst of cst_member - * int (* current foccussed arg *) - * int list (* remaining args *) - * 'a t * Cst_stack.t + | Case of case_info * 'a * 'a array + | Proj of Projection.t + | Fix of ('a, 'a) pfixpoint * 'a t + | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red and 'a t = 'a member list val pr : ('a -> Pp.t) -> 'a t -> Pp.t @@ -119,8 +100,7 @@ module Stack : sig val tail : int -> 'a t -> 'a t val nth : 'a t -> int -> 'a - val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t - val zip : ?refold:bool -> evar_map -> constr * constr t -> constr + val zip : evar_map -> constr * constr t -> constr end (************************************************************************) @@ -155,10 +135,10 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a -val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool -> - CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t +val whd_state_gen : + CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state -val iterate_whd_gen : bool -> CClosure.RedFlags.reds -> +val iterate_whd_gen : CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> constr -> constr (** {6 Generic Optimized Reduction Function using Closures } *) @@ -260,7 +240,7 @@ val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EI val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool -val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixpoint -> constr +val contract_fix : evar_map -> fixpoint -> constr val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 88eec5ea01..95b07e227e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -487,7 +487,7 @@ let expand_table_key env = function | RelKey _ -> None let unfold_projection env p stk = - let s = Stack.Proj (p, Cst_stack.empty) in + let s = Stack.Proj p in s :: stk let expand_key ts env sigma = function diff --git a/tactics/cbn.ml b/tactics/cbn.ml new file mode 100644 index 0000000000..21e38df6db --- /dev/null +++ b/tactics/cbn.ml @@ -0,0 +1,797 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +open Names +open Constr +open Context +open Termops +open Univ +open Evd +open Environ +open EConstr +open Vars +open Context.Rel.Declaration + +(** This module implements a call by name reduction used by the cbn tactic. + + It has an ability to "refold" constants by storing constants and + their parameters in its stack. +*) + +(** Machinery to custom the behavior of the reduction *) +module ReductionBehaviour = Reductionops.ReductionBehaviour + +(** 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 +- there is at most one arguments with an empty list of args, it must be the first. +- in args, the int represents the indice of the first arg to consider *) + type t = (constr * constr list * (int * constr array) list) list + + let empty = [] + let is_empty = CList.is_empty + + let drop_useless = function + | _ :: ((_,_,[])::_ as q) -> q + | l -> l + + let add_param h cst_l = + let append2cst = function + | (c,params,[]) -> (c, h::params, []) + | (c,params,((i,t)::q)) when i = pred (Array.length t) -> + (c, params, q) + | (c,params,(i,t)::q) -> + (c, params, (succ i,t)::q) + in + drop_useless (List.map append2cst cst_l) + + let add_args cl = + List.map (fun (a,b,args) -> (a,b,(0,cl)::args)) + + let add_cst cst = function + | (_,_,[]) :: q as l -> l + | l -> (cst,[],[])::l + + let best_cst = function + | (cst,params,[])::_ -> Some(cst,params) + | _ -> None + + 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] + by [cst_l] in [c] *) + let best_replace sigma d cst_l c = + 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 + (reconstruct_head d args) + (applist (cst, List.rev params)) + t) cst_l c + + let pr env sigma l = + let open Pp in + let p_c c = Termops.Internal.print_constr_env env sigma 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:" ++ + pr_sequence (fun (i,el) -> prvect_with_sep spc p_c (Array.sub el i (Array.length el - i))) args ++ + str ")")) l +end + + +(** The type of (machine) stacks (= lambda-bar-calculus' contexts) *) +module Stack : +sig + open EConstr + type 'a app_node + + type cst_member = + | Cst_const of pconstant + | Cst_proj of Projection.t + + type 'a member = + | App of 'a app_node + | Case of case_info * 'a * 'a array * Cst_stack.t + | Proj of Projection.t * Cst_stack.t + | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t + | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t + | Cst of cst_member * int * int list * 'a t * Cst_stack.t + + and 'a t = 'a member list + + exception IncompatibleFold2 + + val pr : ('a -> Pp.t) -> 'a t -> Pp.t + val empty : 'a t + val append_app : 'a array -> 'a t -> 'a t + val decomp : 'a t -> ('a * 'a t) option + val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool) + -> 'a t -> 'a t -> bool + val strip_app : 'a t -> 'a t * 'a t + val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option + val will_expose_iota : 'a t -> bool + val list_of_app_stack : constr t -> constr list option + val args_size : 'a t -> int + val tail : int -> 'a t -> 'a t + val nth : 'a t -> int -> 'a + val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t + val zip : ?refold:bool -> evar_map -> constr * constr t -> constr + val check_native_args : CPrimitives.t -> 'a t -> bool + val get_next_primitive_args : CPrimitives.args_red -> 'a t -> CPrimitives.args_red * ('a t * 'a * 'a t) option +end = +struct + open EConstr + type 'a app_node = int * 'a array * int + (* first releavnt position, arguments, last relevant position *) + + (* + Invariant that this module must ensure : + (behare of direct access to app_node by the rest of Reductionops) + - in app_node (i,_,j) i <= j + - There is no array realocation (outside of debug printing) + *) + + let pr_app_node pr (i,a,j) = + let open Pp in surround ( + prvect_with_sep pr_comma pr (Array.sub a i (j - i + 1)) + ) + + + type cst_member = + | Cst_const of pconstant + | Cst_proj of Projection.t + + type 'a member = + | App of 'a app_node + | Case of case_info * 'a * 'a array * Cst_stack.t + | Proj of Projection.t * Cst_stack.t + | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t + | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t + | Cst of cst_member * int * int list * 'a t * Cst_stack.t + + and 'a t = 'a member list + + (* Debugging printer *) + let rec pr_member pr_c member = + let open Pp in + let pr_c x = hov 1 (pr_c x) in + match member with + | App app -> str "ZApp" ++ pr_app_node pr_c app + | Case (_,_,br,cst) -> + str "ZCase(" ++ + prvect_with_sep (pr_bar) pr_c br + ++ str ")" + | Proj (p,cst) -> + str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")" + | Fix (f,args,cst) -> + str "ZFix(" ++ Constr.debug_print_fix pr_c f + ++ pr_comma () ++ pr pr_c args ++ str ")" + | Primitive (p,c,args,kargs,cst_l) -> + str "ZPrimitive(" ++ str (CPrimitives.to_string p) + ++ 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 + ++ pr_comma () ++ + prlist_with_sep pr_semicolon int remains ++ + pr_comma () ++ pr pr_c params ++ str ")" + and pr pr_c l = + let open Pp in + prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l + + and pr_cst_member pr_c c = + let open Pp in + match c with + | Cst_const (c, u) -> + if Univ.Instance.is_empty u then Constant.debug_print c + else str"(" ++ Constant.debug_print c ++ str ", " ++ + Univ.Instance.pr Univ.Level.pr u ++ str")" + | Cst_proj p -> + str".(" ++ Constant.debug_print (Projection.constant p) ++ str")" + + let empty = [] + + let append_app v s = + let le = Array.length v in + if Int.equal le 0 then s else App (0,v,pred le) :: s + + let decomp_node (i,l,j) sk = + if i < j then (l.(i), App (succ i,l,j) :: sk) + else (l.(i), sk) + + let decomp = function + | App node::s -> Some (decomp_node node s) + | _ -> None + + let decomp_node_last (i,l,j) sk = + if i < j then (l.(j), App (i,l,pred j) :: sk) + else (l.(j), sk) + + let equal f f_fix sk1 sk2 = + let equal_cst_member x y = + match x, y with + | Cst_const (c1,u1), Cst_const (c2, u2) -> + Constant.equal c1 c2 && Univ.Instance.equal u1 u2 + | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2 + | _, _ -> false + in + let rec equal_rec sk1 sk2 = + match sk1,sk2 with + | [],[] -> true + | App a1 :: s1, App a2 :: s2 -> + let t1,s1' = decomp_node_last a1 s1 in + let t2,s2' = decomp_node_last a2 s2 in + (f t1 t2) && (equal_rec s1' s2') + | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> + f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 + | (Proj (p,_)::s1, Proj(p2,_)::s2) -> + Projection.Repr.equal (Projection.repr p) (Projection.repr p2) + && equal_rec s1 s2 + | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> + f_fix f1 f2 + && equal_rec (List.rev s1) (List.rev s2) + && equal_rec s1' s2' + | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' -> + equal_cst_member c1 c2 + && equal_rec (List.rev params1) (List.rev params2) + && equal_rec s1' s2' + | ((App _|Case _|Proj _|Fix _|Cst _|Primitive _)::_|[]), _ -> false + in equal_rec (List.rev sk1) (List.rev sk2) + + exception IncompatibleFold2 + + let append_app_list l s = + let a = Array.of_list l in + append_app a s + + let rec args_size = function + | App (i,_,j)::s -> j + 1 - i + args_size s + | (Case _|Fix _|Proj _|Cst _|Primitive _)::_ | [] -> 0 + + let strip_app s = + let rec aux out = function + | ( App _ as e) :: s -> aux (e :: out) s + | s -> List.rev out,s + in aux [] s + let strip_n_app n s = + let rec aux n out = function + | App (i,a,j) as e :: s -> + let nb = j - i + 1 in + if n >= nb then + aux (n - nb) (e::out) s + else + let p = i+n in + Some (CList.rev + (if Int.equal n 0 then out else App (i,a,p-1) :: out), + a.(p), + if j > p then App(succ p,a,j)::s else s) + | s -> None + in aux n [] s + + let will_expose_iota args = + List.exists + (function (Fix (_,_,l) | Case (_,_,_,l) | + Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false) + args + + let list_of_app_stack s = + let rec aux = function + | App (i,a,j) :: s -> + let (args',s') = aux s in + let a' = Array.sub a i (j - i + 1) in + (Array.fold_right (fun x y -> x::y) a' args', s') + | s -> ([],s) in + let (out,s') = aux s in + let init = match s' with [] -> true | _ -> false in + Option.init init out + + let tail n0 s0 = + let rec aux n s = + if Int.equal n 0 then s else + match s with + | App (i,a,j) :: s -> + let nb = j - i + 1 in + if n >= nb then + aux (n - nb) s + else + let p = i+n in + if j >= p then App(p,a,j)::s else s + | _ -> raise (Invalid_argument "Reductionops.Stack.tail") + in aux n0 s0 + + let nth s p = + match strip_n_app p s with + | Some (_,el,_) -> el + | None -> raise Not_found + + (** This function breaks the abstraction of Cst_stack ! *) + 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 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) + | _ -> def + in List.fold_left (aux sk) s l + + let constr_of_cst_member f sk = + match f with + | Cst_const (c, u) -> mkConstU (c, EInstance.make u), sk + | Cst_proj p -> + match decomp sk with + | Some (hd, sk) -> mkProj (p, hd), sk + | None -> assert false + + 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 (mkApp (f, a'), s) + | f, (Case (ci,rt,br,cst_l)::s) when refold -> + 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 (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 (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) + | f, (Cst (cst,_,_,params,_)::s) -> + zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) + | f, (Proj (p,cst_l)::s) when refold -> + zip (best_state sigma (mkProj (p,f),s) cst_l) + | f, (Proj (p,_)::s) -> zip (mkProj (p,f),s) + | f, (Primitive (p,c,args,kargs,cst_l)::s) -> + zip (mkConstU c, args @ append_app [|f|] s) + in + zip s + + (* Check if there is enough arguments on [stk] w.r.t. arity of [op] *) + let check_native_args op stk = + let nargs = CPrimitives.arity op in + let rargs = args_size stk in + nargs <= rargs + + let get_next_primitive_args kargs stk = + let rec nargs = function + | [] -> 0 + | CPrimitives.Kwhnf :: _ -> 0 + | _ :: s -> 1 + nargs s + in + let n = nargs kargs in + (List.skipn (n+1) kargs, strip_n_app n stk) + +end + +(** The type of (machine) states (= lambda-bar-calculus' cuts) *) + +(*************************************) +(*** Reduction Functions Operators ***) +(*************************************) + +let safe_meta_value sigma ev = + try Some (Evd.meta_value sigma ev) + with Not_found -> None + +(*************************************) +(*** Reduction using bindingss ***) +(*************************************) + +(* Beta Reduction tools *) + +let apply_subst recfun env sigma refold cst_l t stack = + let rec aux env cst_l t stack = + 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 sigma cst_l (substl env t, stack) + in aux env cst_l t stack + +(* Iota reduction tools *) + +(** @return c if there is a constant c whose body is bd + @return bd else. + + It has only a meaning because internal representation of "Fixpoint f x + := t" is Definition f := fix f x => t + + Even more fragile that we could hope because do Module M. Fixpoint + f x := t. End M. Definition f := u. and say goodbye to any hope + of refolding M.f this way ... +*) +let magically_constant_of_fixbody env sigma reference bd = function + | Name.Anonymous -> bd + | Name.Name id -> + let open UnivProblem in + let (cst_mod,_) = Constant.repr2 reference in + let cst = Constant.make2 cst_mod (Label.of_id id) in + if not (Environ.mem_constant cst env) then bd + else + let (cst, u), ctx = UnivGen.fresh_constant_instance env cst in + match constant_opt_value_in env (cst,u) with + | None -> bd + | Some t -> + let csts = EConstr.eq_constr_universes env sigma (EConstr.of_constr t) bd in + begin match csts with + | Some csts -> + let subst = Set.fold (fun cst acc -> + let l, r = match cst with + | ULub (u, v) | UWeak (u, v) -> u, v + | UEq (u, v) | ULe (u, v) -> + let get u = Option.get (Universe.level u) in + get u, get v + in + Univ.LMap.add l r acc) + csts Univ.LMap.empty + in + let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in + mkConstU (cst, EInstance.make inst) + | None -> bd + end + +let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = + let nbodies = Array.length bodies in + let make_Fi j = + let ind = nbodies-j-1 in + if Int.equal bodynum ind then mkCoFix (ind,typedbodies) + else + let bd = mkCoFix (ind,typedbodies) in + match env with + | None -> bd + | Some e -> + match reference with + | None -> bd + | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in + let closure = List.init nbodies make_Fi in + substl closure bodies.(bodynum) + +(** Similar to the "fix" case below *) +let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk = + let raw_answer = + let env = if refold then Some env else None in + contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in + apply_subst + (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')) + [] sigma refold Cst_stack.empty raw_answer sk + +(* 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 sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = + let nbodies = Array.length recindices in + let make_Fi j = + let ind = nbodies-j-1 in + if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies) + else + let bd = mkFix ((recindices,ind),typedbodies) in + match env with + | None -> bd + | Some e -> + match reference with + | None -> bd + | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in + let closure = List.init nbodies make_Fi in + 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 raw_answer = + let env = if refold then Some env else None in + contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in + apply_subst + (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')) + [] sigma refold Cst_stack.empty raw_answer sk + +module CredNative = Reductionops.CredNative + +(** Generic reduction function with environment + + Here is where unfolded constant are stored in order to be + eventually refolded. + + If tactic_mode is true, it uses ReductionBehaviour, prefers + refold constant instead of value and tries to infer constants + fix and cofix came from. + + It substitutes fix and cofix by the constant they come from in + contract_* in any case . +*) + +let debug_RAKAM = Reductionops.debug_RAKAM + +let equal_stacks sigma (x, l) (y, l') = + let f_equal x y = eq_constr sigma x y in + let eq_fix a b = f_equal (mkFix a) (mkFix b) in + Stack.equal f_equal eq_fix l l' && f_equal x y + +let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = + let open Context.Named.Declaration in + let open ReductionBehaviour in + let rec whrec cst_l (x, stack) = + let () = if debug_RAKAM () then + let open Pp in + let pr c = Termops.Internal.print_constr_env env sigma c in + Feedback.msg_debug + (h 0 (str "<<" ++ pr x ++ + str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ + 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_debug (str "<><><><><>") in + ((EConstr.of_kind c0, stack),cst_l) + in + 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) + | _ -> 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) + | _ -> fold ()) + | Evar ev -> fold () + | Meta ev -> + (match safe_meta_value sigma ev with + | Some body -> whrec cst_l (body, stack) + | None -> fold ()) + | Const (c,u as const) -> + Reductionops.reduction_effect_hook env sigma c + (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack)))); + if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then + let u' = EInstance.kind sigma u in + match constant_value_in env (c, u') with + | body -> + begin + 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) + else (* Looks for ReductionBehaviour *) + match ReductionBehaviour.get (GlobRef.ConstRef c) with + | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) + | Some behavior -> + begin match behavior with + | NeverUnfold -> fold () + | (UnfoldWhen { nargs = Some n } | + UnfoldWhenNoMatch { nargs = Some n } ) + when Stack.args_size stack < n -> + fold () + | UnfoldWhenNoMatch { recargs } -> (* maybe unfolds *) + let app_sk,sk = Stack.strip_app stack in + let (tm',sk'),cst_l' = + whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) + in + 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 sigma (x, app_sk) (tm', sk') + || Stack.will_expose_iota sk' + || is_case tm' + then fold () + else whrec cst_l' (tm', sk' @ sk) + | UnfoldWhen { recargs } -> (* maybe unfolds *) + begin match recargs with + |[] -> (* if nargs has been specified *) + (* CAUTION : the constant is NEVER refold + (even when it hides a (co)fix) *) + whrec cst_l (body, stack) + |curr::remains -> match Stack.strip_n_app curr stack with + | None -> fold () + | Some (bef,arg,s') -> + whrec Cst_stack.empty + (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') + end + end + end + | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack -> + let kargs = CPrimitives.kind p in + let (kargs,o) = Stack.get_next_primitive_args kargs stack in + (* Should not fail thanks to [check_native_args] *) + let (before,a,after) = Option.get o in + whrec Cst_stack.empty (a,Stack.Primitive(p,const,before,kargs,cst_l)::after) + | exception NotEvaluableConst _ -> fold () + else fold () + | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> + (let npars = Projection.npars p in + if not tactic_mode then + let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in + whrec Cst_stack.empty stack' + else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with + | None -> + let stack' = (c, Stack.Proj (p, cst_l) :: stack) in + let stack'', csts = whrec Cst_stack.empty stack' in + if equal_stacks sigma stack' stack'' then fold () + else stack'', csts + | Some behavior -> + begin match behavior with + | NeverUnfold -> fold () + | (UnfoldWhen { nargs = Some n } + | UnfoldWhenNoMatch { nargs = Some n }) + when Stack.args_size stack < n - (npars + 1) -> fold () + | UnfoldWhen { recargs } + | UnfoldWhenNoMatch { recargs }-> (* maybe unfolds *) + let recargs = List.map_filter (fun x -> + let idx = x - npars in + if idx < 0 then None else Some idx) recargs + in + match recargs with + |[] -> (* if nargs has been specified *) + (* CAUTION : the constant is NEVER refold + (even when it hides a (co)fix) *) + let stack' = (c, Stack.Proj (p, cst_l) :: stack) in + whrec Cst_stack.empty(* cst_l *) stack' + | curr::remains -> + if curr == 0 then (* Try to reduce the record argument *) + whrec Cst_stack.empty + (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack) + else + match Stack.strip_n_app curr stack with + | None -> fold () + | Some (bef,arg,s') -> + whrec Cst_stack.empty + (arg,Stack.Cst(Stack.Cst_proj p,curr,remains, + Stack.append_app [|c|] bef,cst_l)::s') + end) + + | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> + apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack + | Cast (c,_,_) -> whrec cst_l (c, stack) + | App (f,cl) -> + whrec + (if refold then Cst_stack.add_args cl cst_l else cst_l) + (f, Stack.append_app cl stack) + | Lambda (na,t,c) -> + (match Stack.decomp stack with + | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> + 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 whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in + (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 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 mkApp (f,lc) in + if noccurn sigma 1 u then (pop u,Stack.empty),Cst_stack.empty else fold () + | _ -> fold () + else fold () + | _ -> fold ()) + | _ -> fold ()) + + | Case (ci,p,d,lf) -> + whrec Cst_stack.empty (d, Stack.Case (ci,p,lf,cst_l) :: stack) + + | Fix ((ri,n),_ as f) -> + (match Stack.strip_n_app ri.(n) stack with + |None -> fold () + |Some (bef,arg,s') -> + whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s')) + + | Construct ((ind,c),u) -> + let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in + let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in + if use_match || use_fix then + match Stack.strip_app stack with + |args, (Stack.Case(ci, _, lf,_)::s') when use_match -> + whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') + |args, (Stack.Proj (p,_)::s') when use_match -> + whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s') + |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> + 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 sigma (x, args) in + begin match remains with + | [] -> + (match const with + | Stack.Cst_const const -> + (match constant_opt_value_in env const with + | None -> fold () + | Some body -> + let const = (fst const, EInstance.make (snd const)) in + 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 -> + let stack = s' @ (Stack.append_app [|x'|] s'') in + match Stack.strip_n_app 0 stack with + | None -> assert false + | Some (_,arg,s'') -> + whrec Cst_stack.empty (arg, Stack.Proj (p,cst_l) :: s'')) + | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with + | None -> fold () + | Some (bef,arg,s''') -> + whrec Cst_stack.empty + (arg, + Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') + end + |_, (Stack.App _)::_ -> assert false + |_, _ -> fold () + else fold () + + | CoFix cofix -> + if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then + match Stack.strip_app stack with + |args, ((Stack.Case _ |Stack.Proj _)::s') -> + reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack + |_ -> fold () + else fold () + + | Int _ | Float _ -> + begin match Stack.strip_app stack with + | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) -> + let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in + if more_to_reduce then + let (kargs,o) = Stack.get_next_primitive_args kargs s in + (* Should not fail because Primitive is put on the stack only if fully applied *) + let (before,a,after) = Option.get o in + whrec Cst_stack.empty (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs,cst_l')::after) + else + let n = List.length kargs in + let (args,s) = Stack.strip_app s in + let (args,extra_args) = + try List.chop n args + with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *) + in + let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in + begin match CredNative.red_prim env sigma p args with + | Some t -> whrec cst_l' (t,s) + | None -> ((mkApp (mkConstU kn, args), s), cst_l) + end + | _ -> fold () + end + + | Rel _ | Var _ | LetIn _ | Proj _ -> fold () + | Sort _ | Ind _ | Prod _ -> fold () + 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 sigma s cst_l,Cst_stack.empty) else res + +let whd_cbn flags env sigma t = + let (state,_) = + (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty)) + in + Stack.zip ~refold:true sigma state diff --git a/tactics/cbn.mli b/tactics/cbn.mli new file mode 100644 index 0000000000..af54771382 --- /dev/null +++ b/tactics/cbn.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val whd_cbn : + CClosure.RedFlags.reds -> + Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index f681e4e99e..e000ddce74 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -44,11 +44,7 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) -let whd_cbn flags env sigma t = - let (state,_) = - (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty)) - in - Reductionops.Stack.zip ~refold:true sigma state +let whd_cbn = Cbn.whd_cbn let strong_cbn flags = strong_with_flags whd_cbn flags diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 36d61feed1..88025e3fb4 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -9,6 +9,7 @@ Eqschemes Elimschemes Genredexpr Redops +Cbn Redexpr Ppred Tactics |