feat: Detect undefined symbols

KLR/Python.lean

@@ -183,12 +183,16 @@ An example of a global is:
     else:
       ...
 -/
+instance : Repr Lean.Json where
+  reprPrec jsn _ := jsn.compress
+
 structure Kernel where
   entry : String
   funcs : List (String × Fun)
   args : List Expr'
   kwargs : List (String × Expr')
   globals : List (String × Expr')
+  undefinedSymbols : List Lean.Json
   deriving Repr
 
 /-
@@ -230,6 +234,8 @@ abbrev Parser := StM Pos
 private def str : Json -> Parser String :=
   monadLift ∘ Json.getStr?
 
+private def json (jsn : Json) : Parser Json := return jsn
+
 private def field (f: Json -> Parser a) (j : Json) (name : String) : Parser a :=
   j.getObjVal? name >>= f
 
@@ -461,10 +467,12 @@ def kernel (j : Json) : Parser Kernel := do
   let args <- field (list global) j "args"
   let kwargs <- field (dict global) j "kwargs"
   let globals <- field (dict global) j "globals"
-  return Kernel.mk name funcs args kwargs globals
+  let undefinedSymbols <- field (list json) j "undefined_symbols"
+  return Kernel.mk name funcs args kwargs globals undefinedSymbols
 
 def parse (s : String) : Err Kernel := do
   let jsn <- Json.parse s
   match kernel jsn {} with
-  | .ok x _ => .ok x
+  | .ok x _ =>
+    if !x.undefinedSymbols.isEmpty then .error "undefined symbols" else .ok x
   | .error s _ => .error s

bin/gather

@@ -21,10 +21,12 @@ if len(sys.argv) != 2:
   print(f"Usage: {sys.argv[0]} function", file=sys.stderr)
   sys.exit(1)
 
-pieces = sys.argv[1].split(".")
+[bin, kernel] = sys.argv
+
+pieces = kernel.split(".")
 if len(pieces) < 2:
   print("Please, specify full path name of function, e.g.:", file=sys.stderr)
-  print(f"  {sys.argv[0]} mylib.mykernel", sys.argv[0], file=sys.stderr)
+  print(f"  {bin} mylib.mykernel", file=sys.stderr)
   sys.exit(1)
 
 try:
@@ -33,8 +35,7 @@ try:
   m = importlib.import_module(module)
   f = getattr(m, fn)
   F = klr.parser.Parser(f)
+  print(F.json())
 except Exception as e:
   print(str(e), file=sys.stderr)
   sys.exit(1)
-
-print(F.json())

interop/klr/parser.py

@@ -14,6 +14,8 @@
 from collections import deque
 from textwrap import dedent
 from importlib.resources import files
+from typing import List
+
 
 def up(f, n):
   d = os.path.dirname(f)
@@ -101,6 +103,7 @@ def __init__(self, f: types.FunctionType):
     self.args = []
     self.kwargs = {}
     self.entry = f.__module__ + "." + f.__name__
+    self.undefined_symbols = [] # Lean can send these back to the caller as linter errors
     self.ref_global(self.entry, f)
     self.do_work()
 
@@ -110,6 +113,7 @@ def json(self):
         , 'args' : self.args
         , 'kwargs' : self.kwargs
         , 'globals': self.globals
+        , 'undefined_symbols': self.undefined_symbols
         }
     return json.dumps(d, cls=Enc)
 
@@ -202,7 +206,7 @@ def do_work(self):
         continue
       self.funcs[fullname] = self.translate(src, line, f, args, body)
 
-  def translate(self, src: str, line: int, f: types.FunctionType, args: ast.arguments, body: [ast.AST]):
+  def translate(self, src: str, line: int, f: types.FunctionType, args: ast.arguments, body: List[ast.AST]):
     self.f = f
     for s in body:
       self.visit(s)
@@ -221,14 +225,20 @@ def translate(self, src: str, line: int, f: types.FunctionType, args: ast.argume
   # if we find other uses of potentially global names
   # and fail to understand them; as long as we find and record
   # the "real" uses into the environment for the Lean code.
-  def lookup(self, s):
-    return self.f.__globals__.get(s) or self.f.__builtins__.get(s)
+  def lookup(self, node):
+    s = node.id
+    if s in self.f.__globals__:
+      return self.f.__globals__[s]
+    if s in self.f.__builtins__:
+      return self.f.__builtins__[s]
+    self.undefined_symbols.append(node)
+    return None
 
   def visit_Name(self, node):
     if node.id not in self.f.__code__.co_names:
       return
     try:
-      y = self.lookup(node.id)
+      y = self.lookup(node)
       self.ref_global(node.id, y)
       return node.id, y
     except Unsupported as e:
@@ -250,3 +260,13 @@ def visit_Attribute(self, node):
       raise e
     except Exception:
       return
+
+
+if __name__ == '__main__':
+  y = None
+  z = 5
+
+  def unknown():
+    return (x, y, z)
+
+  print (Parser(unknown).json())

interop/test/test_basic.py

@@ -125,7 +125,7 @@ def test_succeed(f):
 # (These functions are expected to fail elaboration to KLR)
 
 def name_not_found():
-  return x
+  x
 
 @pytest.mark.parametrize("f", [
   name_not_found,