fixing type equality stuff

selfhost/binding.wyv

@@ -58,8 +58,6 @@ 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.makeRefines(t.members))
-                t:bound.TypeAlias =>
                     types.TypeType(t.name, t.typ)
                 s:bound.SubtypeDecl =>
                     types.SubtypeType(s.subtype, s.supertype)
@@ -101,11 +99,11 @@ def bindDecl(e:raw.Exp, context:bound.Context):bound.Decl = match e:
 
         val declSeq = makeSeq(context.parse(lexUtil.stripLeadingWhitespace(t.decls)))
         val declList:List[DeclType] = declSeq.exps.map[DeclType](e => bindDeclTypes(e,context.extend(nominalDecl)))
-        bound.TypeDecl(b, declList)
+        bound.TypeDecl(b, types.makeRefines(declList))
     t:raw.TypeAlias =>
         val b = types.Binding(t.name, context.counter)
         val aliasType = stringToType(t.alias, context)
-        bound.TypeAlias(b, aliasType)
+        bound.TypeDecl(b, aliasType)
     s:raw.SubtypeDecl =>
         bound.SubtypeDecl(stringToType(s.subtype,context),stringToType(s.supertype,context))
     default => error.report("not a declaration: " + raw.expToString(e),error.unknownLocation)

selfhost/bound.wyv

@@ -41,8 +41,7 @@ datatype Statement
 datatype Decl
     Val(binding:Binding, typ:types.Type, exp:Exp)
     Def(binding:Binding, args:List[Arg], retTyp:types.Type, body:Statement)
-    TypeDecl(name:Binding, members:List[DeclType])
-    TypeAlias(name:Binding, typ:types.Type)
+    TypeDecl(name:Binding, typ:types.Type)
     SubtypeDecl(subtype:types.Type, supertype:types.Type)
 
 datatype Exp
@@ -61,7 +60,6 @@ def lowerDecl(decl:Decl):Decl = match decl:
     v:Val         => Val(v.binding, v.typ, lowerExp(v.exp))
     d:Def         => Def(d.binding, d.args, d.retTyp, lowerStatement(d.body))
     t:TypeDecl    => t
-    t:TypeAlias   => t
     s:SubtypeDecl => s
 
 def lowerExp(exp:Exp):Exp = match exp:

selfhost/subtyping.wyv

@@ -54,17 +54,24 @@ def equalDeclType(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean
                 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:
+def equalBaseType(a:BaseType, b:BaseType, gamma:List[DeclType]):Boolean = match a:
     u:UnitType => match b:
         v:UnitType => true
         default => false
     n:NominalType => match b:
-        v:NominalType => types.equalBinding(n.L,v.L)
+        v:NominalType => 
+            def getNominalRoot(bind:Binding):Binding
+                val pred = types.findTypePredicate(bind)
+                val par = types.findInDeclList[TypeType](gamma, pred)
+                match par.unfld.base:
+                    u:UnitType    => bind
+                    n:NominalType => getNominalRoot(n.L)
+            types.equalBinding(getNominalRoot(n.L),getNominalRoot(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)
+    equalBaseType(t1.base,t2.base,gamma) && checkDeclList(t1.refines,t2.refines,pred)
 
 def isSubtypeDeclList(xs:List[DeclType], ys:List[DeclType], gamma:List[DeclType]):Boolean
     checkDeclList(xs,ys,x=>y=>isSubtypeDecl(x,y,gamma))

selfhost/tests/subtypeTest.wyv

@@ -14,4 +14,10 @@ type B:
     val z:Int
 subtype B extends A
 subtype B extends Unit
+type C:
+    def calc(x:Int):C
+    val z:Int
+    val y:B
+subtype C extends B
+subtype C extends A
 0

selfhost/toBytecode.wyv

@@ -23,7 +23,6 @@ def toBytecodeDecl(e:bound.Decl):b.Decl = match e:
     v:bound.Val       => b.ValDecl(v.binding.name, toBytecodeExpr(v.exp))
     d:bound.Def       => b.MethodDecl(d.binding.name, d.args.map[String](e => e.arg.name), b.SeqExpr(toBytecodeStmt(d.body)))
     t:bound.TypeDecl  => b.ValDecl("_", toBytecodeExpr(bound.UnitVal()))
-    t:bound.TypeAlias => b.ValDecl("_", toBytecodeExpr(bound.UnitVal()))
     s:bound.SubtypeDecl => b.ValDecl("_", toBytecodeExpr(bound.UnitVal()))
 
     default => error.report("not a declaration",error.unknownLocation)

selfhost/typecheck.wyv

@@ -26,7 +26,7 @@ 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.makeRefines(t.members))
+        types.TypeType(t.name, t.typ)
     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)
@@ -35,8 +35,6 @@ def typecheckDecl(e:bound.Decl, gamma:List[DeclType]):types.DeclType = match e:
             types.DefType(d.binding, argtypes, d.retTyp)
           else
             error.report("def decl is not well-formed",error.unknownLocation)
-    t:bound.TypeAlias =>     
-        types.TypeType(t.name, t.typ)
     s:bound.SubtypeDecl =>
         if (subtyping.checkSubtypeWF(s.subtype, s.supertype, gamma))
             types.SubtypeType(s.subtype, s.supertype)
@@ -90,7 +88,6 @@ def typecheckExpr(e:bound.Exp, gamma:List[DeclType]):types.Type = match e:
                 v:bound.Val       => typecheckDecl(d, gamma)
                 d:bound.Def       => typecheckDecl(d, ngamma)
                 t:bound.TypeDecl  => typecheckDecl(d, ngamma)
-                t:bound.TypeAlias => typecheckDecl(d, ngamma)
         val decls = n.body.map[DeclType](x => typeNewDecls(x))
         if (subtyping.checkDeclList(decls, unfold, x=>y=>subtyping.isSubtypeDecl(x,y,gamma)))
             n.typ

selfhost/types.wyv

@@ -63,16 +63,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 findTypePredicate(bind:Binding):DeclType->Option[TypeType]
+    val pred = ((b:DeclType) =>
+        val z = match b:
+            t:TypeType => if (equalBinding(bind, t.name)) { option.Some[TypeType](t) } else { option.None[TypeType]() }
+            default => option.None[TypeType]()
+        z
+    )
+    pred
+
 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
-            )
+            val pred = findTypePredicate(x.L)
             unfoldType(findInDeclList[TypeType](gamma, pred).unfld,gamma)
     x.refines.append(decls)