		Search-engine friendly clone of the ACL2 documentation.

Defmapping-input-processing

Defmapping-process-functions

Process the doma, domb, alpha, and beta inputs.

Signature
(defmapping-process-functions doma domb alpha beta guard-thms$ ctx state) → (mv erp result state)
Returns: result — A tuple (doma$ domb$ alpha$ beta$) satisfying (typed-tuplep pseudo-termfnp pseudo-termfnp pseudo-termfnp pseudo-termfnp result).

We call defmapping-process-function on each and then we check the constraints on the arities and numbers of results.

Definitions and Theorems

Function: defmapping-process-functions

(defun defmapping-process-functions
       (doma domb alpha beta guard-thms$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defmapping-process-functions))
  (declare (ignorable __function__))
  (b*
   (((er (list doma$ doma-arity doma-numres))
     (defmapping-process-function doma 2 guard-thms$ ctx state))
    ((er (list domb$ domb-arity domb-numres))
     (defmapping-process-function domb 3 guard-thms$ ctx state))
    ((er (list alpha$ alpha-arity alpha-numres))
     (defmapping-process-function alpha 4 guard-thms$ ctx state))
    ((er (list beta$ beta-arity beta-numres))
     (defmapping-process-function beta 5 guard-thms$ ctx state))
    ((unless (= doma-numres 1))
     (er-soft+
      ctx t nil
      "The number of results returned by the domain ~x0 ~
                   must be 1, but it is ~x1 instead."
      doma doma-numres))
    ((unless (= domb-numres 1))
     (er-soft+
      ctx t nil
      "The number of results returned by the domain ~x0 ~
                   must be 1, but it is ~x1 instead."
      domb domb-numres))
    ((unless (= alpha-arity doma-arity))
     (er-soft+
      ctx t nil
      "The arity of the conversion ~x0 ~
                   must equal the arity ~x1 of the domain ~x2, ~
                   but it is ~x3 instead."
      alpha doma-arity doma alpha-arity))
    ((unless (= alpha-numres domb-arity))
     (er-soft+
      ctx t nil
      "The number of results of the conversion ~x0 ~
                   must equal the arity ~x1 of the domain ~x2, ~
                   but it is ~x3 instead."
      alpha domb-arity domb alpha-numres))
    ((unless (= beta-arity domb-arity))
     (er-soft+
      ctx t nil
      "The arity of the conversion ~x0 ~
                   must equal the arity ~x1 of the domain ~x2, ~
                   but it is ~x3 instead."
      beta domb-arity domb beta-arity))
    ((unless (= beta-numres doma-arity))
     (er-soft+
      ctx t nil
      "The number of results of the conversion ~x0 ~
                   must equal the arity ~x1 of the domain ~x2, ~
                   but it is ~x3 instead."
      beta doma-arity doma beta-numres)))
   (value (list doma$ domb$ alpha$ beta$)))))