Runtime support for converting AST representations back to generated types. Defines the OfAstM error monad and argument-parsing combinators used by the ofAst functions that #strata_gen emits.

class StrataDDM.HasEta (α : Type u) (β : outParam (Type v)) : Type (max u v)

• bvar : Nat → α
• lambda : String → β → α → α

@[irreducible]

def StrataDDM.etaExpand {E : Type u_1} {T : Type u_2} [HasEta E T] (argTypes : Array (String × T)) (provided : Nat) (e : E) : E

Equations

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

def StrataDDM.OfAstM (α : Type u_1) : Type u_1

Equations

• StrataDDM.OfAstM α = Except String α

@[implicit_reducible]

instance StrataDDM.instToStringOfAstM {α : Type u_1} [ToString α] : ToString (OfAstM α)

Equations

• StrataDDM.instToStringOfAstM = { toString := fun (e : StrataDDM.OfAstM α) => StrataDDM.instToStringOfAstM._private_1 e }

@[implicit_reducible]

instance StrataDDM.instReprOfAstM {α : Type u_1} [Repr α] : Repr (OfAstM α)

Equations

• StrataDDM.instReprOfAstM = { reprPrec := fun (e : StrataDDM.OfAstM α) (prec : Nat) => StrataDDM.instReprOfAstM._private_1 e prec }

@[implicit_reducible]

instance StrataDDM.OfAstM.instMonad : Monad OfAstM

Equations

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

def StrataDDM.OfAstM.throwUnknownExpr {α : Type u_1} (tp : QualifiedIdent) (e : Expr) : OfAstM α

Thrown when an expression is provided but not expected.

Equations

• StrataDDM.OfAstM.throwUnknownExpr tp e = Except.error (toString "Unknown expr " ++ toString (repr e) ++ toString " when parsing as " ++ toString tp ++ toString ".")

def StrataDDM.OfAstM.throwUnknownType {α : Type u_1} (e : TypeExpr) : OfAstM α

Thrown when an expression is provided but not expected.

Equations

• StrataDDM.OfAstM.throwUnknownType e = Except.error (toString "Unknown type " ++ toString (repr e) ++ toString ".")

def StrataDDM.OfAstM.throwExpected {Ann : Type} {α : Type u_1} [Repr Ann] (cat : String) (a : ArgF Ann) : OfAstM α

Raise error when passed an argument that is not an expression when expression expected.

Equations

• StrataDDM.OfAstM.throwExpected cat a = Except.error (toString "Expected " ++ toString cat ++ toString " " ++ toString (repr a) ++ toString ".")

def StrataDDM.OfAstM.throwExpectedExpr {Ann : Type} {α : Type u_1} [Repr Ann] (a : ArgF Ann) : OfAstM α

Raise error when passed an argument that is not an expression when expression expected.

Equations

• StrataDDM.OfAstM.throwExpectedExpr a = StrataDDM.OfAstM.throwExpected "expression" a

def StrataDDM.OfAstM.throwExpectedOperation {α : Type u_1} (a : Arg) : OfAstM α

Raise error when passed an argument that is not an expression when expression expected.

Equations

• StrataDDM.OfAstM.throwExpectedOperation a = StrataDDM.OfAstM.throwExpected "operation" a

def StrataDDM.OfAstM.throwUnexpectedBvar {α : Type u_1} (tp : QualifiedIdent) : OfAstM α

Equations

• StrataDDM.OfAstM.throwUnexpectedBvar tp = Except.error (toString tp ++ toString " has unexpected bound variable.")

def StrataDDM.OfAstM.throwUnexpectedArgCount {α : Type u_1} (tp : QualifiedIdent) (expected actual : Nat) : OfAstM α

Equations

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

def StrataDDM.OfAstM.throwUnknownIdentifier {α : Type u_1} (tp f : QualifiedIdent) : OfAstM α

Equations

• StrataDDM.OfAstM.throwUnknownIdentifier tp f = Except.error (toString tp ++ toString " given unknown operator " ++ toString f ++ toString ".")

def StrataDDM.OfAstM.checkTypeArgCount {α : Type u_1} (expected : Nat) (args : Array α) : OfAstM (PLift (args.size = expected))

Equations

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

def StrataDDM.OfAstM.checkArgCount {α : Type u_1} (tp : QualifiedIdent) (expected : Nat) (args : Array α) : OfAstM (PLift (args.size = expected))

Equations

• StrataDDM.OfAstM.checkArgCount tp expected args = if p : args.size = expected then pure { down := p } else StrataDDM.OfAstM.throwUnexpectedArgCount tp expected args.size

def StrataDDM.OfAstM.checkEtaExprArgCount {Tp : Type u_1} (tp : QualifiedIdent) (expected : Array (String × Tp)) (args : Array Arg) : OfAstM (PLift (args.size ≤ expected.size))

Equations

• StrataDDM.OfAstM.checkEtaExprArgCount tp expected args = if p : args.size ≤ expected.size then pure { down := p } else StrataDDM.OfAstM.throwUnexpectedArgCount tp expected.size args.size

def StrataDDM.OfAstM.ofExpressionM {α : Type} {β : Type u_1} [Repr α] [SizeOf α] (val : ArgF α) (act : (e : ExprF α) → sizeOf e < sizeOf val → OfAstM β) : OfAstM β

Equations

• StrataDDM.OfAstM.ofExpressionM (StrataDDM.ArgF.expr a1) act_2 = act_2 a1 ⋯
• StrataDDM.OfAstM.ofExpressionM val act = StrataDDM.OfAstM.throwExpected "expression" val

def StrataDDM.OfAstM.ofTypeM {α : Type} {β : Type u_1} [Repr α] [SizeOf α] (val : ArgF α) (act : (e : TypeExprF α) → sizeOf e < sizeOf val → OfAstM β) : OfAstM β

Equations

• StrataDDM.OfAstM.ofTypeM (StrataDDM.ArgF.type a1) act_2 = act_2 a1 ⋯
• StrataDDM.OfAstM.ofTypeM val act = StrataDDM.OfAstM.throwExpected "type" val

def StrataDDM.OfAstM.ofOperationM {α : Type} {β : Type u_1} [Repr α] [SizeOf α] (val : ArgF α) (act : (o : OperationF α) → sizeOf o < sizeOf val → OfAstM β) : OfAstM β

Equations

• StrataDDM.OfAstM.ofOperationM (StrataDDM.ArgF.op a1) act_2 = act_2 a1 ⋯
• StrataDDM.OfAstM.ofOperationM val act = StrataDDM.OfAstM.throwExpected "operation" val

def StrataDDM.OfAstM.ofIdentM {α : Type} [Repr α] : ArgF α → OfAstM String

Equations

• StrataDDM.OfAstM.ofIdentM (StrataDDM.ArgF.ident ann val) = pure val
• StrataDDM.OfAstM.ofIdentM x✝ = StrataDDM.OfAstM.throwExpected "identifier" x✝

def StrataDDM.OfAstM.ofAnnIdentM {α : Type} [Repr α] : ArgF α → OfAstM (Ann String α)

Equations

• StrataDDM.OfAstM.ofAnnIdentM (StrataDDM.ArgF.ident ann val) = pure { ann := ann, val := val }
• StrataDDM.OfAstM.ofAnnIdentM x✝ = StrataDDM.OfAstM.throwExpected "identifier" x✝

def StrataDDM.OfAstM.ofNumM {α : Type} [Repr α] : ArgF α → OfAstM Nat

Equations

• StrataDDM.OfAstM.ofNumM (StrataDDM.ArgF.num ann val) = pure val
• StrataDDM.OfAstM.ofNumM x✝ = StrataDDM.OfAstM.throwExpected "numeric literal" x✝

def StrataDDM.OfAstM.ofAnnNumM {α : Type} [Repr α] : ArgF α → OfAstM (Ann Nat α)

Equations

• StrataDDM.OfAstM.ofAnnNumM (StrataDDM.ArgF.num ann val) = pure { ann := ann, val := val }
• StrataDDM.OfAstM.ofAnnNumM x✝ = StrataDDM.OfAstM.throwExpected "numeric literal" x✝

def StrataDDM.OfAstM.ofDecimalM {α : Type} [Repr α] : ArgF α → OfAstM Decimal

Equations

• StrataDDM.OfAstM.ofDecimalM (StrataDDM.ArgF.decimal ann val) = pure val
• StrataDDM.OfAstM.ofDecimalM x✝ = StrataDDM.OfAstM.throwExpected "scientific literal" x✝

def StrataDDM.OfAstM.ofAnnDecimalM {α : Type} [Repr α] : ArgF α → OfAstM (Ann Decimal α)

Equations

• StrataDDM.OfAstM.ofAnnDecimalM (StrataDDM.ArgF.decimal ann val) = pure { ann := ann, val := val }
• StrataDDM.OfAstM.ofAnnDecimalM x✝ = StrataDDM.OfAstM.throwExpected "scientific literal" x✝

def StrataDDM.OfAstM.ofStrlitM {α : Type} [Repr α] : ArgF α → OfAstM String

Equations

• StrataDDM.OfAstM.ofStrlitM (StrataDDM.ArgF.strlit ann val) = pure val
• StrataDDM.OfAstM.ofStrlitM x✝ = StrataDDM.OfAstM.throwExpected "string literal" x✝

def StrataDDM.OfAstM.ofAnnStrlitM {α : Type} [Repr α] : ArgF α → OfAstM (Ann String α)

Equations

• StrataDDM.OfAstM.ofAnnStrlitM (StrataDDM.ArgF.strlit ann val) = pure { ann := ann, val := val }
• StrataDDM.OfAstM.ofAnnStrlitM x✝ = StrataDDM.OfAstM.throwExpected "string literal" x✝

def StrataDDM.OfAstM.ofBytesM {α : Type} [Repr α] : ArgF α → OfAstM ByteArray

Equations

• StrataDDM.OfAstM.ofBytesM (StrataDDM.ArgF.bytes ann val) = pure val
• StrataDDM.OfAstM.ofBytesM x✝ = StrataDDM.OfAstM.throwExpected "byte array" x✝

def StrataDDM.OfAstM.ofAnnBytesM {α : Type} [Repr α] : ArgF α → OfAstM (Ann ByteArray α)

Equations

• StrataDDM.OfAstM.ofAnnBytesM (StrataDDM.ArgF.bytes ann val) = pure { ann := ann, val := val }
• StrataDDM.OfAstM.ofAnnBytesM x✝ = StrataDDM.OfAstM.throwExpected "byte array" x✝

def StrataDDM.OfAstM.toAstBool {α : Type} [Inhabited α] (v : Ann Bool α) : OperationF α

Convert Ann Bool to OperationF

Equations

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

def StrataDDM.OfAstM.ofAstBool {α : Type} [Inhabited α] [Repr α] (op : OperationF α) : OfAstM (Ann Bool α)

Convert OperationF to Ann Bool

Equations

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

def StrataDDM.OfAstM.ofBoolM {α : Type} [Inhabited α] [Repr α] : ArgF α → OfAstM Bool

Equations

• StrataDDM.OfAstM.ofBoolM (StrataDDM.ArgF.op op) = StrataDDM.Ann.val <$> StrataDDM.OfAstM.ofAstBool op
• StrataDDM.OfAstM.ofBoolM x✝ = StrataDDM.OfAstM.throwExpected "boolean" x✝

def StrataDDM.OfAstM.ofAnnBoolM {α : Type} [Inhabited α] [Repr α] : ArgF α → OfAstM (Ann Bool α)

Equations

• StrataDDM.OfAstM.ofAnnBoolM (StrataDDM.ArgF.op op) = StrataDDM.OfAstM.ofAstBool op
• StrataDDM.OfAstM.ofAnnBoolM x✝ = StrataDDM.OfAstM.throwExpected "boolean" x✝

def StrataDDM.OfAstM.ofOptionM {α β : Type} [Repr α] [SizeOf α] (arg : ArgF α) (act : (e : ArgF α) → sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Option β) α)

Equations

• StrataDDM.OfAstM.ofOptionM (StrataDDM.ArgF.option ann none) act_3 = pure { ann := ann, val := none }
• StrataDDM.OfAstM.ofOptionM (StrataDDM.ArgF.option ann (some v)) act_3 = (fun (v : β) => { ann := ann, val := some v }) <$> act_3 v ⋯
• StrataDDM.OfAstM.ofOptionM arg act = StrataDDM.OfAstM.throwExpected "option" arg

def StrataDDM.OfAstM.ofSeqM {α β : Type} [Repr α] [SizeOf α] (sep : SepFormat) (arg : ArgF α) (act : (e : ArgF α) → sizeOf e < sizeOf arg → OfAstM β) : OfAstM (Ann (Array β) α)

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.OfAstM.ofSeqM sep arg act = StrataDDM.OfAstM.throwExpected sep.toString arg

def StrataDDM.OfAstM.matchTypeParamOrType {Ann : Type} {α : Type u_1} [Repr Ann] (a : ArgF Ann) (onTypeParam : Ann → α) (onType : TypeExprF Ann → OfAstM α) : OfAstM α

Distinguishes between a type parameter (category reference) and a type expression in Init.TypeP, applying the appropriate handler.

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.OfAstM.matchTypeParamOrType (StrataDDM.ArgF.type tp) onTypeParam onType = onType tp
• StrataDDM.OfAstM.matchTypeParamOrType a onTypeParam onType = StrataDDM.OfAstM.throwExpected "Type parameter or type expression" a