source: extracted/registerSet.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.3 KB
Line 
1open Preamble
2
3open Exp
4
5open Extranat
6
7open Vector
8
9open Div_and_mod
10
11open Russell
12
13open Types
14
15open List
16
17open Util
18
19open FoldStuff
20
21open BitVector
22
23open Arithmetic
24
25open Jmeq
26
27open Bool
28
29open Hints_declaration
30
31open Core_notation
32
33open Pts
34
35open Logic
36
37open Relations
38
39open Nat
40
41open I8051
42
43open Order
44
45open Proper
46
47open PositiveMap
48
49open Deqsets
50
51open ErrorMessages
52
53open PreIdentifiers
54
55open Errors
56
57open Extralib
58
59open Setoids
60
61open Monad
62
63open Option
64
65open Lists
66
67open Positive
68
69open Identifiers
70
71open Registers
72
73type register_set = { rs_empty : __; rs_singleton : (I8051.register -> __);
74                      rs_fold : (__ -> (I8051.register -> __ -> __) -> __ ->
75                                __ -> __);
76                      rs_insert : (I8051.register -> __ -> __);
77                      rs_exists : (I8051.register -> __ -> Bool.bool);
78                      rs_union : (__ -> __ -> __);
79                      rs_subset : (__ -> __ -> Bool.bool);
80                      rs_to_list : (__ -> I8051.register List.list);
81                      rs_from_list : (I8051.register List.list -> __) }
82
83val register_set_rect_Type4 :
84  (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
85  -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
86  -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
87  I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
88  register_set -> 'a1
89
90val register_set_rect_Type5 :
91  (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
92  -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
93  -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
94  I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
95  register_set -> 'a1
96
97val register_set_rect_Type3 :
98  (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
99  -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
100  -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
101  I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
102  register_set -> 'a1
103
104val register_set_rect_Type2 :
105  (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
106  -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
107  -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
108  I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
109  register_set -> 'a1
110
111val register_set_rect_Type1 :
112  (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
113  -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
114  -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
115  I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
116  register_set -> 'a1
117
118val register_set_rect_Type0 :
119  (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
120  -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
121  -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
122  I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
123  register_set -> 'a1
124
125type rs_set
126
127val rs_empty : register_set -> __
128
129val rs_singleton : register_set -> I8051.register -> __
130
131val rs_fold0 :
132  register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1
133
134val rs_insert : register_set -> I8051.register -> __ -> __
135
136val rs_exists : register_set -> I8051.register -> __ -> Bool.bool
137
138val rs_union : register_set -> __ -> __ -> __
139
140val rs_subset : register_set -> __ -> __ -> Bool.bool
141
142val rs_to_list : register_set -> __ -> I8051.register List.list
143
144val rs_from_list : register_set -> I8051.register List.list -> __
145
146val register_set_inv_rect_Type4 :
147  register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
148  (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
149  __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
150  -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
151  List.list -> __) -> __ -> 'a1) -> 'a1
152
153val register_set_inv_rect_Type3 :
154  register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
155  (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
156  __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
157  -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
158  List.list -> __) -> __ -> 'a1) -> 'a1
159
160val register_set_inv_rect_Type2 :
161  register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
162  (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
163  __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
164  -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
165  List.list -> __) -> __ -> 'a1) -> 'a1
166
167val register_set_inv_rect_Type1 :
168  register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
169  (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
170  __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
171  -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
172  List.list -> __) -> __ -> 'a1) -> 'a1
173
174val register_set_inv_rect_Type0 :
175  register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
176  (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
177  __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
178  -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
179  List.list -> __) -> __ -> 'a1) -> 'a1
180
181val register_set_jmdiscr : register_set -> register_set -> __
182
183val rs_list_set_empty : I8051.register List.list
184
185val rs_list_set_singleton : I8051.register -> I8051.register List.list
186
187val rs_list_set_fold :
188  (I8051.register -> 'a1 -> 'a1) -> I8051.register List.list -> 'a1 -> 'a1
189
190val rs_list_set_insert :
191  I8051.register -> I8051.register List.list -> I8051.register List.list
192
193val rs_list_set_exists :
194  I8051.register -> I8051.register List.list -> Bool.bool
195
196val rs_list_set_union :
197  I8051.register List.list -> I8051.register List.list -> I8051.register
198  List.list
199
200val rs_list_set_subset :
201  I8051.register List.list -> I8051.register List.list -> Bool.bool
202
203val rs_list_set_from_list :
204  I8051.register List.list -> I8051.register List.list
205
206val register_list_set : register_set
207
Note: See TracBrowser for help on using the repository browser.