source: extracted/errors.ml @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 8.7 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open List
20
21open Positive
22
23open Char
24
25open String
26
27open PreIdentifiers
28
29open Jmeq
30
31open Russell
32
33open Setoids
34
35open Monad
36
37open Option
38
39type errcode =
40| MSG of String.string
41| CTX of String.string * PreIdentifiers.identifier
42
43(** val errcode_rect_Type4 :
44    (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
45    'a1) -> errcode -> 'a1 **)
46let rec errcode_rect_Type4 h_MSG h_CTX = function
47| MSG x_1982 -> h_MSG x_1982
48| CTX (tag, x_1983) -> h_CTX tag x_1983
49
50(** val errcode_rect_Type5 :
51    (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
52    'a1) -> errcode -> 'a1 **)
53let rec errcode_rect_Type5 h_MSG h_CTX = function
54| MSG x_1987 -> h_MSG x_1987
55| CTX (tag, x_1988) -> h_CTX tag x_1988
56
57(** val errcode_rect_Type3 :
58    (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
59    'a1) -> errcode -> 'a1 **)
60let rec errcode_rect_Type3 h_MSG h_CTX = function
61| MSG x_1992 -> h_MSG x_1992
62| CTX (tag, x_1993) -> h_CTX tag x_1993
63
64(** val errcode_rect_Type2 :
65    (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
66    'a1) -> errcode -> 'a1 **)
67let rec errcode_rect_Type2 h_MSG h_CTX = function
68| MSG x_1997 -> h_MSG x_1997
69| CTX (tag, x_1998) -> h_CTX tag x_1998
70
71(** val errcode_rect_Type1 :
72    (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
73    'a1) -> errcode -> 'a1 **)
74let rec errcode_rect_Type1 h_MSG h_CTX = function
75| MSG x_2002 -> h_MSG x_2002
76| CTX (tag, x_2003) -> h_CTX tag x_2003
77
78(** val errcode_rect_Type0 :
79    (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
80    'a1) -> errcode -> 'a1 **)
81let rec errcode_rect_Type0 h_MSG h_CTX = function
82| MSG x_2007 -> h_MSG x_2007
83| CTX (tag, x_2008) -> h_CTX tag x_2008
84
85(** val errcode_inv_rect_Type4 :
86    errcode -> (String.string -> __ -> 'a1) -> (String.string ->
87    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
88let errcode_inv_rect_Type4 hterm h1 h2 =
89  let hcut = errcode_rect_Type4 h1 h2 hterm in hcut __
90
91(** val errcode_inv_rect_Type3 :
92    errcode -> (String.string -> __ -> 'a1) -> (String.string ->
93    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
94let errcode_inv_rect_Type3 hterm h1 h2 =
95  let hcut = errcode_rect_Type3 h1 h2 hterm in hcut __
96
97(** val errcode_inv_rect_Type2 :
98    errcode -> (String.string -> __ -> 'a1) -> (String.string ->
99    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
100let errcode_inv_rect_Type2 hterm h1 h2 =
101  let hcut = errcode_rect_Type2 h1 h2 hterm in hcut __
102
103(** val errcode_inv_rect_Type1 :
104    errcode -> (String.string -> __ -> 'a1) -> (String.string ->
105    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
106let errcode_inv_rect_Type1 hterm h1 h2 =
107  let hcut = errcode_rect_Type1 h1 h2 hterm in hcut __
108
109(** val errcode_inv_rect_Type0 :
110    errcode -> (String.string -> __ -> 'a1) -> (String.string ->
111    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
112let errcode_inv_rect_Type0 hterm h1 h2 =
113  let hcut = errcode_rect_Type0 h1 h2 hterm in hcut __
114
115(** val errcode_discr : errcode -> errcode -> __ **)
116let errcode_discr x y =
117  Logic.eq_rect_Type2 x
118    (match x with
119     | MSG a0 -> Obj.magic (fun _ dH -> dH __)
120     | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
121
122(** val errcode_jmdiscr : errcode -> errcode -> __ **)
123let errcode_jmdiscr x y =
124  Logic.eq_rect_Type2 x
125    (match x with
126     | MSG a0 -> Obj.magic (fun _ dH -> dH __)
127     | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
128
129type errmsg = errcode List.list
130
131(** val msg : String.string -> errmsg **)
132let msg s =
133  List.Cons ((MSG s), List.Nil)
134
135type 'a res =
136| OK of 'a
137| Error of errmsg
138
139(** val res_rect_Type4 :
140    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
141let rec res_rect_Type4 h_OK h_Error = function
142| OK x_2047 -> h_OK x_2047
143| Error x_2048 -> h_Error x_2048
144
145(** val res_rect_Type5 :
146    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
147let rec res_rect_Type5 h_OK h_Error = function
148| OK x_2052 -> h_OK x_2052
149| Error x_2053 -> h_Error x_2053
150
151(** val res_rect_Type3 :
152    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
153let rec res_rect_Type3 h_OK h_Error = function
154| OK x_2057 -> h_OK x_2057
155| Error x_2058 -> h_Error x_2058
156
157(** val res_rect_Type2 :
158    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
159let rec res_rect_Type2 h_OK h_Error = function
160| OK x_2062 -> h_OK x_2062
161| Error x_2063 -> h_Error x_2063
162
163(** val res_rect_Type1 :
164    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
165let rec res_rect_Type1 h_OK h_Error = function
166| OK x_2067 -> h_OK x_2067
167| Error x_2068 -> h_Error x_2068
168
169(** val res_rect_Type0 :
170    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
171let rec res_rect_Type0 h_OK h_Error = function
172| OK x_2072 -> h_OK x_2072
173| Error x_2073 -> h_Error x_2073
174
175(** val res_inv_rect_Type4 :
176    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
177let res_inv_rect_Type4 hterm h1 h2 =
178  let hcut = res_rect_Type4 h1 h2 hterm in hcut __
179
180(** val res_inv_rect_Type3 :
181    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
182let res_inv_rect_Type3 hterm h1 h2 =
183  let hcut = res_rect_Type3 h1 h2 hterm in hcut __
184
185(** val res_inv_rect_Type2 :
186    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
187let res_inv_rect_Type2 hterm h1 h2 =
188  let hcut = res_rect_Type2 h1 h2 hterm in hcut __
189
190(** val res_inv_rect_Type1 :
191    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
192let res_inv_rect_Type1 hterm h1 h2 =
193  let hcut = res_rect_Type1 h1 h2 hterm in hcut __
194
195(** val res_inv_rect_Type0 :
196    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
197let res_inv_rect_Type0 hterm h1 h2 =
198  let hcut = res_rect_Type0 h1 h2 hterm in hcut __
199
200(** val res_discr : 'a1 res -> 'a1 res -> __ **)
201let res_discr x y =
202  Logic.eq_rect_Type2 x
203    (match x with
204     | OK a0 -> Obj.magic (fun _ dH -> dH __)
205     | Error a0 -> Obj.magic (fun _ dH -> dH __)) y
206
207(** val res_jmdiscr : 'a1 res -> 'a1 res -> __ **)
208let res_jmdiscr x y =
209  Logic.eq_rect_Type2 x
210    (match x with
211     | OK a0 -> Obj.magic (fun _ dH -> dH __)
212     | Error a0 -> Obj.magic (fun _ dH -> dH __)) y
213
214(** val res0 : Monad.monadProps **)
215let res0 =
216  Monad.makeMonadProps (fun _ x -> OK x) (fun _ _ m f ->
217    match m with
218    | OK x -> f x
219    | Error msg0 -> Error msg0)
220
221(** val mfold_left_i_aux :
222    (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> Nat.nat -> 'a2 List.list
223    -> __ **)
224let rec mfold_left_i_aux f x i = function
225| List.Nil -> Obj.magic x
226| List.Cons (hd0, tl) ->
227  Monad.m_bind0 (Monad.max_def res0) (Obj.magic x) (fun x0 ->
228    mfold_left_i_aux f (f i x0 hd0) (Nat.S i) tl)
229
230(** val mfold_left_i :
231    (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> __ **)
232let mfold_left_i f x =
233  mfold_left_i_aux f x Nat.O
234
235(** val wrongLength : String.string **)
236let wrongLength = "wrong length"
237  (*failwith "AXIOM TO BE REALIZED"*)
238
239(** val mfold_left2 :
240    ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3
241    List.list -> 'a1 res **)
242let rec mfold_left2 f accu left right =
243  match left with
244  | List.Nil ->
245    (match right with
246     | List.Nil -> accu
247     | List.Cons (hd0, tl) -> Error (msg wrongLength))
248  | List.Cons (hd0, tl) ->
249    (match right with
250     | List.Nil -> Error (msg wrongLength)
251     | List.Cons (hd', tl') ->
252       Obj.magic
253         (Monad.m_bind0 (Monad.max_def res0) (Obj.magic accu) (fun accu0 ->
254           Obj.magic (mfold_left2 f (f accu0 hd0 hd') tl tl'))))
255
256(** val opt_to_res : errmsg -> 'a1 Types.option -> 'a1 res **)
257let opt_to_res msg0 = function
258| Types.None -> Error msg0
259| Types.Some v0 -> OK v0
260
261(** val bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res **)
262let bind_eq f g0 =
263  (match f with
264   | OK x -> g0 x
265   | Error msg0 -> (fun _ -> Error msg0)) __
266
267(** val bind2_eq :
268    ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res **)
269let bind2_eq f g0 =
270  (match f with
271   | OK x -> let { Types.fst = a; Types.snd = b } = x in g0 a b
272   | Error msg0 -> (fun _ -> Error msg0)) __
273
274(** val res_to_opt : 'a1 res -> 'a1 Types.option **)
275let res_to_opt = function
276| OK v0 -> Types.Some v0
277| Error x -> Types.None
278
279(** val bind : __ -> ('a1 -> __) -> __ **)
280let bind x_1758 x_1759 =
281  Monad.m_bind0 (Monad.max_def res0) x_1758 x_1759
282
283(** val bind2 : __ -> ('a1 -> 'a2 -> __) -> __ **)
284let bind2 m f =
285  Monad.m_bind2 (Monad.max_def res0) m f
286
287(** val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
288let bind3 x x0 =
289  Monad.m_bind3 (Monad.max_def res0) x x0
290
291(** val mmap : ('a1 -> __) -> 'a1 List.list -> __ **)
292let mmap x x0 =
293  Monad.m_list_map (Monad.max_def res0) x x0
294
295(** val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __ **)
296let mmap_sigma x x0 =
297  Monad.m_list_map_sigma (Monad.max_def res0) x x0
298
Note: See TracBrowser for help on using the repository browser.