- the disambiguation of unified binders continues

[helm.git] / helm / software / helena / src / basic_rg / brgReduction.ml

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index c0ff7757552962f150acba8c17f29493f01391c5..61f1d9038b9495b05c50a995f80227a006e7d475 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -17,7 +17,6 @@ module N  = Level
 module E  = Entity
 module G  = Options
 module O  = Output
-module Q  = Ccs
 module S  = Status
 module B  = Brg
 module BO = BrgOutput
@@ -37,13 +36,15 @@ type message = (kam, B.term) L.message
 
 let level = 4
 
-let log1 s c t =
-   let sc, st = s ^ " in the environment", "the term" in
-   L.log BO.specs level (L.et_items1 sc c st t)
+let sublevel = succ level
 
-let log2 s cu u ct t =
+let log1 st s c t =
+   let s1, s2 = s ^ " in the environment", "the term" in
+   L.log st BO.specs level (L.et_items1 s1 c s2 t)
+
+let log2 st s cu u ct t =
    let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in
-   L.log BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+   L.log st 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 ->
@@ -82,14 +83,17 @@ let assert_tstep m vo = match m.n with
 
 let tstep m = {m with d = succ m.d}
 
+let tsteps m = match m.n with
+   | Some n when n > m.d -> n - m.d
+   | _                   -> 0
+
 let get m i =
    let _, c, a, b = B.get m.e i in c, a, b
 
 (* to share *)
 let rec step st m x = 
-(*
-   log1 (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;
-*)   
+   if !G.trace >= sublevel then 
+   log1 st.S.lenv (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;
    match x with
    | B.Sort (a, h)                ->
       if assert_tstep m false then
@@ -139,11 +143,12 @@ let rec step st m x =
    | B.Bind (a, B.Abst (n, w), t) ->
       begin match m.s with
          | []          ->
-            if n = N.infinite || m.d = 0 then m, x, None else
-            let n = N.minus n m.d in
+            let i = tsteps m in
+            if i = 0 then m, x, None else
+            let n = N.minus st.S.lenv n i in
             m, B.Bind (a, B.Abst (n, w), t), None
         | (c, v) :: s ->
-(*            if N.is_zero n then Q.add_nonzero st.S.cc a; *)
+            if !G.cc && not (N.assert_not_zero st.S.lenv n) then assert false;
            if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
            let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in
             let e = B.push m.e c a (B.abbr v) in
@@ -170,7 +175,7 @@ let push m a b =
    {m with e = e; l = l}
 
 let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
-   if !G.trace >= level then log2 "Now converting nfs" m1.e t1 m2.e t2;
+   if !G.trace >= level then log2 st.S.lenv "Now converting nfs" m1.e t1 m2.e t2;
    match t1, r1, t2, r2 with
       | B.Sort (_, h1), _, B.Sort (_, h2), _                ->
          h1 = h2
@@ -200,16 +205,16 @@ let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
         ac_nfs st (step st m1 v1) (m2, t2, r2)
       | 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 !G.cc && not (N.assert_equal st.S.lenv n1 n2) then false else
          if ac {st with S.si = false} (reset m1 zero) w1 (reset m2 zero) w2 then
            ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
         else false
       | B.Sort _, _, B.Bind (a, (B.Abst (n, _) as b), t), _ ->
-         if st.S.si then begin
-(*       if N.is_zero n then () else Q.add_zero st.S.cc a; *)
+         if st.S.si then
+            if !G.cc && not (N.assert_zero st.S.lenv n) then false else begin
            if !G.summary then O.add ~si:1 ();
-           ac st (push m1 a b) t1 (push m2 a b) t
-         end else false
+           ac st (push m1 a b) t1 (push m2 a b) t end
+         else false
       | _                                                   -> false
 
 and ac st m1 t1 m2 t2 =
@@ -236,12 +241,12 @@ let get m i =
    let _, _, _, b = B.get m.e i in b
 
 let xwhd st m n t =
-   if !G.trace >= level then log1 "Now scanning" m.e t;   
+   if !G.trace >= level then log1 st.S.lenv "Now scanning" m.e t;   
    let m, t, _ = step {st with S.delta = true} (reset m n) t in
    m, t
 
 let are_convertible st m1 n1 t1 m2 n2 t2 = 
-   if !G.trace >= level then log2 "Now converting" m1.e t1 m2.e t2;
+   if !G.trace >= level then log2 st.S.lenv "Now converting" m1.e t1 m2.e t2;
    let r = ac {st with S.delta = !G.expand} (reset m1 n1) t1 (reset m2 n2) t2 in
    r
 (*    let err _ = in 
@@ -249,9 +254,9 @@ let are_convertible st m1 n1 t1 m2 n2 t2 =
 
 (* error reporting **********************************************************)
 
-let pp_term m frm t = BO.specs.L.pp_term m.e frm t
+let pp_term st m och t = BO.specs.L.pp_term st m.e och t
 
-let pp_lenv frm m = BO.specs.L.pp_lenv frm m.e
+let pp_lenv st och m = BO.specs.L.pp_lenv st och m.e
 
 let specs = {
    L.pp_term = pp_term; L.pp_lenv = pp_lenv