source: extracted/interference.mli @ 3019

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

New extraction after ERTLptr abortion.

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