helm/software/components/binaries/matitaprover/tptp_cnf.ml

   1
   2 let trans_atom = function
   3   | Ast.True | Ast.False | Ast.Predicate _ | Ast.Proposition _ -> assert false
   4   | Ast.Eq (a,b) -> true, Ast.Function ("==",[Ast.Constant "_"; a; b])
   5   | Ast.NotEq (a,b) -> false, Ast.Function ("==",[Ast.Constant "_"; a; b])
   6 ;;
   7
   8 let trans_formulae = function
   9   | Ast.Disjunction _ -> assert false
  10   | Ast.Atom a -> trans_atom a
  11   | Ast.NegAtom _ -> assert false
  12 ;;
  13
  14
  15 (* HELPERS *)
  16 let resolve ~tptppath s =
  17   let resolved_name =
  18     if HExtlib.is_regular s then s else
  19     if tptppath = "/" then s else
  20     if Filename.check_suffix s ".p" then
  21      (assert (String.length s > 5);
  22      let prefix = String.sub s 0 3 in
  23      tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
  24     else tptppath ^ "/" ^ s
  25   in
  26   if HExtlib.is_regular resolved_name then
  27     resolved_name
  28   else
  29     begin
  30       prerr_endline ("Unable to find " ^ s ^ " (" ^ resolved_name ^ ")");
  31       exit 1
  32     end
  33 ;;
  34
  35 (* MAIN *)
  36 let parse ~tptppath filename =
  37   let rec aux = function
  38     | [] -> []
  39     | (Ast.Inclusion (file,_)) :: tl ->
  40         let file = resolve ~tptppath file in
  41         let lexbuf = Lexing.from_channel (open_in file) in
  42         let statements = Parser.main Lexer.yylex lexbuf in
  43         aux (statements @ tl)
  44     | hd::tl -> hd :: aux tl
  45   in
  46   let statements = aux [Ast.Inclusion (filename,[])] in
  47   let positives, negatives =
  48     let rec aux p n = function
  49       | [] -> p,n
  50       | Ast.Comment _ :: tl -> aux p n tl
  51       | Ast.AnnotatedFormula (name,
  52           (Ast.Axiom | Ast.Hypothesis|Ast.Negated_conjecture), f,_,_) :: tl->
  53           let is_positive, f = trans_formulae f in
  54           if is_positive then aux (p@[Ast.Constant name,f]) n tl
  55           else aux p (n@[Ast.Constant name,f]) tl
  56       | _ -> prerr_endline "bad syntax"; assert false
  57     in
  58       aux [] [] statements
  59   in
  60   positives, negatives
  61 ;;
  62