• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
          • Simplify-defun
          • Isodata
          • Tailrec
          • Schemalg
            • Schemalg-implementation
              • Schemalg-event-generation
              • Schemalg-fn
              • Schemalg-macro-definition
              • Schemalg-input-processing
                • Schemalg-process-inputs
                • Schemalg-process-schema-inputs
                • Schemalg-process-divconq-list-0-1-2-inputs
                • Schemalg-process-divconq-oset-0-1-inputs
                • Schemalg-process-divconq-list-0-1-inputs
                • Schemalg-process-algo-name
                • Schemalg-process-oset-input
                • Schemalg-process-list-input
                • Schemalg-check-allowed-input
                • Schemalg-process-tail-output
                • Schemalg-process-cdr-output
                • Schemalg-process-spec-2-name
                • Schemalg-process-spec-1-name
                • Schemalg-process-spec-0-name
                • Schemalg-process-equal-algo-name
                • Schemalg-process-fvar-2-name
                • Schemalg-process-fvar-1-name
                • Schemalg-process-fvar-0-name
                • Schemalg-process-schema
                • Schemalg-process-algo-name-aux
                • *schemalg-schemas*
            • Schemalg-divconq-oset-0-1
            • Schemalg-divconq-list-0-1
          • Restrict
          • Expdata
          • Casesplit
          • Simplify-term
          • Simplify-defun-sk
          • Parteval
          • Solve
          • Wrap-output
          • Propagate-iso
          • Simplify
          • Finite-difference
          • Drop-irrelevant-params
          • Copy-function
          • Lift-iso
          • Rename-params
          • Utilities
          • Simplify-term-programmatic
          • Simplify-defun-sk-programmatic
          • Simplify-defun-programmatic
          • Simplify-defun+
          • Common-options
          • Common-concepts
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Soft
        • Bv
        • Imp-language
        • C
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Number-theory
        • Cryptography
        • Lists-light
        • Builtins
        • Axe
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Schemalg-implementation

Schemalg-input-processing

Input processing performed by schemalg.

See input processing for general background.

Subtopics

Schemalg-process-inputs
Process all the inputs.
Schemalg-process-schema-inputs
Process all the schema-specific inputs.
Schemalg-process-divconq-list-0-1-2-inputs
Process some of the schema-specific inputs when the schema is :divconq-list-0-1.
Schemalg-process-divconq-oset-0-1-inputs
Process some of the schema-specific inputs when the schema is :divconq-oset-0-1.
Schemalg-process-divconq-list-0-1-inputs
Process some of the schema-specific inputs when the schema is :divconq-list-0-1.
Schemalg-process-algo-name
Process the :algo-name input.
Schemalg-process-oset-input
Process the :oset-input input.
Schemalg-process-list-input
Process the :list-input input.
Schemalg-check-allowed-input
Check whether an input is allowed for the current schema.
Schemalg-process-tail-output
Process the :tail-output input.
Schemalg-process-cdr-output
Process the :cdr-output input.
Schemalg-process-spec-2-name
Process the :spec-2-name input.
Schemalg-process-spec-1-name
Process the :spec-1-name input.
Schemalg-process-spec-0-name
Process the :spec-0-name input.
Schemalg-process-equal-algo-name
Process the :equal-algo-name input.
Schemalg-process-fvar-2-name
Process the :fvar-2-name input.
Schemalg-process-fvar-1-name
Process the :fvar-1-name input.
Schemalg-process-fvar-0-name
Process the :fvar-0-name input.
Schemalg-process-schema
Process the :schema input.
Schemalg-process-algo-name-aux
*schemalg-schemas*
Allowed values of the :schema input.