X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Flevel.ml;h=5f5251f6cc7307067ef41bcbc23fd6eced9492fa;hb=30eb28f8c35d7667b3a0052c30d2750a492fa464;hp=b10dda06a4b83f30618790322dd2e5459c3bf49f;hpb=0175318715aeb84215a6d3257d417ee5c6091e53;p=helm.git

diff --git a/helm/software/helena/src/common/level.ml b/helm/software/helena/src/common/level.ml
index b10dda06a..5f5251f6c 100644
--- a/helm/software/helena/src/common/level.ml
+++ b/helm/software/helena/src/common/level.ml
@@ -9,34 +9,177 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-type level = int option
+module H = Hashtbl
+
+module L = Log
+module G = Options
+module J = Marks
+
+type value = Inf                 (* infinite level *)
+           | Fin of int          (* finite level *)
+           | Ref of J.mark * int (* referred level, step *)
+           | Unk                 (* no level set *)
+
+type level = {
+  mutable v: value; (* value *)  
+          s: bool;  (* static level? *)
+  mutable b: bool;  (* beta allowed? *)
+}
+
+type status = (J.mark, level) H.t (* environment for level variables *)
+
+(* Internal functions *******************************************************)
+
+let level = 6
+
+let env_size = 1300
+
+let zero = Fin 0
+
+let warn s = L.warn level s
+
+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
+
+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
+      )
+   in
+   H.iter map st 
+
+let cell s v = {
+   v = v; s = s; b = false
+}
+
+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 
+
+let find st k =
+   try H.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
+   | cell                        -> k, cell
+
+let rec resolve_key st k = match find st k with
+   | {v = Ref (k, i)} when i = 0 -> resolve_key st k
+   | cell                        -> k, cell
+
+let resolve_level st = function
+   | {v = Ref (k, i)} when i = 0 -> resolve_key st k
+   | cell                        -> J.null_mark, cell
+
+let rec generated st h i =
+   let default = dynamic h i in
+   let k = J.new_mark () in
+   match resolve_key_with_default st default k with
+      | k, n when n = default   -> if !G.trace >= level then pp_table st; n
+      | _, n when n.s = true -> generated st h i
+      | _                    -> assert false
+
+let assert_finite st n j =
+   if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" 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 (**)
+      | 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
+      | Ref (k, i)       -> n.v <- Fin j; aux (resolve_key st k) (i+j) 
+   in
+   let k, n = resolve_level st n in
+(*   if j = 0 && n.b then begin
+      Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**)
+   end else *)
+      aux (k, n) j
+
+let assert_infinite st n =
+   if !G.trace >= level then warn "ASSERT INFINITE";
+   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
+      | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k) 
+   in
+   aux (resolve_level st n)
 
 (* Interface functions ******************************************************)
 
-let infinite = None
+let initial_status () =
+   H.create env_size
+
+let infinite = cell true Inf
+
+let finite i = cell true (Fin i)
+
+let one = finite 1
 
-let finite i = Some i
+let two = finite 2
 
-let is_zero xi = 
-   xi = (Some 0)
+let rec unknown st =
+   if !G.trace >= level then warn "UNKNOWN";
+   let default = empty () in
+   let k = J.new_mark () in
+   match resolve_key_with_default st default k with
+      | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
+      | _, n when n.s = true  -> n
+      | _                     -> unknown st
 
-let is_infinite xi =
-   xi = None
+let minus st n j =
+   if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
+   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
+      | Ref (k, i)       -> 
+         let k, n = resolve_key st k in
+         aux k n (i+j)      
+   in
+   let k, n = resolve_level st n in
+   aux k n j
 
-let succ = function
-   | None   -> None
-   | Some i -> Some (succ i)
+let to_string st n =
+   let k, n = resolve_level st n in
+   string_of_value k n.v
 
-let pred = function
-   | None              -> None
-   | Some i when i > 1 -> Some (pred i)
-   | _                 -> Some 0
+let assert_not_zero st n =
+   if !G.trace >= level then warn "ASSERT NOT ZERO";
+   let k, n = resolve_level st n in
+   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); *)      
+      | _                      -> n.b <- true; if !G.trace >= level then pp_table st; n.b
 
-let minus n j = match n with
-   | None              -> None
-   | Some i when i > j -> Some (i - j)
-   | _                 -> Some 0
+let assert_zero st n = assert_finite st n 0
 
-let to_string = function
-   | None   -> ""
-   | Some i -> string_of_int i
+let assert_equal st n1 n2 =
+   let k1, n1 = resolve_level st n1 in
+   let k2, n2 = resolve_level st n2 in
+   if n1 = n2 then true else
+   let b =
+      if not n1.b || assert_not_zero st n2 then match n1.v with
+         | Inf   -> assert_infinite st n2
+         | Fin i -> assert_finite st n2 i
+         | 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