source: src/ERTL/Uses.ma @ 745

Last change on this file since 745 was 745, checked in by mulligan, 10 years ago

Changes from yesterday. Slowly implementing the functorized imperative code from ERTL :(

File size: 6.2 KB
Line 
1include "ERTL/ERTL.ma".
2include "utilities/BitVectorTrieSet.ma".
3include "ASM/Arithmetic.ma".
4include "ASM/I8051.ma".
5
6definition count ≝
7  λregister.
8  λuses.
9    let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
10      insert ? 16 register l uses.
11     
12definition word_of_register: Register → Word ≝
13  λregister.
14    bitvector_of_nat ? (nat_of_register register).
15     
16definition examine_statement ≝
17  λstatement: ERTLStatement.
18  λuses.
19  match statement with
20  [ ERTL_St_Skip _ ⇒ uses
21  | ERTL_St_Comment _ _ ⇒ uses
22  | ERTL_St_Cost _ _ ⇒ uses
23  | ERTL_St_Hdw_To_Hdw _ _ _ ⇒ uses
24  | ERTL_St_NewFrame _ ⇒ uses
25  | ERTL_St_DelFrame _ ⇒ uses
26  | ERTL_St_ClearCarry _ ⇒ uses
27  | ERTL_St_Call_Id _ _ _ ⇒ uses
28  | ERTL_St_Return _ ⇒ uses
29  | ERTL_St_Get_Hdw r _ _ ⇒ count (word_of_register r) uses
30  | ERTL_St_Set_Hdw _ r _ ⇒ count (word_of_register r) uses
31  | ERTL_St_FrameSize ar _ ⇒
32    match ar with [
33      mkAbstractRegister r ⇒
34        (* dpm: shift the abstract registers above the physical registers *)
35        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
36          count offset uses
37    ]
38  | ERTL_St_Pop ar _ ⇒
39    match ar with [
40      mkAbstractRegister r ⇒
41        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
42          count offset uses
43    ]
44  | ERTL_St_Push ar _ ⇒
45    match ar with [
46      mkAbstractRegister r ⇒
47        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
48          count offset uses
49    ]
50  | ERTL_St_Int ar _ _ ⇒
51    match ar with [
52      mkAbstractRegister r ⇒
53        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
54          count offset uses
55    ]
56  | ERTL_St_AddrH ar _ _ ⇒
57    match ar with [
58      mkAbstractRegister r ⇒
59        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
60          count offset uses
61    ]
62  | ERTL_St_AddrL ar _ _ ⇒
63    match ar with [
64      mkAbstractRegister r ⇒
65        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
66          count offset uses
67    ]
68  | ERTL_St_CondAcc ar _ _ ⇒
69    match ar with [
70      mkAbstractRegister r ⇒
71        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
72          count offset uses
73    ]
74  | ERTL_St_Move ar1 ar2 _ ⇒
75    match ar1 with [
76      mkAbstractRegister r1 ⇒
77      match ar2 with [
78        mkAbstractRegister r2 ⇒
79          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
80          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
81            count offset1 (count offset2 uses)
82      ]
83    ]
84  | ERTL_St_Op1 op1 ar1 ar2 _ ⇒
85    match ar1 with [
86      mkAbstractRegister r1 ⇒
87      match ar2 with [
88        mkAbstractRegister r2 ⇒
89          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
90          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
91            count offset1 (count offset2 uses)
92      ]
93    ]
94  | ERTL_St_Op2 op2 ar1 ar2 ar3 _ ⇒
95    match ar1 with [
96      mkAbstractRegister r1 ⇒
97      match ar2 with [
98        mkAbstractRegister r2 ⇒
99        match ar3 with [
100          mkAbstractRegister r3 ⇒
101          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
102          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
103          let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
104            count offset1 (count offset2 (count offset3 uses))
105        ]
106      ]
107    ]
108  | ERTL_St_Opaccs opaccs ar1 ar2 ar3 _ ⇒
109    match ar1 with [
110      mkAbstractRegister r1 ⇒
111      match ar2 with [
112        mkAbstractRegister r2 ⇒
113        match ar3 with [
114          mkAbstractRegister r3 ⇒
115          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
116          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
117          let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
118            count offset1 (count offset2 (count offset3 uses))
119        ]
120      ]
121    ]
122  | ERTL_St_Load ar1 ar2 ar3 _ ⇒
123    match ar1 with [
124      mkAbstractRegister r1 ⇒
125      match ar2 with [
126        mkAbstractRegister r2 ⇒
127        match ar3 with [
128          mkAbstractRegister r3 ⇒
129          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
130          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
131          let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
132            count offset1 (count offset2 (count offset3 uses))
133        ]
134      ]
135    ]
136  | ERTL_St_Store ar1 ar2 ar3 _ ⇒
137    match ar1 with [
138      mkAbstractRegister r1 ⇒
139      match ar2 with [
140        mkAbstractRegister r2 ⇒
141        match ar3 with [
142          mkAbstractRegister r3 ⇒
143          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
144          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
145          let 〈offset3, ignore〉 ≝ add_n_with_carry ? r3 (bitvector_of_nat ? physical_register_count) false ? in
146            count offset1 (count offset2 (count offset3 uses))
147        ]
148      ]
149    ]
150  ].
151  [*: normalize
152      @ le_S @ le_S @ le_S @ le_S @ le_S @ le_S
153      @ le_S @ le_S @ le_S @ le_S @ le_S @ le_n ]
154qed.
155
156(*
157definition examine_internal ≝
158  λint_fun.
159    let uses ≝ foldr ? ? examine_statement (Stub ? ?) (ERTL_IF_Graph int_fun) in
160      lookup uses.
161*)
Note: See TracBrowser for help on using the repository browser.