Skip to content

Commit

Permalink
Add ticks for tvs
Browse files Browse the repository at this point in the history
  • Loading branch information
@NeilKleistGao
NeilKleistGao committed Dec 20, 2024
1 parent c774a3f commit a080994
Show file tree
Hide file tree
Showing 23 changed files with 371 additions and 371 deletions.
4 changes: 2 additions & 2 deletions hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ sealed abstract class BasicType extends Type:
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}"
if isSkolem then s"'<${name}>" else s"'${name}"
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 +183,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
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
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
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

0 comments on commit a080994

Please sign in to comment.