helm/software/lambda-delta/lib/hierarchy.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 module S = Scanf
  14 module C = Cps
  15
  16 type graph = string * (int -> int)
  17
  18 let sorts = 2
  19 let sort = H.create sorts
  20 let index = ref 0
  21
  22 (* Internal functions *******************************************************)
  23
  24 let set_sort f (h:int) (s:string) =
  25    H.add sort h s; f (succ h)
  26
  27 (* Interface functions ******************************************************)
  28
  29 let set_new_sorts f ss =
  30    let f i = index := i; f i in
  31    C.list_fold_left f set_sort !index ss
  32
  33 let get_sort f h =
  34    try f (Some (H.find sort h))
  35    with Not_found -> f None
  36
  37 let string_of_graph f (s, _) = f s
  38
  39 let apply f (_, g) h = f (g h)
  40
  41 let graph_of_string f s =
  42    try
  43       let x = S.sscanf s "Z%u" C.start in
  44       if x > 0 then f (Some (s, fun h -> x + h)) else f None
  45    with
  46       S.Scan_failure _ | Failure _ | End_of_file -> f None
  47
  48 let graph =
  49    ref (graph_of_string (function Some g -> g | None -> assert false) "Z2")