helm/software/helena/src/common/level.ml

   1 (*
   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.
   5     ||I||
   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_______________________________________________________________ *)
  11
  12 module H = Hashtbl
  13
  14 module J = Marks
  15
  16 type level = Inf           (* infinite *)
  17            | Fin of int    (* finite *)
  18            | Ref of J.mark (* unknown *)
  19
  20 type const = NotZero (* not zero: beta and whnf allowed *)
  21
  22 type contents = Value of level       (* defined with this level *)
  23               | Const of const list  (* undefined with these constraints *)
  24
  25 type status = (J.mark, contents) H.t (* environment for level variables *)
  26
  27 (* Internal functions *******************************************************)
  28
  29 let env_size = 2000
  30
  31 let empty_ref = Const []
  32
  33 let find st k =
  34    try H.find st k with Not_found -> H.add st k empty_ref; empty_ref
  35
  36 let rec resolve st k = match find st k with
  37    | Value (Ref k) -> resolve st k
  38    | cell          -> k, cell
  39
  40 (* Interface functions ******************************************************)
  41
  42 let initial_status () =
  43    H.create env_size
  44
  45 let infinite = Inf
  46
  47 let zero = Fin 0
  48
  49 let one = Fin 1
  50
  51 let two = Fin 2
  52
  53 let finite i = Fin i
  54
  55 let unknown st k = match resolve st k with
  56    | _, Value l -> l
  57    | k, Const _ -> Ref k
  58
  59 let is_zero l =
  60    l = zero
  61
  62 let minus n j = match n with
  63    | Inf              -> Inf
  64    | Fin i when i > j -> Fin (i - j)
  65    | Fin _            -> zero
  66    | Ref i            -> Inf (* assert false *)
  67
  68 let to_string = function
  69    | Inf   -> ""
  70    | Fin i -> string_of_int i
  71    | Ref k -> "-" ^ J.to_string k