source: extracted/errors.mli @ 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: 4.5 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
41val errcode_rect_Type4 :
42  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
43  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
44
45val errcode_rect_Type5 :
46  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
47  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
48
49val errcode_rect_Type3 :
50  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
51  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
52
53val errcode_rect_Type2 :
54  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
55  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
56
57val errcode_rect_Type1 :
58  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
59  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
60
61val errcode_rect_Type0 :
62  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
63  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1
64
65val errcode_inv_rect_Type4 :
66  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
67  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
68  'a1
69
70val errcode_inv_rect_Type3 :
71  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
72  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
73  'a1
74
75val errcode_inv_rect_Type2 :
76  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
77  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
78  'a1
79
80val errcode_inv_rect_Type1 :
81  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
82  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
83  'a1
84
85val errcode_inv_rect_Type0 :
86  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
87  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
88  'a1
89
90val errcode_discr : errcode -> errcode -> __
91
92val errcode_jmdiscr : errcode -> errcode -> __
93
94type errmsg = errcode List.list
95
96val msg : ErrorMessages.errorMessage -> errmsg
97
98type 'a res =
99| OK of 'a
100| Error of errmsg
101
102val res_rect_Type4 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
103
104val res_rect_Type5 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
105
106val res_rect_Type3 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
107
108val res_rect_Type2 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
109
110val res_rect_Type1 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
111
112val res_rect_Type0 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2
113
114val res_inv_rect_Type4 :
115  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
116
117val res_inv_rect_Type3 :
118  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
119
120val res_inv_rect_Type2 :
121  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
122
123val res_inv_rect_Type1 :
124  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
125
126val res_inv_rect_Type0 :
127  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2
128
129val res_discr : 'a1 res -> 'a1 res -> __
130
131val res_jmdiscr : 'a1 res -> 'a1 res -> __
132
133val res0 : Monad.monadProps
134
135val mfold_left_i_aux :
136  (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> Nat.nat -> 'a2 List.list
137  -> __
138
139val mfold_left_i :
140  (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> __
141
142val mfold_left2 :
143  ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3 List.list
144  -> 'a1 res
145
146val opt_to_res : errmsg -> 'a1 Types.option -> 'a1 res
147
148val jmeq_to_eq__o__opt_eq_from_res__o__inject :
149  errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
150
151val dpi1__o__opt_eq_from_res__o__inject :
152  errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a2) Types.dPair -> __ Types.sig0
153
154val eject__o__opt_eq_from_res__o__inject :
155  errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0
156
157val opt_eq_from_res__o__inject :
158  errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
159
160val bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res
161
162val bind2_eq :
163  ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res
164
165val res_to_opt : 'a1 res -> 'a1 Types.option
166
167val bind : __ -> ('a1 -> __) -> __
168
169val bind2 : __ -> ('a1 -> 'a2 -> __) -> __
170
171val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __
172
173val mmap : ('a1 -> __) -> 'a1 List.list -> __
174
175val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __
176
Note: See TracBrowser for help on using the repository browser.