• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
      • Deftreeops
      • Defdefparse
        • Defdefparse-implementation
          • Defdefparse-event-generation
          • Defdefparse-fn
          • Defdefparse-input-processing
            • Defdefparse-process-inputs
            • Defdefparse-process-name
            • Defdefparse-process-package
            • Defdefparse-process-grammar
            • Defdefparse-process-prefix
            • *defdefparse-allowed-options*
          • Defdefparse-table
          • Defdefparse-macro-definition
      • Defgrammar
      • Abnf-tree-utilities
      • Notation
      • Grammar-parser
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
      • Operations
      • Examples
      • Differences-with-paper
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defdefparse-input-processing

Defdefparse-process-inputs

Process all the inputs.

Signature

(defdefparse-process-inputs args ctx state) 
  → 
(mv erp val state)

Arguments

args — Guard (true-listp args).

ctx — Guard (ctxp ctx).

Returns

val — Type (std::tuple (name common-lisp::symbolp) (pkg-wit common-lisp::symbolp) (grammar common-lisp::symbolp) (prefix common-lisp::symbolp) val) .

If successful, we return the inputs, except that we return the package witnesss instead of the package input.

Definitions and Theorems

Function: defdefparse-process-inputs

(defun defdefparse-process-inputs (args ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args) (ctxp ctx))))
 (let ((__function__ 'defdefparse-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((fun (irr)) (list nil nil nil nil))
    ((mv erp name options)
     (partition-rest-and-keyword-args
          args *defdefparse-allowed-options*))
    ((when (or erp (not (consp name))
               (not (endp (cdr name)))))
     (er-soft+
      ctx t (irr)
      "The inputs must be the name (a symbol) ~
                   followed by the options ~&0."
      *defdefparse-allowed-options*))
    (name (car name))
    ((er name :iferr (irr))
     (defdefparse-process-name name ctx state))
    (package-option (assoc-eq :package options))
    ((unless (consp package-option))
     (er-soft+ ctx t (irr)
               "The :PACKAGE input is missing."))
    (package (cdr package-option))
    ((er pkg-wit :iferr (irr))
     (defdefparse-process-package package ctx state))
    (grammar-option (assoc-eq :grammar options))
    ((unless (consp grammar-option))
     (er-soft+ ctx t (irr)
               "The :GRAMMAR input is missing."))
    (grammar (cdr grammar-option))
    ((er grammar :iferr (irr))
     (defdefparse-process-grammar grammar ctx state))
    (prefix-option (assoc-eq :prefix options))
    ((unless (consp prefix-option))
     (er-soft+ ctx t (irr)
               "The :PREFIX input is missing."))
    (prefix (cdr prefix-option))
    ((er prefix :iferr (irr))
     (defdefparse-process-prefix prefix ctx state)))
   (value (list name pkg-wit grammar prefix)))))

Theorem: return-type-of-defdefparse-process-inputs.val

(defthm return-type-of-defdefparse-process-inputs.val
  (b* (((mv acl2::?erp ?val acl2::?state)
        (defdefparse-process-inputs args ctx state)))
    (std::tuple (name common-lisp::symbolp)
                (pkg-wit common-lisp::symbolp)
                (grammar common-lisp::symbolp)
                (prefix common-lisp::symbolp)
                val))
  :rule-classes :rewrite)

Theorem: true-listp-of-defdefparse-process-inputs.val

(defthm true-listp-of-defdefparse-process-inputs.val
  (b* (((mv acl2::?erp ?val acl2::?state)
        (defdefparse-process-inputs args ctx state)))
    (true-listp val))
  :rule-classes :type-prescription)