Changeset 2762 for src/compiler.ma
- Timestamp:
- Mar 2, 2013, 2:37:43 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/compiler.ma
r2754 r2762 52 52 definition assembler : pseudo_assembly_program → res labelled_object_code ≝ 53 53 λp. 54 let 〈preamble, list_instr〉 ≝ p in 55 ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); 56 let p' ≝ 〈preamble, list_instr〉 in 57 ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p'); 54 (* ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); *) 55 ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p); 58 56 let sigma ≝ λppc. \fst sigma_pol ppc in 59 57 let pol ≝ λppc. \snd sigma_pol ppc in 60 58 OK ? (assembly p sigma pol). 61 (* % [1: @list_instr_ok | cases daemon] *)cases daemon59 cases daemon 62 60 qed. 63 61 … … 90 88 ∀clight, code_memory, lbls. 91 89 let abstat ≝ ASM_abstract_status code_memory lbls in 92 (* (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → *)93 90 as_cost_map abstat → clight_cost_map clight ≝ 94 λclight,code_memory,lbls, (*dec,*)k,asm_cost_map.91 λclight,code_memory,lbls,k,asm_cost_map. 95 92 lift_sigma_map_id … 0 (* labels not present in out code get 0 *) 96 (strong_decidable_in_codomain …) (* (* dec *) now eliminated as a hypothesis *) 97 k asm_cost_map. 93 (strong_decidable_in_codomain …) k asm_cost_map. 98 94 99 95 include "ASM/ASMCostsSplit.ma". … … 105 101 let p ≝ back_end p in 106 102 ! p ← assembler p; 107 let k ≝ ASM_cost_map p ? in 108 let k' ≝ lift_cost_map_back_to_front 109 p' 110 (load_code_memory (\fst p)) 111 (\fst (\snd p)) 112 k 113 in 103 let k ≝ ASM_cost_map p in 104 let k' ≝ 105 lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in 114 106 return 〈p, ❬p', k'❭〉. 115 cases daemon116 qed.
Note: See TracChangeset
for help on using the changeset viewer.