/usr/share/acl2-6.5/books/tools/easy-simplify.lisp is in acl2-books-source 6.5-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 | (in-package "ACL2")
(include-book "bstar")
;; This provides a straightforward interface for simplifying a term. It uses
;; the proof checker's pc-rewrite* function. It can handle rewriting under
;; some hypotheses, under a user-provided equivalence relation,
;; Note: replaced this with acl2's built-in expand-assumptions-1
;; (defun if-nest-to-hyp-list (x)
;; (cond ((equal x ''t) nil)
;; ((or (atom x)
;; (not (eq (car x) 'if))
;; (not (equal (fourth x) ''nil)))
;; (list x))
;; (t (append (if-nest-to-hyp-list (second x))
;; (if-nest-to-hyp-list (third x))))))
;; takes a translated term and an implicitly conjoined list of translated hyps
(defun easy-simplify-term1-fn (term hyps hints equiv
normalize rewrite
repeat
backchain-limit
state)
(declare (XargS :mode :program :stobjs state))
(b* ((world (w state))
((er hint-settings)
(translate-hint-settings
'simp-term "Goal" hints 'easy-simplify-term world state))
(ens (ens state))
(base-rcnst
(change rewrite-constant
*empty-rewrite-constant*
:current-enabled-structure ens
:force-info t))
((er rcnst)
(load-hint-settings-into-rcnst
hint-settings base-rcnst nil world 'easy-simplify-term state))
(ens (access rewrite-constant rcnst :current-enabled-structure))
((mv flg hyps-type-alist ?ttree)
(hyps-type-alist hyps ens world state))
((when flg)
(mv "Contradiction in the hypotheses"
nil state))
((mv ?step-limit new-term ?new-ttree state)
(pc-rewrite*
term hyps-type-alist
(if (eq equiv 'equal)
nil
(list (make congruence-rule
:rune *fake-rune-for-anonymous-enabled-rule*
:nume nil
:equiv equiv)))
(eq equiv 'iff)
world rcnst nil nil normalize rewrite ens state
repeat backchain-limit
(initial-step-limit world state))))
(value new-term)))
(defun easy-simplify-term-fn (term hyp-term hints equiv
normalize rewrite repeat backchain-limit state)
(declare (XargS :mode :program :stobjs state))
(b* ((world (w state))
((er trans-term)
(translate term t nil t 'easy-simplify-term world state))
((er trans-hyp-term)
(translate hyp-term t nil t 'easy-simplify-term world state))
;; ;; bozo find out how ACL2 does this, if it does
;; (hyps (if-nest-to-hyp-list trans-hyp-term))
;; ... like this:
(hyps (expand-assumptions-1 trans-hyp-term))
((er new-term)
(easy-simplify-term1-fn
trans-term hyps hints equiv normalize rewrite repeat backchain-limit
state)))
(value (untranslate new-term nil (w state)))))
(defmacro easy-simplify-term (term &key
(hyp 't)
hint
(equiv 'equal)
(normalize 't)
(rewrite 't)
(repeat '1000)
(backchain-limit '1000))
":doc-section programming
Easy-simplify-term: simple interface for simplifying a term.~/
Usage:
~bv[]
(easy-simplify-term (my-fn (foo) (bar baz))
;; optional keyword args:
:hyp (and (integerp baz) (<= 0 baz))
:hint (:in-theory (enable my-fn) :expand ((foo)))
:equiv equal
:normalize t
:rewrite t
:repeat 555
:backchain-limit 5)
~ev[]
Important NOTE: The HINT keyword should be given a hint keyword/val list,
as in the example above, NOT a list of subgoal or computed hints,
e.g. ((\"Goal\" :foo)). ~/
Simplifies a term under the given hypothesis and equivalence context,
with guidance from the given hint."
`(easy-simplify-term-fn
',term ',hyp ',hint ',equiv
',normalize ',rewrite ',repeat ',backchain-limit
state))
(defmacro defopen (name term &key (hyp 't) hint
(rule-classes ':rewrite))
;; This is a simple event generator that creates a theorem by finding out
;; what a term simplifies to under some hyp and with some hint. In contrast
;; to misc/defopener, because this only does simplification (no clausify),
;; the reductions may be less powerful, but it seems to produce more compact
;; expressions compared to defopener, where the result is formed by combining
;; several clauses produced from the original term.
`(make-event
(b* (((er new-hyp-term)
(acl2::easy-simplify-term ,hyp :hint ,hint))
((er new-term)
(acl2::easy-simplify-term-fn
',term new-hyp-term ',hint 'equal t t 1000 1000 state)))
(value `(defthm ,',name
,(if (not (eq ',hyp t))
`(implies ,',hyp (equal ,',term ,new-term))
`(equal ,',term ,new-term))
:hints (("goal" . ,',hint))
:rule-classes ,',rule-classes)))))
|