• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • 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
      • Aleobft
      • Aleovm
      • Leo
        • Grammar
        • Early-version
          • Json2ast
          • Testing
          • Definition
            • Flattening
            • Abstract-syntax
            • Dynamic-semantics
            • Compilation
            • Static-semantics
            • Concrete-syntax
              • Pretty-printer
              • Grammar
              • Lexing-and-parsing
                • Lexer
                • Parser
                  • Parse-symbol-among
                  • Parse-keyword
                  • Parse-named-primitive-type
                  • Parse-rest-of-struct-component-expression
                  • Parse-rest-of-tuple-component-expression
                  • Parse-transition-declaration
                  • Parse-named-type-as-identifier-?-dot-record
                  • Parse-named-type-as-locator-?-dot-record
                  • Parse-assert-not-equal-call
                  • Parse-symbol
                  • Parse-struct-component-declarations
                  • Parse-assert-equal-call
                  • Parse-transition-or-function-declaration
                  • Parse-string-literal
                  • Parse-group-coordinate
                  • Parse-function-declaration
                  • Parse-finalizer
                  • Parse-*-comma-struct-component-declaration
                  • Parse-increment-statement
                  • Parse-function-parameter
                  • Parse-decrement-statement
                  • Parse-struct-component-declaration
                  • Parse-variable-declaration
                  • Parse-mapping-declaration
                  • Parse-function-parameters
                  • Parse-constant-declaration
                  • Parse-assert-call
                  • Parse-*-comma-function-parameter
                  • Parse-program-declaration
                  • Parse-affine-group-literal
                  • Parse-variable-or-free-constant
                  • Parse-struct-declaration
                  • Parse-record-declaration
                  • Parse-finalize-statement
                  • Parse-associated-constant
                  • Parse-numeral
                  • Parse-import-declaration
                  • Parse-identifier
                  • Parse-console-statement
                  • Parse-annotation
                  • Parse-return-statement
                  • Parse-program-item
                  • Parse-assignment-operator
                  • Parse-*-import-declaration
                  • Parse-unit-expression
                  • Parse-named-type
                  • Parse-console-call
                  • Parse-*-comma-natural
                  • Parse-program-id
                  • Parse-atomic-literal
                  • Parse-?-output-type
                  • Parse-unit-type
                  • Parse-*-program-item
                  • Parse-locator
                  • Parse-?-finalizer
                  • Parse-*-annotation
                  • Parse-primary-expression
                  • Parse-literal
                  • Parse-?-comma
                  • Parse-file
                  • Parsize
                  • Check-token-string
                  • Check-token-root
                  • Parse-postfix-expression-rest
                  • Parse-postfix-expression
                  • Parse-token
                  • Token-stringp
                  • Token-rootp
                  • Patbind-pok<
                  • Parse-rest-of-operator-call
                  • Parse-exclusive-disjunctive-expression-rest
                  • Parse-conditional-disjunctive-expression-rest
                  • Parse-conditional-conjunctive-expression-rest
                  • Parse-shift-expression-rest
                  • Parse-multiplicative-expression-rest
                  • Parse-disjunctive-expression-rest
                  • Parse-conjunctive-expression-rest
                  • Parse-additive-expression-rest
                  • Parse-*-statement
                  • Parse-*-comma-type
                  • Parse-*-comma-struct-component-initializer
                  • Parse-*-comma-expression
                  • Parse-unary-expression
                  • Parse-tuple-expression
                  • Parse-struct-expression
                  • Parse-struct-component-initializer
                  • Parse-static-function-call
                  • Parse-shift-expression
                  • Parse-ordering-expression
                  • Parse-multiplicative-expression
                  • Parse-function-arguments
                  • Parse-free-function-call
                  • Parse-exponential-expression
                  • Parse-exclusive-disjunctive-expression
                  • Parse-equality-expression
                  • Parse-disjunctive-expression
                  • Parse-conjunctive-expression
                  • Parse-conditional-ternary-expression
                  • Parse-conditional-statement
                  • Parse-conditional-disjunctive-expression
                  • Parse-conditional-conjunctive-expression
                  • Parse-binary-expression
                  • Parse-additive-expression
                  • Parse-type
                  • Parse-tuple-type
                  • Parse-statement
                  • Parse-loop-statement
                  • Parse-expression
                  • Parse-branch
                  • Parse-block
                  • Patbind-pok
                  • Perr
                • Token-fringe
                • Longest-lexp
                • Parser-interface
                • Grammar-lexp
                • Identifier-lexp
                • Output-file-parsep
                • Input-file-parsep
                • File-lex-parse-p
                • Filter-tokens
                • Lexp
                • File-parsep
                • Input-parser
                • Output-file-lex-parse-p
                • Input-file-lex-parse-p
                • Parser-abstractor-interface
                • Identifier-abnf-stringp
                • Symbol-abnf-stringp
                • Keyword-abnf-stringp
                • Output-parser
                • Tokenizer
              • Input-pretty-printer
              • Output-pretty-printer
              • Unicode-characters
              • Concrete-syntax-trees
              • Symbols
              • Keywords
    • 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

• Parser

Token-rootp

Check if the given token has the given rule name as root.

Signature

(token-rootp rulename token) → yes/no

Arguments

rulename — Guard (stringp rulename).

token — Guard (abnf::tree-optionp token).

Returns

yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: token-rootp

(defun token-rootp (rulename token)
  (declare (xargs :guard (and (stringp rulename)
                              (abnf::tree-optionp token))))
  (let ((__function__ 'token-rootp))
    (declare (ignorable __function__))
    (abnf-tree-with-root-p (abnf::tree-option-fix token)
                           rulename)))

Theorem: booleanp-of-token-rootp

(defthm booleanp-of-token-rootp
  (b* ((yes/no (token-rootp rulename token)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: token-nonnil-when-rootp

(defthm token-nonnil-when-rootp
  (implies (token-rootp string token)
           token)
  :rule-classes :forward-chaining)

Theorem: token-rootp-of-str-fix-rulename

(defthm token-rootp-of-str-fix-rulename
  (equal (token-rootp (str-fix rulename) token)
         (token-rootp rulename token)))

Theorem: token-rootp-streqv-congruence-on-rulename

(defthm token-rootp-streqv-congruence-on-rulename
  (implies (acl2::streqv rulename rulename-equiv)
           (equal (token-rootp rulename token)
                  (token-rootp rulename-equiv token)))
  :rule-classes :congruence)

Theorem: token-rootp-of-tree-option-fix-token

(defthm token-rootp-of-tree-option-fix-token
  (equal (token-rootp rulename (abnf::tree-option-fix token))
         (token-rootp rulename token)))

Theorem: token-rootp-tree-option-equiv-congruence-on-token

(defthm token-rootp-tree-option-equiv-congruence-on-token
  (implies (abnf::tree-option-equiv token token-equiv)
           (equal (token-rootp rulename token)
                  (token-rootp rulename token-equiv)))
  :rule-classes :congruence)