Aelve Codesearch

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

total matches: more than 1000

Agda-2.6.0.1
30 matches
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
                                    <*> viewTC (eCheckpoints . key local_chkpt)
            (,,) <$> viewTC (eCheckpoints . key chkpt) <*> pure tel <*> pure msub2
          let
              addNames []    es = map (fmap unnamed) es
              addNames _     [] = []
              addNames xs     (I.Proj{} : _) = __IMPOSSIBLE__
              addNames xs     (I.IApply x y r : es) =
                -- Needs to be I.Apply so it can have an Origin field.
                addNames xs (I.Apply (defaultArg r) : es)

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
              let (padVisNamed, padRest) = filterAndRest visible pad'

              -- Remove the names from the visible arguments.
              let padVis  = map (fmap (unnamed . namedThing)) padVisNamed

              -- Keep only the rest with the same visibility of @dom@...
              let padTail = filter (sameHiding dom) padRest

              -- ... and even the same name.

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
              let padTail = filter (sameHiding dom) padRest

              -- ... and even the same name.
              let padSame = filter ((Just (fst (unDom dom)) ==) . fmap rangedThing . nameOf . unArg) padTail

              return $ if null padTail || not showImp
                then (padVis           , map (fmap unnamed) es')
                else (padVis ++ padSame, nameFirstIfHidden dom es')

            -- If it is not a projection(-like) function, we need no padding.
            _ -> return ([], map (fmap unnamed) $ drop n es)

           reportSLn "reify.def" 70 $ unlines
             [ "  pad = " ++ show pad
             , "  nes = " ++ show nes
             ]

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
nameFirstIfHidden :: Dom (ArgName, t) -> [Elim' a] -> [Elim' (Named_ a)]
nameFirstIfHidden dom (I.Apply (Arg info e) : es) | notVisible info =
  I.Apply (Arg info (Named (Just $ unranged $ fst $ unDom dom) e)) :
  map (fmap unnamed) es
nameFirstIfHidden _ es =
  map (fmap unnamed) es

instance Reify i a => Reify (Named n i) (Named n a) where
  reify = traverse reify
  reifyWhen b = traverse (reifyWhen b)


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

data NamedClause = NamedClause QName Bool I.Clause
  -- ^ Also tracks whether module parameters should be dropped from the patterns.

-- The Monoid instance for Data.Map doesn't require that the values are a

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
              a'     = setNamedArg a $ A.WildP $ Info.PatRange $ getRange a
              goWild = stripName fixedPos a' : stripArgs True as

          stripName True  = fmap (unnamed . namedThing)
          stripName False = id

          -- TODO: vars appearing in EqualPs shouldn't be stripped.
          canStrip a = and
            [ notVisible a

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs

          isUnnamedHidden x = notVisible x && nameOf (unArg x) == Nothing && isNothing (isProjP x)

          stripArg a = fmap (fmap stripPat) a

          stripPat p = case p of
            A.VarP _      -> p
            A.ConP i c ps -> A.ConP i c $ stripArgs True ps
            A.ProjP{}     -> p

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
            A.LitP _      -> p
            A.AsP i x p   -> A.AsP i x $ stripPat p
            A.PatternSynP _ _ _ -> __IMPOSSIBLE__ -- p
            A.RecP i fs   -> A.RecP i $ map (fmap stripPat) fs  -- TODO Andreas: is this right?
            A.EqualP{}    -> p -- EqualP cannot be blanked.
            A.WithP i p   -> A.WithP i $ stripPat p -- TODO #2822: right?

          varOrDot A.VarP{}      = True
          varOrDot A.WildP{}     = True

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
  blank :: Set Name -> a -> a

  default blank :: (Functor f, BlankVars b, f b ~ a) => Set Name -> a -> a
  blank = fmap . blank

instance BlankVars a => BlankVars (Arg a)              where
instance BlankVars a => BlankVars (Named s a)          where
instance BlankVars a => BlankVars [a]                  where
-- instance BlankVars a => BlankVars (A.Pattern' a)       where  -- see case EqualP !

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
  where
    stripNameFromExplicit :: NamedArg p -> NamedArg p
    stripNameFromExplicit a
      | visible a = fmap (unnamed . namedThing) a
      | otherwise = a

    stripHidingFromPostfixProj :: IsProjP p => NamedArg p -> NamedArg p
    stripHidingFromPostfixProj a = case isProjP a of
      Just (o, _) | o /= ProjPrefix -> setHiding NotHidden a

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
    unview <- intervalUnview'
    forM sys $ \ (alpha,u) -> do
      rhs <- RHS <$> reify u <*> pure Nothing
      ep <- fmap (A.EqualP patNoRange) . forM alpha $ \ (phi,b) -> do
        let
            d True = unview IOne
            d False = unview IZero
        reify (phi, d b)


            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
          return $ A.Def sizeU
        I.PiSort s1 s2 -> do
          pis <- freshName_ ("piSort" :: String) -- TODO: hack
          (e1,e2) <- reify (s1, I.Lam defaultArgInfo $ fmap Sort s2)
          let app x y = A.App defaultAppInfo_ x (defaultNamedArg y)
          return $ A.Var pis `app` e1 `app` e2
        I.UnivSort s -> do
          univs <- freshName_ ("univSort" :: String) -- TODO: hack
          e <- reify s

            
src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs
toAbstractPats pats = case pats of
    []   -> return ([], [])
    p:ps -> do
      (names,  p)  <- (distributeF . fmap distributeF) <$> toAbstract p
      (namess, ps) <- local (names++) $ toAbstractPats ps
      return (namess++names, p:ps)

instance ToAbstract (QNamed R.Clause) A.Clause where
  toAbstract (QNamed name (R.Clause pats rhs)) = do

            
src/full/Agda/Termination/Inlining.hs
  -- Clauses are relative to the empty context, so we operate @inTopContext@.
  let noInline = return Nothing
  -- The de Bruijn indices of @body@ are relative to the @clauseTel cl@.
  body <- fmap stripDontCare <$> instantiate (clauseBody cl)
  case body of
    Just (Def wf els) -> do
      isWith <- isWithFunction wf
      reportSDoc "term.with.inline" 20 $ sep
        [ "inlineWithClauses: isWithFunction ="

            
src/full/Agda/Termination/Inlining.hs
--   to "not containing a call to a mutually defined function".
--
--   Note that the @as@ stem from the *unraised* clause body of @cl@
--   and thus can be simply 'fmap'ped back there (under all the 'Bind'
--   abstractions).
--
--   Precondition: we are 'inTopContext'.
withExprClauses :: Clause -> Type -> Args -> TCM [Clause]
withExprClauses cl t args = {- addContext (clauseTel cl) $ -} loop t args where

            
src/full/Agda/Termination/Inlining.hs

    dispToPats :: DisplayTerm -> TCM ([NamedArg Pattern], Permutation)
    dispToPats (DWithApp (DDef _ es) ws zs) = do
      let es' = es ++ map (Apply . defaultArg) ws ++ map (fmap DTerm) zs
      (ps, (j, ren)) <- (`runStateT` (0, [])) $ mapM (traverse dtermToPat) es'
      let perm = Perm j (map snd $ List.sort ren)
      return (map ePatToPat ps, perm)
    dispToPats t = __IMPOSSIBLE__


            
src/full/Agda/Termination/Inlining.hs
    skip = modify $ \(j, is) -> (j + 1, is)

    ePatToPat :: Elim' Pattern -> NamedArg Pattern
    ePatToPat (Apply p) = fmap unnamed p
    ePatToPat (IApply x y p) = defaultNamedArg p
    ePatToPat (Proj o d) = defaultNamedArg $ ProjP o d

    dtermToPat :: DisplayTerm -> StateT (Int, [(Int, Int)]) TCM Pattern
    dtermToPat v =

            
src/full/Agda/Termination/Inlining.hs
    dtermToPat v =
      case v of
        DWithApp{}       -> __IMPOSSIBLE__   -- I believe
        DCon c ci vs     -> ConP c (toConPatternInfo ci) . map (fmap unnamed)
                              <$> mapM (traverse dtermToPat) vs
        DDef d es        -> do
          ifM (return (null es) `and2M` do isJust <$> lift (isProjection d))
            {-then-} (return $ ProjP ProjPrefix d)
            {-else-} (dotP (dtermToTerm v) <$ skip)

            
src/full/Agda/Termination/Inlining.hs
        DTerm (Var i []) ->
          ifM (bindVar i) (varP . nameToPatVarName <$> lift (nameOfBV i))
                          (pure $ dotP (Var i []))
        DTerm (Con c ci vs) -> ConP c (toConPatternInfo ci) . map (fmap unnamed) <$>
                              mapM (traverse (dtermToPat . DTerm)) (fromMaybe __IMPOSSIBLE__ $ allApplyElims vs)
        DTerm v          -> dotP v <$ skip

isWithFunction :: MonadTCM tcm => QName -> tcm (Maybe QName)
isWithFunction x = liftTCM $ do

            
src/full/Agda/Termination/Monad.hs
  suc <- sizeSucName

  -- The name of sharp (if available).
  sharp <- fmap nameOfSharp <$> coinductionKit

  -- Andreas, 2014-08-28
  -- We do not inline with functions if --without-K.
  inlineWithFunctions <- not <$> withoutKOption


            
src/full/Agda/Termination/Monad.hs
terGetPatterns = do
  n   <- terAsks terPatternsRaise
  mps <- terAsks terPatterns
  return $ if n == 0 then mps else map (fmap (raise n)) mps

terSetPatterns :: MaskedDeBruijnPatterns -> TerM a -> TerM a
terSetPatterns ps = terLocal $ \ e -> e { terPatterns = ps }

terRaise :: TerM a -> TerM a

            
src/full/Agda/Termination/Monad.hs
  return b
  where
    isProjectionButNotCoinductive' qn = do
      flat <- fmap nameOfFlat <$> coinductionKit
      if Just qn == flat
        then return False
        else do
          mp <- isProjection qn
          case mp of

            
src/full/Agda/Termination/Monad.hs
isCoinductiveProjection :: MonadTCM tcm => Bool -> QName -> tcm Bool
isCoinductiveProjection mustBeRecursive q = liftTCM $ do
  reportSLn "term.guardedness" 40 $ "checking isCoinductiveProjection " ++ prettyShow q
  flat <- fmap nameOfFlat <$> coinductionKit
  -- yes for ♭
  if Just q == flat then return True else do
    pdef <- getConstInfo q
    case isProjection_ (theDef pdef) of
      Just Projection{ projProper = Just{}, projFromType = Arg _ r, projIndex = n } ->

            
src/full/Agda/Termination/TermCheck.hs
instance TermToPattern Term DeBruijnPattern where
  termToPattern t = (liftTCM $ constructorForm t) >>= \case
    -- Constructors.
    Con c _ args -> ConP c noConPatternInfo . map (fmap unnamed) <$> termToPattern (fromMaybe __IMPOSSIBLE__ $ allApplyElims args)
    Def s [Apply arg] -> do
      suc <- terGetSizeSuc
      if Just s == suc then ConP (ConHead s Inductive []) noConPatternInfo . map (fmap unnamed) <$> termToPattern [arg]
       else return $ dotP t
    DontCare t  -> termToPattern t -- OR: __IMPOSSIBLE__  -- removed by stripAllProjections
    -- Leaves.
    Var i []    -> varP . (`DBPatVar` i) . prettyShow <$> nameOfBV i
    Lit l       -> return $ LitP l

            
src/full/Agda/Termination/TermCheck.hs
  -- Count the number of coinductive projection(pattern)s in caller and callee.
  -- Only recursive coinductive projections are eligible (Issue 1209).
  projsCaller <- length <$> do
    filterM (isCoinductiveProjection True) $ mapMaybe (fmap (headAmbQ . snd) . isProjP . getMasked) pats
  projsCallee <- length <$> do
    filterM (isCoinductiveProjection True) $ mapMaybe (fmap snd . isProjElim) es
  cutoff <- terGetCutOff
  let ?cutoff = cutoff
  useGuardedness <- liftTCM guardednessOption
  let guardedness =
        if useGuardedness

            
src/full/Agda/TypeChecking/Abstract.hs
    UnreducedLevel v -> UnreducedLevel $ absTerm u v

instance AbsTerm a => AbsTerm (Elim' a) where
  absTerm = fmap . absTerm

instance AbsTerm a => AbsTerm (Arg a) where
  absTerm = fmap . absTerm

instance AbsTerm a => AbsTerm (Dom a) where
  absTerm = fmap . absTerm

instance AbsTerm a => AbsTerm [a] where
  absTerm = fmap . absTerm

instance AbsTerm a => AbsTerm (Maybe a) where
  absTerm = fmap . absTerm

instance (Subst Term a, AbsTerm a) => AbsTerm (Abs a) where
  absTerm u (NoAbs x v) = NoAbs x $ absTerm u v
  absTerm u (Abs   x v) = Abs x $ swap01 $ absTerm (raise 1 u) v


            
src/full/Agda/TypeChecking/CheckInternal.hs
    eraseIfNonvariant :: [Polarity] -> Elims -> Elims
    eraseIfNonvariant []                  es             = es
    eraseIfNonvariant pols                []             = []
    eraseIfNonvariant (Nonvariant : pols) (e : es) = (fmap DontCare e) : eraseIfNonvariant pols es
    eraseIfNonvariant (_          : pols) (e : es) = e : eraseIfNonvariant pols es

-- | Entry point for term checking.
checkInternal :: Term -> Type -> TCM ()
checkInternal v t = void $ checkInternal' defaultAction v t

            
src/full/Agda/TypeChecking/CheckInternal.hs
          sa  = getSort a
          sb  = getSort (unAbs b)
          mkDom v = El sa v <$ a
          mkRng v = fmap (v <$) b
          -- Preserve NoAbs
          goInside = case b of Abs{}   -> addContext (absName b, a)
                               NoAbs{} -> id
      a <- mkDom <$> checkInternal' action (unEl $ unDom a) (sort sa)
      -- TODO: checkPTS sa sb s

            
src/full/Agda/TypeChecking/CompiledClause/Compile.hs
        [ "compiled clauses"
        , nest 2 $ return $ P.pretty cc
        ]
      return (Just splitTree, fmap precomputeFreeVars_ cc)

-- | Stripped-down version of 'Agda.Syntax.Internal.Clause'
--   used in clause compiler.
data Cl = Cl
  { clPats :: [Arg Pattern]

            
src/full/Agda/TypeChecking/CompiledClause/Compile.hs
-- | Strip down a clause. Don't forget to apply the substitution to the dot
--   patterns!
unBruijn :: Clause -> Cl
unBruijn c = Cl (applySubst sub $ (map . fmap) (fmap dbPatVarName . namedThing) $ namedClausePats c)
                (applySubst sub $ clauseBody c)
  where
    sub = renamingR $ fromMaybe __IMPOSSIBLE__ (clausePerm c)

compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses