source: extracted/errors.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 9.6 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 PreIdentifiers
24
25open Jmeq
26
27open Russell
28
29open Setoids
30
31open Monad
32
33open Option
34
35open ErrorMessages
36
37type errcode =
38| MSG of ErrorMessages.errorMessage
39| CTX of PreIdentifiers.identifierTag * PreIdentifiers.identifier
40
41(** val errcode_rect_Type4 :
42    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
43    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
44let rec errcode_rect_Type4 h_MSG h_CTX = function
45| MSG x_2957 -> h_MSG x_2957
46| CTX (tag, x_2958) -> h_CTX tag x_2958
47
48(** val errcode_rect_Type5 :
49    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
50    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
51let rec errcode_rect_Type5 h_MSG h_CTX = function
52| MSG x_2962 -> h_MSG x_2962
53| CTX (tag, x_2963) -> h_CTX tag x_2963
54
55(** val errcode_rect_Type3 :
56    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
57    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
58let rec errcode_rect_Type3 h_MSG h_CTX = function
59| MSG x_2967 -> h_MSG x_2967
60| CTX (tag, x_2968) -> h_CTX tag x_2968
61
62(** val errcode_rect_Type2 :
63    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
64    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
65let rec errcode_rect_Type2 h_MSG h_CTX = function
66| MSG x_2972 -> h_MSG x_2972
67| CTX (tag, x_2973) -> h_CTX tag x_2973
68
69(** val errcode_rect_Type1 :
70    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
71    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
72let rec errcode_rect_Type1 h_MSG h_CTX = function
73| MSG x_2977 -> h_MSG x_2977
74| CTX (tag, x_2978) -> h_CTX tag x_2978
75
76(** val errcode_rect_Type0 :
77    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
78    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
79let rec errcode_rect_Type0 h_MSG h_CTX = function
80| MSG x_2982 -> h_MSG x_2982
81| CTX (tag, x_2983) -> h_CTX tag x_2983
82
83(** val errcode_inv_rect_Type4 :
84    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
85    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
86    -> 'a1 **)
87let errcode_inv_rect_Type4 hterm h1 h2 =
88  let hcut = errcode_rect_Type4 h1 h2 hterm in hcut __
89
90(** val errcode_inv_rect_Type3 :
91    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
92    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
93    -> '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 -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
99    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
100    -> 'a1 **)
101let errcode_inv_rect_Type2 hterm h1 h2 =
102  let hcut = errcode_rect_Type2 h1 h2 hterm in hcut __
103
104(** val errcode_inv_rect_Type1 :
105    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
106    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
107    -> 'a1 **)
108let errcode_inv_rect_Type1 hterm h1 h2 =
109  let hcut = errcode_rect_Type1 h1 h2 hterm in hcut __
110
111(** val errcode_inv_rect_Type0 :
112    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
113    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
114    -> 'a1 **)
115let errcode_inv_rect_Type0 hterm h1 h2 =
116  let hcut = errcode_rect_Type0 h1 h2 hterm in hcut __
117
118(** val errcode_discr : errcode -> errcode -> __ **)
119let errcode_discr x y =
120  Logic.eq_rect_Type2 x
121    (match x with
122     | MSG a0 -> Obj.magic (fun _ dH -> dH __)
123     | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
124
125(** val errcode_jmdiscr : errcode -> errcode -> __ **)
126let errcode_jmdiscr x y =
127  Logic.eq_rect_Type2 x
128    (match x with
129     | MSG a0 -> Obj.magic (fun _ dH -> dH __)
130     | CTX (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
131
132type errmsg = errcode List.list
133
134(** val msg : ErrorMessages.errorMessage -> errmsg **)
135let msg s =
136  List.Cons ((MSG s), List.Nil)
137
138type 'a res =
139| OK of 'a
140| Error of errmsg
141
142(** val res_rect_Type4 :
143    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
144let rec res_rect_Type4 h_OK h_Error = function
145| OK x_3022 -> h_OK x_3022
146| Error x_3023 -> h_Error x_3023
147
148(** val res_rect_Type5 :
149    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
150let rec res_rect_Type5 h_OK h_Error = function
151| OK x_3027 -> h_OK x_3027
152| Error x_3028 -> h_Error x_3028
153
154(** val res_rect_Type3 :
155    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
156let rec res_rect_Type3 h_OK h_Error = function
157| OK x_3032 -> h_OK x_3032
158| Error x_3033 -> h_Error x_3033
159
160(** val res_rect_Type2 :
161    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
162let rec res_rect_Type2 h_OK h_Error = function
163| OK x_3037 -> h_OK x_3037
164| Error x_3038 -> h_Error x_3038
165
166(** val res_rect_Type1 :
167    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
168let rec res_rect_Type1 h_OK h_Error = function
169| OK x_3042 -> h_OK x_3042
170| Error x_3043 -> h_Error x_3043
171
172(** val res_rect_Type0 :
173    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
174let rec res_rect_Type0 h_OK h_Error = function
175| OK x_3047 -> h_OK x_3047
176| Error x_3048 -> h_Error x_3048
177
178(** val res_inv_rect_Type4 :
179    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
180let res_inv_rect_Type4 hterm h1 h2 =
181  let hcut = res_rect_Type4 h1 h2 hterm in hcut __
182
183(** val res_inv_rect_Type3 :
184    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
185let res_inv_rect_Type3 hterm h1 h2 =
186  let hcut = res_rect_Type3 h1 h2 hterm in hcut __
187
188(** val res_inv_rect_Type2 :
189    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
190let res_inv_rect_Type2 hterm h1 h2 =
191  let hcut = res_rect_Type2 h1 h2 hterm in hcut __
192
193(** val res_inv_rect_Type1 :
194    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
195let res_inv_rect_Type1 hterm h1 h2 =
196  let hcut = res_rect_Type1 h1 h2 hterm in hcut __
197
198(** val res_inv_rect_Type0 :
199    'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2 **)
200let res_inv_rect_Type0 hterm h1 h2 =
201  let hcut = res_rect_Type0 h1 h2 hterm in hcut __
202
203(** val res_discr : 'a1 res -> 'a1 res -> __ **)
204let res_discr x y =
205  Logic.eq_rect_Type2 x
206    (match x with
207     | OK a0 -> Obj.magic (fun _ dH -> dH __)
208     | Error a0 -> Obj.magic (fun _ dH -> dH __)) y
209
210(** val res_jmdiscr : 'a1 res -> 'a1 res -> __ **)
211let res_jmdiscr x y =
212  Logic.eq_rect_Type2 x
213    (match x with
214     | OK a0 -> Obj.magic (fun _ dH -> dH __)
215     | Error a0 -> Obj.magic (fun _ dH -> dH __)) y
216
217(** val res0 : Monad.monadProps **)
218let res0 =
219  Monad.makeMonadProps (fun _ x -> OK x) (fun _ _ m f ->
220    match m with
221    | OK x -> f x
222    | Error msg0 -> Error msg0)
223
224(** val mfold_left_i_aux :
225    (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> Nat.nat -> 'a2 List.list
226    -> __ **)
227let rec mfold_left_i_aux f x i = function
228| List.Nil -> Obj.magic x
229| List.Cons (hd0, tl) ->
230  Monad.m_bind0 (Monad.max_def res0) (Obj.magic x) (fun x0 ->
231    mfold_left_i_aux f (f i x0 hd0) (Nat.S i) tl)
232
233(** val mfold_left_i :
234    (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> __ **)
235let mfold_left_i f x =
236  mfold_left_i_aux f x Nat.O
237
238(** val mfold_left2 :
239    ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3
240    List.list -> 'a1 res **)
241let rec mfold_left2 f accu left right =
242  match left with
243  | List.Nil ->
244    (match right with
245     | List.Nil -> accu
246     | List.Cons (hd0, tl) -> Error (msg ErrorMessages.WrongLength))
247  | List.Cons (hd0, tl) ->
248    (match right with
249     | List.Nil -> Error (msg ErrorMessages.WrongLength)
250     | List.Cons (hd', tl') ->
251       Obj.magic
252         (Monad.m_bind0 (Monad.max_def res0) (Obj.magic accu) (fun accu0 ->
253           Obj.magic (mfold_left2 f (f accu0 hd0 hd') tl tl'))))
254
255(** val opt_to_res : errmsg -> 'a1 Types.option -> 'a1 res **)
256let opt_to_res msg0 = function
257| Types.None -> Error msg0
258| Types.Some v0 -> OK v0
259
260(** val jmeq_to_eq__o__opt_eq_from_res__o__inject :
261    errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
262let jmeq_to_eq__o__opt_eq_from_res__o__inject x1 x2 x3 =
263  __
264
265(** val dpi1__o__opt_eq_from_res__o__inject :
266    errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a2) Types.dPair -> __
267    Types.sig0 **)
268let dpi1__o__opt_eq_from_res__o__inject x1 x2 x3 x6 =
269  __
270
271(** val eject__o__opt_eq_from_res__o__inject :
272    errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0 **)
273let eject__o__opt_eq_from_res__o__inject x1 x2 x3 x6 =
274  __
275
276(** val opt_eq_from_res__o__inject :
277    errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 **)
278let opt_eq_from_res__o__inject x1 x2 x3 =
279  __
280
281(** val bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res **)
282let bind_eq f g0 =
283  (match f with
284   | OK x -> g0 x
285   | Error msg0 -> (fun _ -> Error msg0)) __
286
287(** val bind2_eq :
288    ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res **)
289let bind2_eq f g0 =
290  (match f with
291   | OK x -> let { Types.fst = a; Types.snd = b } = x in g0 a b
292   | Error msg0 -> (fun _ -> Error msg0)) __
293
294(** val res_to_opt : 'a1 res -> 'a1 Types.option **)
295let res_to_opt = function
296| OK v0 -> Types.Some v0
297| Error x -> Types.None
298
299(** val bind : __ -> ('a1 -> __) -> __ **)
300let bind x_1758 x_1759 =
301  Monad.m_bind0 (Monad.max_def res0) x_1758 x_1759
302
303(** val bind2 : __ -> ('a1 -> 'a2 -> __) -> __ **)
304let bind2 m f =
305  Monad.m_bind2 (Monad.max_def res0) m f
306
307(** val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
308let bind3 x x0 =
309  Monad.m_bind3 (Monad.max_def res0) x x0
310
311(** val mmap : ('a1 -> __) -> 'a1 List.list -> __ **)
312let mmap x x0 =
313  Monad.m_list_map (Monad.max_def res0) x x0
314
315(** val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __ **)
316let mmap_sigma x x0 =
317  Monad.m_list_map_sigma (Monad.max_def res0) x x0
318
Note: See TracBrowser for help on using the repository browser.