7 let parse_error s = Printf.eprintf "%s: " s ;;
8 let rm_q s = String.sub s 1 (String.length s - 2) ;;
12 %token <string> COMMENT
16 %token <string> QSTRING
32 %type <Ast.ast list> main
36 | tptp_input EOF {[$1]}
37 | tptp_input main {$1::$2}
39 let start_pos = rhs_start_pos 1 in
40 let end_pos = rhs_end_pos 1 in
41 Printf.eprintf "from line %d char %d to line %d char %d\n"
42 start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
43 end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
56 name COMMA formula_type COMMA formula formula_source_and_infos
58 AnnotatedFormula ($3,$5,$7,fst $8,snd $8)
66 | "hypothesis" -> Hypothesis
67 | "definition" -> Definition
69 | "theorem" -> Theorem
70 | "conjecture" -> Conjecture
71 | "lemma_conjecture" -> Lemma_conjecture
72 | "negated_conjecture" -> Negated_conjecture
74 | "unknown" -> Unknown
80 | LPAREN disjunction RPAREN {$2}
86 | literal IOR disjunction {
92 | NOT atom { NegAtom $2 }
97 | atomic_word LPAREN term_list RPAREN { Predicate ($1,$3) }
98 | atomic_word { Proposition $1 }
101 | term IEQ term { Eq ($1,$3) }
102 | term NIEQ term { NotEq ($1,$3) }
103 | PEQ LPAREN term COMMA term RPAREN { Eq ($3,$5) }
108 | term COMMA term_list { $1 :: $3 }
112 | upper_word { Variable $1 }
113 | atomic_word LPAREN term_list RPAREN { Function ($1,$3) }
114 | atomic_word { Constant $1 }
117 upper_word: UNAME { $1 } ;
121 | QSTRING { rm_q $1 }
122 | TYPE { (* workaround! *)
124 | "theorem" -> "theoremP"
125 | "axiom" -> "axiomP"
126 | s -> prerr_endline s;assert false }
129 formula_source_and_infos:
130 | { NoSource, [NoInfo] }
131 | COMMA { assert false }
135 | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
136 let fname = rm_q $3 in
141 selection_of_formulae:
143 | COMMA name selection_of_formulae { $2::$3 }
146 comment: COMMENT {Comment $1} ;
148 name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;