proofs are now built lazily at the end of the computation

[helm.git] / helm / ocaml / paramodulation / inference.mli

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 5ced528bb81055550961d65e489068bded9c49cf..74194e84a0f7aa678d36708d555299a86ef99ef8 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -6,9 +6,16 @@ type equality =
      Utils.comparison) * (* ordering *)  
     Cic.metasenv *       (* environment for metas *)
     Cic.term list        (* arguments *)
-;;
 
-type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
+type proof =
+  | BasicProof of Cic.term
+  | ProofBlock of
+      Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
+        equality
+  | NoProof
+
+
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
 
 
 exception MatchingFailure
@@ -18,7 +25,12 @@ val matching:
   CicUniv.universe_graph ->
   Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
+val unification:
+  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  CicUniv.universe_graph ->
+  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
 
+    
 (**
    Performs the beta expansion of the term "where" w.r.t. "what",
    i.e. returns the list of all the terms t s.t. "(t what) = where".
@@ -82,3 +94,10 @@ val fix_metas: int -> equality -> int * equality
 
 val extract_differing_subterms:
   Cic.term -> Cic.term -> (Cic.term * Cic.term) option
+
+
+val store_proof: equality -> proof -> unit
+
+val delete_proof: equality -> unit
+
+val build_term_proof: equality -> Cic.term