other
(in-package "FTY")
other
(include-book "fty-sum")
other
(include-book "std/util/cons" :dir :system)
other
(program)
other
(define tagprod-parse-formal-item ((ctx "Context for error messages.") (varname "Name of this formal (i.e., field).") (item "A single user-level item that occurs within the formal.") (guards "Accumulator for guards (for this formal/field only).") (docs "Accumulator for docs (for this formal/field only).")) :returns (mv guards docs) (declare (xargs :guard (legal-variablep varname))) (b* (((when (eq item t)) (mv guards docs)) ((when (eq item nil)) (raise "~x0, field ~x1: don't know what to do with an element with a guard of NIL" ctx varname) (mv guards docs)) ((when (symbolp item)) (mv (cons item guards) docs)) ((when (and (consp item) (not (eq (car item) 'quote)))) (if (and (consp (cdr item)) (not (cddr item)) (eq (cadr item) varname)) (mv (cons (car item) guards) docs) (prog2$ (raise "~x0, field ~x1: can't handle a complicated guard like ~x2" ctx varname item) (mv guards docs)))) ((when (stringp item)) (mv guards (cons item docs)))) (raise "~x0: field ~x1: expected guard specifiers or documentation ~ strings, but found ~x2." ctx varname item) (mv guards docs)))
other
(define tagprod-parse-formal-items (ctx varname items guards docs) :returns (mv guards docs) (declare (xargs :guard (legal-variablep varname))) (b* (((when (not items)) (mv guards docs)) ((when (atom items)) (raise "~x0: field ~x1 should be nil-terminated; found ~x2 as the ~ final cdr." ctx varname items) (mv guards docs)) ((mv guards docs) (tagprod-parse-formal-item ctx varname (car items) guards docs))) (tagprod-parse-formal-items ctx varname (cdr items) guards docs)))
other
(define tagprod-parse-formal ((ctx "Context for error messages.") (formal "User-level field description.") (legal-kwds "What keywords are allowed in the item list.")) :returns (formal "A formal-p.") (declare (xargs :guard t)) (b* (((when (atom formal)) (b* ((varname (parse-formal-name ctx formal))) (make-formal :name varname :guard nil :doc "" :opts nil))) (varname (parse-formal-name ctx (car formal))) (items (cdr formal)) ((mv opts items) (extract-keywords (cons ctx varname) legal-kwds items nil)) ((mv guards docs) (tagprod-parse-formal-items ctx varname items nil nil)) (guard (cond ((atom guards) nil) ((atom (cdr guards)) (if (eq (car guards) t) nil (car guards))) (t (raise "~x0: field ~x1: expected a single guard term, ~ but found ~&2." ctx varname guards)))) (doc (cond ((atom docs) "") ((atom (cdr docs)) (car docs)) (t (progn$ (raise "~x0: field ~x1: expected a single xdoc ~ string, but found ~&2." ctx varname docs) ""))))) (make-formal :name varname :guard guard :doc doc :opts opts)))
other
(define tagprod-parse-formals (ctx formals legal-kwds) (declare (xargs :guard t)) (b* (((when (not formals)) nil) ((when (atom formals)) (raise "~x0: expected fields to be nil-terminated, but found ~x1 as ~ the final cdr." ctx formals))) (cons (tagprod-parse-formal ctx (car formals) legal-kwds) (tagprod-parse-formals ctx (cdr formals) legal-kwds))))
other
(define tagsum-acc-for-tree (pos num expr car cdr) (b* (((when (zp num)) (raise "bad programmer")) ((when (eql num 1)) expr) (half (floor num 2)) ((when (< pos half)) (tagsum-acc-for-tree pos half `(,CAR ,FTY::EXPR) car cdr))) (tagsum-acc-for-tree (- pos half) (- num half) `(,CDR ,FTY::EXPR) car cdr)))
other
(define tagsum-formal-to-flexsum-field ((x "A single field, already parsed into a formal.") (pos "X's position in the list of fields.") (num "Total number of fields.") (xvar "Special x variable.") (layout "How the fields are laid out.")) :returns (flexsum-syntax "User-level(!) flexsum syntax for this field.") (b* (((formal x) x) (accessor (case layout (:alist `(cdr (da-nth ,FTY::POS ,FTY::XVAR))) (:tree (tagsum-acc-for-tree pos num xvar 'prod-car 'prod-cdr)) (:fulltree (tagsum-acc-for-tree pos num xvar 'car 'cdr)) (:list `(da-nth ,FTY::POS ,FTY::XVAR))))) `(,FTY::X.NAME :acc-body ,FTY::ACCESSOR :doc ,FTY::X.DOC :type ,FTY::X.GUARD :default ,(CDR (ASSOC :DEFAULT FTY::X.OPTS)) ,@(LET ((FTY::LOOK (ASSOC :RULE-CLASSES FTY::X.OPTS))) (AND FTY::LOOK `(:RULE-CLASSES ,(CDR FTY::LOOK)))) ,@(LET ((FTY::LOOK (ASSOC :REQFIX FTY::X.OPTS))) (AND FTY::LOOK `(:REQFIX ,(CDR FTY::LOOK)))))))
other
(define tagsum-formals-to-flexsum-fields (x pos num xvar layout) (if (atom x) nil (cons (tagsum-formal-to-flexsum-field (car x) pos num xvar layout) (tagsum-formals-to-flexsum-fields (cdr x) (1+ pos) num xvar layout))))
other
(define tagsum-alist-ctor-elts ((fieldnames) (cons "Either cons or hons.")) (if (atom fieldnames) nil (cons `(,CONS ',(CAR FTY::FIELDNAMES) ,(CAR FTY::FIELDNAMES)) (tagsum-alist-ctor-elts (cdr fieldnames) cons))))
other
(define tagsum-tree-ctor (fieldnames len cons) (b* (((when (zp len)) nil) ((when (eql len 1)) (car fieldnames)) (half (floor len 2))) `(,CONS ,(FTY::TAGSUM-TREE-CTOR (FTY::TAKE FTY::HALF FTY::FIELDNAMES) FTY::HALF CONS) ,(FTY::TAGSUM-TREE-CTOR (NTHCDR FTY::HALF FTY::FIELDNAMES) (- FTY::LEN FTY::HALF) CONS))))
other
(define tagsum-fields-to-ctor-body (fieldnames layout honsp) (b* ((list (if honsp 'hons-list 'list))) (case layout (:alist `(,LIST . ,(FTY::TAGSUM-ALIST-CTOR-ELTS FTY::FIELDNAMES (IF FTY::HONSP 'FTY::HONS 'CONS)))) (:tree (tagsum-tree-ctor fieldnames (len fieldnames) (if honsp 'prod-hons 'prod-cons))) (:fulltree (tagsum-tree-ctor fieldnames (len fieldnames) (if honsp 'hons 'cons))) (:list `(,LIST . ,FTY::FIELDNAMES)))))
other
(define tagsum-fields-to-remake-aux ((fieldnames "as in tagsum-tree-ctor") (len "as in tagsum-tree-ctor") (path "current path into the original structure") (cons-with-hint "cons-with-hint or prod-cons-with-hint") (car "car or prod-car") (cdr "cdr or prod-car")) (b* (((when (zp len)) (raise "bad programmer")) ((when (eql len 1)) (car fieldnames)) (half (floor len 2)) (rest (- len half))) `(,FTY::CONS-WITH-HINT ,(FTY::TAGSUM-FIELDS-TO-REMAKE-AUX (FTY::TAKE FTY::HALF FTY::FIELDNAMES) FTY::HALF `(,CAR ,FTY::PATH) FTY::CONS-WITH-HINT CAR CDR) ,(FTY::TAGSUM-FIELDS-TO-REMAKE-AUX (NTHCDR FTY::HALF FTY::FIELDNAMES) REST `(,CDR ,FTY::PATH) FTY::CONS-WITH-HINT CAR CDR) ,FTY::PATH)))
other
(define tagsum-fields-to-remake-body (fieldnames path layout) (b* (((mv cons-with-hint car cdr) (cond ((eq layout :fulltree) (mv 'cons-with-hint 'car 'cdr)) ((eq layout :tree) (mv 'prod-cons-with-hint 'prod-car 'prod-cdr)) (t (mv (er hard? 'tagsum-fields-to-remake-body "Bad layout ~x0" layout) nil nil))))) (tagsum-fields-to-remake-aux fieldnames (len fieldnames) path cons-with-hint car cdr)))
other
(define tagsum-tree-shape (len expr consp car cdr) (b* (((when (zp len)) `((eq ,FTY::EXPR nil))) ((when (eql len 1)) nil) (half (floor len 2))) (cons `(,CONSP ,FTY::EXPR) (append (tagsum-tree-shape half `(,CAR ,FTY::EXPR) consp car cdr) (tagsum-tree-shape (- len half) `(,CDR ,FTY::EXPR) consp car cdr)))))
other
(logic)
other
(defund alist-with-carsp (alist cars) (declare (xargs :guard (symbol-listp cars))) (if (atom cars) (null alist) (and (consp alist) (let ((entry (first alist))) (and (consp entry) (eq (first cars) (car entry)) (alist-with-carsp (rest alist) (rest cars)))))))
other
(defthm alist-with-carsp-correct (implies (true-listp cars) (equal (alist-with-carsp alist cars) (and (alistp alist) (equal (strip-cars alist) cars)))) :hints (("Goal" :in-theory (enable alist-with-carsp))))
other
(program)
other
(define tagsum-fields-to-shape (fields xvar layout) (case layout (:alist `(mbe :logic (and (alistp ,FTY::XVAR) (equal (strip-cars ,FTY::XVAR) ',(FTY::STRIP-CARS FTY::FIELDS))) :exec (alist-with-carsp ,FTY::XVAR ',(FTY::STRIP-CARS FTY::FIELDS)))) (:list `(and (true-listp ,FTY::XVAR) (eql (len ,FTY::XVAR) ,(FTY::LEN FTY::FIELDS)))) (:tree `(and . ,(FTY::TAGSUM-TREE-SHAPE (FTY::LEN FTY::FIELDS) FTY::XVAR 'FTY::PROD-CONSP 'FTY::PROD-CAR 'FTY::PROD-CDR))) (:fulltree `(and . ,(FTY::TAGSUM-TREE-SHAPE (FTY::LEN FTY::FIELDS) FTY::XVAR 'CONSP 'CAR 'CDR)))))
other
(define tagsum-prod-check-base-case (formals our-fixtypes) (if (atom formals) t (and (not (find-fixtype (formal->guard (car formals)) our-fixtypes)) (tagsum-prod-check-base-case (cdr formals) our-fixtypes))))
other
(defconst *tagprod-formal-keywords* '(:rule-classes :default :reqfix))
other
(defconst *tagprod-keywords* '(:layout :hons :inline :base-name :require :short :long :extra-binder-names :count-incr :no-ctor-macros :verbosep))
fty-layout-supports-remake-pfunction
(defun fty-layout-supports-remake-p (fields honsp layout) (and (member layout '(:tree :fulltree)) (not honsp) (consp fields)))
other
(define tagsum-prod-to-flexprod
(x xvar
sum-kwds
lastp
have-basep
our-fixtypes)
(b* (((cons kind args) x) ((mv kwd-alist fields) (extract-keywords kind
*tagprod-keywords*
args
nil))
((when (not (eql (len fields) 1))) (raise "Should have exactly one set of field specifiers: ~x0~%"
fields)
(mv nil nil))
(layout (getarg :layout (getarg :layout :list sum-kwds)
kwd-alist))
(inlinep (assoc :inline kwd-alist))
(requirep (assoc :require kwd-alist))
(shortp (assoc :short kwd-alist))
(longp (assoc :long kwd-alist))
(count-incrp (assoc :count-incr kwd-alist))
(hons (getarg :hons nil kwd-alist))
(fields (car fields))
(field-formals (tagprod-parse-formals kind
fields
*tagprod-formal-keywords*))
(basep (and (if have-basep
(eq have-basep kind)
(tagsum-prod-check-base-case field-formals
our-fixtypes))
kind))
(flexsum-fields (tagsum-formals-to-flexsum-fields field-formals
0
(len field-formals)
`(cdr ,FTY::XVAR)
layout))
(base-name (getarg :base-name nil kwd-alist))
(fieldnames (strip-cars flexsum-fields))
(ctor-body1 (tagsum-fields-to-ctor-body fieldnames
layout
hons))
(remake-body (and (fty-layout-supports-remake-p fieldnames
hons
layout)
`(cons-with-hint ,FTY::KIND
,(FTY::TAGSUM-FIELDS-TO-REMAKE-BODY FTY::FIELDNAMES `(CDR ,FTY::XVAR)
FTY::LAYOUT)
,FTY::XVAR)))
(shape1 (tagsum-fields-to-shape flexsum-fields
`(cdr ,FTY::XVAR)
layout))
(extra-binder-names (getarg :extra-binder-names nil kwd-alist))
(no-ctor-macros (getarg :no-ctor-macros nil kwd-alist)))
(mv `(,FTY::KIND :cond ,(IF FTY::LASTP
T
(IF FTY::BASEP
`(OR (ATOM ,FTY::XVAR) (EQ (CAR ,FTY::XVAR) ,FTY::KIND))
`(EQ (CAR ,FTY::XVAR) ,FTY::KIND)))
:shape ,(IF FTY::LASTP
`(AND (EQ (CAR ,FTY::XVAR) ,FTY::KIND) ,FTY::SHAPE1)
FTY::SHAPE1)
:fields ,FTY::FLEXSUM-FIELDS
,@(AND FTY::INLINEP `(:INLINE ,(CDR FTY::INLINEP)))
,@(AND FTY::REQUIREP `(:REQUIRE ,(CDR FTY::REQUIREP)))
,@(AND FTY::BASE-NAME `(:TYPE-NAME ,FTY::BASE-NAME))
,@(AND FTY::SHORTP `(:SHORT ,(CDR FTY::SHORTP)))
,@(AND FTY::LONGP `(:LONG ,(CDR FTY::LONGP)))
,@(AND FTY::COUNT-INCRP `(:COUNT-INCR ,(CDR FTY::COUNT-INCRP)))
:ctor-body (,(IF FTY::HONS
'FTY::HONS
'CONS) ,FTY::KIND
,FTY::CTOR-BODY1)
,@(AND FTY::REMAKE-BODY `(:REMAKE-BODY ,FTY::REMAKE-BODY))
,@(AND FTY::EXTRA-BINDER-NAMES `(:EXTRA-BINDER-NAMES ,FTY::EXTRA-BINDER-NAMES))
,@(AND FTY::NO-CTOR-MACROS `(:NO-CTOR-MACROS ,FTY::NO-CTOR-MACROS)))
basep)))
other
(define tagsum-prods-to-flexprods
(prods xvar
sum-kwds
have-base-or-override
our-fixtypes
tagsum-name)
(b* (((when (and (atom prods) (not have-base-or-override))) (raise "We couldn't find a base case for tagsum ~x0, so we don't know ~
what its fixing function should return when the input is an ~
atom. To override this, add keyword arg :base-case-override ~
[product], where [product] is one of your product keywords, ~
and provide a measure that will allow the fixing function to ~
terminate."
tagsum-name)) ((when (atom prods)) nil)
((mv first basep) (tagsum-prod-to-flexprod (car prods)
xvar
sum-kwds
(atom (cdr prods))
have-base-or-override
our-fixtypes)))
(cons first
(tagsum-prods-to-flexprods (cdr prods)
xvar
sum-kwds
(or have-base-or-override basep)
our-fixtypes
tagsum-name))))
other
(defconst *tagsum-keywords* '(:pred :fix :equiv :kind :count :measure :measure-debug :xvar :no-count :parents :short :long :inline :layout :case :base-case-override :short-names :prepwork :post-pred-events :post-fix-events :post-acc-events :post-events :enable-rules :verbosep :disable-type-prescription))
other
(define tagsum-tag-events-post-fix (pred fix xvar name kind) (b* ((tag-when-foo-p-forward (intern-in-package-of-symbol (cat "TAG-WHEN-" (symbol-name pred) "-FORWARD") name)) (tag-of-foo-fix (intern-in-package-of-symbol (cat "TAG-OF-" (symbol-name fix)) name))) `((defthmd ,FTY::TAG-WHEN-FOO-P-FORWARD (implies (,FTY::PRED ,FTY::XVAR) (equal (tag ,FTY::XVAR) (,FTY::KIND ,FTY::XVAR))) :rule-classes ((:forward-chaining :trigger-terms ((,FTY::PRED ,FTY::XVAR)))) :hints (("Goal" :expand ((tag ,FTY::XVAR) (,FTY::PRED ,FTY::XVAR) (,FTY::KIND ,FTY::XVAR))))) (defthm ,FTY::TAG-OF-FOO-FIX (equal (tag (,FTY::FIX ,FTY::XVAR)) (,FTY::KIND ,FTY::XVAR)) :hints (("Goal" :in-theory (disable ,FTY::TAG-WHEN-FOO-P-FORWARD tag ,FTY::PRED ,FTY::KIND) :use ((:instance ,FTY::TAG-WHEN-FOO-P-FORWARD (,FTY::XVAR (,FTY::FIX ,FTY::XVAR))))))) (add-to-ruleset tag-reasoning '(,FTY::TAG-WHEN-FOO-P-FORWARD ,FTY::TAG-OF-FOO-FIX)))))
other
(define parse-tagsum
(x xvar
these-fixtypes
fixtypes
state)
(b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed tagsum: ~x0: name must be a symbol"
x))
((mv pre-/// post-///) (split-/// name args))
((mv kwd-alist orig-prods) (extract-keywords name
*tagsum-keywords*
pre-///
nil))
(kwd-alist (append kwd-alist
(table-alist 'deftagsum-defaults
(w state))))
(pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
name)
kwd-alist))
(fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
name)
kwd-alist))
(equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
name)
kwd-alist))
(kind (getarg! :kind (intern-in-package-of-symbol (cat (symbol-name name) "-KIND")
name)
kwd-alist))
(case (getarg! :case (intern-in-package-of-symbol (cat (symbol-name name) "-CASE")
name)
kwd-alist))
(disable-type (getarg :disable-type-prescription nil kwd-alist))
(inline (get-deftypes-inline-opt *inline-defaults*
kwd-alist))
(count (flextype-get-count-fn name kwd-alist))
(xvar (or (getarg :xvar xvar kwd-alist)
(car (find-symbols-named-x (getarg :measure nil kwd-alist)))
(intern-in-package-of-symbol "X" name)))
(layout (getarg :layout :alist kwd-alist))
((unless (member layout '(:tree :fulltree :list :alist))) (raise "In tagsum ~x0: Bad layout type ~x1~%"
name
layout))
(base-override (getarg :base-case-override nil kwd-alist))
(flexprods-in (tagsum-prods-to-flexprods orig-prods
xvar
kwd-alist
base-override
these-fixtypes
name))
((unless (or (not base-override)
(member base-override
(strip-cars flexprods-in)))) (raise "In tagsum ~x0: :base-case-override value must be one of the ~
product names (~x1) but found ~x2."
name
(strip-cars flexprods-in)
base-override))
(prods (parse-flexprods flexprods-in
name
kind
kwd-alist
xvar
nil
these-fixtypes
fixtypes))
(- (flexprods-check-xvar xvar prods))
((when (atom prods)) (raise "In tagsum ~s0: Must have at least one product."
name))
(recp (some-flexprod-recursivep prods))
(measure (getarg! :measure `(acl2-count ,FTY::XVAR)
kwd-alist))
(post-fix-events (append (tagsum-tag-events-post-fix pred
fix
xvar
name
kind)
(cdr (assoc :post-fix-events kwd-alist)))))
(make-flexsum :name name
:pred pred
:fix fix
:equiv equiv
:kind kind
:case case
:kind-body `(car ,FTY::XVAR)
:shape `(consp ,FTY::XVAR)
:count count
:prods prods
:xvar xvar
:inline inline
:measure measure
:kwd-alist (cons (cons :post-fix-events post-fix-events)
(if post-///
(cons (cons :///-events post-///) kwd-alist)
kwd-alist))
:orig-prods orig-prods
:recp recp
:typemacro 'deftagsum
:disable-type-prescription disable-type)))
other
(defconst *defprod-keywords* '(:pred :fix :equiv :count :measure :measure-debug :xvar :no-count :parents :short :long :inline :require :layout :tag :hons :prepwork :post-pred-events :post-fix-events :post-acc-events :post-events :enable-rules :extra-binder-names :no-ctor-macros :verbosep :disable-type-prescription))
other
(define defprod-fields-to-flexsum-prod (fields xvar name kwd-alist) (b* ((layout (getarg :layout :alist kwd-alist)) ((unless (member layout '(:tree :fulltree :list :alist))) (raise "In ~x0: bad layout type ~x1~%" name layout)) (tag (getarg :tag nil kwd-alist)) (hons (getarg :hons nil kwd-alist)) (field-formals (tagprod-parse-formals name fields *tagprod-formal-keywords*)) (xbody (if tag `(cdr ,FTY::XVAR) xvar)) (flexsum-fields (tagsum-formals-to-flexsum-fields field-formals 0 (len field-formals) xbody layout)) (fieldnames (strip-cars flexsum-fields)) (ctor-body1 (tagsum-fields-to-ctor-body fieldnames layout hons)) (ctor-body (if tag `(,(IF FTY::HONS 'FTY::HONS 'CONS) ,FTY::TAG ,FTY::CTOR-BODY1) ctor-body1)) (remake-body1 (and (fty-layout-supports-remake-p fieldnames hons layout) (tagsum-fields-to-remake-body fieldnames xbody layout))) (remake-body (and remake-body1 (if tag `(cons-with-hint ,FTY::TAG ,FTY::REMAKE-BODY1 ,FTY::XVAR) remake-body1))) (shape (tagsum-fields-to-shape flexsum-fields xbody layout)) (requirep (assoc :require kwd-alist)) (kind (or tag (intern$ (symbol-name name) "KEYWORD"))) (extra-binder-names (getarg :extra-binder-names nil kwd-alist)) (no-ctor-macros (getarg :no-ctor-macros nil kwd-alist))) `(,FTY::KIND :shape ,(IF FTY::TAG (FTY::NICE-AND `(EQ (CAR ,FTY::XVAR) ,FTY::TAG) FTY::SHAPE) FTY::SHAPE) :fields ,FTY::FLEXSUM-FIELDS :type-name ,FTY::NAME :ctor-body ,FTY::CTOR-BODY ,@(AND FTY::REMAKE-BODY `(:REMAKE-BODY ,FTY::REMAKE-BODY)) ,@(AND FTY::EXTRA-BINDER-NAMES `(:EXTRA-BINDER-NAMES ,FTY::EXTRA-BINDER-NAMES)) ,@(AND FTY::NO-CTOR-MACROS `(:NO-CTOR-MACROS ,FTY::NO-CTOR-MACROS)) ,@(AND FTY::REQUIREP `(:REQUIRE ,(CDR FTY::REQUIREP))))))
other
(define defprod-tag-events-post-pred (pred xvar tag name) (b* ((tag-when-foo-p (intern-in-package-of-symbol (cat "TAG-WHEN-" (symbol-name pred)) name)) (foo-p-when-wrong-tag (intern-in-package-of-symbol (cat (symbol-name pred) "-WHEN-WRONG-TAG") name))) `((defthmd ,FTY::TAG-WHEN-FOO-P (implies (,FTY::PRED ,FTY::XVAR) (equal (tag ,FTY::XVAR) ,FTY::TAG)) :rule-classes ((:rewrite :backchain-limit-lst 0) (:forward-chaining)) :hints (("Goal" :in-theory (enable tag ,FTY::PRED)))) (defthmd ,FTY::FOO-P-WHEN-WRONG-TAG (implies (not (equal (tag ,FTY::XVAR) ,FTY::TAG)) (equal (,FTY::PRED ,FTY::XVAR) nil)) :rule-classes ((:rewrite :backchain-limit-lst 1)) :hints (("Goal" :in-theory (enable tag ,FTY::PRED)))) (add-to-ruleset tag-reasoning '(,FTY::TAG-WHEN-FOO-P ,FTY::FOO-P-WHEN-WRONG-TAG)))))
other
(define defprod-tag-events-post-fix (pred fix xvar name tag) (declare (ignorable pred)) (let ((tag-of-foo-fix (intern-in-package-of-symbol (cat "TAG-OF-" (symbol-name fix)) name)) (tag-when-foo-p (intern-in-package-of-symbol (cat "TAG-WHEN-" (symbol-name pred)) name))) `((defthm ,FTY::TAG-OF-FOO-FIX (equal (tag (,FTY::FIX ,FTY::XVAR)) ,FTY::TAG) :hints (("Goal" :in-theory (enable ,FTY::TAG-WHEN-FOO-P) :cases ((,FTY::PRED (,FTY::FIX ,FTY::XVAR)))))) (add-to-ruleset tag-reasoning '(,FTY::TAG-OF-FOO-FIX)))))
other
(define defprod-tag-events-post-ctor (tag name formals) (let ((tag-of-foo (intern-in-package-of-symbol (cat "TAG-OF-" (symbol-name name)) name))) `((defthm ,FTY::TAG-OF-FOO (equal (tag (,FTY::NAME . ,FTY::FORMALS)) ,FTY::TAG) :hints (("goal" :in-theory (enable ,FTY::NAME tag)))) (add-to-ruleset tag-reasoning '(,FTY::TAG-OF-FOO)))))
other
(define parse-defprod
(x xvar
our-fixtypes
fixtypes
state)
(b* (((cons name args) x) ((unless (symbolp name)) (raise "Malformed defprod: ~x0: name must be a symbol"
x))
((mv pre-/// post-///) (split-/// name args))
((mv kwd-alist fields) (extract-keywords name
*defprod-keywords*
pre-///
nil))
(kwd-alist (append kwd-alist
(table-alist 'defprod-defaults
(w state))))
((when (atom fields)) (raise "In defprod ~x0: List of fields is missing~%"
name))
((when (consp (cdr fields))) (raise "In defprod ~x0: More than one list of fields present~%"
name))
(fields (car fields))
(pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
name)
kwd-alist))
(fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
name)
kwd-alist))
(equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
name)
kwd-alist))
(disable-type (getarg :disable-type-prescription nil kwd-alist))
(inline (get-deftypes-inline-opt *inline-defaults*
kwd-alist))
(count (flextype-get-count-fn name kwd-alist))
(xvar (or (getarg :xvar xvar kwd-alist)
(car (find-symbols-named-x (getarg :measure nil kwd-alist)))
(intern-in-package-of-symbol "X" name)))
(tag (getarg :tag nil kwd-alist))
((unless (or (not tag) (keywordp tag))) (er hard?
'parse-defprod
":Tag, if provided, must be a keyword symbol"))
(orig-prod (defprod-fields-to-flexsum-prod fields
xvar
name
kwd-alist))
(orig-prods (list orig-prod))
(prods (parse-flexprods orig-prods
name
nil
kwd-alist
xvar
nil
our-fixtypes
fixtypes))
(- (flexprods-check-xvar xvar prods))
(measure (getarg! :measure `(acl2-count ,FTY::XVAR)
kwd-alist))
(field-names (flexprod-fields->names (flexprod->fields (car prods))))
(post-events (if tag
(append (defprod-tag-events-post-ctor tag
name
field-names)
(cdr (assoc :post-events kwd-alist)))
(cdr (assoc :post-events kwd-alist))))
(post-pred-events (if tag
(append (defprod-tag-events-post-pred pred
xvar
tag
name)
(cdr (assoc :post-pred-events kwd-alist)))
(cdr (assoc :post-pred-events kwd-alist))))
(post-fix-events (if tag
(append (defprod-tag-events-post-fix pred
fix
xvar
name
tag)
(cdr (assoc :post-fix-events kwd-alist)))
(cdr (assoc :post-fix-events kwd-alist)))))
(make-flexsum :name name
:pred pred
:fix fix
:equiv equiv
:kind nil
:shape (if tag
`(consp ,FTY::XVAR)
t)
:count count
:prods prods
:xvar xvar
:measure measure
:kwd-alist (list* (cons :///-events post-///)
(cons :post-events post-events)
(cons :post-pred-events post-pred-events)
(cons :post-fix-events post-fix-events)
kwd-alist)
:orig-prods orig-prods
:inline inline
:recp (some-flexprod-recursivep prods)
:typemacro 'defprod
:disable-type-prescription disable-type)))
other
(defconst *option-keywords* '(:pred :fix :equiv :count :measure :measure-debug :xvar :no-count :parents :short :long :inline :case :base-case-override :prepwork :post-pred-events :post-fix-events :post-acc-events :post-events :enable-rules :verbosep))
other
(define defoption-post-pred-events (x) (b* (((flexsum x)) ((fixtype base) (cdr (assoc :basetype x.kwd-alist))) (maybe-foo-p-when-foo-p (intern-in-package-of-symbol (cat (symbol-name x.pred) "-WHEN-" (symbol-name base.pred)) x.pred)) (foo-p-when-maybe-foo-p (intern-in-package-of-symbol (cat (symbol-name base.pred) "-WHEN-" (symbol-name x.pred)) x.pred))) `((defthm ,FTY::MAYBE-FOO-P-WHEN-FOO-P (implies (,FTY::BASE.PRED ,FTY::X.XVAR) (,FTY::X.PRED ,FTY::X.XVAR)) :hints (("Goal" :in-theory (enable ,FTY::X.PRED)))) (defthm ,FTY::FOO-P-WHEN-MAYBE-FOO-P (implies (and (,FTY::X.PRED ,FTY::X.XVAR) (double-rewrite ,FTY::X.XVAR)) (,FTY::BASE.PRED ,FTY::X.XVAR)) :hints (("Goal" :in-theory (enable ,FTY::X.PRED)))))))
other
(define defoption-post-fix-events (x) (b* (((flexsum x)) ((fixtype base) (cdr (assoc :basetype x.kwd-alist))) (maybe-foo-fix-under-iff (intern-in-package-of-symbol (cat (symbol-name x.fix) "-UNDER-IFF") x.pred)) (defoption-lemma-foo-fix-nonnil (intern-in-package-of-symbol (cat "DEFOPTION-LEMMA-" (symbol-name base.fix) "-NONNIL") base.fix))) `((local (defthm ,FTY::DEFOPTION-LEMMA-FOO-FIX-NONNIL (,FTY::BASE.FIX x) :hints (("goal" :use ((:theorem (,FTY::BASE.PRED (,FTY::BASE.FIX x))) (:theorem (not (,FTY::BASE.PRED nil)))) :in-theory '((,FTY::BASE.PRED))) (and stable-under-simplificationp '(:in-theory (enable)))) :rule-classes :type-prescription)) (defthm ,FTY::MAYBE-FOO-FIX-UNDER-IFF (iff (,FTY::X.FIX ,FTY::X.XVAR) ,FTY::X.XVAR) :hints (("Goal" :in-theory (enable ,FTY::X.FIX)))) (defrefinement ,FTY::X.EQUIV ,FTY::BASE.EQUIV :hints (("Goal" :in-theory (enable ,FTY::X.FIX)) (and stable-under-simplificationp '(:in-theory (enable ,FTY::BASE.EQUIV))))))))
other
(define parse-option
(x xvar
these-fixtypes
fixtypes
state)
(b* (((list* name basetype args) x) ((unless (symbolp name)) (raise "Malformed option: ~x0: name must be a symbol"
x))
((unless (symbolp basetype)) (raise "Malformed option: ~x0: basetype must be a symbol, found ~x1"
name
basetype))
(base-fixtype (or (find-fixtype basetype these-fixtypes)
(find-fixtype basetype fixtypes)))
((mv pre-/// post-///) (split-/// name args))
((mv kwd-alist orig-prods) (extract-keywords name
*option-keywords*
pre-///
nil))
(kwd-alist (append kwd-alist
(table-alist 'defoption-defaults
(w state))))
(pred (getarg! :pred (intern-in-package-of-symbol (cat (symbol-name name) "-P")
name)
kwd-alist))
(fix (getarg! :fix (intern-in-package-of-symbol (cat (symbol-name name) "-FIX")
name)
kwd-alist))
(equiv (getarg! :equiv (intern-in-package-of-symbol (cat (symbol-name name) "-EQUIV")
name)
kwd-alist))
(case (getarg! :case (intern-in-package-of-symbol (cat (symbol-name name) "-CASE")
name)
kwd-alist))
(inline (get-deftypes-inline-opt *inline-defaults*
kwd-alist))
(count (flextype-get-count-fn name kwd-alist))
(xvar (or (getarg :xvar xvar kwd-alist)
(car (find-symbols-named-x (getarg :measure nil kwd-alist)))
(intern-in-package-of-symbol "X" name)))
(name-link (see name))
(flexprods-in `((:none :cond (not ,FTY::XVAR)
:ctor-body nil
:short ,(FTY::CAT "Represents that no " FTY::NAME-LINK
" is available, i.e., Nothing or None.")) (:some :cond t
:fields ((val :type ,FTY::BASETYPE :acc-body ,FTY::XVAR))
:ctor-body val
:short ,(FTY::CAT "An available " FTY::NAME-LINK
", i.e., <i>Just val</i> or <i>Some val</i>."))))
(prods (parse-flexprods flexprods-in
name
nil
kwd-alist
xvar
nil
these-fixtypes
fixtypes))
(- (flexprods-check-xvar xvar prods))
((when (atom prods)) (raise "Malformed SUM ~x0: Must have at least one product"
name))
(measure (or (getarg :measure nil kwd-alist)
`(acl2-count ,FTY::XVAR)))
(kwd-alist (cons (cons :basetype base-fixtype)
(if post-///
(cons (cons :///-events post-///) kwd-alist)
kwd-alist)))
(flexsum (make-flexsum :name name
:pred pred
:fix fix
:equiv equiv
:case case
:count count
:prods prods
:shape t
:xvar xvar
:inline inline
:measure measure
:kwd-alist kwd-alist
:orig-prods orig-prods
:recp (some-flexprod-recursivep prods)
:typemacro 'defoption))
(post-pred-events (append (defoption-post-pred-events flexsum)
(cdr (assoc :post-pred-events kwd-alist))))
(post-fix-events (append (defoption-post-fix-events flexsum)
(cdr (assoc :post-fix-events kwd-alist))))
(kwd-alist `((:post-pred-events . ,FTY::POST-PRED-EVENTS) (:post-fix-events . ,FTY::POST-FIX-EVENTS) . ,FTY::KWD-ALIST)))
(change-flexsum flexsum :kwd-alist kwd-alist)))