0 | module Libraries.Data.VarSet.Core
 1 |
 2 | import Data.Bits
 3 |
 4 | import Libraries.Data.NatSet
 5 |
 6 | import Core.Name.Scoped
 7 | import Core.TT.Var
 8 |
 9 | import Libraries.Data.List.SizeOf
10 |
11 | %default total
12 |
13 | export
14 | VarSet : Scoped
15 | VarSet vars = NatSet
16 |
17 | export %inline
18 | empty : VarSet vs
19 | empty = NatSet.empty
20 |
21 | export %inline
22 | elem : Var vs -> VarSet vs -> Bool
23 | elem (MkVar {varIdx} _) = NatSet.elem varIdx
24 |
25 | export %inline
26 | isEmpty : VarSet vs -> Bool
27 | isEmpty = NatSet.isEmpty
28 |
29 | export %inline
30 | size : VarSet vs -> Nat
31 | size = NatSet.size
32 |
33 | export %inline
34 | insert : Var vs -> VarSet vs -> VarSet vs
35 | insert (MkVar {varIdx} _) = NatSet.insert varIdx
36 |
37 | export %inline
38 | delete : Var vs -> VarSet vs -> VarSet vs
39 | delete (MkVar {varIdx} _) = NatSet.delete varIdx
40 |
41 | export %inline
42 | full : SizeOf vs -> VarSet vs
43 | full p = NatSet.allLessThan p.size
44 |
45 | export %inline
46 | intersection : VarSet vs -> VarSet vs -> VarSet vs
47 | intersection = NatSet.intersection
48 |
49 | export %inline
50 | union : VarSet vs -> VarSet vs -> VarSet vs
51 | union = NatSet.union
52 |
53 | export %inline %unsafe
54 | unsafeToList : VarSet vs -> List (Var vs)
55 | unsafeToList = believe_me NatSet.toList
56 |
57 | export %inline
58 | toList : {vs : Scope} -> VarSet vs -> List (Var vs)
59 | toList = mapMaybe (`isDeBruijn` vs) . NatSet.toList
60 |
61 | -- Pop the zero (whether or not in the set) and shift all the
62 | -- other positions by -1 (useful when coming back from under
63 | -- a binder)
64 | export %inline
65 | dropFirst : VarSet (v :: vs) -> VarSet vs
66 | dropFirst = NatSet.popZ
67 |
68 | export %inline
69 | dropInner : SizeOf inner -> VarSet (inner ++ vs) -> VarSet vs
70 | dropInner p = NatSet.popNs p.size
71 |
72 | export %hint
73 | varSetFreelyEmbeddable : FreelyEmbeddable VarSet
74 | varSetFreelyEmbeddable = MkFreelyEmbeddable id
75 |
76 | export %hint
77 | varSetWeaken : Weaken VarSet
78 | varSetWeaken = MkWeaken NatSet.addZ (\ inn, vs => cast (cast {to = Integer} vs `shiftL` inn.size))
79 |