The smt! term DSL

smt! writes a term in notation close to Lean's own — smt! i + 2 * j ≤ k ∧ ¬ b — and builds it in Env. smtU! builds a sort-erased term and smtT! a typed one; open Cvc.Untyped or open Cvc.Typed makes smt! stand for the matching one.

This module declares the forms that belong to no theory: parentheses, ![e] to splice a Lean term, identifiers, application f a b, let x ← t; u and fun (x : s) => t. Every other form — literals, operators, if, match, quantifiers — is declared by the theory module it belongs to, so smt! accepts exactly the notations of the theories imported.

def Cvc.smtTerm.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.smtTerm : Category

Equations

• Lean.Parser.Category.smtTerm = { }

def Cvc.smtParen : Lean.ParserDescr

Parenthesized SMT term.

Equations

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

def Cvc.smtEscape : Lean.ParserDescr

Escape back into Lean: ![e] splices the Lean term e, which must be an Env-term.

Equations

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

def Cvc.smtIdent : Lean.ParserDescr

An identifier denotes an already-built term, lifted with pure.

Equations

• Cvc.smtIdent = Lean.ParserDescr.node `Cvc.smtIdent 1024 (Lean.ParserDescr.const `ident)

def Cvc.smtLet : Lean.ParserDescr

let x ← t; u binds the term t to x in u.

Equations

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

def Cvc.smtApp : Lean.TrailingParserDescr

Function application, f arg₁ arg₂ …, spelled as Lean spells it.

f i b applies f to two arguments, and a new line at or left of the application's column is not read as one more argument. if, let, match and every operator need parentheses to be an argument, exactly as in Lean.

Equations

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

Binders

A lambda and a quantifier bind their variables the way Lean's do, in parentheses with a sort after the colon: (x y : s). Sort-erased, the sort is a Lean type (Int) or a Srt value (int); typed, it is the Lean type indexing the variable.

def Cvc.smtQuantBinder.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.smtQuantBinder : Category

Binders of an smt! lambda or quantifier.

Equations

• Lean.Parser.Category.smtQuantBinder = { }

def Cvc.smtQuantBinder : Lean.ParserDescr

Variables sharing a sort: (x y : s).

Equations

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

def Cvc.smtFun : Lean.ParserDescr

A lambda, fun (x y : s) => body, spelled as Lean spells it.

The body extends as far right as it can, as in Lean, so a lambda in argument position needs parentheses. cvc5 prints the variables under the names written.

Equations

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

def Cvc.smtExpand : Lean.ParserDescr

Expands one smtTerm of the layer whose root is named, deferring its sub-terms to itself.

This is the DSL's dispatch: each theory adds the expansion of its own forms as a macro_rules alternative for it, tried before those of the modules it imports.

Equations

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

def Cvc.smtIdentElab : Lean.ParserDescr

An identifier leaf of the layer whose root is named, elaborated by Cvc.Ext.elabSmtIdent.

Equations

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

def Cvc.smtUStx : Lean.ParserDescr

Builds a sort-erased term in Env from smt! notation.

Equations

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

def Cvc.smtTStx : Lean.ParserDescr

Builds a typed term in Env from smt! notation.

Equations

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

The expander

The DSL's own machinery, used by the theory modules to declare their forms.

structure Cvc.Ext.Layer : Type

The layer an smt! expansion targets.

• root : Lean.Name

  The layer's own namespace, holding what is not a term constructor.

@[instance_reducible]

instance Cvc.Ext.instInhabitedLayer : Inhabited Layer

Equations

• Cvc.Ext.instInhabitedLayer = { default := Cvc.Ext.instInhabitedLayer.default }

@[instance_reducible]

instance Cvc.Ext.instBEqLayer : BEq Layer

Equations

• Cvc.Ext.instBEqLayer = { beq := Cvc.Ext.instBEqLayer.beq }

def Cvc.Ext.instBEqLayer.beq : Layer → Layer → Bool

Equations

• Cvc.Ext.instBEqLayer.beq { root := a } { root := b } = (a == b)
• Cvc.Ext.instBEqLayer.beq x✝¹ x✝ = false

def Cvc.Ext.Layer.untyped : Layer

The sort-erased layer.

Equations

• Cvc.Ext.Layer.untyped = { root := `Cvc.Untyped }

def Cvc.Ext.Layer.typed : Layer

The typed layer.

Equations

• Cvc.Ext.Layer.typed = { root := `Cvc.Typed }

def Cvc.Ext.Layer.ofIdent (id : Lean.Ident) : Layer

The layer a smtExpand% node names.

Equations

• Cvc.Ext.Layer.ofIdent id = { root := Lean.TSyntax.getId id }

def Cvc.Ext.Layer.ident (layer : Layer) : Lean.Ident

The identifier naming this layer in a smtExpand% node.

Equations

• layer.ident = Lean.mkIdent layer.root

def Cvc.Ext.Layer.ops (layer : Layer) : Lean.Name

Namespace holding the generated operator constructors.

Equations

• layer.ops = layer.root ++ `Term

def Cvc.Ext.Layer.op (layer : Layer) (id : Lean.Name) : Lean.Ident

The identifier of an operator of this layer.

Equations

• layer.op id = Lean.mkIdent (layer.ops ++ id)

def Cvc.Ext.Layer.name (layer : Layer) (id : Lean.Name) : Lean.Ident

The identifier of a declaration of this layer that is not a term constructor.

Equations

• layer.name id = Lean.mkIdent (layer.root ++ id)

def Cvc.Ext.smtOpKind? : Lean.Name → Option (Lean.Name × Lean.Name)

Decomposes a generated operator node kind into its shape and operator name.

Grammar rules are named …smtOp.<shape>.<id>, so the trailing three components identify the operator regardless of the namespace the rule was generated in.

Equations

• Cvc.Ext.smtOpKind? (((pre.str "smtOp").str shape).str id) = some (Lean.Name.mkSimple shape, Lean.Name.mkSimple id)
• Cvc.Ext.smtOpKind? x✝ = none

def Cvc.Ext.naryIdOf (id : Lean.Name) : Lean.Name

Name of the n-ary function of an operator, <id>N.

Equations

• Cvc.Ext.naryIdOf id = id.appendAfter "N"

def Cvc.Ext.bindArgs (args : Array (Lean.TSyntax `term)) (mk : Array Lean.Ident → Lean.MacroM (Lean.TSyntax `term)) (binder : String := "smtArg") : Lean.MacroM (Lean.TSyntax `term)

Binds every argument in order, then applies mk to the identifiers they were bound to.

Binder names are macro-scoped, so they cannot capture user identifiers. Two calls in one expansion produce the same binder names, macro scopes and all, so a nested one shadows what the outer bound. binder is what tells them apart where that matters.

Equations

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

def Cvc.Ext.freshId (base : String) : Lean.MacroM Lean.Ident

A macro-scoped identifier, for a name the expansion binds but the writer never sees.

Equations

• Cvc.Ext.freshId base = do let __do_lift ← Lean.MonadQuotation.addMacroScope (Lean.Name.mkSimple base) pure (Lean.mkIdent __do_lift)

def Cvc.Ext.deferSmt (layer : Layer) (stx : Lean.Syntax) : Lean.MacroM (Lean.TSyntax `term)

A sub-term's expansion, deferred to smtExpand% so that a theory's forms can be reached.

Equations

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

def Cvc.Ext.expandSmt (layer : Layer) (stx : Lean.Syntax) : Lean.MacroM (Lean.TSyntax `term)

Expands one smtTerm node into a term of the given layer.

Operator nodes are dispatched by kind; everything else is a fixed form declared above. Sub-terms are not expanded here — they go back through smtExpand%, so a form this module does not know can still occur inside one it does.

Equations

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

def Cvc.Ext.isSmtTermType (type : Lean.Expr) : Bool

Whether a type is one of the layers' terms, or what converts to one.

This is where a dotted identifier stops being a Lean projection and starts reading record fields.

Equations

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

def Cvc.Ext.typedToTerm? (type : Lean.Expr) : Option Lean.Name

The conversion to a term of a typed non-terminal's, bound variable's or state symbol's type.

A state symbol is a Symbols.At, whose get answers the term it wraps when the wrap is the layer's terms, as it is wherever smt! meets one.

Equations

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

def Cvc.Ext.elabSmtIdent (layer : Layer) (id : Lean.Term) (expected? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Elaborates an identifier leaf: the term it names, lifted with pure.

Typed, a non-terminal, a bound variable or a state symbol (Symbols.At) is converted to its term, at the index its own type carries, so smt! n * m works over two non-terminals with nothing else fixing the index. Anything else is elaborated exactly as written. Not only identifiers come through here: a field projection on a Lean value does too.

Equations

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

def Cvc.Ext.elabSmtIdentTerm : Lean.Elab.Term.TermElab

An identifier leaf of the layer whose root is named, elaborated by Cvc.Ext.elabSmtIdent.

Equations

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

def Cvc.Ext.quantBinders (binders : Lean.Syntax) : Array (Lean.Ident × Lean.Term)

The variables of a lambda's or quantifier's binders, in order, each with its written sort.

Equations

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

def Cvc.Ext.quantName (id : Lean.Ident) : Lean.StrLit

The name cvc5 gives a bound variable: the one the writer gave it.

Equations

• Cvc.Ext.quantName id = Lean.Syntax.mkStrLit (Lean.TSyntax.getId id).eraseMacroScopes.toString