source: extracted/eRTL.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: 3.8 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open Graphs
12
13open I8051
14
15open Order
16
17open Registers
18
19open BitVectorTrie
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Identifiers
48
49open Integers
50
51open AST
52
53open Division
54
55open Exp
56
57open Arithmetic
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107type move_dst =
108| PSD of Registers.register
109| HDW of I8051.register
110
111val move_dst_rect_Type4 :
112  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
113
114val move_dst_rect_Type5 :
115  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
116
117val move_dst_rect_Type3 :
118  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
119
120val move_dst_rect_Type2 :
121  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
122
123val move_dst_rect_Type1 :
124  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
125
126val move_dst_rect_Type0 :
127  (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
128
129val move_dst_inv_rect_Type4 :
130  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
131  'a1) -> 'a1
132
133val move_dst_inv_rect_Type3 :
134  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
135  'a1) -> 'a1
136
137val move_dst_inv_rect_Type2 :
138  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
139  'a1) -> 'a1
140
141val move_dst_inv_rect_Type1 :
142  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
143  'a1) -> 'a1
144
145val move_dst_inv_rect_Type0 :
146  move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
147  'a1) -> 'a1
148
149val move_dst_discr : move_dst -> move_dst -> __
150
151val move_dst_jmdiscr : move_dst -> move_dst -> __
152
153type move_src = move_dst Joint.argument
154
155val move_src_from_dst : move_dst -> move_src
156
157val psd_argument_move_src : Joint.psd_argument -> move_src
158
159type ertl_seq =
160| Ertl_new_frame
161| Ertl_del_frame
162| Ertl_frame_size of Registers.register
163
164val ertl_seq_rect_Type4 :
165  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
166
167val ertl_seq_rect_Type5 :
168  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
169
170val ertl_seq_rect_Type3 :
171  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
172
173val ertl_seq_rect_Type2 :
174  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
175
176val ertl_seq_rect_Type1 :
177  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
178
179val ertl_seq_rect_Type0 :
180  'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
181
182val ertl_seq_inv_rect_Type4 :
183  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
184  -> 'a1
185
186val ertl_seq_inv_rect_Type3 :
187  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
188  -> 'a1
189
190val ertl_seq_inv_rect_Type2 :
191  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
192  -> 'a1
193
194val ertl_seq_inv_rect_Type1 :
195  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
196  -> 'a1
197
198val ertl_seq_inv_rect_Type0 :
199  ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
200  -> 'a1
201
202val ertl_seq_discr : ertl_seq -> ertl_seq -> __
203
204val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __
205
206val eRTL_uns : Joint.unserialized_params
207
208val eRTL : Joint.graph_params
209
210type ertl_program = Joint.joint_program
211
212val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq
213
214val byte_to_ertl_snd_argument__o__psd_argument_to_move_src : BitVector.byte -> unit
Note: See TracBrowser for help on using the repository browser.