source: extracted/iOMonad.mli @ 2716

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

...

File size: 3.6 KB
RevLine 
[2601]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
[2649]31open ErrorMessages
32
[2601]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.