
  0 | module Libraries.Data.VarSet
  1 | 
  2 | -- If we had defined these functions in the same file as `VarSet`,
  3 | -- we would see a lot of unsolved metas because `VarSet` computes
  4 | -- away to `NatSet`.
  5 | -- Hence the split between (unsafe, bit-manipulating) `.Core`
  6 | -- primitive definitions and type-safe derived notions
  7 | 
  8 | import Core.Name.Scoped
  9 | import Core.TT.Var
 10 | 
 11 | import Libraries.Data.List.SizeOf
 12 | 
 13 | import public Libraries.Data.VarSet.Core as VarSet
 14 | 
 15 | %default total
 16 | 
 17 | export %inline
 18 | singleton : Var vs -> VarSet vs
 19 | singleton v = insert v Core.empty
 20 | 
 21 | export %inline
 22 | append : SizeOf inner -> VarSet inner -> VarSet outer ->
 23 |          VarSet (inner ++ outer)
 24 | append p inn out = union (embed {tm = VarSet} inn) (weakenNs {tm = VarSet} p out)
 25 | 
 26 | export
 27 | fromVarSet : (vars : Scope) -> VarSet vars -> (newvars ** Thin newvars vars)
 28 | fromVarSet [] xs = (Scope.empty ** Refl)
 29 | fromVarSet (n :: ns) xs =
 30 |     let (_ ** svs) = fromVarSet ns (VarSet.dropFirst xs) in
 31 |     if first `VarSet.elem` xs
 32 |       then (_ ** Keep svs)
 33 |       else (_ ** Drop svs)
 34 |