source: extracted/iOMonad.mli @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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 Option
32
33open Setoids
34
35open Monad
36
37open Positive
38
39open Char
40
41open String
42
43open PreIdentifiers
44
45open Errors
46
47type ('output, 'input, 't) iO =
48| Interact of 'output * ('input -> ('output, 'input, 't) iO)
49| Value of 't
50| Wrong of Errors.errmsg
51
52val iO_rect_Type4 :
53  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
54  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
55
56val iO_rect_Type3 :
57  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
58  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
59
60val iO_rect_Type2 :
61  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
62  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
63
64val iO_rect_Type1 :
65  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
66  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
67
68val iO_rect_Type0 :
69  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
70  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
71
72val iO_inv_rect_Type4 :
73  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
74  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
75  'a4
76
77val iO_inv_rect_Type3 :
78  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
79  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
80  'a4
81
82val iO_inv_rect_Type2 :
83  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
84  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
85  'a4
86
87val iO_inv_rect_Type1 :
88  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
89  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
90  'a4
91
92val iO_inv_rect_Type0 :
93  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
94  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
95  'a4
96
97val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __
98
99val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __
100
101open Proper
102
103val bindIO :
104  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO
105
106val iOMonad : Monad.monadProps
107
108val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __
109
110type rel_io = __
111
112val iORel : Monad.monadRel
113
114type pred_io = __
115
116val pred_io_inject : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
117
118val iOPred : Monad.injMonadPred
119
120val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO
121
122val err_to_io_sig :
123  'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO
124
125type p_io = __
126
127type p_io' = __
128
129val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
130
131val io_inject :
132  ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO
133
134val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO
135
136val opt_to_io : Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO
137
138val bind_res_value :
139  'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
140  'a5) -> 'a5
141
142val bindIO_value :
143  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
144  __ -> 'a5) -> 'a5
145
146val bindIO_res_interact :
147  'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1, 'a2,
148  'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
149
150val bindIO_opt_interact :
151  Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 ->
152  ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
153
Note: See TracBrowser for help on using the repository browser.