{-# LANGUAGE NondecreasingIndentation #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Errors
( prettyError
, tcErrString
, prettyTCWarnings'
, prettyTCWarnings
, tcWarningsToError
, applyFlagsToTCWarningsPreserving
, applyFlagsToTCWarnings
, getAllUnsolvedWarnings
, getAllWarningsPreserving
, getAllWarnings
, getAllWarningsOfTCErr
, dropTopLevelModule
, topLevelModuleDropper
, stringTCErr
, explainWhyInScope
, Verbalize(verbalize)
) where
import Prelude hiding ( null, foldl )
import qualified Control.Exception as E
import Control.Monad.Except
import qualified Data.CaseInsensitive as CaseInsens
import Data.Foldable (foldl)
import Data.Function
import Data.List (sortBy, dropWhileEnd, intercalate)
import Data.Maybe
import qualified Data.Set as Set
import qualified Text.PrettyPrint.Boxes as Boxes
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Definitions (notSoNiceDeclarations)
import Agda.Syntax.Concrete.Pretty (prettyHiding, prettyRelevance)
import Agda.Syntax.Notation
import Agda.Syntax.Position
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Scope.Monad (isDatatypeModule)
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Closure
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.SizedTypes ( sizeType )
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Pretty.Call
import Agda.TypeChecking.Pretty.Warning
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope ( ifPiType )
import Agda.TypeChecking.Reduce (instantiate)
import Agda.Utils.FileName
import Agda.Utils.Float ( toStringWithoutDotZero )
import Agda.Utils.Function
import Agda.Utils.List ( initLast )
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Null
import Agda.Utils.Pretty ( prettyShow, render )
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Size
import Agda.Utils.Impossible
{-# SPECIALIZE prettyError :: TCErr -> TCM String #-}
prettyError :: MonadTCM tcm => TCErr -> tcm String
prettyError :: forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
prettyError TCErr
err = TCM [Char] -> tcm [Char]
forall a. TCM a -> tcm a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [Char] -> tcm [Char]) -> TCM [Char] -> tcm [Char]
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. Show a => a -> [Char]
show (Doc -> [Char]) -> TCMT IO Doc -> TCM [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCErr -> [TCErr] -> TCMT IO Doc
prettyError' TCErr
err []
where
prettyError' :: TCErr -> [TCErr] -> TCM Doc
prettyError' :: TCErr -> [TCErr] -> TCMT IO Doc
prettyError' TCErr
err [TCErr]
errs
| [TCErr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TCErr]
errs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3 = [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
[Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"total panic: error when printing error from printing error from printing error." [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [TCMT IO Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"I give up! Approximations of errors (original error last):" )
TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ((TCErr -> TCMT IO Doc) -> [TCErr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (TCErr -> [Char]) -> TCErr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> [Char]
tcErrString) [TCErr]
errs)
| Bool
otherwise = Bool -> (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a. Bool -> (a -> a) -> a -> a
applyUnless ([TCErr] -> Bool
forall a. Null a => a -> Bool
null [TCErr]
errs) (TCMT IO Doc
"panic: error when printing error!" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$) (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
(TCErr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ((TCErr -> TCMT IO Doc) -> [TCErr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> TCMT IO Doc)
-> (TCErr -> [Char]) -> TCErr -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"when printing error " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> (TCErr -> [Char]) -> TCErr -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCErr -> [Char]
tcErrString) [TCErr]
errs))
TCMT IO Doc -> (TCErr -> TCMT IO Doc) -> TCMT IO Doc
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
err' -> TCErr -> [TCErr] -> TCMT IO Doc
prettyError' TCErr
err' (TCErr
errTCErr -> [TCErr] -> [TCErr]
forall a. a -> [a] -> [a]
:[TCErr]
errs)
panic :: Monad m => String -> m Doc
panic :: forall (m :: * -> *). Monad m => [Char] -> m Doc
panic [Char]
s = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Panic: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
nameWithBinding :: MonadPretty m => QName -> m Doc
nameWithBinding :: forall (m :: * -> *). MonadPretty m => QName -> m Doc
nameWithBinding QName
q =
(QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"bound 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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r
where
r :: Range
r = Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q
tcErrString :: TCErr -> String
tcErrString :: TCErr -> [Char]
tcErrString TCErr
err = Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (TCErr -> Range
forall a. HasRange a => a -> Range
getRange TCErr
err) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ case TCErr
err of
TypeError CallStack
_ TCState
_ Closure TypeError
cl -> TypeError -> [Char]
errorString (TypeError -> [Char]) -> TypeError -> [Char]
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> TypeError
forall a. Closure a -> a
clValue Closure TypeError
cl
Exception Range
r Doc
s -> Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Range
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
s
IOException TCState
_ Range
r IOException
e -> Range -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Range
r [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ IOException -> [Char]
forall e. Exception e => e -> [Char]
E.displayException IOException
e
PatternErr{} -> [Char]
"PatternErr"
stringTCErr :: String -> TCErr
stringTCErr :: [Char] -> TCErr
stringTCErr = Range -> Doc -> TCErr
Exception Range
forall a. Range' a
noRange (Doc -> TCErr) -> ([Char] -> Doc) -> [Char] -> TCErr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc
P.text
errorString :: TypeError -> String
errorString :: TypeError -> [Char]
errorString TypeError
err = case TypeError
err of
AmbiguousModule{} -> [Char]
"AmbiguousModule"
AmbiguousName{} -> [Char]
"AmbiguousName"
AmbiguousParseForApplication{} -> [Char]
"AmbiguousParseForApplication"
AmbiguousParseForLHS{} -> [Char]
"AmbiguousParseForLHS"
AmbiguousTopLevelModuleName {} -> [Char]
"AmbiguousTopLevelModuleName"
BadArgumentsToPatternSynonym{} -> [Char]
"BadArgumentsToPatternSynonym"
TooFewArgumentsToPatternSynonym{} -> [Char]
"TooFewArgumentsToPatternSynonym"
CannotResolveAmbiguousPatternSynonym{} -> [Char]
"CannotResolveAmbiguousPatternSynonym"
TypeError
BothWithAndRHS -> [Char]
"BothWithAndRHS"
BuiltinInParameterisedModule{} -> [Char]
"BuiltinInParameterisedModule"
BuiltinMustBeConstructor{} -> [Char]
"BuiltinMustBeConstructor"
ClashingDefinition{} -> [Char]
"ClashingDefinition"
ClashingFileNamesFor{} -> [Char]
"ClashingFileNamesFor"
ClashingImport{} -> [Char]
"ClashingImport"
ClashingModule{} -> [Char]
"ClashingModule"
ClashingModuleImport{} -> [Char]
"ClashingModuleImport"
CompilationError{} -> [Char]
"CompilationError"
ConstructorPatternInWrongDatatype{} -> [Char]
"ConstructorPatternInWrongDatatype"
CyclicModuleDependency{} -> [Char]
"CyclicModuleDependency"
DataMustEndInSort{} -> [Char]
"DataMustEndInSort"
CantResolveOverloadedConstructorsTargetingSameDatatype{} -> [Char]
"CantResolveOverloadedConstructorsTargetingSameDatatype"
DoesNotConstructAnElementOf{} -> [Char]
"DoesNotConstructAnElementOf"
DuplicateBuiltinBinding{} -> [Char]
"DuplicateBuiltinBinding"
DuplicateConstructors{} -> [Char]
"DuplicateConstructors"
DuplicateFields{} -> [Char]
"DuplicateFields"
DuplicateImports{} -> [Char]
"DuplicateImports"
TypeError
FieldOutsideRecord -> [Char]
"FieldOutsideRecord"
FileNotFound{} -> [Char]
"FileNotFound"
GenericError{} -> [Char]
"GenericError"
GenericDocError{} -> [Char]
"GenericDocError"
InstanceNoCandidate{} -> [Char]
"InstanceNoCandidate"
IllformedProjectionPattern{} -> [Char]
"IllformedProjectionPattern"
CannotEliminateWithPattern{} -> [Char]
"CannotEliminateWithPattern"
IllegalLetInTelescope{} -> [Char]
"IllegalLetInTelescope"
IllegalPatternInTelescope{} -> [Char]
"IllegalPatternInTelescope"
InternalError{} -> [Char]
"InternalError"
InvalidPattern{} -> [Char]
"InvalidPattern"
LocalVsImportedModuleClash{} -> [Char]
"LocalVsImportedModuleClash"
MetaCannotDependOn{} -> [Char]
"MetaCannotDependOn"
MetaOccursInItself{} -> [Char]
"MetaOccursInItself"
MetaIrrelevantSolution{} -> [Char]
"MetaIrrelevantSolution"
MetaErasedSolution{} -> [Char]
"MetaErasedSolution"
ModuleArityMismatch{} -> [Char]
"ModuleArityMismatch"
ModuleDefinedInOtherFile {} -> [Char]
"ModuleDefinedInOtherFile"
ModuleNameUnexpected{} -> [Char]
"ModuleNameUnexpected"
ModuleNameDoesntMatchFileName {} -> [Char]
"ModuleNameDoesntMatchFileName"
NeedOptionCopatterns{} -> [Char]
"NeedOptionCopatterns"
NeedOptionRewriting{} -> [Char]
"NeedOptionRewriting"
NeedOptionProp{} -> [Char]
"NeedOptionProp"
NeedOptionTwoLevel{} -> [Char]
"NeedOptionTwoLevel"
GeneralizeNotSupportedHere{} -> [Char]
"GeneralizeNotSupportedHere"
GeneralizeCyclicDependency{} -> [Char]
"GeneralizeCyclicDependency"
GeneralizeUnsolvedMeta{} -> [Char]
"GeneralizeUnsolvedMeta"
MultipleFixityDecls{} -> [Char]
"MultipleFixityDecls"
MultiplePolarityPragmas{} -> [Char]
"MultiplePolarityPragmas"
NoBindingForBuiltin{} -> [Char]
"NoBindingForBuiltin"
NoParseForApplication{} -> [Char]
"NoParseForApplication"
NoParseForLHS{} -> [Char]
"NoParseForLHS"
NoRHSRequiresAbsurdPattern{} -> [Char]
"NoRHSRequiresAbsurdPattern"
NoSuchBuiltinName{} -> [Char]
"NoSuchBuiltinName"
NoSuchModule{} -> [Char]
"NoSuchModule"
DuplicatePrimitiveBinding{} -> [Char]
"DuplicatePrimitiveBinding"
NoSuchPrimitiveFunction{} -> [Char]
"NoSuchPrimitiveFunction"
WrongModalityForPrimitive{} -> [Char]
"WrongModalityForPrimitive"
NotAModuleExpr{} -> [Char]
"NotAModuleExpr"
TypeError
NotAProperTerm -> [Char]
"NotAProperTerm"
InvalidType{} -> [Char]
"InvalidType"
InvalidTypeSort{} -> [Char]
"InvalidTypeSort"
FunctionTypeInSizeUniv{} -> [Char]
"FunctionTypeInSizeUniv"
NotAValidLetBinding{} -> [Char]
"NotAValidLetBinding"
NotValidBeforeField{} -> [Char]
"NotValidBeforeField"
NotAnExpression{} -> [Char]
"NotAnExpression"
NotImplemented{} -> [Char]
"NotImplemented"
NotSupported{} -> [Char]
"NotSupported"
AbstractConstructorNotInScope{} -> [Char]
"AbstractConstructorNotInScope"
NotInScope{} -> [Char]
"NotInScope"
NotLeqSort{} -> [Char]
"NotLeqSort"
NothingAppliedToHiddenArg{} -> [Char]
"NothingAppliedToHiddenArg"
NothingAppliedToInstanceArg{} -> [Char]
"NothingAppliedToInstanceArg"
OverlappingProjects {} -> [Char]
"OverlappingProjects"
OperatorInformation {} -> [Char]
"OperatorInformation"
PatternShadowsConstructor {} -> [Char]
"PatternShadowsConstructor"
TypeError
PropMustBeSingleton -> [Char]
"PropMustBeSingleton"
RepeatedVariablesInPattern{} -> [Char]
"RepeatedVariablesInPattern"
ShadowedModule{} -> [Char]
"ShadowedModule"
ShouldBeASort{} -> [Char]
"ShouldBeASort"
ShouldBeApplicationOf{} -> [Char]
"ShouldBeApplicationOf"
ShouldBeAppliedToTheDatatypeParameters{} -> [Char]
"ShouldBeAppliedToTheDatatypeParameters"
ShouldBeEmpty{} -> [Char]
"ShouldBeEmpty"
ShouldBePi{} -> [Char]
"ShouldBePi"
ShouldBePath{} -> [Char]
"ShouldBePath"
ShouldBeRecordType{} -> [Char]
"ShouldBeRecordType"
ShouldBeRecordPattern{} -> [Char]
"ShouldBeRecordPattern"
NotAProjectionPattern{} -> [Char]
"NotAProjectionPattern"
ShouldEndInApplicationOfTheDatatype{} -> [Char]
"ShouldEndInApplicationOfTheDatatype"
SplitError{} -> [Char]
"SplitError"
ImpossibleConstructor{} -> [Char]
"ImpossibleConstructor"
TooManyFields{} -> [Char]
"TooManyFields"
TooManyPolarities{} -> [Char]
"TooManyPolarities"
SplitOnIrrelevant{} -> [Char]
"SplitOnIrrelevant"
SplitOnUnusableCohesion{} -> [Char]
"SplitOnUnusableCohesion"
SplitOnNonVariable{} -> [Char]
"SplitOnNonVariable"
SplitOnNonEtaRecord{} -> [Char]
"SplitOnNonEtaRecord"
DefinitionIsIrrelevant{} -> [Char]
"DefinitionIsIrrelevant"
DefinitionIsErased{} -> [Char]
"DefinitionIsErased"
VariableIsIrrelevant{} -> [Char]
"VariableIsIrrelevant"
VariableIsErased{} -> [Char]
"VariableIsErased"
VariableIsOfUnusableCohesion{} -> [Char]
"VariableIsOfUnusableCohesion"
UnequalBecauseOfUniverseConflict{} -> [Char]
"UnequalBecauseOfUniverseConflict"
UnequalRelevance{} -> [Char]
"UnequalRelevance"
UnequalQuantity{} -> [Char]
"UnequalQuantity"
UnequalCohesion{} -> [Char]
"UnequalCohesion"
UnequalFiniteness{} -> [Char]
"UnequalFiniteness"
UnequalHiding{} -> [Char]
"UnequalHiding"
UnequalLevel{} -> [Char]
"UnequalLevel"
UnequalSorts{} -> [Char]
"UnequalSorts"
UnequalTerms{} -> [Char]
"UnequalTerms"
UnequalTypes{} -> [Char]
"UnequalTypes"
WithOnFreeVariable{} -> [Char]
"WithOnFreeVariable"
UnexpectedWithPatterns{} -> [Char]
"UnexpectedWithPatterns"
UninstantiatedDotPattern{} -> [Char]
"UninstantiatedDotPattern"
ForcedConstructorNotInstantiated{} -> [Char]
"ForcedConstructorNotInstantiated"
SolvedButOpenHoles{} -> [Char]
"SolvedButOpenHoles"
TypeError
UnusedVariableInPatternSynonym -> [Char]
"UnusedVariableInPatternSynonym"
UnquoteFailed{} -> [Char]
"UnquoteFailed"
DeBruijnIndexOutOfScope{} -> [Char]
"DeBruijnIndexOutOfScope"
WithClausePatternMismatch{} -> [Char]
"WithClausePatternMismatch"
WrongHidingInApplication{} -> [Char]
"WrongHidingInApplication"
WrongHidingInLHS{} -> [Char]
"WrongHidingInLHS"
WrongHidingInLambda{} -> [Char]
"WrongHidingInLambda"
WrongIrrelevanceInLambda{} -> [Char]
"WrongIrrelevanceInLambda"
WrongQuantityInLambda{} -> [Char]
"WrongQuantityInLambda"
WrongCohesionInLambda{} -> [Char]
"WrongCohesionInLambda"
WrongNamedArgument{} -> [Char]
"WrongNamedArgument"
WrongNumberOfConstructorArguments{} -> [Char]
"WrongNumberOfConstructorArguments"
QuantityMismatch{} -> [Char]
"QuantityMismatch"
HidingMismatch{} -> [Char]
"HidingMismatch"
RelevanceMismatch{} -> [Char]
"RelevanceMismatch"
NonFatalErrors{} -> [Char]
"NonFatalErrors"
InstanceSearchDepthExhausted{} -> [Char]
"InstanceSearchDepthExhausted"
TriedToCopyConstrainedPrim{} -> [Char]
"TriedToCopyConstrainedPrim"
SortOfSplitVarError{} -> [Char]
"SortOfSplitVarError"
instance PrettyTCM TCErr where
prettyTCM :: forall (m :: * -> *). MonadPretty m => TCErr -> m Doc
prettyTCM TCErr
err = case TCErr
err of
TypeError CallStack
loc TCState
_ Closure{ clValue :: forall a. Closure a -> a
clValue = NonFatalErrors [TCWarning]
ws } -> do
[Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"error" Int
2 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Error raised at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CallStack -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow CallStack
loc
(m Doc -> m Doc -> m Doc) -> [m Doc] -> m Doc
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
($$) ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning -> m Doc) -> [TCWarning] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TCWarning -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM [TCWarning]
ws
TypeError CallStack
loc TCState
s Closure TypeError
e -> (TCState -> TCState) -> m Doc -> m Doc
forall a. (TCState -> TCState) -> m a -> m a
forall (m :: * -> *) a.
ReadTCState m =>
(TCState -> TCState) -> m a -> m a
withTCState (TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
s) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ do
[Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"error" Int
2 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Error raised at " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CallStack -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow CallStack
loc
Range -> Maybe (Closure Call) -> m Doc -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Range -> Maybe (Closure Call) -> m Doc -> m Doc
sayWhen (TCEnv -> Range
envRange (TCEnv -> Range) -> TCEnv -> Range
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure TypeError
e) (TCEnv -> Maybe (Closure Call)
envCall (TCEnv -> Maybe (Closure Call)) -> TCEnv -> Maybe (Closure Call)
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> TCEnv
forall a. Closure a -> TCEnv
clEnv Closure TypeError
e) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Closure TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Closure TypeError -> m Doc
prettyTCM Closure TypeError
e
Exception Range
r Doc
s -> Range -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
s
IOException TCState
_ Range
r IOException
e -> Range -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere Range
r (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ IOException -> [Char]
forall a. Show a => a -> [Char]
show IOException
e
PatternErr{} -> TCErr -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadPretty m, HasRange a) =>
a -> m Doc -> m Doc
sayWhere TCErr
err (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Monad m => [Char] -> m Doc
panic [Char]
"uncaught pattern violation"
dropTopLevelModule' :: Int -> QName -> QName
dropTopLevelModule' :: Int -> QName -> QName
dropTopLevelModule' Int
k (QName (MName [Name]
ns) Name
n) = ModuleName -> Name -> QName
QName ([Name] -> ModuleName
MName (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop Int
k [Name]
ns)) Name
n
dropTopLevelModule :: QName -> TCM QName
dropTopLevelModule :: QName -> TCM QName
dropTopLevelModule QName
q = ((QName -> QName) -> QName -> QName
forall a b. (a -> b) -> a -> b
$ QName
q) ((QName -> QName) -> QName)
-> TCMT IO (QName -> QName) -> TCM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (QName -> QName)
forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper
topLevelModuleDropper :: (MonadDebug m, MonadTCEnv m, ReadTCState m) => m (QName -> QName)
topLevelModuleDropper :: forall (m :: * -> *).
(MonadDebug m, MonadTCEnv m, ReadTCState m) =>
m (QName -> QName)
topLevelModuleDropper =
m (Maybe TopLevelModuleName)
-> m (QName -> QName)
-> (TopLevelModuleName -> m (QName -> QName))
-> m (QName -> QName)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM m (Maybe TopLevelModuleName)
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule
((QName -> QName) -> m (QName -> QName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return QName -> QName
forall a. a -> a
id)
((QName -> QName) -> m (QName -> QName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName -> QName) -> m (QName -> QName))
-> (TopLevelModuleName -> QName -> QName)
-> TopLevelModuleName
-> m (QName -> QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> QName -> QName
dropTopLevelModule' (Int -> QName -> QName)
-> (TopLevelModuleName -> Int)
-> TopLevelModuleName
-> QName
-> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> Int
forall a. Sized a => a -> Int
size)
instance PrettyTCM TypeError where
prettyTCM :: forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM TypeError
err = case TypeError
err of
InternalError [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Monad m => [Char] -> m Doc
panic [Char]
s
NotImplemented [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Not implemented: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
NotSupported [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Not supported: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
CompilationError [Char]
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Compilation error:", [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
s]
GenericError [Char]
s -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
s
GenericDocError Doc
d -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d
TypeError
PropMustBeSingleton -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords
[Char]
"Datatypes in Prop must have at most one constructor when proof irrelevance is enabled"
DataMustEndInSort Term
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The type of a datatype must end in a sort."
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"isn't a sort."
ShouldEndInApplicationOfTheDatatype Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The target of a constructor must be the datatype applied to its parameters,"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"isn't"
ShouldBeAppliedToTheDatatypeParameters Term
s Term
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The target of the constructor should be" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
s] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"instead of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t]
ShouldBeApplicationOf Type
t QName
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The pattern constructs an element 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which is not the right datatype"
ShouldBeRecordType Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Expected non-abstract record type, found " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]
ShouldBeRecordPattern DeBruijnPattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Expected record pattern"
NotAProjectionPattern NamedArg Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Not a valid projection for a copattern: " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p ]
TypeError
WrongHidingInLHS -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Unexpected implicit argument"
WrongHidingInLambda Type
t ->
[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Found an implicit lambda where an explicit lambda was expected"
TypeError
WrongIrrelevanceInLambda ->
[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Found a non-strict lambda where a irrelevant lambda was expected"
TypeError
WrongQuantityInLambda ->
[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Incorrect quantity annotation in lambda"
TypeError
WrongCohesionInLambda ->
[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Incorrect cohesion annotation in lambda"
WrongNamedArgument NamedArg Expr
a [NamedName]
xs0 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Function does not accept argument "
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NamedArg Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedArg Expr -> m Doc
prettyTCM NamedArg Expr
a]
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"possible arguments:" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: (NamedName -> m Doc) -> [NamedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedName]
xs | Bool -> Bool
not ([NamedName] -> Bool
forall a. Null a => a -> Bool
null [NamedName]
xs)]
where
xs :: [NamedName]
xs = (NamedName -> Bool) -> [NamedName] -> [NamedName]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (NamedName -> Bool) -> NamedName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedName -> Bool
forall a. IsNoName a => a -> Bool
isNoName) [NamedName]
xs0
WrongHidingInApplication Type
t ->
[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Found an implicit application where an explicit application was expected"
HidingMismatch Hiding
h Hiding
h' -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"Expected " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Indefinite Hiding -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Hiding -> Indefinite Hiding
forall a. a -> Indefinite a
Indefinite Hiding
h') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" argument, but found " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
Indefinite Hiding -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Hiding -> Indefinite Hiding
forall a. a -> Indefinite a
Indefinite Hiding
h) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" argument"
RelevanceMismatch Relevance
r Relevance
r' -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"Expected " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Indefinite Relevance -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Relevance -> Indefinite Relevance
forall a. a -> Indefinite a
Indefinite Relevance
r') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" argument, but found " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
Indefinite Relevance -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Relevance -> Indefinite Relevance
forall a. a -> Indefinite a
Indefinite Relevance
r) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" argument"
QuantityMismatch Quantity
q Quantity
q' -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"Expected " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Indefinite Quantity -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Quantity -> Indefinite Quantity
forall a. a -> Indefinite a
Indefinite Quantity
q') [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" argument, but found " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
Indefinite Quantity -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Quantity -> Indefinite Quantity
forall a. a -> Indefinite a
Indefinite Quantity
q) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" argument"
UninstantiatedDotPattern Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Failed to infer the value of dotted pattern"
ForcedConstructorNotInstantiated Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Failed to infer that constructor pattern "
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is forced"
IllformedProjectionPattern Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ill-formed projection pattern " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p]
CannotEliminateWithPattern Maybe Blocker
b NamedArg Pattern
p Type
a -> do
let isProj :: Bool
isProj = Maybe (ProjOrigin, AmbiguousQName) -> Bool
forall a. Maybe a -> Bool
isJust (NamedArg Pattern -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP NamedArg Pattern
p)
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot eliminate 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: if
| Bool
isProj -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"with projection pattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p]
| A.ProjP PatInfo
_ ProjOrigin
_ AmbiguousQName
f <- NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"with pattern" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(suggestion: write" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
".(" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (ProjOrigin -> AmbiguousQName -> Expr
A.Proj ProjOrigin
ProjPrefix AmbiguousQName
f) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
")"] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"for a dot pattern," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"or remove the braces for a postfix projection)"
| Bool
otherwise ->
m Doc
"with" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Pattern -> [Char]
forall {e}. Pattern' e -> [Char]
kindOfPattern (NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
namedArg NamedArg Pattern
p)) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: m Doc
"pattern" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: NamedArg Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA NamedArg Pattern
p m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(did you supply too many arguments?)"
where
kindOfPattern :: Pattern' e -> [Char]
kindOfPattern = \case
A.VarP{} -> [Char]
"variable"
A.ConP{} -> [Char]
"constructor"
A.ProjP{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
A.DefP{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
A.WildP{} -> [Char]
"wildcard"
A.DotP{} -> [Char]
"dot"
A.AbsurdP{} -> [Char]
"absurd"
A.LitP{} -> [Char]
"literal"
A.RecP{} -> [Char]
"record"
A.WithP{} -> [Char]
"with"
A.EqualP{} -> [Char]
"equality"
A.AsP PatInfo
_ BindName
_ Pattern' e
p -> Pattern' e -> [Char]
kindOfPattern Pattern' e
p
A.PatternSynP{} -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
A.AnnP PatInfo
_ e
_ Pattern' e
p -> Pattern' e -> [Char]
kindOfPattern Pattern' e
p
WrongNumberOfConstructorArguments QName
c Int
expect Int
given -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"expects" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
expect] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"arguments (including hidden ones), but has been given"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> m Doc
prettyTCM Int
given] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(including hidden ones)"
CantResolveOverloadedConstructorsTargetingSameDatatype QName
d List1 QName
cs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Can't resolve overloaded constructors targeting the same datatype"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> QName
qnameToConcrete QName
d)) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
colon]
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (QName -> m Doc) -> [QName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (List1 QName -> [Item (List1 QName)]
forall l. IsList l => l -> [Item l]
List1.toList List1 QName
cs)
DoesNotConstructAnElementOf QName
c Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"does not construct an element of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]
ConstructorPatternInWrongDatatype QName
c QName
d -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not a constructor of the datatype"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
d]
ShadowedModule Name
x [] -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
ShadowedModule Name
x ms :: [ModuleName]
ms@(ModuleName
m0 : [ModuleName]
_) -> do
(Range
r, ModuleName
m) <- do
ScopeInfo
scope <- m ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
let xms0 :: [(QName, ModuleName)]
xms0 = [ModuleName]
ms [ModuleName]
-> (ModuleName -> [(QName, ModuleName)]) -> [(QName, ModuleName)]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ ModuleName
m -> (QName -> (QName, ModuleName)) -> [QName] -> [(QName, ModuleName)]
forall a b. (a -> b) -> [a] -> [b]
map (,ModuleName
m) ([QName] -> [(QName, ModuleName)])
-> [QName] -> [(QName, ModuleName)]
forall a b. (a -> b) -> a -> b
$ ModuleName -> ScopeInfo -> [QName]
inverseScopeLookupModule ModuleName
m ScopeInfo
scope
[Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.clash.error" Int
30 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"candidates = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(QName, ModuleName)] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [(QName, ModuleName)]
xms0
let xms :: [(QName, ModuleName)]
xms = ((QName, ModuleName) -> Bool)
-> [(QName, ModuleName)] -> [(QName, ModuleName)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((\ QName
y -> Bool -> Bool
not (Range -> Bool
forall a. Null a => a -> Bool
null (Range -> Bool) -> Range -> Bool
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall a. HasRange a => a -> Range
getRange QName
y) Bool -> Bool -> Bool
&& QName
y QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> QName
C.QName Name
x) (QName -> Bool)
-> ((QName, ModuleName) -> QName) -> (QName, ModuleName) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName, ModuleName) -> QName
forall a b. (a, b) -> a
fst) [(QName, ModuleName)]
xms0
[Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.class.error" Int
30 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"filtered candidates = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(QName, ModuleName)] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [(QName, ModuleName)]
xms
Maybe (QName, ModuleName)
-> ((QName, ModuleName) -> m (Range, ModuleName))
-> m (Range, ModuleName)
-> m (Range, ModuleName)
forall a b. Maybe a -> (a -> b) -> b -> b
ifJust ([(QName, ModuleName)] -> Maybe (QName, ModuleName)
forall a. [a] -> Maybe a
listToMaybe [(QName, ModuleName)]
xms) (\ (QName
x', ModuleName
m) -> (Range, ModuleName) -> m (Range, ModuleName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
x', ModuleName
m)) (m (Range, ModuleName) -> m (Range, ModuleName))
-> m (Range, ModuleName) -> m (Range, ModuleName)
forall a b. (a -> b) -> a -> b
$ do
let rms :: [(Range, ModuleName)]
rms = [ModuleName]
ms [ModuleName]
-> (ModuleName -> [(Range, ModuleName)]) -> [(Range, ModuleName)]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ ModuleName
m -> (Range -> (Range, ModuleName)) -> [Range] -> [(Range, ModuleName)]
forall a b. (a -> b) -> [a] -> [b]
map (,ModuleName
m) ([Range] -> [(Range, ModuleName)])
-> [Range] -> [(Range, ModuleName)]
forall a b. (a -> b) -> a -> b
$
(Range -> Bool) -> [Range] -> [Range]
forall a. (a -> Bool) -> [a] -> [a]
filter (Range
forall a. Range' a
noRange Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/=) ([Range] -> [Range]) -> [Range] -> [Range]
forall a b. (a -> b) -> a -> b
$ (Name -> Range) -> [Name] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Range
nameBindingSite ([Name] -> [Range]) -> [Name] -> [Range]
forall a b. (a -> b) -> a -> b
$ [Name] -> [Name]
forall a. [a] -> [a]
reverse ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList ModuleName
m
[Char] -> Int -> [Char] -> m ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"scope.class.error" Int
30 ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"rangeful clashing modules = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Range, ModuleName)] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow [(Range, ModuleName)]
rms
(Range, ModuleName) -> m (Range, ModuleName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Range, ModuleName) -> m (Range, ModuleName))
-> (Range, ModuleName) -> m (Range, ModuleName)
forall a b. (a -> b) -> a -> b
$ (Range, ModuleName)
-> Maybe (Range, ModuleName) -> (Range, ModuleName)
forall a. a -> Maybe a -> a
fromMaybe (Range
forall a. Range' a
noRange, ModuleName
m0) (Maybe (Range, ModuleName) -> (Range, ModuleName))
-> Maybe (Range, ModuleName) -> (Range, ModuleName)
forall a b. (a -> b) -> a -> b
$ [(Range, ModuleName)] -> Maybe (Range, ModuleName)
forall a. [a] -> Maybe a
listToMaybe [(Range, ModuleName)]
rms
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Duplicate definition of module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Previous definition of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"at" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r]
where
help :: MonadPretty m => ModuleName -> m Doc
help :: forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help ModuleName
m = m (Maybe DataOrRecordModule)
-> m Doc -> (DataOrRecordModule -> m Doc) -> m Doc
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ModuleName -> m (Maybe DataOrRecordModule)
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe DataOrRecordModule)
isDatatypeModule ModuleName
m) m Doc
forall a. Null a => a
empty ((DataOrRecordModule -> m Doc) -> m Doc)
-> (DataOrRecordModule -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \case
DataOrRecordModule
IsDataModule -> m Doc
"(datatype)"
DataOrRecordModule
IsRecordModule -> m Doc
"(record)"
ModuleArityMismatch ModuleName
m Telescope
EmptyTel [NamedArg Expr]
args -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not parameterized, but is being applied to arguments"
ModuleArityMismatch ModuleName
m tel :: Telescope
tel@(ExtendTel Dom Type
_ Abs Telescope
_) [NamedArg Expr]
args -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The arguments to " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"do not fit the telescope" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
tel]
ShouldBeEmpty Type
t [] -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should be empty, but that's not obvious to me"
ShouldBeEmpty Type
t [DeBruijnPattern]
ps -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should be empty, but the following constructor patterns are valid:"
) 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 Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (DeBruijnPattern -> m Doc) -> [DeBruijnPattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> DeBruijnPattern -> m Doc
forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
0) [DeBruijnPattern]
ps)
ShouldBeASort Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should be a sort, but it isn't"
ShouldBePi Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should be a function type, but it isn't"
ShouldBePath Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should be a Path or PathP type, but it isn't"
TypeError
NotAProperTerm -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"Found a malformed term"
InvalidTypeSort Sort
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not a valid type"
InvalidType Term
v -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not a valid type"
FunctionTypeInSizeUniv Term
v -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Functions may not return sizes, thus, function type " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is illegal"
SplitOnIrrelevant Dom Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot pattern match against" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ Relevance -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Relevance -> [Char]) -> Relevance -> [Char]
forall a b. (a -> b) -> a -> b
$ Dom Type -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Dom Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"argument 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> m Doc) -> Type -> m Doc
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t]
SplitOnUnusableCohesion Dom Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot pattern match against" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ Cohesion -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Cohesion -> [Char]) -> Cohesion -> [Char]
forall a b. (a -> b) -> a -> b
$ Dom Type -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Dom Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"argument 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> m Doc) -> Type -> m Doc
forall a b. (a -> b) -> a -> b
$ Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
t]
SplitOnNonVariable Term
v Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot pattern match because the (refined) argument " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is not a variable."
SplitOnNonEtaRecord QName
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Pattern matching on no-eta record type"
, [ QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q, m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc
"defined 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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r) ]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not allowed"
, [ m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens m Doc
"to activate, add declaration `pattern` to record definition" ]
]
where r :: Range
r = Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q
DefinitionIsIrrelevant QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
m Doc
"Identifier" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is declared irrelevant, so it cannot be used here"
DefinitionIsErased QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
m Doc
"Identifier" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is declared erased, so it cannot be used here"
VariableIsIrrelevant Name
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
m Doc
"Variable" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM (Name -> Name
nameConcrete Name
x) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is declared irrelevant, so it cannot be used here"
VariableIsErased Name
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
m Doc
"Variable" m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM (Name -> Name
nameConcrete Name
x) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is declared erased, so it cannot be used here"
VariableIsOfUnusableCohesion Name
x Cohesion
c -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
[m Doc
"Variable", Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM (Name -> Name
nameConcrete Name
x), m Doc
"is declared", [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Cohesion -> [Char]
forall a. Show a => a -> [Char]
show Cohesion
c), m Doc
"so it cannot be used here"]
UnequalBecauseOfUniverseConflict Comparison
cmp Term
s Term
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
s, Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t, m Doc
"because this would result in an invalid use of Setω" ]
UnequalTerms Comparison
cmp Term
s Term
t CompareAs
a -> case (Term
s,Term
t) of
(Sort Sort
s1 , Sort Sort
s2 )
| Comparison
CmpEq <- Comparison
cmp -> TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM (TypeError -> m Doc) -> TypeError -> m Doc
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> TypeError
UnequalSorts Sort
s1 Sort
s2
| Comparison
CmpLeq <- Comparison
cmp -> TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM (TypeError -> m Doc) -> TypeError -> m Doc
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> TypeError
NotLeqSort Sort
s1 Sort
s2
(Sort MetaS{} , Term
t ) -> TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM (TypeError -> m Doc) -> TypeError -> m Doc
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
t
(Term
s , Sort MetaS{} ) -> TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM (TypeError -> m Doc) -> TypeError -> m Doc
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
s
(Sort DefS{} , Term
t ) -> TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM (TypeError -> m Doc) -> TypeError -> m Doc
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
t
(Term
s , Sort DefS{} ) -> TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM (TypeError -> m Doc) -> TypeError -> m Doc
forall a b. (a -> b) -> a -> b
$ Type -> TypeError
ShouldBeASort (Type -> TypeError) -> Type -> TypeError
forall a b. (a -> b) -> a -> b
$ Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
forall a. HasCallStack => a
__IMPOSSIBLE__ Term
s
(Term
_ , Term
_ ) -> do
(Doc
d1, Doc
d2, Doc
d) <- Term -> Term -> m (Doc, Doc, Doc)
forall (m :: * -> *).
MonadPretty m =>
Term -> Term -> m (Doc, Doc, Doc)
prettyInEqual Term
s Term
t
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
[ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d1, Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d2]
, case CompareAs
a of
AsTermsOf Type
t -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]
CompareAs
AsSizes -> [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM (Type -> m Doc) -> m Type -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m Type
forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType]
CompareAs
AsTypes -> []
, [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d]
]
UnequalLevel Comparison
cmp Level
s Level
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Level -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM Level
s, Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, Level -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Level -> m Doc
prettyTCM Level
t]
UnequalTypes Comparison
cmp Type
a Type
b -> Type -> m Doc -> Type -> m Doc
forall a (m :: * -> *).
(PrettyUnequal a, MonadPretty m) =>
a -> m Doc -> a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Type -> m Doc -> Type -> m Doc
prettyUnequal Type
a (Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp) Type
b
UnequalRelevance Comparison
cmp Term
a Term
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
a, Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is a relevant function type and the other is an irrelevant function type"
UnequalQuantity Comparison
cmp Term
a Term
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
a, Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is a non-erased function type and the other is an erased function type"
UnequalCohesion Comparison
cmp Term
a Term
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
a, Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is a non-flat function type and the other is a flat function type"
UnequalFiniteness Comparison
cmp Term
a Term
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
a, Comparison -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp, Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is a type of partial elements and the other is a function type"
UnequalHiding Term
a Term
b -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
a, m Doc
"!=", Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
b] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because one is an implicit function type and the other is an explicit function type"
UnequalSorts Sort
s1 Sort
s2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1, m Doc
"!=", Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2]
NotLeqSort Sort
s1 Sort
s2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s1] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not less or equal than" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Sort -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Sort -> m Doc
prettyTCM Sort
s2]
TooManyFields QName
r [Name]
missing [Name]
xs -> QName -> [Name] -> [Name] -> m Doc
forall (m :: * -> *).
MonadPretty m =>
QName -> [Name] -> [Name] -> m Doc
prettyTooManyFields QName
r [Name]
missing [Name]
xs
DuplicateConstructors [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Duplicate" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name] -> [m Doc]
forall {a} {m :: * -> *}. (Sized a, Applicative m) => a -> [m Doc]
constructors [Name]
xs [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ((Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs) [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in datatype"
where
constructors :: a -> [m Doc]
constructors a
ys = a -> [m Doc] -> [m Doc] -> [m Doc]
forall a c. Sized a => a -> c -> c -> c
P.singPlural a
ys [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"constructor"] [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"constructors"]
DuplicateFields [Name]
xs -> [Name] -> m Doc
forall (m :: * -> *). MonadPretty m => [Name] -> m Doc
prettyDuplicateFields [Name]
xs
WithOnFreeVariable Expr
e Term
v -> do
Doc
de <- Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
Doc
dv <- Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
if Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
de [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== Doc -> [Char]
forall a. Show a => a -> [Char]
show Doc
dv
then [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot `with` on variable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
dv] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" bound in a module telescope (or patterns of a parent clause)"
else [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot `with` on expression" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
de] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which reduces to variable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
dv] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" bound in a module telescope (or patterns of a parent clause)"
UnexpectedWithPatterns [Pattern]
ps -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unexpected with patterns" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
" |" ((Pattern -> m Doc) -> [Pattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Pattern]
ps)
WithClausePatternMismatch Pattern
p NamedArg DeBruijnPattern
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"With clause pattern " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Pattern
p] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is not an instance of its parent pattern " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.fsep ([Doc] -> Doc) -> m [Doc] -> m Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedArg DeBruijnPattern] -> m [Doc]
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m [Doc]
prettyTCMPatterns [NamedArg DeBruijnPattern
q]]
MetaCannotDependOn MetaId
m Int
i -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The metavariable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> Term -> m Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
m []] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot depend on" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> m Doc
pvar Int
i] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[]
where
pvar :: Int -> m Doc
pvar = Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> (Int -> Term) -> Int -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term
I.var
MetaOccursInItself MetaId
m -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot construct infinite solution of metavariable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> m Doc) -> Term -> m Doc
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
m []]
MetaIrrelevantSolution MetaId
m Term
_ -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot instantiate the metavariable because (part of) the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"solution was created in an irrelevant context."
MetaErasedSolution MetaId
m Term
_ -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot instantiate the metavariable because (part of) the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"solution was created in an erased context."
BuiltinMustBeConstructor [Char]
s Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"must be a constructor in the binding to builtin" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
s]
NoSuchBuiltinName [Char]
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"There is no built-in thing called" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
s]
DuplicateBuiltinBinding [Char]
b Term
x Term
y -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Duplicate binding for built-in thing" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
b m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"previous binding to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
x]
NoBindingForBuiltin [Char]
x
| [Char]
x [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]
builtinZero, [Char]
builtinSuc] -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"No binding for builtin " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"use {-# BUILTIN " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
builtinNat [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" name #-} to bind builtin natural " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"numbers to the type 'name'")
| Bool
otherwise -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"No binding for builtin thing" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"use {-# BUILTIN " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" name #-} to bind it to 'name'")
DuplicatePrimitiveBinding [Char]
b QName
x QName
y -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Duplicate binding for primitive thing" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
b m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"previous binding to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]
NoSuchPrimitiveFunction [Char]
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"There is no primitive function called" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
x]
WrongModalityForPrimitive [Char]
x ArgInfo
got ArgInfo
expect ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Wrong modality for primitive" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
x]
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Got: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [[Char]]
gs
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Expected: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [[Char]]
es ]
where
([[Char]]
gs, [[Char]]
es) = [([Char], [Char])] -> ([[Char]], [[Char]])
forall a b. [(a, b)] -> ([a], [b])
unzip [ ([Char], [Char])
p | p :: ([Char], [Char])
p@([Char]
g, [Char]
e) <- [[Char]] -> [[Char]] -> [([Char], [Char])]
forall a b. [a] -> [b] -> [(a, b)]
zip (ArgInfo -> [[Char]]
forall {a}.
(LensHiding a, LensRelevance a, LensQuantity a, LensCohesion a) =>
a -> [[Char]]
things ArgInfo
got) (ArgInfo -> [[Char]]
forall {a}.
(LensHiding a, LensRelevance a, LensQuantity a, LensCohesion a) =>
a -> [[Char]]
things ArgInfo
expect), [Char]
g [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
e ]
things :: a -> [[Char]]
things a
i = [Hiding -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Hiding -> [Char]) -> Hiding -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding a
i,
Relevance -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Relevance -> [Char]) -> Relevance -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance a
i,
Quantity -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Quantity -> [Char]) -> Quantity -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity a
i,
Cohesion -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Cohesion -> [Char]) -> Cohesion -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion a
i]
BuiltinInParameterisedModule [Char]
x -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"The BUILTIN pragma cannot appear inside a bound context " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"(for instance, in a parameterised module or as a local declaration)"
IllegalLetInTelescope TypedBinding
tb -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
TypedBinding -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TypedBinding
tb m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is not allowed in a telescope here."
IllegalPatternInTelescope Binder
bd -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
Binder -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Binder
bd m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is not allowed in a telescope here."
NoRHSRequiresAbsurdPattern [NamedArg Pattern]
ps -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"The right-hand side can only be omitted if there " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"is an absurd pattern, () or {}, in the left-hand side."
LocalVsImportedModuleClash ModuleName
m -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can refer to either a local module or an imported module"
TypeError
SolvedButOpenHoles -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Module cannot be imported since it has open interaction points" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(consider adding {-# OPTIONS --allow-unsolved-metas #-} to this module)"
CyclicModuleDependency [TopLevelModuleName]
ms ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cyclic module dependency:")
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 Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (TopLevelModuleName -> m Doc) -> [TopLevelModuleName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [TopLevelModuleName]
ms)
FileNotFound TopLevelModuleName
x [AbsolutePath]
files ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Failed to find source of module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in any of the following locations:"
) 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 Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> [AbsolutePath] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc)
-> (AbsolutePath -> [Char]) -> AbsolutePath -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
filePath) [AbsolutePath]
files)
OverlappingProjects AbsolutePath
f TopLevelModuleName
m1 TopLevelModuleName
m2
| Doc -> CI [Char]
canon Doc
d1 CI [Char] -> CI [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== Doc -> CI [Char]
canon Doc
d2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Case mismatch when accessing file"
, [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
f ]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"through module name"
, [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d2 ]
]
| Bool
otherwise -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep
( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The file" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (AbsolutePath -> [Char]
filePath AbsolutePath
f)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"can be accessed via several project roots. Both" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d1 ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"and" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d2 ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"point to this file."
)
where
canon :: Doc -> CI [Char]
canon = [Char] -> CI [Char]
forall s. FoldCase s => s -> CI s
CaseInsens.mk ([Char] -> CI [Char]) -> (Doc -> [Char]) -> Doc -> CI [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
P.render
d1 :: Doc
d1 = TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
m1
d2 :: Doc
d2 = TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
m2
AmbiguousTopLevelModuleName TopLevelModuleName
x [AbsolutePath]
files ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ambiguous module name. The module name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"could refer to any of the following files:"
) 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 Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> [AbsolutePath] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc)
-> (AbsolutePath -> [Char]) -> AbsolutePath -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
filePath) [AbsolutePath]
files)
ClashingFileNamesFor ModuleName
x [AbsolutePath]
files ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Multiple possible sources for module"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"found:"
) 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 Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> [AbsolutePath] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc)
-> (AbsolutePath -> [Char]) -> AbsolutePath -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
filePath) [AbsolutePath]
files)
ModuleDefinedInOtherFile TopLevelModuleName
mod AbsolutePath
file AbsolutePath
file' -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"You tried to load" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (AbsolutePath -> [Char]
filePath AbsolutePath
file)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"which defines the module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
mod m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"However, according to the include path this module should" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"be defined in" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (AbsolutePath -> [Char]
filePath AbsolutePath
file') m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
ModuleNameUnexpected TopLevelModuleName
given TopLevelModuleName
expected
| Doc -> CI [Char]
canon Doc
dGiven CI [Char] -> CI [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== Doc -> CI [Char]
canon Doc
dExpected -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Case mismatch between the actual module name"
, [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
dGiven ]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"and the expected module name"
, [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
dExpected ]
]
| Bool
otherwise -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The name of the top level module does not match the file name. The module"
, [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
dGiven ]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should probably be named"
, [ Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
dExpected ]
]
where
canon :: Doc -> CI [Char]
canon = [Char] -> CI [Char]
forall s. FoldCase s => s -> CI s
CaseInsens.mk ([Char] -> CI [Char]) -> (Doc -> [Char]) -> Doc -> CI [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
P.render
dGiven :: Doc
dGiven = TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
given
dExpected :: Doc
dExpected = TopLevelModuleName -> Doc
forall a. Pretty a => a -> Doc
P.pretty TopLevelModuleName
expected
ModuleNameDoesntMatchFileName TopLevelModuleName
given [AbsolutePath]
files ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The name of the top level module does not match the file name. The module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[ TopLevelModuleName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
given ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"should be defined in one of the following files:")
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 Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (AbsolutePath -> m Doc) -> [AbsolutePath] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc)
-> (AbsolutePath -> [Char]) -> AbsolutePath -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> [Char]
filePath) [AbsolutePath]
files)
TypeError
BothWithAndRHS -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unexpected right hand side"
AbstractConstructorNotInScope QName
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ m Doc
"Constructor"
, QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is abstract, thus, not in scope here"
NotInScope [QName]
xs ->
Warning -> m Doc
forall (m :: * -> *). MonadPretty m => Warning -> m Doc
prettyWarning ([QName] -> Warning
NotInScopeW [QName]
xs)
NoSuchModule QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"No module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"in scope"
AmbiguousName QName
x AmbiguousNameReason
reason -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ambiguous name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It could refer to any one of"
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ List2 (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (List2 (m Doc) -> m Doc) -> List2 (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (QName -> m Doc) -> List2 QName -> List2 (m Doc)
forall a b. (a -> b) -> List2 a -> List2 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
nameWithBinding (List2 QName -> List2 (m Doc)) -> List2 QName -> List2 (m Doc)
forall a b. (a -> b) -> a -> b
$ AmbiguousNameReason -> List2 QName
ambiguousNamesInReason AmbiguousNameReason
reason
, WhyInScopeData -> m Doc
forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope (WhyInScopeData -> m Doc) -> WhyInScopeData -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousNameReason -> WhyInScopeData
whyInScopeDataFromAmbiguousNameReason QName
x AmbiguousNameReason
reason
]
AmbiguousModule QName
x List1 ModuleName
ys -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ambiguous module name" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"It could refer to any one of"
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (ModuleName -> m Doc) -> List1 ModuleName -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ModuleName -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help List1 ModuleName
ys
, [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"(hint: Use C-c C-w (in Emacs) if you want to know why)"
]
where
help :: MonadPretty m => ModuleName -> m Doc
help :: forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
help ModuleName
m = do
m Doc
anno <- m (Maybe DataOrRecordModule)
-> m (m Doc) -> (DataOrRecordModule -> m (m Doc)) -> m (m Doc)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ModuleName -> m (Maybe DataOrRecordModule)
forall (m :: * -> *).
ReadTCState m =>
ModuleName -> m (Maybe DataOrRecordModule)
isDatatypeModule ModuleName
m) (m Doc -> m (m Doc)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return m Doc
forall a. Null a => a
empty) ((DataOrRecordModule -> m (m Doc)) -> m (m Doc))
-> (DataOrRecordModule -> m (m Doc)) -> m (m Doc)
forall a b. (a -> b) -> a -> b
$ \case
DataOrRecordModule
IsDataModule -> m Doc -> m (m Doc)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (m Doc -> m (m Doc)) -> m Doc -> m (m Doc)
forall a b. (a -> b) -> a -> b
$ m Doc
"(datatype module)"
DataOrRecordModule
IsRecordModule -> m Doc -> m (m Doc)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (m Doc -> m (m Doc)) -> m Doc -> m (m Doc)
forall a b. (a -> b) -> a -> b
$ m Doc
"(record module)"
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m, m Doc
anno ]
ClashingDefinition QName
x QName
y Maybe NiceDeclaration
suggestion -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Multiple definitions of" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Previous definition at"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Range -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (Range -> m Doc) -> Range -> m Doc
forall a b. (a -> b) -> a -> b
$ Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
y] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
Maybe NiceDeclaration
-> [m Doc] -> (NiceDeclaration -> [m Doc]) -> [m Doc]
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe NiceDeclaration
suggestion [] (\NiceDeclaration
d ->
[ m Doc
"Perhaps you meant to write "
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 Int
2 (m Doc
"'" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> [Declaration] -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (NiceDeclaration -> [Declaration]
notSoNiceDeclarations NiceDeclaration
d) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"'")
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ (m Doc
"at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (Range -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Range -> m Doc) -> (TCEnv -> Range) -> TCEnv -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> Range
envRange (TCEnv -> m Doc) -> m TCEnv -> m Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m TCEnv
forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC)) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"?"
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ m Doc
"In data definitions separate from data declaration, the ':' and type must be omitted."
])
ClashingModule ModuleName
m1 ModuleName
m2 -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The modules" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m1, m Doc
"and", ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
m2]
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"clash."
ClashingImport Name
x QName
y -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Import clash between" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
x, m Doc
"and", QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
y]
ClashingModuleImport Name
x ModuleName
y -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Module import clash between" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Name
x, m Doc
"and", ModuleName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ModuleName -> m Doc
prettyTCM ModuleName
y]
PatternShadowsConstructor Name
x QName
c -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The pattern variable" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Name -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Name -> m Doc
prettyTCM Name
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"has the same name as 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c]
DuplicateImports QName
m [ImportedName]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Ambiguous imports from module" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty QName
m] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
m Doc -> [m Doc] -> [m Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate m Doc
forall (m :: * -> *). Applicative m => m Doc
comma ((ImportedName -> m Doc) -> [ImportedName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map ImportedName -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [ImportedName]
xs)
NotAModuleExpr Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The right-hand side of a module definition must have the form 'M e1 .. en'" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"where M is a module name. The expression"
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e, m Doc
"doesn't."]
TypeError
FieldOutsideRecord -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Field appearing outside record declaration."
InvalidPattern Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not a valid pattern"
RepeatedVariablesInPattern [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Repeated variables in pattern:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs
NotAnExpression Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"is not a valid expression."
NotAValidLetBinding NiceDeclaration
nd -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"Not a valid let-declaration"
NotValidBeforeField NiceDeclaration
nd -> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"This declaration is illegal in a record before the last field"
NothingAppliedToHiddenArg Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot appear by itself. It needs to be the argument to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function expecting an implicit argument."
NothingAppliedToInstanceArg Expr
e -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"cannot appear by itself. It needs to be the argument to" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"a function expecting an instance argument."
NoParseForApplication List2 Expr
es -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Could not parse the application" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Expr -> m Doc) -> Expr -> m Doc
forall a b. (a -> b) -> a -> b
$ Range -> List2 Expr -> Expr
C.RawApp Range
forall a. Range' a
noRange List2 Expr
es])
AmbiguousParseForApplication List2 Expr
es List1 Expr
es' -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Don't know how to parse" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc
forall (m :: * -> *). MonadPretty m => m Doc
pretty_es m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Could mean any one of:"
) 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 Int
2 (NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ (Expr -> m Doc) -> List1 Expr -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
pretty' List1 Expr
es')
where
pretty_es :: MonadPretty m => m Doc
pretty_es :: forall (m :: * -> *). MonadPretty m => m Doc
pretty_es = Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Expr -> m Doc) -> Expr -> m Doc
forall a b. (a -> b) -> a -> b
$ Range -> List2 Expr -> Expr
C.RawApp Range
forall a. Range' a
noRange List2 Expr
es
pretty' :: MonadPretty m => C.Expr -> m Doc
pretty' :: forall (m :: * -> *). MonadPretty m => Expr -> m Doc
pretty' Expr
e = do
Doc
p1 <- m Doc
forall (m :: * -> *). MonadPretty m => m Doc
pretty_es
Doc
p2 <- Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e
if Doc -> [Char]
render Doc
p1 [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== Doc -> [Char]
render Doc
p2 then Expr -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
unambiguous Expr
e else Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
p2
unambiguous :: MonadPretty m => C.Expr -> m Doc
unambiguous :: forall (m :: * -> *). MonadPretty m => Expr -> m Doc
unambiguous e :: Expr
e@(C.OpApp Range
r QName
op Set Name
_ OpAppArgs
xs)
| (NamedArg (MaybePlaceholder (OpApp Expr)) -> Bool)
-> OpAppArgs -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (MaybePlaceholder (OpApp Expr) -> Bool
forall e. MaybePlaceholder (OpApp e) -> Bool
isOrdinary (MaybePlaceholder (OpApp Expr) -> Bool)
-> (NamedArg (MaybePlaceholder (OpApp Expr))
-> MaybePlaceholder (OpApp Expr))
-> NamedArg (MaybePlaceholder (OpApp Expr))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (MaybePlaceholder (OpApp Expr))
-> MaybePlaceholder (OpApp Expr)
forall a. NamedArg a -> a
namedArg) OpAppArgs
xs =
Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Expr -> m Doc) -> Expr -> m Doc
forall a b. (a -> b) -> a -> b
$
(Expr -> NamedArg Expr -> Expr) -> Expr -> [NamedArg Expr] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Range -> Expr -> NamedArg Expr -> Expr
C.App Range
r) (QName -> Expr
C.Ident QName
op) ([NamedArg Expr] -> Expr) -> [NamedArg Expr] -> Expr
forall a b. (a -> b) -> a -> b
$
((NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> OpAppArgs -> [NamedArg Expr]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> OpAppArgs -> [NamedArg Expr])
-> ((MaybePlaceholder (OpApp Expr) -> Expr)
-> NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> (MaybePlaceholder (OpApp Expr) -> Expr)
-> OpAppArgs
-> [NamedArg Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (MaybePlaceholder (OpApp Expr)) -> Named_ Expr)
-> NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName (MaybePlaceholder (OpApp Expr)) -> Named_ Expr)
-> NamedArg (MaybePlaceholder (OpApp Expr)) -> NamedArg Expr)
-> ((MaybePlaceholder (OpApp Expr) -> Expr)
-> Named NamedName (MaybePlaceholder (OpApp Expr)) -> Named_ Expr)
-> (MaybePlaceholder (OpApp Expr) -> Expr)
-> NamedArg (MaybePlaceholder (OpApp Expr))
-> NamedArg Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (MaybePlaceholder (OpApp Expr) -> Expr)
-> Named NamedName (MaybePlaceholder (OpApp Expr)) -> Named_ Expr
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) MaybePlaceholder (OpApp Expr) -> Expr
forall e. MaybePlaceholder (OpApp e) -> e
fromOrdinary OpAppArgs
xs
| (NamedArg (MaybePlaceholder (OpApp Expr)) -> Bool)
-> OpAppArgs -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (MaybePlaceholder (OpApp Expr) -> Bool
forall a. MaybePlaceholder a -> Bool
isPlaceholder (MaybePlaceholder (OpApp Expr) -> Bool)
-> (NamedArg (MaybePlaceholder (OpApp Expr))
-> MaybePlaceholder (OpApp Expr))
-> NamedArg (MaybePlaceholder (OpApp Expr))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (MaybePlaceholder (OpApp Expr))
-> MaybePlaceholder (OpApp Expr)
forall a. NamedArg a -> a
namedArg) OpAppArgs
xs =
Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"(section)"
unambiguous Expr
e = Expr -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Expr
e
isOrdinary :: MaybePlaceholder (C.OpApp e) -> Bool
isOrdinary :: forall e. MaybePlaceholder (OpApp e) -> Bool
isOrdinary (NoPlaceholder Maybe PositionInName
_ (C.Ordinary e
_)) = Bool
True
isOrdinary MaybePlaceholder (OpApp e)
_ = Bool
False
fromOrdinary :: MaybePlaceholder (C.OpApp e) -> e
fromOrdinary :: forall e. MaybePlaceholder (OpApp e) -> e
fromOrdinary (NoPlaceholder Maybe PositionInName
_ (C.Ordinary e
e)) = e
e
fromOrdinary MaybePlaceholder (OpApp e)
_ = e
forall a. HasCallStack => a
__IMPOSSIBLE__
isPlaceholder :: MaybePlaceholder a -> Bool
isPlaceholder :: forall a. MaybePlaceholder a -> Bool
isPlaceholder Placeholder{} = Bool
True
isPlaceholder NoPlaceholder{} = Bool
False
BadArgumentsToPatternSynonym AmbiguousQName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Bad arguments to pattern synonym " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> m Doc) -> QName -> m Doc
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
x]
TooFewArgumentsToPatternSynonym AmbiguousQName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Too few arguments to pattern synonym " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM (QName -> m Doc) -> QName -> m Doc
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> QName
headAmbQ AmbiguousQName
x]
CannotResolveAmbiguousPatternSynonym List1 (QName, PatternSynDefn)
defs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot resolve overloaded pattern synonym" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
forall (m :: * -> *). Applicative m => m Doc
comma] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"since candidates have different shapes:"
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ NonEmpty (m Doc) -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (NonEmpty (m Doc) -> m Doc) -> NonEmpty (m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ ((QName, PatternSynDefn) -> m Doc)
-> List1 (QName, PatternSynDefn) -> NonEmpty (m Doc)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName, PatternSynDefn) -> m Doc
forall {m :: * -> *}.
(MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
Semigroup (m Doc)) =>
(QName, PatternSynDefn) -> m Doc
prDef List1 (QName, PatternSynDefn)
defs
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(hint: overloaded pattern synonyms must be equal up to variable and constructor names)"
]
where
(QName
x, PatternSynDefn
_) = List1 (QName, PatternSynDefn) -> (QName, PatternSynDefn)
forall a. NonEmpty a -> a
List1.head List1 (QName, PatternSynDefn)
defs
prDef :: (QName, PatternSynDefn) -> m Doc
prDef (QName
x, ([Arg Name]
xs, Pattern' Void
p)) = Declaration -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (QName -> [Arg BindName] -> Pattern' Void -> Declaration
A.PatternSynDef QName
x ((Arg Name -> Arg BindName) -> [Arg Name] -> [Arg BindName]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> BindName) -> Arg Name -> Arg BindName
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> BindName
BindName) [Arg Name]
xs) Pattern' Void
p) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> (m Doc
"at" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Range -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Range
r)
where r :: Range
r = Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x
TypeError
UnusedVariableInPatternSynonym -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unused variable in pattern synonym."
NoParseForLHS LHSOrPatSyn
lhsOrPatSyn [Pattern]
errs Pattern
p -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Could not parse the" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [m Doc]
prettyLhsOrPatSyn [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p]
, m Doc
prettyErrs
]
where
prettyLhsOrPatSyn :: [m Doc]
prettyLhsOrPatSyn = [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ case LHSOrPatSyn
lhsOrPatSyn of
LHSOrPatSyn
IsLHS -> [Char]
"left-hand side"
LHSOrPatSyn
IsPatSyn -> [Char]
"pattern synonym"
prettyErrs :: m Doc
prettyErrs = case [Pattern]
errs of
[] -> m Doc
forall a. Null a => a
empty
Pattern
p0 : [Pattern]
_ -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Problematic expression:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p0]
AmbiguousParseForLHS LHSOrPatSyn
lhsOrPatSyn Pattern
p [Pattern]
ps -> do
Doc
d <- Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Don't know how to parse" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
d m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Could mean any one of:"
]
[m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
(Pattern -> m Doc) -> [Pattern] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> (Pattern -> m Doc) -> Pattern -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Pattern -> m Doc
forall (m :: * -> *). MonadPretty m => Doc -> Pattern -> m Doc
pretty' Doc
d) [Pattern]
ps
where
pretty' :: MonadPretty m => Doc -> C.Pattern -> m Doc
pretty' :: forall (m :: * -> *). MonadPretty m => Doc -> Pattern -> m Doc
pretty' Doc
d1 Pattern
p' = do
Doc
d2 <- Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Pattern
p'
if Doc -> [Char]
render Doc
d1 [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== Doc -> [Char]
render Doc
d2 then Pattern -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (Pattern -> m Doc) -> Pattern -> m Doc
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
p' else Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d2
unambiguousP :: C.Pattern -> C.Pattern
unambiguousP :: Pattern -> Pattern
unambiguousP (C.AppP Pattern
x Arg (Named NamedName Pattern)
y) = Pattern -> Arg (Named NamedName Pattern) -> Pattern
C.AppP (Pattern -> Pattern
unambiguousP Pattern
x) (Arg (Named NamedName Pattern) -> Pattern)
-> Arg (Named NamedName Pattern) -> Pattern
forall a b. (a -> b) -> a -> b
$ ((Named NamedName Pattern -> Named NamedName Pattern)
-> Arg (Named NamedName Pattern) -> Arg (Named NamedName Pattern)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap((Named NamedName Pattern -> Named NamedName Pattern)
-> Arg (Named NamedName Pattern) -> Arg (Named NamedName Pattern))
-> ((Pattern -> Pattern)
-> Named NamedName Pattern -> Named NamedName Pattern)
-> (Pattern -> Pattern)
-> Arg (Named NamedName Pattern)
-> Arg (Named NamedName Pattern)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Pattern -> Pattern)
-> Named NamedName Pattern -> Named NamedName Pattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Pattern -> Pattern
unambiguousP Arg (Named NamedName Pattern)
y
unambiguousP (C.HiddenP Range
r Named NamedName Pattern
x) = Range -> Named NamedName Pattern -> Pattern
C.HiddenP Range
r (Named NamedName Pattern -> Pattern)
-> Named NamedName Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Pattern -> Pattern)
-> Named NamedName Pattern -> Named NamedName Pattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
unambiguousP Named NamedName Pattern
x
unambiguousP (C.InstanceP Range
r Named NamedName Pattern
x) = Range -> Named NamedName Pattern -> Pattern
C.InstanceP Range
r (Named NamedName Pattern -> Pattern)
-> Named NamedName Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ (Pattern -> Pattern)
-> Named NamedName Pattern -> Named NamedName Pattern
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Pattern
unambiguousP Named NamedName Pattern
x
unambiguousP (C.ParenP Range
r Pattern
x) = Range -> Pattern -> Pattern
C.ParenP Range
r (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
x
unambiguousP (C.AsP Range
r Name
n Pattern
x) = Range -> Name -> Pattern -> Pattern
C.AsP Range
r Name
n (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Pattern
unambiguousP Pattern
x
unambiguousP (C.OpAppP Range
r QName
op Set Name
_ [Arg (Named NamedName Pattern)]
xs) = (Pattern -> Arg (Named NamedName Pattern) -> Pattern)
-> Pattern -> [Arg (Named NamedName Pattern)] -> Pattern
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Pattern -> Arg (Named NamedName Pattern) -> Pattern
C.AppP (QName -> Pattern
C.IdentP QName
op) [Arg (Named NamedName Pattern)]
xs
unambiguousP Pattern
e = Pattern
e
OperatorInformation [NotationSection]
sects TypeError
err ->
TypeError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TypeError -> m Doc
prettyTCM TypeError
err
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$+$
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Operators used in the grammar:")
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 Int
2
(if [NotationSection] -> Bool
forall a. Null a => a -> Bool
null [NotationSection]
sects then m Doc
"None" else
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (([Char] -> m Doc) -> [[Char]] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([[Char]] -> [m Doc]) -> [[Char]] -> [m Doc]
forall a b. (a -> b) -> a -> b
$
[Char] -> [[Char]]
lines ([Char] -> [[Char]]) -> [Char] -> [[Char]]
forall a b. (a -> b) -> a -> b
$
Box -> [Char]
Boxes.render (Box -> [Char]) -> Box -> [Char]
forall a b. (a -> b) -> a -> b
$
(\([Box]
col1, [Box]
col2, [Box]
col3) ->
Int -> Alignment -> [Box] -> Box
forall (f :: * -> *).
Foldable f =>
Int -> Alignment -> f Box -> Box
Boxes.hsep Int
1 Alignment
Boxes.top ([Box] -> Box) -> [Box] -> Box
forall a b. (a -> b) -> a -> b
$
([Box] -> Box) -> [[Box]] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map (Alignment -> [Box] -> Box
forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.left) [[Box]
col1, [Box]
col2, [Box]
col3]) (([Box], [Box], [Box]) -> Box) -> ([Box], [Box], [Box]) -> Box
forall a b. (a -> b) -> a -> b
$
[(Box, Box, Box)] -> ([Box], [Box], [Box])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([(Box, Box, Box)] -> ([Box], [Box], [Box]))
-> [(Box, Box, Box)] -> ([Box], [Box], [Box])
forall a b. (a -> b) -> a -> b
$
(NotationSection -> (Box, Box, Box))
-> [NotationSection] -> [(Box, Box, Box)]
forall a b. (a -> b) -> [a] -> [b]
map NotationSection -> (Box, Box, Box)
prettySect ([NotationSection] -> [(Box, Box, Box)])
-> [NotationSection] -> [(Box, Box, Box)]
forall a b. (a -> b) -> a -> b
$
(NotationSection -> NotationSection -> Ordering)
-> [NotationSection] -> [NotationSection]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ([Char] -> [Char] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Char] -> [Char] -> Ordering)
-> (NotationSection -> [Char])
-> NotationSection
-> NotationSection
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> [Char])
-> (NotationSection -> QName) -> NotationSection -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> QName
notaName (NewNotation -> QName)
-> (NotationSection -> NewNotation) -> NotationSection -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotationSection -> NewNotation
sectNotation) ([NotationSection] -> [NotationSection])
-> [NotationSection] -> [NotationSection]
forall a b. (a -> b) -> a -> b
$
(NotationSection -> Bool) -> [NotationSection] -> [NotationSection]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (NotationSection -> Bool) -> NotationSection -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NotationSection -> Bool
closedWithoutHoles) [NotationSection]
sects))
where
trimLeft :: [NotationPart] -> [NotationPart]
trimLeft = (NotationPart -> Bool) -> [NotationPart] -> [NotationPart]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile NotationPart -> Bool
isAHole
trimRight :: [NotationPart] -> [NotationPart]
trimRight = (NotationPart -> Bool) -> [NotationPart] -> [NotationPart]
forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd NotationPart -> Bool
isAHole
closedWithoutHoles :: NotationSection -> Bool
closedWithoutHoles NotationSection
sect =
NotationSection -> NotationKind
sectKind NotationSection
sect NotationKind -> NotationKind -> Bool
forall a. Eq a => a -> a -> Bool
== NotationKind
NonfixNotation
Bool -> Bool -> Bool
&&
[()] -> Bool
forall a. Null a => a -> Bool
null [ () | HolePart{} <- [NotationPart] -> [NotationPart]
trimLeft ([NotationPart] -> [NotationPart])
-> [NotationPart] -> [NotationPart]
forall a b. (a -> b) -> a -> b
$ [NotationPart] -> [NotationPart]
trimRight ([NotationPart] -> [NotationPart])
-> [NotationPart] -> [NotationPart]
forall a b. (a -> b) -> a -> b
$
NewNotation -> [NotationPart]
notation (NotationSection -> NewNotation
sectNotation NotationSection
sect) ]
prettyName :: Name -> Box
prettyName Name
n = [Char] -> Box
Boxes.text ([Char] -> Box) -> [Char] -> Box
forall a b. (a -> b) -> a -> b
$
Doc -> [Char]
P.render (Name -> Doc
forall a. Pretty a => a -> Doc
P.pretty Name
n) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
" (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
P.render (Range -> Doc
forall a. Pretty a => a -> Doc
P.pretty (Name -> Range
nameBindingSite Name
n)) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
prettySect :: NotationSection -> (Box, Box, Box)
prettySect NotationSection
sect =
( [Char] -> Box
Boxes.text (Doc -> [Char]
P.render ([NotationPart] -> Doc
forall a. Pretty a => a -> Doc
P.pretty [NotationPart]
section))
Box -> Box -> Box
Boxes.//
Box
strut
, [Char] -> Box
Boxes.text
([Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
kind [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
(if NewNotation -> Bool
notaIsOperator NewNotation
nota
then [Char]
"operator"
else [Char]
"notation") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
(if NotationSection -> Bool
sectIsSection NotationSection
sect
then [Char]
" section"
else [Char]
"") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
(case NotationSection -> Maybe FixityLevel
sectLevel NotationSection
sect of
Maybe FixityLevel
Nothing -> [Char]
""
Just FixityLevel
Unrelated -> [Char]
", unrelated"
Just (Related PrecedenceLevel
l) -> [Char]
", level " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PrecedenceLevel -> [Char]
toStringWithoutDotZero PrecedenceLevel
l) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
")")
Box -> Box -> Box
Boxes.//
Box
strut
, Box
"["
Box -> Box -> Box
Boxes.<>
Alignment -> [Box] -> Box
forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
Boxes.vcat Alignment
Boxes.left
((Name -> Box) -> [Name] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> Name -> Box
prettyName Name
n Box -> Box -> Box
Boxes.<> Box
",") [Name]
names [Box] -> [Box] -> [Box]
forall a. [a] -> [a] -> [a]
++
[Name -> Box
prettyName Name
name Box -> Box -> Box
Boxes.<> Box
"]"])
)
where
nota :: NewNotation
nota = NotationSection -> NewNotation
sectNotation NotationSection
sect
section :: [NotationPart]
section = [Char] -> [NotationPart] -> [NotationPart]
qualifyFirstIdPart
((Name -> [Char] -> [Char]) -> [Char] -> [Name] -> [Char]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Name
x [Char]
s -> Name -> [Char]
C.nameToRawName Name
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"." [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s)
[Char]
""
(NonEmpty Name -> [Name]
forall a. NonEmpty a -> [a]
List1.init (QName -> NonEmpty Name
C.qnameParts (NewNotation -> QName
notaName NewNotation
nota))))
([NotationPart] -> [NotationPart]
spacesBetweenAdjacentIds ([NotationPart] -> [NotationPart])
-> [NotationPart] -> [NotationPart]
forall a b. (a -> b) -> a -> b
$
[NotationPart] -> [NotationPart]
trim (NewNotation -> [NotationPart]
notation NewNotation
nota))
qualifyFirstIdPart :: [Char] -> [NotationPart] -> [NotationPart]
qualifyFirstIdPart [Char]
_ [] = []
qualifyFirstIdPart [Char]
q (IdPart Ranged [Char]
x : [NotationPart]
ps) = Ranged [Char] -> NotationPart
IdPart (([Char] -> [Char]) -> Ranged [Char] -> Ranged [Char]
forall a b. (a -> b) -> Ranged a -> Ranged b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char]
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) Ranged [Char]
x) NotationPart -> [NotationPart] -> [NotationPart]
forall a. a -> [a] -> [a]
: [NotationPart]
ps
qualifyFirstIdPart [Char]
q (NotationPart
p : [NotationPart]
ps) = NotationPart
p NotationPart -> [NotationPart] -> [NotationPart]
forall a. a -> [a] -> [a]
: [Char] -> [NotationPart] -> [NotationPart]
qualifyFirstIdPart [Char]
q [NotationPart]
ps
spacesBetweenAdjacentIds :: [NotationPart] -> [NotationPart]
spacesBetweenAdjacentIds (IdPart Ranged [Char]
x : ps :: [NotationPart]
ps@(IdPart Ranged [Char]
_ : [NotationPart]
_)) =
Ranged [Char] -> NotationPart
IdPart Ranged [Char]
x NotationPart -> [NotationPart] -> [NotationPart]
forall a. a -> [a] -> [a]
: Ranged [Char] -> NotationPart
IdPart ([Char] -> Ranged [Char]
forall a. a -> Ranged a
unranged [Char]
" ") NotationPart -> [NotationPart] -> [NotationPart]
forall a. a -> [a] -> [a]
: [NotationPart] -> [NotationPart]
spacesBetweenAdjacentIds [NotationPart]
ps
spacesBetweenAdjacentIds (NotationPart
p : [NotationPart]
ps) =
NotationPart
p NotationPart -> [NotationPart] -> [NotationPart]
forall a. a -> [a] -> [a]
: [NotationPart] -> [NotationPart]
spacesBetweenAdjacentIds [NotationPart]
ps
spacesBetweenAdjacentIds [] = []
trim :: [NotationPart] -> [NotationPart]
trim = case NotationSection -> NotationKind
sectKind NotationSection
sect of
NotationKind
InfixNotation -> [NotationPart] -> [NotationPart]
trimLeft ([NotationPart] -> [NotationPart])
-> ([NotationPart] -> [NotationPart])
-> [NotationPart]
-> [NotationPart]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NotationPart] -> [NotationPart]
trimRight
NotationKind
PrefixNotation -> [NotationPart] -> [NotationPart]
trimRight
NotationKind
PostfixNotation -> [NotationPart] -> [NotationPart]
trimLeft
NotationKind
NonfixNotation -> [NotationPart] -> [NotationPart]
forall a. a -> a
id
NotationKind
NoNotation -> [NotationPart] -> [NotationPart]
forall a. HasCallStack => a
__IMPOSSIBLE__
([Name]
names, Name
name) = ([Name], Name) -> Maybe ([Name], Name) -> ([Name], Name)
forall a. a -> Maybe a -> a
fromMaybe ([Name], Name)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe ([Name], Name) -> ([Name], Name))
-> Maybe ([Name], Name) -> ([Name], Name)
forall a b. (a -> b) -> a -> b
$ [Name] -> Maybe ([Name], Name)
forall a. [a] -> Maybe ([a], a)
initLast ([Name] -> Maybe ([Name], Name)) -> [Name] -> Maybe ([Name], Name)
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
Set.toList (Set Name -> [Name]) -> Set Name -> [Name]
forall a b. (a -> b) -> a -> b
$ NewNotation -> Set Name
notaNames NewNotation
nota
strut :: Box
strut = Int -> Int -> Box
Boxes.emptyBox ([Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
names) Int
0
kind :: [Char]
kind = case NotationSection -> NotationKind
sectKind NotationSection
sect of
NotationKind
PrefixNotation -> [Char]
"prefix"
NotationKind
PostfixNotation -> [Char]
"postfix"
NotationKind
NonfixNotation -> [Char]
"closed"
NotationKind
NoNotation -> [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__
NotationKind
InfixNotation ->
case Fixity -> Associativity
fixityAssoc (Fixity -> Associativity) -> Fixity -> Associativity
forall a b. (a -> b) -> a -> b
$ NewNotation -> Fixity
notaFixity NewNotation
nota of
Associativity
NonAssoc -> [Char]
"infix"
Associativity
LeftAssoc -> [Char]
"infixl"
Associativity
RightAssoc -> [Char]
"infixr"
SplitError SplitError
e -> SplitError -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => SplitError -> m Doc
prettyTCM SplitError
e
ImpossibleConstructor QName
c NegativeUnification
neg -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"The case for 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is impossible" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [NegativeUnification -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NegativeUnification -> m Doc
prettyTCM NegativeUnification
neg] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible solution: remove the clause, or use an absurd pattern ()."
TooManyPolarities QName
x Int
n -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Too many polarities given in the POLARITY pragma for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"(at most" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"allowed)."
InstanceNoCandidate Type
t [(Term, TCErr)]
errs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"No instance 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"was found in scope."
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Term, TCErr) -> m Doc) -> [(Term, TCErr)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Term, TCErr) -> m Doc
forall {m :: * -> *} {a} {a}.
(MonadFresh NameId m, MonadInteractionPoints m,
MonadStConcreteNames m, PureTCM m, IsString (m Doc), Null (m Doc),
Semigroup (m Doc), PrettyTCM a, PrettyTCM a) =>
(a, a) -> m Doc
prCand [(Term, TCErr)]
errs ]
where
prCand :: (a, a) -> m Doc
prCand (a
term, a
err) =
[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"-" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+>
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
term m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"was ruled out because"
, a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM a
err ]
UnquoteFailed UnquoteError
e -> case UnquoteError
e of
BadVisibility [Char]
msg Arg Term
arg -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [Char]
"Unable to unquote the argument. It should be `" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"'."
ConInsteadOfDef QName
x [Char]
def [Char]
con -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"Use " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
con [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" instead of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
def [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" for 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]
DefInsteadOfCon QName
x [Char]
def [Char]
con -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"Use " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
def [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" instead of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
con [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" for non-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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x]
NonCanonical [Char]
kind Term
t ->
[Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char]
"Cannot unquote non-canonical " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
kind)
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 Int
2 (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t)
BlockedOnMeta TCState
_ Blocker
m -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [Char]
"Unquote failed because of unsolved meta variables."
UnquotePanic [Char]
err -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
DeBruijnIndexOutOfScope Int
i Telescope
EmptyTel [] -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [Char]
"de Bruijn index " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not in scope in the empty context"
DeBruijnIndexOutOfScope Int
i Telescope
cxt [Name]
names ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char]
"de Bruijn index " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not in scope in the context")
, m Doc -> m Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => [Char] -> m a -> m a
addContext ([Char]
"_" :: String) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Telescope -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Telescope -> m Doc
prettyTCM Telescope
cxt' ]
where
cxt' :: Telescope
cxt' = Telescope
cxt Telescope -> Telescope -> Telescope
forall t. Abstract t => Telescope -> t -> t
`abstract` Int -> Telescope -> Telescope
forall a. Subst a => Int -> a -> a
raise (Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
cxt) ([Name] -> Telescope
nameCxt [Name]
names)
nameCxt :: [Name] -> I.Telescope
nameCxt :: [Name] -> Telescope
nameCxt [] = Telescope
forall a. Tele a
EmptyTel
nameCxt (Name
x : [Name]
xs) = Dom Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel (Type -> Dom Type
forall a. a -> Dom a
defaultDom (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
HasCallStack => Sort
__DUMMY_SORT__ (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Term
I.var Int
0)) (Abs Telescope -> Telescope) -> Abs Telescope -> Telescope
forall a b. (a -> b) -> a -> b
$
[Char] -> Telescope -> Abs Telescope
forall a. [Char] -> a -> Abs a
NoAbs (Name -> [Char]
forall a. Pretty a => a -> [Char]
P.prettyShow Name
x) (Telescope -> Abs Telescope) -> Telescope -> Abs Telescope
forall a b. (a -> b) -> a -> b
$ [Name] -> Telescope
nameCxt [Name]
xs
TypeError
NeedOptionCopatterns -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Option --copatterns needed to enable destructor patterns"
TypeError
NeedOptionRewriting -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Option --rewriting needed to add and use rewrite rules"
TypeError
NeedOptionProp -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Universe Prop is disabled (use options --prop and --no-prop to enable/disable Prop)"
TypeError
NeedOptionTwoLevel -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Universe SSet is disabled (use option --two-level to enable SSet)"
GeneralizeNotSupportedHere QName
x -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char] -> [m Doc]) -> [Char] -> [m Doc]
forall a b. (a -> b) -> a -> b
$ [Char]
"Generalizable variable " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not supported here"
TypeError
GeneralizeCyclicDependency -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cyclic dependency between generalized variables"
TypeError
GeneralizeUnsolvedMeta -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Unsolved meta not generalized"
MultipleFixityDecls [(Name, [Fixity'])]
xs ->
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Multiple fixity or syntax declarations for"
, [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ ((Name, [Fixity']) -> m Doc) -> [(Name, [Fixity'])] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [Fixity']) -> m Doc
forall {m :: * -> *} {a} {a}.
(Semigroup (m Doc), Applicative m, IsString (m Doc), Pretty a,
Pretty a) =>
(a, [a]) -> m Doc
f [(Name, [Fixity'])]
xs
]
where
f :: (a, [a]) -> m Doc
f (a
x, [a]
fs) = (a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty a
x m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
": ") m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((a -> m Doc) -> [a] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [a]
fs)
MultiplePolarityPragmas [Name]
xs -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Multiple polarity pragmas for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ (Name -> m Doc) -> [Name] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Name]
xs
NonFatalErrors [TCWarning]
ws -> (m Doc -> m Doc -> m Doc) -> [m Doc] -> m Doc
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
($$) ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ (TCWarning -> m Doc) -> [TCWarning] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TCWarning -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TCWarning -> m Doc
prettyTCM [TCWarning]
ws
InstanceSearchDepthExhausted Term
c Type
a Int
d -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([Char]
"Instance search depth exhausted (max depth: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
d [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") for candidate") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[m Doc -> Int -> m Doc -> m Doc
forall (m :: * -> *).
Applicative m =>
m Doc -> Int -> m Doc -> m Doc
hang (Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
":") Int
2 (Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a)]
TriedToCopyConstrainedPrim QName
q -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot create a module containing a copy 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
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q]
SortOfSplitVarError Maybe Blocker
_ Doc
doc -> Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
doc
where
mpar :: a -> a -> m Doc -> m Doc
mpar a
n a
args
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
forall a. Null a => a -> Bool
null a
args) = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens
| Bool
otherwise = m Doc -> m Doc
forall a. a -> a
id
prettyArg :: MonadPretty m => Arg (I.Pattern' a) -> m Doc
prettyArg :: forall (m :: * -> *) a. MonadPretty m => Arg (Pattern' a) -> m Doc
prettyArg (Arg ArgInfo
info Pattern' a
x) = case ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info of
Hiding
Hidden -> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
braces (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Integer -> Pattern' a -> m Doc
forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
0 Pattern' a
x
Instance{} -> m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
dbraces (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Integer -> Pattern' a -> m Doc
forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
0 Pattern' a
x
Hiding
NotHidden -> Integer -> Pattern' a -> m Doc
forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
1 Pattern' a
x
prettyPat :: MonadPretty m => Integer -> (I.Pattern' a) -> m Doc
prettyPat :: forall (m :: * -> *) a.
MonadPretty m =>
Integer -> Pattern' a -> m Doc
prettyPat Integer
_ (I.VarP PatternInfo
_ a
_) = m Doc
"_"
prettyPat Integer
_ (I.DotP PatternInfo
_ Term
_) = m Doc
"._"
prettyPat Integer
n (I.ConP ConHead
c ConPatternInfo
_ [NamedArg (Pattern' a)]
args) =
Integer -> [NamedArg (Pattern' a)] -> m Doc -> m Doc
forall {a} {a} {m :: * -> *}.
(Ord a, Num a, Null a, Functor m) =>
a -> a -> m Doc -> m Doc
mpar Integer
n [NamedArg (Pattern' a)]
args (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
ConHead -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Arg (Pattern' a) -> m Doc
forall (m :: * -> *) a. MonadPretty m => Arg (Pattern' a) -> m Doc
prettyArg (Arg (Pattern' a) -> m Doc)
-> (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' a) -> Pattern' a
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
args)
prettyPat Integer
n (I.DefP PatternInfo
o QName
q [NamedArg (Pattern' a)]
args) =
Integer -> [NamedArg (Pattern' a)] -> m Doc -> m Doc
forall {a} {a} {m :: * -> *}.
(Ord a, Num a, Null a, Functor m) =>
a -> a -> m Doc -> m Doc
mpar Integer
n [NamedArg (Pattern' a)]
args (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$
QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ((NamedArg (Pattern' a) -> m Doc)
-> [NamedArg (Pattern' a)] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Arg (Pattern' a) -> m Doc
forall (m :: * -> *) a. MonadPretty m => Arg (Pattern' a) -> m Doc
prettyArg (Arg (Pattern' a) -> m Doc)
-> (NamedArg (Pattern' a) -> Arg (Pattern' a))
-> NamedArg (Pattern' a)
-> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a) -> Arg (Pattern' a)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' a) -> Pattern' a
forall name a. Named name a -> a
namedThing) [NamedArg (Pattern' a)]
args)
prettyPat Integer
_ (I.LitP PatternInfo
_ Literal
l) = Literal -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Literal -> m Doc
prettyTCM Literal
l
prettyPat Integer
_ (I.ProjP ProjOrigin
_ QName
p) = m Doc
"." m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
p
prettyPat Integer
_ (I.IApplyP PatternInfo
_ Term
_ Term
_ a
_) = m Doc
"_"
notCmp :: MonadPretty m => Comparison -> m Doc
notCmp :: forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
notCmp Comparison
cmp = m Doc
"!" m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> Comparison -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Comparison -> m Doc
prettyTCM Comparison
cmp
prettyInEqual :: MonadPretty m => Term -> Term -> m (Doc, Doc, Doc)
prettyInEqual :: forall (m :: * -> *).
MonadPretty m =>
Term -> Term -> m (Doc, Doc, Doc)
prettyInEqual Term
t1 Term
t2 = do
Doc
d1 <- Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t1
Doc
d2 <- Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
t2
(Doc
d1, Doc
d2,) (Doc -> (Doc, Doc, Doc)) -> m Doc -> m (Doc, Doc, Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
if Doc -> [Char]
P.render Doc
d1 [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= Doc -> [Char]
P.render Doc
d2 then m Doc
forall a. Null a => a
empty else do
(Term
v1, Term
v2) <- (Term, Term) -> m (Term, Term)
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Term
t1, Term
t2)
case (Term
v1, Term
v2) of
(I.Var Int
i1 Elims
_, I.Var Int
i2 Elims
_)
| Int
i1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i2 -> m Doc
forall (m :: * -> *). MonadPretty m => m Doc
generic
| Bool
otherwise -> Int -> Int -> m Doc
forall (m :: * -> *). MonadPretty m => Int -> Int -> m Doc
varVar Int
i1 Int
i2
(I.Def{}, I.Con{}) -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
(I.Con{}, I.Def{}) -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
(I.Var{}, I.Def{}) -> m Doc
forall (m :: * -> *). MonadPretty m => m Doc
varDef
(I.Def{}, I.Var{}) -> m Doc
forall (m :: * -> *). MonadPretty m => m Doc
varDef
(I.Var{}, I.Con{}) -> m Doc
forall (m :: * -> *). MonadPretty m => m Doc
varCon
(I.Con{}, I.Var{}) -> m Doc
forall (m :: * -> *). MonadPretty m => m Doc
varCon
(Term, Term)
_ -> m Doc
forall a. Null a => a
empty
where
varDef, varCon, generic :: MonadPretty m => m Doc
varDef :: forall (m :: * -> *). MonadPretty m => m Doc
varDef = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"because one is a variable and one a defined identifier"
varCon :: forall (m :: * -> *). MonadPretty m => m Doc
varCon = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords [Char]
"because one is a variable and one a constructor"
generic :: forall (m :: * -> *). MonadPretty m => m Doc
generic = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"although these terms are looking the same, " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
"they contain different but identically rendered identifiers somewhere"
varVar :: MonadPretty m => Int -> Int -> m Doc
varVar :: forall (m :: * -> *). MonadPretty m => Int -> Int -> m Doc
varVar Int
i Int
j = m Doc -> m Doc
forall (m :: * -> *). Functor m => m Doc -> m Doc
parens (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
fwords ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char]
"because one has de Bruijn index " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" and the other " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
j
class PrettyUnequal a where
prettyUnequal :: MonadPretty m => a -> m Doc -> a -> m Doc
instance PrettyUnequal Term where
prettyUnequal :: forall (m :: * -> *).
MonadPretty m =>
Term -> m Doc -> Term -> m Doc
prettyUnequal Term
t1 m Doc
ncmp Term
t2 = do
(Doc
d1, Doc
d2, Doc
d) <- Term -> Term -> m (Doc, Doc, Doc)
forall (m :: * -> *).
MonadPretty m =>
Term -> Term -> m (Doc, Doc, Doc)
prettyInEqual Term
t1 Term
t2
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d1 m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: m Doc
ncmp m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d2 m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: Doc -> m Doc
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
d m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
: []
instance PrettyUnequal I.Type where
prettyUnequal :: forall (m :: * -> *).
MonadPretty m =>
Type -> m Doc -> Type -> m Doc
prettyUnequal Type
t1 m Doc
ncmp Type
t2 = Term -> m Doc -> Term -> m Doc
forall a (m :: * -> *).
(PrettyUnequal a, MonadPretty m) =>
a -> m Doc -> a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
Term -> m Doc -> Term -> m Doc
prettyUnequal (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t1) m Doc
ncmp (Type -> Term
forall t a. Type'' t a -> a
unEl Type
t2)
instance PrettyTCM SplitError where
prettyTCM :: forall m. MonadPretty m => SplitError -> m Doc
prettyTCM :: forall (m :: * -> *). MonadPretty m => SplitError -> m Doc
prettyTCM SplitError
err = case SplitError
err of
NotADatatype Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot split on argument of non-datatype" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]
BlockedType Blocker
b Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot split on argument of unresolved 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]
ErasedDatatype Bool
causedByWithoutK Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot branch on erased argument of datatype" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
if Bool
causedByWithoutK
then [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because the K rule is turned off"
else []
CoinductiveDatatype Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \ Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot pattern match on the coinductive 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t]
UnificationStuck Maybe Blocker
b QName
c Telescope
tel Args
cIxs Args
gIxs [UnificationFailure]
errs
| Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
cIxs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
gIxs -> m Doc
forall a. HasCallStack => a
__IMPOSSIBLE__
| Bool
otherwise -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> m Doc) -> [[m Doc]] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ [ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> ([[m Doc]] -> [m Doc]) -> [[m Doc]] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[m Doc]] -> [m Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[m Doc]] -> m Doc) -> [[m Doc]] -> m Doc
forall a b. (a -> b) -> a -> b
$
[ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"I'm not sure if there should be a case for the constructor"
, [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
c m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
","]
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because I get stuck when trying to solve the following"
, [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"unification problems (inferred index ≟ expected index):"
]
]
, (Arg Term -> Arg Term -> m Doc) -> Args -> Args -> [m Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Arg Term -> Arg Term -> m Doc
prEq Args
cIxs Args
gIxs
, if [UnificationFailure] -> Bool
forall a. Null a => a -> Bool
null [UnificationFailure]
errs then [] else
[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ( [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Possible" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords ([UnificationFailure] -> [Char] -> [Char] -> [Char]
forall a c. Sized a => a -> c -> c -> c
P.singPlural [UnificationFailure]
errs [Char]
"reason" [Char]
"reasons") [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"why unification failed:" ) m Doc -> [m Doc] -> [m Doc]
forall a. a -> [a] -> [a]
:
(UnificationFailure -> m Doc) -> [UnificationFailure] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc)
-> (UnificationFailure -> m Doc) -> UnificationFailure -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UnificationFailure -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => UnificationFailure -> m Doc
prettyTCM) [UnificationFailure]
errs
]
where
prEq :: Arg Term -> Arg Term -> m Doc
prEq :: Arg Term -> Arg Term -> m Doc
prEq Arg Term
cIx Arg Term
gIx = Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep [ Arg Term -> m Doc
forall {f :: * -> *} {a}.
(PrettyTCM a, MonadFresh NameId f, MonadInteractionPoints f,
MonadStConcreteNames f, PureTCM f, IsString (f Doc), Null (f Doc),
Semigroup (f Doc)) =>
Arg a -> f Doc
pr Arg Term
cIx , m Doc
"≟" , Arg Term -> m Doc
forall {f :: * -> *} {a}.
(PrettyTCM a, MonadFresh NameId f, MonadInteractionPoints f,
MonadStConcreteNames f, PureTCM f, IsString (f Doc), Null (f Doc),
Semigroup (f Doc)) =>
Arg a -> f Doc
pr Arg Term
gIx ]
pr :: Arg a -> f Doc
pr Arg a
arg = Arg a -> Doc -> Doc
forall a. LensRelevance a => a -> Doc -> Doc
prettyRelevance Arg a
arg (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg a -> (Doc -> Doc) -> Doc -> Doc
forall a. LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
prettyHiding Arg a
arg Doc -> Doc
forall a. a -> a
id (Doc -> Doc) -> f Doc -> f Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => a -> m Doc
prettyTCM (Arg a -> a
forall e. Arg e -> e
unArg Arg a
arg)
SplitError
CosplitCatchall -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot split into projections because not all clauses have a projection copattern"
SplitError
CosplitNoTarget -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot split into projections because target type is unknown"
CosplitNoRecordType Closure Type
t -> Closure Type -> (Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure Type
t ((Type -> m Doc) -> m Doc) -> (Type -> m Doc) -> m Doc
forall a b. (a -> b) -> a -> b
$ \Type
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot split into projections because the target 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" is not a record type"
CannotCreateMissingClause QName
f (Telescope, [NamedArg DeBruijnPattern])
cl Doc
msg Closure (Abs Type)
t -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot generate inferred clause for" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
f m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Case to handle:") 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 Int
2 ([m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [(Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope, [NamedArg DeBruijnPattern])
cl])
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$ ((Doc -> m Doc
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Doc
msg m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Closure (Abs Type) -> (Abs Type -> m Doc) -> m Doc
forall (m :: * -> *) a c b.
(MonadTCEnv m, ReadTCState m, LensClosure a c) =>
c -> (a -> m b) -> m b
enterClosure Closure (Abs Type)
t Abs Type -> m Doc
displayAbs) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
".")
where
displayAbs :: Abs I.Type -> m Doc
displayAbs :: Abs Type -> m Doc
displayAbs (Abs [Char]
x Type
t) = [Char] -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a. MonadAddContext m => [Char] -> m a -> m a
addContext [Char]
x (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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
displayAbs (NoAbs [Char]
x Type
t) = Type -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
display :: (Telescope, [NamedArg DeBruijnPattern]) -> m Doc
display (Telescope
tel, [NamedArg DeBruijnPattern]
ps) = NamedClause -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => NamedClause -> m Doc
prettyTCM (NamedClause -> m Doc) -> NamedClause -> m Doc
forall a b. (a -> b) -> a -> b
$ QName -> Bool -> Clause -> NamedClause
NamedClause QName
f Bool
True (Clause -> NamedClause) -> Clause -> NamedClause
forall a b. (a -> b) -> a -> b
$
Clause
forall a. Null a => a
empty { clauseTel :: Telescope
clauseTel = Telescope
tel, namedClausePats :: [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps }
GenericSplitError [Char]
s -> [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Split failed:" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
s
instance PrettyTCM NegativeUnification where
prettyTCM :: forall (m :: * -> *). MonadPretty m => NegativeUnification -> m Doc
prettyTCM NegativeUnification
err = case NegativeUnification
err of
UnifyConflict Telescope
tel Term
u Term
v -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because unification ended with a conflicting equation "
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"≟" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
]
UnifyCycle Telescope
tel Int
i Term
u -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because unification ended with a cyclic equation "
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
i) m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"≟" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u
]
instance PrettyTCM UnificationFailure where
prettyTCM :: forall (m :: * -> *). MonadPretty m => UnificationFailure -> m Doc
prettyTCM UnificationFailure
err = case UnificationFailure
err of
UnifyIndicesNotVars Telescope
tel Type
a Term
u Term
v Args
ixs -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot apply injectivity to the equation" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"=" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because I cannot generalize over the indices" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[[m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
t (m Doc) -> m Doc
prettyList ((Arg Term -> m Doc) -> Args -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Args
ixs) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
"."]
UnifyRecursiveEq Telescope
tel Type
a Int
i Term
u -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot solve variable " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
i)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" 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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" with 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" because the variable occurs in the solution," [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
" or in the type of one of the variables in the solution."
UnifyReflexiveEq Telescope
tel Type
a Term
u -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot eliminate reflexive equation" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"=" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because K has been disabled."
UnifyUnusableModality Telescope
tel Type
a Int
i Term
u Modality
mod -> Telescope -> m Doc -> m Doc
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep ([m Doc] -> m Doc) -> [m Doc] -> m Doc
forall a b. (a -> b) -> a -> b
$
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Cannot solve variable " [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++ [Term -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Int -> Term
var Int
i)] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
a] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"with 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
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"because the solution cannot be used at" [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (Relevance -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Relevance -> [Char]) -> Relevance -> [Char]
forall a b. (a -> b) -> a -> b
$ Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod) m Doc -> m Doc -> m Doc
forall a. Semigroup a => a -> a -> a
<> m Doc
","
, [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text ([Char] -> m Doc) -> [Char] -> m Doc
forall a b. (a -> b) -> a -> b
$ Quantity -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize (Quantity -> [Char]) -> Quantity -> [Char]
forall a b. (a -> b) -> a -> b
$ Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod ] [m Doc] -> [m Doc] -> [m Doc]
forall a. [a] -> [a] -> [a]
++
[Char] -> [m Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"modality"
explainWhyInScope :: forall m. MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope :: forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope (WhyInScopeData QName
y [Char]
_ Maybe LocalVar
Nothing [] []) = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not in scope.")
explainWhyInScope (WhyInScopeData QName
y [Char]
_ Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms) = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is in scope as")
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [Maybe LocalVar -> [AbstractName] -> m Doc
variable Maybe LocalVar
v [AbstractName]
xs, [AbstractModule] -> m Doc
modules [AbstractModule]
ms]
]
where
variable :: Maybe LocalVar -> [AbstractName] -> m Doc
variable Maybe LocalVar
Nothing [AbstractName]
vs = [AbstractName] -> m Doc
names [AbstractName]
vs
variable (Just LocalVar
x) [AbstractName]
vs
| [AbstractName] -> Bool
forall a. Null a => a -> Bool
null [AbstractName]
vs = m Doc
asVar
| Bool
otherwise = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
[ [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ m Doc
asVar, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ LocalVar -> m Doc
shadowing LocalVar
x]
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ [AbstractName] -> m Doc
names [AbstractName]
vs
]
where
asVar :: m Doc
asVar :: m Doc
asVar = do
m Doc
"* a variable bound 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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ LocalVar -> Name
localVar LocalVar
x)
shadowing :: LocalVar -> m Doc
shadowing :: LocalVar -> m Doc
shadowing (LocalVar Name
_ BindingSource
_ []) = m Doc
"shadowing"
shadowing LocalVar
_ = m Doc
"in conflict with"
names :: [AbstractName] -> m Doc
names = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc)
-> ([AbstractName] -> [m Doc]) -> [AbstractName] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName -> m Doc) -> [AbstractName] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> m Doc
pName
modules :: [AbstractModule] -> m Doc
modules = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([m Doc] -> m Doc)
-> ([AbstractModule] -> [m Doc]) -> [AbstractModule] -> m Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractModule -> m Doc) -> [AbstractModule] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbstractModule -> m Doc
pMod
pKind :: KindOfName -> m Doc
pKind = \case
KindOfName
ConName -> m Doc
"constructor"
KindOfName
CoConName -> m Doc
"coinductive constructor"
KindOfName
FldName -> m Doc
"record field"
KindOfName
PatternSynName -> m Doc
"pattern synonym"
KindOfName
GeneralizeName -> m Doc
"generalizable variable"
KindOfName
DisallowedGeneralizeName -> m Doc
"generalizable variable from let open"
KindOfName
MacroName -> m Doc
"macro name"
KindOfName
QuotableName -> m Doc
"quotable name"
KindOfName
DataName -> m Doc
"data type"
KindOfName
RecName -> m Doc
"record type"
KindOfName
AxiomName -> m Doc
"postulate"
KindOfName
PrimName -> m Doc
"primitive function"
KindOfName
FunName -> m Doc
"defined name"
KindOfName
OtherDefName -> m Doc
"defined name"
pName :: AbstractName -> m Doc
pName :: AbstractName -> m Doc
pName AbstractName
a = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ m Doc
"* a"
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> KindOfName -> m Doc
pKind (AbstractName -> KindOfName
anameKind AbstractName
a)
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> [Char]) -> QName -> [Char]
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
a)
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
"brought into scope by"
] 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 Int
2 (Range -> WhyInScope -> m Doc
pWhy (Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName (QName -> Name) -> QName -> Name
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
a) (AbstractName -> WhyInScope
anameLineage AbstractName
a))
pMod :: AbstractModule -> m Doc
pMod :: AbstractModule -> m Doc
pMod AbstractModule
a = [m Doc] -> m Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
[ m Doc
"* a module" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text (ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (ModuleName -> [Char]) -> ModuleName -> [Char]
forall a b. (a -> b) -> a -> b
$ AbstractModule -> ModuleName
amodName AbstractModule
a)
, Int -> m Doc -> m Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ m Doc
"brought into scope by"
] 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 Int
2 (Range -> WhyInScope -> m Doc
pWhy (Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName (QName -> Name) -> QName -> Name
forall a b. (a -> b) -> a -> b
$ ModuleName -> QName
mnameToQName (ModuleName -> QName) -> ModuleName -> QName
forall a b. (a -> b) -> a -> b
$ AbstractModule -> ModuleName
amodName AbstractModule
a) (AbstractModule -> WhyInScope
amodLineage AbstractModule
a))
pWhy :: Range -> WhyInScope -> m Doc
pWhy :: Range -> WhyInScope -> m Doc
pWhy Range
r WhyInScope
Defined = m Doc
"- its definition 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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM Range
r
pWhy Range
r (Opened (C.QName Name
x) WhyInScope
w) | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x = Range -> WhyInScope -> m Doc
pWhy Range
r WhyInScope
w
pWhy Range
r (Opened QName
m WhyInScope
w) =
m Doc
"- the opening of"
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
m
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
m)
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
Range -> WhyInScope -> m Doc
pWhy Range
r WhyInScope
w
pWhy Range
r (Applied QName
m WhyInScope
w) =
m Doc
"- the application of"
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
m
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> m Doc
"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
forall (m :: * -> *). MonadPretty m => Range -> m Doc
prettyTCM (QName -> Range
forall a. HasRange a => a -> Range
getRange QName
m)
m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
$$
Range -> WhyInScope -> m Doc
pWhy Range
r WhyInScope
w
class Verbalize a where
verbalize :: a -> String
instance Verbalize Hiding where
verbalize :: Hiding -> [Char]
verbalize Hiding
h =
case Hiding
h of
Hiding
Hidden -> [Char]
"hidden"
Hiding
NotHidden -> [Char]
"visible"
Instance{} -> [Char]
"instance"
instance Verbalize Relevance where
verbalize :: Relevance -> [Char]
verbalize Relevance
r =
case Relevance
r of
Relevance
Relevant -> [Char]
"relevant"
Relevance
Irrelevant -> [Char]
"irrelevant"
Relevance
NonStrict -> [Char]
"shape-irrelevant"
instance Verbalize Quantity where
verbalize :: Quantity -> [Char]
verbalize = \case
Quantity0{} -> [Char]
"erased"
Quantity1{} -> [Char]
"linear"
Quantityω{} -> [Char]
"unrestricted"
instance Verbalize Cohesion where
verbalize :: Cohesion -> [Char]
verbalize Cohesion
r =
case Cohesion
r of
Cohesion
Flat -> [Char]
"flat"
Cohesion
Continuous -> [Char]
"continuous"
Cohesion
Squash -> [Char]
"squashed"
instance Verbalize Modality where
verbalize :: Modality -> [Char]
verbalize Modality
mod | Modality
mod Modality -> Modality -> Bool
forall a. Eq a => a -> a -> Bool
== Modality
defaultModality = [Char]
"default"
verbalize (Modality Relevance
rel Quantity
qnt Cohesion
coh) = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
[ Relevance -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize Relevance
rel | Relevance
rel Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Relevance
defaultRelevance ] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++
[ Quantity -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize Quantity
qnt | Quantity
qnt Quantity -> Quantity -> Bool
forall a. Eq a => a -> a -> Bool
/= Quantity
defaultQuantity ] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++
[ Cohesion -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize Cohesion
coh | Cohesion
coh Cohesion -> Cohesion -> Bool
forall a. Eq a => a -> a -> Bool
/= Cohesion
defaultCohesion ]
data Indefinite a = Indefinite a
instance Verbalize a => Verbalize (Indefinite a) where
verbalize :: Indefinite a -> [Char]
verbalize (Indefinite a
a) =
case a -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize a
a of
[Char]
"" -> [Char]
""
w :: [Char]
w@(Char
c:[Char]
cs) | Char
c Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
'a',Char
'e',Char
'i',Char
'o'] -> [Char]
"an " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
w
| Bool
otherwise -> [Char]
"a " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
w