Changeset 3021 for src/compiler.ma


Ignore:
Timestamp:
Mar 28, 2013, 7:11:09 PM (8 years ago)
Author:
campbell
Message:

Replace clight_clock_after with a more sensible definition that uses
an intensional trace. Also drop the proof argument for the clight cost
map to avoid proving that costs come from the clight program - it doesn't
seem to give us much of a benefit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r3018 r3021  
    128128include "ASM/ASMCosts.ma".
    129129
     130definition lift_out_of_sigma :
     131  ∀A,B : Type[0].∀P_out : A → Prop.B →
     132    (∀a.P_out a + ¬ P_out a) →
     133  ((Σa.P_out a) → B) → A → B ≝ λA,B,P_out,dflt,dec,m,a_sig.
     134   match dec a_sig with
     135   [ inl prf ⇒ m «a_sig, prf»
     136   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
     137   ].
     138
    130139definition lift_cost_map_back_to_front :
    131   ∀clight, oc.
     140  ∀oc.
    132141    let abstat ≝ OC_abstract_status oc in
    133   as_cost_map abstat → clight_cost_map clight
    134   λclight,oc,k,asm_cost_map.
    135   lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    136     (strong_decidable_in_codomain …) k asm_cost_map.
     142  as_cost_map abstat → clight_cost_map
     143  λoc,asm_cost_map.
     144  lift_out_of_sigma … 0 (* labels not present in out code get 0 *)
     145    (strong_decidable_in_codomain …) asm_cost_map.
    137146
    138147(* Cost model computation *)
     
    144153 ; c_max_stack: nat
    145154 ; c_labelled_clight: clight_program
    146  ; c_clight_cost_map: clight_cost_map c_labelled_clight
     155 ; c_clight_cost_map: clight_cost_map
    147156 }.
    148157
     
    154163  let k ≝ ASM_cost_map p in
    155164  let k' ≝
    156    lift_cost_map_back_to_front p' p k in
     165   lift_cost_map_back_to_front p k in
    157166  return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracChangeset for help on using the changeset viewer.