source: extracted/lINToASM.mli @ 2746

Last change on this file since 2746 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: 6.5 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Relations
12
13open Nat
14
15open Hints_declaration
16
17open Core_notation
18
19open Pts
20
21open Logic
22
23open Types
24
25open List
26
27open Util
28
29open Extranat
30
31open Vector
32
33open FoldStuff
34
35open BitVector
36
37open BitVectorTrie
38
39open BitVectorTrieSet
40
41open String
42
43open Sets
44
45open Listb
46
47open LabelledObjects
48
49open Graphs
50
51open I8051
52
53open Order
54
55open Registers
56
57open CostLabel
58
59open Hide
60
61open Proper
62
63open PositiveMap
64
65open Deqsets
66
67open ErrorMessages
68
69open PreIdentifiers
70
71open Errors
72
73open Extralib
74
75open Setoids
76
77open Monad
78
79open Option
80
81open Lists
82
83open Identifiers
84
85open Integers
86
87open AST
88
89open Division
90
91open Exp
92
93open Arithmetic
94
95open Positive
96
97open Z
98
99open BitVectorZ
100
101open Pointers
102
103open ByteValues
104
105open BackEndOps
106
107open Joint
108
109open Joint_LTL_LIN
110
111open LIN
112
113open ASM
114
115open State
116
117type aSM_universe = { id_univ : Identifiers.universe;
118                      current_funct : AST.ident;
119                      ident_map : ASM.identifier0 Identifiers.identifier_map;
120                      label_map : ASM.identifier0 Identifiers.identifier_map
121                                  Identifiers.identifier_map;
122                      address_map : BitVector.word Identifiers.identifier_map }
123
124val aSM_universe_rect_Type4 :
125  AST.ident List.list -> (Identifiers.universe -> AST.ident ->
126  ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
127  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
128  Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
129
130val aSM_universe_rect_Type5 :
131  AST.ident List.list -> (Identifiers.universe -> AST.ident ->
132  ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
133  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
134  Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
135
136val aSM_universe_rect_Type3 :
137  AST.ident List.list -> (Identifiers.universe -> AST.ident ->
138  ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
139  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
140  Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
141
142val aSM_universe_rect_Type2 :
143  AST.ident List.list -> (Identifiers.universe -> AST.ident ->
144  ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
145  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
146  Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
147
148val aSM_universe_rect_Type1 :
149  AST.ident List.list -> (Identifiers.universe -> AST.ident ->
150  ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
151  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
152  Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
153
154val aSM_universe_rect_Type0 :
155  AST.ident List.list -> (Identifiers.universe -> AST.ident ->
156  ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
157  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
158  Identifiers.identifier_map -> __ -> 'a1) -> aSM_universe -> 'a1
159
160val id_univ : AST.ident List.list -> aSM_universe -> Identifiers.universe
161
162val current_funct : AST.ident List.list -> aSM_universe -> AST.ident
163
164val ident_map :
165  AST.ident List.list -> aSM_universe -> ASM.identifier0
166  Identifiers.identifier_map
167
168val label_map :
169  AST.ident List.list -> aSM_universe -> ASM.identifier0
170  Identifiers.identifier_map Identifiers.identifier_map
171
172val address_map :
173  AST.ident List.list -> aSM_universe -> BitVector.word
174  Identifiers.identifier_map
175
176val aSM_universe_inv_rect_Type4 :
177  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
178  -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
179  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
180  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
181
182val aSM_universe_inv_rect_Type3 :
183  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
184  -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
185  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
186  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
187
188val aSM_universe_inv_rect_Type2 :
189  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
190  -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
191  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
192  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
193
194val aSM_universe_inv_rect_Type1 :
195  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
196  -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
197  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
198  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
199
200val aSM_universe_inv_rect_Type0 :
201  AST.ident List.list -> aSM_universe -> (Identifiers.universe -> AST.ident
202  -> ASM.identifier0 Identifiers.identifier_map -> ASM.identifier0
203  Identifiers.identifier_map Identifiers.identifier_map -> BitVector.word
204  Identifiers.identifier_map -> __ -> __ -> 'a1) -> 'a1
205
206val aSM_universe_jmdiscr :
207  AST.ident List.list -> aSM_universe -> aSM_universe -> __
208
209val new_ASM_universe : Joint.joint_program -> aSM_universe
210
211val identifier_of_label :
212  AST.ident List.list -> Graphs.label -> ASM.identifier0
213  Monad.smax_def__o__monad
214
215val identifier_of_ident :
216  AST.ident List.list -> AST.ident -> ASM.identifier0
217  Monad.smax_def__o__monad
218
219val start_funct_translation :
220  AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod ->
221  Types.unit0 Monad.smax_def__o__monad
222
223val address_of_ident :
224  __ List.list -> __ -> ASM.subaddressing_mode Monad.smax_def__o__monad
225
226val aSM_fresh :
227  AST.ident List.list -> ASM.identifier0 Monad.smax_def__o__monad
228
229val register_address : I8051.register -> ASM.subaddressing_mode
230
231val vector_cast :
232  Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector
233
234val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode
235
236type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj
237
238val data_of_int : BitVector.byte -> ASM.addressing_mode
239
240val data16_of_int : Nat.nat -> ASM.addressing_mode
241
242val accumulator_address : ASM.addressing_mode
243
244val asm_other_bit : ASM.addressing_mode
245
246val translate_statements :
247  AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction
248  Monad.smax_def__o__monad
249
250val build_translated_statement : AST.ident List.list -> lin_statement -> __
251
252val translate_code : AST.ident List.list -> lin_statement List.list -> __
253
254val translate_fun_def :
255  AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __
256
257val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program
258
Note: See TracBrowser for help on using the repository browser.