de meilleurs messages d'erreur pour les commentaires et les chaines non termines

parent 3136d482
......@@ -22,7 +22,7 @@ theory Int
type t = int, logic zero = zero,
logic (_+_) = (_+_), logic (_*_) = (_*_), logic (-_) = (-_)
(* int is a unitary, communtative ring *)
(* int is a unitary, commutative ring *)
axiom Mul_comm: forall x,y:int. x * y = y * x
axiom One_neutral: forall x:int. 1 * x = x
......
......@@ -35,3 +35,5 @@ val report : Format.formatter -> error -> unit
val parse_logic_file : Lexing.lexbuf -> Ptree.logic_file
val remove_leading_plus : string -> string
val with_location : (Lexing.lexbuf -> 'a) -> Lexing.lexbuf -> 'a
......@@ -78,8 +78,11 @@
lexbuf.lex_curr_p <-
{ pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
let string_start_loc = ref Loc.dummy_position
let string_buf = Buffer.create 1024
let comment_start_loc = ref Loc.dummy_position
let char_for_backslash = function
| 'n' -> '\n'
| 't' -> '\t'
......@@ -99,6 +102,8 @@
let n = String.length s in
if n > 0 && s.[0] = '+' then String.sub s 1 (n-1) else s
let loc lb = (lexeme_start_p lb, lexeme_end_p lb)
}
let newline = '\n'
......@@ -147,7 +152,7 @@ rule token = parse
['p' 'P'] (['-' '+']? digit+ as e)
{ FLOAT (RConstHexa (i, f, remove_leading_plus e)) }
| "(*"
{ comment lexbuf; token lexbuf }
{ comment_start_loc := loc lexbuf; comment lexbuf; token lexbuf }
| "'"
{ QUOTE }
| ","
......@@ -187,7 +192,7 @@ rule token = parse
| "|"
{ BAR }
| "\""
{ STRING (string lexbuf) }
{ string_start_loc := loc lexbuf; STRING (string lexbuf) }
| eof
{ EOF }
| _ as c
......@@ -201,7 +206,7 @@ and comment = parse
| newline
{ newline lexbuf; comment lexbuf }
| eof
{ raise (Error UnterminatedComment) }
{ raise (Loc.Located (!comment_start_loc, Error UnterminatedComment)) }
| _
{ comment lexbuf }
......@@ -215,7 +220,7 @@ and string = parse
| newline
{ newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf }
| eof
{ raise (Error UnterminatedString) }
{ raise (Loc.Located (!string_start_loc, Error UnterminatedString)) }
| _ as c
{ Buffer.add_char string_buf c; string lexbuf }
......@@ -223,10 +228,12 @@ and string = parse
{
let loc lb = (lexeme_start_p lb, lexeme_end_p lb)
let with_location f lb =
try f lb with e -> raise (Loc.Located (loc lb, e))
try
f lb
with
| Loc.Located _ as e -> raise e
| e -> raise (Loc.Located (loc lb, e))
let parse_lexpr = with_location (lexpr token)
let parse_logic_file = with_location (logic_file token)
......
......@@ -18,11 +18,20 @@
(**************************************************************************)
{
open Format
open Lexing
open Lexer
open Term
open Pgm_parser
type error =
| UnterminatedLogic
exception Error of error
let report fmt = function
| UnterminatedLogic -> fprintf fmt "unterminated logic block"
let keywords = Hashtbl.create 97
let () =
List.iter
......@@ -72,6 +81,11 @@
pos_bol = pos.pos_cnum - int_of_string chars;
}
let logic_start_loc = ref Loc.dummy_position
let logic_buffer = Buffer.create 1024
let loc lb = (lexeme_start_p lb, lexeme_end_p lb)
}
let newline = '\n'
......@@ -156,9 +170,7 @@ rule token = parse
| "]"
{ RIGHTSQ }
| "{"
{ LEFTB }
| "}"
{ RIGHTB }
{ logic_start_loc := loc lexbuf; LOGIC (logic lexbuf) }
| "{{"
{ LEFTBLEFTB }
| "}}"
......@@ -176,31 +188,23 @@ rule token = parse
| eof
{ EOF }
| _ as c
{ raise (Error (IllegalCharacter c)) }
(* and logic = parse *)
(* | "\"" *)
(* { let s = Buffer.contents string_buf in *)
(* Buffer.clear string_buf; *)
(* s } *)
(* | "\\" (_ as c) *)
(* { Buffer.add_char string_buf (char_for_backslash c); string lexbuf } *)
(* | newline *)
(* { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf } *)
(* | eof *)
(* { raise (Error UnterminatedString) } *)
(* | _ as c *)
(* { Buffer.add_char string_buf c; string lexbuf } *)
{ raise (Lexer.Error (IllegalCharacter c)) }
and logic = parse
| "}"
{ let s = Buffer.contents logic_buffer in
Buffer.clear logic_buffer;
s }
| newline
{ newline lexbuf; Buffer.add_char logic_buffer '\n'; logic lexbuf }
| eof
{ raise (Loc.Located (!logic_start_loc, Error UnterminatedLogic)) }
| _ as c
{ Buffer.add_char logic_buffer c; logic lexbuf }
{
let loc lb = (lexeme_start_p lb, lexeme_end_p lb)
let with_location f lb =
try f lb with e -> raise (Loc.Located (loc lb, e))
let parse_file = with_location (file token)
}
......
......@@ -23,6 +23,8 @@ let () =
let rec report fmt = function
| Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e;
| Pgm_lexer.Error e ->
fprintf fmt "lexical error: %a" Pgm_lexer.report e;
| Loc.Located (loc, e) ->
fprintf fmt "%a%a" Loc.report_position loc report e
| Parsing.Parse_error ->
......
......@@ -85,6 +85,7 @@
%token <string> OP0 OP1 OP2 OP3
%token <Ptree.real_constant> FLOAT
%token <string> STRING
%token <string> LOGIC
/* keywords */
......@@ -95,7 +96,7 @@
/* symbols */
%token UNDERSCORE QUOTE COMMA LEFTPAR RIGHTPAR BANG COLON SEMICOLON
%token COLONEQUAL ARROW EQUAL AT DOT LEFTSQ RIGHTSQ LEFTB RIGHTB
%token COLONEQUAL ARROW EQUAL AT DOT LEFTSQ RIGHTSQ
%token LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP BIGARROW
%token EOF
......
(* test file for ML-why *)
{ }
(*
Local Variables:
......
......@@ -3,7 +3,6 @@
theory Test
use import prelude.Int
use BuiltIn
logic id(x: int) : int = x
logic even(x: int) = 2*(x/2) = x
goal G : forall x:int. 0 = zero
......@@ -14,3 +13,4 @@ Local Variables:
compile-command: "make -C .. test"
End:
*)
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