2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
18 type value = Inf (* infinite level *)
19 | Fin of int (* finite level *)
20 | Ref of J.mark * int (* referred level, step *)
21 | Unk (* no level set *)
24 mutable v: value; (* value *)
25 s: bool; (* static level? *)
26 mutable b: bool; (* beta allowed? *)
29 type status = (J.mark, level) H.t (* environment for level variables *)
31 (* Internal functions *******************************************************)
39 let warn s = L.warn level s
41 let string_of_value k = function
43 | Fin i -> string_of_int i
44 | Ref (k, i) -> "-" ^ J.string_of_mark k ^ "-" ^ string_of_int i
45 | Unk -> "-" ^ J.string_of_mark k
49 warn (Printf.sprintf "%s: v %s (s:%b b:%b)"
50 (J.string_of_mark k) (string_of_value k n.v) n.s n.b
56 v = v; s = s; b = false
59 let empty () = cell true Unk
61 let dynamic k i = cell false (Ref (k, i))
63 let find_with_default st default k =
64 try H.find st k with Not_found -> H.add st k default; default
67 try H.find st k with Not_found -> assert false
69 let rec resolve_key_with_default st default k = match find_with_default st default k with
70 | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
73 let rec resolve_key st k = match find st k with
74 | {v = Ref (k, i)} when i = 0 -> resolve_key st k
77 let resolve_level st = function
78 | {v = Ref (k, i)} when i = 0 -> resolve_key st k
79 | cell -> J.null_mark, cell
81 let rec generated st h i =
82 let default = dynamic h i in
83 let k = J.new_mark () in
84 match resolve_key_with_default st default k with
85 | k, n when n = default -> if !G.trace >= level then pp_table st; n
86 | _, n when n.s = true -> generated st h i
89 let assert_finite st n j =
90 if !G.trace >= level then warn (Printf.sprintf "ASSERT FINITE %u" j);
91 let rec aux (k, n) j = match n.v with
92 | Fin i when i = j -> true
94 Printf.printf "binder %s is %u but must be %u\n" (J.string_of_mark k) i j; true (**)
96 Printf.printf "binder %s is infinite but must be %u\n" (J.string_of_mark k) j; true (**)
97 | Unk -> n.v <- Fin j; if !G.trace >= level then pp_table st; true
98 | Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j)
100 let k, n = resolve_level st n in
101 (* if j = 0 && n.b then begin
102 Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false (**)
106 let assert_infinite st n =
107 if !G.trace >= level then warn "ASSERT INFINITE";
108 let rec aux (k, n) = match n.v with
111 Printf.printf "binder %s is %u but must be infinite\n" (J.string_of_mark k) i; true (**)
112 | Unk -> n.v <- Inf; if !G.trace >= level then pp_table st; true
113 | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k)
115 aux (resolve_level st n)
117 (* Interface functions ******************************************************)
119 let initial_status () =
122 let infinite = cell true Inf
124 let finite i = cell true (Fin i)
131 if !G.trace >= level then warn "UNKNOWN";
132 let default = empty () in
133 let k = J.new_mark () in
134 match resolve_key_with_default st default k with
135 | k, n when n = default -> if !G.trace >= level then pp_table st; cell true (Ref (k, 0))
136 | _, n when n.s = true -> n
140 if !G.trace >= level then warn (Printf.sprintf "MINUS %u" j);
141 let rec aux k n j = match n.v with
142 | Inf -> cell false n.v
143 | Fin i when i > j -> cell false (Fin (i - j))
144 | Fin _ -> cell false zero
146 if k = J.null_mark then assert false else generated st k j
148 let k, n = resolve_key st k in
151 let k, n = resolve_level st n in
155 let k, n = resolve_level st n in
156 string_of_value k n.v
158 let assert_not_zero st n =
159 if !G.trace >= level then warn "ASSERT NOT ZERO";
160 let k, n = resolve_level st n in
163 (* | _ , Fin i when i = 0 ->
164 Printf.printf "^Pi reduction on binder %s\n" (J.string_of_mark k); false *) (**)
165 (* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (J.string_of_mark k); *)
166 | _ -> n.b <- true; if !G.trace >= level then pp_table st; n.b
168 let assert_zero st n = assert_finite st n 0
170 let assert_equal st n1 n2 =
171 let k1, n1 = resolve_level st n1 in
172 let k2, n2 = resolve_level st n2 in
173 if n1 = n2 then true else
175 if not n1.b || assert_not_zero st n2 then match n1.v with
176 | Inf -> assert_infinite st n2
177 | Fin i -> assert_finite st n2 i
179 | Ref _ -> assert false
182 if !G.trace >= level then warn "ASSERT EQUAL";
183 if b && k1 <> J.null_mark && k2 <> J.null_mark then begin
184 n1.v <- Ref (k2, 0); if !G.trace >= level then pp_table st