• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • 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
            • Grammar
            • Files
              • Fileset
              • File-at-path
              • Filedata
              • Fileset-paths
              • Filepath-filedata-map
              • Irr-fileset
            • Grammar-character-p
            • Keywords
            • Grammar-character-listp
            • File-paths
          • Ascii-identifiers
          • Unambiguity
          • Preprocessing
          • Abstraction-mapping
        • 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

• Files

File-at-path

File data at a certain path in a file set.

Signature

(file-at-path path files) → data

Arguments

path — Guard (filepathp path).

files — Guard (filesetp files).

Returns

data — Type (filedatap data).

This is the value associated to the key (path) in the map, which the guard requires to be in the file set.

It is more concise, and more abstract, than accessing the map and then looking up the path.

Together with fileset-paths, it can be used an as API to inspect a file set.

Definitions and Theorems

Function: file-at-path

(defun file-at-path (path files)
  (declare (xargs :guard (and (filepathp path)
                              (filesetp files))))
  (declare (xargs :guard (in path (fileset-paths files))))
  (let ((__function__ 'file-at-path))
    (declare (ignorable __function__))
    (filedata-fix (omap::lookup (filepath-fix path)
                                (fileset->unwrap files)))))

Theorem: filedatap-of-file-at-path

(defthm filedatap-of-file-at-path
  (b* ((data (file-at-path path files)))
    (filedatap data))
  :rule-classes :rewrite)

Theorem: file-at-path-of-filepath-fix-path

(defthm file-at-path-of-filepath-fix-path
  (equal (file-at-path (filepath-fix path) files)
         (file-at-path path files)))

Theorem: file-at-path-filepath-equiv-congruence-on-path

(defthm file-at-path-filepath-equiv-congruence-on-path
  (implies (filepath-equiv path path-equiv)
           (equal (file-at-path path files)
                  (file-at-path path-equiv files)))
  :rule-classes :congruence)

Theorem: file-at-path-of-fileset-fix-files

(defthm file-at-path-of-fileset-fix-files
  (equal (file-at-path path (fileset-fix files))
         (file-at-path path files)))

Theorem: file-at-path-fileset-equiv-congruence-on-files

(defthm file-at-path-fileset-equiv-congruence-on-files
  (implies (fileset-equiv files files-equiv)
           (equal (file-at-path path files)
                  (file-at-path path files-equiv)))
  :rule-classes :congruence)