Ignore:
Timestamp:
Jul 6, 2012, 11:25:43 AM (8 years ago)
Author:
tranquil
Message:

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils_paolo.ma

    r1882 r2155  
    11include "joint/Joint_paolo.ma".
    2 include "utilities/bindLists.ma".
     2include "joint/blocks.ma".
    33
    44(* general type of functions generating fresh things *)
     
    3535
    3636(* insert into a graph a block of instructions *)
    37 let rec adds_graph
     37let rec adds_graph_list
    3838  (g_pars: graph_params)
    3939  (globals: list ident)
    40   (insts: list (joint_step g_pars globals))
     40  (insts: list (joint_seq g_pars globals))
    4141  (src : label)
    42   (dest : label)
    43   (def: joint_internal_function … g_pars) on insts
     42  (def: joint_internal_function … g_pars) on insts
     43  : (joint_internal_function … g_pars) × label
    4444  match insts with
    45   [ nil ⇒ add_graph … src (GOTO … dest) def
     45  [ nil ⇒ 〈def, src〉
    4646  | cons instr others ⇒
    47     match others with
    48     [ nil ⇒ (* only one instruction *)
    49       add_graph … src (sequential … instr dest) def
    50     | _ ⇒ (* need to generate label *)
    51       let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    52       adds_graph g_pars globals others tmp_lbl dest
    53         (add_graph … src (sequential … instr tmp_lbl) def)
    54     ]
     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
     50  ].
     51
     52definition adds_graph :
     53  ∀g_pars : graph_params.
     54  ∀globals: list ident.
     55  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
     56       seq_block g_pars globals (joint_fin_step g_pars).
     57  label → if is_inl … b then label else unit →
     58  joint_internal_function … g_pars → joint_internal_function … g_pars ≝
     59  λg_pars,globals,insts,src.
     60  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     61  [ inl b ⇒ λdst,def.
     62    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     63    add_graph … mid (sequential … (\snd b) dst) def
     64  | inr b ⇒ λdst,def.
     65    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     66    add_graph … mid (final … (\snd b)) def
    5567  ].
    5668
     
    6072  (* fresh register creation *)
    6173  freshT globals g_pars (localsT … g_pars) →
    62   ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals).
    63   ∀src : label.
    64   ∀dest : label.
     74  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
     75       bind_seq_block g_pars globals (joint_fin_step g_pars).
     76  label → if is_inl … b then label else unit →
    6577  joint_internal_function globals g_pars →
    6678  joint_internal_function globals g_pars ≝
    67   λg_pars,globals,fresh_r,insts,src,dest,def.
    68   let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in
    69   adds_graph … stmts src dest def'.
     79  λg_pars,globals,fresh_r,insts,src.
     80  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     81  [ inl b ⇒ λdst,def.
     82    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     83    adds_graph … (inl … stmts) src dst def
     84  | inr b ⇒ λdst,def.
     85    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     86    adds_graph … (inr … stmts) src dst def
     87  ].
    7088
    7189(* translation with inline fresh register allocation *)
     
    7593  (* fresh register creation *)
    7694  freshT globals dst_g_pars (localsT dst_g_pars) →
    77   (* function dictating the translation *)
    78   (label → joint_step src_g_pars globals →
    79     bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals)
    80     (* this can be added to allow redirections: × label *)) →
    81   (label → ext_fin_stmt src_g_pars →
    82      bind_new (localsT dst_g_pars)
    83       ((list (joint_step dst_g_pars globals))
    84       ×
    85       (joint_statement dst_g_pars globals))) →
    8695  (* initialized function definition with empty graph *)
    8796  joint_internal_function globals dst_g_pars →
     97  (* functions dictating the translation *)
     98  (label → joint_step src_g_pars globals →
     99    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
     100  (label → joint_fin_step src_g_pars →
     101    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    88102  (* source function *)
    89103  joint_internal_function globals src_g_pars →
    90104  (* destination function *)
    91   joint_internal_function globals dst_g_pars ≝ 
    92   λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def.
     105  joint_internal_function globals dst_g_pars ≝
     106  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
    93107  let f : label → joint_statement (src_g_pars : params) globals →
    94108    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
    95109    λlbl,stmt,def.
    96110    match stmt with
    97     [ sequential inst next ⇒ b_adds_graph … fresh_reg (trans lbl inst) lbl next def
    98     | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    99     | RETURN ⇒ add_graph … lbl (RETURN …) def
    100     | extension_fin c ⇒
    101       let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in
    102       let 〈insts, fin〉 ≝ p in
    103       let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in
    104       adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def)
     111    [ sequential inst next ⇒
     112      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
     113    | final inst ⇒
     114      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
    105115    ] in
    106116  foldi … f (joint_if_code … def) empty.
    107  
     117(* 
    108118(* translation without register allocation *)
    109119definition graph_translate :
     
    137147    ] in
    138148  foldi ??? f (joint_if_code ?? def) empty.
    139 
     149*)
     150(*
    140151definition graph_to_lin_statement :
    141152  ∀p : unserialized_params.∀globals.
    142153  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
    143   λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globals with
     154  λp,globals,stmt.match stmt with
    144155  [ sequential c _ ⇒ sequential … c it
    145   | GOTO l ⇒ GOTO … l
    146   | RETURN ⇒ RETURN …
    147   | extension_fin c ⇒ extension_fin … c
     156  | final c ⇒
     157    final ?? match c return λx.joint_fin_step (mk_lin_params p) globals with
     158    [ GOTO l ⇒ GOTO … l
     159    | RETURN ⇒ RETURN …
     160    | extension_fin c ⇒ extension_fin ?? c
     161    ]
    148162  ].
    149163
     
    152166  stmt_labels … (graph_to_lin_statement p globals s) =
    153167  stmt_explicit_labels … s.
    154 #p#globals * //
     168#p#globals * [//] * //
    155169qed.
    156170
     
    216230(*----------------------------*)⊢
    217231list lo ≡ codeT lp globals.
     232
    218233
    219234definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
     
    791806#f_out * #f_out_closed #H assumption
    792807qed.
    793 
    794  
     808*) 
    795809
    796810     
Note: See TracChangeset for help on using the changeset viewer.