register-type - ACL2 Book

other

(in-package "DEFDATA")

other

(include-book "defdata-attach")

other

(def-const *register-type-keywords*
  '(:predicate :enumerator :enum/acc :domain-size :clique :def :normalized-def :prettyified-def :verbose :hints :theory-name :min-rec-depth :max-rec-depth :recp :satisfies :satisfies-fixer :default-base-value :equiv :equiv-fixer :fixer :fixer-domain :lub :glb :sampling))

type-of-pred-auxfunction

(defun type-of-pred-aux
  (pred tbl)
  (declare (xargs :guard (and (symbolp pred)
        (sym-aalist1p tbl))))
  (cond ((endp tbl) nil)
    ((equal pred
       (get-alist :predicate (cdar tbl))) (caar tbl))
    (t (type-of-pred-aux pred (cdr tbl)))))

type-of-predfunction

(defun type-of-pred
  (pred tbl ptbl)
  (declare (xargs :guard (and (symbolp pred)
        (sym-aalist1p tbl)
        (sym-aalist1p ptbl))))
  (let ((apred (assoc-equal :type (get-alist pred ptbl))))
    (if apred
      (cdr apred)
      (type-of-pred-aux pred tbl))))

enum-of-typefunction

(defun enum-of-type
  (type tbl)
  (declare (xargs :guard (and (symbolp type) (sym-aalist1p tbl))))
  (get-alist :enumerator (get-alist type tbl)))

trans1-cmpfunction

(defun trans1-cmp
  (form wrld)
  (declare (xargs :mode :program))
  (declare (xargs :guard (plist-worldp wrld)))
  (translate1-cmp form
    nil
    nil
    nil
    'ctx
    wrld
    (default-state-vars nil)))

base-val-of-typefunction

(defun base-val-of-type
  (type tbl wrld)
  (declare (xargs :mode :program))
  (declare (xargs :guard (and (symbolp type)
        (sym-aalist1p tbl)
        (plist-worldp wrld))))
  (b* ((base-val (get-alist :default-base-value (get-alist type tbl))) ((mv - trans-base-val -) (if (and (symbolp base-val)
            (legal-variable-or-constant-namep base-val)
            (legal-constantp1 base-val))
          (trans1-cmp base-val wrld)
          (mv nil `',DEFDATA::BASE-VAL nil))))
    trans-base-val))

type-of-typefunction

(defun type-of-type
  (type tbl atbl)
  (declare (xargs :guard (and (symbolp type)
        (sym-aalist1p tbl)
        (sym-aalist1p atbl))))
  (let ((atype (assoc-equal :type (get-alist type atbl))))
    (if atype
      (cdr atype)
      (let ((res (get-alist type tbl)))
        (if res
          type
          nil)))))

pred-of-typefunction

(defun pred-of-type
  (type tbl atbl)
  (declare (xargs :guard (and (symbolp type)
        (sym-aalist1p tbl)
        (sym-aalist1p atbl))))
  (let ((atype (assoc-equal :predicate (get-alist type atbl))))
    (if atype
      (cdr atype)
      (let ((res (get-alist :predicate (get-alist type tbl))))
        res))))

defdata-domain-size-fnfunction

(defun defdata-domain-size-fn
  (type wrld)
  (declare (xargs :guard (and (symbolp type) (plist-worldp wrld))
      :verify-guards nil))
  (b* ((tbl (table-alist 'type-metadata-table
         wrld)) (atbl (table-alist 'type-alias-table
          wrld))
      (ttype (type-of-type type tbl atbl))
      (type-info (assoc ttype tbl))
      (domain (cdr (assoc :domain-size (cdr type-info)))))
    (if (natp domain)
      domain
      'infinite)))

defdata-domain-sizemacro

(defmacro defdata-domain-size
  (type)
  `(defdata-domain-size-fn ',TYPE
    (w state)))

defdata-base-val-of-type-fnfunction

(defun defdata-base-val-of-type-fn
  (type wrld)
  (declare (xargs :mode :program :guard (and (symbolp type) (plist-worldp wrld))
      :verify-guards nil))
  (b* ((tbl (type-metadata-table wrld)) (atbl (table-alist 'type-alias-table
          wrld))
      (ttype (type-of-type type tbl atbl)))
    (base-val-of-type ttype
      tbl
      wrld)))

defdata-base-val-of-typemacro

(defmacro defdata-base-val-of-type
  (type)
  `(defdata-base-val-of-type-fn ',TYPE
    (w state)))

get-or-size-accfunction

(defun get-or-size-acc
  (or-def acc wrld)
  (declare (xargs :mode :program))
  (if (endp or-def)
    acc
    (b* ((type (car or-def)) (size-type (if (legal-variablep type)
            (defdata-domain-size-fn (car or-def)
              wrld)
            1)))
      (if (natp size-type)
        (get-or-size-acc (cdr or-def)
          (+ size-type acc)
          wrld)
        t))))

get-or-sizefunction

(defun get-or-size
  (or-def wrld)
  (declare (xargs :mode :program))
  (get-or-size-acc or-def 0 wrld))

(defun register-type-fn
  (name args
    ctx
    pkg
    wrld)
  (declare (xargs :mode :program))
  (b* (((mv kwd-alist rest) (extract-keywords ctx
         *register-type-keywords*
         args
         nil
         nil)) ((when rest) (er hard?
          ctx
          "~| Extra args: ~x0~%"
          rest))
      ((unless (proper-symbolp name)) (er hard?
          ctx
          "~| ~x0 should be a proper symbol.~%"
          name))
      ((unless (well-formed-type-metadata-p kwd-alist
           wrld)) (er hard?
          ctx
          "~| ~s0~%"
          (ill-formed-type-metadata-msg kwd-alist
            wrld)))
      (?pred-name (get1 :predicate kwd-alist))
      (enum (get1 :enumerator kwd-alist))
      (enum/acc (get1 :enum/acc kwd-alist))
      (enum-formals (formals enum wrld))
      (enum-guard (guard enum nil wrld))
      (enum/acc-formals (or (and enum/acc
            (formals enum/acc wrld))
          '(m seed)))
      (enum/acc-guard (or (and enum/acc
            (guard enum/acc nil wrld))
          '(and (natp m)
            (unsigned-byte-p 63 seed))))
      (enum-name (make-enumerator-symbol name pkg))
      (enum/acc-name (make-uniform-enumerator-symbol name
          pkg))
      (def (get1 :def kwd-alist))
      (enum-type? (and (consp def)
          (equal (car def) 'enum)))
      (normalized-def (get1 :normalized-def kwd-alist))
      (or-type? (and (consp def) (equal (car def) 'or)))
      (or-size (if or-type?
          (get-or-size (cdr normalized-def)
            wrld)
          0))
      (domain-size (or (get1 :domain-size kwd-alist)
          (and enum-type?
            (nfix (1- (len normalized-def))))
          (and or-type? or-size)
          (and (quotep def) 1)
          (and (atom def) 1)
          t))
      ((when (eq enum enum-name)) (er hard?
          ctx
          "~| Please rename the enumerator ~x0 to be different from ~x1, to which it will be attached.~%"
          enum
          enum-name))
      ((when (eq enum/acc enum/acc-name)) (er hard?
          ctx
          "~| Please rename the enumerator ~x0 to be different from ~x1, to which it will be attached.~%"
          enum/acc
          enum/acc-name))
      (enum/acc-default (s+ enum/acc-name
          '-builtin
          :pkg pkg))
      (kwd-alist (put-assoc-eq :enumerator enum-name
          kwd-alist))
      (kwd-alist (put-assoc-eq :enum/acc enum/acc-name
          kwd-alist))
      (kwd-alist (put-assoc-eq :domain-size domain-size
          kwd-alist))
      (kwd-alist (put-assoc-eq :theory-name (or (get1 :theory-name kwd-alist)
            (s+ name
              '-theory
              :pkg pkg))
          kwd-alist))
      (existing-entry (assoc-eq name
          (table-alist 'type-metadata-table
            wrld)))
      ((when existing-entry) (if (not (equal kwd-alist (cdr existing-entry)))
          (er hard?
            ctx
            "~| ~x0 is already a registered defdata type.~%"
            name)
          'nil))
      (default-val (or (get1 :default-base-value kwd-alist)
          (funcall-w enum
            (list 0)
            ctx
            wrld)))
      (kwd-alist (put-assoc-eq :default-base-value default-val
          kwd-alist))
      (kwd-alist (put-assoc-eq :min-rec-depth (or (get1 :min-rec-depth kwd-alist) 0)
          kwd-alist))
      (kwd-alist (put-assoc-eq :max-rec-depth (or (get1 :max-rec-depth kwd-alist) 30)
          kwd-alist)))
    `(encapsulate nil
      (logic)
      (with-output :summary-off (:other-than form)
        :on (error)
        (progn ,@(AND (DEFDATA::TABLE-ALIST 'ACL2S-DEFAULTS-TABLE DEFDATA::WRLD)
       '((DEFDATA::LOCAL (ACL2S-DEFAULTS :SET :TESTING-ENABLED :NAIVE))))
          (encapsulate (((,DEFDATA::ENUM-NAME *) =>
               *
               :formals ,DEFDATA::ENUM-FORMALS
               :guard ,DEFDATA::ENUM-GUARD))
            (local (defun ,DEFDATA::ENUM-NAME
                ,DEFDATA::ENUM-FORMALS
                (declare (xargs :guard ,DEFDATA::ENUM-GUARD))
                (declare (ignorable . ,DEFDATA::ENUM-FORMALS))
                ',DEFDATA::DEFAULT-VAL)))
          ,@(AND (NOT DEFDATA::ENUM/ACC)
       (DEFDATA::MAKE-ENUM-UNIFORM-DEFUN-EV DEFDATA::ENUM/ACC-DEFAULT
        DEFDATA::ENUM-NAME))
          (encapsulate (((,DEFDATA::ENUM/ACC-NAME * *) =>
               (mv * *)
               :formals ,DEFDATA::ENUM/ACC-FORMALS
               :guard ,DEFDATA::ENUM/ACC-GUARD))
            (local (defun ,DEFDATA::ENUM/ACC-NAME
                ,DEFDATA::ENUM/ACC-FORMALS
                (declare (xargs :guard ,DEFDATA::ENUM/ACC-GUARD))
                (declare (ignorable . ,DEFDATA::ENUM/ACC-FORMALS))
                (mv ',DEFDATA::DEFAULT-VAL 0))))
          (defttag :defdata-attach)
          (defattach (,DEFDATA::ENUM-NAME ,DEFDATA::ENUM)
            :skip-checks t)
          (defattach (,DEFDATA::ENUM/ACC-NAME ,(OR DEFDATA::ENUM/ACC DEFDATA::ENUM/ACC-DEFAULT))
            :skip-checks t)
          (defttag nil)
          (table type-metadata-table
            ',DEFDATA::NAME
            ',DEFDATA::KWD-ALIST)
          (value-triple :registered))))))

(defmacro register-type
  (name &rest keys)
  (b* ((verbosep (let ((lst (member :verbose keys)))
         (and lst (cadr lst)))) (ctx 'register-type)
      ((unless (and (member :predicate keys)
           (member :enumerator keys))) (er hard
          ctx
          "~| Keyword args predicate, enumerator are mandatory.~%")))
    `(encapsulate nil
      (with-output ,@(IF DEFDATA::VERBOSEP
      '(:ON :ALL)
      '(:ON ERROR))
        :stack :push (make-event (register-type-fn ',DEFDATA::NAME
            ',DEFDATA::KEYS
            ',DEFDATA::CTX
            (current-package state)
            (w state)))))))