source: driver/extracted/rTLabs_semantics.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 9.9 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open ErrorMessages
22
23open Option
24
25open Setoids
26
27open Monad
28
29open Jmeq
30
31open Russell
32
33open Positive
34
35open PreIdentifiers
36
37open Errors
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 Globalenvs
96
97open CostLabel
98
99open Events
100
101open IOMonad
102
103open IO
104
105open SmallstepExec
106
107open BitVectorTrie
108
109open Graphs
110
111open Order
112
113open Registers
114
115open FrontEndOps
116
117open RTLabs_syntax
118
119type genv = RTLabs_syntax.internal_function AST.fundef Globalenvs.genv_t
120
121type frame = { func : RTLabs_syntax.internal_function;
122               locals : Values.val0 Registers.register_env;
123               next : Graphs.label; sp : Pointers.block;
124               retdst : Registers.register Types.option }
125
126val frame_rect_Type4 :
127  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
128  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
129  'a1) -> frame -> 'a1
130
131val frame_rect_Type5 :
132  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
133  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
134  'a1) -> frame -> 'a1
135
136val frame_rect_Type3 :
137  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
138  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
139  'a1) -> frame -> 'a1
140
141val frame_rect_Type2 :
142  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
143  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
144  'a1) -> frame -> 'a1
145
146val frame_rect_Type1 :
147  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
148  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
149  'a1) -> frame -> 'a1
150
151val frame_rect_Type0 :
152  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
153  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
154  'a1) -> frame -> 'a1
155
156val func : frame -> RTLabs_syntax.internal_function
157
158val locals : frame -> Values.val0 Registers.register_env
159
160val next : frame -> Graphs.label
161
162val sp : frame -> Pointers.block
163
164val retdst : frame -> Registers.register Types.option
165
166val frame_inv_rect_Type4 :
167  frame -> (RTLabs_syntax.internal_function -> Values.val0
168  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
169  Registers.register Types.option -> __ -> 'a1) -> 'a1
170
171val frame_inv_rect_Type3 :
172  frame -> (RTLabs_syntax.internal_function -> Values.val0
173  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
174  Registers.register Types.option -> __ -> 'a1) -> 'a1
175
176val frame_inv_rect_Type2 :
177  frame -> (RTLabs_syntax.internal_function -> Values.val0
178  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
179  Registers.register Types.option -> __ -> 'a1) -> 'a1
180
181val frame_inv_rect_Type1 :
182  frame -> (RTLabs_syntax.internal_function -> Values.val0
183  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
184  Registers.register Types.option -> __ -> 'a1) -> 'a1
185
186val frame_inv_rect_Type0 :
187  frame -> (RTLabs_syntax.internal_function -> Values.val0
188  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
189  Registers.register Types.option -> __ -> 'a1) -> 'a1
190
191val frame_jmdiscr : frame -> frame -> __
192
193val adv : Graphs.label -> frame -> frame
194
195type state =
196| State of frame * frame List.list * GenMem.mem
197| Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef
198   * Values.val0 List.list * Registers.register Types.option
199   * frame List.list * GenMem.mem
200| Returnstate of Values.val0 Types.option * Registers.register Types.option
201   * frame List.list * GenMem.mem
202| Finalstate of Integers.int
203
204val state_rect_Type4 :
205  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
206  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
207  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
208  (Values.val0 Types.option -> Registers.register Types.option -> frame
209  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
210
211val state_rect_Type5 :
212  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
213  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
214  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
215  (Values.val0 Types.option -> Registers.register Types.option -> frame
216  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
217
218val state_rect_Type3 :
219  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
220  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
221  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
222  (Values.val0 Types.option -> Registers.register Types.option -> frame
223  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
224
225val state_rect_Type2 :
226  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
227  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
228  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
229  (Values.val0 Types.option -> Registers.register Types.option -> frame
230  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
231
232val state_rect_Type1 :
233  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
234  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
235  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
236  (Values.val0 Types.option -> Registers.register Types.option -> frame
237  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
238
239val state_rect_Type0 :
240  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
241  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
242  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
243  (Values.val0 Types.option -> Registers.register Types.option -> frame
244  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
245
246val state_inv_rect_Type4 :
247  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
248  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
249  List.list -> Registers.register Types.option -> frame List.list ->
250  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
251  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
252  (Integers.int -> __ -> 'a1) -> 'a1
253
254val state_inv_rect_Type3 :
255  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
256  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
257  List.list -> Registers.register Types.option -> frame List.list ->
258  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
259  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
260  (Integers.int -> __ -> 'a1) -> 'a1
261
262val state_inv_rect_Type2 :
263  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
264  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
265  List.list -> Registers.register Types.option -> frame List.list ->
266  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
267  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
268  (Integers.int -> __ -> 'a1) -> 'a1
269
270val state_inv_rect_Type1 :
271  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
272  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
273  List.list -> Registers.register Types.option -> frame List.list ->
274  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
275  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
276  (Integers.int -> __ -> 'a1) -> 'a1
277
278val state_inv_rect_Type0 :
279  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
280  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
281  List.list -> Registers.register Types.option -> frame List.list ->
282  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
283  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
284  (Integers.int -> __ -> 'a1) -> 'a1
285
286val state_jmdiscr : state -> state -> __
287
288val build_state :
289  frame -> frame List.list -> GenMem.mem -> Graphs.label -> state
290
291val next_instruction : frame -> RTLabs_syntax.statement
292
293val init_locals :
294  (Registers.register, AST.typ) Types.prod List.list -> Values.val0
295  Registers.register_env
296
297val reg_store :
298  PreIdentifiers.identifier -> Values.val0 -> Values.val0
299  Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map
300  Errors.res
301
302val params_store :
303  (Registers.register, AST.typ) Types.prod List.list -> Values.val0 List.list
304  -> Values.val0 Registers.register_env -> Values.val0 Registers.register_env
305  Errors.res
306
307val reg_retrieve :
308  Values.val0 Registers.register_env -> Registers.register -> Values.val0
309  Errors.res
310
311val eval_statement :
312  genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
313  IOMonad.iO
314
315val rTLabs_is_final : state -> Integers.int Types.option
316
317val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
318
319val make_global : RTLabs_syntax.rTLabs_program -> genv
320
321val make_initial_state : RTLabs_syntax.rTLabs_program -> state Errors.res
322
323val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
324
325val bind_ok :
326  'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ ->
327  'a3) -> 'a3
328
329val jmeq_hackT : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
330
331val func_block_of_exec :
332  genv -> state -> Events.trace -> AST.ident ->
333  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
334  Registers.register Types.option -> frame List.list -> GenMem.mem ->
335  Pointers.block Types.sig0
336
Note: See TracBrowser for help on using the repository browser.