Ignore:
Timestamp:
Jul 6, 2012, 5:53:01 PM (9 years ago)
Author:
tranquil
Message:
  • yet another correction to joint
  • added functions adding prologues and epilogues in TranslateUtils?. Adding a prologue will preserve the invariant of having a cost label at the start of the function, without needing transformations later
  • redefined ERTL and rewritten RTLToERTL (with suffix "_paolo")
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils_paolo.ma

    r2155 r2162  
    3939  (globals: list ident)
    4040  (insts: list (joint_seq g_pars globals))
    41   (src : label)
    42   (def: joint_internal_function … g_pars) on insts
    43   : (joint_internal_function … g_pars) × label ≝
     41  (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝
    4442  match insts with
    45   [ nil ⇒ 〈def, src〉
     43  [ nil ⇒ return src
    4644  | cons instr others ⇒
    47     let 〈def, mid〉 ≝ fresh_label … def in
    48     let def ≝ add_graph … src (sequential … instr mid) def in
    49     adds_graph_list g_pars globals others mid def
     45    ! mid ← fresh_label … ;
     46    ! def ← state_get … ;
     47    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
     48    adds_graph_list g_pars globals others mid
    5049  ].
    5150
     
    6665    add_graph … mid (final … (\snd b)) def
    6766  ].
     67
     68(* preserves first statement if a cost label (should be an invariant) *)
     69definition insert_prologue ≝
     70  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     71  λdef : joint_internal_function globals g_pars.
     72  let entry ≝ joint_if_entry … def in
     73  match stmt_at … entry
     74  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
     75  with
     76  [ Some s ⇒ λ_.
     77    match s with
     78    [ sequential s' next ⇒
     79      match s' with
     80      [ step_seq s'' ⇒
     81        match s'' with
     82        [ COST_LABEL _ ⇒
     83          adds_graph ?? (inl … (s'' :: insts)) entry next def
     84        | _ ⇒
     85          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     86          add_graph … tmp s def'
     87        ]
     88      | _ ⇒
     89        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     90        add_graph … tmp s def'
     91      ]
     92    | _ ⇒
     93      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     94      add_graph … tmp s def'
     95    ]
     96  | None ⇒ Ⓧ
     97  ] (pi2 … entry).
     98
     99definition insert_epilogue ≝
     100  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     101  λdef : joint_internal_function globals g_pars.
     102  let exit ≝ joint_if_exit … def in
     103  match stmt_at … exit
     104  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
     105  with
     106  [ Some s ⇒ λ_.
     107    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
     108    let def'' ≝ add_graph … tmp s def' in
     109    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
     110  | None ⇒ Ⓧ
     111  ] (pi2 … exit).
     112whd in match def''; >graph_code_has_point //
     113qed.
    68114
    69115definition b_adds_graph :
Note: See TracChangeset for help on using the changeset viewer.