Aelve Codesearch

grep over package repositories
Please provide a string to search for.
3+ characters are required.
Index updated just now

total matches: more than 1000

ADPfusion-0.5.2.2
14 matches
ADP/Fusion/Core/TH/Backtrack.hs
-- we have that @x ~ r@.

buildLeftType :: Name -> (Name, Name, Name) -> (Name, Name) -> [TyVarBndr] -> Type
buildLeftType tycon (m, x, r) (mL, xL) = foldl AppT (ConT tycon) . map (VarT . go)
  where go (PlainTV z)
          | z == m        = mL  -- correct monad name
          | z == x        = xL  -- point to new x type
          | z == r        = xL  -- stream and return type are the same
          | otherwise     = z   -- everything else can stay as is

            
ADP/Fusion/Core/TH/Backtrack.hs
-- | Here, we do not set any restrictions on the types @m@ and @r@.

buildRightType :: Name -> (Name, Name, Name) -> (Name, Name, Name) -> [TyVarBndr] -> Type
buildRightType tycon (m, x, r) (mR, xR, rR) = foldl AppT (ConT tycon) . map (VarT . go)
  where go (PlainTV z)
          | z == m    = mR  -- have discovered a monadic type
          | z == x    = xR  -- have discovered a type that is equal to the stream type (and hence we have a synvar type)
          | z == r    = rR  -- have discovered a type that is equal to the result type (for @<||@) equal to the stream type, hence synvar
          | otherwise = z   -- this is a terminal or a terminal stack (we don't care)

            
ADP/Fusion/Core/TH/Backtrack.hs
-- return results in a list.

buildSigBacktrackingType :: Name -> (Name, Name, Name) -> (Name) -> (Name, Name, Name) -> [TyVarBndr] -> TypeQ
buildSigBacktrackingType tycon (m, x, r) (xL) (mR, xR, rR) = foldl appT (conT tycon) . map go
  where go (PlainTV z)
          | z == m    = varT mR
          | z == x    = [t| ($(varT xL) , [ $(varT xR) ] ) |]
          | z == r    = varT rR
          | otherwise = varT z

            
ADP/Fusion/Core/TH/Backtrack.hs
-- want this. We will have to change the function combination then?

buildSigCombiningType :: Name -> Name -> (Name, Name, Name) -> (Name, Name, Name) -> (Name, Name, Name) -> [TyVarBndr] -> TypeQ
buildSigCombiningType tycon vG (m, x, r) (mL, xL, rL) (mR, xR, rR) = foldl appT (conT tycon) . map go
  where go (PlainTV z)
          | z == m    = varT mR
          | z == x    = [t| ($(varT xL) , [ $(varT xR) ] ) |]   -- [1]
          | z == r    = [t| V.Vector ($(varT rL) , $(varT rR)) |]
          | otherwise = varT z

            
ADP/Fusion/Core/TH/Backtrack.hs
  -> [VarStrictType]
  -> Q Clause
genAlgProdFunctions choice conName allFunNames evalFunNames choiceFunNames = do
  let nonTermNames = nub . map getRuleResultType $ evalFunNames
  -- bind the l'eft and r'ight variable of the two algebras we want to join,
  -- also create unique names for the function names we shall bind later.
  nameL <- newName "l"
  varL  <- varP nameL
  fnmsL <- sequence $ replicate (length allFunNames) (newName "fnamL")

            
ADP/Fusion/Core/TH/Backtrack.hs
  varR  <- varP nameR
  fnmsR <- sequence $ replicate (length allFunNames) (newName "fnamR")
  -- bind the individual variables in the where part
  whereL <- valD (conP conName (map varP fnmsL)) (normalB $ varE nameL) []
  whereR <- valD (conP conName (map varP fnmsR)) (normalB $ varE nameR) []
  rce <- recConE conName
          $  zipWith3 (genChoiceFunction choice) (drop (length evalFunNames) fnmsL) (drop (length evalFunNames) fnmsR) choiceFunNames
          ++ zipWith3 (genAttributeFunction nonTermNames) fnmsL fnmsR evalFunNames
  -- build the function pairs
  -- to keep our sanity, lets print this stuff

            
ADP/Fusion/Core/TH/Backtrack.hs
recBuildLamPat nts fL' fR' ts = do
  -- here we just run through all arguments, either creating an @x@ and
  -- a @ys@ for a non-term or a @t@ for a term.
  ps <- mapM argTyArgs ts
  lamPat <- buildLamPat ps
  lfun <- buildLns (VarE fL') ps -- foldl buildLfun (varE fL') ps
  rfun <- buildRns (VarE fR') ps
  return (lamPat, lfun, rfun)


            
ADP/Fusion/Core/TH/Backtrack.hs
  return (lamPat, lfun, rfun)

buildLamPat :: [ArgTy Pat] -> Q [Pat]
buildLamPat = mapM go where
  go (SynVar      p ) = return p
  go (Term        p ) = return p
  go (StackedVars ps) = build ps
  build :: [ArgTy Pat] -> Q Pat
  build = foldl (\s v -> [p| $(s) :. $(return v) |]) [p|Z|] . map get

            
ADP/Fusion/Core/TH/Backtrack.hs
  go (Term        p ) = return p
  go (StackedVars ps) = build ps
  build :: [ArgTy Pat] -> Q Pat
  build = foldl (\s v -> [p| $(s) :. $(return v) |]) [p|Z|] . map get
  get :: ArgTy Pat -> Pat
  get (SynVar p) = p
  get (Term   p) = p

-- | Look at the argument type and build the capturing variables. In

            
ADP/Fusion/Core/TH/Backtrack.hs
argTyArgs (SynVar n) = SynVar <$> tupP [newName "x" >>= varP , newName "ys" >>= varP]
argTyArgs (Term n)          = Term <$> (newName "t" >>= varP)
argTyArgs (StackedTerms _)  = Term <$> (newName "t" >>= varP) -- !!!
argTyArgs (StackedVars vs)  = StackedVars <$> mapM argTyArgs vs
argTyArgs NilVar            = Term <$> (newName "t" >>= varP)
argTyArgs (Result _)        = error "argTyArgs: should not receive @Result@"

buildLns
  :: Exp

            
ADP/Fusion/Core/TH/Backtrack.hs
        go f (Term        (VarP v         )) = appE f (varE v)
        go f (StackedVars vs               ) = appE f (build vs)
        build :: [ArgTy Pat] -> ExpQ
        build = foldl (\s v -> [| $(s) :. $(varE v) |]) [|Z|] . map get
        get (SynVar (TupP [VarP v,_])) = v
        get (Term   (VarP t)         ) = t

-- | Build the right-hand side of a function combined in @f <|| g@. This
-- splits the paired synvars @(x,xs)@ such that we calculate @f x@ and @g

            
ADP/Fusion/Core/TH/Backtrack.hs
buildRns f' ps = do
  -- get all synvars, shallow or deep and create a new name to bind
  -- individual parts to.
  sy :: M.Map Pat Name <- M.fromList <$> (mapM (\s -> newName "y" >>= \y -> return (s,y)) $ concatMap flattenSynVars ps)
  -- bind them for the right part of the list expression (even though they
  -- are left in @CompE@. We don't use @sy@ directly to keep the order in
  -- which the comprehensions run.
  let rs = map (\k@(TupP [_,VarP v]) -> BindS (VarP $ sy M.! k) (VarE v)) $ concatMap flattenSynVars ps
  let go :: ExpQ -> ArgTy Pat -> ExpQ
      go f (SynVar      k       ) = appE f (varE $ sy M.! k) -- needed like this, because we need the @y@ in @y <- ys@
      go f (Term        (VarP v)) = appE f (varE v)
      go f (StackedVars vs      ) = appE f (foldl build [|Z|] vs)
      build :: ExpQ -> ArgTy Pat -> ExpQ

            
ADP/Fusion/Core/TH/Backtrack.hs
      -- turn the stream into a list
      ysM <- SM.toList xs
      -- based only on the @fst@ elements, select optimal value
      hFres <- $(varE hL') $ SM.map fst $ SM.fromList ysM
      -- filter accordingly
      $(varE hR') $ SM.fromList $ concatMap snd $ filter ((hFres==) . fst) $ ysM
  |]

-- | We assume parses of type @(x,y)@ in a vector @<(x,y)>@. the function

            
ADP/Fusion/Core/TH/Backtrack.hs
      -- ys <- SM.toList xs
      -- -- but now, we actually get a list of co-optimals to keep. Yes,
      -- -- a @[fst]@ list.
      -- cooptFsts <- S.fromList <$> ( ( $(varE hL') $ SM.map fst $ SM.fromList ys ) >>= SM.toList )
      -- -- now we create a map with all the coopts, where we collect in the
      -- -- value parts the list of parses for each co-optimal @snd@ for
      -- -- a @fst@.
      -- let cooptMap = M.fromListWith (++) [ y | y <- ys, y `S.member` cooptFsts ]
      -- -- We now need to map @actSnd@ over the resulting intermediates
      -- actSnd <- mapM (\y -> $(varE hR') (SM.fromList y)) cooptMap
      -- -- a vector with co-optimals, each one associated with its optimal
      -- -- @snd@.
      -- return . VG.fromList . M.toList $ actSnd
      return undefined
  |]

            
Agda-2.6.0.1
16 matches
src/full/Agda/TypeChecking/Monad/Statistics.hs
modifyCounter :: String -> (Integer -> Integer) -> TCM ()
modifyCounter x f = modifyStatistics $ force . update
  where
    -- We need to be strict in the map.
    -- Andreas, 2014-03-22:  Could we take Data.Map.Strict instead of this hack?
    -- Or force the map by looking up the very element we inserted?
    -- force m = Map.lookup x m `seq` m
    -- Or use insertLookupWithKey?
    -- update m = old `seq` m' where
    --   (old, m') = Map.insertLookupWithKey (\ _ new old -> f old) x dummy m
    -- Ulf, 2018-04-10: Neither of these approaches are strict enough in the

            
src/full/Agda/TypeChecking/Monad/Statistics.hs
    -- update m = old `seq` m' where
    --   (old, m') = Map.insertLookupWithKey (\ _ new old -> f old) x dummy m
    -- Ulf, 2018-04-10: Neither of these approaches are strict enough in the
    -- map (nor are they less hacky). It's not enough to be strict in the
    -- values stored in the map, we also need to be strict in the *structure*
    -- of the map. A less hacky solution is to deepseq the map.
    force m = rnf m `seq` m
    update  = Map.insertWith (\ new old -> f old) x dummy
    dummy   = f 0

-- | Print the given statistics if verbosity "profile.ticks" is given.

            
src/full/Agda/TypeChecking/Monad/Statistics.hs
printStatistics vl mmname stats = verboseS "profile.ticks" vl $ do
  unlessNull (Map.toList stats) $ \ stats -> do
    let -- First column (left aligned) is accounts.
        col1 = Boxes.vcat Boxes.left  $ map (Boxes.text . fst) stats
        -- Second column (right aligned) is numbers.
        col2 = Boxes.vcat Boxes.right $ map (Boxes.text . showThousandSep . snd) stats
        table = Boxes.hsep 1 Boxes.left [col1, col2]
    reportSLn "profile" 1 $ caseMaybe mmname "Accumulated statistics" $ \ mname ->
      "Statistics for " ++ prettyShow mname
    reportSLn "profile" 1 $ Boxes.render table

            
src/full/Agda/TypeChecking/Positivity/Occurrence.hs
instance Sized OccursWhere where
  size (OccursWhere _ cs os) = 1 + size cs + size os

-- | The map contains bindings of the form @bound |-> ess@, satisfying
-- the following property: for every non-empty list @w@,
-- @'foldr1' 'otimes' w '<=' bound@ iff
-- @'or' [ 'all' every w '&&' 'any' some w | (every, some) <- ess ]@.

boundToEverySome ::

            
src/full/Agda/TypeChecking/Positivity/Occurrence.hs
-- | @productOfEdgesInBoundedWalk occ g u v bound@ returns a value
-- distinct from 'Nothing' iff there is a walk @c@ (a list of edges)
-- in @g@, from @u@ to @v@, for which the product @'foldr1' 'otimes'
-- ('map' occ c) '<=' bound@. In this case the returned value is
-- @'Just' ('foldr1' 'otimes' c)@ for one such walk @c@.
--
-- Preconditions: @u@ and @v@ must belong to @g@, and @bound@ must
-- belong to the domain of @boundToEverySome@.


            
src/full/Agda/TypeChecking/Positivity/Occurrence.hs
                    g u v
                | (every, some) <- ess
                ] of
        Just es@(_ : _) -> Just (foldr1 otimes (map Graph.label es))
        Just []         -> __IMPOSSIBLE__
        Nothing         -> Nothing

            
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