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

Add ticks for type variable pretty-printing in BbML #255

Merged
merged 4 commits into from
Dec 21, 2024
+371 −371
Merged

Add ticks for type variable pretty-printing in BbML #255

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a080994
Add ticks for tvs
NeilKleistGao Dec 20, 2024
8e0fff7
Improve skolem pp
NeilKleistGao Dec 20, 2024
af3924c
Remove unecessary ticks for skolem
NeilKleistGao Dec 21, 2024
3ad0ae2
Merge branch 'hkmc2' into tick🕚
LPTK Dec 21, 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: 3 additions & 4 deletions hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -168,9 +168,8 @@ sealed abstract class BasicType extends Type:
this match
case ClassLikeType(name, targs) =>
if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.show).mkString(", ")}]"
case v @ InfVar(lvl, uid, _, isSkolem) =>
val name = scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.hint))
if isSkolem then s"<${name}>" else s"${name}"
case v @ InfVar(lvl, uid, _, _) =>
"'" + scope.lookup(v.sym).getOrElse(scope.allocateName(v.sym, v.hint))
case FunType(arg :: Nil, ret, eff) => s"${arg.paren} ->${printEff(eff)} ${ret.paren}"
case FunType(args, ret, eff) => s"(${args.map(_.show).mkString(", ")}) ->${printEff(eff)} ${ret.paren}"
case ComposedType(lhs, rhs, pol) => s"${lhs.paren} ${if pol then "∨" else "∧"} ${rhs.paren}"
Expand All @@ -183,7 +182,7 @@ sealed abstract class BasicType extends Type:
if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]"
case v @ InfVar(lvl, uid, _, isSkolem) =>
val name = if v.hint.isEmpty then s"${v.sym.nme}" else s"${v.sym.nme}(${v.hint})"
if isSkolem then s"<${name}${uid}>_${lvl}" else s"${name}${uid}_${lvl}"
if isSkolem then s"<${name}${uid}>_${lvl}" else s"'${name}${uid}_${lvl}"
case FunType(arg :: Nil, ret, eff) => s"${arg.parenDbg} ->{${eff.showDbg}} ${ret.parenDbg}"
case FunType(args, ret, eff) => s"(${args.map(_.showDbg).mkString(", ")}) ->{${eff.showDbg}} ${ret.parenDbg}"
case ComposedType(lhs, rhs, pol) => s"${lhs.parenDbg} ${if pol then "∨" else "∧"} ${rhs.parenDbg}"
Expand Down
62 changes: 31 additions & 31 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 @@ -20,7 +20,7 @@ false

fun id(x) = x
id
//│ Type: forall x: x -> x
//│ Type: forall 'x: 'x -> 'x

fun inc(x) = x + 1
//│ Type: ⊤
Expand All @@ -29,7 +29,7 @@ fun mul(x, y) = x * y
//│ Type: ⊤

x => x
//│ Type: (x) ->{⊥} x
//│ Type: ('x) ->{⊥} 'x

+
//│ Type: (Int, Int) ->{⊥} Int
Expand Down Expand Up @@ -109,14 +109,14 @@ class Some[A](value: A)
//│ Type: ⊤

new Some(true)
//│ Type: Some[A]
//│ Type: Some['A]
//│ Where:
//│ Bool <: A
//│ Bool <: 'A

new Some(42)
//│ Type: Some[A]
//│ Type: Some['A]
//│ Where:
//│ Int <: A
//│ Int <: 'A

let p = new Point(1.0, 0.0, 0.0) in p.Point#x
//│ Type: Num
Expand Down Expand Up @@ -150,22 +150,22 @@ fun foofoo(x) =
//│ Type: ⊤

new Printer(foofoo)
//│ Type: Printer[T]
//│ Type: Printer['T]
//│ Where:
//│ T <: Int
//│ 'T <: Int

let ip = new Printer(foofoo) in ip.Printer#f(42)
//│ Type: Str

:e
let ip = new Printer(foofoo) in ip.Printer#f("42")
//│ ╔══[ERROR] Type error in string literal with expected type T
//│ ╔══[ERROR] Type error in string literal with expected type 'T
//│ ║ l.161: let ip = new Printer(foofoo) in ip.Printer#f("42")
//│ ║ ^^^^
//│ ╟── because: cannot constrain Str <: T
//│ ╟── because: cannot constrain Str <: T
//│ ╟── because: cannot constrain Str <: ¬(¬T)
//│ ╟── because: cannot constrain Str <: T
//│ ╟── because: cannot constrain Str <: 'T
//│ ╟── because: cannot constrain Str <: 'T
//│ ╟── because: cannot constrain Str <: ¬(¬'T)
//│ ╟── because: cannot constrain Str <: 'T
//│ ╙── because: cannot constrain Str <: ¬(¬{Int})
//│ Type: Str

Expand All @@ -176,23 +176,23 @@ fun inc(x) = x + 1
//│ Type: ⊤

new TFun(inc)
//│ Type: TFun[T]
//│ Type: TFun['T]
//│ Where:
//│ Int <: T
//│ T <: Int
//│ Int <: 'T
//│ 'T <: Int

let tf = new TFun(inc) in tf.TFun#f(1)
//│ Type: Int

:e
let tf = new TFun(inc) in tf.TFun#f("1")
//│ ╔══[ERROR] Type error in string literal with expected type T
//│ ╔══[ERROR] Type error in string literal with expected type 'T
//│ ║ l.188: let tf = new TFun(inc) in tf.TFun#f("1")
//│ ║ ^^^
//│ ╟── because: cannot constrain Str <: T
//│ ╟── because: cannot constrain Str <: T
//│ ╟── because: cannot constrain Str <: ¬(¬T)
//│ ╟── because: cannot constrain Str <: T
//│ ╟── because: cannot constrain Str <: 'T
//│ ╟── because: cannot constrain Str <: 'T
//│ ╟── because: cannot constrain Str <: ¬(¬'T)
//│ ╟── because: cannot constrain Str <: 'T
//│ ╙── because: cannot constrain Str <: ¬(¬{Int})
//│ Type: Str ∨ Int

Expand All @@ -207,17 +207,17 @@ class Pair[A, B](fst: A, snd: B)


new Pair(id, id)
//│ Type: Pair[A, B]
//│ Type: Pair['A, 'B]
//│ Where:
//│ x -> x <: A
//│ x1 -> x1 <: B
//│ 'x -> 'x <: 'A
//│ 'x1 -> 'x1 <: 'B


new Pair(x => x, x => x)
//│ Type: Pair[A, B]
//│ Type: Pair['A, 'B]
//│ Where:
//│ x -> x <: A
//│ x1 -> x1 <: B
//│ 'x -> 'x <: 'A
//│ 'x1 -> 'x1 <: 'B


if 1 < 2 then 1 else 0
Expand Down Expand Up @@ -276,17 +276,17 @@ class Foo[A](x: A -> A)
//│ Type: ⊤

new Foo(x => x)
//│ Type: Foo[A]
//│ Type: Foo['A]

fun f(g) = new Foo(g)
f
//│ Type: forall A: (A -> A) -> Foo[A]
//│ Type: forall 'A: ('A -> 'A) -> Foo['A]

f(x => x).Foo#x
//│ Type: (A) ->{⊥} A
//│ Type: ('A) ->{⊥} 'A

g => (new Foo(g)).Foo#x
//│ Type: (A -> A) ->{⊥} (A) ->{⊥} A
//│ Type: ('A -> 'A) ->{⊥} ('A) ->{⊥} 'A


throw new Error("oops")
Expand Down
52 changes: 26 additions & 26 deletions hkmc2/shared/src/test/mlscript/bbml/bbBorrowing.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,9 @@ fun next: [A, Br] -> Iter[A, Br] ->{Br} A
//│ Type: ⊤

letreg(r => r)
//│ Type: Reg[?, E]
//│ Type: Reg[?, 'E]
//│ Where:
//│ E <: ⊥
//│ 'E <: ⊥

letreg of r =>
let b = mkVec(r)
Expand All @@ -48,9 +48,9 @@ letreg of r =>
123
clear(b)
r
//│ Type: Reg[?, E]
//│ Type: Reg[?, 'E]
//│ Where:
//│ E <: ⊥
//│ 'E <: ⊥


// * Non-lexical borrowing pattern encoded with a thunk
Expand Down Expand Up @@ -90,10 +90,10 @@ letreg of r =>
//│ ║ ^^^^^^^^^^^^^^^^^^
//│ ║ l.75: k()
//│ ║ ^^^^^
//│ ╟── because: cannot constrain E <: ⊥
//│ ╟── because: cannot constrain E <: ¬()
//│ ╟── because: cannot constrain ¬⊥ ∧ ¬Rg <: ¬()
//│ ╟── because: cannot constrain <: Rg
//│ ╟── because: cannot constrain 'E <: ⊥
//│ ╟── because: cannot constrain 'E <: ¬()
//│ ╟── because: cannot constrain ¬⊥ ∧ ¬'Rg <: ¬()
//│ ╟── because: cannot constrain <: 'Rg
//│ ╙── because: cannot constrain <: ¬()
//│ Type: ⊥

Expand Down Expand Up @@ -126,15 +126,15 @@ letreg of r =>
//│ ║ ^^^^^^^^^^
//│ ║ l.109: r
//│ ║ ^^^
//│ ╟── because: cannot constrain E <: ⊥
//│ ╟── because: cannot constrain E <: ¬()
//│ ╟── because: cannot constrain ¬⊥ ∧ Rg <: ¬()
//│ ╟── because: cannot constrain Rg <: ¬()
//│ ╟── because: cannot constrain 'E <: ⊥
//│ ╟── because: cannot constrain 'E <: ¬()
//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬()
//│ ╟── because: cannot constrain 'Rg <: ¬()
//│ ╙── because: cannot constrain <: ¬()
//│ Type: Reg[?, E]
//│ Type: Reg[?, 'E]
//│ Where:
//│ ⊤ <: E
//│ E <: ⊥
//│ ⊤ <: 'E
//│ 'E <: ⊥


letreg of r =>
Expand All @@ -143,9 +143,9 @@ letreg of r =>
next(it)
use(r)
r
//│ Type: Reg[?, E]
//│ Type: Reg[?, 'E]
//│ Where:
//│ E <: ⊥
//│ 'E <: ⊥

:e
letreg of r =>
Expand All @@ -170,15 +170,15 @@ letreg of r =>
//│ ║ ^^^^^^^^
//│ ║ l.157: r
//│ ║ ^^^
//│ ╟── because: cannot constrain E <: ⊥
//│ ╟── because: cannot constrain E <: ¬()
//│ ╟── because: cannot constrain ¬⊥ ∧ Rg <: ¬()
//│ ╟── because: cannot constrain Rg <: ¬()
//│ ╟── because: cannot constrain 'E <: ⊥
//│ ╟── because: cannot constrain 'E <: ¬()
//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬()
//│ ╟── because: cannot constrain 'Rg <: ¬()
//│ ╙── because: cannot constrain <: ¬()
//│ Type: Reg[?, E]
//│ Type: Reg[?, 'E]
//│ Where:
//│ ⊤ <: E
//│ E <: ⊥
//│ ⊤ <: 'E
//│ 'E <: ⊥

letreg of r0 =>
letreg of r1 =>
Expand All @@ -187,9 +187,9 @@ letreg of r0 =>
next(it)
use(r1)
r1
//│ Type: Reg[?, in E]
//│ Type: Reg[?, in 'E]
//│ Where:
//│ E <: ⊥
//│ 'E <: ⊥


// * Can leak the iterator
Expand Down
8 changes: 4 additions & 4 deletions hkmc2/shared/src/test/mlscript/bbml/bbBorrowing2.mls
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,10 +47,10 @@ letreg of r =>
//│ ║ ^^^^^^^^^^^
//│ ║ l.36: write(r)
//│ ║ ^^^^^^^^^^
//│ ╟── because: cannot constrain E <: ⊥
//│ ╟── because: cannot constrain E <: ¬()
//│ ╟── because: cannot constrain ¬⊥ ∧ Rg <: ¬()
//│ ╟── because: cannot constrain Rg <: ¬()
//│ ╟── because: cannot constrain 'E <: ⊥
//│ ╟── because: cannot constrain 'E <: ¬()
//│ ╟── because: cannot constrain ¬⊥ ∧ 'Rg <: ¬()
//│ ╟── because: cannot constrain 'Rg <: ¬()
//│ ╙── because: cannot constrain <: ¬()
//│ Type: Int

Expand Down
Loading
Loading