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/Translation/ConcreteToAbstract.hs
          GeneralizeName -> do
            gvs <- useTC stGeneralizedVars
            case gvs of   -- Subtle: Use (left-biased) union instead of insert to keep the old name if
                          -- already present. This way we can sort by source location when generalizing
                          -- (Issue 3354).
                Just s -> stGeneralizedVars `setTCLens` Just (s `Set.union` Set.singleton (anameName d))
                Nothing -> typeError $ GeneralizeNotSupportedHere $ anameName d
          DisallowedGeneralizeName -> do
            typeError . GenericDocError =<<

            
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
      withLocalVars $ do
        -- Minor hack: record types don't have indices so we include t when
        -- computing generalised parameters, but in the type checker any named
        -- generalizable arguments in the sort should be bound variables.
        (ls', _) <- toAbstract (GenTelAndType (map makeDomainFull ls) t)
        t'  <- toAbstract t
        f   <- getConcreteFixity x
        x'  <- freshAbstractQName f x
        bindName' p DefName (GeneralizedVarsMetadata $ generalizeTelVars ls') x x'

            
src/full/Agda/Termination/Inlining.hs
    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__

    bindVar i = do
      (j, is)  <- get

            
src/full/Agda/Termination/SparseMatrix.hs
{- | Sparse matrices.

We assume the matrices to be very sparse, so we just implement them as
sorted association lists.

Most operations are linear in the number of non-zero elements.

An exception is transposition, which needs to sort the association
list again; it has the complexity of sorting: @n log n@ where @n@ is
the number of non-zero elements.

Another exception is matrix multiplication, of course.

 -}

            
src/full/Agda/Termination/SparseMatrix.hs

fromIndexList :: (Ord i, HasZero b) => Size i -> [(MIx i, b)] -> Matrix i b
fromIndexList sz = Matrix sz
                 . List.sortBy (compare `on` fst)
                 . filter ((zeroElement /=) . snd)

-- | @'fromLists' sz rs@ constructs a matrix from a list of lists of
--   values (a list of rows).
--   @O(size)@ where @size = rows × cols@.

            
src/full/Agda/Termination/SparseMatrix.hs
instance Ord i => Transpose (Matrix i b) where
  transpose (Matrix size m) =
    Matrix (transpose size) $
      List.sortBy (compare `on` fst) $
        map (mapFst transpose) m


-- | General pointwise combination function for association lists.
--   @O(n1 + n2)@ where @ni@ is the number of non-zero element in matrix @i@.

            
src/full/Agda/Termination/TermCheck.hs
  extract (a, b) = CallGraph.union <$> extract a <*> extract b

-- | Sorts can contain arbitrary terms of type @Level@,
--   so look for recursive calls also in sorts.
--   Ideally, 'Sort' would not be its own datatype but just
--   a subgrammar of 'Term', then we would not need this boilerplate.

instance ExtractCalls Sort where
  extract s = do

            
src/full/Agda/Termination/TermCheck.hs
instance ExtractCalls Sort where
  extract s = do
    liftTCM $ do
      reportSDoc "term.sort" 20 $
        "extracting calls from sort" <+> prettyTCM s
      reportSDoc "term.sort" 50 $
        text ("s = " ++ show s)
    case s of
      Inf        -> return empty
      SizeUniv   -> return empty
      Type t     -> terUnguarded $ extract t  -- no guarded levels

            
src/full/Agda/TypeChecking/Conversion.hs
        _            -> throwError err

antiUnifyType :: ProblemId -> Type -> Type -> TCM Type
antiUnifyType pid (El s a) (El _ b) = El s <$> antiUnify pid (sort s) a b

antiUnifyElims :: ProblemId -> Type -> Term -> Elims -> Elims -> TCM Term
antiUnifyElims pid a self [] [] = return self
antiUnifyElims pid a self (Proj o f : es1) (Proj _ g : es2) | f == g = do
  res <- projectTyped self a o f

            
src/full/Agda/TypeChecking/Conversion.hs
        reportSDoc "tc.conv.type" 50 $ vcat
          [ "compareType" <+> sep [ prettyTCM ty1 <+> prettyTCM cmp
                                       , prettyTCM ty2 ]
          , hsep [ "   sorts:", prettyTCM s1, " and ", prettyTCM s2 ]
          ]
-- Andreas, 2011-4-27 should not compare sorts, but currently this is needed
-- for solving sort and level metas
        compareSort CmpEq s1 s2 `catchError` \err -> case err of
          TypeError _ e -> do
            reportSDoc "tc.conv.type" 30 $ vcat
              [ "sort comparison failed"
              , nest 2 $ vcat
                [ "s1 =" <+> prettyTCM s1
                , "s2 =" <+> prettyTCM s2
                ]
              ]

            
src/full/Agda/TypeChecking/Conversion.hs
                ]
              ]
            -- This error will probably be more informative
            compareTerm cmp (sort s1) a1 a2
            -- Throw the original error if the above doesn't
            -- give an error (for instance, due to pending
            -- constraints).
            -- Or just ignore it... We run into this with irrelevant levels
            -- which may show up in sort constraints, causing them to fail.

            
src/full/Agda/TypeChecking/Conversion.hs
            -- give an error (for instance, due to pending
            -- constraints).
            -- Or just ignore it... We run into this with irrelevant levels
            -- which may show up in sort constraints, causing them to fail.
            -- In any case it's not safe to ignore the error, for instance
            -- a1 might be Set and a2 a meta of type Set, in which case we
            -- really need the sort comparison to fail, instead of silently
            -- instantiating the meta.
            -- Andreas, 2013-10-31 Maybe the error went away
            -- when we compared the types.  So we try the sort comparison
            -- again, this time not catching the error.  (see Issue 930)
            -- throwError err
            compareSort CmpEq s1 s2
          _             -> throwError err
        compareTerm cmp (sort s1) a1 a2

            
src/full/Agda/TypeChecking/Conversion.hs
            -- throwError err
            compareSort CmpEq s1 s2
          _             -> throwError err
        compareTerm cmp (sort s1) a1 a2
        return ()

leqType :: Type -> Type -> TCM ()
leqType = compareType CmpLeq


            
src/full/Agda/TypeChecking/Conversion.hs
compareSort CmpEq  = equalSort
compareSort CmpLeq = leqSort

-- | Check that the first sort is less or equal to the second.
--
--   We can put @SizeUniv@ below @Inf@, but otherwise, it is
--   unrelated to the other universes.
--
leqSort :: Sort -> Sort -> TCM ()

            
src/full/Agda/TypeChecking/Conversion.hs
  let postpone = addConstraint (SortCmp CmpLeq s1 s2)
      no       = typeError $ NotLeqSort s1 s2
      yes      = return ()
  reportSDoc "tc.conv.sort" 30 $
    sep [ "leqSort"
        , nest 2 $ fsep [ prettyTCM s1 <+> "=<"
                        , prettyTCM s2 ]
        ]
  propEnabled <- isPropEnabled

            
src/full/Agda/TypeChecking/Conversion.hs
  badRigid <- s1 `rigidVarsNotContainedIn` fvsRHS

  case (s1, s2) of
      -- Andreas, 2018-09-03: crash on dummy sort
      (DummyS s, _) -> impossibleSort s
      (_, DummyS s) -> impossibleSort s

      -- The most basic rule: @Set l =< Set l'@ iff @l =< l'@
      (Type a  , Type b  ) -> leqLevel a b

            
src/full/Agda/TypeChecking/Conversion.hs
      (Prop a  , Type b  ) -> leqLevel a b
      (Type a  , Prop b  ) -> no

      -- Setω is the top sort
      (_       , Inf     ) -> yes
      (Inf     , _       ) -> equalSort s1 s2

      -- @SizeUniv@ and @Prop0@ are bottom sorts.
      -- So is @Set0@ if @Prop@ is not enabled.
      (_       , SizeUniv) -> equalSort s1 s2
      (_       , Prop (Max [])) -> equalSort s1 s2
      (_       , Type (Max []))
        | not propEnabled  -> equalSort s1 s2

            
src/full/Agda/TypeChecking/Conversion.hs
      (SizeUniv, Type{}  ) -> no
      (SizeUniv, Prop{}  ) -> no

      -- If the first sort rigidly depends on a variable and the second
      -- sort does not mention this variable, the second sort must be Inf.
      (_       , _       ) | badRigid -> equalSort s2 Inf

      -- This shouldn't be necessary
      (UnivSort Inf , UnivSort Inf) -> yes


            
src/full/Agda/TypeChecking/Conversion.hs
      (MetaS{} , _       ) -> postpone
      (_       , MetaS{} ) -> postpone

      -- DefS are postulated sorts, so they do not reduce.
      (DefS d es , DefS d' es') | d == d' -> postpone
      (DefS{} , _     ) -> no
      (_      , DefS{}) -> no

  where

            
src/full/Agda/TypeChecking/Conversion.hs
  where
  impossibleSort s = do
    reportSLn "impossible" 10 $ unlines
      [ "leqSort: found dummy sort with description:"
      , s
      ]
    __IMPOSSIBLE__

leqLevel :: Level -> Level -> TCM ()

            
src/full/Agda/TypeChecking/Conversion.hs
      -- let cs = Set.filter (not . hasMeta) $ Set.intersection as bs
      -- as <- return $ Set.toList $ as Set.\\ cs
      -- bs <- return $ Set.toList $ bs Set.\\ cs
      as <- return $ List.sort $ closed0 as
      bs <- return $ List.sort $ closed0 bs
      reportSDoc "tc.conv.level" 40 $
        sep [ "equalLevel"
            , vcat [ nest 2 $ sep [ prettyTCM a <+> "=="
                                  , prettyTCM b
                                  ]

            
src/full/Agda/TypeChecking/Conversion.hs
          [ n | Plus n y <- ys, x == y, m < n ]


-- | Check that the first sort equal to the second.
equalSort :: Sort -> Sort -> TCM ()
equalSort s1 s2 = do
    catchConstraint (SortCmp CmpEq s1 s2) $ do
        (s1,s2) <- reduce (s1,s2)
        let postpone = addConstraint (SortCmp CmpEq s1 s2)

            
src/full/Agda/TypeChecking/Conversion.hs
              if | equal     -> yes
                 | otherwise -> postpone

        reportSDoc "tc.conv.sort" 30 $ sep
          [ "equalSort"
          , vcat [ nest 2 $ fsep [ prettyTCM s1 <+> "=="
                                 , prettyTCM s2 ]
                 , nest 2 $ fsep [ pretty s1 <+> "=="
                                 , pretty s2 ]

            
src/full/Agda/TypeChecking/Conversion.hs

        case (s1, s2) of

            -- Andreas, 2018-09-03: crash on dummy sort
            (DummyS s, _) -> impossibleSort s
            (_, DummyS s) -> impossibleSort s

            -- one side is a meta sort: try to instantiate
            -- In case both sides are meta sorts, instantiate the
            -- bigger (i.e. more recent) one.
            (MetaS x es , MetaS y es')
              | x == y                 -> synEq
              | x < y                  -> meta y es' s1
              | otherwise              -> meta x es s2

            
src/full/Agda/TypeChecking/Conversion.hs
            (MetaS x es , _          ) -> meta x es s2
            (_          , MetaS x es ) -> meta x es s1

            -- Other blocked sorts: check syntactic equality
            (PiSort{}    , PiSort{}   ) -> synEq
            (UnivSort{}  , UnivSort{} ) -> synEq

            -- diagonal cases for rigid sorts
            (Type a     , Type b     ) -> equalLevel a b
            (SizeUniv   , SizeUniv   ) -> yes
            (Prop a     , Prop b     ) -> equalLevel a b
            (Inf        , Inf        ) -> yes


            
src/full/Agda/TypeChecking/Conversion.hs
            (UnivSort{} , _          ) -> postpone
            (_          , UnivSort{} ) -> postpone

            -- postulated sorts can only be equal if they have the same head
            (DefS d es  , DefS d' es') | d == d' -> synEq

            -- any other combinations of sorts are not equal
            (_          , _          ) -> no

    where
      -- perform assignment (MetaS x es) := s
      meta x es s = do

            
src/full/Agda/TypeChecking/Conversion.hs
    where
      -- perform assignment (MetaS x es) := s
      meta x es s = do
        reportSLn "tc.meta.sort" 30 $ "Assigning meta sort"
        reportSDoc "tc.meta.sort" 50 $ "meta" <+> sep [pretty x, prettyList $ map pretty es, pretty s]
        assignE DirEq x es (Sort s) __IMPOSSIBLE__

      set0 = Type $ Max []
      prop0 = Prop $ Max []


            
src/full/Agda/TypeChecking/Conversion.hs
      set0 = Type $ Max []
      prop0 = Prop $ Max []

      -- equate @piSort a b@ to @s0@, which is assumed to be a (closed) bottom sort
      -- i.e. @piSort a b == s0@ implies @b == s0@.
      piSortEqualsBottom s0 a b = do
        underAbstraction_ b $ equalSort s0
        -- we may have instantiated some metas, so @a@ could reduce
        a <- reduce a

            
src/full/Agda/TypeChecking/Conversion.hs
          Nothing -> addConstraint $ SortCmp CmpEq (funSort a s0) s0
      impossibleSort s = do
        reportSLn "impossible" 10 $ unlines
          [ "equalSort: found dummy sort with description:"
          , s
          ]
        __IMPOSSIBLE__



            
src/full/Agda/TypeChecking/Coverage.hs
    , nest 2 $ "tel  =" <+> prettyTCM tel
    , nest 2 $ "ps   =" <+> do addContext tel $ prettyTCMPatternList $ fromSplitPatterns ps
    , nest 2 $ "target =" <+> do addContext tel $ maybe (text "<none>") prettyTCM target
    , nest 2 $ "target sort =" <+> do addContext tel $ maybe (text "<none>") (prettyTCM . getSort . unArg) target
    ]
  match cs ps >>= \case
    Yes (i,mps) -> do
      exact <- allM (map snd mps) isTrivialPattern
      let cl0 = indexWithDefault __IMPOSSIBLE__ cs i