Changeset 2762 for src/compiler.ma


Ignore:
Timestamp:
Mar 2, 2013, 2:37:43 AM (7 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 < 216). 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2754 r2762  
    5252definition assembler : pseudo_assembly_program → res labelled_object_code ≝
    5353λ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);
    5856  let sigma ≝ λppc. \fst sigma_pol ppc in
    5957  let pol ≝ λppc. \snd sigma_pol ppc in
    6058  OK ? (assembly p sigma pol).
    61   (* % [1: @list_instr_ok | cases daemon] *) cases daemon
     59  cases daemon
    6260qed.
    6361
     
    9088  ∀clight, code_memory, lbls.
    9189    let abstat ≝ ASM_abstract_status code_memory lbls in
    92 (*   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → *)
    9390  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.
    9592  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.
    9894
    9995include "ASM/ASMCostsSplit.ma".
     
    105101  let p ≝ back_end p in
    106102    ! 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
    114106  return 〈p, ❬p', k'❭〉.
    115  cases daemon
    116 qed.
Note: See TracChangeset for help on using the changeset viewer.