source: extracted/measurable.mli @ 2903

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

Extracted again.

File size: 8.9 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_state_change :
188  classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
189  StructuredTraces.intensional_event List.list) Types.prod
190
191val intensional_trace_of_trace :
192  classified_system -> AST.ident List.list -> (cs_state, Events.trace)
193  Types.prod List.list -> (AST.ident List.list,
194  StructuredTraces.intensional_event List.list) Types.prod
195
196val normal_state : classified_system -> cs_state -> Bool.bool
197
198val measure_stack :
199  (AST.ident -> Nat.nat) -> Nat.nat -> StructuredTraces.intensional_event
200  List.list -> (Nat.nat, Nat.nat) Types.prod
201
202val max_stack :
203  (AST.ident -> Nat.nat) -> Nat.nat -> StructuredTraces.intensional_event
204  List.list -> Nat.nat
205
206val will_return_aux :
207  classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
208  List.list -> Bool.bool
209
210val will_return' :
211  classified_system -> (cs_state, Events.trace) Types.prod List.list ->
212  Bool.bool
213
214type preclassified_system = { pcs_exec : (IO.io_out, IO.io_in)
215                                         SmallstepExec.fullexec;
216                              pcs_labelled : (__ -> __ -> Bool.bool);
217                              pcs_classify : (__ -> __ ->
218                                             StructuredTraces.status_class);
219                              pcs_callee : (__ -> __ -> __ -> AST.ident) }
220
221val preclassified_system_rect_Type4 :
222  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
223  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
224  AST.ident) -> 'a1) -> preclassified_system -> 'a1
225
226val preclassified_system_rect_Type5 :
227  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
228  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
229  AST.ident) -> 'a1) -> preclassified_system -> 'a1
230
231val preclassified_system_rect_Type3 :
232  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
233  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
234  AST.ident) -> 'a1) -> preclassified_system -> 'a1
235
236val preclassified_system_rect_Type2 :
237  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
238  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
239  AST.ident) -> 'a1) -> preclassified_system -> 'a1
240
241val preclassified_system_rect_Type1 :
242  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
243  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
244  AST.ident) -> 'a1) -> preclassified_system -> 'a1
245
246val preclassified_system_rect_Type0 :
247  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
248  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
249  AST.ident) -> 'a1) -> preclassified_system -> 'a1
250
251val pcs_exec :
252  preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
253
254val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool
255
256val pcs_classify :
257  preclassified_system -> __ -> __ -> StructuredTraces.status_class
258
259val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident
260
261val preclassified_system_inv_rect_Type4 :
262  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
263  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
264  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
265
266val preclassified_system_inv_rect_Type3 :
267  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
268  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
269  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
270
271val preclassified_system_inv_rect_Type2 :
272  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
273  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
274  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
275
276val preclassified_system_inv_rect_Type1 :
277  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
278  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
279  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
280
281val preclassified_system_inv_rect_Type0 :
282  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
283  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
284  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
285
286val pcs_exec__o__es1 :
287  preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
288
289val pcs_to_cs : preclassified_system -> __ -> classified_system
290
291val observables :
292  preclassified_system -> __ -> Nat.nat -> Nat.nat ->
293  (StructuredTraces.intensional_event List.list,
294  StructuredTraces.intensional_event List.list) Types.prod Errors.res
295
296val observe_all_in_measurable :
297  Nat.nat -> classified_system -> (StructuredTraces.intensional_event ->
298  Types.unit0) -> AST.ident List.list -> __ ->
299  (StructuredTraces.intensional_event List.list, Integers.int Errors.res)
300  Types.prod
301
Note: See TracBrowser for help on using the repository browser.