Commit 609d04ff authored by Simon Cruanes's avatar Simon Cruanes
Browse files

proper handling of lexing/parsing error

parent 9582e1aa
......@@ -4,6 +4,8 @@ open TptpTree
open Why
open Lexing
open TptpTranslate
......@@ -16,10 +18,20 @@ end= struct
(** for a given file, returns the list of declarations
for this file and all the files it includes, recursively *)
let rec getAllDecls ?first:(first=false) include_dir filename =
let rec myparse chan =
let lb = Lexing.from_channel chan in
try TptpParser.tptp TptpLexer.token lb
with
| TptpLexer.LexicalError s -> report lb;
Format.eprintf "lexical error: %s@." s; exit 1
| TptpParser.Error -> report lb; Format.eprintf "syntax error@."; exit 1
and report lb = let pos = lexeme_start_p lb in
Format.eprintf "file %s, line %d, char %d@."
filename (pos.pos_lnum) (pos.pos_cnum-pos.pos_bol) in
try
let filename = if first then filename else include_dir^"/"^filename in
let input = if filename = "-" then stdin else open_in filename in
let decls = TptpParser.tptp TptpLexer.token (Lexing.from_channel input) in
let decls = myparse input in
let isInclude = function | Include _ -> true | _ -> false in
close_in input;
let (to_include, real_decl) = List.partition isInclude decls in
......
......@@ -17,7 +17,6 @@
"conjecture", CONJECTURE;
"negated_conjecture", NEGATED_CONJECTURE;
"axiom", AXIOM;
"definition", AXIOM; (* TODO : what's the difference ? *)
"hypothesis", AXIOM;
"include", INCLUDE
]
......@@ -29,6 +28,8 @@
let stringBuf = Buffer.create 256
exception LexicalError of string
}
let newline = '\n'
......@@ -104,10 +105,10 @@ rule token = parse
| eof
{ EOF }
| _ as c
{ eprintf "illegal character: %c@." c; exit 1 }
{ raise (LexicalError (Format.sprintf "illegal character: %c" c)) }
and comment = parse (* read until newline *)
| newline
{ token lexbuf }
{ newline lexbuf; token lexbuf }
| _
{ comment lexbuf }
and string = parse
......@@ -118,6 +119,6 @@ and string = parse
| "\\'"
{ Buffer.add_char stringBuf '\''; string lexbuf }
| eof
{ eprintf "unterminated single quoted\n"; exit 1 }
{ raise (LexicalError "unterminated single quoted") }
| _ as c
{ Buffer.add_char stringBuf c; string lexbuf }
......@@ -42,8 +42,8 @@
tptp:
| e = decl* EOF
{ e }
| error
{ Printf.printf "error at lexing pos %i\n" $endpos.Lexing.pos_lnum; assert false }
(* | error
{ Printf.printf "error at lexing pos %i\n" $endpos.Lexing.pos_lnum; assert false } *)
decl:
| CNF LPAREN name = lident COMMA ty = decl_type COMMA f = fmla RPAREN DOT
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment