adding library support (not ready yet)

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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 38bc6abe54ca24196cfdfcf40bee65db1ce9eefd..1252c6069cd3664a492c52b0c6a358127a99f3be 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1117,6 +1117,66 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 ;;
 
 
+let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta = 
+  let module C = Cic in
+  let module S = CicSubstitution in
+  let module T = CicTypeChecker in
+  let candidates =
+    List.map
+      (fun uri ->
+         let t = CicUtil.term_of_uri uri in
+         let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+         t, ty)
+      (MetadataQuery.equations_for_goal ~dbd status)
+  in
+  let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
+  and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
+  let iseq uri =
+    uri == eq_uri1 || uri == eq_uri2
+  in
+  let rec aux newmeta = function
+    | [] -> [], newmeta
+    | (term, termty)::tl ->
+        let res, newmeta = 
+          match termty with
+          | C.Prod (name, s, t) ->
+              let head, newmetas, args, newmeta =
+                ProofEngineHelpers.saturate_term newmeta [] [] termty
+              in
+              let p =
+                if List.length args = 0 then
+                  term
+                else
+                  C.Appl (term::args)
+              in (
+                match head with
+                | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+                    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 proof = BasicProof p in
+                    let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+                    Some e, (newmeta+1)
+                | _ -> None, newmeta
+              )
+          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+              let o = !Utils.compare_terms t1 t2 in
+              let w = compute_equality_weight ty t1 t2 in
+              let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
+              Some e, (newmeta+1)
+          | _ -> None, newmeta
+        in
+        match res with
+        | Some e ->
+            let tl, newmeta' = aux newmeta tl in
+            e::tl, max newmeta newmeta'
+        | None ->
+            aux newmeta tl
+  in
+  aux maxmeta candidates
+;;
+
+
 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
 (*   print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
   let table = Hashtbl.create (List.length args) in
@@ -1667,3 +1727,5 @@ let extract_differing_subterms t1 t2 =
   | hd::[] -> Some hd
   | _ -> None
 ;;
+
+