source: extracted/rTLToERTL.mli @ 2890

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

Everything extracted again.

File size: 3.8 KB
Line 
1open Preamble
2
3open Order
4
5open Proper
6
7open PositiveMap
8
9open Deqsets
10
11open ErrorMessages
12
13open PreIdentifiers
14
15open Errors
16
17open Extralib
18
19open Lists
20
21open Positive
22
23open Identifiers
24
25open Registers
26
27open Exp
28
29open Setoids
30
31open Monad
32
33open Option
34
35open Extranat
36
37open Vector
38
39open Div_and_mod
40
41open Russell
42
43open Types
44
45open List
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Arithmetic
54
55open Jmeq
56
57open Bool
58
59open Hints_declaration
60
61open Core_notation
62
63open Pts
64
65open Logic
66
67open Relations
68
69open Nat
70
71open I8051
72
73open RegisterSet
74
75open String
76
77open Sets
78
79open Listb
80
81open LabelledObjects
82
83open BitVectorTrie
84
85open Graphs
86
87open CostLabel
88
89open Hide
90
91open Integers
92
93open AST
94
95open Division
96
97open Z
98
99open BitVectorZ
100
101open Pointers
102
103open ByteValues
104
105open BackEndOps
106
107open Joint
108
109open RTL
110
111open ERTL
112
113open Deqsets_extra
114
115open State
116
117open Bind_new
118
119open BindLists
120
121open Blocks
122
123open TranslateUtils
124
125val save_hdws :
126  AST.ident List.list -> (Registers.register, I8051.register) Types.prod
127  List.list -> Joint.joint_seq List.list
128
129val restore_hdws :
130  AST.ident List.list -> (Joint.psd_argument, I8051.register) Types.prod
131  List.list -> Joint.joint_seq List.list
132
133val get_params_hdw :
134  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
135  List.list
136
137val get_param_stack :
138  AST.ident List.list -> Registers.register -> Registers.register ->
139  Registers.register -> Joint.joint_seq List.list
140
141val get_params_stack :
142  AST.ident List.list -> Registers.register -> Registers.register ->
143  Registers.register -> Registers.register List.list -> Joint.joint_seq
144  List.list
145
146val get_params :
147  AST.ident List.list -> Registers.register -> Registers.register ->
148  Registers.register -> Registers.register List.list -> Joint.joint_seq
149  List.list
150
151val save_return :
152  AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
153  List.list
154
155val assign_result : AST.ident List.list -> Joint.joint_seq List.list
156
157val epilogue :
158  AST.ident List.list -> Registers.register List.list -> Registers.register
159  -> Registers.register -> (Registers.register, I8051.register) Types.prod
160  List.list -> Joint.joint_seq List.list Types.sig0
161
162val prologue :
163  AST.ident List.list -> Registers.register List.list -> Registers.register
164  -> Registers.register -> Registers.register -> Registers.register ->
165  Registers.register -> (Registers.register, I8051.register) Types.prod
166  List.list -> (Registers.register, Joint.joint_seq List.list)
167  Bind_new.bind_new
168
169val set_params_hdw :
170  AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
171  List.list
172
173val set_param_stack :
174  AST.ident List.list -> Registers.register -> Registers.register ->
175  Joint.psd_argument -> Joint.joint_seq List.list
176
177val set_params_stack :
178  AST.ident List.list -> Joint.psd_argument List.list -> (Registers.register,
179  Joint.joint_seq List.list) Bind_new.bind_new
180
181val set_params :
182  AST.ident List.list -> Joint.psd_argument List.list -> (Registers.register,
183  Joint.joint_seq List.list) Bind_new.bind_new Types.sig0
184
185val fetch_result :
186  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
187  List.list Types.sig0
188
189val translate_step :
190  AST.ident List.list -> Graphs.label -> Joint.joint_step ->
191  Blocks.bind_step_block
192
193val translate_fin_step :
194  AST.ident List.list -> Registers.register List.list -> Registers.register
195  -> Registers.register -> (Registers.register, I8051.register) Types.prod
196  List.list -> Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block
197
198val allocate_regs :
199  ((Registers.register, I8051.register) Types.prod List.list ->
200  (Registers.register, 'a1) Bind_new.bind_new) -> (Registers.register, 'a1)
201  Bind_new.bind_new
202
203val translate_data :
204  AST.ident List.list -> Joint.joint_closed_internal_function ->
205  TranslateUtils.bound_b_graph_translate_data
206
207val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program
208
Note: See TracBrowser for help on using the repository browser.