def StrataDDM.isIdBegin (c : Char) : Bool

Check if a character is valid for starting a regular identifier. Regular identifiers must start with a letter or underscore.

NOTE: When updating this function, you will want to consider updating Strata/DDM/Parser.lean as well.

Equations

• StrataDDM.isIdBegin c = (c.isAlpha || c == '_' || c == '$')

def StrataDDM.isIdContinue (c : Char) : Bool

Check if a character is valid for continuing a regular identifier. Includes @ and $ which are valid in SMT-LIB 2.6 simple symbols and used by the encoder for disambiguated names (e.g. x@1) and generated names (e.g. $__bv0). Note: ' (apostrophe) is intentionally excluded. Although SMT-LIB 2.6 allows it in simple symbols, both cvc5 and Z3 reject it as an unquoted character. Names containing ' (e.g. Lean's v') will be pipe-quoted instead.

Equations

• StrataDDM.isIdContinue c = (c.isAlphanum || c == '_' || c == '.' || c == '?' || c == '!' || c == '@' || c == '$')

def StrataDDM.quoteIdent (s : String) : String

Quote an identifier string for SMT-LIB, adding pipe delimiters if needed.

Equations

• StrataDDM.quoteIdent s = if StrataDDM.needsPipeDelimiters✝ s = true then "|" ++ StrataDDM.escapePipeIdent✝ s ++ "|" else s

structure StrataDDM.PrecFormat : Type

• format : Std.Format
• prec : Nat

@[implicit_reducible]

instance StrataDDM.instInhabitedPrecFormat : Inhabited PrecFormat

Equations

• StrataDDM.instInhabitedPrecFormat = { default := StrataDDM.instInhabitedPrecFormat.default }

def StrataDDM.instInhabitedPrecFormat.default : PrecFormat

Equations

• StrataDDM.instInhabitedPrecFormat.default = { format := default, prec := default }

structure StrataDDM.FormatOptions : Type

Options to control parenthesis

• alwaysParen : Bool

  Always add parenthesis when feasible.

• smtStringEscaping : Bool

  Use SMT-LIB 2.7 string escaping ("" for quotes) instead of C-style (\").

• formatModes : Std.HashMap String FormatMode

  Force a format mode per literal kind (e.g. "decimal"), overriding any dialect-declared spec. An absent entry means "use each type's default".

structure StrataDDM.FormatContext : Type

A format context provides callbacks and information needed to properly pretty-print Strata AST types.

• opts : StrataDDM.FormatOptions
• getFnDecl : StrataDDM.QualifiedIdent → Option StrataDDM.FunctionDecl
• getOpDecl : StrataDDM.QualifiedIdent → Option StrataDDM.OpDecl
• globalContext : StrataDDM.GlobalContext
• argFormatMode : Option StrataDDM.FormatMode

def StrataDDM.FormatContext.withArgFormatMode (ctx : FormatContext) (mode : Option FormatMode) : FormatContext

Set the format mode carried from the current argument's declaration.

Equations

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

def StrataDDM.FormatContext.ofDialects (dialects : DialectMap) (globalContext : GlobalContext := ∅) (opts : FormatOptions := { }) : FormatContext

Equations

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

structure StrataDDM.FormatState : Type

Format state

• openDialects : Std.HashSet String
• bindings : Array String

def StrataDDM.FormatState.empty : FormatState

A format context that uses no syntactic sugar.

Equations

• StrataDDM.FormatState.empty = { openDialects := ∅ }

@[implicit_reducible]

instance StrataDDM.FormatState.instInhabited : Inhabited FormatState

Equations

• StrataDDM.FormatState.instInhabited = { default := StrataDDM.FormatState.empty }

def StrataDDM.FormatState.pushBinding (s : FormatState) (ident : String) : FormatState

Equations

• s.pushBinding ident = { openDialects := s.openDialects, bindings := s.bindings.push ident }

def StrataDDM.StrataFormat : Type

A StrataFormat is a closure which given contextual information produces a format operation as well as a precedence. This is used for auto-inserting parenthesis when needed.

Formats should return maxPrec when parenthesis are not required.

Equations

• StrataDDM.StrataFormat = (StrataDDM.FormatContext → StrataDDM.FormatState → StrataDDM.PrecFormat)

class StrataDDM.ToStrataFormat (α : Type u) : Type u

• mformat : α → StrataFormat

def StrataDDM.eformat {α : Type u_1} [ToStrataFormat α] (a : α) : Std.Format

Equations

• StrataDDM.eformat a = (StrataDDM.mformat a StrataDDM.FormatContext.explicit✝ StrataDDM.FormatState.empty).format

@[implicit_reducible]

instance StrataDDM.instToStrataFormatString : ToStrataFormat String

Equations

• StrataDDM.instToStrataFormatString = { mformat := fun (s : String) (x : StrataDDM.FormatContext) (x_1 : StrataDDM.FormatState) => StrataDDM.instToStrataFormatString._private_1 s }

@[implicit_reducible]

instance StrataDDM.instToStrataFormatFormat : ToStrataFormat Std.Format

Equations

• StrataDDM.instToStrataFormatFormat = { mformat := fun (s : Std.Format) (x : StrataDDM.FormatContext) (x_1 : StrataDDM.FormatState) => StrataDDM.instToStrataFormatFormat._private_1 s }

@[implicit_reducible]

instance StrataDDM.instToStrataFormatStrataFormat : ToStrataFormat StrataFormat

Equations

• StrataDDM.instToStrataFormatStrataFormat = { mformat := id }

@[implicit_reducible]

instance StrataDDM.instToStrataFormatNat : ToStrataFormat Nat

Equations

• StrataDDM.instToStrataFormatNat = { mformat := fun (n : Nat) (x : StrataDDM.FormatContext) (x_1 : StrataDDM.FormatState) => StrataDDM.instToStrataFormatNat._private_1 n }

@[implicit_reducible]

instance StrataDDM.instToStrataFormatDecimal : ToStrataFormat Decimal

Equations

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

@[implicit_reducible]

instance StrataDDM.StrataFormat.instAppend : Append StrataFormat

Equations

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

def StrataDDM.StrataFormat.withState (f : FormatState → FormatState) (fmt : StrataFormat) : StrataFormat

Equations

• StrataDDM.StrataFormat.withState f fmt c s = fmt c (f s)

def StrataDDM.termMf!_ : Lean.ParserDescr

Equations

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

@[implicit_reducible]

instance StrataDDM.instToStrataFormatQualifiedIdent : ToStrataFormat QualifiedIdent

Equations

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

@[implicit_reducible]

instance StrataDDM.TypeExprF.instToStrataFormat {α : Type} : ToStrataFormat (TypeExprF α)

Equations

• StrataDDM.TypeExprF.instToStrataFormat = { mformat := fun (e : StrataDDM.TypeExprF α) => StrataDDM.TypeExprF.instToStrataFormat._private_1 e }

@[implicit_reducible]

instance StrataDDM.PreType.instToStrataFormat : ToStrataFormat PreType

Equations

• StrataDDM.PreType.instToStrataFormat = { mformat := StrataDDM.PreType.instToStrataFormat._private_1 }

@[implicit_reducible]

instance StrataDDM.SyntaxCatF.instToStrataFormat {α : Type} : ToStrataFormat (SyntaxCatF α)

Equations

• StrataDDM.SyntaxCatF.instToStrataFormat = { mformat := StrataDDM.SyntaxCatF.instToStrataFormat._private_1 }

@[implicit_reducible]

instance StrataDDM.ExprF.instToStrataFormat {α : Type} : ToStrataFormat (ExprF α)

Equations

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

@[implicit_reducible]

instance StrataDDM.ArgF.instToStrataFormat {α : Type} : ToStrataFormat (ArgF α)

Equations

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

@[implicit_reducible]

instance StrataDDM.OperationF.instToStrataFormat {α : Type} : ToStrataFormat (OperationF α)

Equations

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

def StrataDDM.OperationF.render {α : Type} (op : OperationF α) (ctx : FormatContext) (s : FormatState) : String × FormatState

This renders an operation returning its string representation and new state.

Equations

• op.render ctx s = match StrataDDM.OperationF.mformatM✝ op ctx s with | (f, s) => (Std.Format.render✝ f.format, s)

@[implicit_reducible]

instance StrataDDM.MetadataArg.instToStrataFormat : ToStrataFormat MetadataArg

Equations

• StrataDDM.MetadataArg.instToStrataFormat = { mformat := StrataDDM.MetadataArg.instToStrataFormat._private_1 }

@[implicit_reducible]

instance StrataDDM.MetadataAttr.instToStrataFormat : ToStrataFormat MetadataAttr

Equations

• StrataDDM.MetadataAttr.instToStrataFormat = { mformat := fun (a : StrataDDM.MetadataAttr) => StrataDDM.MetadataAttr.instToStrataFormat._private_1 a }

@[implicit_reducible]

instance StrataDDM.Metadata.instToStrataFormat : ToStrataFormat Metadata

Equations

• StrataDDM.Metadata.instToStrataFormat = { mformat := fun (m : StrataDDM.Metadata) => StrataDDM.Metadata.instToStrataFormat._private_1 m }

@[implicit_reducible]

instance StrataDDM.ArgDeclKind.instToStrataFormat : ToStrataFormat ArgDeclKind

Equations

• StrataDDM.ArgDeclKind.instToStrataFormat = { mformat := StrataDDM.ArgDeclKind.instToStrataFormat._private_1 }

@[implicit_reducible]

instance StrataDDM.ArgDecl.instToStrataFormat : ToStrataFormat ArgDecl

Equations

• StrataDDM.ArgDecl.instToStrataFormat = { mformat := fun (b : StrataDDM.ArgDecl) => StrataDDM.ArgDecl.instToStrataFormat._private_1 b }

@[implicit_reducible]

instance StrataDDM.ArgDecls.instToStrataFormat : ToStrataFormat ArgDecls

Equations

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

@[implicit_reducible]

instance StrataDDM.SyntaxDefAtom.instToStrataFormat : ToStrataFormat SyntaxDefAtom

Equations

• StrataDDM.SyntaxDefAtom.instToStrataFormat = { mformat := StrataDDM.SyntaxDefAtom.instToStrataFormat._private_1 }

@[implicit_reducible]

instance StrataDDM.SyntaxDef.instToStrataFormat : ToStrataFormat SyntaxDef

Equations

• StrataDDM.SyntaxDef.instToStrataFormat = { mformat := StrataDDM.SyntaxDef.instToStrataFormat._private_1 }

@[implicit_reducible]

instance StrataDDM.SynCatDecl.instToStrataFormat : ToStrataFormat SynCatDecl

Equations

• StrataDDM.SynCatDecl.instToStrataFormat = { mformat := fun (d : StrataDDM.SynCatDecl) => StrataDDM.SynCatDecl.instToStrataFormat._private_1 d }

@[implicit_reducible]

instance StrataDDM.OpDecl.instToStrataFormat : ToStrataFormat OpDecl

Equations

• StrataDDM.OpDecl.instToStrataFormat = { mformat := fun (d : StrataDDM.OpDecl) => StrataDDM.OpDecl.instToStrataFormat._private_1 d }

@[implicit_reducible]

instance StrataDDM.TypeDecl.instToStrataFormat : ToStrataFormat TypeDecl

Equations

• StrataDDM.TypeDecl.instToStrataFormat = { mformat := fun (d : StrataDDM.TypeDecl) => StrataDDM.TypeDecl.instToStrataFormat._private_1 d }

@[implicit_reducible]

instance StrataDDM.FunctionDecl.instToStrataFormat : ToStrataFormat FunctionDecl

Equations

• StrataDDM.FunctionDecl.instToStrataFormat = { mformat := fun (d : StrataDDM.FunctionDecl) => StrataDDM.FunctionDecl.instToStrataFormat._private_1 d }

@[implicit_reducible]

instance StrataDDM.MetadataArgType.instToStrataFormat : ToStrataFormat MetadataArgType

Equations

• StrataDDM.MetadataArgType.instToStrataFormat = { mformat := StrataDDM.MetadataArgType.instToStrataFormat._private_1 }

@[implicit_reducible]

instance StrataDDM.MetadataDecl.instToStrataFormat : ToStrataFormat MetadataDecl

Equations

• StrataDDM.MetadataDecl.instToStrataFormat = { mformat := fun (d : StrataDDM.MetadataDecl) => StrataDDM.MetadataDecl.instToStrataFormat._private_1 d }

@[implicit_reducible]

instance StrataDDM.Decl.instToStrataFormat : ToStrataFormat Decl

Equations

• StrataDDM.Decl.instToStrataFormat = { mformat := StrataDDM.Decl.instToStrataFormat._private_1 }

def StrataDDM.DialectMap.format (dialects : DialectMap) (name : DialectName) (mem : name ∈ dialects) (opts : FormatOptions := { }) : Std.Format

Pretty print the dialect with the given name in the map.

Equations

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

def StrataDDM.Program.formatContext (p : Program) (opts : FormatOptions) : FormatContext

Equations

• p.formatContext opts = StrataDDM.FormatContext.ofDialects p.dialects p.globalContext opts

def StrataDDM.Program.formatState (p : Program) : FormatState

Equations

• p.formatState = { openDialects := List.foldl (fun (a : Std.HashSet String) (d : StrataDDM.Dialect) => a.insert d.name) ∅ p.dialects.toList }

def StrataDDM.Program.format (p : Program) (opts : FormatOptions := { }) : Std.Format

Equations

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

def StrataDDM.Program.toString (p : Program) (opts : FormatOptions := { }) : String

Equations

• p.toString opts = Std.Format.render✝ (p.format opts)

@[implicit_reducible]

instance StrataDDM.Program.instToString : ToString Program

Equations

• StrataDDM.Program.instToString = { toString := fun (p : StrataDDM.Program) => p.toString }

def StrataDDM.Program.ppDialect! (p : Program) (name : DialectName := p.dialect) (opts : FormatOptions := { }) : Std.Format

Equations

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