source: extracted/rTLToERTL.mli @ 2746

Last change on this file since 2746 was 2730, checked in by sacerdot, 7 years ago

Exported again.

File size: 3.7 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 Setoids
20
21open Monad
22
23open Option
24
25open Lists
26
27open Positive
28
29open Identifiers
30
31open Registers
32
33open Exp
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 Graphs
84
85open BitVectorTrie
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 List.list -> (Registers.register,
143  Joint.joint_seq List.list) Bind_new.bind_new
144
145val get_params :
146  AST.ident List.list -> Registers.register List.list -> (Registers.register,
147  Joint.joint_seq) BindLists.bind_list
148
149val save_return :
150  AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
151  List.list
152
153val assign_result : AST.ident List.list -> Joint.joint_seq List.list
154
155val epilogue :
156  AST.ident List.list -> Registers.register List.list -> Registers.register
157  -> Registers.register -> (Registers.register, I8051.register) Types.prod
158  List.list -> Joint.joint_seq List.list Types.sig0
159
160val prologue :
161  AST.ident List.list -> Registers.register List.list -> Registers.register
162  -> Registers.register -> (Registers.register, I8051.register) Types.prod
163  List.list -> (Registers.register, Joint.joint_seq List.list)
164  Bind_new.bind_new
165
166val set_params_hdw :
167  AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
168  List.list
169
170val set_param_stack :
171  AST.ident List.list -> Registers.register -> Registers.register ->
172  Joint.psd_argument -> Joint.joint_seq List.list
173
174val set_params_stack :
175  AST.ident List.list -> Joint.psd_argument List.list -> (Registers.register,
176  Joint.joint_seq List.list) Bind_new.bind_new
177
178val set_params :
179  AST.ident List.list -> Joint.psd_argument List.list -> (Registers.register,
180  Joint.joint_seq List.list) Bind_new.bind_new Types.sig0
181
182val fetch_result :
183  AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
184  List.list Types.sig0
185
186val translate_step :
187  AST.ident List.list -> Graphs.label -> Joint.joint_step ->
188  Blocks.bind_step_block
189
190val translate_fin_step :
191  AST.ident List.list -> Registers.register List.list -> Registers.register
192  -> Registers.register -> (Registers.register, I8051.register) Types.prod
193  List.list -> Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block
194
195val allocate_regs :
196  (Registers.register -> Registers.register -> (Registers.register,
197  I8051.register) Types.prod List.list -> (Registers.register, 'a1)
198  Bind_new.bind_new) -> (Registers.register, 'a1) Bind_new.bind_new
199
200val translate_data :
201  AST.ident List.list -> Joint.joint_closed_internal_function ->
202  (Registers.register, TranslateUtils.b_graph_translate_data)
203  Bind_new.bind_new
204
205val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program
206
Note: See TracBrowser for help on using the repository browser.