]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUniv.mli
parameter sintax added to axiom statement
[helm.git] / helm / software / components / cic / cicUniv.mli
index 288efe616885b833ceedb5984af376fda2f8b2ae..8a24614c2a814482838d09be95c148ebd179d52a 100644 (file)
@@ -57,17 +57,27 @@ val name_universe: universe -> UriManager.uri -> universe
 *)
 val empty_ugraph: universe_graph
 
+(* an universe that does nothing: i.e. no constraints are kept, no merges.. *)
+val oblivion_ugraph: universe_graph
+
+(* one of the previous two, no set to empty_ugraph *)
+val default_ugraph: universe_graph
+
+
 (*
   These are the real functions to add eq/ge/gt constraints 
   to the passed graph, returning an updated graph or raising
   UniverseInconsistency
 *)
 val add_eq: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  universe -> universe -> universe_graph -> universe_graph
 val add_ge: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  universe -> universe -> universe_graph -> universe_graph
 val add_gt: 
-  ?fast:bool -> universe -> universe -> universe_graph -> universe_graph
+  universe -> universe -> universe_graph -> universe_graph
+
+val do_rank: universe_graph -> int list * universe list
+val get_rank: universe -> int
 
 (*
   debug function to print the graph to standard error
@@ -127,6 +137,7 @@ val restart_numbering:
   returns the universe number (used to save it do xml) 
 *) 
 val univno: universe -> int 
+val univuri: universe -> UriManager.uri
 
   (** re-hash-cons URIs contained in the given universe so that phisicaly
    * equality could be enforced. Mainly used by
@@ -146,9 +157,4 @@ val assert_univ: universe -> unit
 val compare: universe -> universe -> int
 val eq: universe -> universe -> bool
 
-(*
-  Benchmarking stuff
-*)
-val get_spent_time: unit -> float
-val reset_spent_time: unit -> unit
-
+val is_anon: universe -> bool