Added recursive path ordering and demodulation tactic.

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

diff --git a/helm/ocaml/tactics/paramodulation/inference.ml b/helm/ocaml/tactics/paramodulation/inference.ml
index 6c2a9b9dccfa83788706545862bc82c86690c8ba..f22b49ceedfbb1e15345f37a1594b546a14a6a81 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/inference.ml
+++ b/helm/ocaml/tactics/paramodulation/inference.ml
@@ -39,7 +39,7 @@ type equality =
     Cic.term list        (* arguments *)
 
 and proof =
-  | NoProof
+  | NoProof (* term is the goal missing a proof *)
   | BasicProof of Cic.term
   | ProofBlock of
       Cic.substitution * UriManager.uri *
@@ -70,7 +70,7 @@ let string_of_equality ?env =
 
 
 let rec string_of_proof = function
-  | NoProof -> "NoProof"
+  | NoProof -> "NoProof " 
   | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
   | SubProof (t, i, p) ->
       Printf.sprintf "SubProof(%s, %s, %s)"
@@ -101,12 +101,12 @@ let build_ens_for_sym_eq sym_eq_URI termlist =
 ;;
 
 
-let build_proof_term proof =
+let build_proof_term ?(noproof=Cic.Implicit None) proof =
   let rec do_build_proof proof = 
     match proof with
     | NoProof ->
         Printf.fprintf stderr "WARNING: no proof!\n";
-        Cic.Implicit None
+        noproof
     | BasicProof term -> term
     | ProofGoalBlock (proofbit, proof) ->
         print_endline "found ProofGoalBlock, going up...";
@@ -191,11 +191,6 @@ exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
   let module C = Cic in
-  let print_table t =
-    String.concat ", "
-      (List.map
-         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
-  in
   let rec aux ((table_l, table_r) as table) t1 t2 =
     match t1, t2 with
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
@@ -309,16 +304,11 @@ let meta_convertibility_eq eq1 eq2 =
 
 
 let meta_convertibility t1 t2 =
-  let f t =
-    String.concat ", "
-      (List.map
-         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
-  in
   if t1 = t2 then
     true
   else
     try
-      let l, r = meta_convertibility_aux ([], []) t1 t2 in
+      ignore(meta_convertibility_aux ([], []) t1 t2);
       true
     with NotMetaConvertible ->
       false
@@ -648,7 +638,6 @@ let find_library_equalities dbd context status maxmeta =
   let candidates =
     List.fold_left
       (fun l uri ->
-       let suri = UriManager.string_of_uri uri in
          if UriManager.UriSet.mem uri blacklist then
            l
          else
@@ -806,7 +795,7 @@ let find_context_hypotheses env equalities_indexes =
 ;;
 
 
-let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
+let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
   let table = Hashtbl.create (List.length args) in
   let newargs, newmeta =
     List.fold_right
@@ -866,7 +855,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
         (Hashtbl.copy table)
   in
   let rec fix_proof = function
-    | NoProof -> NoProof
+    | NoProof -> NoProof 
     | BasicProof term -> BasicProof (repl term)
     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
         let subst' =
@@ -922,8 +911,8 @@ let equality_of_term proof term =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 
-let is_identity ((metasenv, context, ugraph) as env) = function
-  | ((_, _, (ty, left, right, _), menv, _) as equality) ->
+let is_identity (metasenv, context, ugraph) = function
+  | (_, _, (ty, left, right, _), menv, _) ->
        (left = right ||
           (* (meta_convertibility left right) || *)
           (fst (CicReduction.are_convertible