Auto.Parser.SMTParser

Note: Make sure that the next character of s is either EOF or white space This is because wee rely on the property that: For each lexicon l with a white space at position p, the part of l before p will always be identified as incomplete by ERE.ADFALexEagerL SMTSexp.lexiconADFA, and never as done.

Equations

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

Instances For

source

partial def Auto.Parser.SMTTerm.lexAllTerms {m : Type → Type} [Monad m] [Lean.MonadError m] (s : String) (p : String.Pos) (acc : List Term) :

m (List Term)

source

inductive Auto.Parser.SMTTerm.SymbolInput :

Type

UnaryBool : SymbolInput
UnaryProp : SymbolInput
LeftAssocNoConstraint : SymbolInput
LeftAssocAllProp : SymbolInput
LeftAssocAllBool : SymbolInput
TwoExactNoConstraint : SymbolInput
TwoExactEq : SymbolInput
Minus : SymbolInput
Ite : SymbolInput

Instances For

source

def Auto.Parser.SMTTerm.smtSymbolToLeanName (s : String) :

List (Lean.Name × SymbolInput)

If s is a theory symbol that we have a hardcoded interpretation for, then return a list of the possible corresponding constants in Lean. When there are no typing constraints to determine which item in the list is to be chosen, earlier items in the list are preferred over later items in the list.

Equations

Auto.Parser.SMTTerm.smtSymbolToLeanName "<" = [(`LT.lt, Auto.Parser.SMTTerm.SymbolInput.TwoExactNoConstraint )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "<=" = [(`LE.le, Auto.Parser.SMTTerm.SymbolInput.TwoExactNoConstraint )]
Auto.Parser.SMTTerm.smtSymbolToLeanName ">" = [(`GT.gt, Auto.Parser.SMTTerm.SymbolInput.TwoExactNoConstraint )]
Auto.Parser.SMTTerm.smtSymbolToLeanName ">=" = [(`GE.ge, Auto.Parser.SMTTerm.SymbolInput.TwoExactNoConstraint )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "+" = [(`HAdd.hAdd, Auto.Parser.SMTTerm.SymbolInput.LeftAssocNoConstraint )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "-" = [(`HSub.hSub, Auto.Parser.SMTTerm.SymbolInput.Minus )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "nsub" = [(`Nat.sub, Auto.Parser.SMTTerm.SymbolInput.Minus )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "*" = [(`HMul.hMul, Auto.Parser.SMTTerm.SymbolInput.LeftAssocNoConstraint )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "/" = [(`HDiv.hDiv, Auto.Parser.SMTTerm.SymbolInput.LeftAssocNoConstraint )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "or" = [(`Or, Auto.Parser.SMTTerm.SymbolInput.LeftAssocAllProp ), (`Bool.or, Auto.Parser.SMTTerm.SymbolInput.LeftAssocAllBool )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "and" = [(`And, Auto.Parser.SMTTerm.SymbolInput.LeftAssocAllProp ), (`Bool.and, Auto.Parser.SMTTerm.SymbolInput.LeftAssocAllBool )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "not" = [(`Not, Auto.Parser.SMTTerm.SymbolInput.UnaryProp ), (`Bool.not, Auto.Parser.SMTTerm.SymbolInput.UnaryBool )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "=" = [(`Eq, Auto.Parser.SMTTerm.SymbolInput.TwoExactEq )]
Auto.Parser.SMTTerm.smtSymbolToLeanName "ite" = [(`Auto.Parser.SMTTerm.SymbolInput.Ite, Auto.Parser.SMTTerm.SymbolInput.Ite )]
Auto.Parser.SMTTerm.smtSymbolToLeanName s = []

Instances For

source

def Auto.Parser.SMTTerm.builtInSymbolMap :

Std.HashMap String Lean.Expr

Equations

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

Instances For

source

partial def Auto.Parser.SMTTerm.getForallArgumentTypes (e : Lean.Expr) :

List Lean.Expr

Given an expression ∀ x1 : t1, x2 : t2, ... xn : tn, b, returns [t1, t2, ..., tn]. If the given expression is not a forall expression, then getForallArgumentTypes just returns the empty list

source

partial def Auto.Parser.SMTTerm.getExplicitForallArgumentTypes (e : Lean.Expr) :

List Lean.Expr

Like getForallArgumentTypes but skips over the types of arguments that have implicit binderInfos

source

inductive Auto.Parser.SMTTerm.ParseTermConstraint :

Type

expectedType : Lean.Expr → ParseTermConstraint
noConstraint : ParseTermConstraint

Instances For

source

instance Auto.Parser.SMTTerm.instInhabitedParseTermConstraint :

Inhabited ParseTermConstraint

Equations

Auto.Parser.SMTTerm.instInhabitedParseTermConstraint = { default := Auto.Parser.SMTTerm.instInhabitedParseTermConstraint.default }

source

def Auto.Parser.SMTTerm.instInhabitedParseTermConstraint.default :

ParseTermConstraint

Equations

Auto.Parser.SMTTerm.instInhabitedParseTermConstraint.default = Auto.Parser.SMTTerm.ParseTermConstraint.expectedType default

Instances For

source

instance Auto.Parser.SMTTerm.instReprParseTermConstraint :

Repr ParseTermConstraint

Equations

Auto.Parser.SMTTerm.instReprParseTermConstraint = { reprPrec := Auto.Parser.SMTTerm.instReprParseTermConstraint.repr }

source

def Auto.Parser.SMTTerm.instReprParseTermConstraint.repr :

ParseTermConstraint → Nat → Std.Format

Equations

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

Instances For

source

instance Auto.Parser.SMTTerm.instToMessageDataParseTermConstraint :

Lean.ToMessageData ParseTermConstraint

Equations

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

source

def Auto.Parser.SMTTerm.getNextSortedVars (originalSortedVars : Array (String × Lean.Expr)) (curPropBoolChoice : Array (Fin originalSortedVars.size × Bool)) :

Array (String × Lean.Expr) × Option (Array (Fin originalSortedVars.size × Bool))

A helper function for parseForall, parseExists, and parseLambda

When parsing the arguments of SMT forall and exists expressions, the SMT type "Bool" can appear, which sometimes must be interpreted as Prop and sometimes must be interpreted as Bool. In parseForall and parseExists, if there are x "Bool" binders, then there are 2^x possible ways to interpret each of those binders. This helper function serves to facilitate the generation of those interpretations.

getNextSortedVars takes as input originalSortedVars obtained by parseSortedVar and curPropBoolChoice which is an Array indicating which of the "Bool" binders should be interpreted as Prop (if curPropBoolChoice contains (i, false), then the ith element of the output sortedVars array should be Bool, and if curPropBoolChoice contains (i, true), then the ith element should be Prop)

getNextSortedVars outputs the resulting sortedVars array (which is identical to originalSortedVars except at the indices where Bool is replaced with Prop) as well as nextPropBoolChoice (obtained by incrementing curPropBoolChoice like a bitvector with the least significant bit first).

If curPropBoolChoice is an Array where no idx is mapped to false, then instead of supplying the next curPropBoolChoice, getNextSortedVars returns none for the second argument

Equations

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

Instances For

source

def Auto.Parser.SMTTerm.correctType (e : Lean.Expr) (parseTermConstraint : ParseTermConstraint) :

Lean.MetaM Lean.Expr

Given an expression e and a ParseTermConstraint, returns an expression that is equivalent to e and conforms to the constraint. If parseTermConstraint is noConstraint, then correctType will prefer interpreting the SMT "Int" sort as Int over Nat.

Equations

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

Instances For

source

partial def Auto.Parser.SMTTerm.parseSortedVar (sortedVar : Term) (symbolMap : Std.HashMap String Lean.Expr) (parseTermConstraint : ParseTermConstraint) :

Lean.MetaM (String × Lean.Expr)

Given a sorted var of the form (symbol type), returns the string of the symbol and the type as an Expr

source

partial def Auto.Parser.SMTTerm.parseForallBodyWithSortedVars (vs : List Term) (sortedVars : Array (String × Lean.Expr)) (symbolMap : Std.HashMap String Lean.Expr) (forallBody : Term) :

Lean.MetaM Lean.Expr

source

partial def Auto.Parser.SMTTerm.parseForall (vs : List Term) (symbolMap : Std.HashMap String Lean.Expr) :

Lean.MetaM Lean.Expr

source

partial def Auto.Parser.SMTTerm.parseExistsBodyWithSortedVars (vs : List Term) (sortedVars : Array (String × Lean.Expr)) (symbolMap : Std.HashMap String Lean.Expr) (existsBody : Term) :

Lean.MetaM Lean.Expr

source

partial def Auto.Parser.SMTTerm.parseExists (vs : List Term) (symbolMap : Std.HashMap String Lean.Expr) :

Lean.MetaM Lean.Expr

source

partial def Auto.Parser.SMTTerm.parseLambdaBodyWithSortedVars (vs : List Term) (sortedVars : Array (String × Lean.Expr)) (symbolMap : Std.HashMap String Lean.Expr) (lambdaBody : Term) (parseTermConstraint : ParseTermConstraint) :

Lean.MetaM Lean.Expr

Note: The parseTermConstraint argument passed into parseLambdaBodyWithSortedVars corresponds to the expected type of the entire lambda expression, not the expected type of the lambda's body.

source

partial def Auto.Parser.SMTTerm.parseLambda (vs : List Term) (symbolMap : Std.HashMap String Lean.Expr) (parseTermConstraint : ParseTermConstraint) :

Lean.MetaM Lean.Expr

source

partial def Auto.Parser.SMTTerm.parseVarBinding (varBinding : Term) (symbolMap : Std.HashMap String Lean.Expr) :

Lean.MetaM (String × Lean.Expr × Lean.Expr)

Given a varBinding of the form (symbol value) returns the string of the symbol, the type of the value, and the value itself

source

partial def Auto.Parser.SMTTerm.parseLet (vs : List Term) (symbolMap : Std.HashMap String Lean.Expr) (parseTermConstraint : ParseTermConstraint) :

Lean.MetaM Lean.Expr

source

partial def Auto.Parser.SMTTerm.parseLeftAssocAppAux (headSymbol : Lean.Name) (args : List Term) (symbolMap : Std.HashMap String Lean.Expr) (acc : Lean.Expr) (parseTermConstraint : ParseTermConstraint) :

Lean.MetaM Lean.Expr

source

partial def Auto.Parser.SMTTerm.parseLeftAssocApp (headSymbol : Lean.Name) (args : List Term) (symbolMap : Std.HashMap String Lean.Expr) (parseTermConstraint : ParseTermConstraint) :

Lean.MetaM Lean.Expr

source

partial def Auto.Parser.SMTTerm.parseImplicationAux (args : List Term) (symbolMap : Std.HashMap String Lean.Expr) (acc : Lean.Expr) :

Lean.MetaM Lean.Expr

Note: parseImplicationAux expects to receive args in reverse order (meaining if args = [x, y, z], this should become z => y => x)

source

partial def Auto.Parser.SMTTerm.parseImplication (args : List Term) (symbolMap : Std.HashMap String Lean.Expr) :

Lean.MetaM Lean.Expr

SMT implication is right associative

source

partial def Auto.Parser.SMTTerm.parseTerm (e : Term) (symbolMap : Std.HashMap String Lean.Expr) (parseTermConstraint : ParseTermConstraint) :

Lean.MetaM Lean.Expr

The entry function for the variety of mutually recursive functions used to parse SMT terms. symbolMap is used to map smt constants to the original Lean expressions they are meant to represent. parseTermConstraint is used to indicate whether the output expression must be a particular type.

source

def Auto.Parser.SMTTerm.parseTermAndAbstractSelectors (e : Term) (symbolMap : Std.HashMap String Lean.Expr) (selMVars : Array Lean.Expr) :

Lean.MetaM Lean.Expr

Calls parseTerm on e and then abstracts all of the metavariables corresponding to selectors given by selMVars (replacing the first metavariable with selMVars with Expr.bvar 0 and so on)

Equations

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

Instances For

source

def Auto.Parser.SMTTerm.tryParseTermAndAbstractSelectors (e : Term) (symbolMap : Std.HashMap String Lean.Expr) (selMVars : Array Lean.Expr) :

Lean.MetaM (Option Lean.Expr)

Calls parseTerm on e and then abstracts all of the metavariables corresponding to selectors given by selMVars (replacing the first metavariable with selMVars with Expr.bvar 0 and so on). Returns none if any error occurs.

Equations

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

Instances For