source: src/joint/TranslateUtils.ma @ 1280

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

Some progress in the porting of RTLAbstoRTL to the joint syntax:

1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are

probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.

File size: 3.6 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  λglobals,params. λdef: joint_internal_function globals params.
39    fresh LabelTag (joint_if_luniverse … def).
40
41definition 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! *)
51let 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 *)
70let 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]].
Note: See TracBrowser for help on using the repository browser.