proofs are now built lazily at the end of the computation

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index d8ff4a7d9d116537f963b222f92da5da379c62d0..163fabddbac6ebf6e04eaac05363615b9839ac02 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1,6 +1,26 @@
 open Utils;;
 
 
+type equality =
+    Cic.term  *          (* proof *)
+    (Cic.term *          (* type *)
+     Cic.term *          (* left side *)
+     Cic.term *          (* right side *)
+     Utils.comparison) * (* ordering *)  
+    Cic.metasenv *       (* environment for metas *)
+    Cic.term list        (* arguments *)
+;;
+
+
+type proof =
+  | BasicProof of Cic.term
+  | ProofBlock of
+      Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
+        equality
+  | NoProof
+;;
+
+
 let string_of_equality ?env =
   match env with
   | None -> (
@@ -20,6 +40,45 @@ let string_of_equality ?env =
 ;;
 
 
+let prooftable = Hashtbl.create 2001;;
+
+let store_proof equality proof =
+  if not (Hashtbl.mem prooftable equality) then
+    Hashtbl.add prooftable equality proof
+;;
+
+
+let delete_proof equality =
+(*   Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
+(*   print_newline (); *)
+  Hashtbl.remove prooftable equality
+;;
+
+
+let rec build_term_proof equality =
+(*   Printf.printf "build_term_proof %s" (string_of_equality equality); *)
+(*   print_newline (); *)
+  let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
+  match proof with
+  | NoProof ->
+      Printf.fprintf stderr "WARNING: no proof for %s\n"
+        (string_of_equality equality);
+      Cic.Implicit None
+  | BasicProof term -> term
+  | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
+(*       Printf.printf "   ProofBlock: eq = %s, eq' = %s" *)
+(*         (string_of_equality eq) (string_of_equality eq'); *)
+(*       print_newline (); *)
+      let proof' = build_term_proof eq in
+      let eqproof = build_term_proof eq' in
+      let _, (ty, what, other, _), menv', args' = eq in
+      let what, other = if pos = Utils.Left then what, other else other, what in
+      CicMetaSubst.apply_subst subst
+        (Cic.Appl [Cic.Const (eq_URI, []); ty;
+                   what; t'; eqproof; other; proof'])
+;;
+
+
 let rec metas_of_term = function
   | Cic.Meta (i, c) -> [i]
   | Cic.Var (_, ens) 
@@ -933,17 +992,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
 ;;
 
 
-type equality =
-    Cic.term  *          (* proof *)
-    (Cic.term *          (* type *)
-     Cic.term *          (* left side *)
-     Cic.term *          (* right side *)
-     Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
-;;
-
-
 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -978,14 +1026,18 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
                     let o = !Utils.compare_terms t1 t2 in
-                    Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1)
+                    let e = (p, (ty, t1, t2, o), newmetas, args) in
+                    store_proof e (BasicProof p);
+                    Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
               let t1 = S.lift index t1
               and t2 = S.lift index t2 in
               let o = !Utils.compare_terms t1 t2 in
-              Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1)
+              let e = (C.Rel index, (ty, t1, t2, o), [], []) in
+              store_proof e (BasicProof (C.Rel index));
+              Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
           match do_find context term with
@@ -1047,7 +1099,10 @@ exception TermIsNotAnEquality;;
 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
       let o = !Utils.compare_terms t1 t2 in
-      (proof, (ty, t1, t2, o), [], [])
+      let e = (proof, (ty, t1, t2, o), [], []) in
+      store_proof e (BasicProof proof);
+      e
+(*       (proof, (ty, t1, t2, o), [], []) *)
   | _ ->
       raise TermIsNotAnEquality
 ;;