Skip to content

Commit

Permalink
misc
Browse files Browse the repository at this point in the history
  • Loading branch information
@Kraks
Kraks committed Jul 12, 2024
1 parent d26ece1 commit 7ee3b79
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 37 deletions.
15 changes: 5 additions & 10 deletions src/main/scala/avoidancefsub/TypeCheck.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -281,7 +281,6 @@ def qualUpcast(g: TEnv, p: Qual, r: Qual): (Qual /*filter*/, Qual /*ub*/) = {

def subQualCheck(g: TEnv, p: Qual, r: Qual): Option[Qual] =
val (fl, p1) = qualUpcast(g, p, r)
println(s"$g |- p1: $p1 r: $r")
if (p1 ⊆ r) Some(fl ++ r) else None

/* Subtype checking */
Expand All @@ -303,8 +302,6 @@ def subtypeCheck(tenv: TEnv, t1: Type, t2: Type): (Qual /*filter*/, Qual /*growt
val (fl1, gr1) = subtypeCheck(tenv, t2, t1)
val (fl2, gr2) = subtypeCheck(tenv, u1, u2)
assert(p2.subsetAt(Qual(Set(f, Fresh())), p1), "argument qualifier contravariance")
println(s"$F <: $G")
println(s"r1: $r1 r2: $r2")
assert(r1.subsetAt(Qual(Set(f, Fresh())), r2), "return qualifier covariance")
val p1_* = (p2 -- Qual(Set(f, Fresh()))) ++ gr1
val r2_* = (r1 -- Qual(Set(f, x, Fresh()))) ++ gr2
Expand Down Expand Up @@ -557,21 +554,19 @@ def check(tenv: TEnv, e: Expr, tq: QType): Qual = e match {
val r1 = if (p.contains(f)) r else r.subst(f, q)
val x1 = if (!p.isFresh && p ⊆ r1) Qual.singleton(x) else Qual.untrack
val fl = check(tenv + (x -> QType(t, p.subst(f, q))), body, QType(u, x1 ++ r.subst(f, q)))
assert(fl ⊆ (q + x), s"filter must be a subset of the provided qualifier: $fl ⊆ ${q + x}")
//assert(fl ⊆ (q + x), s"filter must be a subset of the provided qualifier: $fl ⊆ ${q + x}")
(p ++ q) -- Qual(Set(Fresh(), f))
case ETyLam(f, tvar, qvar, bound@QType(t, p), body, rt@Some(QType(u, r)), qual) =>
// XXX: Need double check
val QType(ft, q) = tq
val r1 = if (p.contains(f)) r else r.subst(f, q)
val tenv1 = tenv + TypeBound(tvar, qvar, QType(t, p.subst(f, q)))
val fl = check(tenv1, body, QType(u, r.subst(f, q)))
assert(fl ⊆ (q + qvar), s"filter must be a subset of the provided qualifier: $fl ⊆ ${q + qvar}")
val fl = check(tenv1, body, QType(u.substType(tvar, t), r.subst(f, q)))
//assert(fl ⊆ (q + qvar), s"filter must be a subset of the provided qualifier: $fl ⊆ ${q + qvar}")
(p ++ q) -- Qual(Set(Fresh(), f))
case _ =>
//println(s"check $e $tq")
val QType(t, q) = tq
val (fl1, q1) = checkInfer(tenv, e, t)
//println(s"$e $q1 $q")
val Some(fl2) = subQualCheck(tenv, q1, q)
(fl1 ++ fl2) - Fresh()
}
Expand Down Expand Up @@ -661,8 +656,8 @@ def infer(tenv: TEnv, e: Expr): (Qual, QType) = {
val tq = QType(TForall(f, tvar, qvar, bound, rt), q)
val fl = check(tenv, ETyLam(f, tvar, qvar, bound, body, Some(rt), Some(q)), tq)
(fl, tq)
case ETyApp(e, tq, _) =>
val (fl1, t1) = infer(tenv, e)
case ETyApp(e1, tq, _) =>
val (fl1, t1) = infer(tenv, e1)
val QType(TForall(f, tvar, qvar, bound@QType(t, p), rt@QType(u, r)), q) = t1.expose(tenv)
val (fl2, gr) = subtypeCheck(tenv, tq.ty, t)
assert(wellFormed(tenv, tq), "must be well-formed")
Expand Down
50 changes: 23 additions & 27 deletions src/test/scala/avoidancefsub/TypeCheck.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,37 +17,26 @@ import ExprSyntax.given_Conversion_Int_ENum
class AvoidanceFSubTests extends AnyFunSuite {
def parseAndCheck(s: String): QType = topTypeCheck(parseToCore(s))

test("type arg infer") {
test("reachability polymorphism") {
val p1 = """
def id[T <: Top](x: T^<>): T^x = x;
val x = id(3); // : Int^∅
val c = id(Ref 42); // : Ref[Int]^◆
val y = id(x); // : Int^∅
(! c) // : Int^∅
val x = id[Int](3); // : Int^∅
val c = id[Ref[Int]](Ref 42); // : Ref[Int]^◆
val y = id[Int](x); // : Int^∅
(! c) // : Int^∅
"""
parseToCore(p1)
//assert(parseAndCheck(p1) == (TNum^()))
}

test("forall type") {
val p = """
val p: forall [A^a <: Top^<>] => ((x: A^a) => A^x)^a =
([A^a <: Top^<>] => { (x: A^a) => { x } });
p
"""
parseToCore(p)
//assert(parseAndCheck(p) ==
// (TForall("𝐹#2","A","a",TTop^ ◆,
// TFun("𝑓#3","x",TVar("A")^"a",TVar("A")^"x")^"a")^()))
}

test("transparent poly pair") {
def makePair(a: String, b: String) = s"""
[A <: Top] => { [B <: Top] => {
[C <: Top] => {
p(f: (f(x: A^$a) => (g(y: B^$b) => C^g)^f)^{<>, p})^{$a, $b}: C^f => { f($a)($b) }
(x: A^$a) => { (y: B^$b) => {
[C <: Top] => {
p(f: (f(x: A^$a) => (g(y: B^$b) => C^g)^f)^{<>, p})^{$a, $b}: C^f => { f(x)(y) }
}
}
} }
} }
"""
def fstT(a: String, p: String) = s"""
[A <: Top] => { [B <: Top] => {
Expand All @@ -59,18 +48,15 @@ class AvoidanceFSubTests extends AnyFunSuite {
$p(f(x: A^{<>, f})^$b: (g(y: B^$b) => B^g)^f => { g(y: B^$b)^f: B^g => { y } })
} }
"""
//println(parseToCore(makePair("r1", "r2")))
//println(parseToCore(fstT("r1")("p")))
//println(parseToCore(sndT("r1")("p")))

val prog1 = s"""
val r1 = Ref 1;
val r2 = Ref 2;
val p = ${makePair("r1", "r2")}[Ref[Int], Ref[Int]];
val p = ${makePair("r1", "r2")}[Ref[Int], Ref[Int]](r1, r2);
p
"""
//${fstT("r1", "p")}[Ref[Int], Ref[Int]]
//println(parseToCore(prog1))
println(parseToCore(prog1))
assert(parseAndCheck(prog1) == (TRef(TNum^()) ^ ◆))
val prog2 = s"""
val r1 = Ref 1;
Expand Down Expand Up @@ -143,4 +129,14 @@ class AvoidanceFSubTests extends AnyFunSuite {
*/
}

}
}


/*
ELet(r1,None,EAlloc(ENum(1)),ELet(r2,None,EAlloc(ENum(2)),
ELet(p,None,
ETyApp(ETyApp(
ETyLam(𝐹#0,A,𝑥#1,TTop^◆,ETyLam(𝐹#2,B,𝑥#3,TTop^◆,ETyLam(𝐹#4,C,𝑥#5,TTop^◆,ELam(p,f,TFun(f,x,TVar(A)^r1,TFun(g,y,TVar(B)^r2,TVar(C)^g)^f)^{◆,p},EApp(EApp(EVar(f),EVar(r1),None),EVar(r2),None),Some(TVar(C)^f),Some({r1,r2})),None,None),None,None),None,None),
TRef(TNum^∅)^∅,None),
TRef(TNum^∅)^∅,None),EVar(p),false),false),false)
*/

0 comments on commit 7ee3b79

Please sign in to comment.