6 module T = CicNotationPt
8 let parse_error s = Printf.eprintf "%s: " s ;;
9 let rm_q s = String.sub s 1 (String.length s - 2) ;;
18 try List.assoc k reserved with Not_found -> k
24 %token <string> COMMENT
28 %token <string> QSTRING
67 %type <AstTHF.ast list> main
71 | tptp_input EOF {[$1]}
72 | tptp_input main {$1::$2}
74 let start_pos = rhs_start_pos 1 in
75 let end_pos = rhs_end_pos 1 in
76 Printf.eprintf "from line %d char %d to line %d char %d\n"
77 start_pos.pos_lnum (start_pos.pos_cnum - start_pos.pos_bol)
78 end_pos.pos_lnum (end_pos.pos_cnum - end_pos.pos_bol);
89 formula_source_and_infos:
91 | COMMA { assert false }
95 | THF LPAREN name COMMA formula_type COMMA
96 term formula_source_and_infos RPAREN DOT {
100 | T.Appl [T.Symbol("Eq",_);T.Ident(name,_);body] ->
101 ThfDefinition($3,unreserve name,body)
102 | _ -> prerr_endline ("near " ^ $3); assert false)
105 | T.Cast (T.Ident(name,_),ty) -> ThfType($3,unreserve name,ty)
107 | _ -> ThfFormula($3,$5,$7)
115 | "hypothesis" -> Hypothesis
116 | "definition" -> Definition
118 | "theorem" -> Theorem
119 | "conjecture" -> Conjecture
120 | "lemma_conjecture" -> Lemma_conjecture
121 | "negated_conjecture" -> Negated_conjecture
123 | "unknown" -> Unknown
135 | UNAME { T.Ident($1,None), None }
136 | UNAME COLON term { T.Ident($1,None),Some $3 }
140 | vardecl COMMA varlist { $1 :: $3 }
143 | quantifier BEGINVARLIST varlist ENDVARLIST COLON term {
144 List.fold_right (fun v t -> T.Binder($1,v,t)) $3 $6
148 | T.Appl l -> T.Appl (l @ [$3])
149 | x -> T.Appl ([$1; $3])
151 | LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
152 | term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
153 | term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
154 | term IMPLYLR term { T.Binder (`Forall,(T.Ident("_",None),Some $3),$1) }
155 | term COIMPLY term { T.Appl [T.Symbol("Iff",0);$1;$3] }
156 | term XOR term { T.Appl [T.Symbol("Xor",0);$1;$3] }
157 | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
158 | term NIEQ term { T.Appl [T.Symbol("NotEq",0);$1;$3] }
159 | term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
160 | term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
161 | NOT term { T.Appl [T.Symbol("Not",0);$2] }
162 | LPAREN term RPAREN {$2}
163 | LNAME { T.Ident(unreserve $1,None) }
164 | UNAME { T.Ident($1,None) }
165 | TYPE_I { T.Symbol("i",0) }
166 | TYPE_O { T.Symbol("o",0) }
167 | TYPE_U { T.Sort (`NType "0") }
168 | FALSE { T.Symbol("False",0)}
169 | TRUE { T.Symbol("True",0)}
173 | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
174 let fname = rm_q $3 in
179 selection_of_formulae:
181 | COMMA name selection_of_formulae { $2::$3 }
184 comment: COMMENT {Comment $1} ;
186 name: NUM { string_of_int $1} | LNAME { $1 } | UNAME { $1 } ;