• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
        • Deftreeops
        • Defdefparse
        • Defgrammar
        • Tree-utilities
        • Notation
          • Syntax-abstraction
          • Semantics
          • Abstract-syntax
            • Convenience-constructors
            • Num-val
            • Char-val
            • Repeat-range
            • Rulename
            • Rule
            • Rulename-option
            • Num-base
            • Rule-option
            • Prose-val
            • Rulelist
            • Char-val-set
            • Rulename-set
            • Rulename-list
            • Grammar
            • Alt/conc/rep/elem
          • Core-rules
          • Concrete-syntax
        • 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
      • Taspi
      • Bitcoin
      • Riscv
      • 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
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Notation

Abstract-syntax

Abstract syntax of ABNF.

ABNF is a language to describe the concrete syntax of languages. Being itself a language, ABNF has its own concrete syntax, described in [RFC:4] using ABNF itself. To break the self-description circularity, we start by formalizing an abstract syntax of ABNF, based on an inspection of the concrete syntax in [RFC:4]. The ABNF abstract syntax abstracts away from the ABNF concrete syntax things that are not relevant to the ABNF semantics, such as blank space and comments, as well as certain restrictions that are not needed to define the semantics.

Subtopics

Convenience-constructors
Utilities to conveniently construct abstract syntactic entities.
Num-val
Fixtype of numeric value notations.
Char-val
Fixtype of character value notations.
Repeat-range
Fixtype of repetition ranges.
Rulename
Fixtype of rule names.
Rule
Fixtype of rules.
Rulename-option
Fixtype of rule names and nil.
Num-base
Fixtype of numeric bases.
Rule-option
Fixtype of rules and nil.
Prose-val
Fixtype of prose value notations.
Rulelist
Fixtype of lists of rules.
Char-val-set
Fixtype of sets of character value notations.
Rulename-set
Finite sets of rule names.
Rulename-list
Fixtype of lists of rule names.
Grammar
An ABNF grammar is a list of rules.
Alt/conc/rep/elem