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=ed2b140e4a339b823a68e9e1c7004487be6487f1;hpb=cd77f8898787aab4808437ee731f5c7f87cd64df;p=helm.git

diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index ed2b140e4..c0b6bcc19 100644
--- a/helm/software/helena/src/common/layer.ml
+++ b/helm/software/helena/src/common/layer.ml
@@ -9,15 +9,15 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module H = Hashtbl
+module KH = Hashtbl
 
-module L = Log
-module G = Options
-module J = Marks
+module L  = Log
+module P  = Marks
+module G  = Options
 
 type value = Inf                 (* infinite layer *)
            | Fin of int          (* finite layer *)
-           | Ref of J.mark * int (* referred layer, step *)
+           | Ref of P.mark * int (* referred layer, step *)
            | Unk                 (* no layer set *)
 
 type layer = {
@@ -26,7 +26,7 @@ type layer = {
   mutable b: bool;  (* beta allowed? *)
 }
 
-type status = (J.mark, layer) H.t (* environment for layer variables *)
+type status = (P.mark, layer) KH.t (* environment for layer variables *)
 
 (* Internal functions *******************************************************)
 
@@ -39,19 +39,23 @@ 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) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i
-   | Unk        -> "-" ^ J.string_of_mark k
+   | 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 = 
       warn (Printf.sprintf "%s: v %s (s:%b b:%b)" 
-         (J.string_of_mark k) (string_of_value k n.v) n.s n.b
+         (P.string_of_mark k) (string_of_value k n.v) n.s n.b
       )
    in
-   H.iter map st 
+   KH.iter map st 
+
+END
 
 let cell s v = {
    v = v; s = s; b = false
@@ -62,10 +66,10 @@ let empty () = cell true Unk
 let dynamic k i = cell false (Ref (k, i))
 
 let find_with_default st default k =
-   try H.find st k with Not_found -> H.add st k default; default 
+   try KH.find st k with Not_found -> KH.add st k default; default 
 
 let find st k =
-   try H.find st k with Not_found -> assert false 
+   try KH.find st k with Not_found -> assert false 
 
 let rec resolve_key_with_default st default k = match find_with_default st default k with
    | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
@@ -77,41 +81,58 @@ let rec resolve_key st k = match find st k with
 
 let resolve_layer st = function
    | {v = Ref (k, i)} when i = 0 -> resolve_key st k
-   | cell                        -> J.null_mark, cell
+   | cell                        -> P.null_mark, cell
 
 let rec generated st h i =
    let default = dynamic h i in
-   let k = J.new_mark () in
+   let k = P.new_mark () in
    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 H.replace st k default;
-      if !G.trace >= level then pp_table st; default
+      if n <> default then KH.replace st k 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" (J.string_of_mark k) i j; true (**)
+         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" (J.string_of_mark k) j; true (**)
-      | Unk              -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
+         Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; 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
 (*   if j = 0 && n.b then begin
-      Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**)
+      Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false (**)
    end else *)
       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" (J.string_of_mark k) i; true (**)
-      | Unk        -> n.v <- Inf; if !G.trace >= level then pp_table st; true
+         Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; 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)
@@ -119,11 +140,11 @@ let assert_infinite st n =
 (* Interface functions ******************************************************)
 
 let initial_status () =
-   H.create env_size
+   KH.create env_size
 
 let refresh_status st = st 
 
-let infinite = cell true Inf
+let infinity = cell true Inf
 
 let finite i = cell true (Fin i)
 
@@ -132,25 +153,33 @@ 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 = J.new_mark () 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))
       | Fin _            -> cell false zero
       | Unk              ->
-         if k = J.null_mark then assert false else generated st k j
+         if k = P.null_mark then assert false else generated st k j
       | Ref (k, i)       -> 
          let k, n = resolve_key st k in
          aux k n (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" (J.string_of_mark k); false *) (**)
-(*      if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (J.string_of_mark k); *)      
-      | _                      -> n.b <- true; if !G.trace >= level then pp_table st; n.b
+         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;
+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";
-   if b && k1 <> J.null_mark && k2 <> J.null_mark then begin
-      n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st
-   end; b end
+   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);
+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