source: src/ERTL/Uses.ma @ 746

Last change on this file since 746 was 746, checked in by mulligan, 9 years ago

Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.

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