• 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
            • Input-files-implementation
              • Input-files-process-inputs
              • Input-files-gen-events
              • Input-files-process-preprocess-args
              • Input-files-process-inputs-and-gen-events
              • Input-files-complete-preprocess-extra-args
              • Input-files-process-ienv
              • Input-files-fn
              • Input-files-read-files
              • Input-files-process-const
              • String-stringlist-map-map-cons-values
              • Input-files-process-path
              • Input-files-process-files
              • Input-files-process-process
              • Input-files-preprocess-arg-std
              • Input-files-process-preprocess
              • Input-files-process-keep-going
              • Input-files-process-inputp
              • Input-files-preprocess-inputp
              • *input-files-allowed-options*
              • Input-files-definition
            • Input-files-prog
          • Compilation-database
          • Printer
          • Output-files
          • Abstract-syntax-operations
          • Implementation-environments
          • Abstract-syntax
          • Concrete-syntax
          • Disambiguation
          • Validation
          • Gcc-builtins
          • 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

• Input-files-implementation

Input-files-process-inputs

Process the inputs.

Signature

(input-files-process-inputs files-presentp files path preprocess 
                            preprocess-args process const-presentp 
                            const keep-going std gcc short-bytes 
                            int-bytes long-bytes long-long-bytes 
                            plain-char-signed progp state) 
 
  → 
(mv erp new-files new-path 
    preprocessor preprocess-extra-args 
    new-process new-const keep-going ienv) 

Arguments

files-presentp — Guard (booleanp files-presentp).

const-presentp — Guard (booleanp const-presentp).

progp — Guard (booleanp progp).

Returns

new-files — Type (string-listp new-files).

new-path — Type (stringp new-path).

preprocessor — Type (string-optionp preprocessor).

preprocess-extra-args — Type (or (string-listp preprocess-extra-args) (acl2::string-stringlist-mapp preprocess-extra-args)) .

new-process — Type (input-files-process-inputp new-process).

new-const — Type (symbolp new-const).

keep-going — Type (booleanp keep-going).

ienv — Type (ienvp ienv).

The preprocessor result of this function is calculated from the :preprocess input. The use of `preprocessor' vs. `preprocess' is intentional.

The other results of this function are the homonymous inputs, except that the last five inputs are combined into an implementation environment result.

Definitions and Theorems

Function: input-files-process-inputs

(defun input-files-process-inputs
       (files-presentp files path preprocess
                       preprocess-args process const-presentp
                       const keep-going std gcc short-bytes
                       int-bytes long-bytes long-long-bytes
                       plain-char-signed progp state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (booleanp files-presentp)
                              (booleanp const-presentp)
                              (booleanp progp))))
  (let ((__function__ 'input-files-process-inputs))
    (declare (ignorable __function__))
    (b* (((reterr)
          nil ""
          nil nil :parse nil nil (ienv-default))
         ((erp files)
          (input-files-process-files files-presentp files))
         ((erp path)
          (input-files-process-path path))
         ((erp preprocessor)
          (input-files-process-preprocess preprocess))
         ((erp preprocess-extra-args)
          (input-files-process-preprocess-args
               preprocessor preprocess-args state))
         ((erp process)
          (input-files-process-process process))
         ((erp const)
          (input-files-process-const const-presentp const progp))
         ((erp keep-going)
          (input-files-process-keep-going keep-going))
         ((erp ienv)
          (input-files-process-ienv
               std gcc short-bytes int-bytes long-bytes
               long-long-bytes plain-char-signed)))
      (retok files
             path preprocessor preprocess-extra-args
             process const keep-going ienv))))

Theorem: string-listp-of-input-files-process-inputs.new-files

(defthm string-listp-of-input-files-process-inputs.new-files
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (string-listp new-files))
  :rule-classes :rewrite)

Theorem: stringp-of-input-files-process-inputs.new-path

(defthm stringp-of-input-files-process-inputs.new-path
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (stringp new-path))
  :rule-classes :rewrite)

Theorem: string-optionp-of-input-files-process-inputs.preprocessor

(defthm string-optionp-of-input-files-process-inputs.preprocessor
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (string-optionp preprocessor))
  :rule-classes :rewrite)

Theorem: return-type-of-input-files-process-inputs.preprocess-extra-args

(defthm
    return-type-of-input-files-process-inputs.preprocess-extra-args
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (or (string-listp preprocess-extra-args)
        (acl2::string-stringlist-mapp preprocess-extra-args)))
  :rule-classes :rewrite)

Theorem: input-files-process-inputp-of-input-files-process-inputs.new-process

(defthm
 input-files-process-inputp-of-input-files-process-inputs.new-process
 (b* (((mv acl2::?erp
           ?new-files ?new-path ?preprocessor
           ?preprocess-extra-args ?new-process
           ?new-const ?keep-going ?ienv)
       (input-files-process-inputs
            files-presentp files path preprocess
            preprocess-args process const-presentp
            const keep-going std gcc short-bytes
            int-bytes long-bytes long-long-bytes
            plain-char-signed progp state)))
   (input-files-process-inputp new-process))
 :rule-classes :rewrite)

Theorem: symbolp-of-input-files-process-inputs.new-const

(defthm symbolp-of-input-files-process-inputs.new-const
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (symbolp new-const))
  :rule-classes :rewrite)

Theorem: booleanp-of-input-files-process-inputs.keep-going

(defthm booleanp-of-input-files-process-inputs.keep-going
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (booleanp keep-going))
  :rule-classes :rewrite)

Theorem: ienvp-of-input-files-process-inputs.ienv

(defthm ienvp-of-input-files-process-inputs.ienv
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (ienvp ienv))
  :rule-classes :rewrite)

Theorem: string-listp-of-input-files-process-inputs.preprocess-extra-args

(defthm
   string-listp-of-input-files-process-inputs.preprocess-extra-args
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (implies
         (not (acl2::string-stringlist-mapp preprocess-extra-args))
         (string-listp preprocess-extra-args))))

Theorem: string-stringlist-mapp-of-input-files-process-inputs.preprocess-extra-args

(defthm
 string-stringlist-mapp-of-input-files-process-inputs.preprocess-extra-args
 (b* (((mv acl2::?erp
           ?new-files ?new-path ?preprocessor
           ?preprocess-extra-args ?new-process
           ?new-const ?keep-going ?ienv)
       (input-files-process-inputs
            files-presentp files path preprocess
            preprocess-args process const-presentp
            const keep-going std gcc short-bytes
            int-bytes long-bytes long-long-bytes
            plain-char-signed progp state)))
   (implies (not (string-listp preprocess-extra-args))
            (acl2::string-stringlist-mapp preprocess-extra-args))))

Theorem: input-files-process-inputs.new-process

(defthm input-files-process-inputs.new-process
  (b* (((mv acl2::?erp
            ?new-files ?new-path ?preprocessor
            ?preprocess-extra-args ?new-process
            ?new-const ?keep-going ?ienv)
        (input-files-process-inputs
             files-presentp files path preprocess
             preprocess-args process const-presentp
             const keep-going std gcc short-bytes
             int-bytes long-bytes long-long-bytes
             plain-char-signed progp state)))
    (implies (not erp)
             (equal new-process process))))