--- /dev/null
+%{
+ (* header *)
+ open Ast
+ open Parsing
+ open Lexing
+
+ let parse_error s = Printf.eprintf "%s: " s ;;
+ let rm_q s = String.sub s 1 (String.length s - 2) ;;
+
+%}
+ %token <string> TYPE
+ %token <string> COMMENT
+ %token <int> NUM
+ %token <string> LNAME
+ %token <string> UNAME
+ %token <string> QSTRING
+ %token COMMA
+ %token INCLUSION
+ %token LPAREN
+ %token RPAREN
+ %token CNF
+ %token TRUE
+ %token FALSE
+ %token IOR
+ %token NOT
+ %token NIEQ
+ %token IEQ
+ %token PEQ
+ %token DOT
+ %token EOF
+
+ %type <Ast.ast list> main
+ %start main
+%%
+ main:
+ | tptp_input EOF {[$1]}
+ | tptp_input main {$1::$2}
+ | error {
+ let start_pos = rhs_start_pos 1 in
+ let end_pos = rhs_end_pos 1 in
+ Printf.eprintf "from line %d char %d to line %d char %d\n"
+ start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
+ end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
+ exit 1
+ }
+ ;
+
+ tptp_input:
+ | annot_formula {$1}
+ | include_ {$1}
+ | comment {$1}
+ ;
+
+ annot_formula:
+ | CNF LPAREN
+ name COMMA formula_type COMMA formula formula_source_and_infos
+ RPAREN DOT {
+ AnnotatedFormula ($3,$5,$7,fst $8,snd $8)
+ }
+ ;
+
+ formula_type:
+ | TYPE {
+ match $1 with
+ | "axiom" -> Axiom
+ | "hypothesis" -> Hypothesis
+ | "definition" -> Definition
+ | "lemma" -> Lemma
+ | "theorem" -> Theorem
+ | "conjecture" -> Conjecture
+ | "lemma_conjecture" -> Lemma_conjecture
+ | "negated_conjecture" -> Negated_conjecture
+ | "plain" -> Plain
+ | "unknown" -> Unknown
+ | _ -> assert false
+ }
+ ;
+
+ formula:
+ | LPAREN disjunction RPAREN {$2}
+ | disjunction {$1}
+ ;
+
+ disjunction:
+ | literal {$1}
+ | literal IOR disjunction {
+ Disjunction ($1,$3)
+ }
+ ;
+
+ literal:
+ | NOT atom { NegAtom $2 }
+ | atom { Atom $1 }
+ ;
+
+ atom:
+ | atomic_word LPAREN term_list RPAREN { Predicate ($1,$3) }
+ | atomic_word { Proposition $1 }
+ | TRUE { True }
+ | FALSE { False }
+ | term IEQ term { Eq ($1,$3) }
+ | term NIEQ term { NotEq ($1,$3) }
+ | PEQ LPAREN term COMMA term RPAREN { Eq ($3,$5) }
+ ;
+
+ term_list:
+ | term { [$1] }
+ | term COMMA term_list { $1 :: $3 }
+ ;
+
+ term:
+ | upper_word { Variable $1 }
+ | atomic_word LPAREN term_list RPAREN { Function ($1,$3) }
+ | atomic_word { Constant $1 }
+ ;
+
+ upper_word: UNAME { $1 } ;
+
+ atomic_word:
+ | LNAME { $1 }
+ | QSTRING { rm_q $1 }
+ | TYPE { (* workaround! *)
+ match $1 with
+ | "theorem" -> "theoremP"
+ | "axiom" -> "axiomP"
+ | s -> prerr_endline s;assert false }
+ ;
+
+ formula_source_and_infos:
+ | { NoSource, [NoInfo] }
+ | COMMA { assert false }
+ ;
+
+ include_:
+ | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
+ let fname = rm_q $3 in
+ Inclusion (fname,$4)
+ }
+ ;
+
+ selection_of_formulae:
+ | { [] }
+ | COMMA name selection_of_formulae { $2::$3 }
+ ;
+
+ comment: COMMENT {Comment $1} ;
+
+ name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;
+%%
+ (* trailer *)