feat(frontend): accept digits after identifier prefixes

src/Examples.thy

@@ -77,6 +77,13 @@ lemma lexical_shadow:
   "reference ''(let x 7 (let x (+ x 2) (* x x)))'' ''1'' ''2'' ''3'' = (True,''81'' @ newline)"
   by eval
 
+lemma numeric_identifier:
+  "reference ''(let x1 7 (let x1 (+ x1 2) (* x1 x1)))'' ''0'' ''0'' ''0'' = (True,''81'' @ newline)"
+  by eval
+
+lemma numeric_prefix_rejected: "prepare ''(let 1x 3 1x)'' = None"
+  by eval
+
 lemma nested_temporaries:
   "reference ''(+ 10 (let a 3 (+ a (let b 4 (* a b)))))'' ''0'' ''0'' ''0'' = (True,''25'' @ newline)"
   by eval

src/Frontend.thy

@@ -33,8 +33,10 @@ theorem number_bound: "number s = Some n \<Longrightarrow> n < 2 ^ 64"
   by (auto simp: number_def parse_digits_def Let_def split: list.splits if_splits)
 
 definition valid_name :: "string \<Rightarrow> bool" where
-  "valid_name s = (s \<noteq> [] \<and> list_all (\<lambda>c. (97 \<le> nat_of_char c \<and> nat_of_char c \<le> 122)) s
-    \<and> s \<noteq> ''let'' \<and> s \<noteq> ''if'')"
+  "valid_name s = (case s of [] \<Rightarrow> False | c # cs \<Rightarrow>
+    97 \<le> nat_of_char c \<and> nat_of_char c \<le> 122 \<and>
+    list_all (\<lambda>d. (97 \<le> nat_of_char d \<and> nat_of_char d \<le> 122) \<or>
+      (48 \<le> nat_of_char d \<and> nat_of_char d < 58)) cs \<and> s \<noteq> ''let'' \<and> s \<noteq> ''if'')"
 
 fun lookup :: "string \<Rightarrow> string list \<Rightarrow> nat option" where
   "lookup name [] = None"

tests/cli.py

@@ -22,6 +22,10 @@ def main():
             assert int(invoke('eval',source,'0','0','0')) == expected, text
         source.write_text('(+ x y)')
         assert int(invoke('eval',source,'0xFF','0x1','0x0')) == 256
+        source.write_text('(let x1 7 (let x1 (+ x1 2) (* x1 x1)))')
+        assert int(invoke('eval',source,'0','0','0')) == 81
+        source.write_text('(let 1x 3 1x)')
+        invoke(source,binary,ok=False)
         for text in ['0x','0x10000000000000000','0xfg','0xffextra','-0x1']:
             source.write_text(text)
             binary.write_bytes(b'preserve')

tests/native.py

@@ -69,6 +69,7 @@ def main():
     cases += [("*", "x", 1), ("*", 1, "x"), ("and", "x", MASK)]
     cases += [("*", "x", 0), ("and", "x", 0), ("shl", 0, "y"), ("shr", 0, "y"), ("or", "x", MASK)]
     cases += [("if", "x", ("+", "y", "t"), ("+", "y", "t"))]
+    cases += [("let", "x1", ("+", "x", 1), ("*", "x1", "x1"))]
     cases += [("let", "a", ("+", "x", 3), ("+", "y", ("let", "b", "t", ("*", "a", "b")))),
               ("let", "x", "y", ("if", "t", ("+", "x", 1), ("-", "x", 1)))]
     cases += [generate(rng, 5, ["x", "y", "t"]) for _ in range(117)]