clone - ACL2 Book

other

(in-package "STOBJS")

other

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

other

(include-book "tools/rulesets" :dir :system)

other

(include-book "tools/templates" :dir :system)

other

(program)

other

(defxdoc defstobj-clone
  :parents (std/stobjs)
  :short "Create a new stobj that is @(':congruent-to') an existing (concrete
or abstract) stobj, and can be given to functions that operate on the old
stobj."
  :long "<p>@('Defstobj-clone') lets you easily introduce a new @(see stobj)
that is @(':congruent-to') an existing stobj.  This allows you to have two (or
more) copies of a stobj that coexist simultaneously.</p>

<h3>Basic Example</h3>

<p>If you want to write an algorithm that operates on two bit arrays, you might
clone the @(see bitarr) to get a second stobj, @('bitarr2').  A minimal way to
do this is:</p>

@({
    (defstobj-clone bitarr2 bitarr :suffix "2")
})

<p>This introduces:</p>

<ul>

<li>A new stobj, @('bitarr2'), which is congruent to @('bitarr'), and</li>

<li>New functions that are basically renamed @('bitarr') operations.  In
particular, whereas @('bitarr') has operations like @('get-bit') and
@('set-bit'), we'll get new functions named @('get-bit2') and
@('set-bit2').</li>

</ul>

<p>Usually you can just <b>ignore</b> these new functions.  They are added only
because of the way that ACL2 stobj definition works and, strictly speaking, are
not really necessary for anything else because you can still use the original
stobj's functions on the new stobj.</p>

<p>Ignoring the new functions is particularly useful when you have already
built up more complex functionality on top of a stobj.  That is, if you've
implemented functions like @('clear-range') and @('invert-range') or similar,
you can just use these on @('bitarr2') without reimplementing them.</p>


<h3>Renaming Accessors</h3>

<p>On the other hand, it may occasionally be useful for code clarity to rename
the new functions in some semantically meaningful way.  For instance, if your
cloned bit array will be used as a seen table, it may be convenient to use
operations like @('set-seen') instead of @('set-bit').</p>

<p>To support using such semantically meaningful names, @('defstobj-clone') has
a variety of options.  Here is a contrived example that uses all of them:</p>

@({
    (defstobj-clone fancy-bitarr bitarr
      :strsubst (("GET" . "FETCH")     ;; Substring replacements to make
                 ("SET" . "INSTALL"))  ;;   (capitalized per symbol names)
      :prefix "MY-"                      ;; Name prefix to add
      :suffix "-FOR-JUSTICE"             ;; Name suffix to add
      :pkg acl2::rewrite                   ;; Package for new symbols
                                           ;;   default: new stobj name
      )
})

<p>The result is to define new analogues of the @('bitarr') functions with the
following names:</p>

@({
      bitarrp       -->  fancy-bitarrp
      create-bitarr -->  create-fancy-bitarr
      bits-length   -->  my-bits-length-for-justice
      get-bit       -->  my-fetch-bit-for-justice
      set-bit       -->  my-install-bit-for-justice
      resize-bits   -->  my-resize-bits-for-justice
})


<h3>Alternate Syntax for Abstract Stobjs</h3>

<p>For an abstract stobj, the accessors/updaters are known as "exports".
Another way to specifying their names in the new stobj is to provide the
@(':exports') argument, which should be a list of symbols corresponding to the
exported functions from the original abstract stobj.  When this is provided,
the other keyword arguments are unused.  For example:</p>

@({
    (defstobj-clone xx-bitarr bitarr
      :exports (xx-size xx-nth !xx-nth xx-resize))
})

<p>Defines a new @('xx-bitarr') stobj with:</p>

@({
    bitarrp       --> xx-bitarrp
    create-bitarr --> create-xx-bitarr
    bits-length   --> xx-size
    get-bit       --> xx-nth
    set-bit       --> !xx-nth
    resize-bits   --> xx-resize
})")

clone-stobj-change-symbolfunction

(defun clone-stobj-change-symbol
  (sym renaming)
  (if renaming
    (b* (((list prefix
          suffix
          strsubst
          pkg) renaming) ((mv sub pkg?) (tmpl-str-sublis strsubst (symbol-name sym))))
      (intern-in-package-of-symbol (concatenate 'string
          prefix
          sub
          suffix)
        (or pkg? pkg)))
    sym))

clone-stobj-process-rename-alistfunction

(defun clone-stobj-process-rename-alist
  (rename-alist renaming)
  (if (atom rename-alist)
    nil
    (cons (list (clone-stobj-change-symbol (caar rename-alist)
          renaming)
        (clone-stobj-change-symbol (cadar rename-alist)
          renaming))
      (clone-stobj-process-rename-alist (cdr rename-alist)
        renaming))))

clone-stobj-process-fieldsfunction

(defun clone-stobj-process-fields
  (fields renaming)
  (if (atom fields)
    nil
    (cons (if (consp (car fields))
        (cons (clone-stobj-change-symbol (caar fields)
            renaming)
          (cdar fields))
        (clone-stobj-change-symbol (car fields)
          renaming))
      (clone-stobj-process-fields (cdr fields)
        renaming))))

keep-nonbool-symbolsfunction

(defun keep-nonbool-symbols
  (x)
  (if (atom x)
    nil
    (let* ((k (car x)))
      (if (and k (not (eq k t)) (symbolp k))
        (cons k
          (keep-nonbool-symbols (cdr x)))
        (keep-nonbool-symbols (cdr x))))))

stobj-field-template-fnnamesfunction

(defun stobj-field-template-fnnames
  (field-templates)
  (if (atom field-templates)
    nil
    (cons (caar field-templates)
      (append (keep-nonbool-symbols (cdddar field-templates))
        (stobj-field-template-fnnames (cdr field-templates))))))

stobj-template-fnnamesfunction

(defun stobj-template-fnnames
  (template)
  (list* (car template)
    (cadr template)
    (stobj-field-template-fnnames (caddr template))))

clone-stobj-process-argsfunction

(defun clone-stobj-process-args
  (stobjname args renaming)
  (b* (((mv erp
        field-descriptors
        key-alist) (partition-rest-and-keyword-args args
         *defstobj-keywords*)) ((when erp) (er hard?
          'defstobj-clone
          "The stobj to be cloned had bad keyword args~%"))
      (inline (assoc-eq :inline key-alist))
      (fields (clone-stobj-process-fields field-descriptors
          renaming)))
    (append fields
      (and inline (list :inline (cdr inline)))
      (list :congruent-to stobjname))))

clone-stobj-rewritefunction

(defun clone-stobj-rewrite
  (newfn oldfn formals)
  (let ((thmname (intern-in-package-of-symbol (concatenate 'string
           (symbol-name newfn)
           "-IS-"
           (symbol-name oldfn))
         newfn)))
    `((defthm ,STOBJS::THMNAME
       (equal (,STOBJS::NEWFN . ,STOBJS::FORMALS)
         (,STOBJS::OLDFN . ,STOBJS::FORMALS))
       :hints (("goal" :in-theory '(,STOBJS::NEWFN ,STOBJS::OLDFN)) (and stable-under-simplificationp
           '(:in-theory (e/d** (clone-stobj-tmp-rules))))
         (and stable-under-simplificationp
           '(:in-theory '(,STOBJS::NEWFN ,STOBJS::OLDFN (:induction ,STOBJS::NEWFN)))))) (local (add-to-ruleset! clone-stobj-tmp-rules
          ,STOBJS::THMNAME)))))

clone-stobj-rewritesfunction

(defun clone-stobj-rewrites
  (new old)
  (b* (((when (atom new)) nil) (newfn (caar new))
      (formals (cadar new))
      (oldfn (caar old)))
    (append (clone-stobj-rewrite newfn
        oldfn
        formals)
      (clone-stobj-rewrites (cdr new)
        (cdr old)))))

clone-base-stobj-fnfunction

(defun clone-base-stobj-fn
  (stobjname name
    renaming
    wrld)
  (b* ((ev-wrld (decode-logical-name stobjname wrld)) ((when (null ev-wrld)) (er hard?
          'defstobj-clone
          "Unrecognized stobjname: ~x0~%"
          stobjname))
      (event (access-event-tuple-form (cddar ev-wrld)))
      ((when (not (eq (car event) 'defstobj))) (er hard?
          'defstobj-clone
          "The event named ~x0 is not a defstobj event~%"
          stobjname))
      ((list* & & args) event)
      (name (or name
          (clone-stobj-change-symbol stobjname
            renaming)))
      (new-args (clone-stobj-process-args stobjname
          args
          renaming))
      (old-template (defstobj-template stobjname
          args
          wrld))
      (new-template (defstobj-template name
          new-args
          wrld))
      (old-defs (defstobj-axiomatic-defs stobjname
          old-template
          wrld))
      (new-defs (defstobj-axiomatic-defs name
          new-template
          wrld)))
    (list* 'encapsulate
      nil
      `(defstobj ,STOBJS::NAME . ,STOBJS::NEW-ARGS)
      '(local (def-ruleset! clone-stobj-tmp-rules nil))
      (clone-stobj-rewrites new-defs
        old-defs))))

clone-absstobj-exportsfunction

(defun clone-absstobj-exports
  (absstobj-tuples exports
    renaming
    foundation
    world)
  (b* (((when (atom absstobj-tuples)) nil) ((list* name
         logic
         exec
         updater) (car absstobj-tuples))
      (name-export-lookup (assoc-eq name exports))
      (new-sym (if name-export-lookup
          (cdr name-export-lookup)
          (clone-stobj-change-symbol name
            renaming)))
      (updater (and updater
          (b* ((updater-export-lookup (assoc-eq updater exports)))
            (if updater-export-lookup
              (cdr updater-export-lookup)
              (clone-stobj-change-symbol updater
                renaming)))))
      (protect (unprotected-export-p foundation
          exec
          world)))
    (cons `(,STOBJS::NEW-SYM :logic ,STOBJS::LOGIC
        :exec ,STOBJS::EXEC
        ,@(AND STOBJS::UPDATER `(:UPDATER ,STOBJS::UPDATER))
        :protect ,STOBJS::PROTECT)
      (clone-absstobj-exports (cdr absstobj-tuples)
        exports
        renaming
        foundation
        world))))

clone-absstobj-fnfunction

(defun clone-absstobj-fn
  (stobjname name
    renaming
    user-exports
    world)
  (b* ((abs-info (fgetprop stobjname
         'absstobj-info
         nil
         world)) (stobj-info (fgetprop stobjname
          'stobj
          nil
          world))
      (`(,STOBJS::FOUNDATION (,STOBJS::?!RECOG-NAME ,STOBJS::RECOG-LOGIC
           ,STOBJS::RECOG-EXEC)
         (,STOBJS::?!CREATOR-NAME ,STOBJS::CREATE-LOGIC
           ,STOBJS::CREATE-EXEC) . ,STOBJS::EXPORT-ABSSTOBJ-TUPLES) abs-info)
      (?pred (access stobj-property
          stobj-info
          :recognizer))
      (?create (access stobj-property stobj-info :creator))
      (?exports (access stobj-property stobj-info :names))
      (exports (and user-exports
          (pairlis$ (strip-cars export-absstobj-tuples)
            user-exports)))
      (creator (defstobj-fnname name :creator :top nil))
      (recognizer (defstobj-fnname name :recognizer :top nil)))
    `(defabsstobj ,STOBJS::NAME
      :foundation ,STOBJS::FOUNDATION
      :recognizer (,STOBJS::RECOGNIZER :logic ,STOBJS::RECOG-LOGIC
        :exec ,STOBJS::RECOG-EXEC)
      :creator (,STOBJS::CREATOR :logic ,STOBJS::CREATE-LOGIC
        :exec ,STOBJS::CREATE-EXEC)
      :exports ,(STOBJS::CLONE-ABSSTOBJ-EXPORTS STOBJS::EXPORT-ABSSTOBJ-TUPLES STOBJS::EXPORTS
  STOBJS::RENAMING STOBJS::FOUNDATION STOBJS::WORLD)
      :congruent-to ,STOBJS::STOBJNAME)))

clone-stobj-fnfunction

(defun clone-stobj-fn
  (stobjname name
    prefix
    suffix
    strsubst
    pkg
    exports
    world)
  (declare (xargs :guard (and (stringp prefix)
        (stringp suffix)
        (alistp strsubst)
        (string-listp (strip-cars strsubst))
        (string-listp (strip-cdrs strsubst))
        (symbol-listp exports)
        (symbolp pkg)
        (not (and (equal prefix "")
            (equal suffix "")
            (not strsubst)
            (not exports)
            (not pkg))))))
  (b* ((stobjp (fgetprop stobjname
         'stobj
         nil
         world)) (absstobjp (fgetprop stobjname
          'absstobj-info
          nil
          world))
      (pkg (or pkg name))
      (renaming (and (not exports)
          (list prefix
            suffix
            strsubst
            pkg)))
      ((unless stobjp) (er hard?
          'defstobj-clone
          "~x0 is not a stobj~%"
          stobjname)))
    (if absstobjp
      (clone-absstobj-fn stobjname
        name
        renaming
        exports
        world)
      (if exports
        (er hard?
          'defstobj-clone
          ":Exports is not supported for concrete stobjs")
        (clone-base-stobj-fn stobjname
          name
          renaming
          world)))))

defstobj-clonemacro

(defmacro defstobj-clone
  (newname origname
    &key
    strsubst
    (prefix '"")
    (suffix '"")
    pkg
    exports)
  `(make-event (clone-stobj-fn ',STOBJS::ORIGNAME
      ',STOBJS::NEWNAME
      ',STOBJS::PREFIX
      ',STOBJS::SUFFIX
      ',STOBJS::STRSUBST
      ',STOBJS::PKG
      ',STOBJS::EXPORTS
      (w state))))