source: extracted/iO.mli @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 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: 2.7 KB
Line 
1open Preamble
2
3open Proper
4
5open Option
6
7open Setoids
8
9open Monad
10
11open Positive
12
13open Char
14
15open String
16
17open PreIdentifiers
18
19open Errors
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29open Bool
30
31open Relations
32
33open Nat
34
35open List
36
37open Hints_declaration
38
39open Core_notation
40
41open Pts
42
43open Logic
44
45open Types
46
47open Extralib
48
49open IOMonad
50
51open CostLabel
52
53open PositiveMap
54
55open Deqsets
56
57open Lists
58
59open Identifiers
60
61open Floats
62
63open Integers
64
65open AST
66
67open Division
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 illTypedEvent : String.string
98
99val convert_eventval : Events.eventval -> AST.typ -> Values.val0 Errors.res
100
101val check_eventval' : Values.val0 -> AST.typ -> Events.eventval Errors.res
102
103val check_eventval_list :
104  Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
105  Errors.res
106
107type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
108                io_in_typ : AST.typ }
109
110val io_out_rect_Type4 :
111  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
112
113val io_out_rect_Type5 :
114  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
115
116val io_out_rect_Type3 :
117  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
118
119val io_out_rect_Type2 :
120  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
121
122val io_out_rect_Type1 :
123  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
124
125val io_out_rect_Type0 :
126  (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out -> 'a1
127
128val io_function : io_out -> AST.ident
129
130val io_args : io_out -> Events.eventval List.list
131
132val io_in_typ : io_out -> AST.typ
133
134val io_out_inv_rect_Type4 :
135  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
136  -> 'a1
137
138val io_out_inv_rect_Type3 :
139  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
140  -> 'a1
141
142val io_out_inv_rect_Type2 :
143  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
144  -> 'a1
145
146val io_out_inv_rect_Type1 :
147  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
148  -> 'a1
149
150val io_out_inv_rect_Type0 :
151  io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ -> 'a1)
152  -> 'a1
153
154val io_out_discr : io_out -> io_out -> __
155
156val io_out_jmdiscr : io_out -> io_out -> __
157
158type io_in = eventval_type
159
160val do_io :
161  AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
162  eventval_type) IOMonad.iO
163
164val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO
165
Note: See TracBrowser for help on using the repository browser.