Documentation

Network2Go.Expression

Compiling TLA⁺ expressions into Go expressions.

The output is a single Go.Expression, never a statement prelude: everything that needs statements to express — the quantifiers' search loops, IF/CASE's laziness, EXCEPT's record update — is wrapped in an immediately-applied Go.Expression.funcLit. That keeps this function callable from any expression position (a branch's guard, an argument, another expression's sub-term) without every caller having to thread a list of statements to emit first. funcLit exists in Core.Go.Syntax precisely because these forms cannot be compiled without it.

Recurring conventions, all forced by the runtime library's own types:

Deliberately not handled here, since they are not expression forms: operator and function definitions (including MkRecFn for recursive ones), which live in Network2Go.Definition, and the renaming of user-chosen names that collide after capitalization.

source
def Network2Go.goBool :
ComputableGo.Expression → ComputableGo.Expression

bool(e) — Go's conversion out of the runtime's Bool, needed wherever a real bool is required: an if condition, and every predicate the runtime library takes.

Cancels against tlaBool rather than nesting inside it. The two meet constantly — every runtime predicate answers in Go's bool, gets wrapped so that the TLA⁺ expression has a TLA⁺ type, and is then unwrapped again by whatever consumes it as a condition — and bool(tlaplus.Bool(e)) is merely e, so a compiled guard reads as one comparison instead of three nested calls.

Equations
Instances For
    source
    partial def Network2Go.compileExpr {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (e : ComputablePlusCal.Expression) :
    m ComputableGo.Expression

    Compiles a checked TLA⁺ expression into the Go expression that computes it.

    source
    partial def Network2Go.compilePredicate {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (x : String) (τ : ComputableTLAPlus.Typ) (body : ComputablePlusCal.Expression) :
    m ComputableGo.Expression

    func(x τ) bool { return bool(P) } — the callback shape every runtime set operation takes. SetFilter/Choose are declared over a Go bool predicate rather than a tlaplus.Bool one, so the body converts.

    source
    partial def Network2Go.compileQuantifier {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (isForall : Bool) (x : String) (τ : ComputableTLAPlus.Typ) (dom body : ComputablePlusCal.Expression) :
    m ComputableGo.Expression

    \A x \in S : P and \E x \in S : P: delegates the search of S for the first counterexample/witness to the runtime, the two quantifiers sharing one implementation (SetForall/SetExists) the same way compilePredicate's callback shape is shared by every other set operation here (SetFilter, Choose, SetMap, …). S's domain expression is evaluated exactly once either way, since it is passed as an argument rather than inlined.

    source
    partial def Network2Go.compileExcept {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (pos : SourceSpan) (τ : ComputableTLAPlus.Typ) (base : ComputableGo.Expression) (path : List (String ⊕ ComputablePlusCal.Expression)) (rhs : ComputablePlusCal.Expression) :
    m ComputableGo.Expression

    One ![e] = v / !.x = v override of an EXCEPT, following the path down and rebuilding on the way back up. τ is the type of what base computes.

    A function override is FnOverload, which keeps the fresh map header Insert returns so that the override stays scoped to the overloaded copy. Records and tuples have no such helper — Go has no functional update for a struct — so they go through a literal taking the struct by value: the parameter is already a copy, so assigning into it cannot reach the original.

    source
    partial def Network2Go.compileStructUpdate {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (pos : SourceSpan) (τ : ComputableTLAPlus.Typ) (field : String) (fieldτ : ComputableTLAPlus.Typ) (base : ComputableGo.Expression) (rest : List (String ⊕ ComputablePlusCal.Expression)) (rhs : ComputablePlusCal.Expression) :
    m ComputableGo.Expression

    func(r T) T { r.X = …; return r }(base) — the struct update shared by record and tuple overrides. Taking r by value is the whole trick: Go copies a struct argument, so the assignment cannot be seen by whoever still holds base.

    source
    def Network2Go.compileIntrinsic {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (pos : SourceSpan) (name : String) (τ : ComputableTLAPlus.Typ) (args : List ComputableGo.Expression) :
    m ComputableGo.Expression

    A builtin operator, applied. τ is the operator's own type, already specialized by the checker, which is where the operand type = dispatches on comes from.

    Every case producing a truth value converts back into tlaplus.Bool: the runtime's predicates answer in Go's bool, but a TLA⁺ expression of type Bool must be one of the newtypes, since everything in a specification has to satisfy Eq/Ord.

    Equations
    Instances For
      source
      def Network2Go.compileBuiltinVar {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (pos : SourceSpan) (mod name : String) (τ : ComputableTLAPlus.Typ) :
      m ComputableGo.Expression

      A reference to a builtin operator that carries no arguments — a value exported by a standard module, not something to apply.

      Equations
      Instances For
        source
        def Network2Go.compileBuiltinCall {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (pos : SourceSpan) (mod name : String) (τ : ComputableTLAPlus.Typ) (args : List ComputableGo.Expression) :
        m ComputableGo.Expression

        A builtin operator from a standard module, applied. Naturals's comparisons all go through tlaplus.IntOrd — Lt is one of the dictionary's two primitive fields, Gt/Le/Ge are methods the runtime derives from it once. Arithmetic is not a comparison and takes no dictionary.

        Instances For
          source
          def Network2Go.compileExprTop {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (e : ComputablePlusCal.Expression) (outer : List String := []) :
          m ComputableGo.Expression

          compileExpr for a term straight from an earlier pass — its binders' bodies still carry de Bruijn .bound indices. outer names any binders enclosing e that are not nodes within it: an operator's or function's parameters, or a multicast filter's recipient, in source order. Every caller outside this file goes through here so that compileExpr itself only ever meets .free occurrences.

          Equations
          Instances For
            source
            def Network2Go.compileExceptTop {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] [MonadFresh m] (pos : SourceSpan) (τ : ComputableTLAPlus.Typ) (base : ComputableGo.Expression) (path : List (String ⊕ ComputablePlusCal.Expression)) (rhs : ComputablePlusCal.Expression) :
            m ComputableGo.Expression

            compileExcept for a path and right-hand side straight from an earlier pass — opens every de Bruijn index in the index expressions and the right-hand side against its binder hint first.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For