source: src/joint/TranslateUtils.ma @ 2286

Last change on this file since 2286 was 2286, checked in by tranquil, 7 years ago

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 size: 8.4 KB
Line 
1include "joint/Joint.ma".
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 «[ ], ?»
14  | S n' ⇒
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 //
112qed.
113
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
200qed.
201
202
203(*
204let rec add_translates
205  (pars1: params1) (globals: list ident)
206  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
207  (def: joint_internal_function … (graph_params pars1 globals))
208    on translate_list ≝
209  match translate_list with
210  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
211  | cons trans translate_list ⇒
212    match translate_list with
213    [ nil ⇒ trans start_lbl dest_lbl def
214    | _ ⇒
215      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
216      let def ≝ trans start_lbl tmp_lbl def in
217        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
218
219definition adds_graph ≝
220 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
221  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
222  *)
Note: See TracBrowser for help on using the repository browser.