source: extracted/errors.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: 9.0 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_2931 -> h_MSG x_2931
46| CTX (tag, x_2932) -> h_CTX tag x_2932
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_2936 -> h_MSG x_2936
53| CTX (tag, x_2937) -> h_CTX tag x_2937
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_2941 -> h_MSG x_2941
60| CTX (tag, x_2942) -> h_CTX tag x_2942
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_2946 -> h_MSG x_2946
67| CTX (tag, x_2947) -> h_CTX tag x_2947
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_2951 -> h_MSG x_2951
74| CTX (tag, x_2952) -> h_CTX tag x_2952
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_2956 -> h_MSG x_2956
81| CTX (tag, x_2957) -> h_CTX tag x_2957
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_2996 -> h_OK x_2996
146| Error x_2997 -> h_Error x_2997
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_3001 -> h_OK x_3001
152| Error x_3002 -> h_Error x_3002
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_3006 -> h_OK x_3006
158| Error x_3007 -> h_Error x_3007
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_3011 -> h_OK x_3011
164| Error x_3012 -> h_Error x_3012
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_3016 -> h_OK x_3016
170| Error x_3017 -> h_Error x_3017
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_3021 -> h_OK x_3021
176| Error x_3022 -> h_Error x_3022
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.