source: extracted/interference.mli @ 2746

Last change on this file since 2746 was 2740, checked in by sacerdot, 7 years ago

Graph colouring terminated up to Uses that will be implemented
in Matita.

File size: 4.3 KB
Line 
1open Preamble
2
3open Fixpoints
4
5open Set_adt
6
7open String
8
9open Sets
10
11open Listb
12
13open LabelledObjects
14
15open Graphs
16
17open I8051
18
19open Order
20
21open Registers
22
23open BitVectorTrie
24
25open CostLabel
26
27open Hide
28
29open Proper
30
31open PositiveMap
32
33open Deqsets
34
35open ErrorMessages
36
37open PreIdentifiers
38
39open Errors
40
41open Extralib
42
43open Setoids
44
45open Monad
46
47open Option
48
49open Lists
50
51open Identifiers
52
53open Integers
54
55open AST
56
57open Division
58
59open Exp
60
61open Arithmetic
62
63open Extranat
64
65open Vector
66
67open FoldStuff
68
69open BitVector
70
71open Positive
72
73open Z
74
75open BitVectorZ
76
77open Pointers
78
79open ByteValues
80
81open BackEndOps
82
83open Joint
84
85open ERTL
86
87open ERTLptr
88
89open Div_and_mod
90
91open Jmeq
92
93open Russell
94
95open Bool
96
97open Relations
98
99open Nat
100
101open Hints_declaration
102
103open Core_notation
104
105open Pts
106
107open Logic
108
109open Types
110
111open List
112
113open Util
114
115open Liveness
116
117type decision =
118| Decision_spill of Nat.nat
119| Decision_colour of I8051.register
120
121val decision_rect_Type4 :
122  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
123
124val decision_rect_Type5 :
125  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
126
127val decision_rect_Type3 :
128  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
129
130val decision_rect_Type2 :
131  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
132
133val decision_rect_Type1 :
134  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
135
136val decision_rect_Type0 :
137  (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
138
139val decision_inv_rect_Type4 :
140  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
141
142val decision_inv_rect_Type3 :
143  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
144
145val decision_inv_rect_Type2 :
146  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
147
148val decision_inv_rect_Type1 :
149  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
150
151val decision_inv_rect_Type0 :
152  decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
153
154val decision_discr : decision -> decision -> __
155
156val decision_jmdiscr : decision -> decision -> __
157
158type coloured_graph = { colouring : (Liveness.vertex -> decision);
159                        spilled_no : Nat.nat }
160
161val coloured_graph_rect_Type4 :
162  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
163  __ -> 'a1) -> coloured_graph -> 'a1
164
165val coloured_graph_rect_Type5 :
166  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
167  __ -> 'a1) -> coloured_graph -> 'a1
168
169val coloured_graph_rect_Type3 :
170  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
171  __ -> 'a1) -> coloured_graph -> 'a1
172
173val coloured_graph_rect_Type2 :
174  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
175  __ -> 'a1) -> coloured_graph -> 'a1
176
177val coloured_graph_rect_Type1 :
178  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
179  __ -> 'a1) -> coloured_graph -> 'a1
180
181val coloured_graph_rect_Type0 :
182  Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
183  __ -> 'a1) -> coloured_graph -> 'a1
184
185val colouring :
186  Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision
187
188val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat
189
190val coloured_graph_inv_rect_Type4 :
191  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
192  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
193
194val coloured_graph_inv_rect_Type3 :
195  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
196  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
197
198val coloured_graph_inv_rect_Type2 :
199  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
200  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
201
202val coloured_graph_inv_rect_Type1 :
203  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
204  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
205
206val coloured_graph_inv_rect_Type0 :
207  Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
208  Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
209
210val coloured_graph_discr :
211  Fixpoints.valuation -> coloured_graph -> coloured_graph -> __
212
213val coloured_graph_jmdiscr :
214  Fixpoints.valuation -> coloured_graph -> coloured_graph -> __
215
216type coloured_graph_computer =
217  AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
218  -> coloured_graph
219
Note: See TracBrowser for help on using the repository browser.