Skip to content

Commit

Permalink
Merge pull request #181 from rise-lang/kinds-without-type-projections
Browse files Browse the repository at this point in the history
  • Loading branch information
@michel-steuwer
michel-steuwer authored Jun 2, 2021
2 parents 0ec968c + ddc21fa commit e9b9083
Show file tree
Hide file tree
Showing 88 changed files with 781 additions and 1,001 deletions.
40 changes: 27 additions & 13 deletions meta/src/main/scala/meta/generator/DPIAPrimitives.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,23 +140,22 @@ ${generateCaseClass(Type.Name(name), toParamList(definition, scalaParams), param
case DPIA.Type.AST.CommType => t"CommType"
case DPIA.Type.AST.PairType(lhs, rhs) => t"PhrasePairType[${generatePhraseType(lhs)}, ${generatePhraseType(rhs)}]"
case DPIA.Type.AST.FunType(inT, outT) => t"FunType[${generatePhraseType(inT)}, ${generatePhraseType(outT)}]"
case DPIA.Type.AST.DepFunType(id, kind, t) => t"DepFunType[${generateKindType(kind)}, ${generatePhraseType(t)}]"
case DPIA.Type.AST.DepFunType(id, kind, t) => t"DepFunType[${generateKindIdentifierType(kind)}, ${generatePhraseType(t)}]"
case DPIA.Type.AST.Identifier(name) => Type.Name(name)
case DPIA.Type.AST.VariadicType(_, _) => throw new Exception("Can not generate Phrase Type for Variadic Type")
}

// generate Scala type for representing the DPIA/rise kinds themselves
def generateKindType(kindAST: DPIA.Kind.AST): scala.meta.Type = kindAST match {
def generateKindIdentifierType(kindAST: DPIA.Kind.AST): scala.meta.Type = kindAST match {
case DPIA.Kind.AST.RiseKind(riseKind) => riseKind match {
case rise.Kind.AST.Data => Type.Name("DataKind")
case rise.Kind.AST.Address => Type.Name("AddressSpaceKind")
case rise.Kind.AST.Nat2Nat => Type.Name("NatToNatKind")
case rise.Kind.AST.Nat2Data => Type.Name("NatToDataKind")
case rise.Kind.AST.Nat => Type.Name("NatKind")
case rise.Kind.AST.Fragment => throw new Exception("Can not generate Kind for Fragment")
case rise.Kind.AST.MatrixLayout => throw new Exception("Can not generate Kind for Matrix Layout")
}
case DPIA.Kind.AST.Access => Type.Name("AccessKind")
case rise.Kind.AST.Data => Type.Name("DataTypeIdentifier")
case rise.Kind.AST.Address => Type.Name("AddressSpaceIdentifier")
case rise.Kind.AST.Nat2Nat => Type.Name("NatToNatIdentifier")
case rise.Kind.AST.Nat2Data => Type.Name("NatToDataIdentifier")
case rise.Kind.AST.Nat => Type.Name("NatIdentifier")
case rise.Kind.AST.Fragment => throw new Exception("Can not generate Kind for Fragment")
case rise.Kind.AST.MatrixLayout => throw new Exception("Can not generate Kind for Matrix Layout")
}
case DPIA.Kind.AST.Access => Type.Name("AccessTypeIdentifier")
case DPIA.Kind.AST.VariadicKind(_, _) => throw new Exception("Can not generate Kind for Variadic Kind")
}

Expand Down Expand Up @@ -287,7 +286,7 @@ ${generateCaseClass(Type.Name(name), toParamList(definition, scalaParams), param
case DPIA.Type.AST.FunType(inT, outT) =>
q"FunType(${generateTerm(inT)}, ${generateTerm(outT)})"
case DPIA.Type.AST.DepFunType(id, kind, t) =>
q"DepFunType[${generateKindType(kind)}, PhraseType](${Term.Name(id.name)}, ${generateTerm(t)})"
q"DepFunType(${generateKindType(kind)}, ${Term.Name(id.name)}, ${generateTerm(t)})"
case DPIA.Type.AST.VariadicType(_, _) => throw new Exception("Can not generate Term for Variadic Type")
}

Expand All @@ -297,6 +296,21 @@ ${generateCaseClass(Type.Name(name), toParamList(definition, scalaParams), param
case DPIA.Type.Access.AST.Write =>Term.Name("write")
}

// generate Scala type for representing the DPIA/rise kinds themselves
def generateKindType(kindAST: DPIA.Kind.AST): scala.meta.Term = kindAST match {
case DPIA.Kind.AST.RiseKind(riseKind) => riseKind match {
case rise.Kind.AST.Data => Term.Name("DataKind")
case rise.Kind.AST.Address => Term.Name("AddressSpaceKind")
case rise.Kind.AST.Nat2Nat => Term.Name("NatToNatKind")
case rise.Kind.AST.Nat2Data => Term.Name("NatToDataKind")
case rise.Kind.AST.Nat => Term.Name("NatKind")
case rise.Kind.AST.Fragment => throw new Exception("Can not generate Kind for Fragment")
case rise.Kind.AST.MatrixLayout => throw new Exception("Can not generate Kind for Matrix Layout")
}
case DPIA.Kind.AST.Access => Term.Name("AccessKind")
case DPIA.Kind.AST.VariadicKind(_, _) => throw new Exception("Can not generate Kind for Variadic Kind")
}

def generateVisitAndRebuild(name: scala.meta.Type.Name,
paramLists: List[List[scala.meta.Term.Param]]): scala.meta.Defn.Def = {
// little pattern matching helper that ignores if a type name is written with a package prefix
Expand Down
14 changes: 7 additions & 7 deletions meta/src/main/scala/meta/generator/RisePrimitives.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -180,24 +180,24 @@ import arithexpr.arithmetic._
// val ids = Seq.fill(n)(DataTypeIdentifier(freshName("dt"), isExplicit = true))
// ids.foldRight(t){ case (id, t) => DepFunType[DataKind](id, t) }
// to represent n-many dependent function types: (id0: kind) -> (id1: kind) -> ... -> t
val (createIds, typeName) = kind match {
val (createIds, kindName) = kind match {
case AST.Data =>
(q"""DataTypeIdentifier(freshName("dt"), isExplicit = true)""", Type.Name("DataKind"))
(q"""DataTypeIdentifier(freshName("dt"), isExplicit = true)""", Term.Name("DataKind"))
case AST.Address =>
(q"""AddressSpaceIdentifier(freshName("a"), isExplicit = true)""", Type.Name("AddressSpaceKind"))
(q"""AddressSpaceIdentifier(freshName("a"), isExplicit = true)""", Term.Name("AddressSpaceKind"))
case AST.Nat2Nat =>
(q"""NatToNatIdentifier(freshName("n2n"), isExplicit = true)""", Type.Name("NatToNatKind"))
(q"""NatToNatIdentifier(freshName("n2n"), isExplicit = true)""", Term.Name("NatToNatKind"))
case AST.Nat2Data =>
(q"""NatToDataIdentifier(freshName("n2d"), isExplicit = true)""", Type.Name("NatToDataKind"))
(q"""NatToDataIdentifier(freshName("n2d"), isExplicit = true)""", Term.Name("NatToDataKind"))
case AST.Nat =>
(q"""NatIdentifier(freshName("n"), isExplicit = true)""", Type.Name("NatKind"))
(q"""NatIdentifier(freshName("n"), isExplicit = true)""", Term.Name("NatKind"))
case AST.Fragment => throw new Exception("No support for Fragment Kind yet")
case AST.MatrixLayout => throw new Exception("No support for Matrix Layout Kind yet")
}
q"""{
val ${Pat.Var(Term.Name(ids.name))} = Seq.fill(${Term.Name(n.name)})($createIds)
${Term.Name(ids.name)}.foldRight(${generateTypeScheme(t)}: Type) {
case (id, t) => DepFunType[$typeName, Type](id, t)
case (id, t) => DepFunType($kindName, id, t)
}
}"""
case _ => generateDataType(typeAST)
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/apps/cameraPipelineRewrite.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ object cameraPipelineRewrite {

case class depFunction(s: Strategy[Rise]) extends Strategy[Rise] {
def apply(e: Rise): RewriteResult[Rise] = e match {
case ap @ DepApp(f, x) => s(f).mapSuccess(DepApp(_, x)(ap.t))
case ap @ DepApp(kind, f, x) => s(f).mapSuccess(DepApp(kind, _, x)(ap.t))
case _ => Failure(s)
}
override def toString: String = s"depFunction($s)"
Expand Down
12 changes: 6 additions & 6 deletions src/main/scala/rise/core/Builder.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,12 @@ trait Builder {
throw new Exception("apply method must be overridden")
def apply(e: DSL.ToBeTyped[Expr]): DSL.ToBeTyped[App] =
DSL.app(DSL.toBeTyped(apply), e)
def apply(n: Nat): DSL.ToBeTyped[DepApp[NatKind]] =
DSL.depApp[NatKind](DSL.toBeTyped(apply), n)
def apply(dt: DataType): DSL.ToBeTyped[DepApp[DataKind]] =
DSL.depApp[DataKind](DSL.toBeTyped(apply), dt)
def apply(a: AddressSpace): DSL.ToBeTyped[DepApp[AddressSpaceKind]] =
DSL.depApp[AddressSpaceKind](DSL.toBeTyped(apply), a)
def apply(n: Nat): DSL.ToBeTyped[DepApp[Nat]] =
DSL.depApp(NatKind, DSL.toBeTyped(apply), n)
def apply(dt: DataType): DSL.ToBeTyped[DepApp[DataType]] =
DSL.depApp(DataKind, DSL.toBeTyped(apply), dt)
def apply(a: AddressSpace): DSL.ToBeTyped[DepApp[AddressSpace]] =
DSL.depApp(AddressSpaceKind, DSL.toBeTyped(apply), a)

def unapply(arg: Expr): Boolean =
throw new Exception("unapply method must be overridden")
Expand Down
24 changes: 12 additions & 12 deletions src/main/scala/rise/core/DSL/Type.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,27 +94,27 @@ object Type {
object expl {
def apply(w: NatFunctionWrapper[Type]): Type = {
val x = NatIdentifier(freshName("n"), isExplicit = true)
DepFunType[NatKind, Type](x, w.f(x))
DepFunType(NatKind, x, w.f(x))
}

def apply(w: DataTypeFunctionWrapper[Type]): Type = {
val x = DataTypeIdentifier(freshName("dt"), isExplicit = true)
DepFunType[DataKind, Type](x, w.f(x))
DepFunType(DataKind, x, w.f(x))
}

def apply(w: NatToDataFunctionWrapper[Type]): Type = {
val x = NatToDataIdentifier(freshName("n2d"), isExplicit = true)
DepFunType[NatToDataKind, Type](x, w.f(x))
DepFunType(NatToDataKind, x, w.f(x))
}

def apply(w: NatToNatFunctionWrapper[Type]): Type = {
val x = NatToNatIdentifier(freshName("n2n"), isExplicit = true)
DepFunType[NatToNatKind, Type](x, w.f(x))
DepFunType(NatToNatKind, x, w.f(x))
}

def apply(w: AddressSpaceFunctionWrapper[Type]): Type = {
val x = AddressSpaceIdentifier(freshName("a"), isExplicit = true)
DepFunType[AddressSpaceKind, Type](x, w.f(x))
DepFunType(AddressSpaceKind, x, w.f(x))
}
}

Expand Down Expand Up @@ -160,24 +160,24 @@ object Type {
object Nat {
def `**`(f: Nat => DataType): Type = {
val x = NatIdentifier(freshName("n"), isExplicit = true)
DepPairType[NatKind](x, f(x))
DepPairType(NatKind, x, f(x))
}
}

object NatCollection {
def `**`(f: NatCollection => DataType): Type = {
val x = NatCollectionIdentifier(freshName("ns"), isExplicit = true)
DepPairType[NatCollectionKind](x, f(x))
DepPairType(NatCollectionKind, x, f(x))
}
}

object `:Nat **` {
def unapply(arg: DepPairType[NatKind]): Option[(NatIdentifier, DataType)] =
def unapply(arg: DepPairType[Nat, NatIdentifier]): Option[(NatIdentifier, DataType)] =
Some(arg.x, arg.t)
}

object `:NatCollection **` {
def unapply(arg: DepPairType[NatCollectionKind]): Option[(NatCollectionIdentifier, DataType)] =
def unapply(arg: DepPairType[NatCollection, NatCollectionIdentifier]): Option[(NatCollectionIdentifier, DataType)] =
Some(arg.x, arg.t)
}

Expand All @@ -195,7 +195,7 @@ object Type {
}

object `(Addr)->:` {
def unapply[K <: Kind, T <: Type](funType: DepFunType[K, T]): Option[(AddressSpaceIdentifier, T)] = {
def unapply[T, I <: Kind.Identifier, U <: Type](funType: DepFunType[T, I, U]): Option[(AddressSpaceIdentifier, U)] = {
funType.x match {
case a: AddressSpaceIdentifier => Some((a, funType.t))
case _ => throw new Exception("Expected AddressSpace DepFunType")
Expand All @@ -204,7 +204,7 @@ object Type {
}

object `(Nat)->:` {
def unapply[K <: Kind, T <: Type](funType: DepFunType[K, T]): Option[(NatIdentifier, T)] = {
def unapply[T, I <: Kind.Identifier, U <: Type](funType: DepFunType[T, I, U]): Option[(NatIdentifier, U)] = {
funType.x match {
case n: NatIdentifier => Some((n, funType.t))
case _ => throw new Exception("Expected Nat DepFunType")
Expand All @@ -213,7 +213,7 @@ object Type {
}

object `(NatToNat)->:` {
def unapply[K <: Kind, T <: Type](funType: DepFunType[K, T]): Option[(NatToNatIdentifier, T)] = {
def unapply[T, I <: Kind.Identifier, U <: Type](funType: DepFunType[T, I, U]): Option[(NatToNatIdentifier, U)] = {
funType.x match {
case n: NatToNatIdentifier => Some((n, funType.t))
case _ => throw new Exception("Expected NatToNat DepFunType")
Expand Down
19 changes: 5 additions & 14 deletions src/main/scala/rise/core/DSL/infer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,26 +118,17 @@ object infer {
val c = TypeConstraint(tf.t, FunType(te.t, exprT))
(App(tf, te)(exprT), csF ++ csE :+ c)

case expr@DepLambda(x, e) =>
case expr@DepLambda(kind, x, e) =>
val (te, csE) = constrainTypes(exprEnv)(e)
val tf = x match {
case n: NatIdentifier =>
DepLambda[NatKind](n, te)(DepFunType[NatKind, Type](n, te.t))
case dt: DataTypeIdentifier =>
DepLambda[DataKind](dt, te)(DepFunType[DataKind, Type](dt, te.t))
case ad: AddressSpaceIdentifier =>
DepLambda[AddressSpaceKind](ad, te)(DepFunType[AddressSpaceKind, Type](ad, te.t))
case n2n: NatToNatIdentifier =>
DepLambda[NatToNatKind](n2n, te)(DepFunType[NatToNatKind, Type](n2n, te.t))
}
val tf = DepLambda(kind, x, te)(DepFunType(kind, x, te.t))
val csE1 = ifTyped(expr.t)(TypeConstraint(expr.t, tf.t))
(tf, csE ++ csE1)

case expr@DepApp(f, x) =>
case expr@DepApp(kind, f, x) =>
val (tf, csF) = constrainTypes(exprEnv)(f)
val exprT = genType(expr)
val c = DepConstraint(tf.t, x, exprT)
(DepApp(tf, x)(exprT), csF :+ c)
val c = DepConstraint(kind, tf.t, x, exprT)
(DepApp(kind, tf, x)(exprT), csF :+ c)

case TypeAnnotation(e, t) =>
val (te, csE) = constrainTypes(exprEnv)(e)
Expand Down
73 changes: 36 additions & 37 deletions src/main/scala/rise/core/DSL/package.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,13 +19,12 @@ package object DSL {
x >>= (x => e >>= (e => toBeTyped(Lambda(x, e)(TypePlaceholder))))
def app(f: ToBeTyped[Expr], e: ToBeTyped[Expr]): ToBeTyped[App] =
f >>= (f => e >>= (e => toBeTyped(App(f, e)(TypePlaceholder))))
def depLambda[K <: Kind: KindName](
x: K#I with Kind.Explicitness,
e: ToBeTyped[Expr]
): ToBeTyped[DepLambda[K]] =
e >>= (e => toBeTyped(DepLambda[K](x, e)(TypePlaceholder)))
def depApp[K <: Kind](f: ToBeTyped[Expr], x: K#T): ToBeTyped[DepApp[K]] =
f >>= (f => toBeTyped(DepApp[K](f, x)(TypePlaceholder)))
def depLambda[T, I <: Kind.Identifier](kind: Kind[T, I],
x: I with Kind.Explicitness,
e: ToBeTyped[Expr]): ToBeTyped[DepLambda[T, I]] =
e >>= (e => toBeTyped(DepLambda(kind, x, e)(TypePlaceholder)))
def depApp[T](kind: Kind[T, _ <: Kind.Identifier], f: ToBeTyped[Expr], x: T): ToBeTyped[DepApp[T]] =
f >>= (f => toBeTyped(DepApp(kind, f, x)(TypePlaceholder)))
def literal(d: semantics.Data): ToBeTyped[Literal] = toBeTyped(Literal(d))

def store(cont: ToBeTyped[Expr] => ToBeTyped[Expr]): ToBeTyped[Expr] =
Expand Down Expand Up @@ -109,16 +108,16 @@ package object DSL {
e5: ToBeTyped[Expr]): ToBeTyped[App] =
f(e1)(e2)(e3)(e4)(e5)

def apply(n: Nat): ToBeTyped[DepApp[NatKind]] =
depApp[NatKind](f, n)
def apply(dt: DataType): ToBeTyped[DepApp[DataKind]] =
depApp[DataKind](f, dt)
def apply(a: AddressSpace): ToBeTyped[DepApp[AddressSpaceKind]] =
depApp[AddressSpaceKind](f, a)
def apply(n2n: NatToNat): ToBeTyped[DepApp[NatToNatKind]] =
depApp[NatToNatKind](f, n2n)
def apply(n2d: NatToData): ToBeTyped[DepApp[NatToDataKind]] =
depApp[NatToDataKind](f, n2d)
def apply(n: Nat): ToBeTyped[DepApp[Nat]] =
depApp(NatKind, f, n)
def apply(dt: DataType): ToBeTyped[DepApp[DataType]] =
depApp(DataKind, f, dt)
def apply(a: AddressSpace): ToBeTyped[DepApp[AddressSpace]] =
depApp(AddressSpaceKind, f, a)
def apply(n2n: NatToNat): ToBeTyped[DepApp[NatToNat]] =
depApp(NatToNatKind, f, n2n)
def apply(n2d: NatToData): ToBeTyped[DepApp[NatToData]] =
depApp(NatToDataKind, f, n2d)
}

implicit class FunPipe(e: ToBeTyped[Expr]) {
Expand Down Expand Up @@ -405,70 +404,70 @@ package object DSL {
object depFun {
def apply(r: arithexpr.arithmetic.Range,
w: NatFunction1Wrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[NatKind]] = {
): ToBeTyped[DepLambda[Nat, NatIdentifier]] = {
val n = NatIdentifier(freshName("n"), r, isExplicit = true)
depLambda[NatKind](n, w.f(n))
depLambda(NatKind, n, w.f(n))
}

def apply(w: NatFunction1Wrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[NatKind]] = {
): ToBeTyped[DepLambda[Nat, NatIdentifier]] = {
val r = arithexpr.arithmetic.RangeAdd(0, arithexpr.arithmetic.PosInf, 1)
val n = NatIdentifier(freshName("n"), r, isExplicit = true)
depLambda[NatKind](n, w.f(n))
depLambda(NatKind, n, w.f(n))
}

def apply(w: NatFunction2Wrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[NatKind]] = {
): ToBeTyped[DepLambda[Nat, NatIdentifier]] = {
val r = arithexpr.arithmetic.RangeAdd(0, arithexpr.arithmetic.PosInf, 1)
val n1 = NatIdentifier(freshName("n"), r, isExplicit = true)
depLambda[NatKind](n1, depFun((n2: Nat) => w.f(n1, n2)))
depLambda(NatKind, n1, depFun((n2: Nat) => w.f(n1, n2)))
}

def apply(w: NatFunction3Wrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[NatKind]] = {
): ToBeTyped[DepLambda[Nat, NatIdentifier]] = {
val r = arithexpr.arithmetic.RangeAdd(0, arithexpr.arithmetic.PosInf, 1)
val n1 = NatIdentifier(freshName("n"), r, isExplicit = true)
depLambda[NatKind](n1, depFun((n2: Nat, n3: Nat) => w.f(n1, n2, n3)))
depLambda(NatKind, n1, depFun((n2: Nat, n3: Nat) => w.f(n1, n2, n3)))
}

def apply(w: NatFunction4Wrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[NatKind]] = {
): ToBeTyped[DepLambda[Nat, NatIdentifier]] = {
val r = arithexpr.arithmetic.RangeAdd(0, arithexpr.arithmetic.PosInf, 1)
val n1 = NatIdentifier(freshName("n"), r, isExplicit = true)
depLambda[NatKind](n1, depFun((n2: Nat, n3: Nat, n4: Nat) =>
depLambda(NatKind, n1, depFun((n2: Nat, n3: Nat, n4: Nat) =>
w.f(n1, n2, n3, n4)))
}

def apply(w: NatFunction5Wrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[NatKind]] = {
): ToBeTyped[DepLambda[Nat, NatIdentifier]] = {
val r = arithexpr.arithmetic.RangeAdd(0, arithexpr.arithmetic.PosInf, 1)
val n1 = NatIdentifier(freshName("n"), r, isExplicit = true)
depLambda[NatKind](n1, depFun((n2: Nat, n3: Nat, n4: Nat, n5: Nat) =>
depLambda(NatKind, n1, depFun((n2: Nat, n3: Nat, n4: Nat, n5: Nat) =>
w.f(n1, n2, n3, n4, n5)))
}

def apply(w: DataTypeFunctionWrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[DataKind]] = {
): ToBeTyped[DepLambda[DataType, DataTypeIdentifier]] = {
val x = DataTypeIdentifier(freshName("dt"), isExplicit = true)
depLambda[DataKind](x, w.f(x))
depLambda(DataKind, x, w.f(x))
}

def apply(w: NatToDataFunctionWrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[NatToDataKind]] = {
): ToBeTyped[DepLambda[NatToData, NatToDataIdentifier]] = {
val x = NatToDataIdentifier(freshName("n2d"), isExplicit = true)
depLambda[NatToDataKind](x, w.f(x))
depLambda(NatToDataKind, x, w.f(x))
}

def apply(w: NatToNatFunctionWrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[NatToNatKind]] = {
): ToBeTyped[DepLambda[NatToNat, NatToNatIdentifier]] = {
val x = NatToNatIdentifier(freshName("n2n"), isExplicit = true)
depLambda[NatToNatKind](x, w.f(x))
depLambda(NatToNatKind, x, w.f(x))
}

def apply(w: AddressSpaceFunctionWrapper[ToBeTyped[Expr]]
): ToBeTyped[DepLambda[AddressSpaceKind]] = {
): ToBeTyped[DepLambda[AddressSpace, AddressSpaceIdentifier]] = {
val x = AddressSpaceIdentifier(freshName("a"), isExplicit = true)
depLambda[AddressSpaceKind](x, w.f(x))
depLambda(AddressSpaceKind, x, w.f(x))
}
}

Expand Down
Loading

0 comments on commit e9b9083

Please sign in to comment.