Aelve Codesearch

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

total matches: more than 1000

Agda-2.6.0.1
30 matches
src/full/Agda/Syntax/Scope/Base.hs
inScopeBecause :: (WhyInScope -> WhyInScope) -> Scope -> Scope
inScopeBecause f = mapScope_ mapName mapMod id
  where
    mapName = fmap . map $ \a -> a { anameLineage = f $ anameLineage a }
    mapMod  = fmap . map $ \a -> a { amodLineage  = f $ amodLineage a  }

-- | Get the public parts of the public modules of a scope
publicModules :: ScopeInfo -> Map A.ModuleName Scope
publicModules scope = Map.filterWithKey (\ m _ -> reachable m) allMods
  where

            
src/full/Agda/Syntax/Scope/Base.hs
      ModuleTag -> first (`AbsModule` Defined) <$> imported q

    imported :: C.QName -> Maybe (A.ModuleName, Access)
    imported q = fmap (,PublicAccess) $ Map.lookup q $ scopeImports root

    -- 3. Finding a name in the imports belonging to an initial part of the qualifier.

    imports :: [(a, Access)]
    imports = do

            
src/full/Agda/Syntax/Scope/Monad.hs
          filtName = filter $ \ y -> maybe True (Set.member (aName (fst y))) names
      caseListNe (filtKind $ filtName $ scopeLookup' x scope) (return UnknownName) $ \ case
        ds       | all ((ConName ==) . anameKind . fst) ds ->
          return $ ConstructorName $ fmap (upd . fst) ds

        ds       | all ((FldName ==) . anameKind . fst) ds ->
          return $ FieldName $ fmap (upd . fst) ds

        ds       | all ((PatternSynName ==) . anameKind . fst) ds ->
          return $ PatternSynResName $ fmap (upd . fst) ds

        (d, a) :! [] ->
          return $ DefinedName a $ upd d

        ds -> typeError $ AmbiguousName x (fmap (anameName . fst) ds)

            
src/full/Agda/Syntax/Scope/Monad.hs
        (d, a) :! [] ->
          return $ DefinedName a $ upd d

        ds -> typeError $ AmbiguousName x (fmap (anameName . fst) ds)
  where
  upd d = updateConcreteName d $ unqualify x
  updateConcreteName :: AbstractName -> C.Name -> AbstractName
  updateConcreteName d@(AbsName { anameName = A.QName qm qn }) x =
    d { anameName = A.QName (setRange (getRange x) qm) (qn { nameConcrete = x }) }

            
src/full/Agda/Syntax/Scope/Monad.hs
  ms <- scopeLookup x <$> getScope
  caseListNe ms (typeError $ NoSuchModule x) $ \ case
    AbsModule m why :! [] -> return $ AbsModule (m `withRangeOf` x) why
    ms                    -> typeError $ AmbiguousModule x (fmap amodName ms)

-- | Get the fixity of a not yet bound name.
getConcreteFixity :: C.Name -> ScopeM Fixity'
getConcreteFixity x = Map.findWithDefault noFixity' x . scopeFixities <$> getScope


            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
--   name in the current scope?
lookupNameInScope :: C.Name -> AbsToCon (Maybe A.Name)
lookupNameInScope y =
  fmap localVar . lookup y . scopeLocals <$> asks currentScope

-- | Have we already committed to a specific concrete name for this
--   abstract name? If yes, return the concrete name(s).
hasConcreteNames :: (MonadTCState m) => A.Name -> m [C.Name]
hasConcreteNames x = Map.findWithDefault [] x <$> useTC stConcreteNames

            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
  bindToConcrete x = bindName x

instance ToConcrete BindName C.BoundName where
  toConcrete       = fmap C.mkBoundName_ . toConcreteName . unBind
  bindToConcrete x = bindName (unBind x) . (. C.mkBoundName_)

instance ToConcrete A.QName C.QName where
  toConcrete = lookupQName AmbiguousConProjs


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

    toConcrete (A.Rec i fs) =
      bracket appBrackets $ do
        C.Rec (getRange i) . map (fmap (\x -> ModuleAssignment x [] defaultImportDir)) <$> toConcreteTop fs

    toConcrete (A.RecUpdate i e fs) =
      bracket appBrackets $ do
        C.RecUpdate (getRange i) <$> toConcrete e <*> toConcreteTop fs


            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
        | otherwise          -> bindToConcrete (map UserPattern args) $ ret . A.ConP i c
      A.DefP i f args        -> bindToConcrete (map UserPattern args) $ ret . A.DefP i f
      A.PatternSynP i f args -> bindToConcrete (map UserPattern args) $ ret . A.PatternSynP i f
      A.RecP i args          -> bindToConcrete ((map . fmap) UserPattern args) $ ret . A.RecP i
      A.AsP i x p            -> bindName' (unBind x) $
                                bindToConcrete (UserPattern p) $ \ p ->
                                ret (A.AsP i x p)
      A.WithP i p            -> bindToConcrete (UserPattern p) $ ret . A.WithP i


            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
  bindToConcrete (UserPattern np) ret =
    case getOrigin np of
      CaseSplit -> ret np
      _         -> bindToConcrete (fmap (fmap UserPattern) np) ret

-- Pass 2a: locate case-split pattern.  Don't bind anything!
instance ToConcrete (SplitPattern A.Pattern) A.Pattern where
  bindToConcrete (SplitPattern p) ret = do
    reportSLn "toConcrete.pat" 100 $ "binding pattern (pass 2a)" ++ show p

            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
      -- For patterns generated by case-split here, switch to freshening & binding.
      A.ConP i c args
        | patOrigin i == ConOSplit
                             -> bindToConcrete ((map . fmap . fmap) BindingPat args) $ ret . A.ConP i c
        | otherwise          -> bindToConcrete (map SplitPattern args) $ ret . A.ConP i c
      A.DefP i f args        -> bindToConcrete (map SplitPattern args) $ ret . A.DefP i f
      A.PatternSynP i f args -> bindToConcrete (map SplitPattern args) $ ret . A.PatternSynP i f
      A.RecP i args          -> bindToConcrete ((map . fmap) SplitPattern args) $ ret . A.RecP i
      A.AsP i x p            -> bindToConcrete (SplitPattern p)  $ \ p ->
                                ret (A.AsP i x p)
      A.WithP i p            -> bindToConcrete (SplitPattern p) $ ret . A.WithP i

instance ToConcrete (SplitPattern (NamedArg A.Pattern)) (NamedArg A.Pattern) where

            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
instance ToConcrete (SplitPattern (NamedArg A.Pattern)) (NamedArg A.Pattern) where
  bindToConcrete (SplitPattern np) ret =
    case getOrigin np of
      CaseSplit -> bindToConcrete (fmap (fmap BindingPat  ) np) ret
      _         -> bindToConcrete (fmap (fmap SplitPattern) np) ret


-- Pass 2b:
-- Takes care of freshening and binding pattern variables introduced by case split.
-- Still does not translate anything to Concrete.

            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
      A.LitP{}               -> ret p
      A.DotP{}               -> ret p
      A.EqualP{}             -> ret p
      A.ConP i c args        -> bindToConcrete ((map . fmap . fmap) BindingPat args) $ ret . A.ConP i c
      A.DefP i f args        -> bindToConcrete ((map . fmap . fmap) BindingPat args) $ ret . A.DefP i f
      A.PatternSynP i f args -> bindToConcrete ((map . fmap . fmap) BindingPat args) $ ret . A.PatternSynP i f
      A.RecP i args          -> bindToConcrete ((map . fmap)        BindingPat args) $ ret . A.RecP i
      A.AsP i x p            -> bindToConcrete (FreshenName x) $ \ x ->
                                bindToConcrete (BindingPat p)  $ \ p ->
                                ret (A.AsP i (BindName x) p)
      A.WithP i p            -> bindToConcrete (BindingPat p) $ ret . A.WithP i


            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
            go (y : ys) (arg : args)
              | visible arg
              , A.Var y' <- snd $ namedArg arg
              , y == y' = (fmap (YesSection <$) arg :) <$> go ys args
            go ys (arg : args)
              | visible arg, noXs arg = ((fmap . fmap) NoSection arg :) <$> go ys args
            go _ _ = Nothing

    view e = (, (map . fmap . fmap) NoSection args) <$> getHead hd
      where Application hd args = A.appView' e

tryToRecoverOpAppP :: A.Pattern -> AbsToCon (Maybe C.Pattern)
tryToRecoverOpAppP p = do
  res <- recoverOpApp bracketP_ (const False) opApp view p

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

    view :: A.Pattern -> Maybe (Hd, [NamedArg (MaybeSection (AppInfo, A.Pattern))])
    view p = case p of
      ConP _        cs ps -> Just (HdCon (headAmbQ cs), (map . fmap . fmap) (NoSection . (appInfo,)) ps)
      DefP _        fs ps -> Just (HdDef (headAmbQ fs), (map . fmap . fmap) (NoSection . (appInfo,)) ps)
      PatternSynP _ ns ps -> Just (HdSyn (headAmbQ ns), (map . fmap . fmap) (NoSection . (appInfo,)) ps)
      _                   -> Nothing
      -- ProjP _ _ d   -> Just (HdDef (headAmbQ d), [])   -- ? Andreas, 2016-04-21

recoverOpApp :: forall a c . (ToConcrete a c, HasRange c)
  => ((PrecedenceStack -> Bool) -> AbsToCon c -> AbsToCon c)

            
src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
                                         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.
    score :: Pattern' Void -> Int

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
          _ -> return ()
        -- and then we return the name
        return $ nameExpr d
      FieldName     ds     -> return $ A.Proj ProjPrefix $ AmbQ (fmap anameName ds)
      ConstructorName ds   -> return $ A.Con $ AmbQ (fmap anameName ds)
      UnknownName          -> notInScope x
      PatternSynResName ds -> return $ A.PatternSyn $ AmbQ (fmap anameName ds)

instance ToAbstract ResolveQName ResolvedName where
  toAbstract (ResolveQName x) = resolveName x >>= \case
    UnknownName -> notInScope x
    q -> return q

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
    where
      bindPatVar = VarPatName <.> bindPatternVariable
      patCon ds = do
        reportSLn "scope.pat" 10 $ "it was a con: " ++ prettyShow (fmap anameName ds)
        return $ ConPatName ds
      patSyn ds = do
        reportSLn "scope.pat" 10 $ "it was a pat syn: " ++ prettyShow (fmap anameName ds)
        return $ PatternSynPatName ds

-- | Translate and possibly bind a pattern variable
--   (which could have been bound before due to non-linearity).
bindPatternVariable :: C.Name -> ScopeM A.Name

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
  toAbstract = traverse toAbstract

instance ToAbstract C.LamBinding A.LamBinding where
  toAbstract (C.DomainFree x)  = A.DomainFree <$> toAbstract ((fmap . fmap) (NewName LambdaBound) x)
  toAbstract (C.DomainFull tb) = A.DomainFull <$> toAbstract tb

makeDomainFull :: C.LamBinding -> C.TypedBinding
makeDomainFull (C.DomainFull b) = b
makeDomainFull (C.DomainFree x) = C.TBind r [x] $ C.Underscore r Nothing

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
instance ToAbstract C.TypedBinding A.TypedBinding where
  toAbstract (C.TBind r xs t) = do
    t' <- toAbstractCtx TopCtx t
    xs' <- toAbstract $ (map . fmap . fmap) (NewName LambdaBound) xs
    return $ A.TBind r xs' t'
  toAbstract (C.TLet r ds) = A.TLet r <$> toAbstract (LetDefs ds)

-- | Scope check a module (top level function).
--

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
        VarName x' _                -> return . (False,) $ A.qnameFromList [x']
        DefinedName _ d             -> return . (False,) $ anameName d
        FieldName     (d :! [])     -> return . (False,) $ anameName d
        FieldName ds                -> genericError $ "Ambiguous projection " ++ prettyShow top ++ ": " ++ prettyShow (fmap anameName ds)
        ConstructorName (d :! [])   -> return . (False,) $ anameName d
        ConstructorName ds          -> genericError $ "Ambiguous constructor " ++ prettyShow top ++ ": " ++ prettyShow (fmap anameName ds)
        UnknownName                 -> notInScope top
        PatternSynResName (d :! []) -> return . (True,) $ anameName d
        PatternSynResName ds        -> genericError $ "Ambiguous pattern synonym" ++ prettyShow top ++ ": " ++ prettyShow (fmap anameName ds)

    lhs <- toAbstract $ LeftHandSide top lhs
    ps  <- case lhs of
             A.LHS _ (A.LHSHead _ ps) -> return ps
             _ -> err

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
mergeEqualPs :: [NamedArg (Pattern' e)] -> [NamedArg (Pattern' e)]
mergeEqualPs = go Nothing
  where
    go acc (Arg i (Named n (A.EqualP r es)) : ps) = go (fmap (fmap (++es)) acc `mplus` Just ((i,n,r),es)) ps
    go Nothing [] = []
    go Nothing (p : ps) = p : go Nothing ps
    go (Just ((i,n,r),es)) ps = Arg i (Named n (A.EqualP r es)) :
      case ps of
        (p : ps) -> p : go Nothing ps

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
          "Ill-formed projection pattern" P.<+> P.pretty (foldl C.AppP (C.IdentP d) ps1)
        qx <- resolveName d
        ds <- case qx of
                FieldName ds -> return $ fmap anameName ds
                UnknownName -> notInScope d
                _           -> genericError $
                  "head of copattern needs to be a field identifier, but "
                  ++ prettyShow d ++ " isn't one"
        A.LHSProj (AmbQ ds) <$> toAbstract l <*> (mergeEqualPs <$> toAbstract ps2)

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
      reportSLn "scope.pat" 60 $ "  resolved to VarPatName " ++ show y ++ " with range " ++ show (getRange y)
      return $ VarP $ A.BindName y
    ConPatName ds        -> return $ ConP (ConPatInfo ConOCon (PatRange r) ConPatEager)
                                          (AmbQ $ fmap anameName ds) []
    PatternSynPatName ds -> return $ PatternSynP (PatRange r)
                                                 (AmbQ $ fmap anameName ds) []

-- | Apply an abstract syntax pattern head to pattern arguments.
--
--   Fails with 'InvalidPattern' if head is not a constructor pattern
--   (or similar) that can accept arguments.

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
      A.DotP i (Ident x)   -> resolveName x >>= \case
        ConstructorName ds -> do
          let cpi = ConPatInfo ConOCon i ConPatLazy
              c   = AmbQ (fmap anameName ds)
          return $ A.ConP cpi c ps
        _ -> failure
      A.DotP{}    -> failure
      A.VarP{}    -> failure
      A.ProjP{}   -> failure

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
          -- Andreas, 2018-06-19, #3130
          -- We interpret .x as postfix projection if x is a field name in scope
          FieldName xs -> return $ A.ProjP (PatRange r) ProjPostfix $ AmbQ $
            fmap anameName xs
          _ -> fallback
        _ -> fallback

    toAbstract p0@(C.AbsurdP r)    = return $ A.AbsurdP (PatRange r)
    toAbstract (C.RecP r fs)       = A.RecP (PatRange r) <$> mapM (traverse toAbstract) fs

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
               )
      where
      set :: a -> NamedArg b -> NamedArg a
      set x arg = fmap (fmap (const x)) arg


{--------------------------------------------------------------------------
    Things we parse but are not part of the Agda file syntax
 --------------------------------------------------------------------------}

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

-- | Drops hidden arguments unless --show-implicit.
elims :: Expr -> [I.Elim' Expr] -> TCM Expr
elims e = nelims e . map (fmap unnamed)

-- Omitting information ---------------------------------------------------

noExprInfo :: ExprInfo
noExprInfo = ExprRange noRange

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
    flattenWith :: DisplayTerm -> (QName, [I.Elim' DisplayTerm], [I.Elim' DisplayTerm])
    flattenWith (DWithApp d ds1 es2) =
      let (f, es, ds0) = flattenWith d
      in  (f, es, ds0 ++ map (I.Apply . defaultArg) ds1 ++ map (fmap DTerm) es2)
    flattenWith (DDef f es) = (f, es, [])     -- .^ hacky, but we should only hit this when printing debug info
    flattenWith (DTerm (I.Def f es)) = (f, map (fmap DTerm) es, [])
    flattenWith _ = __IMPOSSIBLE__

    displayLHS
      :: A.Patterns   -- ^ Patterns to substituted into display term.
      -> DisplayTerm  -- ^ Display term.

            
src/full/Agda/Syntax/Translation/InternalToAbstract.hs
        -- Main action HERE:
        termToPat (DTerm (I.Var n [])) = return $ unArg $ fromMaybe __IMPOSSIBLE__ $ ps !!! n

        termToPat (DCon c ci vs)          = fmap unnamed <$> tryRecPFromConP =<< do
           A.ConP (ConPatInfo ci patNoRange ConPatEager) (unambiguous (conName c)) <$> mapM argToPat vs

        termToPat (DTerm (I.Con c ci vs)) = fmap unnamed <$> tryRecPFromConP =<< do
           A.ConP (ConPatInfo ci patNoRange ConPatEager) (unambiguous (conName c)) <$> mapM (elimToPat . fmap DTerm) vs

        termToPat (DTerm (I.Def _ [])) = return $ unnamed $ A.WildP patNoRange
        termToPat (DDef _ [])          = return $ unnamed $ A.WildP patNoRange

        termToPat (DTerm (I.Lit l))    = return $ unnamed $ A.LitP l