other
(in-package "FTY")
other
(include-book "database")
other
(include-book "docgen")
other
(include-book "fixequiv")
other
(include-book "fty-sum")
other
(include-book "fty-alist")
other
(include-book "fty-list")
other
(include-book "fty-transsum")
other
(include-book "kestrel/fty/fty-set" :dir :system)
other
(include-book "kestrel/fty/fty-omap" :dir :system)
other
(include-book "fty-sugar")
other
(include-book "std/util/deflist-base" :dir :system)
other
(include-book "std/util/defalist-base" :dir :system)
other
(include-book "std/lists/acl2-count" :dir :system)
other
(set-state-ok t)
other
(set-compile-fns t)
other
(defthmd equal-of-strip-cars (implies (syntaxp (quotep y)) (equal (equal (strip-cars x) y) (if (atom y) (and (not y) (atom x)) (and (consp x) (equal (strip-cars (cdr x)) (cdr y)) (if (car y) (and (consp (car x)) (equal (caar x) (car y))) (or (atom (car x)) (equal (caar x) nil))))))))
other
(defthm strip-cars-under-iff (iff (strip-cars x) (consp x)))
other
(defthmd equal-of-plus-one (implies (syntaxp (quotep y)) (equal (equal (+ 1 x) y) (and (acl2-numberp y) (equal (fix x) (+ -1 y))))))
other
(defthmd consp-when-tag (implies (tag x) (consp x)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
other
(defthmd equal-of-len (implies (syntaxp (quotep n)) (equal (equal (len x) n) (if (zp n) (and (equal n 0) (not (consp x))) (and (consp x) (equal (len (cdr x)) (+ -1 n)))))))
other
(defthmd open-member-equal-on-list-of-tags (implies (syntaxp (and (quotep val) (symbol-listp (unquote val)))) (equal (member-equal a val) (cond ((atom val) nil) ((equal a (car val)) val) (t (member-equal a (cdr val)))))) :hints (("Goal" :in-theory (enable member-equal))))
other
(defthmd alistp-compound-recognizer (implies (alistp x) (true-listp x)) :rule-classes :compound-recognizer)
other
(define equal-when-strip-cars ((x alistp) y cars) :measure (len cars) (if (atom cars) (equal y nil) (and (consp y) (consp (car y)) (equal (caar y) (car cars)) (equal (cdar y) (cdar x)) (equal-when-strip-cars (cdr x) (cdr y) (cdr cars)))) /// (defthm equal-when-strip-cars-of-nil (equal (equal-when-strip-cars x y nil) (equal y nil))) (defthmd equal-when-strip-cars-of-cons (equal (equal-when-strip-cars x (cons (cons key val) rest-y) (cons key rest-cars)) (and (equal val (cdar x)) (equal-when-strip-cars (cdr x) rest-y rest-cars)))) (local (in-theory (disable cons-car-cdr))) (defthmd equal-of-strip-cars-correct (implies (and (alistp x) (equal (strip-cars x) (true-list-fix cars))) (equal (equal-when-strip-cars x y cars) (equal x y))) :hints (("Goal" :induct (equal-when-strip-cars x y cars) :in-theory (disable (:d equal-when-strip-cars)) :expand ((equal-when-strip-cars x y cars) (equal-when-strip-cars nil nil cars) (equal-when-strip-cars nil y cars) (strip-cars x) (true-list-fix cars) (alistp x))))) (local (defthm true-list-fix-of-strip-cars (equal (true-list-fix (strip-cars x)) (strip-cars x)) :hints (("Goal" :in-theory (enable true-list-fix))))) (defthmd equal-of-cons-by-equal-of-strip-cars (implies (and (equal (strip-cars x) cars) (syntaxp (quotep cars)) (true-listp cars) (alistp x)) (equal (equal (cons (cons key1 val1) rest) x) (equal-when-strip-cars x (cons (cons key1 val1) rest) cars))) :hints (("Goal" :in-theory (e/d (equal-of-strip-cars-correct true-list-fix) (equal-when-strip-cars)) :do-not-induct t))))
other
(defthmd prove-equal-of-cons-when-first-quotep (implies (and (syntaxp (quotep car)) (consp x) (equal (car x) car) (equal (cdr x) cdr)) (equal (equal (cons car cdr) x) t)))
other
(deftheory deftypes-theory '(prove-equal-of-cons-when-first-quotep equal-when-strip-cars-of-cons equal-when-strip-cars-of-nil equal-of-cons-by-equal-of-strip-cars car-cons cdr-cons strip-cars strip-cars-under-iff eqlablep (len) len-of-cons equal-of-len (zp) (:t acl2-count) acl2-count-of-car acl2-count-of-cdr acl2-count-of-consp-positive acl2-count-of-cons-greater o< o-finp (natp) natp-compound-recognizer hons open-member-equal-on-list-of-tags alistp-compound-recognizer alistp identity prod-car prod-cdr prod-hons cons-with-hint prod-cons-with-hint car-of-prod-cons cdr-of-prod-cons prod-cons-of-car/cdr acl2-count-of-prod-cons prod-cons-equal-cons prod-cons-when-either prod-consp-compound-recognizer prod-cons-not-consp-forward))
other
(program)
parse-flextypelistfunction
(defun parse-flextypelist (x xvar our-fixtypes fixtypes state) (if (atom x) nil (cons (case (caar x) (defflexsum (parse-flexsum (cdar x) xvar our-fixtypes fixtypes state)) (defprod (parse-defprod (cdar x) xvar our-fixtypes fixtypes state)) (deftagsum (parse-tagsum (cdar x) xvar our-fixtypes fixtypes state)) (defoption (parse-option (cdar x) xvar our-fixtypes fixtypes state)) (deftranssum (parse-transsum (cdar x) xvar our-fixtypes fixtypes state)) (deflist (parse-flexlist (cdar x) xvar our-fixtypes fixtypes state)) (defalist (parse-flexalist (cdar x) xvar our-fixtypes fixtypes state)) (defmap (let ((al (parse-flexalist (cdar x) xvar our-fixtypes fixtypes state))) (change-flexalist al :strategy :drop-keys))) (defset (parse-flexset (cdar x) xvar our-fixtypes fixtypes state)) (defomap (parse-flexomap (cdar x) xvar our-fixtypes fixtypes state)) (otherwise (er hard? 'parse-flextypelist "Recognized flextypes are ~x0, not ~x1~%" *known-flextype-generators* (caar x)))) (parse-flextypelist (cdr x) xvar our-fixtypes fixtypes state))))
other
(defconst *flextypes-keywords* '(:xvar :no-count :parents :short :long :prepwork :post-pred-events :post-fix-events :post-acc-events :post-events :enable-rules :verbosep))
flextypelist-check-bad-namefunction
(defun flextypelist-check-bad-name (types) (if (atom types) nil (prog2$ (b* ((main-lisp-pkg *main-lisp-package-name*)) (with-flextype-bindings (x (car types)) (and (equal (symbol-package-name x.name) main-lisp-pkg) (er hard? 'flextypelist-check-bad-name "Name must be a symbol not in the ~s0 package: ~x1~%" main-lisp-pkg x.name)))) (flextypelist-check-bad-name (cdr types)))))
parse-flextypesfunction
(defun parse-flextypes (x state) (b* (((cons name x) x) ((unless (symbolp name)) (er hard? 'parse-flextypes "Malformed flextypes: name must be a symbol, but found ~x0" name)) ((when (equal (symbol-package-name name) *main-lisp-package-name*)) (er hard? 'parse-flextypes "Name must be a symbol not in the ~s0 package: ~x1~%" *main-lisp-package-name* name)) ((mv pre-/// post-///) (split-/// 'parse-flexsum x)) ((mv kwd-alist typedecls) (extract-keywords 'parse-flextypes *flextypes-keywords* pre-/// nil)) (our-fixtypes (flextype-forms->fixtypes typedecls)) (fixtype-al (append our-fixtypes (get-fixtypes-alist (w state)))) (xvar (getarg :xvar nil kwd-alist)) (no-count (getarg :no-count nil kwd-alist)) (types (parse-flextypelist typedecls xvar our-fixtypes fixtype-al state))) (make-flextypes :name name :types types :no-count no-count :kwd-alist (if post-/// (cons (cons :///-events post-///) kwd-alist) kwd-alist) :recp (flextypelist-recp types))))
flextypelist-predicate-defsfunction
(defun flextypelist-predicate-defs (types) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) (flex*-predicate-def x)) (flextypelist-predicate-defs (cdr types)))))
flextypes-predicate-deffunction
(defun flextypes-predicate-def (x) (b* (((flextypes x) x) (defs (flextypelist-predicate-defs x.types))) (if (atom (cdr x.types)) `(,(CAR FTY::DEFS) (local (in-theory (disable . ,(FTY::FLEXTYPELIST-PREDICATES FTY::X.TYPES))))) `((defines ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL (FTY::CAT (SYMBOL-NAME FTY::X.NAME) "-P") FTY::X.NAME) :progn t ,@FTY::DEFS) (local (in-theory (disable . ,(FTY::FLEXTYPELIST-PREDICATES FTY::X.TYPES))))))))
flextypelist-fix-defsfunction
(defun flextypelist-fix-defs (types flagp) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) (flex*-fix-def x flagp)) (flextypelist-fix-defs (cdr types) flagp))))
flextypelist-fix-posteventsfunction
(defun flextypelist-fix-postevents (types) (if (atom types) nil (append (with-flextype-bindings (x (car types)) (flex*-fix-postevents x)) (flextypelist-fix-postevents (cdr types)))))
flextypelist-fix-when-pred-thmsfunction
(defun flextypelist-fix-when-pred-thms (types flagp) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) (flex*-fix-when-pred-thm x flagp)) (flextypelist-fix-when-pred-thms (cdr types) flagp))))
flextypelist-pred-callsfunction
(defun flextypelist-pred-calls (types) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) (list x.pred x.xvar)) (flextypelist-pred-calls (cdr types)))))
flextypelist-fixtypesfunction
(defun flextypelist-fixtypes (types) (if (atom types) nil (append (with-flextype-bindings (x (car types)) `((defsection ,FTY::X.EQUIV :parents (,FTY::X.NAME) :short ,(FTY::CAT "Basic equivalence relation for " (XDOC::SEE FTY::X.NAME) " structures.") (deffixtype ,FTY::X.NAME :pred ,FTY::X.PRED :fix ,FTY::X.FIX :equiv ,FTY::X.EQUIV :define t :forward t)) (local (in-theory (enable ,FTY::X.EQUIV))))) (flextypelist-fixtypes (cdr types)))))
flextypes-form-append-hintsfunction
(defun flextypes-form-append-hints (new-hints form) (b* ((mem (member :hints form)) ((unless mem) (append form `(:hints ,FTY::NEW-HINTS))) (prefix (take (- (len form) (len mem)) form))) (append prefix (cons :hints (cons (append new-hints (cadr mem)) (cddr mem))))))
flextypes-collect-sum-kind-callsfunction
(defun flextypes-collect-sum-kind-calls (types) (if (atom types) nil (append (case (tag (car types)) (:sum (b* (((flexsum sum) (car types))) (if sum.kind (list `(,FTY::SUM.KIND ,FTY::SUM.XVAR)) nil))) (otherwise nil)) (flextypes-collect-sum-kind-calls (cdr types)))))
flextypes-fix-deffunction
(defun flextypes-fix-def (x) (b* (((flextypes x) x) (flagp (consp (cdr x.types))) (defs (flextypelist-fix-defs x.types flagp)) (flag-name (and flagp (intern-in-package-of-symbol (cat (symbol-name x.name) "-FIX-FLAG") x.name))) (flag-defthm-name (and flagp (thm-macro-name flag-name))) (fix-when-pred-thms (flextypelist-fix-when-pred-thms x.types flagp)) (sum-kind-calls (flextypes-collect-sum-kind-calls x.types))) `(,(APPEND (IF FTY::FLAGP `(FTY::DEFINES ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL (FTY::CAT (SYMBOL-NAME FTY::X.NAME) "-FIX") FTY::X.NAME) :FLAG ,FTY::FLAG-NAME :BOGUS-OK T :PROGN T ,@(AND FTY::SUM-KIND-CALLS `(:HINTS ((AND FTY::STABLE-UNDER-SIMPLIFICATIONP '(:EXPAND ,FTY::SUM-KIND-CALLS))))) ,@FTY::DEFS ///) (CAR FTY::DEFS)) `((FTY::LOCAL (FTY::IN-THEORY (FTY::DISABLE . ,(FTY::PAIRLIS$ (MAKE-LIST (FTY::LEN FTY::X.TYPES) :INITIAL-ELEMENT :D) (FTY::PAIRLIS$ (FTY::FLEXTYPELIST-FIXES FTY::X.TYPES) NIL))))) ,(IF FTY::FLAGP `(,FTY::FLAG-DEFTHM-NAME . ,FTY::FIX-WHEN-PRED-THMS) (IF FTY::X.RECP (FTY::FLEXTYPES-FORM-APPEND-HINTS '(("goal" :INDUCT T)) (CAR FTY::FIX-WHEN-PRED-THMS)) (CAR FTY::FIX-WHEN-PRED-THMS))) (FTY::VERIFY-GUARDS+ ,(FTY::WITH-FLEXTYPE-BINDINGS (FTY::X (CAR FTY::X.TYPES)) FTY::X.FIX) :HINTS (("goal" :EXPAND (,@(APPEND (FTY::FLEXTYPELIST-PRED-CALLS FTY::X.TYPES) FTY::SUM-KIND-CALLS))))) ,@(FTY::FLEXTYPELIST-FIXTYPES FTY::X.TYPES) . ,(FTY::FLEXTYPELIST-FIX-POSTEVENTS FTY::X.TYPES))) (local (in-theory (enable . ,(FTY::FLEXTYPELIST-EQUIVS FTY::X.TYPES)))) (local (in-theory (disable . ,(FTY::FLEXTYPELIST-FIXES FTY::X.TYPES)))))))
flextypes-fnsfunction
(defun flextypes-fns (types) (if (atom types) nil (append (with-flextype-bindings (x (car types)) (flex*-fns x)) (flextypes-fns (cdr types)))))
flextypes-acc/ctorsfunction
(defun flextypes-acc/ctors (types) (if (atom types) nil (append (and (eq (caar types) :sum) (flexsum-prod-fns (flexsum->prods (car types)))) (flextypes-acc/ctors (cdr types)))))
flextypes-ctorsfunction
(defun flextypes-ctors (types) (if (atom types) nil (append (and (eq (caar types) :sum) (flexsum-prod-ctors (flexsum->prods (car types)))) (flextypes-ctors (cdr types)))))
flextypes-count-defsfunction
(defun flextypes-count-defs (x alltypes) (if (atom x) nil (append (with-flextype-bindings (x (car x)) (flex*-count x alltypes)) (flextypes-count-defs (cdr x) alltypes))))
flextypes-count-expandsfunction
(defun flextypes-count-expands (types) (if (atom types) nil (append (with-flextype-bindings (x (car types)) (and x.count `((,FTY::X.COUNT ,FTY::X.XVAR) (,FTY::X.COUNT (,FTY::X.FIX ,FTY::X.XVAR))))) (flextypes-count-expands (cdr types)))))
flextypes-count-namesfunction
(defun flextypes-count-names (x) (if (atom x) nil (append (with-flextype-bindings (x (car x)) (and x.count (list x.count))) (flextypes-count-names (cdr x)))))
flextypes-count-post-eventsfunction
(defun flextypes-count-post-events (types alltypes) (if (atom types) nil (append (with-flextype-bindings (x (car types)) (flex*-count-post-events x alltypes)) (flextypes-count-post-events (cdr types) alltypes))))
flextypes-nokind-expand-fixesfunction
(defun flextypes-nokind-expand-fixes (types) (if (atom types) nil (if (and (eq (tag (car types)) :sum) (not (flexsum->kind (car types)))) (cons `(,(FTY::FLEXSUM->FIX (CAR FTY::TYPES)) ,(FTY::FLEXSUM->XVAR (CAR FTY::TYPES))) (flextypes-nokind-expand-fixes (cdr types))) (flextypes-nokind-expand-fixes (cdr types)))))
flextypes-expand-fixesfunction
(defun flextypes-expand-fixes (types) (if (atom types) nil (cons (with-flextype-bindings (x (car types)) `(,FTY::X.FIX ,FTY::X.XVAR)) (flextypes-expand-fixes (cdr types)))))
flexprods-ctor-of-fields-thmsfunction
(defun flexprods-ctor-of-fields-thms (prods) (b* (((when (atom prods)) nil) ((unless (consp (flexprod->fields (car prods)))) (flexprods-ctor-of-fields-thms (cdr prods))) (foo-of-fields (intern-in-package-of-symbol (cat (symbol-name (flexprod->ctor-name (car prods))) "-OF-FIELDS") (flexprod->ctor-name (car prods))))) (cons foo-of-fields (flexprods-ctor-of-fields-thms (cdr prods)))))
flextypes-ctor-of-fields-thmsfunction
(defun flextypes-ctor-of-fields-thms (types) (if (atom types) nil (append (and (eq (caar types) :sum) (flexprods-ctor-of-fields-thms (flexsum->prods (car types)))) (flextypes-ctor-of-fields-thms (cdr types)))))
flexprods-fix-when-kind-thmsfunction
(defun flexprods-fix-when-kind-thms (prods sum) (b* (((when (atom prods)) nil) ((unless (consp (flexprod->fields (car prods)))) (flexprods-fix-when-kind-thms (cdr prods) sum)) (foo-fix-when-subfoo-kind (intern-in-package-of-symbol (cat (symbol-name (flexsum->fix sum)) "-WHEN-" (symbol-name (flexprod->kind (car prods)))) (flexsum->fix sum)))) (cons foo-fix-when-subfoo-kind (flexprods-fix-when-kind-thms (cdr prods) sum))))
flextypes-fix-when-kind-thmsfunction
(defun flextypes-fix-when-kind-thms (types) (if (atom types) nil (append (and (eq (caar types) :sum) (consp (cdr (flexsum->prods (car types)))) (flexprods-fix-when-kind-thms (flexsum->prods (car types)) (car types))) (flextypes-fix-when-kind-thms (cdr types)))))
flextypes-countfunction
(defun flextypes-count (x) (b* (((flextypes x) x) ((when x.no-count) nil) (defs (flextypes-count-defs x.types x.types)) (names (flextypes-count-names x.types)) ((when (not defs)) nil) (flagp (consp (cdr defs))) (measure-hints `((and stable-under-simplificationp '(:expand ,(FTY::FLEXTYPES-EXPAND-FIXES FTY::X.TYPES) :in-theory (e/d ,(FTY::FLEXTYPES-CTORS FTY::X.TYPES)))))) (prepwork `((local (in-theory (e/d ,(FTY::FLEXTYPES-FIX-WHEN-KIND-THMS FTY::X.TYPES) ,(FTY::FLEXTYPES-CTOR-OF-FIELDS-THMS FTY::X.TYPES))))))) (if flagp (let ((defines-name (intern-in-package-of-symbol (cat (symbol-name x.name) "-COUNT") x.name))) `((defines ,FTY::DEFINES-NAME :hints ,FTY::MEASURE-HINTS :prepwork ,FTY::PREPWORK :progn t ,@FTY::DEFS /// (local (in-theory (disable . ,(FTY::FLEXTYPES-COUNT-NAMES FTY::X.TYPES)))) (verify-guards+ ,(CADR (CAR FTY::DEFS))) (deffixequiv-mutual ,FTY::DEFINES-NAME :hints ((and stable-under-simplificationp (let ((lit (car (last clause)))) (and (eq (car lit) 'equal) (let ((expands (append (and (consp (cadr lit)) (member (car (cadr lit)) ',FTY::NAMES) (list (cadr lit))) (and (consp (caddr lit)) (member (car (caddr lit)) ',FTY::NAMES) (list (caddr lit)))))) (and expands `(:expand ,FTY::EXPANDS)))))))) . ,(FTY::FLEXTYPES-COUNT-POST-EVENTS FTY::X.TYPES FTY::X.TYPES)))) (list (append (car defs) `(:hints ,FTY::MEASURE-HINTS :prepwork ,FTY::PREPWORK /// (local (in-theory (disable . ,(FTY::FLEXTYPES-COUNT-NAMES FTY::X.TYPES)))) (verify-guards+ ,(CADR (CAR FTY::DEFS)) :hints ((and stable-under-simplificationp '(:expand ,(FTY::FLEXTYPES-NOKIND-EXPAND-FIXES FTY::X.TYPES))))) (deffixequiv ,(CADR (CAR FTY::DEFS)) :hints (("goal" :expand ,(FTY::FLEXTYPES-COUNT-EXPANDS FTY::X.TYPES)) (and stable-under-simplificationp '(:expand ,(FTY::FLEXTYPES-NOKIND-EXPAND-FIXES FTY::X.TYPES))))) . ,(FTY::FLEXTYPES-COUNT-POST-EVENTS FTY::X.TYPES FTY::X.TYPES)))))))
find-fix-when-pred-thm-auxfunction
(defun find-fix-when-pred-thm-aux (fix pred fix-rules) (if (atom fix-rules) (let ((body `(implies (,FTY::PRED x) (equal (,FTY::FIX x) x)))) (mv nil `(local (make-event '(:or (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL (FTY::CAT "TMP-DEFTYPES-" (SYMBOL-NAME FTY::FIX) "-WHEN-" (SYMBOL-NAME FTY::PRED)) 'FTY::FTY) ,FTY::BODY) (value-triple (er hard? 'deftypes "To use ~x0/~x1 as a fixing function/predicate, we must ~ be able to prove the following: ~x2. But this proof ~ failed! Please try to prove this rule yourself." ',FTY::FIX ',FTY::PRED ',FTY::BODY))))))) (let ((rune (b* ((rule (car fix-rules)) (subclass (access rewrite-rule rule :subclass)) ((unless (eq subclass 'backchain)) nil) (lhs (access rewrite-rule rule :lhs)) ((unless (symbolp (cadr lhs))) nil) (var (cadr lhs)) (rhs (access rewrite-rule rule :rhs)) ((unless (eq rhs var)) nil) (hyps (access rewrite-rule rule :hyps)) ((unless (and (consp hyps) (not (cdr hyps)) (consp (car hyps)) (eq pred (caar hyps)) (eq var (cadr (car hyps))))) nil) (equiv (access rewrite-rule rule :equiv)) ((unless (eq equiv 'equal)) nil) ((unless (eq (access rewrite-rule rule :backchain-limit-lst) nil)) nil)) (access rewrite-rule rule :rune)))) (if rune (mv t rune) (find-fix-when-pred-thm-aux fix pred (cdr fix-rules))))))
find-fix-when-unsigned-byte-p-pred-thm-auxfunction
(defun find-fix-when-unsigned-byte-p-pred-thm-aux (fix pred size fix-rules) (if (atom fix-rules) (let ((body `(implies (unsigned-byte-p ',FTY::SIZE x) (equal (,FTY::FIX x) x)))) (mv nil `(local (make-event '(:or (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL (FTY::CAT "TMP-DEFTYPES-" (SYMBOL-NAME FTY::FIX) "-WHEN-" (SYMBOL-NAME FTY::PRED)) 'FTY::FTY) ,FTY::BODY) (value-triple (er hard? 'deftypes "To use ~x0/~x1 as a fixing function/predicate, we must ~ be able to prove the following: ~x2. But this proof ~ failed! Please try to prove this rule yourself." ',FTY::FIX ',FTY::PRED ',FTY::BODY))))))) (let ((rune (b* ((rule (car fix-rules)) (subclass (access rewrite-rule rule :subclass)) ((unless (eq subclass 'backchain)) nil) (lhs (access rewrite-rule rule :lhs)) ((unless (symbolp (cadr lhs))) nil) (var (cadr lhs)) (rhs (access rewrite-rule rule :rhs)) ((unless (eq rhs var)) nil) (hyps (access rewrite-rule rule :hyps)) ((unless (and (consp hyps) (not (cdr hyps)) (consp (car hyps)) (eq 'unsigned-byte-p (caar hyps)) (consp (cadar hyps)) (equal 'quote (car (cadar hyps))) (eq size (cadr (cadar hyps))) (eq var (caddr (car hyps))))) nil) (equiv (access rewrite-rule rule :equiv)) ((unless (eq equiv 'equal)) nil) ((unless (eq (access rewrite-rule rule :backchain-limit-lst) nil)) nil)) (access rewrite-rule rule :rune)))) (if rune (mv t rune) (find-fix-when-unsigned-byte-p-pred-thm-aux fix pred size (cdr fix-rules))))))
find-pred-of-fix-thm-auxfunction
(defun find-pred-of-fix-thm-aux (fix pred pred-rules) (if (atom pred-rules) (let ((body `(,FTY::PRED (,FTY::FIX x)))) (mv nil `(local (make-event '(:or (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL (FTY::CAT "TMP-DEFTYPES-" (SYMBOL-NAME FTY::PRED) "-OF-" (SYMBOL-NAME FTY::FIX)) 'FTY::FTY) ,FTY::BODY) (value-triple (er hard? 'deftypes "To use ~x0/~x1 as a fixing function/predicate, we must ~ be able to prove the following: ~x2. But this proof ~ failed! Please try to prove this rule yourself." ',FTY::FIX ',FTY::PRED ',FTY::BODY))))))) (let ((rune (b* ((rule (car pred-rules)) (subclass (access rewrite-rule rule :subclass)) ((unless (eq subclass 'abbreviation)) nil) (lhs (access rewrite-rule rule :lhs)) ((unless (and (consp (cadr lhs)) (eq fix (car (cadr lhs))) (symbolp (cadr (cadr lhs))))) nil) (rhs (access rewrite-rule rule :rhs)) ((unless (equal rhs ''t)) nil) (hyps (access rewrite-rule rule :hyps)) ((unless (atom hyps)) nil) (equiv (access rewrite-rule rule :equiv)) ((unless (member equiv '(equal iff))) nil)) (access rewrite-rule rule :rune)))) (if rune (mv t rune) (find-pred-of-fix-thm-aux fix pred (cdr pred-rules))))))
find-unsigned-byte-p-pred-of-fix-thm-auxfunction
(defun find-unsigned-byte-p-pred-of-fix-thm-aux (fix pred size pred-rules) (if (atom pred-rules) (let ((body `(unsigned-byte-p ',FTY::SIZE (,FTY::FIX x)))) (mv nil `(local (make-event '(:or (defthm ,(FTY::INTERN-IN-PACKAGE-OF-SYMBOL (FTY::CAT "TMP-DEFTYPES-" (SYMBOL-NAME FTY::PRED) "-OF-" (SYMBOL-NAME FTY::FIX)) 'FTY::FTY) ,FTY::BODY) (value-triple (er hard? 'deftypes "To use ~x0/~x1 as a fixing function/predicate, we must ~ be able to prove the following: ~x2. But this proof ~ failed! Please try to prove this rule yourself." ',FTY::FIX ',FTY::PRED ',FTY::BODY))))))) (let ((rune (b* ((rule (car pred-rules)) (subclass (access rewrite-rule rule :subclass)) ((unless (eq subclass 'abbreviation)) nil) (lhs (access rewrite-rule rule :lhs)) ((unless (and (eq 'unsigned-byte-p (car lhs)) (consp (cadr lhs)) (eq (car (cadr lhs)) 'quote) (eq size (cadr (cadr lhs))) (consp (caddr lhs)) (eq fix (car (caddr lhs))) (symbolp (cadr (caddr lhs))))) nil) (rhs (access rewrite-rule rule :rhs)) ((unless (equal rhs ''t)) nil) (hyps (access rewrite-rule rule :hyps)) ((unless (atom hyps)) nil) (equiv (access rewrite-rule rule :equiv)) ((unless (member equiv '(equal iff))) nil)) (access rewrite-rule rule :rune)))) (if rune (mv t rune) (find-unsigned-byte-p-pred-of-fix-thm-aux fix pred size (cdr pred-rules))))))
flextypes-collect-fix/pred-pairs-auxfunction
(defun flextypes-collect-fix/pred-pairs-aux (types) (if (atom types) nil (append (with-flextype-bindings (x (car types)) (flex*-collect-fix/pred-pairs x)) (flextypes-collect-fix/pred-pairs-aux (cdr types)))))
flextypes-collect-fix/pred-pairsfunction
(defun flextypes-collect-fix/pred-pairs (types) (remove-duplicates-equal (flextypes-collect-fix/pred-pairs-aux types)))
collect-fix/pred-enable-rulesfunction
(defun collect-fix/pred-enable-rules (pairs world) (if (atom pairs) (mv nil nil) (b* (((cons fix pred) (car pairs)) (fix (deref-macro-name fix (macro-aliases world))) (pred (deref-macro-name pred (macro-aliases world))) (fix-exists (not (eq :none (getprop fix 'formals :none 'current-acl2-world world)))) (pred-macro-args (getprop pred 'macro-args :none 'current-acl2-world world)) (pred-macro-body (getprop pred 'macro-body nil 'current-acl2-world world)) (unsigned-byte-p-pred-exists (and (not (eq :none pred-macro-args)) (equal (car pred-macro-body) 'cons) (equal (cadr pred-macro-body) ''unsigned-byte-p) (consp (caddr pred-macro-body)) (equal (car (caddr pred-macro-body)) 'cons) (consp (cadr (caddr pred-macro-body))) (equal (caadr (caddr pred-macro-body)) 'quote) (consp (cdadr (caddr pred-macro-body))) (natp (cadadr (caddr pred-macro-body))) (not (cddadr (caddr pred-macro-body))) (consp (caddr (caddr pred-macro-body))) (equal (car (caddr (caddr pred-macro-body))) 'cons) (consp (cdr (caddr (caddr pred-macro-body)))) (equal (cadr (caddr (caddr pred-macro-body))) (car pred-macro-args)) (consp (cddr (caddr (caddr pred-macro-body)))) (equal (caddr (caddr (caddr pred-macro-body))) ''nil) (not (cdddr (caddr (caddr pred-macro-body)))) (not (cdddr (caddr pred-macro-body))) (not (cdddr pred-macro-body)))) (pred-exists (or unsigned-byte-p-pred-exists (not (eq :none (getprop pred 'formals :none 'current-acl2-world world))))) ((unless (and fix-exists pred-exists)) (and (or fix-exists pred-exists) (cw "WARNING: ~x0 is defined but ~x1 is not" (if fix-exists fix pred) (if fix-exists pred fix))) (collect-fix/pred-enable-rules (cdr pairs) world)) (fix-rules (getprop fix 'lemmas nil 'current-acl2-world world)) (pred-rules (getprop (if unsigned-byte-p-pred-exists 'unsigned-byte-p pred) 'lemmas nil 'current-acl2-world world)) ((mv fix-rule-exists fix-rule) (if unsigned-byte-p-pred-exists (find-fix-when-unsigned-byte-p-pred-thm-aux fix pred (cadadr (caddr pred-macro-body)) fix-rules) (find-fix-when-pred-thm-aux fix pred fix-rules))) ((mv pred-rule-exists pred-rule) (if unsigned-byte-p-pred-exists (find-unsigned-byte-p-pred-of-fix-thm-aux fix pred (cadadr (caddr pred-macro-body)) pred-rules) (find-pred-of-fix-thm-aux fix pred pred-rules))) ((mv enables thms) (collect-fix/pred-enable-rules (cdr pairs) world)) ((mv enables thms) (if fix-rule-exists (mv (cons fix-rule enables) thms) (mv enables (cons fix-rule thms)))) ((mv enables thms) (if pred-rule-exists (mv (cons pred-rule enables) thms) (mv enables (cons pred-rule thms))))) (mv enables thms))))
flextypelist-append-eventsfunction
(defun flextypelist-append-events (kwd types) (if (atom types) nil (append (with-flextype-bindings (x (car types)) (cdr (assoc kwd x.kwd-alist))) (flextypelist-append-events kwd (cdr types)))))
flextype-collect-eventsfunction
(defun flextype-collect-events (kwd kwd-alist types) (append (getarg kwd nil kwd-alist) (flextypelist-append-events kwd types)))
flextypelist-collect-enable-rulesfunction
(defun flextypelist-collect-enable-rules (types) (if (atom types) nil (append (with-flextype-bindings (x (car types)) (cdr (assoc :enable-rules x.kwd-alist))) (flextypelist-collect-enable-rules (cdr types)))))
flextypes-collect-enable-rulesfunction
(defun flextypes-collect-enable-rules (x) (append (cdr (assoc :enable-rules (flextypes->kwd-alist x))) (flextypelist-collect-enable-rules (flextypes->types x))))
collect-uncond-type-prescriptions-from-listfunction
(defun collect-uncond-type-prescriptions-from-list (x ens) (if (atom x) nil (if (and (enabled-numep (access type-prescription (car x) :nume) ens) (not (access type-prescription (car x) :hyps))) (let ((rune (access type-prescription (car x) :rune))) (if (eq (car rune) :type-prescription) (cons rune (collect-uncond-type-prescriptions-from-list (cdr x) ens)) (collect-uncond-type-prescriptions-from-list (cdr x) ens))) (collect-uncond-type-prescriptions-from-list (cdr x) ens))))
collect-uncond-type-prescriptionsfunction
(defun collect-uncond-type-prescriptions (wrld ens fns-seen) (declare (xargs :guard (plist-worldp wrld))) (if (atom wrld) nil (b* (((list* sym key val) (car wrld)) ((unless (eq key 'type-prescriptions)) (collect-uncond-type-prescriptions (cdr wrld) ens fns-seen)) ((when (hons-get sym fns-seen)) (collect-uncond-type-prescriptions (cdr wrld) ens fns-seen))) (append (collect-uncond-type-prescriptions-from-list val ens) (collect-uncond-type-prescriptions (cdr wrld) ens (hons-acons sym t fns-seen))))))
deftypes-eventsfunction
(defun deftypes-events (x state) (b* (((flextypes x) x) (- (flextypelist-check-bad-name x.types)) (fix/pred-pairs (flextypes-collect-fix/pred-pairs x.types)) ((mv enable-rules temp-thms) (collect-fix/pred-enable-rules fix/pred-pairs (w state))) (verbosep (getarg :verbosep nil x.kwd-alist))) `(with-output ,@(AND (NOT FTY::VERBOSEP) `(:OFF (FTY::PROVE FTY::EVENT FTY::OBSERVATION) :SUMMARY-OFF (:OTHER-THAN FORM TIME))) (encapsulate nil (with-output ,@(AND (NOT FTY::VERBOSEP) `(:SUMMARY-OFF (:OTHER-THAN FORM TIME))) (progn (local (table xdoc 'post-defxdoc-event nil)) (local (set-returnspec-mrec-default-hints nil)) (local (set-returnspec-default-hints nil)) (local (set-deffixequiv-default-hints nil)) (local (set-deffixequiv-mutual-default-hints nil)) (local (deftheory deftypes-orig-theory (current-theory :here))) ,@(FTY::FLEXTYPE-COLLECT-EVENTS :PREPWORK FTY::X.KWD-ALIST FTY::X.TYPES) (local (set-inhibit-warnings "disable" "subsume" "non-rec" "double-rewrite")) (set-bogus-defun-hints-ok t) (set-ignore-ok t) (set-irrelevant-formals-ok t) (local (make-event `(deftheory deftypes-type-theory ',(FTY::COLLECT-UNCOND-TYPE-PRESCRIPTIONS (FTY::W FTY::STATE) (ENS FTY::STATE) NIL)))) (local (in-theory (enable identity))) (local (deflabel deftypes-before-temp-thms)) (progn . ,FTY::TEMP-THMS) (local (deftheory deftypes-temp-thms (set-difference-theories (current-theory :here) (current-theory 'deftypes-before-temp-thms)))) (local (in-theory (disable deftypes-orig-theory))) (local (in-theory (enable deftypes-type-theory))) (local (in-theory (enable* deftypes-theory ,@(FTY::FLEXTYPES-COLLECT-ENABLE-RULES FTY::X) . ,FTY::ENABLE-RULES))) (local (set-default-hints '((and stable-under-simplificationp '(:in-theory (enable deftypes-orig-theory)))))) (local (remove-default-post-define-hook :fix)) ,@(FTY::FLEXTYPES-PREDICATE-DEF FTY::X) ,@(FTY::FLEXTYPE-COLLECT-EVENTS :POST-PRED-EVENTS FTY::X.KWD-ALIST FTY::X.TYPES) ,@(FTY::FLEXTYPE-DEF-SUM-KINDS FTY::X.TYPES) ,@(FTY::FLEXTYPES-FIX-DEF FTY::X) ,@(FTY::FLEXTYPE-COLLECT-EVENTS :POST-FIX-EVENTS FTY::X.KWD-ALIST FTY::X.TYPES) ,@(FTY::FLEXTYPES-SUM-ACCESSOR/CONSTRUCTORS FTY::X.TYPES FTY::X.TYPES) (local (in-theory (disable . ,(FTY::FLEXTYPES-FNS FTY::X.TYPES)))) ,@(FTY::FLEXTYPE-COLLECT-EVENTS :POST-ACC-EVENTS FTY::X.KWD-ALIST FTY::X.TYPES) ,@(FTY::FLEXTYPES-COUNT FTY::X) (local (in-theory (enable deftypes-orig-theory))) (local (set-default-hints nil)) ,@(FTY::FLEXTYPE-COLLECT-EVENTS :POST-EVENTS FTY::X.KWD-ALIST FTY::X.TYPES) ,@(FTY::FLEXTYPE-COLLECT-EVENTS :///-EVENTS FTY::X.KWD-ALIST FTY::X.TYPES) (add-flextype ,FTY::X) . ,(FTY::FLEXTYPES-DEFXDOC FTY::X (FTY::W FTY::STATE))))))))
deftypes-fnfunction
(defun deftypes-fn (args state) (b* ((x (parse-flextypes args state))) (deftypes-events x state)))
deftypesmacro
(defmacro deftypes (&rest args) `(make-event (deftypes-fn ',FTY::ARGS state)))
flextypes-kwd-alist-from-specialized-kwd-alistfunction
(defun flextypes-kwd-alist-from-specialized-kwd-alist (kwd-alist) (if (getarg :verbosep nil kwd-alist) '((:verbosep . t)) nil))
defflexsum-fnfunction
(defun defflexsum-fn (whole state) (b* ((our-fixtypes (list (flextype-form->fixtype whole))) (fixtype-al (append our-fixtypes (get-fixtypes-alist (w state)))) (x (parse-flexsum (cdr whole) nil our-fixtypes fixtype-al state)) (x (if (or (flexsum->recp x) (member :count (cdr whole))) x (change-flexsum x :count nil))) ((flexsum x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
defflexsummacro
(defmacro defflexsum (&whole form &rest args) (declare (ignore args)) `(make-event (defflexsum-fn ',FTY::FORM state)))
deflist-fnfunction
(defun deflist-fn (whole state) (b* ((our-fixtypes (list (flextype-form->fixtype whole))) (fixtype-al (append our-fixtypes (get-fixtypes-alist (w state)))) (x (parse-flexlist (cdr whole) nil our-fixtypes fixtype-al state)) (x (if (or (flexlist->recp x) (member :count (cdr whole))) x (change-flexlist x :count nil))) ((flexlist x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
deflistmacro
(defmacro deflist (&whole form &rest args) (declare (ignore args)) `(make-event (deflist-fn ',FTY::FORM state)))
defalist-fnfunction
(defun defalist-fn (whole state) (b* ((our-fixtypes (list (flextype-form->fixtype whole))) (fixtype-al (append our-fixtypes (get-fixtypes-alist (w state)))) (x (parse-flexalist (cdr whole) nil our-fixtypes fixtype-al state)) (x (if (or (flexalist->recp x) (member :count (cdr whole))) x (change-flexalist x :count nil))) ((flexalist x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
defalistmacro
(defmacro defalist (&whole form &rest args) (declare (ignore args)) `(make-event (defalist-fn ',FTY::FORM state)))
defmap-fnfunction
(defun defmap-fn (whole state) (b* ((our-fixtypes (list (flextype-form->fixtype whole))) (fixtype-al (append our-fixtypes (get-fixtypes-alist (w state)))) (x (parse-flexalist (cdr whole) nil our-fixtypes fixtype-al state)) (x (change-flexalist x :strategy :drop-keys)) (x (if (or (flexalist->recp x) (member :count (cdr whole))) x (change-flexalist x :count nil))) ((flexalist x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
defmapmacro
(defmacro defmap (&whole form &rest args) (declare (ignore args)) `(make-event (defmap-fn ',FTY::FORM state)))
deftagsum-fnfunction
(defun deftagsum-fn (whole state) (b* ((fixtype (flextype-form->fixtype whole)) (fixtype-al (cons fixtype (get-fixtypes-alist (w state)))) (x (parse-tagsum (cdr whole) nil (list fixtype) fixtype-al state)) (x (if (or (flexsum->recp x) (member :count (cdr whole))) x (change-flexsum x :count nil))) ((flexsum x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
deftagsummacro
(defmacro deftagsum (&whole form &rest args) (declare (ignore args)) `(make-event (deftagsum-fn ',FTY::FORM state)))
defoption-fnfunction
(defun defoption-fn (whole state) (b* ((fixtype (flextype-form->fixtype whole)) (fixtype-al (cons fixtype (get-fixtypes-alist (w state)))) (x (parse-option (cdr whole) nil (list fixtype) fixtype-al state)) (x (if (or (flexsum->recp x) (member :count (cdr whole))) x (change-flexsum x :count nil))) ((flexsum x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
defoptionmacro
(defmacro defoption (&whole form &rest args) (declare (ignore args)) `(make-event (defoption-fn ',FTY::FORM state)))
deftranssum-fnfunction
(defun deftranssum-fn (whole state) (b* ((fixtype (flextype-form->fixtype whole)) (fixtype-al (cons fixtype (get-fixtypes-alist (w state)))) (x (parse-transsum (cdr whole) nil (list fixtype) fixtype-al state)) (x (if (or (flextranssum->recp x) (member :count (cdr whole))) x (change-flextranssum x :count nil))) ((flextranssum x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
deftranssummacro
(defmacro deftranssum (&whole form &rest args) (declare (ignore args)) `(make-event (deftranssum-fn ',FTY::FORM state)))
defprod-fnfunction
(defun defprod-fn (whole state) (b* ((fixtype (flextype-form->fixtype whole)) (fixtype-al (cons fixtype (get-fixtypes-alist (w state)))) (x (parse-defprod (cdr whole) nil (list fixtype) fixtype-al state)) (x (if (member :count (cdr whole)) x (change-flexsum x :count nil))) ((flexsum x) x) (flextypes (make-flextypes :name x.name :types (list x) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :no-count (not x.count) :recp x.recp))) (deftypes-events flextypes state)))
defprodmacro
(defmacro defprod (&whole form &rest args) (declare (ignore args)) `(make-event (defprod-fn ',FTY::FORM state)))
defset-fnfunction
(defun defset-fn (whole state) (b* ((our-fixtypes (list (flextype-form->fixtype whole))) (fixtype-al (append our-fixtypes (get-fixtypes-alist (w state)))) (x (parse-flexset (cdr whole) nil our-fixtypes fixtype-al state)) (x (if (member :count (cdr whole)) x (change-flexset x :count nil))) ((flexset x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
defsetmacro
(defmacro defset (&whole form &rest args) (declare (ignore args)) `(make-event (defset-fn ',FTY::FORM state)))
defomap-fnfunction
(defun defomap-fn (whole state) (b* ((our-fixtypes (list (flextype-form->fixtype whole))) (fixtype-al (append our-fixtypes (get-fixtypes-alist (w state)))) (x (parse-flexomap (cdr whole) nil our-fixtypes fixtype-al state)) (x (if (member :count (cdr whole)) x (change-flexomap x :count nil))) ((flexomap x) x) (flextypes (make-flextypes :name x.name :types (list x) :no-count (not x.count) :kwd-alist (flextypes-kwd-alist-from-specialized-kwd-alist x.kwd-alist) :recp x.recp))) (deftypes-events flextypes state)))
defomapmacro
(defmacro defomap (&whole form &rest args) (declare (ignore args)) `(make-event (defomap-fn ',FTY::FORM state)))