From: Andrea Asperti 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