Context Navigation

LINToASM.ma @ 687

Last change on this file since 687 was 687, checked in by mulligan, 10 years ago
Renamed to enforce consistency of filenames
File size: 9.7 KB

Line
1	include "cerco/Util.ma".
2	include "cerco-intermediate-languages/utilities/BitVectorTrieSet.ma".
3	include "cerco-intermediate-languages/LIN/LIN.ma".
4
5	let rec association (i: Identifier) (l: list (Identifier × nat))
6	on l: member i (eq_bv ?) l → nat ≝
7	match l return λl. member i (eq_bv ?) l → nat with
8	[ nil ⇒ λabsd. ?
9	\| cons hd tl ⇒
10	λprf: member i (eq_bv ?) (cons ? hd tl).
11	(match eq_bv ? (\fst hd) i return λb. eq_bv ? (\fst hd) i = b → nat with
12	[ true ⇒ λeq_prf. \snd hd
13	\| false ⇒ λeq_prf. association i tl ?
14	]) (refl ? (eq_bv ? (\fst hd) i))
15	].
16	[ cases absd
17	\| cases prf
18	[ > eq_prf
19	# H
20	cases H
21	\| # H
22	assumption
23	]
24	]
25	qed.
26
27	definition statement_labels ≝
28	λg: list (Identifier × nat).
29	λs: LINStatement g.
30	match s with
31	[ LIN_St_Goto lbl ⇒ set_insert ? lbl (set_empty ?)
32	\| LIN_St_Label lbl ⇒ set_insert ? lbl (set_empty ?)
33	\| LIN_St_CostLabel lbl ⇒ set_insert ? lbl (set_empty ?)
34	\| LIN_St_CondAcc lbl ⇒ set_insert ? lbl (set_empty ?)
35	\| _ ⇒ set_empty ?
36	].
37
38	definition function_labels_internal ≝
39	λglobals: list (Identifier × nat).
40	λlabels: BitVectorTrieSet 8.
41	λstatement: LINStatement globals.
42	set_union ? labels (statement_labels globals statement).
43
44	(* dpm: A = Identifier *)
45	definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet 8 ≝
46	λA: Type[0].
47	λglobals: list (Identifier × nat).
48	λf: A × (LINFunctionDefinition globals).
49	let 〈ignore, fun_def〉 ≝ f in
50	match fun_def return λ_. BitVectorTrieSet 8 with
51	[ LIN_Fu_Internal stmts ⇒
52	foldl ? ? (function_labels_internal globals) (set_empty 8) stmts
53	\| LIN_Fu_External _ ⇒ set_empty ?
54	].
55
56	definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet 8 ≝
57	λA: Type[0].
58	λglobals: list (Identifier × nat).
59	λlabels: BitVectorTrieSet 8.
60	λfunct: A × (LINFunctionDefinition globals).
61	set_union ? labels (function_labels ? globals funct).
62
63	definition program_labels ≝
64	λglobals: list (Identifier × nat).
65	λprogram.
66	foldl ? ? (program_labels_internal ? globals)
67	(set_empty 8) (LIN_Pr_funs globals program).
68
69	definition data_of_int ≝ λbv. DATA bv.
70	definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
71	definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
72
73	axiom ImplementedInRuntime: False.
74
75	definition translate_statements ≝
76	λglobals: list (Identifier × nat).
77	λlin_statement: LINStatement globals.
78	match lin_statement with
79	[ LIN_St_Goto lbl ⇒ [ Jmp lbl ]
80	\| LIN_St_Label lbl ⇒ [ Label lbl ]
81	\| LIN_St_Comment _ ⇒ [ ]
82	\| LIN_St_CostLabel lbl ⇒ [ Cost lbl ]
83	\| LIN_St_Pop ⇒ [ Instruction (POP ? accumulator_address) ]
84	\| LIN_St_Push ⇒ [ Instruction (PUSH ? accumulator_address) ]
85	\| LIN_St_ClearCarry ⇒ [ Instruction (CLR ? CARRY) ]
86	\| LIN_St_Return ⇒ [ Instruction (RET ?) ]
87	\| LIN_St_CallId f ⇒ [ Call f ]
88	\| LIN_St_OpAccs accs ⇒
89	match accs with
90	[ Mul ⇒ [ Instruction (MUL ? ACC_A ACC_B) ]
91	\| Divu ⇒ [ Instruction (DIV ? ACC_A ACC_B) ]
92	\| Modu ⇒ ?
93	]
94	\| LIN_St_Op1 op1 ⇒
95	match op1 with
96	[ Cmpl ⇒ [ Instruction (CPL ? ACC_A) ]
97	\| Inc ⇒ [ Instruction (INC ? ACC_A) ]
98	]
99	\| LIN_St_Op2 op2 reg ⇒
100	match op2 with
101	[ Add ⇒
102	let reg' ≝ register_address reg in
103	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
104	direct;
105	register ]] x) → ? with
106	[ ACC_A ⇒ λacc_a: True.
107	[ Instruction (ADD ? ACC_A accumulator_address) ]
108	\| DIRECT d ⇒ λdirect1: True.
109	[ Instruction (ADD ? ACC_A (DIRECT d)) ]
110	\| REGISTER r ⇒ λregister1: True.
111	[ Instruction (ADD ? ACC_A (REGISTER r)) ]
112	\| _ ⇒ λother: False. ⊥
113	] (subaddressing_modein … reg')
114	\| Addc ⇒
115	let reg' ≝ register_address reg in
116	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
117	direct;
118	register ]] x) → ? with
119	[ ACC_A ⇒ λacc_a: True.
120	[ Instruction (ADDC ? ACC_A accumulator_address) ]
121	\| DIRECT d ⇒ λdirect2: True.
122	[ Instruction (ADDC ? ACC_A (DIRECT d)) ]
123	\| REGISTER r ⇒ λregister2: True.
124	[ Instruction (ADDC ? ACC_A (REGISTER r)) ]
125	\| _ ⇒ λother: False. ⊥
126	] (subaddressing_modein … reg')
127	\| Sub ⇒
128	let reg' ≝ register_address reg in
129	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
130	direct;
131	register ]] x) → ? with
132	[ ACC_A ⇒ λacc_a: True.
133	[ Instruction (SUBB ? ACC_A accumulator_address) ]
134	\| DIRECT d ⇒ λdirect3: True.
135	[ Instruction (SUBB ? ACC_A (DIRECT d)) ]
136	\| REGISTER r ⇒ λregister3: True.
137	[ Instruction (SUBB ? ACC_A (REGISTER r)) ]
138	\| _ ⇒ λother: False. ⊥
139	] (subaddressing_modein … reg')
140	\| And ⇒
141	let reg' ≝ register_address reg in
142	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
143	direct;
144	register ]] x) → ? with
145	[ ACC_A ⇒ λacc_a: True.
146	[ Instruction (NOP ?) ]
147	\| DIRECT d ⇒ λdirect4: True.
148	[ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
149	\| REGISTER r ⇒ λregister4: True.
150	[ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
151	\| _ ⇒ λother: False. ⊥
152	] (subaddressing_modein … reg')
153	\| Or ⇒
154	let reg' ≝ register_address reg in
155	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
156	direct;
157	register ]] x) → ? with
158	[ ACC_A ⇒ λacc_a: True.
159	[ Instruction (NOP ?) ]
160	\| DIRECT d ⇒ λdirect5: True.
161	[ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))) ]
162	\| REGISTER r ⇒ λregister5: True.
163	[ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))) ]
164	\| _ ⇒ λother: False. ⊥
165	] (subaddressing_modein … reg')
166	\| Xor ⇒
167	let reg' ≝ register_address reg in
168	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
169	direct;
170	register ]] x) → ? with
171	[ ACC_A ⇒ λacc_a: True.
172	[ Instruction (XRL ? (inr ? ? 〈accumulator_address, ACC_A〉)) ]
173	\| DIRECT d ⇒ λdirect6: True.
174	[ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉)) ]
175	\| REGISTER r ⇒ λregister6: True.
176	[ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉)) ]
177	\| _ ⇒ λother: False. ⊥
178	] (subaddressing_modein … reg')
179	]
180	\| LIN_St_Int reg byte ⇒
181	let reg' ≝ register_address reg in
182	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
183	direct;
184	register ]] x) → ? with
185	[ REGISTER r ⇒ λregister7: True.
186	[ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, (data_of_int byte)〉)))))) ]
187	\| ACC_A ⇒ λacc: True.
188	[ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, (data_of_int byte)〉)))))) ]
189	\| DIRECT d ⇒ λdirect7: True.
190	[ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, (data_of_int byte)〉))))) ]
191	\| _ ⇒ λother: False. ⊥
192	] (subaddressing_modein … reg')
193	\| LIN_St_FromAcc reg ⇒
194	let reg' ≝ register_address reg in
195	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
196	direct;
197	register ]] x) → ? with
198	[ REGISTER r ⇒ λregister8: True.
199	[ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉)))))) ]
200	\| ACC_A ⇒ λacc: True.
201	[ Instruction (NOP ?) ]
202	\| DIRECT d ⇒ λdirect8: True.
203	[ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉))))) ]
204	\| _ ⇒ λother: False. ⊥
205	] (subaddressing_modein … reg')
206	\| LIN_St_ToAcc reg ⇒
207	let reg' ≝ register_address reg in
208	match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
209	direct;
210	register ]] x) → ? with
211	[ REGISTER r ⇒ λregister9: True.
212	[ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))))) ]
213	\| DIRECT d ⇒ λdirect9: True.
214	[ Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))))) ]
215	\| ACC_A ⇒ λacc_a: True.
216	[ Instruction (NOP ?) ]
217	\| _ ⇒ λother: False. ⊥
218	] (subaddressing_modein … reg')
219	\| LIN_St_Load ⇒ [ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉)) ]
220	\| LIN_St_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
221	\| LIN_St_Address addr proof ⇒
222	let look ≝ association addr globals proof in
223	[ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ]
224	\| LIN_St_CondAcc lbl ⇒
225	(* dpm: this should be handled in translate_code! *)
226	[ WithLabel (JNZ ? lbl) ]
227	].
228	try assumption
229	try @ I
230	cases ImplementedInRuntime
231	qed.
232
233	definition translate_code ≝
234	λglobals: list (Identifier × nat).
235	λcode: list (LINStatement globals).
236	flatten ? (map ? ? (translate_statements globals) code).

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format