chore: update python tests to use new parser

NKL/FFI.lean

@@ -24,6 +24,6 @@ def parse_json_old (json : String) : IO Unit := do
 @[export parse_json]
 def parse_json (s : String) : IO Unit := do
   let kernel <- Python.Parsing.parse s
-  for (n,f) in kernel.funcs do
-    IO.println s!"found {n}"
-    IO.println s!"{repr f}"
+  let names := kernel.funcs.map fun x => x.fst
+  let names := String.intercalate "," names
+  IO.println s!"Found functions: {names}"

NKL/Python.lean

@@ -32,6 +32,8 @@ inductive Const where
   | ellipsis
   deriving Repr
 
+-- We don't need these, but we preserve them to make copying
+-- the Python AST over easier.
 inductive Ctx where
   | load | store | del
   deriving Repr
@@ -80,6 +82,25 @@ inductive Stmt' where
   deriving Repr
 end
 
+/-
+This structure is a mirror of the python arguments AST node.
+If we have the following Python function:
+
+  def f(a, b=1, /, c=2, *args, d, e=3, **kwargs): pass
+
+then the structure will be populated with:
+
+  posonlyargs = [a, b]
+  args = [c]
+  defaults = [1, 2]
+  vararg = "args"
+  kwonlyargs = [d, e]
+  kw_defaults = [None, 3]
+  kwarg = "kwargs"
+
+Note, defaults and kw_defaults are inconsistent in how they treat
+missing arguments, but this is just how it works in the python AST.
+-/
 structure Args where
   posonlyargs : List String
   args : List String
@@ -90,6 +111,12 @@ structure Args where
   kwarg : Option String
   deriving Repr
 
+/-
+In addition to the defaults above from the AST, we also collect
+the values from f.__defaults__ here in the Fun structure. These
+values are evaluated in a different context from the other names
+in the function, so we need to capture them on the Python side.
+-/
 structure Fun where
   source : String
   args : Args

interop/nkl/parser.py

@@ -10,6 +10,25 @@
 from textwrap import dedent
 from itertools import chain
 from collections import deque
+from nkl.lean import py_to_lean
+
+# This is a custom JSON encoder for use with AST nodes.
+# The AST nodes are not handled by the default encoder.
+# For an AST node, we return a dictionary with the class
+# name mapped to the object dictionary. If the object
+# dictionary is empty we just return the class name.
+# e.g.
+# Binop(left=l,op=o,right=r), becomes:
+#    { BinOp : { left:l, op:o, right:r } }
+# Pass(), becomes
+#    'Pass'
+#
+# For anything else not handled by the default
+# encoder, we return "...", the Ellipsis.
+# Conveniently, Ellipsis is one of the things
+# that isn't handled, so it is properly mapped.
+
+# See also: NKL/Python.lean for the Lean side
 
 class Enc(json.JSONEncoder):
   def default(self, obj):
@@ -40,6 +59,10 @@ def json(self):
         }
     return json.dumps(d, cls=Enc)
 
+  # TODO: just a placeholder for testing
+  def load(self):
+    py_to_lean(self.json())
+
   # resolve a reference: either populating the environment,
   # or adding new items to the work queue
   def reference(self, refname, val):

interop/test/test_examples.py

@@ -1,7 +1,7 @@
 import pytest
 
 from examples import *
-from nkl.loader import Loader
+from nkl.parser import Parser
 
 @pytest.mark.parametrize("module,name",
     [ (getting_started, "nki_tensor_add_kernel"),
@@ -31,6 +31,5 @@
     ])
 def test_parse(module, name):
   f = getattr(module, name)
-  F = Loader(f)
-  F.translate(F.ast)
-
+  F = Parser(f)
+  F.load()