inductive Auto.Parser.SMTTerm.LexVal : Type

• lparen : LexVal
• rparen : LexVal
• num (n : Nat) : LexVal
• rat (n m : Nat) : LexVal
• str (s : String) : LexVal
• symb (s : String) : LexVal
• kw (s : String) : LexVal
• reserved (s : String) : LexVal
• comment (s : String) : LexVal
• underscore : LexVal

instance Auto.Parser.SMTTerm.instInhabitedLexVal : Inhabited LexVal

Equations

• Auto.Parser.SMTTerm.instInhabitedLexVal = { default := Auto.Parser.SMTTerm.LexVal.lparen }

instance Auto.Parser.SMTTerm.instBEqLexVal : BEq LexVal

Equations

• Auto.Parser.SMTTerm.instBEqLexVal = { beq := Auto.Parser.SMTTerm.beqLexVal✝ }

instance Auto.Parser.SMTTerm.instHashableLexVal : Hashable LexVal

Equations

• Auto.Parser.SMTTerm.instHashableLexVal = { hash := Auto.Parser.SMTTerm.hashLexVal✝ }

def Auto.Parser.SMTTerm.LexVal.toString : LexVal → String

Equations

• One or more equations did not get rendered due to their size.
• Auto.Parser.SMTTerm.LexVal.lparen.toString = "("
• Auto.Parser.SMTTerm.LexVal.rparen.toString = ")"
• (Auto.Parser.SMTTerm.LexVal.num a).toString = toString "" ++ toString a ++ toString ""
• (Auto.Parser.SMTTerm.LexVal.str a).toString = "\"" ++ "\"\"".intercalate (a.splitOn "\"") ++ "\""
• (Auto.Parser.SMTTerm.LexVal.symb a).toString = toString "|" ++ toString a ++ toString "|"
• (Auto.Parser.SMTTerm.LexVal.kw a).toString = toString ":" ++ toString a ++ toString ""
• (Auto.Parser.SMTTerm.LexVal.reserved a).toString = a
• (Auto.Parser.SMTTerm.LexVal.comment a).toString = toString ";" ++ toString a ++ toString "\n"
• Auto.Parser.SMTTerm.LexVal.underscore.toString = "_"

instance Auto.Parser.SMTTerm.instToStringLexVal : ToString LexVal

Equations

• Auto.Parser.SMTTerm.instToStringLexVal = { toString := Auto.Parser.SMTTerm.LexVal.toString }

def Auto.Parser.SMTTerm.LexVal.ofString (s attr : String) : LexVal

Equations

• One or more equations did not get rendered due to their size.
• Auto.Parser.SMTTerm.LexVal.ofString s "(" = Auto.Parser.SMTTerm.LexVal.lparen
• Auto.Parser.SMTTerm.LexVal.ofString s ")" = Auto.Parser.SMTTerm.LexVal.rparen
• Auto.Parser.SMTTerm.LexVal.ofString s "numeral" = Auto.Parser.SMTTerm.LexVal.num s.toNat!
• Auto.Parser.SMTTerm.LexVal.ofString s "hexadecimal" = Auto.Parser.SMTTerm.LexVal.num (String.foldl (fun (x : Nat) (c : Char) => x * 16 + Auto.Parser.SMTTerm.hexDigitToNat✝ c) 0 (s.drop 2))
• Auto.Parser.SMTTerm.LexVal.ofString s "binary" = Auto.Parser.SMTTerm.LexVal.num (String.foldl (fun (x : Nat) (c : Char) => x * 2 + c.toNat - '0'.toNat) 0 (s.drop 2))
• Auto.Parser.SMTTerm.LexVal.ofString s "string" = Auto.Parser.SMTTerm.LexVal.str ("\"".intercalate (((s.drop 1).take (s.length - 2)).splitOn "\"\""))
• Auto.Parser.SMTTerm.LexVal.ofString s "simplesymbol" = Auto.Parser.SMTTerm.LexVal.symb s
• Auto.Parser.SMTTerm.LexVal.ofString s "quotedsymbol" = Auto.Parser.SMTTerm.LexVal.symb ((s.drop 1).take (s.length - 2))
• Auto.Parser.SMTTerm.LexVal.ofString s "keyword" = Auto.Parser.SMTTerm.LexVal.kw (s.drop 1)
• Auto.Parser.SMTTerm.LexVal.ofString s "comment" = Auto.Parser.SMTTerm.LexVal.comment ((s.drop 1).take (s.length - 2 - if (s.get (s.prev (s.prev s.endPos)) == '\x0d') = true then 1 else 0))
• Auto.Parser.SMTTerm.LexVal.ofString s "reserved" = Auto.Parser.SMTTerm.LexVal.reserved s
• Auto.Parser.SMTTerm.LexVal.ofString s "forall" = Auto.Parser.SMTTerm.LexVal.reserved "forall"
• Auto.Parser.SMTTerm.LexVal.ofString s "exists" = Auto.Parser.SMTTerm.LexVal.reserved "exists"
• Auto.Parser.SMTTerm.LexVal.ofString s "lambda" = Auto.Parser.SMTTerm.LexVal.reserved "lambda"
• Auto.Parser.SMTTerm.LexVal.ofString s "let" = Auto.Parser.SMTTerm.LexVal.reserved "let"
• Auto.Parser.SMTTerm.LexVal.ofString s "_" = Auto.Parser.SMTTerm.LexVal.underscore

inductive Auto.Parser.SMTTerm.Term : Type

• atom : LexVal → Term
• app : Array Term → Term

instance Auto.Parser.SMTTerm.instInhabitedTerm : Inhabited Term

Equations

• Auto.Parser.SMTTerm.instInhabitedTerm = { default := Auto.Parser.SMTTerm.Term.atom default }

instance Auto.Parser.SMTTerm.instBEqTerm : BEq Term

Equations

• Auto.Parser.SMTTerm.instBEqTerm = { beq := Auto.Parser.SMTTerm.beqTerm✝ }

instance Auto.Parser.SMTTerm.instHashableTerm : Hashable Term

Equations

• Auto.Parser.SMTTerm.instHashableTerm = { hash := Auto.Parser.SMTTerm.hashTerm✝ }

partial def Auto.Parser.SMTTerm.Term.toString : Term → String

instance Auto.Parser.SMTTerm.instToStringTerm : ToString Term

Equations

• Auto.Parser.SMTTerm.instToStringTerm = { toString := fun (e : Auto.Parser.SMTTerm.Term) => e.toString }

structure Auto.Parser.SMTTerm.PartialResult : Type

• lst : Nat
• lexpart : String
• pstk : Array (Array Term)

instance Auto.Parser.SMTTerm.instInhabitedPartialResult : Inhabited PartialResult

Equations

• Auto.Parser.SMTTerm.instInhabitedPartialResult = { default := { lst := default, lexpart := default, pstk := default } }

instance Auto.Parser.SMTTerm.instBEqPartialResult : BEq PartialResult

Equations

• Auto.Parser.SMTTerm.instBEqPartialResult = { beq := Auto.Parser.SMTTerm.beqPartialResult✝ }

instance Auto.Parser.SMTTerm.instHashablePartialResult : Hashable PartialResult

Equations

• Auto.Parser.SMTTerm.instHashablePartialResult = { hash := Auto.Parser.SMTTerm.hashPartialResult✝ }

def Auto.Parser.SMTTerm.PartialResult.toString : PartialResult → String

Equations

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

instance Auto.Parser.SMTTerm.instToStringPartialResult : ToString PartialResult

Equations

• Auto.Parser.SMTTerm.instToStringPartialResult = { toString := Auto.Parser.SMTTerm.PartialResult.toString }

inductive Auto.Parser.SMTTerm.LexResult : Type

• complete : Term → String.Pos → LexResult
• incomplete : PartialResult → String.Pos → LexResult
• malformed : LexResult

instance Auto.Parser.SMTTerm.instInhabitedLexResult : Inhabited LexResult

Equations

• Auto.Parser.SMTTerm.instInhabitedLexResult = { default := Auto.Parser.SMTTerm.LexResult.complete default default }

instance Auto.Parser.SMTTerm.instBEqLexResult : BEq LexResult

Equations

• Auto.Parser.SMTTerm.instBEqLexResult = { beq := Auto.Parser.SMTTerm.beqLexResult✝ }

instance Auto.Parser.SMTTerm.instHashableLexResult : Hashable LexResult

Equations

• Auto.Parser.SMTTerm.instHashableLexResult = { hash := Auto.Parser.SMTTerm.hashLexResult✝ }

def Auto.Parser.SMTTerm.LexResult.toString : LexResult → String

Equations

• (Auto.Parser.SMTTerm.LexResult.complete a a_1).toString = toString "ParseResult.complete " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• (Auto.Parser.SMTTerm.LexResult.incomplete a a_1).toString = toString "ParseResult.incomplete " ++ toString a ++ toString " " ++ toString a_1 ++ toString ""
• Auto.Parser.SMTTerm.LexResult.malformed.toString = "ParseResult.malformed"

def Auto.Parser.SMTTerm.instHashableChar_auto : Hashable Char

Equations

• Auto.Parser.SMTTerm.instHashableChar_auto = { hash := fun (c : Char) => hash c.val }

def Auto.Parser.SMTTerm.lexTerm {m : Type → Type} [Monad m] [Lean.MonadError m] (s : String) (p : String.Pos) (partialResult : PartialResult) : m LexResult

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.

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)

inductive Auto.Parser.SMTTerm.SymbolInput : Type

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

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 = []

def Auto.Parser.SMTTerm.builtInSymbolMap : Std.HashMap String Lean.Expr

Equations

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

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

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

inductive Auto.Parser.SMTTerm.ParseTermConstraint : Type

• expectedType : Lean.Expr → ParseTermConstraint
• noConstraint : ParseTermConstraint

instance Auto.Parser.SMTTerm.instInhabitedParseTermConstraint : Inhabited ParseTermConstraint

Equations

• Auto.Parser.SMTTerm.instInhabitedParseTermConstraint = { default := Auto.Parser.SMTTerm.ParseTermConstraint.expectedType default }

instance Auto.Parser.SMTTerm.instReprParseTermConstraint : Repr ParseTermConstraint

Equations

• Auto.Parser.SMTTerm.instReprParseTermConstraint = { reprPrec := Auto.Parser.SMTTerm.reprParseTermConstraint✝ }

instance Auto.Parser.SMTTerm.instToMessageDataParseTermConstraint : Lean.ToMessageData ParseTermConstraint

Equations

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

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.

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.

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

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

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

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

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

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.

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

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

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

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

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

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)

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

SMT implication is right associative

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.

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.

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.