From a4f6d8195352f6f3bbd40e4034583e97f01e24dc Mon Sep 17 00:00:00 2001 From: tmoux Date: Mon, 13 Jul 2020 17:56:16 -0500 Subject: [PATCH] adding more stuff --- selfhost/binding.wyv | 4 +- selfhost/bound.wyv | 1 + selfhost/main.wyv | 40 ++++++------ selfhost/run.sh | 6 +- selfhost/tests/monoid.wyv | 8 +-- selfhost/tests/object.wyv | 8 +-- selfhost/tests/typemember.wyv | 5 +- selfhost/toBytecode.wyv | 2 + selfhost/typecheck.wyv | 116 +++++++++++++++++++++++++--------- selfhost/types.wyv | 3 +- selfhost/typesUtil.wyv | 14 ++++ 11 files changed, 140 insertions(+), 67 deletions(-) diff --git a/selfhost/binding.wyv b/selfhost/binding.wyv index 19e59302d..c15e67126 100644 --- a/selfhost/binding.wyv +++ b/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 => diff --git a/selfhost/bound.wyv b/selfhost/bound.wyv index 7d69f9cbc..8618c4ce4 100644 --- a/selfhost/bound.wyv +++ b/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 diff --git a/selfhost/main.wyv b/selfhost/main.wyv index ef8f16c09..542b23d51 100644 --- a/selfhost/main.wyv +++ b/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) -*/ diff --git a/selfhost/run.sh b/selfhost/run.sh index 656b3286a..01ef69248 100755 --- a/selfhost/run.sh +++ b/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/'` diff --git a/selfhost/tests/monoid.wyv b/selfhost/tests/monoid.wyv index 390bc1f35..a464b5bdd 100644 --- a/selfhost/tests/monoid.wyv +++ b/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 diff --git a/selfhost/tests/object.wyv b/selfhost/tests/object.wyv index 0fb8c858e..9daf79c53 100644 --- a/selfhost/tests/object.wyv +++ b/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 diff --git a/selfhost/tests/typemember.wyv b/selfhost/tests/typemember.wyv index 148ead4bc..66e592dee 100644 --- a/selfhost/tests/typemember.wyv +++ b/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) diff --git a/selfhost/toBytecode.wyv b/selfhost/toBytecode.wyv index 69351c194..ae93e8e3f 100644 --- a/selfhost/toBytecode.wyv +++ b/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) diff --git a/selfhost/typecheck.wyv b/selfhost/typecheck.wyv index eb10a9c71..912f14551 100644 --- a/selfhost/typecheck.wyv +++ b/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,11 +72,20 @@ 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 ) @@ -83,8 +93,7 @@ def typecheckExpr(e:types.Exp, gamma:List[DeclType]):Type = match e: //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,9 +110,10 @@ 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) @@ -111,9 +121,13 @@ def typecheckExpr(e:types.Exp, gamma:List[DeclType]):Type = match e: 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) diff --git a/selfhost/types.wyv b/selfhost/types.wyv index cd288a036..b707af7cd 100644 --- a/selfhost/types.wyv +++ b/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() diff --git a/selfhost/typesUtil.wyv b/selfhost/typesUtil.wyv index a2f3fd282..19ffe5373 100644 --- a/selfhost/typesUtil.wyv +++ b/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