source: extracted/iO.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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