Skip to content

Commit

Permalink
more TLA+ units
Browse files Browse the repository at this point in the history
  • Loading branch information
@fhackett
fhackett committed Oct 30, 2024
1 parent 6e75743 commit 9e87397
Show file tree
Hide file tree
Showing 5 changed files with 158 additions and 15 deletions.
9 changes: 6 additions & 3 deletions Node.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -372,14 +372,17 @@ object Node:

val children: Node.Children

final def apply(tok: Token): Node =
final def apply(tok: Token, toks: Token*): Node =
val results = children.iterator
.collect:
case node: Node if node.token == tok =>
case node: Node if node.token == tok || toks.contains(node.token) =>
node
.toList

require(results.size == 1)
require(
results.size == 1,
s"token(s) not found ${(tok +: toks).map(_.name).mkString(", ")}"
)
results.head

final def firstChild: Option[Node.Child] =
Expand Down
3 changes: 3 additions & 0 deletions SeqPattern.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -265,6 +265,9 @@ object SeqPattern:
def children[T](using DebugInfo)(pattern: SeqPattern[T]): SeqPattern[T] =
refine(atFirstChild(pattern.asManip))

def onlyChild[T](using DebugInfo)(pattern: SeqPattern[T]): SeqPattern[T] =
refine(atFirstChild((field(pattern) ~ eof).asManip))

def parent[T](using DebugInfo)(pattern: SeqPattern[T]): SeqPattern[T] =
refine(atParent(on(pattern).value))

Expand Down
11 changes: 8 additions & 3 deletions Wellformed.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,11 @@ final class Wellformed private (
private lazy val tokenByShortName: Map[SourceRange, Token] =
shortNameByToken.map(_.reverse)

def shapeOf(tokenOrTop: Token | Node.Top.type): Shape =
tokenOrTop match
case token: Token => assigns(token)
case Node.Top => topShape

lazy val markErrorsPass: Manip[Unit] =
getNode.tapEffect(markErrors).void

Expand Down Expand Up @@ -182,7 +187,7 @@ final class Wellformed private (
else
node.replaceThis:
Builtin.Error(
s"found token ${node.token}, but expected ${choice.choices.mkString(" or ")}",
s"in $desc, found token ${node.token}, but expected ${choice.choices.mkString(" or ")}",
child.unparent()
)
done(())
Expand All @@ -192,7 +197,7 @@ final class Wellformed private (
else
embed.replaceThis:
Builtin.Error(
s"found embed ${embed.meta.canonicalName}, but expected ${choice.choices.mkString(" or ")}",
s"in $desc, found embed ${embed.meta.canonicalName}, but expected ${choice.choices.mkString(" or ")}",
embed.unparent()
)
done(())
Expand Down Expand Up @@ -220,7 +225,7 @@ final class Wellformed private (
else
node.replaceThis:
Builtin.Error(
s"found token ${node.token}, but expected ${choice.choices.mkString(" or ")}",
s"in $desc, found token ${node.token}, but expected ${choice.choices.mkString(" or ")}",
node.unparent()
)
done(())
Expand Down
135 changes: 128 additions & 7 deletions tla/TLAParser.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,8 @@ object TLAParser extends PassSeq:
case None => Nil
case Some(end) =>
val endIdx = end.idxInParent
m.unparentedChildren.view.drop(endIdx)
// .init to remove the EqSeq at end
m.unparentedChildren.view.drop(endIdx).init
splice(
tokens.Module(
tokens.Id().like(name),
Expand Down Expand Up @@ -290,7 +291,7 @@ object TLAParser extends PassSeq:
splice(tokens.Assumption().like(kw))
// theorem
| on(
tok(defns.THEOREM)
tok(defns.THEOREM, defns.PROPOSITION, defns.LEMMA, defns.COROLLARY)
).rewrite: kw =>
splice(tokens.Theorem().like(kw))
// recursive
Expand Down Expand Up @@ -331,20 +332,140 @@ object TLAParser extends PassSeq:
).rewrite: name =>
splice(tokens.Instance(tokens.Id().like(name)))

val liftLocals = passDef:
val joinCompoundUnits = passDef:
wellformed := prevWellformed.makeDerived:
tokens.Module.Defns.removeCases(defns.LOCAL)
tokens.Module.Defns.addCases(tokens.Local)
tokens.Module.Defns.addCases(tokens.Local, tokens.ModuleDefinition)
tokens.Local.importFrom(tla.wellformed)
TLAReader.groupTokens.foreach: tok =>
tok.removeCases(defns.LOCAL)
tok.addCases(tokens.Local)
tok.addCases(tokens.Local, tokens.ModuleDefinition)

tokens.ModuleDefinition ::= fields(
choice(tokens.Id, tokens.OpSym),
TLAReader.ParenthesesGroup,
tokens.Instance
)

pass(once = true, strategy = pass.bottomUp)
.rules:
// LOCAL <op>
on(
field(defns.LOCAL)
field(tok(defns.LOCAL) <* parent(tokens.Module.Defns))
~ field(tok(tokens.Operator, tokens.Instance))
~ trailing
).rewrite: (local, op) =>
splice(tokens.Local(op.unparent()).like(local))
spliceThen(tokens.Local(op.unparent()).like(local)):
// try again at this location; you might catch LOCAL op == INSTANCE ...
continuePass
// <op> == INSTANCE ...
| on(
field(
tok(tokens.Operator) <* children(
skip(anyNode)
~ skip(not(TLAReader.SqBracketsGroup))
~ trailing
)
)
~ field(tokens.Instance)
~ trailing
).rewrite: (op, instance) =>
splice(
tokens.ModuleDefinition(
op(tokens.Id, tokens.OpSym).unparent(),
op(TLAReader.ParenthesesGroup).unparent(),
instance.unparent()
)
)
// TODO: actually look for LOCAL <op> INSTANCE

// val consumeDefinitionContents = passDef:
// val delimiterSeq = Seq(
// tokens.Operator,
// tokens.Instance,
// tokens.Local,
// tokens.Recursive,
// tokens.Theorem,
// tokens.Assumption,
// tokens.Variable,
// tokens.Constant,
// tokens.ModuleDefinition,
// TLAReader.DashSeq,
// )
// wellformed := prevWellformed.makeDerived:
// tokens.Operator ::=! fields(
// choice(tokens.Id, tokens.OpSym),
// choice(TLAReader.ParenthesesGroup, TLAReader.SqBracketsGroup),
// tokens.Expr,
// )

// tokens.Expr ::= prevWellformed.shapeOf(TLAReader.ParenthesesGroup)
// tokens.Expr.removeCases(delimiterSeq*)
// TLAReader.groupTokens.foreach: tok =>
// tok.removeCases(delimiterSeq*)

// TLAReader.LetGroup ::=! tla.wellformed.shapeOf(tokens.Expr.Let.Defns)
// tokens.Module.Defns ::=! tla.wellformed.shapeOf(tokens.Module.Defns)
// tokens.Assumption ::=! tla.wellformed.shapeOf(tokens.Assumption)
// tokens.Theorem ::=! tla.wellformed.shapeOf(tokens.Theorem)
// tokens.Instance ::=! fields(
// tokens.Id,
// tokens.Instance.With,
// )
// tokens.Instance.With ::= repeated(choice(tokens.Expr.existingCases))

// val delimiters = tok(delimiterSeq*)

// pass(once = true, strategy = pass.bottomUp)
// .rules:
// val restChildren = field(repeated(anyChild <* not(delimiters)))
// on(
// TLAReader.DashSeq // delete all ----
// ).rewrite: _ =>
// splice()
// | on(
// fields(
// (tok(tokens.Local), onlyChild(tokens.Operator)).tupled
// | (tok(tokens.Operator) <* not(parent(tokens.Local))).map(op => (op, op))
// )
// ~ restChildren
// ~ trailing
// ).rewrite: (owner, op, contents) =>
// op.children += tokens.Expr(contents.iterator.map(_.unparent()))
// splice(owner)
// | on(
// field(tokens.Theorem)
// ~ restChildren
// ~ trailing
// ).rewrite: (thm, contents) =>
// thm.children += tokens.Expr(contents.iterator.map(_.unparent()))
// splice(thm)
// | on(
// field(tokens.Assumption)
// ~ restChildren
// ~ trailing
// ).rewrite: (assm, contents) =>
// assm.children += tokens.Expr(contents.iterator.map(_.unparent()))
// splice(assm)
// | on(
// fields(
// (tok(tokens.Instance) <* not(parent(tokens.ModuleDefinition))).map(inst => (inst, inst))
// | tok(tokens.ModuleDefinition).product(children(
// skip(tok(tokens.Id, tokens.OpSym))
// ~ skip(TLAReader.ParenthesesGroup)
// ~ field(tokens.Instance)
// ~ eof
// ))
// )
// ~ field(optional(
// skip(defns.WITH)
// ~ restChildren
// ~ trailing
// ))
// ~ trailing
// ).rewrite: (parent, inst, contentsOpt) =>
// // TODO: actually handle WITH structure (multiple bindings), maybe in another pass
// inst.children += tokens.Instance.With(
// contentsOpt.getOrElse(Nil).iterator.map(_.unparent())
// )
// splice(parent)
15 changes: 13 additions & 2 deletions tla/package.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,8 @@ val wellformed: Wellformed =
t.Constant,
t.Assumption,
t.Theorem,
t.Instance
t.Instance,
t.ModuleDefinition
)
)

Expand All @@ -147,6 +148,12 @@ val wellformed: Wellformed =
t.Order2
)

t.ModuleDefinition ::= fields(
t.Id,
t.Operator.Params,
t.Instance
)

t.Id ::= Atom
t.Ids ::= repeated(t.Id, minCount = 1)
t.OpSym ::= choice(defns.Operator.instances.toSet)
Expand Down Expand Up @@ -228,7 +235,11 @@ val wellformed: Wellformed =
t.Expr
)
t.Expr.Let.Defns ::= repeated(
t.Operator,
choice(
t.Operator,
t.ModuleDefinition,
t.Recursive
),
minCount = 1
)

Expand Down

0 comments on commit 9e87397

Please sign in to comment.