1(DEFPKG "M1"
2        '(&REST * + - / < <= > >= ACL2-COUNT AND ASSOC
3                ATOM CAR CASE CDR COERCE CONCATENATE
4                COND CONS CONSP DECLARE DEFCONST
5                DEFMACRO DEFTHM DEFUN DISABLE E/D ENDP
6                EQUAL EXPT IF IGNORE IMPLIES IN-THEORY
7                INCLUDE-BOOK INTERN-IN-PACKAGE-OF-SYMBOL
8                LET LET* LIST
9                LIST* MOD MUTUAL-RECURSION NATP NIL NOT
10                O-P O< OR OTHERWISE PAIRLIS$ PAIRLIS-X2
11                PROGN QUOTE QUOTEP STRING STRIP-CARS
12                SYMBOL-NAME SYMBOLP SYNTAXP T XARGS ZP))
13
14; NOTE: Only the forms above are evaluated (as opposed the ones below,
15; which merely are read) when translating to ML.  On a related note:
16; the following IN-PACKAGE form is for use by a2ml, but all forms in
17; this file assume that the current package is actually "ACL2".
18
19(IN-PACKAGE "M1")
20
21(DEFUN M1::PUSH (M1::X M1::Y) (CONS M1::X M1::Y))
22
23(DEFUN M1::TOP (M1::STACK) (CAR M1::STACK))
24
25(DEFUN M1::POP (M1::STACK) (CDR M1::STACK))
26
27(DEFUN M1::NTH (M1::N LIST)
28       (IF (ZP M1::N)
29           (CAR LIST)
30           (M1::NTH (BINARY-+ '-1 M1::N)
31                    (CDR LIST))))
32
33(DEFUN M1::MAKE-STATE
34       (M1::PC M1::LOCALS M1::STACK M1::PROGRAM)
35       (CONS M1::PC
36             (CONS M1::LOCALS
37                   (CONS M1::STACK (CONS M1::PROGRAM 'NIL)))))
38
39(DEFUN M1::PC (M1::S) (M1::NTH '0 M1::S))
40
41(DEFUN M1::LOCALS (M1::S) (M1::NTH '1 M1::S))
42
43(DEFUN M1::STACK (M1::S) (M1::NTH '2 M1::S))
44
45(DEFUN M1::PROGRAM (M1::S) (M1::NTH '3 M1::S))
46
47(DEFUN M1::OP-CODE (M1::INST) (CAR M1::INST))
48
49(DEFUN M1::ARG1 (M1::INST) (M1::NTH '1 M1::INST))
50
51(DEFUN M1::ARG2 (M1::INST) (M1::NTH '2 M1::INST))
52
53(DEFUN M1::ARG3 (M1::INST) (M1::NTH '3 M1::INST))
54
55(DEFUN M1::LEN (M1::X)
56       (IF (ENDP M1::X)
57           '0
58           (BINARY-+ '1 (M1::LEN (CDR M1::X)))))
59
60(DEFUN M1::APP (M1::X M1::Y)
61       (IF (ENDP M1::X)
62           M1::Y
63           (CONS (CAR M1::X)
64                 (M1::APP (CDR M1::X) M1::Y))))
65
66(DEFUN M1::REV (M1::X)
67       (IF (ENDP M1::X)
68           'NIL
69           (M1::APP (M1::REV (CDR M1::X))
70                    (CONS (CAR M1::X) 'NIL))))
71
72(DEFUN M1::REV1 (M1::X M1::A)
73       (IF (ENDP M1::X)
74           M1::A
75           (M1::REV1 (CDR M1::X)
76                     (CONS (CAR M1::X) M1::A))))
77
78(DEFUN M1::FREV (M1::X) (M1::REV1 M1::X 'NIL))
79
80(DEFUN M1::REPEAT (M1::TH M1::N)
81       (IF (ZP M1::N)
82           'NIL
83           (CONS M1::TH
84                 (M1::REPEAT M1::TH (BINARY-+ '-1 M1::N)))))
85
86(DEFUN M1::POPN (M1::N M1::STK)
87       (IF (ZP M1::N)
88           M1::STK
89           (M1::POPN (BINARY-+ '-1 M1::N)
90                     (M1::POP M1::STK))))
91
92(DEFUN M1::UPDATE-NTH (M1::N M1::V LIST)
93       (IF (ZP M1::N)
94           (CONS M1::V (CDR LIST))
95           (CONS (CAR LIST)
96                 (M1::UPDATE-NTH (BINARY-+ '-1 M1::N)
97                                 M1::V (CDR LIST)))))
98
99(DEFUN M1::MEMBER (M1::E LIST)
100       (IF (ENDP LIST)
101           'NIL
102           (IF (EQUAL M1::E (CAR LIST))
103               'T
104               (M1::MEMBER M1::E (CDR LIST)))))
105
106(DEFUN M1::INDEX (M1::E M1::LST)
107       (IF (ENDP M1::LST)
108           '0
109           (IF (EQUAL M1::E (CAR M1::LST))
110               '0
111               (BINARY-+ '1
112                         (M1::INDEX M1::E (CDR M1::LST))))))
113
114(DEFUN M1::SUPPLIEDP (M1::KEY M1::ARGS)
115       (IF (ENDP M1::ARGS)
116           'NIL
117           (IF (EQUAL M1::KEY (CAR M1::ARGS))
118               'T
119               (M1::SUPPLIEDP M1::KEY (CDR (CDR M1::ARGS))))))
120
121(DEFUN M1::ACTUAL (M1::KEY M1::ARGS)
122       (IF (ENDP M1::ARGS)
123           'NIL
124           (IF (EQUAL M1::KEY (CAR M1::ARGS))
125               (CAR (CDR M1::ARGS))
126               (M1::ACTUAL M1::KEY (CDR (CDR M1::ARGS))))))
127
128(DEFUN M1::BOUNDP (M1::VAR M1::ALIST)
129       (IF (ENDP M1::ALIST)
130           'NIL
131           (IF (EQUAL M1::VAR (CAR (CAR M1::ALIST)))
132               'T
133               (M1::BOUNDP M1::VAR (CDR M1::ALIST)))))
134
135(DEFUN M1::BINDING (M1::VAR M1::ALIST)
136       (IF (ENDP M1::ALIST)
137           'NIL
138           (IF (EQUAL M1::VAR (CAR (CAR M1::ALIST)))
139               (CAR (CDR (CAR M1::ALIST)))
140               (M1::BINDING M1::VAR (CDR M1::ALIST)))))
141
142(DEFUN M1::BIND (M1::VAR M1::VAL M1::ALIST)
143       (IF (ENDP M1::ALIST)
144           (CONS (CONS M1::VAR (CONS M1::VAL 'NIL))
145                 'NIL)
146           (IF (EQUAL M1::VAR (CAR (CAR M1::ALIST)))
147               (CONS (CONS M1::VAR (CONS M1::VAL 'NIL))
148                     (CDR M1::ALIST))
149               (CONS (CAR M1::ALIST)
150                     (M1::BIND M1::VAR M1::VAL (CDR M1::ALIST))))))
151
152(DEFUN M1::U-FIX (M1::X M1::N) (MOD M1::X (EXPT '2 M1::N)))
153
154(DEFUN M1::S-FIX (M1::X M1::N)
155       ((LAMBDA (M1::TEMP M1::N)
156                (IF (< M1::TEMP (EXPT '2 (BINARY-+ '-1 M1::N)))
157                    M1::TEMP
158                    (BINARY-+ M1::TEMP (UNARY-- (EXPT '2 M1::N)))))
159        (MOD M1::X (EXPT '2 M1::N))
160        M1::N))
161
162(DEFUN M1::U-BIG1 (M1::LST M1::ACC)
163       (IF (ENDP M1::LST)
164           M1::ACC
165           (M1::U-BIG1 (CDR M1::LST)
166                       (BINARY-+ (M1::U-FIX (CAR M1::LST) '8)
167                                 (BINARY-* (EXPT '2 '8) M1::ACC)))))
168
169(DEFUN M1::U-BIG (M1::LST) (M1::U-BIG1 M1::LST '0))
170
171(DEFUN M1::S-BIG (M1::LST)
172       (M1::S-FIX (M1::U-BIG M1::LST)
173                  (BINARY-* '8 (M1::LEN M1::LST))))
174
175(DEFUN M1::NEXTN (M1::N M1::LST)
176       (IF (ZP M1::N)
177           'NIL
178           (CONS (CAR M1::LST)
179                 (M1::NEXTN (BINARY-+ '-1 M1::N)
180                            (CDR M1::LST)))))
181
182(DEFUN M1::SKIPN (M1::N M1::LST)
183       (IF (ZP M1::N)
184           M1::LST
185           (M1::SKIPN (BINARY-+ '-1 M1::N)
186                      (CDR M1::LST))))
187