SyGuS grammars, typed

A grammar restricts the shape of a term the solver may produce, for synthFun, getInterpolant or getAbduct. smt.grammar! writes one as a block, its first non-terminal being the start symbol:

smt.grammar! s (x y : Int) where
  start : Int  := x | y | 0 | if c then start else start
  c     : Bool := start ≤ start

A rule must have its non-terminal's sort, or it does not compile. A Grammar σ carries the parameters it was built over, and σ is their sorts arrowed onto the start symbol's (Int → Int → Int above), so synthFun needs nothing else. Any solver of the scope accepts a grammar, but a grammar freezes once used: after synthFun, cvc5 rejects further rules.

Non-terminal symbols

structure Cvc.Typed.NT [Ω] (α : Type) : Type

A grammar's non-terminal symbol, at the sort its index describes.

A bound variable, but not interchangeable with one: mkGrammar takes the parameters and the non-terminals separately, and only the type keeps them apart.

• ofUntyped :: (
• untyped : Cvc.Untyped.NT
• )

@[reducible, inline]

abbrev Cvc.Typed.NTs [Ω] : Type 1

Non-terminal symbols of assorted sorts.

Equations

• Cvc.Typed.NTs = List ((α : Type) × Cvc.Typed.NT α)

def Cvc.Typed.NT.mk' [Ω] (α : Type) [ToTyp α] (name : String) : Env (NT α)

A non-terminal symbol of the sort α describes.

Equations

• Cvc.Typed.NT.mk' α name = do let __do_lift ← Cvc.Srt.of α let __do_lift ← Cvc.Untyped.NT.mk __do_lift name pure { untyped := __do_lift }

@[reducible, inline]

abbrev Cvc.Typed.NT.mk [Ω] {α : Type} [ToTyp α] (name : String) : Env (NT α)

A non-terminal symbol of the sort α describes.

Equations

• Cvc.Typed.NT.mk name = Cvc.Typed.NT.mk' α name

def Cvc.Typed.NT.toBVar [Ω] {α : Type} (nt : NT α) : BVar α

Turns itself into a bound variable.

Explicit on purpose: there is no coercion, because a non-terminal is not a parameter.

Equations

• nt.toBVar = (Cvc.Typed.NT.untyped✝ nt).toBVar

def Cvc.Typed.NT.toTerm [Ω] {α : Type} (nt : NT α) : Term α

Turns itself into a term, which is how a non-terminal appears inside its own rules.

Equations

• nt.toTerm = (Cvc.Typed.NT.untyped✝ nt).toTerm

@[instance_reducible]

instance Cvc.Typed.NT.instCoeTerm [Ω] {α : Type} : Coe (NT α) (Term α)

Equations

• Cvc.Typed.NT.instCoeTerm = { coe := Cvc.Typed.NT.toTerm }

def Cvc.Typed.NT.toUntyped [Ω] {α : Type} (nt : NT α) : Untyped.NT

The sort-erased non-terminal it wraps, for free.

Equations

• nt.toUntyped = Cvc.Typed.NT.untyped✝ nt

@[reducible, inline]

abbrev Cvc.Typed.NT.erase [Ω] {α : Type} (nt : NT α) : Untyped.NT

The sort-erased non-terminal it wraps, for free.

Equations

• @Cvc.Typed.NT.erase = @Cvc.Typed.NT.toUntyped

def Cvc.Untyped.NT.toTypedAs [Ω] (α : Type) [ToTyp α] (nt : NT) : Env (Typed.NT α)

Types a sort-erased non-terminal at α, checking its sort against α's.

The non-terminal counterpart of Untyped.Term.toTypedAs, so that the non-terminals a sort-erased grammar was built with can be given rules through the typed Grammar.addRule. toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

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

def Cvc.Untyped.NT.toTyped [Ω] {α : Type} [ToTyp α] (nt : NT) : Env (Typed.NT α)

Types a sort-erased non-terminal at α, checking its sort against α's.

The non-terminal counterpart of Untyped.Term.toTypedAs, so that the non-terminals a sort-erased grammar was built with can be given rules through the typed Grammar.addRule. toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• nt.toTyped = Cvc.Untyped.NT.toTypedAs α nt

@[reducible, inline]

abbrev Cvc.Untyped.NT.typeCheckAs [Ω] (α : Type) [ToTyp α] (nt : NT) : Env (Typed.NT α)

Types a sort-erased non-terminal at α, checking its sort against α's.

The non-terminal counterpart of Untyped.Term.toTypedAs, so that the non-terminals a sort-erased grammar was built with can be given rules through the typed Grammar.addRule. toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• @Cvc.Untyped.NT.typeCheckAs = @Cvc.Untyped.NT.toTypedAs

@[reducible, inline]

abbrev Cvc.Untyped.NT.typeCheck [Ω] {α : Type} [ToTyp α] (nt : NT) : Env (Typed.NT α)

Types a sort-erased non-terminal at α, checking its sort against α's.

The non-terminal counterpart of Untyped.Term.toTypedAs, so that the non-terminals a sort-erased grammar was built with can be given rules through the typed Grammar.addRule. toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• @Cvc.Untyped.NT.typeCheck = @Cvc.Untyped.NT.toTyped

@[reducible, inline]

abbrev Cvc.Typed.NTs.push [Ω] {α : Type} (nt : NT α) (nts : NTs) : NTs

Adds a non-terminal.

Equations

• Cvc.Typed.NTs.push nt nts = ⟨α, nt⟩ :: nts

def Cvc.Typed.NTs.toUntyped [Ω] (nts : NTs) : Untyped.NTs

The sort-erased non-terminals, in the same order.

Equations

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

@[reducible, inline]

abbrev Cvc.Typed.NTs.erase [Ω] (nts : NTs) : Untyped.NTs

The sort-erased non-terminals, in the same order.

Equations

• @Cvc.Typed.NTs.erase = @Cvc.Typed.NTs.toUntyped

Grammars

def Cvc.Typed.Solver.mkGrammar [Ω] (s : Solver) {α : Type} [ToTyp α] (boundVars : BVars) (start : NT α) (others : NTs := []) : Env (Grammar (BVars.signatureTo α boundVars))

A grammar over the given parameters, starting at start.

boundVars are the parameters of the function the grammar will constrain, and the index is their sorts arrowed onto start's. others are the other non-terminals the rules may mention.

Equations

• s.mkGrammar boundVars start others = do let __do_lift ← Cvc.Untyped.Solver.mkGrammar s boundVars.erase start.erase others.erase pure { untyped := __do_lift }

def Cvc.Untyped.Grammar.toTypedAs [Ω] (σ : Type) [ToTyp σ] (g : Grammar) : Env (Typed.Grammar σ)

Types a sort-erased grammar at signature σ, checking it against what the grammar generates.

σ is compared with the grammar's parameters' sorts arrowed onto its start symbol's. toTyped infers σ from the expected type; typeCheckAs and typeCheck are the same two functions.

Equations

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

def Cvc.Untyped.Grammar.toTyped [Ω] {σ : Type} [ToTyp σ] (g : Grammar) : Env (Typed.Grammar σ)

Types a sort-erased grammar at signature σ, checking it against what the grammar generates.

σ is compared with the grammar's parameters' sorts arrowed onto its start symbol's. toTyped infers σ from the expected type; typeCheckAs and typeCheck are the same two functions.

Equations

• g.toTyped = Cvc.Untyped.Grammar.toTypedAs σ g

@[reducible, inline]

abbrev Cvc.Untyped.Grammar.typeCheckAs [Ω] (σ : Type) [ToTyp σ] (g : Grammar) : Env (Typed.Grammar σ)

Types a sort-erased grammar at signature σ, checking it against what the grammar generates.

σ is compared with the grammar's parameters' sorts arrowed onto its start symbol's. toTyped infers σ from the expected type; typeCheckAs and typeCheck are the same two functions.

Equations

• @Cvc.Untyped.Grammar.typeCheckAs = @Cvc.Untyped.Grammar.toTypedAs

@[reducible, inline]

abbrev Cvc.Untyped.Grammar.typeCheck [Ω] {σ : Type} [ToTyp σ] (g : Grammar) : Env (Typed.Grammar σ)

Types a sort-erased grammar at signature σ, checking it against what the grammar generates.

σ is compared with the grammar's parameters' sorts arrowed onto its start symbol's. toTyped infers σ from the expected type; typeCheckAs and typeCheck are the same two functions.

Equations

• @Cvc.Untyped.Grammar.typeCheck = @Cvc.Untyped.Grammar.toTyped

def Cvc.Typed.Grammar.addRule {σ : Type} [Ω] (g : Grammar σ) {α : Type} (nt : NT α) (rule : Term α) : Env (Grammar σ)

Adds a production rule.

The rule's index is the non-terminal's, so a sort mismatch does not typecheck. That the non-terminal belongs to this grammar is a property of a value rather than a type, so it is checked when the rule is added.

Equations

• g.addRule nt rule = do let __do_lift ← (Cvc.Typed.Grammar.untyped✝ g).addRule nt.erase rule.erase pure { untyped := __do_lift }

def Cvc.Typed.Grammar.addRules {σ : Type} [Ω] (g : Grammar σ) {α : Type} (nt : NT α) (rules : Terms α) : Env (Grammar σ)

Adds a production rule.

The rule's index is the non-terminal's, so a sort mismatch does not typecheck. That the non-terminal belongs to this grammar is a property of a value rather than a type, so it is checked when the rule is added.

Equations

• g.addRules nt rules = do let __do_lift ← (Cvc.Typed.Grammar.untyped✝ g).addRules nt.erase (Array.map Cvc.Typed.Term.erase rules) pure { untyped := __do_lift }

def Cvc.Typed.Grammar.addAnyConstant {σ : Type} [Ω] (g : Grammar σ) {α : Type} (nt : NT α) : Env (Grammar σ)

Allows any constant of the non-terminal's sort.

Equations

• g.addAnyConstant nt = do let __do_lift ← (Cvc.Typed.Grammar.untyped✝ g).addAnyConstant nt.erase pure { untyped := __do_lift }

def Cvc.Typed.Grammar.addAnyVariable {σ : Type} [Ω] (g : Grammar σ) {α : Type} (nt : NT α) : Env (Grammar σ)

Allows any of the grammar's parameters that has the non-terminal's sort.

Equations

• g.addAnyVariable nt = do let __do_lift ← (Cvc.Typed.Grammar.untyped✝ g).addAnyVariable nt.erase pure { untyped := __do_lift }

smt.grammar!

Available under open Cvc.Typed. A parameter's or a non-terminal's sort is written as a Lean type. To add rules afterwards, smt.mkGrammar! and smt.letGrammar! also hand back the parameters, as BVar α, and the non-terminals, as NT α; there, a non-terminal may be declared with no alternatives (n : Int).

def Cvc.Typed.«termSmt.grammar!_» : Lean.ParserDescr

A grammar written as a block: smt.grammar! s (x : Int) where start : Int := x | ?const.

After the solver building it and the parameters, one line per non-terminal, the first being the start symbol, with |-separated smt! alternatives. ?const and ?var allow any constant and any parameter of the non-terminal's sort.

Equations

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

def Cvc.Typed.«termSmt.mkGrammar!_» : Lean.ParserDescr

smt.grammar!, also answering the parameters and non-terminals it made.

The result is (g, nt₁, …), or ((g, p₁, …), nt₁, …) when there are parameters p₁, ….

Equations

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

def Cvc.Typed.«doElemSmt.letGrammar!_←_» : Lean.ParserDescr

smt.grammar! as a do element, binding the grammar, its parameters and its non-terminals.

smt.letGrammar! g ← s (x : Int) where … binds g, and each parameter and non-terminal under its own name.

Equations

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