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 value = Inf           (* infinite level *)
  17            | Fin of int    (* finite level *)
  18            | Ref of J.mark (* referred level *)
  19
  20 type level = bool * value (* static level? value *)
  21
  22 type const = NotZero (* not zero: beta allowed *)
  23
  24 type contents = Value of value       (* defined with this level *)
  25               | Const of const list  (* undefined with these constraints *)
  26
  27 type status = (J.mark, contents) H.t (* environment for level variables *)
  28
  29 (* Internal functions *******************************************************)
  30
  31 let env_size = 1300
  32
  33 let empty_ref = Const []
  34
  35 let zero = Fin 0
  36
  37 let find st k =
  38    try H.find st k with Not_found -> H.add st k empty_ref; empty_ref
  39
  40 let rec resolve st k = match find st k with
  41    | Value (Ref k) -> resolve st k
  42    | cell          -> k, cell
  43
  44 (* Interface functions ******************************************************)
  45
  46 let initial_status () =
  47    H.create env_size
  48
  49 let infinite = true, Inf
  50
  51 let one = true, Fin 1
  52
  53 let two = true, Fin 2
  54
  55 let finite i = true, Fin i
  56
  57 let unknown st k = match resolve st k with
  58    | _, Value l -> true, l
  59    | k, Const _ -> true, Ref k
  60
  61 let to_string = function
  62    | _, Inf   -> ""
  63    | _, Fin i -> string_of_int i
  64    | _, Ref k -> "-" ^ J.to_string k
  65 (*
  66 let is_finite j l =
  67    let b, k = l in
  68    match resolve st k with
  69       | k, Value (Fin i) ->
  70          if i <> j then Printf.printf "%s is %u but it must be %u\n" (to_string l) i j;
  71          i = j
  72       | k, Value Inf     ->
  73          Printf.printf "%s is infinite but it must be %u\n" j;
  74
  75    | k,
  76 *)
  77 let is_zero (_, n) =
  78    n = zero
  79
  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 *)