(* ||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 KH = Hashtbl module KS = Scanf module C = Cps type graph = string * (int -> int) let sorts = 3 let sort = KH.create sorts let default_graph = "Z1" (* Internal functions *******************************************************) let set_sort h s = KH.add sort h s; succ h let graph_of_string err f s = try let x = KS.sscanf s "Z%u" C.start in if x > 0 then f (s, fun h -> x + h) else err () with KS.Scan_failure _ | Failure _ | End_of_file -> err () let graph = ref (graph_of_string C.err C.start default_graph) (* Interface functions ******************************************************) let set_sorts i ss = List.fold_left set_sort i ss let string_of_sort err f h = try f (KH.find sort h) with Not_found -> err () let sort_of_string err f s = let map h n = function | None when n = s -> Some h | xh -> xh in match KH.fold map sort None with | None -> err () | Some h -> f h let string_of_graph () = fst !graph let apply h = snd !graph h let set_graph s = let err () = false in let f g = graph := g; true in graph_of_string err f s let clear () = KH.clear sort; graph := graph_of_string C.err C.start default_graph