From bf0b45e399db67a9f27308827bd786a98f2c0122 Mon Sep 17 00:00:00 2001 From: intsuc Date: Thu, 27 Jul 2023 02:57:16 +0900 Subject: [PATCH] Use HOAS --- src/main/kotlin/box/pass/Values.kt | 8 ++------ src/main/kotlin/box/pass/backend/Stage.kt | 19 +++++-------------- .../box/pass/frontend/elaborate/Elaborate.kt | 7 +++++-- .../box/pass/frontend/elaborate/Normalize.kt | 13 +++---------- 4 files changed, 15 insertions(+), 32 deletions(-) diff --git a/src/main/kotlin/box/pass/Values.kt b/src/main/kotlin/box/pass/Values.kt index dd9ea672..e1e144bf 100644 --- 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> +typealias Closure = ((List>) -> Value) -data class Closure( - val env: Env, - val body: Term, -) +typealias Env = PersistentList> diff --git a/src/main/kotlin/box/pass/backend/Stage.kt b/src/main/kotlin/box/pass/backend/Stage.kt index 278fc327..217f38dc 100644 --- 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> -> (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> -> (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>, - phase: Phase, - ): Value { - return (env + args).evalTerm(body, phase) - } - private fun Closure.open( next: Lvl, types: List>, - 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 index 87c36c5c..b89263a2 100644 --- 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 index e3e85a55..9148ca4f 100644 --- 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> -> (this + args).evalTerm(term.result) } Value.Func(term.open, params, result) } is Term.FuncOf -> { - val result = Closure(this, term.result) + val result = { args: List> -> (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>): 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,