Merge pull request #827 from CakeML/hex

Implement parsing of hex integer literals
CakeML · May 6, 2021 · dcd58cd · dcd58cd
2 parents c39f0f7 + 559b482
commit dcd58cd
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 10 deletions.
diff --git a/compiler/parsing/lexer_implScript.sml b/compiler/parsing/lexer_implScript.sml
@@ -191,10 +191,16 @@ val next_sym_alt_def = tDefine "next_sym_alt" `
                    rest)
          else SOME (ErrorS, Locs loc loc, TL str)
        else
-         let (n,rest) = read_while isDigit str [] in
-           SOME (NumberS (&(num_from_dec_string_alt (c::n))),
-                 Locs loc (loc with col := loc.col + LENGTH n),
-                 rest)
+         if str ≠ "" ∧ c = #"0" ∧ HD str = #"x" then
+           let (n,rest) = read_while isHexDigit (TL str) [] in
+             SOME (NumberS (& num_from_hex_string_alt n),
+                   Locs loc (loc with col := loc.col + LENGTH n + 2),
+                   rest)
+         else
+           let (n,rest) = read_while isDigit str [] in
+             SOME (NumberS (&(num_from_dec_string_alt (c::n))),
+                   Locs loc (loc with col := loc.col + LENGTH n),
+                   rest)
      else if c = #"~" /\ str <> "" /\ isDigit (HD str) then (* read negative number *)
        let (n,rest) = read_while isDigit str [] in
          SOME (NumberS (0- &(num_from_dec_string_alt n)),

diff --git a/semantics/lexer_funScript.sml b/semantics/lexer_funScript.sml
@@ -184,10 +184,16 @@ val next_sym_def = tDefine "next_sym" `
                    rest)
          else SOME (ErrorS, Locs loc loc, TL str)
        else
-         let (n,rest) = read_while isDigit str [] in
-           SOME (NumberS (&(num_from_dec_string (c::n))),
-                 Locs loc (loc with col := loc.col + LENGTH n),
-                 rest)
+         if str ≠ "" ∧ c = #"0" ∧ HD str = #"x" then
+           let (n,rest) = read_while isHexDigit (TL str) [] in
+             SOME (NumberS (& (num_from_hex_string n)),
+                   Locs loc (loc with col := loc.col + LENGTH n + 2),
+                   rest)
+         else
+           let (n,rest) = read_while isDigit str [] in
+             SOME (NumberS (&(num_from_dec_string (c::n))),
+                   Locs loc (loc with col := loc.col + LENGTH n),
+                   rest)
      else if c = #"~" /\ str <> "" /\ isDigit (HD str) then (* read negative number *)
        let (n,rest) = read_while isDigit str [] in
          SOME (NumberS (0- &(num_from_dec_string n)),
@@ -207,11 +213,9 @@ val next_sym_def = tDefine "next_sym" `
          SOME (mkCharS t, Locs loc loc', rest)
      else if isPREFIX "#(" (c::str) then
        let (t, loc', rest) = read_FFIcall (TL str) "" (loc with col := loc.col + 2) in
-
          SOME (t, Locs loc loc', rest)
      else if isPREFIX "#{" (c::str) then
        let (t, loc', rest) = read_REPLcommand (TL str) "" (loc with col := loc.col + 2) in
-
          SOME (t, Locs loc loc', rest)
      else if isPREFIX "(*" (c::str) then
        case skip_comment (TL str) 0 (loc with col := loc.col + 2) of