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 layer *)
19 | Fin of int (* finite layer *)
20 | Ref of P.mark * int (* referred layer, step *)
21 | Unk (* no layer set *)
24 mutable v: value; (* value *)
25 s: bool; (* static layer? *)
26 mutable b: bool; (* beta allowed? *)
29 type status = (P.mark, layer) KH.t (* environment for layer variables *)
31 (* Internal functions *******************************************************)
37 let warn s = L.warn (pred level) s
41 let string_of_value k = function
43 | Fin i -> string_of_int i
44 | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i
45 | Unk -> "-" ^ P.string_of_mark k
49 (* Note: remove assigned variables *)
52 warn (Printf.sprintf "%s: v %s (s:%b b:%b)"
53 (P.string_of_mark k) (string_of_value k n.v) n.s n.b
61 v = v; s = s; b = false
64 let empty () = cell true Unk
66 let dynamic k i = cell false (Ref (k, i))
68 let find_with_default st default k =
69 try KH.find st k with Not_found -> KH.add st k default; default
72 try KH.find st k with Not_found -> assert false
74 let rec resolve_key_with_default st default k = match find_with_default st default k with
75 | {v = Ref (k, i)} when i = 0 -> resolve_key_with_default st default k
78 let rec resolve_key st k = match find st k with
79 | {v = Ref (k, i)} when i = 0 -> resolve_key st k
82 let resolve_layer st = function
83 | {v = Ref (k, i)} when i = 0 -> resolve_key st k
84 | cell -> P.null_mark, cell
86 let rec generated st h i =
87 let default = dynamic h i in
88 let k = P.new_mark () in
89 let k, n = resolve_key_with_default st default k in
90 if n.s then generated st h i else begin
91 if n <> default then KH.replace st k default;
93 if !G.ct >= level then pp_table st
98 let assert_finite st n j =
100 if !G.ct >= level then warn (Printf.sprintf "ASSERT FINITE %u" j)
102 let rec aux (k, n) j = match n.v with
103 | Fin i when i = j -> true
105 Printf.printf "binder %s is %u but must be %u\n" (P.string_of_mark k) i j; true (**)
107 Printf.printf "binder %s is infinite but must be %u\n" (P.string_of_mark k) j; true (**)
111 if !G.ct >= level then pp_table st
114 | Ref (k, i) -> n.v <- Fin j; aux (resolve_key st k) (i+j)
116 let k, n = resolve_layer st n in
117 (* if j = 0 && n.b then begin
118 Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false (**)
122 let assert_infinite st n =
124 if !G.ct >= level then warn "ASSERT INFINITE"
126 let rec aux (k, n) = match n.v with
129 Printf.printf "binder %s is %u but must be infinite\n" (P.string_of_mark k) i; true (**)
133 if !G.ct >= level then pp_table st
136 | Ref (k, _) -> n.v <- Inf; aux (resolve_key st k)
138 aux (resolve_layer st n)
140 (* Interface functions ******************************************************)
142 let initial_status () =
145 let refresh_status st = st
147 let infinity = cell true Inf
149 let finite i = cell true (Fin i)
157 if !G.ct >= level then warn "UNKNOWN"
159 let default = empty () in
160 let k = P.new_mark () in
161 let k, n = resolve_key_with_default st default k in
162 if n.s then match n.v with
167 if !G.ct >= level then pp_table st
169 cell true (Ref (k, 0))
170 | Ref _ -> assert false
175 if !G.ct >= level then warn (Printf.sprintf "MINUS %u" j)
177 let rec aux k n j = match n.v with
178 | Inf -> cell false n.v
179 | Fin i when i > j -> cell false (Fin (i - j))
180 | Fin _ -> cell false zero
182 if k = P.null_mark then assert false else generated st k j
184 let k, n = resolve_key st k in
187 let k, n = resolve_layer st n in
191 let k, n = resolve_layer st n in
192 string_of_value k n.v
194 let assert_not_zero st n =
196 if !G.ct >= level then warn "ASSERT NOT ZERO"
198 let k, n = resolve_layer st n in
201 (* | _ , Fin i when i = 0 ->
202 Printf.printf "^Pi reduction on binder %s\n" (P.string_of_mark k); false *) (**)
203 (* if n.s && n.v = Fin 1 then Printf.printf "Pi reduction on binder %s\n" (P.string_of_mark k); *)
207 if !G.ct >= level then pp_table st
211 let assert_zero st n = assert_finite st n 0
213 let assert_equal st n1 n2 =
214 let k1, n1 = resolve_layer st n1 in
215 let k2, n2 = resolve_layer st n2 in
216 if n1 = n2 then true else
218 if not n1.b || assert_not_zero st n2 then match n1.v with
219 | Inf -> assert_infinite st n2
220 | Fin i -> assert_finite st n2 i
222 | Ref _ -> assert false
226 if !G.ct >= level then warn "ASSERT EQUAL"
228 if b && k1 <> P.null_mark && k2 <> P.null_mark then begin
231 if !G.ct >= level then pp_table st
235 let is_not_zero st n =
236 (* let _, n = resolve_layer st n in *) n.v <> zero
238 let are_equal st n1 n2 =
240 let _, n1 = resolve_layer st n1 in
241 let _, n2 = resolve_layer st n2 in