Aelve Codesearch

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

total matches: more than 1000

Agda-2.6.0.1
30 matches
src/full/Agda/TypeChecking/CompiledClause/Compile.hs
         -- When the split tree is finished, we continue with @compile@.
        updLits = Map.mapWithKey $ \ l cl ->
          caseMaybe (lookup (SplitLit l) ts) compile compileWithSplitTree cl
        updCatchall = fmap $ caseMaybe (lookup SplitCatchall ts) compile compileWithSplitTree
    compiles _ Branches{etaBranch = Just{}} = __IMPOSSIBLE__  -- we haven't inserted eta matches yet

compile :: Cls -> CompiledClauses
compile [] = Fail
compile cs = case nextSplit cs of

            
src/full/Agda/TypeChecking/CompiledClause/Compile.hs
compile :: Cls -> CompiledClauses
compile [] = Fail
compile cs = case nextSplit cs of
  Just (isRecP, n) -> Case n $ fmap compile $ splitOn isRecP (unArg n) cs
  Nothing -> case clBody c of
    -- It's possible to get more than one clause here due to
    -- catch-all expansion.
    Just t  -> Done (map (fmap name) $ clPats c) t
    Nothing -> Fail
  where
    -- If there are more than one clauses, take the first one.
    c = headWithDefault __IMPOSSIBLE__ cs
    name (VarP _ x) = x

            
src/full/Agda/TypeChecking/CompiledClause/Compile.hs
-- | @splitOn single n cs@ will force expansion of catch-alls
--   if @single@.
splitOn :: Bool -> Int -> Cls -> Case Cls
splitOn single n cs = mconcat $ map (fmap (:[]) . splitC n) $
  -- (\ cs -> trace ("splitting on " ++ show n ++ " after expandCatchAlls " ++ show single ++ ": " ++ prettyShow (P.prettyList cs)) cs) $
    expandCatchAlls single n cs

splitC :: Int -> Cl -> Case Cl
splitC n (Cl ps b) = caseMaybe mp fallback $ \case

            
src/full/Agda/TypeChecking/CompiledClause/Compile.hs
  ProjP _ d   -> projCase d $ Cl (ps0 ++ ps1) b
  IApplyP{}   -> fallback
  ConP c i qs -> (conCase (conName c) (conPFallThrough i) $ WithArity (length qs) $
                   Cl (ps0 ++ map (fmap namedThing) qs ++ ps1) b) { lazyMatch = conPLazy i }
  DefP o q qs -> (conCase q False $ WithArity (length qs) $
                   Cl (ps0 ++ map (fmap namedThing) qs ++ ps1) b) { lazyMatch = False }
  LitP l      -> litCase l $ Cl (ps0 ++ ps1) b
  VarP{}      -> fallback
  DotP{}      -> fallback
  where
    (ps0, rest) = splitAt n ps

            
src/full/Agda/TypeChecking/CompiledClause/Compile.hs
            m        = length qs'
            -- replace all direct subpatterns of q by _
            -- TODO Andrea: might need these to sometimes be IApply?
            conPArgs = map (fmap ($> varP "_")) qs'
            conArgs  = zipWith (\ q' i -> q' $> var i) qs' $ downFrom m
        LitP l -> Cl (ps0 ++ [q $> LitP l] ++ ps1) (substBody n' 0 (Lit l) b)
        DefP o d qs' -> Cl (ps0 ++ [q $> DefP o d conPArgs] ++ ps1)
                            (substBody n' m (Def d (map Apply conArgs)) b)
          where

            
src/full/Agda/TypeChecking/CompiledClause/Compile.hs
          where
            m        = length qs'
            -- replace all direct subpatterns of q by _
            conPArgs = map (fmap ($> varP "_")) qs'
            conArgs  = zipWith (\ q' i -> q' $> var i) qs' $ downFrom m
        _ -> __IMPOSSIBLE__
      where
        -- Andreas, 2016-09-19 issue #2168
        -- Due to varying function arity, some clauses might be eta-contracted.

            
src/full/Agda/TypeChecking/CompiledClause/Match.hs

matchCompiled :: CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
matchCompiled c args = do
  r <- matchCompiledE c $ map (fmap Apply) args
  case r of
    YesReduction simpl v -> return $ YesReduction simpl v
    NoReduction bes      -> return $ NoReduction $ fmap (map (fromMaybe __IMPOSSIBLE__ . isApplyElim)) bes

-- | @matchCompiledE c es@ takes a function given by case tree @c@ and
--   and a spine @es@ and tries to apply the function to @es@.
matchCompiledE :: CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
matchCompiledE c args = match' [(c, args, id)]

            
src/full/Agda/TypeChecking/CompiledClause.hs
-- * KillRange instances.

instance KillRange c => KillRange (WithArity c) where
  killRange = fmap killRange

instance KillRange c => KillRange (Case c) where
  killRange (Branches cop con eta lit all b lazy) = Branches cop
    (killRangeMap con)
    (killRange eta)

            
src/full/Agda/TypeChecking/Conversion.hs
    -- equality at function type (accounts for eta)
    equalFun :: Sort -> Term -> Term -> Term -> TCM ()
    equalFun s a@(Pi dom b) m n | domFinite dom = do
       mp <- fmap getPrimName <$> getBuiltin' builtinIsOne
       case unEl $ unDom dom of
          Def q [Apply phi]
              | Just q == mp -> compareTermOnFace cmp (unArg phi) (El s (Pi (dom {domFinite = False}) b)) m n
          _                  -> equalFun s (Pi (dom{domFinite = False}) b) m n
    equalFun _ (Pi dom@Dom{domInfo = info} b) m n | not $ domFinite dom = do

            
src/full/Agda/TypeChecking/Coverage/Match.hs
match cs ps = foldr choice (return No) $ zipWith matchIt [0..] cs
  where
    matchIt :: (MonadReduce m , HasConstInfo m , HasBuiltins m) => Nat -> Clause -> m (Match (Nat,[SplitAssignment]))
    matchIt i c = fmap (i,) <$> matchClause ps c

-- | For each variable in the patterns of a split clause, we remember the
--   de Bruijn-index and the literals excluded by previous matches.
data SplitPatVar = SplitPatVar
  { splitPatVarName   :: PatVarName

            
src/full/Agda/TypeChecking/Coverage/Match.hs
  debruijnNamedVar n i = toSplitVar (debruijnNamedVar n i)

toSplitPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg SplitPattern]
toSplitPatterns = (fmap . fmap . fmap . fmap) toSplitVar

fromSplitPatterns :: [NamedArg SplitPattern] -> [NamedArg DeBruijnPattern]
fromSplitPatterns = (fmap . fmap . fmap . fmap) fromSplitVar

instance DeBruijn SplitPattern where
  debruijnNamedVar n i  = varP $ SplitPatVar n i []
  deBruijnView _        = Nothing


            
src/full/Agda/TypeChecking/Coverage/Match.hs
type SplitPSubstitution = Substitution' SplitPattern

toSplitPSubst :: PatternSubstitution -> SplitPSubstitution
toSplitPSubst = (fmap . fmap) toSplitVar

fromSplitPSubst :: SplitPSubstitution -> PatternSubstitution
fromSplitPSubst = (fmap . fmap) fromSplitVar

applySplitPSubst :: (Subst Term a) => SplitPSubstitution -> a -> a
applySplitPSubst = applyPatSubst . fromSplitPSubst

-- TODO: merge this instance and the one for DeBruijnPattern in

            
src/full/Agda/TypeChecking/Coverage/Match.hs
unDotP (DotP o v) = reduce v >>= \case
  Var i [] -> return $ deBruijnVar i
  Con c _ vs -> do
    let ps = map (fmap $ unnamed . DotP o) $ fromMaybe __IMPOSSIBLE__ $ allApplyElims vs
    return $ ConP c noConPatternInfo ps
  Lit l -> return $ LitP l
  v     -> return $ dotP v
unDotP p = return p


            
src/full/Agda/TypeChecking/Coverage/Match.hs
     | otherwise -> return Nothing
isLitP (ConP c ci [a]) | visible a && isRelevant a = do
  Con suc _ [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSuc
  if | c == suc  -> fmap inc <$> isLitP (namedArg a)
     | otherwise -> return Nothing
  where
    inc :: Literal -> Literal
    inc (LitNat r n) = LitNat (fuseRange c r) $ n + 1
    inc _ = __IMPOSSIBLE__

            
src/full/Agda/TypeChecking/Coverage.hs
    No        ->  do
      reportSLn "tc.cover" 20 $ "pattern is not covered"
      -- TODO Andrea: add hcomp clause!
      case fmap getHiding target of
        Just h | isInstance h -> do
          -- Ulf, 2016-10-31: For now we only infer instance clauses. It would
          -- make sense to do it also for hidden, but since the value of a
          -- hidden clause is expected to be forced by later clauses, it's too
          -- late to add it now. If it was inferrable we would have gotten a

            
src/full/Agda/TypeChecking/Coverage.hs
      -> (SplitError -> TCM CoverResult)
      -> TCM CoverResult
    continue xs allowPartialCover handle = do
      r <- altM1 (\ x -> fmap (,x) <$> split Inductive allowPartialCover sc x) xs
      case r of
        Left err -> handle err
        -- If we get the empty covering, we have reached an impossible case
        -- and are done.
        Right (Covering n [], _) ->

            
src/full/Agda/TypeChecking/Coverage.hs
          --          map (mapArgInfo hiddenInserted) $ tele2NamedArgs gamma0 gamma
          -- -- Andreas, 2016-09-08, issue #2166: use gamma0 for correct argument names
          defp = DefP PatOSystem hCompName . map (setOrigin Inserted) $
                   map (fmap unnamed) [setHiding Hidden $ defaultArg $ applySubst rho1 $ DotP PatOSystem $ dlvl
                                      ,setHiding Hidden $ defaultArg $ applySubst rho1 $ DotP PatOSystem $ dterm]
                   ++ applySubst rho2 (teleNamedArgs gamma) -- rho0?
      -- Compute final context and substitution
      let rho3    = consS defp rho1            -- Δ₁' ⊢ ρ₃ : Δ₁(x:D)
          delta2' = applySplitPSubst rho3 delta2  -- Δ₂' = Δ₂ρ₃

            
src/full/Agda/TypeChecking/Coverage.hs

  let preserve (x, t@(El _ (Def d' _))) | d == d' = (n, t)
      preserve (x, t) = (x, t)
      gammal = map (fmap preserve) . telToList $ gamma0
      gamma  = telFromList gammal
      delta1Gamma = delta1 `abstract` gamma

  debugInit con ctype d pars ixs cixs delta1 delta2 gamma tel ps hix


            
src/full/Agda/TypeChecking/Coverage.hs
      -> BlockingVar
      -> TCM (Either SplitError Covering)
split ind allowPartialCover sc x =
  fmap blendInAbsurdClause <$> split' NoCheckEmpty ind allowPartialCover YesFixTarget sc x
  where
    n = lookupPatternVar sc $ blockingVarNo x
    blendInAbsurdClause :: Either SplitClause Covering -> Covering
    blendInAbsurdClause = fromRight (const $ Covering n [])


            
src/full/Agda/TypeChecking/Coverage.hs
        cons <- case checkEmpty of
          CheckEmpty   -> ifM (liftTCM $ inContextOfT $ isEmptyType $ unDom t) (pure []) (pure cons')
          NoCheckEmpty -> pure cons'
        mns  <- forM cons $ \ con -> fmap (SplitCon con,) <$>
          computeNeighbourhood delta1 n delta2 d pars ixs x tel ps cps con
        hcompsc <- if isHIT then case fixtarget of YesFixTarget -> computeHCompSplit delta1 n delta2 d pars ixs x tel ps cps; _ -> return Nothing
                            else return Nothing
        return $ (dr, catMaybes (mns ++ [hcompsc]))


            
src/full/Agda/TypeChecking/Coverage.hs
splitResult :: QName -> SplitClause -> TCM (Either SplitError [SplitClause])
splitResult f sc = do
  caseMaybeM (splitResultPath f sc)
             ((fmap . fmap) splitClauses $ splitResultRecord f sc)
             (return . Right . (:[]))


-- | Tries to split the result to introduce an IApply pattern.
splitResultPath :: QName -> SplitClause -> TCM (Maybe SplitClause)

            
src/full/Agda/TypeChecking/Coverage.hs
            dType <- defType <$> do getConstInfo $ unArg proj -- WRONG: typeOfConst $ unArg proj
            let -- type of projection instantiated at self
                target' = Just $ proj $> dType `piApply` pargs      -- Always visible (#2287)
                projArg = fmap (Named Nothing . ProjP projOrigin) $ setHiding NotHidden proj
                sc' = sc { scPats   = scPats sc ++ [projArg]
                         , scSubst  = idS
                         , scTarget = target'
                         }
            return (SplitCon (unArg proj), sc')

            
src/full/Agda/TypeChecking/Datatypes.hs
isDataOrRecord :: Term -> TCM (Maybe QName)
isDataOrRecord v = do
  case v of
    Def d _ -> fmap (const d) <$> isDataOrRecordType d
    _       -> return Nothing

getNumberOfParameters :: QName -> TCM (Maybe Nat)
getNumberOfParameters d = do
  def <- getConstInfo d

            
src/full/Agda/TypeChecking/DisplayForm.hs
dtermToTerm dt = case dt of
  DWithApp d ds es ->
    dtermToTerm d `apply` map (defaultArg . dtermToTerm) ds `applyE` es
  DCon c ci args   -> Con c ci $ map (Apply . fmap dtermToTerm) args
  DDef f es        -> Def f $ map (fmap dtermToTerm) es
  DDot v           -> v
  DTerm v          -> v

-- | Get the arities of all display forms for a name.
displayFormArities :: QName -> TCM [Int]

            
src/full/Agda/TypeChecking/DisplayForm.hs
instance SubstWithOrigin (Arg DisplayTerm) where
  substWithOrigin rho ots (Arg ai dt) =
    case dt of
      DTerm v        -> fmap DTerm $ substWithOrigin rho ots $ Arg ai v
      DDot  v        -> Arg ai $ DDot      $ applySubst rho v
      DDef q es      -> Arg ai $ DDef q    $ substWithOrigin rho ots es
      DCon c ci args -> Arg ai $ DCon c ci $ substWithOrigin rho ots args
      DWithApp t ts es -> Arg ai $ DWithApp
        (substWithOrigin rho ots t)

            
src/full/Agda/TypeChecking/Errors.hs
             map (pretty . dropTopLevel) $
               concatMap termErrFunctions because)
        $$ fwords "Problematic calls:"
        $$ (nest 2 $ fmap (P.vcat . nub) $
              mapM prettyTCM $ sortBy (compare `on` callInfoRange) $
              concatMap termErrCalls because)

    UnreachableClauses f pss -> fsep $
      pwords "Unreachable" ++ pwords (plural (length pss) "clause")

            
src/full/Agda/TypeChecking/Errors.hs
      [pretty o] ++ pwords "flag from a module which does."

prettyTCWarnings :: [TCWarning] -> TCM String
prettyTCWarnings = fmap (unlines . intersperse "") . prettyTCWarnings'

prettyTCWarnings' :: [TCWarning] -> TCM [String]
prettyTCWarnings' = mapM (fmap show . prettyTCM)

-- | Turns all warnings into errors.
tcWarningsToError :: [TCWarning] -> TCM a
tcWarningsToError ws = typeError $ case ws of
  [] -> SolvedButOpenHoles

            
src/full/Agda/TypeChecking/Errors.hs
  -- For some reason some SafeFlagPragma seem to be created multiple times.
  -- This is a way to collect all of them and remove duplicates.
  let pragmas w = case tcWarning w of { SafeFlagPragma ps -> ([w], ps); _ -> ([], []) }
  let sfp = case fmap nub (foldMap pragmas ws) of
              (TCWarning r w p b:_, sfp) ->
                 [TCWarning r (SafeFlagPragma sfp) p b]
              _                        -> []

  warnSet <- do

            
src/full/Agda/TypeChecking/Errors.hs
    -- Gallais, 2016-05-14
    -- Given where `NonFatalErrors` are created, we know for a
    -- fact that ̀ws` is non-empty.
    TypeError _ Closure{ clValue = NonFatalErrors ws } -> foldr1 ($$) $ fmap prettyTCM ws
    -- Andreas, 2014-03-23
    -- This use of localState seems ok since we do not collect
    -- Benchmark info during printing errors.
    TypeError s e -> localTCState $ do
      putTC s

            
src/full/Agda/TypeChecking/Errors.hs
          | all (isOrdinary . namedArg) xs =
            pretty $
              foldl (C.App r) (C.Ident op) $
                (map . fmap . fmap) fromOrdinary xs
          | any (isPlaceholder . namedArg) xs =
              pretty e <+> "(section)"
        unambiguous e = pretty e

        isOrdinary :: MaybePlaceholder (C.OpApp e) -> Bool