source: extracted/joint_fullexec.mli @ 2829

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

Semantics files committed.

File size: 8.7 KB
Line 
1open Preamble
2
3open StructuredTraces
4
5open ExtraGlobalenvs
6
7open I8051bis
8
9open String
10
11open Sets
12
13open Listb
14
15open LabelledObjects
16
17open BitVectorTrie
18
19open Graphs
20
21open I8051
22
23open Order
24
25open Registers
26
27open BackEndOps
28
29open Joint
30
31open BEMem
32
33open CostLabel
34
35open Events
36
37open IOMonad
38
39open IO
40
41open Extra_bool
42
43open Coqlib
44
45open Values
46
47open FrontEndVal
48
49open Hide
50
51open ByteValues
52
53open Division
54
55open Z
56
57open BitVectorZ
58
59open Pointers
60
61open GenMem
62
63open FrontEndMem
64
65open Proper
66
67open PositiveMap
68
69open Deqsets
70
71open Extralib
72
73open Lists
74
75open Identifiers
76
77open Exp
78
79open Arithmetic
80
81open Vector
82
83open Div_and_mod
84
85open Util
86
87open FoldStuff
88
89open BitVector
90
91open Extranat
92
93open Integers
94
95open AST
96
97open ErrorMessages
98
99open Option
100
101open Setoids
102
103open Monad
104
105open Jmeq
106
107open Russell
108
109open Positive
110
111open PreIdentifiers
112
113open Bool
114
115open Relations
116
117open Nat
118
119open List
120
121open Hints_declaration
122
123open Core_notation
124
125open Pts
126
127open Logic
128
129open Types
130
131open Errors
132
133open Globalenvs
134
135open Joint_semantics
136
137open Traces
138
139open SmallstepExec
140
141open Executions
142
143open Measurable
144
145type joint_global = { jglobals : AST.ident List.list;
146                      jgenv : Joint_semantics.genv }
147
148val joint_global_rect_Type4 :
149  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
150  -> 'a1) -> joint_global -> 'a1
151
152val joint_global_rect_Type5 :
153  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
154  -> 'a1) -> joint_global -> 'a1
155
156val joint_global_rect_Type3 :
157  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
158  -> 'a1) -> joint_global -> 'a1
159
160val joint_global_rect_Type2 :
161  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
162  -> 'a1) -> joint_global -> 'a1
163
164val joint_global_rect_Type1 :
165  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
166  -> 'a1) -> joint_global -> 'a1
167
168val joint_global_rect_Type0 :
169  Joint_semantics.sem_params -> (AST.ident List.list -> Joint_semantics.genv
170  -> 'a1) -> joint_global -> 'a1
171
172val jglobals :
173  Joint_semantics.sem_params -> joint_global -> AST.ident List.list
174
175val jgenv :
176  Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
177
178val joint_global_inv_rect_Type4 :
179  Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
180  Joint_semantics.genv -> __ -> 'a1) -> 'a1
181
182val joint_global_inv_rect_Type3 :
183  Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
184  Joint_semantics.genv -> __ -> 'a1) -> 'a1
185
186val joint_global_inv_rect_Type2 :
187  Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
188  Joint_semantics.genv -> __ -> 'a1) -> 'a1
189
190val joint_global_inv_rect_Type1 :
191  Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
192  Joint_semantics.genv -> __ -> 'a1) -> 'a1
193
194val joint_global_inv_rect_Type0 :
195  Joint_semantics.sem_params -> joint_global -> (AST.ident List.list ->
196  Joint_semantics.genv -> __ -> 'a1) -> 'a1
197
198val joint_global_discr :
199  Joint_semantics.sem_params -> joint_global -> joint_global -> __
200
201val joint_global_jmdiscr :
202  Joint_semantics.sem_params -> joint_global -> joint_global -> __
203
204val dpi1__o__jgenv__o__inject :
205  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
206  Joint_semantics.genv Types.sig0
207
208val dpi1__o__jgenv__o__genv_to_genv_t__o__inject :
209  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
210  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
211  Types.sig0
212
213val dpi1__o__jgenv__o__genv_to_genv_t :
214  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
215  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
216
217val eject__o__jgenv__o__inject :
218  Joint_semantics.sem_params -> joint_global Types.sig0 ->
219  Joint_semantics.genv Types.sig0
220
221val eject__o__jgenv__o__genv_to_genv_t__o__inject :
222  Joint_semantics.sem_params -> joint_global Types.sig0 ->
223  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
224  Types.sig0
225
226val eject__o__jgenv__o__genv_to_genv_t :
227  Joint_semantics.sem_params -> joint_global Types.sig0 ->
228  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
229
230val jgenv__o__genv_to_genv_t :
231  Joint_semantics.sem_params -> joint_global ->
232  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
233
234val jgenv__o__genv_to_genv_t__o__inject :
235  Joint_semantics.sem_params -> joint_global ->
236  Joint.joint_closed_internal_function AST.fundef Globalenvs.genv_t
237  Types.sig0
238
239val jgenv__o__inject :
240  Joint_semantics.sem_params -> joint_global -> Joint_semantics.genv
241  Types.sig0
242
243val dpi1__o__jgenv :
244  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
245  Joint_semantics.genv
246
247val eject__o__jgenv :
248  Joint_semantics.sem_params -> joint_global Types.sig0 ->
249  Joint_semantics.genv
250
251val eval_params_of_global :
252  Joint_semantics.sem_params -> joint_global -> Traces.evaluation_params
253
254val dpi1__o__eval_params_of_global__o__sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
255  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
256  Joint.unserialized_params
257
258val dpi1__o__eval_params_of_global__o__sparams__o__spp__o__stmt_pars__o__uns_pars :
259  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
260  Joint.uns_params
261
262val dpi1__o__eval_params_of_global__o__sparams__o__spp__o__stmt_pars :
263  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
264  Joint.stmt_params
265
266val dpi1__o__eval_params_of_global__o__sparams__o__spp :
267  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
268  Joint.params
269
270val dpi1__o__eval_params_of_global__o__sparams__o__msu_pars__o__st_pars :
271  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
272  Joint_semantics.sem_state_params
273
274val dpi1__o__eval_params_of_global__o__sparams__o__msu_pars :
275  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
276  Joint.joint_closed_internal_function
277  Joint_semantics.sem_unserialized_params
278
279val dpi1__o__eval_params_of_global__o__sparams :
280  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
281  Joint_semantics.sem_params
282
283val eject__o__eval_params_of_global__o__sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
284  Joint_semantics.sem_params -> joint_global Types.sig0 ->
285  Joint.unserialized_params
286
287val eject__o__eval_params_of_global__o__sparams__o__spp__o__stmt_pars__o__uns_pars :
288  Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.uns_params
289
290val eject__o__eval_params_of_global__o__sparams__o__spp__o__stmt_pars :
291  Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.stmt_params
292
293val eject__o__eval_params_of_global__o__sparams__o__spp :
294  Joint_semantics.sem_params -> joint_global Types.sig0 -> Joint.params
295
296val eject__o__eval_params_of_global__o__sparams__o__msu_pars__o__st_pars :
297  Joint_semantics.sem_params -> joint_global Types.sig0 ->
298  Joint_semantics.sem_state_params
299
300val eject__o__eval_params_of_global__o__sparams__o__msu_pars :
301  Joint_semantics.sem_params -> joint_global Types.sig0 ->
302  Joint.joint_closed_internal_function
303  Joint_semantics.sem_unserialized_params
304
305val eject__o__eval_params_of_global__o__sparams :
306  Joint_semantics.sem_params -> joint_global Types.sig0 ->
307  Joint_semantics.sem_params
308
309val eval_params_of_global__o__sparams :
310  Joint_semantics.sem_params -> joint_global -> Joint_semantics.sem_params
311
312val eval_params_of_global__o__sparams__o__msu_pars :
313  Joint_semantics.sem_params -> joint_global ->
314  Joint.joint_closed_internal_function
315  Joint_semantics.sem_unserialized_params
316
317val eval_params_of_global__o__sparams__o__msu_pars__o__st_pars :
318  Joint_semantics.sem_params -> joint_global ->
319  Joint_semantics.sem_state_params
320
321val eval_params_of_global__o__sparams__o__spp :
322  Joint_semantics.sem_params -> joint_global -> Joint.params
323
324val eval_params_of_global__o__sparams__o__spp__o__stmt_pars :
325  Joint_semantics.sem_params -> joint_global -> Joint.stmt_params
326
327val eval_params_of_global__o__sparams__o__spp__o__stmt_pars__o__uns_pars :
328  Joint_semantics.sem_params -> joint_global -> Joint.uns_params
329
330val eval_params_of_global__o__sparams__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
331  Joint_semantics.sem_params -> joint_global -> Joint.unserialized_params
332
333val dpi1__o__eval_params_of_global :
334  Joint_semantics.sem_params -> (joint_global, 'a1) Types.dPair ->
335  Traces.evaluation_params
336
337val eject__o__eval_params_of_global :
338  Joint_semantics.sem_params -> joint_global Types.sig0 ->
339  Traces.evaluation_params
340
341val make_joint_global :
342  Joint_semantics.sem_params -> (Joint.joint_program, AST.ident -> Nat.nat
343  Types.option) Types.prod -> joint_global
344
345val joint_exec :
346  Joint_semantics.sem_params -> (IO.io_out, IO.io_in)
347  SmallstepExec.trans_system
348
349val joint_fullexec :
350  Joint_semantics.sem_params -> (IO.io_out, IO.io_in) SmallstepExec.fullexec
351
352val joint_preclassified_system :
353  Joint_semantics.sem_params -> Measurable.preclassified_system
354
Note: See TracBrowser for help on using the repository browser.