Included Books
other
(in-package "ACL2")
other
(program)
include-book
(include-book "symbol-btree")
rtl-untrans-lopfunction
(defun rtl-untrans-lop (lop x y width) (cond ((and (consp y) (eq (car y) lop) (equal (car (last y)) width)) (list* lop x (cdr y))) (t (list lop x y width))))
sum-cat-sizesfunction
(defun sum-cat-sizes (lst acc) (if (endp lst) acc (if (acl2-numberp (cadr lst)) (sum-cat-sizes (cddr lst) (+ (cadr lst) acc)) nil)))
rtl-untrans-catfunction
(defun rtl-untrans-cat (x xsize y ysize) (cond ((and (consp y) (eq (car y) 'cat) (integerp ysize) (eql ysize (sum-cat-sizes (cdr y) 0))) (list* 'cat x xsize (cdr y))) (t (list 'cat x xsize y ysize))))
cond1-lengthfunction
(defun cond1-length (term) (case-match term (('if1 & & z) (1+ (cond1-length z))) (& 1)))
rtl-untrans-andmacro
(defmacro rtl-untrans-and (&rest args) (cons 'untranslate-and args))
rtl-untrans-ormacro
(defmacro rtl-untrans-or (&rest args) (cons 'untranslate-or args))
*rtl-untrans-boolean-primitives*constant
(defconst *rtl-untrans-boolean-primitives* *untranslate-boolean-primitives*)
rtl-untrans1mutual-recursion
(mutual-recursion (defun rtl-untrans1 (term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (let ((term (if preprocess-fn (mv-let (erp term1) (ev-fncall-w! preprocess-fn (list term wrld) wrld nil nil nil nil t) (or (and (null erp) term1) term)) term))) (cond ((variablep term) term) ((fquotep term) (cond ((or (acl2-numberp (cadr term)) (stringp (cadr term)) (characterp (cadr term)) (eq (cadr term) nil) (eq (cadr term) t) (keywordp (cadr term))) (cadr term)) (t term))) ((flambda-applicationp term) (make-let-or-let* (collect-non-trivial-bindings (lambda-formals (ffn-symb term)) (rtl-untrans1-lst (fargs term) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) nil (rtl-untrans1 (lambda-body (ffn-symb term)) iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((and (eq (ffn-symb term) 'nth) (quotep (fargn term 1)) (integerp (cadr (fargn term 1))) (<= 0 (cadr (fargn term 1)))) (let ((accessor-name (accessor-root (cadr (fargn term 1)) (fargn term 2) wrld))) (list 'nth (or accessor-name (cadr (fargn term 1))) (rtl-untrans1 (fargn term 2) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))) ((and (eq (ffn-symb term) 'update-nth) (quotep (fargn term 1)) (integerp (cadr (fargn term 1))) (<= 0 (cadr (fargn term 1)))) (let ((accessor-name (accessor-root (cadr (fargn term 1)) (fargn term 3) wrld))) (list 'update-nth (or accessor-name (cadr (fargn term 1))) (rtl-untrans1 (fargn term 2) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 3) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))) ((and (eq (ffn-symb term) 'update-nth-array) (quotep (fargn term 1)) (integerp (cadr (fargn term 1))) (<= 0 (cadr (fargn term 1)))) (let ((accessor-name (accessor-root (cadr (fargn term 1)) (fargn term 4) wrld))) (list 'update-nth-array (or accessor-name (cadr (fargn term 1))) (rtl-untrans1 (fargn term 2) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 3) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 4) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))) ((eq (ffn-symb term) 'binary-+) (cons '+ (rtl-untrans1-lst (right-associated-args 'binary-+ term) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((eq (ffn-symb term) 'unary-/) (list '/ (rtl-untrans1 (fargn term 1) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((eq (ffn-symb term) 'unary--) (list '- (rtl-untrans1 (fargn term 1) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((eq (ffn-symb term) 'if) (case-match term (('if x1 *nil* *t*) (list 'not (rtl-untrans1 x1 t untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (('if x1 x2 *nil*) (rtl-untrans-and (rtl-untrans1 x1 t untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 x2 iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) iff-flg)) (('if x1 *nil* x2) (rtl-untrans-and (list 'not (rtl-untrans1 x1 t untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) (rtl-untrans1 x2 iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) iff-flg)) (('if x1 x1 x2) (rtl-untrans-or (rtl-untrans1 x1 iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 x2 iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (('if x1 x2 *t*) (rtl-untrans-or (list 'not (rtl-untrans1 x1 t untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) (rtl-untrans1 x2 iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (('if x1 *t* x2) (cond ((or iff-flg (and (nvariablep x1) (not (fquotep x1)) (member-eq (ffn-symb x1) *rtl-untrans-boolean-primitives*))) (rtl-untrans-or (rtl-untrans1 x1 t untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 x2 iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (t (rtl-untrans-if term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))) (& (rtl-untrans-if term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))) ((eq (ffn-symb term) 'if1) (cond ((> (cond1-length term) 2) (cons 'cond1 (rtl-untrans-into-cond1-clauses term untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (t (list 'if1 (rtl-untrans1 (fargn term 1) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 2) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 3) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))))) ((and (eq (ffn-symb term) 'not) (nvariablep (fargn term 1)) (not (fquotep (fargn term 1))) (member-eq (ffn-symb (fargn term 1)) '(< o<))) (list (if (eq (ffn-symb (fargn term 1)) '<) '<= 'o<=) (rtl-untrans1 (fargn (fargn term 1) 2) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn (fargn term 1) 1) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((eq (ffn-symb term) 'not) (dumb-negate-lit (rtl-untrans1 (fargn term 1) t untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((member-eq (ffn-symb term) '(implies iff)) (fcons-term* (ffn-symb term) (rtl-untrans1 (fargn term 1) t untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 2) t untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((eq (ffn-symb term) 'cons) (rtl-untrans-cons term untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) ((and (eq (ffn-symb term) 'synp) (quotep (fargn term 2))) (cadr (fargn term 2))) ((eq (ffn-symb term) 'binary-cat) (rtl-untrans-cat (rtl-untrans1 (fargn term 1) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 2) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 3) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 4) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((and (eq (fargn term 2) '$path) (let ((fn (symbol-btree-lookup (ffn-symb term) sigs-btree))) (and fn (list fn (rtl-untrans1 (fargn term 1) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))))) ((and (eq (ffn-symb term) 'return-last) (quotep (fargn term 1)) (let* ((key (unquote (fargn term 1))) (fn (and (symbolp key) key (let ((tmp (return-last-lookup key wrld))) (if (consp tmp) (car tmp) tmp))))) (and fn (cons fn (rtl-untrans1-lst (cdr (fargs term)) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))))) (t (let* ((pair (cdr (assoc-eq (ffn-symb term) untrans-tbl))) (op (car pair)) (flg (cdr pair))) (cond (op (cons op (rtl-untrans1-lst (cond ((and flg (cdr (fargs term)) (null (cddr (fargs term)))) (right-associated-args (ffn-symb term) term)) (t (fargs term))) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (t (let ((op (cdr (assoc-eq (ffn-symb term) lops-alist)))) (cond (op (rtl-untrans-lop op (rtl-untrans1 (fargn term 1) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 2) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 3) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (t (mv-let (ad-list base) (make-reversed-ad-list term nil) (cond (ad-list (pretty-parse-ad-list ad-list '(#\R) 1 (rtl-untrans1 base nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (t (cons (ffn-symb term) (rtl-untrans1-lst (fargs term) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))))))))))))))) (defun rtl-untrans-cons1 (term untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (cond ((variablep term) (mv nil (rtl-untrans1 term nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((fquotep term) (mv nil (rtl-untrans1 term nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) ((eq (ffn-symb term) 'cons) (mv-let (elements x) (rtl-untrans-cons1 (fargn term 2) untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (mv (cons (rtl-untrans1 (fargn term 1) nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) elements) x))) (t (mv nil (rtl-untrans1 term nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld))))) (defun rtl-untrans-cons (term untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (mv-let (elements x) (rtl-untrans-cons1 term untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (cond ((eq x nil) (cons 'list elements)) ((null (cdr elements)) (list 'cons (car elements) x)) (t (cons 'list* (append elements (list x))))))) (defun rtl-untrans-if (term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (cond ((> (case-length nil term) 2) (case-match term (('if (& key &) & &) (list* 'case key (rtl-untrans-into-case-clauses key term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))))) ((> (cond-length term) 2) (cons 'cond (rtl-untrans-into-cond-clauses term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (t (list 'if (rtl-untrans1 (fargn term 1) t untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 2) iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 (fargn term 3) iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))))) (defun rtl-untrans-into-case-clauses (key term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (case-match term (('if (pred !key ('quote val)) x y) (cond ((and (or (eq pred 'equal) (eq pred 'eql)) (eqlablep val)) (cond ((or (eq val t) (eq val nil) (eq val 'otherwise)) (cons (list (list val) (rtl-untrans1 x iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) (rtl-untrans-into-case-clauses key y iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (t (cons (list val (rtl-untrans1 x iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) (rtl-untrans-into-case-clauses key y iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))))) ((and (eq pred 'member) (eqlable-listp val)) (cons (list val (rtl-untrans1 x iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) (rtl-untrans-into-case-clauses key y iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (t (list (list 'otherwise (rtl-untrans1 term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))))) (& (list (list 'otherwise (rtl-untrans1 term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))))) (defun rtl-untrans-into-cond-clauses (term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (case-match term (('if x1 x2 x3) (cons (list (rtl-untrans1 x1 t untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 x2 iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) (rtl-untrans-into-cond-clauses x3 iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (& (list (list t (rtl-untrans1 term iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))))) (defun rtl-untrans-into-cond1-clauses (term untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (case-match term (('if1 x1 x2 x3) (cons (list (rtl-untrans1 x1 nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1 x2 nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld)) (rtl-untrans-into-cond1-clauses x3 untrans-tbl sigs-btree lops-alist preprocess-fn wrld))) (& (list (list t (rtl-untrans1 term nil untrans-tbl sigs-btree lops-alist preprocess-fn wrld)))))) (defun rtl-untrans1-lst (lst iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (cond ((null lst) nil) (t (cons (rtl-untrans1 (car lst) iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld) (rtl-untrans1-lst (cdr lst) iff-flg untrans-tbl sigs-btree lops-alist preprocess-fn wrld))))))
str=-up-tofunction
(defun str=-up-to (str1 str2 i bound) (declare (xargs :mode :program)) (if (>= i bound) t (and (eql (char str1 i) (char str2 i)) (str=-up-to str1 str2 (1+ i) bound))))
all-dollar-symbsfunction
(defun all-dollar-symbs (alist) (declare (xargs :guard (symbol-alistp alist) :mode :program)) (if (endp alist) t (and (let* ((name (symbol-name (caar alist))) (len (length name))) (and (not (eql len 0)) (eql (char name (1- len)) #\$) (symbolp (cdar alist)) (let* ((name2 (symbol-name (cdar alist))) (len2 (length name2))) (and (eql len2 (1- len)) (str=-up-to name name2 0 len2))))) (all-dollar-symbs (cdr alist)))))
other
(table rtl-tbl nil nil :guard (cond ((eq key 'lops-alist) t) ((eq key 'sigs-btree) t) (t nil)))
other
(table rtl-tbl 'lops-alist '((binary-land . land) (binary-lior . lior) (binary-lxor . lxor)))
dollarfyfunction
(defun dollarfy (sym) (declare (xargs :mode :logic :guard (symbolp sym))) (let* ((old-name (symbol-name sym)) (name (concatenate 'string old-name "$"))) (if (eq (intern old-name "ACL2") sym) (intern name "ACL2") (intern-in-package-of-symbol name sym))))
dollar-alistfunction
(defun dollar-alist (syms acc) (declare (xargs :mode :logic :guard (and (symbol-listp syms) (alistp acc)))) (if (endp syms) acc (dollar-alist (cdr syms) (acons (dollarfy (car syms)) (car syms) acc))))
rtl-untranslatefunction
(defun rtl-untranslate (term iff-flg wrld) (let ((rtl-tbl (table-alist 'rtl-tbl wrld))) (rtl-untrans1 term iff-flg (untrans-table wrld) (cdr (assoc 'sigs-btree rtl-tbl)) (cdr (assoc 'lops-alist rtl-tbl)) (untranslate-preprocess-fn wrld) wrld)))
rtl-untranslate-lstfunction
(defun rtl-untranslate-lst (lst iff-flg wrld) (let ((rtl-tbl (table-alist 'rtl-tbl wrld))) (rtl-untrans1-lst lst iff-flg (untrans-table wrld) (cdr (assoc-eq 'sigs-btree rtl-tbl)) (cdr (assoc-eq 'lops-alist rtl-tbl)) (untranslate-preprocess-fn wrld) wrld)))
other
(table user-defined-functions-table 'untranslate 'rtl-untranslate)
other
(table user-defined-functions-table 'untranslate-lst 'rtl-untranslate-lst)
extend-sigs-btreemacro
(defmacro extend-sigs-btree (name) (let ((name$ (dollarfy name))) `(table rtl-tbl 'sigs-btree (rebalance-symbol-btree (symbol-btree-update ',NAME$ ',NAME (cdr (assoc 'sigs-btree (table-alist 'rtl-tbl world))))))))
rebalance-sigs-btreemacro
(defmacro rebalance-sigs-btree nil `(table rtl-tbl 'sigs-btree (rebalance-symbol-btree (cdr (assoc 'sigs-btree (table-alist 'rtl-tbl world))))))
expand-address-catfunction
(defun expand-address-cat (car-addr raw-term term wrld) (declare (ignore term wrld)) (cond ((member car-addr '(1 2)) (list car-addr)) ((evenp car-addr) (msg "It is illegal to dive to arguments in even-numbered positions of a ~ CAT expression, after the first. Hence, address ~x0 is illegal for ~ (untranslated) term~|~x1." car-addr raw-term)) ((eql car-addr (- (length raw-term) 2)) (make-list (floor (1- car-addr) 2) :initial-element 3)) (t (append (make-list (floor (1- car-addr) 2) :initial-element 3) (list 1)))))
other
(add-dive-into-macro cat expand-address-cat)
expand-address-lxorfunction
(defun expand-address-lxor (car-addr raw-term term wrld) (declare (ignore term wrld)) (let* ((diff (- car-addr (- (length raw-term) 2)))) (cond ((eql diff 0) (make-list (1- car-addr) :initial-element 2)) ((< diff 0) (append (make-list (1- car-addr) :initial-element 2) '(1))) ((eql diff 1) (list 3)) (t (msg "Argument position ~x0 is too big for diving into ~ (untranslated) term~|~x1." car-addr raw-term)))))
other
(add-dive-into-macro lxor expand-address-lxor)
other
(add-dive-into-macro lior expand-address-lxor)
other
(add-dive-into-macro land expand-address-lxor)