• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • 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
        • C
          • Syntax-for-tools
            • Formalized-subset
            • Mapping-to-language-definition
            • Input-files
            • Compilation-database
            • Printer
            • Output-files
            • Abstract-syntax-operations
            • Implementation-environments
            • Abstract-syntax
            • Concrete-syntax
            • Disambiguation
            • Validation
            • Gcc-builtins
            • Preprocessing
              • Preprocessor
                • Preprocessor-states
                • Pread-token/newline
                • Pread-token
                • Preprocessor-lexer
                • Pproc-files
                • Preprocessor-printer
                • Pproc-file
                • Filepath-plexeme-list-alist-to-filepath-filedata-map
                • Filepath-plexeme-list-alist
                  • Filepath-plexeme-list-alistp
                  • Filepath-plexeme-list-alist-fix
                  • Filepath-plexeme-list-alist-equiv
                • Preprocessor-reader
                • Preprocessor-messages
              • External-preprocessing
            • Parsing
          • Atc
          • Transformation-tools
          • Language
          • Representation
          • Insertion-sort
          • Pack
        • Soft
        • Bv
        • Imp-language
        • Ethereum
        • Event-macros
        • Java
        • Riscv
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Axe
        • Lists-light
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Preprocessor

Filepath-plexeme-list-alist

Fixtype of alists from file paths to lists of preprocessing lexemes.

We use these alists to keep track of which files have been already preprocessed, namely the ones whose paths are the keys of the alist. The values associated to the keys are the lexemes resulting from the preprocessing.

These alists always have unique keys, i.e. there are no shadowed pairs. This is not enforced in this fixtype, but we could consider wrapping the alist into a fty::defprod with the invariant.

Subtopics

Filepath-plexeme-list-alistp
Recognizer for filepath-plexeme-list-alist.
Filepath-plexeme-list-alist-fix
(filepath-plexeme-list-alist-fix x) is an ACL2::fty alist fixing function that follows the fix-keys strategy.
Filepath-plexeme-list-alist-equiv
Basic equivalence relation for filepath-plexeme-list-alist structures.