- static disambiguation of Automath unified binders

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

diff --git a/helm/software/helena/src/common/level.ml b/helm/software/helena/src/common/level.ml
index 60f7ac4381b6d2c0e2ccaefde91229d0a6cb231d..75058cf83066e456bb674ed7e051dc84124db27e 100644 (file)
--- a/helm/software/helena/src/common/level.ml
+++ b/helm/software/helena/src/common/level.ml
@@ -13,23 +13,27 @@ module H = Hashtbl
 
 module J = Marks
 
-type level = Inf           (* infinite *)
-           | Fin of int    (* finite *)
-           | Ref of J.mark (* unknown *)
+type value = Inf           (* infinite level *)
+           | Fin of int    (* finite level *)
+           | Ref of J.mark (* referred level *)
 
-type const = NotZero (* not zero: beta and whnf allowed *)
+type level = bool * value (* static level? value *)
 
-type contents = Value of level       (* defined with this level *)
+type const = NotZero (* not zero: beta allowed *)
+
+type contents = Value of value       (* defined with this level *)
               | Const of const list  (* undefined with these constraints *)
 
 type status = (J.mark, contents) H.t (* environment for level variables *)
 
 (* Internal functions *******************************************************)
 
-let env_size = 2000
+let env_size = 1300
 
 let empty_ref = Const []
 
+let zero = Fin 0
+
 let find st k =
    try H.find st k with Not_found -> H.add st k empty_ref; empty_ref 
 
@@ -42,30 +46,39 @@ let rec resolve st k = match find st k with
 let initial_status () =
    H.create env_size
 
-let infinite = Inf
-
-let zero = Fin 0
+let infinite = true, Inf
 
-let one = Fin 1
+let one = true, Fin 1
 
-let two = Fin 2
+let two = true, Fin 2
 
-let finite i = Fin i
+let finite i = true, Fin i
 
 let unknown st k = match resolve st k with
-   | _, Value l -> l
-   | k, Const _ -> Ref k
+   | _, Value l -> true, l
+   | k, Const _ -> true, Ref k
 
-let is_zero l = 
-   l = zero
+let to_string = function
+   | _, Inf   -> ""
+   | _, Fin i -> string_of_int i
+   | _, Ref k -> "-" ^ J.to_string k
+(*
+let is_finite j l =
+   let b, k = l in
+   match resolve st k with
+      | k, Value (Fin i) -> 
+         if i <> j then Printf.printf "%s is %u but it must be %u\n" (to_string l) i j;
+         i = j
+      | k, Value Inf     -> 
+         Printf.printf "%s is infinite but it must be %u\n" j;
+
+   | k,  
+*)
+let is_zero (_, n) =
+   n = zero
 
 let minus n j = match n with
-   | Inf              -> Inf
-   | Fin i when i > j -> Fin (i - j)
-   | Fin _            -> zero
-   | Ref i            -> Inf (* assert false *)
-
-let to_string = function
-   | Inf   -> ""
-   | Fin i -> string_of_int i
-   | Ref k -> "-" ^ J.to_string k
+   | _, Inf              -> false, Inf
+   | _, Fin i when i > j -> false, Fin (i - j)
+   | _, Fin _            -> false, zero
+   | _, Ref i            -> false, Inf (* assert false *)