From 5c30c7ad21143d9b63457d957a588d8250210c5e Mon Sep 17 00:00:00 2001 From: tmoux Date: Thu, 16 Jul 2020 14:15:49 -0500 Subject: [PATCH] update tests --- selfhost/failtests/badsubtype2.wyv | 2 +- selfhost/main.wyv | 38 +++++++-------- selfhost/run.sh | 6 +-- selfhost/tests/aliasTest.wyv | 16 ------- selfhost/tests/arity.wyv | 4 +- selfhost/tests/counter.wyv | 6 +-- selfhost/tests/fib.wyv | 6 +-- selfhost/tests/loop.wyv | 4 +- selfhost/tests/newtest.wyv | 7 ++- selfhost/tests/pair.wyv | 17 +++++++ selfhost/tests/subtypeTest.wyv | 10 ++-- selfhost/tests/testFn.wyv | 6 +-- selfhost/tests/testInt.wyv | 2 +- selfhost/tests/testShadow.wyv | 8 ++-- selfhost/tests/testVar.wyv | 4 +- selfhost/tests/tree.wyv | 8 ++-- selfhost/tests/typeTest.wyv | 10 ++-- selfhost/typecheck.wyv | 74 +++++++++++++++++++++--------- selfhost/typesUtil.wyv | 2 + 19 files changed, 133 insertions(+), 97 deletions(-) delete mode 100644 selfhost/tests/aliasTest.wyv create mode 100644 selfhost/tests/pair.wyv diff --git a/selfhost/failtests/badsubtype2.wyv b/selfhost/failtests/badsubtype2.wyv index 1626bcccb..ae87248bb 100644 --- a/selfhost/failtests/badsubtype2.wyv +++ b/selfhost/failtests/badsubtype2.wyv @@ -14,6 +14,6 @@ type C:z: val a:Int subtype Unit {val a:Int} extends C -subtype Unit {val a:Int} extends A +subtype Unit {type T <= Int, val a:Int} extends B 0 diff --git a/selfhost/main.wyv b/selfhost/main.wyv index 542b23d51..29fef49dd 100644 --- a/selfhost/main.wyv +++ b/selfhost/main.wyv @@ -62,24 +62,25 @@ def parse(s:String):raw.Exp 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: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 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") @@ -93,3 +94,4 @@ stdout.print(outputFileName) stdout.print("...\n") toBytecode.writeExpToFile(ooExp, outputFileName) +*/ diff --git a/selfhost/run.sh b/selfhost/run.sh index 01ef69248..656b3286a 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/aliasTest.wyv b/selfhost/tests/aliasTest.wyv deleted file mode 100644 index 2ce983032..000000000 --- a/selfhost/tests/aliasTest.wyv +++ /dev/null @@ -1,16 +0,0 @@ -type Int: - def +(i:Int):Int - def -(i:Int):Int - -type A = Int -type B = Int -type C = B -type D = C -type E = A - -subtype A extends B -subtype B extends A - -val calc = x:D => y:E => x + y -val id = x:C => x -calc (id 3) (id 2) diff --git a/selfhost/tests/arity.wyv b/selfhost/tests/arity.wyv index cd52d392a..643e8b138 100644 --- a/selfhost/tests/arity.wyv +++ b/selfhost/tests/arity.wyv @@ -1,8 +1,8 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type A: +type A:z: def f(x:Int):Int def g(x:Int,y:Int,z:Int):Int diff --git a/selfhost/tests/counter.wyv b/selfhost/tests/counter.wyv index a1710c7e8..d8c9c020d 100644 --- a/selfhost/tests/counter.wyv +++ b/selfhost/tests/counter.wyv @@ -1,12 +1,12 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type Counter: +type Counter:z: val a:Int def next(u:Unit):Counter -type X: +type X:z: def makeCounter(b:Int):Counter val x = new self:X: diff --git a/selfhost/tests/fib.wyv b/selfhost/tests/fib.wyv index 6940cc0e0..4ac5dd056 100644 --- a/selfhost/tests/fib.wyv +++ b/selfhost/tests/fib.wyv @@ -1,13 +1,13 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type Fib: +type Fib:z: val a1:Int val a2:Int def next(u:Unit):Fib -type X: +type X:z: def makeFib(x:Int,y:Int):Fib val x = new self:X: diff --git a/selfhost/tests/loop.wyv b/selfhost/tests/loop.wyv index 2951a56a5..c0c69f4cb 100644 --- a/selfhost/tests/loop.wyv +++ b/selfhost/tests/loop.wyv @@ -1,8 +1,8 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type X: +type X:z: def f(x:Int):Int val temp:Int diff --git a/selfhost/tests/newtest.wyv b/selfhost/tests/newtest.wyv index 3a08c3c8f..4fc79635a 100644 --- a/selfhost/tests/newtest.wyv +++ b/selfhost/tests/newtest.wyv @@ -1,8 +1,8 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type Foo: +type Foo:z: def sum(x:Int):Int val a:Int @@ -11,8 +11,7 @@ val foo = new this:Foo: this.a + x val a = 5 -type Bar = Foo -val bar = new this:Bar: +val bar = new this:Foo: def sum(x:Int):Int: this.a + x val a = 5 diff --git a/selfhost/tests/pair.wyv b/selfhost/tests/pair.wyv new file mode 100644 index 000000000..53c330544 --- /dev/null +++ b/selfhost/tests/pair.wyv @@ -0,0 +1,17 @@ +type Int:z: + def +(i:Int):Int + def -(i:Int):Int + +type Pair:z: + type S <= Unit + type T <= Unit + val fst:z.S + val snd:z.T + +val p1 = new this:Pair {type S = Int, type T = Unit}: + type S = Int + type T = Unit + val fst:this.S = 3 + val snd:this.T = () + +p1 diff --git a/selfhost/tests/subtypeTest.wyv b/selfhost/tests/subtypeTest.wyv index 09d6d6710..7bf8938e2 100644 --- a/selfhost/tests/subtypeTest.wyv +++ b/selfhost/tests/subtypeTest.wyv @@ -1,20 +1,20 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type Foo: +type Foo:z: def +(i:Int):Foo def -(i:Int):Foo subtype Foo extends Int -type A: +type A:z: def calc(x:Int):A -type B: +type B:z: def calc(x:Int):B val z:Int subtype B extends A subtype B extends Unit -type C: +type C:z: def calc(x:Int):C val z:Int val y:B diff --git a/selfhost/tests/testFn.wyv b/selfhost/tests/testFn.wyv index 0dd737525..34d5f4eae 100644 --- a/selfhost/tests/testFn.wyv +++ b/selfhost/tests/testFn.wyv @@ -1,15 +1,15 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type IntToInt: +type IntToInt:z: def f(i:Int):Int val succ = new this:IntToInt: def f(i:Int):Int: i+1 -type A: +type A:z: def f(i:IntToInt):Int val apply0 = new this:A: diff --git a/selfhost/tests/testInt.wyv b/selfhost/tests/testInt.wyv index 41f775a42..5fd1bbcfb 100644 --- a/selfhost/tests/testInt.wyv +++ b/selfhost/tests/testInt.wyv @@ -1,4 +1,4 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int diff --git a/selfhost/tests/testShadow.wyv b/selfhost/tests/testShadow.wyv index e6a0657e9..3b91fc83e 100644 --- a/selfhost/tests/testShadow.wyv +++ b/selfhost/tests/testShadow.wyv @@ -1,21 +1,21 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type X: +type X:z: val a:Int val x = new this:X: val a = 5 -type Fn: +type Fn:z: def f(x:Int):Int val fn = new this:Fn: def f(b:Int):Int: x.a + b -type X: +type X:z: val b:Int val y = new this:X: diff --git a/selfhost/tests/testVar.wyv b/selfhost/tests/testVar.wyv index da10c308a..4c4abe714 100644 --- a/selfhost/tests/testVar.wyv +++ b/selfhost/tests/testVar.wyv @@ -1,8 +1,8 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type A: +type A:z: val a:Int val x = new this:A: diff --git a/selfhost/tests/tree.wyv b/selfhost/tests/tree.wyv index bea68e0dc..f6e323bd9 100644 --- a/selfhost/tests/tree.wyv +++ b/selfhost/tests/tree.wyv @@ -1,15 +1,15 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type Tree: +type Tree:z: def sum(u:Unit):Int -type Empty: +type Empty:z: def sum(u:Unit):Int subtype Empty extends Tree -type Branch: +type Branch:z: def sum(u:Unit):Int val a:Int val left:Tree diff --git a/selfhost/tests/typeTest.wyv b/selfhost/tests/typeTest.wyv index 60b2dd4b6..f82d4cecc 100644 --- a/selfhost/tests/typeTest.wyv +++ b/selfhost/tests/typeTest.wyv @@ -1,23 +1,23 @@ -type Int: +type Int:z: def +(i:Int):Int def -(i:Int):Int -type Polygon: +type Polygon:z: def perim(u:Unit):Int -type Triangle: +type Triangle:z: val s1:Int val s2:Int val s3:Int def perim(u:Unit):Int subtype Triangle extends Polygon -type Square: +type Square:z: val s:Int def perim(u:Unit):Int subtype Square extends Polygon -type A: +type A:z: def makeTri(a:Int,b:Int,c:Int):Triangle val a = new this:A: diff --git a/selfhost/typecheck.wyv b/selfhost/typecheck.wyv index f176363a1..e2bd5bebe 100644 --- a/selfhost/typecheck.wyv +++ b/selfhost/typecheck.wyv @@ -37,10 +37,18 @@ def typecheckStmt(e:types.Statement, gamma:List[DeclType]):Type = match e: def typecheckDecl(e:types.Decl, gamma:List[DeclType]):DeclType = match e: v:types.Val => val typ = typecheckExpr(v.exp, gamma) - types.ValType(v.binding, typ) + if (isSubtype(typ,v.typ,gamma)) + types.ValType(v.binding, v.typ) + else + error.report("val expr not a subtype of declared type",error.unknownLocation) t:types.TypeDecl => - //TODO: check WF here - types.TypeType(t.name, t.z, t.typ) + val tt = types.TypeType(t.name, t.z, t.typ) + val ngamma = llist.Cons[DeclType](types.ValType(t.z,types.makeNominalType(t.name)),gamma) + val nngamma = llist.Cons[DeclType](tt,ngamma) + if (t.typ.foldRight[Boolean]((x:DeclType,y:Boolean)=>checkDeclTypeWF(x,nngamma),true)) + tt + else + error.report("type decl is not well-formed",error.unknownLocation) d:types.Def => val ngamma = d.args.map[DeclType](e=>e).append(gamma) val testType = typecheckStmt(d.body, ngamma) @@ -49,12 +57,16 @@ def typecheckDecl(e:types.Decl, gamma:List[DeclType]):DeclType = match e: else error.report("def decl is not well-formed: " + typesUtil.typeToString(testType) + " is not subtype of " + typesUtil.typeToString(d.retTyp),error.unknownLocation) s:types.SubtypeDecl => - if (checkSubtypeWF(s.subtype, s.supertype, gamma)) - types.SubtypeType(s.subtype, s.supertype) + val subDecl = types.SubtypeType(s.subtype, s.supertype) + if (checkDeclTypeWF(subDecl, gamma)) + subDecl else error.report("subtype decl is not well-formed",error.unknownLocation) t:types.TypeEq => - types.MemberType(t.name, types.EQ(),t.typ) + if (checkTypeWF(t.typ,gamma)) + types.MemberType(t.name, types.EQ(),t.typ) + else + error.report("typeEq type not well-formed",error.unknownLocation) def typecheckExpr(e:types.Exp, gamma:List[DeclType]):Type = match e: v:types.Var => @@ -115,18 +127,17 @@ def typecheckExpr(e:types.Exp, gamma:List[DeclType]):Type = match e: val ngamma = llist.Cons[DeclType](thisType, gamma) def typeNewDecls(d:types.Decl):DeclType match d: - v:types.Val => typecheckDecl(d, gamma) + v:types.Val => typecheckDecl(d, ngamma) 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)) val unfoldDecls = unfold.decls.map[DeclType](d => types.substituteDeclType(d,types.Var(n.binding),unfold.z)) - //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) + error.report("invalid new expression: "+"decls:\n" + typesUtil.combineWithNewlines(decls.map[String](e => typesUtil.declTypeToString(e))),error.unknownLocation) i:types.Integer => val pred = ((b:DeclType) => @@ -313,7 +324,7 @@ def isSubtype(t1:Type, t2:Type, gamma:List[DeclType]):Boolean val d = fetchDeclFromList(path,pUnfold.decls) match d: m:MemberType => match m.bound: - l:types.LEQ => false + l:types.LEQ => normalAns() default => val typeBound = typesUtil.addRefines(m.typ,t2.refines) val subType = types.substituteType(typeBound,path.p,pUnfold.z) @@ -331,7 +342,7 @@ def isSubtype(t1:Type, t2:Type, gamma:List[DeclType]):Boolean val d = fetchDeclFromList(path,pUnfold.decls) match d: m:MemberType => match m.bound: - g:types.GEQ => false + g:types.GEQ => normalAns() default => val typeBound = typesUtil.addRefines(m.typ,t1.refines) val subType = types.substituteType(typeBound,path.p,pUnfold.z) @@ -365,14 +376,35 @@ def isSubtypeBase(t1:Type, t2:BaseType, gamma:List[DeclType]):Boolean s:option.Some => true default => false -def checkSubtypeWF(t1:Type, t2:Type, gamma:List[DeclType]):Boolean - val ua = unfoldType(t1,gamma) - val ub = unfoldType(t2,gamma) - val ngamma = llist.Cons[DeclType](types.SubtypeType(t1,t2),gamma) - val nngamma = llist.Cons[DeclType](types.ValType(ua.z,t1),ngamma) - //ADD ua.z to ctx, substitute ub.z for ua.z - val supertypeDecls = ub.decls.map[DeclType](d => types.substituteDeclType(d,types.Var(ua.z),ub.z)) - isSubtypeDeclList(ua.decls,supertypeDecls,nngamma) +def checkTypeWF(t:Type, gamma:List[DeclType]):Boolean + match t.refines: + n:llist.Nil => true + c:llist.Cons => + val ua = unfoldType(t,gamma) + val ub = unfoldType(types.Type(t.base,llist.Nil[DeclType]()),gamma) + val ngamma = llist.Cons[DeclType](types.ValType(ua.z,t),gamma) + //error.report("decl list: " + typesUtil.printDeclList(ngamma)+"\n",error.unknownLocation) + isSubtypeDeclList(ua.decls,ub.decls,ngamma) -def checkTypeDeclWF(d:DeclType,gamma:List[DeclType]):Boolean - true +def checkDeclTypeWF(decl:DeclType,gamma:List[DeclType]):Boolean + match decl: + v:ValType => checkTypeWF(v.typ,gamma) + t:TypeType => + val ngamma = llist.Cons[DeclType](types.ValType(t.z,types.makeNominalType(t.name)),gamma) + val nngamma = llist.Cons[DeclType](t,ngamma) + t.unfld.foldRight[Boolean]((d:DeclType,y:Boolean)=>checkDeclTypeWF(d,nngamma) && y,true) + d:DefType => + val ngamma = d.args.map[DeclType](e=>e).append(gamma) + val checkArgsWF = d.args.foldRight[Boolean]((v:ValType,y:Boolean)=>checkTypeWF(v.typ,ngamma) && y,true) + val checkRetWF = checkTypeWF(d.retTyp,ngamma) + checkArgsWF && checkRetWF + s:SubtypeType => + val t1 = s.subtype + val t2 = s.supertype + val ua = unfoldType(t1,gamma) + val ub = unfoldType(t2,gamma) + val ngamma = llist.Cons[DeclType](types.SubtypeType(t1,t2),gamma) + val nngamma = llist.Cons[DeclType](types.ValType(ua.z,t1),ngamma) + val supertypeDecls = ub.decls.map[DeclType](d => types.substituteDeclType(d,types.Var(ua.z),ub.z)) + isSubtypeDeclList(ua.decls,supertypeDecls,nngamma) + m:MemberType => checkTypeWF(m.typ,gamma) diff --git a/selfhost/typesUtil.wyv b/selfhost/typesUtil.wyv index d6d3d0920..daa4b9e4b 100644 --- a/selfhost/typesUtil.wyv +++ b/selfhost/typesUtil.wyv @@ -76,6 +76,8 @@ def findTypePredicateFromStr(s:String):DeclType->Option[TypeType] ) pred ///////////////////////// +def printDeclList(ls:List[DeclType]):String + combineWithNewlines(ls.map[String](e => declTypeToString(e))) def combineWithNewlines(ls:List[String]):String = match ls: c:llist.Cons => match c.next: n:llist.Nil => c.value