source: src/joint/TranslateUtils.ma @ 2562

Last change on this file since 2562 was 2557, checked in by tranquil, 8 years ago

minor modification of commented (for now) proof of correctness of adds_graph

File size: 12.1 KB
Line 
1include "joint/Joint.ma".
2include "joint/blocks.ma".
3include "utilities/hide.ma".
4include "utilities/deqsets.ma".
5
6(* general type of functions generating fresh things *)
7definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
8
9include alias "basics/lists/list.ma".
10let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
11  on n :
12  freshT pars globals (Σl : list A. |l| = n) ≝
13  match n  return λx.freshT … (Σl.|l| = x) with
14  [ O ⇒ return «[ ], ?»
15  | S n' ⇒
16    ! regs' ← repeat_fresh … fresh n';
17    ! reg ← fresh ;
18    return «reg::regs',?»
19  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
20
21definition fresh_label:
22 ∀g_pars,globals.freshT globals g_pars label ≝
23  λg_pars,globals,def.
24    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
25     〈set_luniverse … def luniverse, r〉.
26
27(* insert into a graph a block of instructions *)
28let rec adds_graph_list
29  (g_pars: graph_params)
30  (globals: list ident)
31  (insts: list (joint_seq g_pars globals))
32  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
33  match insts with
34  [ nil ⇒ return src
35  | cons instr others ⇒
36    ! mid ← fresh_label … ;
37    ! def ← state_get … ;
38    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
39    adds_graph_list g_pars globals others mid
40  ].
41
42definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
43  [ inl _ ⇒ true
44  | inr _ ⇒ false
45  ].
46definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
47  [ inl _ ⇒ true
48  | inr _ ⇒ false
49  ].
50
51definition adds_graph :
52  ∀g_pars : graph_params.
53  ∀globals: list ident.
54  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
55       seq_block g_pars globals (joint_fin_step g_pars).
56  label → if is_inl … b then label else unit →
57  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
58  λg_pars,globals,insts,src.
59  match insts return λx.if is_inl … x then ? else ? → ? → ? with
60  [ inl b ⇒ λdst,def.
61    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
62    add_graph … mid (sequential … (\snd b) dst) def
63  | inr b ⇒ λdst,def.
64    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
65    add_graph … mid (final … (\snd b)) def
66  ].
67
68(* ignoring register allocation for now *)
69
70definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
71λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
72
73lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
74#tag #A * #l * #m whd in ⊢ (%→?%);
75elim (lookup tag ???)
76[ * #ABS elim (ABS ?) %
77| #a #_ %
78] qed.
79
80lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
81#tag #A * #l * #m whd in ⊢ (?%→%);
82elim (lookup tag ???)
83[ * | #a * % #ABS destruct(ABS) ] qed.
84
85(*
86lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
87  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
88  〈id, u'〉 = fresh tag u →
89  ¬id ∈ l.
90#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
91[ #hd_fresh #tl_fresh #EQfresh
92  whd in ⊢ (?(?%));
93  change with (eq_identifier ???) in match (?==?);
94  >eq_identifier_sym
95  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
96  normalize nodelta @(IH … tl_fresh EQfresh)
97| #_ %
98]
99qed.
100*)
101
102lemma fresh_was_fresh : ∀tag,id,id',u,u'.
103〈id,u'〉 = fresh tag u →
104fresh_for_univ tag id' u' →
105id' ≠ id →
106fresh_for_univ tag id' u.
107#tag * #id * #id' * #u * #u'
108normalize #EQfresh destruct
109#H #NEQ
110elim (le_to_or_lt_eq … H)
111[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
112#H >(succ_injective … H) in NEQ;
113* #G elim (G (refl …))
114qed.
115
116(* use Russell? *)
117axiom adds_graph_list_ok :
118  ∀g_pars,globals,b,src,def.
119  fresh_for_univ … src (joint_if_luniverse … def) →
120  luniverse_ok ?? def →
121  let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
122  luniverse_ok ?? def' ∧
123  ∃l.bool_to_Prop (uniqueb … l) ∧
124     All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
125                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
126     src ~❨b,l❩~> dst in joint_if_code … def'.
127(*
128#p #g #l elim l -l
129[ #src #def #_ #Hdef whd
130  %{Hdef} %{[ ]} %%% ]
131#hd #tl #IH #src #def #src_fresh #Hdef
132whd in match (adds_graph_list ?????);
133whd in match (fresh_label ???);
134@(pair_elim … (fresh ??)) normalize nodelta
135#mid #luniverse' #EQfresh
136whd in ⊢ (match % with [ _ ⇒ ?]);
137letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
138cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
139  [ % ] #EQ_aux
140  lapply (IH mid def' ??)
141  [ #l whd in match def'; #Hpres
142    lapply (present_to_memb … Hpres) -Hpres
143    >mem_set_add @eq_identifier_elim
144    [ #EQ destruct(EQ) *
145    | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
146      #l_in
147    ]
148    @(fresh_remains_fresh … (sym_eq … EQfresh))
149    [2: @Hdef @memb_to_present ] assumption
150  | whd in match def';
151    cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
152    whd in match (set_luniverse ????);
153    @(fresh_is_fresh … (sym_eq … EQfresh))
154  ]
155  elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
156  * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
157  % [ % ]
158  [ whd in ⊢ (?%);
159    cut (Not (bool_to_Prop (mid∈l)))
160    [ % #H elim (All_memb … Hl2 H)
161      whd in match (joint_if_luniverse ???);
162      #G #_ @(absurd ?? G)
163      @ (fresh_is_fresh … (sym_eq … EQfresh))
164    | #H >H assumption
165    ]
166  | %
167    [ %
168      [
169      normalize #H10 #H11
170     
171    >(All_fresh_not_memb … (sym_eq … EQfresh))
172    [ assumption ]
173    @(All_mp … Hl2) #lbl *
174    cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
175    normalize #EQfresh #H #lbl_not_mid
176    lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
177   
178    elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
179    [ normalize
180*)
181
182(* preserves first statement if a cost label (should be an invariant) *)
183definition insert_prologue ≝
184  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
185  λdef : joint_internal_function g_pars globals.
186  let entry ≝ joint_if_entry … def in
187  match stmt_at … entry
188  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
189  with
190  [ Some s ⇒ λ_.
191    match s with
192    [ sequential s' next ⇒
193      match s' with
194      [ step_seq s'' ⇒
195        match s'' with
196        [ COST_LABEL _ ⇒
197          adds_graph ?? (inl … (s'' :: insts)) entry next def
198        | _ ⇒
199          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
200          add_graph … tmp s def'
201        ]
202      | _ ⇒
203        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
204        add_graph … tmp s def'
205      ]
206    | _ ⇒
207      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
208      add_graph … tmp s def'
209    ]
210  | None ⇒ Ⓧ
211  ] (pi2 … entry).
212
213definition insert_epilogue ≝
214  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
215  λdef : joint_internal_function g_pars globals.
216  let exit ≝ joint_if_exit … def in
217  match stmt_at … exit
218  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
219  with
220  [ Some s ⇒ λ_.
221    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
222    let def'' ≝ add_graph … tmp s def' in
223    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
224  | None ⇒ Ⓧ
225  ] (pi2 … exit).
226whd in match def''; >graph_code_has_point //
227qed.
228
229definition b_adds_graph :
230  ∀g_pars: graph_params.
231  ∀globals: list ident.
232  (* fresh register creation *)
233  freshT g_pars globals (localsT … g_pars) →
234  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
235       bind_seq_block g_pars globals (joint_fin_step g_pars).
236  label → if is_inl … b then label else unit →
237  joint_internal_function g_pars globals→
238  joint_internal_function g_pars globals ≝
239  λg_pars,globals,fresh_r,insts,src.
240  match insts return λx.if is_inl … x then ? else ? → ? → ? with
241  [ inl b ⇒ λdst,def.
242    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
243    adds_graph … (inl … stmts) src dst def
244  | inr b ⇒ λdst,def.
245    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
246    adds_graph … (inr … stmts) src dst def
247  ].
248
249 
250
251(* translation with inline fresh register allocation *)
252definition b_graph_translate :
253  ∀src_g_pars,dst_g_pars : graph_params.
254  ∀globals: list ident.
255  (* fresh register creation *)
256  freshT dst_g_pars globals (localsT dst_g_pars) →
257  (* initialized function definition with empty graph *)
258  joint_internal_function dst_g_pars globals →
259  (* functions dictating the translation *)
260  (label → joint_step src_g_pars globals →
261    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
262  (label → joint_fin_step src_g_pars →
263    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
264  (* source function *)
265  joint_internal_function src_g_pars globals →
266  (* destination function *)
267  joint_internal_function dst_g_pars globals ≝
268  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
269  let f : label → joint_statement (src_g_pars : params) globals →
270    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
271    λlbl,stmt,def.
272    match stmt with
273    [ sequential inst next ⇒
274      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
275    | final inst ⇒
276      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
277    | FCOND abs _ _ _ ⇒ Ⓧabs
278    ] in
279  foldi … f (joint_if_code … def) empty.
280
281(* translation without register allocation *)
282definition graph_translate :
283  ∀src_g_pars,dst_g_pars : graph_params.
284  ∀globals: list ident.
285  (* initialized function definition with empty graph *)
286  joint_internal_function dst_g_pars globals →
287  (* functions dictating the translation *)
288  (label → joint_step src_g_pars globals →
289    seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
290  (label → joint_fin_step src_g_pars →
291    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
292  (* source function *)
293  joint_internal_function src_g_pars globals →
294  (* destination function *)
295  joint_internal_function dst_g_pars globals ≝
296  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
297  let f : label → joint_statement (src_g_pars : params) globals →
298    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
299    λlbl,stmt,def.
300    match stmt with
301    [ sequential inst next ⇒
302      adds_graph … (inl … (trans_step lbl inst)) lbl next def
303    | final inst ⇒
304      adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
305    | FCOND abs _ _ _ ⇒ Ⓧabs
306    ] in
307  foldi … f (joint_if_code … def) empty.
308
309definition init_graph_if ≝
310  λg_pars : graph_params.λglobals.
311  λluniverse,runiverse,ret,params,locals,stack_size,entry,exit.
312  let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
313  let graph ≝ add ? ? graph exit (RETURN …) in
314  mk_joint_internal_function g_pars globals
315    luniverse runiverse ret params locals stack_size
316    graph entry exit.
317>graph_code_has_point @map_mem_prop
318[@graph_add_lookup] @graph_add
319qed.
320
321
322(*
323let rec add_translates
324  (pars1: params1) (globals: list ident)
325  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
326  (def: joint_internal_function … (graph_params pars1 globals))
327    on translate_list ≝
328  match translate_list with
329  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
330  | cons trans translate_list ⇒
331    match translate_list with
332    [ nil ⇒ trans start_lbl dest_lbl def
333    | _ ⇒
334      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
335      let def ≝ trans start_lbl tmp_lbl def in
336        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
337
338definition adds_graph ≝
339 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
340  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
341  *)
Note: See TracBrowser for help on using the repository browser.