add more TLA+ units, consider TLA+2

DistCompiler · Oct 28, 2024 · dce5aeb · dce5aeb
1 parent 2d19b56
commit dce5aeb
Show file tree

Hide file tree

Showing 5 changed files with 161 additions and 14 deletions.
diff --git a/tla/TLAParser.scala b/tla/TLAParser.scala
@@ -91,14 +91,23 @@ object TLAParser extends PassSeq:
       val addedTokens = List(
         tokens.Operator,
         tokens.Variable,
-        tokens.Constant
+        tokens.Constant,
+        tokens.Assumption,
+        tokens.Theorem,
+        tokens.Recursive,
+        tokens.Instance
       )
       val removedTokens = List(
         TLAReader.`_==_`,
         defns.VARIABLE,
         defns.VARIABLES,
         defns.CONSTANT,
-        defns.CONSTANTS
+        defns.CONSTANTS,
+        defns.ASSUME,
+        defns.AXIOM,
+        defns.ASSUMPTION,
+        defns.THEOREM,
+        defns.INSTANCE
       )
 
       tokens.Module ::= fields(
@@ -125,6 +134,10 @@ object TLAParser extends PassSeq:
       tokens.Variable.importFrom(tla.wellformed)
       tokens.Constant.importFrom(tla.wellformed)
       tokens.OpSym.importFrom(tla.wellformed)
+      tokens.Assumption ::= Atom
+      tokens.Theorem ::= Atom
+      tokens.Recursive.importFrom(tla.wellformed)
+      tokens.Instance ::= tokens.Id
 
     pass(once = true, strategy = pass.bottomUp)
       .rules:
@@ -270,3 +283,68 @@ object TLAParser extends PassSeq:
                 case alpha: Node =>
                   tokens.Constant(tokens.Id().like(alpha))
           )
+        // assume
+        | on(
+          tok(defns.ASSUME, defns.ASSUMPTION, defns.AXIOM)
+        ).rewrite: kw =>
+          splice(tokens.Assumption().like(kw))
+        // theorem
+        | on(
+          tok(defns.THEOREM)
+        ).rewrite: kw =>
+          splice(tokens.Theorem().like(kw))
+        // recursive
+        | on(
+          skip(tok(defns.RECURSIVE))
+            ~ field(
+              repeatedSepBy1(`,`):
+                opDeclPattern
+                  | tok(Alpha)
+            )
+            ~ trailing
+        ).rewrite: decls =>
+          splice(
+            decls.iterator
+              .map:
+                case (alpha, arity) if alpha.token == Alpha =>
+                  tokens.Recursive(
+                    tokens.Order2(
+                      tokens.Id().like(alpha),
+                      Node.Embed(arity)
+                    )
+                  )
+                case (op, arity) =>
+                  tokens.Recursive(
+                    tokens.Order2(
+                      op.unparent(),
+                      Node.Embed(arity)
+                    )
+                  )
+                case alpha: Node =>
+                  tokens.Recursive(tokens.Id().like(alpha))
+          )
+        // instance
+        | on(
+          skip(defns.INSTANCE)
+            ~ field(TLAReader.Alpha)
+            ~ trailing
+        ).rewrite: name =>
+          splice(tokens.Instance(tokens.Id().like(name)))
+
+  val liftLocals = passDef:
+    wellformed := prevWellformed.makeDerived:
+      tokens.Module.Defns.removeCases(defns.LOCAL)
+      tokens.Module.Defns.addCases(tokens.Local)
+      tokens.Local.importFrom(tla.wellformed)
+      TLAReader.groupTokens.foreach: tok =>
+        tok.removeCases(defns.LOCAL)
+        tok.addCases(tokens.Local)
+
+    pass(once = true, strategy = pass.bottomUp)
+      .rules:
+        on(
+          field(defns.LOCAL)
+            ~ field(tok(tokens.Operator, tokens.Instance))
+            ~ trailing
+        ).rewrite: (local, op) =>
+          splice(tokens.Local(op.unparent()).like(local))
diff --git a/tla/TLAParser.test.scala b/tla/TLAParser.test.scala
@@ -29,11 +29,12 @@ class TLAParserTests extends munit.FunSuite, test.WithTLACorpus:
       top /*, tracer = Manip.RewriteDebugTracer(os.pwd / "parser_passes")*/
     )
 
-    os.write.over(
-      os.pwd / "dbg_tla_parser" / s"${file.last}.dbg",
-      top.toPrettyWritable(TLAReader.wellformed),
-      createFolders = true
-    )
+    // re-enable if interesting:
+    // os.write.over(
+    //   os.pwd / "dbg_tla_parser" / s"${file.last}.dbg",
+    //   top.toPrettyWritable(TLAReader.wellformed),
+    //   createFolders = true
+    // )
 
     if top.hasErrors
     then fail(top.presentErrors(debug = true))

diff --git a/tla/TLAReader.test.scala b/tla/TLAReader.test.scala
@@ -23,11 +23,12 @@ class TLAReaderTests extends munit.FunSuite, test.WithTLACorpus:
     val src = Source.mapFromFile(file)
     val top = TLAReader(SourceRange.entire(src))
 
-    os.write.over(
-      os.pwd / "dbg_tla_reader" / s"${file.last}.dbg",
-      top.toPrettyWritable(TLAReader.wellformed),
-      createFolders = true
-    )
+    // re-enable if interesting:
+    // os.write.over(
+    //   os.pwd / "dbg_tla_reader" / s"${file.last}.dbg",
+    //   top.toPrettyWritable(TLAReader.wellformed),
+    //   createFolders = true
+    // )
 
     if top.hasErrors
     then fail(top.presentErrors(debug = true))

diff --git a/tla/defns.scala b/tla/defns.scala
@@ -47,6 +47,32 @@ object defns:
   case object ELSE extends ReservedWord
   case object CONSTANT extends ReservedWord
   case object CASE extends ReservedWord
+  case object COROLLARY extends ReservedWord
+  case object BY extends ReservedWord
+  case object HAVE extends ReservedWord
+  case object QED extends ReservedWord
+  case object TAKE extends ReservedWord
+  case object DEF extends ReservedWord
+  case object HIDE extends ReservedWord
+  case object RECURSIVE extends ReservedWord
+  case object USE extends ReservedWord
+  case object DEFINE extends ReservedWord
+  case object PROOF extends ReservedWord
+  case object WITNESS extends ReservedWord
+  case object PICK extends ReservedWord
+  case object DEFS extends ReservedWord
+  case object PROVE extends ReservedWord
+  case object SUFFICES extends ReservedWord
+  case object NEW extends ReservedWord
+  case object LAMBDA extends ReservedWord
+  case object STATE extends ReservedWord
+  case object ACTION extends ReservedWord
+  case object TEMPORAL extends ReservedWord
+  case object OBVIOUS extends ReservedWord
+  case object OMITTED extends ReservedWord
+  case object LEMMA extends ReservedWord
+  case object PROPOSITION extends ReservedWord
+  case object ONLY extends ReservedWord
 
   sealed trait Operator extends Token, HasSpelling
 

diff --git a/tla/package.scala b/tla/package.scala
@@ -105,11 +105,25 @@ object tokens:
   object Constant extends Token:
     override val lookedUpBy: Manip[Set[Node]] =
       on(
-        tok(Constant) *> children:
+        tok(Constant).withChildren:
           tok(Id).map(Set(_))
             | refine(Order2.lookedUpBy)
       ).value
 
+  object Local extends Token
+  object Recursive extends Token:
+    override val lookedUpBy: Manip[Set[Node]] =
+      on(
+        tok(Recursive).withChildren:
+          tok(Id).map(Set(_))
+            | refine(Order2.lookedUpBy)
+      ).value
+  object Assumption extends Token
+  object Theorem extends Token
+  object Instance extends Token:
+    object Substitutions extends Token
+    object Substitution extends Token
+
   object QuantifierBound extends Token:
     override val lookedUpBy: Manip[Set[Node]] =
       on(
@@ -136,12 +150,28 @@ val wellformed: Wellformed =
     Module.Extends ::= repeated(Id)
     Module.Defns ::= repeated(
       choice(
+        Local,
+        Recursive,
         Operator,
         Variable,
-        Constant
+        Constant,
+        Assumption,
+        Theorem,
+        Instance
       )
     )
 
+    Local ::= choice(
+      Operator,
+      Instance
+      // ModuleDefinition,
+    )
+
+    Recursive ::= choice(
+      Id,
+      Order2
+    )
+
     Id ::= Atom
     Ids ::= repeated(Id, minCount = 1)
     OpSym ::= choice(defns.Operator.instances.toSet)
@@ -293,6 +323,17 @@ val wellformed: Wellformed =
 
     Variable ::= Id
     Constant ::= choice(Id, Order2)
+    Assumption ::= Expr
+    Theorem ::= Expr
+    Instance ::= fields(
+      Id,
+      Instance.Substitutions
+    )
+    Instance.Substitutions ::= repeated(Instance.Substitution)
+    Instance.Substitution ::= fields(
+      choice(Id, OpSym),
+      Expr
+    )
 
     QuantifierBound ::= fields(
       choice(Id, Ids),