apalache-mc · konnov · Jul 18, 2022 · Jul 12, 2022 · Jul 12, 2022 · Jul 12, 2022
diff --git a/.unreleased/features/1843.md b/.unreleased/features/1843.md
@@ -0,0 +1 @@
+introduce new syntax for type aliases, see #1977
diff --git a/test/tla/ChangRobertsTyped_Test.tla b/test/tla/ChangRobertsTyped_Test.tla
@@ -128,9 +128,9 @@ TestExec_n0_n1 ==
 \* We expect no winner in the final state.
 \* Note that Assert_noWinner is a predicate over a trace of states.
 \*
-\* @typeAlias: STATE = [ msgs: Int -> Set(Int), pc: Int -> Str,
+\* @typeAlias: state = [ msgs: Int -> Set(Int), pc: Int -> Str,
 \*                       initiator: Int -> Bool, state: Int -> Str ];
-\* @type: Seq(STATE) => Bool;
+\* @type: Seq($state) => Bool;
 Assert_noWinner(trace) ==
     LET last == trace[Len(trace)] IN
         \A n \in Node:

diff --git a/test/tla/MC3_TwoPhaseTyped.tla b/test/tla/MC3_TwoPhaseTyped.tla
@@ -10,7 +10,7 @@ VARIABLES
   \* @type: Set(RM);
   tmPrepared,    \* The set of RMs from which the TM has received $"Prepared"$
                  \* messages.
-  \* @type: Set(MESSAGE);
+  \* @type: Set($message);
   msgs
 
 INSTANCE TwoPhaseTyped

diff --git a/test/tla/MissionariesAndCannibalsTyped.tla b/test/tla/MissionariesAndCannibalsTyped.tla
@@ -34,16 +34,16 @@ EXTENDS Integers, FiniteSets
 (* instantiated.                                                           *)
 (***************************************************************************)
 
-\* @typeAlias: PERSONS = Set(PERSON);
+\* @typeAlias: persons = Set(PERSON);
 MCTypeAliases == TRUE
 
 (***************************************************************************)
 (* Next comes the declaration of the sets of missionaries and cannibals.   *)
 (***************************************************************************)
 CONSTANTS
-    \* @type: PERSONS;
+    \* @type: $persons;
     Missionaries,
-    \* @type: PERSONS;
+    \* @type: $persons;
     Cannibals 
 
 (***************************************************************************)
@@ -85,7 +85,7 @@ CONSTANTS
 VARIABLES
     \* @type: Str;
     bank_of_boat,
-    \* @type: Str -> PERSONS;
+    \* @type: Str -> $persons;
     who_is_on_bank 
 
 (***************************************************************************)
@@ -184,7 +184,7 @@ OtherBank(b) == IF b = "E" THEN "W" ELSE "E"
 (* of the two variables (their values in state t) in terms of their old    *)
 (* values (their values in state s).                                       *)
 (***************************************************************************)
-\* @type: (PERSONS, Str) => Bool;
+\* @type: ($persons, Str) => Bool;
 Move(S,b) ==
              /\ Cardinality(S) \in {1,2}
              /\ LET newThisBank  == who_is_on_bank[b] \ S

diff --git a/test/tla/TestAliasNew.tla b/test/tla/TestAliasNew.tla
@@ -0,0 +1,8 @@
+------------------------- MODULE TestAliasNew ---------------------------------
+\* Syntax for type aliases in Type System 1.2.
+\*
+\* @typeAlias: newAlias = UNINTERPRETED_TYPE;
+\* @type: $newAlias => Set($newAlias);
+Foo(x) == { x }
+
+===============================================================================
diff --git a/test/tla/TestAliasNewMissing.tla b/test/tla/TestAliasNewMissing.tla
@@ -0,0 +1,9 @@
+--------------------- MODULE TestAliasNewMissing ------------------------------
+\* Syntax for type aliases in Type System 1.2.
+\*
+\* Here we are missing a type alias, and the type checker should complain.
+\*
+\* @type: $newAlias => Set($newAlias);
+Foo(x) == { x }
+
+===============================================================================
diff --git a/test/tla/TestAliasOld.tla b/test/tla/TestAliasOld.tla
@@ -0,0 +1,8 @@
+-------------------------- MODULE TestAliasOld --------------------------------
+\* This is the old syntax for type aliases.
+\* It should still work for some time, but you should get a warning.
+\*
+\* @typeAlias: OLD_ALIAS = UNINTERPRETED_TYPE;
+TestAlias_aliases == TRUE
+
+===============================================================================
diff --git a/test/tla/TestAnnotations.tla b/test/tla/TestAnnotations.tla
@@ -4,11 +4,11 @@
 VARIABLES
     \* See issue #718
     \*
-    \* @typeAlias: ELEM =
+    \* @typeAlias: elem =
     \*             Int;
     \* @type:
     \*   Set(
-    \*        ELEM
+    \*        $elem
     \*      );
     \*
     \* See issue #757

diff --git a/test/tla/TwoPhaseTyped.tla b/test/tla/TwoPhaseTyped.tla
@@ -10,13 +10,13 @@
 EXTENDS Integers, FiniteSets, Variants, TwoPhaseTyped_typedefs
 
 \* ANCHOR: constructors
-\* @type: MESSAGE;
+\* @type: $message;
 MkCommit == Variant("Commit", "0_OF_NIL")
 
-\* @type: MESSAGE;
+\* @type: $message;
 MkAbort == Variant("Abort", "0_OF_NIL")
 
-\* @type: RM => MESSAGE;
+\* @type: RM => $message;
 MkPrepared(rm) == Variant("Prepared", rm)
 \* ANCHOR_END: constructors
 
@@ -37,11 +37,11 @@ VARIABLES
                  \* messages.
 \* ANCHOR_END: vars1
 \* ANCHOR: vars2
-  \* @type: Set(MESSAGE);
+  \* @type: Set($message);
   msgs
 \* ANCHOR_END: vars2
 
-\* @type: Set(MESSAGE);
+\* @type: Set($message);
 Message ==
   { MkPrepared(rm): rm \in RM }
     \union

diff --git a/test/tla/TwoPhaseTyped_typedefs.tla b/test/tla/TwoPhaseTyped_typedefs.tla
@@ -1,6 +1,6 @@
 ----------------------- MODULE TwoPhaseTyped_typedefs ----------------
 (*
- @typeAlias: MESSAGE = Commit(NIL) | Abort(NIL) | Prepared(RM);
+ @typeAlias: message = Commit(NIL) | Abort(NIL) | Prepared(RM);
  *)
 TwoPhaseTyped_aliases == TRUE
 

diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
@@ -3109,9 +3109,38 @@ $ apalache-mc typecheck --features=rows TestReqAckVariants.tla | sed 's/[IEW]@.*
 EXITCODE: OK
 ```
 
+### typecheck TestAliasOld.tla
+
+```sh
+$ apalache-mc typecheck TestAliasOld.tla | sed 's/[IEW]@.*//'
+...
+Operator TestAlias_aliases: Deprecated syntax in type alias OLD_ALIAS. Use camelCase of Type System 1.2.
+...
+EXITCODE: OK
+```
+
+### typecheck TestAliasNew.tla
+
+```sh
+$ apalache-mc typecheck TestAliasNew.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: OK
+```
+
+### typecheck TestAliasNewMissing.tla
+
+```sh
+$ apalache-mc typecheck TestAliasNewMissing.tla | sed 's/[IEW]@.*//'
+...
+Typing input error: Missing @typeAlias: newAlias = <type>;
+...
+EXITCODE: ERROR (255)
+```
+
 ## configuring the output manager
 
 ### output manager: set out-dir by CLI flag
+
 If we run with the `--out-dir` flag
 
 ```sh

diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/DefaultType1Parser.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/DefaultType1Parser.scala
@@ -23,6 +23,10 @@ import scala.util.parsing.input.NoPosition
 object DefaultType1Parser extends Parsers with Type1Parser {
   override type Elem = Type1Token
 
+  // This pattern recognizes camelCase and lowercase:
+  // https://stackoverflow.com/questions/23936280/matching-camelcase-to-a-regular-expression-in-java
+  private val camelCasePattern = "^[a-z]+(?:[A-Z][a-z]*)*$".r
+
   /**
    * Parse a type from a string, possibly substituting aliases with types.
    *
@@ -64,7 +68,7 @@ object DefaultType1Parser extends Parsers with Type1Parser {
   private def closedTypeExpr: Parser[TlaType1] = phrase(typeExpr) ^^ (e => e)
 
   private def aliasExpr: Parser[(String, TlaType1)] = {
-    (typeConst ~ EQ() ~ typeExpr) ^^ { case ConstT1(name) ~ _ ~ tt =>
+    (oldOrNewAlias ~ EQ() ~ typeExpr) ^^ { case ConstT1(name) ~ _ ~ tt =>
       (name, tt)
     }
   }
@@ -80,6 +84,7 @@ object DefaultType1Parser extends Parsers with Type1Parser {
       | record | recordFromRow
       | variant | variantVar
       | typeVar | typeConst
+      | aliasReference
       | parenExpr) ^^ {
       case INT()        => IntT1
       case REAL()       => RealT1
@@ -259,6 +264,11 @@ object DefaultType1Parser extends Parsers with Type1Parser {
     }
   }
 
+  // a reference to an alias
+  private def aliasReference: Parser[TlaType1] = {
+    DOLLAR() ~> newAlias
+  }
+
   // A record field name, like foo_BAR2.
   // As field name are colliding with CAPS_IDENT and TYPE_VAR, we expect all of them.
   private def fieldName: Parser[IDENT] = {
@@ -285,6 +295,22 @@ object DefaultType1Parser extends Parsers with Type1Parser {
 
   // a type constant or an alias name, e.g., BAZ
   private def typeConst: Parser[ConstT1] = {
-    acceptMatch("type constant", { case IDENT(name) if (name.toUpperCase() == name) => ConstT1(name) })
+    acceptMatch("type constant", { case IDENT(name) if name.toUpperCase() == name => ConstT1(name) })
+  }
+
+  // old ALIAS_SYNTAX, or newSyntaxInCamelCase
+  private def oldOrNewAlias: Parser[ConstT1] = {
+    acceptMatch("alias name",
+        {
+          case IDENT(name) if name.toUpperCase() == name =>
+            ConstT1(name)
+
+          case IDENT(name) if camelCasePattern.matches(name) =>
+            ConstT1("$" + name)
+        })
+  }
+
+  private def newAlias: Parser[ConstT1] = {
+    acceptMatch("type constant", { case IDENT(name) if camelCasePattern.matches(name) => ConstT1("$" + name) })
   }
 }
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/Type1Lexer.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/Type1Lexer.scala
@@ -1,7 +1,6 @@
 package at.forsyte.apalache.io.typecheck.parser
 
 import java.io.Reader
-
 import scala.util.matching.Regex
 import scala.util.parsing.combinator.RegexParsers
 
@@ -38,7 +37,7 @@ private[parser] object Type1Lexer extends RegexParsers {
         int | real | bool | str | set | seq | rec | variant | identifier | fieldNumber | stringLiteral |
           rightArrow | doubleRightArrow | eq | leftRow | rightRow | leftTupleRow | rightTupleRow |
           leftParen | rightParen | pipe | leftBracket | rightBracket |
-          leftCurly | rightCurly | doubleLeftAngle | doubleRightAngle | comma | colon
+          leftCurly | rightCurly | doubleLeftAngle | doubleRightAngle | comma | colon | dollar
     ) ///
 
   // it is important that linefeed is not in whiteSpace, as otherwise singleComment consumes the whole input!
@@ -163,4 +162,8 @@ private[parser] object Type1Lexer extends RegexParsers {
   private def colon: Parser[COLON] = {
     ":".r ^^ { _ => COLON() }
   }
+
+  private def dollar: Parser[DOLLAR] = {
+    "\\$".r ^^ { _ => DOLLAR() }
+  }
 }
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/tokens.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/typecheck/parser/tokens.scala
@@ -109,6 +109,13 @@ private[parser] case class COLON() extends Type1Token {
   override def toString: String = ":"
 }
 
+/**
+ * The dollar sign.
+ */
+private[parser] case class DOLLAR() extends Type1Token {
+  override def toString: String = "$"
+}
+
 /**
  * Left parenthesis "(".
  */

diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/TypeCheckerTool.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/TypeCheckerTool.scala
@@ -2,13 +2,12 @@ package at.forsyte.apalache.tla.typecheck
 
 import at.forsyte.apalache.io.annotations.store.AnnotationStore
 import at.forsyte.apalache.io.annotations.{AnnotationStr, StandardAnnotations}
-import at.forsyte.apalache.io.typecheck.parser.Type1ParseError
+import at.forsyte.apalache.io.typecheck.parser.{DefaultType1Parser, Type1ParseError}
 import at.forsyte.apalache.tla.lir
-import at.forsyte.apalache.tla.lir.transformations.TransformationTracker
 import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.lir.transformations.TransformationTracker
 import at.forsyte.apalache.tla.typecheck.etc._
 import at.forsyte.apalache.tla.typecheck.integration.{RecordingTypeCheckerListener, TypeRewriter}
-import at.forsyte.apalache.io.typecheck.parser.DefaultType1Parser
 import com.typesafe.scalalogging.LazyLogging
 
 /**
@@ -87,7 +86,7 @@ class TypeCheckerTool(annotationStore: AnnotationStore, inferPoly: Boolean, useR
     }
   }
 
-  private def loadTypeAliases(declarations: Seq[TlaDecl]): ConstSubstitution = {
+  private def loadTypeAliases(declarations: Seq[TlaDecl]): TypeAliasSubstitution = {
     var aliases = Map[String, lir.TlaType1]()
 
     // extract all aliases from the annotations
@@ -96,7 +95,13 @@ class TypeCheckerTool(annotationStore: AnnotationStore, inferPoly: Boolean, useR
         annotations.filter(_.name == StandardAnnotations.TYPE_ALIAS).foreach { annot =>
           annot.args match {
             case Seq(AnnotationStr(text)) =>
-              aliases += parseTypeAlias(decl.name, text)
+              val (alias, assignedType) = parseTypeAlias(decl.name, text)
+              if (!ConstT1.isAliasReference(alias)) {
+                val msg =
+                  s"Operator ${decl.name}: Deprecated syntax in type alias $alias. Use camelCase of Type System 1.2."
+                logger.warn(msg)
+              }
+              aliases += alias -> assignedType
 
             case args =>
               throw new TypingInputException(
@@ -107,7 +112,7 @@ class TypeCheckerTool(annotationStore: AnnotationStore, inferPoly: Boolean, useR
     }
 
     // Aliases can refer to one another. Substitute the aliases until we arrive at a fixpoint.
-    ConstSubstitution(aliases).closure()
+    TypeAliasSubstitution(aliases).closure()
   }
 
   // parse type from its text representation

diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
@@ -23,7 +23,7 @@ import scala.annotation.nowarn
  */
 class ToEtcExpr(
     annotationStore: AnnotationStore,
-    aliasSubstitution: ConstSubstitution,
+    aliasSubstitution: TypeAliasSubstitution,
     varPool: TypeVarPool,
     val useRows: Boolean = false)
     extends EtcBuilder with LazyLogging {
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		introduce new syntax for type aliases, see #1977