source: extracted/set_adt.mli @ 2717

Last change on this file since 2717 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: 2.9 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open List
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29type 'x set
30
31type 'elt_type set0 =
32| Empty
33| Node of Nat.nat * 'elt_type set0 * 'elt_type * 'elt_type set0
34
35val set_rect_Type4 :
36  'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> 'a1
37  set0 -> 'a2
38
39val set_rect_Type3 :
40  'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> 'a1
41  set0 -> 'a2
42
43val set_rect_Type2 :
44  'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> 'a1
45  set0 -> 'a2
46
47val set_rect_Type1 :
48  'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> 'a1
49  set0 -> 'a2
50
51val set_rect_Type0 :
52  'a2 -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> 'a2 -> 'a2 -> 'a2) -> 'a1
53  set0 -> 'a2
54
55val set_inv_rect_Type4 :
56  'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
57  -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
58
59val set_inv_rect_Type3 :
60  'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
61  -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
62
63val set_inv_rect_Type2 :
64  'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
65  -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
66
67val set_inv_rect_Type1 :
68  'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
69  -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
70
71val set_inv_rect_Type0 :
72  'a1 set0 -> (__ -> 'a2) -> (Nat.nat -> 'a1 set0 -> 'a1 -> 'a1 set0 -> (__
73  -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
74
75val set_discr : 'a1 set0 -> 'a1 set0 -> __
76
77val set_jmdiscr : 'a1 set0 -> 'a1 set0 -> __
78
79val set_empty : 'a1 set0
80
81val set_size : 'a1 set0 -> Nat.nat
82
83val set_to_list : 'a1 set0 -> 'a1 List.list
84
85val set_insert : 'a1 -> 'a1 set0 -> 'a1 set0
86
87val set_remove : 'a1 -> 'a1 set0 -> 'a1 set0
88
89val set_member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool
90
91val set_forall : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool
92
93val set_exists : ('a1 -> Bool.bool) -> 'a1 set0 -> Bool.bool
94
95val set_filter : ('a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0
96
97val set_map : ('a1 -> 'a2) -> 'a1 set0 -> 'a2 set0
98
99val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set0 -> 'a2 -> 'a2
100
101val set_equal :
102  ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool
103
104val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0
105
106val set_is_empty : 'a1 set0 -> Bool.bool
107
108val set_singleton : 'a1 -> 'a1 set0
109
110val set_from_list : 'a1 List.list -> 'a1 set0
111
112val set_split :
113  ('a1 -> Bool.bool) -> 'a1 set0 -> ('a1 set0, 'a1 set0) Types.prod
114
115val set_subset :
116  ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool
117
118val set_subseteq :
119  ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool
120
121val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0
122
123val set_intersection :
124  ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> 'a1 set0
125
Note: See TracBrowser for help on using the repository browser.