Documentation

Desugarer.TLAPlus

source
def SurfaceTLAPlus.PrefixOperator.canonicalName :
PrefixOperator → String

The canonical (single-spelling) name a builtin prefix operator becomes as a CoreTLAPlus.Expression.var, reachable via opCall.

Equations
Instances For
    source
    def SurfaceTLAPlus.PostfixOperator.canonicalName :
    PostfixOperator → String

    The canonical name a builtin postfix operator becomes.

    Equations
    Instances For
      source
      def SurfaceTLAPlus.InfixOperator.canonicalName :
      InfixOperator → String

      The canonical name a builtin infix operator becomes (collapsing every alternative spelling — e.g. <=/=</\leq — to one).

      Equations
      Instances For
        source
        def SurfaceTLAPlus.cartesianProduct :
        InfixOperator

        Cartesian product, used to collapse a multi-binder function literal/set-map into a single fresh tuple binder (see flattenBound/collapseToSingleBinder below). Reused by Desugarer/PlusCal.lean for multicast's own filter collapse, which builds the same product out of the filter's components.

        Equations
        Instances For
          source
          partial def SurfaceTLAPlus.CoreTLAPlus.Expression.subst {α : Type} (x : String) (e target : CoreTLAPlus.Expression α) :
          CoreTLAPlus.Expression α

          Substitute every free occurrence of CoreTLAPlus.Expression.var x with e, stopping at any binder that rebinds x. Used to reconstruct tuple-pattern/multi-binder variables as projections off a single fresh binder (flattenBound, collapseToSingleBinder).

          Substitution rebuilds every node on the path it walks, so each rebuilt node is re-registered (match_source/@@) at the span the original carried. Skipping that would leave a whole subtree of the desugared body positionless, and posOf answers for an unregistered node with an unrelated node's span rather than failing (Common/Position.lean).

          source
          def SurfaceTLAPlus.tupleProj {α : Type} (pos : SourceSpan) (z : String) (i : ℕ) :
          CoreTLAPlus.Expression α

          The z[i] (1-based, TLA⁺-style) tuple projection — a single index, so no <<…>> wrapping (wrapIndices below) is needed. Registered at pos, the span of the tuple-pattern binder this projection was synthesized to replace. Reused by Desugarer/PlusCal.lean, which rewrites a collapsed multicast filter's component names the same way.

          Equations
          Instances For
            source
            def SurfaceTLAPlus.wrapIndices {α : Type} (pos : SourceSpan) :
            List (CoreTLAPlus.Expression α) → CoreTLAPlus.Expression α

            f[e₁, …, eₙ]'s/![e₁, …, eₙ]'s indices, collapsed to the single CoreTLAPlus.Expression fnCall/except take: a lone index (n = 1) stays exactly that, f[e]; more than one becomes the tuple f[<<e₁, …, eₙ>>]. es is always non-empty by construction of the parser. Reused by Desugarer/PlusCal.lean for SurfacePlusCal.Ref's own indices.

            Equations
            Instances For
              source
              def SurfaceTLAPlus.flattenBound {α : Type} [Inhabited α] {m : Type → Type} [MonadDesugarerExpr α m] [Monad m] (pos : SourceSpan) (qb : QuantifierBound α (CoreTLAPlus.Expression α)) (body : CoreTLAPlus.Expression α) :
              m (List (String × α × CoreTLAPlus.Expression α) × CoreTLAPlus.Expression α)

              Flatten one already-desugared QuantifierBound into a list of single-variable (name, annotation, domain) bindings, plus how body needs rewriting to still make sense in terms of those flattened names:

              • .var ann x dom is already single-variable: one binding, no rewriting.
              • .vars [(ann₁,x),(ann₂,y),…] dom (\A x, y ∈ S : …) shares one domain across several names: expands to one binding per name, no rewriting.
              • .varTuple [(ann₁,x),(ann₂,y),…] dom (\A ⟨x,y⟩ ∈ S : …) is a tuple pattern: collapses to one fresh binding over dom, rewriting body to substitute each x/y with the corresponding projection out of the fresh variable.
              Equations
              Instances For
                source
                def SurfaceTLAPlus.collapseToSingleBinder {α : Type} [Inhabited α] {m : Type → Type} [MonadDesugarerExpr α m] [Monad m] (pos : SourceSpan) (bindings : List (String × α × CoreTLAPlus.Expression α)) (body : CoreTLAPlus.Expression α) :
                m (String × α × CoreTLAPlus.Expression α × CoreTLAPlus.Expression α)

                Collapse a list of already-flattened single-variable bindings into exactly one, as required by CoreTLAPlus's single-binder function literals/set-maps. A single binding needs no change; multiple bindings x ∈ A, y ∈ B, … collapse to one fresh variable over the Cartesian product A × B × …, rewriting body to project each original name back out. Not the same transformation as \A x, y : P's sequential nesting (nestQuantifier below): [x ∈ A, y ∈ B ↦ e] denotes one function over pairs, not a function of functions.

                Equations
                Instances For
                  source
                  def SurfaceTLAPlus.nestQuantifier {α : Type} (pos : SourceSpan) (mk : String → α → Option (CoreTLAPlus.Expression α) → CoreTLAPlus.Expression α → CoreTLAPlus.Expression α) (bindings : List (String × α × CoreTLAPlus.Expression α)) (body : CoreTLAPlus.Expression α) :
                  CoreTLAPlus.Expression α

                  Sequentially nest a list of (name, annotation, domain) bindings into repeated single-variable quantification: x ∈ A, y ∈ B becomes ∫ x ∈ A : ∫ y ∈ B : body (a true nesting, unlike collapseToSingleBinder's product collapse).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    partial def SurfaceTLAPlus.Expression.desugar {α : Type} [Inhabited α] {m : Type → Type} [MonadDesugarerExpr α m] [Monad m] (e : Expression α) :
                    m (CoreTLAPlus.Expression α)
                    source
                    def SurfaceTLAPlus.Declaration.desugar {α : Type} [Inhabited α] {m : Type → Type} [MonadDesugarerExpr α m] [Monad m] :
                    Declaration α → m (CoreTLAPlus.Declaration α)
                    Equations
                    Instances For
                      source
                      def SurfaceTLAPlus.Module.desugar {α : Type} [Inhabited α] {m : Type → Type} [MonadDesugarerExpr α m] [Monad m] (mod : Module (SurfacePlusCal.Algorithm α (Expression α)) α) :
                      m (CoreTLAPlus.Module (SurfacePlusCal.Algorithm α (CoreTLAPlus.Expression α)) α)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def SurfaceTLAPlus.Module.runDesugarer {α : Type} [Inhabited α] {n : Type → Type} [Monad n] [MonadFresh n] (mod : Module (SurfacePlusCal.Algorithm α (Expression α)) α) :
                        DiagT DesugarWarning DesugarError n (CoreTLAPlus.Module (SurfacePlusCal.Algorithm α (CoreTLAPlus.Expression α)) α)

                        Run expression desugaring against the concrete monad it needs: @'s Reader context, fresh-name generation, and MonadDiagnostic's error reporting/warning accumulation (instantiated at DiagT, so a warning survives a later fatal error). No expression-level rule actually emits a DesugarWarning yet, but the concrete stack stays uniform with Desugarer/PlusCal.lean's statement-level runDesugarer. The base monad n stays abstract, constrained only to supply the fresh-name counter (MonadStateOf Nat, which Common/Fresh.lean's MonadFresh instance reads): the counter belongs to one compile, so the driver owns it (Driver/Modules.lean's DriverState) rather than this pass pinning a base monad that can reach a process-wide one.

                        Equations
                        Instances For
                          source
                          def extractType {m : Type → Type} [Monad m] [MonadDiagnostic DesugarWarning DesugarError m] (anns : List Annotation) :
                          m (Option SurfaceTLAPlus.Typ)

                          Validate an annotation slot known to be @type-only: must contain only @type, and at most one, then is replaced by the Typ it names. Shared between the TLA⁺ half below (stripTLAPlusAnnotations) and Desugarer/PlusCal.lean's equivalent check.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def CoreTLAPlus.Module.stripTLAPlusAnnotations {γ : Type} (mod : Module γ (List Annotation)) :
                            DiagT DesugarWarning DesugarError Id (Module γ (Option SurfaceTLAPlus.Typ))

                            Validate every List Annotation slot reachable from a module's own declarations/expressions — excluding the embedded PlusCal algorithm, which Desugarer/PlusCal.lean's SurfacePlusCal.Algorithm.desugar covers separately — must contain only @type, and at most one (extractType above), and is replaced by the Option Typ it names. Runs after Module.desugar/runDesugarer, since this check is only meaningful once α is concretely List Annotation.

                            DiagT … Id rather than a bare Except, so every diagnostics-producing entry point in the compiler reports through the same MonadDiagnostic shape — the caller absorbs it with DiagT.lift, exactly as it already does for parseModule and runDesugarer. This check emits no warnings today; the List DesugarWarning it pairs against its result is simply always [].

                            Equations
                            Instances For