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 level = Inf (* infinite *)
17 | Fin of int (* finite *)
18 | Ref of J.mark (* unknown *)
20 type const = NotZero (* not zero: beta and whnf allowed *)
22 type contents = Value of level (* defined with this level *)
23 | Const of const list (* undefined with these constraints *)
25 type status = (J.mark, contents) H.t (* environment for level variables *)
27 (* Internal functions *******************************************************)
31 let empty_ref = Const []
34 try H.find st k with Not_found -> H.add st k empty_ref; empty_ref
36 let rec resolve st k = match find st k with
37 | Value (Ref k) -> resolve st k
40 (* Interface functions ******************************************************)
42 let initial_status () =
55 let unknown st k = match resolve st k with
62 let minus n j = match n with
64 | Fin i when i > j -> Fin (i - j)
66 | Ref i -> Inf (* assert false *)
68 let to_string = function
70 | Fin i -> string_of_int i
71 | Ref k -> "-" ^ J.to_string k