source: driver/extracted/iO.ml @ 3106

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 6.9 KB
Line 
1open Preamble
2
3open Proper
4
5open ErrorMessages
6
7open Option
8
9open Setoids
10
11open Monad
12
13open Positive
14
15open PreIdentifiers
16
17open Errors
18
19open Div_and_mod
20
21open Jmeq
22
23open Russell
24
25open Util
26
27open Bool
28
29open Relations
30
31open Nat
32
33open List
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open Extralib
46
47open IOMonad
48
49open CostLabel
50
51open PositiveMap
52
53open Deqsets
54
55open Lists
56
57open Identifiers
58
59open Integers
60
61open AST
62
63open Division
64
65open Exp
66
67open Arithmetic
68
69open Extranat
70
71open Vector
72
73open FoldStuff
74
75open BitVector
76
77open Z
78
79open BitVectorZ
80
81open Pointers
82
83open Coqlib
84
85open Values
86
87open Events
88
89type eventval_type = __
90
91(** val mk_eventval : AST.typ -> eventval_type -> Events.eventval **)
92let mk_eventval = function
93| AST.ASTint (sz, sg) -> (fun v -> Events.EVint (sz, (Obj.magic v)))
94| AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))
95
96(** val mk_val : AST.typ -> eventval_type -> Values.val0 **)
97let mk_val = function
98| AST.ASTint (sz, x) -> (fun v -> Values.Vint (sz, (Obj.magic v)))
99| AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))
100
101(** val convert_eventval :
102    Events.eventval -> AST.typ -> Values.val0 Errors.res **)
103let convert_eventval ev = function
104| AST.ASTint (sz, x) ->
105  let Events.EVint (sz', i) = ev in
106  (match AST.eq_intsize sz sz' with
107   | Bool.True -> Errors.OK (Values.Vint (sz', i))
108   | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
109| AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
110
111(** val check_eventval' :
112    Values.val0 -> AST.typ -> Events.eventval Errors.res **)
113let check_eventval' v = function
114| AST.ASTint (sz, x) ->
115  (match v with
116   | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
117   | Values.Vint (sz', i) ->
118     (match AST.eq_intsize sz sz' with
119      | Bool.True -> Errors.OK (Events.EVint (sz', i))
120      | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
121   | Values.Vnull -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
122   | Values.Vptr x0 -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
123| AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
124
125(** val check_eventval_list :
126    Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
127    Errors.res **)
128let rec check_eventval_list vs tys =
129  match vs with
130  | List.Nil ->
131    (match tys with
132     | List.Nil -> Errors.OK List.Nil
133     | List.Cons (x, x0) ->
134       Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
135  | List.Cons (v, vt) ->
136    (match tys with
137     | List.Nil -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
138     | List.Cons (ty, tyt) ->
139       Obj.magic
140         (Monad.m_bind0 (Monad.max_def Errors.res0)
141           (Obj.magic (check_eventval' v ty)) (fun ev ->
142           Monad.m_bind0 (Monad.max_def Errors.res0)
143             (Obj.magic (check_eventval_list vt tyt)) (fun evt ->
144             Obj.magic (Errors.OK (List.Cons (ev, evt)))))))
145
146type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
147                io_in_typ : AST.typ }
148
149(** val io_out_rect_Type4 :
150    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
151    'a1 **)
152let rec io_out_rect_Type4 h_mk_io_out x_5899 =
153  let { io_function = io_function0; io_args = io_args0; io_in_typ =
154    io_in_typ0 } = x_5899
155  in
156  h_mk_io_out io_function0 io_args0 io_in_typ0
157
158(** val io_out_rect_Type5 :
159    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
160    'a1 **)
161let rec io_out_rect_Type5 h_mk_io_out x_5901 =
162  let { io_function = io_function0; io_args = io_args0; io_in_typ =
163    io_in_typ0 } = x_5901
164  in
165  h_mk_io_out io_function0 io_args0 io_in_typ0
166
167(** val io_out_rect_Type3 :
168    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
169    'a1 **)
170let rec io_out_rect_Type3 h_mk_io_out x_5903 =
171  let { io_function = io_function0; io_args = io_args0; io_in_typ =
172    io_in_typ0 } = x_5903
173  in
174  h_mk_io_out io_function0 io_args0 io_in_typ0
175
176(** val io_out_rect_Type2 :
177    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
178    'a1 **)
179let rec io_out_rect_Type2 h_mk_io_out x_5905 =
180  let { io_function = io_function0; io_args = io_args0; io_in_typ =
181    io_in_typ0 } = x_5905
182  in
183  h_mk_io_out io_function0 io_args0 io_in_typ0
184
185(** val io_out_rect_Type1 :
186    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
187    'a1 **)
188let rec io_out_rect_Type1 h_mk_io_out x_5907 =
189  let { io_function = io_function0; io_args = io_args0; io_in_typ =
190    io_in_typ0 } = x_5907
191  in
192  h_mk_io_out io_function0 io_args0 io_in_typ0
193
194(** val io_out_rect_Type0 :
195    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
196    'a1 **)
197let rec io_out_rect_Type0 h_mk_io_out x_5909 =
198  let { io_function = io_function0; io_args = io_args0; io_in_typ =
199    io_in_typ0 } = x_5909
200  in
201  h_mk_io_out io_function0 io_args0 io_in_typ0
202
203(** val io_function : io_out -> AST.ident **)
204let rec io_function xxx =
205  xxx.io_function
206
207(** val io_args : io_out -> Events.eventval List.list **)
208let rec io_args xxx =
209  xxx.io_args
210
211(** val io_in_typ : io_out -> AST.typ **)
212let rec io_in_typ xxx =
213  xxx.io_in_typ
214
215(** val io_out_inv_rect_Type4 :
216    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
217    'a1) -> 'a1 **)
218let io_out_inv_rect_Type4 hterm h1 =
219  let hcut = io_out_rect_Type4 h1 hterm in hcut __
220
221(** val io_out_inv_rect_Type3 :
222    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
223    'a1) -> 'a1 **)
224let io_out_inv_rect_Type3 hterm h1 =
225  let hcut = io_out_rect_Type3 h1 hterm in hcut __
226
227(** val io_out_inv_rect_Type2 :
228    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
229    'a1) -> 'a1 **)
230let io_out_inv_rect_Type2 hterm h1 =
231  let hcut = io_out_rect_Type2 h1 hterm in hcut __
232
233(** val io_out_inv_rect_Type1 :
234    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
235    'a1) -> 'a1 **)
236let io_out_inv_rect_Type1 hterm h1 =
237  let hcut = io_out_rect_Type1 h1 hterm in hcut __
238
239(** val io_out_inv_rect_Type0 :
240    io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
241    'a1) -> 'a1 **)
242let io_out_inv_rect_Type0 hterm h1 =
243  let hcut = io_out_rect_Type0 h1 hterm in hcut __
244
245(** val io_out_discr : io_out -> io_out -> __ **)
246let io_out_discr x y =
247  Logic.eq_rect_Type2 x
248    (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
249    Obj.magic (fun _ dH -> dH __ __ __)) y
250
251(** val io_out_jmdiscr : io_out -> io_out -> __ **)
252let io_out_jmdiscr x y =
253  Logic.eq_rect_Type2 x
254    (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
255    Obj.magic (fun _ dH -> dH __ __ __)) y
256
257type io_in = eventval_type
258
259(** val do_io :
260    AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
261    eventval_type) IOMonad.iO **)
262let do_io fn args t =
263  IOMonad.Interact ({ io_function = fn; io_args = args; io_in_typ = t },
264    (fun res -> IOMonad.Value res))
265
266(** val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO **)
267let ret x =
268  IOMonad.Value x
269
Note: See TracBrowser for help on using the repository browser.