Changeset 2508 for src/compiler.ma


Ignore:
Timestamp:
Nov 29, 2012, 8:12:34 PM (8 years ago)
Author:
mckinna
Message:

more tweaks. compiler and correctness still build.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2505 r2508  
    6666  λclight,code_memory,lbls,dec,k,asm_cost_map.
    6767  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    68     dec k asm_cost_map
    69   (*
    70    match dec asm_cost_map with
    71    [ inl prf ⇒ k «l_sig, prf»
    72    | inr _ ⇒ 0 (* labels not present in out code get 0 *)
    73    ]*).
     68    dec k asm_cost_map.
    7469
    7570include "ASM/ASMCostsSplit.ma".
    7671
    7772definition compile : clight_program →
    78   res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) (*(Σl.in_clight_program labelled l) → ℕ*)
     73  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled))
    7974λp.
    8075  ! 〈init_cost,p',p〉 ← front_end p;
Note: See TracChangeset for help on using the changeset viewer.