Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix elaboration of case and support as patterns #231

Merged
merged 10 commits into from
Nov 7, 2024
Merged

Fix elaboration of case and support as patterns #231

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
d266c17
No need to turn off type checking globally
chengluyu Nov 6, 2024
5dc38ac
Fix a typo
chengluyu Nov 6, 2024
22a7476
Fix getting modified files from `git status`
chengluyu Nov 6, 2024
2be4a22
Port test files about patterns
chengluyu Nov 6, 2024
b32b647
Fix elaboration of `case` and support `as` patterns
chengluyu Nov 6, 2024
15a7240
Reduce the boilerplate of extractors
chengluyu Nov 6, 2024
79bb49d
Fix a misreference in a test of simple tuple patterns
chengluyu Nov 7, 2024
72bf8ee
Fix the commands of tests of patterns
chengluyu Nov 7, 2024
00de2a2
Merge branch 'hkmc2' into hkmc2-ucs2
LPTK Nov 7, 2024
8ec1356
Rerun test on SimpleTuple.mls
chengluyu Nov 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions hkmc2/jvm/src/test/scala/hkmc2/DiffTestRunner.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,9 @@ object DiffTestRunner:
else if filePath.ext =/= "mls" then N
else S(filePath)
}.toSet catch
case err: Throwable => System.err.println("/!\\ git command failed with: " + err)
Set.empty
case err: Throwable =>
System.err.println("/!\\ git command failed with: " + err)
Set.empty

end State

Expand All @@ -82,7 +83,7 @@ abstract class DiffTestRunner(state: DiffTestRunner.State)
"\n\tNote: you can increase this limit by changing DiffTests.TimeLimit")
// * Thread.stop() is considered bad practice because normally it's better to implement proper logic
// * to terminate threads gracefully, avoiding leaving applications in a bad state.
// * But here we DGAF since all the test is doing is runnign a type checker and some Node REPL,
// * But here we DGAF since all the test is doing is running a type checker and some Node REPL,
// * which would be a much bigger pain to make receptive to "gentle" interruption.
// * It would feel extremely wrong to intersperse the pure type checker algorithms
// * with ugly `Thread.isInterrupted` checks everywhere...
Expand Down
39 changes: 16 additions & 23 deletions hkmc2/shared/src/main/scala/hkmc2/semantics/Desugarer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,33 +6,19 @@ import mlscript.utils.*, shorthands.*
import Message.MessageContext
import utils.TraceLogger
import hkmc2.syntax.Literal
import Keyword.`let`
import Keyword.{as, and, `else`, is, let, `then`}

object Desugarer:
object and:
extension (op: Keyword.Infix)
infix def unapply(tree: Tree): Opt[(Tree, Tree)] = tree match
case InfixApp(lhs, Keyword.and, rhs) => S((lhs, rhs))
case InfixApp(lhs, `op`, rhs) => S((lhs, rhs))
case _ => N

object is:
infix def unapply(tree: Tree): Opt[(Tree, Tree)] = tree match
case InfixApp(lhs, Keyword.is, rhs) => S((lhs, rhs))
case _ => N

object `then`:
infix def unapply(tree: Tree): Opt[(Tree, Tree)] = tree match
case InfixApp(lhs, Keyword.`then`, rhs) => S((lhs, rhs))
case _ => N

object `->`:
/** An extractor that accepts either `A and B` or `A then B`. */
object `~>`:
infix def unapply(tree: Tree): Opt[(Tree, Tree \/ Tree)] = tree match
case InfixApp(lhs, Keyword.and, rhs) => S((lhs, L(rhs)))
case InfixApp(lhs, Keyword.`then`, rhs) => S((lhs, R(rhs)))
case _ => N

object `else`:
infix def unapply(tree: Tree): Opt[(Tree, Tree)] = tree match
case InfixApp(lhs, Keyword.`else`, rhs) => S((lhs, rhs))
case lhs and rhs => S((lhs, L(rhs)))
case lhs `then` rhs => S((lhs, R(rhs)))
case _ => N
end Desugarer

Expand Down Expand Up @@ -182,7 +168,7 @@ class Desugarer(tl: TraceLogger, elaborator: Elaborator)(using raise: Raise, sta
case coda is rhs => fallback => ctx =>
nominate(ctx, finish(term(coda)(using ctx))):
patternSplit(rhs, _)(fallback)
case matches -> consequent => fallback =>
case matches ~> consequent => fallback =>
// There are N > 0 conjunct matches. We use `::[T]` instead of `List[T]`.
// Each match is represented by a pair of a _coda_ and a _pattern_
// that is yet to be elaborated.
Expand Down Expand Up @@ -343,7 +329,7 @@ class Desugarer(tl: TraceLogger, elaborator: Elaborator)(using raise: Raise, sta
post = (res: Split) => s"patternSplit (alternative) >>> ${res.showDbg}"
):
patternSplit(branch, scrutSymbol)(elabFallback(backup)(ctx))(ctx)
case patternAndMatches -> consequent => fallback =>
case patternAndMatches ~> consequent => fallback =>
// There are N > 0 conjunct matches. We use `::[T]` instead of `List[T]`.
// Each match is represented by a pair of a _coda_ and a _pattern_
// that is yet to be elaborated.
Expand Down Expand Up @@ -380,6 +366,13 @@ class Desugarer(tl: TraceLogger, elaborator: Elaborator)(using raise: Raise, sta
pattern match
// A single wildcard pattern.
case Ident("_") => _ => ctx => sequel(ctx)
// Alias pattern
case pat as (alias @ Ident(_)) => fallback =>
val aliasSymbol = VarSymbol(alias, nextUid)
val inner = (ctx: Ctx) =>
val ctxWithAlias = ctx + (alias.name -> aliasSymbol)
Split.Let(aliasSymbol, ref, sequel(ctxWithAlias))
expandMatch(scrutSymbol, pat, inner)(fallback)
// A single variable pattern or constructor pattern without parameters.
case ctor: Ident => fallback => ctx => ctx.get(ctor.name) match
case S(sym: ClassSymbol) => // TODO: refined
Expand Down
31 changes: 10 additions & 21 deletions hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,27 +206,16 @@ extends Importer:
Term.If(body)(body)
case Tree.Quoted(body) => Term.Quoted(term(body))
case Tree.Unquoted(body) => Term.Unquoted(term(body))
case Tree.Case(Block(branches)) => branches.lastOption match
case S(InfixApp(id: Ident, Keyword.`then`, dflt)) =>
val sym = VarSymbol(id, nextUid)
val nestCtx = ctx.copy(locals = ctx.locals ++ Ls(id.name -> sym))
val body = branches.dropRight(1).foldRight(Split.default(term(dflt)(using nestCtx))):
case (InfixApp(target, Keyword.`then`, cons), res) =>
val scrutIdent = Ident("scrut"): Ident
val cond = term(App(Ident("=="), Tree.Tup(id :: target :: Nil)))(using nestCtx)
val scrut = TempSymbol(nextUid, S(cond), "scrut")
Split.Let(scrut, cond, Branch(
scrut.ref(),
Pattern.LitPat(Tree.BoolLit(true)),
Split.default(term(cons)(using nestCtx))
) :: res)
case _ =>
raise(ErrorReport(msg"Unsupported case branch." -> tree.toLoc :: Nil))
Split.default(Term.Error)
Term.Lam(Param(FldFlags.empty, sym, N) :: Nil, Term.If(body)(body))
case _ =>
raise(ErrorReport(msg"Unsupported default case branch." -> tree.toLoc :: Nil))
Term.Error
case Tree.Case(branches) =>
val scrut = VarSymbol(Ident("caseScrut"), nextUid)
val desugarer = new Desugarer(tl, this)
val des = desugarer.patternSplit(branches, scrut)(Split.Nil)(ctx)
scoped("ucs:desugared"):
log(s"Desugared:\n${Split.display(des)}")
val nor = new ucs.Normalization(tl)(des)
scoped("ucs:normalized"):
log(s"Normalized:\n${Split.display(nor)}")
Term.Lam(Param(FldFlags.empty, scrut, N) :: Nil, Term.If(des)(nor))
case Modified(Keyword.`return`, kwLoc, body) =>
Term.Ret(term(body))
case Tree.Region(id: Tree.Ident, body) =>
Expand Down
4 changes: 2 additions & 2 deletions hkmc2/shared/src/main/scala/hkmc2/syntax/Keyword.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,11 +65,11 @@ object Keyword:
val `fun` = Keyword("fun", N, N)
// val `val` = Keyword("val", N, N)
val `var` = Keyword("var", N, N)
val `as` = Keyword("as", N, N)
val `of` = Keyword("of", N, N)
val `or` = Keyword("or", nextPrec, curPrec)
val `and` = Keyword("and", nextPrec, nextPrec)
val `is` = Keyword("is", nextPrec, curPrec, canStartInfixOnNewLine = false)
val `as` = Keyword("as", nextPrec, curPrec)
val `let` = Keyword("let", nextPrec, curPrec)
val `region` = Keyword("region", curPrec, curPrec)
val `rec` = Keyword("rec", N, N)
Expand Down Expand Up @@ -118,7 +118,7 @@ object Keyword:
`abstract`, mut, virtual, `override`, declare, public, `private`)

type Infix = `and`.type | `or`.type | `then`.type | `else`.type | `is`.type | `:`.type | `->`.type |
`=>`.type | `extends`.type | `restricts`.type
`=>`.type | `extends`.type | `restricts`.type | `as`.type

type letLike = `let`.type | `set`.type

Expand Down
1 change: 1 addition & 0 deletions hkmc2/shared/src/main/scala/hkmc2/syntax/ParseRule.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -313,6 +313,7 @@ object ParseRule:
genInfixRule(`and`, (rhs, _: Unit) => lhs => InfixApp(lhs, `and`, rhs)),
genInfixRule(`or`, (rhs, _: Unit) => lhs => InfixApp(lhs, `or`, rhs)),
genInfixRule(`is`, (rhs, _: Unit) => lhs => InfixApp(lhs, `is`, rhs)),
genInfixRule(`as`, (rhs, _: Unit) => lhs => InfixApp(lhs, `as`, rhs)),
genInfixRule(`then`, (rhs, _: Unit) => lhs => InfixApp(lhs, `then`, rhs)),
// genInfixRule(`else`, (rhs, _: Unit) => lhs => InfixApp(lhs, `else`, rhs)),
genInfixRule(`:`, (rhs, _: Unit) => lhs => InfixApp(lhs, `:`, rhs)),
Expand Down
1 change: 0 additions & 1 deletion hkmc2/shared/src/main/scala/hkmc2/syntax/Tree.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,6 @@ enum Tree extends AutoLocated:
case If(split: Tree)
@deprecated("Use If instead", "hkmc2-ucs")
case IfElse(cond: Tree, alt: Tree)
@deprecated("Use If instead", "hkmc2-ucs")
case Case(branches: Tree)
case Region(name: Tree, body: Tree)
case RegRef(reg: Tree, value: Tree)
Expand Down
10 changes: 5 additions & 5 deletions hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,7 +247,7 @@ fact(1)
fun fact2 = case
0 then 1
n then n * fact2(n - 1)
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut@161),LitPat(BoolLit(true)),Else(Lit(IntLit(1)))),Else(App(Ref(.*),Tup(List(Fld(‹›,Ref(n@156),None), Fld(‹›,App(Ref(globalThis:block#52.fact2),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@156),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))),None)))))) (of class hkmc2.semantics.Split$Cons)
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@156),LitPat(IntLit(0)),Else(Lit(IntLit(1)))),Let(n@157,Ref(caseScrut@156),Else(App(Ref(.*),Tup(List(Fld(‹›,Ref(n@157),None), Fld(‹›,App(Ref(globalThis:block#52.fact2),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@157),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))),None))))))) (of class hkmc2.semantics.Split$Cons)

fact2
//│ Type: ⊥
Expand All @@ -260,16 +260,16 @@ class Foo[A](x: A -> A)
//│ Type: ⊤

new Foo(x => x)
//│ Type: Foo[α76_1]
//│ Type: Foo[α74_1]

fun f(g) = new Foo(g)
f
//│ Type: forall α79_2: (α79_2 -> α79_2) -> Foo[α79_2]
//│ Type: forall α77_2: (α77_2 -> α77_2) -> Foo[α77_2]

f(x => x).Foo#x
//│ Type: (α81_1) ->{⊥} α81_1
//│ Type: (α79_1) ->{⊥} α79_1

g => (new Foo(g)).Foo#x
//│ Type: (α86_1 -> α86_1) ->{⊥} (α86_1) ->{⊥} α86_1
//│ Type: (α84_1 -> α84_1) ->{⊥} (α84_1) ->{⊥} α84_1


16 changes: 8 additions & 8 deletions hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ fun power(x) = case
0 then `1.0
n then x `*. power(x)(n - 1)
power
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut@48),LitPat(BoolLit(true)),Else(Quoted(Lit(DecLit(1.0))))),Else(Quoted(App(Ref(.*.),Tup(List(Fld(‹›,Unquoted(Ref(x@41)),None), Fld(‹›,Unquoted(App(App(Ref(globalThis:block#0.power),Tup(List(Fld(‹›,Ref(x@41),None)))),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@42),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),None))))))) (of class hkmc2.semantics.Split$Cons)
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@42),LitPat(IntLit(0)),Else(Quoted(Lit(DecLit(1.0))))),Let(n@43,Ref(caseScrut@42),Else(Quoted(App(Ref(.*.),Tup(List(Fld(‹›,Unquoted(Ref(x@41)),None), Fld(‹›,Unquoted(App(App(Ref(globalThis:block#0.power),Tup(List(Fld(‹›,Ref(x@41),None)))),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@43),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),None)))))))) (of class hkmc2.semantics.Split$Cons)


fun id: [A] -> A -> A
Expand All @@ -22,7 +22,7 @@ fun assertNotZero(x) =
`if (x `== `0.0) then `error else x
let checkedDiv = x `=> y `=> x `/. (assertNotZero(y))
run(checkedDiv)
//│ ═══[ERROR] Cannot quote If(Let($scrut@72,Unquoted(Quoted(App(Ref(.==),Tup(List(Fld(‹›,Unquoted(Ref(x@70)),None), Fld(‹›,Unquoted(Quoted(Lit(DecLit(0.0)))),None)))))),Cons(Branch(Ref($scrut@72),LitPat(BoolLit(true)),Else(Unquoted(Quoted(Ref(.error))))),Else(Unquoted(Ref(x@70))))))
//│ ═══[ERROR] Cannot quote If(Let($scrut@71,Unquoted(Quoted(App(Ref(.==),Tup(List(Fld(‹›,Unquoted(Ref(x@69)),None), Fld(‹›,Unquoted(Quoted(Lit(DecLit(0.0)))),None)))))),Cons(Branch(Ref($scrut@71),LitPat(BoolLit(true)),Else(Unquoted(Quoted(Ref(.error))))),Else(Unquoted(Ref(x@69))))))
//│ Type: Num -> (Num -> Num)


Expand All @@ -35,7 +35,7 @@ show
fun inc(dbg) =
x `=> let c = x `+ `1 in let t = dbg(c) in c
inc
//│ Type: forall α65_2: (CodeBase[out Int, ?, ?] ->{α65_2} ⊤) ->{α65_2} CodeBase[out Int -> Int, ⊥, ?]
//│ Type: forall α63_2: (CodeBase[out Int, ?, ?] ->{α63_2} ⊤) ->{α63_2} CodeBase[out Int -> Int, ⊥, ?]

inc(c => log(show(c)))
//│ Type: CodeBase[out Int -> Int, ⊥, ?]
Expand All @@ -49,11 +49,11 @@ fun body(x, y) = case
fun gib_naive(n) =
(x, y) `=> body(x, y)(n)
let gn5 = run(gib_naive(5))
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut@111),LitPat(BoolLit(true)),Else(Ref(x@101))),Let($scrut@109,App(Ref(.==),Tup(List(Fld(‹›,Ref(n@103),None), Fld(‹›,Lit(IntLit(1)),None)))),Cons(Branch(Ref($scrut@109),LitPat(BoolLit(true)),Else(Ref(y@102))),Else(App(App(Ref(globalThis:block#7.body),Tup(List(Fld(‹›,Ref(y@102),None), Fld(‹›,Quoted(App(Ref(.+),Tup(List(Fld(‹›,Unquoted(Ref(x@101)),None), Fld(‹›,Unquoted(Ref(y@102)),None))))),None)))),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@103),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))))))) (of class hkmc2.semantics.Split$Cons)
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@102),LitPat(IntLit(0)),Else(Ref(x@100))),Cons(Branch(Ref(caseScrut@102),LitPat(IntLit(1)),Else(Ref(y@101))),Let(n@103,Ref(caseScrut@102),Else(App(App(Ref(globalThis:block#7.body),Tup(List(Fld(‹›,Ref(y@101),None), Fld(‹›,Quoted(App(Ref(.+),Tup(List(Fld(‹›,Unquoted(Ref(x@100)),None), Fld(‹›,Unquoted(Ref(y@101)),None))))),None)))),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@103),None), Fld(‹›,Lit(IntLit(1)),None)))),None)))))))) (of class hkmc2.semantics.Split$Cons)

fun bind(rhs, k) = `let x = rhs `in k(x)
bind
//│ Type: forall α102_2, α103_2, α107_2, α110_2, α113_2, α114_2: (CodeBase[out α102_2, out α103_2, ?], CodeBase[in α107_2 out α107_2 ∨ α102_2, ?, ⊥] ->{α110_2} CodeBase[out α113_2, out α114_2, ?]) ->{α110_2} CodeBase[out α113_2, out α103_2 ∨ α114_2, ?]
//│ Type: forall α98_2, α99_2, α103_2, α106_2, α109_2, α110_2: (CodeBase[out α98_2, out α99_2, ?], CodeBase[in α103_2 out α103_2 ∨ α98_2, ?, ⊥] ->{α106_2} CodeBase[out α109_2, out α110_2, ?]) ->{α106_2} CodeBase[out α109_2, out α99_2 ∨ α110_2, ?]

:e
:fixme
Expand All @@ -62,12 +62,12 @@ fun body(x, y) = case
0 then x
1 then y
n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out C, out Any]
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut@145),LitPat(BoolLit(true)),Else(Ref(x@132))),Let($scrut@143,App(Ref(.==),Tup(List(Fld(‹›,Ref(n@134),None), Fld(‹›,Lit(IntLit(1)),None)))),Cons(Branch(Ref($scrut@143),LitPat(BoolLit(true)),Else(Ref(y@133))),Else(App(Ref(globalThis:block#8.bind),Tup(List(Fld(‹›,Quoted(App(Ref(.+),Tup(List(Fld(‹›,Unquoted(Ref(x@132)),None), Fld(‹›,Unquoted(Ref(y@133)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z@137,None)),App(App(Ref(globalThis:block#9.body),Tup(List(Fld(‹›,Ref(y@133),None), Fld(‹›,Ref(z@137),None)))),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@134),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C@141,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Ref(class:CodeBase),List(WildcardTy(None,Some(Ref(class:Int))), WildcardTy(None,Some(Ref(C@141))), WildcardTy(None,Some(Ref(class:Any))))),None))),TyApp(Ref(class:CodeBase),List(WildcardTy(None,Some(Ref(C@141))), WildcardTy(None,Some(Ref(class:Any))))),None))))))))))) (of class hkmc2.semantics.Split$Cons)
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@130),LitPat(IntLit(0)),Else(Ref(x@128))),Cons(Branch(Ref(caseScrut@130),LitPat(IntLit(1)),Else(Ref(y@129))),Let(n@131,Ref(caseScrut@130),Else(App(Ref(globalThis:block#8.bind),Tup(List(Fld(‹›,Quoted(App(Ref(.+),Tup(List(Fld(‹›,Unquoted(Ref(x@128)),None), Fld(‹›,Unquoted(Ref(y@129)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z@134,None)),App(App(Ref(globalThis:block#9.body),Tup(List(Fld(‹›,Ref(y@129),None), Fld(‹›,Ref(z@134),None)))),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@131),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C@138,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Ref(class:CodeBase),List(WildcardTy(None,Some(Ref(class:Int))), WildcardTy(None,Some(Ref(C@138))), WildcardTy(None,Some(Ref(class:Any))))),None))),TyApp(Ref(class:CodeBase),List(WildcardTy(None,Some(Ref(C@138))), WildcardTy(None,Some(Ref(class:Any))))),None))))))))))) (of class hkmc2.semantics.Split$Cons)

fun bind: [G] -> (CodeBase[out Int, out G, out Any], [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C | G, out Any]) -> CodeBase[out Int, out G, out Any]
fun bind(rhs, k) = `let x = rhs `in k(x)
bind
//│ Type: forall α127_2: (CodeBase[out Int, out α127_2, ?], forall α128_3: (CodeBase[out Int, out α128_3, ?]) ->{⊥} CodeBase[out Int, out α128_3 ∨ α127_2, ?]) ->{⊥} CodeBase[out Int, out α127_2, ?]
//│ Type: forall α121_2: (CodeBase[out Int, out α121_2, ?], forall α122_3: (CodeBase[out Int, out α122_3, ?]) ->{⊥} CodeBase[out Int, out α122_3 ∨ α121_2, ?]) ->{⊥} CodeBase[out Int, out α121_2, ?]


:fixme
Expand All @@ -77,7 +77,7 @@ fun body(x, y) = case
1 then y
n then bind of x `+ y, (z => body(y, z)(n - 1)): [C] -> CodeBase[out Int, out C, out Any] -> CodeBase[out Int, out C, out Any]
body
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref($scrut@175),LitPat(BoolLit(true)),Else(Ref(x@162))),Let($scrut@173,App(Ref(.==),Tup(List(Fld(‹›,Ref(n@164),None), Fld(‹›,Lit(IntLit(1)),None)))),Cons(Branch(Ref($scrut@173),LitPat(BoolLit(true)),Else(Ref(y@163))),Else(App(Ref(globalThis:block#10.bind),Tup(List(Fld(‹›,Quoted(App(Ref(.+),Tup(List(Fld(‹›,Unquoted(Ref(x@162)),None), Fld(‹›,Unquoted(Ref(y@163)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z@167,None)),App(App(Ref(globalThis:block#11.body),Tup(List(Fld(‹›,Ref(y@163),None), Fld(‹›,Ref(z@167),None)))),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@164),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C@171,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Ref(class:CodeBase),List(WildcardTy(None,Some(Ref(class:Int))), WildcardTy(None,Some(Ref(C@171))), WildcardTy(None,Some(Ref(class:Any))))),None))),TyApp(Ref(class:CodeBase),List(WildcardTy(None,Some(Ref(class:Int))), WildcardTy(None,Some(Ref(C@171))), WildcardTy(None,Some(Ref(class:Any))))),None))))))))))) (of class hkmc2.semantics.Split$Cons)
//│ /!!!\ Uncaught error: scala.MatchError: Cons(Branch(Ref(caseScrut@157),LitPat(IntLit(0)),Else(Ref(x@155))),Cons(Branch(Ref(caseScrut@157),LitPat(IntLit(1)),Else(Ref(y@156))),Let(n@158,Ref(caseScrut@157),Else(App(Ref(globalThis:block#10.bind),Tup(List(Fld(‹›,Quoted(App(Ref(.+),Tup(List(Fld(‹›,Unquoted(Ref(x@155)),None), Fld(‹›,Unquoted(Ref(y@156)),None))))),None), Fld(‹›,Lam(List(Param(‹›,z@161,None)),App(App(Ref(globalThis:block#11.body),Tup(List(Fld(‹›,Ref(y@156),None), Fld(‹›,Ref(z@161),None)))),Tup(List(Fld(‹›,App(Ref(.-),Tup(List(Fld(‹›,Ref(n@158),None), Fld(‹›,Lit(IntLit(1)),None)))),None))))),Some(Forall(List(QuantVar(C@165,None,None)),FunTy(Tup(List(Fld(‹›,TyApp(Ref(class:CodeBase),List(WildcardTy(None,Some(Ref(class:Int))), WildcardTy(None,Some(Ref(C@165))), WildcardTy(None,Some(Ref(class:Any))))),None))),TyApp(Ref(class:CodeBase),List(WildcardTy(None,Some(Ref(class:Int))), WildcardTy(None,Some(Ref(C@165))), WildcardTy(None,Some(Ref(class:Any))))),None))))))))))) (of class hkmc2.semantics.Split$Cons)

fun gib(n) = (x, y) `=> body(x, y)(n)
let g5 = run(gib(5))
Expand Down
Loading
Loading