- bugfix is refreshed state of AutCrg: now we return a fresh state

[helm.git] / helm / software / helena / src / common / layer.ml

diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml
index ed2b140e4a339b823a68e9e1c7004487be6487f1..ea02538d2cd13e11d8c07798ef97ad15b773e2b6 100644 (file)
--- 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 P = Marks
 module G = Options
-module J = Marks
 
 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 *******************************************************)
 
@@ -41,17 +41,17 @@ let zero = Fin 0
 let string_of_value k = function
    | 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
 
 (* 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 
 
 let cell s v = {
    v = v; s = s; b = false
@@ -62,10 +62,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,14 +77,14 @@ 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 n <> default then KH.replace st k default;
       if !G.trace >= level then pp_table st; default
    end
 
@@ -93,15 +93,15 @@ let assert_finite st n j =
    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 (**)
+         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
       | 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
 
@@ -110,7 +110,7 @@ let assert_infinite st n =
    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 (**)
+         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
       | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
    in
@@ -119,7 +119,7 @@ let assert_infinite st n =
 (* Interface functions ******************************************************)
 
 let initial_status () =
-   H.create env_size
+   KH.create env_size
 
 let refresh_status st = st 
 
@@ -134,7 +134,7 @@ let two = finite 2
 let rec unknown st =
    if !G.trace >= level then warn "UNKNOWN";
    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
@@ -150,7 +150,7 @@ let minus st n j =
       | 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)      
@@ -168,8 +168,8 @@ let assert_not_zero st n =
    match n.b, n.v with
       | 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); *)      
+         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
 
 let assert_zero st n = assert_finite st n 0
@@ -187,7 +187,7 @@ let assert_equal st n1 n2 =
       else false
    in begin
    if !G.trace >= level then warn "ASSERT EQUAL";
-   if b && k1 <> J.null_mark && k2 <> J.null_mark then begin
+   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