source: extracted/iO.mli @ 2649

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

...

File size: 2.7 KB
Line 
1open Preamble
2
3open Proper
4
5open ErrorMessages
6
7open Option
8
9open Setoids
10
11open Monad
12
13open Positive
14
15open PreIdentifiers
16
17open Errors
18
19open Div_and_mod
20
21open Jmeq
22
23open Russell
24
25open Util
26
27open Bool
28
29open Relations
30
31open Nat
32
33open List
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Types
44
45open Extralib
46
47open IOMonad
48
49open CostLabel
50
51open PositiveMap
52
53open Deqsets
54
55open Lists
56
57open Identifiers
58
59open Integers
60
61open AST
62
63open Division
64
65open Arithmetic
66
67open Extranat
68
69open Vector
70
71open FoldStuff
72
73open BitVector
74
75open Z
76
77open BitVectorZ
78
79open Pointers
80
81open Coqlib
82
83open Values
84
85open Events
86
87type eventval_type = __
88
89val mk_eventval : AST.typ -> eventval_type -> Events.eventval
90
91val mk_val : AST.typ -> eventval_type -> Values.val0
92
93val convert_eventval : Events.eventval -> AST.typ -> Values.val0 Errors.res
94
95val check_eventval' : Values.val0 -> AST.typ -> Events.eventval Errors.res
96
97val check_eventval_list :
98  Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
99  Errors.res
100
101type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
102                io_in_typ : AST.typ }
103
104val io_out_rect_Type4 :
105  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
106
107val io_out_rect_Type5 :
108  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
109
110val io_out_rect_Type3 :
111  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
112
113val io_out_rect_Type2 :
114  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
115
116val io_out_rect_Type1 :
117  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
118
119val io_out_rect_Type0 :
120  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
121
122val io_function : io_out -> AST.ident
123
124val io_args : io_out -> Events.eventval List.list
125
126val io_in_typ : io_out -> AST.typ
127
128val io_out_inv_rect_Type4 :
129  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
130  -> 'a1
131
132val io_out_inv_rect_Type3 :
133  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
134  -> 'a1
135
136val io_out_inv_rect_Type2 :
137  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
138  -> 'a1
139
140val io_out_inv_rect_Type1 :
141  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
142  -> 'a1
143
144val io_out_inv_rect_Type0 :
145  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
146  -> 'a1
147
148val io_out_discr : io_out -> io_out -> __
149
150val io_out_jmdiscr : io_out -> io_out -> __
151
152type io_in = eventval_type
153
154val do_io :
155  AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
156  eventval_type) IOMonad.iO
157
158val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO
159
Note: See TracBrowser for help on using the repository browser.