1 | include "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, [ ]〉 |
---|
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 | |
---|
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 ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?) |
---|
24 | cases (fresh_regs pars0 globals def m) normalize nodelta |
---|
25 | #def' #regs #EQ change in EQ with (|regs| = m) <EQ |
---|
26 | change with |
---|
27 | (|let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ?| = ?) |
---|
28 | cases (fresh … (joint_if_runiverse … def')) normalize // ] |
---|
29 | qed. |
---|
30 | |
---|
31 | definition fresh_regs_strong: |
---|
32 | ∀pars0,globals. joint_internal_function … (rtl_ertl_params pars0 globals) → |
---|
33 | ∀n: nat. Σregs: (joint_internal_function … (rtl_ertl_params pars0 globals)) × (list register). |\snd regs| = n ≝ |
---|
34 | λpars0,globals,def,n.fresh_regs pars0 globals def n. // |
---|
35 | qed. |
---|
36 | |
---|
37 | definition fresh_label ≝ |
---|
38 | λglobals,params. λdef: joint_internal_function globals params. |
---|
39 | fresh LabelTag (joint_if_luniverse … def). |
---|
40 | |
---|
41 | definition change_label ≝ |
---|
42 | λpars1,globals.λe: joint_statement (graph_params pars1 globals) globals.λl. |
---|
43 | match e with |
---|
44 | [ joint_st_goto _ ⇒ joint_st_goto … l |
---|
45 | | joint_st_return ⇒ joint_st_return ?? |
---|
46 | | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr l]. |
---|
47 | |
---|
48 | (*CSC: bad programming habit: the code below puts everywhere a fake |
---|
49 | label and then adds_graph fixes them *) |
---|
50 | (*CSC: this is just an instance of add_translates below! *) |
---|
51 | let rec adds_graph |
---|
52 | (pars1: params1) (globals: list ident) |
---|
53 | (stmt_list: list (joint_statement (graph_params_ pars1) globals)) |
---|
54 | (start_lbl: label) (dest_lbl: label) |
---|
55 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
56 | on stmt_list ≝ |
---|
57 | match stmt_list with |
---|
58 | [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def |
---|
59 | | cons stmt stmt_list ⇒ |
---|
60 | match stmt_list with |
---|
61 | [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def |
---|
62 | | _ ⇒ |
---|
63 | let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in |
---|
64 | let stmt ≝ change_label … stmt tmp_lbl in |
---|
65 | let def ≝ add_graph … start_lbl stmt def in |
---|
66 | adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]]. |
---|
67 | |
---|
68 | (*CSC: bad programming habit: the code below puts everywhere a fake |
---|
69 | label and then adds_graph fixes them *) |
---|
70 | let rec add_translates |
---|
71 | (pars1: params1) (globals: list ident) |
---|
72 | (translate_list: list ?) (start_lbl: label) (dest_lbl: label) |
---|
73 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
74 | on translate_list ≝ |
---|
75 | match translate_list with |
---|
76 | [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def |
---|
77 | | cons trans translate_list ⇒ |
---|
78 | match translate_list with |
---|
79 | [ nil ⇒ trans start_lbl dest_lbl def |
---|
80 | | _ ⇒ |
---|
81 | let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in |
---|
82 | let def ≝ trans start_lbl tmp_lbl def in |
---|
83 | add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. |
---|