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

Agda-2.6.0.1
30 matches
src/full/Agda/Syntax/Concrete/Definitions.hs
                OtherDecl   -> cons d (untilAllDefined tcpc ds)
          where
            -- ASR (26 December 2015): Type annotated version of the @cons@ function.
            -- cons d = fmap $
            --            (id :: (([TerminationCheck], [PositivityCheck]) -> ([TerminationCheck], [PositivityCheck])))
            --            *** (d :)
            --            *** (id :: [NiceDeclaration] -> [NiceDeclaration])
            cons d = fmap (id *** (d :) *** id)

    notMeasure TerminationMeasure{} = False
    notMeasure _ = True

    nice :: [Declaration] -> Nice [NiceDeclaration]

            
src/full/Agda/Syntax/Concrete/Definitions.hs
        let ds = replaceSigs ps ds'

        -- -- Remove the declarations that aren't allowed in old style mutual blocks
        -- ds <- fmap catMaybes $ forM ds $ \ d -> let success = pure (Just d) in case d of
        --   -- Andreas, 2013-11-23 allow postulates in mutual blocks
        --   Axiom{}          -> success
        --   -- Andreas, 2017-10-09, issue #2576, raise error about missing type signature
        --   -- in ConcreteToAbstract rather than here.
        --   NiceFunClause{}  -> success

            
src/full/Agda/Syntax/Concrete/Operators.hs
                Hidden     -> e2
                Instance{} -> e2
                NotHidden  -> fullParen' <$> e2
    OpAppV x ns es -> par $ unExprView $ OpAppV x ns $ (map . fmap . fmap . fmap . fmap) fullParen' es
    LamV bs e -> par $ unExprView $ LamV bs (fullParen e)
    where
        par = unExprView . ParenV

            
src/full/Agda/Syntax/Concrete/Pretty.hs
                                 , namedBinding :: NamedArg BoundName }

getLabel :: NamedArg a -> Maybe String
getLabel = fmap rangedThing . nameOf . unArg

isLabeled :: NamedArg BoundName -> Bool
isLabeled x
  | visible x            = False  -- Ignore labels on visible arguments
  | Just l <- getLabel x = l /= nameToRawName (boundName $ namedArg x)

            
src/full/Agda/Syntax/Concrete/Pretty.hs
            IdentP x        -> pretty x
            AppP p1 p2      -> sep [ pretty p1, nest 2 $ pretty p2 ]
            RawAppP _ ps    -> fsep $ map pretty ps
            OpAppP _ q _ ps -> fsep $ prettyOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps)
            HiddenP _ p     -> braces' $ pretty p
            InstanceP _ p   -> dbraces $ pretty p
            ParenP _ p      -> parens $ pretty p
            WildP _         -> underscore
            AsP _ x p       -> pretty x <> "@" <> pretty p

            
src/full/Agda/Syntax/IdiomBrackets.hs
    _               -> return [e]
  where
    onlyVisible a
      | defaultNamedArg () == (fmap (() <$) a) = return $ namedArg a
      | otherwise = genericError $ "Only regular arguments are allowed in idiom brackets (no implicit or instance arguments)"
    noPlaceholder Placeholder{}       = genericError "Naked sections are not allowed in idiom brackets"
    noPlaceholder (NoPlaceholder _ x) = return x

    ordinary (Ordinary a) = return a

            
src/full/Agda/Syntax/Internal/Pattern.hs
  default unlabelPatVars
    :: (Traversable f, LabelPatVars a' b' i, f a' ~ a, f b' ~ b)
    => b -> a
  unlabelPatVars = fmap unlabelPatVars

instance LabelPatVars a b i => LabelPatVars (Arg a) (Arg b) i         where
instance LabelPatVars a b i => LabelPatVars (Named x a) (Named x b) i where
instance LabelPatVars a b i => LabelPatVars [a] [b] i                 where


            
src/full/Agda/Syntax/Internal/Pattern.hs
      IApplyP o u t x -> do i <- next
                            return $ IApplyP o u t (DBPatVar x i)
    where next = caseListM get __IMPOSSIBLE__ $ \ x xs -> do put xs; return x
  unlabelPatVars = fmap dbPatVarName

-- | Augment pattern variables with their de Bruijn index.
{-# SPECIALIZE numberPatVars :: Int -> Permutation -> [NamedArg Pattern] -> [NamedArg DeBruijnPattern] #-}
--
--  Example:

            
src/full/Agda/Syntax/Internal/Pattern.hs
patternToElim :: Arg DeBruijnPattern -> Elim
patternToElim (Arg ai (VarP o x)) = Apply $ Arg ai $ var $ dbPatVarIndex x
patternToElim (Arg ai (ConP c cpi ps)) = Apply $ Arg ai $ Con c ci $
      map (patternToElim . fmap namedThing) ps
  where ci = fromConPatternInfo cpi
patternToElim (Arg ai (DefP o q ps)) = Apply $ Arg ai $ Def q $
      map (patternToElim . fmap namedThing) ps
patternToElim (Arg ai (DotP o t)   ) = Apply $ Arg ai t
patternToElim (Arg ai (LitP l)     ) = Apply $ Arg ai $ Lit l
patternToElim (Arg ai (ProjP o dest)) = Proj o dest
patternToElim (Arg ai (IApplyP o t u x)) = IApply t u $ var $ dbPatVarIndex x


            
src/full/Agda/Syntax/Internal/Pattern.hs
patternsToElims ps = map build ps
  where
    build :: NamedArg DeBruijnPattern -> Elim
    build = patternToElim . fmap namedThing

patternToTerm :: DeBruijnPattern -> Term
patternToTerm p = case patternToElim (defaultArg p) of
  Apply x -> unArg x
  Proj{}  -> __IMPOSSIBLE__

            
src/full/Agda/Syntax/Internal/Pattern.hs
  default mapNamedArgPattern
    :: (Functor f, MapNamedArgPattern a p', p ~ f p')
    => (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p
  mapNamedArgPattern = fmap . mapNamedArgPattern

-- | Modify the content of @VarP@, and the closest surrounding @NamedArg@.
--
--   Note: the @mapNamedArg@ for @Pattern'@ is not expressible simply
--   by @fmap@ or @traverse@ etc., since @ConP@ has @NamedArg@ subpatterns,

            
src/full/Agda/Syntax/Internal/Pattern.hs
-- | Modify the content of @VarP@, and the closest surrounding @NamedArg@.
--
--   Note: the @mapNamedArg@ for @Pattern'@ is not expressible simply
--   by @fmap@ or @traverse@ etc., since @ConP@ has @NamedArg@ subpatterns,
--   which are taken into account by @mapNamedArg@.

instance MapNamedArgPattern a (NamedArg (Pattern' a)) where
  mapNamedArgPattern f np =
    case namedArg np of

            
src/full/Agda/Syntax/Internal.hs
  deriving (Data, Show)

clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats = map (fmap namedThing) . namedClausePats

instance HasRange Clause where
  getRange = clauseLHSRange

-- | Pattern variables.

            
src/full/Agda/Syntax/Internal.hs
  where named = if isUnderscore x then Nothing else Just $ unranged x

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
namedDBVarP m = (fmap . fmap) (\x -> DBPatVar x m) . namedVarP

-- | Make an absurd pattern with the given de Bruijn index.
absurdP :: Int -> DeBruijnPattern
absurdP = VarP PatOAbsurd . DBPatVar absurdPatternName


            
src/full/Agda/Syntax/Internal.hs

-- | Build 'ConInfo' from 'ConPatternInfo'.
fromConPatternInfo :: ConPatternInfo -> ConInfo
fromConPatternInfo = fromMaybe ConOCon . fmap patToConO . conPRecord
  where
    patToConO :: PatOrigin -> ConOrigin
    patToConO = \case
      PatOSystem -> ConOSystem
      PatOSplit  -> ConOSplit

            
src/full/Agda/Syntax/Internal.hs


instance PatternVars a (NamedArg (Pattern' a)) where
  patternVars = patternVars . fmap namedThing

instance PatternVars a b => PatternVars a [b] where
  patternVars = concatMap patternVars



            
src/full/Agda/Syntax/Internal.hs
-- | Convert a telescope to its list form.
telToList :: Tele (Dom t) -> [Dom (ArgName,t)]
telToList EmptyTel                    = []
telToList (ExtendTel arg (Abs x tel)) = fmap (x,) arg : telToList tel
telToList (ExtendTel _    NoAbs{}   ) = __IMPOSSIBLE__

-- | Lens to edit a 'Telescope' as a list.
listTel :: Lens' ListTel Telescope
listTel f = fmap telFromList . f . telToList

            
src/full/Agda/Syntax/Internal.hs

-- | Lens to edit a 'Telescope' as a list.
listTel :: Lens' ListTel Telescope
listTel f = fmap telFromList . f . telToList

-- | Drop the types from a telescope.
class TelToArgs a where
  telToArgs :: a -> [Arg ArgName]


            
src/full/Agda/Syntax/Internal.hs
    killRange8 Clause rl rf tel ps body t catchall unreachable

instance KillRange a => KillRange (Tele a) where
  killRange = fmap killRange

instance KillRange a => KillRange (Blocked a) where
  killRange = fmap killRange

instance KillRange a => KillRange (Abs a) where
  killRange = fmap killRange

instance KillRange a => KillRange (Elim' a) where
  killRange = fmap killRange

---------------------------------------------------------------------------
-- * UniverseBi instances.
---------------------------------------------------------------------------


            
src/full/Agda/Syntax/Internal.hs
  prettyPrec _ (DotP _o t)   = "." P.<> prettyPrec 10 t
  prettyPrec n (ConP c i nps)= mparens (n > 0 && not (null nps)) $
    pretty (conName c) <+> fsep (map (prettyPrec 10) ps)
    where ps = map (fmap namedThing) nps
  prettyPrec n (DefP o q nps)= mparens (n > 0 && not (null nps)) $
    pretty q <+> fsep (map (prettyPrec 10) ps)
    where ps = map (fmap namedThing) nps
  -- -- Version with printing record type:
  -- prettyPrec _ (ConP c i ps) = (if b then braces else parens) $ prTy $
  --   text (show $ conName c) <+> fsep (map (pretty . namedArg) ps)
  --   where
  --     b = maybe False (== ConOSystem) $ conPRecord i

            
src/full/Agda/Syntax/Notation.hs

    Example:
    @
       syntax fmap (λ x → e) xs = for x ∈ xs return e
    @

    The declared notation for @fmap@ is @for_∈_return_@ where the first hole is a binder.
-}

module Agda.Syntax.Notation where

import Control.DeepSeq

            
src/full/Agda/Syntax/Notation.hs
      holeMap = do
        (i, h) <- numberedHoles    -- v This range is filled in by mkPart
        let ri x = Ranged (getRange x) i
            normalHole y = NormalHole noRange $ fmap (ri y <$) h
        case namedArg h of
          ExprHole y       -> [(y, normalHole y)]
          LambdaHole x y
            | "_" <- rangedThing x -> [(x, WildHole (ri x)),         (y, normalHole y)]
            | otherwise            -> [(x, BindHole noRange (ri x)), (y, normalHole y)]

            
src/full/Agda/Syntax/Parser/Literate.hs
unMkLayers = map ((,) <$> layerRole <*> layerContent)

atomizeLayers :: Layers -> [(LayerRole, Char)]
atomizeLayers = (>>= fmap <$> ((,) . fst) <*> snd) . unMkLayers

-- | Type of a literate preprocessor:
--   Invariants:
--
--   > f : Processor

            
src/full/Agda/Syntax/Parser.hs
warning w = PM (modify (w:))

runPMIO :: (MonadIO m) => PM a -> m (Either ParseError a, [ParseWarning])
runPMIO = liftIO . fmap (second reverse) . flip runStateT [] . runExceptT . unPM

------------------------------------------------------------------------
-- Parse functions

-- | Wrapped Parser type.

            
src/full/Agda/Syntax/Position.hs
  setRange = const

instance SetRange a => SetRange [a] where
  setRange r = fmap $ setRange r

-- | Killing the range of an object sets all range information to 'noRange'.
class KillRange a where
  killRange :: KillRangeT a


            
src/full/Agda/Syntax/Position.hs
  killRange = map killRange

instance KillRange a => KillRange (NonemptyList a) where
  killRange = fmap killRange

-- | Overlaps with @KillRange [a]@.
instance {-# OVERLAPPING #-} KillRange String where
  killRange = id


            
src/full/Agda/Syntax/Position.hs
  killRange = id

instance {-# OVERLAPPABLE #-} KillRange a => KillRange (Map k a) where
  killRange = fmap killRange

instance {-# OVERLAPPABLE #-} (Ord a, KillRange a) => KillRange (Set a) where
  killRange = Set.map killRange

instance (KillRange a, KillRange b) => KillRange (a, b) where

            
src/full/Agda/Syntax/Position.hs
  killRange (x, y, z, u) = killRange4 (,,,) x y z u

instance KillRange a => KillRange (Maybe a) where
  killRange = fmap killRange

instance (KillRange a, KillRange b) => KillRange (Either a b) where
  killRange (Left  x) = Left  $ killRange x
  killRange (Right x) = Right $ killRange x


            
src/full/Agda/Syntax/Position.hs
    Just i  -> show i

instance Show a => Show (Range' (Maybe a)) where
  show = show . fmap Strict.toStrict

------------------------------------------------------------------------
-- Printing
------------------------------------------------------------------------


            
src/full/Agda/Syntax/Scope/Base.hs

-- | Disallow using generalized variables from the scope
disallowGeneralizedVars :: Scope -> Scope
disallowGeneralizedVars = mapScope_ ((fmap . map) disallow) id id
  where
    disallow a = a { anameKind = disallowGen (anameKind a) }
    disallowGen GeneralizeName = DisallowedGeneralizeName
    disallowGen k              = k