• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
      • Deftreeops
      • Defdefparse
      • Defgrammar
      • Tree-utilities
      • Notation
        • Syntax-abstraction
        • Semantics
          • Tree-terminatedp
          • Tree->string
          • String-has-finite-parse-trees-p
          • Parse-trees-of-string-p
          • Tree-match-element-p
          • Parse-treep
          • Symbol
          • String-unambiguousp
          • Tree-match-num-val-p
          • Nat-match-insensitive-char-p
          • Nats-match-insensitive-chars-p
          • Tree-option
          • String-parsablep
          • Lookup-rulename
          • Nats-match-sensitive-chars-p
          • Numrep-match-repeat-range-p
          • Tree-match-char-val-p
          • Tree-list-match-repetition-p
          • String-ambiguousp
          • Parse
          • Tree-match-prose-val-p
          • Nat-match-sensitive-char-p
          • Theorems-about-terminated-trees-matching-elements
          • Tree-option-result
          • Tree-list-result
          • Tree-list-list-result
          • Tree-result
          • Tree-list-list-match-concatenation-p
          • Languagep
          • Terminal-string-for-rules-p
          • Tree-list-list-match-alternation-p
          • Tree-list-match-element-p
          • Parse!
          • String
          • Tree-set
          • Trees
        • Abstract-syntax
        • 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

Semantics

Semantics of ABNF.

The abstract syntactic entities of ABNF denote tree structures built by expanding the rules. When all the rule names are expanded, the leaves of the tree form a sequence of terminal values, for which the tree is a parse tree.

These concepts are analogous to the ones for the typical notion of formal grammar in textbooks, but because ABNF is more complex, its semantics are more complex.

Subtopics

Tree-terminatedp

Notion of terminated tree.

Tree->string

String at the leaves of trees.

String-has-finite-parse-trees-p

Check if a string has a finite number of parse trees.

Parse-trees-of-string-p

Check if a finite set of trees is the set of all and only the parse trees of a string.

Tree-match-element-p

Semantics of elements.

Parse-treep

Recognize the parse trees of a string, with respect to a rule name and a list of rules.

Symbol

Symbols.

String-unambiguousp

Notion of unambiguous string.

Tree-match-num-val-p

Semantics of numeric value notations.

Nat-match-insensitive-char-p

Semantics of characters in case-insensitive character value notations.

Nats-match-insensitive-chars-p

Lifting of nat-match-insensitive-char-p to lists.

Tree-option

Union of trees and nil.

String-parsablep

Notion of parsable string.

Lookup-rulename

Collect all the alternatives associated to a rule name from some rules.

Nats-match-sensitive-chars-p

Lifting of nat-match-sensitive-char-p to lists.

Numrep-match-repeat-range-p

Semantics of repetition ranges.

Tree-match-char-val-p

Semantics of character value notations.

Tree-list-match-repetition-p

Semantics of repetitions.

String-ambiguousp

Notion of ambiguous string.

Parse

Parse a string.

Tree-match-prose-val-p

Semantics of prose value notations.

Nat-match-sensitive-char-p

Semantics of characters in case-sensitive character value notations.

Theorems-about-terminated-trees-matching-elements

Some theorems about terminated trees matching certain elements.

Tree-option-result

Fixtype of errors and optional trees.

Tree-list-result

Fixtype of errors and lists of trees.

Tree-list-list-result

Fixtype of errors and lists of lists of trees.

Tree-result

Fixtype of errors and trees.

Tree-list-list-match-concatenation-p

Semantics of concatenations.

Languagep

Notion of language.

Terminal-string-for-rules-p

Recognize terminal strings generated by a grammar.

Tree-list-list-match-alternation-p

Semantics of alternations.

Tree-list-match-element-p

Auxiliary function to define tree-list-match-repetition-p.

Parse!

Parse an unambiguous string.

String

Strings.

Tree-set

Finite sets of trees.

Trees