(*
    ||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 value = Inf           (* infinite level *)
           | Fin of int    (* finite level *)
           | Ref of J.mark (* referred level *)

type level = bool * value (* static level? value *)

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

type contents = Value of value       (* 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 = 1300

let empty_ref = Const []

let zero = Fin 0

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 = true, Inf

let one = true, Fin 1

let two = true, Fin 2

let finite i = true, Fin i

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

let to_string = function
   | _, Inf   -> ""
   | _, Fin i -> string_of_int i
   | _, Ref k -> "-" ^ J.to_string k
(*
let is_finite j l =
   let b, k = l in
   match resolve st k with
      | k, Value (Fin i) -> 
         if i <> j then Printf.printf "%s is %u but it must be %u\n" (to_string l) i j;
         i = j
      | k, Value Inf     -> 
         Printf.printf "%s is infinite but it must be %u\n" j;

   | k,  
*)
let is_zero (_, n) =
   n = zero

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