outer-local - ACL2 Book

Included Books

top bstar

other

(in-package "ACL2")

include-book

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

include-book

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

other

(defxdoc outer-local
  :parents (macro-libraries)
  :short "Support for events that are local to the outer context."
  :long "<p>Think of @('outer-local') as being like @('progn'), except that the
events inside it are local to some encapsulate context above in which they are
sitting.  Outer-local only works when paired with @('with-outer-locals'), which
is essentially like @('(encapsulate nil ...)') except that it allows
@('outer-local') events to work.</p>

<p>Example:</p>
@({
 (with-outer-locals
   (defun exported-fn ...)
   (local (defthm lemma ...))
   (defthm exported-thm ...)
   (outer-local :depth 1 (defthm book-thm ...)))
})
<p>produces, essentially:</p>
@({
 (local
  (encapsulate nil
    (defun exported-fn ...)
    (local (defthm lemma ...))
    (defthm exported-thm ...)
    (defthm book-thm ...)))
 (defun exported-fn ...)
 (defthm exported-thm ...))
})

<p>Effectively, the event marked @('outer-local') is visible in book or
encapsulate surrounding this with-outer-locals event, but local to that
context.</p>

<p>The @(':depth') argument to @('outer-local') is optional but must occur
first if it is present.  It takes a positive integer, defaulting to 1.  There
must be @('depth') nestings of @('with-outer-locals') surrounding each
outer-local invocation in order for it to work as intended; in that case, the
events inside the outer-local are local to the context @('depth') levels
outside it.</p>

<p>Note: IN-THEORY events inside outer-local probably won't act as you would
like them to, at least in the presence of nonlocal IN-THEORY events.</p>")

outer-local-pushmacro

(defmacro outer-local-push
  (&key (level '1))
  `(progn (table outer-local-event-table :action :no-op)
    (table outer-local-event-table :action '(:push . ,LEVEL))
    (value-triple :invisible)))

outer-local-popmacro

(defmacro outer-local-pop
  nil
  '(progn (table outer-local-event-table :action :no-op)
    (table outer-local-event-table :action :pop)
    (value-triple :invisible)))

outer-localmacro

(defmacro outer-local
  (&rest args)
  (b* (((mv level events) (if (eq (car args) :level)
         (if (or (atom (cdr args)) (not (posp (cadr args))))
           (progn$ (er hard?
               'outer-local
               ":level must be provided a positive integer argument")
             (mv nil nil))
           (mv (cadr args) (cddr args)))
         (if (member :level args)
           (progn$ (er hard?
               'outer-local
               ":level must occur first in an outer-local form, if given")
             (mv nil nil))
           (mv 1 args)))))
    `(with-output :off :all :stack :push (progn (outer-local-push :level ,LEVEL)
        (with-output :stack :pop (progn . ,EVENTS))
        (outer-local-pop)))))

with-outer-local-collect-eventsfunction

(defun with-outer-local-collect-events
  (world context-depth event-stack-top event-stack)
  (declare (xargs :mode :program))
  (b* (((when (atom world)) (er hard?
         'with-outer-local
         "Reached end of world while scanning")) ((unless (eq (caar world) 'event-landmark)) (with-outer-local-collect-events (cdr world)
          context-depth
          event-stack-top
          event-stack))
      (event-tuple (cddr (car world)))
      (event-depth (access-event-tuple-depth event-tuple))
      ((when (<= event-depth context-depth)) (b* (((when (consp event-stack)) (er hard?
               'with-outer-local
               "Found the previous event while still in an outer-local context")))
          event-stack-top))
      ((unless (eql event-depth (+ 1 context-depth))) (with-outer-local-collect-events (cdr world)
          context-depth
          event-stack-top
          event-stack))
      (form (access-event-tuple-form event-tuple))
      ((unless (and (eq (first form) 'table)
           (eq (second form) 'outer-local-event-table)
           (eq (third form) :action))) (with-outer-local-collect-events (cdr world)
          context-depth
          (cons form event-stack-top)
          event-stack))
      ((when (eq (fourth form) :no-op)) (with-outer-local-collect-events (cdr world)
          context-depth
          event-stack-top
          event-stack))
      ((when (eq (fourth form) :pop)) (with-outer-local-collect-events (cdr world)
          context-depth
          nil
          (cons event-stack-top event-stack)))
      ((unless (and (consp (fourth form))
           (eq (car (fourth form)) 'quote)
           (eq (car (cadr (fourth form))) ':push)
           (posp (cdr (cadr (fourth form)))))) (er hard?
          'with-outer-local
          "bad outer-local-event-table form: ~x0"
          form))
      ((unless (consp event-stack)) (er hard?
          'with-outer-local
          "event stack was empty when we reached an outer-local-push event"))
      (level (cdr (cadr (fourth form))))
      ((when (eql level 1)) (with-outer-local-collect-events (cdr world)
          context-depth
          (car event-stack)
          (cdr event-stack))))
    (with-outer-local-collect-events (cdr world)
      context-depth
      (cons `(outer-local :level ,(1- LEVEL) . ,EVENT-STACK-TOP)
        (car event-stack))
      (cdr event-stack))))

with-outer-local-eventsfunction

(defun with-outer-local-events
  (world)
  (declare (xargs :mode :program))
  (b* ((world (scan-to-event world)) (tuple (cddr (car world)))
      (context-depth (access-event-tuple-depth tuple)))
    (cons 'progn
      (with-outer-local-collect-events (cdr world)
        context-depth
        nil
        nil))))

finish-with-outer-localmacro

(defmacro finish-with-outer-local
  nil
  `(make-event (with-outer-local-events (w state))))

with-outer-localsmacro

(defmacro with-outer-locals
  (&rest events)
  `(with-output :off :all :stack :push (progn (local (with-output :stack :pop (encapsulate nil . ,EVENTS)))
      (finish-with-outer-local))))