source: src/LIN/LINToASM.ma @ 3370

Last change on this file since 3370 was 3066, checked in by tranquil, 7 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 
1include "utilities/BitVectorTrieSet.ma".
2include "utilities/state.ma".
3
4include "ASM/Util.ma".
5include "ASM/ASM.ma".
6
7include "LIN/LIN.ma".
8
9(* utilities to provide Identifier's and addresses  *)
10record 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
18definition 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
28definition Identifier_of_label :
29  label → state_monad ASM_universe Identifier ≝
30λl,u.
31let current ≝ current_funct … u in
32let lmap ≝ lookup_def … (label_map … u) current (empty_map …) in
33let 〈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
43definition Identifier_of_ident :
44  ident → state_monad ASM_universe Identifier ≝
45λi,u.
46let imap ≝ ident_map … u in
47let 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
53let id ≝ \fst (\fst res) in
54let univ ≝ \snd (\fst res) in
55let imap ≝ \snd res in
56〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
57  (fresh_cost_label … u), id〉.
58
59definition new_ASM_universe :
60∀p : joint_program LIN.ASM_universe ≝
61λp.
62mk_ASM_universe (mk_universe … one)
63  (an_identifier … one (* dummy *))
64  (empty_map …) (empty_map …) one.
65(*@hide_prf normalize nodelta
66cases p -p * #vars #functs #main #cost_init
67#i #H
68normalize nodelta
69letin init_val ≝ (〈empty_map SymbolTag Identifier, mk_universe ASMTag one〉)
70cut (bool_to_Prop (i ∈ \fst init_val) ∨ bool_to_Prop (i ∈ map … (λx.\fst (\fst x)) vars))
71[ %2{H} ] -H
72lapply i -i lapply init_val -init_val
73whd in match prog_var_names; normalize nodelta
74elim 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]
86qed.
87*)
88
89definition 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
96definition 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
102definition 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
120definition vector_cast :
121∀A,n,m.A → Vector A n → Vector A m ≝
122λA,n,m,dflt,v.
123If leb n m then with prf do
124  replicate … (m - n) dflt @@ v ⌈Vector ?? ↦ ?⌉
125else with prf do
126  \snd (vsplit … (v ⌈Vector ?? ↦ Vector ? (n - m + m)⌉)).
127lapply 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
132qed.
133
134definition 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
143qed.
144
145definition lin_statement ≝ λg.labelled_obj LabelTag (joint_statement LIN g).
146
147definition data_of_int ≝ λbv. DATA bv.
148definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
149definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
150
151(* TODO: check and change to free bit *)
152definition asm_other_bit ≝ BIT_ADDR (zero_byte).
153definition one_word : Word ≝ bv_zero 15 @@ [[ true ]].
154
155definition 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
320qed.
321
322
323definition 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
335definition translate_code ≝
336  λglobals.
337  λcode: list (lin_statement globals).
338    m_list_map … (build_translated_statement globals) code.
339
340definition 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
361record 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
368definition store_byte_or_Identifier :
369  (Byte ⊎ (word_side × Identifier)) → init_mutable → init_mutable ≝
370λby,mut.
371match 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
396definition 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 ;
401let store_byte ≝ λby.store_byte_or_Identifier (inl … by) in
402let store_Identifier ≝ λside,id.store_byte_or_Identifier (inr … 〈side, id〉) in
403match 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
426definition 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
437let rec reversed_flatten_aux A acc (l : list (list A)) on l : list A ≝
438match l with
439[ nil ⇒ acc
440| cons hd tl ⇒ reversed_flatten_aux … (hd @ acc) tl
441].
442
443definition 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
479definition 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
486definition 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 ? ?))).
506cases daemon
507qed.
Note: See TracBrowser for help on using the repository browser.