module Agda.TypeChecking.Pretty.Call where import Prelude hiding ( null ) import Agda.Syntax.Abstract as A import Agda.Syntax.Abstract.Views import Agda.Syntax.Common import Agda.Syntax.Fixity import qualified Agda.Syntax.Concrete.Definitions as D import qualified Agda.Syntax.Info as A import Agda.Syntax.Position import Agda.Syntax.Scope.Monad import Agda.Syntax.Translation.AbstractToConcrete import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Monad.Context import Agda.TypeChecking.Monad.Debug import Agda.TypeChecking.Pretty import Agda.Utils.Function import Agda.Utils.Null import qualified Agda.Utils.Pretty as P import Agda.Utils.Impossible sayWhere :: MonadPretty m => HasRange a => a -> m Doc -> m Doc sayWhere :: a -> m Doc -> m Doc sayWhere x :: a x d :: m Doc d = Bool -> (m Doc -> m Doc) -> m Doc -> m Doc forall a. Bool -> (a -> a) -> a -> a applyUnless (Range -> Bool forall a. Null a => a -> Bool null Range r) (Range -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Range r m Doc -> m Doc -> m Doc forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc $$) m Doc d where r :: Range r = a -> Range forall t. HasRange t => t -> Range getRange a x sayWhen :: MonadPretty m => Range -> Maybe (Closure Call) -> m Doc -> m Doc sayWhen :: Range -> Maybe (Closure Call) -> m Doc -> m Doc sayWhen r :: Range r Nothing m :: m Doc m = Range -> m Doc -> m Doc forall (m :: * -> *) a. (MonadPretty m, HasRange a) => a -> m Doc -> m Doc sayWhere Range r m Doc m sayWhen r :: Range r (Just cl :: Closure Call cl) m :: m Doc m = Range -> m Doc -> m Doc forall (m :: * -> *) a. (MonadPretty m, HasRange a) => a -> m Doc -> m Doc sayWhere Range r (m Doc m m Doc -> m Doc -> m Doc forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc $$ Closure Call -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Closure Call cl) instance PrettyTCM CallInfo where prettyTCM :: CallInfo -> m Doc prettyTCM c :: CallInfo c = do let call :: m Doc call = Closure Term -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM (Closure Term -> m Doc) -> Closure Term -> m Doc forall a b. (a -> b) -> a -> b $ CallInfo -> Closure Term callInfoCall CallInfo c r :: Range r = CallInfo -> Range callInfoRange CallInfo c if Doc -> Bool forall a. Null a => a -> Bool null (Doc -> Bool) -> Doc -> Bool forall a b. (a -> b) -> a -> b $ Range -> Doc forall a. Pretty a => a -> Doc P.pretty Range r then m Doc call else m Doc call m Doc -> m Doc -> m Doc forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc $$ Int -> m Doc -> m Doc forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc nest 2 ("(at" m Doc -> m Doc -> m Doc forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc <+> Range -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Range r) m Doc -> m Doc -> m Doc forall a. Semigroup a => a -> a -> a <> ")" instance PrettyTCM Call where prettyTCM :: Call -> m Doc prettyTCM = Precedence -> m Doc -> m Doc forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a withContextPrecedence Precedence TopCtx (m Doc -> m Doc) -> (Call -> m Doc) -> Call -> m Doc forall b c a. (b -> c) -> (a -> b) -> a -> c . \case CheckClause t :: Type t cl :: SpineClause cl -> do VerboseKey -> Int -> m () -> m () forall (m :: * -> *). MonadDebug m => VerboseKey -> Int -> m () -> m () verboseS "error.checkclause" 40 (m () -> m ()) -> m () -> m () forall a b. (a -> b) -> a -> b $ do VerboseKey -> Int -> VerboseKey -> m () forall (m :: * -> *). MonadDebug m => VerboseKey -> Int -> VerboseKey -> m () reportSLn "error.checkclause" 60 (VerboseKey -> m ()) -> VerboseKey -> m () forall a b. (a -> b) -> a -> b $ "prettyTCM CheckClause: cl = " VerboseKey -> VerboseKey -> VerboseKey forall a. [a] -> [a] -> [a] ++ SpineClause -> VerboseKey forall a. Show a => a -> VerboseKey show (SpineClause -> SpineClause forall a. ExprLike a => a -> a deepUnscope SpineClause cl) [Declaration] clc <- SpineClause -> m [Declaration] forall a c (m :: * -> *). (ToConcrete a c, MonadAbsToCon m) => a -> m c abstractToConcrete_ SpineClause cl VerboseKey -> Int -> VerboseKey -> m () forall (m :: * -> *). MonadDebug m => VerboseKey -> Int -> VerboseKey -> m () reportSLn "error.checkclause" 40 (VerboseKey -> m ()) -> VerboseKey -> m () forall a b. (a -> b) -> a -> b $ "cl (Concrete) = " VerboseKey -> VerboseKey -> VerboseKey forall a. [a] -> [a] -> [a] ++ [Declaration] -> VerboseKey forall a. Show a => a -> VerboseKey show [Declaration] clc [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the clause" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [SpineClause -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA SpineClause cl] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "has type" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type t] CheckLHS lhs :: SpineLHS lhs -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ [ [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the clause left hand side" , SpineLHS -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA (SpineLHS -> m Doc) -> SpineLHS -> m Doc forall a b. (a -> b) -> a -> b $ SpineLHS lhs { spLhsInfo :: LHSInfo A.spLhsInfo = (SpineLHS -> LHSInfo A.spLhsInfo SpineLHS lhs) { lhsEllipsis :: ExpandedEllipsis A.lhsEllipsis = ExpandedEllipsis NoEllipsis } } ] CheckPattern p :: Pattern p tel :: Telescope tel t :: Type t -> Telescope -> m Doc -> m Doc forall b (m :: * -> *) a. (AddContext b, MonadAddContext m) => b -> m a -> m a addContext Telescope tel (m Doc -> m Doc) -> m Doc -> m Doc forall a b. (a -> b) -> a -> b $ [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the pattern" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Pattern -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA Pattern p] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "has type" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type t] CheckLetBinding b :: LetBinding b -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the let binding" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [LetBinding -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA LetBinding b] InferExpr e :: Expr e -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when inferring the type of" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Expr -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA Expr e] CheckExprCall cmp :: Comparison cmp e :: Expr e t :: Type t -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the expression" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Expr -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA Expr e] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "has type" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type t] IsTypeCall cmp :: Comparison cmp e :: Expr e s :: Sort s -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the expression" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Expr -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA Expr e] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "is a type of sort" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Sort -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Sort s] IsType_ e :: Expr e -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the expression" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Expr -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA Expr e] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "is a type" CheckProjection _ x :: QName x t :: Type t -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the projection" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [ [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc sep [ QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName x m Doc -> m Doc -> m Doc forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc <+> ":" , Int -> m Doc -> m Doc forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc nest 2 (m Doc -> m Doc) -> m Doc -> m Doc forall a b. (a -> b) -> a -> b $ Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type t ] ] CheckArguments r :: Range r es :: [NamedArg Expr] es t0 :: Type t0 t1 :: Maybe Type t1 -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ (NamedArg Expr -> m Doc) -> [NamedArg Expr] -> [m Doc] forall a b. (a -> b) -> [a] -> [b] map NamedArg Expr -> m Doc forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc hPretty [NamedArg Expr] es [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords ([NamedArg Expr] -> VerboseKey -> VerboseKey -> VerboseKey forall a c. Sized a => a -> c -> c -> c P.singPlural [NamedArg Expr] es "is a valid argument" "are valid arguments") [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "to a function of type" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type t0] CheckMetaSolution r :: Range r m :: MetaId m a :: Type a v :: Term v -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the solution" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Term -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Term v] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "of metavariable" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [MetaId -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM MetaId m] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "has the expected type" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type a] CheckTargetType r :: Range r infTy :: Type infTy expTy :: Type expTy -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc sep [ "when checking that the inferred type of an application" , Int -> m Doc -> m Doc forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc nest 2 (m Doc -> m Doc) -> m Doc -> m Doc forall a b. (a -> b) -> a -> b $ Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type infTy , "matches the expected type" , Int -> m Doc -> m Doc forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc nest 2 (m Doc -> m Doc) -> m Doc -> m Doc forall a b. (a -> b) -> a -> b $ Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type expTy ] CheckRecDef _ x :: QName x ps :: [LamBinding] ps cs :: [Constructor] cs -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the definition of" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName x] CheckDataDef _ x :: QName x ps :: [LamBinding] ps cs :: [Constructor] cs -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the definition of" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName x] CheckConstructor d :: QName d _ _ (A.Axiom _ _ _ _ c :: QName c _) -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the constructor" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName c] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "in the declaration of" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName d] CheckConstructor{} -> m Doc forall a. HasCallStack => a __IMPOSSIBLE__ CheckConstructorFitsIn c :: QName c t :: Type t s :: Sort s -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the type" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type t] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "of the constructor" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName c] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "fits in the sort" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Sort -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Sort s] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "of the datatype." CheckFunDefCall _ f :: QName f _ -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the definition of" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName f] CheckPragma _ p :: Pragma p -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the pragma" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [RangeAndPragma -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA (RangeAndPragma -> m Doc) -> RangeAndPragma -> m Doc forall a b. (a -> b) -> a -> b $ Range -> Pragma -> RangeAndPragma RangeAndPragma Range forall a. Range' a noRange Pragma p] CheckPrimitive _ x :: QName x e :: Expr e -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the type of the primitive function" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName x] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "is" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Expr -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA Expr e] CheckWithFunctionType a :: Type a -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the type" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type a] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "of the generated with function is well-formed" CheckDotPattern e :: Expr e v :: Term v -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that the given dot pattern" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Expr -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA Expr e] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "matches the inferred value" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Term -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Term v] CheckNamedWhere m :: ModuleName m -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the named where block" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [ModuleName -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA ModuleName m] InferVar x :: Name x -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when inferring the type of" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Name -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Name x] InferDef x :: QName x -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when inferring the type of" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName x] CheckIsEmpty r :: Range r t :: Type t -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking that" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Type -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Type t] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "has no constructors" CheckConfluence r1 :: QName r1 r2 :: QName r2 -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking confluence of the rewrite rule" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName r1] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "with" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ if QName r1 QName -> QName -> Bool forall a. Eq a => a -> a -> Bool == QName r2 then VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "itself" else [QName -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM QName r2] ScopeCheckExpr e :: Expr e -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when scope checking" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Expr -> m Doc forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc pretty Expr e] ScopeCheckDeclaration d :: NiceDeclaration d -> VerboseKey -> m Doc forall (m :: * -> *). Monad m => VerboseKey -> m Doc fwords ("when scope checking the declaration" VerboseKey -> VerboseKey -> VerboseKey forall a. [a] -> [a] -> [a] ++ VerboseKey suffix) m Doc -> m Doc -> m Doc forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc $$ Int -> m Doc -> m Doc forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc nest 2 ([m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ (Declaration -> m Doc) -> [Declaration] -> [m Doc] forall a b. (a -> b) -> [a] -> [b] map Declaration -> m Doc forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc pretty [Declaration] ds) where ds :: [Declaration] ds = NiceDeclaration -> [Declaration] D.notSoNiceDeclarations NiceDeclaration d suffix :: VerboseKey suffix = case [Declaration] ds of [_] -> "" _ -> "s" ScopeCheckLHS x :: QName x p :: Pattern p -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when scope checking the left-hand side" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Pattern -> m Doc forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc pretty Pattern p] [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "in the definition of" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [QName -> m Doc forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc pretty QName x] NoHighlighting -> m Doc forall a. Null a => a empty SetRange r :: Range r -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep (VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when doing something at") m Doc -> m Doc -> m Doc forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc <+> Range -> m Doc forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc prettyTCM Range r CheckSectionApplication _ m1 :: ModuleName m1 modapp :: ModuleApplication modapp -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when checking the module application" [m Doc] -> [m Doc] -> [m Doc] forall a. [a] -> [a] -> [a] ++ [Constructor -> m Doc forall c a (m :: * -> *). (Pretty c, ToConcrete a c, MonadAbsToCon m) => a -> m Doc prettyA (Constructor -> m Doc) -> Constructor -> m Doc forall a b. (a -> b) -> a -> b $ ModuleInfo -> ModuleName -> ModuleApplication -> ScopeCopyInfo -> ImportDirective -> Constructor A.Apply ModuleInfo info ModuleName m1 ModuleApplication modapp ScopeCopyInfo initCopyInfo ImportDirective forall n m. ImportDirective' n m defaultImportDir] where info :: ModuleInfo info = Range -> Range -> Maybe Name -> Maybe OpenShortHand -> Maybe ImportDirective -> ModuleInfo A.ModuleInfo Range forall a. Range' a noRange Range forall a. Range' a noRange Maybe Name forall a. Maybe a Nothing Maybe OpenShortHand forall a. Maybe a Nothing Maybe ImportDirective forall a. Maybe a Nothing ModuleContents -> [m Doc] -> m Doc forall (m :: * -> *). Monad m => [m Doc] -> m Doc fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc forall a b. (a -> b) -> a -> b $ VerboseKey -> [m Doc] forall (m :: * -> *). Monad m => VerboseKey -> [m Doc] pwords "when retrieving the contents of a module" where hPretty :: MonadPretty m => Arg (Named_ Expr) -> m Doc hPretty :: NamedArg Expr -> m Doc hPretty a :: NamedArg Expr a = do Precedence -> m Doc -> m Doc forall (m :: * -> *) a. ReadTCState m => Precedence -> m a -> m a withContextPrecedence (ParenPreference -> Precedence ArgumentCtx ParenPreference PreferParen) (m Doc -> m Doc) -> m Doc -> m Doc forall a b. (a -> b) -> a -> b $ Arg (Named (WithOrigin (Ranged VerboseKey)) Expr) -> m Doc forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc pretty (Arg (Named (WithOrigin (Ranged VerboseKey)) Expr) -> m Doc) -> m (Arg (Named (WithOrigin (Ranged VerboseKey)) Expr)) -> m Doc forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b =<< NamedArg Expr -> NamedArg Expr -> m (Arg (Named (WithOrigin (Ranged VerboseKey)) Expr)) forall i a c (m :: * -> *). (LensHiding i, ToConcrete a c, MonadAbsToCon m) => i -> a -> m c abstractToConcreteHiding NamedArg Expr a NamedArg Expr a