From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/reductionops.ml | 1676 +++++++++++++++++++++++++++++++-------------- 1 file changed, 1160 insertions(+), 516 deletions(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7c348d97..a23963ab 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,107 +1,572 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Dispose + | ReqGlobal _, _ as o -> Substitute o + + let subst (subst, (_, (r,o as orig))) = + ReqLocal, + let r' = fst (subst_global subst r) in if r==r' then orig else (r',o) + + let discharge = function + | _,(ReqGlobal (ConstRef c, req), (_, b)) -> + let c' = pop_con c in + let vars, _subst, _ctx = Lib.section_segment_of_constant c in + let extra = List.length vars in + let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in + let recargs' = List.map ((+) extra) b.b_recargs in + let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in + Some (ReqGlobal (ConstRef c', req), (ConstRef c', b')) + | _ -> None + + let rebuild = function + | req, (ConstRef c, _ as x) -> req, x + | _ -> assert false + + let inRedBehaviour = declare_object { + (default_object "REDUCTIONBEHAVIOUR") with + load_function = load; + cache_function = cache; + classify_function = classify; + subst_function = subst; + discharge_function = discharge; + rebuild_function = rebuild; + } + + let set local r (recargs, nargs, flags as req) = + let nargs = if List.mem `ReductionNeverUnfold flags then max_int else nargs in + let behaviour = { + b_nargs = nargs; b_recargs = recargs; + b_dont_expose_case = List.mem `ReductionDontExposeCase flags } in + let req = if local then ReqLocal else ReqGlobal (r, req) in + Lib.add_anonymous_leaf (inRedBehaviour (req, (r, behaviour))) + ;; + + let get r = + try + let b = Refmap.find r !table in + let flags = + if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold] + else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in + Some (b.b_recargs, (if Int.equal b.b_nargs max_int then -1 else b.b_nargs), flags) + with Not_found -> None + + let print ref = + let open Pp in + let pr_global = Nametab.pr_global_env Id.Set.empty in + match get ref with + | None -> mt () + | Some (recargs, nargs, flags) -> + let never = List.mem `ReductionNeverUnfold flags in + let nomatch = List.mem `ReductionDontExposeCase flags in + let pp_nomatch = spc() ++ if nomatch then + str "but avoid exposing match constructs" else str"" in + let pp_recargs = spc() ++ str "when the " ++ + pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (String.plural (List.length recargs) " argument") ++ + str (String.plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++ + str " to a constructor" in + let pp_nargs = + spc() ++ str "when applied to " ++ int nargs ++ + str (String.plural nargs " argument") in + hov 2 (str "The reduction tactics " ++ + match recargs, nargs, never with + | _,_, true -> str "never unfold " ++ pr_global ref + | [], 0, _ -> str "always unfold " ++ pr_global ref + | _::_, n, _ when n < 0 -> + str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch + | _::_, n, _ when n > List.fold_left max 0 recargs -> + str "unfold " ++ pr_global ref ++ pp_recargs ++ + str " and" ++ pp_nargs ++ pp_nomatch + | _::_, _, _ -> + str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch + | [], n, _ when n > 0 -> + str "unfold " ++ pr_global ref ++ pp_nargs ++ pp_nomatch + | _ -> str "unfold " ++ pr_global ref ++ pp_nomatch ) +end + +(** Machinery about stack of unfolded constants *) +module Cst_stack = struct +(** 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 sanity x y = + assert(Term.eq_constr x y) + + 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) -> + 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 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 t = match best_cst t with + | Some (c, _) when Term.isConst c -> Some (fst (Term.destConst c)) + | _ -> None + + (** [best_replace d cst_l c] makes the best replacement for [d] + by [cst_l] in [c] *) + let best_replace 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 + (reconstruct_head d args) + (applist (cst, List.rev params)) + t) cst_l c + + let pr l = + let open Pp in + let p_c = Termops.print_constr in + 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 + type 'a app_node + val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds + + type cst_member = + | Cst_const of pconstant + | Cst_proj of projection + + type 'a member = + | App of 'a app_node + | Case of case_info * 'a * 'a array * Cst_stack.t + | Proj of int * int * projection * Cst_stack.t + | Fix of fixpoint * 'a t * Cst_stack.t + | Cst of cst_member * int * int list * 'a t * Cst_stack.t + | Shift of int + | Update of 'a + and 'a t = 'a member list + val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val empty : 'a t + val is_empty : 'a t -> bool + val append_app : 'a array -> 'a t -> 'a t + val decomp : 'a t -> ('a * 'a t) option + val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + val equal : ('a * int -> 'a * int -> bool) -> (fixpoint * int -> fixpoint * int -> bool) + -> 'a t -> 'a t -> (int * int) option + val compare_shape : 'a t -> 'a t -> bool + val map : (constr -> constr) -> constr t -> constr t + val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> + constr t -> constr t -> 'a * int * int + val append_app_list : 'a list -> 'a t -> 'a t + 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 : constr * constr t -> Cst_stack.t -> constr * constr t + val zip : ?refold:bool -> constr * constr t -> constr +end = +struct + 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 + + type 'a member = + | App of 'a app_node + | Case of Term.case_info * 'a * 'a array * Cst_stack.t + | Proj of int * int * projection * Cst_stack.t + | Fix of fixpoint * 'a t * Cst_stack.t + | Cst of cst_member * int * int list * 'a t * Cst_stack.t + | Shift of int + | Update of 'a + and 'a t = 'a member list + + 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 (n,m,p,cst) -> + str "ZProj(" ++ int n ++ pr_comma () ++ int m ++ + pr_comma () ++ pr_con (Projection.constant p) ++ str ")" + | Fix (f,args,cst) -> + str "ZFix(" ++ Termops.pr_fix Termops.print_constr f + ++ 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 ")" + | Shift i -> str "ZShift(" ++ int i ++ str ")" + | Update t -> str "ZUpdate(" ++ pr_c t ++ 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.print c + else str"(" ++ Constant.print c ++ str ", " ++ + Univ.Instance.pr Univ.Level.pr u ++ str")" + | Cst_proj p -> + str".(" ++ Constant.print (Projection.constant p) ++ str")" + + let empty = [] + let is_empty = CList.is_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 lft1 y lft2 = + 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 -> + Constant.equal (Projection.constant p1) (Projection.constant p2) + | _, _ -> false + in + let rec equal_rec sk1 lft1 sk2 lft2 = + match sk1,sk2 with + | [],[] -> Some (lft1,lft2) + | (Update _ :: _, _ | _, Update _ :: _) -> assert false + | Shift k :: s1, _ -> equal_rec s1 (lft1+k) sk2 lft2 + | _, Shift k :: s2 -> equal_rec sk1 lft1 s2 (lft2+k) + | App a1 :: s1, App a2 :: s2 -> + let t1,s1' = decomp_node_last a1 s1 in + let t2,s2' = decomp_node_last a2 s2 in + if f (t1,lft1) (t2,lft2) then equal_rec s1' lft1 s2' lft2 else None + | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> + if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2 + then equal_rec s1 lft1 s2 lft2 + else None + | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> + if Int.equal n1 n2 && Int.equal m1 m2 + && Constant.equal (Projection.constant p) (Projection.constant p2) + then equal_rec s1 lft1 s2 lft2 + else None + | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> + if f_fix (f1,lft1) (f2,lft2) then + match equal_rec (List.rev s1) lft1 (List.rev s2) lft2 with + | None -> None + | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' + else None + | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' -> + if equal_cst_member c1 lft1 c2 lft2 then + match equal_rec (List.rev params1) lft1 (List.rev params2) lft2 with + | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' + | None -> None + else None + | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> None + in equal_rec (List.rev sk1) 0 (List.rev sk2) 0 + + let compare_shape stk1 stk2 = + let rec compare_rec bal stk1 stk2 = + match (stk1,stk2) with + ([],[]) -> Int.equal bal 0 + | ((Update _|Shift _)::s1, _) -> compare_rec bal s1 stk2 + | (_, (Update _|Shift _)::s2) -> compare_rec bal stk1 s2 + | (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) -> + Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 + | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> + Int.equal bal 0 && compare_rec 0 s1 s2 + | (Fix(_,a1,_)::s1, Fix(_,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 + | (_,_) -> false in + compare_rec 0 stk1 stk2 + + let fold2 f o sk1 sk2 = + let rec aux o lft1 sk1 lft2 sk2 = + let fold_array = + Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y)) + in + match sk1,sk2 with + | [], [] -> o,lft1,lft2 + | Shift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2 + | _, Shift n :: q2 -> aux o lft1 sk1 (lft2+n) q2 + | App n1 :: q1, App n2 :: q2 -> + let t1,l1 = decomp_node_last n1 q1 in + let t2,l2 = decomp_node_last n2 q2 in + aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) + lft1 l1 lft2 l2 + | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 -> + aux (fold_array + (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) + a1 a2) lft1 q1 lft2 q2 + | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 -> + aux o lft1 q1 lft2 q2 + | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 -> + let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2) + lft1 (List.rev s1) lft2 (List.rev s2) in + aux o' lft1' q1 lft2' q2 + | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 -> + let (o',lft1',lft2') = + aux o lft1 (List.rev params1) lft2 (List.rev params2) + in aux o' lft1' q1 lft2' q2 + | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> + raise (Invalid_argument "Reductionops.Stack.fold2") + in aux o 0 (List.rev sk1) 0 (List.rev sk2) + + let rec map f x = List.map (function + | Update _ -> assert false + | (Proj (_,_,_,_) | Shift _) 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) + ) x + + 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 + | Shift(_)::s -> args_size s + | Update(_)::s -> args_size s + | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0 + + let strip_app s = + let rec aux out = function + | ( App _ | Shift _ 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 + | Shift k as e :: s -> aux n (e :: out) s + | 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 not_purely_applicative args = + List.exists (function (Fix _ | Case _ | Proj _ | Cst _) -> true | _ -> 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 + | App (i,a,j) :: s -> + let (k,(args',s')) = aux s in + let a' = Array.map (Vars.lift k) (Array.sub a i (j - i + 1)) in + k,(Array.fold_right (fun x y -> x::y) a' args', s') + | Shift n :: s -> + let (k,(args',s')) = aux s in (k+n,(args', s')) + | s -> (0,([],s)) in + let (lft,(out,s')) = aux s in + let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in + Option.init init out + + let assign s p c = + match strip_n_app p s with + | Some (pre,_,sk) -> pre @ (App (0,[|c|],0)::sk) + | None -> assert false + + let tail n0 s0 = + let rec aux lft n s = + let out s = if Int.equal lft 0 then s else Shift lft :: s in + if Int.equal n 0 then out s else + match s with + | App (i,a,j) :: s -> + let nb = j - i + 1 in + if n >= nb then + aux lft (n - nb) s + else + let p = i+n in + if j >= p then App(p,a,j)::s else s + | Shift k :: s' -> aux (lft+k) n s' + | _ -> raise (Invalid_argument "Reductionops.Stack.tail") + in aux 0 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 (_,sk as s) l = + let rec aux sk def = function + |(cst, params, []) -> (cst, append_app_list (List.rev params) sk) + |(cst, params, (i,t)::q) -> match decomp sk with + | Some (el,sk') when Constr.equal el t.(i) -> + 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,u), sk + | Cst_proj p -> + match decomp sk with + | Some (hd, sk) -> mkProj (p, hd), sk + | None -> assert false + + let rec zip ?(refold=false) = function + | f, [] -> f + | f, (App (i,a,j) :: s) -> + let a' = if Int.equal i 0 && Int.equal j (Array.length a - 1) + then a + else Array.sub a i (j - i + 1) in + zip ~refold (mkApp (f, a'), s) + | f, (Case (ci,rt,br,cst_l)::s) when refold -> + zip ~refold (best_state (mkCase (ci,rt,f,br), s) cst_l) + | f, (Case (ci,rt,br,_)::s) -> zip ~refold (mkCase (ci,rt,f,br), s) + | f, (Fix (fix,st,cst_l)::s) when refold -> + zip ~refold (best_state (mkFix fix, st @ (append_app [|f|] s)) cst_l) + | f, (Fix (fix,st,_)::s) -> zip ~refold + (mkFix fix, st @ (append_app [|f|] s)) + | f, (Cst (cst,_,_,params,cst_l)::s) when refold -> + zip ~refold (best_state (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) + | f, (Cst (cst,_,_,params,_)::s) -> + zip ~refold (constr_of_cst_member cst (params @ (append_app [|f|] s))) + | f, (Shift n::s) -> zip ~refold (lift n f, s) + | f, (Proj (n,m,p,cst_l)::s) when refold -> + zip ~refold (best_state (mkProj (p,f),s) cst_l) + | f, (Proj (n,m,p,_)::s) -> zip ~refold (mkProj (p,f),s) + | _, (Update _::_) -> assert false +end + +(** The type of (machine) states (= lambda-bar-calculus' cuts) *) +type state = constr * constr Stack.t type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr +type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list @@ -114,6 +579,10 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state +let pr_state (tm,sk) = + let open Pp in + h 0 (Termops.print_constr tm ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr sk) + (*************************************) (*** Reduction Functions Operators ***) (*************************************) @@ -122,26 +591,10 @@ let safe_evar_value sigma ev = try Some (Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None -let rec whd_app_state sigma (x, stack as s) = - match kind_of_term x with - | App (f,cl) -> whd_app_state sigma (f, append_stack cl stack) - | Cast (c,_,_) -> whd_app_state sigma (c, stack) - | Evar ev -> - (match safe_evar_value sigma ev with - Some c -> whd_app_state sigma (c,stack) - | _ -> s) - | _ -> s - let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) with Not_found -> None -let appterm_of_stack (f,s) = (f,list_of_stack s) - -let whd_stack sigma x = - appterm_of_stack (whd_app_state sigma (x, empty_stack)) -let whd_castapp_stack = whd_stack - let strong whdfun env sigma t = let rec strongrec env t = map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in @@ -161,70 +614,39 @@ let rec strong_prodspine redfun sigma c = (*** Reduction using bindingss ***) (*************************************) -(* This signature is very similar to Closure.RedFlagsSig except there - is eta but no per-constant unfolding *) - -module type RedFlagsSig = sig - type flags - type flag - val fbeta : flag - val fdelta : flag - val feta : flag - val fiota : flag - val fzeta : flag - val mkflags : flag list -> flags - val red_beta : flags -> bool - val red_delta : flags -> bool - val red_eta : flags -> bool - val red_iota : flags -> bool - val red_zeta : flags -> bool -end - -(* Compact Implementation *) -module RedFlags = (struct - type flag = int - type flags = int - let fbeta = 1 - let fdelta = 2 - let feta = 8 - let fiota = 16 - let fzeta = 32 - let mkflags = List.fold_left (lor) 0 - let red_beta f = f land fbeta <> 0 - let red_delta f = f land fdelta <> 0 - let red_eta f = f land feta <> 0 - let red_iota f = f land fiota <> 0 - let red_zeta f = f land fzeta <> 0 -end : RedFlagsSig) - -open RedFlags - (* Local *) -let beta = mkflags [fbeta] -let eta = mkflags [feta] -let zeta = mkflags [fzeta] -let betaiota = mkflags [fiota; fbeta] -let betaiotazeta = mkflags [fiota; fbeta;fzeta] +let nored = Closure.RedFlags.no_red +let beta = Closure.beta +let eta = Closure.RedFlags.mkflags [Closure.RedFlags.fETA] +let zeta = Closure.RedFlags.mkflags [Closure.RedFlags.fZETA] +let betaiota = Closure.betaiota +let betaiotazeta = Closure.betaiotazeta (* Contextual *) -let delta = mkflags [fdelta] -let betadelta = mkflags [fbeta;fdelta;fzeta] -let betadeltaeta = mkflags [fbeta;fdelta;fzeta;feta] -let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fiota] -let betadeltaiota_nolet = mkflags [fbeta;fdelta;fiota] -let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fiota;feta] -let betaetalet = mkflags [fbeta;feta;fzeta] -let betalet = mkflags [fbeta;fzeta] +let delta = Closure.RedFlags.mkflags [Closure.RedFlags.fDELTA] +let betalet = Closure.RedFlags.mkflags [Closure.RedFlags.fBETA;Closure.RedFlags.fZETA] +let betaetalet = Closure.RedFlags.red_add betalet Closure.RedFlags.fETA +let betadelta = Closure.RedFlags.red_add betalet Closure.RedFlags.fDELTA +let betadeltaeta = Closure.RedFlags.red_add betadelta Closure.RedFlags.fETA +let betadeltaiota = Closure.RedFlags.red_add betadelta Closure.RedFlags.fIOTA +let betadeltaiota_nolet = Closure.betadeltaiotanolet +let betadeltaiotaeta = Closure.RedFlags.red_add betadeltaiota Closure.RedFlags.fETA (* Beta Reduction tools *) -let rec stacklam recfun env t stack = - match (decomp_stack stack,kind_of_term t) with - | Some (h,stacktl), Lambda (_,_,c) -> stacklam recfun (h::env) c stacktl - | _ -> recfun (substl env t, stack) +let apply_subst recfun env cst_l t stack = + let rec aux env cst_l t stack = + match (Stack.decomp stack,kind_of_term t) with + | Some (h,stacktl), Lambda (_,_,c) -> + 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 let beta_applist (c,l) = - stacklam app_stack [] c (append_stack_list l empty_stack) + stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty) (* Iota reduction tools *) @@ -239,16 +661,64 @@ let reducible_mind_case c = match kind_of_term c with | Construct _ | CoFix _ -> true | _ -> false -let contract_cofix (bodynum,(types,names,bodies as typedbodies)) = +(** @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 magicaly_constant_of_fixbody env reference bd = function + | Name.Anonymous -> bd + | Name.Name id -> + try + let (cst_mod,cst_sect,_) = Constant.repr3 reference in + let cst = Constant.make3 cst_mod cst_sect (Label.of_id id) in + let (cst, u), ctx = Universes.fresh_constant_instance env cst in + match constant_opt_value_in env (cst,u) with + | None -> bd + | Some t -> + let b, csts = Universes.eq_constr_universes t bd in + let subst = Universes.Constraints.fold (fun (l,d,r) acc -> + Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) + csts Univ.LMap.empty + in + let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in + if b then mkConstU (cst,inst) else bd + with + | Not_found -> bd + +let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in - let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in - substl (list_tabulate make_Fi nbodies) bodies.(bodynum) + let make_Fi j = + let ind = nbodies-j-1 in + if 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 -> magicaly_constant_of_fixbody e r bd names.(ind) 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 cst_l cofix sk = + let raw_answer = contract_cofix ~env ?reference:(Cst_stack.reference cst_l) cofix in + apply_subst + (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkCoFix cofix) cst_l t,sk')) + [] Cst_stack.empty raw_answer sk let reduce_mind_case mia = match kind_of_term mia.mconstr with - | Construct (ind_sp,i) -> + | Construct ((ind_sp,i),u) -> (* let ncargs = (fst mia.mci).(i-1) in*) - let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in + let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in applist (mia.mlf.(i-1),real_cargs) | CoFix cofix -> let cofix_def = contract_cofix cofix in @@ -258,164 +728,370 @@ let reduce_mind_case 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 ((recindices,bodynum),(types,names,bodies as typedbodies)) = - let nbodies = Array.length recindices in - let make_Fi j = mkFix ((recindices,nbodies-j-1),typedbodies) in - substl (list_tabulate make_Fi nbodies) bodies.(bodynum) +let contract_fix ?env ?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 -> magicaly_constant_of_fixbody e r bd names.(ind) 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 cst_l fix sk = + let raw_answer = contract_fix ~env ?reference:(Cst_stack.reference cst_l) fix in + apply_subst + (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkFix fix) cst_l t,sk')) + [] Cst_stack.empty raw_answer sk let fix_recarg ((recindices,bodynum),_) stack = - assert (0 <= bodynum & bodynum < Array.length recindices); + assert (0 <= bodynum && bodynum < Array.length recindices); let recargnum = Array.get recindices bodynum in try - Some (recargnum, stack_nth stack recargnum) + Some (recargnum, Stack.nth stack recargnum) with Not_found -> None -type fix_reduction_result = NotReducible | Reduced of state +(** Generic reduction function with environment -let reduce_fix whdfun sigma fix stack = - match fix_recarg fix stack with - | None -> NotReducible - | Some (recargnum,recarg) -> - let (recarg'hd,_ as recarg') = whdfun sigma (recarg, empty_stack) in - let stack' = stack_assign stack recargnum (app_stack recarg') in - (match kind_of_term recarg'hd with - | Construct _ -> Reduced (contract_fix fix, stack') - | _ -> NotReducible) + Here is where unfolded constant are stored in order to be + eventualy refolded. -(* Generic reduction function *) + If tactic_mode is true, it uses ReductionBehaviour, prefers + refold constant instead of value and tries to infer constants + fix and cofix came from. -(* Y avait un commentaire pour whd_betadeltaiota : - - NB : Cette fonction alloue peu c'est l'appel - ``let (c,cargs) = whfun (recarg, empty_stack)'' - ------------------- - qui coute cher *) + It substitutes fix and cofix by the constant they come from in + contract_* in any case . +*) -let rec whd_state_gen flags ts env sigma = - let rec whrec (x, stack as s) = +let debug_RAKAM = ref (false) +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = + "Print states of the Reductionops abstract machine"; + Goptions.optkey = ["Debug";"RAKAM"]; + Goptions.optread = (fun () -> !debug_RAKAM); + Goptions.optwrite = (fun a -> debug_RAKAM:=a); +} + +let equal_stacks (x, l) (y, l') = + let f_equal (x,lft1) (y,lft2) = Constr.equal (Vars.lift lft1 x) (Vars.lift lft2 y) in + let eq_fix (a,b) (c,d) = f_equal (Constr.mkFix a, b) (Constr.mkFix c, d) in + match Stack.equal f_equal eq_fix l l' with + | None -> false + | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) + +let rec whd_state_gen ?csts tactic_mode flags env sigma = + let rec whrec cst_l (x, stack as s) = + let () = if !debug_RAKAM then + let open Pp in + pp (h 0 (str "<<" ++ Termops.print_constr x ++ + str "|" ++ cut () ++ Cst_stack.pr cst_l ++ + str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++ + str ">>") ++ fnl ()) + in + let fold () = + let () = if !debug_RAKAM then + let open Pp in pp (str "<><><><><>" ++ fnl ()) in + if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l) + in match kind_of_term x with - | Rel n when red_delta flags -> - (match lookup_rel n env with - | (_,Some body,_) -> whrec (lift n body, stack) - | _ -> s) - | Var id when red_delta flags -> - (match lookup_named id env with - | (_,Some body,_) -> whrec (body, stack) - | _ -> s) - | Evar ev -> - (match safe_evar_value sigma ev with - | Some body -> whrec (body, stack) - | None -> s) - | Meta ev -> - (match safe_meta_value sigma ev with - | Some body -> whrec (body, stack) - | None -> s) - | Const const when is_transparent_constant ts const -> - (match constant_opt_value env const with - | Some body -> whrec (body, stack) - | None -> s) - | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack - | Cast (c,_,_) -> whrec (c, stack) - | App (f,cl) -> whrec (f, append_stack cl stack) - | Lambda (na,t,c) -> - (match decomp_stack stack with - | Some (a,m) when red_beta flags -> stacklam whrec [a] c m - | None when red_eta flags -> - let env' = push_rel (na,None,t) env in - let whrec' = whd_state_gen flags ts env' sigma in - (match kind_of_term (app_stack (whrec' (c, empty_stack))) with - | App (f,cl) -> - let napp = Array.length cl in - if napp > 0 then - let x', l' = whrec' (array_last cl, empty_stack) in - match kind_of_term x', decomp_stack l' with - | Rel 1, None -> - let lc = Array.sub cl 0 (napp-1) in - let u = if napp=1 then f else appvect (f,lc) in - if noccurn 1 u then (pop u,empty_stack) else s - | _ -> s - else s - | _ -> s) - | _ -> s) - - | Case (ci,p,d,lf) when red_iota flags -> - let (c,cargs) = whrec (d, empty_stack) in - if reducible_mind_case c then - whrec (reduce_mind_case - {mP=p; mconstr=c; mcargs=list_of_stack cargs; - mci=ci; mlf=lf}, stack) - else - (mkCase (ci, p, app_stack (c,cargs), lf), stack) - - | Fix fix when red_iota flags -> - (match reduce_fix (fun _ -> whrec) sigma fix stack with - | Reduced s' -> whrec s' - | NotReducible -> s) - - | x -> s + | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA -> + (match lookup_rel n env with + | (_,Some body,_) -> whrec Cst_stack.empty (lift n body, stack) + | _ -> fold ()) + | Var id when Closure.RedFlags.red_set flags (Closure.RedFlags.fVAR id) -> + (match lookup_named id env with + | (_,Some body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack) + | _ -> fold ()) + | Evar ev -> + (match safe_evar_value sigma ev with + | Some body -> whrec cst_l (body, stack) + | None -> fold ()) + | Meta ev -> + (match safe_meta_value sigma ev with + | Some body -> whrec cst_l (body, stack) + | None -> fold ()) + | Const (c,u as const) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST c) -> + (match constant_opt_value_in env const with + | None -> fold () + | Some body -> + if not tactic_mode + then whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) + else (* Looks for ReductionBehaviour *) + match ReductionBehaviour.get (Globnames.ConstRef c) with + | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) + | Some (recargs, nargs, flags) -> + if (List.mem `ReductionNeverUnfold flags + || (nargs > 0 && Stack.args_size stack < nargs)) + then fold () + else (* maybe unfolds *) + if List.mem `ReductionDontExposeCase flags then + 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 + if equal_stacks (x, app_sk) (tm', sk') || Stack.will_expose_iota sk' + then fold () + else whrec cst_l' (tm', sk' @ sk) + else 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 const,curr,remains,bef,cst_l)::s') + ) + | Proj (p, c) when Closure.RedFlags.red_projection flags p -> + (let pb = lookup_projection p env in + let kn = Projection.constant p in + let npars = pb.Declarations.proj_npars + and arg = pb.Declarations.proj_arg in + if not tactic_mode then + let stack' = (c, Stack.Proj (npars, arg, p, Cst_stack.empty (*cst_l*)) :: stack) in + whrec Cst_stack.empty stack' + else match ReductionBehaviour.get (Globnames.ConstRef kn) with + | None -> + let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in + let stack'', csts = whrec Cst_stack.empty stack' in + if equal_stacks stack' stack'' then fold () + else stack'', csts + | Some (recargs, nargs, flags) -> + if (List.mem `ReductionNeverUnfold flags + || (nargs > 0 && Stack.args_size stack < (nargs - (npars + 1)))) + then fold () + else + 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 (npars, arg, 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')) + + | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> + apply_subst whrec [b] cst_l c stack + | Cast (c,_,_) -> whrec cst_l (c, stack) + | App (f,cl) -> + whrec + (Cst_stack.add_args cl cst_l) + (f, Stack.append_app cl stack) + | Lambda (na,t,c) -> + (match Stack.decomp stack with + | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> + apply_subst whrec [] cst_l x stack + | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> + let env' = push_rel (na,None,t) env in + let whrec' = whd_state_gen tactic_mode flags env' sigma in + (match kind_of_term (Stack.zip ~refold:true (fst (whrec' (c, Stack.empty)))) with + | App (f,cl) -> + let napp = Array.length cl in + if napp > 0 then + let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in + match kind_of_term x', l' with + | Rel 1, [] -> + let lc = Array.sub cl 0 (napp-1) in + let u = if Int.equal napp 1 then f else appvect (f,lc) in + if noccurn 1 u then (pop u,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) -> + if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + match Stack.strip_app stack with + |args, (Stack.Case(ci, _, lf,_)::s') -> + whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') + |args, (Stack.Proj (n,m,p,_)::s') -> + whrec Cst_stack.empty (Stack.nth args (n+m), s') + |args, (Stack.Fix (f,s',cst_l)::s'') -> + let x' = Stack.zip(x,args) in + let out_sk = s' @ (Stack.append_app [|x'|] s'') in + reduce_and_refold_fix whrec env cst_l f out_sk + |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') -> + let x' = Stack.zip(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 -> + whrec (Cst_stack.add_cst (mkConstU const) cst_l) + (body, s' @ (Stack.append_app [|x'|] s''))) + | Stack.Cst_proj p -> + let pb = lookup_projection p env in + let npars = pb.Declarations.proj_npars in + let narg = pb.Declarations.proj_arg in + 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 (npars,narg,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 _|Stack.Update _|Stack.Shift _)::_ -> assert false + |_, [] -> fold () + else fold () + + | CoFix cofix -> + if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + match Stack.strip_app stack with + |args, (Stack.Case(ci, _, lf,_)::s') -> + reduce_and_refold_cofix whrec env cst_l cofix stack + |_ -> fold () + else fold () + + | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold () + | Sort _ | Ind _ | Prod _ -> fold () in - whrec + whrec (Option.default Cst_stack.empty csts) +(** reduction machine without global env and refold machinery *) let local_whd_state_gen flags sigma = let rec whrec (x, stack as s) = match kind_of_term x with - | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack - | Cast (c,_,_) -> whrec (c, stack) - | App (f,cl) -> whrec (f, append_stack cl stack) - | Lambda (_,_,c) -> - (match decomp_stack stack with - | Some (a,m) when red_beta flags -> stacklam whrec [a] c m - | None when red_eta flags -> - (match kind_of_term (app_stack (whrec (c, empty_stack))) with - | App (f,cl) -> - let napp = Array.length cl in - if napp > 0 then - let x', l' = whrec (array_last cl, empty_stack) in - match kind_of_term x', decomp_stack l' with - | Rel 1, None -> - let lc = Array.sub cl 0 (napp-1) in - let u = if napp=1 then f else appvect (f,lc) in - if noccurn 1 u then (pop u,empty_stack) else s - | _ -> s - else s - | _ -> s) - | _ -> s) - - | Case (ci,p,d,lf) when red_iota flags -> - let (c,cargs) = whrec (d, empty_stack) in - if reducible_mind_case c then - whrec (reduce_mind_case - {mP=p; mconstr=c; mcargs=list_of_stack cargs; - mci=ci; mlf=lf}, stack) - else - (mkCase (ci, p, app_stack (c,cargs), lf), stack) - - | Fix fix when red_iota flags -> - (match reduce_fix (fun _ ->whrec) sigma fix stack with - | Reduced s' -> whrec s' - | NotReducible -> s) - - | Evar ev -> - (match safe_evar_value sigma ev with - Some c -> whrec (c,stack) - | None -> s) - - | Meta ev -> - (match safe_meta_value sigma ev with - Some c -> whrec (c,stack) - | None -> s) - - | x -> s + | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA -> + stacklam whrec [b] c stack + | Cast (c,_,_) -> whrec (c, stack) + | App (f,cl) -> whrec (f, Stack.append_app cl stack) + | Lambda (_,_,c) -> + (match Stack.decomp stack with + | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA -> + stacklam whrec [a] c m + | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA -> + (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with + | App (f,cl) -> + let napp = Array.length cl in + if napp > 0 then + let x', l' = whrec (Array.last cl, Stack.empty) in + match kind_of_term x', l' with + | Rel 1, [] -> + let lc = Array.sub cl 0 (napp-1) in + let u = if Int.equal napp 1 then f else appvect (f,lc) in + if noccurn 1 u then (pop u,Stack.empty) else s + | _ -> s + else s + | _ -> s) + | _ -> s) + + | Proj (p,c) when Closure.RedFlags.red_projection flags p -> + (let pb = lookup_projection p (Global.env ()) in + whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, + p, Cst_stack.empty) + :: stack)) + + | Case (ci,p,d,lf) -> + whrec (d, Stack.Case (ci,p,lf,Cst_stack.empty) :: 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')) + + | Evar ev -> + (match safe_evar_value sigma ev with + Some c -> whrec (c,stack) + | None -> s) + + | Meta ev -> + (match safe_meta_value sigma ev with + Some c -> whrec (c,stack) + | None -> s) + + | Construct ((ind,c),u) -> + if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + match Stack.strip_app stack with + |args, (Stack.Case(ci, _, lf,_)::s') -> + whrec (lf.(c-1), (Stack.tail ci.ci_npar args) @ s') + |args, (Stack.Proj (n,m,p,_) :: s') -> + whrec (Stack.nth args (n+m), s') + |args, (Stack.Fix (f,s',cst)::s'') -> + let x' = Stack.zip(x,args) in + whrec (contract_fix f, s' @ (Stack.append_app [|x'|] s'')) + |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false + |_, [] -> s + else s + + | CoFix cofix -> + if Closure.RedFlags.red_set flags Closure.RedFlags.fIOTA then + match Stack.strip_app stack with + |args, (Stack.Case(ci, _, lf,_)::s') -> + whrec (contract_cofix cofix, stack) + |_ -> s + else s + + | x -> s in whrec +let raw_whd_state_gen flags env = + let f sigma s = fst (whd_state_gen false flags env sigma s) in + f -let stack_red_of_state_red f sigma x = - appterm_of_stack (f sigma (x, empty_stack)) +let stack_red_of_state_red f = + let f sigma x = decompose_app (Stack.zip (f sigma (x, Stack.empty))) in + f + +(* Drops the Cst_stack *) +let iterate_whd_gen refold flags env sigma s = + let rec aux t = + let (hd,sk),_ = whd_state_gen refold flags env sigma (t,Stack.empty) in + let whd_sk = Stack.map aux sk in + Stack.zip ~refold (hd,whd_sk) + in aux s let red_of_state_red f sigma x = - app_stack (f sigma (x,empty_stack)) + Stack.zip (f sigma (x,Stack.empty)) + +(* 0. No Reduction Functions *) + +let whd_nored_state = local_whd_state_gen nored +let whd_nored_stack = stack_red_of_state_red whd_nored_state +let whd_nored = red_of_state_red whd_nored_state (* 1. Beta Reduction Functions *) @@ -434,19 +1110,18 @@ let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) -let whd_delta_state e = whd_state_gen delta full_transparent_state e +let whd_delta_state e = raw_whd_state_gen delta e let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env) let whd_delta env = red_of_state_red (whd_delta_state env) -let whd_betadelta_state e = whd_state_gen betadelta full_transparent_state e +let whd_betadelta_state e = raw_whd_state_gen betadelta e let whd_betadelta_stack env = stack_red_of_state_red (whd_betadelta_state env) let whd_betadelta env = red_of_state_red (whd_betadelta_state env) -let whd_betadeltaeta_state e = - whd_state_gen betadeltaeta full_transparent_state e +let whd_betadeltaeta_state e = raw_whd_state_gen betadeltaeta e let whd_betadeltaeta_stack env = stack_red_of_state_red (whd_betadeltaeta_state env) let whd_betadeltaeta env = @@ -462,29 +1137,19 @@ let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state -let whd_betadeltaiota_state env = - whd_state_gen betadeltaiota full_transparent_state env +let whd_betadeltaiota_state env = raw_whd_state_gen betadeltaiota env let whd_betadeltaiota_stack env = stack_red_of_state_red (whd_betadeltaiota_state env) let whd_betadeltaiota env = red_of_state_red (whd_betadeltaiota_state env) -let whd_betadeltaiota_state_using ts env = - whd_state_gen betadeltaiota ts env -let whd_betadeltaiota_stack_using ts env = - stack_red_of_state_red (whd_betadeltaiota_state_using ts env) -let whd_betadeltaiota_using ts env = - red_of_state_red (whd_betadeltaiota_state_using ts env) - -let whd_betadeltaiotaeta_state env = - whd_state_gen betadeltaiotaeta full_transparent_state env +let whd_betadeltaiotaeta_state env = raw_whd_state_gen betadeltaiotaeta env let whd_betadeltaiotaeta_stack env = stack_red_of_state_red (whd_betadeltaiotaeta_state env) let whd_betadeltaiotaeta env = red_of_state_red (whd_betadeltaiotaeta_state env) -let whd_betadeltaiota_nolet_state env = - whd_state_gen betadeltaiota_nolet full_transparent_state env +let whd_betadeltaiota_nolet_state env = raw_whd_state_gen betadeltaiota_nolet env let whd_betadeltaiota_nolet_stack env = stack_red_of_state_red (whd_betadeltaiota_nolet_state env) let whd_betadeltaiota_nolet env = @@ -492,11 +1157,11 @@ let whd_betadeltaiota_nolet env = (* 4. Eta reduction Functions *) -let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack)) +let whd_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty)) (* 5. Zeta Reduction Functions *) -let whd_zeta c = app_stack (local_whd_state_gen zeta Evd.empty (c,empty_stack)) +let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty)) (****************************************************************************) (* Reduction Functions *) @@ -506,10 +1171,23 @@ let whd_zeta c = app_stack (local_whd_state_gen zeta Evd.empty (c,empty_stack)) let rec whd_evar sigma c = match kind_of_term c with | Evar ev -> - (match safe_evar_value sigma ev with + let (evk, args) = ev in + let args = Array.map (fun c -> whd_evar sigma c) args in + (match safe_evar_value sigma (evk, args) with Some c -> whd_evar sigma c | None -> c) - | Sort s -> whd_sort_variable sigma c + | Sort (Type u) -> + let u' = Evd.normalize_universe sigma u in + if u' == u then c else mkSort (Sorts.sort_of_univ u') + | Const (c', u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkConstU (c', u') + | Ind (i, u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkIndU (i, u') + | Construct (co, u) when not (Univ.Instance.is_empty u) -> + let u' = Evd.normalize_universe_instance sigma u in + if u' == u then c else mkConstructU (co, u') | _ -> c let nf_evar = @@ -520,66 +1198,19 @@ let nf_evar = a [nf_evar] here *) let clos_norm_flags flgs env sigma t = try - norm_val - (create_clos_infos ~evars:(safe_evar_value sigma) flgs env) - (inject t) - with Anomaly _ -> error "Tried to normalized ill-typed term" - -let nf_beta = clos_norm_flags Closure.beta empty_env -let nf_betaiota = clos_norm_flags Closure.betaiota empty_env + let evars ev = safe_evar_value sigma ev in + Closure.norm_val + (Closure.create_clos_infos ~evars flgs env) + (Closure.inject t) + with e when is_anomaly e -> error "Tried to normalize ill-typed term" + +let nf_beta = clos_norm_flags Closure.beta (Global.env ()) +let nf_betaiota = clos_norm_flags Closure.betaiota (Global.env ()) +let nf_betaiotazeta = clos_norm_flags Closure.betaiotazeta (Global.env ()) let nf_betadeltaiota env sigma = clos_norm_flags Closure.betadeltaiota env sigma -(* Attention reduire un beta-redexe avec un argument qui n'est pas - une variable, peut changer enormement le temps de conversion lors - du type checking : - (fun x => x + x) M -*) -let rec whd_betaiota_preserving_vm_cast env sigma t = - let rec stacklam_var subst t stack = - match (decomp_stack stack,kind_of_term t) with - | Some (h,stacktl), Lambda (_,_,c) -> - begin match kind_of_term h with - | Rel i when not (evaluable_rel i env) -> - stacklam_var (h::subst) c stacktl - | Var id when not (evaluable_named id env)-> - stacklam_var (h::subst) c stacktl - | _ -> whrec (substl subst t, stack) - end - | _ -> whrec (substl subst t, stack) - and whrec (x, stack as s) = - match kind_of_term x with - | Evar ev -> - (match safe_evar_value sigma ev with - | Some body -> whrec (body, stack) - | None -> s) - | Cast (c,VMcast,t) -> - let c = app_stack (whrec (c,empty_stack)) in - let t = app_stack (whrec (t,empty_stack)) in - (mkCast(c,VMcast,t),stack) - | Cast (c,DEFAULTcast,_) -> - whrec (c, stack) - | App (f,cl) -> whrec (f, append_stack cl stack) - | Lambda (na,t,c) -> - (match decomp_stack stack with - | Some (a,m) -> stacklam_var [a] c m - | _ -> s) - | Case (ci,p,d,lf) -> - let (c,cargs) = whrec (d, empty_stack) in - if reducible_mind_case c then - whrec (reduce_mind_case - {mP=p; mconstr=c; mcargs=list_of_stack cargs; - mci=ci; mlf=lf}, stack) - else - (mkCase (ci, p, app_stack (c,cargs), lf), stack) - | x -> s - in - app_stack (whrec (t,empty_stack)) - -let nf_betaiota_preserving_vm_cast = - strong whd_betaiota_preserving_vm_cast - (********************************************************************) (* Conversion *) (********************************************************************) @@ -591,40 +1222,88 @@ let fakey = Profile.declare_profile "fhnf_apply";; let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; *) -let is_transparent k = - Conv_oracle.get_strategy k <> Conv_oracle.Opaque +let is_transparent e k = + match Conv_oracle.get_strategy (Environ.oracle e) k with + | Conv_oracle.Opaque -> false + | _ -> true (* Conversion utility functions *) type conversion_test = constraints -> constraints -let pb_is_equal pb = pb = CONV +let pb_is_equal pb = pb == Reduction.CONV let pb_equal = function - | CUMUL -> CONV - | CONV -> CONV - -let sort_cmp = sort_cmp + | Reduction.CUMUL -> Reduction.CONV + | Reduction.CONV -> Reduction.CONV -let test_conversion (f: ?l2r:bool-> ?evars:'a->'b) env sigma x y = - try let _ = - f ~evars:(safe_evar_value sigma) env x y in true - with NotConvertible -> false - | Anomaly _ -> error "Conversion test raised an anomaly" - -let is_conv env sigma = test_conversion Reduction.conv env sigma -let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma -let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq +let sort_cmp cv_pb s1 s2 u = + Reduction.check_sort_cmp_universes cv_pb s1 s2 u let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = - try let _ = f ~evars:(safe_evar_value sigma) reds env x y in true - with NotConvertible -> false - | Anomaly _ -> error "Conversion test raised an anomaly" - -let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv reds env sigma -let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq reds env sigma -let is_trans_fconv = function | CONV -> is_trans_conv | CUMUL -> is_trans_conv_leq - + try + let evars ev = safe_evar_value sigma ev in + let _ = f ~evars reds env (Evd.universes sigma) x y in + true + with Reduction.NotConvertible -> false + | e when is_anomaly e -> error "Conversion test raised an anomaly" + +let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma +let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma +let is_trans_fconv = function Reduction.CONV -> is_trans_conv | Reduction.CUMUL -> is_trans_conv_leq + +let is_conv = is_trans_conv full_transparent_state +let is_conv_leq = is_trans_conv_leq full_transparent_state +let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv_leq + +let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = + let f = match pb with + | Reduction.CONV -> Reduction.trans_conv_universes + | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + in + try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true + with Reduction.NotConvertible -> false + | Univ.UniverseInconsistency _ -> false + | e when is_anomaly e -> error "Conversion test raised an anomaly" + +let sigma_compare_sorts env pb s0 s1 sigma = + match pb with + | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1 + | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1 + +let sigma_compare_instances flex i0 i1 sigma = + try Evd.set_eq_instances ~flex sigma i0 i1 + with Evd.UniversesDiffer -> raise Reduction.NotConvertible + +let sigma_univ_state = + { Reduction.compare = sigma_compare_sorts; + Reduction.compare_instances = sigma_compare_instances } + +let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = + try + let b, sigma = + let b, cstrs = + if pb == Reduction.CUMUL then + Universes.leq_constr_univs_infer (Evd.universes sigma) x y + else + Universes.eq_constr_univs_infer (Evd.universes sigma) x y + in + if b then + try true, Evd.add_universe_constraints sigma cstrs + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> false, sigma + else false, sigma + in + if b then sigma, true + else + let sigma' = + Reduction.generic_conv pb false (safe_evar_value sigma) ts + env (sigma, sigma_univ_state) x y in + sigma', true + with + | Reduction.NotConvertible -> sigma, false + | Univ.UniverseInconsistency _ -> sigma, false + | e when is_anomaly e -> error "Conversion test raised an anomaly" + (********************************************************************) (* Special-Purpose Reduction *) (********************************************************************) @@ -633,33 +1312,36 @@ let whd_meta sigma c = match kind_of_term c with | Meta p -> (try meta_value sigma p with Not_found -> c) | _ -> c +let default_plain_instance_ident = Id.of_string "H" + (* Try to replace all metas. Does not replace metas in the metas' values * Differs from (strong whd_meta). *) let plain_instance s c = let rec irec n u = match kind_of_term u with - | Meta p -> (try lift n (List.assoc p s) with Not_found -> u) + | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) | App (f,l) when isCast f -> let (f,_,t) = destCast f in - let l' = Array.map (irec n) l in + let l' = CArray.Fun1.smartmap irec n l in (match kind_of_term f with | Meta p -> (* Don't flatten application nodes: this is used to extract a proof-term from a proof-tree and we want to keep the structure of the proof-tree *) - (try let g = List.assoc p s in + (try let g = Metamap.find p s in match kind_of_term g with | App _ -> - let h = id_of_string "H" in - mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l')) + let l' = CArray.Fun1.smartmap lift 1 l' in + mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) | _ -> mkApp (irec n f,l')) | Cast (m,_,_) when isMeta m -> - (try lift n (List.assoc (destMeta m) s) with Not_found -> u) + (try lift n (Metamap.find (destMeta m) s) with Not_found -> u) | _ -> map_constr_with_binders succ irec n u in - if s = [] then c else irec 0 c + if Metamap.is_empty s then c + else irec 0 c (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] has (unfortunately) different subtle side effects: @@ -708,7 +1390,7 @@ let instance sigma s c = let hnf_prod_app env sigma t n = match kind_of_term (whd_betadeltaiota env sigma t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly "hnf_prod_app: Need a product" + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") let hnf_prod_appvect env sigma t nl = Array.fold_left (hnf_prod_app env sigma) t nl @@ -719,7 +1401,7 @@ let hnf_prod_applist env sigma t nl = let hnf_lam_app env sigma t n = match kind_of_term (whd_betadeltaiota env sigma t) with | Lambda (_,_,b) -> subst1 n b - | _ -> anomaly "hnf_lam_app: Need an abstraction" + | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") let hnf_lam_appvect env sigma t nl = Array.fold_left (hnf_lam_app env sigma) t nl @@ -760,7 +1442,10 @@ let splay_prod_assum env sigma = prodec_rec (push_rel (x, Some b, t) env) (add_rel_decl (x, Some b, t) l) c | Cast (c,_,_) -> prodec_rec env l c - | _ -> l,t + | _ -> + let t' = whd_betadeltaiota env sigma t in + if Term.eq_constr t t' then l,t + else prodec_rec env l t' in prodec_rec env empty_rel_context @@ -773,7 +1458,7 @@ let splay_arity env sigma c = let sort_of_arity env sigma c = snd (splay_arity env sigma c) let splay_prod_n env sigma n = - let rec decrec env m ln c = if m = 0 then (ln,c) else + let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Prod (n,a,c0) -> decrec (push_rel (n,None,a) env) @@ -783,7 +1468,7 @@ let splay_prod_n env sigma n = decrec env n empty_rel_context let splay_lam_n env sigma n = - let rec decrec env m ln c = if m = 0 then (ln,c) else + let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Lambda (n,a,c0) -> decrec (push_rel (n,None,a) env) @@ -792,87 +1477,34 @@ let splay_lam_n env sigma n = in decrec env n empty_rel_context -exception NotASort - -let decomp_sort env sigma t = +let is_sort env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with - | Sort s -> s - | _ -> raise NotASort - -let is_sort env sigma arity = - try let _ = decomp_sort env sigma arity in true - with NotASort -> false + | Sort s -> true + | _ -> false (* reduction to head-normal-form allowing delta/zeta only in argument of case/fix (heuristic used by evar_conv) *) -let whd_betaiota_deltazeta_for_iota_state ts env sigma s = - let rec whrec s = - let (t, stack as s) = whd_betaiota_state sigma s in - match kind_of_term t with - | Case (ci,p,d,lf) -> - let (cr,crargs) = whd_betadeltaiota_stack_using ts env sigma d in - let rslt = mkCase (ci, p, applist (cr,crargs), lf) in - if reducible_mind_case cr then - whrec (rslt, stack) - else - s - | Fix fix -> - (match - reduce_fix (whd_betadeltaiota_state_using ts env) sigma fix stack - with - | Reduced s -> whrec s - | NotReducible -> s) - | _ -> s - in whrec s - -(* A reduction function like whd_betaiota but which keeps casts - * and does not reduce redexes containing existential variables. - * Used in Correctness. - * Added by JCF, 29/1/98. *) - -let whd_programs_stack env sigma = - let rec whrec (x, stack as s) = - match kind_of_term x with - | App (f,cl) -> - let n = Array.length cl - 1 in - let c = cl.(n) in - if occur_existential c then - s - else - whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack) - | LetIn (_,b,_,c) -> - if occur_existential b then - s - else - stacklam whrec [b] c stack - | Lambda (_,_,c) -> - (match decomp_stack stack with - | None -> s - | Some (a,m) -> stacklam whrec [a] c m) - | Case (ci,p,d,lf) -> - if occur_existential d then - s - else - let (c,cargs) = whrec (d, empty_stack) in - if reducible_mind_case c then - whrec (reduce_mind_case - {mP=p; mconstr=c; mcargs=list_of_stack cargs; - mci=ci; mlf=lf}, stack) - else - (mkCase (ci, p, app_stack(c,cargs), lf), stack) - | Fix fix -> - (match reduce_fix (fun _ ->whrec) sigma fix stack with - | Reduced s' -> whrec s' - | NotReducible -> s) - | _ -> s - in - whrec - -let whd_programs env sigma x = - app_stack (whd_programs_stack env sigma (x, empty_stack)) - -exception IsType +let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = + let rec whrec csts s = + let (t, stack as s),csts' = whd_state_gen ~csts false betaiota env sigma s in + match Stack.strip_app stack with + |args, (Stack.Case _ :: _ as stack') -> + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false + (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' + |args, (Stack.Fix _ :: _ as stack') -> + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false + (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts' + |args, (Stack.Proj (n,m,p,_) :: stack'') -> + let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false + (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in + if isConstruct t_o then + whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') + else s,csts' + |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' + in whrec csts s let find_conclusion env sigma = let rec decrec env c = @@ -896,74 +1528,86 @@ let meta_value evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> - instance evd - (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) - b.rebus + let metas = Metamap.bind valrec b.freemetas in + instance evd metas b.rebus | None -> mkMeta mv in valrec mv let meta_instance sigma b = - let c_sigma = - List.map - (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas) - in - if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus + let fm = b.freemetas in + if Metaset.is_empty fm then b.rebus + else + let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in + instance sigma c_sigma b.rebus let nf_meta sigma c = meta_instance sigma (mk_freelisted c) (* Instantiate metas that create beta/iota redexes *) let meta_reducible_instance evd b = - let fm = Metaset.elements b.freemetas in - let metas = List.fold_left (fun l mv -> - match (try meta_opt_fvalue evd mv with Not_found -> None) with - | Some (g,(_,s)) -> (mv,(g.rebus,s))::l - | None -> l) [] fm in + let fm = b.freemetas in + let fold mv accu = + let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in + match fvalue with + | None -> accu + | Some (g, (_, s)) -> Metamap.add mv (g.rebus, s) accu + in + let metas = Metaset.fold fold fm Metamap.empty in let rec irec u = let u = whd_betaiota Evd.empty u in match kind_of_term u with - | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) -> - let m = - try destMeta c - with e when Errors.noncritical e -> destMeta (pi1 (destCast c)) - in + | Case (ci,p,c,bl) when isMeta (strip_outer_cast c) -> + let m = destMeta (strip_outer_cast c) in (match try - let g,s = List.assoc m metas in - if isConstruct g or s <> CoerceToType then Some g else None + let g, s = Metamap.find m metas in + let is_coerce = match s with CoerceToType -> true | _ -> false in + if isConstruct g || not is_coerce then Some g else None with Not_found -> None with | Some g -> irec (mkCase (ci,p,g,bl)) | None -> mkCase (ci,irec p,c,Array.map irec bl)) - | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) -> - let m = - try destMeta f - with e when Errors.noncritical e -> destMeta (pi1 (destCast f)) - in + | App (f,l) when isMeta (strip_outer_cast f) -> + let m = destMeta (strip_outer_cast f) in (match try - let g,s = List.assoc m metas in - if isLambda g or s <> CoerceToType then Some g else None + let g, s = Metamap.find m metas in + let is_coerce = match s with CoerceToType -> true | _ -> false in + if isLambda g || not is_coerce then Some g else None with Not_found -> None with | Some g -> irec (mkApp (g,l)) | None -> mkApp (f,Array.map irec l)) | Meta m -> - (try let g,s = List.assoc m metas in if s<>CoerceToType then irec g else u + (try let g, s = Metamap.find m metas in + let is_coerce = match s with CoerceToType -> true | _ -> false in + if not is_coerce then irec g else u with Not_found -> u) + | Proj (p,c) when isMeta c || isCast c && isMeta (pi1 (destCast c)) -> + let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in + (match + try + let g, s = Metamap.find m metas in + let is_coerce = match s with CoerceToType -> true | _ -> false in + if isConstruct g || not is_coerce then Some g else None + with Not_found -> None + with + | Some g -> irec (mkProj (p,g)) + | None -> mkProj (p,c)) | _ -> map_constr irec u in - if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus + if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus + else irec b.rebus let head_unfold_under_prod ts env _ c = - let unfold cst = + let unfold (cst,u as cstu) = if Cpred.mem cst (snd ts) then - match constant_opt_value env cst with + match constant_opt_value_in env cstu with | Some c -> c - | None -> mkConst cst - else mkConst cst in + | None -> mkConstU cstu + else mkConstU cstu in let rec aux c = match kind_of_term c with | Prod (n,t,c) -> mkProd (n,aux t, aux c) -- cgit v1.2.3