the prover is almost OK, types in fuctors a bit extended to

[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 5a438c7b6fa700d9a139669b32765db58530bb60..b80091e810701b15ad5cb0b0b300e8772e3143a3 100644 (file)
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -1,3 +1,22 @@
+module OT = struct type t = string  let compare = Pervasives.compare end 
+module HC = Map.Make(OT)
+
+type leaf = int * string
+
+let cache = ref HC.empty 
+let num = ref 100
+
+let hash s = 
+  try HC.find s !cache
+  with Not_found ->
+          cache := HC.add s (!num,s) !cache;
+          decr num;
+          HC.find s !cache
+;;
+
+hash "==";;
+hash "_";;
+
 let main () =
   let problem_file = ref "no-file-given" in
   let tptppath = ref "./" in
@@ -6,40 +25,34 @@ let main () =
    ] (fun x -> problem_file := x) "matitaprover [problemfile]";
   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.Constant "=="
-        let pp = function
-          | Ast.Constant x -> x
-          | Ast.Variable _ -> assert false
-          | Ast.Function _ -> assert false
-        ;;
-        let embed x = 
-          let rec aux m = function
+  let module B : Terms.Blob with type t = leaf and type input = Ast.term = struct
+        type t = leaf
+        let eq a b = a == b
+        let compare (a,_) (b,_) = Pervasives.compare a b
+        let eqP = hash "=="
+        let pp (_,a) =  a 
+        type input = Ast.term
+        let rec embed m = function
             | Ast.Variable name ->
                 (try m, List.assoc name m
                  with Not_found -> 
-                    let t = Terms.Var (List.length m) in
+                    let t = Terms.Var ~-(List.length m) in
                     (name,t)::m, t)
-            | Ast.Constant _ as t -> m, Terms.Leaf t
+            | Ast.Constant name -> m, Terms.Leaf (hash name)
             | Ast.Function (name,args) -> 
                 let m, args = 
                   HExtlib.list_mapi_acc 
-                    (fun x _ m -> aux m x) m args
+                    (fun x _ m -> embed m x) m args
                 in
-                m, Terms.Node (Terms.Leaf (Ast.Constant name):: args) 
-          in
-            aux [] x
+                m, Terms.Node (Terms.Leaf (hash name):: args) 
         ;;
         let saturate bo ty = 
-          let vars, ty = embed ty in
-          let _, bo = embed bo in
+          let vars, ty = embed [] ty in
+          let _, bo = embed vars bo in
           let bo = Terms.Node (bo :: List.map snd (List.rev vars)) in
           bo, ty
         ;;
-        let embed t = snd(embed t);;
+        let embed t = snd(embed [] t);;
 
   end
   in
@@ -50,10 +63,12 @@ let main () =
   let bag, passives = 
     HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
   in
+  prerr_endline "Order";
+  HC.iter (fun _ (w,x) -> prerr_endline (" " ^ x ^ " is " ^ string_of_int w)) !cache;
   prerr_endline "Facts";
-  prerr_endline (String.concat "\n" (List.map Pp.pp_unit_clause passives));
+  List.iter (fun x -> prerr_endline (" " ^ Pp.pp_unit_clause x)) passives;
   prerr_endline "Goal";
-  prerr_endline (Pp.pp_unit_clause g_passives);
+  prerr_endline (" " ^ Pp.pp_unit_clause g_passives);
   ignore(P.paramod bag ~g_passives:[g_passives] ~passives);
   ()
 ;;