other
(in-package "FTY")
other
(include-book "std/util/da-base" :dir :system)
other
(include-book "xdoc/str" :dir :system)
other
(def-primitive-aggregate flexprod-field
(name acc-body
acc-name
type
fix
equiv
reqfix
reqfix-vars
default
doc
rule-classes
recp
shared)
:tag :field)
other
(def-primitive-aggregate flexprod (kind cond guard shape require fields type-name ctor-name ctor-macro ctor-body remake-name remake-body short long inline extra-binder-names count-incr no-ctor-macros) :tag :prod)
other
(def-primitive-aggregate flexsum
(name pred
fix
equiv
kind
kind-body
count
case
prods
measure
shape
xvar
kwd-alist
orig-prods
inline
recp
typemacro
disable-type-prescription)
:tag :sum)
other
(def-primitive-aggregate flexlist
(name pred
fix
equiv
count
elt-type
elt-fix
elt-equiv
measure
xvar
non-emptyp
kwd-alist
true-listp
elementp-of-nil
cheap
recp
already-definedp
fix-already-definedp)
:tag :list)
other
(def-primitive-aggregate flexalist
(name pred
fix
equiv
count
key-type
key-fix
key-equiv
val-type
val-fix
val-equiv
strategy
measure
xvar
kwd-alist
keyp-of-nil
valp-of-nil
true-listp
unique-keys
recp
already-definedp
fix-already-definedp)
:tag :alist)
other
(def-primitive-aggregate flextranssum-member
(name pred
fix
equiv
tags
recp)
:tag :flextranssum-member)
other
(def-primitive-aggregate flextranssum
(name pred
fix
equiv
count
case
kind
members
measure
xvar
kwd-alist
inline
recp)
:tag :transsum)
other
(def-primitive-aggregate flexset
(name pred
fix
equiv
count
elt-type
elt-fix
elt-equiv
measure
xvar
kwd-alist
elementp-of-nil
recp
already-definedp
fix-already-definedp)
:tag :set)
other
(def-primitive-aggregate flexomap
(name pred
fix
equiv
count
key-type
key-fix
key-equiv
val-type
val-fix
val-equiv
measure
xvar
kwd-alist
keyp-of-nil
valp-of-nil
recp
already-definedp
fix-already-definedp)
:tag :omap)
other
(def-primitive-aggregate flextypes
(name types
kwd-alist
no-count
recp)
:tag :flextypes)
other
(defund flexprod-field-listp (x) (declare (xargs :guard t)) (if (consp x) (and (flexprod-field-p (car x)) (flexprod-field-listp (cdr x))) (null x)))
other
(defund flexprod-listp (x) (declare (xargs :guard t)) (if (consp x) (and (flexprod-p (car x)) (flexprod-listp (cdr x))) (null x)))
other
(defund flexsum-listp (x) (declare (xargs :guard t)) (if (consp x) (and (flexsum-p (car x)) (flexsum-listp (cdr x))) (null x)))
other
(table flextypes-table)
get-flextypesfunction
(defun get-flextypes (world) (declare (xargs :guard (plist-worldp world))) "Get the database of defined flextypes." (table-alist 'flextypes-table world))
add-flextypemacro
(defmacro add-flextype (x) (declare (xargs :guard (flextypes-p x))) `(table flextypes-table ',(FTY::FLEXTYPES->NAME FTY::X) ',FTY::X))
flexprod-fields->namesfunction
(defun flexprod-fields->names (fields) (declare (xargs :mode :program)) (if (atom fields) nil (cons (flexprod-field->name (car fields)) (flexprod-fields->names (cdr fields)))))
flexprod-fields->defaultsfunction
(defun flexprod-fields->defaults (fields) (declare (xargs :mode :program)) (if (atom fields) nil (cons (flexprod-field->default (car fields)) (flexprod-fields->defaults (cdr fields)))))
flexprod-fields->acc-namesfunction
(defun flexprod-fields->acc-names (fields) (declare (xargs :mode :program)) (if (atom fields) nil (cons (flexprod-field->acc-name (car fields)) (flexprod-fields->acc-names (cdr fields)))))
flexprods->kindsfunction
(defun flexprods->kinds (prods) (declare (xargs :mode :program)) (if (atom prods) nil (cons (flexprod->kind (car prods)) (flexprods->kinds (cdr prods)))))
replace-*-in-symbol-with-strfunction
(defun replace-*-in-symbol-with-str (x str) (declare (xargs :mode :program)) (b* ((name (symbol-name x)) (idx (search "*" name)) ((unless idx) x) (newname (cat (subseq name 0 idx) str (subseq name (+ 1 idx) nil)))) (intern-in-package-of-symbol newname x)))
replace-*-in-symbols-with-str-recfunction
(defun replace-*-in-symbols-with-str-rec (x str) (declare (xargs :mode :program)) (b* (((when (atom x)) (if (symbolp x) (let* ((newx (replace-*-in-symbol-with-str x str))) (if (eq newx x) (mv nil x) (mv t newx))) (mv nil x))) ((mv changed1 car) (replace-*-in-symbols-with-str-rec (car x) str)) ((mv changed2 cdr) (replace-*-in-symbols-with-str-rec (cdr x) str)) ((unless (or changed1 changed2)) (mv nil x))) (mv t (cons car cdr))))
has-vardot-symsfunction
(defun has-vardot-syms (x vardot) (declare (xargs :mode :program)) (if (atom x) (and (symbolp x) (eql (search vardot (symbol-name x)) 0)) (or (has-vardot-syms (car x) vardot) (has-vardot-syms (cdr x) vardot))))
replace-*-in-symbols-with-strfunction
(defun replace-*-in-symbols-with-str (x str) (declare (xargs :mode :program)) (b* (((mv ?ch newx) (replace-*-in-symbols-with-str-rec x str))) newx))
with-flextype-bindings-fnfunction
(defun with-flextype-bindings-fn (binding body default) (declare (xargs :mode :program)) (b* ((var (if (consp binding) (car binding) binding)) (add-binds (has-vardot-syms body (cat (symbol-name var) "."))) (sumbody (replace-*-in-symbols-with-str body "SUM")) (listbody (replace-*-in-symbols-with-str body "LIST")) (alistbody (replace-*-in-symbols-with-str body "ALIST")) (transsumbody (replace-*-in-symbols-with-str body "TRANSSUM")) (setbody (replace-*-in-symbols-with-str body "SET")) (omapbody (replace-*-in-symbols-with-str body "OMAP")) (cases `(case (tag ,FTY::VAR) (:sum ,(IF FTY::ADD-BINDS `(FTY::B* (((FTY::FLEXSUM ,FTY::VAR) ,FTY::VAR)) ,FTY::SUMBODY) FTY::SUMBODY)) (:list ,(IF FTY::ADD-BINDS `(FTY::B* (((FTY::FLEXLIST ,FTY::VAR) ,FTY::VAR)) ,FTY::LISTBODY) FTY::LISTBODY)) (:alist ,(IF FTY::ADD-BINDS `(FTY::B* (((FTY::FLEXALIST ,FTY::VAR) ,FTY::VAR)) ,FTY::ALISTBODY) FTY::ALISTBODY)) (:transsum ,(IF FTY::ADD-BINDS `(FTY::B* (((FTY::FLEXTRANSSUM ,FTY::VAR) ,FTY::VAR)) ,FTY::TRANSSUMBODY) FTY::TRANSSUMBODY)) (:set ,(IF FTY::ADD-BINDS `(FTY::B* (((FTY::FLEXSET ,FTY::VAR) ,FTY::VAR)) ,FTY::SETBODY) FTY::SETBODY)) (:omap ,(IF FTY::ADD-BINDS `(FTY::B* (((FTY::FLEXOMAP ,FTY::VAR) ,FTY::VAR)) ,FTY::OMAPBODY) FTY::OMAPBODY)) (otherwise ,FTY::DEFAULT)))) (if (consp binding) `(let ((,FTY::VAR ,(CADR FTY::BINDING))) ,FTY::CASES) cases)))
with-flextype-bindingsmacro
(defmacro with-flextype-bindings (binding body &key default) (with-flextype-bindings-fn binding body default))
flextypelist-recpfunction
(defun flextypelist-recp (x) (declare (xargs :mode :program)) (if (atom x) nil (or (with-flextype-bindings (x (car x)) x.recp) (flextypelist-recp (cdr x)))))
flextypelist-namesfunction
(defun flextypelist-names (types) (declare (xargs :mode :program)) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) x.name) (flextypelist-names (cdr types)))))
flextypelist-fixesfunction
(defun flextypelist-fixes (types) (declare (xargs :mode :program)) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) x.fix) (flextypelist-fixes (cdr types)))))
flextypelist-equivsfunction
(defun flextypelist-equivs (types) (declare (xargs :mode :program)) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) x.equiv) (flextypelist-equivs (cdr types)))))
flextypelist-predicatesfunction
(defun flextypelist-predicates (types) (declare (xargs :mode :program)) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) x.pred) (flextypelist-predicates (cdr types)))))
flextypes-find-count-for-predfunction
(defun flextypes-find-count-for-pred (pred types) (declare (xargs :mode :program)) (if (atom types) nil (or (with-flextype-bindings (x (car types)) (and (eq pred x.pred) x.count)) (flextypes-find-count-for-pred pred (cdr types)))))
search-deftypes-typesfunction
(defun search-deftypes-types (type-name types) (declare (xargs :mode :program)) (if (atom types) nil (or (with-flextype-bindings (x (car types)) (and (eq type-name x.name) x)) (search-deftypes-types type-name (cdr types)))))
search-deftypes-tablefunction
(defun search-deftypes-table (type-name table) (declare (xargs :mode :program)) (if (atom table) (mv nil nil) (let ((type (search-deftypes-types type-name (flextypes->types (cdar table))))) (if type (mv (cdar table) type) (search-deftypes-table type-name (cdr table))))))