• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
            • Disambiguator
            • Abstract-syntax
            • Parser
            • Validator
            • Printer
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Defpred
            • Output-files
            • Abstract-syntax-operations
            • Validation-information
            • Implementation-environments
            • Concrete-syntax
            • Unambiguity
            • Ascii-identifiers
            • Preprocessing
            • Abstraction-mapping
              • Abs-uppercase-letter
              • Abs-lowercase-letter
              • Abs-letter
              • Abs-digit
          • Atc
          • Language
          • Representation
          • Transformation-tools
          • Insertion-sort
          • Pack
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Syntax-for-tools

Abstraction-mapping

Syntax abstraction mapping.

We define the mapping from concrete syntax to abstract syntax. The mapping maps concrete syntax trees (CSTs), which are defined by the ABNF grammar, to abstract syntax trees (ASTs), which are defined as fixtypes in the abstract syntax, or to data that is part of those ASTs.

This mapping formalizes the relation between concrete and abstract syntax. In particular, it is needed to express formal properties of our parser and printer.

The definition of this syntax abstraction mapping is work in progress.

Subtopics

Abs-uppercase-letter
Abstract an uppercase-letter CST to an ACL2 uppercase letter character.
Abs-lowercase-letter
Abstract a lowercase-letter CST to an ACL2 lowercase letter character.
Abs-letter
Abstract a letter CST to an ACL2 letter character.
Abs-digit
Abstract a digit CST to an ACL2 digit character.