source: extracted/iO.mli @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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 BitVectorTrie
50
51open CostLabel
52
53open PositiveMap
54
55open Deqsets
56
57open Lists
58
59open Identifiers
60
61open Integers
62
63open AST
64
65open Division
66
67open Exp
68
69open Arithmetic
70
71open Extranat
72
73open Vector
74
75open FoldStuff
76
77open BitVector
78
79open Z
80
81open BitVectorZ
82
83open Pointers
84
85open Coqlib
86
87open Values
88
89open Events
90
91type eventval_type = __
92
93val mk_eventval : AST.typ -> eventval_type -> Events.eventval
94
95val mk_val : AST.typ -> eventval_type -> Values.val0
96
97val convert_eventval : Events.eventval -> AST.typ -> Values.val0 Errors.res
98
99val check_eventval' : Values.val0 -> AST.typ -> Events.eventval Errors.res
100
101val check_eventval_list :
102  Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
103  Errors.res
104
105type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
106                io_in_typ : AST.typ }
107
108val io_out_rect_Type4 :
109  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
110
111val io_out_rect_Type5 :
112  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
113
114val io_out_rect_Type3 :
115  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
116
117val io_out_rect_Type2 :
118  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
119
120val io_out_rect_Type1 :
121  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
122
123val io_out_rect_Type0 :
124  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
125
126val io_function : io_out -> AST.ident
127
128val io_args : io_out -> Events.eventval List.list
129
130val io_in_typ : io_out -> AST.typ
131
132val io_out_inv_rect_Type4 :
133  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
134  -> 'a1
135
136val io_out_inv_rect_Type3 :
137  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
138  -> 'a1
139
140val io_out_inv_rect_Type2 :
141  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
142  -> 'a1
143
144val io_out_inv_rect_Type1 :
145  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
146  -> 'a1
147
148val io_out_inv_rect_Type0 :
149  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
150  -> 'a1
151
152val io_out_discr : io_out -> io_out -> __
153
154val io_out_jmdiscr : io_out -> io_out -> __
155
156type io_in = eventval_type
157
158val do_io :
159  AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
160  eventval_type) IOMonad.iO
161
162val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO
163
Note: See TracBrowser for help on using the repository browser.