Skip to content

Commit

Permalink
moved subtyping functions to new file
Browse files Browse the repository at this point in the history
  • Loading branch information
tmoux committed Jul 3, 2020
1 parent c8dc37b commit 7d7a2f3
Show file tree
Hide file tree
Showing 4 changed files with 101 additions and 84 deletions.
3 changes: 2 additions & 1 deletion selfhost/binding.wyv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import error
import lexUtil
import types
import typecheck
import subtyping
import wyvern.collections.llist

type List = llist.LinkedList
Expand Down Expand Up @@ -76,7 +77,7 @@ def bindDecl(e:raw.Exp, context:bound.Context):bound.Decl = match e:
val body = bindExpr(v.exp, context)
val expType = typecheck.typecheckExpr(body, context.bindings)
val annotType = stringToType(v.typ,context)
if (!types.isSubtype(expType,annotType,context.bindings))
if (!subtyping.isSubtype(expType,annotType,context.bindings))
error.report("val expr doesn't match annotation",error.unknownLocation)
bound.Val(b, annotType, body)
d:raw.Def =>
Expand Down
94 changes: 94 additions & 0 deletions selfhost/subtyping.wyv
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,94 @@
module subtyping

import types
import error
import wyvern.collections.llist
type List = llist.LinkedList
type Binding = types.Binding
type Type = types.Type
type DeclType = types.DeclType
type BaseType = types.BaseType
type ValType = types.ValType
type TypeType = types.TypeType
type DefType = types.DefType
type UnitType = types.UnitType
type NominalType = types.NominalType

//Check if two lists of arguments line up in the right way
def checkArgList(xs:List[Type],ys:List[Type],pred:Type->Type->Boolean):Boolean
if (xs.size() == ys.size())
def f(xs:List[Type],ys:List[Type]):Boolean = match xs:
a:llist.Cons => match ys:
b:llist.Cons =>
(pred(a.value)(b.value)) && f(a.next,b.next)
default => true
f(xs,ys)
else
false

//Check if for each y in ys there is an x in xs s.t. (pred x y) is true
def checkDeclList(xs:List[DeclType],ys:List[DeclType],pred:DeclType->DeclType->Boolean):Boolean
def isValid(d:DeclType):Boolean
val search = llist.find[DeclType](xs, (e:DeclType) => pred(e)(d))
match search:
s:option.Some => true
default => false
ys.foldRight[Boolean]((x:DeclType,y:Boolean) => isValid(x) && y, true)

def equalDeclType(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean
match a:
v:ValType => match b:
u:ValType => v.name.name == u.name.name && equalType(v.typ,u.typ,gamma)
default => false
t:TypeType => match b:
u:TypeType =>
val tt = types.unfoldType(types.makeNominalType(t.name),gamma)
val uu = types.unfoldType(types.makeNominalType(u.name),gamma)
t.name.name == u.name.name && checkDeclList(tt,uu,x=>y=>equalDeclType(x,y,gamma))
default => false
d:DefType => match b:
u:DefType =>
val pred = x:Type => y:Type => equalType(x,y,gamma)
d.name.name == u.name.name && checkArgList(d.args,u.args,pred) && equalType(d.retTyp,u.retTyp,gamma)
default => false

def equalBaseType(a:BaseType, b:BaseType):Boolean = match a:
u:UnitType => match b:
v:UnitType => true
default => false
n:NominalType => match b:
v:NominalType => types.equalBinding(n.L,v.L)
default => false

def equalType(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
val pred = x:DeclType => y:DeclType => equalDeclType(x,y,gamma)
equalBaseType(t1.base,t2.base) && checkDeclList(t1.refines,t2.refines,pred)

type SubtypePair
val S:Type
val T:Type
def SubtypePair(S:Type, T:Type):SubtypePair = new
val S = S
val T = T

def isSubtypeDecl(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match a:
v:ValType => match b:
u:ValType => v.name.name == u.name.name && isSubtype(v.typ,u.typ,gamma)
default => false
t:TypeType => match b:
u:TypeType => equalDeclType(a,b,gamma)
default => false
d:DefType => match b:
u:DefType =>
val pred = x:Type => y:Type => isSubtype(x,y,gamma)
d.name.name == u.name.name && checkArgList(u.args,d.args,pred) && isSubtype(d.retTyp,u.retTyp,gamma)
default => false

def isSubtype(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
if (equalType(t2,types.theUnit,gamma))
true
else
isSubtypeBase(t1,t2.base,gamma) && checkDeclList(t1.refines,t2.refines,x=>y=>isSubtypeDecl(x,y,gamma))

def isSubtypeBase(t1:Type, t2:BaseType, gamma:List[DeclType]):Boolean
true //TODO--also need to add "subtype extends" decl
9 changes: 5 additions & 4 deletions selfhost/typecheck.wyv
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module typecheck

import types
import subtyping
import bound
import error
import wyvern.option
Expand Down Expand Up @@ -30,7 +31,7 @@ def typecheckDecl(e:bound.Decl, gamma:List[DeclType]):types.DeclType = match e:
val argdecls:List[DeclType] = d.args.map[types.ValType]((a:bound.Arg) => types.ValType(a.arg,a.argTyp))
val argtypes:List[types.Type] = d.args.map[types.Type]((a:bound.Arg) => a.argTyp)
val testType = typecheckStmt(d.body, argdecls.append(gamma))
if (types.isSubtype(testType, d.retTyp, gamma))
if (subtyping.isSubtype(testType, d.retTyp, gamma))
types.DefType(d.binding, argtypes, d.retTyp)
else
error.report("argument typ in def doesn't match expected:",error.unknownLocation)
Expand All @@ -53,11 +54,11 @@ def typecheckExpr(e:bound.Exp, gamma:List[DeclType]):types.Type = match e:
val unfold = types.unfoldType(recType, gamma)
val argtypes:List[types.Type] = c.args.map[types.Type](e => typecheckExpr(e,gamma))

val subcheck = x:types.Type => y:types.Type => types.isSubtype(x,y,gamma)
val subcheck = x:types.Type => y:types.Type => subtyping.isSubtype(x,y,gamma)
val pred = ((b:DeclType) =>
val z = match b:
da:types.DefType =>
if (c.name == da.name.name && types.checkArgList(argtypes,da.args,subcheck)) { option.Some[types.DefType](da) } else { option.None[types.DefType]() }
if (c.name == da.name.name && subtyping.checkArgList(argtypes,da.args,subcheck)) { option.Some[types.DefType](da) } else { option.None[types.DefType]() }
default => option.None[types.DefType]()
z
)
Expand Down Expand Up @@ -86,7 +87,7 @@ def typecheckExpr(e:bound.Exp, gamma:List[DeclType]):types.Type = match e:
t:bound.TypeDecl => typecheckDecl(d, ngamma)
t:bound.TypeAlias => typecheckDecl(d, ngamma)
val decls = n.body.map[DeclType](x => typeNewDecls(x))
if (types.checkDeclList(decls, unfold, x=>y=>types.isSubtypeDecl(x,y,gamma)))
if (subtyping.checkDeclList(decls, unfold, x=>y=>subtyping.isSubtypeDecl(x,y,gamma)))
n.typ
else
error.report("invalid new expression",error.unknownLocation)
Expand Down
79 changes: 0 additions & 79 deletions selfhost/types.wyv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,85 +73,6 @@ def unfoldType(x:Type, gamma:List[DeclType]):List[DeclType]
unfoldType(findInDeclList[TypeType](gamma, pred).unfld,gamma)
x.refines.append(decls)

//Check if two lists of arguments line up in the right way
def checkArgList(xs:List[Type],ys:List[Type],pred:Type->Type->Boolean):Boolean
if (xs.size() == ys.size())
def f(xs:List[Type],ys:List[Type]):Boolean = match xs:
a:llist.Cons => match ys:
b:llist.Cons =>
(pred(a.value)(b.value)) && f(a.next,b.next)
default => true
f(xs,ys)
else
false

//Check if for each y in ys there is an x in xs s.t. (pred x y) is true
def checkDeclList(xs:List[DeclType],ys:List[DeclType],pred:DeclType->DeclType->Boolean):Boolean
def isValid(d:DeclType):Boolean
val search = llist.find[DeclType](xs, (e:DeclType) => pred(e)(d))
match search:
s:option.Some => true
default => false
ys.foldRight[Boolean]((x:DeclType,y:Boolean) => isValid(x) && y, true)

def equalDeclType(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean
match a:
v:ValType => match b:
u:ValType => v.name.name == u.name.name && equalType(v.typ,u.typ,gamma)
default => false
t:TypeType => match b:
u:TypeType =>
val tt = unfoldType(makeNominalType(t.name),gamma)
val uu = unfoldType(makeNominalType(u.name),gamma)
t.name.name == u.name.name && checkDeclList(tt,uu,x=>y=>equalDeclType(x,y,gamma))
default => false
d:DefType => match b:
u:DefType =>
val pred = x:Type => y:Type => equalType(x,y,gamma)
d.name.name == u.name.name && checkArgList(d.args,u.args,pred) && equalType(d.retTyp,u.retTyp,gamma)
default => false

def equalBaseType(a:BaseType, b:BaseType):Boolean = match a:
u:UnitType => match b:
v:UnitType => true
default => false
n:NominalType => match b:
v:NominalType => equalBinding(n.L,v.L)
default => false

def equalType(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
val pred = x:DeclType => y:DeclType => equalDeclType(x,y,gamma)
equalBaseType(t1.base,t2.base) && checkDeclList(t1.refines,t2.refines,pred)

type SubtypePair
val S:Type
val T:Type
def SubtypePair(S:Type, T:Type):SubtypePair = new
val S = S
val T = T

def isSubtypeDecl(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match a:
v:ValType => match b:
u:ValType => v.name.name == u.name.name && isSubtype(v.typ,u.typ,gamma)
default => false
t:TypeType => match b:
u:TypeType => equalDeclType(a,b,gamma)
default => false
d:DefType => match b:
u:DefType =>
val pred = x:Type => y:Type => isSubtype(x,y,gamma)
d.name.name == u.name.name && checkArgList(u.args,d.args,pred) && isSubtype(d.retTyp,u.retTyp,gamma)
default => false

def isSubtype(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
if (equalType(t2,theUnit,gamma))
true
else
isSubtypeBase(t1,t2.base,gamma) && checkDeclList(t1.refines,t2.refines,x=>y=>isSubtypeDecl(x,y,gamma))

def isSubtypeBase(t1:Type, t2:BaseType, gamma:List[DeclType]):Boolean
true

def combineStringList(ls:List[String]):String = match ls:
c:llist.Cons => match c.next:
n:llist.Nil => c.value
Expand Down

0 comments on commit 7d7a2f3

Please sign in to comment.