source: extracted/errors.ml @ 2649

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

...

File size: 8.9 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_969 -> h_MSG x_969
46| CTX (tag, x_970) -> h_CTX tag x_970
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_974 -> h_MSG x_974
53| CTX (tag, x_975) -> h_CTX tag x_975
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_979 -> h_MSG x_979
60| CTX (tag, x_980) -> h_CTX tag x_980
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_984 -> h_MSG x_984
67| CTX (tag, x_985) -> h_CTX tag x_985
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_989 -> h_MSG x_989
74| CTX (tag, x_990) -> h_CTX tag x_990
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_994 -> h_MSG x_994
81| CTX (tag, x_995) -> h_CTX tag x_995
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_1034 -> h_OK x_1034
146| Error x_1035 -> h_Error x_1035
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_1039 -> h_OK x_1039
152| Error x_1040 -> h_Error x_1040
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_1044 -> h_OK x_1044
158| Error x_1045 -> h_Error x_1045
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_1049 -> h_OK x_1049
164| Error x_1050 -> h_Error x_1050
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_1054 -> h_OK x_1054
170| Error x_1055 -> h_Error x_1055
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_1059 -> h_OK x_1059
176| Error x_1060 -> h_Error x_1060
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 bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res **)
261let bind_eq f g0 =
262  (match f with
263   | OK x -> g0 x
264   | Error msg0 -> (fun _ -> Error msg0)) __
265
266(** val bind2_eq :
267    ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res **)
268let bind2_eq f g0 =
269  (match f with
270   | OK x -> let { Types.fst = a; Types.snd = b } = x in g0 a b
271   | Error msg0 -> (fun _ -> Error msg0)) __
272
273(** val res_to_opt : 'a1 res -> 'a1 Types.option **)
274let res_to_opt = function
275| OK v0 -> Types.Some v0
276| Error x -> Types.None
277
278(** val bind : __ -> ('a1 -> __) -> __ **)
279let bind x_1758 x_1759 =
280  Monad.m_bind0 (Monad.max_def res0) x_1758 x_1759
281
282(** val bind2 : __ -> ('a1 -> 'a2 -> __) -> __ **)
283let bind2 m f =
284  Monad.m_bind2 (Monad.max_def res0) m f
285
286(** val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __ **)
287let bind3 x x0 =
288  Monad.m_bind3 (Monad.max_def res0) x x0
289
290(** val mmap : ('a1 -> __) -> 'a1 List.list -> __ **)
291let mmap x x0 =
292  Monad.m_list_map (Monad.max_def res0) x x0
293
294(** val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __ **)
295let mmap_sigma x x0 =
296  Monad.m_list_map_sigma (Monad.max_def res0) x x0
297
Note: See TracBrowser for help on using the repository browser.