Aelve Codesearch

grep over package repositories
Please provide a string to search for.
3+ characters are required.
Index updated 4 hours ago

total matches: more than 1000

Agda-2.6.0.1
29 matches
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs

-- | Directed graphs (can of course simulate undirected graphs).
--
--   Represented as adjacency maps in direction from source to target.
--
--   Each source node maps to an adjacency map of outgoing edges,
--   which is a map from target nodes to edges.
--
--   Listed time complexities are for the worst case (and possibly
--   amortised), with /n/ standing for the number of nodes in the
--   graph and /e/ standing for the number of edges. Comparisons,
--   predicates etc. are assumed to take constant time (unless

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
  , union, unionWith
  , unions, unionsWith
    -- * Transformation
  , mapWithEdge
  , transposeEdge, transpose
  , clean
  , removeNode, removeNodes
  , removeEdge
  , filterEdges

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
--   can be simulated by letting the edge type @e@ be a collection
--   type.
--
--   The graphs are represented as adjacency maps (adjacency lists,
--   but using finite maps instead of arrays and lists). This makes it
--   possible to compute a node's outgoing edges in logarithmic time
--   (/O(log n)/). However, computing the incoming edges may be more
--   expensive.
--
--   Note that neither the number of nodes nor the number of edges may

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
  }
  deriving Eq

-- The Functor instance for strict maps is the one for lazy maps, so a
-- custom Functor instance using strict map functions is used here.

instance Functor (Graph n) where
  fmap f = Graph . Map.map (Map.map f) . graph

-- | Internal invariant.

invariant :: Ord n => Graph n e -> Bool
invariant g =

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
  Set.isSubsetOf (targetNodes g) (nodes g)

instance (Ord n, Pretty n, Pretty e) => Pretty (Graph n e) where
  pretty g = vcat (concat $ map pretty' (Set.toAscList (nodes g)))
    where
    pretty' n = case edgesFrom g [n] of
      [] -> [pretty n]
      es -> map pretty es

instance (Ord n, Show n, Show e) => Show (Graph n e) where
  showsPrec _ g =
    showString "union (fromEdges " .
    shows (edges g) .

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
-- | Nodes with incoming edges. /O(n + e log n)/.

targetNodes :: Ord n => Graph n e -> Set n
targetNodes = Set.fromList . map target . edges

-- | Various kinds of nodes.

data Nodes n = Nodes
  { srcNodes :: Set n

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
--   nodes. /O(n log n)/.

fromNodes :: Ord n => [n] -> Graph n e
fromNodes ns = Graph $ Map.fromList $ map (, Map.empty) ns

-- | Constructs a completely disconnected graph containing the given
--   nodes. /O(n)/.

fromNodeSet :: Ord n => Set n -> Graph n e

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
------------------------------------------------------------------------
-- Transformation

-- | A variant of 'fmap' that provides extra information to the
-- function argument. /O(n + e)/.

mapWithEdge :: (Edge n e -> e') -> Graph n e -> Graph n e'
mapWithEdge f (Graph g) = Graph $ flip Map.mapWithKey g $ \ s m ->
  flip Map.mapWithKey m $ \ t e -> f (Edge s t e)

-- | Reverses an edge. /O(1)/.

transposeEdge :: Edge n e -> Edge n e
transposeEdge (Edge s t e) = Edge t s e

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs

transpose :: Ord n => Graph n e -> Graph n e
transpose g =
  fromEdges (map transposeEdge (edges g))
    `union`
  fromNodeSet (isolatedNodes g)

-- | Removes 'null' edges. /O(n + e)/.


            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
-- | Removes 'null' edges. /O(n + e)/.

clean :: Null e => Graph n e -> Graph n e
clean = Graph . Map.map (Map.filter (not . null)) . graph

-- | @removeNodes ns g@ removes the nodes in @ns@ (and all
-- corresponding edges) from @g@. /O((n + e) log |@ns@|)/.

removeNodes :: Ord n => Set n -> Graph n e -> Graph n e

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
-- corresponding edges) from @g@. /O((n + e) log |@ns@|)/.

removeNodes :: Ord n => Set n -> Graph n e -> Graph n e
removeNodes ns (Graph g) = Graph (Map.mapMaybeWithKey remSrc g)
  where
  remSrc s m
    | Set.member s ns = Nothing
    | otherwise       =
        Just (Map.filterWithKey (\t _ -> not (Set.member t ns)) m)

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
filterEdges :: (Edge n e -> Bool) -> Graph n e -> Graph n e
filterEdges f =
  Graph .
  Map.mapWithKey (\s ->
    Map.filterWithKey (\t l ->
      f (Edge { source = s, target = t, label = l }))) .
  graph

-- | Unzips the graph. /O(n + e)/.

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs

-- | Unzips the graph. /O(n + e)/.

-- This is a naive implementation that uses fmap.

unzip :: Graph n (e, e') -> (Graph n e, Graph n e')
unzip g = (fst <$> g, snd <$> g)

-- | @composeWith times plus g g'@ finds all edges

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
  Ord n =>
  (c -> d -> e) -> (e -> e -> e) ->
  Graph n c -> Graph n d -> Graph n e
composeWith times plus (Graph g) (Graph g') = Graph (Map.map comp g)
  where
  comp m = Map.fromListWith plus
    [ (u, c `times` d)
    | (t, c) <- Map.assocs m
    , m'     <- maybeToList (Map.lookup t g')

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
sccs' :: Ord n => Graph n e -> [Graph.SCC n]
sccs' g =
  Graph.stronglyConnComp
    [ (n, n, map target (edgesFrom g [n]))
    | n <- Set.toList (nodes g)
    ]

-- | The graph's strongly connected components, in reverse topological
-- order.

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
-- order.

sccs :: Ord n => Graph n e -> [[n]]
sccs = map Graph.flattenSCC . sccs'

-- | SCC DAGs.
--
-- The maps map SCC indices to and from SCCs/nodes.

data DAG n = DAG
  { dagGraph        :: Graph.Graph
  , dagComponentMap :: IntMap (Graph.SCC n)
  , dagNodeMap      :: Map n Int

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
    Just i  -> i

  componentMap :: IntMap (Graph.SCC n)
  componentMap = IntMap.fromList (map (mapFst convertInt) components)

  secondNodeMap :: Map n Int
  secondNodeMap = Map.map convertInt firstNodeMap

-- | Constructs a DAG containing the graph's strongly connected
-- components.

sccDAG :: Ord n => Graph n e -> DAG n

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
------------------------------------------------------------------------
-- Reachability

-- | @reachableFrom g n@ is a map containing all nodes reachable from
-- @n@ in @g@. For each node a simple path to the node is given, along
-- with its length (the number of edges). The paths are as short as
-- possible (in terms of the number of edges).
--
-- Precondition: @n@ must be a node in @g@. The number of nodes in the

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
reachableFromInternal ::
  Ord n => Graph n e -> Set n -> Map n (Int, [Edge n e])
reachableFromInternal g ns =
  bfs (SQ.fromList (map (, BQ.empty) (Set.toList ns))) Map.empty
  where
  bfs !q !map = case SQ.lview q of
    Nothing          -> map
    Just ((u, p), q) ->
      if u `Map.member` map
      then bfs q map
      else bfs (foldr SQ.rcons q
                      [ (v, BQ.rcons (Edge u v e) p)
                      | (v, e) <- neighbours u g
                      ])
               (let n = BQ.size p in

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
                      | (v, e) <- neighbours u g
                      ])
               (let n = BQ.size p in
                n `seq` Map.insert u (n, BQ.toList p) map)

-- | @walkSatisfying every some g from to@ determines if there is a
-- walk from @from@ to @to@ in @g@, in which every edge satisfies the
-- predicate @every@, and some edge satisfies the predicate @some@. If
-- there are several such walks, then a shortest one (in terms of the

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
  Graph n e -> n -> n -> Maybe [Edge n e]
walkSatisfying every some g from to =
  case
    [ (l1 + l2, p1 ++ [e] ++ map transposeEdge (reverse p2))
    | e <- everyEdges
    , some e
    , (l1, p1) <- maybeToList (Map.lookup (source e) fromReaches)
    , (l2, p2) <- maybeToList (Map.lookup (target e) reachesTo)
    ] of

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
  fromReaches = reachableFrom (fromEdges everyEdges) from

  reachesTo =
    reachableFrom (fromEdges (map transposeEdge everyEdges)) to

------------------------------------------------------------------------
-- Transitive closure

-- | Transitive closure ported from "Agda.Termination.CallGraph".

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
--   Relatively efficient, see Issue 1560.

complete :: (Eq e, Null e, SemiRing e, Ord n) => Graph n e -> Graph n e
complete g = repeatWhile (mapFst (not . discrete) . combineNewOld' g) g
  where
    combineNewOld' new old = unzip $ unionWith comb new' old'
      where
      -- The following procedure allows us to check if anything new happened:
      -- Pair the composed graphs with an empty graph.

            
src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs
  toGraph (foldr step initialMatrix nodeIndices)
  where
  indicesAndNodes = zip [1..] $ Set.toList $ nodes g
  nodeMap         = Map.fromList $ map swap indicesAndNodes
  indexMap        = Map.fromList            indicesAndNodes

  noNodes      = Map.size nodeMap
  nodeIndices  = [1 .. noNodes]
  matrixBounds = ((1, 1), (noNodes, noNodes))

            
src/full/Agda/Utils/Parser/MemoisedCPS.hs
    p input i $ \j x -> unP (f x) input j k

instance Functor (Parser k r tok) where
  fmap f (P p) = P $ \input i k ->
    p input i $ \i -> k i . f

instance Applicative (Parser k r tok) where
  pure x        = P $ \_ i k -> k i x
  P p1 <*> P p2 = P $ \input i k ->

            
src/full/Agda/Utils/Parser/MemoisedCPS.hs
    let alter j zero f m =
          IntMap.alter (Just . f . fromMaybe zero) j m

        lookupTable   = fmap (\m -> Map.lookup key =<<
                                    IntMap.lookup i m) get
        insertTable v = modify' $ alter i Map.empty (Map.insert key v)

    v <- lookupTable
    case v of

            
src/full/Agda/Utils/Parser/MemoisedCPS.hs
        unP p input i $ \j r -> do
          ~(Just (Value rs ks)) <- lookupTable
          insertTable (Value (alter j [] (r :) rs) ks)
          concat <$> mapM (\k -> k j r) ks  -- See note [Reverse ks?].
      Just (Value rs ks) -> do
        insertTable (Value rs (k : ks))
        concat . concat <$>
          mapM (\(i, rs) -> mapM (k i) rs) (IntMap.toList rs)

-- [Reverse ks?]
--
-- If ks were reversed, then the code would be productive for some
-- infinitely ambiguous grammars, including S ∷= S | ε. However, in

            
src/full/Agda/Utils/Parser/MemoisedCPS.hs
          <$> docs p)

instance Functor (ParserWithGrammar k r tok) where
  fmap f p = pg (fmap f (parser p)) (docs p)

instance Applicative (ParserWithGrammar k r tok) where
  pure x    = pg (pure x) (return ("ε", atomP))
  p1 <*> p2 =
    pg (parser p1 <*> parser p2)

            
src/full/Agda/Utils/Parser/MemoisedCPS.hs
      $+$
    nest 2 (foldr1 ($+$) $
      "where" :
      map (\(k, d) -> fst (prettyKey k) <+> "∷=" <+>
                        maybe __IMPOSSIBLE__ fst d)
          (Map.toList ds))
    where
    ((d, _), ds) = runState (docs p) Map.empty

            
Allure-0.8.3.0
1 matches
GameDefinition/Content/ModeKind.hs
  , rosterAlly = [] }

-- Exactly one scout gets a sight boost, to help the aggressor, because he uses
-- the scout for initial attack, while camper (on big enough maps)
-- can't guess where the attack would come and so can't position his single
-- scout to counter the stealthy advance.
rosterShootout = Roster
  { rosterList = [ ( playerHero { fcanEscape = False
                                , fhiCondPoly = hiDweller }