From 918247aaae4e98db62a9f46945648eefc0c6f97c Mon Sep 17 00:00:00 2001 From: NeilKleistGao Date: Mon, 13 Jan 2025 15:40:00 +0800 Subject: [PATCH] Update outer pp --- .../src/main/scala/hkmc2/bbml/types.scala | 4 +++- .../src/test/mlscript/bbml/bbBasics.mls | 4 ++-- .../src/test/mlscript/bbml/bbBounds.mls | 20 +++++++++---------- .../shared/src/test/mlscript/bbml/bbCheck.mls | 20 +++++++++---------- .../src/test/mlscript/bbml/bbCodeGen.mls | 2 +- .../test/mlscript/bbml/bbCyclicExtrude.mls | 20 +++++++++---------- .../src/test/mlscript/bbml/bbDisjoint.mls | 14 ++++++------- .../src/test/mlscript/bbml/bbExtrude.mls | 8 ++++---- .../src/test/mlscript/bbml/bbFunGenFix.mls | 2 +- .../shared/src/test/mlscript/bbml/bbFuns.mls | 6 +++--- .../shared/src/test/mlscript/bbml/bbGPCE.mls | 10 +++++----- hkmc2/shared/src/test/mlscript/bbml/bbId.mls | 10 +++++----- .../test/mlscript/bbml/bbLetRegEncoding.mls | 2 +- .../src/test/mlscript/bbml/bbOption.mls | 2 +- .../shared/src/test/mlscript/bbml/bbPoly.mls | 20 +++++++++---------- hkmc2/shared/src/test/mlscript/bbml/bbRec.mls | 4 ++-- hkmc2/shared/src/test/mlscript/bbml/bbRef.mls | 10 +++++----- .../src/test/mlscript/bbml/bbSelfApp.mls | 2 +- hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls | 2 +- 19 files changed, 82 insertions(+), 80 deletions(-) diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala index 459c79d2f..f048683e0 100644 --- a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala +++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala @@ -290,7 +290,9 @@ case class PolyType(tvs: Ls[InfVar], outer: InfVar, body: GeneralType) extends G override lazy val lvl: Int = (body :: tvs).map(_.lvl).max override def show(using scope: Scope): Str = given Scope = scope.nest - s"forall(${outer.show}) ${tvs.map(_.show).mkString(", ")}: ${body.show}" + val op = outer.show + val lst = (if op === "outer" then op else s"outer $op") :: tvs.map(_.show) + s"forall ${lst.mkString(", ")}: ${body.show}" override def showDbg: Str = s"forall(outer ${outer.showDbg}) ${tvs.map(_.showDbg).mkString(", ")}: ${body.showDbg}" override def monoOr(fallback: => Type): Type = fallback override def map(f: GeneralType => GeneralType): PolyType = PolyType(tvs, outer, f(body)) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls index 660f81d39..22b31b3ed 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBasics.mls @@ -20,7 +20,7 @@ false fun id(x) = x id -//│ Type: forall(outer) 'x: 'x -> 'x +//│ Type: forall outer, 'x: 'x -> 'x fun inc(x) = x + 1 //│ Type: ⊤ @@ -280,7 +280,7 @@ new Foo(x => x) fun f(g) = new Foo(g) f -//│ Type: forall(outer) 'A: ('A -> 'A) -> Foo['A] +//│ Type: forall outer, 'A: ('A -> 'A) -> Foo['A] f(x => x).Foo#x //│ Type: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls index f1122d806..1a3696fe1 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls @@ -8,13 +8,13 @@ (x => x): [A restricts Int] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ Int <: 'A (x => x - 1): [A extends Int restricts Int] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ Int <: 'A //│ 'A <: Int @@ -24,7 +24,7 @@ fun iid(x) = x //│ Type: ⊤ iid -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ 'A <: Int @@ -47,7 +47,7 @@ class Foo[A] fun foo: [A extends Foo[in Nothing out Any] restricts Foo[in Num]] -> A -> A foo -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ Foo[in Num] <: 'A //│ 'A <: Foo[?] @@ -73,7 +73,7 @@ baz fun bazbaz: [A extends Int] -> A -> [B extends A] -> B bazbaz -//│ Type: (Int) ->{⊥} forall(outer) 'B: ⊥ +//│ Type: (Int) ->{⊥} forall outer, 'B: ⊥ fun foofun: [A extends Int -> Int restricts Any -> Int] -> A -> Int -> Int foofun @@ -84,7 +84,7 @@ foofun(x => x + 1)(42) fun bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A bazbaz -//│ Type: forall(outer) 'A: ('A) ->{⊥} (forall(outer1) 'B: 'A -> 'A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} (forall outer outer1, 'B: 'A -> 'A) ->{⊥} 'A //│ Where: //│ 'A <: Int @@ -93,7 +93,7 @@ bazbaz(42)(x => x + 1) fun cc: [A extends B -> B restricts B -> B, B extends A -> A restricts A -> A] -> A -> B -> Bool cc -//│ Type: forall(outer) 'A, 'B: ('A) ->{⊥} ('B) ->{⊥} Bool +//│ Type: forall outer, 'A, 'B: ('A) ->{⊥} ('B) ->{⊥} Bool //│ Where: //│ 'A -> 'A <: 'B //│ 'B <: 'A -> 'A @@ -111,16 +111,16 @@ fun h: [C] -> ([A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B :e bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A -//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as (A) ->{⊥} (forall(outer) 'B: 'B) ->{⊥} A +//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as (A) ->{⊥} (forall outer, 'B: 'B) ->{⊥} A //│ ║ l.113: bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A //│ ╙── ^^^^^^ -//│ Type: forall(outer) 'A: ('A) ->{⊥} (forall(outer1) 'B: 'A -> 'A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} (forall outer outer1, 'B: 'A -> 'A) ->{⊥} 'A //│ Where: //│ 'A <: Int (x => f => bazbaz(x)(f)): [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} (forall(outer1) 'B: 'A -> 'A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} (forall outer outer1, 'B: 'A -> 'A) ->{⊥} 'A //│ Where: //│ 'A <: Int diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls index ec45ce993..a3be07bc9 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCheck.mls @@ -78,7 +78,7 @@ fun high(f) = f(42) //│ Type: ⊤ high -//│ Type: (forall(outer) 'A: ('A) ->{⊥} 'A) ->{⊥} Int +//│ Type: (forall outer, 'A: ('A) ->{⊥} 'A) ->{⊥} Int high((x => x): [A] -> A -> A) @@ -100,11 +100,11 @@ high(x => x + 1) //│ Type: Int (let a = 0 in x => x): [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A (if false then x => x else y => y): [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A fun baz: Int -> (([A] -> A -> A), Int) -> Int @@ -119,24 +119,24 @@ fun baz(z) = :e baz: Int -> (([A] -> A -> A), Int) -> Int -//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#18),Ident(baz)) as (Int) ->{⊥} (forall(outer) 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int +//│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#18),Ident(baz)) as (Int) ->{⊥} (forall outer, 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int //│ ║ l.121: baz: Int -> (([A] -> A -> A), Int) -> Int //│ ╙── ^^^ //│ Type: ⊥ baz(42) -//│ Type: (forall(outer) 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int +//│ Type: (forall outer, 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int :e baz(42): (([A] -> A -> A), Int) -> Int -//│ ╔══[ERROR] Cannot type non-function term App(SynthSel(Ref(globalThis:block#18),Ident(baz)),Tup(List(Fld(‹›,Lit(IntLit(42)),None)))) as (forall(outer) 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int +//│ ╔══[ERROR] Cannot type non-function term App(SynthSel(Ref(globalThis:block#18),Ident(baz)),Tup(List(Fld(‹›,Lit(IntLit(42)),None)))) as (forall outer, 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int //│ ║ l.132: baz(42): (([A] -> A -> A), Int) -> Int //│ ╙── ^^^^^^^ //│ Type: ⊥ (z => (f, x) => baz(z)(f, x)): Int -> (([A] -> A -> A), Int) -> Int -//│ Type: (Int) ->{⊥} (forall(outer) 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int +//│ Type: (Int) ->{⊥} (forall outer, 'A: ('A) ->{⊥} 'A, Int) ->{⊥} Int fun id: [A] -> A -> A @@ -144,11 +144,11 @@ fun id(x) = x //│ Type: ⊤ id: [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A (id: [A] -> A -> A): [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A 42: Int | Num //│ Type: Int ∨ Num @@ -171,7 +171,7 @@ foo fun foo: [A] -> (A, ~A) -> A foo -//│ Type: forall(outer) 'A: ('A, ¬'A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A, ¬'A) ->{⊥} 'A :e diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCodeGen.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCodeGen.mls index 7d0415119..65eae5a09 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCodeGen.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCodeGen.mls @@ -54,7 +54,7 @@ false //│ JS (unsanitized): //│ (x) => { return x; } //│ = [Function (anonymous)] -//│ Type: forall(outer) 'T: ('T) ->{⊥} 'T +//│ Type: forall outer, 'T: ('T) ->{⊥} 'T :sjs diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls index 60177f8be..96ff89452 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls @@ -5,18 +5,18 @@ let f = (x => (x : [A] -> A -> A)) in f -//│ Type: (⊤ -> ⊥) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: (⊤ -> ⊥) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A let f = ((x => x) : [A] -> A -> A) in f -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A let foo = f => (x => f(x(x)) : [A] -> A -> A) in foo -//│ Type: ('app -> (⊤ -> ⊥)) ->{⊥} ('x -> 'app) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: ('app -> (⊤ -> ⊥)) ->{⊥} ('x -> 'app) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ 'x <: 'x -> 'app f => (let g = x => x(x) in f(g(g))) : [A] -> A -> A -//│ Type: (⊥ -> (⊤ -> ⊥)) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: (⊥ -> (⊤ -> ⊥)) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A :e f => (let g = x => f(x(x)) in g) : [A] -> A -> A @@ -27,34 +27,34 @@ f => (let g = x => f(x(x)) in g) : [A] -> A -> A //│ ╟── because: cannot constrain A <: 'x //│ ╟── because: cannot constrain A <: 'x //│ ╙── because: cannot constrain A <: ¬(¬{'x ->{'eff1} 'app1}) -//│ Type: (⊥ -> ⊥) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: (⊥ -> ⊥) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A f => (x => f(x(x)) : [A] -> A -> A) -//│ Type: ('app -> (⊤ -> ⊥)) ->{⊥} ('x -> 'app) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: ('app -> (⊤ -> ⊥)) ->{⊥} ('x -> 'app) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ 'x <: 'x -> 'app let foo = f => (f(x => x(x)) : [A] -> A -> A) in foo -//│ Type: ((('x ->{'eff} 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: ((('x ->{'eff} 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ 'x <: 'x ->{'eff} 'app :todo let foo(f) = (f(x => x(x)) : [A] -> A -> A) in foo -//│ Type: ((('x ->{'eff} 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: ((('x ->{'eff} 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ 'x <: 'x ->{'eff} 'app :todo fun foo(f) = (f(x => x(x)) : [A] -> A -> A) -//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but ('f) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A found +//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but ('f) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A found //│ ║ l.49: fun foo(f) = (f(x => x(x)) : [A] -> A -> A) //│ ╙── ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ //│ Type: ⊤ f => (let g = x => x(x) in let tmp = g(g) in f(g)) : [A] -> A -> A -//│ Type: (((('x ∨ ('x ->{'eff} 'app)) -> 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: (((('x ∨ ('x ->{'eff} 'app)) -> 'app) ->{'eff} 'app) -> (⊤ -> ⊥)) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ 'x <: ('x ∨ ('x ->{'eff} 'app)) -> 'app diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbDisjoint.mls b/hkmc2/shared/src/test/mlscript/bbml/bbDisjoint.mls index 828784977..5c1727f29 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbDisjoint.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbDisjoint.mls @@ -9,7 +9,7 @@ class Pair[P, Q](fst: P, snd: Q) fun fork: [A, B extends ~A, T1, T2] -> (Any ->{A} T1, Any ->{B} T2) ->{A | B} Pair[out T1, out T2] fork -//│ Type: forall(outer) 'A, 'B, 'T1, 'T2: ((⊤) ->{'A} 'T1, (⊤) ->{'B} 'T2) ->{'A ∨ 'B} Pair[out 'T1, out 'T2] +//│ Type: forall outer, 'A, 'B, 'T1, 'T2: ((⊤) ->{'A} 'T1, (⊤) ->{'B} 'T2) ->{'A ∨ 'B} Pair[out 'T1, out 'T2] //│ Where: //│ 'B <: ¬'A @@ -102,7 +102,7 @@ fun helper(r1) = region r2 in fork((_ => r1.ref 1), (_ => r2.ref 2)) helper -//│ Type: forall(outer) 'reg, 'reg1: Region[in 'reg out 'reg1] ->{'reg1} Pair[out Ref[Int, out 'reg1], out Ref[Int, out ¬outer]] +//│ Type: forall outer, 'reg, 'reg1: Region[in 'reg out 'reg1] ->{'reg1} Pair[out Ref[Int, out 'reg1], out Ref[Int, out ¬outer]] //│ Where: //│ 'reg <: outer //│ 'reg <: 'reg1 @@ -138,7 +138,7 @@ region x in //│ ╟── because: cannot constrain x <: 'env //│ ╟── because: cannot constrain x <: 'env //│ ╙── because: cannot constrain x <: outer ∨ y -//│ ╔══[ERROR] Type error in region expression with expected type forall(outer) 'A: Int +//│ ╔══[ERROR] Type error in region expression with expected type forall outer, 'A: Int //│ ║ l.129: (region y in let t = helper(x) in 42): [A] -> Int //│ ║ ^^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'eff <: ⊥ @@ -180,7 +180,7 @@ fun annohelper(r1) = region r2 in fork((_ => r1.ref 1), (_ => r2.ref 2)) annohelper -//│ Type: forall(outer) 'T: (Region['T]) ->{'T} Pair[out Ref[Int, out 'T], out Ref[Int, out ¬outer]] +//│ Type: forall outer, 'T: (Region['T]) ->{'T} Pair[out Ref[Int, out 'T], out Ref[Int, out ¬outer]] //│ Where: //│ 'T <: outer @@ -249,7 +249,7 @@ fun foo(r1) = region r2 in foo(r2) foo -//│ Type: forall(S) 'T: (Region['T]) ->{'T} ⊥ +//│ Type: forall outer S, 'T: (Region['T]) ->{'T} ⊥ //│ Where: //│ 'T <: S @@ -267,7 +267,7 @@ fun bar: [outer S, T extends S] -> Region[T] ->{T} Int bar: [outer Q, P extends Q] -> Region[P] ->{P} Int -//│ Type: forall(Q) 'P: (Region['P]) ->{'P} Int +//│ Type: forall outer Q, 'P: (Region['P]) ->{'P} Int //│ Where: //│ 'P <: Q @@ -275,7 +275,7 @@ bar: [outer Q, P extends Q] -> Region[P] ->{P} Int fun foo: [outer To, T extends To] -> Region[T] ->{T} ([outer So, S extends So] -> Region[S]->{S} Int) fun foo(r1) = bar foo -//│ Type: forall(To) 'T: (Region['T]) ->{'T} forall(So) 'S: (Region['S]) ->{'S} Int +//│ Type: forall outer To, 'T: (Region['T]) ->{'T} forall outer So, 'S: (Region['S]) ->{'S} Int //│ Where: //│ 'T <: To //│ 'S <: So diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls index 8492f26d4..b508152d9 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbExtrude.mls @@ -8,7 +8,7 @@ fun f(y) = // * the parameter type of y is extruded. f -//│ Type: forall(outer) 'y: 'y -> 'y +//│ Type: forall outer, 'y: 'y -> 'y //│ Where: //│ 'y <: ⊤ -> Int @@ -28,7 +28,7 @@ fun g(y) = //│ Type: ⊤ g -//│ Type: (forall(outer) 'A: (⊥) ->{⊥} Int) ->{⊥} forall(outer) 'A: (⊤) ->{⊥} Int +//│ Type: (forall outer, 'A: (⊥) ->{⊥} Int) ->{⊥} forall outer, 'A: (⊤) ->{⊥} Int g(foo) //│ Type: (⊤) ->{⊥} Int @@ -54,11 +54,11 @@ class C[A](m: A, n: A -> Int) fun f: [A] -> ([B] -> (C[out B] & A) -> B) -> A -> Int f -//│ Type: forall(outer) 'A: (forall(outer1) 'B: (C[out 'B] ∧ 'A) ->{⊥} 'B) ->{⊥} ('A) ->{⊥} Int +//│ Type: forall outer, 'A: (forall outer outer1, 'B: (C[out 'B] ∧ 'A) ->{⊥} 'B) ->{⊥} ('A) ->{⊥} Int fun g: [D] -> C[in Int out D] -> D g -//│ Type: forall(outer) 'D: (C[in Int out 'D]) ->{⊥} 'D +//│ Type: forall outer, 'D: (C[in Int out 'D]) ->{⊥} 'D f(g) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls b/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls index 21e186646..28956f765 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbFunGenFix.mls @@ -31,7 +31,7 @@ fun helper(a) = write(a) //│ Type: ⊤ helper -//│ Type: forall(outer) 'Rg: Reg[out 'Rg, ?] ->{'Rg} Int +//│ Type: forall outer, 'Rg: Reg[out 'Rg, ?] ->{'Rg} Int subreg(basereg) of r0 => helper(r0) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls b/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls index d9fede1b9..e9837699e 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbFuns.mls @@ -5,7 +5,7 @@ fun f(x, y) = x(y) f -//│ Type: forall(outer) 'y, 'eff, 'app: ('y ->{'eff} 'app, 'y) ->{'eff} 'app +//│ Type: forall outer, 'y, 'eff, 'app: ('y ->{'eff} 'app, 'y) ->{'eff} 'app f((x => x), 42) @@ -19,9 +19,9 @@ fun id: [A] -> A -> A //│ Type: ⊤ id : [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A id(id) : [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls index 4fd8cba24..06a5b794c 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbGPCE.mls @@ -8,7 +8,7 @@ fun power(x) = case 0 then `1.0 n then x `*. power(x)(n - 1) power -//│ Type: forall(outer) 'C: (CodeBase[out Num, out 'C, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Num, out 'C, ?] +//│ Type: forall outer, 'C: (CodeBase[out Num, out 'C, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Num, out 'C, ?] fun id: [A] -> A -> A @@ -38,7 +38,7 @@ show fun inc(dbg) = x `=> let c = x `+ `1 in let t = dbg(c) in c inc -//│ Type: forall(outer) 'eff: (CodeBase[out Int, ?, ?] ->{'eff} ⊤) ->{'eff} CodeBase[out Int -> Int, ⊥, ?] +//│ Type: forall outer, 'eff: (CodeBase[out Int, ?, ?] ->{'eff} ⊤) ->{'eff} CodeBase[out Int -> Int, ⊥, ?] inc(c => log(show(c))) //│ Type: CodeBase[out Int -> Int, ⊥, ?] @@ -56,7 +56,7 @@ let gn5 = run(gib_naive(5)) fun bind(rhs, k) = `let x = rhs `in k(x) bind -//│ Type: forall(outer) 'cde, 'ctx, 'cde1, 'eff, 'cde2, 'ctx1: (CodeBase[out 'cde, out 'ctx, ?], CodeBase[in 'cde1 out 'cde1 ∨ 'cde, ?, ⊥] ->{'eff} CodeBase[out 'cde2, out 'ctx1, ?]) ->{'eff} CodeBase[out 'cde2, out 'ctx ∨ 'ctx1, ?] +//│ Type: forall outer, 'cde, 'ctx, 'cde1, 'eff, 'cde2, 'ctx1: (CodeBase[out 'cde, out 'ctx, ?], CodeBase[in 'cde1 out 'cde1 ∨ 'cde, ?, ⊥] ->{'eff} CodeBase[out 'cde2, out 'ctx1, ?]) ->{'eff} CodeBase[out 'cde2, out 'ctx ∨ 'ctx1, ?] :e fun body: [G] -> (CodeBase[out Int, out G, out Any], CodeBase[out Int, out G, out Any]) -> Int -> CodeBase[out Int, out G, out Any] @@ -78,7 +78,7 @@ fun body(x, y) = case 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(outer) 'G: (CodeBase[out Int, out 'G, ?], forall(outer1) 'C: (CodeBase[out Int, out 'C, ?]) ->{⊥} CodeBase[out Int, out 'C ∨ 'G, ?]) ->{⊥} CodeBase[out Int, out 'G, ?] +//│ Type: forall outer, 'G: (CodeBase[out Int, out 'G, ?], forall outer outer1, 'C: (CodeBase[out Int, out 'C, ?]) ->{⊥} CodeBase[out Int, out 'C ∨ 'G, ?]) ->{⊥} CodeBase[out Int, out 'G, ?] fun body: [G] -> (CodeBase[out Int, out G, out Any], CodeBase[out Int, out G, out Any]) -> Int -> CodeBase[out Int, out G, out Any] @@ -87,7 +87,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 -//│ Type: forall(outer) 'G: (CodeBase[out Int, out 'G, ?], CodeBase[out Int, out 'G, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Int, out 'G, ?] +//│ Type: forall outer, 'G: (CodeBase[out Int, out 'G, ?], CodeBase[out Int, out 'G, ?]) ->{⊥} (Int) ->{⊥} CodeBase[out Int, out 'G, ?] fun gib(n) = (x, y) `=> body(x, y)(n) let g5 = run(gib(5)) diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbId.mls b/hkmc2/shared/src/test/mlscript/bbml/bbId.mls index 24ad310a4..ee35d6755 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbId.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbId.mls @@ -10,28 +10,28 @@ id(1) //│ Type: Int id -//│ Type: forall(outer) 'x: 'x -> 'x +//│ Type: forall outer, 'x: 'x -> 'x id(true) //│ Type: Bool id -//│ Type: forall(outer) 'x: 'x -> 'x +//│ Type: forall outer, 'x: 'x -> 'x fun id(x) = x //│ Type: ⊤ id : [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A (y => y) : [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A fun id(x) = x (y => id(y)) : [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls index 557900cc6..2b1f5d806 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbLetRegEncoding.mls @@ -8,7 +8,7 @@ fun letreg: [E,Res] -> ([R] -> Region[R] ->{E | R} Res) ->{E} Res //│ Type: ⊤ letreg -//│ Type: forall(outer) 'E, 'Res: (forall(outer1) 'R: (Region['R]) ->{'E ∨ 'R} 'Res) ->{'E} 'Res +//│ Type: forall outer, 'E, 'Res: (forall outer outer1, 'R: (Region['R]) ->{'E ∨ 'R} 'Res) ->{'E} 'Res letreg(r => r) //│ Type: Region[?] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls b/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls index bbb365b5d..d3796ad30 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbOption.mls @@ -7,7 +7,7 @@ class Option[out A](inspect: [E, Res] -> (() ->{E} Res, A ->{E} Res) ->{E} Res) //│ Type: ⊤ opt => opt.Option#inspect -//│ Type: (Option[out '+A]) ->{⊥} forall(outer) 'E, 'Res: (() ->{'E} 'Res, ('+A) ->{'E} 'Res) ->{'E} 'Res +//│ Type: (Option[out '+A]) ->{⊥} forall outer, 'E, 'Res: (() ->{'E} 'Res, ('+A) ->{'E} 'Res) ->{'E} 'Res opt => opt.Option#inspect( () => 42 diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls index f5d0560ec..d3d2844ef 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls @@ -19,7 +19,7 @@ fun id(x) = x //│ Type: ⊤ id -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A :e (x => x + 1): [A] -> A -> A @@ -31,14 +31,14 @@ id //│ ║ l.25: (x => x + 1): [A] -> A -> A //│ ║ ^^^^^ //│ ╙── because: cannot constrain Int <: A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A (x => x): [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A id: [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A id: Int -> Int //│ Type: (Int) ->{⊥} Int @@ -50,7 +50,7 @@ myInc(id, 0) //│ Type: Int let t = 42 in ((x => x): [A] -> A -> A) -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A id(42) @@ -75,7 +75,7 @@ fun swap(p) = new Pair(p.Pair#b, p.Pair#a) swap -//│ Type: forall(outer) 'A, 'B: (Pair[out 'A, out 'B]) ->{⊥} Pair[out 'B, out 'A] +//│ Type: forall outer, 'A, 'B: (Pair[out 'A, out 'B]) ->{⊥} Pair[out 'B, out 'A] let t = new Pair(42, true) in swap(t) //│ Type: Pair[out Bool, out Int] @@ -94,7 +94,7 @@ fun foo(x) = 42 //│ Type: ⊤ foo -//│ Type: (forall(outer) 'A: ('A) ->{⊥} 'A) ->{⊥} Int +//│ Type: (forall outer, 'A: ('A) ->{⊥} 'A) ->{⊥} Int foo(id) //│ Type: Int @@ -144,11 +144,11 @@ fun gen(x) = //│ Type: ⊤ gen -//│ Type: (Int) ->{⊥} forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: (Int) ->{⊥} forall outer, 'A: ('A) ->{⊥} 'A gen(42) -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A :e @@ -160,4 +160,4 @@ fun cnt(x) = 42 //│ Type: ⊤ (x => x): [A] -> A -> A -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls index 7d2c54b06..553df61c7 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRec.mls @@ -15,7 +15,7 @@ fun f x = f fun f(x) = f f -//│ Type: forall(outer) 'f: ⊤ -> (⊤ -> 'f) +//│ Type: forall outer, 'f: ⊤ -> (⊤ -> 'f) //│ Where: //│ ⊤ -> 'f <: 'f @@ -55,7 +55,7 @@ fun f(x) = f(Foo.a(x)) fun f(x) = f(x.Foo#a) f -//│ Type: forall(outer) 'x: Foo[out 'x] -> ⊥ +//│ Type: forall outer, 'x: Foo[out 'x] -> ⊥ //│ Where: //│ 'x <: Foo[out 'x] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls index 127d239ad..5938d04f5 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbRef.mls @@ -36,7 +36,7 @@ let r = region x in x.ref 42 fun mkRef() = region x in x.ref 42 mkRef -//│ Type: forall(outer) : () -> Ref[Int, out ¬outer] +//│ Type: forall outer: () -> Ref[Int, out ¬outer] :e let t = region x in x in t.ref 42 @@ -125,7 +125,7 @@ fun rid(x) = :e region x in (let dz = x.ref 42 in 42): [A] -> Int -//│ ╔══[ERROR] Type error in block with expected type forall(outer) 'A: Int +//│ ╔══[ERROR] Type error in block with expected type forall outer, 'A: Int //│ ║ l.127: (let dz = x.ref 42 in 42): [A] -> Int //│ ║ ^^^^^^^^^^^^^^ //│ ╟── because: cannot constrain 'reg <: ⊥ @@ -167,7 +167,7 @@ fun foo(x) = x //│ Type: ⊤ foo -//│ Type: forall(outer) 'A: ('A) ->{⊥} 'A +//│ Type: forall outer, 'A: ('A) ->{⊥} 'A //│ Where: //│ 'A <: Int @@ -179,11 +179,11 @@ fun bar(f) = f(42) //│ Type: ⊤ bar -//│ Type: (forall(outer) 'A: ('A) ->{⊥} 'A) ->{⊥} Int +//│ Type: (forall outer, 'A: ('A) ->{⊥} 'A) ->{⊥} Int :e region x in x.ref bar -//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall(outer) 'A: ('A) ->{⊥} 'A) ->{⊥} Int found +//│ ╔══[ERROR] Expected a monomorphic type or an instantiable type here, but (forall outer, 'A: ('A) ->{⊥} 'A) ->{⊥} Int found //│ ║ l.185: region x in x.ref bar //│ ╙── ^^^ //│ Type: Ref[⊥, ?] diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls index 68a92c665..583ab98d3 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSelfApp.mls @@ -12,7 +12,7 @@ fun f(x) = x(x) //│ Type: ⊤ f -//│ Type: forall(outer) 'x, 'eff, 'app: ('x ->{'eff} 'app) ->{'eff} 'app +//│ Type: forall outer, 'x, 'eff, 'app: ('x ->{'eff} 'app) ->{'eff} 'app //│ Where: //│ 'x <: 'x ->{'eff} 'app diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls index 8c6e19461..0316cb036 100644 --- a/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls +++ b/hkmc2/shared/src/test/mlscript/bbml/bbSeq.mls @@ -96,7 +96,7 @@ fun mapi = s => f => i := !i + 1 f(!i, x) mapi -//│ Type: forall(outer) 'A, 'E, 'app, 'eff: Seq[out 'A, out 'E] -> (((Int, 'A) ->{'eff} 'app) -> Seq[out 'app, out (¬outer ∨ 'eff) ∨ 'E]) +//│ Type: forall outer, 'A, 'E, 'app, 'eff: Seq[out 'A, out 'E] -> (((Int, 'A) ->{'eff} 'app) -> Seq[out 'app, out (¬outer ∨ 'eff) ∨ 'E]) // * 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) ->{E} Seq[out A, Nothing]