let trans_atom ~neg = 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
;;

let trans_formulae ~neg = function
  | Ast.Disjunction _ -> assert false
  | Ast.Atom a -> trans_atom ~neg a
  | Ast.NegAtom _ -> assert false
;;


(* HELPERS *)
let resolve ~tptppath s = 
  let resolved_name = 
    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), 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
      | _ -> prerr_endline "bad syntax"; assert false
    in
      aux [] [] statements
  in
  positives, negatives
;;