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/TypeChecking/LevelConstraints.hs
    free = List.nub . runFree (:[]) IgnoreNot  -- Note: use a list to preserve order of variables
    xs  = free (a, b)
    ys  = free (c, d)
    rho = mkSub $ List.sort $ zip ys xs
    mkSub = go 0
      where
        go _ [] = IdS
        go y ren0@((y', x) : ren)
          | y == y'   = Var x [] :# go (y + 1) ren

            
src/full/Agda/TypeChecking/MetaVars.hs

-- * Creating meta variables.

-- | Create a sort meta that cannot be instantiated with 'Inf' (Setω).
newSortMetaBelowInf :: TCM Sort
newSortMetaBelowInf = do
  x <- newSortMeta
  hasBiggerSort x
  return x

            
src/full/Agda/TypeChecking/MetaVars.hs
  hasBiggerSort x
  return x

-- | Create a sort meta that may be instantiated with 'Inf' (Setω).
newSortMeta :: TCM Sort
newSortMeta =
  ifM hasUniversePolymorphism (newSortMetaCtx =<< getContextArgs)
  -- else (no universe polymorphism)
  $ do i   <- createMetaInfo

            
src/full/Agda/TypeChecking/MetaVars.hs
       x   <- newMeta Instantiable i normalMetaPriority (idP 0) $ IsSort () __DUMMY_TYPE__
       return $ MetaS x []

-- | Create a sort meta that may be instantiated with 'Inf' (Setω).
newSortMetaCtx :: Args -> TCM Sort
newSortMetaCtx vs = do
    i   <- createMetaInfo
    tel <- getContextTelescope
    let t = telePi_ tel __DUMMY_TYPE__

            
src/full/Agda/TypeChecking/MetaVars.hs
    let t = telePi_ tel __DUMMY_TYPE__
    x   <- newMeta Instantiable i normalMetaPriority (idP $ size tel) $ IsSort () t
    reportSDoc "tc.meta.new" 50 $
      "new sort meta" <+> prettyTCM x <+> ":" <+> prettyTCM t
    return $ MetaS x $ map Apply vs

newTypeMeta :: Sort -> TCM Type
newTypeMeta s = El s . snd <$> newValueMeta RunMetaOccursCheck (sort s)

newTypeMeta_ ::  TCM Type
newTypeMeta_  = newTypeMeta =<< (workOnTypes $ newSortMeta)
-- TODO: (this could be made work with new uni-poly)
-- Andreas, 2011-04-27: If a type meta gets solved, than we do not have to check

            
src/full/Agda/TypeChecking/MetaVars.hs
newTypeMeta_  = newTypeMeta =<< (workOnTypes $ newSortMeta)
-- TODO: (this could be made work with new uni-poly)
-- Andreas, 2011-04-27: If a type meta gets solved, than we do not have to check
-- that it has a sort.  The sort comes from the solution.
-- newTypeMeta_  = newTypeMeta Inf

-- | @newInstanceMeta s t cands@ creates a new instance metavariable
--   of type the output type of @t@ with name suggestion @s@.
newInstanceMeta :: MetaNameSuggestion -> Type -> TCM (MetaId, Term)

            
src/full/Agda/TypeChecking/MetaVars.hs
assignMeta :: Int -> MetaId -> Type -> [Int] -> Term -> TCM ()
assignMeta m x t ids v = do
  let n    = length ids
      cand = List.sort $ zip ids $ map var $ downFrom n
  assignMeta' m x t n cand v

-- | @assignMeta' m x t ids u@ solves @x = [ids]u@ for meta @x@ of type @t@,
--   where term @u@ lives in a context of length @m@,
--   and @ids@ is a partial substitution.

            
src/full/Agda/TypeChecking/MetaVars.hs
    --   v' = (λ a b c d e. v) _ 1 _ 2 0
    --
    -- Andreas, 2013-10-25 Solve using substitutions:
    -- Convert assocList @ids@ (which is sorted) into substitution,
    -- filling in __IMPOSSIBLE__ for the missing terms, e.g.
    -- [(0,0),(1,2),(3,1)] --> [0, 2, __IMP__, 1, __IMP__]
    -- ALT 1: O(m * size ids), serves as specification
    -- let ivs = [fromMaybe __IMPOSSIBLE__ $ lookup i ids | i <- [0..m-1]]
    -- ALT 2: O(m)

            
src/full/Agda/TypeChecking/MetaVars.hs
          checkInternal v' a
        IsSort{}  -> void $ do
          reportSDoc "tc.meta.check" 30 $ nest 2 $
            prettyTCM v' <+> " is a sort"
          checkSort defaultAction =<< shouldBeSort (El __DUMMY_SORT__ v')

    reportSDoc "tc.meta.assign" 10 $
      "solving" <+> prettyTCM x <+> ":=" <+> prettyTCM vsol


            
src/full/Agda/TypeChecking/MetaVars.hs
--   Otherwise, raise the error.
checkLinearity :: SubstCand -> ExceptT () TCM SubstCand
checkLinearity ids0 = do
  let ids = List.sortBy (compare `on` fst) ids0  -- see issue 920
  let grps = groupOn fst ids
  concat <$> mapM makeLinear grps
  where
    -- | Non-determinism can be healed if type is singleton. [Issue 593]
    --   (Same as for irrelevance.)

            
src/full/Agda/TypeChecking/MetaVars.hs

      -- Debug.
      reportSDoc "meta.postulate" 20 $ vcat
        [ text ("Turning " ++ if isSortMeta_ mv then "sort" else "value" ++ " meta ")
            <+> prettyTCM (MetaId x) <+> " into postulate."
        , nest 2 $ vcat
          [ "Name: " <+> prettyTCM q
          , "Type: " <+> prettyTCM t
          ]

            
src/full/Agda/TypeChecking/Monad/Base.hs
-- | Parametrized since it is used without MetaId when creating a new meta.
data Judgement a
  = HasType { jMetaId :: a, jMetaType :: Type }
  | IsSort  { jMetaId :: a, jMetaType :: Type } -- Andreas, 2011-04-26: type needed for higher-order sort metas

instance Show a => Show (Judgement a) where
    show (HasType a t) = show a ++ " : " ++ show t
    show (IsSort  a t) = show a ++ " :sort " ++ show t

-----------------------------------------------------------------------------
-- ** Generalizable variables
-----------------------------------------------------------------------------


            
src/full/Agda/TypeChecking/Monad/Base.hs
        | WrongNumberOfConstructorArguments QName Nat Nat
        | ShouldBeEmpty Type [DeBruijnPattern]
        | ShouldBeASort Type
            -- ^ The given type should have been a sort.
        | ShouldBePi Type
            -- ^ The given type should have been a pi.
        | ShouldBePath Type
        | ShouldBeRecordType Type
        | ShouldBeRecordPattern DeBruijnPattern

            
src/full/Agda/TypeChecking/Monad/Base.hs
        | NotAProjectionPattern (NamedArg A.Pattern)
        | NotAProperTerm
        | InvalidTypeSort Sort
            -- ^ This sort is not a type expression.
        | InvalidType Term
            -- ^ This term is not a type expression.
        | FunctionTypeInSizeUniv Term
            -- ^ This term, a function type constructor, lives in
            --   @SizeUniv@, which is not allowed.

            
src/full/Agda/TypeChecking/Positivity.hs
instance ComputeOccurrences Clause where
  occurrences cl = do
    let ps    = namedClausePats cl
        items = IntMap.elems $ patItems ps -- sorted from low to high DBI
    (Concat (mapMaybe matching (zip [0..] ps)) >+<) <$>
      withExtendedOccEnv' items (occurrences $ clauseBody cl)
    where
      matching (i, p)
        | properlyMatching (namedThing $ unArg p) =

            
src/full/Agda/TypeChecking/Positivity.hs
           map (\(i, n) ->
                   text (show i) <> ":" <+> text (show n) <+>
                   "occurrences") $
           List.sortBy (compare `on` snd) $
           Map.toList (flatten occs))

      -- Placing this line before the reportSDoc lines above creates a
      -- space leak: occs is retained for too long.
      es <- computeEdges qs q occs

            
src/full/Agda/TypeChecking/Primitive.hs
  t <- runNamesT [] $
       hPi' "a" (el $ cl primLevel) $ \ a ->
       hPi' "c" (el $ cl primLevel) $ \ c ->
       hPi' "A" (sort . tmSort <$> a) $ \ bA ->
       hPi' "x" (el' a bA) $ \ x ->
       nPi' "C" (nPi' "y" (el' a bA) $ \ y ->
                 (el' a $ cl primId <#> a <#> bA <@> x <@> y) --> (sort . tmSort <$> c)) $ \ bC ->
       (el' c $ bC <@> x <@>
            (cl primConId <#> a <#> bA <#> x <#> x <@> cl primIOne
                       <@> lam "i" (\ _ -> x))) -->
       (hPi' "y" (el' a bA) $ \ y ->
        nPi' "p" (el' a $ cl primId <#> a <#> bA <@> x <@> y) $ \ p ->

            
src/full/Agda/TypeChecking/Primitive.hs
  t <- runNamesT [] $
       hPi' "a" (el $ cl primLevel) $ \ a ->
       hPi' "c" (el $ cl primLevel) $ \ c ->
       hPi' "A" (sort . tmSort <$> a) $ \ bA ->
       hPi' "x" (el' a bA) $ \ x ->
       nPi' "C" (nPi' "y" (el' a bA) $ \ y ->
                 (el' a $ cl primId <#> a <#> bA <@> x <@> y) --> (sort . tmSort <$> c)) $ \ bC ->
       (nPi' "φ" (elInf $ cl primInterval) $ \ phi ->
        nPi' "y" (elInf $ cl primSub <#> a <@> bA <@> phi <@> (lam "o" $ const x)) $ \ y ->
        let pathxy = (cl primPath <#> a <@> bA <@> x <@> oucy)
            oucy = (cl primSubOut <#> a <#> bA <#> phi <#> (lam "o" $ const x) <@> y)
            reflx = (lam "o" $ \ _ -> lam "i" $ \ _ -> x) -- TODO Andrea, should block on o

            
src/full/Agda/TypeChecking/Primitive.hs
  t <- runNamesT [] $
       (hPi' "a" (el $ cl primLevel) $ \ a ->
        nPi' "φ" (elInf (cl primInterval)) $ \ _ ->
        nPi' "A" (sort . tmSort <$> a) $ \ bA ->
        return (sort $ Inf))
  isOne <- primIsOne
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 3 $ \ ts -> do
    case ts of
      [l,phi,a] -> do
          (El s (Pi d b)) <- runNamesT [] $ do

            
src/full/Agda/TypeChecking/Primitive.hs
       (hPi' "a" (el $ cl primLevel) $ \ a ->
        nPi' "φ" (elInf (cl primInterval)) $ \ phi ->
        nPi' "A" (pPi' "o" phi $ \ _ -> el' (cl primLevelSuc <@> a) (Sort . tmSort <$> a)) $ \ bA ->
        return (sort $ Inf))
  let toFinitePi :: Type -> Term
      toFinitePi (El _ (Pi d b)) = Pi (setRelevance Irrelevant $ d { domFinite = True }) b
      toFinitePi _               = __IMPOSSIBLE__
  v <- runNamesT [] $
        lam "a" $ \ l ->

            
src/full/Agda/TypeChecking/Primitive.hs
  requireCubical
  t <- runNamesT [] $
       hPi' "a" (el $ cl primLevel) $ \ a ->
       hPi' "A" (sort . tmSort <$> a) $ \ bA ->
       hPi' "x" (el' a bA) $ \ x ->
       hPi' "y" (el' a bA) $ \ y ->
       (el' a $ cl primId <#> a <#> bA <@> x <@> y)
       --> elInf (cl primInterval)
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 5 $ \ ts -> do

            
src/full/Agda/TypeChecking/Primitive.hs
  requireCubical
  t <- runNamesT [] $
       hPi' "a" (el $ cl primLevel) $ \ a ->
       hPi' "A" (sort . tmSort <$> a) $ \ bA ->
       hPi' "x" (el' a bA) $ \ x ->
       hPi' "y" (el' a bA) $ \ y ->
       (el' a $ cl primId <#> a <#> bA <@> x <@> y)
       --> (el' a $ cl primPath <#> a <#> bA <@> x <@> y)
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 5 $ \ ts -> do

            
src/full/Agda/TypeChecking/Primitive.hs
  requireCubical
  t    <- runNamesT [] $
          hPi' "a" (elInf (cl primInterval) --> (el $ cl primLevel)) $ \ a ->
          nPi' "A" (nPi' "i" (elInf (cl primInterval)) $ \ i -> (sort . tmSort <$> (a <@> i))) $ \ bA ->
          nPi' "φ" (elInf $ cl primInterval) $ \ phi ->
          (el' (a <@> cl primIZero) (bA <@> cl primIZero) --> el' (a <@> cl primIOne) (bA <@> cl primIOne))
  return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 4 $ \ ts nelims -> do
    primTransHComp DoTransp ts nelims


            
src/full/Agda/TypeChecking/Primitive.hs
  requireCubical
  t    <- runNamesT [] $
          hPi' "a" (el $ cl primLevel) $ \ a ->
          hPi' "A" (sort . tmSort <$> a) $ \ bA ->
          hPi' "φ" (elInf $ cl primInterval) $ \ phi ->
          (nPi' "i" (elInf $ cl primInterval) $ \ i -> pPi' "o" phi $ \ _ -> el' a bA) -->
          (el' a bA --> el' a bA)
  return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 5 $ \ ts nelims -> do
    primTransHComp DoHComp ts nelims

            
src/full/Agda/TypeChecking/Primitive.hs
  requireCubical
  t    <- runNamesT [] $
          hPi' "a" (elInf (cl primInterval) --> (el $ cl primLevel)) $ \ a ->
          nPi' "A" (nPi' "i" (elInf (cl primInterval)) $ \ i -> (sort . tmSort <$> (a <@> i))) $ \ bA ->
          nPi' "φ" (elInf $ cl primInterval) $ \ phi ->
          (nPi' "i" (elInf $ cl primInterval) $ \ i -> pPi' "o" phi $ \ _ -> el' (a <@> i) (bA <@> i)) -->
          (el' (a <@> cl primIZero) (bA <@> cl primIZero) --> el' (a <@> cl primIOne) (bA <@> cl primIOne))
  one <- primItIsOne
  io  <- primIOne

            
src/full/Agda/TypeChecking/Primitive.hs
  t <- runNamesT [] $
       (hPi' "la" (el $ cl primLevel) $ \ la ->
       hPi' "lb" (el $ cl primLevel) $ \ lb ->
       nPi' "A" (sort . tmSort <$> la) $ \ a ->
       hPi' "φ" (elInf $ cl primInterval) $ \ φ ->
       nPi' "T" (pPi' "o" φ $ \ o -> el' (cl primLevelSuc <@> lb) (Sort . tmSort <$> lb)) $ \ t ->
       (pPi' "o" φ $ \ o -> el' (cl primLevelMax <@> la <@> lb) $ cl primEquiv <#> lb <#> la <@> (t <@> o) <@> a)
       --> (sort . tmSort <$> lb))
  view <- intervalView'
  one <- primItIsOne
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ts ->
    case ts of
     [la,lb,a,phi,t,e] -> do

            
src/full/Agda/TypeChecking/Primitive.hs
  t <- runNamesT [] $
       (hPi' "la" (el $ cl primLevel) $ \ la ->
       hPi' "lb" (el $ cl primLevel) $ \ lb ->
       hPi' "A" (sort . tmSort <$> la) $ \ a ->
       hPi' "φ" (elInf $ cl primInterval) $ \ φ ->
       hPi' "T" (pPi' "o" φ $ \ o ->  el' (cl primLevelSuc <@> lb) (Sort . tmSort <$> lb)) $ \ t ->
       hPi' "e" (pPi' "o" φ $ \ o -> el' (cl primLevelMax <@> la <@> lb) $ cl primEquiv <#> lb <#> la <@> (t <@> o) <@> a) $ \ e ->
       (pPi' "o" φ $ \ o -> el' lb (t <@> o)) --> (el' la a --> el' lb (cl primGlue <#> la <#> lb <@> a <#> φ <@> t <@> e)))
  view <- intervalView'

            
src/full/Agda/TypeChecking/Primitive.hs
  t <- runNamesT [] $
       (hPi' "la" (el $ cl primLevel) $ \ la ->
       hPi' "lb" (el $ cl primLevel) $ \ lb ->
       hPi' "A" (sort . tmSort <$> la) $ \ a ->
       hPi' "φ" (elInf $ cl primInterval) $ \ φ ->
       hPi' "T" (pPi' "o" φ $ \ o ->  el' (cl primLevelSuc <@> lb) (Sort . tmSort <$> lb)) $ \ t ->
       hPi' "e" (pPi' "o" φ $ \ o -> el' (cl primLevelMax <@> la <@> lb) $ cl primEquiv <#> lb <#> la <@> (t <@> o) <@> a) $ \ e ->
       (el' lb (cl primGlue <#> la <#> lb <@> a <#> φ <@> t <@> e)) --> el' la a)
  view <- intervalView'

            
src/full/Agda/TypeChecking/Primitive.hs
genPrimForce b ret = do
  let varEl s a = El (varSort s) <$> a
      varT s a  = varEl s (varM a)
      varS s    = pure $ sort $ varSort s
  t <- hPi "a" (el primLevel) $
       hPi "b" (el primLevel) $
       hPi "A" (varS 1) $
       hPi "B" (varT 2 0 --> varS 1) b
  return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \ ts ->

            
src/full/Agda/TypeChecking/Primitive.hs
                Con{}      -> return True
                Lam{}      -> return True
                Pi{}       -> return True
                Sort{}     -> return True  -- sorts and levels are considered whnf
                Level{}    -> return True
                DontCare{} -> return True
                Def q _    -> do
                  def <- theDef <$> getConstInfo q
                  return $ case def of