source: extracted/iO.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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