structure Strata.Laurel.TransState : Type

• uri : Uri
• 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 α) : Except String α

Equations

• Strata.Laurel.TransM.run uri m = match StateT.run m { uri := uri, errors := #[] } with | Except.ok (v, snd) => Except.ok v | Except.error e => Except.error e

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

Equations

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

def Strata.Laurel.SourceRange.toMetaData (uri : Uri) (sr : SourceRange) : Imperative.MetaData Core.Expression

Equations

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

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

Equations

• Strata.Laurel.getArgMetaData arg = do let __do_lift ← get pure (Strata.Laurel.SourceRange.toMetaData __do_lift.uri (Strata.ArgF.ann arg))

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

Equations

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

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

Equations

• Strata.Laurel.translateIdent (Strata.ArgF.ident ann id) = pure id
• Strata.Laurel.translateIdent arg = Strata.Laurel.TransM.error (toString "translateIdent expects ident")

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

Equations

• One or more equations did not get rendered due to their size.
• Strata.Laurel.translateBool (Strata.ArgF.expr (Strata.ExprF.fn ann { dialect := "Init", name := "boolTrue" })) = pure true
• Strata.Laurel.translateBool (Strata.ArgF.expr (Strata.ExprF.fn ann { dialect := "Init", name := "boolFalse" })) = pure false
• Strata.Laurel.translateBool (Strata.ArgF.expr (Strata.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))

instance Strata.Laurel.instInhabitedParameter : Inhabited Parameter

Equations

• Strata.Laurel.instInhabitedParameter = { default := { name := "", type := { val := Strata.Laurel.HighType.TVoid, md := #[] } } }

def Strata.Laurel.mkHighTypeMd (t : HighType) (md : Imperative.MetaData Core.Expression) : HighTypeMd

Equations

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

def Strata.Laurel.mkStmtExprMd (e : StmtExpr) (md : Imperative.MetaData Core.Expression) : StmtExprMd

Equations

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

def Strata.Laurel.mkStmtExprMdEmpty (e : StmtExpr) : StmtExprMd

Equations

• Strata.Laurel.mkStmtExprMdEmpty e = { val := e, md := #[] }

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

Equations

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

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

Equations

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

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

Equations

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

def Strata.Laurel.translateParameter (arg : 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 : Arg) : TransM (List Parameter)

Equations

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

instance Strata.Laurel.instInhabitedProcedure : Inhabited Procedure

Equations

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

def Strata.Laurel.getBinaryOp? (name : 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 := "implies" } = some Strata.Laurel.Operation.Implies
• Strata.Laurel.getBinaryOp? name = none

def Strata.Laurel.getUnaryOp? (name : 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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Strata.Laurel.parseProcedure (arg : 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 : 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 : 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.parseTopLevel (arg : Arg) : TransM (Option Procedure × Option TypeDefinition)

Equations

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

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

Translate concrete Laurel syntax into abstract Laurel syntax

Equations

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