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_______________________________________________________________ *)
16 type value = Inf (* infinite level *)
17 | Fin of int (* finite level *)
18 | Ref of J.mark (* referred level *)
20 type level = bool * value (* static level? value *)
22 type const = NotZero (* not zero: beta allowed *)
24 type contents = Value of value (* defined with this level *)
25 | Const of const list (* undefined with these constraints *)
27 type status = (J.mark, contents) H.t (* environment for level variables *)
29 (* Internal functions *******************************************************)
33 let empty_ref = Const []
38 try H.find st k with Not_found -> H.add st k empty_ref; empty_ref
40 let rec resolve st k = match find st k with
41 | Value (Ref k) -> resolve st k
44 (* Interface functions ******************************************************)
46 let initial_status () =
49 let infinite = true, Inf
55 let finite i = true, Fin i
57 let unknown st k = match resolve st k with
58 | _, Value l -> true, l
59 | k, Const _ -> true, Ref k
61 let to_string = function
63 | _, Fin i -> string_of_int i
64 | _, Ref k -> "-" ^ J.to_string k
68 match resolve st k with
70 if i <> j then Printf.printf "%s is %u but it must be %u\n" (to_string l) i j;
73 Printf.printf "%s is infinite but it must be %u\n" j;
80 let minus n j = match n with
81 | _, Inf -> false, Inf
82 | _, Fin i when i > j -> false, Fin (i - j)
83 | _, Fin _ -> false, zero
84 | _, Ref i -> false, Inf (* assert false *)