X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Flayer.ml;h=c0b6bcc19e47b8209838448f6e0a0a3b3642d602;hb=9bdda2beaa7b0f836e3700a2e2458761e8eee06d;hp=ea02538d2cd13e11d8c07798ef97ad15b773e2b6;hpb=9935a5bf5bdc98ad01a2b0234cf4e612a62c939f;p=helm.git

diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index ea02538d2..c0b6bcc19 100644
--- a/helm/software/helena/src/common/layer.ml
+++ b/helm/software/helena/src/common/layer.ml
@@ -11,9 +11,9 @@
 
 module KH = Hashtbl
 
-module L = Log
-module P = Marks
-module G = Options
+module L  = Log
+module P  = Marks
+module G  = Options
 
 type value = Inf                 (* infinite layer *)
            | Fin of int          (* finite layer *)
@@ -39,11 +39,13 @@ let warn s = L.warn (pred level) s
 let zero = Fin 0
 
 let string_of_value k = function
-   | Inf        -> ""
+   | Inf        -> "-"
    | Fin i      -> string_of_int i
    | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i
    | Unk        -> "-" ^ P.string_of_mark k
 
+IFDEF TRACE THEN
+
 (* Note: remove assigned variables *)
 let pp_table st =
    let map k n = 
@@ -53,6 +55,8 @@ let pp_table st =
    in
    KH.iter map st 
 
+END
+
 let cell s v = {
    v = v; s = s; b = false
 }
@@ -85,18 +89,28 @@ let rec generated st h i =
    let k, n = resolve_key_with_default st default k in 
    if n.s then generated st h i else begin
       if n <> default then KH.replace st k default;
-      if !G.trace >= level then pp_table st; default
+IFDEF TRACE THEN
+      if !G.ct >= level then pp_table st
+ELSE () END;
+      default
    end
 
 let assert_finite st n j =
-   if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
+IFDEF TRACE THEN
+   if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j)
+ELSE () END;
    let rec aux (k, n) j = match n.v with    
       | Fin i when i = j -> true
       | Fin i            ->
          Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
       | Inf              ->
          Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
-      | Unk              -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
+      | Unk              ->
+         n.v <- Fin j;
+IFDEF TRACE THEN
+         if !G.ct >= level then pp_table st
+ELSE () END;
+         true
       | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j) 
    in
    let k, n = resolve_layer st n in
@@ -106,12 +120,19 @@ let assert_finite st n j =
       aux (k, n) j
 
 let assert_infinite st n =
-   if !G.trace >= level then warn "ASSERT INFINITE";
+IFDEF TRACE THEN 
+   if !G.ct >= level then warn "ASSERT INFINITE"
+ELSE () END;
    let rec aux (k, n) = match n.v with
       | Inf        -> true
       | Fin i      -> 
          Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
-      | Unk        -> n.v <- Inf; if !G.trace >= level then pp_table st; true
+      | Unk        ->
+         n.v <- Inf;
+IFDEF TRACE THEN
+         if !G.ct >= level then pp_table st
+ELSE () END;
+         true
       | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
    in
    aux (resolve_layer st n)
@@ -123,7 +144,7 @@ let initial_status () =
 
 let refresh_status st = st 
 
-let infinite = cell true Inf
+let infinity = cell true Inf
 
 let finite i = cell true (Fin i)
 
@@ -132,19 +153,27 @@ let one = finite 1
 let two = finite 2
 
 let rec unknown st =
-   if !G.trace >= level then warn "UNKNOWN";
+IFDEF TRACE THEN 
+   if !G.ct >= level then warn "UNKNOWN"
+ELSE () END;
    let default = empty () in
    let k = P.new_mark () in
    let k, n = resolve_key_with_default st default k in
    if n.s then match n.v with
       | Inf
       | Fin _ -> n
-      | Unk   -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+      | Unk   ->
+IFDEF TRACE THEN 
+         if !G.ct >= level then pp_table st
+ELSE () END;
+         cell true (Ref (k, 0))
       | Ref _ -> assert false
    else unknown st
  
 let minus st n j =
-   if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
+IFDEF TRACE THEN
+   if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j)
+ELSE () END;
    let rec aux k n j = match n.v with
       | Inf              -> cell false n.v
       | Fin i when i > j -> cell false (Fin (i - j))
@@ -163,14 +192,21 @@ let to_string st n =
    string_of_value k n.v
 
 let assert_not_zero st n =
-   if !G.trace >= level then warn "ASSERT NOT ZERO";
+IFDEF TRACE THEN
+   if !G.ct >= level then warn "ASSERT NOT ZERO"
+ELSE () END;
    let k, n = resolve_layer st n in
    match n.b, n.v with
-      | true, _                -> n.b
+      | true, _ -> n.b
 (*      | _   , Fin i when i = 0 ->   
          Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
 (*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)      
-      | _                      -> n.b <- true; if !G.trace >= level then pp_table st; n.b
+      | _       ->
+         n.b <- true;
+IFDEF TRACE THEN
+         if !G.ct >= level then pp_table st
+ELSE () END;
+         n.b
 
 let assert_zero st n = assert_finite st n 0
 
@@ -185,12 +221,23 @@ let assert_equal st n1 n2 =
          | Unk   -> true
          | Ref _ -> assert false
       else false
-   in begin
-   if !G.trace >= level then warn "ASSERT EQUAL";
+   in
+IFDEF TRACE THEN
+   if !G.ct >= level then warn "ASSERT EQUAL"
+ELSE () END;
    if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
-      n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
-   end; b end
+      n1.v <- Ref (k2, 0);
+IFDEF TRACE THEN
+      if !G.ct >= level then pp_table st
+ELSE () END
+   end; b
 
 let is_not_zero st n  =
-   let _, n = resolve_layer st n in n.v <> zero
+(*   let _, n = resolve_layer st n in *) n.v <> zero
 
+let are_equal st n1 n2 =
+(*
+   let _, n1 = resolve_layer st n1 in
+   let _, n2 = resolve_layer st n2 in
+*)
+   n1.v = n2.v