Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r1995 r2286  
    11include "joint/Joint.ma".
    2 
    3 definition fresh_reg:
    4  ∀pars0,globals. joint_internal_function … (rtl_ertl_params pars0 globals) → (joint_internal_function … (rtl_ertl_params pars0 globals)) × register ≝
    5   λpars0,globals,def.
    6     let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    7      〈set_locals ?? (set_runiverse ?? def runiverse) (r::joint_if_locals ?? def), r〉.
    8 
    9 let rec fresh_regs (pars0:?) (globals: list ident) (def: joint_internal_function … (rtl_ertl_params pars0 globals)) (n: nat) on n ≝
    10   match n with
    11   [ O ⇒ 〈def, [ ]〉
     2include "joint/blocks.ma".
     3include "utilities/hide.ma".
     4
     5(* general type of functions generating fresh things *)
     6definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
     7
     8include alias "basics/lists/list.ma".
     9let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
     10  on n :
     11  freshT pars globals (Σl : list A. |l| = n) ≝
     12  match n  return λx.freshT … (Σl.|l| = x) with
     13  [ O ⇒ return «[ ], ?»
    1214  | S n' ⇒
    13     let 〈def', regs'〉 ≝ fresh_regs pars0 globals def n' in
    14     let 〈def', reg〉 ≝ fresh_reg … def' in
    15       〈def', reg :: regs'〉
    16   ].
    17  
    18 lemma fresh_regs_length:
    19  ∀pars0,globals.∀def: joint_internal_function … (rtl_ertl_params pars0 globals). ∀n: nat.
    20   |(\snd (fresh_regs … def n))| = n.
    21  #pars0 #globals #def #n elim n
    22   [ %
    23   | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
    24     #def' #regs #EQ >EQ cases (fresh_reg ???)  normalize // ]
     15    ! regs' ← repeat_fresh … fresh n';
     16    ! reg ← fresh ;
     17    return «reg::regs',?»
     18  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
     19
     20definition fresh_label:
     21 ∀g_pars,globals.freshT globals g_pars label ≝
     22  λg_pars,globals,def.
     23    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
     24     〈set_luniverse … def luniverse, r〉.
     25
     26(* insert into a graph a block of instructions *)
     27let rec adds_graph_list
     28  (g_pars: graph_params)
     29  (globals: list ident)
     30  (insts: list (joint_seq g_pars globals))
     31  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
     32  match insts with
     33  [ nil ⇒ return src
     34  | cons instr others ⇒
     35    ! mid ← fresh_label … ;
     36    ! def ← state_get … ;
     37    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
     38    adds_graph_list g_pars globals others mid
     39  ].
     40
     41definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     42  [ inl _ ⇒ true
     43  | inr _ ⇒ false
     44  ].
     45definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     46  [ inl _ ⇒ true
     47  | inr _ ⇒ false
     48  ].
     49
     50definition adds_graph :
     51  ∀g_pars : graph_params.
     52  ∀globals: list ident.
     53  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
     54       seq_block g_pars globals (joint_fin_step g_pars).
     55  label → if is_inl … b then label else unit →
     56  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
     57  λg_pars,globals,insts,src.
     58  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     59  [ inl b ⇒ λdst,def.
     60    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     61    add_graph … mid (sequential … (\snd b) dst) def
     62  | inr b ⇒ λdst,def.
     63    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     64    add_graph … mid (final … (\snd b)) def
     65  ].
     66
     67(* preserves first statement if a cost label (should be an invariant) *)
     68definition insert_prologue ≝
     69  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     70  λdef : joint_internal_function g_pars globals.
     71  let entry ≝ joint_if_entry … def in
     72  match stmt_at … entry
     73  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
     74  with
     75  [ Some s ⇒ λ_.
     76    match s with
     77    [ sequential s' next ⇒
     78      match s' with
     79      [ step_seq s'' ⇒
     80        match s'' with
     81        [ COST_LABEL _ ⇒
     82          adds_graph ?? (inl … (s'' :: insts)) entry next def
     83        | _ ⇒
     84          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     85          add_graph … tmp s def'
     86        ]
     87      | _ ⇒
     88        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     89        add_graph … tmp s def'
     90      ]
     91    | _ ⇒
     92      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     93      add_graph … tmp s def'
     94    ]
     95  | None ⇒ Ⓧ
     96  ] (pi2 … entry).
     97
     98definition insert_epilogue ≝
     99  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     100  λdef : joint_internal_function g_pars globals.
     101  let exit ≝ joint_if_exit … def in
     102  match stmt_at … exit
     103  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
     104  with
     105  [ Some s ⇒ λ_.
     106    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
     107    let def'' ≝ add_graph … tmp s def' in
     108    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
     109  | None ⇒ Ⓧ
     110  ] (pi2 … exit).
     111whd in match def''; >graph_code_has_point //
    25112qed.
    26113
    27 definition fresh_regs_strong:
    28  ∀pars0,globals. joint_internal_function … (rtl_ertl_params pars0 globals) →
    29   ∀n: nat. Σregs: (joint_internal_function … (rtl_ertl_params pars0 globals)) × (list register). |\snd regs| = n ≝
    30  λpars0,globals,def,n.fresh_regs pars0 globals def n. //
     114definition b_adds_graph :
     115  ∀g_pars: graph_params.
     116  ∀globals: list ident.
     117  (* fresh register creation *)
     118  freshT g_pars globals (localsT … g_pars) →
     119  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
     120       bind_seq_block g_pars globals (joint_fin_step g_pars).
     121  label → if is_inl … b then label else unit →
     122  joint_internal_function g_pars globals→
     123  joint_internal_function g_pars globals ≝
     124  λg_pars,globals,fresh_r,insts,src.
     125  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     126  [ inl b ⇒ λdst,def.
     127    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     128    adds_graph … (inl … stmts) src dst def
     129  | inr b ⇒ λdst,def.
     130    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     131    adds_graph … (inr … stmts) src dst def
     132  ].
     133
     134(* translation with inline fresh register allocation *)
     135definition b_graph_translate :
     136  ∀src_g_pars,dst_g_pars : graph_params.
     137  ∀globals: list ident.
     138  (* fresh register creation *)
     139  freshT dst_g_pars globals (localsT dst_g_pars) →
     140  (* initialized function definition with empty graph *)
     141  joint_internal_function dst_g_pars globals →
     142  (* functions dictating the translation *)
     143  (label → joint_step src_g_pars globals →
     144    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
     145  (label → joint_fin_step src_g_pars →
     146    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
     147  (* source function *)
     148  joint_internal_function src_g_pars globals →
     149  (* destination function *)
     150  joint_internal_function dst_g_pars globals ≝
     151  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
     152  let f : label → joint_statement (src_g_pars : params) globals →
     153    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     154    λlbl,stmt,def.
     155    match stmt with
     156    [ sequential inst next ⇒
     157      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
     158    | final inst ⇒
     159      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
     160    ] in
     161  foldi … f (joint_if_code … def) empty.
     162
     163(* translation without register allocation *)
     164definition graph_translate :
     165  ∀src_g_pars,dst_g_pars : graph_params.
     166  ∀globals: list ident.
     167  (* initialized function definition with empty graph *)
     168  joint_internal_function dst_g_pars globals →
     169  (* functions dictating the translation *)
     170  (label → joint_step src_g_pars globals →
     171    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
     172  (label → joint_fin_step src_g_pars →
     173    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
     174  (* source function *)
     175  joint_internal_function src_g_pars globals →
     176  (* destination function *)
     177  joint_internal_function dst_g_pars globals ≝
     178  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
     179  let f : label → joint_statement (src_g_pars : params) globals →
     180    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     181    λlbl,stmt,def.
     182    match stmt with
     183    [ sequential inst next ⇒
     184      adds_graph … (inl … (trans_step lbl inst)) lbl next def
     185    | final inst ⇒
     186      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
     187    ] in
     188  foldi … f (joint_if_code … def) empty.
     189
     190definition init_graph_if ≝
     191  λg_pars : graph_params.λglobals.
     192  λluniverse,runiverse,ret,params,locals,stack_size,entry,exit.
     193  let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
     194  let graph ≝ add ? ? graph exit (RETURN …) in
     195  mk_joint_internal_function g_pars globals
     196    luniverse runiverse ret params locals stack_size
     197    graph entry exit.
     198>graph_code_has_point @map_mem_prop
     199[@graph_add_lookup] @graph_add
    31200qed.
    32201
    33 definition fresh_label:
    34  ∀pars0,globals. joint_internal_function … (graph_params pars0 globals) → label × (joint_internal_function … (graph_params pars0 globals)) ≝
    35   λpars0,globals,def.
    36     let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
    37      〈r,set_luniverse … def luniverse〉.
    38 
     202
     203(*
    39204let rec add_translates
    40205  (pars1: params1) (globals: list ident)
     
    55220 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
    56221  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
     222  *)
Note: See TracChangeset for help on using the changeset viewer.