		Search-engine friendly clone of the ACL2 documentation.

Stmt-gin

Make-stmt-gin

Basic constructor macro for stmt-gin structures.

Syntax

(make-stmt-gin [:context <context>] 
               [:var-term-alist <var-term-alist>] 
               [:typed-formals <typed-formals>] 
               [:inscope <inscope>] 
               [:loop-flag <loop-flag>] 
               [:affect <affect>] 
               [:fn <fn>] 
               [:fn-guard <fn-guard>] 
               [:compst-var <compst-var>] 
               [:fenv-var <fenv-var>] 
               [:limit-var <limit-var>] 
               [:prec-fns <prec-fns>] 
               [:prec-tags <prec-tags>] 
               [:prec-objs <prec-objs>] 
               [:thm-index <thm-index>] 
               [:names-to-avoid <names-to-avoid>] 
               [:proofs <proofs>])

This is the usual way to construct stmt-gin structures. It simply conses together a structure with the specified fields.

This macro generates a new stmt-gin structure from scratch. See also change-stmt-gin, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-stmt-gin

(defmacro make-stmt-gin (&rest args)
  (std::make-aggregate 'stmt-gin
                       args
                       '((:context)
                         (:var-term-alist)
                         (:typed-formals)
                         (:inscope)
                         (:loop-flag)
                         (:affect)
                         (:fn)
                         (:fn-guard)
                         (:compst-var)
                         (:fenv-var)
                         (:limit-var)
                         (:prec-fns)
                         (:prec-tags)
                         (:prec-objs)
                         (:thm-index)
                         (:names-to-avoid)
                         (:proofs))
                       'make-stmt-gin
                       nil))

Function: stmt-gin

(defun stmt-gin (context var-term-alist
                         typed-formals inscope loop-flag
                         affect fn fn-guard compst-var fenv-var
                         limit-var prec-fns prec-tags prec-objs
                         thm-index names-to-avoid proofs)
 (declare
      (xargs :guard (and (atc-contextp context)
                         (symbol-pseudoterm-alistp var-term-alist)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (atc-symbol-varinfo-alist-listp inscope)
                         (booleanp loop-flag)
                         (symbol-listp affect)
                         (symbolp fn)
                         (symbolp fn-guard)
                         (symbolp compst-var)
                         (symbolp fenv-var)
                         (symbolp limit-var)
                         (atc-symbol-fninfo-alistp prec-fns)
                         (atc-string-taginfo-alistp prec-tags)
                         (atc-string-objinfo-alistp prec-objs)
                         (posp thm-index)
                         (symbol-listp names-to-avoid)
                         (booleanp proofs))))
 (declare (xargs :guard t))
 (let ((__function__ 'stmt-gin))
  (declare (ignorable __function__))
  (b*
   ((context (mbe :logic (atc-context-fix context)
                  :exec context))
    (var-term-alist
         (mbe :logic (symbol-pseudoterm-alist-fix var-term-alist)
              :exec var-term-alist))
    (typed-formals
         (mbe :logic (atc-symbol-varinfo-alist-fix typed-formals)
              :exec typed-formals))
    (inscope (mbe :logic (atc-symbol-varinfo-alist-list-fix inscope)
                  :exec inscope))
    (loop-flag (mbe :logic (acl2::bool-fix loop-flag)
                    :exec loop-flag))
    (affect (mbe :logic (symbol-list-fix affect)
                 :exec affect))
    (fn (mbe :logic (symbol-fix fn) :exec fn))
    (fn-guard (mbe :logic (symbol-fix fn-guard)
                   :exec fn-guard))
    (compst-var (mbe :logic (symbol-fix compst-var)
                     :exec compst-var))
    (fenv-var (mbe :logic (symbol-fix fenv-var)
                   :exec fenv-var))
    (limit-var (mbe :logic (symbol-fix limit-var)
                    :exec limit-var))
    (prec-fns (mbe :logic (atc-symbol-fninfo-alist-fix prec-fns)
                   :exec prec-fns))
    (prec-tags (mbe :logic (atc-string-taginfo-alist-fix prec-tags)
                    :exec prec-tags))
    (prec-objs (mbe :logic (atc-string-objinfo-alist-fix prec-objs)
                    :exec prec-objs))
    (thm-index (mbe :logic (pos-fix thm-index)
                    :exec thm-index))
    (names-to-avoid (mbe :logic (symbol-list-fix names-to-avoid)
                         :exec names-to-avoid))
    (proofs (mbe :logic (acl2::bool-fix proofs)
                 :exec proofs)))
   (list (cons 'context context)
         (cons 'var-term-alist var-term-alist)
         (cons 'typed-formals typed-formals)
         (cons 'inscope inscope)
         (cons 'loop-flag loop-flag)
         (cons 'affect affect)
         (cons 'fn fn)
         (cons 'fn-guard fn-guard)
         (cons 'compst-var compst-var)
         (cons 'fenv-var fenv-var)
         (cons 'limit-var limit-var)
         (cons 'prec-fns prec-fns)
         (cons 'prec-tags prec-tags)
         (cons 'prec-objs prec-objs)
         (cons 'thm-index thm-index)
         (cons 'names-to-avoid names-to-avoid)
         (cons 'proofs proofs)))))