Aelve Codesearch

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

total matches: more than 1000

Agda-2.6.0.1
30 matches
src/full/Agda/TypeChecking/Coverage.hs
          s      -> do
            reportSDoc "tc.cover.hcomp" 20 $ text "getLevel, s = " <+> prettyTCM s
            typeError . GenericDocError =<<
                    (text "The sort of" <+> prettyTCM t <+> text "should be of the form \"Set l\"")

      -- Γ ⊢ hdelta = (x : H)(δ : Δ)
      (gamma,hdelta@(ExtendTel hdom delta)) = splitTelescopeAt (size old_tel - (blockingVarNo x + 1)) old_tel

      -- Γ,φ,u,u0,Δ(x = hcomp φ u u0) ⊢

            
src/full/Agda/TypeChecking/Coverage.hs
computeHCompSplit delta1 n delta2 d pars ixs hix tel ps cps = do
    -- Get the type of the datatype
  -- Δ1 ⊢ dtype
  dsort <- liftTCM $ (parallelS (reverse $ map unArg pars) `applySubst`) . dataSort . theDef <$> getConstInfo d
  hCompName <- fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinHComp
  theHCompT <- defType <$> getConstInfo hCompName
  let
    dlvl = Level . (\ (Type s) -> s) $ dsort
    dterm = Def d [] `apply` (pars ++ ixs)
  -- Δ1 ⊢ gamma
  TelV gamma _ <- lift $ telView (theHCompT `piApply` [setHiding Hidden $ defaultArg $ dlvl , defaultArg $ dterm])
  case (delta1 `abstract` gamma,IdS) of
    (delta1',rho0) -> do

            
src/full/Agda/TypeChecking/Coverage.hs
      (con,) . snd <$> fixTarget sc{ scTarget = target }

  -- Andreas, 2018-10-27, issue #3324; use isPropM.
  -- Need to reduce sort to decide on Prop.
  -- Cannot split if domain is a Prop but target is relevant.
  propArrowRel <- isPropM t `and2M`
    maybe (return True) (not <.> isPropM) target

  mHCompName <- getPrimitiveName' builtinHComp

            
src/full/Agda/TypeChecking/Errors.hs
import Control.Monad.State

import Data.Function
import Data.List (nub, sortBy, intersperse, isInfixOf, dropWhileEnd)
import Data.Maybe
import Data.Char (toLower)
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Text.PrettyPrint.Boxes as Boxes

            
src/full/Agda/TypeChecking/Errors.hs
               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")
        where

            
src/full/Agda/TypeChecking/Errors.hs
      ++ [prettyTCM ocs]

    CantGeneralizeOverSorts ms -> vcat
            [ text "Cannot generalize over unsolved sort metas:"
            , nest 2 $ vcat [ prettyTCM x <+> text "at" <+> (pretty =<< getMetaRange x) | x <- ms ]
            , fsep $ pwords "Suggestion: add a `variable Any : Set _` and replace unsolved metas by Any"
            ]

    AbsurdPatternRequiresNoRHS ps -> fwords $

            
src/full/Agda/TypeChecking/Errors.hs
      "Datatypes in Prop must have at most one constructor when proof irrelevance is enabled"

    DataMustEndInSort t -> fsep $
      pwords "The type of a datatype must end in a sort."
      ++ [prettyTCM t] ++ pwords "isn't a sort."

{- UNUSED:
    DataTooManyParameters -> fsep $ pwords "Too many parameters given to data type."
-}


            
src/full/Agda/TypeChecking/Errors.hs
      ) $$ nest 2 (vcat $ map (prettyPat 0) ps)

    ShouldBeASort t -> fsep $
      [prettyTCM t] ++ pwords "should be a sort, but it isn't"

    ShouldBePi t -> fsep $
      [prettyTCM t] ++ pwords "should be a function type, but it isn't"

    ShouldBePath t -> fsep $

            
src/full/Agda/TypeChecking/Errors.hs
                   map (Boxes.vcat Boxes.left) [col1, col2, col3]) $
               unzip3 $
               map prettySect $
               sortBy (compare `on` show . notaName . sectNotation) $
               filter (not . closedWithoutHoles) sects))
      where
      trimLeft  = dropWhile isNormalHole
      trimRight = dropWhileEnd isNormalHole


            
src/full/Agda/TypeChecking/Errors.hs

    IsTypeCall e s -> fsep $
      pwords "when checking that the expression"
      ++ [prettyA e] ++ pwords "is a type of sort" ++ [prettyTCM s]

    IsType_ e -> fsep $
      pwords "when checking that the expression"
      ++ [prettyA e] ++ pwords "is a type"


            
src/full/Agda/TypeChecking/Errors.hs
    CheckConstructorFitsIn c t s -> fsep $
      pwords "when checking that the type" ++ [prettyTCM t] ++
      pwords "of the constructor" ++ [prettyTCM c] ++
      pwords "fits in the sort" ++ [prettyTCM s] ++
      pwords "of the datatype."

    CheckFunDefCall _ f _ ->
      fsep $ pwords "when checking the definition of" ++ [prettyTCM f]


            
src/full/Agda/TypeChecking/Generalize.hs
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.List (nub, partition, init, sortBy)
import Data.Monoid
import Data.Function (on)
import Data.Traversable

import Agda.Syntax.Common

            
src/full/Agda/TypeChecking/Generalize.hs
withGenRecVar :: (Type -> TCM a) -> TCM a
withGenRecVar ret = do
  -- Create a meta type (in Set₀) for the telescope record. It won't
  -- necessarily fit in Set₀, but since it's only used locally the sort
  -- shouldn't matter. Another option would be to put it in Setω, which is a
  -- bit more honest, but this leads to performance problems (see #3306).
  genRecMeta <- newTypeMeta (mkType 0)
  addContext (defaultDom ("genTel" :: String, genRecMeta)) $ ret genRecMeta


            
src/full/Agda/TypeChecking/Generalize.hs
      (openSortMetas, generalizableOpen)        = partition isSort generalizableOpen'
      nongeneralizableOpen                      = filter isOpen nongeneralizable

  -- Issue 3301: We can't generalize over sorts
  case openSortMetas of
    [] -> return ()
    ms -> warning $ CantGeneralizeOverSorts (map fst ms)

  -- Any meta in the solution of a generalizable meta should be generalized over (if possible).

            
src/full/Agda/TypeChecking/Generalize.hs
  -- Sort metas in dependency order. Include open metas that we are not
  -- generalizing over, since they will need to be pruned appropriately (see
  -- Issue 3672).
  allSortedMetas <- sortMetas (generalizeOver ++ reallyDontGeneralize)
  let sortedMetas = filter shouldGeneralize allSortedMetas

  let dropCxt err = updateContext (strengthenS err 1) (drop 1)

  -- Create the pre-record type (we don't yet know the types of the fields)
  (genRecName, genRecCon, genRecFields) <- dropCxt __IMPOSSIBLE__ $

            
src/full/Agda/TypeChecking/Generalize.hs

  -- Create the pre-record type (we don't yet know the types of the fields)
  (genRecName, genRecCon, genRecFields) <- dropCxt __IMPOSSIBLE__ $
      createGenRecordType genRecMeta sortedMetas

  -- Solve the generalizable metas. Each generalizable meta is solved by projecting the
  -- corresponding field from the genTel record.
  cxtTel <- getContextTelescope
  let solve m field = do

            
src/full/Agda/TypeChecking/Generalize.hs
        -- generating bogus types.
        whenM (isInstantiatedMeta m) __IMPOSSIBLE__
        assignTerm' m (telToArgs cxtTel) $ Var 0 [Proj ProjSystem field]
  zipWithM_ solve sortedMetas genRecFields

  -- Record the named variables in the telescope
  let telNames = map (`Map.lookup` nameMap) sortedMetas

  -- Build the telescope of generalized metas
  teleTypes <- do
    args <- getContextArgs
    fmap concat $ forM sortedMetas $ \ m -> do

            
src/full/Agda/TypeChecking/Generalize.hs
  -- Build the telescope of generalized metas
  teleTypes <- do
    args <- getContextArgs
    fmap concat $ forM sortedMetas $ \ m -> do
      mv   <- lookupMeta m
      let info = getArgInfo $ miGeneralizable $ mvInfo mv
          HasType{ jMetaType = t } = mvJudgement mv
      return [(Arg info $ miNameSuggestion $ mvInfo mv, piApply t args)]
  let genTel = buildGeneralizeTel genRecCon teleTypes

            
src/full/Agda/TypeChecking/Generalize.hs

  return (genTel, telNames, sub)

-- | Prune unsolved metas (#3672). The input includes also the generalized metas and is sorted in
-- dependency order. The telescope is the generalized telescope.
pruneUnsolvedMetas :: QName -> ConHead -> Telescope -> [QName] -> Map MetaId InteractionId -> (MetaId -> Bool) -> [MetaId] -> TCM ()
pruneUnsolvedMetas genRecName genRecCon genTel genRecFields interactionPoints isGeneralized metas
  | all isGeneralized metas = return ()
  | otherwise               = prune [] genTel metas

            
src/full/Agda/TypeChecking/Generalize.hs
        let (_Γ, _Δ) = (telFromList gs, telFromList ds)
              where (gs, _ : ds) = splitAt (size _ΓrΔ - i - 1) (telToList _ΓrΔ)

        -- Get the type of x. By doing this here we let the checkpoint machinery sort out the
        _A <- case mvJudgement mv of
                IsSort{}  -> return Nothing
                HasType{} -> Just <$> getMetaTypeInContext x

        -- We have

            
src/full/Agda/TypeChecking/Generalize.hs
        -- generalization, use equalTerm instead of assigning to x. If this fails (see
        -- test/Fail/Issue3655b.agda for a test case), we need to give an error. This can happen if
        -- there are dependencies between generalized variables that are hidden by constraints and
        -- the dependency sorting happens to pick the wrong order. For instance, if we have
        --    α : Nat   (unsolved meta)
        --    t : F α   (named variable)
        --    n : Nat   (named variable)
        -- and a constraint F α == F n, where F does some pattern matching preventing the constraint
        -- to be solved when n is still a meta. If t appears before n in the type these will be sorted

            
src/full/Agda/TypeChecking/Generalize.hs
        --    t : F α   (named variable)
        --    n : Nat   (named variable)
        -- and a constraint F α == F n, where F does some pattern matching preventing the constraint
        -- to be solved when n is still a meta. If t appears before n in the type these will be sorted
        -- as α, t, n, but we will solve α := n before we get to the pruning here. It's good that we
        -- solve first though, because that means we can give a more informative error message than
        -- the "Cannot instantiate..." we would otherwise get.
        let uρ' = applySubst ρ' u
        reportSDoc "tc.generalize.prune" 80 $ vcat

            
src/full/Agda/TypeChecking/Generalize.hs
        []    -> return Nothing
        _:_:_ -> __IMPOSSIBLE__
        [i]   -> return (Just i)
                                                    -- Nothing if sort meta
    newMetaFromOld :: MetaVariable -> Substitution -> Maybe Type -> TCM (MetaId, Term)
    newMetaFromOld mv ρ mA = setCurrentRange mv $
      case mA of
        Nothing -> do
          s @ (MetaS y _) <- newSortMeta

            
src/full/Agda/TypeChecking/Generalize.hs
createGenValues :: Set QName -> TCM (Map MetaId QName, Map QName GeneralizedValue)
createGenValues s = do
  genvals <- locallyTC eGeneralizeMetas (const YesGeneralize) $
               forM (sortBy (compare `on` getRange) $ Set.toList s) createGenValue
  let metaMap = Map.fromList [ (m, x) | (x, m, _) <- genvals ]
      nameMap = Map.fromList [ (x, v) | (x, _, v) <- genvals ]
  return (metaMap, nameMap)

-- | Create a generalisable meta for a generalisable variable.

            
src/full/Agda/TypeChecking/Generalize.hs
                                , genvalType       = metaType })

-- | Sort metas in dependency order.
sortMetas :: [MetaId] -> TCM [MetaId]
sortMetas metas = do
  metaGraph <- concat <$> do
    forM metas $ \ m -> do
      deps <- allMetas (\ m' -> if m' `elem` metas then singleton m' else mempty) <$> getType m
      return [ (m, m') | m' <- Set.toList deps ]


            
src/full/Agda/TypeChecking/Generalize.hs
            return

  where
    -- Sort metas don't have types, but we still want to sort them.
    getType m = do
      mv <- lookupMeta m
      case mvJudgement mv of
        IsSort{}                 -> return Nothing
        HasType{ jMetaType = t } -> Just <$> instantiateFull t

            
src/full/Agda/TypeChecking/Generalize.hs
-- | Create a not-yet correct record type for the generalized telescope. It's not yet correct since
--   we haven't computed the telescope yet, and we need the record type to do it.
createGenRecordType :: Type -> [MetaId] -> TCM (QName, ConHead, [QName])
createGenRecordType genRecMeta@(El genRecSort _) sortedMetas = do
  current <- currentModule
  let freshQName s = qualify current <$> freshName_ (s :: String)
      mkFieldName  = freshQName . (generalizedFieldName ++) <=< getMetaNameSuggestion
  genRecFields <- mapM (defaultArg <.> mkFieldName) sortedMetas
  genRecName   <- freshQName "GeneralizeTel"
  genRecCon    <- freshQName "mkGeneralizeTel" <&> \ con -> ConHead
                  { conName      = con
                  , conInductive = Inductive
                  , conFields    = genRecFields }

            
src/full/Agda/TypeChecking/Generalize.hs
                  { conName      = con
                  , conInductive = Inductive
                  , conFields    = genRecFields }
  forM_ (zip sortedMetas genRecFields) $ \ (meta, fld) -> do
    fieldTy <- getMetaType meta
    let field = unArg fld
    addConstant field $ defaultDefn (argInfo fld) field fieldTy $
      let proj = Projection { projProper   = Just genRecName
                            , projOrig     = field

            
src/full/Agda/TypeChecking/Generalize.hs
                }
  let dummyTel 0 = EmptyTel
      dummyTel n = ExtendTel (defaultDom __DUMMY_TYPE__) $ Abs "_" $ dummyTel (n - 1)
  addConstant genRecName $ defaultDefn defaultArgInfo genRecName (sort genRecSort) $
    Record { recPars         = 0
           , recClause       = Nothing
           , recConHead      = genRecCon
           , recNamedCon     = False
           , recFields       = genRecFields

            
src/full/Agda/TypeChecking/InstanceArguments.hs
          -- #3676: Sort the candidates based on the size of the range for the errors and
          --        set the range of the full error to the range of the most precise candidate
          --        error.
          let sortedErrs = List.sortBy (compare `on` precision) errs
                where precision (_, err) = maybe infinity iLength $ rangeToInterval $ getRange err
                      infinity = 1000000000
          setCurrentRange (take 1 $ map snd sortedErrs) $
            typeError $ InstanceNoCandidate t [ (candidateTerm c, err) | (c, err) <- sortedErrs ]

        Just (_, [Candidate term t' _]) -> do
          reportSDoc "tc.instance" 15 $ vcat
            [ "findInstance 5: solved by instance search using the only candidate"
            , nest 2 $ prettyTCM term