source: src/joint/TranslateUtils_paolo.ma @ 2214

Last change on this file since 2214 was 2214, checked in by tranquil, 9 years ago
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File size: 8.6 KB
Line 
1include "joint/Joint_paolo.ma".
2include "joint/blocks.ma".
3
4(* general type of functions generating fresh things *)
5(* type T is the syntactic type of the generated things *)
6(* (sig for RTLabs registers, unit in others ) *)
7definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g).
8
9definition rtl_ertl_fresh_reg:
10 ∀inst_pars,funct_pars,globals.
11  freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝
12  λinst_pars,var_pars,globals,def.
13    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
14    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
15
16include alias "basics/lists/list.ma".
17let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
18  freshT globals (rtl_ertl_params inst_pars funct_pars)
19    (Σl : list register. |l| = n) ≝
20  let ret_type ≝ (Σl : list register. |l| = n) in
21  match n  return λx.x = n → freshT … ret_type with
22  [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
23  | S n' ⇒ λeq'.
24    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
25    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
26    return (mk_Sig … (reg :: regs') ?)
27  ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
28  qed.
29
30definition fresh_label:
31 ∀g_pars,globals.freshT globals g_pars label ≝
32  λg_pars,globals,def.
33    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
34     〈set_luniverse … def luniverse, r〉.
35
36(* insert into a graph a block of instructions *)
37let rec adds_graph_list
38  (g_pars: graph_params)
39  (globals: list ident)
40  (insts: list (joint_seq g_pars globals))
41  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
42  match insts with
43  [ nil ⇒ return src
44  | cons instr others ⇒
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
49  ].
50
51definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
52  [ inl _ ⇒ true
53  | inr _ ⇒ false
54  ].
55definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
56  [ inl _ ⇒ true
57  | inr _ ⇒ false
58  ].
59
60definition adds_graph :
61  ∀g_pars : graph_params.
62  ∀globals: list ident.
63  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
64       seq_block g_pars globals (joint_fin_step g_pars).
65  label → if is_inl … b then label else unit →
66  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
67  λg_pars,globals,insts,src.
68  match insts return λx.if is_inl … x then ? else ? → ? → ? with
69  [ inl b ⇒ λdst,def.
70    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
71    add_graph … mid (sequential … (\snd b) dst) def
72  | inr b ⇒ λdst,def.
73    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
74    add_graph … mid (final … (\snd b)) def
75  ].
76
77(* preserves first statement if a cost label (should be an invariant) *)
78definition insert_prologue ≝
79  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
80  λdef : joint_internal_function g_pars globals.
81  let entry ≝ joint_if_entry … def in
82  match stmt_at … entry
83  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
84  with
85  [ Some s ⇒ λ_.
86    match s with
87    [ sequential s' next ⇒
88      match s' with
89      [ step_seq s'' ⇒
90        match s'' with
91        [ COST_LABEL _ ⇒
92          adds_graph ?? (inl … (s'' :: insts)) entry next def
93        | _ ⇒
94          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
95          add_graph … tmp s def'
96        ]
97      | _ ⇒
98        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
99        add_graph … tmp s def'
100      ]
101    | _ ⇒
102      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
103      add_graph … tmp s def'
104    ]
105  | None ⇒ Ⓧ
106  ] (pi2 … entry).
107
108definition insert_epilogue ≝
109  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
110  λdef : joint_internal_function g_pars globals.
111  let exit ≝ joint_if_exit … def in
112  match stmt_at … exit
113  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
114  with
115  [ Some s ⇒ λ_.
116    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
117    let def'' ≝ add_graph … tmp s def' in
118    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
119  | None ⇒ Ⓧ
120  ] (pi2 … exit).
121whd in match def''; >graph_code_has_point //
122qed.
123
124definition b_adds_graph :
125  ∀g_pars: graph_params.
126  ∀globals: list ident.
127  (* fresh register creation *)
128  freshT globals g_pars (localsT … g_pars) →
129  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
130       bind_seq_block g_pars globals (joint_fin_step g_pars).
131  label → if is_inl … b then label else unit →
132  joint_internal_function g_pars globals→
133  joint_internal_function g_pars globals ≝
134  λg_pars,globals,fresh_r,insts,src.
135  match insts return λx.if is_inl … x then ? else ? → ? → ? with
136  [ inl b ⇒ λdst,def.
137    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
138    adds_graph … (inl … stmts) src dst def
139  | inr b ⇒ λdst,def.
140    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
141    adds_graph … (inr … stmts) src dst def
142  ].
143
144(* translation with inline fresh register allocation *)
145definition b_graph_translate :
146  ∀src_g_pars,dst_g_pars : graph_params.
147  ∀globals: list ident.
148  (* fresh register creation *)
149  freshT globals dst_g_pars (localsT dst_g_pars) →
150  (* initialized function definition with empty graph *)
151  joint_internal_function dst_g_pars globals →
152  (* functions dictating the translation *)
153  (label → joint_step src_g_pars globals →
154    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
155  (label → joint_fin_step src_g_pars →
156    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
157  (* source function *)
158  joint_internal_function src_g_pars globals →
159  (* destination function *)
160  joint_internal_function dst_g_pars globals ≝
161  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
162  let f : label → joint_statement (src_g_pars : params) globals →
163    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
164    λlbl,stmt,def.
165    match stmt with
166    [ sequential inst next ⇒
167      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
168    | final inst ⇒
169      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
170    ] in
171  foldi … f (joint_if_code … def) empty.
172
173(* translation without register allocation *)
174definition graph_translate :
175  ∀src_g_pars,dst_g_pars : graph_params.
176  ∀globals: list ident.
177  (* initialized function definition with empty graph *)
178  joint_internal_function dst_g_pars globals →
179  (* functions dictating the translation *)
180  (label → joint_step src_g_pars globals →
181    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
182  (label → joint_fin_step src_g_pars →
183    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
184  (* source function *)
185  joint_internal_function src_g_pars globals →
186  (* destination function *)
187  joint_internal_function dst_g_pars globals ≝
188  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
189  let f : label → joint_statement (src_g_pars : params) globals →
190    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
191    λlbl,stmt,def.
192    match stmt with
193    [ sequential inst next ⇒
194      adds_graph … (inl … (trans_step lbl inst)) lbl next def
195    | final inst ⇒
196      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
197    ] in
198  foldi … f (joint_if_code … def) empty.
199
200(*
201let rec add_translates
202  (pars1: params1) (globals: list ident)
203  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
204  (def: joint_internal_function … (graph_params pars1 globals))
205    on translate_list ≝
206  match translate_list with
207  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
208  | cons trans translate_list ⇒
209    match translate_list with
210    [ nil ⇒ trans start_lbl dest_lbl def
211    | _ ⇒
212      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
213      let def ≝ trans start_lbl tmp_lbl def in
214        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
215
216definition adds_graph ≝
217 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
218  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
219  *)
Note: See TracBrowser for help on using the repository browser.