the tactic now returns as open goals the open metas in the proof

[helm.git] / helm / software / components / tactics / paramodulation / inference.mli

diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index b31d8bacff7dc10b2f69eb5427f53498afdae7fa..b08054ca4f2c90c72dc97ade2d53e493b8ed0260 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/components/tactics/paramodulation/inference.mli
@@ -23,6 +23,11 @@
  * http://cs.unibo.it/helm/.
  *)
 
+val metas_of_proof_time : float ref
+
+(* type substitution = Cic.substitution *)
+type substitution = (int * Cic.term) list 
+
 type equality =
     int *                (* weight *)
     proof *              (* proof *)
@@ -30,14 +35,13 @@ type equality =
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
+    Cic.metasenv        (* environment for metas *)
 
 and proof =
   | NoProof   (* no proof *)
-  | BasicProof of Cic.term (* already a proof of a goal *)
+  | BasicProof of substitution * Cic.term (* already a proof of a goal *)
   | ProofBlock of (* proof of a rewrite step *)
-      Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
+      substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof
       (* proof of the new meta, proof of the goal from which this comes *)
@@ -52,22 +56,24 @@ val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
 
 val string_of_proof: proof -> string
 
+val filter : substitution -> Cic.metasenv -> Cic.metasenv
+
 exception MatchingFailure
 
 (** matching between two terms. Can raise MatchingFailure *)
 val matching:
-  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+  substitution * Cic.metasenv * CicUniv.universe_graph
 
 (**
    special unification that checks if the two terms are "simple", and in
    such case should be significantly faster than CicUnification.fo_unif
 *)
 val unification:
-  Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+  substitution * Cic.metasenv * CicUniv.universe_graph
 
     
 (**
@@ -128,7 +134,13 @@ val is_identity: environment -> equality -> bool
 
 val string_of_equality: ?env:environment -> equality -> string
 
+
 val metas_of_term: Cic.term -> int list
+val metas_of_proof: proof -> int list
 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality
+
+val apply_subst: substitution -> Cic.term -> Cic.term
+val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
+val ppsubst: substitution -> string