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
|
(in-package "ACL2")
(include-book "../../../../../data-structures/utilities")
(u::import-as-macros
U::A-UNIQUE-SYMBOL-IN-THE-U-PACKAGE
defloop)
(defloop non-rec-functions (runes world)
(for ((rune in runes))
(unless (fgetprop (cadr rune) 'induction-machine nil world)
(collect rune))))
(defloop rec-functions (runes world)
(for ((rune in runes))
(when (fgetprop (cadr rune) 'induction-machine nil world)
(collect rune))))
(defmacro ww (form)
"With (W state) ..."
`(LET ((WORLD (W STATE))) ,form))
;Example
;(ww (non-rec-functions (definition-theory (current-theory :here)) world))
;Example
; (deftheory test (non-rec-functions (theory 'table-def) world))
;
; Macro ld-up-to fast loads ACL2 events in a file to a specified point.
; (ld-up-to "<filename>" <event_name> {:speed <speed> })
; This command loads ACL2 file <filename> to the point where
; <event_name> is first defined.
; Since ld-up-to skips proofs of the theorems in a loaded file by
; default, a user can quickly reach the state where he or she wants
; to work in. <even_name> can be any symbol newly defined by the
; event at the desired breaking point. For instance, a label
; defined by deflabel can be used as well. Keyword :all can be
; specified when the user want to load the whole file.
;
; The user can specify loading speed using keyword :speed
; :speed 0 Does not skip proofs. The slowest way to load a file.
; :speed 1 Skips proofs, but performs other checks on theorems.
; Ld-up-to loads files at this speed by default.
; :speed 2 Skips proofs and other checks on theorems. Warning
; will not be printed out. It also skips events local to
; the ACL2 file.
; Example
; (ld-up-to "invariants-def.lisp" invariants)
; This command loads ACL2 file invariant-def.lisp until it finds the
; definition of function invariants.
;
; (ld-up-to "invariants-def.lisp" :all :speed 2)
; this command load the all events in invariants-def.lisp except
; events local to the ACL2 book.
(defmacro ld-up-to (file event &key (speed '1))
(let ((skip-proofs-flag (if (equal speed 0) nil
(if (equal speed 1) t ''include-book))))
`(ld ,file :ld-pre-eval-filter ',event :ld-skip-proofsp ,skip-proofs-flag)))
; Macro refresh rolls back ACL2 history and reloads ACL2 events fast.
;
; (refresh <filename> {:back-to <event1>} {:up-to <event2>} {:speed <speed>})
;
; Refresh first undoes events back to the point where <event1> was
; defined, then it loads ACL2 file <filename> up to the point where
; <event2> is newly defined. When previously executed ACL2 events
; like definition and theorems are modified, the current world of ACL2
; is corrupted and a user may want to restart the ACL2 from scratch.
; However, restarting ACL2 takes a long time especially if many books
; are loaded. Refresh helps to reload modified files and get the
; newest state of ACL2 world quickly. It only undoes to the point
; where symbol <event1> is defined, and then loads file <filename>,
; skipping proofs by default. Since refresh loads ACL2 books included
; by <filename>, usually the user only has to specify the top ACL2 book.
; <event1> can be a symbol defined in an included book, and refresh
; undoes the include-book of the included book. If :back-to
; keyword is not supplied, refresh undoes all user defined events. If
; :up-to keyword is not given, it load all events in <filename>. So
; (refresh <filename>) is equivalent to (refresh <filename> :back-to 1
; :up-to :all). <event1> can be a number designating an event.
;
; The user can also specify loading speed using keyword :speed
; :speed 0 Does not skip proofs. The slowest way to load a file.
; :speed 1 Skips proofs, but performs other checks on theorems.
; Ld-up-to loads files at this speed by default.
; :speed 2 Skips proofs and other checks on theorems. Warning
; will not be printed out. It also skips events local to
; the ACL2 file.
(defmacro refresh (file &key (back-to '1) (up-to ':all) (speed '1))
(let ((skip-proofs-flag (if (equal speed 0) nil
(if (equal speed 1) t ''include-book))))
`(ld '((ubt! ',back-to) (ld ,file :ld-pre-eval-filter ',up-to
:ld-skip-proofsp ,skip-proofs-flag)))))
|
