X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_rg%2FbrgReduction.ml;h=c4b2e9c15e7d0ed8104e4e889d0865c6336d56f5;hb=cee0c3ca597ebbff2250674c255ed1bc909521fb;hp=03ed05b053a603985fea79550c313397b3cfe675;hpb=ab13cfa248f0ee58d239ceeddfb50ec49a6b5c6d;p=helm.git diff --git a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml index 03ed05b05..c4b2e9c15 100644 --- a/helm/software/lambda-delta/src/basic_rg/brgReduction.ml +++ b/helm/software/lambda-delta/src/basic_rg/brgReduction.ml @@ -9,15 +9,18 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module C = Cps -module S = Share -module L = Log -module Y = Entity -module P = Output -module B = Brg -module O = BrgOutput -module E = BrgEnvironment +module U = NUri +module C = Cps +module W = Share +module L = Log +module E = Entity +module N = Level +module O = Output +module Q = Ccs +module S = Status +module B = Brg +module BO = BrgOutput +module BE = BrgEnvironment type kam = { e: B.lenv; (* environment *) @@ -31,11 +34,11 @@ let level = 5 let log1 s c t = let sc, st = s ^ " in the environment", "the term" in - L.log O.specs level (L.et_items1 sc c st t) + L.log BO.specs level (L.et_items1 sc c st t) let log2 s cu u ct t = let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in - L.log O.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) + L.log BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) let rec list_and map = function | hd1 :: tl1, hd2 :: tl2 -> @@ -59,12 +62,12 @@ let are_alpha_convertible err f t1 t2 = aux_bind f (b1, b2) | _ -> err () and aux_bind f = function - | B.Abbr v1, B.Abbr v2 - | B.Abst v1, B.Abst v2 -> aux f (v1, v2) - | B.Void, B.Void -> f () - | _ -> err () + | B.Abbr v1, B.Abbr v2 -> aux f (v1, v2) + | B.Abst (n1, v1), B.Abst (n2, v2) when n1 = n2 -> aux f (v1, v2) + | B.Void, B.Void -> f () + | _ -> err () in - if S.eq t1 t2 then f () else aux f (t1, t2) + if W.eq t1 t2 then f () else aux f (t1, t2) let get m i = let _, c, a, b = B.get m.e i in c, a, b @@ -73,57 +76,58 @@ let get m i = let rec step st m x = (* L.warn "entering R.step"; *) match x with - | B.Sort _ -> m, None, x - | B.GRef (_, uri) -> - begin match E.get_entity uri with - | _, _, Y.Abbr v when st.Y.delta -> - P.add ~gdelta:1 (); step st m v - | _, _, Y.Abst w when st.Y.rt -> - P.add ~grt:1 (); step st m w - | a, _, Y.Abbr v -> - let e = Y.apix C.err C.start a in + | B.Sort _ -> m, None, x + | B.GRef (_, uri) -> + begin match BE.get_entity uri with + | _, _, E.Abbr v when st.S.delta -> + O.add ~gdelta:1 (); step st m v + | _, _, E.Abst (_, w) when st.S.rt -> + O.add ~grt:1 (); step st m w + | a, _, E.Abbr v -> + let e = E.apix C.err C.start a in m, Some (e, a, B.Abbr v), x - | a, _, Y.Abst w -> - let e = Y.apix C.err C.start a in - m, Some (e, a, B.Abst w), x - | _, _, Y.Void -> assert false + | a, _, E.Abst (n, w) -> + let e = E.apix C.err C.start a in + m, Some (e, a, B.Abst (n, w)), x + | _, _, E.Void -> assert false end - | B.LRef (_, i) -> + | B.LRef (_, i) -> begin match get m i with - | c, _, B.Abbr v -> - P.add ~ldelta:1 (); + | c, _, B.Abbr v -> + O.add ~ldelta:1 (); step st {m with e = c} v - | c, _, B.Abst w when st.Y.rt -> - P.add ~lrt:1 (); + | c, _, B.Abst (_, w) when st.S.rt -> + O.add ~lrt:1 (); step st {m with e = c} w - | c, _, B.Void -> + | c, _, B.Void -> assert false - | c, a, (B.Abst _ as b) -> - let e = Y.apix C.err C.start a in + | c, a, (B.Abst _ as b) -> + let e = E.apix C.err C.start a in {m with e = c}, Some (e, a, b), x end - | B.Cast (_, _, t) -> - P.add ~tau:1 (); + | B.Cast (_, _, t) -> + O.add ~tau:1 (); step st m t - | B.Appl (_, v, t) -> + | B.Appl (_, v, t) -> step st {m with s = (m.e, v) :: m.s} t - | B.Bind (a, B.Abst w, t) -> + | B.Bind (a, B.Abst (n, w), t) -> begin match m.s with | [] -> m, None, x | (c, v) :: s -> - P.add ~beta:1 ~upsilon:(List.length s) (); + if N.is_zero n then Q.add_nonzero st.S.cc a; + O.add ~beta:1 ~upsilon:(List.length s) (); let e = B.push m.e c a (B.abbr v) (* (B.Cast ([], w, v)) *) in step st {m with e = e; s = s} t end | B.Bind (a, b, t) -> - P.add ~upsilon:(List.length m.s) (); + O.add ~upsilon:(List.length m.s) (); let e = B.push m.e m.e a b in step st {m with e = e} t let push m a b = assert (m.s = []); let a, d = match b with - | B.Abst _ -> Y.Apix m.d :: a, succ m.d + | B.Abst _ -> E.Apix m.d :: a, succ m.d | b -> a, m.d in let e = B.push m.e m.e a b in @@ -139,28 +143,30 @@ let rec ac_nfs st (m1, r1, u) (m2, r2, t) = | Some (e1, _, B.Abbr v1), _, Some (e2, _, B.Abbr v2), _ -> if e1 = e2 then if ac_stacks st m1 m2 then true else begin - P.add ~gdelta:2 (); ac st m1 v1 m2 v2 + O.add ~gdelta:2 (); ac st m1 v1 m2 v2 end else if e1 < e2 then begin - P.add ~gdelta:1 (); + O.add ~gdelta:1 (); ac_nfs st (m1, r1, u) (step st m2 v2) end else begin - P.add ~gdelta:1 (); + O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, r2, t) end | _, _, Some (_, _, B.Abbr v2), _ -> - P.add ~gdelta:1 (); + O.add ~gdelta:1 (); ac_nfs st (m1, r1, u) (step st m2 v2) | Some (_, _, B.Abbr v1), _, _, _ -> - P.add ~gdelta:1 (); + O.add ~gdelta:1 (); ac_nfs st (step st m1 v1) (m2, r2, t) - | _, B.Bind (a1, (B.Abst w1 as b1), t1), - _, B.Bind (a2, (B.Abst w2 as b2), t2) -> - if ac {st with Y.si = false} m1 w1 m2 w2 then + | _, B.Bind (a1, (B.Abst (n1, w1) as b1), t1), + _, B.Bind (a2, (B.Abst (n2, w2) as b2), t2) -> + if n1 = n2 then () else Q.add_equal st.S.cc a1 a2; + if ac {st with S.si = false} m1 w1 m2 w2 then ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2 else false - | _, B.Sort _, _, B.Bind (a, b, t) when st.Y.si -> - P.add ~si:1 (); + | _, B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t) -> + if N.is_zero n then () else Q.add_zero st.S.cc a; + O.add ~si:1 (); ac st (push m1 a b) u (push m2 a b) t | _ -> false @@ -173,7 +179,7 @@ and ac_stacks st m1 m2 = if List.length m1.s <> List.length m2.s then false else let map (c1, v1) (c2, v2) = let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in - ac {st with Y.si = false} m1 v1 m2 v2 + ac {st with S.si = false} m1 v1 m2 v2 in list_and map (m1.s, m2.s) @@ -189,21 +195,21 @@ let get m i = let xwhd st m t = L.box level; log1 "Now scanning" m.e t; - let m, _, t = step {st with Y.delta = true; Y.rt = true} m t in + let m, _, t = step {st with S.delta = true; S.rt = true} m t in L.unbox level; m, t let are_convertible st mu u mw w = L.box level; log2 "Now converting" mu.e u mw.e w; - let r = ac {st with Y.delta = st.Y.expand; Y.rt = false} mu u mw w in + let r = ac {st with S.delta = st.S.expand; S.rt = false} mu u mw w in L.unbox level; r (* let err _ = in - if S.eq mu mw then are_alpha_convertible err f u w else err () *) + if W.eq mu mw then are_alpha_convertible err f u w else err () *) (* error reporting **********************************************************) -let pp_term m frm t = O.specs.L.pp_term m.e frm t +let pp_term m frm t = BO.specs.L.pp_term m.e frm t -let pp_lenv frm m = O.specs.L.pp_lenv frm m.e +let pp_lenv frm m = BO.specs.L.pp_lenv frm m.e let specs = { L.pp_term = pp_term; L.pp_lenv = pp_lenv