adding library support (not ready yet)

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

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index a6c4fc8adf0fe614be3e204bc1783f096805df67..94f26a7e68c5c58c59d9fdf5ecbc906edf2ca5eb 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -986,9 +986,7 @@ let rec given_clause_fullred env passive active =
 ;;
 
 
-let get_from_user () =
-  let dbd = Mysql.quick_connect
-    ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
+let get_from_user ~(dbd:Mysql.dbd) =
   let rec get () =
     match read_line () with
     | "" -> []
@@ -1010,7 +1008,9 @@ let main () =
   let module T = CicTypeChecker in
   let module PET = ProofEngineTypes in
   let module PP = CicPp in
-  let term, metasenv, ugraph = get_from_user () in
+  let dbd = Mysql.quick_connect
+    ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
+  let term, metasenv, ugraph = get_from_user ~dbd in
   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
   let proof, goals = status in
@@ -1018,6 +1018,8 @@ let main () =
   let _, metasenv, meta_proof, _ = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
   let equalities, maxm = find_equalities context proof in
+  let library_equalities, maxm =
+    find_library_equalities ~dbd (proof, goal') (maxm+1) in
   maxmeta := maxm+2; (* TODO ugly!! *)
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let new_meta_goal, metasenv, type_of_goal =
@@ -1113,6 +1115,81 @@ let main () =
 ;;
 
 
+let saturation_tactic status =
+  let module C = Cic in
+  let saturation_tac (proof, goal) =
+    maxmeta := 0;
+(*     if List.length goals <> 1 then *)
+(*       raise (ProofEngineTypes.Fail "There should be only one open goal"); *)
+    
+(*     let goal' = List.hd goals in *)
+    let goal' = goal in
+    let uri, metasenv, meta_proof, term_to_prove = proof in
+    let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+    let equalities, maxm = find_equalities context proof in
+    maxmeta := maxm+2;
+    let new_meta_goal, metasenv, type_of_goal =
+      let irl =
+        CicMkImplicit.identity_relocation_list_for_metavariable context in
+      let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+      Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
+      print_newline ();
+      Cic.Meta (maxm+1, irl),
+      (maxm+1, context, ty)::metasenv,
+      ty
+    in
+    let ugraph = CicUniv.empty_ugraph in
+    let env = (metasenv, context, ugraph) in
+    try
+      let term_equality = equality_of_term new_meta_goal goal in
+(*       let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *)
+      let active = make_active () in
+      let passive = make_passive [term_equality] equalities in
+      let res = given_clause_fullred env passive active in
+      match res with
+      | Success (Some goal, env) ->
+          Printf.printf "OK, found a proof!\n";
+          let proof = Inference.build_proof_term goal in         
+          let names = names_of_context context in
+          print_endline (CicPp.pp proof names);
+          let newmetasenv =
+            let i1 =
+              match new_meta_goal with
+              | C.Meta (i, _) -> i | _ -> assert false
+            in
+            let i2 =
+              match meta_proof with
+              | C.Meta (i, _) -> i | _ -> assert false
+            in
+            List.filter (fun (i, _, _) -> i <> i1 && i <> i2) metasenv
+          in
+          let newstatus =
+            try
+              let ty, ug =
+                CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+              in
+              Printf.printf
+                "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
+                (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+                (string_of_bool
+                   (fst (CicReduction.are_convertible
+                           context type_of_goal ty ug)));
+              ((uri, newmetasenv, proof, term_to_prove), [])
+            with e ->
+              raise (ProofEngineTypes.Fail
+                       "Found a proof, but it doesn't typecheck")
+          in
+          newstatus          
+      | _ ->
+          raise (ProofEngineTypes.Fail "NO proof found")
+    with e ->
+      raise (ProofEngineTypes.Fail "saturation failed")
+  in
+  ProofEngineTypes.mk_tactic saturation_tac
+;;
+
+
+
 let configuration_file = ref "../../matita/matita.conf.xml";;
 
 let _ =