- new attributes system

[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 b10dda06a4b83f30618790322dd2e5459c3bf49f..60f7ac4381b6d2c0e2ccaefde91229d0a6cb231d 100644 (file)
--- a/helm/software/helena/src/common/level.ml
+++ b/helm/software/helena/src/common/level.ml
@@ -9,34 +9,63 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-type level = int option
+module H = Hashtbl
+
+module J = Marks
+
+type level = Inf           (* infinite *)
+           | Fin of int    (* finite *)
+           | Ref of J.mark (* unknown *)
+
+type const = NotZero (* not zero: beta and whnf allowed *)
+
+type contents = Value of level       (* 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 empty_ref = Const []
+
+let find st k =
+   try H.find st k with Not_found -> H.add st k empty_ref; empty_ref 
+
+let rec resolve st k = match find st k with
+   | Value (Ref k) -> resolve st k
+   | cell          -> k, cell
 
 (* Interface functions ******************************************************)
 
-let infinite = None
+let initial_status () =
+   H.create env_size
+
+let infinite = Inf
+
+let zero = Fin 0
 
-let finite i = Some i
+let one = Fin 1
 
-let is_zero xi = 
-   xi = (Some 0)
+let two = Fin 2
 
-let is_infinite xi =
-   xi = None
+let finite i = Fin i
 
-let succ = function
-   | None   -> None
-   | Some i -> Some (succ i)
+let unknown st k = match resolve st k with
+   | _, Value l -> l
+   | k, Const _ -> Ref k
 
-let pred = function
-   | None              -> None
-   | Some i when i > 1 -> Some (pred i)
-   | _                 -> Some 0
+let is_zero l = 
+   l = zero
 
 let minus n j = match n with
-   | None              -> None
-   | Some i when i > j -> Some (i - j)
-   | _                 -> Some 0
+   | Inf              -> Inf
+   | Fin i when i > j -> Fin (i - j)
+   | Fin _            -> zero
+   | Ref i            -> Inf (* assert false *)
 
 let to_string = function
-   | None   -> ""
-   | Some i -> string_of_int i
+   | Inf   -> ""
+   | Fin i -> string_of_int i
+   | Ref k -> "-" ^ J.to_string k