Changeset 2762 for src/compiler.ma

Timestamp:

Mar 2, 2013, 2:37:43 AM (8 years ago)

Author:

sacerdot

Message:

All repaired up to compiler.ma.

Note: one daemon is left for one final property of a pseudo-program
(code < 2^{16). James implemented a check, but the commit was partial.
I will put the property in the record together with the other and, if
James commit the check, use it in the LINToASM pass.}

File:

• src/compiler.ma (modified) (3 diffs)

src/compiler.ma

@@ -52 +52 @@
 definition assembler : pseudo_assembly_program → res labelled_object_code ≝
 λp.
-  let 〈preamble, list_instr〉 ≝ p in
-  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); 
-  let p' ≝ 〈preamble, list_instr〉 in
-  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
+(*  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*); *)
+  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p);
   let sigma ≝ λppc. \fst sigma_pol ppc in
   let pol ≝ λppc. \snd sigma_pol ppc in
   OK ? (assembly p sigma pol).
-  (* % [1: @list_instr_ok | cases daemon] *) cases daemon
+  cases daemon
 qed.
 
@@ -90 +88 @@
   ∀clight, code_memory, lbls.
     let abstat ≝ ASM_abstract_status code_memory lbls in 
-(*   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → *)
   as_cost_map abstat → clight_cost_map clight ≝ 
-  λclight,code_memory,lbls,(*dec,*)k,asm_cost_map.
+  λclight,code_memory,lbls,k,asm_cost_map.
   lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
-    (strong_decidable_in_codomain …) (* (* dec *) now eliminated as a hypothesis *)
-    k asm_cost_map.
+    (strong_decidable_in_codomain …) k asm_cost_map.
 
 include "ASM/ASMCostsSplit.ma". 
@@ -105 +101 @@
   let p ≝ back_end p in
     ! p ← assembler p;
-  let k ≝ ASM_cost_map p ? in
-  let k' ≝ lift_cost_map_back_to_front
-    p'
-    (load_code_memory (\fst p))
-    (\fst (\snd p))
-    k
-    in
+  let k ≝ ASM_cost_map p in
+  let k' ≝
+   lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
   return 〈p, ❬p', k'❭〉.
- cases daemon 
-qed.