diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 160 |
1 files changed, 60 insertions, 100 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index ba0502ca4..ac8846854 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -284,8 +284,6 @@ sig | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * '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 exception IncompatibleFold2 @@ -296,12 +294,12 @@ 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 * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool) - -> 'a t -> 'a t -> (int * int) option + 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 -> - constr t -> constr t -> 'a * int * int + constr t -> constr t -> 'a 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 @@ -343,8 +341,6 @@ struct | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * '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 = @@ -367,8 +363,6 @@ struct ++ 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 @@ -403,54 +397,42 @@ struct else (l.(j), sk) let equal f f_fix sk1 sk2 = - let equal_cst_member x lft1 y lft2 = + 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 + Constant.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj p1, Cst_proj p2 -> - Constant.equal (Projection.constant p1) (Projection.constant p2) + Constant.equal (Projection.constant p1) (Projection.constant p2) | _, _ -> false in - let rec equal_rec sk1 lft1 sk2 lft2 = + let rec equal_rec sk1 sk2 = 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) + | [],[] -> 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 - if f (t1,lft1) (t2,lft2) then equal_rec s1' lft1 s2' lft2 else None + 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 -> - 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 + f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 | (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 + Int.equal n1 n2 && Int.equal m1 m2 + && Constant.equal (Projection.constant p) (Projection.constant p2) + && equal_rec s1 s2 | 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 + 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' -> - 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 + equal_cst_member c1 c2 + && equal_rec (List.rev params1) (List.rev params2) + && equal_rec s1' s2' + | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> 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 - | ((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) -> @@ -466,40 +448,29 @@ struct exception IncompatibleFold2 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 + let rec aux o sk1 sk2 = 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 + | [], [] -> o | 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 + 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 -> - aux (fold_array - (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - a1 a2) lft1 q1 lft2 q2 + aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 -> - aux o lft1 q1 lft2 q2 + aux o q1 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 + 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',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 IncompatibleFold2 - in aux o 0 (List.rev sk1) 0 (List.rev sk2) + let o' = aux o (List.rev params1) (List.rev params2) in + aux o' q1 q2 + | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> + raise IncompatibleFold2 + in aux o (List.rev sk1) (List.rev sk2) let rec map f x = List.map (function - | Update _ -> assert false - | (Proj (_,_,_,_) | Shift _) 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) @@ -516,18 +487,15 @@ struct 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 + | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s let strip_n_app n s = let rec aux n out = function - | 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 @@ -552,14 +520,12 @@ struct 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 + let (args',s') = aux s in + let a' = Array.sub a i (j - i + 1) in + (Array.fold_right (fun x y -> x::y) a' args', s') + | s -> ([],s) in + let (out,s') = aux s in + let init = match s' with [] -> true | _ -> false in Option.init init out let assign s p c = @@ -568,20 +534,18 @@ struct | 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 + let rec aux n s = + if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> let nb = j - i + 1 in if n >= nb then - aux lft (n - nb) s + aux (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 + in aux n0 s0 let nth s p = match strip_n_app p s with @@ -627,11 +591,9 @@ struct 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, (Shift n::s) -> zip (lift n f, s) | f, (Proj (n,m,p,cst_l)::s) when refold -> zip (best_state sigma (mkProj (p,f),s) cst_l) | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s) - | _, (Update _::_) -> assert false in zip s @@ -868,11 +830,9 @@ let _ = Goptions.declare_bool_option { } let equal_stacks sigma (x, l) (y, l') = - let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in - let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (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 f_equal x y = eq_constr sigma x y in + let eq_fix a b = f_equal (mkFix a) (mkFix b) in + Stack.equal f_equal eq_fix l l' && f_equal x y let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in @@ -1074,7 +1034,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (arg, Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') end - |_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false + |_, (Stack.App _)::_ -> assert false |_, _ -> fold () else fold () @@ -1155,7 +1115,7 @@ let local_whd_state_gen flags sigma = |args, (Stack.Fix (f,s',cst)::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.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false + |_, (Stack.App _|Stack.Cst _)::_ -> assert false |_, _ -> s else s @@ -1292,11 +1252,11 @@ let nf_all env sigma = (* Conversion *) (********************************************************************) (* -let fkey = Profile.declare_profile "fhnf";; -let fhnf info v = Profile.profile2 fkey fhnf info v;; +let fkey = CProfile.declare_profile "fhnf";; +let fhnf info v = CProfile.profile2 fkey fhnf info v;; -let fakey = Profile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +let fakey = CProfile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; *) let is_transparent e k = @@ -1306,7 +1266,7 @@ let is_transparent e k = (* Conversion utility functions *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t let pb_is_equal pb = pb == Reduction.CONV @@ -1685,7 +1645,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = if isConstruct sigma 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' + |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts' in whrec csts s let find_conclusion env sigma = |