inductive Auto.Parser.TPTP.Tokenizer.Status : Type

• default : Status
• ident : Status
• string : Status
• comment : Status

instance Auto.Parser.TPTP.Tokenizer.instReprStatus : Repr Status

Equations

• Auto.Parser.TPTP.Tokenizer.instReprStatus = { reprPrec := Auto.Parser.TPTP.Tokenizer.reprStatus✝ }

instance Auto.Parser.TPTP.Tokenizer.instBEqStatus : BEq Status

Equations

• Auto.Parser.TPTP.Tokenizer.instBEqStatus = { beq := Auto.Parser.TPTP.Tokenizer.beqStatus✝ }

inductive Auto.Parser.TPTP.Tokenizer.Token : Type

• op (op : String) : Token
• ident (ident : String) : Token

instance Auto.Parser.TPTP.Tokenizer.instReprToken : Repr Token

Equations

• Auto.Parser.TPTP.Tokenizer.instReprToken = { reprPrec := Auto.Parser.TPTP.Tokenizer.reprToken✝ }

instance Auto.Parser.TPTP.Tokenizer.instInhabitedToken : Inhabited Token

Equations

• Auto.Parser.TPTP.Tokenizer.instInhabitedToken = { default := Auto.Parser.TPTP.Tokenizer.Token.op default }

instance Auto.Parser.TPTP.Tokenizer.instBEqToken : BEq Token

Equations

• Auto.Parser.TPTP.Tokenizer.instBEqToken = { beq := Auto.Parser.TPTP.Tokenizer.beqToken✝ }

def Auto.Parser.TPTP.Tokenizer.Token.toString : Token → String

Equations

• (Auto.Parser.TPTP.Tokenizer.Token.op a).toString = a
• (Auto.Parser.TPTP.Tokenizer.Token.ident a).toString = a

structure Auto.Parser.TPTP.Tokenizer.State : Type

• status : Status
• currToken : String
• res : Array Token

instance Auto.Parser.TPTP.Tokenizer.instReprState : Repr State

Equations

• Auto.Parser.TPTP.Tokenizer.instReprState = { reprPrec := Auto.Parser.TPTP.Tokenizer.reprState✝ }

def Auto.Parser.TPTP.Tokenizer.tokens : List String

Equations

• Auto.Parser.TPTP.Tokenizer.tokens = ["@", "|", "&", "<=>", "=>", "<=", "<~>", "~|", "~&", ">", "=", "!=", "!!", "??", "~", ",", "(", ")", "*", "!", "?", "^", ":", "[", "]", "!>", ".", "*"]

def Auto.Parser.TPTP.Tokenizer.tokenHashMap : Std.HashSet String

Equations

• Auto.Parser.TPTP.Tokenizer.tokenHashMap = Std.HashSet.emptyWithCapacity.insertMany Auto.Parser.TPTP.Tokenizer.tokens

def Auto.Parser.TPTP.Tokenizer.tokenPrefixes : Std.HashSet String

Equations

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

@[reducible, inline]

abbrev Auto.Parser.TPTP.Tokenizer.TokenizerM (α : Type) : Type

Equations

• Auto.Parser.TPTP.Tokenizer.TokenizerM = StateRefT' IO.RealWorld Auto.Parser.TPTP.Tokenizer.State IO

def Auto.Parser.TPTP.Tokenizer.setStatus (status : Status) : TokenizerM Unit

Equations

• Auto.Parser.TPTP.Tokenizer.setStatus status = modify fun (s : Auto.Parser.TPTP.Tokenizer.State) => { status := status, currToken := s.currToken, res := s.res }

def Auto.Parser.TPTP.Tokenizer.getStatus : TokenizerM Status

Equations

• Auto.Parser.TPTP.Tokenizer.getStatus = do let __do_lift ← get pure __do_lift.status

def Auto.Parser.TPTP.Tokenizer.addToCurrToken (char : Char) : TokenizerM Unit

Equations

• Auto.Parser.TPTP.Tokenizer.addToCurrToken char = modify fun (s : Auto.Parser.TPTP.Tokenizer.State) => { status := s.status, currToken := s.currToken.push char, res := s.res }

def Auto.Parser.TPTP.Tokenizer.getCurrToken : TokenizerM String

Equations

• Auto.Parser.TPTP.Tokenizer.getCurrToken = do let __do_lift ← get pure __do_lift.currToken

def Auto.Parser.TPTP.Tokenizer.addCurrToken : TokenizerM Unit

Equations

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

def Auto.Parser.TPTP.Tokenizer.finalizeToken : TokenizerM Unit

Equations

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

def Auto.Parser.TPTP.Tokenizer.tokenizeAux (str : String) : TokenizerM Unit

Equations

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

def Auto.Parser.TPTP.Tokenizer.tokenize (s : String) : IO (Array Token)

Equations

• Auto.Parser.TPTP.Tokenizer.tokenize s = do let __do_lift ← StateRefT'.run (Auto.Parser.TPTP.Tokenizer.tokenizeAux s) { } pure __do_lift.snd.res

structure Auto.Parser.TPTP.State : Type

• tokens : Array Tokenizer.Token
• curr : Nat

instance Auto.Parser.TPTP.instReprState : Repr State

Equations

• Auto.Parser.TPTP.instReprState = { reprPrec := Auto.Parser.TPTP.reprState✝ }

@[reducible, inline]

abbrev Auto.Parser.TPTP.ParserM (α : Type) : Type

Equations

• Auto.Parser.TPTP.ParserM = StateRefT' IO.RealWorld Auto.Parser.TPTP.State IO

def Auto.Parser.TPTP.isEOF : ParserM Bool

Equations

• Auto.Parser.TPTP.isEOF = do let __do_lift ← get let __do_lift_1 ← get pure (__do_lift.curr == __do_lift_1.tokens.size)

def Auto.Parser.TPTP.peek : ParserM Tokenizer.Token

Equations

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

def Auto.Parser.TPTP.peek? : ParserM (Option Tokenizer.Token)

Equations

• Auto.Parser.TPTP.peek? = do let __do_lift ← Auto.Parser.TPTP.isEOF if __do_lift = true then pure none else do let __do_lift ← Auto.Parser.TPTP.peek pure (some __do_lift)

def Auto.Parser.TPTP.next : ParserM Tokenizer.Token

Equations

• Auto.Parser.TPTP.next = do let c ← Auto.Parser.TPTP.peek modify fun (s : Auto.Parser.TPTP.State) => { tokens := s.tokens, curr := s.curr + 1 } pure c

def Auto.Parser.TPTP.infixBindingPower? : String → Option (Nat × Nat)

Equations

• Auto.Parser.TPTP.infixBindingPower? "|" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "&" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "<=>" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "=>" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "<=" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "<~>" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "~|" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "~&" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "@" = some (60, 61)
• Auto.Parser.TPTP.infixBindingPower? "=" = some (90, 90)
• Auto.Parser.TPTP.infixBindingPower? "!=" = some (90, 90)
• Auto.Parser.TPTP.infixBindingPower? "*" = some (41, 40)
• Auto.Parser.TPTP.infixBindingPower? ">" = some (51, 50)
• Auto.Parser.TPTP.infixBindingPower? x✝ = none

def Auto.Parser.TPTP.prefixBindingPower? : String → Option Nat

Equations

• Auto.Parser.TPTP.prefixBindingPower? "~" = some 70
• Auto.Parser.TPTP.prefixBindingPower? x✝ = none

def Auto.Parser.TPTP.binderBindingPower? : String → Option Nat

Equations

• Auto.Parser.TPTP.binderBindingPower? "!" = some 70
• Auto.Parser.TPTP.binderBindingPower? "!>" = some 70
• Auto.Parser.TPTP.binderBindingPower? "?" = some 70
• Auto.Parser.TPTP.binderBindingPower? "^" = some 70
• Auto.Parser.TPTP.binderBindingPower? x✝ = none

def Auto.Parser.TPTP.isPolyIL? : String → Bool

Equations

• Auto.Parser.TPTP.isPolyIL? "??" = true
• Auto.Parser.TPTP.isPolyIL? "!!" = true
• Auto.Parser.TPTP.isPolyIL? "=" = true
• Auto.Parser.TPTP.isPolyIL? x✝ = false

inductive Auto.Parser.TPTP.Term : Type

• mk : Tokenizer.Token → List Term → Term

instance Auto.Parser.TPTP.instInhabitedTerm : Inhabited Term

Equations

• Auto.Parser.TPTP.instInhabitedTerm = { default := Auto.Parser.TPTP.Term.mk default default }

instance Auto.Parser.TPTP.instBEqTerm : BEq Term

Equations

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

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

instance Auto.Parser.TPTP.instToStringTerm : ToString Term

Equations

• Auto.Parser.TPTP.instToStringTerm = { toString := Auto.Parser.TPTP.Term.toString }

def Auto.Parser.TPTP.Term.func : Term → Tokenizer.Token

Equations

• (Auto.Parser.TPTP.Term.mk head tail).func = head

def Auto.Parser.TPTP.Term.args : Term → List Term

Equations

• (Auto.Parser.TPTP.Term.mk head tail).args = tail

def Auto.Parser.TPTP.parseToken (t : Tokenizer.Token) : ParserM Unit

Equations

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

def Auto.Parser.TPTP.parseIdent : ParserM String

Equations

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

partial def Auto.Parser.TPTP.parseSep {α : Type} (sep : Tokenizer.Token) (p : ParserM α) : ParserM (List α)

partial def Auto.Parser.TPTP.parseTerm (minbp : Nat := 0) : ParserM Term

partial def Auto.Parser.TPTP.parseLhs : ParserM Term

partial def Auto.Parser.TPTP.addOpAndRhs (lhs : Term) (minbp : Nat) : ParserM Term

partial def Auto.Parser.TPTP.parseTypeDecl : ParserM Term

partial def Auto.Parser.TPTP.parseAtomTyping : ParserM Term

<thf_atom_typing> <tff_atom_typing>

structure Auto.Parser.TPTP.Command : Type

• cmd : String
• args : List Term

instance Auto.Parser.TPTP.instInhabitedCommand : Inhabited Command

Equations

• Auto.Parser.TPTP.instInhabitedCommand = { default := { cmd := default, args := default } }

instance Auto.Parser.TPTP.instBEqCommand : BEq Command

Equations

• Auto.Parser.TPTP.instBEqCommand = { beq := Auto.Parser.TPTP.beqCommand✝ }

def Auto.Parser.TPTP.Command.toString : Command → String

Equations

• { cmd := cmd, args := args }.toString = cmd ++ "(" ++ ", ".intercalate (List.map Auto.Parser.TPTP.Term.toString args) ++ ")"

instance Auto.Parser.TPTP.instToStringCommand : ToString Command

Equations

• Auto.Parser.TPTP.instToStringCommand = { toString := Auto.Parser.TPTP.Command.toString }

def Auto.Parser.TPTP.parseCommand : ParserM Command

Equations

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

partial def Auto.Parser.TPTP.parseCommands : ParserM (List Command)

def Auto.Parser.TPTP.parse (s : String) : IO (Array Command)

Equations

• Auto.Parser.TPTP.parse s = do let tokens ← Auto.Parser.TPTP.Tokenizer.tokenize s let res ← StateRefT'.run Auto.Parser.TPTP.parseCommands { tokens := tokens } pure { toList := res.fst }

def Auto.Parser.TPTP.ident2LamSort (s : String) : Option Embedding.Lam.LamSort

Equations

• One or more equations did not get rendered due to their size.
• Auto.Parser.TPTP.ident2LamSort "s_nat" = some (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.nat)
• Auto.Parser.TPTP.ident2LamSort "s_int" = some (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.int)
• Auto.Parser.TPTP.ident2LamSort "s_string" = some (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.string)
• Auto.Parser.TPTP.ident2LamSort "s_empty" = some (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.empty)

def Auto.Parser.TPTP.ident2NatConst (s : String) : Option Embedding.Lam.NatConst

def Auto.Parser.TPTP.ident2StringConst (s : String) : Option Embedding.Lam.StringConst

def Auto.Parser.TPTP.ident2IntConst (s : String) : Option Embedding.Lam.IntConst

Equations

• Auto.Parser.TPTP.ident2IntConst "t_iofNat" = some Auto.Embedding.Lam.IntConst.iofNat
• Auto.Parser.TPTP.ident2IntConst "t_inegSucc" = some Auto.Embedding.Lam.IntConst.inegSucc
• Auto.Parser.TPTP.ident2IntConst "t_ineg" = some Auto.Embedding.Lam.IntConst.ineg
• Auto.Parser.TPTP.ident2IntConst "t_iabs" = some Auto.Embedding.Lam.IntConst.iabs
• Auto.Parser.TPTP.ident2IntConst "t_iadd" = some Auto.Embedding.Lam.IntConst.iadd
• Auto.Parser.TPTP.ident2IntConst "t_isub" = some Auto.Embedding.Lam.IntConst.isub
• Auto.Parser.TPTP.ident2IntConst "t_imul" = some Auto.Embedding.Lam.IntConst.imul
• Auto.Parser.TPTP.ident2IntConst "t_idiv" = some Auto.Embedding.Lam.IntConst.idiv
• Auto.Parser.TPTP.ident2IntConst "t_imod" = some Auto.Embedding.Lam.IntConst.imod
• Auto.Parser.TPTP.ident2IntConst "t_iediv" = some Auto.Embedding.Lam.IntConst.iediv
• Auto.Parser.TPTP.ident2IntConst "t_iemod" = some Auto.Embedding.Lam.IntConst.iemod
• Auto.Parser.TPTP.ident2IntConst "t_ile" = some Auto.Embedding.Lam.IntConst.ile
• Auto.Parser.TPTP.ident2IntConst "t_ilt" = some Auto.Embedding.Lam.IntConst.ilt
• Auto.Parser.TPTP.ident2IntConst "t_imax" = some Auto.Embedding.Lam.IntConst.imax
• Auto.Parser.TPTP.ident2IntConst "t_imin" = some Auto.Embedding.Lam.IntConst.imin
• Auto.Parser.TPTP.ident2IntConst s = none

def Auto.Parser.TPTP.ident2BitVecConst (s : String) : Option Embedding.Lam.BitVecConst

inductive Auto.Parser.TPTP.LamConstr : Type

• error : String → LamConstr
• kind : LamConstr
• sort : Embedding.Lam.LamSort → LamConstr
• term : Embedding.Lam.LamSort → Embedding.Lam.LamTerm → LamConstr

instance Auto.Parser.TPTP.instInhabitedLamConstr : Inhabited LamConstr

Equations

• Auto.Parser.TPTP.instInhabitedLamConstr = { default := Auto.Parser.TPTP.LamConstr.error default }

instance Auto.Parser.TPTP.instHashableLamConstr : Hashable LamConstr

Equations

• Auto.Parser.TPTP.instHashableLamConstr = { hash := Auto.Parser.TPTP.hashLamConstr✝ }

instance Auto.Parser.TPTP.instBEqLamConstr : BEq LamConstr

Equations

• Auto.Parser.TPTP.instBEqLamConstr = { beq := Auto.Parser.TPTP.beqLamConstr✝ }

def Auto.Parser.TPTP.LamConstr.toString : LamConstr → String

Equations

• (Auto.Parser.TPTP.LamConstr.error a).toString = toString "error " ++ toString a ++ toString ""
• Auto.Parser.TPTP.LamConstr.kind.toString = "kind"
• (Auto.Parser.TPTP.LamConstr.sort a).toString = toString "sort " ++ toString a ++ toString ""
• (Auto.Parser.TPTP.LamConstr.term a a_1).toString = toString "term " ++ toString a_1 ++ toString " : " ++ toString a ++ toString ""

instance Auto.Parser.TPTP.instToStringLamConstr : ToString LamConstr

Equations

• Auto.Parser.TPTP.instToStringLamConstr = { toString := Auto.Parser.TPTP.LamConstr.toString }

structure Auto.Parser.TPTP.ParsingInfo : Type

• lamVarTy : Array Embedding.Lam.LamSort
• lamEVarTy : Array Embedding.Lam.LamSort
• proverSkolem : Std.HashMap String (Embedding.Lam.LamSort × Nat)

def Auto.Parser.TPTP.ParsingInfo.toLamTyVal (pi : ParsingInfo) : Embedding.Lam.LamTyVal

Equations

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

def Auto.Parser.TPTP.ParsingInfo.addSkolem (pi : ParsingInfo) (name : String) (s : Embedding.Lam.LamSort) : ParsingInfo

Equations

• pi.addSkolem name s = { lamVarTy := pi.lamVarTy, lamEVarTy := pi.lamEVarTy, proverSkolem := pi.proverSkolem.insert name (s, pi.proverSkolem.size) }

def Auto.Parser.TPTP.LamConstr.ofBaseTerm (pi : ParsingInfo) (b : Embedding.Lam.LamBaseTerm) : LamConstr

Equations

• Auto.Parser.TPTP.LamConstr.ofBaseTerm pi b = Auto.Parser.TPTP.LamConstr.term (Auto.Embedding.Lam.LamBaseTerm.lamCheck pi.toLamTyVal b) (Auto.Embedding.Lam.LamTerm.base b)

def Auto.Parser.TPTP.ident2LamConstr (pi : ParsingInfo) (s : String) : LamConstr

Equations

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

partial def Auto.Parser.TPTP.term2LamTerm (pi : ParsingInfo) (t : Term) (lctx : Std.HashMap String (Nat × Embedding.Lam.LamSort) := ∅) : LamConstr

This function is only for zipperposition's output

partial def Auto.Parser.TPTP.term2LamTerm.processVar (pi : ParsingInfo) (var : Term) (lctx : Std.HashMap String (Nat × Embedding.Lam.LamSort)) : Option (String × Embedding.Lam.LamSort)

def Auto.Parser.TPTP.term2LamTerm.deBruijnAndSort? (lctx : Std.HashMap String (Nat × Embedding.Lam.LamSort)) (id : String) : Option (Nat × Embedding.Lam.LamSort)

Equations

• Auto.Parser.TPTP.term2LamTerm.deBruijnAndSort? lctx id = match lctx.get? id with | some (n, s) => some (lctx.size - 1 - n, s) | none => none

partial def Auto.Parser.TPTP.term2LamTerm.lamConstrMkAppN (head : LamConstr) (args : List LamConstr) : LamConstr

def Auto.Parser.TPTP.getProof (lamVarTy lamEVarTy : Array Embedding.Lam.LamSort) (cmds : Array Command) : Lean.MetaM (Array Embedding.Lam.LamTerm)

Turn TSTP term into LamSort/LamTerm This function is only for zipperposition's output

Equations

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

def Auto.Parser.TPTP.unsatCore (cmds : Array Command) : Lean.MetaM (Array Nat)

Returns the unsat core of an array of TSTP steps

Equations

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