Filtering...

map

books/acl2s/defdata/map
other
(in-package "DEFDATA")
other
(include-book "data-structures/utilities" :dir :system)
other
(include-book "coi/symbol-fns/symbol-fns" :dir :system)
other
(include-book "tools/templates" :dir :system)
other
(include-book "register-combinator")
other
(def-const *map-local-events* 'nil)
other
(def-const *map-export-defthms*
  '((defthm _pred_-implies-alistp
     (implies (_pred_ x)
       (alistp x))
     :hints (("goal" :in-theory (e/d (_pred_))))
     :rule-classes ((:rewrite :backchain-limit-lst 1) (:forward-chaining))) (defthm _pred_-implies-no-nil-val-alistp
      (implies (_pred_ x)
        (no-nil-val-alistp x))
      :hints (("goal" :in-theory (e/d (_pred_))))
      :rule-classes ((:rewrite :backchain-limit-lst 1) (:forward-chaining)))
    (defthm _pred_-implies-ordered-unique-key-alistp
      (implies (_pred_ x)
        (ordered-unique-key-alistp x))
      :hints (("goal" :in-theory (e/d (_pred_))))
      :rule-classes ((:rewrite :backchain-limit-lst 1) (:forward-chaining)))
    (defthm _pred_-implies-recordp
      (implies (_pred_ x)
        (recordp x))
      :hints (("goal" :in-theory (e/d (_pred_))))
      :rule-classes ((:rewrite :backchain-limit-lst 1) (:forward-chaining)))
    (defthm _pred_-excludes-atom-list
      (implies (and (_pred_ x) (consp x))
        (not (atom-listp x)))
      :hints (("goal" :in-theory (e/d (_pred_))))
      :rule-classes (:tau-system))
    (defthm _pred_-map-identity2-generalize
      (implies (_pred_ x)
        (_pred_ (map-identity2 a x)))
      :rule-classes (:generalize))
    (:@ :key-is-typename (defthm _pred_-domain-lemma
        (implies (and (_pred_ x)
            (mget a x))
          (_keypred_ a))
        :hints (("Goal" :in-theory (e/d (_pred_ mget)
             (_keypred_))))
        :rule-classes ((:forward-chaining :trigger-terms ((mget a x))) :generalize))
      (defthm deleting-an-entry-in-_pred_
        (implies (and (_pred_ x)
            (_keypred_ a))
          (_pred_ (mset a nil x)))
        :hints (("Goal" :in-theory (e/d (minimal-records-theory))))))
    (:@ (and :key-is-typename :val-is-typename)
      (defthm _pred_-selector
        (implies (and (_pred_ x)
            (mget a x))
          (_valpred_ (mget a x)))
        :hints (("Goal" :in-theory (e/d (_pred_ mget minimal-records-theory)
             (_keypred_ _valpred_)))))
      (defthm _pred_-selector-generalize
        (implies (and (_pred_ x))
          (or (_valpred_ (mget a x))
            (equal (mget a x) nil)))
        :hints (("Goal" :in-theory (e/d (_pred_ mget minimal-records-theory)
             (_keypred_ _valpred_))))
        :rule-classes :generalize)
      (defthm _pred_-modifier
        (implies (and (_pred_ x)
            (_keypred_ a)
            (_valpred_ v))
          (_pred_ (mset a v x)))
        :hints (("Goal" :in-theory (e/d (_pred_ mset minimal-records-theory)
             (_keypred_ _valpred_))))
        :rule-classes (:rewrite :generalize)))))
map-attach-constraint-rules-evfunction
(defun map-attach-constraint-rules-ev
  (p wrld)
  (b* (((cons name a) p) ((assocs pdef new-types) a))
    (case-match pdef
      (('map keybody valbody) (b* ((m (append new-types
               (type-metadata-table wrld))) (a (type-alias-table wrld))
            (pred (predicate-name name
                a
                m))
            (?keypred (and (proper-symbolp keybody)
                (assoc-eq keybody m)
                (predicate-name keybody
                  a
                  m)))
            (?valpred (and (proper-symbolp keybody)
                (assoc-eq keybody m)
                (predicate-name valbody
                  a
                  m))))
          `((defdata-attach ,DEFDATA::NAME
             :constraint (mget a x)
             :constraint-variable x
             :rule (implies (and (,DEFDATA::KEYPRED a)
                 (,DEFDATA::VALPRED x.a)
                 (,DEFDATA::PRED x1))
               (equal x
                 (mset a x.a x1)))
             :meta-precondition (or (variablep a) (fquotep a))
             :match-type :subterm-match))))
      (& 'nil))))
other
(defloop map-attach-constraint-rules-events
  (ps kwd-alist wrld)
  (declare (ignorable kwd-alist))
  (for ((p in ps))
    (append (map-attach-constraint-rules-ev p
        wrld))))
other
(program)
map-theory-eventsfunction
(defun map-theory-events
  (name keybody
    valbody
    new-types
    kwd-alist
    wrld)
  (b* ((m (append new-types
         (type-metadata-table wrld))) (a (type-alias-table wrld))
      (pred (predicate-name name
          a
          m))
      ((when (not (proper-symbolp pred))) (er hard?
          'map-theory-events
          "~| Couldnt find predicate name for ~x0.~%"
          name))
      ((mv ?symbol-alist-subtypep
         ?keypred) (if (and (proper-symbolp keybody)
            (assoc-eq keybody m))
          (mv (subtype-p (predicate-name keybody
                a
                m)
              'symbolp
              wrld)
            (predicate-name keybody
              a
              m))
          (mv nil nil)))
      (?valpred (and (proper-symbolp keybody)
          (assoc-eq keybody m)
          (predicate-name valbody
            a
            m)))
      (disabled (get1 :disabled kwd-alist))
      (curr-pkg (get1 :current-package kwd-alist))
      (pkg-sym (pkg-witness curr-pkg))
      (disabled (append '(mset-diff-mset1 mset-diff-mset2)
          disabled))
      (local-events-template *map-local-events*)
      (export-defthms-template *map-export-defthms*)
      (features (append (and keypred '(:key-is-typename))
          (and valpred '(:val-is-typename))))
      (splice-alist `((_disabled-runes_ . ,DEFDATA::DISABLED)))
      (atom-alist `((_pred_ . ,DEFDATA::PRED) (_typename_ . ,DEFDATA::NAME)
          (_keypred_ . ,DEFDATA::KEYPRED)
          (_valpred_ . ,DEFDATA::VALPRED)))
      (str-alist `(("_PRED_" . ,(SYMBOL-NAME DEFDATA::PRED)) ("_KEYPRED_" . ,(SYMBOL-NAME DEFDATA::KEYPRED))
          ("_VALPRED_" . ,(SYMBOL-NAME DEFDATA::VALPRED))))
      (local-events (template-subst local-events-template
          :features features
          :splice-alist splice-alist
          :atom-alist atom-alist
          :str-alist str-alist
          :pkg-sym pkg-sym))
      (export-defthms (template-subst export-defthms-template
          :features features
          :splice-alist splice-alist
          :atom-alist atom-alist
          :str-alist str-alist
          :pkg-sym pkg-sym))
      (all-defthm-names (get-event-names export-defthms))
      (theory-name (get1 :theory-name kwd-alist)))
    `(,@(AND DEFDATA::LOCAL-EVENTS
       `((DEFDATA::LOCAL (PROGN . ,DEFDATA::LOCAL-EVENTS)))) ,@DEFDATA::EXPORT-DEFTHMS
      (def-ruleset! ,DEFDATA::THEORY-NAME
        ',DEFDATA::ALL-DEFTHM-NAMES))))
map-theory-evfunction
(defun map-theory-ev
  (p top-kwd-alist wrld)
  (b* (((cons name a) p) ((assocs pdef new-types kwd-alist) a)
      (kwd-alist (append kwd-alist top-kwd-alist)))
    (case-match pdef
      (('map key-body val-body) (map-theory-events name
          key-body
          val-body
          new-types
          kwd-alist
          wrld))
      (& 'nil))))
other
(defloop user-map-theory-events1
  (ps kwd-alist wrld)
  (for ((p in ps))
    (append (map-theory-ev p
        kwd-alist
        wrld))))
user-map-theory-eventsfunction
(defun user-map-theory-events
  (ps kwd-alist wrld)
  (b* ((events (user-map-theory-events1 ps
         kwd-alist
         wrld)))
    (and (consp events)
      (append `((commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
           "~| Map theory events...~%") (value-triple (progn$ (time-tracker :map-theory-events :end)
              (time-tracker :map-theory-events :init :times '(2 7)
                :interval 5
                :msg "Elapsed runtime in theory events for maps is ~st secs;~|~%")
              :invisible)))
        events))))
other
(logic)
other
(deflabel map)
other
(register-user-combinator map
  :arity 2
  :verbose t
  :aliases (map)
  :expansion (lambda (_name _args)
    `(or nil
      (mset ,(CAR DEFDATA::_ARGS)
        ,(CADR DEFDATA::_ARGS)
        ,DEFDATA::_NAME)))
  :syntax-restriction-fn proper-symbol-listp
  :syntax-restriction-msg "map syntax restriction: ~x0 should be type names."
  :polymorphic-type-form (alistof :a :b)
  :post-pred-hook-fns (user-map-theory-events)
  :post-hook-fns (map-attach-constraint-rules-events))