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
|
;;
;; Copyright (C) 2021, Collins Aerospace
;; All rights reserved.
;;
;; This software may be modified and distributed under the terms
;; of the 3-clause BSD license. See the LICENSE file for details.
;;
(in-package "ACL2")
(skip-proofs
(defthm skip-proof-hint
nil
:rule-classes nil)
)
(defun sub-seq (spec id)
(if (and (not (consp spec)) (not (consp id))) nil
(if (not (consp id)) t
(if (not (consp spec)) nil
(and (equal (car spec) (car id))
(sub-seq (cdr spec) (cdr id)))))))
(set-state-ok t)
(defun except-fn (spec print clause stable id state)
(declare (ignorable stable clause state)
(xargs :mode :program))
(let ((id (cadr id)))
(if (equal spec id) (and print (cw "~x0~%" (prettyify-clause clause nil (w state))))
(and id
(if (sub-seq id spec) nil ;; (cw "~x0~%" (prettyify-clause clause nil (w state)))
(and
(not (sub-seq spec id))
'(:use skip-proof-hint)))))))
(defmacro except (subgoal &key (print 't))
(let ((spec (cadr (parse-clause-id subgoal))))
`(except-fn ',spec ,print clause stable-under-simplificationp id state)))
;; (include-book "except" :skip-proofs-okp t)
(defun goal-fn (spec clause stable id state)
(declare (ignore clause stable state))
(let ((id (cadr id)))
(equal spec id)))
(defmacro Goal (subgoal)
(let ((spec (cadr (parse-clause-id subgoal))))
`(goal-fn ',spec clause stable-under-simplificationp id state)))
|
