Aelve Codesearch

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

total matches: more than 1000

Agda-2.6.0.1
30 matches
src/full/Agda/TypeChecking/Rules/Data.hs
              -- error which we replace by a more understandable error
              -- in case of a suspected dependency.
              s <- newSortMetaBelowInf
              catchError_ (addContext ixTel $ equalType s0 $ raise nofIxs $ sort s) $ \ err ->
                  if any (`freeIn` s0) [0..nofIxs - 1] then typeError . GenericDocError =<<
                     fsep [ "The sort of" <+> prettyTCM name
                          , "cannot depend on its indices in the type"
                          , prettyTCM t0
                          ]
                  else throwError err
              reduce s

            
src/full/Agda/TypeChecking/Rules/Data.hs
              reduce s

            -- when `--without-K`, all the indices should fit in the
            -- sort of the datatype (see #3420).
            let s' = case s of
                  Prop l -> Type l
                  _      -> s
            whenM withoutKOption $ checkIndexSorts s' ixTel


            
src/full/Agda/TypeChecking/Rules/Data.hs
                  _      -> s
            whenM withoutKOption $ checkIndexSorts s' ixTel

            reportSDoc "tc.data.sort" 20 $ vcat
              [ "checking datatype" <+> prettyTCM name
              , nest 2 $ vcat
                [ "type (parameters instantiated):   " <+> prettyTCM t0
                , "type (full):   " <+> prettyTCM t
                , "sort:   " <+> prettyTCM s

            
src/full/Agda/TypeChecking/Rules/Data.hs
              , nest 2 $ vcat
                [ "type (parameters instantiated):   " <+> prettyTCM t0
                , "type (full):   " <+> prettyTCM t
                , "sort:   " <+> prettyTCM s
                , "indices:" <+> text (show nofIxs)
                , "gparams:" <+> text (show parNames)
                , "params: " <+> text (show $ deepUnscope ps)
                ]
              ]

            
src/full/Agda/TypeChecking/Rules/Data.hs
            dataDef{ dataCons = cons }


-- | Ensure that the type is a sort.
--   If it is not directly a sort, compare it to a 'newSortMetaBelowInf'.
forceSort :: Type -> TCM Sort
forceSort t = reduce (unEl t) >>= \case
  Sort s -> return s
  _      -> do
    s <- newSortMetaBelowInf

            
src/full/Agda/TypeChecking/Rules/Data.hs
  Sort s -> return s
  _      -> do
    s <- newSortMetaBelowInf
    equalType t (sort s)
    return s


-- | Type check a constructor declaration. Checks that the constructor targets
--   the datatype and that it fits inside the declared sort.

            
src/full/Agda/TypeChecking/Rules/Data.hs


-- | Type check a constructor declaration. Checks that the constructor targets
--   the datatype and that it fits inside the declared sort.
--   Returns the non-linear parameters.
checkConstructor
  :: QName         -- ^ Name of data type.
  -> UniverseCheck -- ^ Check universes?
  -> Telescope     -- ^ Parameter telescope.

            
src/full/Agda/TypeChecking/Rules/Data.hs
        (t, isPathCons) <- checkConstructorType e d
        -- compute which constructor arguments are forced
        forcedArgs <- computeForcingAnnotations c t
        -- check that the sort (universe level) of the constructor type
        -- is contained in the sort of the data type
        -- (to avoid impredicative existential types)
        debugFitsIn s
        -- To allow propositional squash, we turn @Prop ℓ@ into @Set ℓ@
        -- for the purpose of checking the type of the constructors.
        let s' = case s of

            
src/full/Agda/TypeChecking/Rules/Data.hs
-- * Special cases of Type
-----------------------------------------------------------

-- | A @Type@ with sort @Type l@
--   Such a type supports both hcomp and transp.
data LType = LEl Level Term deriving (Eq,Show)

fromLType :: LType -> Type
fromLType (LEl l t) = El (Type l) t

            
src/full/Agda/TypeChecking/Rules/Data.hs

toLType :: MonadReduce m => Type -> m (Maybe LType)
toLType ty = do
  sort <- reduce $ getSort ty
  case sort of
    Type l -> return $ Just $ LEl l (unEl ty)
    _      -> return $ Nothing

instance Subst Term LType where
  applySubst rho (LEl l t) = LEl (applySubst rho l) (applySubst rho t)

            
src/full/Agda/TypeChecking/Rules/Data.hs
instance Subst Term LType where
  applySubst rho (LEl l t) = LEl (applySubst rho l) (applySubst rho t)

-- | A @Type@ that either has sort @Type l@ or is a closed definition.
--   Such a type supports some version of transp.
--   In particular we want to allow the Interval as a @ClosedType@.
data CType = ClosedType QName | LType LType deriving (Eq,Show)

fromCType :: CType -> Type

            
src/full/Agda/TypeChecking/Rules/Data.hs

toCType :: MonadReduce m => Type -> m (Maybe CType)
toCType ty = do
  sort <- reduce $ getSort ty
  case sort of
    Type l -> return $ Just $ LType (LEl l (unEl ty))
    Inf    -> do
      t <- reduce (unEl ty)
      case t of
        Def q [] -> return $ Just $ ClosedType q

            
src/full/Agda/TypeChecking/Rules/Data.hs
               (absApp <$> rect' <*> pure iz) --> (absApp <$> rect' <*> pure io)

  reportSDoc "trans.rec" 20 $ prettyTCM theType
  reportSDoc "trans.rec" 60 $ text $ "sort = " ++ show (getSort rect')

  noMutualBlock $ addConstant theName $ (defaultDefn defaultArgInfo theName theType
    (emptyFunction { funTerminates = Just True }))
    { defNoCompilation = True }
  -- ⊢ Γ = gamma = (δ : Δ^I) (φ : I) (u0 : R (δ i0))

            
src/full/Agda/TypeChecking/Rules/Data.hs
        let
          filled_ty = lam_i $ (unEl . fromCType . unDom) filled_ty'
          -- Γ ⊢ l : I -> Level of filled_ty
        -- sort <- reduce $ getSort $ unDom filled_ty'
        case unDom filled_ty' of
          LType (LEl l _) -> do
            let lvl = lam_i $ Level l
            return $ runNames [] $ do
             lvl <- open lvl

            
src/full/Agda/TypeChecking/Rules/Data.hs
               rect --> rect

  reportSDoc "hcomp.rec" 20 $ prettyTCM theType
  reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (lTypeLevel rect)

  noMutualBlock $ addConstant theName $ (defaultDefn defaultArgInfo theName theType
    (emptyFunction { funTerminates = Just True }))
    { defNoCompilation = True }
  --   ⊢ Γ = gamma = (δ : Δ) (φ : I) (_ : (i : I) -> Partial φ (R δ)) (_ : R δ)

            
src/full/Agda/TypeChecking/Rules/Data.hs
  let -- Γ ⊢ R δ
      drect_gamma = raiseS (size gamma - size delta) `applySubst` rect

  reportSDoc "hcomp.rec" 60 $ text $ "sort = " ++ show (lTypeLevel drect_gamma)

  let

      -- (γ : Γ) ⊢ hcompR γ : rtype
      compTerm = Def theName [] `apply` teleArgs gamma

            
src/full/Agda/TypeChecking/Rules/Data.hs
                  (lam "i" $ \ i -> lam "o" $ \ o -> proj $ w <@> i <@> o) -- TODO wait for phi = 1
                  (proj w0)

  reportSDoc "hcomp.rec" 60 $ text $ "filled_types sorts:" ++ show (map (getSort . fromLType . unDom) filled_types)

  bodys <- mapM mkBody (zip fns filled_types)
  return $ ((theName, gamma, rtype, map (fmap fromLType) clause_types, bodys),IdS)



            
src/full/Agda/TypeChecking/Rules/Data.hs
    bindParameters (npars - 1) ps (absBody b) $ \ tel s ->
      ret (ExtendTel a $ Abs (nameToArgName x) tel) s

-- | Check that the arguments to a constructor fits inside the sort of the datatype.
--   The third argument is the type of the constructor.
--
--   As a side effect, return the arity of the constructor.

fitsIn :: UniverseCheck -> [IsForced] -> Type -> Sort -> TCM Int

            
src/full/Agda/TypeChecking/Rules/Data.hs
fitsIn uc forceds t s = do
  reportSDoc "tc.data.fits" 10 $
    sep [ "does" <+> prettyTCM t
        , "of sort" <+> prettyTCM (getSort t)
        , "fit in" <+> prettyTCM s <+> "?"
        ]
  -- The code below would be simpler, but doesn't allow datatypes
  -- to be indexed by the universe level.
  -- s' <- instantiateFull (getSort t)

            
src/full/Agda/TypeChecking/Rules/Data.hs
      getSort t `leqSort` s
      return 0

-- | When --without-K is enabled, we should check that the sorts of
--   the index types fit into the sort of the datatype.
checkIndexSorts :: Sort -> Telescope -> TCM ()
checkIndexSorts s = \case
  EmptyTel -> return ()
  ExtendTel a tel' -> do
    getSort a `leqSort` s

            
src/full/Agda/TypeChecking/Rules/Decl.hs
  reportSDoc "tc.decl.ax" 10 $ sep
    [ text $ "checked type signature"
    , nest 2 $ prettyTCM rel <> prettyTCM x <+> ":" <+> prettyTCM t
    , nest 2 $ "of sort " <+> prettyTCM (getSort t)
    ]

  when (not $ null genParams) $
    reportSLn "tc.decl.ax" 40 $ "  generalized params: " ++ show genParams


            
src/full/Agda/TypeChecking/Rules/Decl.hs

  -- Jesper, 2018-06-05: should be done AFTER generalizing
  --whenM (optDoubleCheck <$> pragmaOptions) $ workOnTypes $ do
  --  checkInternal (unEl t) (sort $ getSort t)

  -- Andreas, 2015-03-17 Issue 1428: Do not postulate sizes in parametrized
  -- modules!
  when (funSig == A.NoFunSig) $ do
    whenM ((== SizeUniv) <$> do reduce $ getSort t) $ do

            
src/full/Agda/TypeChecking/Rules/Def.hs
  solveSizeConstraints DontDefaultToInfty

  v <- instantiateFull v  -- if we omit this, we loop (stdlib: Relation.Binary.Sum)
    -- or the termination checker might stumble over levels in sorts
    -- that cannot be converted to expressions without the level built-ins
    -- (test/succeed/Issue655.agda)

  -- compute body modification for irrelevant definitions, see issue 610
  let bodyMod = case getRelevance ai of

            
src/full/Agda/TypeChecking/Rules/Def.hs
                weak [] = idS
                weak (i:is) = weak is `composeS` liftS i (raiseS 1)
                tel = telFromList (takeLast extra (telToList delta))
                u = abstract tel (liftS extra (weak $ List.sort $ map fst alpha) `applySubst` b)
            return (map (first var) alpha,u)

      reportSDoc "tc.sys.cover.sys" 20 $ fsep $ prettyTCM gamma : map prettyTCM sys
      reportSDoc "tc.sys.cover.sys" 40 $ fsep $ (text . show) gamma : map (text . show) sys
      return (System gamma sys) -- gamma uses names from the type, not the patterns, could we do better?

            
src/full/Agda/TypeChecking/Rules/Def.hs
          eqt@(EqualityType _s _eq _params (Arg _ dom) a b) -> do
            s <- inferSort dom
            return (eqt, El s dom, unArg a, unArg b)
            -- Note: the sort _s of the equality need not be the sort of the type @dom@!
          OtherType{} -> typeError . GenericDocError =<< do
            "Cannot rewrite by equation of type" <+> prettyTCM t'

        -- Get the name of builtin REFL.


            
src/full/Agda/TypeChecking/Rules/LHS.hs
import Data.Either (partitionEithers)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.List (delete, sortBy, stripPrefix, (\\), findIndex)
import qualified Data.List as List
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Semigroup ( Semigroup )
import qualified Data.Semigroup as Semigroup
import Data.Map (Map)

            
src/full/Agda/TypeChecking/Rules/LHS.hs
    Var{}      -> softTypeError =<< notData
    MetaV{}    -> softTypeError =<< notData

    -- pi or sort: fail hard
    Pi{}       -> hardTypeError =<< notData
    Sort{}     -> hardTypeError =<< notData

    Lam{}      -> __IMPOSSIBLE__
    Lit{}      -> __IMPOSSIBLE__

            
src/full/Agda/TypeChecking/Rules/LHS.hs
    Inf{} | infOk -> return ()
    _      -> softTypeError =<< do
      liftTCM $ GenericDocError <$> sep
        [ "Cannot split on datatype in sort" , prettyTCM (getSort a) ]

  where
    splitOnPropError = softTypeError $ GenericError
      "Cannot split on datatype in Prop unless target is in Prop"

            
src/full/Agda/TypeChecking/Rules/Term.hs
isType :: A.Expr -> Sort -> TCM Type
isType e s =
    traceCall (IsTypeCall e s) $ do
    v <- checkExpr e (sort s)
    return $ El s v

-- | Check that an expression is a type without knowing the sort.
isType_ :: A.Expr -> TCM Type
isType_ e = traceCall (IsType_ e) $ do
  let fallback = isType e =<< do workOnTypes $ newSortMeta
  case unScope e of
    A.Fun i (Arg info t) b -> do

            
src/full/Agda/TypeChecking/Rules/Term.hs

    -- Setᵢ
    A.Set _ n -> do
      return $ sort (mkType n)

    -- Propᵢ
    A.Prop _ n -> do
      unlessM isPropEnabled $ typeError NeedOptionProp
      return $ sort (mkProp n)