source: extracted/errors.mli @ 2716

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

...

File size: 4.1 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 bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res
149
150val bind2_eq :
151  ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res
152
153val res_to_opt : 'a1 res -> 'a1 Types.option
154
155val bind : __ -> ('a1 -> __) -> __
156
157val bind2 : __ -> ('a1 -> 'a2 -> __) -> __
158
159val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __
160
161val mmap : ('a1 -> __) -> 'a1 List.list -> __
162
163val mmap_sigma : ('a1 -> __) -> 'a1 List.list -> __
164
Note: See TracBrowser for help on using the repository browser.