Changeset 3145 for src/compiler.ma


Ignore:
Timestamp:
Apr 15, 2013, 4:31:50 PM (8 years ago)
Author:
tranquil
Message:
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r3083 r3145  
    8282(* Inefficient, replace with Trie lookup *)
    8383definition lookup_stack_cost ≝
    84  λP,p,id.
    85   assoc_list_lookup ?? id (eq_identifier …) (stack_cost P p).
     84 λP,p.stack_sizes … (stack_cost P p).
    8685
    8786definition back_end :
     
    121120  OK ? p.
    122121
    123 (* Cost lifting *)
    124 include "ASM/ASMCosts.ma".
    125 
    126 definition lift_out_of_sigma :
    127   ∀A,B : Type[0].∀P_out : A → Prop.B →
    128     (∀a.P_out a + ¬ P_out a) →
    129   ((Σa.P_out a) → B) → A → B ≝ λA,B,P_out,dflt,dec,m,a_sig.
    130    match dec a_sig with
    131    [ inl prf ⇒ m «a_sig, prf»
    132    | inr _ ⇒ dflt (* labels not present in out code get 0 *)
    133    ].
    134 
    135 definition lift_cost_map_back_to_front :
    136   ∀oc.
    137     let abstat ≝ OC_abstract_status oc in
    138   as_cost_map abstat → clight_cost_map ≝
    139   λoc,asm_cost_map.
    140   lift_out_of_sigma … 0 (* labels not present in out code get 0 *)
    141     (strong_decidable_in_codomain …) asm_cost_map.
    142 
    143122(* Cost model computation *)
    144123include "ASM/ASMCostsSplit.ma".
     
    160139  ! p ← assembler observe p;
    161140  let k ≝ ASM_cost_map p in
    162   let k' ≝
    163    lift_cost_map_back_to_front p k in
    164   return mk_compiler_output p stack_cost max_stack init_costlabel p' k'.
     141  return mk_compiler_output p stack_cost max_stack init_costlabel p' k.
Note: See TracChangeset for help on using the changeset viewer.