From 53956580411686302b5f9379329bccfe31d17b66 Mon Sep 17 00:00:00 2001 From: NeilKleistGao Date: Wed, 11 Dec 2024 15:23:07 +0800 Subject: [PATCH] Remove unnecessary Alloc type --- .../src/main/scala/hkmc2/bbml/bbML.scala | 13 +-- .../scala/hkmc2/semantics/Elaborator.scala | 6 -- .../src/test/mlscript/bbml/bbBorrowing.mls | 42 +++++----- .../src/test/mlscript/bbml/bbBorrowing2.mls | 10 +-- .../test/mlscript/bbml/bbLetRegEncoding.mls | 38 ++++----- .../shared/src/test/mlscript/bbml/bbList.mls | 74 +++++++--------- .../src/test/mlscript/bbml/bbPrelude.mls | 2 - hkmc2/shared/src/test/mlscript/bbml/bbRef.mls | 84 +++++++++---------- hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls | 12 +-- 9 files changed, 123 insertions(+), 158 deletions(-) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala index b30d1a0be..94e116c69 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala @@ -41,7 +41,6 @@ final case class BbCtx( given (using ctx: BbCtx): Raise = ctx.raise object BbCtx: - def allocTy(using ctx: BbCtx): Type = ClassLikeType(ctx.getCls("Alloc").get, Nil) def intTy(using ctx: BbCtx): Type = ClassLikeType(ctx.getCls("Int").get, Nil) def numTy(using ctx: BbCtx): Type = ClassLikeType(ctx.getCls("Num").get, Nil) def strTy(using ctx: BbCtx): Type = ClassLikeType(ctx.getCls("Str").get, Nil) @@ -77,9 +76,6 @@ class BBTyper(using elState: Elaborator.State, tl: TL): // in.state.upperBounds ::= out // * Not needed for soundness; complicates inferred types Wildcard(in, out) - private def allocType(using BbCtx): Type = - BbCtx.allocTy - private def error(msg: Ls[Message -> Opt[Loc]])(using BbCtx) = raise(ErrorReport(msg)) Bot // TODO: error type? @@ -100,10 +96,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): case N => ctx.get(sym) match case Some(ty) => ty case _ => - if sym.nme === "Alloc" then - allocType - else - error(msg"Variable not found: ${sym.nme}" -> ty.toLoc :: Nil) + error(msg"Variable not found: ${sym.nme}" -> ty.toLoc :: Nil) case FunTy(Term.Tup(params), ret, eff) => PolyFunType(params.map { case Fld(_, p, _) => typeAndSubstType(p, !pol) @@ -517,7 +510,7 @@ class BBTyper(using elState: Elaborator.State, tl: TL): val (res, eff) = typeCheck(body) val tv = freshVar(N)(using ctx) constrain(eff, tv | sk) - (extrude(res)(using ctx, true), tv | allocType) + (extrude(res)(using ctx, true), tv) case Term.RegRef(reg, value) => val (regTy, regEff) = typeCheck(reg) val (valTy, valEff) = typeCheck(value) @@ -551,5 +544,5 @@ class BBTyper(using elState: Elaborator.State, tl: TL): def typePurely(t: Term)(using BbCtx): GeneralType = val (ty, eff) = typeCheck(t) given CCtx = CCtx.init(t, N) - constrain(eff, allocType) + constrain(eff, Bot) ty diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala index 20103a46a..20bda70ca 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala @@ -133,11 +133,6 @@ class Elaborator(val tl: TraceLogger, val wd: os.Path) extends Importer: import tl.* - // * Ref allocation skolem UID, preserved - private val allocSkolemSym = VarSymbol(Ident("Alloc")) - private val allocSkolemDef = TyParam(FldFlags.empty, N, allocSkolemSym) - allocSkolemSym.decl = S(allocSkolemDef) - def mkLetBinding(sym: LocalSymbol, rhs: Term): Ls[Statement] = LetDecl(sym) :: DefineVar(sym, rhs) :: Nil @@ -220,7 +215,6 @@ extends Importer: case N => raise(ErrorReport(msg"Cannot use 'this' outside of an object scope." -> tree.toLoc :: Nil)) Term.Error - case id @ Ident("Alloc") => Term.Ref(allocSkolemSym)(id, 1) case id @ Ident(name) => ctx.get(name) match case S(sym) => sym.ref(id) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls index 1a4586da3..56f3fb78c 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls @@ -37,7 +37,7 @@ fun next: [A, Br] -> Iter[A, Br] ->{Br} A letreg(r => r) //│ Type: Reg[?, E23_1] //│ Where: -//│ E23_1 <: Alloc +//│ E23_1 <: ⊥ letreg of r => let b = mkVec(r) @@ -49,7 +49,7 @@ letreg of r => r //│ Type: Reg[?, E28_1] //│ Where: -//│ E28_1 <: Alloc +//│ E28_1 <: ⊥ // * Non-lexical borrowing pattern encoded with a thunk @@ -89,11 +89,11 @@ letreg of r => //│ ║ ^^^^^^^^^^^^^^^^^^ //│ ║ l.74: k() //│ ║ ^^^^^ -//│ ╟── because: cannot constrain E73_1 <: Alloc -//│ ╟── because: cannot constrain E73_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ ¬Rg96_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ~{Alloc} <: Rg96_1 -//│ ╙── because: cannot constrain ~{Alloc} <: ¬() +//│ ╟── because: cannot constrain E73_1 <: ⊥ +//│ ╟── because: cannot constrain E73_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ ¬Rg96_1 <: ¬() +//│ ╟── because: cannot constrain <: Rg96_1 +//│ ╙── because: cannot constrain <: ¬() //│ Type: ⊥ :e @@ -125,15 +125,15 @@ letreg of r => //│ ║ ^^^^^^^^^^ //│ ║ l.108: r //│ ║ ^^^ -//│ ╟── because: cannot constrain E97_1 <: Alloc -//│ ╟── because: cannot constrain E97_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ Rg117_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain Rg117_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain E97_1 <: ⊥ +//│ ╟── because: cannot constrain E97_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ Rg117_1 <: ¬() +//│ ╟── because: cannot constrain Rg117_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Reg[?, E97_1] //│ Where: //│ ⊤ <: E97_1 -//│ E97_1 <: Alloc +//│ E97_1 <: ⊥ letreg of r => @@ -144,7 +144,7 @@ letreg of r => r //│ Type: Reg[?, E123_1] //│ Where: -//│ E123_1 <: Alloc +//│ E123_1 <: ⊥ :e letreg of r => @@ -169,15 +169,15 @@ letreg of r => //│ ║ ^^^^^^^^ //│ ║ l.156: r //│ ║ ^^^ -//│ ╟── because: cannot constrain E137_1 <: Alloc -//│ ╟── because: cannot constrain E137_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ Rg149_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain Rg149_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain E137_1 <: ⊥ +//│ ╟── because: cannot constrain E137_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ Rg149_1 <: ¬() +//│ ╟── because: cannot constrain Rg149_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Reg[?, E137_1] //│ Where: //│ ⊤ <: E137_1 -//│ E137_1 <: Alloc +//│ E137_1 <: ⊥ letreg of r0 => letreg of r1 => @@ -188,7 +188,7 @@ letreg of r0 => r1 //│ Type: Reg[?, in E174_1] //│ Where: -//│ E174_1 <: Alloc +//│ E174_1 <: ⊥ // * Can leak the iterator diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls index 79d8c5bca..07403561b 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls @@ -46,11 +46,11 @@ letreg of r => //│ ║ ^^^^^^^^^^^ //│ ║ l.35: write(r) //│ ║ ^^^^^^^^^^ -//│ ╟── because: cannot constrain E29_1 <: Alloc -//│ ╟── because: cannot constrain E29_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ Rg41_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain Rg41_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain E29_1 <: ⊥ +//│ ╟── because: cannot constrain E29_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ Rg41_1 <: ¬() +//│ ╟── because: cannot constrain Rg41_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls index c954a5c7c..d38f48fc9 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls @@ -30,11 +30,11 @@ letreg(r => r).ref 1 //│ ╔══[ERROR] Type error in block //│ ║ l.16: letreg(r => r).ref 1 //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α15_1 ∨ E10_1 <: Alloc -//│ ╟── because: cannot constrain α15_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain R14_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain R14_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α15_1 ∨ E10_1 <: ⊥ +//│ ╟── because: cannot constrain α15_1 <: ¬() +//│ ╟── because: cannot constrain R14_1 <: ¬() +//│ ╟── because: cannot constrain R14_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Ref[Int, ?] letreg(r => r.ref 1) @@ -48,13 +48,13 @@ letreg(r => !(r.ref 1)) //│ ╔══[ERROR] Type error in block //│ ║ l.47: !letreg(r => r.ref 1) //│ ║ ^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α34_1 ∨ E28_1 <: Alloc -//│ ╟── because: cannot constrain α34_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α32_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α32_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ R33_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain R33_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α34_1 ∨ E28_1 <: ⊥ +//│ ╟── because: cannot constrain α34_1 <: ¬() +//│ ╟── because: cannot constrain α32_1 <: ¬() +//│ ╟── because: cannot constrain α32_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ R33_1 <: ¬() +//│ ╟── because: cannot constrain R33_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Int letreg of r => @@ -74,13 +74,13 @@ letreg(r => arg => r.ref arg)(0) //│ ╔══[ERROR] Type error in block //│ ║ l.73: letreg(r => arg => r.ref arg)(0) //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain α63_1 ∨ E54_1 <: Alloc -//│ ╟── because: cannot constrain α63_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α61_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α61_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ R62_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain R62_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α63_1 ∨ E54_1 <: ⊥ +//│ ╟── because: cannot constrain α63_1 <: ¬() +//│ ╟── because: cannot constrain α61_1 <: ¬() +//│ ╟── because: cannot constrain α61_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ R62_1 <: ¬() +//│ ╟── because: cannot constrain R62_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Ref[arg59_1, ?] //│ Where: //│ Int <: arg59_1 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls index 92ca159c9..caff09953 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbList.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbList.mls @@ -11,13 +11,13 @@ fun map: [A, B, E] -> List[out A] -> (A ->{E} B) ->{E} List[out B] // * Dummy implementation -fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{Alloc | E} List[out A] +fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{E} List[out A] fun mapi = s => f => region r in map(s) of x => f(0, x) //│ Type: ⊤ -fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{Alloc | E} List[out A] +fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{E} List[out A] fun mapi = s => f => region r in let i = r.ref 0 @@ -43,14 +43,14 @@ region r in // * Should be an error. This definition would not be referentially transparent. // * The error message needs improvement, though. :e -fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{Alloc | E} List[out A] +fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{E} List[out A] fun mapi = s => region r in let i = r.ref 0 f => map(s) of x => i := !i + 1 f(!i, x) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 54_2) ->{55_2} 54_2) ->{55_2} List[out 54_2] //│ ║ l.49: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.50: f => map(s) of x => @@ -59,15 +59,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.52: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] -//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ 56_2 -//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~56_2) -//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~56_2) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] +//│ ╟── because: cannot constrain f70_2 ->{E78_2} List[out B77_2] <: ((Int, 54_2) ->{55_2} 54_2) ->{55_2} List[out 54_2] +//│ ╟── because: cannot constrain D( E78_2 ) <: 55_2 +//│ ╟── because: cannot constrain E78_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain α79_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain r80_2 <: ¬(~55_2) +//│ ╙── because: cannot constrain <: ¬(~55_2) +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 54_2) ->{55_2} 54_2) ->{55_2} List[out 54_2] //│ ║ l.49: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.50: f => map(s) of x => @@ -76,15 +76,15 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.52: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] -//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ 56_2 -//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~56_2) -//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~56_2) -//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] +//│ ╟── because: cannot constrain f70_2 ->{E78_2} List[out B77_2] <: ((Int, 54_2) ->{55_2} 54_2) ->{55_2} List[out 54_2] +//│ ╟── because: cannot constrain D( E78_2 ) <: 55_2 +//│ ╟── because: cannot constrain E78_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain α79_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain r80_2 <: ¬(~55_2) +//│ ╙── because: cannot constrain <: ¬(~55_2) +//│ ╔══[ERROR] Type error in region expression with expected type ((Int, 54_2) ->{55_2} 54_2) ->{55_2} List[out 54_2] //│ ║ l.49: let i = r.ref 0 //│ ║ ^^^^^^^ //│ ║ l.50: f => map(s) of x => @@ -93,28 +93,14 @@ fun mapi = s => //│ ║ ^^^^^^^^^^^^^^^^^ //│ ║ l.52: f(!i, x) //│ ║ ^^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] -//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ 56_2 -//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~56_2) -//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~56_2) -//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~56_2) -//│ ╔══[ERROR] Type error in function literal with expected type (List[out 55_2]) ->{⊥} ((Int, 55_2) ->{56_2} 55_2) ->{Alloc ∨ 56_2} List[out 55_2] -//│ ║ l.47: fun mapi = s => -//│ ║ ^^^^ -//│ ║ l.48: region r in -//│ ║ ^^^^^^^^^^^^^ -//│ ║ l.49: let i = r.ref 0 -//│ ║ ^^^^^^^^^^^^^^^^^^^ -//│ ║ l.50: f => map(s) of x => -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^ -//│ ║ l.51: i := !i + 1 -//│ ║ ^^^^^^^^^^^^^^^^^ -//│ ║ l.52: f(!i, x) -//│ ║ ^^^^^^^^^^^^^^ -//│ ╙── because: cannot constrain α70_2 ∨ Alloc <: ⊥ +//│ ╟── because: cannot constrain f70_2 ->{E78_2} List[out B77_2] <: ((Int, 54_2) ->{55_2} 54_2) ->{55_2} List[out 54_2] +//│ ╟── because: cannot constrain D( E78_2 ) <: 55_2 +//│ ╟── because: cannot constrain E78_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain α79_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~55_2) +//│ ╟── because: cannot constrain r80_2 <: ¬(~55_2) +//│ ╙── because: cannot constrain <: ¬(~55_2) //│ Type: ⊤ diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPrelude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPrelude.mls index 7dc6c9387..7400a1ea5 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbPrelude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbPrelude.mls @@ -1,7 +1,5 @@ // :bbml -class Alloc - class CodeBase[T, C, S] class Region[T] class Ref[T, S] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls index 7674ef08b..cfb4fbdc5 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls @@ -24,18 +24,18 @@ let r = region x in x.ref 42 //│ ║ ^^^^^^^^ //│ ║ l.21: !r //│ ║ ^^ -//│ ╟── because: cannot constrain (α23_1 ∨ α20_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α23_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α21_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α21_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ x22_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain x22_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α23_1 ∨ α20_1 <: ⊥ +//│ ╟── because: cannot constrain α23_1 <: ¬() +//│ ╟── because: cannot constrain α21_1 <: ¬() +//│ ╟── because: cannot constrain α21_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ x22_1 <: ¬() +//│ ╟── because: cannot constrain x22_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Int fun mkRef() = region x in x.ref 42 mkRef -//│ Type: () ->{Alloc} Ref[Int, ?] +//│ Type: () -> Ref[Int, ?] :e let t = region x in x in t.ref 42 @@ -53,11 +53,11 @@ let t = region x in x in t.ref 42 //│ ╔══[ERROR] Type error in block //│ ║ l.41: let t = region x in x in t.ref 42 //│ ║ ^^^^^^^^^^^^^ -//│ ╟── because: cannot constrain (α35_1 ∨ α32_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α35_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain x34_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain x34_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α35_1 ∨ α32_1 <: ⊥ +//│ ╟── because: cannot constrain α35_1 <: ¬() +//│ ╟── because: cannot constrain x34_1 <: ¬() +//│ ╟── because: cannot constrain x34_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Ref[Int, ?] @@ -74,13 +74,13 @@ in t := 0 //│ ║ ^^^^^^^^ //│ ║ l.71: in t := 0 //│ ║ ^^^^^^^^^ -//│ ╟── because: cannot constrain (α45_1 ∨ α42_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α45_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α43_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α43_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ x44_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain x44_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α45_1 ∨ α42_1 <: ⊥ +//│ ╟── because: cannot constrain α45_1 <: ¬() +//│ ╟── because: cannot constrain α43_1 <: ¬() +//│ ╟── because: cannot constrain α43_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ x44_1 <: ¬() +//│ ╟── because: cannot constrain x44_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Int @@ -97,41 +97,35 @@ in !t //│ ║ ^^^^^^^^ //│ ║ l.94: in !t //│ ║ ^^^^^ -//│ ╟── because: cannot constrain (α57_1 ∨ α54_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α57_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α55_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain α55_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ x56_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain x56_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α57_1 ∨ α54_1 <: ⊥ +//│ ╟── because: cannot constrain α57_1 <: ¬() +//│ ╟── because: cannot constrain α55_1 <: ¬() +//│ ╟── because: cannot constrain α55_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ x56_1 <: ¬() +//│ ╟── because: cannot constrain x56_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Int region x in let r = x.ref 42 in let t = r := 0 in !r //│ Type: Int -fun rid: [A] -> A ->{Alloc} A +fun rid: [A] -> A -> A fun rid(x) = let t = (region y in 42) in x //│ Type: ⊤ -:e + fun rid: [A] -> A -> A fun rid(x) = let t = (region y in 42) in x -//│ ╔══[ERROR] Type error in function literal with expected type (73_2) ->{⊥} 73_2 -//│ ║ l.120: fun rid(x) = -//│ ║ ^^^^ -//│ ║ l.121: let t = (region y in 42) in x -//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -//│ ╙── because: cannot constrain α75_2 ∨ Alloc <: ⊥ //│ Type: ⊤ :e region x in (let dz = x.ref 42 in 42): [A] -> Int //│ ╔══[ERROR] Type error in block with expected type forall A77_3: Int -//│ ║ l.132: (let dz = x.ref 42 in 42): [A] -> Int +//│ ║ l.126: (let dz = x.ref 42 in 42): [A] -> Int //│ ║ ^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain α79_3 <: ⊥ //│ ╟── because: cannot constrain α79_3 <: ¬() @@ -145,18 +139,18 @@ let t = y => x.ref y in t(42) //│ ╔══[ERROR] Type error in block -//│ ║ l.145: y => x.ref y +//│ ║ l.139: y => x.ref y //│ ║ ^^^^^^^^^^^^ -//│ ║ l.146: in t(42) +//│ ║ l.140: in t(42) //│ ║ ^^^^^^^^ -//│ ╟── because: cannot constrain (α90_1 ∨ α84_1) ∨ Alloc <: Alloc -//│ ╟── because: cannot constrain α90_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain ¬⊥ ∧ x91_1 <: ¬(~{Alloc}) -//│ ╟── because: cannot constrain x91_1 <: ¬(~{Alloc}) -//│ ╙── because: cannot constrain <: ¬(~{Alloc}) +//│ ╟── because: cannot constrain α90_1 ∨ α84_1 <: ⊥ +//│ ╟── because: cannot constrain α90_1 <: ¬() +//│ ╟── because: cannot constrain ¬⊥ ∧ x91_1 <: ¬() +//│ ╟── because: cannot constrain x91_1 <: ¬() +//│ ╙── because: cannot constrain <: ¬() //│ Type: Ref[in y86_1 out y86_1 ∨ Int, ?] -fun foo: [A] -> Int ->{A | Alloc} Int +fun foo: [A] -> Int ->{A} Int fun foo(x) = region y in x + 1 //│ Type: ⊤ @@ -189,6 +183,6 @@ bar :e region x in x.ref bar //│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall A119_2: (A119_2) ->{⊥} A119_2) ->{⊥} Int found -//│ ║ l.190: region x in x.ref bar +//│ ║ l.184: region x in x.ref bar //│ ╙── ^^^ //│ Type: Ref[⊥, ?] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls index 8c9680a1c..9fd0af1cd 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls @@ -18,7 +18,7 @@ fun force_cache: [A, B, E] -> Seq[out A, out E] ->{E} Seq[out B, Nothing] // * Dummy implementation -fun mapi: [A, E] -> Seq[out A, out E] -> ((Int, A) ->{E} A) ->{Alloc} Seq[out A, out E] +fun mapi: [A, E] -> Seq[out A, out E] -> ((Int, A) ->{E} A) ->{Nothing} Seq[out A, out E] fun mapi = s => f => region r in map(s) of x => f(0, x) @@ -27,7 +27,7 @@ fun mapi = s => f => // * Should be an error. This definition would not be referentially transparent. // * The error message needs improvement, though. :e -fun mapi: [A, E] -> Seq[out A, out E] -> ((Int, A) ->{E} A) ->{Alloc} Seq[out A, out E] +fun mapi: [A, E] -> Seq[out A, out E] -> ((Int, A) ->{E} A) ->{Nothing} Seq[out A, out E] fun mapi = s => f => region r in let i = r.ref 0 @@ -95,10 +95,10 @@ fun mapi = s => f => i := !i + 1 f(!i, x) mapi -//│ Type: forall A50_2, E51_2, α61_2, α62_2: Seq[out A50_2, out E51_2] -> (((Int, A50_2) ->{α62_2} α61_2) ->{Alloc} Seq[out α61_2, ?]) +//│ Type: forall A50_2, E51_2, α61_2, α62_2: Seq[out A50_2, out E51_2] -> (((Int, A50_2) ->{α62_2} α61_2) -> Seq[out α61_2, ?]) // * This version is correct as it keeps the mutation encapsulated within the region -fun mapi_force: [A, E] -> Seq[out A, out E] -> ((Int, A) ->{E} A) ->{Alloc | E} Seq[out A, Nothing] +fun mapi_force: [A, E] -> Seq[out A, out E] -> ((Int, A) ->{E} A) ->{E} Seq[out A, Nothing] fun mapi_force = s => f => region r in let i = r.ref 0 @@ -108,7 +108,7 @@ fun mapi_force = s => f => //│ Type: ⊤ // * An alternative version that takes an existing region in parameter -fun mapi: [A, R, E] -> (Seq[out A, out E], Region[R]) -> ((Int, A) ->{E} A) ->{R | Alloc} Seq[out A, out E | R] +fun mapi: [A, R, E] -> (Seq[out A, out E], Region[R]) -> ((Int, A) ->{E} A) ->{R} Seq[out A, out E | R] fun mapi = (s, r) => f => let i = r.ref 0 map(s) of x => @@ -117,7 +117,7 @@ fun mapi = (s, r) => f => //│ Type: ⊤ // * Simpler; should be equivalent when Region is covariant -fun mapi: [A, E] -> (Seq[out A, out E], Region[E]) -> ((Int, A) ->{E} A) ->{E | Alloc} Seq[out A, out E] +fun mapi: [A, E] -> (Seq[out A, out E], Region[E]) -> ((Int, A) ->{E} A) ->{E} Seq[out A, out E] fun mapi = (s, r) => f => let i = r.ref 0 map(s) of x =>