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.

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

Remove unnecessary Alloc type in BbML #249

Merged
merged 1 commit into from
Dec 11, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
13 changes: 3 additions & 10 deletions hkmc2/shared/src/main/scala/hkmc2/bbml/bbML.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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?
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
6 changes: 0 additions & 6 deletions hkmc2/shared/src/main/scala/hkmc2/semantics/Elaborator.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down
42 changes: 21 additions & 21 deletions hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 =>
Expand All @@ -144,7 +144,7 @@ letreg of r =>
r
//│ Type: Reg[?, E123_1]
//│ Where:
//│ E123_1 <: Alloc
//│ E123_1 <:

:e
letreg of r =>
Expand All @@ -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 =>
Expand All @@ -188,7 +188,7 @@ letreg of r0 =>
r1
//│ Type: Reg[?, in E174_1]
//│ Where:
//│ E174_1 <: Alloc
//│ E174_1 <:


// * Can leak the iterator
Expand Down
10 changes: 5 additions & 5 deletions hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down
38 changes: 19 additions & 19 deletions hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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 =>
Expand All @@ -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
Expand Down
74 changes: 30 additions & 44 deletions hkmc2/shared/src/test/mlscript/bbml/bbList.mls
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>55_2]
//│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>54_2) ->{<E>55_2} <A>54_2) ->{<E>55_2} List[out <A>54_2]
//│ ║ l.49: let i = r.ref 0
//│ ║ ^^^^^^^
//│ ║ l.50: f => map(s) of x =>
Expand All @@ -59,15 +59,15 @@ fun mapi = s =>
//│ ║ ^^^^^^^^^^^^^^^^^
//│ ║ l.52: f(!i, x)
//│ ║ ^^^^^^^^^^^^^^
//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>55_2]
//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ <E>56_2
//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~<E>56_2)
//│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>55_2]
//│ ╟── because: cannot constrain f70_2 ->{E78_2} List[out B77_2] <: ((Int, <A>54_2) ->{<E>55_2} <A>54_2) ->{<E>55_2} List[out <A>54_2]
//│ ╟── because: cannot constrain D( E78_2 ) <: <E>55_2
//│ ╟── because: cannot constrain E78_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain α79_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain r80_2 <: ¬(~<E>55_2)
//│ ╙── because: cannot constrain <: ¬(~<E>55_2)
//│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>54_2) ->{<E>55_2} <A>54_2) ->{<E>55_2} List[out <A>54_2]
//│ ║ l.49: let i = r.ref 0
//│ ║ ^^^^^^^
//│ ║ l.50: f => map(s) of x =>
Expand All @@ -76,15 +76,15 @@ fun mapi = s =>
//│ ║ ^^^^^^^^^^^^^^^^^
//│ ║ l.52: f(!i, x)
//│ ║ ^^^^^^^^^^^^^^
//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>55_2]
//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ <E>56_2
//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~<E>56_2)
//│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>55_2]
//│ ╟── because: cannot constrain f70_2 ->{E78_2} List[out B77_2] <: ((Int, <A>54_2) ->{<E>55_2} <A>54_2) ->{<E>55_2} List[out <A>54_2]
//│ ╟── because: cannot constrain D( E78_2 ) <: <E>55_2
//│ ╟── because: cannot constrain E78_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain α79_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain r80_2 <: ¬(~<E>55_2)
//│ ╙── because: cannot constrain <: ¬(~<E>55_2)
//│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>54_2) ->{<E>55_2} <A>54_2) ->{<E>55_2} List[out <A>54_2]
//│ ║ l.49: let i = r.ref 0
//│ ║ ^^^^^^^
//│ ║ l.50: f => map(s) of x =>
Expand All @@ -93,28 +93,14 @@ fun mapi = s =>
//│ ║ ^^^^^^^^^^^^^^^^^
//│ ║ l.52: f(!i, x)
//│ ║ ^^^^^^^^^^^^^^
//│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>55_2]
//│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ <E>56_2
//│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~<E>56_2)
//│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~<E>56_2)
//│ ╔══[ERROR] Type error in function literal with expected type (List[out <A>55_2]) ->{⊥} ((Int, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>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, <A>54_2) ->{<E>55_2} <A>54_2) ->{<E>55_2} List[out <A>54_2]
//│ ╟── because: cannot constrain D( E78_2 ) <: <E>55_2
//│ ╟── because: cannot constrain E78_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain α79_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~<E>55_2)
//│ ╟── because: cannot constrain r80_2 <: ¬(~<E>55_2)
//│ ╙── because: cannot constrain <: ¬(~<E>55_2)
//│ Type: ⊤


Expand Down
2 changes: 0 additions & 2 deletions hkmc2/shared/src/test/mlscript/bbml/bbPrelude.mls
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
// :bbml

class Alloc

class CodeBase[T, C, S]
class Region[T]
class Ref[T, S]
Expand Down
Loading
Loading