X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Flexer.mll;h=2b6c4e8020f9afa321d21e8b290ac746e73c0614;hb=e23952e03c37201fe805ad3d1635e7d2d41e5908;hp=d0f4a1dec90903f302f885563c21b2fbeebda589;hpb=5a6a8b2b8e515941f9a2b3cc051da646ae696251;p=goals.git diff --git a/src/lexer.mll b/src/lexer.mll index d0f4a1d..2b6c4e8 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -28,13 +28,13 @@ exception SyntaxError of string let new_line lexbuf = let pos = lexbuf.lex_curr_p in lexbuf.lex_curr_p <- - { pos with pos_bol = lexbuf.lex_curr_pos; pos_lnum = pos.pos_lnum + 1 } + { pos with pos_bol = pos.pos_cnum; pos_lnum = pos.pos_lnum + 1 } } let white = [' ' '\t']+ let newline = '\r' | '\n' | "\r\n" let comment = '#' (_#'\n')* -let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* +let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_' '-']* rule read = parse @@ -43,15 +43,36 @@ rule read = | newline { new_line lexbuf; read lexbuf } | "," { COMMA } | ":" { COLON } + | ";" { SEMICOLON } | "=" { EQUALS } | "(" { LEFT_PAREN } | ")" { RIGHT_PAREN } | "[" { LEFT_ARRAY } | "]" { RIGHT_ARRAY } | '"' { read_string (Ast.Substs.create ()) lexbuf } - | "{" { read_code (Ast.Substs.create ()) (ref 1) lexbuf } + | "{" { read_code false (Ast.Substs.create ()) (ref 1) lexbuf } + | "@{" { read_code true (Ast.Substs.create ()) (ref 1) lexbuf } | "goal" { GOAL } + | "tactic" + { TACTIC_KEYWORD } + | "function" + { FUNCTION } + | "pure" { PURE } | "let" { LET } + | "include" + { INCLUDE } + | "-include" + { OPTINCLUDE } + | "returning" + { RETURNING } + | "expression" + { EXPRESSION } + | "string" + { STRING_KEYWORD } + | "strings" + { STRINGS } + | "*" id { (* NB: The initial '*' is part of the name. *) + TACTIC (Lexing.lexeme lexbuf) } | id { ID (Lexing.lexeme lexbuf) } | _ { raise (SyntaxError ("unexpected character: " ^ Lexing.lexeme lexbuf)) } @@ -100,30 +121,31 @@ and read_string buf = * Note the range of %-substitutions possible is larger than * for strings. *) -and read_code buf level = +and read_code quiet buf level = parse - | '{' { incr level; read_code buf level lexbuf } + | '{' { Ast.Substs.add_char buf '{'; + incr level; read_code quiet buf level lexbuf } | '}' { decr level; - if !level = 0 then CODE (Ast.Substs.get buf) + if !level = 0 then CODE (Ast.Substs.get buf, quiet) else ( Ast.Substs.add_char buf '}'; - read_code buf level lexbuf + read_code quiet buf level lexbuf ) } | newline { Ast.Substs.add_char buf '\n'; - new_line lexbuf; read_code buf level lexbuf } - | '%' '%' { Ast.Substs.add_char buf '%'; read_code buf level lexbuf } - | '%' '@' { Ast.Substs.add_var buf "@"; read_code buf level lexbuf } - | '%' '<' { Ast.Substs.add_var buf "<"; read_code buf level lexbuf } - | '%' '^' { Ast.Substs.add_var buf "^"; read_code buf level lexbuf } + new_line lexbuf; read_code quiet buf level lexbuf } + | '%' '%' { Ast.Substs.add_char buf '%'; read_code quiet buf level lexbuf } + | '%' '@' { Ast.Substs.add_var buf "@"; read_code quiet buf level lexbuf } + | '%' '<' { Ast.Substs.add_var buf "<"; read_code quiet buf level lexbuf } + | '%' '^' { Ast.Substs.add_var buf "^"; read_code quiet buf level lexbuf } | '%' id { let id = Lexing.lexeme lexbuf in let len = String.length id in Ast.Substs.add_var buf (String.sub id 1 (len-1)); - read_code buf level lexbuf } + read_code quiet buf level lexbuf } | '%' _ { raise (SyntaxError ("illegal character in %-substitution: " ^ Lexing.lexeme lexbuf)) } | [^ '{' '}' '\r' '\n' '%' ]+ { Ast.Substs.add_string buf (Lexing.lexeme lexbuf); - read_code buf level lexbuf } + read_code quiet buf level lexbuf } | _ { raise (SyntaxError ("illegal character in code section: " ^ Lexing.lexeme lexbuf)) } | eof { raise (SyntaxError ("unterminated code section")) }