• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Error-checking
        • Apt
        • Abnf
          • Defdefparse
          • Deftreeops
          • Defgrammar
          • Notation
          • Grammar-parser
          • Meta-circular-validation
          • Parsing-primitives-defresult
          • Parsing-primitives-seq
            • Parse-exact-list
            • Parse-in-range
            • Parse-exact
            • Parse-any
          • Operations
          • Differences-with-paper
          • Examples
          • Grammar-printer
          • Parsing-tools
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Prime-field-constraint-systems
        • Soft
        • Bv
        • Imp-language
        • Event-macros
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Java
        • C
        • Syntheto
        • Number-theory
        • Cryptography
        • Lists-light
        • File-io-light
        • Json
        • Built-ins
        • Solidity
        • Axe
        • Std-extensions
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Execloader
      • Axe
    • Testing-utilities
    • Math
  • Abnf

Parsing-primitives-seq

Some basic ABNF parsing functions for use with Seq.

These functions may be useful when writing Seq-based parsers for languages specified via ABNF grammars. These functions take lists of natural numbers as inputs and return outputs of the form prescribed for Seq actions.

These parsing functions are somewhat similar to the fty::defresult-based parsing primitives, but they have an interface suitable for Seq instead of an interface suitable for fty::defresult.

These parsing functions are being moved here from the ABNF grammar parser: they are used by the ABNF grammar parser, but they are more general.

Subtopics

Parse-exact-list
Parse zero or more given natural numbers into a tree that matches a direct numeric value notation that consists of that list of numbers.
Parse-in-range
Parse a natural number in a given range into a tree that matches a range numeric value notation that consists of that range.
Parse-exact
Parse a given natural number into a tree that matches a direct numeric value notation that consists of that number.
Parse-any
Parse any natural number.