Use HOAS

mcenv · Jul 26, 2023 · bf0b45e · bf0b45e
1 parent 2c0ae58
commit bf0b45e
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 32 deletions.
diff --git a/src/main/kotlin/box/pass/Values.kt b/src/main/kotlin/box/pass/Values.kt
@@ -2,7 +2,6 @@ package box.pass
 
 import box.ast.Core.Definition
 import box.ast.Core.Pattern
-import box.ast.Core.Term
 import box.ast.common.Lvl
 import box.ast.common.Proj
 import box.ast.common.Repr
@@ -312,9 +311,6 @@ sealed class Value {
   }
 }
 
-typealias Env = PersistentList<Lazy<Value>>
+typealias Closure = ((List<Lazy<Value>>) -> Value)
 
-data class Closure(
-  val env: Env,
-  val body: Term,
-)
+typealias Env = PersistentList<Lazy<Value>>
diff --git a/src/main/kotlin/box/pass/backend/Stage.kt b/src/main/kotlin/box/pass/backend/Stage.kt
@@ -142,12 +142,12 @@ class Stage private constructor() {
           modify(this + lazyOf(Value.Var("#${next()}", next(), type)))
           param to type
         }
-        val result = Closure(this, term.result)
+        val result = { args: List<Lazy<Value>> -> (this + args).evalTerm(term.result, phase) }
         Value.Func(term.open, params, result)
       }
 
       is Term.FuncOf     -> {
-        val result = Closure(this, term.result)
+        val result = { args: List<Lazy<Value>> -> (this + args).evalTerm(term.result, phase) }
         val type = lazy { evalTerm(term.type, phase) }
         Value.FuncOf(term.open, term.params, result, type)
       }
@@ -159,7 +159,7 @@ class Stage private constructor() {
           Phase.WORLD -> null
           Phase.CONST -> {
             when (func) {
-              is Value.FuncOf  -> func.result(args, phase)
+              is Value.FuncOf  -> func.result(args)
               is Value.Builtin -> func.builtin(args)
               else             -> null
             }
@@ -430,7 +430,7 @@ class Stage private constructor() {
           pattern to (this + i).quoteValue(type.value, phase)
         }
         val result = (this + value.params.size).quoteValue(
-          value.result.open(this, value.params.map { (_, type) -> type }, phase),
+          value.result.open(this, value.params.map { (_, type) -> type }),
           phase,
         )
         Term.Func(value.open, params, result)
@@ -441,7 +441,6 @@ class Stage private constructor() {
           value.result.open(
             this,
             (value.type.value as Value.Func /* TODO: unify */).params.map { (_, type) -> type },
-            phase,
           ),
           phase,
         )
@@ -540,21 +539,13 @@ class Stage private constructor() {
     }
   }
 
-  private operator fun Closure.invoke(
-    args: List<Lazy<Value>>,
-    phase: Phase,
-  ): Value {
-    return (env + args).evalTerm(body, phase)
-  }
-
   private fun Closure.open(
     next: Lvl,
     types: List<Lazy<Value>>,
-    phase: Phase,
   ): Value {
     return this(types.mapIndexed { i, type ->
       lazyOf(Value.Var("#${next + i}", next + i, type))
-    }, phase)
+    })
   }
 
   companion object {

diff --git a/src/main/kotlin/box/pass/frontend/elaborate/Elaborate.kt b/src/main/kotlin/box/pass/frontend/elaborate/Elaborate.kt
@@ -7,8 +7,11 @@ import box.lsp.Instruction
 import box.lsp.contains
 import box.lsp.diagnostic
 import box.lsp.rangeTo
-import box.pass.*
+import box.pass.Env
+import box.pass.Phase
+import box.pass.Value
 import box.pass.frontend.Resolve
+import box.pass.prettyTerm
 import box.util.collections.mapWith
 import box.util.unreachable
 import kotlinx.collections.immutable.PersistentList
@@ -288,7 +291,7 @@ class Elaborate private constructor(
           }
         }
         val (result, resultType) = ctx.elaborateTerm(term.result, null, phase)
-        val type = Value.Func(term.open, params, Closure(env, next().quoteValue(resultType)))
+        val type = Value.Func(term.open, params) { args -> (env + args).evalTerm(next().quoteValue(resultType)) }
         typed(type) {
           C.Term.FuncOf(term.open, params.map { param -> param.first }, result, it)
         }

diff --git a/src/main/kotlin/box/pass/frontend/elaborate/Normalize.kt b/src/main/kotlin/box/pass/frontend/elaborate/Normalize.kt
@@ -122,12 +122,12 @@ fun Env.evalTerm(term: Term): Value {
         modify(this + lazyOf(Value.Var("#${next()}", next(), type)))
         param to type
       }
-      val result = Closure(this, term.result)
+      val result = { args: List<Lazy<Value>> -> (this + args).evalTerm(term.result) }
       Value.Func(term.open, params, result)
     }
 
     is Term.FuncOf     -> {
-      val result = Closure(this, term.result)
+      val result = { args: List<Lazy<Value>> -> (this + args).evalTerm(term.result) }
       val type = lazy { evalTerm(term.type) }
       Value.FuncOf(term.open, term.params, result, type)
     }
@@ -450,14 +450,7 @@ fun Lvl.quoteValue(value: Value): Term {
 }
 
 /**
- * Applies [this] [Closure] closure to [args] and returns the result [Value].
- */
-operator fun Closure.invoke(args: List<Lazy<Value>>): Value {
-  return (env + args).evalTerm(body)
-}
-
-/**
- * Converts [this] [Closure] closure to an open [Value] with the free variables of [types] under the context of the [size].
+ * Converts [this] closure to an open [Value] with the free variables of [types] under the context of the [size].
  */
 fun Closure.open(
   size: Lvl,