source: extracted/measurable.mli @ 2890

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

More code extracted, used to debug the compiler.

File size: 8.7 KB
Line 
1open Preamble
2
3open IO
4
5open CostLabel
6
7open PositiveMap
8
9open Deqsets
10
11open Lists
12
13open Identifiers
14
15open AST
16
17open Division
18
19open Z
20
21open BitVectorZ
22
23open Pointers
24
25open Coqlib
26
27open Values
28
29open Events
30
31open Exp
32
33open Arithmetic
34
35open Vector
36
37open FoldStuff
38
39open BitVector
40
41open Extranat
42
43open Integers
44
45open Proper
46
47open ErrorMessages
48
49open Option
50
51open Setoids
52
53open Monad
54
55open Positive
56
57open PreIdentifiers
58
59open Errors
60
61open IOMonad
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open Util
70
71open Bool
72
73open Relations
74
75open Nat
76
77open List
78
79open Hints_declaration
80
81open Core_notation
82
83open Pts
84
85open Logic
86
87open Types
88
89open Extralib
90
91open SmallstepExec
92
93open Executions
94
95open Hide
96
97open Sets
98
99open Listb
100
101open StructuredTraces
102
103type classified_system = { cs_exec : (IO.io_out, IO.io_in)
104                                     SmallstepExec.fullexec; cs_global : 
105                           __; cs_labelled : (__ -> Bool.bool);
106                           cs_classify : (__ ->
107                                         StructuredTraces.status_class);
108                           cs_callee : (__ -> __ -> AST.ident) }
109
110val classified_system_rect_Type4 :
111  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
112  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
113  classified_system -> 'a1
114
115val classified_system_rect_Type5 :
116  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
117  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
118  classified_system -> 'a1
119
120val classified_system_rect_Type3 :
121  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
122  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
123  classified_system -> 'a1
124
125val classified_system_rect_Type2 :
126  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
127  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
128  classified_system -> 'a1
129
130val classified_system_rect_Type1 :
131  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
132  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
133  classified_system -> 'a1
134
135val classified_system_rect_Type0 :
136  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
137  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
138  classified_system -> 'a1
139
140val cs_exec :
141  classified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
142
143val cs_global : classified_system -> __
144
145val cs_labelled : classified_system -> __ -> Bool.bool
146
147val cs_classify : classified_system -> __ -> StructuredTraces.status_class
148
149val cs_callee0 : classified_system -> __ -> AST.ident
150
151val classified_system_inv_rect_Type4 :
152  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
153  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
154  AST.ident) -> __ -> 'a1) -> 'a1
155
156val classified_system_inv_rect_Type3 :
157  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
158  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
159  AST.ident) -> __ -> 'a1) -> 'a1
160
161val classified_system_inv_rect_Type2 :
162  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
163  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
164  AST.ident) -> __ -> 'a1) -> 'a1
165
166val classified_system_inv_rect_Type1 :
167  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
168  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
169  AST.ident) -> __ -> 'a1) -> 'a1
170
171val classified_system_inv_rect_Type0 :
172  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
173  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
174  AST.ident) -> __ -> 'a1) -> 'a1
175
176val cs_exec__o__es1 :
177  classified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
178
179type cs_state = __
180
181val intensional_event_of_event :
182  Events.event -> StructuredTraces.intensional_event List.list
183
184val intensional_events_of_events :
185  Events.trace -> StructuredTraces.intensional_event List.list
186
187val intensional_trace_of_trace :
188  classified_system -> AST.ident List.list -> (cs_state, Events.trace)
189  Types.prod List.list -> (AST.ident List.list,
190  StructuredTraces.intensional_event List.list) Types.prod
191
192val normal_state : classified_system -> cs_state -> Bool.bool
193
194val measure_stack :
195  (AST.ident -> Nat.nat) -> Nat.nat -> StructuredTraces.intensional_event
196  List.list -> (Nat.nat, Nat.nat) Types.prod
197
198val max_stack :
199  (AST.ident -> Nat.nat) -> Nat.nat -> StructuredTraces.intensional_event
200  List.list -> Nat.nat
201
202val will_return_aux :
203  classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
204  List.list -> Bool.bool
205
206val will_return' :
207  classified_system -> (cs_state, Events.trace) Types.prod List.list ->
208  Bool.bool
209
210type preclassified_system = { pcs_exec : (IO.io_out, IO.io_in)
211                                         SmallstepExec.fullexec;
212                              pcs_labelled : (__ -> __ -> Bool.bool);
213                              pcs_classify : (__ -> __ ->
214                                             StructuredTraces.status_class);
215                              pcs_callee : (__ -> __ -> __ -> AST.ident) }
216
217val preclassified_system_rect_Type4 :
218  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
219  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
220  AST.ident) -> 'a1) -> preclassified_system -> 'a1
221
222val preclassified_system_rect_Type5 :
223  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
224  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
225  AST.ident) -> 'a1) -> preclassified_system -> 'a1
226
227val preclassified_system_rect_Type3 :
228  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
229  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
230  AST.ident) -> 'a1) -> preclassified_system -> 'a1
231
232val preclassified_system_rect_Type2 :
233  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
234  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
235  AST.ident) -> 'a1) -> preclassified_system -> 'a1
236
237val preclassified_system_rect_Type1 :
238  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
239  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
240  AST.ident) -> 'a1) -> preclassified_system -> 'a1
241
242val preclassified_system_rect_Type0 :
243  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
244  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
245  AST.ident) -> 'a1) -> preclassified_system -> 'a1
246
247val pcs_exec :
248  preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
249
250val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool
251
252val pcs_classify :
253  preclassified_system -> __ -> __ -> StructuredTraces.status_class
254
255val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident
256
257val preclassified_system_inv_rect_Type4 :
258  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
259  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
260  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
261
262val preclassified_system_inv_rect_Type3 :
263  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
264  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
265  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
266
267val preclassified_system_inv_rect_Type2 :
268  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
269  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
270  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
271
272val preclassified_system_inv_rect_Type1 :
273  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
274  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
275  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
276
277val preclassified_system_inv_rect_Type0 :
278  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
279  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
280  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
281
282val pcs_exec__o__es1 :
283  preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
284
285val pcs_to_cs : preclassified_system -> __ -> classified_system
286
287val observables :
288  preclassified_system -> __ -> Nat.nat -> Nat.nat ->
289  (StructuredTraces.intensional_event List.list,
290  StructuredTraces.intensional_event List.list) Types.prod Errors.res
291
292val observe_all_in_measurable :
293  Nat.nat -> classified_system -> (StructuredTraces.intensional_event ->
294  Types.unit0) -> AST.ident List.list -> __ ->
295  (StructuredTraces.intensional_event List.list, Integers.int Errors.res)
296  Types.prod
297
Note: See TracBrowser for help on using the repository browser.