From a4eaa9ca427cdc752b0d55663085a5d0eccfb551 Mon Sep 17 00:00:00 2001 From: tmoux Date: Sat, 4 Jul 2020 13:32:08 -0500 Subject: [PATCH] fixing type equality stuff --- selfhost/binding.wyv | 6 ++---- selfhost/bound.wyv | 4 +--- selfhost/subtyping.wyv | 13 ++++++++++--- selfhost/tests/subtypeTest.wyv | 6 ++++++ selfhost/toBytecode.wyv | 1 - selfhost/typecheck.wyv | 5 +---- selfhost/types.wyv | 16 ++++++++++------ 7 files changed, 30 insertions(+), 21 deletions(-) diff --git a/selfhost/binding.wyv b/selfhost/binding.wyv index 7fa4edba6..295b46cb5 100644 --- a/selfhost/binding.wyv +++ b/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) diff --git a/selfhost/bound.wyv b/selfhost/bound.wyv index 3dd30679f..093d6ee7e 100644 --- a/selfhost/bound.wyv +++ b/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: diff --git a/selfhost/subtyping.wyv b/selfhost/subtyping.wyv index 806036593..65fff2767 100644 --- a/selfhost/subtyping.wyv +++ b/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)) diff --git a/selfhost/tests/subtypeTest.wyv b/selfhost/tests/subtypeTest.wyv index 243f12361..09d6d6710 100644 --- a/selfhost/tests/subtypeTest.wyv +++ b/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 diff --git a/selfhost/toBytecode.wyv b/selfhost/toBytecode.wyv index ddb93d557..4300b3a90 100644 --- a/selfhost/toBytecode.wyv +++ b/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) diff --git a/selfhost/typecheck.wyv b/selfhost/typecheck.wyv index 8ee125056..d2118efa4 100644 --- a/selfhost/typecheck.wyv +++ b/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 diff --git a/selfhost/types.wyv b/selfhost/types.wyv index 17b668284..56a0404e4 100644 --- a/selfhost/types.wyv +++ b/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)