aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarconv.ml21
-rw-r--r--pretyping/reductionops.ml552
-rw-r--r--pretyping/reductionops.mli48
-rw-r--r--pretyping/unification.ml2
4 files changed, 127 insertions, 496 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:33:44 +0000