blob: 817f11260adbb6005a60b96063bf656ec6ed5f28 (
plain)
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
|
(IN-PACKAGE "ACL2")
; Edited by Matt K.:
; (INCLUDE-BOOK "source_shallow" :DIR :BOOKS)
(INCLUDE-BOOK "../books/source_shallow")
; Edited by Matt K.:
; (INCLUDE-BOOK "computed-hints" :DIR :BOOKS)
(INCLUDE-BOOK "../books/computed-hints")
(DEFUND |itr_tmp_11| NIL (LIST 0 1))
(DEFUN |$itr_loop_iter_fibs_3| (|tmp_10| |$limit| |hist_2|)
(DECLARE
(XARGS :MEASURE (ACL2-COUNT (|+| 1 |$limit| (|-| |tmp_10|))) :HINTS
(MEASURE-HINT)))
(IF (NOT (AND (NATP |tmp_10|) (NATP |$limit|) (TRUE-LISTP |hist_2|)))
(LIST 0 0)
(IF (> |tmp_10| |$limit|) |hist_2|
(LET
((|$arm-result|
(COND
((< |tmp_10| 2)
(NTH (NAT-REP (REVERSE (LIST (= (LOGHEAD 1 |tmp_10|) 1))))
(|itr_tmp_11|)))
(T
(C-WORD-+ 8
(NTH
(NAT-REP
(REVERSE
(LIST (= (LOGHEAD 1 (C-WORD-- 32 |tmp_10| 1)) 1))))
|hist_2|)
(NTH
(NAT-REP
(REVERSE
(LIST (= (LOGHEAD 1 (C-WORD-- 32 |tmp_10| 2)) 1))))
|hist_2|))))))
(|$itr_loop_iter_fibs_3| (|1+| |tmp_10|) |$limit|
(UPDATE-NTH (LOGHEAD 1 |tmp_10|) |$arm-result| |hist_2|))))))
(DEFUND |itr_iter_fibs_3| (|tmp_10|)
(IF (NOT (NATP |tmp_10|)) (LIST 0 0)
(|$itr_loop_iter_fibs_3| 0 |tmp_10| (LIST 0 0))))
(DEFUN |$itr_0_typep| (X) (AND (NATP X) (< X 4294967296)))
(DEFUND |itr_fib| (|i|)
(IF (NOT (AND (|$itr_0_typep| |i|))) 0
(LET* ((|tmp_8| (|itr_iter_fibs_3| |i|)))
(NTH (NAT-REP (REVERSE (LIST (= (LOGHEAD 1 |i|) 1)))) |tmp_8|))))
|
