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
30 matches
src/full/Agda/Compiler/Common.hs
curDefs :: TCM Definitions
curDefs = fmap (HMap.filter (not . defNoCompilation)) $ (^. sigDefinitions) <$> curSig

sortDefs :: Definitions -> [(QName, Definition)]
sortDefs defs =
  -- The list is sorted to ensure that the order of the generated
  -- definitions does not depend on things like the number of bits
  -- in an Int (see Issue 1900).
  List.sortBy (compare `on` fst) $
  HMap.toList defs

sigMName :: Signature -> ModuleName
sigMName sig = case Map.keys (sig ^. sigSections) of
  []    -> __IMPOSSIBLE__

            
src/full/Agda/Compiler/Common.hs
  visited <- List.map (iModuleName . miInterface) . Map.elems <$>
    getVisitedModules
  -- find the module with the longest matching prefix to m
  let ms = sortBy (compare `on` (length . mnameToList)) $
       List.filter (\ m' -> mnameToList m' `isPrefixOf` mnameToList m) visited
  case ms of
    (m' : _) -> return m'
    -- if we did not get anything, it may be because m is a section
    -- (a module _ ), see e.g. #1866

            
src/full/Agda/Compiler/JS/Compiler.hs
  kit <- coinductionKit
  m <- (jsMod <$> curMName)
  is <- map jsMod <$> (map fst . iImportedModules <$> curIF)
  es <- catMaybes <$> (mapM (definition kit) =<< (sortDefs <$> curDefs))
  return $ Module m (reorder es) main
  where
    main = case isMain of
      IsMain -> Just $ Apply (Lookup Self $ MemberId "main") [Lambda 1 emp]
      NotMain -> Nothing

            
src/full/Agda/Compiler/MAlonzo/Compiler.hs
  mnames = Set.elems <$> useTC stImportedModules

  uniq :: [HS.ModuleName] -> [HS.ModuleName]
  uniq = List.map head . List.group . List.sort

--------------------------------------------------
-- Main compiling clauses
--------------------------------------------------


            
src/full/Agda/Compiler/MAlonzo/Pragmas.hs
        _ -> return Nothing
    _ -> return Nothing

-- | Get content of @FOREIGN GHC@ pragmas, sorted by 'KindOfForeignCode':
--   file header pragmas, import statements, rest.
foreignHaskell :: TCM ([String], [String], [String])
foreignHaskell = partitionByKindOfForeignCode classifyForeign
    . map getCode . fromMaybe [] . Map.lookup ghcBackendName . iForeignCode <$> curIF
  where getCode (ForeignCode _ code) = code

            
src/full/Agda/Compiler/Treeless/Simplify.hs
  | otherwise        = a : aCancel as
aCancel [] = []

sortR :: Ord a => [a] -> [a]
sortR = List.sortBy (flip compare)

aAdd :: Arith -> Arith -> Arith
aAdd (a, xs) (b, ys) = (a + b, aCancel $ sortR $ xs ++ ys)

aSub :: Arith -> Arith -> Arith
aSub (a, xs) (b, ys) = (a - b, aCancel $ sortR $ xs ++ map aNeg ys)

fromArith :: Arith -> TTerm
fromArith (n, []) = tInt n
fromArith (0, xs)
  | (ys, Pos a : zs) <- break isPos xs = foldl addAtom a (ys ++ zs)

            
src/full/Agda/Interaction/Highlighting/Generate.hs
  -- Converts an aspect and a range to a file.
  aToF a r = singletonC (rToR r) (mempty { aspect = Just a })

  -- Merges /sorted, non-overlapping/ compressed files.
  merge = CompressedFile . concat . map ranges

  tokenToCFile :: T.Token -> CompressedFile
  tokenToCFile (T.TokSetN (i, _))               = aToF PrimitiveType (P.getRange i)
  tokenToCFile (T.TokPropN (i, _))              = aToF PrimitiveType (P.getRange i)

            
src/full/Agda/Interaction/Highlighting/Precise.hs
    )
    where
    [(a, ma), (b, _), (c, _), (d, md)] =
      List.sortBy (compare `on` fst)
             [(from i1, m1), (to i1, m1), (from i2, m2), (to i2, m2)]
    fix = filter (not . empty . fst)

instance Semigroup CompressedFile where
  (<>) = mergeC

            
src/full/Agda/Interaction/Highlighting/Vim.hs
matches :: [String] -> [String] -> [String] -> [String] -> [String] -> [String] -> [String]
matches cons icons defs idefs flds iflds =
    map snd
    $ List.sortBy (compare `on` fst)
    $ cons' ++ defs' ++ icons' ++ idefs'
    where
        cons'  = foo "agdaConstructor"      $ classify length cons
        icons' = foo "agdaInfixConstructor" $ classify length icons
        defs'  = foo "agdaFunction"         $ classify length defs

            
src/full/Agda/Interaction/Highlighting/Vim.hs
        iflds' = foo "agdaInfixProjection"  $ classify length iflds

        classify f = List.groupBy ((==) `on` f)
                     . List.sortBy (compare `on` f)

        foo :: String -> [[String]] -> [(Int, String)]
        foo cat = map (length . head /\ match cat)

toVim :: NamesInScope -> String

            
src/full/Agda/Interaction/InteractionTop.hs
    -- "current file" are stored.
    t' <- liftIO $ getModificationTime file
    when (t == t') $ do
      is <- lift $ sortInteractionPoints =<< getInteractionPoints
      modify $ \st -> st { theInteractionPoints = is
                         , theCurrentFile       = Just (f, t)
                         }

    cmd ok

            
src/full/Agda/Interaction/InteractionTop.hs
        return (ae, given, mis' List.\\ mis)
    -- favonia: backup the old scope for highlighting
    insertOldInteractionScope ii scope
    -- sort the new interaction points and put them into the state
    -- in replacement of the old interaction point
    iis       <- lift $ sortInteractionPoints iis
    modifyTheInteractionPoints $ replace ii iis
    -- print abstract expr
    ce        <- lift $ abstractToConcreteScope scope ae
    lift $ reportSLn "interaction.give" 30 $ unlines
      [ "ce = " ++ show ce

            
src/full/Agda/Interaction/InteractionTop.hs

-- | Sorts interaction points based on their ranges.

sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
sortInteractionPoints is =
  map fst . List.sortBy (compare `on` snd) <$> do
    forM is $ \ i -> do
      (i,) <$> getInteractionRange i

-- | Pretty-prints the type of the meta-variable.


            
src/full/Agda/Interaction/Library.hs
    l : ls' -> l : takeWhile (((==) `on` versionMeasure) l) ls'
    []      -> []
  where
    -- @LibName@s that match @x@, sorted descendingly.
    -- The unversioned LibName, if any, will come first.
    ls = List.sortBy (flip compare `on` versionMeasure) [ l | l <- libs, x `hasMatch` libName l ]

    -- foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0
    versionMeasure l = (rx, null vs, vs)
      where
        VersionView rx vs = versionView (libName l)

            
src/full/Agda/Interaction/Options/Warnings.hs
  SafeFlagNoUniverseCheck_         -> "`NO_UNIVERSE_CHECK' pragmas with the safe flag."
  UserWarning_                     -> "User-defined warning added using the 'WARNING_ON_USAGE' pragma."
  AbsurdPatternRequiresNoRHS_      -> "A clause with an absurd pattern does not need a Right Hand Side."
  CantGeneralizeOverSorts_         -> "Attempt to generalize over sort metas in 'variable' declaration."
  WithoutKFlagPrimEraseEquality_   -> "`primEraseEquality' usages with the without-K flags."
  InfectiveImport_                 -> "Importing a file using e.g. `--cubical' into one which doesn't"
  CoInfectiveImport_               -> "Importing a file not using e.g. `--safe'  from one which does"

            
src/full/Agda/Syntax/Abstract/Copatterns.hs
  let cps :: [(Clause, [ProjPath Expr])]
      cps = groupClauses pcs
  ces <- mapM (mapSndM pathToRecord) $
    map (mapSnd $ sortBy (compare `on` thePath)) cps
  return $ map (\ (c, e) -> c { clauseRHS = RHS e Nothing }) ces  -- TODO: preserve C.Expr
  where
    noCopats Clause{ clauseLHS = LHS _ LHSHead{} } = True
    noCopats _                                     = False


            
src/full/Agda/Syntax/Abstract/Copatterns.hs
        fromVarP (VarP n) = Just $ unBind n
        fromVarP _        = Nothing

-- | Expects a sorted list.
pathToRecord :: [ProjPath Expr] -> ScopeM Expr
pathToRecord []          = __IMPOSSIBLE__
pathToRecord [Path [] e] = return e
pathToRecord pps =
  case pathHeads pps of

            
src/full/Agda/Syntax/Concrete/Name.hs
--     explicitly applied modules.
--   Also assumes namespaces are generative by just using derived
--     equality. We will have to define an equality instance to
--     non-generative namespaces (as well as having some sort of
--     lookup table for namespace names).
data QName
  = Qual  Name QName -- ^ @A.rest@.
  | QName Name       -- ^ @x@.
  deriving (Data, Eq, Ord)

            
src/full/Agda/Syntax/Concrete/Operators.hs
        relatedOperators =
          map (\((l, ns) : rest) -> (l, ns ++ concat (map snd rest))) .
          List.groupBy ((==) `on` fst) .
          List.sortBy (compare `on` fst) .
          mapMaybe (\n -> case level n of
                            Unrelated     -> Nothing
                            r@(Related l) ->
                              Just (l, filterCorrectUnderscoresOp [n] ++
                                       nonClosedSections r [n])) $

            
src/full/Agda/Syntax/Internal.hs
  traverseF f (Abs   x a) = Abs   x <$> f a
  traverseF f (NoAbs x a) = NoAbs x <$> f a

-- | Types are terms with a sort annotation.
--
data Type' a = El { _getSort :: Sort, unEl :: a }
  deriving (Data, Show, Functor, Foldable, Traversable)

type Type = Type' Term

            
src/full/Agda/Syntax/Internal.hs
  = Type Level  -- ^ @Set ℓ@.
  | Prop Level  -- ^ @Prop ℓ@.
  | Inf         -- ^ @Setω@.
  | SizeUniv    -- ^ @SizeUniv@, a sort inhabited by type @Size@.
  | PiSort Sort (Abs Sort) -- ^ Sort of the pi type.
  | UnivSort Sort -- ^ Sort of another sort.
  | MetaS {-# UNPACK #-} !MetaId Elims
  | DefS QName Elims -- ^ A postulated sort.
  | DummyS String
    -- ^ A (part of a) term or type which is only used for internal purposes.
    --   Replaces the abuse of @Prop@ for a dummy sort.
    --   The @String@ typically describes the location where we create this dummy,
    --   but can contain other information as well.
  deriving (Data, Show)

-- | A level is a maximum expression of 0..n 'PlusLevel' expressions

            
src/full/Agda/Syntax/Internal.hs
    DontCare{} -> v
    _          -> DontCare v

-- | Aux: A dummy term to constitute a dummy term/level/sort/type.
dummyTerm' :: String -> Int -> Term
dummyTerm' file line = Dummy $ file ++ ":" ++ show line

-- | Aux: A dummy level to constitute a level/sort.
dummyLevel' :: String -> Int -> Level
dummyLevel' file line = unreducedLevel $ dummyTerm' file line

-- | A dummy term created at location.
--   Note: use macro __DUMMY_TERM__ !

            
src/full/Agda/Syntax/Internal.hs
dummyLevel :: String -> Int -> Level
dummyLevel file line = dummyLevel' ("dummyLevel: " ++ file) line

-- | A dummy sort created at location.
--   Note: use macro __DUMMY_SORT__ !
dummySort :: String -> Int -> Sort
dummySort file line = DummyS $ file ++ ":" ++ show line

-- | A dummy type created at location.

            
src/full/Agda/Syntax/Internal.hs
unreducedLevel :: Term -> Level
unreducedLevel v = Max [ Plus 0 $ UnreducedLevel v ]

-- | Top sort (Set\omega).
topSort :: Type
topSort = sort Inf

sort :: Sort -> Type
sort s = El (UnivSort s) $ Sort s

varSort :: Int -> Sort
varSort n = Type $ Max [Plus 0 $ NeutralLevel mempty $ var n]

tmSort :: Term -> Sort

            
src/full/Agda/Syntax/Internal.hs
--
--   Not counting towards the term size are:
--
--     * sort and color annotations,
--     * projections.
--
class TermSize a where
  termSize :: a -> Int
  termSize = getSum . tsize

            
src/full/Agda/Syntax/Notation.hs
      -- The hole names are the keys of the @holeMap@.
      uniqueHoleNames = distinct [ x | (x, _) <- holeMap, rangedThing x /= "_" ]

      isExprLinear   xs = List.sort [ i | x <- xs, isNormalHole x, let Just i = holeTarget x ] == holeNumbers
      isLambdaLinear xs = List.sort [ rangedThing x | BindHole _ x <- xs ] ==
                          [ i | (i, h) <- numberedHoles,
                                LambdaHole x _ <- [namedArg h], rangedThing x /= "_" ]

      isAlternating :: [GenPart] -> Bool
      isAlternating []       = __IMPOSSIBLE__

            
src/full/Agda/Syntax/Position.hs
fuseIntervals :: Ord a => Interval' a -> Interval' a -> Interval' a
fuseIntervals x y = Interval { iStart = head ss, iEnd = last es }
    where
    ss = sort [iStart x, iStart y]
    es = sort [iEnd   x, iEnd   y]

-- | @fuseRanges r r'@ unions the ranges @r@ and @r'@.
--
--   Meaning it finds the least range @r0@ that covers @r@ and @r'@.
--

            
src/full/Agda/Syntax/Scope/Base.hs
    len (C.Qual _ x) = 1 + len x

    best :: [C.QName] -> [C.QName]
    best = List.sortBy (compare `on` len)

    unique :: forall a . [a] -> Bool
    unique []      = __IMPOSSIBLE__
    unique [_]     = True
    unique (_:_:_) = False

            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
import qualified Data.Map as Map
import Data.Traversable (traverse)
import Data.Void
import Data.List (sortBy)

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Info as A

            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
                                         isConP rhs, Just args <- [match psyndef e],
                                         isNameInScope q scope ]
        cmp (_, _, x) (_, _, y) = flip compare x y
    case sortBy cmp cands of
      (q, args, _) : _ -> toConcrete $ applySyn q $ (map . fmap) unnamed args
      []               -> fallback
  where
    -- Heuristic to pick the best pattern synonym: the one that folds the most
    -- constructors.