register-combinator

other

(in-package "DEFDATA")

other

(include-book "defdata-util")

get-defconst-valfunction

(defun get-defconst-val
  (x wrld)
  (cadr (acl2-getprop x 'const wrld)))

other

(def-const *register-user-combinator-keywords*
  '(:arity :aliases :expansion :verbose :syntax-restriction-fn :syntax-restriction-msg :polymorphic-type-form :polymorphic-events :pre-pred-hook-fns :in-pred-hook-fns :post-pred-hook-fns :post-hook-fns))

(defun register-user-combinator-fn
  (name args ctx wrld)
  (declare (ignorable wrld))
  (b* (((mv kwd-alist rest) (extract-keywords ctx
         *register-user-combinator-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))
      (aliases (union-eq (list name)
          (get1 :aliases kwd-alist)))
      (theory-name (get1 :theory-name kwd-alist
          (suffix name '-theory)))
      (kwd-alist (put-assoc-eq :aliases aliases
          kwd-alist))
      (kwd-alist (put-assoc-eq :theory-name theory-name
          kwd-alist)))
    `((table user-combinator-table
       ',DEFDATA::NAME
       ',DEFDATA::KWD-ALIST) (add-pre-post-hook defdata-defaults-table
        :pre-pred-hook-fns ',(DEFDATA::GET1 :PRE-PRED-HOOK-FNS DEFDATA::KWD-ALIST))
      (add-pre-post-hook defdata-defaults-table
        :in-pred-hook-fns ',(DEFDATA::GET1 :IN-PRED-HOOK-FNS DEFDATA::KWD-ALIST))
      (add-pre-post-hook defdata-defaults-table
        :post-pred-hook-fns ',(DEFDATA::GET1 :POST-PRED-HOOK-FNS DEFDATA::KWD-ALIST))
      (add-pre-post-hook defdata-defaults-table
        :post-hook-fns ',(DEFDATA::GET1 :POST-HOOK-FNS DEFDATA::KWD-ALIST)))))

other

(logic)

(defmacro register-user-combinator
  (name &rest keys)
  (b* ((verbosep (let ((lst (member :verbose keys)))
         (and lst (cadr lst)))) (ctx 'register-user-combinator)
      ((unless (and (member :arity keys)
           (member :expansion keys))) (er hard?
          ctx
          "~| Keyword args arity, expansion are mandatory.~%")))
    `(with-output ,@(AND (NOT DEFDATA::VERBOSEP) '(:OFF :ALL))
      :stack :push (make-event (cons 'progn
          (register-user-combinator-fn ',DEFDATA::NAME
            ',DEFDATA::KEYS
            ',DEFDATA::CTX
            (w state)))))))