diff options
| author | Alasdair Armstrong | 2017-11-24 20:25:26 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-24 20:25:26 +0000 |
| commit | 381071686f99aabdc8d618051b1b63d5aeb0108c (patch) | |
| tree | eb488e0f80a76ca2699a4e5118a0c08c2ed01b69 /src/lexer2.mll | |
| parent | a1b47ed3bf5c6a4cf4d61b119c73e4fd50bea6d0 (diff) | |
Use unbound precision big_ints throughout sail.
Alastair's test cases revealed that using regular ints causes issues
throughout sail, where all kinds of things can internally overflow in
edge cases. This either causes crashes (e.g. int_of_string fails for
big ints) or bizarre inexplicable behaviour. This patch switches the
sail AST to use big_int rather than int, and updates everything
accordingly.
This touches everything and there may be bugs where I mistranslated
things, and also n = m will still typecheck with big_ints but fail at
runtime (ocaml seems to have decided that static typing is unnecessary
for equality...), as it needs to be changed to eq_big_int.
I also got rid of the old unused ocaml backend while I was updating
things, so as to not have to fix it.
Diffstat (limited to 'src/lexer2.mll')
| -rw-r--r-- | src/lexer2.mll | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/lexer2.mll b/src/lexer2.mll index 1763b3a6..40e7eec6 100644 --- a/src/lexer2.mll +++ b/src/lexer2.mll @@ -42,6 +42,7 @@ { open Parser2 +open Big_int open Parse_ast module M = Map.Make(String) exception LexError of string * Lexing.position @@ -216,13 +217,13 @@ rule token = parse | "<=" { (LtEq(r"<=")) } | "infix" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators; - Fixity (Infix, int_of_string (Char.escaped p), op) } + Fixity (Infix, big_int_of_string (Char.escaped p), op) } | "infixl" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators; - Fixity (InfixL, int_of_string (Char.escaped p), op) } + Fixity (InfixL, big_int_of_string (Char.escaped p), op) } | "infixr" ws (digit as p) ws (operator as op) { operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators; - Fixity (InfixR, int_of_string (Char.escaped p), op) } + Fixity (InfixR, big_int_of_string (Char.escaped p), op) } | operator as op { try M.find op !operators with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) } @@ -239,8 +240,8 @@ rule token = parse else Id(r i) } | (digit+ as i1) "." (digit+ as i2) { (Real (i1 ^ "." ^ i2)) } | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) } - | digit+ as i { (Num(int_of_string i)) } - | "-" digit+ as i { (Num(int_of_string i)) } + | digit+ as i { (Num(big_int_of_string i)) } + | "-" digit+ as i { (Num(big_int_of_string i)) } | "0b" (binarydigit+ as i) { (Bin(i)) } | "0x" (hexdigit+ as i) { (Hex(i)) } | '"' { (String( |