This file is indexed.

/usr/share/acl2-6.3/books/tools/easy-simplify.lisp is in acl2-books-source 6.3-5.

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