Skip to content

Commit

Permalink
reworked type representation and added part of subtyping rules
Browse files Browse the repository at this point in the history
  • Loading branch information
tmoux committed Jul 3, 2020
1 parent b4e9b1a commit c8dc37b
Show file tree
Hide file tree
Showing 3 changed files with 105 additions and 106 deletions.
16 changes: 8 additions & 8 deletions selfhost/binding.wyv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ type DeclType = types.DeclType

def stringToType(s:String, ctx:bound.Context):types.Type
if (s == "Unit")
types.UnitType()
types.theUnit
else
val pred = ((b:DeclType) =>
val z = match b:
Expand All @@ -20,7 +20,7 @@ def stringToType(s:String, ctx:bound.Context):types.Type
default => option.None[types.TypeType]()
z
)
types.NominalType(types.findInDeclList[types.TypeType](ctx.bindings, pred).name)
types.makeNominalType(types.findInDeclList[types.TypeType](ctx.bindings, pred).name)

def bindDeclTypes(e:raw.Exp, context:bound.Context):DeclType = match e:
v:raw.ValType =>
Expand All @@ -32,11 +32,11 @@ def bindDeclTypes(e:raw.Exp, context:bound.Context):DeclType = match e:
types.DefType(b, argtypes, stringToType(d.retTyp,context))
t:raw.TypeDecl =>
val b = types.Binding(t.name, context.counter)
val nominalDecl = types.TypeType(b, types.NominalType(b))
val nominalDecl = types.TypeType(b, types.makeNominalType(b))

val declSeq = makeSeq(context.parse(lexUtil.stripLeadingWhitespace(t.decls)))
val declList:List[DeclType] = declSeq.exps.map[DeclType](e => bindDeclTypes(e,context.extend(nominalDecl)))
types.TypeType(b,types.UnfoldedType(declList))
types.TypeType(b,types.makeRefines((declList)))

default => error.report("unexpected construct", error.unknownLocation)

Expand All @@ -57,7 +57,7 @@ def bindStatement(e:raw.Seq, context:bound.Context):bound.Statement = match e.ex
d:bound.Def =>
types.DefType(d.binding, d.args.map[types.Type](e => e.argTyp), d.retTyp)
t:bound.TypeDecl =>
types.TypeType(t.name, types.UnfoldedType(t.members))
types.TypeType(t.name, types.makeRefines(t.members))
t:bound.TypeAlias =>
types.TypeType(t.name, t.typ)
val newCtx = context.extend(decl)
Expand Down Expand Up @@ -94,7 +94,7 @@ def bindDecl(e:raw.Exp, context:bound.Context):bound.Decl = match e:
bound.Def(b, arglist, methodDecl.retTyp, bindStatement(defn, context.extend(methodDecl).extendList(argdecls)))
t:raw.TypeDecl =>
val b = types.Binding(t.name, context.counter)
val nominalDecl = types.TypeType(b, types.NominalType(b))
val nominalDecl = types.TypeType(b, types.makeNominalType(b))

val declSeq = makeSeq(context.parse(lexUtil.stripLeadingWhitespace(t.decls)))
val declList:List[DeclType] = declSeq.exps.map[DeclType](e => bindDeclTypes(e,context.extend(nominalDecl)))
Expand Down Expand Up @@ -130,7 +130,7 @@ def bindExpr(e:raw.Exp, context:bound.Context):bound.Exp = match e:
default => false
z
)
val searchMethod = llist.find[types.DeclType](types.unfoldType(recType,context.bindings).decls, pred)
val searchMethod = llist.find[types.DeclType](types.unfoldType(recType,context.bindings), pred)
match searchMethod:
s:option.Some => bound.Call(f.receiver, f.field, llist.Singleton[bound.Exp](arg))
default => app
Expand All @@ -148,7 +148,7 @@ def bindExpr(e:raw.Exp, context:bound.Context):bound.Exp = match e:
val defDeclaration:bound.Decl = bound.Def(applyb, llist.Singleton[bound.Arg](bound.Arg(argb,argDecl.typ)), expType, bound.ExprStatement(boundExp))

val thisb = types.Binding("_this", context.counter)
val thisType = types.UnfoldedType(llist.Singleton[DeclType](decl))
val thisType = types.makeRefines(llist.Singleton[DeclType](decl))
bound.New(thisb, thisType, llist.Singleton[bound.Decl](defDeclaration))
c:raw.Call =>
bound.Call(bindExpr(c.receiver, context), c.name, c.args.map[bound.Exp](e => bindExpr(e, context)))
Expand Down
24 changes: 12 additions & 12 deletions selfhost/typecheck.wyv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,15 +25,15 @@ def typecheckDecl(e:bound.Decl, gamma:List[DeclType]):types.DeclType = match e:
val typ = typecheckExpr(v.exp, gamma)
types.ValType(v.binding, typ)
t:bound.TypeDecl =>
types.TypeType(t.name, types.UnfoldedType(t.members))
types.TypeType(t.name, types.makeRefines(t.members))
d:bound.Def =>
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))
types.DefType(d.binding, argtypes, d.retTyp)
else
error.report("argument typ in def doesn't match expected:" + types.typeToString(testType) + ", " + types.typeToString(d.retTyp),error.unknownLocation)
error.report("argument typ in def doesn't match expected:",error.unknownLocation)
t:bound.TypeAlias =>
types.TypeType(t.name, t.typ)

Expand All @@ -50,7 +50,7 @@ def typecheckExpr(e:bound.Exp, gamma:List[DeclType]):types.Type = match e:

c:bound.Call => //T-Invk
val recType = typecheckExpr(c.receiver, gamma)
val unfold:types.UnfoldedType = types.unfoldType(recType, gamma)
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)
Expand All @@ -61,22 +61,22 @@ def typecheckExpr(e:bound.Exp, gamma:List[DeclType]):types.Type = match e:
default => option.None[types.DefType]()
z
)
types.findInDeclList[types.DefType](unfold.decls, pred).retTyp
types.findInDeclList[types.DefType](unfold, pred).retTyp

f:bound.Field => //T-Field
val recType = typecheckExpr(f.receiver, gamma)
val unfold:types.UnfoldedType = types.unfoldType(recType, gamma)
val unfold = types.unfoldType(recType, gamma)
val pred = ((b:DeclType) =>
val z = match b:
va:types.ValType =>
if (f.field == va.name.name) { option.Some[types.ValType](va) } else { option.None[types.ValType]() }
default => option.None[types.ValType]()
z
)
types.findInDeclList[types.ValType](unfold.decls, pred).typ
types.findInDeclList[types.ValType](unfold, pred).typ

n:bound.New => //T-New
val unfold:types.UnfoldedType = types.unfoldType(n.typ, gamma)
val unfold = types.unfoldType(n.typ, gamma)
def typeNewDecls(d:bound.Decl):DeclType
val thisType = types.ValType(n.binding, n.typ)
val ngamma = llist.Cons[DeclType](thisType, gamma)
Expand All @@ -85,11 +85,11 @@ def typecheckExpr(e:bound.Exp, gamma:List[DeclType]):types.Type = match e:
d:bound.Def => typecheckDecl(d, ngamma)
t:bound.TypeDecl => typecheckDecl(d, ngamma)
t:bound.TypeAlias => typecheckDecl(d, ngamma)
val decls = types.UnfoldedType(n.body.map[DeclType](x => typeNewDecls(x)))
if (types.isSubtype(decls, unfold, gamma))
val decls = n.body.map[DeclType](x => typeNewDecls(x))
if (types.checkDeclList(decls, unfold, x=>y=>types.isSubtypeDecl(x,y,gamma)))
n.typ
else
error.report("invalid new expression, unfold = " + types.typeToString(unfold) + "\nnewexpr = " + types.typeToString(decls),error.unknownLocation)
error.report("invalid new expression",error.unknownLocation)

i:bound.Integer =>
val pred = ((b:DeclType) =>
Expand All @@ -99,8 +99,8 @@ def typecheckExpr(e:bound.Exp, gamma:List[DeclType]):types.Type = match e:
default => option.None[types.TypeType]()
z
)
types.NominalType(types.findInDeclList[types.TypeType](gamma, pred).name)
types.makeNominalType(types.findInDeclList[types.TypeType](gamma, pred).name)

u:bound.UnitVal => types.UnitType()
u:bound.UnitVal => types.theUnit

default => error.report("type error: unrecognized expression",error.unknownLocation)
171 changes: 85 additions & 86 deletions selfhost/types.wyv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,33 @@ def Binding(name:String, c:Counter):Binding
val name = name
val id = count

def equalBinding(b1:Binding, b2:Binding):Boolean
b1.name == b2.name && b1.id == b2.id
//////////////////////////////
datatype BaseType
UnitType()
NominalType(L:Binding)

type Type
val base:BaseType
val refines:List[DeclType]
def Type(b:BaseType, r:List[DeclType]):Type = new
val base = b
val refines = r
def makeNominalType(L:Binding):Type = new
val base = NominalType(L)
val refines = llist.Nil[DeclType]()
def makeRefines(ls:List[DeclType]):Type = new
val base = UnitType()
val refines = ls

datatype DeclType
ValType(name:Binding, typ:Type)
TypeType(name:Binding, unfld:Type)
DefType(name:Binding, args:List[Type], retTyp:Type)

val theUnit = Type(UnitType(),llist.Nil[DeclType]())
//////////////////////////////
def findInDeclList[T](gamma:List[DeclType], pred:DeclType->Option[T]):T
def f(gamma:List[DeclType], pred:DeclType->Option[T]):Option[T]
match gamma:
Expand All @@ -33,36 +60,20 @@ def findInDeclList[T](gamma:List[DeclType], pred:DeclType->Option[T]):T
s:option.Some => s.get()
default => error.report("search in decllist failed",error.unknownLocation)

def unfoldType(x:Type, gamma:List[DeclType]):UnfoldedType
match x:
u:UnitType => UnfoldedType(llist.Nil[DeclType]())
def unfoldType(x:Type, gamma:List[DeclType]):List[DeclType]
val decls = match x.base:
u:UnitType => llist.Nil[DeclType]()
x:NominalType =>
val pred = ((b:DeclType) =>
val z = match b:
t:TypeType => if (equalBinding(x.L, t.name)) { option.Some[TypeType](t) } else { option.None[TypeType]() }
default => option.None[TypeType]()
z
)
unfoldType(findInDeclList[TypeType](gamma, pred).typ, gamma)
u:UnfoldedType => u

def equalBinding(b1:Binding, b2:Binding):Boolean
b1.name == b2.name && b1.id == b2.id

//nominal types that point to other nominal types form a tree,
//so we find the "root" nominal type to compare if two aliases are equal
def getNominalRoot(n:NominalType, gamma:List[DeclType]):NominalType
val pred = ((b:DeclType) =>
val z = match b:
t:TypeType => if (equalBinding(t.name, n.L)) { option.Some[TypeType](t) } else { option.None[TypeType]() }
default => option.None[TypeType]()
z
)
val par = findInDeclList[TypeType](gamma, pred)
match par.typ:
nn:NominalType => getNominalRoot(nn,gamma)
default => n
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:
Expand All @@ -74,102 +85,90 @@ def checkArgList(xs:List[Type],ys:List[Type],pred:Type->Type->Boolean):Boolean
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 => t.name.name == u.name.name && equalType(t.typ,u.typ,gamma)
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
match t1:
u:UnitType => match t2:
v:UnitType => true
default => equalType(unfoldType(t1,gamma),t2,gamma)
n:NominalType => match t2:
v:NominalType =>
val r1 = getNominalRoot(n,gamma)
val r2 = getNominalRoot(v,gamma)
equalBinding(r1.L, r2.L)
default => equalType(unfoldType(t1,gamma),t2,gamma)
u:UnfoldedType => match t2:
v:UnfoldedType =>
def isValidDecl(d:DeclType):Boolean
val search = llist.find[DeclType](u.decls, (e:DeclType) => equalDeclType(e,d,gamma))
match search:
s:option.Some => true
default => false
v.decls.foldRight[Boolean]((x:DeclType,y:Boolean) => isValidDecl(x) && y, true)
default => equalType(t1,unfoldType(t2,gamma),gamma)
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], stack:List[SubtypePair]):Boolean = match a:
def isSubtypeDecl(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match a:
v:ValType => match b:
u:ValType => v.name.name == u.name.name && isSubtypeHelper(v.typ,u.typ,gamma,stack)
u:ValType => v.name.name == u.name.name && isSubtype(v.typ,u.typ,gamma)
default => false
t:TypeType => match b:
u:TypeType => t.name.name == u.name.name && equalType(t.typ,u.typ,gamma)
u:TypeType => equalDeclType(a,b,gamma)
default => false
d:DefType => match b:
u:DefType =>
val pred = x:Type => y:Type => isSubtypeHelper(x,y,gamma,stack)
d.name.name == u.name.name && checkArgList(u.args,d.args,pred) && isSubtypeHelper(d.retTyp,u.retTyp,gamma,stack)
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
isSubtypeHelper(t1,t2,gamma,llist.Nil[SubtypePair]())

def isSubtypeHelper(t1:Type, t2:Type, gamma:List[DeclType], stack:List[SubtypePair]):Boolean
//if t1 <: t2 appears within its own judgement, return true
val findPrev = llist.find[SubtypePair](stack, (j:SubtypePair) => equalType(j.S,t1,gamma) && equalType(j.T,t2,gamma))
match findPrev:
s:option.Some => true
default =>
if (equalType(t1,t2,gamma))
true
else
val newstack = llist.Cons[SubtypePair](SubtypePair(t1,t2), stack)
val u = unfoldType(t1,gamma)
val v = unfoldType(t2,gamma)
def isValidDecl(d:DeclType):Boolean
val search = llist.find[DeclType](u.decls, (e:DeclType) => isSubtypeDecl(e,d,gamma,newstack))
match search:
s:option.Some => true
default => false
v.decls.foldRight[Boolean]((x:DeclType,y:Boolean) => isValidDecl(x) && y, true)

datatype Type
UnitType()
NominalType(L:Binding)
UnfoldedType(decls:List[DeclType])
if (equalType(t2,theUnit,gamma))
true
else
isSubtypeBase(t1,t2.base,gamma) && checkDeclList(t1.refines,t2.refines,x=>y=>isSubtypeDecl(x,y,gamma))

datatype DeclType
ValType(name:Binding, typ:Type)
TypeType(name:Binding, typ:Type)
DefType(name:Binding, args:List[Type], retTyp:Type)
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
cc:llist.Cons => c.value + ", " + combineStringList(c.next)
default => ""

def declTypeToString(d:DeclType):String = match d:
v:ValType => "val " + v.name.name + ":" + typeToString(v.typ)
t:TypeType => "type " + t.name.name + ":" + typeToString(t.typ)
d:DefType => "def " + d.name.name + "(args):" + typeToString(d.retTyp)

def typeToString(t:Type):String = match t:
u:UnitType => "Unit"
n:NominalType => n.L.name
u:UnfoldedType =>
val s = u.decls.map[String](e => declTypeToString(e))
s.foldLeft[String]((x:String,y:String) => x + ", " + y, "UNFLD: { ") + " }"
t:TypeType => "type " + t.name.name + ":" + typeToString(t.unfld)
d:DefType =>
val arglist = d.args.map[String](t => typeToString(t))
"def " + d.name.name + "(" + combineStringList(arglist) + "):" + typeToString(d.retTyp)

def typeToString(t:Type):String
val baseString = match t.base:
u:UnitType => "Unit"
n:NominalType => n.L.name
val s = t.refines.map[String](e => declTypeToString(e))
val refinesString = combineStringList(s)
baseString + " {" + refinesString + "}"

0 comments on commit c8dc37b

Please sign in to comment.