fork for Matita version B

[helm.git] / matitaB / components / binaries / matitaprover / tptp_cnf.ml

diff --git a/matitaB/components/binaries/matitaprover/tptp_cnf.ml b/matitaB/components/binaries/matitaprover/tptp_cnf.ml
new file mode 100644 (file)
index 0000000..8d3cedf
--- /dev/null
+++ b/matitaB/components/binaries/matitaprover/tptp_cnf.ml
@@ -0,0 +1,62 @@
+
+let trans_atom = function 
+  | Ast.True | Ast.False | Ast.Predicate _ | Ast.Proposition _ -> assert false
+  | Ast.Eq (a,b) -> true, Ast.Function ("==",[Ast.Constant "_"; a; b])
+  | Ast.NotEq (a,b) -> false, Ast.Function ("==",[Ast.Constant "_"; a; b])
+;;
+
+let trans_formulae = function
+  | Ast.Disjunction _ -> assert false
+  | Ast.Atom a -> trans_atom a
+  | Ast.NegAtom _ -> assert false
+;;
+
+
+(* HELPERS *)
+let resolve ~tptppath s = 
+  let resolved_name = 
+    if HExtlib.is_regular s then s else
+    if tptppath = "/" then s else
+    if Filename.check_suffix s ".p" then
+     (assert (String.length s > 5);
+     let prefix = String.sub s 0 3 in
+     tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
+    else tptppath ^ "/" ^ s
+  in
+  if HExtlib.is_regular resolved_name then
+    resolved_name
+  else
+    begin
+      prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
+      exit 1
+    end
+;;
+
+(* MAIN *)
+let parse ~tptppath filename =
+  let rec aux = function
+    | [] -> []
+    | (Ast.Inclusion (file,_)) :: tl ->
+        let file = resolve ~tptppath file in
+        let lexbuf = Lexing.from_channel (open_in file) in
+        let statements = Parser.main Lexer.yylex lexbuf in
+        aux (statements @ tl)
+    | hd::tl -> hd :: aux tl
+  in
+  let statements = aux [Ast.Inclusion (filename,[])] in
+  let positives, negatives = 
+    let rec aux p n = function
+      | [] -> p,n
+      | Ast.Comment _ :: tl -> aux p n tl
+      | Ast.AnnotatedFormula (name, 
+          (Ast.Axiom | Ast.Hypothesis|Ast.Negated_conjecture), f,_,_) :: tl->
+          let is_positive, f = trans_formulae f in
+          if is_positive then aux (p@[Ast.Constant name,f]) n tl
+          else aux p (n@[Ast.Constant name,f]) tl
+      | _ -> prerr_endline "bad syntax"; assert false
+    in
+      aux [] [] statements
+  in
+  positives, negatives
+;;
+