source: extracted/lINToASM.mli @ 2773

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