source: extracted/joint_LTL_LIN.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: 5.9 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 registers_move =
108| From_acc of I8051.register * Types.unit0
109| To_acc of Types.unit0 * I8051.register
110| Int_to_reg of I8051.register * BitVector.byte
111| Int_to_acc of Types.unit0 * BitVector.byte
112
113val registers_move_rect_Type4 :
114  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
115  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
116  BitVector.byte -> 'a1) -> registers_move -> 'a1
117
118val registers_move_rect_Type5 :
119  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
120  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
121  BitVector.byte -> 'a1) -> registers_move -> 'a1
122
123val registers_move_rect_Type3 :
124  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
125  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
126  BitVector.byte -> 'a1) -> registers_move -> 'a1
127
128val registers_move_rect_Type2 :
129  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
130  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
131  BitVector.byte -> 'a1) -> registers_move -> 'a1
132
133val registers_move_rect_Type1 :
134  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
135  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
136  BitVector.byte -> 'a1) -> registers_move -> 'a1
137
138val registers_move_rect_Type0 :
139  (I8051.register -> Types.unit0 -> 'a1) -> (Types.unit0 -> I8051.register ->
140  'a1) -> (I8051.register -> BitVector.byte -> 'a1) -> (Types.unit0 ->
141  BitVector.byte -> 'a1) -> registers_move -> 'a1
142
143val registers_move_inv_rect_Type4 :
144  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
145  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
146  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
147  'a1) -> 'a1
148
149val registers_move_inv_rect_Type3 :
150  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
151  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
152  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
153  'a1) -> 'a1
154
155val registers_move_inv_rect_Type2 :
156  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
157  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
158  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
159  'a1) -> 'a1
160
161val registers_move_inv_rect_Type1 :
162  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
163  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
164  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
165  'a1) -> 'a1
166
167val registers_move_inv_rect_Type0 :
168  registers_move -> (I8051.register -> Types.unit0 -> __ -> 'a1) ->
169  (Types.unit0 -> I8051.register -> __ -> 'a1) -> (I8051.register ->
170  BitVector.byte -> __ -> 'a1) -> (Types.unit0 -> BitVector.byte -> __ ->
171  'a1) -> 'a1
172
173val registers_move_discr : registers_move -> registers_move -> __
174
175val registers_move_jmdiscr : registers_move -> registers_move -> __
176
177type ltl_lin_seq =
178| SAVE_CARRY
179| RESTORE_CARRY
180| LOW_ADDRESS of I8051.register * Graphs.label
181| HIGH_ADDRESS of I8051.register * Graphs.label
182
183val ltl_lin_seq_rect_Type4 :
184  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
185  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
186
187val ltl_lin_seq_rect_Type5 :
188  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
189  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
190
191val ltl_lin_seq_rect_Type3 :
192  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
193  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
194
195val ltl_lin_seq_rect_Type2 :
196  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
197  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
198
199val ltl_lin_seq_rect_Type1 :
200  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
201  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
202
203val ltl_lin_seq_rect_Type0 :
204  'a1 -> 'a1 -> (I8051.register -> Graphs.label -> 'a1) -> (I8051.register ->
205  Graphs.label -> 'a1) -> ltl_lin_seq -> 'a1
206
207val ltl_lin_seq_inv_rect_Type4 :
208  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
209  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
210  -> 'a1
211
212val ltl_lin_seq_inv_rect_Type3 :
213  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
214  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
215  -> 'a1
216
217val ltl_lin_seq_inv_rect_Type2 :
218  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
219  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
220  -> 'a1
221
222val ltl_lin_seq_inv_rect_Type1 :
223  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
224  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
225  -> 'a1
226
227val ltl_lin_seq_inv_rect_Type0 :
228  ltl_lin_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (I8051.register ->
229  Graphs.label -> __ -> 'a1) -> (I8051.register -> Graphs.label -> __ -> 'a1)
230  -> 'a1
231
232val ltl_lin_seq_discr : ltl_lin_seq -> ltl_lin_seq -> __
233
234val ltl_lin_seq_jmdiscr : ltl_lin_seq -> ltl_lin_seq -> __
235
236val ltl_lin_seq_labels : ltl_lin_seq -> Graphs.label List.list
237
238val lTL_LIN : Joint.unserialized_params
239
Note: See TracBrowser for help on using the repository browser.