79 open Hints_declaration
101 open StructuredTraces
105 type classified_system = { cs_exec : (IO.io_out, IO.io_in)
106 SmallstepExec.fullexec; cs_global :
107 __; cs_labelled : (__ -> Bool.bool);
109 StructuredTraces.status_class);
110 cs_callee : (__ -> __ -> AST.ident) }
112 val 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
117 val 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
122 val 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
127 val 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
132 val 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
137 val 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
143 classified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
145 val cs_global : classified_system -> __
147 val cs_labelled : classified_system -> __ -> Bool.bool
149 val cs_classify : classified_system -> __ -> StructuredTraces.status_class
151 val cs_callee0 : classified_system -> __ -> AST.ident
153 val 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
158 val 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
163 val 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
168 val 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
173 val 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
178 val cs_exec__o__es1 :
179 classified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
183 val intensional_event_of_event :
184 Events.event -> StructuredTraces.intensional_event List.list
186 val intensional_events_of_events :
187 Events.trace -> StructuredTraces.intensional_event List.list
189 val intensional_state_change :
190 classified_system -> AST.ident List.list -> __ -> (AST.ident List.list,
191 StructuredTraces.intensional_event List.list) Types.prod
193 val 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
198 val normal_state : classified_system -> cs_state -> Bool.bool
201 (AST.ident -> Nat.nat Types.option) -> Stacksize.stacksize_info ->
202 StructuredTraces.intensional_event List.list -> Stacksize.stacksize_info
204 val will_return_aux :
205 classified_system -> Nat.nat -> (cs_state, Events.trace) Types.prod
206 List.list -> Bool.bool
209 classified_system -> (cs_state, Events.trace) Types.prod List.list ->
212 type 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) }
219 val 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
224 val 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
229 val 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
234 val 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
239 val 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
244 val 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
250 preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
252 val pcs_labelled : preclassified_system -> __ -> __ -> Bool.bool
255 preclassified_system -> __ -> __ -> StructuredTraces.status_class
257 val pcs_callee0 : preclassified_system -> __ -> __ -> AST.ident
259 val 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
264 val 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
269 val 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
274 val 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
279 val 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
284 val pcs_exec__o__es1 :
285 preclassified_system -> (IO.io_out, IO.io_in) SmallstepExec.trans_system
287 val pcs_to_cs : preclassified_system -> __ -> classified_system
290 preclassified_system -> __ -> Nat.nat -> Nat.nat ->
291 (StructuredTraces.intensional_event List.list,
292 StructuredTraces.intensional_event List.list) Types.prod Errors.res
294 val 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)