utilities - ACL2 Book

other

(in-package "CGEN")

other

(set-verify-guards-eagerness 2)

other

(include-book "std/util/bstar" :dir :system)

other

(include-book "acl2s/utilities" :dir :system)

get-cgen-guard-checkingmacro

(defmacro get-cgen-guard-checking
  nil
  `(@ cgen-guard-checking))

set-cgen-guard-checkingmacro

(defmacro set-cgen-guard-checking
  (val)
  `(make-event (er-progn (assign cgen-guard-checking ,CGEN::VAL)
      (value '(value-triple nil)))
    :check-expansion t))

other

(set-cgen-guard-checking :none)

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))))

debug-flagmacro

(defmacro debug-flag (vl) `(> ,CGEN::VL 3))

system-debug-flagmacro

(defmacro system-debug-flag
  (vl)
  `(> ,CGEN::VL 4))

verbose-stats-flagmacro

(defmacro verbose-stats-flag
  (vl)
  `(> ,CGEN::VL 2))

verbose-flagmacro

(defmacro verbose-flag (vl) `(> ,CGEN::VL 1))

inhibit-output-flagmacro

(defmacro inhibit-output-flag
  (vl)
  `(<= ,CGEN::VL 0))

normal-output-flagmacro

(defmacro normal-output-flag
  (vl)
  `(> ,CGEN::VL 0))

acl2-getpropmacro

(defmacro acl2-getprop
  (name prop w &key default)
  `(getprop ,CGEN::NAME
    ,CGEN::PROP
    ,CGEN::DEFAULT
    'current-acl2-world
    ,CGEN::W))

or-listfunction

(defun or-list
  (lst)
  (if (atom lst)
    lst
    (or (car lst) (or-list (cdr lst)))))

to-symbol-in-packagefunction

(defun to-symbol-in-package
  (sym pkg-name)
  (declare (xargs :guard (and (symbolp sym) (pkgp pkg-name))))
  (fix-intern$ (symbol-name sym) pkg-name))

to-symbol-in-package-lstfunction

(defun to-symbol-in-package-lst
  (sym-lst pkg)
  (declare (xargs :guard (and (symbol-listp sym-lst)
        (pkgp pkg))))
  (if (endp sym-lst)
    nil
    (cons (to-symbol-in-package (car sym-lst) pkg)
      (to-symbol-in-package-lst (cdr sym-lst)
        pkg))))

list-up-listsfunction

(defun list-up-lists
  (l1 l2)
  (declare (xargs :guard (and (true-listp l1)
        (true-listp l2)
        (= (len l1) (len l2)))))
  "same as listlis"
  (if (endp l1)
    nil
    (cons (list (car l1) (car l2))
      (list-up-lists (cdr l1) (cdr l2)))))

other

(verify-termination legal-variable-or-constant-namep)

other

(verify-termination legal-constantp)

other

(verify-termination lambda-keywordp)

other

(verify-guards lambda-keywordp)

other

(verify-guards legal-constantp)

proper-symbolpfunction

(defun proper-symbolp
  (x)
  (declare (xargs :guard t))
  (and (symbolp x)
    (not (or (keywordp x)
        (booleanp x)
        (legal-constantp x)))))

proper-symbol-listpfunction

(defun proper-symbol-listp
  (xs)
  (declare (xargs :guard t))
  (if (atom xs)
    (null xs)
    (and (proper-symbolp (car xs))
      (proper-symbol-listp (cdr xs)))))

keyword-listpfunction

(defun keyword-listp
  (x)
  (if (consp x)
    (and (keywordp (car x))
      (keyword-listp (cdr x)))
    (null x)))

trans-eval-single-valuefunction

(defun trans-eval-single-value
  (expr ctx state)
  (declare (xargs :mode :program :stobjs (state)))
  (state-global-let* ((guard-checking-on (@ cgen-guard-checking)))
    (er-let* ((ans (trans-eval expr ctx state t)))
      (if (equal (car ans) '(nil))
        (value (cdr ans))
        (er soft
          ctx
          "Expected a single return value in evaluation of ~x0."
          expr)))))

other

(local (defthm union-true-lists
    (implies (and (true-listp l1)
        (true-listp l2))
      (true-listp (union-equal l1 l2)))))

union-lstsfunction

(defun union-lsts
  (lsts)
  (declare (xargs :mode :logic :guard (true-list-listp lsts)))
  (if (endp lsts)
    nil
    (union-equal (car lsts)
      (union-lsts (cdr lsts)))))

assoc-lstfunction

(defun assoc-lst
  (keys alist)
  (declare (xargs :guard (and (true-listp keys)
        (alistp alist))))
  (if (endp keys)
    nil
    (cons (assoc-equal (car keys) alist)
      (assoc-lst (cdr keys) alist))))

flattenfunction

(defun flatten
  (b lst&)
  (declare (xargs :guard (true-listp lst&)))
  (if (atom b)
    (cons b lst&)
    (flatten (car b)
      (flatten (cdr b) lst&))))

other

(defthm flatten-is-true-list1
  (implies (true-listp lst)
    (true-listp (flatten b lst)))
  :hints (("Goal" :in-theory (enable flatten))))

mem-treefunction

(defun mem-tree
  (x tree)
  (declare (xargs :guard (symbolp x)))
  (if (atom tree)
    (eq x tree)
    (or (mem-tree x (car tree))
      (mem-tree x (cdr tree)))))

other

(include-book "misc/total-order" :dir :system)

order-two-termsfunction

(defun order-two-terms
  (t1 t2)
  (declare (xargs :guard t))
  (if (<< t1 t2)
    (mv t1 t2)
    (mv t2 t1)))

other

(defthm flatten-is-true-list
  (implies (true-listp lst)
    (true-listp (flatten b lst)))
  :rule-classes :type-prescription)

other

(in-theory (disable flatten))

listof-alistpfunction

(defun listof-alistp
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (eq x nil))
    (t (and (alistp (car x))
        (listof-alistp (cdr x))))))

true-list-symbol-alistpfunction

(defun true-list-symbol-alistp
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (eq x nil))
    (t (and (symbol-alistp (car x))
        (true-list-symbol-alistp (cdr x))))))

symbol-doublet-list-listpfunction

(defun symbol-doublet-list-listp
  (xs)
  (declare (xargs :guard t))
  (if (null xs)
    t
    (if (atom xs)
      nil
      (and (symbol-doublet-listp (car xs))
        (symbol-doublet-list-listp (cdr xs))))))

symbol-alist-listpfunction

(defun symbol-alist-listp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (and (symbol-alistp (car x))
      (symbol-alist-listp (cdr x)))))

other

(verify-termination >=-len)

other

(verify-termination all->=-len)

strip-cadrsfunction

(defun strip-cadrs
  (x)
  (declare (xargs :guard (all->=-len x 2)))
  (cond ((atom x) nil)
    (t (cons (cadar x) (strip-cadrs (cdr x))))))

boolean-or-macrofunction

(defun boolean-or-macro
  (lst)
  (if (consp lst)
    (list 'if
      (car lst)
      't
      (boolean-or-macro (cdr lst)))
    'nil))

boolean-ormacro

(defmacro boolean-or
  (&rest args)
  (boolean-or-macro args))

pos-listpfunction

(defun pos-listp
  (l)
  (declare (xargs :guard t))
  (cond ((atom l) (eq l nil))
    (t (and (posp (car l)) (pos-listp (cdr l))))))

get-value-from-keyword-value-listfunction

(defun get-value-from-keyword-value-list
  (key kv-lst)
  (declare (xargs :guard (keyword-value-listp kv-lst)))
  (second (assoc-keyword key kv-lst)))

other

(mutual-recursion (defun get-free-vars1
    (term ans)
    "A free variable is a symbol that is not a constant, i.e., it excludes T,
    NIL, and *CONST*, and keywords"
    (declare (xargs :guard (pseudo-termp term)
        :verify-guards nil))
    (cond ((atom term) (if (proper-symbolp term)
          (add-to-set-eq term ans)
          ans))
      ((eq (car term) 'quote) ans)
      (t (get-free-vars1-lst (cdr term) ans))))
  (defun get-free-vars1-lst
    (terms ans)
    (declare (xargs :guard (pseudo-term-listp terms)
        :verify-guards nil))
    (cond ((endp terms) ans)
      (t (get-free-vars1-lst (cdr terms)
          (get-free-vars1 (car terms) ans))))))

get-free-vars0function

(defun get-free-vars0
  (form state)
  (declare (xargs :mode :program :stobjs (state)))
  (if (termp form (w state))
    (value (get-free-vars1 form 'nil))
    (er-let* ((term (translate form
           t
           nil
           t
           'get-free-vars
           (w state)
           state)))
      (value (get-free-vars1 term 'nil)))))

get-free-varsmacro

(defmacro get-free-vars
  (form)
  `(get-free-vars0 ,CGEN::FORM state))

all-vars-lstfunction

(defun all-vars-lst
  (terms)
  "all free variables in list of terms"
  (declare (xargs :guard (pseudo-term-listp terms)))
  (all-vars1-lst terms 'nil))

filter-alist-keysfunction

(defun filter-alist-keys
  (alst wanted-keys)
  (declare (xargs :guard (and (alistp alst)
        (true-listp wanted-keys))))
  (if (endp alst)
    nil
    (let* ((key (caar alst)) (we-want-to-add (member-equal key wanted-keys)))
      (if we-want-to-add
        (cons (car alst)
          (filter-alist-keys (cdr alst) wanted-keys))
        (filter-alist-keys (cdr alst) wanted-keys)))))

remove-entryfunction

(defun remove-entry
  (key alist)
  (declare (xargs :guard (and (alistp alist))))
  (if (endp alist)
    nil
    (if (equal key (caar alist))
      (cdr alist)
      (cons (car alist)
        (remove-entry key (cdr alist))))))

remove-entry-lstfunction

(defun remove-entry-lst
  (keys alist)
  (declare (xargs :guard (and (true-listp keys)
        (alistp alist))))
  (if (endp keys)
    alist
    (remove-entry-lst (cdr keys)
      (remove-entry (car keys) alist))))

get-valfunction

(defun get-val
  (key alist)
  (declare (xargs :guard (and (alistp alist))))
  (if (endp alist)
    nil
    (if (equal key (caar alist))
      (cdar alist)
      (get-val key (cdr alist)))))

get-val-lstfunction

(defun get-val-lst
  (keys alist)
  (declare (xargs :guard (and (true-listp keys)
        (alistp alist))))
  (if (endp keys)
    nil
    (let ((found-val (get-val (car keys) alist)))
      (if found-val
        (cons found-val
          (get-val-lst (cdr keys) alist))
        (get-val-lst (cdr keys) alist)))))

remove-and-add-at-end-entryfunction

(defun remove-and-add-at-end-entry
  (key val alist)
  (declare (xargs :guard (alistp alist)))
  (if (endp alist)
    (list (cons key val))
    (let* ((curr-entry (car alist)) (curr-key (car curr-entry))
        (curr-val (cdr curr-entry)))
      (if (not (equal key curr-key))
        (cons curr-entry
          (remove-and-add-at-end-entry key
            val
            (cdr alist)))
        (if (equal val curr-val)
          alist
          (remove-and-add-at-end-entry key
            val
            (cdr alist)))))))

remove-and-add-at-front-entryfunction

(defun remove-and-add-at-front-entry
  (key val alist)
  (declare (xargs :guard (alistp alist)))
  (cons (cons key val)
    (remove-entry key alist)))

put-entryfunction

(defun put-entry
  (key val alist)
  (declare (xargs :guard (alistp alist)))
  (if (endp alist)
    (list (cons key val))
    (if (equal key (caar alist))
      (cons (cons key val) (cdr alist))
      (cons (car alist)
        (put-entry key val (cdr alist))))))

get-keyfunction

(defun get-key
  (val alist)
  (declare (xargs :guard (alistp alist)))
  (if (endp alist)
    nil
    (if (equal val (cdar alist))
      (caar alist)
      (get-key val (cdr alist)))))

get-key-lstfunction

(defun get-key-lst
  (vals alist)
  (declare (xargs :guard (and (true-listp vals)
        (alistp alist))))
  (if (endp vals)
    nil
    (let ((found-key (get-key (car vals) alist)))
      (if found-key
        (cons found-key
          (get-key-lst (cdr vals) alist))
        (get-key-lst (cdr vals) alist)))))

get-var-from-i-or-is-lstfunction

(defun get-var-from-i-or-is-lst
  (is var-i-alst)
  (declare (xargs :verify-guards nil))
  (if (endp is)
    nil
    (let ((i (car is)))
      (if (atom i)
        (let ((found-key (get-key i var-i-alst)))
          (if found-key
            (cons found-key
              (get-var-from-i-or-is-lst (cdr is)
                var-i-alst))
            (get-var-from-i-or-is-lst (cdr is)
              var-i-alst)))
        (let ((found-keys (get-key-lst i var-i-alst)))
          (if found-keys
            (cons found-keys
              (get-var-from-i-or-is-lst (cdr is)
                var-i-alst))
            (get-var-from-i-or-is-lst (cdr is)
              var-i-alst)))))))

get-all-keys1function

(defun get-all-keys1
  (val alist ans)
  (declare (xargs :guard (alistp alist)))
  (if (endp alist)
    ans
    (let* ((entry (car alist)) (key (car entry))
        (value (cdr entry)))
      (if (equal val value)
        (get-all-keys1 val
          (cdr alist)
          (cons key ans))
        (get-all-keys1 val (cdr alist) ans)))))

get-all-keysfunction

(defun get-all-keys
  (val alist)
  (declare (xargs :guard (alistp alist)))
  (get-all-keys1 val alist nil))

get-all-keys-lstfunction

(defun get-all-keys-lst
  (vals alist)
  (declare (xargs :guard (and (true-listp vals)
        (alistp alist))))
  (if (endp vals)
    nil
    (let ((found-keys (get-all-keys (car vals) alist)))
      (if found-keys
        (cons found-keys
          (get-all-keys-lst (cdr vals) alist))
        (get-all-keys-lst (cdr vals) alist)))))

trans-eval-single-value-with-bindingsfunction

(defun trans-eval-single-value-with-bindings
  (term bindings ctx state)
  (declare (xargs :mode :program :stobjs state))
  (state-global-let* ((guard-checking-on (@ cgen-guard-checking)))
    (er-let* ((term-val (simple-translate-and-eval term
           bindings
           nil
           ""
           ctx
           (w state)
           state
           t)))
      (value (cdr term-val)))))

make-var-value-cons-bindingsfunction

(defun make-var-value-cons-bindings
  (var-lst ans)
  (declare (xargs :guard (and (symbol-listp var-lst)
        (true-listp ans))))
  (if (endp var-lst)
    (cons 'list ans)
    (let ((var (car var-lst)))
      (make-var-value-cons-bindings (cdr var-lst)
        (append ans (list `(cons ',CGEN::VAR ,CGEN::VAR)))))))

make-var-value-list-bindingsfunction

(defun make-var-value-list-bindings
  (var-lst ans)
  (declare (xargs :guard (and (symbol-listp var-lst)
        (true-listp ans))))
  (if (endp var-lst)
    (cons 'list ans)
    (let ((var (car var-lst)))
      (make-var-value-list-bindings (cdr var-lst)
        (append ans (list `(list ',CGEN::VAR ,CGEN::VAR)))))))

make-constant-value-cons-bindingsfunction

(defun make-constant-value-cons-bindings
  (var-lst constant-val ans)
  (declare (xargs :guard (and (symbol-listp var-lst)
        (true-listp ans))))
  (if (endp var-lst)
    (cons 'list ans)
    (let ((var (car var-lst)))
      (make-constant-value-cons-bindings (cdr var-lst)
        constant-val
        (append ans
          (list (cons var constant-val)))))))

make-constant-value-let-bindingsfunction

(defun make-constant-value-let-bindings
  (var-lst constant-val ans)
  (declare (xargs :guard (and (symbol-listp var-lst)
        (true-listp ans))))
  (if (endp var-lst)
    ans
    (let ((var (car var-lst)))
      (make-constant-value-let-bindings (cdr var-lst)
        constant-val
        (append ans
          (list (list var constant-val)))))))

convert-listpair-to-conspair-lstfunction

(defun convert-listpair-to-conspair-lst
  (listpairs)
  (declare (xargs :guard (symbol-doublet-listp listpairs)))
  (if (endp listpairs)
    nil
    (cons (let* ((lstpair (car listpairs)) (fst (car lstpair))
          (snd (cadr lstpair)))
        (cons fst snd))
      (convert-listpair-to-conspair-lst (cdr listpairs)))))

convert-conspairs-to-listpairsfunction

(defun convert-conspairs-to-listpairs
  (conspairs)
  (declare (xargs :guard (symbol-alistp conspairs)))
  (if (endp conspairs)
    nil
    (cons (let* ((conspair (car conspairs)) (fst (car conspair))
          (snd (cdr conspair)))
        (list fst snd))
      (convert-conspairs-to-listpairs (cdr conspairs)))))

other

(local (defthm convert-conspairs-to-listpairs-sig1
    (implies (symbol-alistp p)
      (symbol-doublet-listp (convert-conspairs-to-listpairs p)))
    :rule-classes (:rewrite :type-prescription :forward-chaining)))

other

(local (defthm symbol-doublet-listp-implication1
    (implies (and (symbol-doublet-listp a) (consp a))
      (and (consp (car a))
        (symbolp (caar a))
        (consp (cdr (car a)))
        (null (cddr (car a)))))
    :rule-classes (:forward-chaining)))

count-occurrencesfunction

(defun count-occurrences
  (v lst)
  (declare (xargs :guard (true-listp lst)))
  (if (endp lst)
    0
    (if (equal v (car lst))
      (1+ (count-occurrences v (cdr lst)))
      (count-occurrences v (cdr lst)))))

sym-eq-lstfunction

(defun sym-eq-lst
  (syms1 syms2)
  (declare (xargs :guard (and (symbol-listp syms1)
        (symbol-listp syms2))))
  "returns first symbol in syms2 which is in syms1 o.w nil"
  (if (endp syms2)
    nil
    (if (member-eq (car syms2) syms1)
      (car syms2)
      (sym-eq-lst syms1 (cdr syms2)))))

insert-entry-after-keyfunction

(defun insert-entry-after-key
  (entry k alst)
  (declare (xargs :guard (and (symbolp k) (symbol-alistp alst))))
  "insert entry immediately after the pair in alst having key k"
  (if (endp alst)
    (list entry)
    (if (eq k (caar alst))
      (cons (car alst) (cons entry (cdr alst)))
      (cons (car alst)
        (insert-entry-after-key entry
          k
          (cdr alst))))))

get-ordered-alstfunction

(defun get-ordered-alst
  (keys alst ans)
  (declare (xargs :guard (and (true-listp keys)
        (alistp ans)
        (alistp alst))))
  "accumulate entries of alist in ans in the order of keys"
  (if (endp keys)
    ans
    (let ((at (assoc-equal (car keys) alst)))
      (if at
        (get-ordered-alst (cdr keys)
          alst
          (append ans (list at)))
        (get-ordered-alst (cdr keys)
          alst
          ans)))))

filter-infunction

(defun filter-in
  (lst in-lst)
  (declare (xargs :guard (and (true-listp lst)
        (true-listp in-lst))))
  (if (endp lst)
    nil
    (if (member-equal (car lst) in-lst)
      (cons (car lst)
        (filter-in (cdr lst) in-lst))
      (filter-in (cdr lst) in-lst))))

filter-not-infunction

(defun filter-not-in
  (lst in-lst)
  (declare (xargs :guard (and (true-listp lst)
        (true-listp in-lst))))
  (if (endp lst)
    nil
    (if (not (member-equal (car lst) in-lst))
      (cons (car lst)
        (filter-in (cdr lst) in-lst))
      (filter-in (cdr lst) in-lst))))

compose-two-alistsfunction

(defun compose-two-alists
  (a-b-alst b-c-alst)
  (declare (xargs :guard (and (alistp a-b-alst)
        (alistp b-c-alst))))
  (if (endp a-b-alst)
    nil
    (let* ((a-b (car a-b-alst)) (a (car a-b))
        (b (cdr a-b))
        (c (get-val b b-c-alst))
        (a-c (cons a c)))
      (cons a-c
        (compose-two-alists (cdr a-b-alst)
          b-c-alst)))))

subst-equalfunction

(defun subst-equal
  (new old tree)
  (cond ((equal tree old) new)
    ((atom tree) tree)
    (t (cons (subst-equal new old (car tree))
        (subst-equal new old (cdr tree))))))

other

(defttag :ev-fncall-w-ok)

other

(remove-untouchable ev-fncall-w t)

other

(defttag nil)

other

(mutual-recursion (defun my-ev-w
    (term alist
      ctx
      w
      hard-error-returns-nilp)
    "special eval function that does not need state and
cannot handle if, return-last,mv-list, stobjs, wormhole etc
very restrictive
Mainly to be used for evaluating enum lists "
    (declare (xargs :mode :program :guard (and (termp term w)
          (plist-worldp w)
          (symbol-alistp alist)
          (booleanp hard-error-returns-nilp))))
    (b* (((when (variablep term)) (let ((v (assoc-eq term alist)))
           (if v
             (mv nil (cdr v))
             (prog2$ (er hard
                 ctx
                 "Unbound variable ~x0.~%"
                 term)
               (mv t term))))) ((when (fquotep term)) (mv nil (cadr term)))
        ((when (eq (car term) 'if)) (b* (((mv cond-er cond) (my-ev-w (second term)
                 alist
                 ctx
                 w
                 hard-error-returns-nilp)) ((when cond-er) (prog2$ (er hard ctx "Eval if condition failed~%")
                  (mv t term))))
            (if cond
              (my-ev-w (third term)
                alist
                ctx
                w
                hard-error-returns-nilp)
              (my-ev-w (fourth term)
                alist
                ctx
                w
                hard-error-returns-nilp))))
        ((mv args-er args) (my-ev-w-lst (cdr term)
            alist
            ctx
            w
            hard-error-returns-nilp))
        ((when args-er) (prog2$ (er hard ctx "Eval args failed~%")
            (mv t term)))
        ((when (flambda-applicationp term)) (my-ev-w (lambda-body (car term))
            (pairlis$ (lambda-formals (car term)) args)
            ctx
            w
            hard-error-returns-nilp)))
      (ev-fncall-w (car term)
        args
        w
        nil
        nil
        t
        hard-error-returns-nilp
        nil)))
  (defun my-ev-w-lst
    (term-lst alist
      ctx
      w
      hard-error-returns-nilp)
    "special eval function that does not need state and
cannot handle return-last,mv-list, stobjs, wormhole etc
very restrictive
Mainly to be used for evaluating enum lists "
    (declare (xargs :mode :program :guard (and (term-listp term-lst w)
          (plist-worldp w)
          (symbol-alistp alist)
          (booleanp hard-error-returns-nilp))))
    (if (endp term-lst)
      (mv nil nil)
      (b* (((mv erp1 car-ans) (my-ev-w (car term-lst)
             alist
             ctx
             w
             hard-error-returns-nilp)) ((when erp1) (prog2$ (er hard
                ctx
                "eval ~x0 failed~%"
                (car term-lst))
              (mv t term-lst)))
          ((mv erp2 cdr-ans) (my-ev-w-lst (cdr term-lst)
              alist
              ctx
              w
              hard-error-returns-nilp))
          ((when erp2) (prog2$ (er hard ctx "eval failed~%")
              (mv t term-lst))))
        (mv nil (cons car-ans cdr-ans))))))

other

(push-untouchable ev-fncall-w t)

trans-my-ev-wfunction

(defun trans-my-ev-w
  (form ctx w hard-error-returns-nilp)
  (declare (xargs :mode :program :guard (and (plist-worldp w)
        (booleanp hard-error-returns-nilp))))
  (mv-let (erp term x)
    (translate11 form
      nil
      nil
      nil
      nil
      nil
      nil
      nil
      ctx
      w
      (default-state-vars nil))
    (declare (ignore x))
    (if erp
      (if hard-error-returns-nilp
        (mv erp form)
        (prog2$ (er hard
            ctx
            "~x0 could not be translated.~%"
            form)
          (mv erp form)))
      (my-ev-w term
        nil
        ctx
        w
        hard-error-returns-nilp))))

all-vars-in-var-term-alstfunction

(defun all-vars-in-var-term-alst
  (alst)
  (declare (xargs :guard (alistp alst)
      :verify-guards nil))
  (union-eq (get-free-vars1-lst (strip-cars alst) nil)
    (get-free-vars1-lst (strip-cdrs alst) nil)))

occurring-var-bindingsfunction

(defun occurring-var-bindings
  (bindings vars)
  (declare (xargs :guard (and (true-listp vars)
        (symbol-alistp bindings))))
  (if (endp vars)
    nil
    (let ((b (assoc-eq (car vars) bindings)))
      (if b
        (cons b
          (occurring-var-bindings bindings
            (cdr vars)))
        (occurring-var-bindings bindings
          (cdr vars))))))

quote-conses-and-symbols-in-bindingsfunction

(defun quote-conses-and-symbols-in-bindings
  (val-bs)
  (declare (xargs :guard (symbol-doublet-listp val-bs)))
  (if (endp val-bs)
    nil
    (b* (((list var val) (car val-bs)))
      (if (or (symbolp val)
          (and (consp val) (not (equal (car val) 'quote))))
        (cons (list var (list 'quote val))
          (quote-conses-and-symbols-in-bindings (cdr val-bs)))
        (cons (list var val)
          (quote-conses-and-symbols-in-bindings (cdr val-bs)))))))

filter-symbol-keys-in-alistfunction

(defun filter-symbol-keys-in-alist
  (alst)
  "Given an alist, it filters the entries that have
   symbols as the keys(first elem of cons)"
  (declare (xargs :guard (alistp alst)))
  (if (endp alst)
    nil
    (if (symbolp (caar alst))
      (cons (car alst)
        (filter-symbol-keys-in-alist (cdr alst)))
      (filter-symbol-keys-in-alist (cdr alst)))))

symbol-list-listpfunction

(defun symbol-list-listp
  (v)
  (declare (xargs :guard t))
  (if (atom v)
    (null v)
    (and (symbol-listp (car v))
      (symbol-list-listp (cdr v)))))

order-var-te-alist.function

(defun order-var-te-alist.
  (a connected-vs-lst ans.)
  "helper to order-var-te-alist"
  (declare (xargs :verify-guards nil
      :guard (and (symbol-alistp a)
        (symbol-list-listp connected-vs-lst)
        (symbol-alistp ans.))))
  (if (endp connected-vs-lst)
    ans.
    (b* ((vs (car connected-vs-lst)) (tes (get-val-lst vs a))
        (a-partial (pairlis$ vs tes)))
      (order-var-te-alist. a
        (cdr connected-vs-lst)
        (append ans. a-partial)))))

order-var-te-alistfunction

(defun order-var-te-alist
  (a connected-vs-lst)
  "order var-type-expression-dlist using connected-vertices information"
  (declare (xargs :verify-guards nil
      :guard (and (symbol-alistp a)
        (symbol-list-listp connected-vs-lst))))
  (if (null connected-vs-lst)
    a
    (order-var-te-alist. a
      connected-vs-lst
      'nil)))

to-stringfunction

(defun to-string
  (x)
  (declare (xargs :mode :program))
  (coerce (cdr (coerce (fms-to-string "~x0" (list (cons #\0 x)))
        'list))
    'string))

unsigned-60bits-pfunction

(defun unsigned-60bits-p
  (x)
  (declare (xargs :guard t))
  (unsigned-byte-p 60 x))

fixnumpfunction

(defun fixnump
  (x)
  (declare (xargs :guard t))
  (unsigned-60bits-p x))

accessmacro

(defmacro access
  (r a)
  `(access ,CGEN::R
    ,CGEN::R
    ,(ACL2S::FIX-INTERN-IN-PKG-OF-SYM (SYMBOL-NAME CGEN::A) :KEY)))

changemacro

(defmacro change
  (r a val)
  `(change ,CGEN::R
    ,CGEN::R
    ,(ACL2S::FIX-INTERN-IN-PKG-OF-SYM (SYMBOL-NAME CGEN::A) :KEY)
    ,CGEN::VAL))

get2-fnfunction

(defun get2-fn
  (nm key al default)
  (declare (xargs :guard (eqlable-alistp al)))
  (let ((lookup1 (assoc nm al)))
    (if (and (consp lookup1)
        (eqlable-alistp (cdr lookup1)))
      (let ((lookup2 (assoc key (cdr lookup1))))
        (or (and lookup2 (cdr lookup2)) default))
      default)))

get2macro

(defmacro get2
  (name key al &optional default)
  `(get2-fn ,CGEN::NAME
    ,CGEN::KEY
    ,CGEN::AL
    ,CGEN::DEFAULT))

get1-fnfunction

(defun get1-fn
  (key al default)
  (declare (xargs :guard (eqlable-alistp al)))
  (let* ((lookup (assoc key al)))
    (or (and lookup (cdr lookup)) default)))

get1macro

(defmacro get1
  (key kwd-alist &optional default)
  `(get1-fn ,CGEN::KEY ,CGEN::KWD-ALIST ,CGEN::DEFAULT))

cgen-dumb-negate-litfunction

(defun cgen-dumb-negate-lit
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (if (and (consp term)
      (eq (car term) 'if)
      (equal (third term) ''nil))
    (second term)
    (dumb-negate-lit term)))

cgen-dumb-negate-lit-lstfunction

(defun cgen-dumb-negate-lit-lst
  (lst)
  (declare (xargs :guard (pseudo-term-listp lst)))
  (cond ((endp lst) nil)
    (t (cons (cgen-dumb-negate-lit (car lst))
        (cgen-dumb-negate-lit-lst (cdr lst))))))

clause-mv-hyps-conclfunction

(defun clause-mv-hyps-concl
  (cl)
  (declare (xargs :verify-guards nil))
  (cond ((null cl) (mv 'nil ''nil))
    ((null (cdr cl)) (mv 'nil (car cl)))
    ((null (cddr cl)) (mv (list (cgen-dumb-negate-lit (car cl)))
        (cadr cl)))
    (t (mv (cgen-dumb-negate-lit-lst (butlast cl 1))
        (car (last cl))))))

clausify-hyps-conclfunction

(defun clausify-hyps-concl
  (hyps concl)
  (declare (xargs :verify-guards nil))
  (cond ((and (endp hyps) (equal concl ''nil)) 'nil)
    ((endp hyps) (list concl))
    ((endp (cdr hyps)) (list (cgen-dumb-negate-lit (car hyps))
        concl))
    (t (append (cgen-dumb-negate-lit-lst hyps)
        (list concl)))))

equiv-sym?function

(defun equiv-sym?
  (sym)
  (declare (xargs :guard t))
  (member-equal sym
    '(equal eq
      eql
      =
      int=
      string-equal
      hons-equal
      ==)))

equiv-term?function

(defun equiv-term?
  (term)
  (declare (xargs :guard t))
  (and (true-listp term)
    (= 3 (len term))
    (equiv-sym? (car term))))

is-var-equality-hypfunction

(defun is-var-equality-hyp
  (term)
  (declare (xargs :guard t))
  (and (equiv-term? term)
    (and (or (proper-symbolp (second term))
        (proper-symbolp (third term)))
      (not (equal (second term) (third term))))))

equiv-hyp?function

(defun equiv-hyp?
  (hyp)
  (declare (xargs :guard t))
  (and (equiv-term? hyp)
    (proper-symbolp (second hyp))
    (proper-symbolp (third hyp))))