(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

module H = Hashtbl

module J = Marks

type level = Inf           (* infinite *)
           | Fin of int    (* finite *)
           | Ref of J.mark (* unknown *)

type const = NotZero (* not zero: beta and whnf allowed *)

type contents = Value of level       (* defined with this level *)
              | Const of const list  (* undefined with these constraints *)

type status = (J.mark, contents) H.t (* environment for level variables *)

(* Internal functions *******************************************************)

let env_size = 2000

let empty_ref = Const []

let find st k =
   try H.find st k with Not_found -> H.add st k empty_ref; empty_ref 

let rec resolve st k = match find st k with
   | Value (Ref k) -> resolve st k
   | cell          -> k, cell

(* Interface functions ******************************************************)

let initial_status () =
   H.create env_size

let infinite = Inf

let zero = Fin 0

let one = Fin 1

let two = Fin 2

let finite i = Fin i

let unknown st k = match resolve st k with
   | _, Value l -> l
   | k, Const _ -> Ref k

let is_zero l = 
   l = zero

let minus n j = match n with
   | Inf              -> Inf
   | Fin i when i > j -> Fin (i - j)
   | Fin _            -> zero
   | Ref i            -> Inf (* assert false *)

let to_string = function
   | Inf   -> ""
   | Fin i -> string_of_int i
   | Ref k -> "-" ^ J.to_string k