structure Strata.Laurel.TransState : Type

• uri : Uri

  The file the program being translated came from. Compiler-embedded preludes name their defining .lean file and set synthesized.

• synthesized : Bool

  True when the source is a compiler-embedded prelude rather than a user file. Only affects the Core MetaData provenance; FileRanges still name uri so every AST node carries a real file.

• errors : Array String

@[reducible, inline]

abbrev Strata.Laurel.TransM (α : Type) : Type

Equations

• Strata.Laurel.TransM = StateT Strata.Laurel.TransState (Except String)

def Strata.Laurel.TransM.run {α : Type} (uri : Uri) (m : TransM α) (synthesized : Bool := false) : Except String α

Equations

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

def Strata.Laurel.TransM.error {α : Type} (msg : String) : TransM α

Equations

• Strata.Laurel.TransM.error msg = throw msg

def Strata.Laurel.getArgMetaData (arg : StrataDDM.Arg) : TransM (Imperative.MetaData Core.Expression)

Equations

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

def Strata.Laurel.checkOp (op : StrataDDM.Operation) (name : StrataDDM.QualifiedIdent) (argc : Nat) : TransM Unit

Equations

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

def Strata.Laurel.translateIdent (arg : StrataDDM.Arg) : TransM Identifier

Equations

• Strata.Laurel.translateIdent (StrataDDM.ArgF.ident ann id) = do let source ← Strata.Laurel.getArgFileRange✝ (StrataDDM.ArgF.ident ann id) pure { text := id, source := source }
• Strata.Laurel.translateIdent arg = Strata.Laurel.TransM.error (toString "translateIdent expects ident")

def Strata.Laurel.translateBool (arg : StrataDDM.Arg) : TransM Bool

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.translateBool (StrataDDM.ArgF.expr (StrataDDM.ExprF.fn ann { dialect := "Init", name := "boolTrue" })) = pure true
• Strata.Laurel.translateBool (StrataDDM.ArgF.expr (StrataDDM.ExprF.fn ann { dialect := "Init", name := "boolFalse" })) = pure false
• Strata.Laurel.translateBool (StrataDDM.ArgF.expr (StrataDDM.ExprF.fn ann name)) = Strata.Laurel.TransM.error (toString "translateBool expects boolTrue or boolFalse, got " ++ toString (repr name))
• Strata.Laurel.translateBool arg = Strata.Laurel.TransM.error (toString "translateBool expects expression or operation, got " ++ toString (repr arg))

@[implicit_reducible]

instance Strata.Laurel.instInhabitedParameter : Inhabited Parameter

Equations

• Strata.Laurel.instInhabitedParameter = { default := { name := { text := "" }, type := default } }

def Strata.Laurel.mkHighTypeMd (t : HighType) (source : FileRange) : HighTypeMd

Equations

• Strata.Laurel.mkHighTypeMd t source = { val := t, source := source }

def Strata.Laurel.mkStmtExprMd (e : StmtExpr) (source : FileRange) : StmtExprMd

Equations

• Strata.Laurel.mkStmtExprMd e source = { val := e, source := source }

def Strata.Laurel.translateNat (arg : StrataDDM.Arg) : TransM Nat

Equations

• Strata.Laurel.translateNat (StrataDDM.ArgF.num ann n) = pure n
• Strata.Laurel.translateNat arg = Strata.Laurel.TransM.error (toString "translateNat expects num literal")

@[irreducible]

def Strata.Laurel.translateHighType (arg : StrataDDM.Arg) : TransM HighTypeMd

Equations

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

def Strata.Laurel.translateString (arg : StrataDDM.Arg) : TransM String

Equations

• Strata.Laurel.translateString (StrataDDM.ArgF.strlit ann s) = pure s
• Strata.Laurel.translateString arg = Strata.Laurel.TransM.error (toString "translateString expects string literal")

def Strata.Laurel.translateDecimal (arg : StrataDDM.Arg) : TransM StrataDDM.Decimal

Equations

• Strata.Laurel.translateDecimal (StrataDDM.ArgF.decimal ann d) = pure d
• Strata.Laurel.translateDecimal arg = Strata.Laurel.TransM.error (toString "translateDecimal expects decimal literal")

def Strata.Laurel.translateParameter (arg : StrataDDM.Arg) : TransM Parameter

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.translateParameter arg = Strata.Laurel.TransM.error (toString "translateParameter expects operation")

def Strata.Laurel.translateParameters (arg : StrataDDM.Arg) : TransM (List Parameter)

Equations

• Strata.Laurel.translateParameters (StrataDDM.ArgF.seq ann StrataDDM.SepFormat.comma args) = List.mapM Strata.Laurel.translateParameter args.toList
• Strata.Laurel.translateParameters arg = pure []

@[implicit_reducible]

instance Strata.Laurel.instInhabitedProcedure : Inhabited Procedure

Equations

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

def Strata.Laurel.getBinaryOp? (name : StrataDDM.QualifiedIdent) : Option Operation

Equations

• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "add" } = some Strata.Laurel.Operation.Add
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "sub" } = some Strata.Laurel.Operation.Sub
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "mul" } = some Strata.Laurel.Operation.Mul
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "div" } = some Strata.Laurel.Operation.Div
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "mod" } = some Strata.Laurel.Operation.Mod
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "divT" } = some Strata.Laurel.Operation.DivT
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "modT" } = some Strata.Laurel.Operation.ModT
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "eq" } = some Strata.Laurel.Operation.Eq
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "neq" } = some Strata.Laurel.Operation.Neq
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "gt" } = some Strata.Laurel.Operation.Gt
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "lt" } = some Strata.Laurel.Operation.Lt
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "le" } = some Strata.Laurel.Operation.Leq
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "ge" } = some Strata.Laurel.Operation.Geq
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "and" } = some Strata.Laurel.Operation.And
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "or" } = some Strata.Laurel.Operation.Or
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "andThen" } = some Strata.Laurel.Operation.AndThen
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "orElse" } = some Strata.Laurel.Operation.OrElse
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "implies" } = some Strata.Laurel.Operation.Implies
• Strata.Laurel.getBinaryOp? { dialect := "Laurel", name := "strConcat" } = some Strata.Laurel.Operation.StrConcat
• Strata.Laurel.getBinaryOp? name = none

def Strata.Laurel.getUnaryOp? (name : StrataDDM.QualifiedIdent) : Option Operation

Equations

• Strata.Laurel.getUnaryOp? { dialect := "Laurel", name := "not" } = some Strata.Laurel.Operation.Not
• Strata.Laurel.getUnaryOp? { dialect := "Laurel", name := "neg" } = some Strata.Laurel.Operation.Neg
• Strata.Laurel.getUnaryOp? name = none

def Strata.Laurel.translateInvariantClauses (translate : StrataDDM.Arg → TransM StmtExprMd) (arg : StrataDDM.Arg) : TransM (List StmtExprMd)

Translate a Seq InvariantClause into the list of invariant conditions, using translate for each clause body. Shared by the while, forLoop, and doWhile arms. Takes translate as a parameter so it can stay outside the translateStmtExpr mutual block and thus be a total def.

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.translateInvariantClauses translate arg = pure []

partial def Strata.Laurel.translateStmtExpr (arg : StrataDDM.Arg) : TransM StmtExprMd

partial def Strata.Laurel.translateSeqCommand (arg : StrataDDM.Arg) : TransM (List StmtExprMd)

def Strata.Laurel.translateCommand (arg : StrataDDM.Arg) : TransM StmtExprMd

Equations

• Strata.Laurel.translateCommand arg = Strata.Laurel.translateStmtExpr arg

partial def Strata.Laurel.translateIncrDecrTarget (arg : StrataDDM.Arg) (opName : String) : TransM VariableMd

Translate the target of an increment/decrement operator. The target must be an lvalue: either a local variable reference (Var (.Local _)) or a field access (Var (.Field _ _)). Anything else is reported as a translation error.

def Strata.Laurel.translateModifiesExprs (arg : StrataDDM.Arg) : TransM (List StmtExprMd)

Equations

• Strata.Laurel.translateModifiesExprs (StrataDDM.ArgF.seq ann StrataDDM.SepFormat.comma args) = List.mapM Strata.Laurel.translateStmtExpr args.toList
• Strata.Laurel.translateModifiesExprs arg = pure []

def Strata.Laurel.translateModifiesClauses (arg : StrataDDM.Arg) : TransM (List ModifiesGroup)

User modifies clauses fold into a single unguarded ModifiesGroup — one frame, exactly the pre-guard semantics. A modifiesWhenClause (pass-generated, but parsed here so printed output round-trips) contributes its own guarded group.

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.translateModifiesClauses arg = pure Strata.Laurel.ModifiesGroup.nothingChanges

def Strata.Laurel.translateRequiresClauses (arg : StrataDDM.Arg) : TransM (List Condition)

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.translateRequiresClauses arg = pure []

def Strata.Laurel.translateEnsuresClauses (arg : StrataDDM.Arg) : TransM (List Condition)

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.translateEnsuresClauses arg = pure []

def Strata.Laurel.translateSingleReturnType (returnTypeOp : StrataDDM.Operation) : TransM (List Parameter)

Translate the single-output Laurel.returnType op into the implicit $result output parameter.

A producer may attach a source range only to the outer returnType op: the Java front-end builds the inner type op from a javac Type, which carries no tree position, so the inner op's range is the SourceRange.none sentinel. Fall back to the outer op's range in that case, so the ensures that ConstrainedTypeElim synthesizes for a constrained output type (e.g. int32 for a Java int) inherits a real location — otherwise an implicit no-overflow failure is reported at the whole-file fallback position instead of at the return type.

The jverify producer now stamps the declared type tree's range on the inner op itself (this CR's StrataJavaFrontEnd commit), so for current jverify the inner range wins and this fallback is a safety net — it remains load-bearing for other producers and previously-emitted Ion.

Equations

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

def Strata.Laurel.parseProcedure (arg : StrataDDM.Arg) : TransM Procedure

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.parseProcedure arg = Strata.Laurel.TransM.error (toString "parseProcedure expects operation")

def Strata.Laurel.parseField (arg : StrataDDM.Arg) : TransM Field

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.parseField arg = Strata.Laurel.TransM.error (toString "parseField expects operation")

def Strata.Laurel.parseComposite (arg : StrataDDM.Arg) : TransM TypeDefinition

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.parseComposite arg = Strata.Laurel.TransM.error (toString "parseComposite expects operation")

def Strata.Laurel.parseDatatypeConstructorArg (arg : StrataDDM.Arg) : TransM Parameter

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.parseDatatypeConstructorArg arg = Strata.Laurel.TransM.error (toString "parseDatatypeConstructorArg expects operation")

def Strata.Laurel.parseDatatypeConstructor (arg : StrataDDM.Arg) : TransM DatatypeConstructor

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.parseDatatypeConstructor arg = Strata.Laurel.TransM.error (toString "parseDatatypeConstructor expects operation")

def Strata.Laurel.parseDatatype (arg : StrataDDM.Arg) : TransM TypeDefinition

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.parseDatatype arg = Strata.Laurel.TransM.error (toString "parseDatatype expects operation")

def Strata.Laurel.parseConstrainedType (arg : StrataDDM.Arg) : TransM ConstrainedType

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.parseConstrainedType arg = Strata.Laurel.TransM.error (toString "parseConstrainedType expects operation")

def Strata.Laurel.parseTopLevel (arg : StrataDDM.Arg) : TransM (Option Procedure × Option TypeDefinition)

Translate one non-global top-level command, preserving the existing public API.

Equations

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

def Strata.Laurel.parseProgram (prog : StrataDDM.Program) : TransM Program

Translate concrete Laurel syntax into abstract Laurel syntax

Equations

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