0 | module Data.Collections.Analysis
  1 |
  2 | import Control.Monad.State
  3 |
  4 | import Data.Fin.Map
  5 | import Data.Fin.Set
  6 | import Data.Fin.ToFin
  7 | import Data.List1
  8 | import Data.SortedSet.Extra
  9 | import Data.Vect.Dependent
 10 | import Data.Vect.Extra
 11 |
 12 | import Syntax.IHateParens
 13 | import Syntax.Monad.Logic
 14 |
 15 | %default total
 16 |
 17 | --------------------------------
 18 | --- Transitive clojure stuff ---
 19 | --------------------------------
 20 |
 21 | export covering
 22 | transitiveClosureM : Monad m => Eq a => (a -> m $ List a) -> List a -> m $ List a
 23 | transitiveClosureM f xs = tr xs xs where
 24 |   tr : (curr : List a) -> (new : List a) -> m $ List a
 25 |   tr curr [] = pure curr
 26 |   tr curr st = do
 27 |     next <- join <$> for st f
 28 |     let new = filter (not . (`elem` curr)) next
 29 |     tr (curr ++ new) new
 30 |
 31 | export covering
 32 | holdsOnAnyInTrCl : Monad m => Eq a => (a -> Bool) -> (a -> m $ List a) -> List a -> m Bool
 33 | holdsOnAnyInTrCl prop f xs = pure (any prop xs) || tr xs xs where
 34 |   tr : (curr : List a) -> (new : List a) -> m Bool
 35 |   tr curr [] = pure False
 36 |   tr curr st = do
 37 |     next <- join <$> for st f
 38 |     let new = filter (not . (`elem` curr)) next
 39 |     pure (any prop new) || tr (curr ++ new) new
 40 |
 41 | ---------------------------------------------------
 42 | --- Splitting and rejoining `Either`'ed `Vect`s ---
 43 | ---------------------------------------------------
 44 |
 45 | -- Returns also original positions of `Left`'s
 46 | export
 47 | partitionEithersPos : {n : _} -> Vect n (Either a b) -> (List a, List b, FinSet n)
 48 | partitionEithersPos = map @{Compose} fromList . p where
 49 |   p : forall n. Vect n (Either a b) -> (List a, List b, List $ Fin n)
 50 |   p []        = ([], [], empty)
 51 |   p (ab::abs) = let (as, bs, lefts) = p abs
 52 |                     lefts = FS <$> lefts
 53 |                 in case ab of
 54 |                   Left  a => (a::as,    bs, FZ::lefts)
 55 |                   Right b => (   as, b::bs,     lefts)
 56 |
 57 | export
 58 | joinEithersPos : (as : List a) -> (bs : List b) -> FinSet (as.length + bs.length) -> Maybe $ Vect (as.length + bs.length) $ Either a b
 59 | joinEithersPos as bs lefts =
 60 |   evalState (as, bs) $ for @{Compose} range $ \idx => if contains idx lefts
 61 |     then do
 62 |       (x::as, bs) <- get
 63 |         | ([], _) => pure $ Nothing
 64 |       put (as, bs)
 65 |       pure $ Just $ Left x
 66 |     else do
 67 |       (as, x::bs) <- get
 68 |         | (_, []) => pure $ Nothing
 69 |       put (as, bs)
 70 |       pure $ Just $ Right x
 71 |
 72 | -------------------------------
 73 | --- Manupulations with sets ---
 74 | -------------------------------
 75 |
 76 | export
 77 | disjointDepSets : {n : _} -> (rawDeps : DVect n $ FinSet . Fin.finToNat) -> (givs : FinSet n) -> List $ FinSet n
 78 | disjointDepSets rawDeps givs = do
 79 |
 80 |   -- For each argument calculate the minimal index of its dependency (itself, if no dependencies)
 81 |   let minDeps = flip mapPreI rawDeps $ \i, pre => maybe last FS . leftMost . (`difference` fit givs)
 82 |
 83 |   -- Get rid of dependent vector, weaken indices bounds
 84 |   let minDeps = downmap (weakenToSuper {i=FS _}) minDeps
 85 |
 86 |   -- Reverse the map, i.e. for each minimal index get the set of arguments that depend on it
 87 |   let minDeps : FinMap .| S n .| FinSet n :=
 88 |     concatMap .| uncurry singleton .| mapSnd singleton <$> toListI minDeps
 89 |
 90 |   -- Acquire a list of disjoint sets, which in each set all args dependent somehow, but args from different susets are independent
 91 |   Prelude.toList minDeps
 92 |
 93 | ---------------------
 94 | --- Combinatorics ---
 95 | ---------------------
 96 |
 97 | public export
 98 | combinations : Vect n (List1 a) -> List1 (Vect n a)
 99 | combinations l = map (rewrite plusZeroRightNeutral n in reverse) $ go l $ Nil:::[] where
100 |   go : Vect m (List1 a) -> List1 (Vect k a) -> List1 (Vect (m + k) a)
101 |   go           Nil       rss = rss
102 |   go {m = S m} (xs::xss) rss = rewrite plusSuccRightSucc m k in
103 |     go xss $ join $ map (\x => map (\rs => x :: rs) rss) xs
104 |
105 | export
106 | permutations : Ord a => SortedSet a -> List1 $ List a
107 | permutations s = case fromList s.asList of
108 |   Nothing => pure []
109 |   Just ss => do
110 |     e  <- ss
111 |     es <- permutations $ assert_smaller s $ delete e s
112 |     pure $ e :: es
113 |
114 | export
115 | permutationsFin : {n : _} -> FinSet n -> List1 $ List $ Fin n
116 | permutationsFin s = case fromList s.asList of
117 |   Nothing => pure []
118 |   Just ss => do
119 |     e  <- ss
120 |     es <- permutationsFin $ assert_smaller s $ delete e s
121 |     pure $ e :: es
122 |
123 | public export
124 | permutations' : Ord a => SortedSet a -> List $ List a
125 | permutations' = forget . permutations
126 |
127 | export
128 | indepPermutations : {n : _} -> (independencyGroups : List $ FinSet n) -> FinSet n -> List1 $ List $ Fin n
129 | indepPermutations groups s = map concat $ for groups $ permutationsFin . intersection s
130 |
131 | public export %inline
132 | indepPermutations' : {n : _} -> (independencyGroups : List $ FinSet n) -> FinSet n -> List $ List $ Fin n
133 | indepPermutations' = forget .: indepPermutations
134 |