ElaboratedPlusCal pinned at Typed2Computable's output rather than the type checker's — the same Statement/Block/Branches/Ref/Declarations/Process/Algorithm layer TypedPlusCal pins, but at ComputableTLAPlus's types. See Core/TypedPlusCal/Syntax.lean's module doc for why this pass needs no separate monomorphic copy.

@[reducible, inline]

abbrev ComputablePlusCal.Expression : Type

Computable PlusCal expressions — always ComputableTLAPlus.Expression at ComputableTLAPlus.Typ.

Equations

• ComputablePlusCal.Expression = ComputableTLAPlus.Expression ComputableTLAPlus.Typ

@[reducible, inline]

abbrev ComputablePlusCal.Ref : Type

Equations

• ComputablePlusCal.Ref = ElaboratedPlusCal.Ref ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputablePlusCal.Multicast : Type

Equations

• ComputablePlusCal.Multicast = ElaboratedPlusCal.Multicast ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputablePlusCal.Statement : Bool → Type

Equations

• ComputablePlusCal.Statement = ElaboratedPlusCal.Statement ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputablePlusCal.Block : Bool → Type

Equations

• ComputablePlusCal.Block = ElaboratedPlusCal.Block ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputablePlusCal.Branches : Bool → Type

Equations

• ComputablePlusCal.Branches = ElaboratedPlusCal.Branches ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputablePlusCal.Declarations : Type

Equations

• ComputablePlusCal.Declarations = ElaboratedPlusCal.Declarations ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputablePlusCal.Process : Type

Equations

• ComputablePlusCal.Process = ElaboratedPlusCal.Process ComputableTLAPlus.Typ ComputablePlusCal.Expression

@[reducible, inline]

abbrev ComputablePlusCal.Algorithm : Type

Equations

• ComputablePlusCal.Algorithm = ElaboratedPlusCal.Algorithm ComputableTLAPlus.Typ ComputablePlusCal.Expression

def ComputablePlusCal.Ref.stepType (τ : ComputableTLAPlus.Typ) : String ⊕ Expression → ComputableTLAPlus.Typ

Advances a reference's type by one path step: a field name projects a record, an index expression enters a function, sequence or tuple.

Equations

• ComputablePlusCal.Ref.stepType (SurfaceTLAPlus.Typ.record fs) (Sum.inl field) = (List.lookup field fs).getD (SurfaceTLAPlus.Typ.record fs)
• ComputablePlusCal.Ref.stepType τ (Sum.inl field) = τ
• ComputablePlusCal.Ref.stepType (x_1.function rng) (Sum.inr idx) = rng
• ComputablePlusCal.Ref.stepType elem.seq (Sum.inr idx) = elem
• ComputablePlusCal.Ref.stepType (SurfaceTLAPlus.Typ.tuple τs) (Sum.inr (ComputableTLAPlus.Expression.nat n)) = (n.toNat?.bind fun (x : ℕ) => τs[x - 1]?).getD (SurfaceTLAPlus.Typ.tuple τs)
• ComputablePlusCal.Ref.stepType (SurfaceTLAPlus.Typ.tuple τs) (Sum.inr idx) = SurfaceTLAPlus.Typ.tuple τs
• ComputablePlusCal.Ref.stepType τ (Sum.inr idx) = τ

def ComputablePlusCal.Ref.indexType : ComputableTLAPlus.Typ → ComputableTLAPlus.Typ

The type a Ref's bracket-index expression must have at one particular .inr step, given the type before that step (unlike stepType, which gives the type after). Used by Computable2Guarded/Par.lean's parRef to annotate hoisted index-temp with-bindings.

Equations

• ComputablePlusCal.Ref.indexType (x.function rng) = x
• ComputablePlusCal.Ref.indexType elem.seq = SurfaceTLAPlus.Typ.int
• ComputablePlusCal.Ref.indexType (SurfaceTLAPlus.Typ.tuple τs) = SurfaceTLAPlus.Typ.int
• ComputablePlusCal.Ref.indexType x✝ = x✝

def ComputablePlusCal.Ref.resultType (r : Ref) : ComputableTLAPlus.Typ

The type a whole reference denotes: its base type, advanced one Ref.stepType per index.

Equations

• r.resultType = List.foldl ComputablePlusCal.Ref.stepType r.baseType r.args