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