Filtering...

sig

books/acl2s/defdata/sig
other
(in-package "DEFDATA")
other
(include-book "defdata-core")
other
(def-const *allowed-type-vars*
  '(:a :b :c :d :a1 :b1 :c1 :d1 :a2 :b2 :c2 :d2))
other
(def-const *tvar-typename-alist*
  '((:a . a) (:b . b)
    (:c . c)
    (:d . d)
    (:a1 . a1)
    (:b1 . b1)
    (:c1 . c1)
    (:d1 . d1)
    (:a2 . a2)
    (:b2 . b2)
    (:c2 . c2)
    (:d2 . d2)))
other
(table psig-template-map nil)
other
(defstub psig-templ-instantiation-ev
  (* * * * * * *)
  =>
  *)
other
(defloop psig-inst-templates
  (tname tvar-sigma
    templates
    new-types
    kwd-alist
    wrld)
  (for ((templ in templates))
    (append (psig-templ-instantiation-ev tname
        tvar-sigma
        templ
        (table-alist 'derived-pred->poly-texp-map
          wrld)
        new-types
        kwd-alist
        wrld))))
other
(program)
one-way-unifyfunction
(defun one-way-unify
  (pat term)
  (if (and (pseudo-termp pat)
      (pseudo-termp term))
    (one-way-unify pat term)
    (mv nil nil)))
polymorphic-inst-defdata-events1function
(defun polymorphic-inst-defdata-events1
  (p top-kwd-alist wrld)
  (b* (((cons name a) p) ((assocs pdef new-types kwd-alist) a)
      ((unless (consp pdef)) 'nil)
      (kwd-alist (append kwd-alist top-kwd-alist))
      (comb (car pdef))
      (u (table-alist 'user-combinator-table
          wrld))
      (c (table-alist 'data-constructor-table
          wrld))
      (meta-kwd-alist (or (cdr (assoc-eq comb u))
          (cdr (assoc-eq comb c))))
      (template (get1 :polymorphic-events meta-kwd-alist))
      (ptype (get1 :polymorphic-type-form meta-kwd-alist))
      ((when (null ptype)) 'nil)
      (pdef (remove-names pdef))
      ((mv yesp tvar-sigma) (one-way-unify (sublis-var *tvar-typename-alist* ptype)
          pdef))
      (verbose (get1 :verbose kwd-alist t))
      (- (cw? (and (not yesp) verbose)
          "~|Defdata/Note: Failed to unify ~x0 with ~x1. Skipping polymorphic instantiation events...~%"
          ptype
          pdef))
      ((unless yesp) 'nil))
    (psig-templ-instantiation-ev name
      tvar-sigma
      template
      (table-alist 'derived-pred->poly-texp-map
        wrld)
      new-types
      kwd-alist
      wrld)))
other
(defloop polymorphic-inst-defdata-events0
  (ps kwd-alist wrld)
  (for ((p in ps))
    (append (polymorphic-inst-defdata-events1 p
        kwd-alist
        wrld))))
try-admitting-events-funfunction
(defun try-admitting-events-fun
  (events)
  (if (endp events)
    nil
    (cons `(make-event '(:or ,(CAR DEFDATA::EVENTS) (value-triple t)))
      (try-admitting-events-fun (cdr events)))))
polymorphic-inst-defdata-eventsfunction
(defun polymorphic-inst-defdata-events
  (ps kwd-alist wrld)
  (b* ((events (polymorphic-inst-defdata-events0 ps
         kwd-alist
         wrld)))
    (and (consp events)
      (cons `(commentary ,(DEFDATA::GET1 :PRINT-COMMENTARY DEFDATA::KWD-ALIST)
          "~| Polymorphic sig instantiation events...~%")
        (try-admitting-events-fun events)))))
other
(add-pre-post-hook defdata-defaults-table
  :post-pred-hook-fns '(polymorphic-inst-defdata-events))
other
(logic)
other
(encapsulate (((ap *) => *) ((bp *) => *)
    ((cp *) => *)
    ((dp *) => *)
    ((a1p *) => *)
    ((b1p *) => *)
    ((c1p *) => *)
    ((d1p *) => *)
    ((a2p *) => *)
    ((b2p *) => *)
    ((c2p *) => *)
    ((d2p *) => *))
  (local (defun ap
      (v)
      (declare (ignore v))
      t))
  (local (defun bp
      (v)
      (declare (ignore v))
      t))
  (local (defun cp
      (v)
      (declare (ignore v))
      t))
  (local (defun dp
      (v)
      (declare (ignore v))
      t))
  (local (defun a1p
      (v)
      (declare (ignore v))
      t))
  (local (defun b1p
      (v)
      (declare (ignore v))
      t))
  (local (defun c1p
      (v)
      (declare (ignore v))
      t))
  (local (defun d1p
      (v)
      (declare (ignore v))
      t))
  (local (defun a2p
      (v)
      (declare (ignore v))
      t))
  (local (defun b2p
      (v)
      (declare (ignore v))
      t))
  (local (defun c2p
      (v)
      (declare (ignore v))
      t))
  (local (defun d2p
      (v)
      (declare (ignore v))
      t))
  (defthm ap-is-predicate
    (booleanp (ap x)))
  (defthm bp-is-predicate
    (booleanp (bp x)))
  (defthm cp-is-predicate
    (booleanp (cp x)))
  (defthm dp-is-predicate
    (booleanp (dp x)))
  (defthm a1p-is-predicate
    (booleanp (a1p x)))
  (defthm b1p-is-predicate
    (booleanp (b1p x)))
  (defthm c1p-is-predicate
    (booleanp (c1p x)))
  (defthm d1p-is-predicate
    (booleanp (d1p x)))
  (defthm a2p-is-predicate
    (booleanp (a2p x)))
  (defthm b2p-is-predicate
    (booleanp (b2p x)))
  (defthm c2p-is-predicate
    (booleanp (c2p x)))
  (defthm d2p-is-predicate
    (booleanp (d2p x))))
other
(program)
other
(def-const *initial-tvar-m*
  (type-metadata-bases (strip-cdrs *tvar-typename-alist*)
    "DEFDATA"))
other
(table tvar-metadata-table
  nil
  *initial-tvar-m*
  :clear)
other
(mutual-recursion (defun collect-type-vars-texp
    (texp ctx)
    (cond ((quotep texp) 'nil)
      ((keywordp texp) (list texp))
      ((atom texp) 'nil)
      ((not (true-listp texp)) (er hard?
          ctx
          "~| ~x0 : Named type expressions not supported.~%"
          texp))
      (t (collect-type-vars-texps (cdr texp)
          ctx))))
  (defun collect-type-vars-texps
    (texps ctx)
    (if (endp texps)
      'nil
      (union-eq (collect-type-vars-texp (car texps)
          ctx)
        (collect-type-vars-texps (cdr texps)
          ctx)))))
other
(mutual-recursion (defun collect-undefined-typenames-texp
    (texp ctx wrld)
    (cond ((quotep texp) 'nil)
      ((keywordp texp) 'nil)
      ((atom texp) (if (predicate-name texp)
          'nil
          (list texp)))
      ((not (true-listp texp)) (er hard?
          ctx
          "~| ~x0 : Named type expressions not supported.~%"
          texp))
      (t (collect-undefined-typenames-texps (cdr texp)
          ctx
          wrld))))
  (defun collect-undefined-typenames-texps
    (texps ctx wrld)
    (if (endp texps)
      'nil
      (union-eq (collect-undefined-typenames-texp (car texps)
          ctx
          wrld)
        (collect-undefined-typenames-texps (cdr texps)
          ctx
          wrld)))))
other
(def-const *sig-keywords*
  '(:hints :gen-rule-classes :rule-classes :verbose :satisfies :suffix))
parse-sigfunction
(defun parse-sig
  (args curr-pkg ctx wrld)
  (declare (ignorable wrld))
  (b* (((mv sig kwd-val-list) (separate-kwd-args args 'nil)) ((mv kwd-alist rest) (extract-keywords ctx
          *sig-keywords*
          kwd-val-list
          'nil
          nil))
      ((unless (null rest)) (er hard?
          ctx
          "~| Extra args: ~x0~%"
          rest))
      (dep-hyp (get1 :satisfies kwd-alist))
      (suffix (get1 :suffix kwd-alist))
      (x123vars (numbered-vars (fix-intern$ "X" curr-pkg)
          (len *allowed-type-vars*)))
      (dep-vars (and dep-hyp (all-vars dep-hyp)))
      ((unless (subsetp dep-vars x123vars)) (er hard?
          ctx
          "~| Only variable arguments allowed in SATISFIES are ~x0; but given ~x1~%"
          x123vars
          dep-vars))
      (dep-hyps (cond ((null dep-hyp) nil)
          ((or (eq dep-hyp 't) (equal dep-hyp ''t)) nil)
          ((atom dep-hyp) (list dep-hyp))
          ((eq (car dep-hyp) 'and) (cdr dep-hyp))
          ((proper-symbolp (car dep-hyp)) (list dep-hyp))
          (t dep-hyp)))
      (kwd-alist (put-assoc-eq :satisfies dep-hyps
          kwd-alist))
      (kwd-alist (put-assoc-eq :current-package curr-pkg
          kwd-alist)))
    (case-match sig
      ((name arg-type-list
         '=>
         return-type) (b* (((unless (proper-symbolp name)) (er hard?
               ctx
               "~| Name ~x0 should be a symbol.~%"
               name)) (& (check-syntax-texps arg-type-list
                'nil
                'nil
                ctx
                wrld))
            (undefined-typenames (collect-undefined-typenames-texps (cons return-type arg-type-list)
                ctx
                wrld))
            ((when (consp undefined-typenames)) (er hard?
                ctx
                "~| Undefined types: ~x0~%"
                undefined-typenames))
            (arg-type-vars (collect-type-vars-texps arg-type-list
                ctx))
            (return-type-vars (collect-type-vars-texp return-type
                ctx))
            ((unless (subsetp return-type-vars arg-type-vars)) (er hard?
                ctx
                "~| Return type variables should be from ~x0.~%"
                arg-type-vars))
            ((unless (subsetp arg-type-vars
                 *allowed-type-vars*)) (er hard?
                ctx
                "~| Sorry for the inconvenience, but could you please try again choosing type variables from ~x0.~%"
                *allowed-type-vars*)))
          (list name
            suffix
            arg-type-list
            return-type
            kwd-alist)))
      (& (er hard?
          ctx
          "~| General form: (sig name arg-type-list => return-type).~%")))))
to-symbolfunction
(defun to-symbol
  (obj pkg)
  (declare (xargs :guard (pkgp pkg)))
  (if (symbolp obj)
    obj
    (b* (((mv & str) (fmt1!-to-string "~x0" (acons #\0 obj 'nil) 0)))
      (fix-intern$ str pkg))))
other
(defloop to-symbols
  (objs pkg)
  (declare (xargs :guard (pkgp pkg)))
  (for ((o in objs))
    (collect (to-symbol o pkg))))
assoceqlst1function
(defun assoceqlst1
  (key a)
  (let ((entry (assoc-eq key a)))
    (and entry (list entry))))
other
(defloop assoc-eq-lst
  (keys a)
  (for ((key in keys))
    (append (assoceqlst1 key a))))
stitch-up-defunsfunction
(defun stitch-up-defuns
  (names params-lst
    decls
    bodies)
  (if (endp names)
    nil
    (cons (if (consp decls)
        (list 'defun
          (car names)
          (car params-lst)
          (car decls)
          (car bodies))
        (list 'defun
          (car names)
          (car params-lst)
          (car bodies)))
      (stitch-up-defuns (cdr names)
        (cdr params-lst)
        (cdr decls)
        (cdr bodies)))))
make-derived-tvar-type-defthmfunction
(defun make-derived-tvar-type-defthm
  (pred texp pkg)
  (case-match texp
    (('listof &) `((defthm ,(DEFDATA::S+ DEFDATA::PRED 'DEFDATA::-IMPLIES-TLP :PKG DEFDATA::PKG)
         (implies (,DEFDATA::PRED x)
           (true-listp x))
         :hints (("Goal" :in-theory (enable true-listp)))
         :rule-classes ((:forward-chaining) (:compound-recognizer)))))
    (('alistof & &) `((defthm ,(DEFDATA::S+ DEFDATA::PRED 'DEFDATA::-IMPLIES-ALISTP :PKG DEFDATA::PKG)
         (implies (,DEFDATA::PRED x)
           (alistp x))
         :hints (("Goal" :in-theory (enable ,DEFDATA::PRED alistp)))
         :rule-classes ((:forward-chaining)))))
    (& 'nil)))
other
(defloop make-derived-tvar-type-defthms
  (preds texps pkg)
  (for ((p in preds) (texp in texps))
    (append (make-derived-tvar-type-defthm p
        texp
        pkg))))
other
(defloop parse-top-texps
  (names texps ctx wrld)
  (for ((name in names) (texp in texps))
    (collect (parse-top-texp name
        texp
        (list name)
        ctx
        wrld))))
make-sig-tvar-support-eventsfunction
(defun make-sig-tvar-support-events
  (texps ctx pkg wrld)
  "for each undefined tvar texp, define its predicate and if possible its type defthm"
  (b* ((m (append (table-alist 'tvar-metadata-table
           wrld)
         (table-alist 'type-metadata-table
           wrld))) (texps (remove-names-lst (remove-duplicates-equal texps)))
      (tnames (to-symbols texps "DEFDATA"))
      (undef-tnames (set-difference-eq tnames
          (strip-cars (assoc-eq-lst tnames m))))
      (undef-nm-texp-alst (assoc-eq-lst undef-tnames
          (pairlis$ tnames texps)))
      ((mv undef-tnames undef-texps) (mv (strip-cars undef-nm-texp-alst)
          (strip-cdrs undef-nm-texp-alst)))
      (undef-n-types (parse-top-texps undef-tnames
          undef-texps
          ctx
          wrld))
      (c (table-alist 'data-constructor-table
          wrld))
      (b (table-alist 'builtin-combinator-table
          wrld))
      (new-types (type-metadata-bases undef-tnames
          "DEFDATA"))
      (m (append new-types m))
      (a (table-alist 'type-alias-table
          wrld))
      (undef-pred-bodies (make-pred-is undef-n-types
          (make-list (len undef-n-types)
            :initial-element (fix-intern$ "X" pkg))
          nil
          a
          m
          c
          b
          wrld))
      (undef-pred-names (make-predicate-symbol-lst undef-tnames
          "DEFDATA")))
    (append (stitch-up-defuns undef-pred-names
        (make-list (len undef-pred-names)
          :initial-element `(,(ACL2S::FIX-INTERN$ "X" DEFDATA::PKG)))
        nil
        undef-pred-bodies)
      (make-derived-tvar-type-defthms undef-pred-names
        undef-texps
        pkg))))
other
(def-const *poly-combinators*
  '(listof alistof map))
other
(table derived-pred->poly-texp-map nil)
other
(defloop table-put-events
  (tble-name keys vals)
  (for ((key in keys) (val in vals))
    (collect `(table ,DEFDATA::TBLE-NAME
        ',DEFDATA::KEY
        ',DEFDATA::VAL
        :put))))
other
(def-const *sig-singular-dominant-poly-comb-limitation-msg*
  "~| SIG: Limitation -- There should be one polymorphic combinator argument that dominates all other arguments. ~
But ~x0 does not have this property. Therefore we are unable to functionally instantiate this polymorphic signature. ~
Please send this example to the implementors for considering removal of this restriction.~%")
all-tvarsfunction
(defun all-tvars
  (texp)
  (intersection-eq (strip-cdrs *tvar-typename-alist*)
    (all-vars texp)))
all-tvars-lstfunction
(defun all-tvars-lst
  (texps)
  (intersection-eq (strip-cdrs *tvar-typename-alist*)
    (all-vars1-lst texps 'nil)))
poly-type-sizefunction
(defun poly-type-size
  (ptype)
  (if (atom ptype)
    0
    (case (car ptype)
      ((oneof or anyof) 1)
      (listof (+ 2 (poly-type-size (cadr ptype))))
      (alistof (+ 3
          (+ (poly-type-size (second ptype))
            (poly-type-size (third ptype)))))
      (map (+ 4
          (+ (poly-type-size (second ptype))
            (poly-type-size (third ptype)))))
      (t 0))))
choose-largest-poly-typefunction
(defun choose-largest-poly-type
  (ptypes ans)
  (if (endp ptypes)
    ans
    (if (> (poly-type-size (car ptypes))
        (poly-type-size ans))
      (choose-largest-poly-type (cdr ptypes)
        (car ptypes))
      (choose-largest-poly-type (cdr ptypes)
        ans))))
pick-dominant-poly-type-expr1function
(defun pick-dominant-poly-type-expr1
  (ptypes all-tvars answers)
  (if (endp ptypes)
    (choose-largest-poly-type answers
      (car answers))
    (if (subsetp all-tvars
        (all-tvars (car ptypes)))
      (pick-dominant-poly-type-expr1 (cdr ptypes)
        all-tvars
        (cons (car ptypes) answers))
      (pick-dominant-poly-type-expr1 (cdr ptypes)
        all-tvars
        answers))))
pick-dominant-poly-type-exprfunction
(defun pick-dominant-poly-type-expr
  (ptypes)
  (pick-dominant-poly-type-expr1 ptypes
    (all-tvars-lst ptypes)
    nil))
make-table-append-event2function
(defun make-table-append-event2
  (tble-name key1
    key2
    val
    wrld)
  (b* ((a (table-alist tble-name wrld)) (existing-alst (get1 key1 a))
      (new-val (append (get1 key2 existing-alst)
          val))
      (new-alst (put-assoc-eq key2
          new-val
          existing-alst)))
    `(table ,DEFDATA::TBLE-NAME
      ',DEFDATA::KEY1
      ',DEFDATA::NEW-ALST
      :put)))
filter-texps-with-varsfunction
(defun filter-texps-with-vars
  (texps)
  "Filter from normalized texps, the ones which have :a, :b, ... type vars"
  (if (endp texps)
    'nil
    (if (consp (all-tvars (car texps)))
      (cons (car texps)
        (filter-texps-with-vars (cdr texps)))
      (filter-texps-with-vars (cdr texps)))))
register-poly-sig-eventsfunction
(defun register-poly-sig-events
  (nm atypes
    rtype
    templ
    wrld)
  (b* ((dom-type (pick-dominant-poly-type-expr (append atypes (list rtype)))) (- (cw? nil
          "dom-type: ~x0 nm: ~x1"
          dom-type
          nm))
      ((when (null dom-type)) (prog2$ (cw *sig-singular-dominant-poly-comb-limitation-msg*
            (cons rtype atypes))
          nil)))
    (and (consp dom-type)
      (b* ((pcomb (car dom-type)) ((unless (member-eq pcomb
               *poly-combinators*)) (prog2$ (cw "~x0 currently does not have polymorphic support. Skipping..."
                pcomb)
              nil))
          (vtypes (filter-texps-with-vars (remove-duplicates-equal (cons rtype atypes))))
          (vtnames (to-symbols vtypes "DEFDATA"))
          (vpreds (make-predicate-symbol-lst vtnames
              "DEFDATA")))
        `(,@(DEFDATA::TABLE-PUT-EVENTS 'DEFDATA::DERIVED-PRED->POLY-TEXP-MAP
   DEFDATA::VPREDS DEFDATA::VTYPES) ,@(DEFDATA::TABLE-PUT-EVENTS 'DEFDATA::TVAR-METADATA-TABLE DEFDATA::VTNAMES
   (DEFDATA::STRIP-CDRS
    (DEFDATA::TYPE-METADATA-BASES DEFDATA::VTNAMES "DEFDATA")))
          ,(DEFDATA::MAKE-TABLE-APPEND-EVENT2 'DEFDATA::USER-COMBINATOR-TABLE
  DEFDATA::PCOMB :POLYMORPHIC-EVENTS DEFDATA::TEMPL DEFDATA::WRLD))))))
find-type-namefunction
(defun find-type-name
  (texp m)
  (if (endp m)
    :undefined (b* (((cons tname al) (car m)) (pdef (get1 :prettyified-def al)))
      (if (equal texp pdef)
        tname
        (find-type-name texp (cdr m))))))
other
(defloop find-type-names1
  (texps m)
  (for ((texp in texps))
    (collect (if (and (proper-symbolp texp)
          (assoc-eq texp m))
        texp
        (find-type-name texp m)))))
remove-exprs-with-fnsfunction
(defun remove-exprs-with-fns
  (psigs fns)
  (if (endp psigs)
    'nil
    (if (intersection-eq (all-fnnames (car psigs))
        fns)
      (remove-exprs-with-fns (cdr psigs)
        fns)
      (cons (car psigs)
        (remove-exprs-with-fns (cdr psigs)
          fns)))))
subst-valsfunction
(defun subst-vals
  (map sigma)
  "apply sigma to all values in map"
  (if (endp map)
    'nil
    (b* (((cons key val) (car map)) (val~ (sublis-var sigma val)))
      (cons (cons key val~)
        (subst-vals (cdr map) sigma)))))
undefined-predsfunction
(defun undefined-preds
  (pred->tname-map)
  "return all keys marked :undefined"
  (if (endp pred->tname-map)
    'nil
    (if (equal (cdr (car pred->tname-map)) :undefined)
      (cons (caar pred->tname-map)
        (undefined-preds (cdr pred->tname-map)))
      (undefined-preds (cdr pred->tname-map)))))
remove-undefinedfunction
(defun remove-undefined
  (map)
  "remove all values marked :undefined"
  (if (endp map)
    'nil
    (if (equal (cdr (car map)) :undefined)
      (remove-undefined (cdr map))
      (cons (car map) (remove-undefined (cdr map))))))
predicate-name/lambdafunction
(defun predicate-name/lambda
  (type a m)
  "find predicate characterization for type (either a symbol or a quoted
constant). In the latter return a lambda expression"
  (declare (xargs :guard (and (or (proper-symbolp type)
          (possible-constant-value-p type))
        (symbol-alistp m))))
  (cond ((proper-symbolp type) (predicate-name type a m))
    ((possible-constant-value-p type) `(lambda (x) (equal x ,TYPE)))
    (t nil)))
other
(defloop predicate-names/lambdas
  (types a m)
  (for ((type in types))
    (collect (predicate-name/lambda type a m))))
dlistifyfunction
(defun dlistify
  (alist)
  (declare (xargs :guard (alistp alist)))
  (list-up-lists (strip-cars alist)
    (strip-cdrs alist)))
polypred-instantiated-pred-alistfunction
(defun polypred-instantiated-pred-alist
  (ppred->tname-map new-types wrld)
  (b* ((m (append (table-alist 'tvar-metadata-table
           wrld)
         new-types
         (table-alist 'type-metadata-table
           wrld))) (a (table-alist 'type-alias-table
          wrld))
      (inst-preds (predicate-names (strip-cdrs ppred->tname-map)
          a
          m)))
    (pairlis$ (strip-cars ppred->tname-map)
      inst-preds)))
functional-instantiation-listfunction
(defun functional-instantiation-list
  (ppred->tname-map tvar-sigma
    new-types
    kwd-alist
    wrld)
  (b* ((m (append (table-alist 'tvar-metadata-table
           wrld)
         new-types
         (table-alist 'type-metadata-table
           wrld))) (a (table-alist 'type-alias-table
          wrld))
      (a1 (pairlis$ (predicate-names/lambdas (sublis-var-lst *tvar-typename-alist*
              (strip-cars tvar-sigma))
            a
            m)
          (predicate-names/lambdas (strip-cdrs tvar-sigma)
            a
            m)))
      (a2 (polypred-instantiated-pred-alist ppred->tname-map
          new-types
          wrld))
      (ans (union-alist2 a2 a1))
      (ctx 'functional-instantiation-alist)
      (- (cw? (and (or t (get1 :verbose kwd-alist t))
            (not (alist-equiv ans
                (union-alist2 a1 a2))))
          "~|Defdata/Warning:: ~x0 - tvar-sigma ~x1 entries differ from ppred-instpred-map ~x2"
          ctx
          a1
          a2)))
    (dlistify (remove-duplicates-equal ans))))
polypred-typename-mapfunction
(defun polypred-typename-map
  (tvar-sigma derived-pred->poly-texp-map
    new-types
    wrld)
  (b* ((ppred->texp-map (subst-vals derived-pred->poly-texp-map
         tvar-sigma)) (m (append new-types
          (table-alist 'type-metadata-table
            wrld))))
    (pairlis$ (strip-cars ppred->texp-map)
      (find-type-names1 (strip-cdrs ppred->texp-map)
        m))))
other
(defloop filter-proper-symbols
  (xs)
  (for ((x in xs))
    (append (and (proper-symbolp x) (list x)))))
other
(defloop filter-true-lists
  (xs wrld)
  (for ((x in xs))
    (append (and (subtype-p x 'true-listp wrld)
        (list x)))))
psig-templ-instantiation-ev-userfunction
(defun psig-templ-instantiation-ev-user
  (tname tvar-sigma
    templ
    derived-pred->poly-texp-map
    new-types
    kwd-alist
    wrld)
  "For given tvar-sigma, find functional instantiation and return instantiated templ"
  (b* ((ppred->tname-map (polypred-typename-map tvar-sigma
         derived-pred->poly-texp-map
         new-types
         wrld)) (templ (remove-exprs-with-fns templ
          (undefined-preds ppred->tname-map)))
      (fun-inst-dlist (functional-instantiation-list (remove-undefined ppred->tname-map)
          tvar-sigma
          new-types
          kwd-alist
          wrld))
      (a (table-alist 'type-alias-table
          wrld))
      (pred (predicate-name tname
          a
          (append new-types
            (table-alist 'type-metadata-table
              wrld))))
      (disabled (remove-eq pred
          (union-eq (filter-proper-symbols (strip-cadrs fun-inst-dlist))
            (get1 :disabled kwd-alist))))
      (disabled (set-difference-eq disabled
          (filter-true-lists disabled wrld)))
      (enabled (and pred (list pred)))
      (splice-alist `((_enabled-runes_ . ,DEFDATA::ENABLED) (_disabled-runes_ . ,DEFDATA::DISABLED)
          (_fun-inst-alist_ . ,DEFDATA::FUN-INST-DLIST)))
      (ppred-inst-pred-alist (polypred-instantiated-pred-alist ppred->tname-map
          new-types
          wrld))
      (atom-alist (acons '_pred_
          pred
          ppred-inst-pred-alist))
      (str-alist (acons "_PRED_" (symbol-name pred) 'nil)))
    (template-subst templ
      :features nil
      :splice-alist splice-alist
      :atom-alist atom-alist
      :str-alist str-alist
      :pkg-sym (fix-intern$ "a"
        (get1 :current-package kwd-alist)))))
other
(defttag t)
other
(defattach (psig-templ-instantiation-ev psig-templ-instantiation-ev-user)
  :skip-checks t)
other
(defttag nil)
other
(defloop psig-templ-instantiation-events
  (ps templ
    derived-pred->poly-texp-map
    new-types
    kwd-alist
    wrld)
  (for ((p in ps))
    (append (psig-templ-instantiation-ev (car p)
        (cdr p)
        templ
        derived-pred->poly-texp-map
        new-types
        kwd-alist
        wrld))))
other
(def-const *map-all-to-a*
  (pairlis$ *allowed-type-vars*
    (make-list (len *allowed-type-vars*)
      :initial-element ':a)))
other
(mutual-recursion (defun simplify-prop-comb-texp
    (pdef)
    (cond ((atom pdef) pdef)
      ((possible-constant-value-p pdef) pdef)
      ((member-eq (car pdef)
         '(or and oneof anyof)) (b* ((rest (remove-duplicates-equal (simplify-prop-comb-texps (cdr pdef)))))
          (if (consp (cdr rest))
            (cons 'or rest)
            (car rest))))
      (t (cons (car pdef)
          (simplify-prop-comb-texps (cdr pdef))))))
  (defun simplify-prop-comb-texps
    (texps)
    (if (endp texps)
      'nil
      (cons (simplify-prop-comb-texp (car texps))
        (simplify-prop-comb-texps (cdr texps))))))
find-matchfunction
(defun find-match
  (ptype pdef)
  (b* ((pdef (remove-names pdef)) ((mv yes sigma) (one-way-unify ptype pdef))
      ((when yes) (mv t sigma)))
    (if (eq (car ptype) 'listof)
      (b* (((mv yes sigma) (one-way-unify ptype
             (simplify-prop-comb-texp (sublis-var *map-all-to-a* pdef)))) ((unless yes) (mv yes sigma))
          (val (cdr (car sigma)))
          (tvars (all-vars pdef))
          (sigma (pairlis$ tvars
              (make-list (len tvars)
                :initial-element val))))
        (mv t sigma))
      (mv nil nil))))
find-matches1function
(defun find-matches1
  (ptype m)
  (if (endp m)
    'nil
    (b* (((cons tname al) (car m)) (pdef (get1 :prettyified-def al))
        ((unless pdef) (find-matches1 ptype (cdr m)))
        ((mv yes sigma) (find-match ptype pdef)))
      (if yes
        (cons (cons tname sigma)
          (find-matches1 ptype (cdr m)))
        (find-matches1 ptype (cdr m))))))
find-matchesfunction
(defun find-matches
  (ptype wrld)
  (find-matches1 ptype
    (table-alist 'type-metadata-table
      wrld)))
find/make-type-namefunction
(defun find/make-type-name
  (ptexp m)
  (if (and (proper-symbolp ptexp)
      (assoc ptexp m))
    ptexp
    (to-symbol ptexp "DEFDATA")))
other
(defloop find/make-type-names
  (ptexps m)
  (for ((ptexp in ptexps))
    (collect (find/make-type-name ptexp m))))
find/make-predicate-namefunction
(defun find/make-predicate-name
  (tname a m)
  (or (predicate-name tname
      a
      m)
    (make-predicate-symbol tname
      (symbol-package-name tname))))
other
(defloop find/make-predicate-names
  (tnames a m)
  (for ((tname in tnames))
    (collect (find/make-predicate-name tname
        a
        m))))
instantiate-poly-sig-events-for-current-typesfunction
(defun instantiate-poly-sig-events-for-current-types
  (as rtype
    templ
    kwd-alist
    wrld)
  "limited/linear instantiation of poly signatures for all current types of same shape"
  (declare (ignorable rtype))
  (b* ((atype (pick-dominant-poly-type-expr (append as (list rtype)))) ((when (null atype)) nil)
      ((when (symbolp atype)) nil)
      (tname-ia-alst (find-matches atype wrld))
      (m (append (table-alist 'tvar-metadata-table
            wrld)
          (table-alist 'type-metadata-table
            wrld)))
      (a (table-alist 'type-alias-table
          wrld))
      (arg-tnames (find/make-type-names (remove-names-lst as)
          m))
      (arg-preds (find/make-predicate-names arg-tnames
          a
          m))
      (ret-tname (find/make-type-name (remove-names rtype)
          m))
      (ret-pred (find/make-predicate-name ret-tname
          a
          m))
      (derived-pred->poly-texp-map (cons (cons ret-pred rtype)
          (pairlis$ arg-preds as))))
    (psig-templ-instantiation-events tname-ia-alst
      templ
      derived-pred->poly-texp-map
      'nil
      kwd-alist
      wrld)))
other
(defloop untrans-top-texps
  (nms nexps)
  (for ((nm in nms) (nexp in nexps))
    (collect (untrans-top-texp nm nexp 'nil))))
make-sig-defthm-bodyfunction
(defun make-sig-defthm-body
  (name arg-types
    ret-type
    kwd-alist
    wrld)
  (b* ((m (append (table-alist 'tvar-metadata-table
           wrld)
         (table-alist 'type-metadata-table
           wrld))) (a (table-alist 'type-alias-table
          wrld))
      (arg-tnames (find/make-type-names (remove-names-lst arg-types)
          m))
      (arg-preds (find/make-predicate-names arg-tnames
          a
          m))
      (ret-tname (find/make-type-name (remove-names ret-type)
          m))
      (ret-pred (find/make-predicate-name ret-tname
          a
          m))
      (pkg (get1 :current-package kwd-alist))
      (x1--xk (numbered-vars (fix-intern$ "X" pkg)
          (len arg-preds)))
      (dependent-hyps (get1 :satisfies kwd-alist))
      (hyps (append (list-up-lists arg-preds x1--xk)
          dependent-hyps))
      (psig-defthm-body `(implies (and . ,DEFDATA::HYPS)
          ,(LIST DEFDATA::RET-PRED (CONS DEFDATA::NAME DEFDATA::X1--XK)))))
    psig-defthm-body))
other
(mutual-recursion (defun find-all-instances
    (pat term alists)
    (declare (xargs :mode :program))
    (mv-let (instancep alist)
      (one-way-unify pat term)
      (let ((alists (if instancep
             (add-to-set-equal alist alists)
             alists)))
        (cond ((variablep term) alists)
          ((fquotep term) alists)
          (t (find-all-instances-list pat
              (fargs term)
              alists))))))
  (defun find-all-instances-list
    (pat list-of-terms alists)
    (declare (xargs :mode :program))
    (cond ((null list-of-terms) alists)
      (t (find-all-instances pat
          (car list-of-terms)
          (find-all-instances-list pat
            (cdr list-of-terms)
            alists))))))
map-find-all-instances-listfunction
(defun map-find-all-instances-list
  (pats list-of-terms acc)
  (declare (xargs :mode :program))
  (if (endp pats)
    acc
    (let ((instances (find-all-instances-list (car pats)
           list-of-terms
           nil)))
      (if instances
        (map-find-all-instances-list (cdr pats)
          list-of-terms
          (cons instances acc))
        nil))))
common-instancespfunction
(defun common-instancesp
  (x y)
  (and (consp x)
    (or (member-equal (car x) y)
      (common-instancesp (cdr x) y))))
in-allfunction
(defun in-all
  (a l)
  (or (atom l)
    (and (member-equal a (car l))
      (in-all a (cdr l)))))
common-instances-listpfunction
(defun common-instances-listp
  (l)
  (cond ((atom (car l)) nil)
    ((atom (cdr l)) (consp (car l)))
    (t (or (in-all (caar l) (cdr l))
        (common-instances-listp (cons (cdar l) (cdr l)))))))
make-sig-hint-bodyfunction
(defun make-sig-hint-body
  (name arg-types
    poly-gen-name
    kwd-alist
    wrld)
  (b* ((m (append (table-alist 'tvar-metadata-table
           wrld)
         (table-alist 'type-metadata-table
           wrld))) (a (table-alist 'type-alias-table
          wrld))
      (arg-tnames (find/make-type-names (remove-names-lst arg-types)
          m))
      (arg-preds (find/make-predicate-names arg-tnames
          a
          m))
      (pkg (get1 :current-package kwd-alist))
      (x1--xk (numbered-vars (fix-intern$ "X" pkg)
          (len arg-preds)))
      (dependent-hyps (get1 :satisfies kwd-alist))
      (hyps (append (list-up-lists arg-preds x1--xk)
          dependent-hyps))
      (psig-hint-body `(if (and stable-under-simplificationp
            (member-eq (access history-entry (car hist) :processor)
              '(fertilize-clause simplify-clause))
            (b* ((instances-name (find-all-instances-list '(,DEFDATA::NAME ,@DEFDATA::X1--XK)
                   clause
                   nil)) ((unless instances-name) nil)
                (map-instances (map-find-all-instances-list ',DEFDATA::HYPS
                    clause
                    nil))
                ((unless map-instances) nil)
                (common-insts (common-instances-listp (cons instances-name map-instances))))
              common-insts))
          '(:in-theory (union-theories (current-theory :here)
              '(,DEFDATA::POLY-GEN-NAME)))
          nil)))
    psig-hint-body))
sig-events1function
(defun sig-events1
  (name suffix
    arg-types
    ret-type
    kwd-alist
    ctx
    wrld)
  (b* ((arg-type-list1 (sublis-var-lst *tvar-typename-alist*
         arg-types)) (return-type1 (sublis-var *tvar-typename-alist*
          ret-type))
      (arity (len arg-types))
      (pkg (get1 :current-package kwd-alist))
      (star (fix-intern$ "*" pkg))
      (stars (make-list arity :initial-element star))
      (n-arg-types (parse-top-texps stars
          arg-type-list1
          ctx
          wrld))
      (n-ret-type (parse-top-texp star
          return-type1
          (list star)
          ctx
          wrld))
      (p-arg-types (untrans-top-texps stars
          n-arg-types))
      (p-ret-type (untrans-top-texp star
          n-ret-type
          'nil))
      (name-pre (if suffix
          (s+ name
            '-
            suffix
            :pkg pkg)
          name))
      (psig-name (s+ name-pre
          "-POLYMORPHIC-SIG"
          :pkg pkg))
      (poly-inst-name (s+ name-pre
          "-_PRED_-SIG"
          :pkg pkg))
      (poly-gen-name (s+ name-pre
          "-_PRED_-GENRULE-SIG"
          :pkg pkg))
      (poly-hint-name (s+ name-pre
          "-_PRED_-GENRULE-HINT-SIG"
          :pkg pkg))
      (psig-defthm-body (make-sig-defthm-body name
          p-arg-types
          p-ret-type
          kwd-alist
          wrld))
      (psig-hint-body (make-sig-hint-body name
          p-arg-types
          poly-gen-name
          kwd-alist
          wrld))
      (poly-inst-template `((defthm ,DEFDATA::POLY-INST-NAME
           ,DEFDATA::PSIG-DEFTHM-BODY
           :hints (("Goal" :in-theory (e/d (_enabled-runes_)
                (,DEFDATA::NAME _disabled-runes_))
              :use ((:functional-instance ,DEFDATA::PSIG-NAME
                 _fun-inst-alist_))))
           :rule-classes ,(DEFDATA::GET1 :RULE-CLASSES DEFDATA::KWD-ALIST '(:REWRITE)))))
      (poly-gen-template `((defthmd ,DEFDATA::POLY-GEN-NAME
           ,DEFDATA::PSIG-DEFTHM-BODY
           :hints (("Goal" :by ,DEFDATA::POLY-INST-NAME))
           :rule-classes :generalize)))
      (poly-hints-defun `((defun ,DEFDATA::POLY-HINT-NAME
           (clause stable-under-simplificationp
             id
             hist
             pspv
             ctx)
           (declare (ignorable id
               hist
               pspv
               ctx))
           (declare (xargs :mode :program))
           ,DEFDATA::PSIG-HINT-BODY)))
      (poly-computed-hints `((add-default-hints! '((,DEFDATA::POLY-HINT-NAME clause
              stable-under-simplificationp
              id
              hist
              pspv
              ctx))))))
    `(,@(DEFDATA::MAKE-SIG-TVAR-SUPPORT-EVENTS
   (CONS DEFDATA::P-RET-TYPE DEFDATA::P-ARG-TYPES) DEFDATA::CTX DEFDATA::PKG
   DEFDATA::WRLD) (defthm ,DEFDATA::PSIG-NAME
        ,DEFDATA::PSIG-DEFTHM-BODY
        :hints ,(OR (DEFDATA::GET1 :HINTS DEFDATA::KWD-ALIST)
     `(("Goal" :IN-THEORY (DEFDATA::ENABLE ,DEFDATA::NAME))))
        :rule-classes ,(DEFDATA::GET1 :GEN-RULE-CLASSES DEFDATA::KWD-ALIST '(:REWRITE)))
      ,@(DEFDATA::REGISTER-POLY-SIG-EVENTS DEFDATA::NAME DEFDATA::P-ARG-TYPES
   DEFDATA::P-RET-TYPE DEFDATA::POLY-INST-TEMPLATE DEFDATA::WRLD)
      ,@(DEFDATA::INSTANTIATE-POLY-SIG-EVENTS-FOR-CURRENT-TYPES DEFDATA::P-ARG-TYPES
   DEFDATA::P-RET-TYPE DEFDATA::POLY-INST-TEMPLATE DEFDATA::KWD-ALIST
   DEFDATA::WRLD)
      ,@(DEFDATA::INSTANTIATE-POLY-SIG-EVENTS-FOR-CURRENT-TYPES DEFDATA::P-ARG-TYPES
   DEFDATA::P-RET-TYPE DEFDATA::POLY-GEN-TEMPLATE DEFDATA::KWD-ALIST
   DEFDATA::WRLD)
      ,@(DEFDATA::INSTANTIATE-POLY-SIG-EVENTS-FOR-CURRENT-TYPES DEFDATA::P-ARG-TYPES
   DEFDATA::P-RET-TYPE DEFDATA::POLY-HINTS-DEFUN DEFDATA::KWD-ALIST
   DEFDATA::WRLD)
      ,@(DEFDATA::INSTANTIATE-POLY-SIG-EVENTS-FOR-CURRENT-TYPES DEFDATA::P-ARG-TYPES
   DEFDATA::P-RET-TYPE DEFDATA::POLY-COMPUTED-HINTS DEFDATA::KWD-ALIST
   DEFDATA::WRLD))))
sig-eventsfunction
(defun sig-events
  (parsed wrld)
  (b* (((list name
        suffix
        arg-types
        ret-type
        kwd-alist) parsed) (cgenp (logical-namep 'acl2s-defaults wrld))
      (local-testing-downgraded-form (and cgenp
          '((local (acl2s-defaults :set testing-enabled nil))))))
    `(with-output :on (summary error comment)
      :summary-off (:other-than form)
      (encapsulate nil
        (logic)
        ,@DEFDATA::LOCAL-TESTING-DOWNGRADED-FORM
        ,@(DEFDATA::SIG-EVENTS1 DEFDATA::NAME DEFDATA::SUFFIX DEFDATA::ARG-TYPES
   DEFDATA::RET-TYPE DEFDATA::KWD-ALIST 'DEFDATA::SIG DEFDATA::WRLD)))))
sigmacro
(defmacro sig
  (&rest args)
  (b* ((verbose (let ((lst (member :verbose args)))
         (and lst (cadr lst)))))
    `(with-output ,@(AND (NOT DEFDATA::VERBOSE) '(:OFF :ALL :ON DEFDATA::COMMENT))
      :gag-mode t
      :stack :push (make-event (sig-events (parse-sig ',DEFDATA::ARGS
            (current-package state)
            'sig
            (w state))
          (w state))))))