source: driver/extracted/iO.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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 Exp
66
67open Arithmetic
68
69open Extranat
70
71open Vector
72
73open FoldStuff
74
75open BitVector
76
77open Z
78
79open BitVectorZ
80
81open Pointers
82
83open Coqlib
84
85open Values
86
87open Events
88
89type eventval_type = __
90
91val mk_eventval : AST.typ -> eventval_type -> Events.eventval
92
93val mk_val : AST.typ -> eventval_type -> Values.val0
94
95val convert_eventval : Events.eventval -> AST.typ -> Values.val0 Errors.res
96
97val check_eventval' : Values.val0 -> AST.typ -> Events.eventval Errors.res
98
99val check_eventval_list :
100  Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
101  Errors.res
102
103type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
104                io_in_typ : AST.typ }
105
106val io_out_rect_Type4 :
107  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
108
109val io_out_rect_Type5 :
110  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
111
112val io_out_rect_Type3 :
113  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
114
115val io_out_rect_Type2 :
116  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
117
118val io_out_rect_Type1 :
119  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
120
121val io_out_rect_Type0 :
122  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
123
124val io_function : io_out -> AST.ident
125
126val io_args : io_out -> Events.eventval List.list
127
128val io_in_typ : io_out -> AST.typ
129
130val io_out_inv_rect_Type4 :
131  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
132  -> 'a1
133
134val io_out_inv_rect_Type3 :
135  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
136  -> 'a1
137
138val io_out_inv_rect_Type2 :
139  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
140  -> 'a1
141
142val io_out_inv_rect_Type1 :
143  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
144  -> 'a1
145
146val io_out_inv_rect_Type0 :
147  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
148  -> 'a1
149
150val io_out_discr : io_out -> io_out -> __
151
152val io_out_jmdiscr : io_out -> io_out -> __
153
154type io_in = eventval_type
155
156val do_io :
157  AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
158  eventval_type) IOMonad.iO
159
160val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO
161
Note: See TracBrowser for help on using the repository browser.