Changeset 2320


Ignore:
Timestamp:
Sep 3, 2012, 4:33:33 PM (7 years ago)
Author:
campbell
Message:

Update compiler and correctness with labelling changes.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2319 r2320  
    7979  res (object_code × costlabel_map × clight_program × ((Σl.in_clight_program l) → ℕ)) ≝
    8080λp.
    81   ! 〈p',p〉 ← front_end p;
     81  ! 〈init_cost,p',p〉 ← front_end p;
    8282  let p ≝ back_end p in
    8383    ! p ← assembler p;
  • src/correctness.ma

    r2205 r2320  
    2424#object_code #costlabel_map #labelled #cost_map
    2525#COMPILE
    26 cases (bind_inversion ????? COMPILE) -COMPILE * #labelled' #rtlabs_program * #FRONTEND #COMPILE
     26cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE
    2727cases (bind_inversion ????? COMPILE) -COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE
    2828whd in COMPILE:(??%%); destruct
    2929cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND
    30 cases (bind_inversion ????? FRONTEND) -FRONTEND #rtlabs_program' * #RTLABS #FRONTEND
    3130whd in FRONTEND:(??%%); destruct
    3231
Note: See TracChangeset for help on using the changeset viewer.