source: driver/extracted/measurable.mli @ 3106

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 8.8 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
103open Stacksize
104
105type classified_system = { cs_exec : (IO.io_out, IO.io_in)
106                                     SmallstepExec.fullexec; cs_global : 
107                           __; cs_labelled : (__ -> Bool.bool);
108                           cs_classify : (__ ->
109                                         StructuredTraces.status_class);
110                           cs_callee : (__ -> __ -> AST.ident) }
111
112val classified_system_rect_Type4 :
113  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
114  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
115  classified_system -> 'a1
116
117val classified_system_rect_Type5 :
118  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
119  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
120  classified_system -> 'a1
121
122val classified_system_rect_Type3 :
123  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
124  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
125  classified_system -> 'a1
126
127val classified_system_rect_Type2 :
128  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
129  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
130  classified_system -> 'a1
131
132val classified_system_rect_Type1 :
133  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
134  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
135  classified_system -> 'a1
136
137val classified_system_rect_Type0 :
138  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ -> (__ -> Bool.bool) ->
139  (__ -> StructuredTraces.status_class) -> (__ -> __ -> AST.ident) -> 'a1) ->
140  classified_system -> 'a1
141
142val cs_exec :
143  classified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
144
145val cs_global : classified_system -> __
146
147val cs_labelled : classified_system -> __ -> Bool.bool
148
149val cs_classify : classified_system -> __ -> StructuredTraces.status_class
150
151val cs_callee0 : classified_system -> __ -> AST.ident
152
153val classified_system_inv_rect_Type4 :
154  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
155  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
156  AST.ident) -> __ -> 'a1) -> 'a1
157
158val classified_system_inv_rect_Type3 :
159  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
160  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
161  AST.ident) -> __ -> 'a1) -> 'a1
162
163val classified_system_inv_rect_Type2 :
164  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
165  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
166  AST.ident) -> __ -> 'a1) -> 'a1
167
168val classified_system_inv_rect_Type1 :
169  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
170  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
171  AST.ident) -> __ -> 'a1) -> 'a1
172
173val classified_system_inv_rect_Type0 :
174  classified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> __ ->
175  (__ -> Bool.bool) -> (__ -> StructuredTraces.status_class) -> (__ -> __ ->
176  AST.ident) -> __ -> 'a1) -> 'a1
177
178val cs_exec__o__es1 :
179  classified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
180
181type cs_state = __
182
183val intensional_event_of_event :
184  Events.event -> StructuredTraces.intensional_event List.list
185
186val intensional_events_of_events :
187  Events.trace -> StructuredTraces.intensional_event List.list
188
189val intensional_state_change :
190  classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
191  StructuredTraces.intensional_event List.list) Types.prod
192
193val intensional_trace_of_trace :
194  classified_system -> AST.ident List.list -> (cs_state, Events.trace)
195  Types.prod List.list -> (AST.ident List.list,
196  StructuredTraces.intensional_event List.list) Types.prod
197
198val normal_state : classified_system -> cs_state -> Bool.bool
199
200val measure_stack :
201  (AST.ident -> Nat.nat Types.option) -> Stacksize.stacksize_info ->
202  StructuredTraces.intensional_event List.list -> Stacksize.stacksize_info
203
204val will_return_aux :
205  classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
206  List.list -> Bool.bool
207
208val will_return' :
209  classified_system -> (cs_state, Events.trace) Types.prod List.list ->
210  Bool.bool
211
212type preclassified_system = { pcs_exec : (IO.io_out, IO.io_in)
213                                         SmallstepExec.fullexec;
214                              pcs_labelled : (__ -> __ -> Bool.bool);
215                              pcs_classify : (__ -> __ ->
216                                             StructuredTraces.status_class);
217                              pcs_callee : (__ -> __ -> __ -> AST.ident) }
218
219val preclassified_system_rect_Type4 :
220  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
221  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
222  AST.ident) -> 'a1) -> preclassified_system -> 'a1
223
224val preclassified_system_rect_Type5 :
225  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
226  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
227  AST.ident) -> 'a1) -> preclassified_system -> 'a1
228
229val preclassified_system_rect_Type3 :
230  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
231  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
232  AST.ident) -> 'a1) -> preclassified_system -> 'a1
233
234val preclassified_system_rect_Type2 :
235  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
236  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
237  AST.ident) -> 'a1) -> preclassified_system -> 'a1
238
239val preclassified_system_rect_Type1 :
240  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
241  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
242  AST.ident) -> 'a1) -> preclassified_system -> 'a1
243
244val preclassified_system_rect_Type0 :
245  ((IO.io_out, IO.io_in) SmallstepExec.fullexec -> (__ -> __ -> Bool.bool) ->
246  (__ -> __ -> StructuredTraces.status_class) -> (__ -> __ -> __ ->
247  AST.ident) -> 'a1) -> preclassified_system -> 'a1
248
249val pcs_exec :
250  preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
251
252val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool
253
254val pcs_classify :
255  preclassified_system -> __ -> __ -> StructuredTraces.status_class
256
257val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident
258
259val preclassified_system_inv_rect_Type4 :
260  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
261  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
262  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
263
264val preclassified_system_inv_rect_Type3 :
265  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
266  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
267  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
268
269val preclassified_system_inv_rect_Type2 :
270  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
271  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
272  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
273
274val preclassified_system_inv_rect_Type1 :
275  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
276  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
277  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
278
279val preclassified_system_inv_rect_Type0 :
280  preclassified_system -> ((IO.io_out, IO.io_in) SmallstepExec.fullexec ->
281  (__ -> __ -> Bool.bool) -> (__ -> __ -> StructuredTraces.status_class) ->
282  (__ -> __ -> __ -> AST.ident) -> __ -> 'a1) -> 'a1
283
284val pcs_exec__o__es1 :
285  preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
286
287val pcs_to_cs : preclassified_system -> __ -> classified_system
288
289val observables :
290  preclassified_system -> __ -> Nat.nat -> Nat.nat ->
291  (StructuredTraces.intensional_event List.list,
292  StructuredTraces.intensional_event List.list) Types.prod Errors.res
293
294val observe_all_in_measurable :
295  Nat.nat -> classified_system -> (StructuredTraces.intensional_event ->
296  Types.unit0) -> AST.ident List.list -> __ ->
297  (StructuredTraces.intensional_event List.list, Integers.int Errors.res)
298  Types.prod
299
Note: See TracBrowser for help on using the repository browser.