From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 26 Jun 2009 13:21:55 +0000 (+0000)
Subject: fixed parsing
X-Git-Tag: make_still_working~3783
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c5e6ccfa6049bd5a0b941ec6d00cf452db0e8af9;p=helm.git

fixed parsing
---

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
index ffac76585..8c38d6e65 100644
--- a/helm/software/components/binaries/matitaprover/tptp_cnf.ml
+++ b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
@@ -1,15 +1,13 @@
 
-let trans_atom ~neg = function 
+let trans_atom = function 
   | Ast.True | Ast.False | Ast.Predicate _ | Ast.Proposition _ -> assert false
-  | Ast.Eq _ when neg -> assert false
-  | Ast.Eq (a,b) -> Ast.Function ("==",[Ast.Constant "_"; a; b])
-  | Ast.NotEq (a,b) when neg -> Ast.Function ("==",[Ast.Constant "_"; a; b])
-  | Ast.NotEq _ -> 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 ~neg = function
+let trans_formulae = function
   | Ast.Disjunction _ -> assert false
-  | Ast.Atom a -> trans_atom ~neg a
+  | Ast.Atom a -> trans_atom a
   | Ast.NegAtom _ -> assert false
 ;;
 
@@ -50,11 +48,11 @@ let parse ~tptppath filename =
     let rec aux p n = function
       | [] -> p,n
       | Ast.Comment _ :: tl -> aux p n tl
-      | Ast.AnnotatedFormula (name, (Ast.Axiom | Ast.Hypothesis), f,_,_) :: tl->
-          aux (p@[Ast.Constant name,trans_formulae ~neg:false f]) n tl
-      | Ast.AnnotatedFormula (name, Ast.Negated_conjecture, f,_,_) :: tl ->
-          assert (n = []);
-          aux p (n@[Ast.Constant name, trans_formulae ~neg:true f]) 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