source: extracted/semanticsUtils.mli @ 2829

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

Semantics files committed.

File size: 13.8 KB
Line 
1open Preamble
2
3open ExtraGlobalenvs
4
5open I8051bis
6
7open String
8
9open Sets
10
11open Listb
12
13open LabelledObjects
14
15open BitVectorTrie
16
17open Graphs
18
19open I8051
20
21open Order
22
23open Registers
24
25open BackEndOps
26
27open Joint
28
29open BEMem
30
31open CostLabel
32
33open Events
34
35open IOMonad
36
37open IO
38
39open Extra_bool
40
41open Coqlib
42
43open Values
44
45open FrontEndVal
46
47open Hide
48
49open ByteValues
50
51open Division
52
53open Z
54
55open BitVectorZ
56
57open Pointers
58
59open GenMem
60
61open FrontEndMem
62
63open Proper
64
65open PositiveMap
66
67open Deqsets
68
69open Extralib
70
71open Lists
72
73open Identifiers
74
75open Exp
76
77open Arithmetic
78
79open Vector
80
81open Div_and_mod
82
83open Util
84
85open FoldStuff
86
87open BitVector
88
89open Extranat
90
91open Integers
92
93open AST
94
95open ErrorMessages
96
97open Option
98
99open Setoids
100
101open Monad
102
103open Jmeq
104
105open Russell
106
107open Positive
108
109open PreIdentifiers
110
111open Bool
112
113open Relations
114
115open Nat
116
117open List
118
119open Hints_declaration
120
121open Core_notation
122
123open Pts
124
125open Logic
126
127open Types
128
129open Errors
130
131open Globalenvs
132
133open Joint_semantics
134
135open Deqsets_extra
136
137open State
138
139open Bind_new
140
141open BindLists
142
143open Blocks
144
145open TranslateUtils
146
147open ExtraMonads
148
149type hw_register_env = { reg_env : ByteValues.beval
150                                   BitVectorTrie.bitVectorTrie;
151                         other_bit : ByteValues.bebit }
152
153val hw_register_env_rect_Type4 :
154  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
155  -> hw_register_env -> 'a1
156
157val hw_register_env_rect_Type5 :
158  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
159  -> hw_register_env -> 'a1
160
161val hw_register_env_rect_Type3 :
162  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
163  -> hw_register_env -> 'a1
164
165val hw_register_env_rect_Type2 :
166  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
167  -> hw_register_env -> 'a1
168
169val hw_register_env_rect_Type1 :
170  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
171  -> hw_register_env -> 'a1
172
173val hw_register_env_rect_Type0 :
174  (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
175  -> hw_register_env -> 'a1
176
177val reg_env : hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie
178
179val other_bit : hw_register_env -> ByteValues.bebit
180
181val hw_register_env_inv_rect_Type4 :
182  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
183  ByteValues.bebit -> __ -> 'a1) -> 'a1
184
185val hw_register_env_inv_rect_Type3 :
186  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
187  ByteValues.bebit -> __ -> 'a1) -> 'a1
188
189val hw_register_env_inv_rect_Type2 :
190  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
191  ByteValues.bebit -> __ -> 'a1) -> 'a1
192
193val hw_register_env_inv_rect_Type1 :
194  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
195  ByteValues.bebit -> __ -> 'a1) -> 'a1
196
197val hw_register_env_inv_rect_Type0 :
198  hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
199  ByteValues.bebit -> __ -> 'a1) -> 'a1
200
201val hw_register_env_discr : hw_register_env -> hw_register_env -> __
202
203val hw_register_env_jmdiscr : hw_register_env -> hw_register_env -> __
204
205val empty_hw_register_env : hw_register_env
206
207val hwreg_retrieve : hw_register_env -> I8051.register -> ByteValues.beval
208
209val hwreg_store :
210  I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env
211
212val hwreg_set_other : ByteValues.bebit -> hw_register_env -> hw_register_env
213
214val hwreg_retrieve_sp : hw_register_env -> ByteValues.xpointer Errors.res
215
216val hwreg_store_sp :
217  hw_register_env -> ByteValues.xpointer -> hw_register_env
218
219type reg_sp = { reg_sp_env : ByteValues.beval Identifiers.identifier_map;
220                stackp : ByteValues.xpointer }
221
222val reg_sp_rect_Type4 :
223  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
224  -> reg_sp -> 'a1
225
226val reg_sp_rect_Type5 :
227  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
228  -> reg_sp -> 'a1
229
230val reg_sp_rect_Type3 :
231  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
232  -> reg_sp -> 'a1
233
234val reg_sp_rect_Type2 :
235  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
236  -> reg_sp -> 'a1
237
238val reg_sp_rect_Type1 :
239  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
240  -> reg_sp -> 'a1
241
242val reg_sp_rect_Type0 :
243  (ByteValues.beval Identifiers.identifier_map -> ByteValues.xpointer -> 'a1)
244  -> reg_sp -> 'a1
245
246val reg_sp_env : reg_sp -> ByteValues.beval Identifiers.identifier_map
247
248val stackp : reg_sp -> ByteValues.xpointer
249
250val reg_sp_inv_rect_Type4 :
251  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
252  ByteValues.xpointer -> __ -> 'a1) -> 'a1
253
254val reg_sp_inv_rect_Type3 :
255  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
256  ByteValues.xpointer -> __ -> 'a1) -> 'a1
257
258val reg_sp_inv_rect_Type2 :
259  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
260  ByteValues.xpointer -> __ -> 'a1) -> 'a1
261
262val reg_sp_inv_rect_Type1 :
263  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
264  ByteValues.xpointer -> __ -> 'a1) -> 'a1
265
266val reg_sp_inv_rect_Type0 :
267  reg_sp -> (ByteValues.beval Identifiers.identifier_map ->
268  ByteValues.xpointer -> __ -> 'a1) -> 'a1
269
270val reg_sp_discr : reg_sp -> reg_sp -> __
271
272val reg_sp_jmdiscr : reg_sp -> reg_sp -> __
273
274val dpi1__o__reg_sp_env__o__inject :
275  (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
276  Types.sig0
277
278val eject__o__reg_sp_env__o__inject :
279  reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map Types.sig0
280
281val reg_sp_env__o__inject :
282  reg_sp -> ByteValues.beval Identifiers.identifier_map Types.sig0
283
284val dpi1__o__reg_sp_env :
285  (reg_sp, 'a1) Types.dPair -> ByteValues.beval Identifiers.identifier_map
286
287val eject__o__reg_sp_env :
288  reg_sp Types.sig0 -> ByteValues.beval Identifiers.identifier_map
289
290val reg_store :
291  PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
292  Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map
293
294val reg_retrieve :
295  ByteValues.beval Registers.register_env -> Registers.register ->
296  ByteValues.beval Errors.res
297
298val reg_sp_store :
299  PreIdentifiers.identifier -> ByteValues.beval -> reg_sp -> reg_sp
300
301val reg_sp_retrieve :
302  reg_sp -> Registers.register -> ByteValues.beval Errors.res
303
304val reg_sp_init : ByteValues.xpointer -> reg_sp
305
306val init_hw_register_env : ByteValues.xpointer -> hw_register_env
307
308type sem_graph_params = { sgp_pars : Joint.uns_params;
309                          sgp_sup : (__ -> __
310                                    Joint_semantics.sem_unserialized_params) }
311
312val sem_graph_params_rect_Type4 :
313  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
314  'a1) -> sem_graph_params -> 'a1
315
316val sem_graph_params_rect_Type5 :
317  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
318  'a1) -> sem_graph_params -> 'a1
319
320val sem_graph_params_rect_Type3 :
321  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
322  'a1) -> sem_graph_params -> 'a1
323
324val sem_graph_params_rect_Type2 :
325  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
326  'a1) -> sem_graph_params -> 'a1
327
328val sem_graph_params_rect_Type1 :
329  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
330  'a1) -> sem_graph_params -> 'a1
331
332val sem_graph_params_rect_Type0 :
333  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
334  'a1) -> sem_graph_params -> 'a1
335
336val sgp_pars : sem_graph_params -> Joint.uns_params
337
338val sgp_sup0 :
339  sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params
340
341val sem_graph_params_inv_rect_Type4 :
342  sem_graph_params -> (Joint.uns_params -> (__ -> __
343  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
344
345val sem_graph_params_inv_rect_Type3 :
346  sem_graph_params -> (Joint.uns_params -> (__ -> __
347  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
348
349val sem_graph_params_inv_rect_Type2 :
350  sem_graph_params -> (Joint.uns_params -> (__ -> __
351  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
352
353val sem_graph_params_inv_rect_Type1 :
354  sem_graph_params -> (Joint.uns_params -> (__ -> __
355  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
356
357val sem_graph_params_inv_rect_Type0 :
358  sem_graph_params -> (Joint.uns_params -> (__ -> __
359  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
360
361val sem_graph_params_jmdiscr : sem_graph_params -> sem_graph_params -> __
362
363val sem_graph_params_to_graph_params : sem_graph_params -> Joint.graph_params
364
365val sem_graph_params_to_sem_params :
366  sem_graph_params -> Joint_semantics.sem_params
367
368val sem_params_from_sem_graph_params__o__msu_pars :
369  sem_graph_params -> Joint.joint_closed_internal_function
370  Joint_semantics.sem_unserialized_params
371
372val sem_params_from_sem_graph_params__o__msu_pars__o__st_pars :
373  sem_graph_params -> Joint_semantics.sem_state_params
374
375val sem_params_from_sem_graph_params__o__spp :
376  sem_graph_params -> Joint.params
377
378val sem_params_from_sem_graph_params__o__spp__o__stmt_pars :
379  sem_graph_params -> Joint.stmt_params
380
381val sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars :
382  sem_graph_params -> Joint.uns_params
383
384val sem_params_from_sem_graph_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
385  sem_graph_params -> Joint.unserialized_params
386
387type sem_lin_params = { slp_pars : Joint.uns_params;
388                        slp_sup : (__ -> __
389                                  Joint_semantics.sem_unserialized_params) }
390
391val sem_lin_params_rect_Type4 :
392  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
393  'a1) -> sem_lin_params -> 'a1
394
395val sem_lin_params_rect_Type5 :
396  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
397  'a1) -> sem_lin_params -> 'a1
398
399val sem_lin_params_rect_Type3 :
400  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
401  'a1) -> sem_lin_params -> 'a1
402
403val sem_lin_params_rect_Type2 :
404  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
405  'a1) -> sem_lin_params -> 'a1
406
407val sem_lin_params_rect_Type1 :
408  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
409  'a1) -> sem_lin_params -> 'a1
410
411val sem_lin_params_rect_Type0 :
412  (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) ->
413  'a1) -> sem_lin_params -> 'a1
414
415val slp_pars : sem_lin_params -> Joint.uns_params
416
417val slp_sup0 : sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params
418
419val sem_lin_params_inv_rect_Type4 :
420  sem_lin_params -> (Joint.uns_params -> (__ -> __
421  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
422
423val sem_lin_params_inv_rect_Type3 :
424  sem_lin_params -> (Joint.uns_params -> (__ -> __
425  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
426
427val sem_lin_params_inv_rect_Type2 :
428  sem_lin_params -> (Joint.uns_params -> (__ -> __
429  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
430
431val sem_lin_params_inv_rect_Type1 :
432  sem_lin_params -> (Joint.uns_params -> (__ -> __
433  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
434
435val sem_lin_params_inv_rect_Type0 :
436  sem_lin_params -> (Joint.uns_params -> (__ -> __
437  Joint_semantics.sem_unserialized_params) -> __ -> 'a1) -> 'a1
438
439val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __
440
441val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params
442
443val sem_lin_params_to_sem_params :
444  sem_lin_params -> Joint_semantics.sem_params
445
446val sem_params_from_sem_lin_params__o__msu_pars :
447  sem_lin_params -> Joint.joint_closed_internal_function
448  Joint_semantics.sem_unserialized_params
449
450val sem_params_from_sem_lin_params__o__msu_pars__o__st_pars :
451  sem_lin_params -> Joint_semantics.sem_state_params
452
453val sem_params_from_sem_lin_params__o__spp : sem_lin_params -> Joint.params
454
455val sem_params_from_sem_lin_params__o__spp__o__stmt_pars :
456  sem_lin_params -> Joint.stmt_params
457
458val sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars :
459  sem_lin_params -> Joint.uns_params
460
461val sem_params_from_sem_lin_params__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
462  sem_lin_params -> Joint.unserialized_params
463
464val match_genv_t_rect_Type4 :
465  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
466  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
467
468val match_genv_t_rect_Type5 :
469  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
470  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
471
472val match_genv_t_rect_Type3 :
473  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
474  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
475
476val match_genv_t_rect_Type2 :
477  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
478  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
479
480val match_genv_t_rect_Type1 :
481  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
482  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
483
484val match_genv_t_rect_Type0 :
485  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
486  Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1
487
488val match_genv_t_inv_rect_Type4 :
489  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
490  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
491
492val match_genv_t_inv_rect_Type3 :
493  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
494  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
495
496val match_genv_t_inv_rect_Type2 :
497  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
498  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
499
500val match_genv_t_inv_rect_Type1 :
501  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
502  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
503
504val match_genv_t_inv_rect_Type0 :
505  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
506  Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
507
508val match_genv_t_discr :
509  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
510  Globalenvs.genv_t -> __
511
512val match_genv_t_jmdiscr :
513  AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
514  Globalenvs.genv_t -> __
515
Note: See TracBrowser for help on using the repository browser.