0 | module Libraries.Data.List.Thin
 1 |
 2 | import Libraries.Data.NatSet
 3 |
 4 | %default total
 5 |
 6 | -- TODO implement:
 7 | -- Guillaume Allais: Builtin Types Viewed as Inductive Families
 8 | -- https://doi.org/10.48550/arXiv.2301.02194
 9 | public export
10 | data Thin : List a -> List a -> Type where
11 |   Refl : Thin xs xs
12 |   Drop : Thin xs ys -> Thin xs (y :: ys)
13 |   Keep : Thin xs ys -> Thin (x :: xs) (x :: ys)
14 |
15 | export
16 | none : {xs : List a} -> Thin [] xs
17 | none {xs = []} = Refl
18 | none {xs = _ :: _} = Drop none
19 |
20 | ||| Smart constructor. We should use this to maximise the length
21 | ||| of the Refl segment thus getting more short-circuiting behaviours
22 | export
23 | keep : Thin xs ys -> Thin (x :: xs) (x :: ys)
24 | keep Refl = Refl
25 | keep p = Keep p
26 |
27 | export
28 | keeps : (args : List a) -> Thin xs ys -> Thin (args ++ xs) (args ++ ys)
29 | keeps [] th = th
30 | keeps (x :: xs) th = Keep (keeps xs th)
31 |
32 | export
33 | fromNatSet : NatSet -> (xs : List a) -> (xs' ** Thin xs' xs)
34 | fromNatSet ns xs =
35 |   if isEmpty ns then (_ ** Refl) else go 0 xs
36 |   where
37 |     go : Nat -> (xs : List a) -> (xs' ** Thin xs' xs)
38 |     go i [] = (_ ** Refl)
39 |     go i (x :: xs)
40 |         = let (xs' ** th) = go (S i) xs in
41 |               if i `elem` ns
42 |                  then (xs' ** Drop th)
43 |                  else (x :: xs' ** Keep th)
44 |