Update outer pp

hkust-taco · Jan 13, 2025 · 918247a · 918247a
1 parent e764069
commit 918247a
Show file tree

Hide file tree

Showing 19 changed files with 82 additions and 80 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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,36 +119,36 @@ 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
 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
@@ -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
@@ -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
@@ -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,15 +267,15 @@ 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
 
 
 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
@@ -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
@@ -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
@@ -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