Filtering...

nicestobj

books/std/stobjs/nicestobj
other
(in-package "STOBJS")
other
(include-book "std/util/da-base" :dir :system)
other
(include-book "std/util/defenum" :dir :system)
other
(include-book "tools/templates" :dir :system)
other
(include-book "updater-independence")
other
(program)
other
(defconst *nicestobj-field-userkeys*
  '(:key :type :pred :fix :rule-classes :initially :resizable :fieldname :access :base-access :update :base-update :resize :length :recognizer :boundp :access? :remove :count :clear :init :elementp-of-nil))
other
(defconst *nicestobj-field-keys*
  (append '(:name :arrayp :hashp :elt-type :renaming :stobjp)
    *nicestobj-field-userkeys*))
kwd-alist-field-accessor-alistfunction
(defun kwd-alist-field-accessor-alist
  (keys)
  (if (atom keys)
    nil
    (cons (cons (car keys)
        `(lambda (x)
          (cdr (assoc-eq ,(CAR STOBJS::KEYS) x))))
      (kwd-alist-field-accessor-alist (cdr keys)))))
other
(make-event (da-make-binder-gen 'nicestobj-field
    (kwd-alist-field-accessor-alist *nicestobj-field-keys*)))
kwd-alist-add-defaultmacro
(defmacro kwd-alist-add-default
  (key val kwd-alist)
  `(if (assoc ,STOBJS::KEY ,STOBJS::KWD-ALIST)
    ,STOBJS::KWD-ALIST
    (cons (cons ,STOBJS::KEY ,STOBJS::VAL) ,STOBJS::KWD-ALIST)))
member-eq-treefunction
(defun member-eq-tree
  (x tree)
  (declare (xargs :guard (symbolp x)))
  (if (atom tree)
    (eq x tree)
    (or (member-eq-tree x (car tree))
      (member-eq-tree x (cdr tree)))))
congruent-stobj-predfunction
(defun congruent-stobj-pred
  (x wrld)
  (b* ((stobj (or (fgetprop x
           'congruent-stobj-rep
           nil
           wrld)
         x)) (prop (fgetprop stobj 'stobj nil wrld)))
    (and prop
      (access stobj-property prop :recognizer))))
remove-redundant-pairsfunction
(defun remove-redundant-pairs
  (x)
  (if (atom x)
    nil
    (if (eq (caar x) (cdar x))
      (remove-redundant-pairs (cdr x))
      (cons (car x)
        (remove-redundant-pairs (cdr x))))))
parse-nicestobj-fieldfunction
(defun parse-nicestobj-field
  (stobjname field wrld)
  (b* ((__function__ 'parse-nicestobj-field) ((unless (and (consp field)
           (symbolp (car field))
           (keyword-value-listp (cdr field)))) (raise "Malformed nicestobj field: ~x0~%"
          field))
      (name (car field))
      (args (cdr field))
      ((mv kwd-alist rest) (extract-keywords `(nicestobj-field ,STOBJS::NAME)
          *nicestobj-field-userkeys*
          args
          nil))
      ((when rest) (raise "Malformed nicestobj field: ~x0  Remaining after keyword extraction: ~x1~%"
          field
          rest))
      (kwd-alist (cons (cons :name name) kwd-alist))
      (kwd-alist (kwd-alist-add-default :type t kwd-alist))
      (type (cdr (assoc :type kwd-alist)))
      ((when (and (consp type)
           (member-eq (car type) '(hash-table)))) (raise "Nicestobj doesn't support hash-table fields yet~%"))
      (arrayp (and (consp type) (eq (car type) 'array)))
      (elt-type (if (and (consp type)
            (member-eq (car type) '(array hash-table)))
          (cadr type)
          type))
      (type-pred (translate-declaration-to-guard elt-type
          name
          nil))
      (stobj-pred (and (not type-pred)
          (symbolp elt-type)
          (congruent-stobj-pred elt-type wrld)))
      (type-pred-expr (or type-pred
          (and stobj-pred
            `(,STOBJS::STOBJ-PRED ,STOBJS::NAME))))
      (type-pred-fn (and type-pred-expr
          (member-eq-tree name type-pred-expr)
          `(lambda (,STOBJS::NAME) ,STOBJS::TYPE-PRED-EXPR)))
      (kwd-alist (cons (cons :elt-type elt-type) kwd-alist))
      (kwd-alist (cons (cons :stobjp stobj-pred) kwd-alist))
      (kwd-alist (cons (cons :arrayp arrayp) kwd-alist))
      (kwd-alist (kwd-alist-add-default :key (intern-in-package-of-symbol (symbol-name name)
            :foo)
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :pred type-pred-fn
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :rule-classes :rewrite kwd-alist))
      (kwd-alist (kwd-alist-add-default :fieldname (intern-in-package-of-symbol (concatenate 'string
              (symbol-name stobjname)
              "->"
              (symbol-name name))
            stobjname)
          kwd-alist))
      (fieldname (cdr (assoc :fieldname kwd-alist)))
      (kwd-alist (kwd-alist-add-default :access (intern-in-package-of-symbol (concatenate 'string
              (symbol-name stobjname)
              "->"
              (symbol-name name)
              (if arrayp
                "I"
                ""))
            stobjname)
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :base-access (if (cdr (assoc :fix kwd-alist))
            (intern-in-package-of-symbol (concatenate 'string
                (symbol-name stobjname)
                "->"
                (symbol-name name)
                (if arrayp
                  "I"
                  "")
                "^")
              stobjname)
            (cdr (assoc :access kwd-alist)))
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :update (intern-in-package-of-symbol (concatenate 'string
              "UPDATE-"
              (symbol-name stobjname)
              "->"
              (symbol-name name)
              (if arrayp
                "I"
                ""))
            stobjname)
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :base-update (if (and (cdr (assoc :fix kwd-alist))
              (not stobj-pred))
            (intern-in-package-of-symbol (concatenate 'string
                "UPDATE-"
                (symbol-name stobjname)
                "->"
                (symbol-name name)
                (if arrayp
                  "I"
                  "")
                "^")
              stobjname)
            (cdr (assoc :update kwd-alist)))
          kwd-alist))
      (kwd-alist (if arrayp
          (kwd-alist-add-default :length (intern-in-package-of-symbol (concatenate 'string
                (symbol-name stobjname)
                "->"
                (symbol-name name)
                "-LENGTH")
              stobjname)
            kwd-alist)
          kwd-alist))
      (kwd-alist (if arrayp
          (kwd-alist-add-default :resize (intern-in-package-of-symbol (concatenate 'string
                "RESIZE-"
                (symbol-name stobjname)
                "->"
                (symbol-name name))
              stobjname)
            kwd-alist)
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :recognizer (intern-in-package-of-symbol (concatenate 'string
              (symbol-name stobjname)
              "->"
              (symbol-name name)
              "P")
            stobjname)
          kwd-alist))
      (array-key (if arrayp
          :array :non-array))
      (kwd-alist (cons (cons :renaming (remove-redundant-pairs (append (and arrayp
                  (list (cons (defstobj-fnname fieldname :length :array nil)
                      (cdr (assoc :length kwd-alist)))
                    (cons (defstobj-fnname fieldname :resize :array nil)
                      (cdr (assoc :resize kwd-alist)))))
                (list (cons (defstobj-fnname fieldname
                      :accessor array-key
                      nil)
                    (cdr (assoc :base-access kwd-alist)))
                  (cons (defstobj-fnname fieldname
                      :updater array-key
                      nil)
                    (cdr (assoc :base-update kwd-alist)))
                  (cons (defstobj-fnname fieldname
                      :recognizer array-key
                      nil)
                    (cdr (assoc :recognizer kwd-alist)))))))
          kwd-alist)))
    kwd-alist))
parse-nicestobj-fieldsfunction
(defun parse-nicestobj-fields
  (stobjname fields wrld)
  (if (atom fields)
    nil
    (cons (parse-nicestobj-field stobjname
        (car fields)
        wrld)
      (parse-nicestobj-fields stobjname
        (cdr fields)
        wrld))))
nicestobj-field-templatefunction
(defun nicestobj-field-template
  (field stobjname lastp)
  (b* (((nicestobj-field field)))
    (make-tmplsubst :features (append (if field.fix
          '(:fix)
          '(:no-fix))
        (if field.pred
          '(:pred)
          '(:no-pred))
        (if field.stobjp
          '(:stobjp)
          '(:not-stobjp))
        (if field.arrayp
          '(:arrayp)
          '(:not-arrayp))
        (if field.resizable
          '(:resizable)
          '(:not-resizable))
        (if field.elementp-of-nil
          '(:elementp-of-nil)
          '(:not-elementp-of-nil)))
      :atoms `((<field> . ,STOBJS::FIELD.NAME) (<fieldname> . ,STOBJS::FIELD.FIELDNAME)
        (<stobjname> . ,STOBJS::STOBJNAME)
        (:<field> . ,STOBJS::FIELD.KEY)
        (:<fieldcase> . ,(IF STOBJS::LASTP
     T
     STOBJS::FIELD.KEY))
        (<type> . ,STOBJS::FIELD.TYPE)
        (<elt-type> . ,STOBJS::FIELD.ELT-TYPE)
        (<initially> . ,STOBJS::FIELD.INITIALLY)
        (<pred> . ,STOBJS::FIELD.PRED)
        (<fix> . ,STOBJS::FIELD.FIX)
        (<access> . ,STOBJS::FIELD.ACCESS)
        (<update> . ,STOBJS::FIELD.UPDATE)
        (<length> . ,STOBJS::FIELD.LENGTH)
        (<resize> . ,STOBJS::FIELD.RESIZE)
        (<recognizer> . ,STOBJS::FIELD.RECOGNIZER)
        (<base-access> . ,STOBJS::FIELD.BASE-ACCESS)
        (<base-update> . ,STOBJS::FIELD.BASE-UPDATE)
        (<rule-classes> . ,STOBJS::FIELD.RULE-CLASSES)
        (<resizable> . ,STOBJS::FIELD.RESIZABLE))
      :splices `((<renaming> . ,(STOBJS::PAIRLIS$ (STOBJS::STRIP-CARS STOBJS::FIELD.RENAMING)
  (STOBJS::PAIRLIS$ (STOBJS::STRIP-CDRS STOBJS::FIELD.RENAMING) NIL))))
      :strs `(("<FIELD>" . ,(SYMBOL-NAME STOBJS::FIELD.NAME)) ("<FIELDNAME>" . ,(SYMBOL-NAME STOBJS::FIELD.FIELDNAME))
        ("<ACCESS>" . ,(SYMBOL-NAME STOBJS::FIELD.ACCESS))
        ("<BASE-ACCESS>" . ,(SYMBOL-NAME STOBJS::FIELD.BASE-ACCESS))
        ("<UPDATE>" . ,(SYMBOL-NAME STOBJS::FIELD.UPDATE))
        ("<RECOGNIZER>" . ,(SYMBOL-NAME STOBJS::FIELD.RECOGNIZER))
        ,@(AND STOBJS::FIELD.ARRAYP
       `(("<LENGTH>" . ,(SYMBOL-NAME STOBJS::FIELD.LENGTH))
         ("<RESIZE>" . ,(SYMBOL-NAME STOBJS::FIELD.RESIZE)))))
      :pkg-sym stobjname)))
nicestobj-field-templatesfunction
(defun nicestobj-field-templates
  (fields stobjname)
  (if (atom fields)
    nil
    (cons (nicestobj-field-template (car fields)
        stobjname
        (atom (cdr fields)))
      (nicestobj-field-templates (cdr fields)
        stobjname))))
other
(defconst *nicestobj-userkeys*
  '(:inline :non-memoizable :fieldp :field-fix :field-equiv :get :pred :non-exec-logic))
other
(defconst *nicestobj-keys*
  (append '(:name :fields :raw-fields :template :rename-pred :non-exec-logic)
    *nicestobj-userkeys*))
other
(make-event (da-make-binder-gen 'nicestobj
    (kwd-alist-field-accessor-alist *nicestobj-keys*)))
parse-nicestobjfunction
(defun parse-nicestobj
  (stobjname rest wrld)
  (b* ((__function__ 'parse-nicestobj) ((mv kwd-alist raw-fields) (extract-keywords `(nicestobj ,STOBJS::STOBJNAME)
          *nicestobj-userkeys*
          rest
          nil))
      ((unless raw-fields) (raise "Nicestobj must have at least one field"))
      (fields (parse-nicestobj-fields stobjname
          raw-fields
          wrld))
      (field-templates (nicestobj-field-templates fields
          stobjname))
      (kwd-alist (kwd-alist-add-default :inline t kwd-alist))
      (kwd-alist (kwd-alist-add-default :non-memoizable nil
          kwd-alist))
      (default-pred (packn-pos (list stobjname "P") stobjname))
      (kwd-alist (kwd-alist-add-default :pred default-pred
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :rename-pred (not (eq (cdr (assoc :pred kwd-alist))
              default-pred))
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :fieldp (intern-in-package-of-symbol (concatenate 'string
              (symbol-name stobjname)
              "-FIELD-P")
            stobjname)
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :field-fix (let ((fieldp (cdr (assoc :fieldp kwd-alist))))
            (intern-in-package-of-symbol (concatenate 'string
                (symbol-name (strip-p-from-symbol fieldp))
                "-FIX")
              fieldp))
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :field-equiv (let ((fieldp (cdr (assoc :fieldp kwd-alist))))
            (intern-in-package-of-symbol (concatenate 'string
                (symbol-name (strip-p-from-symbol fieldp))
                "-EQUIV")
              fieldp))
          kwd-alist))
      (kwd-alist (kwd-alist-add-default :get (intern-in-package-of-symbol (concatenate 'string (symbol-name stobjname) "-GET")
            stobjname)
          kwd-alist))
      ((nicestobj x) kwd-alist)
      (template1 (make-tmplsubst :atoms `((<stobjname> . ,STOBJS::STOBJNAME) (<inline> . ,STOBJS::X.INLINE)
            (<non-memoizable> . ,STOBJS::X.NON-MEMOIZABLE)
            (<fieldp> . ,STOBJS::X.FIELDP)
            (<get> . ,STOBJS::X.GET)
            (<field-fix> . ,STOBJS::X.FIELD-FIX)
            (<field-equiv> . ,STOBJS::X.FIELD-EQUIV)
            (<stobjpred> . ,STOBJS::X.PRED))
          :strs `(("<STOBJNAME>" . ,(SYMBOL-NAME STOBJS::STOBJNAME)) ("<STOBJPRED>" . ,(SYMBOL-NAME STOBJS::X.PRED)))
          :features (append (if x.rename-pred
              '(:rename-pred)
              '(:no-rename-pred))
            (and x.non-exec-logic '(:non-exec)))
          :pkg-sym stobjname))
      (field-templates (combine-each-tmplsubst-with-default field-templates
          template1))
      (template (change-tmplsubst template1
          :subsubsts `((:fields . ,STOBJS::FIELD-TEMPLATES))))
      (kwd-alist (list* (cons :name stobjname)
          (cons :fields fields)
          (cons :raw-fields raw-fields)
          (cons :template template)
          kwd-alist)))
    kwd-alist))
other
(defconst *nicestobj-template*
  '(progn (defstobj <stobjname>
      (:@proj :fields (<fieldname> :type <type>
          (:@ :not-stobjp :initially <initially>)
          (:@ :arrayp :resizable <resizable>)))
      :renaming ((:@append :fields <renaming>))
      :inline <inline>
      :non-memoizable <non-memoizable>)
    (def-ruleset! <stobjname>-defs nil)
    (:@append :fields (:@ :fix (:@ :arrayp (defthm <recognizer>-implies-pred-nth
            (implies (and (<recognizer> x)
                (< (nfix i) (len x)))
              (<pred> (nth i x)))
            :hints (("Goal" :in-theory (enable <recognizer> nth)))))
        (define <access>
          ((:@ :arrayp (i natp)) <stobjname>)
          (:@ :arrayp :guard (< i (<length> <stobjname>)))
          :inline t
          :returns (<field> (<pred> <field>)
            :rule-classes <rule-classes>)
          (the <elt-type>
            (mbe :logic ((:@ :non-exec non-exec) (:@ (not :non-exec) progn$)
                (<fix> (<base-access> (:@ :arrayp i)
                    <stobjname>)))
              :exec (<base-access> (:@ :arrayp i)
                <stobjname>)))
          ///
          (add-to-ruleset! <stobjname>-defs <access>))
        (:@ :not-stobjp (define <update>
            ((:@ :arrayp (i natp)) (<field> (<pred> <field>)
                :type <elt-type>)
              <stobjname>)
            (:@ :arrayp :guard (< i (<length> <stobjname>)))
            :inline t
            :split-types t
            (mbe :logic (<base-update> (:@ :arrayp i)
                (<fix> <field>)
                <stobjname>)
              :exec (<base-update> (:@ :arrayp i)
                <field>
                <stobjname>))
            ///
            (add-to-ruleset! <stobjname>-defs <update>)))))
    (defenum <fieldp> ((:@proj :fields :<field>)))
    (define <get>
      ((key <fieldp>) <stobjname>)
      :non-executable t
      :hooks ((:fix :hints (("goal" :in-theory (enable <field-fix>)))))
      (case key
        (:@proj :fields (:<fieldcase> (:@ :not-arrayp (<access> <stobjname>))
            (:@ :arrayp (nth *<base-access>* <stobjname>))))))
    (defsection <stobjname>-field-basics
      (local (in-theory (enable <get>
            <field-fix>
            <stobjpred>
            (:@append :fields (:@ :fix <access> <update>)))))
      (:@append :fields (def-updater-independence-thm <access>-of-update
          (implies (equal (<get> :<field> new)
              (<get> :<field> old))
            (equal (<access> (:@ :arrayp i) new)
              (<access> (:@ :arrayp i) old))))
        (defthm <update>-preserves-others
          (implies (not (equal (<field-fix> key) :<field>))
            (equal (<get> key
                (<update> (:@ :arrayp i)
                  <field>
                  <stobjname>))
              (<get> key <stobjname>))))
        (defthm <update>-self-identity
          (implies (and (<stobjpred> <stobjname>)
              (:@ :arrayp (< (nfix i)
                  (<length> <stobjname>))))
            (equal (<update> (:@ :arrayp i)
                (<access> (:@ :arrayp i)
                  <stobjname>)
                <stobjname>)
              <stobjname>))
          :hints (("Goal" :in-theory (enable redundant-update-nth))))
        (defthm <access>-of-<update>
          (equal (<access> (:@ :arrayp i)
              (<update> (:@ :arrayp i)
                <field>
                <stobjname>))
            (:@ :fix (<fix> <field>))
            (:@ :no-fix <field>)))
        (:@ :arrayp (defthm <access>-of-<update>-diff
            (implies (not (equal (nfix i) (nfix j)))
              (equal (<access> i
                  (<update> j
                    <field>
                    <stobjname>))
                (<access> i <stobjname>))))
          (defthmd <access>-of-<update>-split
            (equal (<access> i
                (<update> j
                  <field>
                  <stobjname>))
              (if (equal (nfix i) (nfix j))
                (:@ :fix (<fix> <field>))
                (:@ :no-fix <field>)
                (<access> i <stobjname>))))
          (def-updater-independence-thm <length>-of-update
            (implies (equal (<get> :<field> new)
                (<get> :<field> old))
              (equal (<length> new)
                (<length> old))))
          (defthm <length>-of-<update>
            (implies (< (nfix i)
                (<length> <stobjname>))
              (equal (<length> (<update> i
                    <field>
                    <stobjname>))
                (<length> <stobjname>))))
          (local (defthm nth-when-<recognizer>
              (implies (and (<recognizer> x)
                  (:@ :not-elementp-of-nil (< (nfix i) (len x))))
                (<pred> (nth i x)))
              :hints (("Goal" :in-theory (enable nth)))))
          (:@ :resizable (defthm <resize>-preserves-others
              (implies (not (equal (<field-fix> key) :<field>))
                (equal (<get> key
                    (<resize> size <stobjname>))
                  (<get> key <stobjname>))))
            (defthm <length>-of-<resize>
              (equal (<length> (<resize> size <stobjname>))
                (nfix size)))))
        (:@ (and :no-fix :pred)
          (defthm <access>-type
            (implies (and (<stobjpred> <stobjname>)
                (:@ (and :arrayp :not-elementp-of-nil)
                  (< (nfix i)
                    (<length> <stobjname>))))
              (<pred> (<access> (:@ :arrayp i)
                  <stobjname>)))
            :hints (("Goal" :in-theory (enable <access>)))
            :rule-classes <rule-classes>)))
      (add-to-ruleset! <stobjname>-defs
        '(<stobjpred> (:@append :fields <base-access>
            <base-update>
            (:@ :arrayp <length> <resize>))))
      (in-theory (disable* <stobjname>-defs)))))
defnicestobj-fnfunction
(defun defnicestobj-fn
  (name args state)
  (declare (xargs :stobjs state))
  (b* (((nicestobj x) (parse-nicestobj name
         args
         (w state))))
    (template-subst-top *nicestobj-template*
      x.template)))
defnicestobjmacro
(defmacro defnicestobj
  (name &rest args)
  `(make-event (defnicestobj-fn ',STOBJS::NAME
      ',STOBJS::ARGS
      state)))
other
(logic)
other
(defthmd redundant-update-nth
  (implies (< (nfix n) (len x))
    (equal (update-nth n
        (nth n x)
        x)
      x))
  :hints (("Goal" :in-theory (enable update-nth nth))))
other
(local (defthm len-of-resize-list
    (equal (len (resize-list x size default))
      (nfix size))))
other
(local (in-theory (disable update-nth nth)))
other
(local (defnicestobj foo
    (nat :type (integer 0 *)
      :pred natp
      :fix nfix
      :initially 0
      :rule-classes :type-prescription)
    (str :type string :fix str-fix :initially "")
    (grumble :type (integer 5 *) :initially 5)
    (any :initially buz)
    (fa :type (array (integer 0 *) (0))
      :pred natp
      :fix nfix
      :initially 1
      :rule-classes :type-prescription)
    (fb :type (array string (0))
      :initially "hi"
      :rule-classes :type-prescription :resizable t)))
other
(local (defnicestobj bar
    (nat :type (integer 0 *)
      :pred natp
      :fix nfix
      :initially 0
      :rule-classes :type-prescription)
    (str :type string :fix str-fix :initially "")
    (foo :type foo)
    (grumble :type (integer 5 *) :initially 5)
    (foos :type (array foo (0)) :resizable t)
    (any :initially buz)))