[1280] | 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 | |
---|
[1284] | 37 | definition fresh_label: |
---|
| 38 | ∀pars0,globals. joint_internal_function … (graph_params pars0 globals) → label × (joint_internal_function … (graph_params pars0 globals)) ≝ |
---|
| 39 | λpars0,globals,def. |
---|
| 40 | let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in |
---|
| 41 | 〈r,set_luniverse … def luniverse〉. |
---|
[1280] | 42 | |
---|
| 43 | let rec add_translates |
---|
| 44 | (pars1: params1) (globals: list ident) |
---|
| 45 | (translate_list: list ?) (start_lbl: label) (dest_lbl: label) |
---|
| 46 | (def: joint_internal_function … (graph_params pars1 globals)) |
---|
| 47 | on translate_list ≝ |
---|
| 48 | match translate_list with |
---|
[1282] | 49 | [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def |
---|
[1280] | 50 | | cons trans translate_list ⇒ |
---|
| 51 | match translate_list with |
---|
| 52 | [ nil ⇒ trans start_lbl dest_lbl def |
---|
| 53 | | _ ⇒ |
---|
[1284] | 54 | let 〈tmp_lbl, def〉 ≝ fresh_label … def in |
---|
[1280] | 55 | let def ≝ trans start_lbl tmp_lbl def in |
---|
[1284] | 56 | add_translates pars1 globals translate_list tmp_lbl dest_lbl def]]. |
---|
| 57 | |
---|
| 58 | definition adds_graph ≝ |
---|
| 59 | λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals). |
---|
[1352] | 60 | add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list). |
---|