chore: remove unused code

NKL.lean

@@ -5,5 +5,5 @@ Authors: Paul Govereau
 -/
 import NKL.Encode
 import NKL.FFI
-import NKL.NKI
+import NKL.KLR
 import NKL.Python

NKL/Python.lean

@@ -31,8 +31,19 @@ inductive Const where
   | ellipsis
   deriving Repr
 
--- This context comes from the Python AST.
--- The store hint is used by the tracing implementation for simplicity.
+/-
+This context comes from the Python AST. The different hints
+indicated how an l-value term is being used. For example:
+
+  x = 1         # x is store context
+  return x + 5  # x is load context
+  del x         # x is del context
+
+The store hint is used by the tracing implementation for
+simplicity: we do not try to resolve names that are being
+"stored" to.
+-/
+
 inductive Ctx where
   | load | store | del
   deriving Repr
@@ -140,6 +151,15 @@ A kernel is collection of:
     are in the field `args` and the keyword argument are in the
     field `kwargs`
   - global variables referenced by any of the functions
+
+An example of a global is:
+
+  use_fancy_thing = true   # this will end up in globals
+  def kernel():
+    if use_fancy_thing:
+      ...
+    else:
+      ...
 -/
 structure Kernel where
   entry : String

interop/mk.sh

@@ -6,8 +6,8 @@ set -x
 # Need to decide which of lake or setuptools is better to use,
 # and how we will distribute everything
 
-# make sure libNKL.a and lean_types.py are generated
-(cd ..; lake build NKL Export)
+# make sure libNKL.a is generated
+(cd ..; lake build NKL)
 
 LEAN_PREFIX=$(lean --print-prefix)
 LEAN_CFLAGS="-I${LEAN_PREFIX}/include"

interop/nkl/__init__.py

@@ -3,11 +3,4 @@
 # Authors: Paul Govereau
 
 from .lean import load, to_json
-from .loader import Loader
-
-def parse(f):
-  F = Loader(f)
-  return F.translate(F.ast)
-
-def parse_and_load(f):
-  load(parse(f))
+from .parser import Parser

interop/nkl/lean.py

@@ -3,7 +3,6 @@
 # Authors: Paul Govereau
 
 import json
-from nkl.lean_types import *
 from nkl.lean_rffi import *
 
 def to_json_dict(obj):
@@ -20,8 +19,8 @@ def to_json_dict(obj):
     return d
   return obj
 
-def to_json(f: Fun):
+def to_json(f):
   return json.dumps(to_json_dict(f))
 
-def load(f: Fun):
+def load(f):
   py_to_lean(to_json(f))