fixed bug in proof generation, new weight function to sort equalities, which

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index f5233d03dbab9e907e5c02711729023019b32afa..fad86a854aeec9f7db327e70ba0dfec5cee78de8 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -3,20 +3,21 @@ open Utils;;
 
 type equality =
     int  *               (* weight *)
+    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 =
+and proof =
   | BasicProof of Cic.term
   | ProofBlock of
-      Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
-        equality
+      Cic.substitution * UriManager.uri *
+        (* name, ty, eq_ty, left, right *)
+        (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * 
+        (Utils.pos * equality) * equality
   | NoProof
 ;;
 
@@ -25,40 +26,25 @@ let string_of_equality ?env =
   match env with
   | None -> (
       function
-        | _, (ty, left, right, o), _, _ ->
-            Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
+        | w, _, (ty, left, right, o), _, _ ->
+            Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
     )
   | Some (_, context, _) -> (
       let names = names_of_context context in
       function
-        | _, (ty, left, right, o), _, _ ->
-            Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
+        | w, _, (ty, left, right, o), _, _ ->
+            Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
               (CicPp.pp left names) (string_of_comparison o)
               (CicPp.pp right names)
     )
 ;;
 
 
-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
+  let _, proof, _, _, _ = equality in
   match proof with
   | NoProof ->
       Printf.fprintf stderr "WARNING: no proof for %s\n"
@@ -66,12 +52,18 @@ let rec build_term_proof equality =
       Cic.Implicit None
   | BasicProof term -> term
   | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
+      let name, ty, eq_ty, left, right = t' in
+      let bo =
+        Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+                  eq_ty; left; right]
+      in
+      let t' = Cic.Lambda (name, ty, CicSubstitution.lift 1 bo) in
 (*       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 _, _, (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;
@@ -220,8 +212,8 @@ let meta_convertibility_aux table t1 t2 =
 
 
 let meta_convertibility_eq eq1 eq2 =
-  let _, (ty, left, right, _), _, _ = eq1
-  and _, (ty', left', right', _), _, _ = eq2 in
+  let _, _, (ty, left, right, _), _, _ = eq1
+  and _, _, (ty', left', right', _), _, _ = eq2 in
   if ty <> ty' then
     false
   else if (left = left') && (right = right') then
@@ -1027,8 +1019,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
-                    let e = (w, (ty, t1, t2, o), newmetas, args) in
-                    store_proof e (BasicProof p);
+                    let proof = BasicProof p in
+                    let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -1037,8 +1029,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
               and t2 = S.lift index t2 in
               let o = !Utils.compare_terms t1 t2 in
               let w = compute_equality_weight ty t1 t2 in
-              let e = (w, (ty, t1, t2, o), [], []) in
-              store_proof e (BasicProof (C.Rel index));
+              let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -1056,7 +1047,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 ;;
 
 
-let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
+let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
   let table = Hashtbl.create (List.length args) in
   let newargs, _ =
     List.fold_right
@@ -1092,7 +1083,7 @@ let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) =
       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
   in
   (newmeta + (List.length newargs) + 1,
-   (weight, (ty, left, right, o), menv', newargs))
+   (w, p, (ty, left, right, o), menv', newargs))
 ;;
 
 
@@ -1102,8 +1093,7 @@ 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
       let w = compute_equality_weight ty t1 t2 in
-      let e = (w, (ty, t1, t2, o), [], []) in
-      store_proof e (BasicProof proof);
+      let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
       e
 (*       (proof, (ty, t1, t2, o), [], []) *)
   | _ ->
@@ -1320,16 +1310,9 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
 
 
 let is_identity ((_, context, ugraph) as env) = function
-  | ((_, (ty, left, right, _), _, _) as equality) ->
-      let res =
-        (left = right ||
-            (fst (CicReduction.are_convertible context left right ugraph)))
-      in
-(*       if res then ( *)
-(*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
-(*         print_newline (); *)
-(*       ); *)
-      res
+  | ((_, _, (ty, left, right, _), _, _) as equality) ->
+      (left = right ||
+          (fst (CicReduction.are_convertible context left right ugraph)))
 ;;