iter - ACL2 Book

Included Books

arith-equivs defs bstar base fixtype basetypes top-with-meta

other

(in-package "ACL2")

include-book

(include-book "std/basic/arith-equivs" :dir :system)

include-book

(include-book "std/basic/defs" :dir :system)

include-book

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

include-book

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

include-book

(include-book "centaur/fty/fixtype" :dir :system)

include-book

(include-book "centaur/fty/basetypes" :dir :system)

iter-upencapsulate

(encapsulate nil
  (local (in-theory (enable* arith-equiv-forwarding)))
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (encapsulate (((iter-step * * *) => *) ((iter-first * *) => *)
      ((iter-last * *) => *)
      ((iter-fix-val *) => *))
    (set-ignore-ok t)
    (set-irrelevant-formals-ok t)
    (local (defun iter-step
        (n aux val)
        (list (update-nth n (car aux) (car val)))))
    (local (defun iter-first (aux val) (cadr aux)))
    (local (defun iter-last (aux val) (caddr aux)))
    (local (defun iter-fix-val (val) (list (car val))))
    (defthm iter-first-of-iter-step
      (equal (iter-first aux (iter-step n aux val))
        (iter-first aux val)))
    (defthm iter-last-of-iter-step
      (equal (iter-last aux (iter-step n aux val))
        (iter-last aux val)))
    (defthm iter-first-of-iter-fix
      (equal (iter-first aux (iter-fix-val val))
        (iter-first aux val)))
    (defthm iter-last-of-iter-fix
      (equal (iter-last aux (iter-fix-val val))
        (iter-last aux val)))
    (defthm iter-fix-of-iter-fix
      (equal (iter-fix-val (iter-fix-val val)) (iter-fix-val val)))
    (defthm iter-step-of-iter-fix
      (equal (iter-step n aux (iter-fix-val val))
        (iter-step n aux val)))
    (defthm iter-fix-of-iter-step
      (equal (iter-fix-val (iter-step n aux val))
        (iter-step n aux val))))
  (defun iter-up
    (n aux val)
    (declare (xargs :measure (nfix (- (ifix (iter-last aux val)) (ifix n)))))
    (if (zp (- (ifix (iter-last aux val)) (ifix n)))
      (iter-fix-val val)
      (iter-up (1+ (ifix n)) aux (iter-step (ifix n) aux val))))
  (defun iter-down
    (n aux val)
    (declare (xargs :measure (nfix (- (ifix n) (ifix (iter-first aux val))))))
    (if (zp (- (ifix n) (ifix (iter-first aux val))))
      (iter-fix-val val)
      (iter-step (1- (ifix n))
        aux
        (iter-down (1- (ifix n)) aux val))))
  (defthm iter-last-of-iter-up
    (equal (iter-last aux (iter-up n aux val))
      (iter-last aux val)))
  (defthm iter-last-of-iter-down
    (equal (iter-last aux (iter-down n aux val))
      (iter-last aux val)))
  (defthm iter-fix-val-of-iter-up
    (equal (iter-fix-val (iter-up n aux val))
      (iter-up n aux val)))
  (defthm iter-fix-val-of-iter-down
    (equal (iter-fix-val (iter-down n aux val))
      (iter-down n aux val))
    :hints (("goal" :induct (iter-down n aux val))))
  (defthm iter-up-of-iter-fix-val
    (equal (iter-up n aux (iter-fix-val val))
      (iter-up n aux val)))
  (defthm iter-down-of-iter-fix-val
    (equal (iter-down n aux (iter-fix-val val))
      (iter-down n aux val)))
  (defthm iter-up-of-iter-down
    (implies (and (<= (ifix n) (ifix (iter-last aux val)))
        (<= (ifix (iter-first aux val)) (ifix n)))
      (equal (iter-up n aux (iter-down n aux val))
        (iter-up (iter-first aux val) aux val)))
    :hints (("goal" :induct (iter-down n aux val)
       :expand ((:free (val) (iter-up n aux val))))))
  (defthm iter-up-is-iter-down
    (equal (iter-up (iter-first aux val) aux val)
      (iter-down (iter-last aux val) aux val))
    :hints (("goal" :use ((:instance iter-up-of-iter-down (n (iter-last aux val))))
       :in-theory (disable iter-up-of-iter-down)) (and stable-under-simplificationp
        '(:expand ((iter-down (iter-last aux val) aux val)))))))

defiteration-sort-argsfunction

(defun defiteration-sort-args
  (args)
  (cond ((atom args) (prog2$ (er hard? 'defiteration "not enough args")
        (mv nil nil nil nil)))
    ((and (consp (car args)) (eq (caar args) 'declare)) (b* (((mv decls doc body kwlist) (defiteration-sort-args (cdr args))))
        (mv (cons (car args) decls) doc body kwlist)))
    ((stringp (car args)) (b* (((when (keyword-value-listp (cdr args))) (mv nil nil (car args) (cdr args))) ((mv decls doc body kwlist) (defiteration-sort-args (cdr args)))
          ((when doc) (er hard? 'defiteration "multiple doc strings")
            (mv nil nil nil nil)))
        (mv decls (car args) body kwlist)))
    ((keyword-value-listp (cdr args)) (mv nil nil (car args) (cdr args)))
    (t (prog2$ (er hard?
          'defiteration
          "args after body not keyword-value-listp")
        (mv nil nil nil nil)))))

get-kwfunction

(defun get-kw
  (key default kwlist)
  (declare (xargs :guard (keyword-value-listp kwlist)))
  (let ((look (assoc-keyword key kwlist)))
    (if look
      (cadr look)
      default)))

var/const-listpfunction

(defun var/const-listp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (eq x nil)
    (and (or (atom (car x)) (eq (caar x) 'quote))
      (var/const-listp (cdr x)))))

defiteration-fnfunction

(defun defiteration-fn
  (name formals args)
  (b* (((mv decls doc body kwlist) (defiteration-sort-args args)) (first (get-kw :first 0 kwlist))
      (last (get-kw :last nil kwlist))
      ((unless last) (er hard? 'defiteration "Need :last argument"))
      (index (get-kw :index (intern-in-package-of-symbol "N" name)
          kwlist))
      ((when (member index formals)) (er hard?
          'defiteration
          "Index variable (~x0) must not be in formals"
          index))
      (init-vals (get-kw :init-vals nil kwlist))
      (init-val-vars (strip-cars init-vals))
      ((unless (and (symbol-listp init-val-vars)
           (not (member-eq index init-val-vars))
           (not (intersectp-eq init-val-vars formals)))) (er hard?
          'defiteration
          "May not assign initial values to formals or index var"))
      (returns (get-kw :returns nil kwlist))
      ((unless returns) (er hard? 'defiteration "Must specify :returns"))
      ((unless (if (symbolp returns)
           (or (member returns formals) (member returns init-val-vars))
           (and (symbol-listp returns)
             (eq (car returns) 'mv)
             (consp (cdr returns))
             (subsetp-eq (set-difference-eq (cdr returns) formals)
               init-val-vars)))) (er hard?
          'defiteration
          "Returns must be either a variable symbol or ~
                                 MV of variable symbols, with each symbol ~
                                 either a formal or given an initial value in ~
                                 :init-vals"))
      (hints (get-kw :hints nil kwlist))
      (iter-guard (get-kw :iter-guard t kwlist))
      (iter-decls (get-kw :iter-decls nil kwlist))
      (top-guard (get-kw :top-guard t kwlist))
      (top-returns (get-kw :top-returns nil kwlist))
      (guard-hints (get-kw :guard-hints nil kwlist))
      (package (get-kw :package name kwlist))
      (val-vars (if (symbolp returns)
          (list returns)
          (cdr returns)))
      (aux-vars (set-difference-eq (append formals init-val-vars) val-vars))
      (body-is-simple (or (atom body)
          (and (symbolp (car body)) (var/const-listp (cdr body)))))
      (iter-formals (cons index (append init-val-vars formals)))
      (step-call (if body-is-simple
          body
          (cons (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-STEP")
              package)
            iter-formals)))
      (step (car step-call))
      (tailrec (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-TAILREC")
          package))
      (iter (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-ITER")
          package))
      (iter-meas (if (equal first 0)
          index
          `(- (ifix ,INDEX) (ifix ,FIRST))))
      (thmname (intern-in-package-of-symbol (concatenate 'string
            (symbol-name tailrec)
            "-IS-"
            (symbol-name iter))
          package)))
    `(encapsulate nil
      ,@(AND (NOT BODY-IS-SIMPLE)
       `((DEFUN-INLINE ,STEP ,ITER-FORMALS
                       (DECLARE
                        (TYPE
                         (INTEGER
                          ,(IF (INTEGERP FIRST)
                               FIRST
                               (QUOTE *))
                          ,(IF (INTEGERP LAST)
                               LAST
                               (QUOTE *)))
                         ,INDEX)
                        (IGNORABLE ,INDEX ,@INIT-VAL-VARS . ,FORMALS)
                        (XARGS :GUARD-HINTS ,GUARD-HINTS)
                        . ,ITER-DECLS)
                       ,@DECLS
                       (DECLARE
                        (XARGS :GUARD
                         (AND (<= ,FIRST ,INDEX) (< ,INDEX ,LAST)
                              ,ITER-GUARD)))
                       ,BODY)))
      (defund ,TAILREC
        ,ITER-FORMALS
        (declare (type (integer ,(IF (INTEGERP FIRST)
     FIRST
     '*)
              ,(IF (INTEGERP LAST)
     LAST
     '*))
            ,INDEX)
          (xargs :measure (nfix (- (ifix ,LAST) (ifix ,INDEX)))) . ,ITER-DECLS)
        ,@DECLS
        (declare (xargs :guard (and (<= ,FIRST ,INDEX) (<= ,INDEX ,LAST) ,ITER-GUARD)))
        (b* (((when (mbe :logic (zp (- (ifix ,LAST) (ifix ,INDEX)))
                :exec (int= ,LAST ,INDEX))) ,RETURNS) (,INDEX (lifix ,INDEX))
            (,RETURNS ,STEP-CALL))
          (,TAILREC (1+ ,INDEX) . ,(CDR ITER-FORMALS))))
      (defund ,ITER
        ,ITER-FORMALS
        (declare (type (integer ,(IF (INTEGERP FIRST)
     FIRST
     '*)
              ,(IF (INTEGERP LAST)
     LAST
     '*))
            ,INDEX)
          (xargs :measure (nfix ,ITER-MEAS) :verify-guards nil) . ,ITER-DECLS)
        ,@DECLS
        (declare (xargs :guard (and (<= ,FIRST ,INDEX) (<= ,INDEX ,LAST) ,ITER-GUARD)))
        (b* (((when (mbe :logic (zp ,ITER-MEAS) :exec (int= ,FIRST ,INDEX))) ,RETURNS) (,INDEX (1- (lifix ,INDEX)))
            (,RETURNS (,ITER . ,ITER-FORMALS)))
          ,STEP-CALL))
      (deffixcong int-equiv
        equal
        (,ITER . ,ITER-FORMALS)
        ,INDEX
        :hints (("goal" :in-theory (enable ,ITER))))
      (encapsulate nil
        (set-ignore-ok t)
        (defthm ,THMNAME
          (equal (,TAILREC ,FIRST . ,(CDR ITER-FORMALS))
            (,ITER ,LAST . ,(CDR ITER-FORMALS)))
          :hints (("goal" :use ((:instance (:functional-instance iter-up-is-iter-down
                  (iter-fix-val (lambda (val) (b* ((,RETURNS val)) ,RETURNS)))
                  (iter-first (lambda (aux val)
                      (b* (((list . ,AUX-VARS) aux) (,RETURNS val)) ,FIRST)))
                  (iter-last (lambda (aux val)
                      (b* (((list . ,AUX-VARS) aux) (,RETURNS val)) ,LAST)))
                  (iter-step (lambda (n aux val)
                      (b* (((list . ,AUX-VARS) aux) (,RETURNS val) (,INDEX n))
                        ,STEP-CALL)))
                  (iter-up (lambda (n aux val)
                      (b* (((list . ,AUX-VARS) aux) (,RETURNS val))
                        (,TAILREC n . ,(CDR ITER-FORMALS)))))
                  (iter-down (lambda (n aux val)
                      (b* (((list . ,AUX-VARS) aux) (,RETURNS val))
                        (,ITER n . ,(CDR ITER-FORMALS))))))
                (aux (list . ,AUX-VARS))
                (val ,RETURNS)))
             :in-theory '(,ITER ,TAILREC
               car-cons
               cdr-cons
               zp-when-integerp
               commutativity-of-+
               (equal)
               (ifix)
               (unary--)
               (zp)
               ifix-positive-to-non-zp
               unicity-of-0
               fix
               lnfix
               lifix
               (:type-prescription ifix))
             :do-not-induct t) ,@HINTS
            (and stable-under-simplificationp '(:in-theory (enable))))))
      ,@(AND TOP-RETURNS '((SET-IGNORE-OK T)))
      (defun-inline ,NAME
        ,FORMALS
        ,@(IF DOC
      (LIST DOC)
      NIL)
        ,@DECLS
        ,@(AND TOP-GUARD `((DECLARE (XARGS :GUARD ,TOP-GUARD))))
        ,(IF TOP-RETURNS
     `(B*
       (,@INIT-VALS
        (,RETURNS
         (MBE :LOGIC (,ITER ,LAST . ,(CDR ITER-FORMALS)) :EXEC
              (,TAILREC ,FIRST . ,(CDR ITER-FORMALS)))))
       ,TOP-RETURNS)
     `(B* ,INIT-VALS
       (MBE :LOGIC (,ITER ,LAST . ,(CDR ITER-FORMALS)) :EXEC
            (,TAILREC ,FIRST . ,(CDR ITER-FORMALS))))))
      (in-theory (enable (:induction ,ITER))))))

other

(defxdoc defiteration
  :parents (programming)
  :short "Define a simple for-loop-style iteration, counting up over some
range."
  :long "<p>This macro defines the logic version of this loop as a
non-tail-recursive function that counts down from the maximum value to the
minimum value.  This is often better for reasoning with.  The executable
version is a function that counts up from the minimum to the maximum value and
is tail-recursive, which may be better for execution, especially in terms of
avoiding stack overflows.</p>

<p>Syntax:</p>

@({
    (defiteration function-name (a b c)
      "optional doc string"
      (declare ...)        ;; optional declare forms
      (body idx-var a b c) ;; one step of the iteration
      :returns (mv b c)    ;; or a single variable, must be from the formals
      :index idx-var       ;; counter variable
      :first (foo a b)     ;; starting index, default 0
      :last  (bar a c)     ;; final index
      :hints ...           ;; optional, for proving that tailrec and non-tailrec
                           ;; are the same
      :guard-hints ...     ;; for defining the step function
      :package foo)        ;; package witness symbol, default is function-name
})")

defiterationmacro

(defmacro defiteration
  (name formals &rest args)
  (defiteration-fn name formals args))

local

(local (progn (defiteration countup
      (a b)
      (declare (xargs :guard (and (natp a) (acl2-numberp b))))
      (1+ b)
      :returns b
      :last a)
    (defiteration countup-from
      (s a b)
      (declare (xargs :guard (and (natp a) (natp s) (<= s a) (acl2-numberp b))))
      (1+ b)
      :index nn
      :returns b
      :first s
      :last a)
    (defiteration countup-more
      (s a b)
      (declare (xargs :guard (and (natp a) (natp s) (<= s a) (acl2-numberp b))))
      (+ nn b)
      :index nn
      :returns b
      :first s
      :last a)
    (defiteration countup-2
      (s a b c)
      (declare (xargs :guard (and (natp a)
            (natp s)
            (<= s a)
            (acl2-numberp b)
            (acl2-numberp c))))
      (mv (+ nn b) (- c nn))
      :index nn
      :returns (mv b c)
      :first s
      :last a)
    (defiteration countup-3
      (s a c)
      (declare (xargs :guard (and (natp a) (natp s) (<= s a) (acl2-numberp c))))
      (mv (+ nn b) (- c nn))
      :index nn
      :returns (mv b c)
      :first s
      :last a
      :init-vals ((b 0))
      :iter-guard (acl2-numberp b))))

other

(defstub listconstr-val (n formals) nil)

other

(defstub listconstr-last (formals) nil)

other

(defiteration listconstr
  (formals)
  (declare (xargs :verify-guards nil))
  (let ((val (listconstr-val n formals)))
    (update-nth n val lst))
  :returns lst
  :last (listconstr-last formals)
  :init-vals ((lst nil))
  :iter-guard (true-listp lst))

nth-of-listconstr-itertheorem

(defthm nth-of-listconstr-iter
  (equal (nth m (listconstr-iter n nil formals))
    (and (< (nfix m) (nfix n))
      (listconstr-val (nfix m) formals)))
  :hints (("goal" :induct (listconstr-iter n nil formals)
     :expand ((listconstr-iter n nil formals)))))

len-of-listconstr-itertheorem

(defthm len-of-listconstr-iter
  (equal (len (listconstr-iter n nil formals)) (nfix n))
  :hints (("goal" :induct (listconstr-iter n nil formals)
     :expand ((listconstr-iter n nil formals)))))

true-listp-of-listconstr-itertheorem

(defthm true-listp-of-listconstr-iter
  (true-listp (listconstr-iter n nil formals))
  :hints (("goal" :induct (listconstr-iter n nil formals)
     :expand ((listconstr-iter n nil formals)))))

nth-of-listconstrtheorem

(defthm nth-of-listconstr
  (equal (nth n (listconstr formals))
    (let ((n (nfix n)))
      (and (< n (nfix (listconstr-last formals)))
        (listconstr-val n formals)))))

len-of-listconstrtheorem

(defthm len-of-listconstr
  (equal (len (listconstr formals))
    (nfix (listconstr-last formals))))

true-listp-of-listconstrtheorem

(defthm true-listp-of-listconstr
  (true-listp (listconstr formals)))

def-list-constructor-fnfunction

(defun def-list-constructor-fn
  (name formals args)
  (b* (((mv decls doc body kwlist) (defiteration-sort-args args)) (index (get-kw :index (intern-in-package-of-symbol "N" name)
          kwlist))
      ((when (member index formals)) (er hard?
          'def-list-constructor
          "Index variable (~x0) must not be in formals"
          index))
      (list-var (get-kw :list-var (intern-in-package-of-symbol "LST" name)
          kwlist))
      ((when (member list-var formals)) (er hard?
          'def-list-constructor
          "List variable (~x0) must not be in formals"
          list-var))
      (length (get-kw :length nil kwlist))
      ((unless length) (er hard? 'def-list-constructor "Need :length argument"))
      (iter-guard (get-kw :iter-guard t kwlist))
      (package (get-kw :package name kwlist))
      (iter (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-ITER")
          package))
      (tailrec (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-TAILREC")
          package))
      (iter-formals (cons index (cons list-var formals)))
      (step-call (cons (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-STEP")
            package)
          iter-formals))
      (step (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-STEP")
          package))
      (?nth-thmname (intern-in-package-of-symbol (concatenate 'string "NTH-OF-" (symbol-name name))
          package))
      (nth-split-thmname (intern-in-package-of-symbol (concatenate 'string "NTH-OF-" (symbol-name name) "-SPLIT")
          package))
      (?true-listp-thmname (intern-in-package-of-symbol (concatenate 'string "TRUE-LISTP-OF-" (symbol-name name))
          package))
      (?len-thmname (intern-in-package-of-symbol (concatenate 'string "LEN-OF-" (symbol-name name))
          package))
      (fsubst `((listconstr-val (lambda (n formals)
             (b* (((list . ,FORMALS) formals) (,INDEX n)) ,BODY))) (listconstr-last (lambda (formals)
              (b* (((list . ,FORMALS) formals)) ,LENGTH)))
          (listconstr-step$inline (lambda (n lst formals)
              (b* (((list . ,FORMALS) formals) (,INDEX n) (,LIST-VAR lst))
                ,STEP-CALL)))
          (listconstr-iter (lambda (n lst formals)
              (b* (((list . ,FORMALS) formals) (,INDEX n) (,LIST-VAR lst))
                (,ITER . ,ITER-FORMALS))))
          (listconstr-tailrec (lambda (n lst formals)
              (b* (((list . ,FORMALS) formals) (,INDEX n) (,LIST-VAR lst))
                (,TAILREC . ,ITER-FORMALS))))
          (listconstr$inline (lambda (formals)
              (b* (((list . ,FORMALS) formals)) (,NAME . ,FORMALS)))))))
    `(encapsulate nil
      (set-ignore-ok t)
      (set-irrelevant-formals-ok t)
      (defiteration ,NAME
        ,FORMALS
        ,@DECLS
        ,@(AND DOC (LIST DOC))
        (let ((val ,BODY))
          (update-nth ,INDEX val ,LIST-VAR))
        :returns ,LIST-VAR
        :first 0
        :last ,LENGTH
        :init-vals ((,LIST-VAR nil))
        :iter-guard (and (true-listp ,LIST-VAR) ,ITER-GUARD) . ,KWLIST)
      (in-theory (disable ,NAME))
      (defthmd ,NTH-SPLIT-THMNAME
        (equal (nth ,INDEX (,NAME . ,FORMALS))
          (let ((,INDEX (nfix ,INDEX)))
            (and (< ,INDEX (nfix ,LENGTH)) ,BODY)))
        :hints (("goal" :use ((:instance (:functional-instance nth-of-listconstr . ,FSUBST)
              (formals (list . ,FORMALS))
              (n ,INDEX)))
           :in-theory '(,ITER ,STEP
             ,NAME
             ,TAILREC
             car-cons
             cdr-cons
             zp-when-integerp
             commutativity-of-+
             (equal)
             (ifix)
             (unary--)
             (zp)
             ifix-positive-to-non-zp
             unicity-of-0
             fix
             (:type-prescription ifix))
           :do-not-induct t)))
      (defthm ,NTH-THMNAME
        (implies (< (nfix ,INDEX) (nfix ,LENGTH))
          (equal (nth ,INDEX (,NAME . ,FORMALS))
            (let ((,INDEX (nfix ,INDEX)))
              ,BODY)))
        :hints (("Goal" :in-theory (enable ,NTH-SPLIT-THMNAME))))
      (defthm ,LEN-THMNAME
        (equal (len (,NAME . ,FORMALS)) (nfix ,LENGTH))
        :hints (("goal" :use ((:instance (:functional-instance len-of-listconstr . ,FSUBST)
              (formals (list . ,FORMALS))))
           :in-theory '(car-cons cdr-cons))))
      (defthm ,TRUE-LISTP-THMNAME
        (true-listp (,NAME . ,FORMALS))
        :hints (("goal" :use ((:instance (:functional-instance true-listp-of-listconstr . ,FSUBST)
              (formals (list . ,FORMALS))))
           :in-theory '(car-cons cdr-cons)))
        :rule-classes (:rewrite :type-prescription)))))

other

(defxdoc def-list-constructor
  :parents (programming)
  :short "Define function that constructs a list, just by giving the length and
how to compute the Nth element in terms of the formals and index."
  :long "<p>This takes many of the same arguments as @(see defiteration), and in fact
it uses defiteration.  But instead of giving the step function for the
iteration, you give the value of the Nth element of the list.  You must also
provide the keyword :last, giving the length of the list.</p>

<p>What you end up with is your top-level function, definition disabled, and
four rules:</p>

<ul>
<li>@('nth-of-fnname') tells what the Nth element is, for N in bounds</li>
<li>@('nth-of-fnname-split') (disabled), tells what the Nth element is,
    causing a case-split on whether it's in bounds or not</li>
<li>@('len-of-fnname'): gives the length of the list</li>
<li>@('true-listp-of-fnname') shows that the list is true-listp.</li>
</ul>

<p>See @('centaur/misc/equal-by-nths') for a strategy that proves equivalences
between lists based on length and Nth value.</p>

<p>Syntax:</p>

@({
    (def-list-constructor foo (x y)
      "optional doc string"
      (declare (xargs ...))   ;; optional declare forms
      (+ idx-var x y)         ;; value of the IDX-VARth element
      :length  (bar x y)      ;; final index
      :index idx-var          ;; counter variable, default N
      ... defiteration args ...)
})")

def-list-constructormacro

(defmacro def-list-constructor
  (name formals &rest args)
  (def-list-constructor-fn name formals args))

local

(local (def-list-constructor foo
    (x y)
    (declare (xargs :guard (and (natp x) (natp y))))
    (+ n x y)
    :length x))