Skip to content

Commit

Permalink
Merge pull request #144 from FStarLang/sedlex
Browse files Browse the repository at this point in the history
Migrate from ulex to sedlex
  • Loading branch information
s-zanella authored Jul 9, 2019
2 parents d6f2fc2 + 2fa43d0 commit 4acd7cc
Show file tree
Hide file tree
Showing 12 changed files with 39 additions and 37 deletions.
2 changes: 1 addition & 1 deletion .merlin
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
S src
S lib
B _build/*
PKG ppx_deriving.std ppx_deriving_yojson zarith pprint unix wasm process ulex
PKG ppx_deriving.std ppx_deriving_yojson zarith pprint unix wasm process sedlex
PKG visitors.ppx visitors.runtime
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ make via homebrew, and invoke `gmake` instead of `make`.

**Regarding OCaml:** Install OPAM via your package manager, then:

`$ opam install ppx_deriving_yojson zarith pprint menhir ulex process fix wasm visitors`
`$ opam install ppx_deriving_yojson zarith pprint menhir sedlex process fix wasm visitors`

Next, make sure you have an up-to-date F\*, and that you ran `make` in the
`ulib/ml` directory of F\*. The `fstar.exe` executable should be on your PATH
Expand Down
4 changes: 2 additions & 2 deletions _tags
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@
# Reinstate @3 once we move to 4.03.0
true: annot, bin_annot, warn(@[email protected]@[email protected]@31..38-39@40-41@43@57), \
package(ppx_deriving.std), package(ppx_deriving_yojson), \
package(zarith), package(pprint), package(unix), package(menhirLib), package(ulex), \
package(zarith), package(pprint), package(unix), package(menhirLib), package(sedlex), \
package(process), package(fix), package(wasm), debug, strict_sequence, \
package(visitors.ppx), package(visitors.runtime)
"parser/Lexer.ml": syntax(camlp4o), syntax(pa_ulex)
"parser/Lexer.ml": package(sedlex.ppx)
<test>: -traverse
<kremlib/{extracted,c,out,dist}>: -traverse
<kremlib/**/*.ml>: package(fstarlib)
4 changes: 2 additions & 2 deletions kremlib/C.Failure.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

14 changes: 7 additions & 7 deletions kremlib/C.String.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions kremlib/C.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions kremlib/TestLib.fsti.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions lib/Utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,9 @@ let theight, twidth =

let parse the_parser arg =
let the_parser = MenhirLib.Convert.Simplified.traditional2revised the_parser in
let lexbuf = Ulexing.from_utf8_string arg in
let lexbuf = Sedlexing.Utf8.from_string arg in
try
the_parser (fun _ -> Lexer.token lexbuf)
with Ulexing.Error | Parser.Error as e ->
with Sedlexing.MalFormed | Sedlexing.InvalidCodepoint _ | Parser.Error as e ->
KPrint.bprintf "Syntax error in: %s\n" arg;
raise e
28 changes: 15 additions & 13 deletions parser/Lexer.ml
Original file line number Diff line number Diff line change
@@ -1,29 +1,30 @@
open Ulexing
open Sedlexing
open Parser

let regexp digit = ['0'-'9']
let regexp int = digit+
let regexp low_alpha = ['a'-'z']
let regexp up_alpha = ['A'-'Z']
let regexp any = up_alpha | low_alpha | '_' | digit
let regexp lident = low_alpha any*
let regexp uident = up_alpha any*
let digit = [%sedlex.regexp? '0'..'9']
let integer = [%sedlex.regexp? Plus digit]
let low_alpha = [%sedlex.regexp? 'a'..'z']
let up_alpha = [%sedlex.regexp? 'A'..'Z']
let any = [%sedlex.regexp? up_alpha | low_alpha | '_' | digit]
let lident = [%sedlex.regexp? low_alpha, Star (any)]
let uident = [%sedlex.regexp? up_alpha, Star (any)]

let locate _ tok = tok, Lexing.dummy_pos, Lexing.dummy_pos

let keywords = [
"rename", RENAME
]

let rec token = lexer
| int ->
let l = utf8_lexeme lexbuf in
let rec token lexbuf =
match%sedlex lexbuf with
| integer ->
let l = Utf8.lexeme lexbuf in
locate lexbuf (INT (int_of_string l))
| uident ->
let l = utf8_lexeme lexbuf in
let l = Utf8.lexeme lexbuf in
locate lexbuf (UIDENT l)
| lident ->
let l = utf8_lexeme lexbuf in
let l = Utf8.lexeme lexbuf in
begin try
locate lexbuf (List.assoc l keywords)
with Not_found ->
Expand All @@ -40,3 +41,4 @@ let rec token = lexer
| "[" -> locate lexbuf LBRACK
| "]" -> locate lexbuf RBRACK
| eof -> locate lexbuf EOF
| _ -> assert false
4 changes: 2 additions & 2 deletions runtime/WasmSupport.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion src/Kremlin.ml
Original file line number Diff line number Diff line change
Expand Up @@ -321,7 +321,7 @@ Supported options:|}
in
begin try
Arg.parse spec anon_fun usage
with Ulexing.Error | Parser.Error ->
with Sedlexing.MalFormed | Sedlexing.InvalidCodepoint _ | Parser.Error ->
KPrint.bprintf "Complete invocation was: %s\n"
(String.concat "" (Array.to_list Sys.argv));
exit 1
Expand Down
4 changes: 2 additions & 2 deletions src/Warnings.ml
Original file line number Diff line number Diff line change
Expand Up @@ -220,12 +220,12 @@ let maybe_fatal_error error =
;;

let parse_warn_error s =
let lexbuf = Ulexing.from_utf8_string s in
let lexbuf = Sedlexing.Utf8.from_string s in
let the_parser = MenhirLib.Convert.Simplified.traditional2revised Parser.warn_error_list in
let user_flags =
try
the_parser (fun _ -> Lexer.token lexbuf)
with Ulexing.Error | Parser.Error ->
with Sedlexing.MalFormed | Sedlexing.InvalidCodepoint _ | Parser.Error ->
fatal_error "Malformed warn-error list"
in
List.iter (fun (f, (l, h)) ->
Expand Down

0 comments on commit 4acd7cc

Please sign in to comment.