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 (* referred level *)
+type value = Inf (* infinite level *)
+ | Fin of int (* finite level *)
+ | Ref of J.mark * int (* referred level, step *)
+ | Unk (* no level set *)
-type level = bool * value (* static level? value *)
+type level = {
+ mutable v: value; (* value *)
+ s: bool; (* static level? *)
+ mutable b: bool; (* beta allowed? *)
+}
-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 *)
+type status = (J.mark, level) H.t (* environment for level variables *)
(* Internal functions *******************************************************)
-let env_size = 1300
+let level = 6
-let empty_ref = Const []
+let env_size = 1300
let zero = Fin 0
-let find st k =
- try H.find st k with Not_found -> H.add st k empty_ref; empty_ref
+let warn s = L.warn level s
-let rec resolve st k = match find st k with
- | Value (Ref k) -> resolve st k
- | cell -> k, cell
+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
-(* Interface functions ******************************************************)
+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 initial_status () =
- H.create env_size
+let cell s v = {
+ v = v; s = s; b = false
+}
-let infinite = true, Inf
+let empty () = cell true Unk
-let one = true, Fin 1
+let dynamic k i = cell false (Ref (k, i))
-let two = true, Fin 2
+let find_with_default st default k =
+ try H.find st k with Not_found -> H.add st k default; default
-let finite i = true, Fin i
+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)
-let unknown st k = match resolve st k with
- | _, Value l -> true, l
- | k, Const _ -> true, Ref k
+(* Interface functions ******************************************************)
-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 -> false, Inf
- | _, Fin i when i > j -> false, Fin (i - j)
- | _, Fin _ -> false, zero
- | _, Ref i -> false, Inf (* assert false *)
+let initial_status () =
+ H.create env_size
+
+let infinite = cell true Inf
+
+let finite i = cell true (Fin i)
+
+let one = finite 1
+
+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
+ 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 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 to_string st n =
+ let k, n = resolve_level st n in
+ string_of_value k n.v
+
+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 assert_zero st n = assert_finite st n 0
+
+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
projects / helm.git / blobdiff