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   ?uri:UriManager.uri ->
  47   unit ->
  48     universe
  49
  50 (*
  51   really useful at the begin and in all the functions that don't care
  52   of universes
  53 *)
  54 val empty_ugraph: universe_graph
  55
  56 (*
  57   These are the real functions to add eq/ge/gt constraints
  58   to the passed graph, returning an updated graph or raising
  59   UniverseInconsistency
  60 *)
  61 val add_eq:
  62   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
  63 val add_ge:
  64   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
  65 val add_gt:
  66   ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
  67
  68 (*
  69   debug function to print the graph to standard error
  70 *)
  71 val print_ugraph:
  72   universe_graph -> unit
  73
  74 (*
  75   does what expected, but I don't remember why this was exported
  76 *)
  77 val string_of_universe:
  78   universe -> string
  79
  80 (*
  81   given the list of visible universes (see universes_of_obj) returns a
  82   cleaned graph (cleaned from the not visible nodes)
  83 *)
  84 val clean_ugraph:
  85   universe_graph -> universe list -> universe_graph
  86
  87 (*
  88   Since fresh() can't add the right uri to each node, you
  89   must fill empty nodes with the uri before you serialize the graph to xml
  90 *)
  91 val fill_empty_nodes_with_uri:
  92   universe_graph -> UriManager.uri -> universe_graph
  93
  94 (*
  95   makes a union.
  96   TODO:
  97   - remember already merged uri so that we completely skip already merged
  98     graphs, this may include a dependecy graph (not merge a subpart of an
  99     already merged graph)
 100 *)
 101 val merge_ugraphs:
 102   universe_graph -> universe_graph -> universe_graph
 103
 104 (*
 105   ugraph to xml file and viceversa
 106 *)
 107 val write_xml_of_ugraph:
 108   string -> universe_graph -> unit
 109
 110 (*
 111   given a filename parses the xml and returns the data structure
 112 *)
 113 val ugraph_of_xml:
 114   string -> universe_graph
 115 val restart_numbering:
 116   unit -> unit
 117
 118   (** re-hash-cons URIs contained in the given universe so that phisicaly
 119    * equality could be enforced. Mainly used by
 120    * CicEnvironment.restore_from_channel *)
 121 val recons_graph: universe_graph -> universe_graph
 122
 123   (** re-hash-cons a single universe *)
 124 val recons_univ: universe -> universe
 125
 126   (** consistency chek that should be done before committin the graph to the
 127    * cache *)
 128 val assert_univs_have_uri: universe_graph -> unit
 129
 130   (** asserts the univers is named *)
 131 val assert_univ: universe -> unit
 132
 133 (*
 134   Benchmarking stuff
 135 *)
 136 val get_spent_time: unit -> float
 137 val reset_spent_time: unit -> unit