0 | ||| WIP: same as Data.List.Quantifiers but for lazy lists
 1 |
 2 | module Data.List.Lazy.Quantifiers
 3 |
 4 | import Data.DPair
 5 | import Data.List.Lazy
 6 |
 7 | %default total
 8 |
 9 | namespace Any
10 |
11 |   -- Note: it is crucial here that we mark `xs` as `Lazy`, otherwise Idris
12 |   --  will happily use `Delay` in the return index and give us a badly-behaved
13 |   -- family!
14 |   public export
15 |   data Any : (p : a -> Type) -> (xs : LazyList a) -> Type where
16 |     Here  : {0 xs : Lazy (LazyList a)} -> p x -> Any p (x :: xs)
17 |     There : {0 xs : Lazy (LazyList a)} -> Any p xs -> Any p (x :: xs)
18 |
19 |   public export
20 |   toExists : Any p xs -> Exists p
21 |   toExists (Here prf) = Evidence _ prf
22 |   toExists (There p) = toExists p
23 |
24 |   public export
25 |   toDPair : {xs : LazyList a} -> Any p xs -> DPair a p
26 |   toDPair (Here prf) = (_ ** prf)
27 |   toDPair (There p) = toDPair p
28 |
29 |   export
30 |   Uninhabited (Any p Nil) where
31 |     uninhabited (Here _) impossible
32 |     uninhabited (There _) impossible
33 |
34 |   export
35 |   {0 p : a -> Type} -> Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p $ x::xs) where
36 |     uninhabited (Here y) = uninhabited y
37 |     uninhabited (There y) = uninhabited y
38 |
39 |   ||| Modify the property given a pointwise function
40 |   export
41 |   mapProperty : (f : {0 x : a} -> p x -> q x) -> Any p l -> Any q l
42 |   mapProperty f (Here p) = Here (f p)
43 |   mapProperty f (There p) = There (mapProperty f p)
44 |
45 |   ||| Given a decision procedure for a property, determine if an element of a
46 |   ||| list satisfies it.
47 |   |||
48 |   ||| @ p the property to be satisfied
49 |   ||| @ dec the decision procedure
50 |   ||| @ xs the list to examine
51 |   public export
52 |   any : (dec : (x : a) -> Dec (p x)) -> (xs : LazyList a) -> Dec (Any p xs)
53 |   any _ Nil = No uninhabited
54 |   any p (x::xs) with (p x)
55 |     any p (x::xs) | Yes prf = Yes (Here prf)
56 |     any p (x::xs) | No ctra =
57 |       case any p xs of
58 |         Yes prf' => Yes (There prf')
59 |         No ctra' => No $ \case
60 |           Here px => ctra px
61 |           There pxs => ctra' pxs
62 |
63 |   public export
64 |   pushOut : Functor p => Any (p . q) xs -> p $ Any q xs
65 |   pushOut @{fp} (Here v)  = map @{fp} Here v
66 |   pushOut @{fp} (There n) = map @{fp} There $ pushOut n
67 |