• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-read-files
        • Vl-find-file
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Loader

Vl-find-basename/extension

Alternative to vl-find-file that can take a list of extensions.

Signature: (vl-find-basename/extension filename extensions searchpath warnings state) returns (mv realname warnings state).

Definitions and Theorems

Function: vl-find-basename/extension-aux

(defun
     vl-find-basename/extension-aux
     (filename extensions dir state)
     (declare (xargs :guard (and (stringp filename)
                                 (string-listp extensions)
                                 (stringp dir)
                                 (state-p state))))
     (b* (((when (atom extensions))
           (mv nil state))
          ((mv rest state)
           (vl-find-basename/extension-aux filename (cdr extensions)
                                           dir state))
          (filename1 (cat filename "." (car extensions)))
          (attempt (vl-extend-pathname dir filename1))
          ((mv channel state)
           (open-input-channel attempt
                               :character state))
          (state (if channel
                     (close-input-channel channel state)
                     state)))
         (mv (if channel (cons attempt rest) rest)
             state)))

Theorem: true-listp-of-vl-find-basename/extension-aux

(defthm
 true-listp-of-vl-find-basename/extension-aux
 (true-listp
  (mv-nth
    0
    (vl-find-basename/extension-aux filename extensions dir state)))
 :rule-classes :type-prescription)

Theorem: state-p1-of-vl-find-basename/extension-aux

(defthm
  state-p1-of-vl-find-basename/extension-aux
  (implies (force (state-p1 state))
           (state-p1 (mv-nth 1
                             (vl-find-basename/extension-aux
                                  filename extensions dir state)))))

Theorem: string-listp-of-vl-find-basename/extension-aux

(defthm
 string-listp-of-vl-find-basename/extension-aux
 (string-listp
  (mv-nth
   0
   (vl-find-basename/extension-aux filename extensions dir state))))

Function: vl-find-basename/extension

(defun
 vl-find-basename/extension
 (filename extensions searchpath warnings state)
 (declare (xargs :guard (and (stringp filename)
                             (string-listp extensions)
                             (string-listp searchpath)
                             (vl-warninglist-p warnings)
                             (state-p state))))
 (b*
  (((when (atom searchpath))
    (mv nil warnings state))
   ((mv hits state)
    (vl-find-basename/extension-aux
         filename extensions (car searchpath)
         state))
   ((unless hits)
    (vl-find-basename/extension filename extensions (cdr searchpath)
                                warnings state))
   (warnings
    (if
     (atom (cdr hits))
     warnings
     (cons
      (make-vl-warning
       :type :vl-ambiguous-load
       :msg
       "Loading ~x0 based on extension order, but there are ~
                       also other matching files in this directory: ~&1."
       :args (list (car hits) (cdr hits))
       :fatalp nil
       :fn 'vl-find-basename/extension)
      warnings))))
  (mv (car hits) warnings state)))

Theorem: state-p1-of-vl-find-basename/extension

(defthm
 state-p1-of-vl-find-basename/extension
 (implies
  (force (state-p1 state))
  (state-p1
     (mv-nth
          2
          (vl-find-basename/extension filename extensions
                                      searchpath warnings state)))))

Theorem: vl-warninglist-p-of-vl-find-basename/extension

(defthm
 vl-warninglist-p-of-vl-find-basename/extension
 (implies
  (force (vl-warninglist-p warnings))
  (vl-warninglist-p
     (mv-nth
          1
          (vl-find-basename/extension filename extensions
                                      searchpath warnings state)))))

Theorem: stringp-of-vl-find-basename/extension

(defthm
 stringp-of-vl-find-basename/extension
 (equal
      (stringp (mv-nth 0
                       (vl-find-basename/extension
                            filename
                            extensions searchpath warnings state)))
      (if (mv-nth 0
                  (vl-find-basename/extension
                       filename
                       extensions searchpath warnings state))
          t nil))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (or
    (not (mv-nth 0
                 (vl-find-basename/extension
                      filename
                      extensions searchpath warnings state)))
    (stringp
     (mv-nth
        0
        (vl-find-basename/extension filename extensions
                                    searchpath warnings state)))))))