source: src/joint/TranslateUtils.ma @ 2125

Last change on this file since 2125 was 1995, checked in by campbell, 8 years ago

Overall compiler definition; bits and pieces to
make everything happy(ish).

File size: 2.5 KB
Line 
1include "joint/Joint.ma".
2
3definition 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
9let 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, [ ]〉
12  | 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 
18lemma 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 // ]
25qed.
26
27definition 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. //
31qed.
32
33definition 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
39let rec add_translates
40  (pars1: params1) (globals: list ident)
41  (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
42  (def: joint_internal_function … (graph_params pars1 globals))
43    on translate_list ≝
44  match translate_list with
45  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
46  | cons trans translate_list ⇒
47    match translate_list with
48    [ nil ⇒ trans start_lbl dest_lbl def
49    | _ ⇒
50      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
51      let def ≝ trans start_lbl tmp_lbl def in
52        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
53
54definition adds_graph ≝
55 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
56  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
Note: See TracBrowser for help on using the repository browser.