/usr/share/acl2-8.0dfsg/books/misc/computed-hint-rewrite.lisp is in acl2-books-source 8.0dfsg-1.
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 139 140 141 142 143 144 145 146 147 | ; Copyright (C) 2013, Regents of the University of Texas
; Written by Matt Kaufmann, May, 2008
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; This book defines a function, computed-hint-rewrite, that makes it easy to
; call the ACL2 rewriter in a computed hint. For details see the comment in
; the definition of computed-hint-rewrite, below. Thanks to Jared Davis for
; requesting this utility.
; This utility does not attempt to build a linear database for the given hyps.
; But it probably could with a little work.
(in-package "ACL2")
(program)
(set-state-ok t)
(defun simplify-clause-rcnst (cl hist pspv wrld)
; Keep this in sync with simplify-clause. We might want to call this function
; in simplify-clause rather than keeping in sync.
(let ((rcnst (access prove-spec-var pspv :rewrite-constant)))
(cond ((assoc-eq 'settled-down-clause hist)
(change rewrite-constant
rcnst
:force-info
(if (ffnnamep-lst 'if cl)
'weak
t)))
(t
(let* ((new-force-info (if (ffnnamep-lst 'if cl)
'weak
t))
(induction-concl-terms
(access prove-spec-var pspv :induction-concl-terms))
(hist-entry-hit (found-hit-rewrite-hist-entry hist))
(hit-rewrite2 (or (eq hist-entry-hit 'hit-rewrite2)
(and (eq hist-entry-hit 'hit-rewrite)
(not (some-element-dumb-occur-lst
induction-concl-terms
cl))))))
(cond (hit-rewrite2
(change rewrite-constant
rcnst
:force-info new-force-info))
(t
(change rewrite-constant
rcnst
:force-info new-force-info
:terms-to-be-ignored-by-rewrite
(append
(access prove-spec-var
pspv :induction-hyp-terms)
(access rewrite-constant
rcnst
:terms-to-be-ignored-by-rewrite))
:expand-lst
(append? (access rewrite-constant
rcnst :expand-lst)
; We give the user's expand-lst priority, in case it specifies :with for a term
; that is also an enabled call in induction-concl-terms.
(filter-disabled-expand-terms
induction-concl-terms
(access rewrite-constant
rcnst
:current-enabled-structure)
wrld))))))))))
(defun computed-hint-rewrite (term hyps provep
cl hist pspv wrld ctx state)
; This function returns an error triple (mv erp val state). Erp is t if we
; find a contradiction in the hypotheses. Otherwise erp is nil and val is a
; pair (cons rewritten-term ttree), where rewritten-term and ttree are
; respectively the rewritten value of term together with the justifying
; tag-tree. If you want only the rewritten term, check that erp is nil and
; then use (car val).
; Set provep to t or nil for optimal results if you are trying to prove term or
; its negation, respectively; otherwise set it to ?.
(let* ((rcnst (simplify-clause-rcnst cl hist pspv wrld))
(ens (access rewrite-constant rcnst :current-enabled-structure))
(gstack nil))
(mv-let
(flg hyps-type-alist ttree)
(hyps-type-alist hyps ens wrld state)
(cond (flg (er hard ctx
"~x0 found a contradiction in the hypotheses."
'computed-hint-rewrite))
(t (sl-let (new-term new-ttree)
(rewrite-entry
(rewrite term nil 'computed-hint-rewrite)
:rdepth (rewrite-stack-limit wrld)
:type-alist hyps-type-alist
:obj provep
:geneqv (if (member-eq provep '(t nil)) *geneqv-iff* nil)
:pequiv-info nil
:fnstack nil
:ancestors nil
:backchain-limit (backchain-limit wrld :rewrite)
:step-limit (initial-step-limit wrld state)
:simplify-clause-pot-lst nil
:rcnst rcnst
:gstack gstack
:ttree ttree)
(declare (ignorable step-limit))
(cons new-term new-ttree)))))))
; Silly example:
#||
(defun my-computed-hint (clause hist pspv wrld ctx state)
(declare (xargs :mode :program
:stobjs state))
(cond ((null (cdr clause))
(value nil))
(t
(let ((hyps (dumb-negate-lit-lst (butlast clause 1)))
(conc (car (last clause))))
(mv-let (erp term-ttree state)
(computed-hint-rewrite conc hyps t clause hist pspv wrld ctx
state)
(cond ((and (not erp) term-ttree)
(prog2$ (cw "~%NOTE: computed-hint-rewrite returned ~
term-ttree pair ~x0.~|~@1"
term-ttree
(if (and (gag-mode)
(@ print-clause-ids))
"~%"
""))
(value (and (equal (car term-ttree)
''t)
'(:use car-cons)))))
(t (value nil))))))))
(add-default-hints '((my-computed-hint clause hist pspv world ctx state)))
; Optional:
(in-theory (disable (:definition binary-append)))
(thm (equal (append (append x y) z) (append (car (cons x x)) y z)))
||#
|