diff options
| -rw-r--r-- | dev/include | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 1 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 32 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 32 |
5 files changed, 36 insertions, 33 deletions
diff --git a/dev/include b/dev/include index 4a025d077..7c63f5443 100644 --- a/dev/include +++ b/dev/include @@ -53,6 +53,8 @@ #install_printer (* type_judgement *) pptype;; #install_printer (* judgement *) ppj;; +#install_printer (* judgement *) pp_cst_stack_t;; + (*#install_printer (* hint_db *) print_hint_db;;*) (*#install_printer (* hints_path *) pphintspath;;*) #install_printer (* goal *) ppgoal;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index fb8509c50..fccf580a5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -140,6 +140,7 @@ 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 Termops.print_constr n) +let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 19175f930..500bb5430 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -65,6 +65,6 @@ val evar_conv_x : transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state -> env -> evar_map -> - conv_pb -> state * constr Cst_stack.t -> state * constr Cst_stack.t -> + conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> Evarsolve.unification_result (**/**) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 74f14aa14..de043aef2 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -141,12 +141,12 @@ module Cst_stack = struct - 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 'a t = ('a * 'a list * (int * 'a array) list) list + type t = (constr * constr list * (int * constr array) list) list let empty = [] let sanity x y = - assert (Constr.equal x y) + assert(Term.eq_constr x y) let drop_useless = function | _ :: ((_,_,[])::_ as q) -> q @@ -158,9 +158,9 @@ module Cst_stack = struct | (c,params,((i,t)::q)) when i = pred (Array.length t) -> let () = sanity h t.(i) in (c, params, q) | (c,params,(i,t)::q) -> - let () = sanity h t.(i) in (c, params, (succ i,t)::q) - in - drop_useless (List.map append2cst cst_l) + let () = sanity h t.(i) in (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)) @@ -202,10 +202,10 @@ sig val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array * 'a Cst_stack.t + | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection - | Fix of fixpoint * 'a t * 'a Cst_stack.t - | Cst of pconstant * int * int list * 'a t * 'a Cst_stack.t + | Fix of fixpoint * 'a t * Cst_stack.t + | Cst of pconstant * int * int list * 'a t * Cst_stack.t | Shift of int | Update of 'a and 'a t = 'a member list @@ -230,7 +230,7 @@ sig val args_size : 'a t -> int val tail : int -> 'a t -> 'a t val nth : 'a t -> int -> 'a - val best_state : constr * constr t -> constr Cst_stack.t -> constr * constr t + val best_state : constr * constr t -> Cst_stack.t -> constr * constr t val zip : ?refold:bool -> constr * constr t -> constr end = struct @@ -251,10 +251,10 @@ struct type 'a member = | App of 'a app_node - | Case of Term.case_info * 'a * 'a array * 'a Cst_stack.t + | Case of Term.case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection - | Fix of fixpoint * 'a t * 'a Cst_stack.t - | Cst of pconstant * int * int list * 'a t * 'a Cst_stack.t + | Fix of fixpoint * 'a t * Cst_stack.t + | Cst of pconstant * int * int list * 'a t * Cst_stack.t | Shift of int | Update of 'a and 'a t = 'a member list @@ -590,9 +590,9 @@ let apply_subst recfun env cst_l t stack = aux (h::env) (Cst_stack.add_param h cst_l) c stacktl | _ -> recfun cst_l (substl env t, stack) in aux env cst_l t stack - + let stacklam recfun env t stack = -apply_subst (fun _ -> recfun) env Cst_stack.empty t stack + apply_subst (fun _ -> recfun) env Cst_stack.empty t stack let beta_applist (c,l) = stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty) @@ -784,7 +784,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = | Proj (p, c) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST p) -> (match (lookup_constant p env).Declarations.const_proj with | None -> assert false - | Some pb -> whrec cst_l (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) + | Some pb -> whrec Cst_stack.empty(* cst_l *) (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) :: stack)) | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> apply_subst whrec [b] cst_l c stack @@ -1385,7 +1385,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in if isConstruct t_o then if Closure.is_transparent_constant ts p then - whrec csts_o (Stack.nth stack_o (n+m), stack'') + whrec Cst_stack.empty (* csts_o *) (Stack.nth stack_o (n+m), stack'') else (* Won't unfold *) (whd_betaiota_state sigma (t_o, stack_o@stack'),csts') else s,csts' |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 548517dbf..2ab19c70c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -34,14 +34,14 @@ end cst applied to params must convertible to term of the state applied to args *) module Cst_stack : sig - type 'a t - val empty : 'a t - val add_param : constr -> constr t -> constr t - val add_args : 'a array -> 'a t -> 'a t - val add_cst : 'a -> 'a t -> 'a t - val best_cst : 'a t -> ('a * 'a list) option - val best_replace : constr -> constr t -> constr -> constr - val pr : constr t -> Pp.std_ppcmds + 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 : constr -> t -> constr -> constr + val pr : t -> Pp.std_ppcmds end @@ -52,11 +52,11 @@ module Stack : sig type 'a member = | App of 'a app_node - | Case of case_info * 'a * 'a array * 'a Cst_stack.t + | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection - | Fix of fixpoint * 'a t * 'a Cst_stack.t + | Fix of fixpoint * 'a t * Cst_stack.t | Cst of pconstant * int (** current foccussed arg *) * int list (** remaining args *) - * 'a t * 'a Cst_stack.t + * 'a t * Cst_stack.t | Shift of int | Update of 'a and 'a t = 'a member list @@ -92,7 +92,7 @@ module Stack : sig val tail : int -> 'a t -> 'a t val nth : 'a t -> int -> 'a - val best_state : constr * constr t -> constr Cst_stack.t -> constr * constr t + val best_state : constr * constr t -> Cst_stack.t -> constr * constr t val zip : ?refold:bool -> constr * constr t -> constr end @@ -130,8 +130,8 @@ val stack_reduction_of_reduction : i*) val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a -val whd_state_gen : ?csts:constr Cst_stack.t -> bool -> Closure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> state -> state * constr Cst_stack.t +val whd_state_gen : ?csts:Cst_stack.t -> bool -> Closure.RedFlags.reds -> + Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t val iterate_whd_gen : bool -> Closure.RedFlags.reds -> Environ.env -> Evd.evar_map -> Term.constr -> Term.constr @@ -277,8 +277,8 @@ val head_unfold_under_prod : transparent_state -> reduction_function (** {6 Heuristic for Conversion with Evar } *) val whd_betaiota_deltazeta_for_iota_state : - transparent_state -> Environ.env -> Evd.evar_map -> constr Cst_stack.t -> state -> - state * constr Cst_stack.t + transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state -> + state * Cst_stack.t (** {6 Meta-related reduction functions } *) val meta_instance : evar_map -> constr freelisted -> constr |