diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /coqpp/coqpp_lex.mll | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'coqpp/coqpp_lex.mll')
-rw-r--r-- | coqpp/coqpp_lex.mll | 168 |
1 files changed, 168 insertions, 0 deletions
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll new file mode 100644 index 00000000..bfa4e2b5 --- /dev/null +++ b/coqpp/coqpp_lex.mll @@ -0,0 +1,168 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +{ + +open Lexing +open Coqpp_parse + +type mode = +| OCaml +| Extend + +exception Lex_error of Coqpp_ast.loc * string + +let loc lexbuf = { + Coqpp_ast.loc_start = lexeme_start_p lexbuf; + Coqpp_ast.loc_end = lexeme_end_p lexbuf; +} + +let newline lexbuf = + let pos = lexbuf.lex_curr_p in + let pos = { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum } in + lexbuf.lex_curr_p <- pos + +let num_comments = ref 0 +let num_braces = ref 0 + +let mode () = if !num_braces = 0 then Extend else OCaml + +let comment_buf = Buffer.create 512 +let ocaml_buf = Buffer.create 512 +let string_buf = Buffer.create 512 + +let lex_error lexbuf msg = + raise (Lex_error (loc lexbuf, msg)) + +let lex_unexpected_eof lexbuf where = + lex_error lexbuf (Printf.sprintf "Unexpected end of file in %s" where) + +let start_comment _ = + let () = incr num_comments in + Buffer.add_string comment_buf "(*" + +let end_comment lexbuf = + let () = decr num_comments in + let () = Buffer.add_string comment_buf "*)" in + if !num_comments < 0 then lex_error lexbuf "Unexpected end of comment" + else if !num_comments = 0 then + let s = Buffer.contents comment_buf in + let () = Buffer.reset comment_buf in + Some (COMMENT s) + else + None + +let start_ocaml _ = + let () = match mode () with + | OCaml -> Buffer.add_string ocaml_buf "{" + | Extend -> () + in + incr num_braces + +let end_ocaml lexbuf = + let () = decr num_braces in + if !num_braces < 0 then lex_error lexbuf "Unexpected end of OCaml code" + else if !num_braces = 0 then + let s = Buffer.contents ocaml_buf in + let () = Buffer.reset ocaml_buf in + Some (CODE { Coqpp_ast.code = s }) + else + let () = Buffer.add_string ocaml_buf "}" in + None + +} + +let letter = ['a'-'z' 'A'-'Z'] +let letterlike = ['_' 'a'-'z' 'A'-'Z'] +let alphanum = ['_' 'a'-'z' 'A'-'Z' '0'-'9' '\''] +let ident = letterlike alphanum* +let qualid = ident ('.' ident)* +let space = [' ' '\t' '\r'] +let number = [ '0'-'9' ] + +rule extend = parse +| "(*" { start_comment (); comment lexbuf } +| "{" { start_ocaml (); ocaml lexbuf } +| "GRAMMAR" { GRAMMAR } +| "VERNAC" { VERNAC } +| "TACTIC" { TACTIC } +| "EXTEND" { EXTEND } +| "END" { END } +| "DECLARE" { DECLARE } +| "PLUGIN" { PLUGIN } +| "DEPRECATED" { DEPRECATED } +(** Camlp5 specific keywords *) +| "GLOBAL" { GLOBAL } +| "FIRST" { FIRST } +| "LAST" { LAST } +| "BEFORE" { BEFORE } +| "AFTER" { AFTER } +| "LEVEL" { LEVEL } +| "LEFTA" { LEFTA } +| "RIGHTA" { RIGHTA } +| "NONA" { NONA } +(** Standard *) +| ident { IDENT (Lexing.lexeme lexbuf) } +| qualid { QUALID (Lexing.lexeme lexbuf) } +| number { INT (int_of_string (Lexing.lexeme lexbuf)) } +| space { extend lexbuf } +| '\"' { string lexbuf } +| '\n' { newline lexbuf; extend lexbuf } +| '[' { LBRACKET } +| ']' { RBRACKET } +| '|' { PIPE } +| "->" { ARROW } +| ',' { COMMA } +| ':' { COLON } +| ';' { SEMICOLON } +| '(' { LPAREN } +| ')' { RPAREN } +| '=' { EQUAL } +| _ { lex_error lexbuf "syntax error" } +| eof { EOF } + +and ocaml = parse +| "{" { start_ocaml (); ocaml lexbuf } +| "}" { match end_ocaml lexbuf with Some tk -> tk | None -> ocaml lexbuf } +| '\n' { newline lexbuf; Buffer.add_char ocaml_buf '\n'; ocaml lexbuf } +| '\"' { Buffer.add_char ocaml_buf '\"'; ocaml_string lexbuf } +| (_ as c) { Buffer.add_char ocaml_buf c; ocaml lexbuf } +| eof { lex_unexpected_eof lexbuf "OCaml code" } + +and comment = parse +| "*)" { match end_comment lexbuf with Some _ -> extend lexbuf | None -> comment lexbuf } +| "(*" { start_comment lexbuf; comment lexbuf } +| '\n' { newline lexbuf; Buffer.add_char comment_buf '\n'; comment lexbuf } +| (_ as c) { Buffer.add_char comment_buf c; comment lexbuf } +| eof { lex_unexpected_eof lexbuf "comment" } + +and string = parse +| '\"' + { + let s = Buffer.contents string_buf in + let () = Buffer.reset string_buf in + STRING s + } +| "\\\"" { Buffer.add_char string_buf '\"'; string lexbuf } +| '\n' { newline lexbuf; Buffer.add_char string_buf '\n'; string lexbuf } +| (_ as c) { Buffer.add_char string_buf c; string lexbuf } +| eof { lex_unexpected_eof lexbuf "string" } + +and ocaml_string = parse +| "\\\"" { Buffer.add_string ocaml_buf "\\\""; ocaml_string lexbuf } +| '\"' { Buffer.add_char ocaml_buf '\"'; ocaml lexbuf } +| (_ as c) { Buffer.add_char ocaml_buf c; ocaml_string lexbuf } +| eof { lex_unexpected_eof lexbuf "OCaml string" } + +{ + +let token lexbuf = match mode () with +| OCaml -> ocaml lexbuf +| Extend -> extend lexbuf + +} |