\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module H = Hashtbl
+module KH = Hashtbl
-module L = Log
-module G = Options
-module J = Marks
+module L = Log
+module P = Marks
+module G = Options
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 = {
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 *******************************************************)
let zero = Fin 0
let string_of_value k = function
- | Inf -> ""
+ | 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
+IFDEF TRACE THEN
+
+(* Note: remove assigned variables *)
let pp_table st =
- let map k n =
+ 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
+
+END
let cell s v = {
v = v; s = s; b = false
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
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
- 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 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 KH.replace st k default;
+IFDEF TRACE THEN
+ if !G.ct >= level then pp_table st
+ELSE () END;
+ default
+ end
let assert_finite st n j =
- if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
+IFDEF TRACE THEN
+ if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j)
+ELSE () END;
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 (**)
- | Unk -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
+ Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
+ | Unk ->
+ n.v <- Fin j;
+IFDEF TRACE THEN
+ if !G.ct >= level then pp_table st
+ELSE () END;
+ 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
let assert_infinite st n =
- if !G.trace >= level then warn "ASSERT INFINITE";
+IFDEF TRACE THEN
+ if !G.ct >= level then warn "ASSERT INFINITE"
+ELSE () END;
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
+ Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
+ | Unk ->
+ n.v <- Inf;
+IFDEF TRACE THEN
+ if !G.ct >= level then pp_table st
+ELSE () END;
+ true
| Ref (k, _) -> n.v <- Inf; aux (resolve_key st k)
in
aux (resolve_layer st n)
(* Interface functions ******************************************************)
let initial_status () =
- H.create env_size
+ KH.create env_size
let refresh_status st = st
-let infinite = cell true Inf
+let infinity = cell true Inf
let finite i = cell true (Fin i)
let two = finite 2
let rec unknown st =
- if !G.trace >= level then warn "UNKNOWN";
+IFDEF TRACE THEN
+ if !G.ct >= level then warn "UNKNOWN"
+ELSE () END;
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 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
+ | Fin _ -> n
+ | Unk ->
+IFDEF TRACE THEN
+ if !G.ct >= level then pp_table st
+ELSE () END;
+ cell true (Ref (k, 0))
+ | Ref _ -> assert false
+ else unknown st
+
let minus st n j =
- if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
+IFDEF TRACE THEN
+ if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j)
+ELSE () END;
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
+ 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)
string_of_value k n.v
let assert_not_zero st n =
- if !G.trace >= level then warn "ASSERT NOT ZERO";
+IFDEF TRACE THEN
+ if !G.ct >= level then warn "ASSERT NOT ZERO"
+ELSE () END;
let k, n = resolve_layer st n in
match n.b, n.v with
- | true, _ -> n.b
+ | 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
+ 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;
+IFDEF TRACE THEN
+ if !G.ct >= level then pp_table st
+ELSE () END;
+ n.b
let assert_zero st n = assert_finite st n 0
| 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
+ in
+IFDEF TRACE THEN
+ if !G.ct >= level then warn "ASSERT EQUAL"
+ELSE () END;
+ if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
+ n1.v <- Ref (k2, 0);
+IFDEF TRACE THEN
+ if !G.ct >= level then pp_table st
+ELSE () END
+ end; b
let is_not_zero st n =
- let _, n = resolve_layer st n in n.v <> zero
+(* let _, n = resolve_layer st n in *) n.v <> zero
+
+let are_equal st n1 n2 =
+(*
+ let _, n1 = resolve_layer st n1 in
+ let _, n2 = resolve_layer st n2 in
+*)
+ n1.v = n2.v
projects / helm.git / blobdiff