		Search-engine friendly clone of the ACL2 documentation.

Context

Make-context

Basic constructor macro for context structures.

Syntax

(make-context [:tops <tops>] 
              [:types <types>] 
              [:functions <functions>] 
              [:variables <variables>] 
              [:obligation-vars <obligation-vars>] 
              [:obligation-hyps <obligation-hyps>])

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

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

Definition

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

Macro: make-context

(defmacro make-context (&rest args)
  (std::make-aggregate 'context
                       args
                       '((:tops)
                         (:types)
                         (:functions)
                         (:variables)
                         (:obligation-vars)
                         (:obligation-hyps))
                       'make-context
                       nil))

Function: context

(defun context (tops types functions variables
                     obligation-vars obligation-hyps)
  (declare
       (xargs :guard (and (toplevel-listp tops)
                          (identifier-listp types)
                          (function-header-listp functions)
                          (variable-contextp variables)
                          (typed-variable-listp obligation-vars)
                          (obligation-hyp-listp obligation-hyps))))
  (declare (xargs :guard t))
  (let ((__function__ 'context))
    (declare (ignorable __function__))
    (b* ((tops (mbe :logic (toplevel-list-fix tops)
                    :exec tops))
         (types (mbe :logic (identifier-list-fix types)
                     :exec types))
         (functions (mbe :logic (function-header-list-fix functions)
                         :exec functions))
         (variables (mbe :logic (variable-context-fix variables)
                         :exec variables))
         (obligation-vars
              (mbe :logic (typed-variable-list-fix obligation-vars)
                   :exec obligation-vars))
         (obligation-hyps
              (mbe :logic (obligation-hyp-list-fix obligation-hyps)
                   :exec obligation-hyps)))
      (list (cons 'tops tops)
            (cons 'types types)
            (cons 'functions functions)
            (cons 'variables variables)
            (cons 'obligation-vars obligation-vars)
            (cons 'obligation-hyps
                  obligation-hyps)))))