forked from ucsd-progsys/liquidhaskell
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathSet.spec
60 lines (41 loc) · 2.79 KB
/
Set.spec
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
module spec Data.Set where
embed Data.Set.Set as Set_Set
// ----------------------------------------------------------------------------------------------
// -- | Logical Set Operators: Interpreted "natively" by the SMT solver -------------------------
// ----------------------------------------------------------------------------------------------
// union
measure Set_cup :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a)
// intersection
measure Set_cap :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a)
// difference
measure Set_dif :: (Data.Set.Set a) -> (Data.Set.Set a) -> (Data.Set.Set a)
// singleton
measure Set_sng :: a -> (Data.Set.Set a)
// emptiness test
measure Set_emp :: (Data.Set.Set a) -> GHC.Types.Bool
// empty set
measure Set_empty :: forall a. GHC.Types.Int -> (Data.Set.Set a)
// membership test
measure Set_mem :: a -> (Data.Set.Set a) -> GHC.Types.Bool
// inclusion test
measure Set_sub :: (Data.Set.Set a) -> (Data.Set.Set a) -> GHC.Types.Bool
// ---------------------------------------------------------------------------------------------
// -- | Refined Types for Data.Set Operations --------------------------------------------------
// ---------------------------------------------------------------------------------------------
isSubsetOf :: (GHC.Classes.Ord a) => x:(Data.Set.Set a) -> y:(Data.Set.Set a) -> {v:Bool | v <=> Set_sub x y}
member :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Set a) -> {v:Bool | v <=> Set_mem x xs}
null :: (GHC.Classes.Ord a) => xs:(Data.Set.Set a) -> {v:Bool | v <=> Set_emp xs}
empty :: {v:(Data.Set.Set a) | Set_emp v}
singleton :: x:a -> {v:(Data.Set.Set a) | v = (Set_sng x)}
insert :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Set a) -> {v:(Data.Set.Set a) | v = Set_cup xs (Set_sng x)}
delete :: (GHC.Classes.Ord a) => x:a -> xs:(Data.Set.Set a) -> {v:(Data.Set.Set a) | v = Set_dif xs (Set_sng x)}
union :: GHC.Classes.Ord a => xs:(Data.Set.Set a) -> ys:(Data.Set.Set a) -> {v:(Data.Set.Set a) | v = Set_cup xs ys}
intersection :: GHC.Classes.Ord a => xs:(Data.Set.Set a) -> ys:(Data.Set.Set a) -> {v:(Data.Set.Set a) | v = Set_cap xs ys}
difference :: GHC.Classes.Ord a => xs:(Data.Set.Set a) -> ys:(Data.Set.Set a) -> {v:(Data.Set.Set a) | v = Set_dif xs ys}
fromList :: GHC.Classes.Ord a => xs:[a] -> {v:Data.Set.Set a | v = listElts xs}
// ---------------------------------------------------------------------------------------------
// -- | The set of elements in a list ----------------------------------------------------------
// ---------------------------------------------------------------------------------------------
measure listElts :: [a] -> (Data.Set.Set a)
listElts([]) = {v | (Set_emp v)}
listElts(x:xs) = {v | v = Set_cup (Set_sng x) (listElts xs) }