module Agda.Interaction.Highlighting.Generate
( Level(..)
, generateAndPrintSyntaxInfo
, generateTokenInfo, generateTokenInfoFromSource
, generateTokenInfoFromString
, printSyntaxInfo
, printErrorInfo, errorHighlighting
, printUnsolvedInfo
, printHighlightingInfo
, highlightAsTypeChecked
, highlightWarning, warningHighlighting
, computeUnsolvedMetaWarnings
, computeUnsolvedConstraints
, storeDisambiguatedName, disambiguateRecordFields
) where
import Prelude hiding (null)
import Control.Monad
import Control.Arrow (second)
import Data.Generics.Geniplate
import qualified Data.Map as Map
import Data.Maybe
import Data.List ((\\))
import qualified Data.List as List
import qualified Data.Foldable as Fold (fold, foldMap, toList)
import qualified Data.IntMap as IntMap
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HMap
import Data.Sequence (Seq)
import qualified Data.Set as Set
import qualified Data.Text.Lazy as T
import Data.Void
import Agda.Interaction.Response
( Response( Resp_HighlightingInfo )
, RemoveTokenBasedHighlighting( KeepHighlighting )
)
import Agda.Interaction.Highlighting.Precise as P
import Agda.Interaction.Highlighting.Range (rToR, minus)
import qualified Agda.TypeChecking.Errors as E
import Agda.TypeChecking.MetaVars (isBlockedTerm)
import Agda.TypeChecking.Monad
hiding (ModuleInfo, MetaInfo, Primitive, Constructor, Record, Function, Datatype)
import qualified Agda.TypeChecking.Monad as M
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Warnings (runPM)
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Concrete (FieldAssignment'(..))
import Agda.Syntax.Concrete.Definitions as W ( DeclarationWarning(..) )
import qualified Agda.Syntax.Common as Common
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Info ( ModuleInfo(..), defMacro )
import qualified Agda.Syntax.Internal as I
import qualified Agda.Syntax.Literal as L
import qualified Agda.Syntax.Parser as Pa
import qualified Agda.Syntax.Parser.Tokens as T
import qualified Agda.Syntax.Position as P
import Agda.Syntax.Position (Range, HasRange, getRange, noRange)
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Impossible
data Level
= Full
| Partial
highlightWarning :: TCWarning -> TCM ()
highlightWarning :: TCWarning -> TCM ()
highlightWarning tcwarn :: TCWarning
tcwarn = do
let h :: CompressedFile
h = File -> CompressedFile
compress (File -> CompressedFile) -> File -> CompressedFile
forall a b. (a -> b) -> a -> b
$ TCWarning -> File
warningHighlighting TCWarning
tcwarn
Lens' CompressedFile TCState
-> (CompressedFile -> CompressedFile) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' CompressedFile TCState
stSyntaxInfo (CompressedFile
h CompressedFile -> CompressedFile -> CompressedFile
forall a. Semigroup a => a -> a -> a
<>)
HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting CompressedFile
h
generateAndPrintSyntaxInfo
:: A.Declaration
-> Level
-> Bool
-> TCM ()
generateAndPrintSyntaxInfo :: Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo decl :: Declaration
decl _ _ | Range -> Bool
forall a. Null a => a -> Bool
null (Range -> Bool) -> Range -> Bool
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall t. HasRange t => t -> Range
getRange Declaration
decl = () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
generateAndPrintSyntaxInfo decl :: Declaration
decl hlLevel :: Level
hlLevel updateState :: Bool
updateState = do
AbsolutePath
file <- TCMT IO AbsolutePath
forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
getCurrentPath
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "import.iface.create" 15 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$
"Generating syntax info for " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> VerboseKey
filePath AbsolutePath
file VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ ' ' Char -> VerboseKey -> VerboseKey
forall a. a -> [a] -> [a]
:
case Level
hlLevel of
Full {} -> "(final)"
Partial {} -> "(first approximation)"
VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ "."
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "highlighting.names" 60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "highlighting names = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [AmbiguousQName] -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow [AmbiguousQName]
names
TCM () -> TCM ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
M.ignoreAbstractMode (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
SourceToModule
modMap <- TCM SourceToModule
sourceToModule
NameKinds
kinds <- Level -> Declaration -> TCM NameKinds
nameKinds Level
hlLevel Declaration
decl
let nameInfo :: File
nameInfo = [File] -> File
forall a. Monoid a => [a] -> a
mconcat ([File] -> File) -> [File] -> File
forall a b. (a -> b) -> a -> b
$ (AmbiguousQName -> File) -> [AmbiguousQName] -> [File]
forall a b. (a -> b) -> [a] -> [b]
map (SourceToModule
-> AbsolutePath -> NameKinds -> AmbiguousQName -> File
generate SourceToModule
modMap AbsolutePath
file NameKinds
kinds) [AmbiguousQName]
names
File
constructorInfo <- case Level
hlLevel of
Full{} -> SourceToModule
-> AbsolutePath -> NameKinds -> Declaration -> TCM File
generateConstructorInfo SourceToModule
modMap AbsolutePath
file NameKinds
kinds Declaration
decl
_ -> File -> TCM File
forall (m :: * -> *) a. Monad m => a -> m a
return File
forall a. Monoid a => a
mempty
SrcFile
cm <- Range -> SrcFile
P.rangeFile (Range -> SrcFile) -> TCMT IO Range -> TCMT IO SrcFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' Range TCEnv -> TCMT IO Range
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Range TCEnv
eRange
VerboseKey -> VerboseLevel -> VerboseKey -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn "highlighting.warning" 60 (VerboseKey -> TCM ()) -> VerboseKey -> TCM ()
forall a b. (a -> b) -> a -> b
$ "current path = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ SrcFile -> VerboseKey
forall a. Show a => a -> VerboseKey
show SrcFile
cm
let (from :: VerboseLevel
from, to :: VerboseLevel
to) = case Range -> Maybe IntervalWithoutFile
forall a. Range' a -> Maybe IntervalWithoutFile
P.rangeToInterval (Declaration -> Range
forall t. HasRange t => t -> Range
getRange Declaration
decl) of
Nothing -> (VerboseLevel, VerboseLevel)
forall a. HasCallStack => a
__IMPOSSIBLE__
Just i :: IntervalWithoutFile
i -> ( Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> VerboseLevel) -> Int32 -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iStart IntervalWithoutFile
i
, Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> VerboseLevel) -> Int32 -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iEnd IntervalWithoutFile
i)
(prevTokens :: CompressedFile
prevTokens, (curTokens :: CompressedFile
curTokens, postTokens :: CompressedFile
postTokens)) <-
(CompressedFile -> (CompressedFile, CompressedFile))
-> (CompressedFile, CompressedFile)
-> (CompressedFile, (CompressedFile, CompressedFile))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (VerboseLevel -> CompressedFile -> (CompressedFile, CompressedFile)
splitAtC VerboseLevel
to) ((CompressedFile, CompressedFile)
-> (CompressedFile, (CompressedFile, CompressedFile)))
-> (CompressedFile -> (CompressedFile, CompressedFile))
-> CompressedFile
-> (CompressedFile, (CompressedFile, CompressedFile))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> CompressedFile -> (CompressedFile, CompressedFile)
splitAtC VerboseLevel
from (CompressedFile
-> (CompressedFile, (CompressedFile, CompressedFile)))
-> TCMT IO CompressedFile
-> TCMT IO (CompressedFile, (CompressedFile, CompressedFile))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' CompressedFile TCState -> TCMT IO CompressedFile
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' CompressedFile TCState
stTokens
let syntaxInfo :: CompressedFile
syntaxInfo = File -> CompressedFile
compress ([File] -> File
forall a. Monoid a => [a] -> a
mconcat [ File
constructorInfo
, SourceToModule -> AbsolutePath -> File
theRest SourceToModule
modMap AbsolutePath
file
, File
nameInfo
])
CompressedFile -> CompressedFile -> CompressedFile
forall a. Monoid a => a -> a -> a
`mappend`
CompressedFile
curTokens
Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
updateState (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
Lens' CompressedFile TCState
stSyntaxInfo Lens' CompressedFile TCState
-> (CompressedFile -> CompressedFile) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` CompressedFile -> CompressedFile -> CompressedFile
forall a. Monoid a => a -> a -> a
mappend CompressedFile
syntaxInfo
Lens' CompressedFile TCState
stTokens Lens' CompressedFile TCState -> CompressedFile -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` (CompressedFile
prevTokens CompressedFile -> CompressedFile -> CompressedFile
forall a. Monoid a => a -> a -> a
`mappend` CompressedFile
postTokens)
HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting CompressedFile
syntaxInfo
where
names :: [A.AmbiguousQName]
names :: [AmbiguousQName]
names =
((QName -> AmbiguousQName) -> [QName] -> [AmbiguousQName]
forall a b. (a -> b) -> [a] -> [b]
map QName -> AmbiguousQName
I.unambiguous ([QName] -> [AmbiguousQName]) -> [QName] -> [AmbiguousQName]
forall a b. (a -> b) -> a -> b
$
(QName -> Bool) -> [QName] -> [QName]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (QName -> Bool) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Bool
isExtendedLambdaName) ([QName] -> [QName]) -> [QName] -> [QName]
forall a b. (a -> b) -> a -> b
$
Declaration -> [QName]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl) [AmbiguousQName] -> [AmbiguousQName] -> [AmbiguousQName]
forall a. [a] -> [a] -> [a]
++
Declaration -> [AmbiguousQName]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
theRest :: SourceToModule -> AbsolutePath -> File
theRest :: SourceToModule -> AbsolutePath -> File
theRest modMap :: SourceToModule
modMap file :: AbsolutePath
file = [File] -> File
forall a. Monoid a => [a] -> a
mconcat
[ (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
getFieldDecl ([Declaration] -> File) -> [Declaration] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (Expr -> File) -> [Expr] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Expr -> File
getVarAndField ([Expr] -> File) -> [Expr] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Expr]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (LetBinding -> File) -> [LetBinding] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap LetBinding -> File
getLet ([LetBinding] -> File) -> [LetBinding] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [LetBinding]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (LamBinding -> File) -> [LamBinding] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap LamBinding -> File
getLam ([LamBinding] -> File) -> [LamBinding] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [LamBinding]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (TypedBinding -> File) -> [TypedBinding] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap TypedBinding -> File
getTyped ([TypedBinding] -> File) -> [TypedBinding] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [TypedBinding]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (Pattern -> File) -> [Pattern] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Pattern -> File
getPattern ([Pattern] -> File) -> [Pattern] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Pattern]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (Pattern' Void -> File) -> [Pattern' Void] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Pattern' Void -> File
getPatternSyn ([Pattern' Void] -> File) -> [Pattern' Void] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Pattern' Void]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (Expr -> File) -> [Expr] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Expr -> File
getExpr ([Expr] -> File) -> [Expr] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Expr]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
getPatSynArgs ([Declaration] -> File) -> [Declaration] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (ModuleName -> File) -> [ModuleName] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap ModuleName -> File
getModuleName ([ModuleName] -> File) -> [ModuleName] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [ModuleName]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (ModuleInfo -> File) -> [ModuleInfo] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap ModuleInfo -> File
getModuleInfo ([ModuleInfo] -> File) -> [ModuleInfo] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [ModuleInfo]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (NamedArg Expr -> File) -> [NamedArg Expr] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap NamedArg Expr -> File
getNamedArgE ([NamedArg Expr] -> File) -> [NamedArg Expr] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [NamedArg Expr]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (NamedArg Pattern -> File) -> [NamedArg Pattern] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap NamedArg Pattern -> File
getNamedArgP ([NamedArg Pattern] -> File) -> [NamedArg Pattern] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [NamedArg Pattern]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (NamedArg BindName -> File) -> [NamedArg BindName] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap NamedArg BindName -> File
getNamedArgB ([NamedArg BindName] -> File) -> [NamedArg BindName] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [NamedArg BindName]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (NamedArg LHSCore -> File) -> [NamedArg LHSCore] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap NamedArg LHSCore -> File
getNamedArgL ([NamedArg LHSCore] -> File) -> [NamedArg LHSCore] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [NamedArg LHSCore]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (Quantity -> File) -> [Quantity] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Quantity -> File
getQuantityAttr([Quantity] -> File) -> [Quantity] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Quantity]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
, (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
getPragma ([Declaration] -> File) -> [Declaration] -> File
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
]
where
bound :: BindName -> File
bound A.BindName{ unBind :: BindName -> Name
unBind = Name
n } =
SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file [] (Name -> Name
A.nameConcrete Name
n) Range
forall a. Range' a
noRange
(\isOp :: Bool
isOp -> Aspects
parserBased { aspect :: Maybe Aspect
aspect =
Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Bound) Bool
isOp })
(Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Name -> Range
A.nameBindingSite Name
n)
patsyn :: AmbiguousQName -> File
patsyn n :: AmbiguousQName
n =
SourceToModule
-> AbsolutePath -> QName -> Bool -> (Bool -> Aspects) -> File
nameToFileA SourceToModule
modMap AbsolutePath
file (AmbiguousQName -> QName
I.headAmbQ AmbiguousQName
n) Bool
True ((Bool -> Aspects) -> File) -> (Bool -> Aspects) -> File
forall a b. (a -> b) -> a -> b
$ \isOp :: Bool
isOp ->
Aspects
parserBased { aspect :: Maybe Aspect
aspect =
Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just (NameKind -> Maybe NameKind) -> NameKind -> Maybe NameKind
forall a b. (a -> b) -> a -> b
$ Induction -> NameKind
Constructor Induction
Common.Inductive) Bool
isOp }
macro :: QName -> File
macro n :: QName
n = SourceToModule
-> AbsolutePath -> QName -> Bool -> (Bool -> Aspects) -> File
nameToFileA SourceToModule
modMap AbsolutePath
file QName
n Bool
True ((Bool -> Aspects) -> File) -> (Bool -> Aspects) -> File
forall a b. (a -> b) -> a -> b
$ \isOp :: Bool
isOp ->
Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Macro) Bool
isOp }
field :: [C.Name] -> C.Name -> File
field :: [Name] -> Name -> File
field m :: [Name]
m n :: Name
n = SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file [Name]
m Name
n Range
forall a. Range' a
noRange
(\isOp :: Bool
isOp -> Aspects
parserBased { aspect :: Maybe Aspect
aspect =
Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Field) Bool
isOp })
Maybe Range
forall a. Maybe a
Nothing
asName :: C.Name -> File
asName :: Name -> File
asName n :: Name
n = SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file []
Name
n Range
forall a. Range' a
noRange
(\isOp :: Bool
isOp -> Aspects
parserBased { aspect :: Maybe Aspect
aspect =
Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Module) Bool
isOp })
Maybe Range
forall a. Maybe a
Nothing
mod :: Bool -> Name -> File
mod isTopLevelModule :: Bool
isTopLevelModule n :: Name
n =
SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap AbsolutePath
file []
(Name -> Name
A.nameConcrete Name
n) Range
forall a. Range' a
noRange
(\isOp :: Bool
isOp -> Aspects
parserBased { aspect :: Maybe Aspect
aspect =
Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Module) Bool
isOp })
(Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Bool -> (Range -> Range) -> Range -> Range
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
isTopLevelModule Range -> Range
P.beginningOfFile (Range -> Range) -> Range -> Range
forall a b. (a -> b) -> a -> b
$
Name -> Range
A.nameBindingSite Name
n)
getVarAndField :: A.Expr -> File
getVarAndField :: Expr -> File
getVarAndField (A.Var x :: Name
x) = BindName -> File
bound (BindName -> File) -> BindName -> File
forall a b. (a -> b) -> a -> b
$ Name -> BindName
A.mkBindName Name
x
getVarAndField (A.Rec _ fs :: RecordAssigns
fs) = [File] -> File
forall a. Monoid a => [a] -> a
mconcat [ [Name] -> Name -> File
field [] Name
x | Left (FieldAssignment x :: Name
x _) <- RecordAssigns
fs ]
getVarAndField (A.RecUpdate _ _ fs :: Assigns
fs) = [File] -> File
forall a. Monoid a => [a] -> a
mconcat [ [Name] -> Name -> File
field [] Name
x | (FieldAssignment x :: Name
x _) <- Assigns
fs ]
getVarAndField _ = File
forall a. Monoid a => a
mempty
getNamedArgE :: Common.NamedArg A.Expr -> File
getNamedArgE :: NamedArg Expr -> File
getNamedArgE = NamedArg Expr -> File
forall a. NamedArg a -> File
getNamedArg
getNamedArgP :: Common.NamedArg A.Pattern -> File
getNamedArgP :: NamedArg Pattern -> File
getNamedArgP = NamedArg Pattern -> File
forall a. NamedArg a -> File
getNamedArg
getNamedArgB :: Common.NamedArg A.BindName -> File
getNamedArgB :: NamedArg BindName -> File
getNamedArgB = NamedArg BindName -> File
forall a. NamedArg a -> File
getNamedArg
getNamedArgL :: Common.NamedArg A.LHSCore -> File
getNamedArgL :: NamedArg LHSCore -> File
getNamedArgL = NamedArg LHSCore -> File
forall a. NamedArg a -> File
getNamedArg
getNamedArg :: Common.NamedArg a -> File
getNamedArg :: NamedArg a -> File
getNamedArg x :: NamedArg a
x = Maybe NamedName -> File -> (NamedName -> File) -> File
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe (Named NamedName a -> Maybe NamedName
forall name a. Named name a -> Maybe name
Common.nameOf (Named NamedName a -> Maybe NamedName)
-> Named NamedName a -> Maybe NamedName
forall a b. (a -> b) -> a -> b
$ NamedArg a -> Named NamedName a
forall e. Arg e -> e
Common.unArg NamedArg a
x) File
forall a. Monoid a => a
mempty ((NamedName -> File) -> File) -> (NamedName -> File) -> File
forall a b. (a -> b) -> a -> b
$ \ s :: NamedName
s ->
Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ NamedName -> Range
forall t. HasRange t => t -> Range
getRange NamedName
s) (Aspects -> File) -> Aspects -> File
forall a b. (a -> b) -> a -> b
$
Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Argument) Bool
False }
getBinder :: A.Binder -> File
getBinder :: Binder -> File
getBinder (A.Binder _ n :: BindName
n) = BindName -> File
bound BindName
n
getLet :: A.LetBinding -> File
getLet :: LetBinding -> File
getLet (A.LetBind _ _ x :: BindName
x _ _) = BindName -> File
bound BindName
x
getLet A.LetPatBind{} = File
forall a. Monoid a => a
mempty
getLet A.LetApply{} = File
forall a. Monoid a => a
mempty
getLet A.LetOpen{} = File
forall a. Monoid a => a
mempty
getLet (A.LetDeclaredVariable x :: BindName
x) = BindName -> File
bound BindName
x
getLam :: A.LamBinding -> File
getLam :: LamBinding -> File
getLam (A.DomainFree _ xs :: NamedArg Binder
xs) = Binder -> File
getBinder (NamedArg Binder -> Binder
forall a. NamedArg a -> a
Common.namedArg NamedArg Binder
xs)
getLam (A.DomainFull {}) = File
forall a. Monoid a => a
mempty
getTyped :: A.TypedBinding -> File
getTyped :: TypedBinding -> File
getTyped (A.TBind _ _ xs :: [NamedArg Binder]
xs _) = (NamedArg Binder -> File) -> [NamedArg Binder] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (Binder -> File
getBinder (Binder -> File)
-> (NamedArg Binder -> Binder) -> NamedArg Binder -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Binder -> Binder
forall a. NamedArg a -> a
Common.namedArg) [NamedArg Binder]
xs
getTyped A.TLet{} = File
forall a. Monoid a => a
mempty
getPatSynArgs :: A.Declaration -> File
getPatSynArgs :: Declaration -> File
getPatSynArgs (A.PatternSynDef _ xs :: [Arg Name]
xs _) = [File] -> File
forall a. Monoid a => [a] -> a
mconcat ([File] -> File) -> [File] -> File
forall a b. (a -> b) -> a -> b
$ (Arg Name -> File) -> [Arg Name] -> [File]
forall a b. (a -> b) -> [a] -> [b]
map (BindName -> File
bound (BindName -> File) -> (Arg Name -> BindName) -> Arg Name -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> BindName
A.mkBindName (Name -> BindName) -> (Arg Name -> Name) -> Arg Name -> BindName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Name -> Name
forall e. Arg e -> e
Common.unArg) [Arg Name]
xs
getPatSynArgs _ = File
forall a. Monoid a => a
mempty
getPragma :: A.Declaration -> File
getPragma :: Declaration -> File
getPragma = \case
A.Pragma _ p :: Pragma
p ->
case Pragma
p of
A.BuiltinPragma b :: RString
b _ -> RString -> File
forall a. HasRange a => a -> File
keyword RString
b
A.BuiltinNoDefPragma b :: RString
b _ -> RString -> File
forall a. HasRange a => a -> File
keyword RString
b
A.CompilePragma b :: RString
b _ _ -> RString -> File
forall a. HasRange a => a -> File
keyword RString
b
A.RewritePragma r :: Range
r _ -> Range -> File
forall a. HasRange a => a -> File
keyword Range
r
A.OptionsPragma{} -> File
forall a. Monoid a => a
mempty
A.StaticPragma{} -> File
forall a. Monoid a => a
mempty
A.EtaPragma{} -> File
forall a. Monoid a => a
mempty
A.InjectivePragma{} -> File
forall a. Monoid a => a
mempty
A.InlinePragma{} -> File
forall a. Monoid a => a
mempty
A.DisplayPragma{} -> File
forall a. Monoid a => a
mempty
_ -> File
forall a. Monoid a => a
mempty
keyword :: HasRange a => a -> File
keyword :: a -> File
keyword x :: a
x = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ a -> Range
forall t. HasRange t => t -> Range
getRange a
x) (Aspects -> File) -> Aspects -> File
forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Keyword }
getPattern' :: IsProjP e => A.Pattern' e -> File
getPattern' :: Pattern' e -> File
getPattern' (A.VarP x :: BindName
x) = BindName -> File
bound BindName
x
getPattern' (A.AsP _ x :: BindName
x _) = BindName -> File
bound BindName
x
getPattern' (A.DotP pi :: PatInfo
pi e :: e
e)
| Just _ <- e -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP e
e = File
forall a. Monoid a => a
mempty
| Bool
otherwise =
Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ PatInfo -> Range
forall t. HasRange t => t -> Range
getRange PatInfo
pi)
(Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
DottedPattern })
getPattern' (A.PatternSynP _ q :: AmbiguousQName
q _) = AmbiguousQName -> File
patsyn AmbiguousQName
q
getPattern' (A.RecP _ fs :: [FieldAssignment' (Pattern' e)]
fs) = [File] -> File
forall a. Monoid a => [a] -> a
mconcat [ [Name] -> Name -> File
field [] Name
x | FieldAssignment x :: Name
x _ <- [FieldAssignment' (Pattern' e)]
fs ]
getPattern' _ = File
forall a. Monoid a => a
mempty
getPattern :: A.Pattern -> File
getPattern :: Pattern -> File
getPattern = Pattern -> File
forall e. IsProjP e => Pattern' e -> File
getPattern'
getPatternSyn :: A.Pattern' Void -> File
getPatternSyn :: Pattern' Void -> File
getPatternSyn = Pattern' Void -> File
forall e. IsProjP e => Pattern' e -> File
getPattern'
getExpr :: A.Expr -> File
getExpr :: Expr -> File
getExpr (A.PatternSyn q :: AmbiguousQName
q) = AmbiguousQName -> File
patsyn AmbiguousQName
q
getExpr (A.Macro q :: QName
q) = QName -> File
macro QName
q
getExpr _ = File
forall a. Monoid a => a
mempty
getFieldDecl :: A.Declaration -> File
getFieldDecl :: Declaration -> File
getFieldDecl (A.RecDef _ _ _ _ _ _ _ _ fs :: [Declaration]
fs) = (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
extractField [Declaration]
fs
where
extractField :: Declaration -> File
extractField (A.ScopedDecl _ ds :: [Declaration]
ds) = (Declaration -> File) -> [Declaration] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Declaration -> File
extractField [Declaration]
ds
extractField (A.Field _ x :: QName
x _) = [Name] -> Name -> File
field (QName -> [Name]
concreteQualifier QName
x)
(QName -> Name
concreteBase QName
x)
extractField _ = File
forall a. Monoid a => a
mempty
getFieldDecl _ = File
forall a. Monoid a => a
mempty
getModuleName :: A.ModuleName -> File
getModuleName :: ModuleName -> File
getModuleName m :: ModuleName
m@(A.MName { mnameToList :: ModuleName -> [Name]
A.mnameToList = [Name]
xs }) =
[File] -> File
forall a. Monoid a => [a] -> a
mconcat ([File] -> File) -> [File] -> File
forall a b. (a -> b) -> a -> b
$ (Name -> File) -> [Name] -> [File]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Name -> File
mod Bool
isTopLevelModule) [Name]
xs
where
isTopLevelModule :: Bool
isTopLevelModule =
case (Name -> Maybe AbsolutePath) -> [Name] -> [AbsolutePath]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Maybe AbsolutePath) -> Maybe AbsolutePath
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Maybe (Maybe AbsolutePath) -> Maybe AbsolutePath)
-> (Name -> Maybe (Maybe AbsolutePath))
-> Name
-> Maybe AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(Position' SrcFile -> Maybe AbsolutePath)
-> Maybe (Position' SrcFile) -> Maybe (Maybe AbsolutePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SrcFile -> Maybe AbsolutePath
forall a. Maybe a -> Maybe a
Strict.toLazy (SrcFile -> Maybe AbsolutePath)
-> (Position' SrcFile -> SrcFile)
-> Position' SrcFile
-> Maybe AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position' SrcFile -> SrcFile
forall a. Position' a -> a
P.srcFile) (Maybe (Position' SrcFile) -> Maybe (Maybe AbsolutePath))
-> (Name -> Maybe (Position' SrcFile))
-> Name
-> Maybe (Maybe AbsolutePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
P.rStart (Range -> Maybe (Position' SrcFile))
-> (Name -> Range) -> Name -> Maybe (Position' SrcFile)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Name -> Range
A.nameBindingSite) [Name]
xs of
f :: AbsolutePath
f : _ -> AbsolutePath -> SourceToModule -> Maybe TopLevelModuleName
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AbsolutePath
f SourceToModule
modMap Maybe TopLevelModuleName -> Maybe TopLevelModuleName -> Bool
forall a. Eq a => a -> a -> Bool
==
TopLevelModuleName -> Maybe TopLevelModuleName
forall a. a -> Maybe a
Just (QName -> TopLevelModuleName
C.toTopLevelModuleName (QName -> TopLevelModuleName) -> QName -> TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ ModuleName -> QName
A.mnameToConcrete ModuleName
m)
[] -> Bool
False
getModuleInfo :: ModuleInfo -> File
getModuleInfo :: ModuleInfo -> File
getModuleInfo (ModuleInfo{ Range
minfoAsTo :: ModuleInfo -> Range
minfoAsTo :: Range
minfoAsTo, Maybe Name
minfoAsName :: ModuleInfo -> Maybe Name
minfoAsName :: Maybe Name
minfoAsName }) =
Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR Range
minfoAsTo) (Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Symbol })
File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend`
File -> (Name -> File) -> Maybe Name -> File
forall b a. b -> (a -> b) -> Maybe a -> b
maybe File
forall a. Monoid a => a
mempty Name -> File
asName Maybe Name
minfoAsName
getQuantityAttr :: Common.Quantity -> File
getQuantityAttr :: Quantity -> File
getQuantityAttr q :: Quantity
q = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Quantity -> Range
forall t. HasRange t => t -> Range
getRange Quantity
q) (Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
Symbol })
generateTokenInfo :: AbsolutePath -> TCM CompressedFile
generateTokenInfo :: AbsolutePath -> TCMT IO CompressedFile
generateTokenInfo file :: AbsolutePath
file =
AbsolutePath -> VerboseKey -> TCMT IO CompressedFile
generateTokenInfoFromSource AbsolutePath
file (VerboseKey -> TCMT IO CompressedFile)
-> (Text -> VerboseKey) -> Text -> TCMT IO CompressedFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> VerboseKey
T.unpack (Text -> TCMT IO CompressedFile)
-> TCMT IO Text -> TCMT IO CompressedFile
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
PM Text -> TCMT IO Text
forall a. PM a -> TCM a
runPM (AbsolutePath -> PM Text
Pa.readFilePM AbsolutePath
file)
generateTokenInfoFromSource
:: AbsolutePath
-> String
-> TCM CompressedFile
generateTokenInfoFromSource :: AbsolutePath -> VerboseKey -> TCMT IO CompressedFile
generateTokenInfoFromSource file :: AbsolutePath
file input :: VerboseKey
input =
PM CompressedFile -> TCMT IO CompressedFile
forall a. PM a -> TCM a
runPM (PM CompressedFile -> TCMT IO CompressedFile)
-> PM CompressedFile -> TCMT IO CompressedFile
forall a b. (a -> b) -> a -> b
$ [Token] -> CompressedFile
tokenHighlighting ([Token] -> CompressedFile)
-> (([Token], FileType) -> [Token])
-> ([Token], FileType)
-> CompressedFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Token], FileType) -> [Token]
forall a b. (a, b) -> a
fst (([Token], FileType) -> CompressedFile)
-> PM ([Token], FileType) -> PM CompressedFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Token]
-> AbsolutePath -> VerboseKey -> PM ([Token], FileType)
forall a.
Show a =>
Parser a -> AbsolutePath -> VerboseKey -> PM (a, FileType)
Pa.parseFile Parser [Token]
Pa.tokensParser AbsolutePath
file VerboseKey
input
generateTokenInfoFromString :: Range -> String -> TCM CompressedFile
generateTokenInfoFromString :: Range -> VerboseKey -> TCMT IO CompressedFile
generateTokenInfoFromString r :: Range
r _ | Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
forall a. Range' a
noRange = CompressedFile -> TCMT IO CompressedFile
forall (m :: * -> *) a. Monad m => a -> m a
return CompressedFile
forall a. Monoid a => a
mempty
generateTokenInfoFromString r :: Range
r s :: VerboseKey
s = do
PM CompressedFile -> TCMT IO CompressedFile
forall a. PM a -> TCM a
runPM (PM CompressedFile -> TCMT IO CompressedFile)
-> PM CompressedFile -> TCMT IO CompressedFile
forall a b. (a -> b) -> a -> b
$ [Token] -> CompressedFile
tokenHighlighting ([Token] -> CompressedFile) -> PM [Token] -> PM CompressedFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Token] -> Position' SrcFile -> VerboseKey -> PM [Token]
forall a. Parser a -> Position' SrcFile -> VerboseKey -> PM a
Pa.parsePosString Parser [Token]
Pa.tokensParser Position' SrcFile
p VerboseKey
s
where
Just p :: Position' SrcFile
p = Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
P.rStart Range
r
tokenHighlighting :: [T.Token] -> CompressedFile
tokenHighlighting :: [Token] -> CompressedFile
tokenHighlighting = [CompressedFile] -> CompressedFile
merge ([CompressedFile] -> CompressedFile)
-> ([Token] -> [CompressedFile]) -> [Token] -> CompressedFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token -> CompressedFile) -> [Token] -> [CompressedFile]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CompressedFile
tokenToCFile
where
aToF :: Aspect -> Range -> CompressedFile
aToF a :: Aspect
a r :: Range
r = Ranges -> Aspects -> CompressedFile
singletonC (Range -> Ranges
rToR Range
r) (Aspects
forall a. Monoid a => a
mempty { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just Aspect
a })
merge :: [CompressedFile] -> CompressedFile
merge = [(Range, Aspects)] -> CompressedFile
CompressedFile ([(Range, Aspects)] -> CompressedFile)
-> ([CompressedFile] -> [(Range, Aspects)])
-> [CompressedFile]
-> CompressedFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Range, Aspects)]] -> [(Range, Aspects)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Range, Aspects)]] -> [(Range, Aspects)])
-> ([CompressedFile] -> [[(Range, Aspects)]])
-> [CompressedFile]
-> [(Range, Aspects)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CompressedFile -> [(Range, Aspects)])
-> [CompressedFile] -> [[(Range, Aspects)]]
forall a b. (a -> b) -> [a] -> [b]
map CompressedFile -> [(Range, Aspects)]
ranges
tokenToCFile :: T.Token -> CompressedFile
tokenToCFile :: Token -> CompressedFile
tokenToCFile (T.TokSetN (i :: Interval
i, _)) = Aspect -> Range -> CompressedFile
aToF Aspect
PrimitiveType (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokPropN (i :: Interval
i, _)) = Aspect -> Range -> CompressedFile
aToF Aspect
PrimitiveType (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokKeyword T.KwSet i :: Interval
i) = Aspect -> Range -> CompressedFile
aToF Aspect
PrimitiveType (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokKeyword T.KwProp i :: Interval
i) = Aspect -> Range -> CompressedFile
aToF Aspect
PrimitiveType (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokKeyword T.KwForall i :: Interval
i) = Aspect -> Range -> CompressedFile
aToF Aspect
Symbol (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokKeyword T.KwREWRITE _) = CompressedFile
forall a. Monoid a => a
mempty
tokenToCFile (T.TokKeyword _ i :: Interval
i) = Aspect -> Range -> CompressedFile
aToF Aspect
Keyword (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokSymbol _ i :: Interval
i) = Aspect -> Range -> CompressedFile
aToF Aspect
Symbol (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokLiteral (L.LitNat r :: Range
r _)) = Aspect -> Range -> CompressedFile
aToF Aspect
Number Range
r
tokenToCFile (T.TokLiteral (L.LitWord64 r :: Range
r _)) = Aspect -> Range -> CompressedFile
aToF Aspect
Number Range
r
tokenToCFile (T.TokLiteral (L.LitFloat r :: Range
r _)) = Aspect -> Range -> CompressedFile
aToF Aspect
Number Range
r
tokenToCFile (T.TokLiteral (L.LitString r :: Range
r _)) = Aspect -> Range -> CompressedFile
aToF Aspect
String Range
r
tokenToCFile (T.TokLiteral (L.LitChar r :: Range
r _)) = Aspect -> Range -> CompressedFile
aToF Aspect
String Range
r
tokenToCFile (T.TokLiteral (L.LitQName r :: Range
r _)) = Aspect -> Range -> CompressedFile
aToF Aspect
String Range
r
tokenToCFile (T.TokLiteral (L.LitMeta r :: Range
r _ _)) = Aspect -> Range -> CompressedFile
aToF Aspect
String Range
r
tokenToCFile (T.TokComment (i :: Interval
i, _)) = Aspect -> Range -> CompressedFile
aToF Aspect
Comment (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokTeX (i :: Interval
i, _)) = Aspect -> Range -> CompressedFile
aToF Aspect
Background (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokMarkup (i :: Interval
i, _)) = Aspect -> Range -> CompressedFile
aToF Aspect
Markup (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokId {}) = CompressedFile
forall a. Monoid a => a
mempty
tokenToCFile (T.TokQId {}) = CompressedFile
forall a. Monoid a => a
mempty
tokenToCFile (T.TokString (i :: Interval
i,s :: VerboseKey
s)) = Aspect -> Range -> CompressedFile
aToF Aspect
Pragma (Interval -> Range
forall t. HasRange t => t -> Range
getRange Interval
i)
tokenToCFile (T.TokDummy {}) = CompressedFile
forall a. Monoid a => a
mempty
tokenToCFile (T.TokEOF {}) = CompressedFile
forall a. Monoid a => a
mempty
type NameKinds = A.QName -> Maybe NameKind
nameKinds :: Level
-> A.Declaration
-> TCM NameKinds
nameKinds :: Level -> Declaration -> TCM NameKinds
nameKinds hlLevel :: Level
hlLevel decl :: Declaration
decl = do
HashMap QName Definition
imported <- Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC (Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition))
-> Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall a b. (a -> b) -> a -> b
$ (Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stImports ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions
HashMap QName Definition
local <- case Level
hlLevel of
Full{} -> Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC (Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition))
-> Lens' (HashMap QName Definition) TCState
-> TCMT IO (HashMap QName Definition)
forall a b. (a -> b) -> a -> b
$ (Signature -> f Signature) -> TCState -> f TCState
Lens' Signature TCState
stSignature ((Signature -> f Signature) -> TCState -> f TCState)
-> ((HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature)
-> (HashMap QName Definition -> f (HashMap QName Definition))
-> TCState
-> f TCState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName Definition -> f (HashMap QName Definition))
-> Signature -> f Signature
Lens' (HashMap QName Definition) Signature
sigDefinitions
_ -> HashMap QName Definition -> TCMT IO (HashMap QName Definition)
forall (m :: * -> *) a. Monad m => a -> m a
return HashMap QName Definition
forall k v. HashMap k v
HMap.empty
Map QName PatternSynDefn
impPatSyns <- Lens' (Map QName PatternSynDefn) TCState
-> TCMT IO (Map QName PatternSynDefn)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName PatternSynDefn) TCState
stPatternSynImports
Map QName PatternSynDefn
locPatSyns <- case Level
hlLevel of
Full{} -> Lens' (Map QName PatternSynDefn) TCState
-> TCMT IO (Map QName PatternSynDefn)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Map QName PatternSynDefn) TCState
stPatternSyns
_ -> Map QName PatternSynDefn -> TCMT IO (Map QName PatternSynDefn)
forall (m :: * -> *) a. Monad m => a -> m a
return Map QName PatternSynDefn
forall a. Null a => a
empty
let syntax :: HashMap QName NameKind
syntax = ((HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> [HashMap QName NameKind -> HashMap QName NameKind]
-> HashMap QName NameKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind -> HashMap QName NameKind
forall a b. (a -> b) -> a -> b
($) HashMap QName NameKind
forall k v. HashMap k v
HMap.empty ([HashMap QName NameKind -> HashMap QName NameKind]
-> HashMap QName NameKind)
-> [HashMap QName NameKind -> HashMap QName NameKind]
-> HashMap QName NameKind
forall a b. (a -> b) -> a -> b
$ (Declaration -> HashMap QName NameKind -> HashMap QName NameKind)
-> [Declaration]
-> [HashMap QName NameKind -> HashMap QName NameKind]
forall a b. (a -> b) -> [a] -> [b]
map Declaration -> HashMap QName NameKind -> HashMap QName NameKind
declToKind ([Declaration]
-> [HashMap QName NameKind -> HashMap QName NameKind])
-> [Declaration]
-> [HashMap QName NameKind -> HashMap QName NameKind]
forall a b. (a -> b) -> a -> b
$ Declaration -> [Declaration]
forall s t. UniverseBi s t => s -> [t]
universeBi Declaration
decl
NameKinds -> TCM NameKinds
forall (m :: * -> *) a. Monad m => a -> m a
return (NameKinds -> TCM NameKinds) -> NameKinds -> TCM NameKinds
forall a b. (a -> b) -> a -> b
$ \ n :: QName
n -> (NameKind -> NameKind -> NameKind)
-> [Maybe NameKind] -> Maybe NameKind
forall a. (a -> a -> a) -> [Maybe a] -> Maybe a
unionsMaybeWith NameKind -> NameKind -> NameKind
merge
[ Defn -> NameKind
defnToKind (Defn -> NameKind)
-> (Definition -> Defn) -> Definition -> NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName Definition
local
, NameKind
con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName PatternSynDefn
locPatSyns
, Defn -> NameKind
defnToKind (Defn -> NameKind)
-> (Definition -> Defn) -> Definition -> NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> NameKind) -> Maybe Definition -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> HashMap QName Definition -> Maybe Definition
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName Definition
imported
, NameKind
con NameKind -> Maybe PatternSynDefn -> Maybe NameKind
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ QName -> Map QName PatternSynDefn -> Maybe PatternSynDefn
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
n Map QName PatternSynDefn
impPatSyns
, QName -> HashMap QName NameKind -> Maybe NameKind
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HMap.lookup QName
n HashMap QName NameKind
syntax
]
where
merge :: NameKind -> NameKind -> NameKind
merge Postulate k :: NameKind
k = NameKind
k
merge _ Macro = NameKind
Macro
merge k :: NameKind
k _ = NameKind
k
insert :: QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert = (NameKind -> NameKind -> NameKind)
-> QName
-> NameKind
-> HashMap QName NameKind
-> HashMap QName NameKind
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
HMap.insertWith NameKind -> NameKind -> NameKind
merge
defnToKind :: Defn -> NameKind
defnToKind :: Defn -> NameKind
defnToKind M.Axiom{} = NameKind
Postulate
defnToKind M.DataOrRecSig{} = NameKind
Postulate
defnToKind M.GeneralizableVar{} = NameKind
Generalizable
defnToKind d :: Defn
d@M.Function{} | Defn -> Bool
isProperProjection Defn
d = NameKind
Field
| Bool
otherwise = NameKind
Function
defnToKind M.Datatype{} = NameKind
Datatype
defnToKind M.Record{} = NameKind
Record
defnToKind M.Constructor{ conInd :: Defn -> Induction
M.conInd = Induction
i } = Induction -> NameKind
Constructor Induction
i
defnToKind M.Primitive{} = NameKind
Primitive
defnToKind M.AbstractDefn{} = NameKind
forall a. HasCallStack => a
__IMPOSSIBLE__
declToKind :: A.Declaration ->
HashMap A.QName NameKind -> HashMap A.QName NameKind
declToKind :: Declaration -> HashMap QName NameKind -> HashMap QName NameKind
declToKind (A.Axiom _ i :: DefInfo
i _ _ q :: QName
q _)
| DefInfo -> IsMacro
forall t. DefInfo' t -> IsMacro
defMacro DefInfo
i IsMacro -> IsMacro -> Bool
forall a. Eq a => a -> a -> Bool
== IsMacro
Common.MacroDef = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Macro
| Bool
otherwise = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Postulate
declToKind (A.Field _ q :: QName
q _) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Field
declToKind (A.Primitive _ q :: QName
q _) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Primitive
declToKind (A.Mutual {}) = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
declToKind (A.Section {}) = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
declToKind (A.Apply {}) = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
declToKind (A.Import {}) = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
declToKind (A.Pragma {}) = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
declToKind (A.ScopedDecl {}) = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
declToKind (A.Open {}) = HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id
declToKind (A.PatternSynDef q :: QName
q _ _) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
con
declToKind (A.Generalize _ _ _ q :: QName
q _) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Generalizable
declToKind (A.FunDef _ q :: QName
q _ _) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Function
declToKind (A.UnquoteDecl _ _ qs :: [QName]
qs _) = (QName
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> [QName]
-> HashMap QName NameKind
-> HashMap QName NameKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ q :: QName
q f :: HashMap QName NameKind -> HashMap QName NameKind
f -> QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Function (HashMap QName NameKind -> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> HashMap QName NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap QName NameKind -> HashMap QName NameKind
f) HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id [QName]
qs
declToKind (A.UnquoteDef _ qs :: [QName]
qs _) = (QName
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> [QName]
-> HashMap QName NameKind
-> HashMap QName NameKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ q :: QName
q f :: HashMap QName NameKind -> HashMap QName NameKind
f -> QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Function (HashMap QName NameKind -> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> HashMap QName NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap QName NameKind -> HashMap QName NameKind
f) HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id [QName]
qs
declToKind (A.DataSig _ q :: QName
q _ _) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Datatype
declToKind (A.DataDef _ q :: QName
q _ _ cs :: [Declaration]
cs) = \m :: HashMap QName NameKind
m ->
QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Datatype (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind -> HashMap QName NameKind
forall a b. (a -> b) -> a -> b
$
(Declaration -> HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> [Declaration]
-> HashMap QName NameKind
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\d :: Declaration
d -> QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert (Declaration -> QName
A.axiomName Declaration
d) NameKind
con)
HashMap QName NameKind
m [Declaration]
cs
declToKind (A.RecSig _ q :: QName
q _ _) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Record
declToKind (A.RecDef _ q :: QName
q _ _ _ c :: Maybe QName
c _ _ _) = QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
insert QName
q NameKind
Record (HashMap QName NameKind -> HashMap QName NameKind)
-> (HashMap QName NameKind -> HashMap QName NameKind)
-> HashMap QName NameKind
-> HashMap QName NameKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashMap QName NameKind -> HashMap QName NameKind)
-> (QName -> HashMap QName NameKind -> HashMap QName NameKind)
-> Maybe QName
-> HashMap QName NameKind
-> HashMap QName NameKind
forall b a. b -> (a -> b) -> Maybe a -> b
maybe HashMap QName NameKind -> HashMap QName NameKind
forall a. a -> a
id (QName
-> NameKind -> HashMap QName NameKind -> HashMap QName NameKind
`insert` NameKind
con) Maybe QName
c
con :: NameKind
con :: NameKind
con = Induction -> NameKind
Constructor Induction
Common.Inductive
generateConstructorInfo
:: SourceToModule
-> AbsolutePath
-> NameKinds
-> A.Declaration
-> TCM File
generateConstructorInfo :: SourceToModule
-> AbsolutePath -> NameKinds -> Declaration -> TCM File
generateConstructorInfo modMap :: SourceToModule
modMap file :: AbsolutePath
file kinds :: NameKinds
kinds decl :: Declaration
decl = do
[IntervalWithoutFile]
-> TCM File -> ([IntervalWithoutFile] -> TCM File) -> TCM File
forall a b. Null a => a -> b -> (a -> b) -> b
ifNull (Range -> [IntervalWithoutFile]
forall a. Range' a -> [IntervalWithoutFile]
P.rangeIntervals (Range -> [IntervalWithoutFile]) -> Range -> [IntervalWithoutFile]
forall a b. (a -> b) -> a -> b
$ Declaration -> Range
forall t. HasRange t => t -> Range
getRange Declaration
decl)
(File -> TCM File
forall (m :: * -> *) a. Monad m => a -> m a
return File
forall a. Monoid a => a
mempty) (([IntervalWithoutFile] -> TCM File) -> TCM File)
-> ([IntervalWithoutFile] -> TCM File) -> TCM File
forall a b. (a -> b) -> a -> b
$ \is :: [IntervalWithoutFile]
is -> do
let start :: VerboseLevel
start = Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> VerboseLevel) -> Int32 -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iStart (IntervalWithoutFile -> Position' ())
-> IntervalWithoutFile -> Position' ()
forall a b. (a -> b) -> a -> b
$ [IntervalWithoutFile] -> IntervalWithoutFile
forall a. [a] -> a
head [IntervalWithoutFile]
is
end :: VerboseLevel
end = Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> VerboseLevel) -> Int32 -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> Int32) -> Position' () -> Int32
forall a b. (a -> b) -> a -> b
$ IntervalWithoutFile -> Position' ()
forall a. Interval' a -> Position' a
P.iEnd (IntervalWithoutFile -> Position' ())
-> IntervalWithoutFile -> Position' ()
forall a b. (a -> b) -> a -> b
$ [IntervalWithoutFile] -> IntervalWithoutFile
forall a. [a] -> a
last [IntervalWithoutFile]
is
DisambiguatedNames
m0 <- Lens' DisambiguatedNames TCState -> TCMT IO DisambiguatedNames
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' DisambiguatedNames TCState
stDisambiguatedNames
let (_, m1 :: DisambiguatedNames
m1) = VerboseLevel
-> DisambiguatedNames -> (DisambiguatedNames, DisambiguatedNames)
forall a. VerboseLevel -> IntMap a -> (IntMap a, IntMap a)
IntMap.split (VerboseLevel -> VerboseLevel
forall a. Enum a => a -> a
pred VerboseLevel
start) DisambiguatedNames
m0
(m2 :: DisambiguatedNames
m2, _) = VerboseLevel
-> DisambiguatedNames -> (DisambiguatedNames, DisambiguatedNames)
forall a. VerboseLevel -> IntMap a -> (IntMap a, IntMap a)
IntMap.split VerboseLevel
end DisambiguatedNames
m1
constrs :: [QName]
constrs = DisambiguatedNames -> [QName]
forall a. IntMap a -> [a]
IntMap.elems DisambiguatedNames
m2
let files :: [File]
files = [QName] -> (QName -> File) -> [File]
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [QName]
constrs ((QName -> File) -> [File]) -> (QName -> File) -> [File]
forall a b. (a -> b) -> a -> b
$ \ q :: QName
q -> SourceToModule
-> AbsolutePath -> NameKinds -> AmbiguousQName -> File
generate SourceToModule
modMap AbsolutePath
file NameKinds
kinds (AmbiguousQName -> File) -> AmbiguousQName -> File
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
I.unambiguous QName
q
File -> TCM File
forall (m :: * -> *) a. Monad m => a -> m a
return (File -> TCM File) -> File -> TCM File
forall a b. (a -> b) -> a -> b
$ [File] -> File
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Fold.fold [File]
files
printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo :: Range -> TCM ()
printSyntaxInfo r :: Range
r = do
CompressedFile
syntaxInfo <- Lens' CompressedFile TCState -> TCMT IO CompressedFile
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' CompressedFile TCState
stSyntaxInfo
HighlightingLevel -> TCM () -> TCM ()
forall (tcm :: * -> *).
MonadTCM tcm =>
HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs HighlightingLevel
NonInteractive (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (Range -> CompressedFile -> CompressedFile
selectC Range
r CompressedFile
syntaxInfo)
printErrorInfo :: TCErr -> TCM ()
printErrorInfo :: TCErr -> TCM ()
printErrorInfo e :: TCErr
e =
RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (CompressedFile -> TCM ())
-> (File -> CompressedFile) -> File -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. File -> CompressedFile
compress (File -> TCM ()) -> TCM File -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
TCErr -> TCM File
errorHighlighting TCErr
e
errorHighlighting :: TCErr -> TCM File
errorHighlighting :: TCErr -> TCM File
errorHighlighting e :: TCErr
e = do
let r :: Range
r = TCErr -> Range
forall t. HasRange t => t -> Range
getRange TCErr
e
erase :: File
erase = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
forall a. Monoid a => a
mempty
VerboseKey
s <- TCErr -> TCMT IO VerboseKey
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm VerboseKey
E.prettyError TCErr
e
let error :: File
error = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR Range
r)
(Aspects -> File) -> Aspects -> File
forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
Error
, note :: Maybe VerboseKey
note = VerboseKey -> Maybe VerboseKey
forall a. a -> Maybe a
Just VerboseKey
s
}
File -> TCM File
forall (m :: * -> *) a. Monad m => a -> m a
return (File -> TCM File) -> File -> TCM File
forall a b. (a -> b) -> a -> b
$ [File] -> File
forall a. Monoid a => [a] -> a
mconcat [ File
erase, File
error ]
warningHighlighting :: TCWarning -> File
warningHighlighting :: TCWarning -> File
warningHighlighting w :: TCWarning
w = case TCWarning -> Warning
tcWarning TCWarning
w of
TerminationIssue terrs :: [TerminationError]
terrs -> [TerminationError] -> File
terminationErrorHighlighting [TerminationError]
terrs
NotStrictlyPositive d :: QName
d ocs :: Seq OccursWhere
ocs -> QName -> Seq OccursWhere -> File
positivityErrorHighlighting QName
d Seq OccursWhere
ocs
UnreachableClauses _ rs :: [Range]
rs -> (Range -> File) -> [Range] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Range -> File
deadcodeHighlighting [Range]
rs
CoverageIssue{} -> Range -> File
coverageErrorHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
CoverageNoExactSplit{} -> Range -> File
catchallHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
UnsolvedConstraints cs :: Constraints
cs -> Constraints -> File
constraintsHighlighting Constraints
cs
UnsolvedMetaVariables rs :: [Range]
rs -> [Range] -> File
metasHighlighting [Range]
rs
AbsurdPatternRequiresNoRHS{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
ModuleDoesntExport{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
FixityInRenamingModule rs :: NonEmpty Range
rs -> (Range -> File) -> NonEmpty Range -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap Range -> File
deadcodeHighlighting NonEmpty Range
rs
CantGeneralizeOverSorts{} -> File
forall a. Monoid a => a
mempty
UnsolvedInteractionMetas{} -> File
forall a. Monoid a => a
mempty
OldBuiltin{} -> File
forall a. Monoid a => a
mempty
EmptyRewritePragma{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
IllformedAsClause{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
UselessPublic{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
UselessInline{} -> File
forall a. Monoid a => a
mempty
ClashesViaRenaming _ xs :: [Name]
xs -> (Name -> File) -> [Name] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (Range -> File
deadcodeHighlighting (Range -> File) -> (Name -> Range) -> Name -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
forall t. HasRange t => t -> Range
getRange) [Name]
xs
WrongInstanceDeclaration{} -> File
forall a. Monoid a => a
mempty
InstanceWithExplicitArg{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
InstanceNoOutputTypeName{} -> File
forall a. Monoid a => a
mempty
InstanceArgWithExplicitArg{} -> File
forall a. Monoid a => a
mempty
ParseWarning{} -> File
forall a. Monoid a => a
mempty
InversionDepthReached{} -> File
forall a. Monoid a => a
mempty
GenericWarning{} -> File
forall a. Monoid a => a
mempty
GenericNonFatalError{} -> File
forall a. Monoid a => a
mempty
SafeFlagPostulate{} -> File
forall a. Monoid a => a
mempty
SafeFlagPragma{} -> File
forall a. Monoid a => a
mempty
SafeFlagNonTerminating -> File
forall a. Monoid a => a
mempty
SafeFlagTerminating -> File
forall a. Monoid a => a
mempty
SafeFlagWithoutKFlagPrimEraseEquality -> File
forall a. Monoid a => a
mempty
SafeFlagEta -> File
forall a. Monoid a => a
mempty
SafeFlagInjective -> File
forall a. Monoid a => a
mempty
SafeFlagNoCoverageCheck -> File
forall a. Monoid a => a
mempty
WithoutKFlagPrimEraseEquality -> File
forall a. Monoid a => a
mempty
SafeFlagNoPositivityCheck -> File
forall a. Monoid a => a
mempty
SafeFlagPolarity -> File
forall a. Monoid a => a
mempty
SafeFlagNoUniverseCheck -> File
forall a. Monoid a => a
mempty
DeprecationWarning{} -> File
forall a. Monoid a => a
mempty
UserWarning{} -> File
forall a. Monoid a => a
mempty
LibraryWarning{} -> File
forall a. Monoid a => a
mempty
InfectiveImport{} -> File
forall a. Monoid a => a
mempty
CoInfectiveImport{} -> File
forall a. Monoid a => a
mempty
RewriteNonConfluent{} -> Range -> File
confluenceErrorHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
RewriteMaybeNonConfluent{} -> Range -> File
confluenceErrorHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
PragmaCompileErased{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
NotInScopeW{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ TCWarning -> Range
forall t. HasRange t => t -> Range
getRange TCWarning
w
NicifierIssue w :: DeclarationWarning
w -> case DeclarationWarning
w of
NotAllowedInMutual{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyAbstract{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyInstance{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyMacro{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyMutual{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyPostulate{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyPrimitive{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyPrivate{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyGeneralize{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
EmptyField{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
UselessAbstract{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
UselessInstance{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
UselessPrivate{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
InvalidNoPositivityCheckPragma{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
InvalidNoUniverseCheckPragma{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
InvalidTerminationCheckPragma{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
InvalidCoverageCheckPragma{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
OpenPublicAbstract{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
OpenPublicPrivate{} -> Range -> File
deadcodeHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
W.ShadowingInTelescope nrs :: [(Name, [Range])]
nrs -> ((Name, [Range]) -> File) -> [(Name, [Range])] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap
([Range] -> File
shadowingTelHighlighting ([Range] -> File)
-> ((Name, [Range]) -> [Range]) -> (Name, [Range]) -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, [Range]) -> [Range]
forall a b. (a, b) -> b
snd)
[(Name, [Range])]
nrs
MissingDefinitions{} -> Range -> File
missingDefinitionHighlighting (Range -> File) -> Range -> File
forall a b. (a -> b) -> a -> b
$ DeclarationWarning -> Range
forall t. HasRange t => t -> Range
getRange DeclarationWarning
w
InvalidCatchallPragma{} -> File
forall a. Monoid a => a
mempty
PolarityPragmasButNotPostulates{} -> File
forall a. Monoid a => a
mempty
PragmaNoTerminationCheck{} -> File
forall a. Monoid a => a
mempty
PragmaCompiled{} -> File
forall a. Monoid a => a
mempty
UnknownFixityInMixfixDecl{} -> File
forall a. Monoid a => a
mempty
UnknownNamesInFixityDecl{} -> File
forall a. Monoid a => a
mempty
UnknownNamesInPolarityPragmas{} -> File
forall a. Monoid a => a
mempty
terminationErrorHighlighting :: [TerminationError] -> File
terminationErrorHighlighting :: [TerminationError] -> File
terminationErrorHighlighting termErrs :: [TerminationError]
termErrs = File
functionDefs File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend` File
callSites
where
m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
TerminationProblem }
functionDefs :: File
functionDefs = (QName -> File) -> [QName] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (\x :: QName
x -> Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ QName -> Range
bindingSite QName
x) Aspects
m) ([QName] -> File) -> [QName] -> File
forall a b. (a -> b) -> a -> b
$
(TerminationError -> [QName]) -> [TerminationError] -> [QName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TerminationError -> [QName]
M.termErrFunctions [TerminationError]
termErrs
callSites :: File
callSites = (Range -> File) -> [Range] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (\r :: Range
r -> Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR Range
r) Aspects
m) ([Range] -> File) -> [Range] -> File
forall a b. (a -> b) -> a -> b
$
(TerminationError -> [Range]) -> [TerminationError] -> [Range]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((CallInfo -> Range) -> [CallInfo] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map CallInfo -> Range
M.callInfoRange ([CallInfo] -> [Range])
-> (TerminationError -> [CallInfo]) -> TerminationError -> [Range]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TerminationError -> [CallInfo]
M.termErrCalls) [TerminationError]
termErrs
positivityErrorHighlighting :: I.QName -> Seq OccursWhere -> File
positivityErrorHighlighting :: QName -> Seq OccursWhere -> File
positivityErrorHighlighting q :: QName
q os :: Seq OccursWhere
os =
[Ranges] -> Aspects -> File
several (Range -> Ranges
rToR (Range -> Ranges) -> [Range] -> [Ranges]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> Range
forall t. HasRange t => t -> Range
getRange QName
q Range -> [Range] -> [Range]
forall a. a -> [a] -> [a]
: [Range]
rs) Aspects
m
where
rs :: [Range]
rs = (OccursWhere -> Range) -> [OccursWhere] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map (\(OccursWhere r :: Range
r _ _) -> Range
r) (Seq OccursWhere -> [OccursWhere]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList Seq OccursWhere
os)
m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
PositivityProblem }
deadcodeHighlighting :: Range -> File
deadcodeHighlighting :: Range -> File
deadcodeHighlighting r :: Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuous Range
r) Aspects
m
where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
Deadcode }
coverageErrorHighlighting :: Range -> File
coverageErrorHighlighting :: Range -> File
coverageErrorHighlighting r :: Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
CoverageProblem }
shadowingTelHighlighting :: [Range] -> File
shadowingTelHighlighting :: [Range] -> File
shadowingTelHighlighting =
(Range -> File) -> [Range] -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (\r :: Range
r -> Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Range' a -> Range' a
P.continuous Range
r) Aspects
m) ([Range] -> File) -> ([Range] -> [Range]) -> [Range] -> File
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Range] -> [Range]
forall a. [a] -> [a]
init
where
m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects =
OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
P.ShadowingInTelescope }
catchallHighlighting :: Range -> File
catchallHighlighting :: Range -> File
catchallHighlighting r :: Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
CatchallClause }
confluenceErrorHighlighting :: Range -> File
confluenceErrorHighlighting :: Range -> File
confluenceErrorHighlighting r :: Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
ConfluenceProblem }
missingDefinitionHighlighting :: Range -> File
missingDefinitionHighlighting :: Range -> File
missingDefinitionHighlighting r :: Range
r = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine Range
r) Aspects
m
where m :: Aspects
m = Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
MissingDefinition }
printUnsolvedInfo :: TCM ()
printUnsolvedInfo :: TCM ()
printUnsolvedInfo = do
File
metaInfo <- TCM File
computeUnsolvedMetaWarnings
File
constraintInfo <- TCM File
computeUnsolvedConstraints
RemoveTokenBasedHighlighting -> CompressedFile -> TCM ()
forall (tcm :: * -> *).
(MonadTCM tcm, ReadTCState tcm) =>
RemoveTokenBasedHighlighting -> CompressedFile -> tcm ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting
(File -> CompressedFile
compress (File -> CompressedFile) -> File -> CompressedFile
forall a b. (a -> b) -> a -> b
$ File
metaInfo File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend` File
constraintInfo)
computeUnsolvedMetaWarnings :: TCM File
computeUnsolvedMetaWarnings :: TCM File
computeUnsolvedMetaWarnings = do
[MetaId]
is <- TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getInteractionMetas
let notBlocked :: MetaId -> TCMT IO Bool
notBlocked m :: MetaId
m = Bool -> Bool
not (Bool -> Bool) -> TCMT IO Bool -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> TCMT IO Bool
isBlockedTerm MetaId
m
[MetaId]
ms <- (MetaId -> TCMT IO Bool) -> [MetaId] -> TCMT IO [MetaId]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM MetaId -> TCMT IO Bool
notBlocked ([MetaId] -> TCMT IO [MetaId])
-> TCMT IO [MetaId] -> TCMT IO [MetaId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
[Range]
rs <- (MetaId -> TCMT IO Range) -> [MetaId] -> TCMT IO [Range]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM MetaId -> TCMT IO Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange ([MetaId]
ms [MetaId] -> [MetaId] -> [MetaId]
forall a. Eq a => [a] -> [a] -> [a]
\\ [MetaId]
is)
File -> TCM File
forall (m :: * -> *) a. Monad m => a -> m a
return (File -> TCM File) -> File -> TCM File
forall a b. (a -> b) -> a -> b
$ [Range] -> File
metasHighlighting [Range]
rs
metasHighlighting :: [Range] -> File
metasHighlighting :: [Range] -> File
metasHighlighting rs :: [Range]
rs = [Ranges] -> Aspects -> File
several ((Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> Ranges
rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine) [Range]
rs)
(Aspects -> File) -> Aspects -> File
forall a b. (a -> b) -> a -> b
$ Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
UnsolvedMeta }
computeUnsolvedConstraints :: TCM File
computeUnsolvedConstraints :: TCM File
computeUnsolvedConstraints = Constraints -> File
constraintsHighlighting (Constraints -> File) -> TCMT IO Constraints -> TCM File
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Constraints
forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints
constraintsHighlighting :: Constraints -> File
constraintsHighlighting :: Constraints -> File
constraintsHighlighting cs :: Constraints
cs =
[Ranges] -> Aspects -> File
several ((Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> Ranges
rToR (Range -> Ranges) -> (Range -> Range) -> Range -> Ranges
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Range
forall a. Ord a => Range' a -> Range' a
P.continuousPerLine) [Range]
rs)
(Aspects
parserBased { otherAspects :: Set OtherAspect
otherAspects = OtherAspect -> Set OtherAspect
forall a. a -> Set a
Set.singleton OtherAspect
UnsolvedConstraint })
where
rs :: [Range]
rs = ((Closure Constraint -> Maybe Range)
-> [Closure Constraint] -> [Range]
forall a b. (a -> Maybe b) -> [a] -> [b]
`mapMaybe` ((ProblemConstraint -> Closure Constraint)
-> Constraints -> [Closure Constraint]
forall a b. (a -> b) -> [a] -> [b]
map ProblemConstraint -> Closure Constraint
theConstraint Constraints
cs)) ((Closure Constraint -> Maybe Range) -> [Range])
-> (Closure Constraint -> Maybe Range) -> [Range]
forall a b. (a -> b) -> a -> b
$ \case
Closure{ clValue :: forall a. Closure a -> a
clValue = IsEmpty r :: Range
r t :: Type
t } -> Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r
Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ValueCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = ElimCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = TelCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = SortCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = LevelCmp{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
Closure{ clEnv :: forall a. Closure a -> TCEnv
clEnv = TCEnv
e, clValue :: forall a. Closure a -> a
clValue = CheckSizeLtSat{} } -> Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ Range -> Range
forall t. HasRange t => t -> Range
getRange (TCEnv -> Range
envRange TCEnv
e)
_ -> Maybe Range
forall a. Maybe a
Nothing
generate :: SourceToModule
-> AbsolutePath
-> NameKinds
-> A.AmbiguousQName
-> File
generate :: SourceToModule
-> AbsolutePath -> NameKinds -> AmbiguousQName -> File
generate modMap :: SourceToModule
modMap file :: AbsolutePath
file kinds :: NameKinds
kinds (A.AmbQ qs :: NonEmpty QName
qs) =
(QName -> File) -> NonEmpty QName -> File
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Fold.foldMap (\ q :: QName
q -> SourceToModule
-> AbsolutePath -> QName -> Bool -> (Bool -> Aspects) -> File
nameToFileA SourceToModule
modMap AbsolutePath
file QName
q Bool
include Bool -> Aspects
m) NonEmpty QName
qs
where
ks :: [Maybe NameKind]
ks = NameKinds -> [QName] -> [Maybe NameKind]
forall a b. (a -> b) -> [a] -> [b]
map NameKinds
kinds (NonEmpty QName -> [QName]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList NonEmpty QName
qs)
kind :: Maybe NameKind
kind = case [ NameKind
k | Just k :: NameKind
k <- [Maybe NameKind]
ks ] of
k :: NameKind
k : _ -> NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
k
[] -> Maybe NameKind
forall a. Maybe a
Nothing
m :: Bool -> Aspects
m isOp :: Bool
isOp = Aspects
parserBased { aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name Maybe NameKind
kind Bool
isOp }
include :: Bool
include = [Range] -> Bool
forall a. Eq a => [a] -> Bool
allEqual ((QName -> Range) -> [QName] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map QName -> Range
bindingSite ([QName] -> [Range]) -> [QName] -> [Range]
forall a b. (a -> b) -> a -> b
$ NonEmpty QName -> [QName]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList NonEmpty QName
qs)
nameToFile :: SourceToModule
-> AbsolutePath
-> [C.Name]
-> C.Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile :: SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile modMap :: SourceToModule
modMap file :: AbsolutePath
file xs :: [Name]
xs x :: Name
x fr :: Range
fr m :: Bool -> Aspects
m mR :: Maybe Range
mR =
if (SrcFile -> Bool) -> [SrcFile] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SrcFile -> SrcFile -> Bool
forall a. Eq a => a -> a -> Bool
== AbsolutePath -> SrcFile
forall a. a -> Maybe a
Strict.Just AbsolutePath
file) [SrcFile]
fileNames then
File
frFile File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend`
[Ranges] -> Aspects -> File
several ((Range -> Ranges) -> [Range] -> [Ranges]
forall a b. (a -> b) -> [a] -> [b]
map Range -> Ranges
rToR [Range]
rs)
(Aspects
aspects { definitionSite :: Maybe DefinitionSite
definitionSite = Maybe DefinitionSite
mFilePos })
else
File
forall a. Monoid a => a
mempty
where
aspects :: Aspects
aspects = Bool -> Aspects
m (Bool -> Aspects) -> Bool -> Aspects
forall a b. (a -> b) -> a -> b
$ Name -> Bool
C.isOperator Name
x
fileNames :: [SrcFile]
fileNames = (Name -> Maybe SrcFile) -> [Name] -> [SrcFile]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((Position' SrcFile -> SrcFile)
-> Maybe (Position' SrcFile) -> Maybe SrcFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Position' SrcFile -> SrcFile
forall a. Position' a -> a
P.srcFile (Maybe (Position' SrcFile) -> Maybe SrcFile)
-> (Name -> Maybe (Position' SrcFile)) -> Name -> Maybe SrcFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
P.rStart (Range -> Maybe (Position' SrcFile))
-> (Name -> Range) -> Name -> Maybe (Position' SrcFile)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Range
forall t. HasRange t => t -> Range
getRange) (Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
xs)
frFile :: File
frFile = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR Range
fr) (Aspects
aspects { definitionSite :: Maybe DefinitionSite
definitionSite = DefinitionSite -> DefinitionSite
notHere (DefinitionSite -> DefinitionSite)
-> Maybe DefinitionSite -> Maybe DefinitionSite
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DefinitionSite
mFilePos })
rs :: [Range]
rs = (Name -> Range) -> [Name] -> [Range]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Range
forall t. HasRange t => t -> Range
getRange (Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
xs)
notHere :: DefinitionSite -> DefinitionSite
notHere d :: DefinitionSite
d = DefinitionSite
d { defSiteHere :: Bool
defSiteHere = Bool
False }
mFilePos :: Maybe DefinitionSite
mFilePos :: Maybe DefinitionSite
mFilePos = do
Range
r <- Maybe Range
mR
P.Pn { srcFile :: forall a. Position' a -> a
P.srcFile = Strict.Just f :: AbsolutePath
f, posPos :: forall a. Position' a -> Int32
P.posPos = Int32
p } <- Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
P.rStart Range
r
TopLevelModuleName
mod <- AbsolutePath -> SourceToModule -> Maybe TopLevelModuleName
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup AbsolutePath
f SourceToModule
modMap
let qualifiers :: [Name]
qualifiers = VerboseLevel -> [Name] -> [Name]
forall a. VerboseLevel -> [a] -> [a]
drop ([VerboseKey] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([VerboseKey] -> VerboseLevel) -> [VerboseKey] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> [VerboseKey]
C.moduleNameParts TopLevelModuleName
mod) [Name]
xs
local :: Bool
local = Bool -> (Aspect -> Bool) -> Maybe Aspect -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Aspect -> Bool
isLocalAspect (Maybe Aspect -> Bool) -> Maybe Aspect -> Bool
forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe Aspect
aspect Aspects
aspects
DefinitionSite -> Maybe DefinitionSite
forall (m :: * -> *) a. Monad m => a -> m a
return (DefinitionSite -> Maybe DefinitionSite)
-> DefinitionSite -> Maybe DefinitionSite
forall a b. (a -> b) -> a -> b
$ DefinitionSite :: TopLevelModuleName
-> VerboseLevel -> Bool -> Maybe VerboseKey -> DefinitionSite
DefinitionSite
{ defSiteModule :: TopLevelModuleName
defSiteModule = TopLevelModuleName
mod
, defSitePos :: VerboseLevel
defSitePos = Int32 -> VerboseLevel
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int32
p
, defSiteHere :: Bool
defSiteHere = Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Range
forall t. HasRange t => t -> Range
getRange Name
x
, defSiteAnchor :: Maybe VerboseKey
defSiteAnchor = if Bool
local Bool -> Bool -> Bool
|| Name -> Bool
forall a. IsNoName a => a -> Bool
C.isNoName Name
x Bool -> Bool -> Bool
|| (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Name -> Bool
forall a. Underscore a => a -> Bool
Common.isUnderscore [Name]
qualifiers
then Maybe VerboseKey
forall a. Maybe a
Nothing
else VerboseKey -> Maybe VerboseKey
forall a. a -> Maybe a
Just (VerboseKey -> Maybe VerboseKey) -> VerboseKey -> Maybe VerboseKey
forall a b. (a -> b) -> a -> b
$ QName -> VerboseKey
forall a. Pretty a => a -> VerboseKey
prettyShow (QName -> VerboseKey) -> QName -> VerboseKey
forall a b. (a -> b) -> a -> b
$ (Name -> QName -> QName) -> QName -> [Name] -> QName
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> QName -> QName
C.Qual (Name -> QName
C.QName Name
x) [Name]
qualifiers
}
isLocalAspect :: Aspect -> Bool
isLocalAspect :: Aspect -> Bool
isLocalAspect = \case
Name mkind :: Maybe NameKind
mkind _ -> Bool -> (NameKind -> Bool) -> Maybe NameKind -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True NameKind -> Bool
isLocal Maybe NameKind
mkind
_ -> Bool
True
isLocal :: NameKind -> Bool
isLocal :: NameKind -> Bool
isLocal = \case
Bound -> Bool
True
Generalizable -> Bool
True
Argument -> Bool
True
Constructor{} -> Bool
False
Datatype -> Bool
False
Field -> Bool
False
Function -> Bool
False
Module -> Bool
False
Postulate -> Bool
False
Primitive -> Bool
False
Record -> Bool
False
Macro -> Bool
False
nameToFileA
:: SourceToModule
-> AbsolutePath
-> A.QName
-> Bool
-> (Bool -> Aspects)
-> File
nameToFileA :: SourceToModule
-> AbsolutePath -> QName -> Bool -> (Bool -> Aspects) -> File
nameToFileA modMap :: SourceToModule
modMap file :: AbsolutePath
file x :: QName
x include :: Bool
include m :: Bool -> Aspects
m =
SourceToModule
-> AbsolutePath
-> [Name]
-> Name
-> Range
-> (Bool -> Aspects)
-> Maybe Range
-> File
nameToFile SourceToModule
modMap
AbsolutePath
file
(QName -> [Name]
concreteQualifier QName
x)
(QName -> Name
concreteBase QName
x)
Range
rangeOfFixityDeclaration
Bool -> Aspects
m
(if Bool
include then Range -> Maybe Range
forall a. a -> Maybe a
Just (Range -> Maybe Range) -> Range -> Maybe Range
forall a b. (a -> b) -> a -> b
$ QName -> Range
bindingSite QName
x else Maybe Range
forall a. Maybe a
Nothing)
File -> File -> File
forall a. Monoid a => a -> a -> a
`mappend` File
notationFile
where
rangeOfFixityDeclaration :: Range
rangeOfFixityDeclaration =
if Range -> SrcFile
P.rangeFile Range
r SrcFile -> SrcFile -> Bool
forall a. Eq a => a -> a -> Bool
== AbsolutePath -> SrcFile
forall a. a -> Maybe a
Strict.Just AbsolutePath
file
then Range
r else Range
forall a. Range' a
noRange
where
r :: Range
r = Fixity' -> Range
Common.theNameRange (Fixity' -> Range) -> Fixity' -> Range
forall a b. (a -> b) -> a -> b
$ Name -> Fixity'
A.nameFixity (Name -> Fixity') -> Name -> Fixity'
forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
x
notationFile :: File
notationFile =
if Range -> SrcFile
P.rangeFile (Notation -> Range
forall t. HasRange t => t -> Range
getRange Notation
notation) SrcFile -> SrcFile -> Bool
forall a. Eq a => a -> a -> Bool
== AbsolutePath -> SrcFile
forall a. a -> Maybe a
Strict.Just AbsolutePath
file
then [File] -> File
forall a. Monoid a => [a] -> a
mconcat ([File] -> File) -> [File] -> File
forall a b. (a -> b) -> a -> b
$ (GenPart -> File) -> Notation -> [File]
forall a b. (a -> b) -> [a] -> [b]
map GenPart -> File
genPartFile Notation
notation
else File
forall a. Monoid a => a
mempty
where
notation :: Notation
notation = Fixity' -> Notation
Common.theNotation (Fixity' -> Notation) -> Fixity' -> Notation
forall a b. (a -> b) -> a -> b
$ Name -> Fixity'
A.nameFixity (Name -> Fixity') -> Name -> Fixity'
forall a b. (a -> b) -> a -> b
$ QName -> Name
A.qnameName QName
x
boundAspect :: Aspects
boundAspect = Aspects
parserBased{ aspect :: Maybe Aspect
aspect = Aspect -> Maybe Aspect
forall a. a -> Maybe a
Just (Aspect -> Maybe Aspect) -> Aspect -> Maybe Aspect
forall a b. (a -> b) -> a -> b
$ Maybe NameKind -> Bool -> Aspect
Name (NameKind -> Maybe NameKind
forall a. a -> Maybe a
Just NameKind
Bound) Bool
False }
genPartFile :: GenPart -> File
genPartFile (Common.BindHole r :: Range
r i :: Ranged VerboseLevel
i) = [Ranges] -> Aspects -> File
several [Range -> Ranges
rToR Range
r, Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ Ranged VerboseLevel -> Range
forall t. HasRange t => t -> Range
getRange Ranged VerboseLevel
i] Aspects
boundAspect
genPartFile (Common.NormalHole r :: Range
r i :: NamedArg (Ranged VerboseLevel)
i) = [Ranges] -> Aspects -> File
several [Range -> Ranges
rToR Range
r, Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ NamedArg (Ranged VerboseLevel) -> Range
forall t. HasRange t => t -> Range
getRange NamedArg (Ranged VerboseLevel)
i] Aspects
boundAspect
genPartFile Common.WildHole{} = File
forall a. Monoid a => a
mempty
genPartFile (Common.IdPart x :: RString
x) = Ranges -> Aspects -> File
singleton (Range -> Ranges
rToR (Range -> Ranges) -> Range -> Ranges
forall a b. (a -> b) -> a -> b
$ RString -> Range
forall t. HasRange t => t -> Range
getRange RString
x) (Bool -> Aspects
m Bool
False)
concreteBase :: I.QName -> C.Name
concreteBase :: QName -> Name
concreteBase = Name -> Name
A.nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName
concreteQualifier :: I.QName -> [C.Name]
concreteQualifier :: QName -> [Name]
concreteQualifier = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Name
A.nameConcrete ([Name] -> [Name]) -> (QName -> [Name]) -> QName -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Name]
A.mnameToList (ModuleName -> [Name]) -> (QName -> ModuleName) -> QName -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
A.qnameModule
bindingSite :: I.QName -> Range
bindingSite :: QName -> Range
bindingSite = Name -> Range
A.nameBindingSite (Name -> Range) -> (QName -> Name) -> QName -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName
storeDisambiguatedName :: A.QName -> TCM ()
storeDisambiguatedName :: QName -> TCM ()
storeDisambiguatedName q :: QName
q = Maybe VerboseLevel -> (VerboseLevel -> TCM ()) -> TCM ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust (Range -> Maybe VerboseLevel
forall b a. Num b => Range' a -> Maybe b
start (Range -> Maybe VerboseLevel) -> Range -> Maybe VerboseLevel
forall a b. (a -> b) -> a -> b
$ QName -> Range
forall t. HasRange t => t -> Range
getRange QName
q) ((VerboseLevel -> TCM ()) -> TCM ())
-> (VerboseLevel -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ i :: VerboseLevel
i ->
Lens' DisambiguatedNames TCState
stDisambiguatedNames Lens' DisambiguatedNames TCState
-> (DisambiguatedNames -> DisambiguatedNames) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` VerboseLevel -> QName -> DisambiguatedNames -> DisambiguatedNames
forall a. VerboseLevel -> a -> IntMap a -> IntMap a
IntMap.insert VerboseLevel
i QName
q
where
start :: Range' a -> Maybe b
start r :: Range' a
r = Int32 -> b
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> b) -> (Position' () -> Int32) -> Position' () -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Position' () -> Int32
forall a. Position' a -> Int32
P.posPos (Position' () -> b) -> Maybe (Position' ()) -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Range' a -> Maybe (Position' ())
forall a. Range' a -> Maybe (Position' ())
P.rStart' Range' a
r
disambiguateRecordFields
:: [C.Name]
-> [A.QName]
-> TCM ()
disambiguateRecordFields :: [Name] -> [QName] -> TCM ()
disambiguateRecordFields cxs :: [Name]
cxs axs :: [QName]
axs = [Name] -> (Name -> TCM ()) -> TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Name]
cxs ((Name -> TCM ()) -> TCM ()) -> (Name -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ cx :: Name
cx -> do
Maybe QName -> TCM () -> (QName -> TCM ()) -> TCM ()
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe ((QName -> Bool) -> [QName] -> Maybe QName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((Name
cx Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
==) (Name -> Bool) -> (QName -> Name) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Name
A.nameConcrete (Name -> Name) -> (QName -> Name) -> QName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Name
A.qnameName) [QName]
axs) (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((QName -> TCM ()) -> TCM ()) -> (QName -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ ax :: QName
ax -> do
QName -> TCM ()
storeDisambiguatedName QName
ax { qnameName :: Name
A.qnameName = (QName -> Name
A.qnameName QName
ax) { nameConcrete :: Name
A.nameConcrete = Name
cx } }