matitaprover is almost there

[helm.git] / helm / software / components / binaries / matitaprover / matitaprover.ml

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 344db716d94661a3f1213cae86bf14852caa77fd..5a438c7b6fa700d9a139669b32765db58530bb60 100644 (file)
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -1,23 +1,60 @@
 let main () =
-  let problem_file = ref "" in
+  let problem_file = ref "no-file-given" in
+  let tptppath = ref "./" in
   Arg.parse [
+   "--tptppath", Arg.String (fun p -> tptppath := p), "[path]  TPTP lib root"
    ] (fun x -> problem_file := x) "matitaprover [problemfile]";
-  let hypotheses, goal = Tptp_cnf.parse !problem_file in
-  let module B : Terms.Blob = struct
-        type t = Ast.atom
+  let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
+  let goal = match goals with [x] -> x | _ -> assert false in
+  let module B : Terms.Blob with type t = Ast.term = struct
+        type t = Ast.term
         let eq a b = a = b
         let compare = Pervasives.compare
-        let eqP = Ast.True
-        let pp x = ""
-        let embed x = Terms.Var 0
-        let saturate x y = Terms.Var 0,Terms.Var 0
+        let eqP = Ast.Constant "=="
+        let pp = function
+          | Ast.Constant x -> x
+          | Ast.Variable _ -> assert false
+          | Ast.Function _ -> assert false
+        ;;
+        let embed x = 
+          let rec aux m = function
+            | Ast.Variable name ->
+                (try m, List.assoc name m
+                 with Not_found -> 
+                    let t = Terms.Var (List.length m) in
+                    (name,t)::m, t)
+            | Ast.Constant _ as t -> m, Terms.Leaf t
+            | Ast.Function (name,args) -> 
+                let m, args = 
+                  HExtlib.list_mapi_acc 
+                    (fun x _ m -> aux m x) m args
+                in
+                m, Terms.Node (Terms.Leaf (Ast.Constant name):: args) 
+          in
+            aux [] x
+        ;;
+        let saturate bo ty = 
+          let vars, ty = embed ty in
+          let _, bo = embed bo in
+          let bo = Terms.Node (bo :: List.map snd (List.rev vars)) in
+          bo, ty
+        ;;
+        let embed t = snd(embed t);;
+
   end
   in
   let module P = Paramod.Paramod(B) in
+  let module Pp = Pp.Pp(B) in
   let bag = Terms.M.empty, 0 in
-  let g_passives = assert false in
-  let passives = assert false in
-  ignore(P.paramod bag ~g_passives ~passives);
+  let bag, g_passives = P.mk_goal bag goal in
+  let bag, passives = 
+    HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
+  in
+  prerr_endline "Facts";
+  prerr_endline (String.concat "\n" (List.map Pp.pp_unit_clause passives));
+  prerr_endline "Goal";
+  prerr_endline (Pp.pp_unit_clause g_passives);
+  ignore(P.paramod bag ~g_passives:[g_passives] ~passives);
   ()
 ;;