Changeset 2319 for src/Cminor


Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (7 years ago)
Author:
campbell
Message:

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

Location:
src/Cminor
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2252 r2319  
    7777] qed.
    7878
    79 definition add_statement : ident → (Σs:stmt. stmt_inv s) →
     79(* FIXME: we need to add a new initialisation function instead of augmenting
     80   main, because this currently breaks a recursive main function. *)
     81
     82definition add_statement : costlabel → ident → (Σs:stmt. stmt_inv s) →
    8083                              list (ident × (fundef internal_function)) →
    8184                              list (ident × (fundef internal_function)) ≝
    82 λid,s. match s with [ mk_Sig s H ⇒
     85λcost,id,s. match s with [ mk_Sig s H ⇒
    8386  map ??
    8487    (λidf.
     
    9396                                           (f_distinct f)
    9497                                           (f_stacksize f)
    95                                            (St_seq s (f_body f))
     98                                           (St_cost cost (St_seq s (f_body f)))
    9699                                           ?)〉
    97100          | External f ⇒ 〈id, External ? f〉 (* Error ? *)
     
    101104[ % //
    102105| %
    103   [ @(stmt_P_mp … H) #s * * #V #L #R %
     106 [ % //
     107 | % [ @(stmt_P_mp … H) #s * * #V #L #R %
    104108    [ @(stmt_vars_mp … V) #i #t *
    105109    | @(stmt_labels_mp … L) #l *
     
    108112  | whd in match (labels_of ?); >(no_labels … H) @(f_inv f)
    109113  ]
     114 ]
    110115] qed.
    111116
     
    115120              size_init_data_list (\snd v)〉).
    116121
    117 definition replace_init : Cminor_program → Cminor_noinit_program ≝
    118 λp.
     122definition replace_init : costlabel → Cminor_program → Cminor_noinit_program ≝
     123λcost,p.
    119124  mk_program ??
    120125    (empty_vars (prog_vars ?? p))
    121     (add_statement (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
     126    (add_statement cost (prog_main ?? p) (init_vars (prog_vars ?? p)) (prog_funct ?? p))
    122127    (prog_main ?? p).
  • src/Cminor/toRTLabs.ma

    r2292 r2319  
    937937include "Cminor/initialisation.ma".
    938938
    939 definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝
    940 λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
     939definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝
     940λinit_cost,p. let p' ≝ replace_init init_cost p in cminor_noinit_to_rtlabs p'.
Note: See TracChangeset for help on using the changeset viewer.