X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagReduction.ml;h=e26a7ec1ed29eec594186fbae3013d1f988f5a72;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=cc3cb36f8266b8edb35cf92617f61aae552c90b6;hpb=67686e04702688cc822e809e5168f765bf69d7cb;p=helm.git diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml index cc3cb36f8..e26a7ec1e 100644 --- a/helm/software/helena/src/basic_ag/bagReduction.ml +++ b/helm/software/helena/src/basic_ag/bagReduction.ml @@ -20,6 +20,8 @@ module ZO = BagOutput module ZE = BagEnvironment module ZS = BagSubstitution +IFDEF TYPE THEN + type machine = { i: int; c: Z.lenv; @@ -30,7 +32,7 @@ type whd_result = | Sort_ of int | LRef_ of P.mark * Z.term option | GRef_ of Z.entity - | Bind_ of Z.attrs * P.mark * Z.term * Z.term + | Bind_ of Z.b_attrs * P.mark * Z.term * Z.term type ho_whd_result = | Sort of int @@ -59,7 +61,7 @@ let empty_machine = {i = 0; c = Z.empty_lenv; s = []} let inc m = {m with i = succ m.i} let unwind_to_term f m t = - let map f t (a, l, b) = f (Z.Bind (a, l, b, t)) in + let map f t (y, l, b) = f (Z.Bind (y, l, b, t)) in let f mc = C.list_fold_left f map t mc in Z.contents f m.c @@ -94,55 +96,59 @@ let rec whd f c m x = get f c m i | Z.Cast (_, t) -> whd f c m t | Z.Appl (v, t) -> whd f c {m with s = v :: m.s} t - | Z.Bind (a, l, Z.Abst w, t) -> + | Z.Bind (y, l, Z.Abst w, t) -> begin match m.s with - | [] -> f m (Bind_ (a, l, w, t)) + | [] -> f m (Bind_ (y, l, w, t)) | v :: tl -> let nl = P.new_mark () in let f mc = ZS.subst (whd f c {m with c = mc; s = tl}) nl l t in - Z.push "!" f m.c a nl (Z.Abbr (Z.Cast (w, v))) + Z.push "!" f m.c y nl (Z.Abbr (Z.Cast (w, v))) end - | Z.Bind (a, l, b, t) -> + | Z.Bind (y, l, b, t) -> let nl = P.new_mark () in let f mc = ZS.subst (whd f c {m with c = mc}) nl l t in - Z.push "!" f m.c a nl b + Z.push "!" f m.c y nl b (* Interface functions ******************************************************) let rec ho_whd f c m x = (* L.warn "entering R.ho_whd"; *) let aux m = function - | Sort_ h -> f (Sort h) - | Bind_ (_, _, w, _) -> + | Sort_ h -> f (Sort h) + | Bind_ (_, _, w, _) -> let f w = f (Abst w) in unwind_to_term f m w - | LRef_ (_, Some w) -> ho_whd f c m w - | GRef_ (_, _, _, E.Abst w) -> ho_whd f c m w - | GRef_ (_, _, _, E.Abbr v) -> ho_whd f c m v - | LRef_ (_, None) -> assert false - | GRef_ (_, _, _, E.Void) -> assert false + | LRef_ (_, Some w) -> ho_whd f c m w + | GRef_ (_, _, _, E.Abst (_, w)) -> ho_whd f c m w + | GRef_ (_, _, _, E.Abbr (_, v)) -> ho_whd f c m v + | LRef_ (_, None) -> assert false + | GRef_ (_, _, _, E.Void) -> assert false in whd aux c m x let ho_whd f st c t = - if !G.ct >= level then log1 st "Now scanning" c t; +IFDEF TRACE THEN + if !G.ct >= level then log1 st "Now scanning" c t +ELSE () END; ho_whd f c empty_machine t let rec are_convertible f st a c m1 t1 m2 t2 = (* L.warn "entering R.are_convertible"; *) let rec aux m1 r1 m2 r2 = (* L.warn "entering R.are_convertible_aux"; *) +IFDEF TRACE THEN let u, t = term_of_whdr r1, term_of_whdr r2 in - if !G.ct >= level then log2 st "Now really converting" c u c t; + if !G.ct >= level then log2 st "Now really converting" c u c t +ELSE () END; match r1, r2 with - | Sort_ h1, Sort_ h2 -> - if h1 = h2 then f a else f false - | LRef_ (i1, _), LRef_ (i2, _) -> + | Sort_ k1, Sort_ k2 -> + if k1 = k2 then f a else f false + | LRef_ (i1, _), LRef_ (i2, _) -> if i1 = i2 then are_convertible_stacks f st a c m1 m2 else f false | GRef_ (_, {E.n_apix = a1}, _, E.Abst _), - GRef_ (_, {E.n_apix = a2}, _, E.Abst _) -> + GRef_ (_, {E.n_apix = a2}, _, E.Abst _) -> if a1 = a2 then are_convertible_stacks f st a c m1 m2 else f false - | GRef_ (_, {E.n_apix = a1}, _, E.Abbr v1), - GRef_ (_, {E.n_apix = a2}, _, E.Abbr v2) -> + | GRef_ (_, {E.n_apix = a1}, _, E.Abbr (_, v1)), + GRef_ (_, {E.n_apix = a2}, _, E.Abbr (_, v2)) -> if a1 = a2 then let f a = if a then f a else are_convertible f st true c m1 v1 m2 v2 @@ -151,25 +157,25 @@ let rec are_convertible f st a c m1 t1 m2 t2 = else if a1 < a2 then whd (aux m1 r1) c m2 v2 else whd (aux_rev m2 r2) c m1 v1 - | _, GRef_ (_, _, _, E.Abbr v2) -> + | _, GRef_ (_, _, _, E.Abbr (_, v2)) -> whd (aux m1 r1) c m2 v2 - | GRef_ (_, _, _, E.Abbr v1), _ -> + | GRef_ (_, _, _, E.Abbr (_, v1)), _ -> whd (aux_rev m2 r2) c m1 v1 - | Bind_ (a1, l1, w1, t1), Bind_ (a2, l2, w2, t2) -> + | Bind_ (y1, l1, w1, t1), Bind_ (_, l2, w2, t2) -> let l = P.new_mark () in let h c = let m1, m2 = inc m1, inc m2 in let f t1 = ZS.subst (are_convertible f st a c m1 t1 m2) l l2 t2 in ZS.subst f l l1 t1 in - let f r = if r then push "!" h c m1 a1 l w1 else f false in + let f r = if r then push "!" h c m1 y1 l w1 else f false in are_convertible f st a c m1 w1 m2 w2 (* we detect the AUT-QE reduction rule for type/prop inclusion *) - | Sort_ _, Bind_ (a2, l2, w2, t2) when !G.si -> + | Sort_ _, Bind_ (y2, l2, w2, t2) when !G.si -> let m1, m2 = inc m1, inc m2 in let f c = are_convertible f st a c m1 (term_of_whdr r1) m2 t2 in - push "nsi" f c m2 a2 l2 w2 - | _ -> f false + push "nsi" f c m2 y2 l2 w2 + | _ -> f false and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in let g m1 r1 = whd (aux m1 r1) c m2 t2 in if a = false then f false else whd g c m1 t1 @@ -188,6 +194,10 @@ and are_convertible_stacks f st a c m1 m2 = else C.list_fold_left2 f map a m1.s m2.s -let are_convertible f st c u t = - if !G.ct >= level then log2 st "Now converting" c u c t; +let are_convertible f st c u t = +IFDEF TRACE THEN + if !G.ct >= level then log2 st "Now converting" c u c t +ELSE () END; are_convertible f st true c empty_machine u empty_machine t + +END