source: src/joint/TranslateUtils.ma @ 1352

Last change on this file since 1352 was 1352, checked in by sacerdot, 9 years ago

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

File size: 2.7 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 ⊢ (? → ??(??%)?) 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 // ]
29qed.
30
31definition 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. //
35qed.
36
37definition 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〉.
42
43let 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
49  [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
50  | cons trans translate_list ⇒
51    match translate_list with
52    [ nil ⇒ trans start_lbl dest_lbl def
53    | _ ⇒
54      let 〈tmp_lbl, def〉 ≝ fresh_label … def in
55      let def ≝ trans start_lbl tmp_lbl def in
56        add_translates pars1 globals translate_list tmp_lbl dest_lbl def]].
57
58definition adds_graph ≝
59 λpars1:params1.λglobals. λstmt_list: list (label → joint_statement (graph_params_ pars1) globals).
60  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.