35 open Hints_declaration
73 type register_set = { rs_empty : __; rs_singleton : (I8051.register -> __);
74 rs_fold : (__ -> (I8051.register -> __ -> __) -> __ ->
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 -> __) }
83 val 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) ->
90 val 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) ->
97 val 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) ->
104 val 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) ->
111 val 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) ->
118 val 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) ->
127 val rs_empty : register_set -> __
129 val rs_singleton : register_set -> I8051.register -> __
132 register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1
134 val rs_insert : register_set -> I8051.register -> __ -> __
136 val rs_exists : register_set -> I8051.register -> __ -> Bool.bool
138 val rs_union : register_set -> __ -> __ -> __
140 val rs_subset : register_set -> __ -> __ -> Bool.bool
142 val rs_to_list : register_set -> __ -> I8051.register List.list
144 val rs_from_list : register_set -> I8051.register List.list -> __
146 val 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
153 val 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
160 val 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
167 val 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
174 val 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
181 val register_set_jmdiscr : register_set -> register_set -> __
183 val rs_list_set_empty : I8051.register List.list
185 val rs_list_set_singleton : I8051.register -> I8051.register List.list
187 val rs_list_set_fold :
188 (I8051.register -> 'a1 -> 'a1) -> I8051.register List.list -> 'a1 -> 'a1
190 val rs_list_set_insert :
191 I8051.register -> I8051.register List.list -> I8051.register List.list
193 val rs_list_set_exists :
194 I8051.register -> I8051.register List.list -> Bool.bool
196 val rs_list_set_union :
197 I8051.register List.list -> I8051.register List.list -> I8051.register
200 val rs_list_set_subset :
201 I8051.register List.list -> I8051.register List.list -> Bool.bool
203 val rs_list_set_from_list :
204 I8051.register List.list -> I8051.register List.list
206 val register_list_set : register_set