other
(in-package "CGEN")
other
(include-book "std/util/bstar" :dir :system)
other
(include-book "acl2s/utilities" :dir :system)
type-sig%-pfunction
(defun type-sig%-p (v) (declare (xargs :guard t)) (case-match v ((input-arg-typs . output-arg-type) (and (symbol-listp input-arg-typs) (or (symbolp output-arg-type) (and (consp output-arg-type) (eq 'mv (car output-arg-type)) (symbol-listp output-arg-type)))))))
def-metadata%-pfunction
(defun def-metadata%-p (v) (declare (xargs :guard t)) (case-match v ((an cn tsig m inline? trace) (and (symbolp an) (symbolp cn) (type-sig%-p tsig) (member-eq m '(:program :logic)) (booleanp inline?) (booleanp trace)))))
other
(table def-metadata-table nil nil :guard (and (symbolp key) (def-metadata%-p val)))
defmacro
(defmacro def (&rest def) `(make-event (defs-fn (list ',CGEN::DEF) 'nil 'nil 'def (w state) state)))
defsmacro
(defmacro defs (&rest def-lst) `(make-event (defs-fn ',CGEN::DEF-LST 'nil 'nil 'defs (w state) state)))
triplelis$function
(defun triplelis$ (xs ys zs) "similar to pairlis$, except now we have 3 lists to zip == [(cons x (cons y z)) | x in xs, y in ys, z in zs]" (declare (xargs :guard (and (true-listp xs) (true-listp ys) (true-listp zs) (= (len xs) (len ys)) (= (len xs) (len zs))))) (if (endp xs) 'nil (cons (cons (car xs) (cons (car ys) (car zs))) (triplelis$ (cdr xs) (cdr ys) (cdr zs)))))
str/sym-listpfunction
(defun str/sym-listp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (or (stringp (car x)) (symbolp (car x))) (str/sym-listp (cdr x)))))
concatenate-namesfunction
(defun concatenate-names (x) (declare (xargs :guard (str/sym-listp x))) (if (consp x) (concatenate 'string (if (symbolp (car x)) (symbol-name (car x)) (car x)) (concatenate-names (cdr x))) ""))
other
(defthm concatenate-names-is-stringp (stringp (concatenate-names x)))
other
(local (in-theory (disable concatenate-names)))
mksymmacro
(defmacro mksym (&rest args) "given a sequence of symbols or strings as args, it returns the concatenated symbol" `(fix-intern-in-pkg-of-sym (concatenate-names (list ,@CGEN::ARGS)) mksym-ps))
modify-symbolfunction
(defun modify-symbol (prefix sym postfix) (declare (xargs :guard (and (symbolp sym) (stringp postfix) (stringp prefix)))) (let* ((name (symbol-name sym)) (name (string-append prefix name)) (name (string-append name postfix))) (if (member-eq sym *common-lisp-symbols-from-main-lisp-package*) (fix-intern-in-pkg-of-sym name 'acl2-pkg-witness) (fix-intern-in-pkg-of-sym name sym))))
modify-symbol-lstfunction
(defun modify-symbol-lst (prefix syms postfix) (declare (xargs :guard (and (symbol-listp syms) (stringp prefix) (stringp postfix)))) (if (endp syms) nil (cons (modify-symbol prefix (car syms) postfix) (modify-symbol-lst prefix (cdr syms) postfix))))
other
(defthm modified-symbol-satisfies-symbolp (implies (and (symbolp sym) (stringp pre) (stringp post)) (symbolp (modify-symbol pre sym post))) :rule-classes :type-prescription)
other
(in-theory (disable modify-symbol))
other
(defthm modified-symbol-lst-satisfies-symbol-listp (implies (and (symbol-listp syms) (stringp pre) (stringp post)) (symbol-listp (modify-symbol-lst pre syms post))) :rule-classes (:rewrite :type-prescription))
other
(defthm modified-symbol-lst-len (= (len (modify-symbol-lst pre syms post)) (len syms)))
other
(in-theory (disable modify-symbol-lst))
fn-pfunction
(defun fn-p (x) (declare (xargs :guard t)) (and (consp x) (symbolp (first x)) (consp (cdr x)) (symbol-listp (second x)) (consp (cddr x))))
fn-list-pfunction
(defun fn-list-p (x) (declare (xargs :guard t)) (if (consp x) (and (fn-p (car x)) (fn-list-p (cdr x))) (equal x 'nil)))
other
(defthm strip-cars-doesnt-change-length (implies (true-listp xs) (= (len (strip-cars xs)) (len xs))))
other
(defthm strip-cdrs-doesnt-change-length (implies (true-listp xs) (= (len (strip-cdrs xs)) (len xs))))
other
(defthm fn-list-p-implies-alistp (implies (fn-list-p fns) (alistp fns)) :rule-classes :forward-chaining)
other
(defthm fn-list-p-strip-cars-is-symbol-listp (implies (fn-list-p fns) (symbol-listp (strip-cars fns))) :rule-classes (:rewrite :forward-chaining))
other
(defthm true-listp-of-make-list-ac (equal (true-listp (make-list-ac n val ac)) (true-listp ac)) :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp ac) (true-listp (make-list-ac n val ac))))))
other
(defthm len-of-make-list-ac (implies (natp n) (equal (len (make-list-ac n val ac)) (+ n (len ac)))))
other
(defthm pairlis$-eqlable-symbol-lists (implies (and (symbol-listp xs) (symbol-listp ys)) (eqlable-alistp (pairlis$ xs ys))))
mk-f*-eventsfunction
(defun mk-f*-events (fns nm) "for given functions return defabbrev events and a substitution mapping original names to inlined actual defabbrev names" (declare (xargs :guard (and (fn-list-p fns) (symbolp nm)))) (b* ((mksym-ps nm) (prefix (mksym "_" nm)) (old-names (strip-cars fns)) (new-names (modify-symbol-lst (symbol-name prefix) old-names "")) (def-events (triplelis$ (make-list (len fns) :initial-element 'defabbrev) new-names (strip-cdrs fns))) (p (pairlis$ old-names new-names)) (def-events~ (sublis p def-events))) (mv def-events~ p)))
other
(def-const *stobjs* '(state r$ types-ht$))
mk-declarefunction
(defun mk-declare (k) (declare (xargs :guard (and (keyword-value-listp k) (assoc-keyword :sig k) (equal :sig (car (assoc-keyword :sig k))) (true-listp (cadr (assoc-keyword :sig k))) (= 3 (len (cadr (assoc-keyword :sig k)))) (true-listp (caadr (assoc-keyword :sig k)))))) "?: make a declare form from the fields of decl keyword value list " (b* (((list & mode) (or (assoc-keyword :mode k) '(:mode :logic))) (`(:sig (,CGEN::IN & &)) (assoc-keyword :sig k)) (stobjs (intersection-eq *stobjs* in))) `(declare (xargs :mode ,CGEN::MODE :stobjs ,CGEN::STOBJS))))
other
(set-verify-guards-eagerness 0)
trans-bodyfunction
(defun trans-body (b nm) "translate body, by making defun events for each f* binding" (declare (xargs :guard (and (symbolp nm)))) (case-match b (('f* fns body) (b* (((mv evts p) (mk-f*-events fns nm)) (body~ (sublis p body))) (mv evts body~))) (& (mv nil b))))
trans-arglistfunction
(defun trans-arglist (a) (declare (xargs :guard (and (true-listp a)))) "not implemented at the moment i.e noop" (mv a nil))
other
(deflabel f*)
def-fn1function
(defun def-fn1 (name arglist decl-kv-list decls body ctx wrld state) (declare (ignorable wrld state)) (declare (xargs :stobjs (state) :guard (and (symbolp name) (symbolp ctx) (true-listp arglist) (keyword-value-listp decl-kv-list) (true-listp decls) (plist-worldp wrld)))) (let ((k decl-kv-list) (a arglist) (b body)) (b* (((unless (keyword-value-listp k)) (er hard ctx "~|~x0 is not a keyword value list.~%" k)) ((unless (assoc-keyword :sig k)) (er hard ctx "~|:sig not found in ~x0.~%" k)) (decl (mk-declare k)) ((list & doc) (or (assoc-keyword :doc k) '(:doc "n/a"))) ((mv a1 b*-bindings) (trans-arglist a)) ((mv aux-events b~) (trans-body b name)) (b~1 (if b*-bindings `(b* ,CGEN::B*-BINDINGS b~) b~))) (list aux-events `(,CGEN::NAME ,CGEN::A1 ,CGEN::DOC ,@(CONS CGEN::DECL CGEN::DECLS) ,CGEN::B~1)))))
def-fnfunction
(defun def-fn (def ctx wrld state) (declare (ignorable wrld state)) (declare (xargs :stobjs (state) :guard (and (symbolp ctx) (plist-worldp wrld)))) (case-match def ((nm a ('decl . k) ('declare . ds) b) (def-fn1 nm a k (list (cons 'declare ds)) b ctx wrld state)) ((nm a ('decl . k) b) (def-fn1 nm a k 'nil b ctx wrld state)) (& (er hard ctx "~|Ill-formed def form. ~ General form: ~ (def name arglist decl [declare] body)~%"))))
defs-fnfunction
(defun defs-fn (def-lst aux-events. defuns-tuples. ctx wrld state) "my own defun for storing type metadata for later type-checking. 1. possible nested (local) defuns 2. list comprehensions 3. destructuring arg list" (declare (xargs :stobjs (state) :guard (and (true-listp def-lst) (true-listp aux-events.) (symbolp ctx) (plist-worldp wrld)))) (if (endp def-lst) `(progn ,@CGEN::AUX-EVENTS. ,(IF (NULL (CDR CGEN::DEFUNS-TUPLES.)) `(DEFUN . ,(CAR CGEN::DEFUNS-TUPLES.)) `(CGEN::DEFUNS . ,CGEN::DEFUNS-TUPLES.))) (b* (((list ae def-tuple) (def-fn (first def-lst) ctx wrld state))) (defs-fn (rest def-lst) (append ae aux-events.) (append defuns-tuples. (list def-tuple)) ctx wrld state))))
other
(def-const *primitives* '(+f *f |1+f| = |1-f| -f /= <= < > >= plus-mod-m31 double-mod-m31 times-expt-2-16-mod-m31 times-mod-m31 mod mod^ floor floor^ expt expt^ min min^ max max^ logand logand^ logior logior^ lognot lognot^ logxor logxor^ ash ash^ mask^ mv mv^ my-fixnum the-fixnum er er0 prog2$ cw ev-fncall-w fn-count-evg lexorder if not implies and or iff acl2-numberp rationalp integerp consp characterp symbolp stringp booleanp termp keywordp true-listp symbol-listp cons null atom endp list list* push-lemma car cdr caar cdar cadr cddr cadar first second third fourth fifth sixth seventh eighth ninth tenth rest last butlast nth nthcdr update-nth append length reverse revappend string-append acons assoc assoc-eq assoc-equal assoc-keyword strip-cars strip-cdrs numerator denominator realpart imagpart char-code char code-char symbol-name symbol-package-name intern intern-in-package-of-symbol symbol-append bozo equal eql eq member-eq member member-equal list-lis ffnnamep subsequencep legal-variable-or-constant-namep genvar collect-non-x arglistp cons-term match-tests-and-binding er-hard-val the-fixnum! the-signed-byte! xxxjoin xxxjoin-fixnum number-of-digits lambda-body flambdap make-lambda make-let flambda-applicationp doublet-listp singleton-list-p ascii-code! formals arity def-body program-termp equivalence-relationp >=-len all->=-len strip-cadrs strip-cddrs sublis-var subcor-var new-namep global-symbol symbol-doublet-listp remove1-eq pair-lis$ add-to-set-eq pseudo-termp all-vars ffn-symb fargs translate-and-test intersectp check-vars-not-free position collect-cdrs-when-car-eq restrict-alist substitute sublis remove1-assoc function-symbolp the with-live-state state-global-let* integer-range-p signed-byte-p unsigned-byte-p boole$ make-var-lst the-mv nth-aliases fix-true-list duplicates evens odds resize-list conjoin2 conjoin-untranslated-terms search count our-multiple-value-prog1 all-calls filter-atoms unprettyify variantp free-vars-in-hyps destructors alist-to-keyword-alist occur dumb-occur sublis-expr generate-variable subst-var subst-var-lst))