tuple

(in-package "STD")

(include-book "std/util/define" :dir :system)

(include-book "xdoc/constructors" :dir :system)

(defsection tuple
  :parents (returns-specifiers)
  :short "A way to use @(tsee mv)-like return specifiers for tuples."
  :long (topstring (p (seetopic "returns-specifiers" "Return specifiers")
      " support individual names and types (and hypothes, etc.)
     for components of @(tsee mv) results.
     However, when a function returns an "
      (seetopic "acl2::error-triple" "error triple")
      " whose value (i.e. middle component) consists of multiple results,
     given that the error triple already consists of multiple results
     (three: the error, the value, and the state),
     it is not possible to use the @(tsee mv) return specifier notation
     for the value of the error triple.")
    (p "So here we provide a macro, called @('tuple'),
     to mimic the @(tsee mv) return specifier notation
     for a single value, such as the middle component of an error triple.")
    (p "The macro call")
    (codeblock "(tuple (var1 type1)"
      "       ..."
      "       (varn typen)"
      "       x)")
    (p "where each @('vari') is a variable symbol,
     each @('typei') is a predicate symbol or a term over @('vari'),
     and @('x') is a variable symbol,
     expands to")
    (codeblock "(and (tuplep n x)"
      "     (b* (((list var1 ... varn) x))"
      "       (and (type1 var1)"
      "            ..."
      "            (typen varn))))")
    (p "where each @('(typei vari)') is as shown if @('typei') is a symbol,
     otherwise we use the term @('typei') instead.")
    (p "This lets us write return specifiers of the form")
    (codeblock ":returns (mv erp"
      "             (val (tuple (var1 type1) ... (varn typen) val))"
      "             state)")
    (p "where we can use the call @('(tuple ...)') as the type of @('val'),
     so that the expansion will express that @('val') is an @('n')-tuple
     whose components have the specified types.")
    (p "We may extend this macro with support for
     @(':hyp') and other features of return specifiers.")
    (p "The macro is in the @('STD') package,
     but we also add a synonym in the @('ACL2') package.")
    (@def "tuple")
    (@def "acl2::tuple"))
  (define tuple-fn
    ((args true-listp))
    :returns (mv vars conjuncts)
    (b* (((when (endp args)) (mv nil nil)) (arg (car args))
        ((unless (tuplep 2 arg)) (mv nil nil))
        (var (first arg))
        (type (second arg))
        (conjunct (if (symbolp type)
            (list type var)
            type))
        ((mv vars conjuncts) (tuple-fn (cdr args))))
      (mv (cons var vars)
        (cons conjunct conjuncts))))
  (defmacro tuple
    (&rest args)
    (b* ((var (car (last args))) (comps (butlast args 1))
        ((mv vars conjuncts) (tuple-fn comps)))
      `(and (tuplep ,(STD::LEN STD::COMPS) ,STD::VAR)
        (b* (((list ,@STD::VARS) ,STD::VAR))
          (and ,@STD::CONJUNCTS)))))
  (defmacro tuple (&rest args) `(tuple ,@STD::ARGS)))