Some progress on getting Python working again (#861)

vehicle-python/pyproject.toml

@@ -15,7 +15,7 @@ readme = 'README.md'
 license = { file = 'LICENSE' }
 dynamic = ["version"]
 requires-python = ">=3.9,<3.14"
-dependencies = ["typing_extensions >=4.6,<5"]
+dependencies = ["typing_extensions >=4.6,<5", "jaxtyping>=0.2, <0.3"]
 
 [project.optional-dependencies]
 test = ["pytest >=7.1,<9", "packaging >=23", "pygments >=2.14, <3"]

vehicle-python/src/vehicle_lang/ast/__init__.py

@@ -386,21 +386,6 @@ def __init__(self) -> None:
         raise TypeError("Cannot instantiate abstract class Expression")
 
 
-@dataclass(frozen=True)
-class App(Expression):
-    provenance: Provenance = field(repr=False)
-    function: Expression
-    arguments: Sequence[Expression]
-
-
-@dataclass(frozen=True)
-class PartialApp(Expression):
-    provenance: Provenance = field(repr=False)
-    arity: int
-    function: Expression
-    arguments: Sequence[Expression]
-
-
 @dataclass(frozen=True)
 class Binder(AST):
     provenance: Provenance = field(repr=False)
@@ -409,49 +394,44 @@ class Binder(AST):
 
 
 @dataclass(frozen=True)
-class BoundVar(Expression):
-    provenance: Provenance = field(repr=False)
-    name: Name
-
-
-@dataclass(frozen=True)
-class Builtin(Expression):
+class Pi(Expression):
     provenance: Provenance = field(repr=False)
-    builtin: Union[BuiltinConstant, BuiltinFunction, BuiltinLiteral, BuiltinType]
+    binder: Binder
+    body: Expression
 
 
 @dataclass(frozen=True)
-class FreeVar(Expression):
+class Lam(Expression):
     provenance: Provenance = field(repr=False)
-    name: Name
+    binder: Binder
+    body: Expression
 
 
 @dataclass(frozen=True)
-class Lam(Expression):
+class App(Expression):
     provenance: Provenance = field(repr=False)
-    binders: Sequence[Binder]
-    body: Expression
+    function: Expression
+    arguments: Sequence[Expression]
 
 
 @dataclass(frozen=True)
-class Let(Expression):
+class PartialApp(Expression):
     provenance: Provenance = field(repr=False)
-    bound: Expression
-    binder: Binder
-    body: Expression
+    arity: int
+    function: Expression
+    arguments: Sequence[Expression]
 
 
 @dataclass(frozen=True)
-class Pi(Expression):
+class Var(Expression):
     provenance: Provenance = field(repr=False)
-    binder: Binder
-    body: Expression
+    name: Name
 
 
 @dataclass(frozen=True)
-class Universe(Expression):
+class Builtin(Expression):
     provenance: Provenance = field(repr=False)
-    level: UniverseLevel
+    builtin: Union[BuiltinConstant, BuiltinFunction, BuiltinLiteral, BuiltinType]
 
 
 ################################################################################

vehicle-python/src/vehicle_lang/compile/abc/translation.py

@@ -66,63 +66,34 @@ def translate_expression(
     ) -> vcl_var.Expression:
         if isinstance(expression, vcl_ast.App):
             return self.translate_App(expression)
-        if isinstance(expression, vcl_ast.BoundVar):
-            return self.translate_BoundVar(expression)
+        if isinstance(expression, vcl_ast.Var):
+            return self.translate_Var(expression)
         if isinstance(expression, vcl_ast.Builtin):
             return self.translate_Builtin(expression)
-        if isinstance(expression, vcl_ast.FreeVar):
-            return self.translate_FreeVar(expression)
         if isinstance(expression, vcl_ast.Lam):
             return self.translate_Lam(expression)
-        if isinstance(expression, vcl_ast.Let):
-            return self.translate_Let(expression)
         if isinstance(expression, vcl_ast.PartialApp):
             return self.translate_PartialApp(expression)
         if isinstance(expression, vcl_ast.Pi):
             return self.translate_Pi(expression)
-        if isinstance(expression, vcl_ast.Universe):
-            return self.translate_Universe(expression)
         raise NotImplementedError(type(expression).__name__)
 
     @abstractmethod
     def translate_App(self, expression: vcl_ast.App) -> vcl_var.Expression: ...
 
     @abstractmethod
-    def translate_BoundVar(
-        self, expression: vcl_ast.BoundVar
-    ) -> vcl_var.Expression: ...
+    def translate_Var(self, expression: vcl_ast.Var) -> vcl_var.Expression: ...
 
     @abstractmethod
     def translate_Builtin(self, expression: vcl_ast.Builtin) -> vcl_var.Expression: ...
 
-    @abstractmethod
-    def translate_FreeVar(self, expression: vcl_ast.FreeVar) -> vcl_var.Expression: ...
-
     @abstractmethod
     def translate_Lam(self, expression: vcl_ast.Lam) -> vcl_var.Expression: ...
 
-    def translate_Let(self, expression: vcl_ast.Let) -> vcl_var.Expression:
-        return self.translate_expression(
-            vcl_ast.App(
-                provenance=expression.provenance,
-                function=vcl_ast.Lam(
-                    provenance=expression.provenance,
-                    binders=(expression.binder,),
-                    body=expression.body,
-                ),
-                arguments=[expression.bound],
-            )
-        )
-
     @abstractmethod
     def translate_PartialApp(
         self, expression: vcl_ast.PartialApp
     ) -> vcl_var.Expression: ...
 
     @abstractmethod
     def translate_Pi(self, expression: vcl_ast.Pi) -> vcl_var.Expression: ...
-
-    @abstractmethod
-    def translate_Universe(
-        self, expression: vcl_ast.Universe
-    ) -> vcl_var.Expression: ...

vehicle-python/src/vehicle_lang/compile/python/__init__.py

@@ -94,18 +94,19 @@ def translate_declarations(
                 self.ignored_types.append(name)
 
     def translate_DefFunction(self, declaration: vcl.DefFunction) -> py.stmt:
-        if isinstance(declaration.body, vcl.Lam):
+        body = declaration.body
+        binders = []
+        while isinstance(body, vcl.Lam):
+            binders.append(self.translate_binder(body.binder))
+            body = body.body
+
+        if binders:
             return py.FunctionDef(
                 name=declaration.name,
-                args=py_binder(
-                    *(
-                        self.translate_binder(binder)
-                        for binder in declaration.body.binders
-                    )
-                ),
+                args=py_binder(*binders),
                 body=[
                     py.Return(
-                        value=self.translate_expression(declaration.body.body),
+                        value=self.translate_expression(body),
                         **asdict(declaration.provenance),
                     )
                 ],
@@ -184,11 +185,9 @@ def translate_App(self, expression: vcl.App) -> py.expr:
             meetOrJoin, loss = expression.arguments
             if not isinstance(loss, vcl.Lam):
                 raise VehicleOptimiseTypeError(expression)
-            if len(loss.binders) != 1:
-                raise VehicleOptimiseTypeError(expression)
             # NOTE: We extract the name of the bound variable from the lambda,
             #       which should be the _second_ argument.
-            name = loss.binders[0].name
+            name = loss.binder.name
             return py_app(
                 py_builtin(
                     builtin=expression.function.builtin.__class__.__name__,
@@ -227,7 +226,7 @@ def translate_App(self, expression: vcl.App) -> py.expr:
             provenance=expression.provenance,
         )
 
-    def translate_BoundVar(self, expression: vcl.BoundVar) -> py.expr:
+    def translate_Var(self, expression: vcl.Var) -> py.expr:
         return py_name(expression.name, provenance=expression.provenance)
 
     def translate_Builtin(self, expression: vcl.Builtin) -> py.expr:
@@ -292,16 +291,9 @@ def translate_Builtin(self, expression: vcl.Builtin) -> py.expr:
                 provenance=expression.provenance,
             )
 
-    def translate_FreeVar(self, expression: vcl.FreeVar) -> py.expr:
-        # NOTE: We ignore any declaration where translation touches a type.
-        if expression.name in self.ignored_types:
-            raise EraseType()
-        else:
-            return py_name(expression.name, provenance=expression.provenance)
-
     def translate_Lam(self, expression: vcl.Lam) -> py.expr:
         return py.Lambda(
-            args=py_binder(*(map(self.translate_binder, expression.binders))),
+            args=py_binder(self.translate_binder(expression.binder)),
             body=self.translate_expression(expression.body),
             **asdict(expression.provenance),
         )
@@ -316,9 +308,6 @@ def translate_PartialApp(self, expression: vcl.PartialApp) -> py.expr:
             provenance=expression.provenance,
         )
 
-    def translate_Universe(self, _expression: vcl.Universe) -> py.expr:
-        raise EraseType()
-
 
 def py_name(name: vcl.Name, *, provenance: vcl.Provenance) -> py.Name:
     """Make a name."""