• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
        • Deftreeops
        • Defdefparse
        • Defgrammar
        • Tree-utilities
          • Check-tree-nonleaf-num-range-4
          • Check-tree-nonleaf-num-range-3
          • Check-tree-num-range-4
          • Check-tree-nonleaf-num-range-2
          • Check-tree-num-range-3
          • Check-tree-num-range-2
          • Tree-list-tuple10
          • Check-tree-nonleaf-num-range
          • Tree-list-tuple9
          • Tree-list-tuple8
          • Tree-list-tuple7
          • Tree-list-tuple6
          • Check-tree-nonleaf-num-seq
          • Check-tree-num-range
          • Tree-list-tuple5
          • Check-tree-nonleaf-10
          • Check-tree-nonleaf-9
          • Check-tree-nonleaf-8
          • Check-tree-nonleaf-7
          • Check-tree-list-list-10
          • Tree-list-tuple4
          • Check-tree-nonleaf-6
          • Check-tree-nonleaf-5
          • Check-tree-list-list-9
          • Check-tree-nonleaf-4
          • Check-tree-nonleaf-3
          • Check-tree-nonleaf-2
          • Check-tree-nonleaf
          • Check-tree-list-list-8
          • Check-tree-nonleaf-1-1
          • Check-tree-nonleaf-1
          • Check-tree-list-list-7
          • Tree-list-tuple3
          • Pass
          • Check-tree-list-list-6
          • Check-tree-list-list-5
          • Tree=>string
          • Tree-list-tuple2
          • Check-tree-list-list-4
          • Check-tree-list-list-3
          • Check-tree-ichars
          • Check-tree-schars
          • Check-tree-num-seq
          • Check-tree-list-list-2
          • Tree-list-tuple9-result
          • Tree-list-tuple8-result
          • Tree-list-tuple7-result
          • Tree-list-tuple6-result
          • Tree-list-tuple5-result
          • Tree-list-tuple4-result
          • Tree-list-tuple3-result
          • Tree-list-tuple2-result
          • Tree-list-tuple10-result
          • Pass-result
          • Check-tree-list-list-1
          • Tree-info-for-error
            • Check-tree-list-1
            • Check-tree-nonleaf?
            • Check-tree-leafterm
          • Notation
          • Grammar-parser
          • Meta-circular-validation
          • Parsing-primitives-defresult
          • Parsing-primitives-seq
          • Operations
          • Examples
          • Differences-with-paper
          • Constructor-utilities
          • Grammar-printer
          • Parsing-tools
        • Vwsim
        • Isar
        • Wp-gen
        • Dimacs-reader
        • Pfcs
        • Legacy-defrstobj
        • Proof-checker-array
        • Soft
        • C
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Riscv
        • Taspi
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Community
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Tree-utilities

    Tree-info-for-error

    Information about a tree for an error result.

    Signature
    (tree-info-for-error tree) → info
    Arguments
    tree — Guard (treep tree).

    When an ABNF tree does not satisfy certain conditions, it is useful to return some information about the tree in the error result. Since ABNF trees may be large, in general we do not want to put the whole tree into the error result. Instead, we want to put some summary information. This function calculates that information.

    Definitions and Theorems

    Function: tree-info-for-error

    (defun tree-info-for-error (tree)
      (declare (xargs :guard (treep tree)))
      (let ((__function__ 'tree-info-for-error))
        (declare (ignorable __function__))
        (tree-case tree
                   :leafterm (list :leafterm tree.get)
                   :leafrule (list :leafrule tree.get)
                   :nonleaf (list :nonleaf
                                  tree.rulename? (len tree.branches)))))

    Theorem: tree-info-for-error-of-tree-fix-tree

    (defthm tree-info-for-error-of-tree-fix-tree
      (equal (tree-info-for-error (tree-fix tree))
             (tree-info-for-error tree)))

    Theorem: tree-info-for-error-tree-equiv-congruence-on-tree

    (defthm tree-info-for-error-tree-equiv-congruence-on-tree
      (implies (tree-equiv tree tree-equiv)
               (equal (tree-info-for-error tree)
                      (tree-info-for-error tree-equiv)))
      :rule-classes :congruence)