From 83d5a7b2a31d4b03345c907d8174cb620296a287 Mon Sep 17 00:00:00 2001 From: Dmitry Kurinskiy Date: Tue, 13 Jul 2021 17:43:24 +0300 Subject: [PATCH] Introducing top and bottom types (#199) * - Added top and bottom types - Added nil for empty streams, options, arrays - Fixed product variance * Version bump due to syntax changes in the type system --- aqua-src/demo.aqua | 16 +++++++++++++++- build.sbt | 2 +- model/src/main/scala/aqua/model/ValueModel.scala | 7 ++++++- .../scala/aqua/model/transform/BodyConfig.scala | 8 +++++++- .../src/main/scala/aqua/parser/lexer/Token.scala | 2 ++ .../main/scala/aqua/parser/lexer/TypeToken.scala | 12 +++++++++++- .../aqua/semantics/rules/types/TypesState.scala | 3 +++ types/src/main/scala/aqua/types/Type.scala | 11 +++++++++-- types/src/test/scala/aqua/types/TypeSpec.scala | 16 ++++++++++++++-- 9 files changed, 68 insertions(+), 9 deletions(-) diff --git a/aqua-src/demo.aqua b/aqua-src/demo.aqua index de501f03..7db88ad6 100644 --- a/aqua-src/demo.aqua +++ b/aqua-src/demo.aqua @@ -2,6 +2,9 @@ service OpH("op"): puk(s: string) -> string pek(s: string, -- trgtr c: string) -> string + pyk: []u32 -> string + pok: []bool -> string + identity: ⊤ -> ⊥ func a( -- ferkjn b: string, -- fr @@ -17,4 +20,15 @@ func a( -- ferkjn catch err: OpH.puk(err.msg) <- f - -- hello \ No newline at end of file + -- hello + +func z(t: ?string, b: []u32, c: *bool): + OpH.puk(t!) + OpH.pyk(b) + OpH.pok(c) + c <- OpH.identity(true) + c <- OpH.identity("string") + + +func k(): + z(nil, nil, nil) \ No newline at end of file diff --git a/build.sbt b/build.sbt index 56ecac63..e96dd42a 100644 --- a/build.sbt +++ b/build.sbt @@ -28,7 +28,7 @@ val cats = "org.typelevel" %% "cats-core" % catsV name := "aqua-hll" val commons = Seq( - baseAquaVersion := "0.1.8", + baseAquaVersion := "0.1.9", version := baseAquaVersion.value + "-" + sys.env.getOrElse("BUILD_NUMBER", "SNAPSHOT"), scalaVersion := dottyVersion, libraryDependencies ++= Seq( diff --git a/model/src/main/scala/aqua/model/ValueModel.scala b/model/src/main/scala/aqua/model/ValueModel.scala index 1791ec56..b179e9e4 100644 --- a/model/src/main/scala/aqua/model/ValueModel.scala +++ b/model/src/main/scala/aqua/model/ValueModel.scala @@ -1,6 +1,6 @@ package aqua.model -import aqua.types.{ProductType, ScalarType, Type} +import aqua.types.{DataType, ProductType, ScalarType, StreamType, Type} import cats.Eq import cats.data.{Chain, NonEmptyMap} import wvlet.log.LogSupport @@ -110,4 +110,9 @@ object VarModel { ) ) ) + + val nil: VarModel = VarModel( + "nil", + StreamType(DataType.Bottom) + ) } diff --git a/model/src/main/scala/aqua/model/transform/BodyConfig.scala b/model/src/main/scala/aqua/model/transform/BodyConfig.scala index 5da61dee..8176bfcf 100644 --- a/model/src/main/scala/aqua/model/transform/BodyConfig.scala +++ b/model/src/main/scala/aqua/model/transform/BodyConfig.scala @@ -1,6 +1,7 @@ package aqua.model.transform import aqua.model.{AquaContext, LiteralModel, ValueModel, VarModel} +import aqua.types.{DataType, OptionType} import cats.kernel.Monoid case class Constant(name: String, value: ValueModel) @@ -26,7 +27,12 @@ case class BodyConfig( AquaContext .implicits( AquaContext.blank - .copy(values = Map(VarModel.lastError.name -> VarModel.lastError) ++ constantsMap) + .copy(values = + Map( + VarModel.lastError.name -> VarModel.lastError, + VarModel.nil.name -> VarModel.nil + ) ++ constantsMap + ) ) .aquaContextMonoid } diff --git a/parser/src/main/scala/aqua/parser/lexer/Token.scala b/parser/src/main/scala/aqua/parser/lexer/Token.scala index ed5133f7..f8c74af6 100644 --- a/parser/src/main/scala/aqua/parser/lexer/Token.scala +++ b/parser/src/main/scala/aqua/parser/lexer/Token.scala @@ -65,6 +65,8 @@ object Token { val `*` : P[Unit] = P.char('*') val `!` : P[Unit] = P.char('!') val `[]` : P[Unit] = P.string("[]") + val `⊤` : P[Unit] = P.char('⊤') + val `⊥` : P[Unit] = P.char('⊥') val `(` : P[Unit] = P.char('(').surroundedBy(` `.?) val `)` : P[Unit] = P.char(')').surroundedBy(` `.?) val `()` : P[Unit] = P.string("()") diff --git a/parser/src/main/scala/aqua/parser/lexer/TypeToken.scala b/parser/src/main/scala/aqua/parser/lexer/TypeToken.scala index ec94d6e3..fb354715 100644 --- a/parser/src/main/scala/aqua/parser/lexer/TypeToken.scala +++ b/parser/src/main/scala/aqua/parser/lexer/TypeToken.scala @@ -12,6 +12,12 @@ import cats.syntax.functor._ sealed trait TypeToken[F[_]] extends Token[F] sealed trait DataTypeToken[F[_]] extends TypeToken[F] +case class TopBottomToken[F[_]: Comonad](override val unit: F[Unit], isTop: Boolean) + extends DataTypeToken[F] { + override def as[T](v: T): F[T] = unit.as(v) + def isBottom: Boolean = !isTop +} + case class ArrayTypeToken[F[_]: Comonad](override val unit: F[Unit], data: DataTypeToken[F]) extends DataTypeToken[F] { override def as[T](v: T): F[T] = unit.as(v) @@ -106,13 +112,17 @@ object DataTypeToken { def `arraytypedef`[F[_]: LiftParser: Comonad]: P[ArrayTypeToken[F]] = (`[]`.lift ~ `datatypedef`[F]).map(ud => ArrayTypeToken(ud._1, ud._2)) + def `topbottomdef`[F[_]: LiftParser: Comonad]: P[TopBottomToken[F]] = + `⊥`.lift.map(TopBottomToken(_, isTop = false)) | `⊤`.lift.map(TopBottomToken(_, isTop = true)) + def `datatypedef`[F[_]: LiftParser: Comonad]: P[DataTypeToken[F]] = P.oneOf( P.defer(`arraytypedef`[F]) :: P.defer(StreamTypeToken.`streamtypedef`) :: P.defer( OptionTypeToken.`optiontypedef` ) :: BasicTypeToken - .`basictypedef`[F] :: CustomTypeToken.ct[F] :: Nil + .`basictypedef`[F] :: CustomTypeToken.ct[F] :: `topbottomdef` :: Nil ) + } object TypeToken { diff --git a/semantics/src/main/scala/aqua/semantics/rules/types/TypesState.scala b/semantics/src/main/scala/aqua/semantics/rules/types/TypesState.scala index b260083e..d74aba84 100644 --- a/semantics/src/main/scala/aqua/semantics/rules/types/TypesState.scala +++ b/semantics/src/main/scala/aqua/semantics/rules/types/TypesState.scala @@ -14,6 +14,7 @@ import aqua.parser.lexer.{ OptionTypeToken, StreamTypeToken, Token, + TopBottomToken, TypeToken } import aqua.types.{ArrayType, ArrowType, DataType, OptionType, ProductType, StreamType, Type} @@ -30,6 +31,8 @@ case class TypesState[F[_]]( def resolveTypeToken(tt: TypeToken[F]): Option[Type] = tt match { + case TopBottomToken(_, isTop) => + Option(if (isTop) DataType.Top else DataType.Bottom) case ArrayTypeToken(_, dtt) => resolveTypeToken(dtt).collect { case it: DataType => ArrayType(it) diff --git a/types/src/main/scala/aqua/types/Type.scala b/types/src/main/scala/aqua/types/Type.scala index 685d89d4..60b5656f 100644 --- a/types/src/main/scala/aqua/types/Type.scala +++ b/types/src/main/scala/aqua/types/Type.scala @@ -15,6 +15,11 @@ sealed trait Type { } sealed trait DataType extends Type +object DataType { + case object Top extends DataType + case object Bottom extends DataType +} + case class ScalarType private (name: String) extends DataType { override def toString: String = name } @@ -137,19 +142,21 @@ object Type { lf.toSortedMap.toList.map(_._2), rf.toSortedMap.view.filterKeys(lf.keys.contains).toList.map(_._2) ) == -1.0 - ) -1.0 + ) 1.0 else if ( rf.keys.forall(lf.contains) && cmpTypesList( lf.toSortedMap.view.filterKeys(rf.keys.contains).toList.map(_._2), rf.toSortedMap.toList.map(_._2) ) == 1.0 - ) 1.0 + ) -1.0 else NaN private def cmp(l: Type, r: Type): Double = if (l == r) 0.0 else (l, r) match { + case (DataType.Top, _: DataType) | (_: DataType, DataType.Bottom) => 1.0 + case (DataType.Bottom, _: DataType) | (_: DataType, DataType.Top) => -1.0 case (x: ScalarType, y: ScalarType) => ScalarType.scalarOrder.partialCompare(x, y) case (LiteralType(xs, _), y: ScalarType) if xs == Set(y) => 0.0 case (LiteralType(xs, _), y: ScalarType) if xs(y) => -1.0 diff --git a/types/src/test/scala/aqua/types/TypeSpec.scala b/types/src/test/scala/aqua/types/TypeSpec.scala index f4d1a218..3c99d07c 100644 --- a/types/src/test/scala/aqua/types/TypeSpec.scala +++ b/types/src/test/scala/aqua/types/TypeSpec.scala @@ -37,6 +37,18 @@ class TypeSpec extends AnyFlatSpec with Matchers { accepts(f32, LiteralType.number) should be(true) } + "top type" should "accept anything" in { + accepts(DataType.Top, u64) should be(true) + accepts(DataType.Top, LiteralType.bool) should be(true) + accepts(DataType.Top, `*`(u64)) should be(true) + } + + "bottom type" should "be accepted by everything" in { + accepts(u64, DataType.Bottom) should be(true) + accepts(LiteralType.bool, DataType.Bottom) should be(true) + accepts(`*`(u64), DataType.Bottom) should be(true) + } + "arrays of scalars" should "be variant" in { (`[]`(u32): Type) <= u32 should be(false) (`[]`(u32): Type) >= u32 should be(false) @@ -55,8 +67,8 @@ class TypeSpec extends AnyFlatSpec with Matchers { val two: Type = ProductType("two", NonEmptyMap.of("field" -> u64, "other" -> string)) val three: Type = ProductType("three", NonEmptyMap.of("field" -> u32)) - one < two should be(true) - two > one should be(true) + accepts(one, two) should be(true) + accepts(two, one) should be(false) PartialOrder[Type].eqv(one, three) should be(true) }