helm/ocaml/cic/cicUniv.mli

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26
  27 (*
  28   The strings contains an unreadable message
  29 *)
  30 exception UniverseInconsistency of string
  31
  32 (*
  33   Cic.Type of universe
  34 *)
  35 type universe
  36
  37 (*
  38   Opaque data structure you will use to store constraints
  39 *)
  40 type universe_graph
  41
  42 (*
  43   returns a fresh universe
  44 *)
  45 val fresh:
  46   unit -> universe
  47
  48 (*
  49   really useful at the begin and in all the functions that don't care
  50   of universes
  51 *)
  52 val empty_ugraph: universe_graph
  53
  54 (*
  55   These are the real functions to add eq/ge/gt constraints
  56   to the passed graph, returning an updated graph or raising
  57   UniverseInconsistency
  58 *)
  59 val add_eq:
  60   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
  61 val add_ge:
  62   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
  63 val add_gt:
  64   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
  65
  66 (*
  67   debug function to print the graph to standard error
  68 *)
  69 val print_ugraph:
  70   universe_graph -> unit
  71
  72 (*
  73   does what expected, but I don't remember why this was exported
  74 *)
  75 val string_of_universe:
  76   universe -> string
  77
  78 (*
  79   given the list of visible universes (see universes_of_obj) returns a
  80   cleaned graph (cleaned from the not visible nodes)
  81 *)
  82 val clean_ugraph:
  83   universe_graph -> universe list -> universe_graph
  84
  85 (*
  86   Since fresh() can't add the right uri to each node, you
  87   must fill empty nodes with the uri before you serialize the graph to xml
  88 *)
  89 val fill_empty_nodes_with_uri:
  90   universe_graph -> UriManager.uri -> universe_graph
  91
  92 (*
  93   makes a union.
  94   TODO:
  95   - remember already merged uri so that we completely skip already merged
  96     graphs, this may include a dependecy graph (not merge a subpart of an
  97     already merged graph)
  98 *)
  99 val merge_ugraphs:
 100   universe_graph -> universe_graph -> universe_graph
 101
 102 (*
 103   ugraph to xml file and viceversa
 104 *)
 105 val write_xml_of_ugraph:
 106   string -> universe_graph -> unit
 107
 108 (*
 109   given a filename parses the xml and returns the data structure
 110 *)
 111 val ugraph_of_xml:
 112   string -> universe_graph
 113 val restart_numbering:
 114   unit -> unit
 115
 116   (** re-hash-cons URIs contained in the given universe so that phisicaly
 117    * equality could be enforced. Mainly used by
 118    * CicEnvironment.restore_from_channel *)
 119 val recons_graph: universe_graph -> universe_graph
 120
 121   (** consistency chek that should be done before committin the graph to the
 122    * cache *)
 123 val assert_univs_have_uri: universe_graph -> unit
 124
 125 (*
 126   Benchmarking stuff
 127 *)
 128 val get_spent_time: unit -> float
 129 val reset_spent_time: unit -> unit