source: driver/extracted/registerSet.mli @ 3106

Last change on this file since 3106 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.3 KB
Line 
1open Preamble
2
3open Exp
4
5open Setoids
6
7open Monad
8
9open Option
10
11open Extranat
12
13open Vector
14
15open Div_and_mod
16
17open Russell
18
19open Types
20
21open List
22
23open Util
24
25open FoldStuff
26
27open BitVector
28
29open Arithmetic
30
31open Jmeq
32
33open Bool
34
35open Hints_declaration
36
37open Core_notation
38
39open Pts
40
41open Logic
42
43open Relations
44
45open Nat
46
47open I8051
48
49open Order
50
51open Proper
52
53open PositiveMap
54
55open Deqsets
56
57open ErrorMessages
58
59open PreIdentifiers
60
61open Errors
62
63open Extralib
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.