Aelve Codesearch

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

total matches: more than 1000

Agata-0.2.1.1
1 matches
Test/AgataTH.hs
  applic nts t0 = do
    b <- t0 `contains` n0
    if not b then return t0 else case flat t0 of
      (TupleT _,ts) -> fmap toTuple $ mapM (applic nts) ts
      (ConT n, ts)  ->
        if (ConT n,ts) `elem` nts then return (ConT n0) else do
          let rec = applic $ (ConT n,ts) : nts
          i <- reify n
          let fs = toTuple $ nub $ iTypes i

            
Agda-2.6.0.1
29 matches
src/full/Agda/Auto/Auto.hs
    -- Add the @autohints@ for that meta to the hints collection.
    mi <- lookupInteractionId ii
    thisdefinfo <- findClauseDeep ii
    ehints <- (ehints ++) <$> do autohints hintmode mi $ fmap fst3 thisdefinfo

    -- If @thisdefinfo /= Nothing@ get the its type (normalized).
    mrectyp <- maybeToList <$> do
      Trav.forM thisdefinfo $ \ (def, _, _) -> do
        normalise =<< do TCM.defType <$> getConstInfo def

            
src/full/Agda/Auto/CaseSplit.hs
                  $ (case meqr of
                        Nothing  -> id
                        Just eqr -> mpret . Sidecondition (calcEqRState eqr trm)
                     ) $ tcSearch False (map (fmap closify) (drophid ctx))
                         (closify tt) trm
      recdefd <- readIORef recdef
      let env = RIEnv { rieHints = (recdef, HMRecCall) : map (, HMNormal) chints
                      , rieDefFreeVars = cddeffreevars recdefd
                      , rieEqReasoningConsts = meqr

            
src/full/Agda/Auto/CaseSplit.hs
      NotM . App uid ok elr . NotM <$> replace' n re args
    Lam hid b -> NotM . Lam hid <$> replace' (n + 1) re b
    Pi uid hid possdep it b ->
      fmap NotM $ Pi uid hid possdep <$> replace' n re it <*> replace' n re b
    Sort{} -> return $ NotM e
    AbsurdLambda{} -> return $ NotM e

instance Replace o t u => Replace o (MM t (RefInfo o)) u where
  replace' n re = replace' n re . rm __IMPOSSIBLE__

            
src/full/Agda/Auto/CaseSplit.hs

-- This definition is only here to respect the previous interface.
unifyexp :: MExp o -> MExp o -> Maybe ([(Nat, MExp o)])
unifyexp e1 e2 = fmap (NotM <$>) <$> unify e1 e2

class Lift t where
  lift' :: Nat -> Nat -> t -> t

lift :: Lift t => Nat -> t -> t

            
src/full/Agda/Auto/Convert.hs
  convert :: a -> m b

instance Conversion TOM [I.Clause] [([Pat O], MExp O)] where
  convert = fmap catMaybes . mapM convert

instance Conversion TOM I.Clause (Maybe ([Pat O], MExp O)) where
  convert cl = do
    let -- Jesper, 2016-07-28:
     -- I can't figure out if this should be the old or new

            
src/full/Agda/Auto/Convert.hs
    I.ConP con _ pats -> do
      let n = I.conName con
      c     <- getConst True n TMAll
      pats' <- mapM (convert . fmap Cm.namedThing) pats
      def   <- lift $ getConstInfo n
      cc    <- lift $ liftIO $ readIORef c
      let Just npar = fst $ cdorigin cc
      return $ PatConApp c (replicate npar PatExp ++ pats')


            
src/full/Agda/Auto/NarrowingSearch.hs
  { runRefCreateEnv :: StateT ((IORef [SubConstraints blk]), Int) IO a }

instance Functor (RefCreateEnv blk) where
  fmap f = RefCreateEnv . fmap f . runRefCreateEnv

instance Applicative (RefCreateEnv blk) where
  pure    = RefCreateEnv . pure
  f <*> t = RefCreateEnv $ runRefCreateEnv f <*> runRefCreateEnv t


            
src/full/Agda/Auto/SearchControl.hs
import Agda.Utils.Impossible

instance Refinable (ArgList o) (RefInfo o) where
 refinements _ infos _ = return $ fmap (Move 0) $
   [ return ALNil, cons NotHidden, cons Hidden ]
   ++ if getIsDep infos then []
      else [ proj NotHidden, proj Hidden ]

   where

            
src/full/Agda/Compiler/Backend.hs
embedFlag l flag = l flag

embedOpt :: Lens' a b -> OptDescr (Flag a) -> OptDescr (Flag b)
embedOpt l = fmap (embedFlag l)

parseBackendOptions :: [Backend] -> [String] -> CommandLineOptions -> OptM ([Backend], CommandLineOptions)
parseBackendOptions backends argv opts0 =
  case makeAll backendWithOpts backends of
    Some bs -> do

            
src/full/Agda/Compiler/Common.hs
curMName = sigMName <$> curSig

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

            
src/full/Agda/Compiler/MAlonzo/Misc.hs

-- the toplevel module containing the given one
tlmodOf :: ModuleName -> TCM HS.ModuleName
tlmodOf = fmap mazMod . topLevelModuleName


-- qualify HS.Name n by the module of QName q, if necessary;
-- accumulates the used module in stImportedModules at the same time.
xqual :: QName -> HS.Name -> TCM HS.QName

            
src/full/Agda/Compiler/MAlonzo/Primitives.hs
-- | Haskell modules to be imported for BUILT-INs
importsForPrim :: TCM [HS.ModuleName]
importsForPrim =
  fmap (++ [HS.ModuleName "Data.Text"]) $
  xForPrim $
  List.map (\(s, ms) -> (s, return (List.map HS.ModuleName ms))) $
  [ "CHAR"              |-> ["Data.Char"]
  , "primIsAlpha"       |-> ["Data.Char"]
  , "primIsAscii"       |-> ["Data.Char"]

            
src/full/Agda/Interaction/BasicOps.hs
    I.Proj _o f -> appl "proj" <$> reify ((defaultArg $ I.Def f []) :: Arg Term)
  where
    appl :: String -> Arg Expr -> Expr
    appl s v = A.App defaultAppInfo_ (A.Lit (LitString noRange s)) $ fmap unnamed v

instance Reify Constraint (OutputConstraint Expr Expr) where
    reify (ValueCmp cmp t u v)   = CmpInType cmp <$> reify t <*> reify u <*> reify v
    reify (ValueCmpOnFace cmp p t u v) = CmpInType cmp <$> (reify =<< ty) <*> reify (lam_o u) <*> reify (lam_o v)
      where

            
src/full/Agda/Interaction/BasicOps.hs
typeOfMeta norm ii = typeOfMeta' norm . (ii,) =<< lookupInteractionId ii

typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta' norm (ii, mi) = fmap (\_ -> ii) <$> typeOfMetaMI norm mi

typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas norm =
  liftTCM $ mapM (typeOfMeta' norm) =<< getInteractionIdsAndMetas


            
src/full/Agda/Interaction/BasicOps.hs
      where
        n = size tel
        hs   = map getHiding tel
        tel' = telFromList [ fmap makeName b | b <- tel ]
        makeName ("_", t) = ("x", t)
        makeName (x, t)   = (x, t)

    introData :: I.Type -> TCM [String]
    introData t = do

            
src/full/Agda/Interaction/BasicOps.hs
            -- We're going inside the top-level module, so we have to set the
            -- checkpoint for it and all its submodules to the new checkpoint.
            cp <- viewTC eCurrentCheckpoint
            stModuleCheckpoints `modifyTCLens` fmap (const cp)
            m

-- | Parse a name.
parseName :: Range -> String -> TCM C.QName
parseName r s = do

            
src/full/Agda/Interaction/CommandLine.hs

        loop =
            do  ms <- readline prompt
                case fmap words ms of
                    Nothing               -> return $ error "** EOF **"
                    Just []               -> loop
                    Just ((':':cmd):args) ->
                        do  case matchCommand cmd cmds of
                                Right c -> go =<< liftTCM (c args)

            
src/full/Agda/Interaction/Highlighting/Generate.hs
      where
      isTopLevelModule =
        case mapMaybe (join .
                  fmap (Strict.toLazy . P.srcFile) .
                  P.rStart .
                  A.nameBindingSite) xs of
          f : _ -> Map.lookup f modMap ==
                   Just (C.toTopLevelModuleName $ A.mnameToConcrete m)
          []    -> False

            
src/full/Agda/Interaction/Highlighting/Generate.hs
    mempty
  where
  aspects    = m $ C.isOperator x
  fileNames  = mapMaybe (fmap P.srcFile . P.rStart . P.getRange) (x : xs)
  frFile     = singleton (rToR fr) (aspects { definitionSite = notHere <$> mFilePos })
  rs         = map P.getRange (x : xs)

  -- The fixity declaration should not get a symbolic anchor.
  notHere d = d { defSiteHere = False }

            
src/full/Agda/Interaction/Highlighting/HTML.hs
    posAttributes :: [Attribute]
    posAttributes = concat
      [ [Attr.id $ stringValue $ show pos ]
      , toList $ fmap link $ definitionSite mi
      , class_ (stringValue $ unwords classes) <$ guard (not $ null classes)
      ]

    -- | Named anchor (not reliable, but useful in the general case for outside refs).
    nameAttributes :: [Attribute]

            
src/full/Agda/Interaction/Highlighting/HTML.hs

    aspectClasses (Name mKind op) = kindClass ++ opClass
      where
      kindClass = toList $ fmap showKind mKind

      showKind (Constructor Inductive)   = "InductiveConstructor"
      showKind (Constructor CoInductive) = "CoinductiveConstructor"
      showKind k                         = show k


            
src/full/Agda/Interaction/Highlighting/LaTeX.hs
  inAbsPath <- liftM filePath (Find.findFile mod)

  liftIO $ do
    latex <- E.encodeUtf8 `fmap`
               toLaTeX (O.optCountClusters $ O.optPragmaOptions options)
                       (mkAbsolute inAbsPath) (iSource i) hi
    createDirectoryIfMissing True $ dir </> takeDirectory outPath
    BS.writeFile (dir </> outPath) latex


            
src/full/Agda/Interaction/Highlighting/LaTeX.hs
          (withLast $
            withTokenText $ \suf ->
              fromMaybe suf $
                fmap (T.dropWhileEnd isSpaceNotNewline) $
                  T.stripSuffix "\n" suf)
        .
        (withLast $ withTokenText $ T.dropWhileEnd isSpaceNotNewline)
        .
        (withFirst $

            
src/full/Agda/Interaction/Highlighting/Precise.hs
-- | Returns the smallest position, if any, in the 'File'.

smallestPos :: File -> Maybe Int
smallestPos = fmap (fst . fst) . IntMap.minViewWithKey . mapping

-- | Convert the 'File' to a map from file positions (counting from 1)
-- to meta information.

toMap :: File -> IntMap Aspects

            
src/full/Agda/Interaction/Imports.hs
                     Just si -> return $ hashText (siSource si)
        ifaceH  <-
          case cached of
            Nothing -> fmap fst <$> getInterfaceFileHashes (filePath $ toIFile file)
            Just i  -> return $ Just $ iSourceHash i
        let unchanged = Just sourceH == ifaceH
        return $ unchanged && (not ignore || isJust cached)

      reportSLn "import.iface" 5 $

            
src/full/Agda/Interaction/Imports.hs
  mi <- MaybeT $ getDecodedModule x

  -- Check that the interface file exists and return its hash.
  h  <- MaybeT $ fmap snd <$> getInterfaceFileHashes ifile

  -- Make sure the hashes match.
  guard $ iFullHash mi == h

  return mi

            
src/full/Agda/Interaction/Imports.hs
  -- stored version (in stDecodedModules), or if there is no stored version,
  -- read and decode it. Otherwise use the stored version.
  let ifile = filePath $ toIFile file
  h <- fmap snd <$> getInterfaceFileHashes ifile
  mm <- getDecodedModule x
  (cached, mi) <- Bench.billTo [Bench.Deserialization] $ case mm of
    Just mi ->
      if Just (iFullHash mi) /= h
      then do

            
src/full/Agda/Interaction/Imports.hs
    return $ first constructIScope (i, mallWarnings)

getUniqueMetasRanges :: [MetaId] -> TCM [Range]
getUniqueMetasRanges = fmap List.nub . mapM getMetaRange

getUnsolvedMetas :: TCM [Range]
getUnsolvedMetas = do
  openMetas            <- getOpenMetas
  interactionMetas     <- getInteractionMetas

            
src/full/Agda/Interaction/Imports.hs
  let showWarn w = classifyWarning w <= ww &&
                    not (null unsolved && onlyShowIfUnsolved w)

  fmap (filter (showWarn . tcWarning))
    $ applyFlagsToTCWarnings' isMain $ reverse
    $ unsolved ++ collectedTCWarnings

getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings
getMaybeWarnings = getMaybeWarnings' NotMainInterface