adding more stuff

selfhost/binding.wyv

@@ -107,12 +107,12 @@ def bindDecl(e:raw.Exp, context:types.Context):types.Decl = match e:
         val body = bindExpr(v.exp, context)
         val expType = typecheck.typecheckExpr(body, context.bindings)
         val annotType = rawToType(v.typ,context)
-        if (false /*TODO: !subtyping.isSubtype(expType,annotType,context.bindings)*/)
+        if (!typecheck.isSubtype(expType,annotType,context.bindings))
             error.report("val expr doesn't match annotation",error.unknownLocation)
         types.Val(b, annotType, body)
     d:raw.Def =>
         val b = types.Binding(d.name, context.counter)
-        //again VAR alert
+
         var newCtx:types.Context = context
         def mapParams(args:List[raw.Arg]):List[types.Arg] = match args:
             c:llist.Cons =>

selfhost/bound.wyv

@@ -17,6 +17,7 @@ def lowerDecl(decl:types.Decl):types.Decl = match decl:
     d:types.Def         => types.Def(d.binding, d.args, d.retTyp, lowerStatement(d.body))
     t:types.TypeDecl    => t
     s:types.SubtypeDecl => s
+    m:types.TypeEq  => m
 
 def lowerExp(exp:types.Exp):types.Exp = match exp:
     v:types.Var     => v

selfhost/main.wyv

@@ -61,23 +61,28 @@ def parse(s:String):raw.Exp
         js.log("WARNING: parse was ambiguous.  Grammar should be fixed.\n")
     pars.results.get(0)
 
-//stdout.print("Binding...\n")
-//val boundExp:types.Statement = binding.bind(parser.results.get(0), s => parse(s))
-val boundExp : exception.Answer[types.Statement,exception.Exception] = exception.try[types.Statement](() => binding.bind(parser.results.get(0), s => parse(s)))
-match boundExp:
-    s1: exception.Success =>
-        stdout.print("binding success\n")
-        val tc = typecheck.typecheck(s1.value)
-        stdout.print("type: " + typesUtil.typeToString(tc) + "\n")
-    f1: exception.Failure =>
-        match f1.exception:
-            exn: error.ErrorReportingException => stdout.print(error.asString(exn)+"\n")
-            default => stdout.print("unexpected exception thrown\n")
-
-//val tc = typecheck.typecheck(boundExp)
-//stdout.print("type: " + types.typeToString(tc) + "\n")
-
-/*
+stdout.print("Binding...\n")
+val boundExp:types.Statement = binding.bind(parser.results.get(0), s => parse(s))
+//val boundExp : exception.Answer[types.Statement,exception.Exception] = exception.try[types.Statement](() => binding.bind(parser.results.get(0), s => parse(s)))
+//match boundExp:
+//    s1: exception.Success =>
+//        stdout.print("binding success\n")
+//        val tc:exception.Answer[types.Type,exception.Exception] = exception.try[types.Type](() => typecheck.typecheck(s1.value))
+//        match tc:
+//            s1: exception.Success =>
+//                stdout.print("type: " + typesUtil.typeToString(s1.value) + "\n")
+//            f1: exception.Failure =>
+//                match f1.exception:
+//                    exn: error.ErrorReportingException => stdout.print(error.asString(exn)+"\n")
+//                    default => stdout.print("unexpected exception thrown\n")
+//    f1: exception.Failure =>
+//        match f1.exception:
+//            exn: error.ErrorReportingException => stdout.print(error.asString(exn)+"\n")
+//            default => stdout.print("unexpected exception thrown\n")
+
+val tc = typecheck.typecheck(boundExp)
+stdout.print("type: " + typesUtil.typeToString(tc) + "\n")
+
 stdout.print("Lowering...\n")
 val ooExp:types.Statement = bound.lowerStatement(boundExp)
 
@@ -88,4 +93,3 @@ stdout.print(outputFileName)
 stdout.print("...\n")
 
 toBytecode.writeExpToFile(ooExp, outputFileName)
-*/

selfhost/run.sh

@@ -7,6 +7,6 @@ wyby main.wyv
 node ../backend/boot.js main.wyb > main.js
 node main.js $1
 
-#echo FINISHED PRODUCING WYB FILE FOR $1 NOW RUNNING IT
-#node ../backend/boot.js `echo $1 | sed 's/\.wyv/\.wyb/'` > `echo $1 | sed 's/\.wyv/\.js/'`
-#node  `echo $1 | sed 's/\.wyv/\.js/'`
+echo FINISHED PRODUCING WYB FILE FOR $1 NOW RUNNING IT
+node ../backend/boot.js `echo $1 | sed 's/\.wyv/\.wyb/'` > `echo $1 | sed 's/\.wyv/\.js/'`
+node  `echo $1 | sed 's/\.wyv/\.js/'`

selfhost/tests/monoid.wyv

@@ -10,7 +10,6 @@ type Monoid:z:
     type T <= Unit
     val id:z.T
     def op(a:z.T, b:z.T):z.T
-subtype Monoid extends Semi
 
 val sum = new this:Monoid {type T = Int}:
     type T = Int
@@ -19,10 +18,11 @@ val sum = new this:Monoid {type T = Int}:
         a + b
 
 type Util:z:
-    def apply3(s:Semi, a:s.T, b:s.T, c:s.T):s.T
+    def apply3(s:Monoid, a:s.T, b:s.T, c:s.T):s.T
 
 val util = new this:Util:
-    def apply3(s:Semi, a:s.T, b:s.T, c:s.T):s.T:
+    def apply3(s:Monoid, a:s.T, b:s.T, c:s.T):s.T:
         s.op(a,s.op(b,c))
 
-util.apply3(sum,1,2,3)
+val ans = util.apply3(sum,1,2,3)
+ans

selfhost/tests/object.wyv

@@ -1,15 +1,15 @@
-type Int:
+type Int:z:
     def +(i:Int):Int
     def -(i:Int):Int
 
-type List:
+type List:z:
     def sum(u:Unit):Int
 
-type Empty:
+type Empty:z:
     def sum(u:Unit):Int
 subtype Empty extends List
 
-type Node:
+type Node:z:
     def sum(u:Unit):Int
     val next:List
 subtype Node extends List

selfhost/tests/typemember.wyv

@@ -10,14 +10,13 @@ type Fruit:z:
     type T <= Unit
     type S <= Unit
     val item:z.T
-    def equals(x:z.T):z.S
-subtype Fruit extends Equatable
+    def equals(x:z.T):Int
 
 val f1 = new this:Fruit {type T = Int}:
     type T = Int
     type S <= Unit
     val item:this.T = 3
-    def equals(x:this.T):this.S:
+    def equals(x:this.T):Int:
         this.item + x
 
 f1.equals(3)

selfhost/toBytecode.wyv

@@ -24,6 +24,8 @@ def toBytecodeDecl(e:types.Decl):b.Decl = match e:
     d:types.Def       => b.MethodDecl(d.binding.name, d.args.map[String](e => e.arg.name), b.SeqExpr(toBytecodeStmt(d.body)))
     t:types.TypeDecl  => b.ValDecl("_", toBytecodeExpr(types.UnitVal()))
     s:types.SubtypeDecl => b.ValDecl("_", toBytecodeExpr(types.UnitVal()))
+    m:types.TypeEq => b.ValDecl("_", toBytecodeExpr(types.UnitVal()))
+
 
     default => error.report("not a declaration",error.unknownLocation)
 

selfhost/typecheck.wyv

@@ -42,13 +42,14 @@ def typecheckDecl(e:types.Decl, gamma:List[DeclType]):DeclType = match e:
         types.TypeType(t.name, t.z, t.typ)
     d:types.Def =>
         val argdecls:List[DeclType] = d.args.map[ValType]((a:types.Arg) => types.ValType(a.arg,a.argTyp))
-        val testType = typecheckStmt(d.body, argdecls.append(gamma))
-        if (true /*TODO: subtyping.isSubtype(testType, d.retTyp, gamma)*/)
+        val ngamma = argdecls.append(gamma)
+        val testType = typecheckStmt(d.body, ngamma)
+        if (isSubtype(testType, d.retTyp, ngamma))
             types.DefType(d.binding, d.args, d.retTyp)
           else
             error.report("def decl is not well-formed",error.unknownLocation)
     s:types.SubtypeDecl =>
-        if (true /*TODO: subtyping.checkSubtypeWF(s.subtype, s.supertype, gamma)*/)
+        if (checkSubtypeWF(s.subtype, s.supertype, gamma))
             types.SubtypeType(s.subtype, s.supertype)
           else
             error.report("subtype decl is not well-formed",error.unknownLocation)
@@ -71,20 +72,28 @@ def typecheckExpr(e:types.Exp, gamma:List[DeclType]):Type = match e:
         val unfold = unfoldType(recType, gamma)
         val argtypes:List[Type] = c.args.map[Type](e => typecheckExpr(e,gamma))
 
-        //val subcheck = x:Type => y:Type => subtyping.isSubtype(x,y,gamma)
         val pred = ((b:DeclType) =>
             val z = match b:
                 da:DefType => 
-                    if (c.name == da.name.name && true /*TODO: subtyping.checkArgList(argtypes,da.args,subcheck)*/) { option.Some[DefType](da) } else { option.None[DefType]() }
+                    val argBindings = da.args.map[Binding](a => a.arg)
+
+                    val argsSub = da.args.map[ValType](e => types.ValType(e.arg,types.substituteType(e.argTyp,c.receiver,unfold.z)))
+                    val argsSub2 = argsSub.map[ValType](e => types.ValType(e.name,typesUtil.doListOfSubstitutions(e.typ,c.args,argBindings)))
+                    val defargs = argsSub2.map[Type](e => e.typ)
+
+                    val argsSub3 = argsSub2.map[DeclType](e => e)
+                    val ngamma:List[DeclType] = argsSub3.append(gamma)
+
+                    val subcheck = x:Type => y:Type => isSubtype(x,y,ngamma)
+                    if (c.name == da.name.name && checkArgList(argtypes,defargs,subcheck)) { option.Some[DefType](da) } else { option.None[DefType]() }
                 default => option.None[DefType]()
             z
         )
         val func = typesUtil.findInDeclList[DefType](unfold.decls, pred)
         //Do substitutions to get the correct return type
         val retTyp = types.substituteType(func.retTyp, c.receiver, unfold.z)
         val argBindings = func.args.map[Binding](a => a.arg)
-        val zipargs = typesUtil.zip[types.Exp,Binding](c.args,argBindings)
-        zipargs.foldRight[Type]((x:Pair[types.Exp,Binding],t:Type)=>types.substituteType(t,x.first,option.Some[Binding](x.second)),retTyp)
+        typesUtil.doListOfSubstitutions(retTyp,c.args,argBindings)
 
     f:types.Field => //T-Field
         val recType = typecheckExpr(f.receiver, gamma)
@@ -101,19 +110,24 @@ def typecheckExpr(e:types.Exp, gamma:List[DeclType]):Type = match e:
 
     n:types.New => //T-New
         val unfold = unfoldType(n.typ, gamma)
+
+        val thisType = types.ValType(n.binding, n.typ)
+        val ngamma = llist.Cons[DeclType](thisType, gamma)
         def typeNewDecls(d:types.Decl):DeclType
-            val thisType = types.ValType(n.binding, n.typ)
-            val ngamma = llist.Cons[DeclType](thisType, gamma)
             match d:
                 v:types.Val         => typecheckDecl(d, gamma)
                 d:types.Def         => typecheckDecl(d, ngamma)
                 t:types.TypeDecl    => typecheckDecl(d, ngamma)
                 s:types.SubtypeDecl => typecheckDecl(d, ngamma)
                 t:types.TypeEq      => typecheckDecl(d, ngamma)
         val decls = n.body.map[DeclType](x => typeNewDecls(x))
-        n.typ
-    //TODO:do proper check with unfold   /*subtyping.checkDeclList(decls, unfold, x=>y=>subtyping.isSubtypeDecl(x,y,gamma))*/
-    //    if (true) {n.typ} else {error.report("invalid new expression",error.unknownLocation)}
+        val unfoldDecls = unfold.decls.map[DeclType](d => types.substituteDeclType(d,types.Var(n.binding),unfold.z))
+        //n.typ
+        //error.report("decls: " + typesUtil.combineStringList(unfoldDecls.map[String](e => typesUtil.declTypeToString(e))),error.unknownLocation)
+        if (isSubtypeDeclList(decls,unfoldDecls,ngamma)) 
+            n.typ 
+          else 
+            error.report("invalid new expression",error.unknownLocation)
 
     i:types.Integer => 
         val pred = ((b:DeclType) =>
@@ -214,10 +228,12 @@ def equalDeclType(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match
         default => false
     d:DefType => match b:
         u:DefType => 
-            val pred = x:Type => y:Type => equalType(x,y,gamma)
             val dargs = d.args.map[Type](e => e.argTyp)
             val uargs = u.args.map[Type](e => e.argTyp)
-            d.name.name == u.name.name && checkArgList(dargs,uargs,pred) && equalType(d.retTyp,u.retTyp,gamma)
+            val ngamma = d.args.map[DeclType](e => types.ValType(e.arg,e.argTyp)).append(gamma)
+            val nngamma = u.args.map[DeclType](e => types.ValType(e.arg,e.argTyp)).append(ngamma)
+            val pred = x:Type => y:Type => equalType(x,y,nngamma)
+            d.name.name == u.name.name && checkArgList(dargs,uargs,pred) && equalType(d.retTyp,u.retTyp,nngamma)
         default => false
     s:SubtypeType => match b:
         u:SubtypeType =>
@@ -258,10 +274,12 @@ def isSubtypeDecl(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match
         default => false
     d:DefType => match b:
         u:DefType => 
-            val pred = x:Type => y:Type => isSubtype(x,y,gamma)
             val dargs = d.args.map[Type](e => e.argTyp)
             val uargs = u.args.map[Type](e => e.argTyp)
-            d.name.name == u.name.name && checkArgList(uargs,dargs,pred) && isSubtype(d.retTyp,u.retTyp,gamma)
+            val ngamma = d.args.map[DeclType](e => types.ValType(e.arg,e.argTyp)).append(gamma)
+            val nngamma = u.args.map[DeclType](e => types.ValType(e.arg,e.argTyp)).append(ngamma)
+            val pred = x:Type => y:Type => isSubtype(x,y,nngamma)
+            d.name.name == u.name.name && checkArgList(uargs,dargs,pred) && isSubtype(d.retTyp,u.retTyp,nngamma)
         default => false
     s:SubtypeType => match b:
         u:SubtypeType => equalType(s.subtype,u.subtype,gamma) && equalType(s.supertype,u.supertype,gamma)
@@ -287,15 +305,43 @@ def isSubtypeDecl(a:DeclType, b:DeclType, gamma:List[DeclType]):Boolean = match
         default => false
 
 def isSubtype(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
-    val normalAns = (() => 
-        if (equalType(t2,types.theUnit,gamma)) { true } else { isSubtypeBase(t1,t2.base,gamma) && isSubtypeDeclList(t1.refines,t2.refines,gamma) }
-    )
-    true
-    //match t1.base:
-    //    path:PathType =>
-    //        val tau = typecheckExpr(path.p,gamma)
-    //        val unfold = unfoldType(tau,gamma)
-    //        //TODO            
+    def normalAns():Boolean
+        if (equalType(t2,types.theUnit,gamma)) 
+            true 
+          else 
+            isSubtypeBase(t1,t2.base,gamma) && isSubtypeDeclList(t1.refines,t2.refines,gamma)
+    def recurseRHS():Boolean = match t2.base:
+        path:PathType =>
+            val tau = typecheckExpr(path.p,gamma)
+            val pUnfold = unfoldType(tau,gamma)
+            val d = fetchDeclFromList(path,pUnfold.decls)
+            match d:
+                m:MemberType => match m.bound:
+                    l:types.LEQ => false
+                    default =>
+                        val typeBound = typesUtil.addRefines(m.typ,t2.refines)
+                        val subType = types.substituteType(typeBound,path.p,pUnfold.z)
+                        isSubtype(t1,subType,gamma)
+                t:TypeType => normalAns()
+        default => normalAns()
+
+    if (equalBaseType(t1.base,t2.base,gamma))
+        isSubtypeDeclList(t1.refines,t2.refines,gamma)
+      else
+        match t1.base:
+            path:PathType =>
+                val tau = typecheckExpr(path.p,gamma)
+                val pUnfold = unfoldType(tau,gamma)
+                val d = fetchDeclFromList(path,pUnfold.decls)
+                match d:
+                    m:MemberType => match m.bound:
+                        g:types.GEQ => false
+                        default => 
+                            val typeBound = typesUtil.addRefines(m.typ,t1.refines)
+                            val subType = types.substituteType(typeBound,path.p,pUnfold.z)
+                            isSubtype(subType,t2,gamma)
+                    t:TypeType => recurseRHS()
+            default => recurseRHS()
 
 def isSubtypeBase(t1:Type, t2:BaseType, gamma:List[DeclType]):Boolean
     val b1 = types.Type(t1.base,llist.Nil[DeclType]())
@@ -324,10 +370,18 @@ def isSubtypeBase(t1:Type, t2:BaseType, gamma:List[DeclType]):Boolean
             default => false
 
 def checkSubtypeWF(t1:Type, t2:Type, gamma:List[DeclType]):Boolean
-    true
-    //TODO:
-    //val ua = types.unfoldType(t1,gamma)
-    //val ub = types.unfoldType(t2,gamma)
-    //val newgamma = llist.Cons[DeclType](types.SubtypeType(t1,t2),gamma)
-    //isSubtypeDeclList(ua,ub,newgamma)
+    val ua = unfoldType(t1,gamma)
+    val ub = unfoldType(t2,gamma)
+    var newgamma:List[DeclType] = llist.Cons[DeclType](types.SubtypeType(t1,t2),gamma)
+    match ua.z:
+        s:option.Some => 
+            val vt = types.ValType(s.get(),t1)
+            newgamma = llist.Cons[DeclType](vt,newgamma)
+    match ub.z:
+        s:option.Some => 
+            val vt = types.ValType(s.get(),t2)
+            newgamma = llist.Cons[DeclType](vt,newgamma)
+    //val ng:List[DeclType] = newgamma
+    //error.report("ngamma: \n" + typesUtil.combineWithNewlines(ng.map[String](e => typesUtil.declTypeToString(e))),error.unknownLocation)
+    isSubtypeDeclList(ua.decls,ub.decls,newgamma)
 

selfhost/types.wyv

@@ -47,6 +47,7 @@ def Context(bs:List[DeclType], c:Counter, p:String -> raw.Exp) : Context = new
 
 def emptyContext(p:String -> raw.Exp):Context = Context(llist.Nil[DeclType](), Counter(), p)
 
+//TODO: ARG should really just be a valType to make things easier
 type Arg
     val arg:Binding
     val argTyp:Type
@@ -91,8 +92,6 @@ def makeNominalType(L:Binding):Type = new
 def makeRefines(ls:List[DeclType]):Type = new
     val base = UnitType()
     val refines = ls
-//def makeBase(b:BaseType):Type
-//    Type(b,llist.Nil[DeclType]())
 
 datatype Bound
     LEQ()    

selfhost/typesUtil.wyv

@@ -39,6 +39,10 @@ def zip[U,T](xs:List[U], ys:List[T]):List[Pair[U,T]] = match xs:
         default => llist.Nil[Pair[U,T]]()
     default => llist.Nil[Pair[U,T]]()
 
+def doListOfSubstitutions(ty:Type, exps:List[types.Exp], bindings:List[Binding]):Type
+    val zipargs = zip[types.Exp,Binding](exps,bindings)
+    zipargs.foldRight[Type]((x:Pair[types.Exp,Binding],t:Type)=>types.substituteType(t,x.first,option.Some[Binding](x.second)),ty)
+
 def equalBound(a:types.Bound, b:types.Bound):Boolean = match a:
     x:types.LEQ => match b:
         y:types.LEQ => true   
@@ -50,6 +54,16 @@ def equalBound(a:types.Bound, b:types.Bound):Boolean = match a:
         y:types.GEQ => true   
         default => false
 
+def addRefines(t:Type, decls:List[DeclType]):Type
+    types.Type(t.base,decls.append(t.refines))
+
+/////////////////////////
+def combineWithNewlines(ls:List[String]):String = match ls:
+    c:llist.Cons => match c.next:
+        n:llist.Nil => c.value
+        cc:llist.Cons => c.value + "\n" + combineWithNewlines(c.next)
+    default => ""
+
 def combineStringList(ls:List[String]):String = match ls:
     c:llist.Cons => match c.next:
         n:llist.Nil => c.value