better error messages and decimal constants

Author: philzook58

src/kdrag/parsers/microlean.py

@@ -8,6 +8,7 @@
 For example \\alpha will tab autocomplete to α.
 """
 
+import difflib
 import lark
 import kdrag.smt as smt
 from lark import Tree
@@ -62,7 +63,7 @@
 theorem : "theorem" NAME ":" expr ":=" "grind"
 
 NAME: /[a-zA-Z_][a-zA-Z0-9_']*/
-NUMBER: /-?\d+/
+NUMBER: /-?\d+(\.\d+)?/
 %import common.WS
 %ignore WS
 COMMENT: "--" /[^\n]*/
@@ -82,7 +83,25 @@ def __getitem__(self, key):
         elif key in self.globals:
             return self.globals[key]
         else:
-            raise KeyError(key)
+            # Suggest a close name in error
+            names = list(self.locals) + list(self.globals)
+            dotted = []
+            for name, value in self.globals.items():
+                if name.startswith("_"):
+                    continue
+                try:
+                    attrs = dir(value)
+                except Exception:
+                    continue
+                for attr in attrs:
+                    if attr.startswith("_"):
+                        continue
+                    dotted.append(f"{name}.{attr}")
+            hints = difflib.get_close_matches(str(key), names + dotted, n=3, cutoff=0.6)
+            msg = f"Unknown name {key!s}"
+            if hints:
+                msg += f". Did you mean: {', '.join(hints)}?"
+            raise NameError(msg)
 
     def __setitem__(self, key, value):
         self.locals[key] = value
@@ -166,7 +185,10 @@ def expr(tree, env: Env) -> smt.ExprRef:
     match tree:
         # TODO: obviously this is not well typed.
         case Tree("num", [n]):
-            return int(n)  # type: ignore
+            text = str(n)
+            if "." in text:
+                return smt.RealVal(text)
+            return int(text)
         case Tree("const", [name, *attrs]):
             res = env[name]  # type: ignore
             for attr in attrs:

tests/test_parsers.py

@@ -2,6 +2,8 @@
 import kdrag.solvers.prolog as prolog
 import kdrag.parsers.tptp as tptp
 import kdrag.parsers.smtlib as smtlib
+import kdrag.parsers.microlean as microlean
+import kdrag.theories.real.seq as seq
 import lark
 import kdrag.smt as smt
 
@@ -33,3 +35,18 @@ def test_smtlib():
     (get-model)
     """
     t = smtlib.parser.parse(ex1)
+
+
+def test_microlean_did_you_mean():
+    ex1 = "has_lim (fun (n : Int) => n) 0"
+    try:
+        microlean.parse(ex1, {"seq": seq})
+    except NameError as exc:
+        assert "seq.has_lim" in str(exc)
+    else:
+        raise AssertionError("Expected NameError with suggestion")
+
+
+def test_microlean_decimal_is_real():
+    t = microlean.parse("1.0", {})
+    assert t.eq(smt.RealVal("1.0"))