source: extracted/iOMonad.mli @ 2729

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

...

File size: 3.6 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open ErrorMessages
32
33open Option
34
35open Setoids
36
37open Monad
38
39open Positive
40
41open PreIdentifiers
42
43open Errors
44
45type ('output, 'input, 't) iO =
46| Interact of 'output * ('input -> ('output, 'input, 't) iO)
47| Value of 't
48| Wrong of Errors.errmsg
49
50val iO_rect_Type4 :
51  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
52  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
53
54val iO_rect_Type3 :
55  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
56  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
57
58val iO_rect_Type2 :
59  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
60  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
61
62val iO_rect_Type1 :
63  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
64  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
65
66val iO_rect_Type0 :
67  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
68  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
69
70val iO_inv_rect_Type4 :
71  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
72  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
73  'a4
74
75val iO_inv_rect_Type3 :
76  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
77  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
78  'a4
79
80val iO_inv_rect_Type2 :
81  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
82  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
83  'a4
84
85val iO_inv_rect_Type1 :
86  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
87  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
88  'a4
89
90val iO_inv_rect_Type0 :
91  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
92  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
93  'a4
94
95val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __
96
97val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __
98
99open Proper
100
101val bindIO :
102  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO
103
104val iOMonad : Monad.monadProps
105
106val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __
107
108type rel_io = __
109
110val iORel : Monad.monadRel
111
112type pred_io = __
113
114val pred_io_inject : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
115
116val iOPred : Monad.injMonadPred
117
118val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO
119
120val err_to_io_sig :
121  'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO
122
123type p_io = __
124
125type p_io' = __
126
127val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
128
129val io_inject :
130  ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO
131
132val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO
133
134val opt_to_io : Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO
135
136val bind_res_value :
137  'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
138  'a5) -> 'a5
139
140val bindIO_value :
141  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
142  __ -> 'a5) -> 'a5
143
144val bindIO_res_interact :
145  'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1, 'a2,
146  'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
147
148val bindIO_opt_interact :
149  Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 ->
150  ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
151
Note: See TracBrowser for help on using the repository browser.