Changeset 2907 for src/compiler.ma


Ignore:
Timestamp:
Mar 19, 2013, 7:48:19 PM (8 years ago)
Author:
sacerdot
Message:
  1. a few bugs fixed
  2. as_return implemented for ASM & OC
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2899 r2907  
    135135
    136136definition lift_cost_map_back_to_front :
    137   ∀clight, code_memory, lbls.
    138     let abstat ≝ OC_abstract_status code_memory lbls in
     137  ∀clight, oc.
     138    let abstat ≝ OC_abstract_status oc in
    139139  as_cost_map abstat → clight_cost_map clight ≝
    140   λclight,code_memory,lbls,k,asm_cost_map.
     140  λclight,oc,k,asm_cost_map.
    141141  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    142142    (strong_decidable_in_codomain …) k asm_cost_map.
     
    160160  let k ≝ ASM_cost_map p in
    161161  let k' ≝
    162    lift_cost_map_back_to_front p' (load_code_memory (oc p)) (costlabels p) k in
     162   lift_cost_map_back_to_front p' p k in
    163163  return mk_compiler_output p stack_cost max_stack p' k'.
Note: See TracChangeset for help on using the changeset viewer.