Context Navigation

LINToASM.ma @ 3444

Last change on this file since 3444 was 3066, checked in by tranquil, 8 years ago
implemented get_arg_16 for ACC_DPTR LINToASM is now agnostic as to where single global variables end up, as long as all global variables end up at the bottom of XData consequently, ASM preamble is back indicating sizes rather than addresses Assembly now correctly maps identifiers with offsets in case of code points
File size: 19.7 KB

Line
1	include "utilities/BitVectorTrieSet.ma".
2	include "utilities/state.ma".
3
4	include "ASM/Util.ma".
5	include "ASM/ASM.ma".
6
7	include "LIN/LIN.ma".
8
9	(* utilities to provide Identifier's and addresses *)
10	record ASM_universe : Type[0] :=
11	{ id_univ : universe ASMTag
12	; current_funct : ident
13	; ident_map : identifier_map SymbolTag Identifier
14	; label_map : identifier_map SymbolTag (identifier_map LabelTag Identifier)
15	; fresh_cost_label: Pos
16	}.
17
18	definition report_cost:
19	costlabel → state_monad ASM_universe unit ≝
20	λcl,u.
21	let clw ≝ word_of_identifier … cl in
22	if leb (fresh_cost_label … u) clw then
23	〈mk_ASM_universe … (id_univ … u) (current_funct … u) (ident_map … u)
24	(label_map … u) (succ clw), it〉
25	else
26	〈u,it〉.
27
28	definition Identifier_of_label :
29	label → state_monad ASM_universe Identifier ≝
30	λl,u.
31	let current ≝ current_funct … u in
32	let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
33	let 〈id, univ, lmap〉 ≝
34	match lookup … lmap l with
35	[ Some id ⇒ 〈id, id_univ … u, lmap〉
36	\| None ⇒
37	let 〈id, univ〉 ≝ fresh … (id_univ … u) in
38	〈id, univ, add … lmap l id〉
39	] in
40	〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
41	(fresh_cost_label … u), id〉.
42
43	definition Identifier_of_ident :
44	ident → state_monad ASM_universe Identifier ≝
45	λi,u.
46	let imap ≝ ident_map … u in
47	let res ≝ match lookup … imap i with
48	[ Some id ⇒ 〈id, id_univ … u, imap〉
49	\| None ⇒
50	let 〈id, univ〉 ≝ fresh … (id_univ … u) in
51	〈id, univ, add … imap i id〉
52	] in
53	let id ≝ \fst (\fst res) in
54	let univ ≝ \snd (\fst res) in
55	let imap ≝ \snd res in
56	〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
57	(fresh_cost_label … u), id〉.
58
59	definition new_ASM_universe :
60	∀p : joint_program LIN.ASM_universe ≝
61	λp.
62	mk_ASM_universe (mk_universe … one)
63	(an_identifier … one (* dummy *))
64	(empty_map …) (empty_map …) one.
65	(*@hide_prf normalize nodelta
66	cases p -p * #vars #functs #main #cost_init
67	#i #H
68	normalize nodelta
69	letin init_val ≝ (〈empty_map SymbolTag Identifier, mk_universe ASMTag one〉)
70	cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
71	[ %2{H} ] -H
72	lapply i -i lapply init_val -init_val
73	whd in match prog_var_names; normalize nodelta
74	elim vars -vars
75	[2: ** #id #r #v #tl #IH ] #init_val #i
76	[2: * [2: * ] #H @H ]
77	* [2: #H cases (orb_Prop_true … H) -H ] #H
78	@IH
79	[ %1 cases init_val normalize nodelta #init_map #off
80	>(proj1 ?? (eqb_true ???) H) @pair_elim #lft #rgt #_ @mem_set_add_id
81	\| %2{H}
82	\| %1 cases init_val in H; normalize nodelta #init_map #off #H
83	@pair_elim #lft #rgt #_
84	>mem_set_add @orb_Prop_r @H
85	]
86	qed.
87	*)
88
89	definition start_funct_translation :
90	∀globals,functions.(ident × (joint_function LIN globals functions)) →
91	state_monad ASM_universe unit ≝
92	λg,functs,id_f,u.
93	〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
94	(fresh_cost_label … u), it〉.
95
96	definition ASM_fresh :
97	state_monad ASM_universe Identifier ≝
98	λu.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
99	〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
100	(fresh_cost_label … u), id〉.
101
102	definition register_address: Register → [[ acc_a; direct; registr ]] ≝
103	λr: Register.
104	match r with
105	[ Register00 ⇒ REGISTER [[ false; false; false ]]
106	\| Register01 ⇒ REGISTER [[ false; false; true ]]
107	\| Register02 ⇒ REGISTER [[ false; true; false ]]
108	\| Register03 ⇒ REGISTER [[ false; true; true ]]
109	\| Register04 ⇒ REGISTER [[ true; false; false ]]
110	\| Register05 ⇒ REGISTER [[ true; false; true ]]
111	\| Register06 ⇒ REGISTER [[ true; true; false ]]
112	\| Register07 ⇒ REGISTER [[ true; true; true ]]
113	\| RegisterA ⇒ ACC_A
114	\| RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
115	\| RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 130)
116	\| RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 131)
117	\| _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
118	]. @I qed.
119
120	definition vector_cast :
121	∀A,n,m.A → Vector A n → Vector A m ≝
122	λA,n,m,dflt,v.
123	If leb n m then with prf do
124	replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
125	else with prf do
126	\snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
127	lapply prf @(leb_elim n)
128	[2,3: #_ * #abs elim (abs I) ]
129	#H #_ >commutative_plus_faster @eq_f [@sym_eq] @(minus_to_plus … (refl …))
130	[ assumption ]
131	@(transitive_le … (not_le_to_lt … H)) %2 %1
132	qed.
133
134	definition arg_address : hdw_argument →
135	[[ acc_a ; direct ; registr ; data ]] ≝
136	λa.
137	match a
138	with
139	[ Reg r ⇒ (register_address r : [[ acc_a ; direct ; registr ; data ]])
140	\| Imm v ⇒ (DATA v : [[ acc_a ; direct ; registr ; data ]])
141	].
142	[ elim (register_address ?) #rslt @is_in_subvector_is_in_supervector ] @I
143	qed.
144
145	definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
146
147	definition data_of_int ≝ λbv. DATA bv.
148	definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
149	definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
150
151	(* TODO: check and change to free bit *)
152	definition asm_other_bit ≝ BIT_ADDR (zero_byte).
153	definition one_word : Word ≝ bv_zero 15 @@ [[ true ]].
154
155	definition translate_statements :
156	∀globals.
157	joint_statement LIN globals →
158	state_monad ASM_universe pseudo_instruction ≝
159	λglobals,statement.
160	match statement with
161	[ final instr ⇒
162	match instr with
163	[ GOTO lbl ⇒
164	! lbl' ← Identifier_of_label … lbl ;
165	return Jmp (toASM_ident ? lbl')
166	\| RETURN ⇒ return Instruction (RET ?)
167	\| TAILCALL abs _ _ ⇒ Ⓧabs
168	]
169	\| sequential instr _ ⇒
170	match instr with
171	[ step_seq instr' ⇒
172	match instr' with
173	[ extension_seq ext ⇒
174	match ext with
175	[ SAVE_CARRY ⇒
176	return Instruction (MOV ? (inr ?? 〈asm_other_bit, CARRY〉))
177	\| RESTORE_CARRY ⇒
178	return Instruction (MOV ? (inl ?? (inr ?? 〈CARRY, asm_other_bit〉)))
179	\| LOW_ADDRESS lbl ⇒
180	! lbl' ← Identifier_of_label … lbl ;
181	return Mov (inr ?? 〈register_address RegisterA, LOW〉) lbl' one_word
182	\| HIGH_ADDRESS lbl ⇒
183	! lbl' ← Identifier_of_label … lbl ;
184	return Mov (inr ?? 〈register_address RegisterA, HIGH〉) lbl' one_word
185	]
186	\| COMMENT comment ⇒ return Comment comment
187	\| POP _ ⇒ return Instruction (POP ? accumulator_address)
188	\| PUSH _ ⇒ return Instruction (PUSH ? accumulator_address)
189	\| CLEAR_CARRY ⇒ return Instruction (CLR ? CARRY)
190	\| OPACCS accs _ _ _ _ ⇒
191	return match accs with
192	[ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
193	\| DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
194	]
195	\| OP1 op1 _ _ ⇒
196	return match op1 with
197	[ Cmpl ⇒ Instruction (CPL ? ACC_A)
198	\| Inc ⇒ Instruction (INC ? ACC_A)
199	\| Rl ⇒ Instruction (RL ? ACC_A)
200	]
201	\| OP2 op2 _ _ reg ⇒
202	return match arg_address … reg
203	return λx.is_in … [[ acc_a;
204	direct;
205	registr;
206	data ]] x → ? with
207	[ ACC_A ⇒ λacc_a: True.
208	match op2 with
209	[ Add ⇒ Instruction (ADD ? ACC_A accumulator_address)
210	\| Addc ⇒ Instruction (ADDC ? ACC_A accumulator_address)
211	\| Sub ⇒ Instruction (SUBB ? ACC_A accumulator_address)
212	\| Xor ⇒ Instruction (CLR ? ACC_A)
213	\| _ ⇒ Instruction (NOP ?)
214	]
215	\| DIRECT d ⇒ λdirect1: True.
216	match op2 with
217	[ Add ⇒ Instruction (ADD ? ACC_A (DIRECT d))
218	\| Addc ⇒ Instruction (ADDC ? ACC_A (DIRECT d))
219	\| Sub ⇒ Instruction (SUBB ? ACC_A (DIRECT d))
220	\| And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
221	\| Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉)))
222	\| Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DIRECT d〉))
223	]
224	\| REGISTER r ⇒ λregister1: True.
225	match op2 with
226	[ Add ⇒ Instruction (ADD ? ACC_A (REGISTER r))
227	\| Addc ⇒ Instruction (ADDC ? ACC_A (REGISTER r))
228	\| Sub ⇒ Instruction (SUBB ? ACC_A (REGISTER r))
229	\| And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
230	\| Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉)))
231	\| Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, REGISTER r〉))
232	]
233	\| DATA b ⇒ λdata : True.
234	match op2 with
235	[ Add ⇒ Instruction (ADD ? ACC_A (DATA b))
236	\| Addc ⇒ Instruction (ADDC ? ACC_A (DATA b))
237	\| Sub ⇒ Instruction (SUBB ? ACC_A (DATA b))
238	\| And ⇒ Instruction (ANL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
239	\| Or ⇒ Instruction (ORL ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉)))
240	\| Xor ⇒ Instruction (XRL ? (inl ? ? 〈ACC_A, DATA b〉))
241	]
242	\| _ ⇒ Ⓧ
243	] (subaddressing_modein …)
244	\| LOAD _ _ _ ⇒ return Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
245	\| STORE _ _ _ ⇒ return Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
246	\| ADDRESS id proof off _ _ ⇒
247	! Id ← Identifier_of_ident … id ;
248	return (Mov (inl ?? DPTR) Id off)
249	\| SET_CARRY ⇒
250	return Instruction (SETB ? CARRY)
251	\| MOVE regs ⇒
252	return match regs with
253	[ to_acc _ reg ⇒
254	match register_address reg return λx.is_in … [[ acc_a;
255	direct;
256	registr]] x → ? with
257	[ REGISTER r ⇒ λregister9: True.
258	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
259	\| DIRECT d ⇒ λdirect9: True.
260	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
261	\| ACC_A ⇒ λacc_a: True.
262	Instruction (NOP ?)
263	\| _ ⇒ Ⓧ
264	] (subaddressing_modein …)
265	\| from_acc reg _ ⇒
266	match register_address reg return λx.is_in … [[ acc_a;
267	direct;
268	registr ]] x → ? with
269	[ REGISTER r ⇒ λregister8: True.
270	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
271	\| ACC_A ⇒ λacc: True.
272	Instruction (NOP ?)
273	\| DIRECT d ⇒ λdirect8: True.
274	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
275	\| _ ⇒ Ⓧ
276	] (subaddressing_modein …)
277	\| int_to_reg reg b ⇒
278	match register_address reg return λx.is_in … [[ acc_a;
279	direct;
280	registr ]] x → ? with
281	[ REGISTER r ⇒ λregister7: True.
282	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, DATA b〉))))))
283	\| ACC_A ⇒ λacc: True.
284	if eq_bv … (bv_zero …) b then
285	Instruction (CLR ? ACC_A)
286	else
287	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
288	\| DIRECT d ⇒ λdirect7: True.
289	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, DATA b〉)))))
290	\| _ ⇒ Ⓧ
291	] (subaddressing_modein …)
292	\| int_to_acc _ b ⇒
293	if eq_bv … (bv_zero …) b then
294	Instruction (CLR ? ACC_A)
295	else
296	Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DATA b〉))))))
297	]
298	]
299	\| CALL f _ _ ⇒
300	match f with
301	[ inl id ⇒
302	! id' ← Identifier_of_ident … id ;
303	return Call (toASM_ident ? id')
304	\| inr _ ⇒
305	return Instruction (JMP … ACC_DPTR)
306	]
307	\| COST_LABEL lbl ⇒
308	!_ report_cost … lbl ;
309	return Cost lbl
310	\| COND _ lbl ⇒
311	! l ← Identifier_of_label … lbl;
312	return Instruction (JNZ ? l)
313	]
314	\| FCOND _ _ lbl_true lbl_false ⇒
315	! l1 ← Identifier_of_label … lbl_true;
316	! l2 ← Identifier_of_label … lbl_false;
317	return Jnz ACC_A l1 l2
318	].
319	try @I
320	qed.
321
322
323	definition build_translated_statement ≝
324	λglobals.
325	λstatement: lin_statement globals.
326	! stmt ← translate_statements globals (\snd statement) ;
327	match \fst statement with
328	[ Some lbl ⇒
329	! lbl' ← Identifier_of_label … lbl ;
330	return 〈Some ? lbl', stmt〉
331	\| None ⇒
332	return 〈None ?, stmt〉
333	].
334
335	definition translate_code ≝
336	λglobals.
337	λcode: list (lin_statement globals).
338	m_list_map … (build_translated_statement globals) code.
339
340	definition translate_fun_def ≝
341	λglobals,functions.
342	λid_def : ident × (joint_function LIN globals functions).
343	!_ start_funct_translation … id_def ;
344	(* ^ modify current function id ^ *)
345	match \snd id_def with
346	[ Internal int ⇒
347	let code ≝ joint_if_code … int in
348	! id ← Identifier_of_ident … (\fst id_def) ;
349	! code' ← translate_code … code ;
350	match code' with
351	[ nil ⇒ return [〈Some ? id, Instruction (RET ?)〉] (* impossible, but whatever *)
352	\| cons hd tl ⇒
353	match \fst hd with
354	[ None ⇒ return (〈Some ? id, \snd hd〉 :: tl)
355	\| _ ⇒ return (〈Some ? id, Instruction (NOP ?)〉 :: hd :: tl) (* should never happen *)
356	]
357	]
358	\| External _ ⇒ return [ ]
359	].
360
361	record init_mutable : Type[0] ≝
362	{ virtual_dptr : Identifier × Z
363	; actual_dptr : Identifier × Z
364	; built_code : list (list labelled_instruction)
365	; built_preamble : list (Identifier × Word)
366	}.
367
368	definition store_byte_or_Identifier :
369	(Byte ⊎ (word_side × Identifier)) → init_mutable → init_mutable ≝
370	λby,mut.
371	match mut with
372	[ mk_init_mutable virt act acc1 acc2 ⇒
373	let pre ≝
374	if eq_identifier … (\fst virt) (\fst act) then
375	let off ≝ \snd virt - \snd act in
376	if eqZb off OZ then [ ]
377	else if eqZb off 1 then [ 〈None ?, Instruction (INC ? DPTR)〉 ]
378	else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ]
379	else [ 〈None ?, Mov (inl … DPTR) (\fst virt) (bitvector_of_Z … (\snd virt))〉 ] in
380	let post ≝ match by with
381	[ inl by ⇒
382	〈None ?, Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ?
383	〈ACC_A, DATA by〉))))))〉
384	\| inr si_id ⇒
385	〈None ?, Mov (inr ?? 〈ACC_A, \fst si_id〉) (\snd si_id) (bv_zero ?)〉
386	] in
387	mk_init_mutable 〈\fst virt, Zsucc (\snd virt)〉 virt
388	((pre @
389	[ post ;
390	〈None ?, Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))〉 ]) ::
391	acc1)
392	acc2
393	]. @I qed.
394
395
396	definition do_store_init_data :
397	state_monad ASM_universe init_mutable → init_data →
398	state_monad ASM_universe init_mutable ≝
399	λm_mut,data.
400	! mut ← m_mut ;
401	let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in
402	let store_Identifier ≝ λside,id.store_byte_or_Identifier (inr … 〈side, id〉) in
403	match data with
404	[ Init_int8 n ⇒
405	return store_byte n mut
406	\| Init_int16 n ⇒
407	let 〈by0, by1〉 ≝ vsplit ? 8 8 n in
408	return store_byte by1 (store_byte by0 mut)
409	\| Init_int32 n ⇒
410	let 〈by0, n〉 ≝ vsplit ? 8 24 n in
411	let 〈by1, n〉 ≝ vsplit ? 8 16 n in
412	let 〈by2, by3〉 ≝ vsplit ? 8 8 n in
413	return store_byte by3 (store_byte by2 (store_byte by1 (store_byte by0 mut)))
414	\| Init_addrof symb ofs ⇒
415	! id ← Identifier_of_ident … symb ;
416	return store_Identifier HIGH id (store_Identifier LOW id mut)
417	\| Init_space n ⇒
418	let 〈virt_id, virt_off〉 ≝ virtual_dptr mut in
419	return mk_init_mutable 〈virt_id, n + virt_off〉 (actual_dptr mut)
420	(built_code mut) (built_preamble mut)
421	\| Init_null ⇒
422	let z ≝ bv_zero ? in
423	return store_byte z (store_byte z mut)
424	].
425
426	definition do_store_global :
427	state_monad ASM_universe init_mutable →
428	(ident × region × (list init_data)) →
429	state_monad ASM_universe init_mutable ≝
430	λm_mut,id_reg_data.! mut ← m_mut ;
431	let 〈id, reg, data〉 ≝ id_reg_data in
432	! Id ← Identifier_of_ident … id ;
433	let mut ≝ mk_init_mutable 〈Id, OZ〉 (actual_dptr … mut) (built_code mut)
434	(〈Id, bitvector_of_nat … (size_init_data_list … data)〉 :: built_preamble mut) in
435	foldl … do_store_init_data (return mut) data.
436
437	let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝
438	match l with
439	[ nil ⇒ acc
440	\| cons hd tl ⇒ reversed_flatten_aux … (hd @ acc) tl
441	].
442
443	definition translate_premain : ∀p : lin_program.Identifier →
444	state_monad ASM_universe (list labelled_instruction × (list (Identifier × Word))) ≝
445	λp : lin_program.λexit_label.
446	! main ← Identifier_of_ident … (prog_main … p) ;
447	! u ← state_get … ;
448	(* setting this as actual_dptr will force loading of the correct dptr *)
449	let dummy_dptr : Identifier × Z ≝ 〈an_identifier … one, -1〉 in
450	let mut ≝ mk_init_mutable dummy_dptr dummy_dptr [ ] [ ] in
451	! globals_init ← foldl … do_store_global (return mut) (prog_vars … p) ;
452	let 〈sph, spl〉 ≝ vsplit … 8 8 (bitvector_of_Z … (-(S (globals_stacksize … p)))) in
453	let init_isp ≝
454	(* initial stack pointer set to 2Fh in order to use addressable bits *)
455	DATA (zero 2 @@ [[true;false]] @@ maximum 4) in
456	let isp_direct ≝
457	(* 81h = 10000001b *)
458	DIRECT (true ::: bv_zero 6 @@ [[ true ]]) in
459	let reg_spl ≝ REGISTER [[ true ; true ; false ]] (* RegisterSPL = Register06 *) in
460	let reg_sph ≝ REGISTER [[ true ; true ; true ]] (* RegisterSPH = Register07 *) in
461	return 〈[
462	〈None ?, Cost (init_cost_label … p)〉 ;
463	(* initialize the internal stack pointer past the addressable bits *)
464	〈None ?, Instruction
465	(MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
466	〈isp_direct, init_isp〉)))))〉 ;
467	(* initialize our stack pointer past the globals *)
468	〈None ?, Instruction
469	(MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
470	〈reg_spl, DATA spl〉))))))〉 ;
471	〈None ?, Instruction
472	(MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ?
473	〈reg_sph, DATA sph〉))))))〉 ] @
474	reversed_flatten_aux … [ ] (built_code globals_init) @
475	[ 〈None ?, Call main〉 ;
476	〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ;
477	〈None ?, Jmp exit_label〉], built_preamble globals_init〉. @I qed.
478
479	definition get_symboltable :
480	state_monad ASM_universe (list (Identifier × ident)) ≝
481	λu.
482	let imap ≝ ident_map … u in
483	let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
484	〈u, foldi ??? f imap [ ]〉.
485
486	definition lin_to_asm : lin_program → option pseudo_assembly_program ≝
487	λp.
488	state_run ?? (new_ASM_universe p)
489	(let add_translation ≝
490	λacc,id_def.
491	! code ← translate_fun_def … id_def ;
492	! acc ← acc ;
493	return (code @ acc) in
494	! exit_label ← ASM_fresh … ;
495	! code ← foldl … add_translation (return [ ]) (prog_funct … p) ;
496	! symboltable ← get_symboltable … ;
497	! 〈init, preamble〉 ← translate_premain p exit_label;
498	return
499	(
500	let code ≝
501	init @ code in
502	! code_ok ← code_size_opt code ;
503	(* atm no data identifier is used in the code, so preamble must be empty *)
504	return
505	(mk_pseudo_assembly_program preamble code code_ok symboltable exit_label ? ?))).
506	cases daemon
507	qed.

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

Download in other formats:

Original Format