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