• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
      • Deftreeops
      • Defdefparse
      • Defgrammar
        • Defgrammar-implementation
          • Defgrammar-fn
          • Defgrammar-input-processing
            • Defgrammar-process-inputs
            • Defgrammar-process-name
            • *defgrammar-allowed-options*
          • Defgrammar-table
          • Defgrammar-event-generation
          • Defgrammar-macro-definition
      • 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

• Defgrammar-input-processing

Defgrammar-process-inputs

Process all the inputs.

Signature

(defgrammar-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) (file common-lisp::stringp) (untranslate booleanp) (well-formed booleanp) (closed booleanp) (parents defgrammar-anyp) (short defgrammar-anyp) (long defgrammar-anyp) (other-events true-listp) val) , given (true-listp args).

Definitions and Theorems

Function: defgrammar-process-inputs

(defun defgrammar-process-inputs (args ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (true-listp args) (ctxp ctx))))
 (let ((__function__ 'defgrammar-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((fun (irr))
     (list nil "" nil nil nil nil nil nil nil))
    ((mv args other-events)
     (std::split-/// ctx args))
    ((mv erp name options)
     (partition-rest-and-keyword-args
          args *defgrammar-allowed-options*))
    ((when (or erp (not (consp name))
               (not (endp (cdr name)))))
     (er-soft+
      ctx t (irr)
      "The inputs must be the constant name ~
                   followed by the options ~&0 ~
                   and possibly /// followed by other events."
      *defgrammar-allowed-options*))
    (name (car name))
    ((er & :iferr (irr))
     (defgrammar-process-name name ctx state))
    (file-option (assoc-eq :file options))
    ((unless (consp file-option))
     (er-soft+ ctx t (irr)
               "The :FILE input must be supplied."))
    (file (cdr file-option))
    ((er &)
     (ensure-value-is-string$ file "The :FILE input" t (irr)))
    (untranslate-option (assoc-eq :untranslate options))
    (untranslate (if (consp untranslate-option)
                     (cdr untranslate-option)
                   nil))
    ((er &)
     (ensure-value-is-boolean$ untranslate
                               "The :UNTRANSLATE input" t (irr)))
    (well-formed-option (assoc-eq :well-formed options))
    (well-formed (if (consp well-formed-option)
                     (cdr well-formed-option)
                   nil))
    ((er &)
     (ensure-value-is-boolean$ well-formed
                               "The :WELL-FORMED input" t (irr)))
    (closed-option (assoc-eq :closed options))
    (closed (if (consp closed-option)
                (cdr closed-option)
              nil))
    ((er &)
     (ensure-value-is-boolean$ closed "The :CLOSED input" t (irr)))
    (parents-option (assoc-eq :parents options))
    (parents (if (consp parents-option)
                 (cdr parents-option)
               :absent))
    (short-option (assoc-eq :short options))
    (short (if (consp short-option)
               (cdr short-option)
             :absent))
    (long-option (assoc-eq :long options))
    (long (if (consp long-option)
              (cdr long-option)
            :absent)))
   (value (list name file untranslate well-formed closed
                parents short long other-events)))))

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

(defthm return-type-of-defgrammar-process-inputs.val
  (implies (true-listp args)
           (b* (((mv acl2::?erp ?val acl2::?state)
                 (defgrammar-process-inputs args ctx state)))
             (std::tuple (name common-lisp::symbolp)
                         (file common-lisp::stringp)
                         (untranslate booleanp)
                         (well-formed booleanp)
                         (closed booleanp)
                         (parents defgrammar-anyp)
                         (short defgrammar-anyp)
                         (long defgrammar-anyp)
                         (other-events true-listp)
                         val)))
  :rule-classes :rewrite)

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

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