module Agda.TypeChecking.Monad.Base where
import Prelude hiding (null)
import qualified Control.Concurrent as C
import qualified Control.Exception as E
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Trans.Maybe
import Control.Applicative hiding (empty)
import Data.Function
import Data.Int
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Semigroup (Semigroup, Monoid, (<>), mempty, mappend, Any(..))
import Data.Typeable (Typeable)
import Data.Foldable (Foldable)
import Data.Traversable
import Data.IORef
import qualified System.Console.Haskeline as Haskeline
import Agda.Benchmarking (Benchmark, Phase)
import Agda.Syntax.Concrete (TopLevelModuleName)
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Definitions as D
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract (AllNames)
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern ()
import Agda.Syntax.Internal.Generic (TermLike(..))
import Agda.Syntax.Parser (PM(..), ParseWarning, runPMIO)
import Agda.Syntax.Treeless (Compiled)
import Agda.Syntax.Fixity
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import qualified Agda.Syntax.Info as Info
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Free.Lazy (Free'(freeVars'), bind', bind)
import Agda.Interaction.Options
import Agda.Interaction.Response
(InteractionOutputCallback, defaultInteractionOutputCallback)
import Agda.Interaction.Highlighting.Precise
(CompressedFile, HighlightingInfo)
import qualified Agda.Compiler.UHC.Pragmas.Base as CR
import Agda.Utils.Except
( Error(strMsg)
, ExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.Benchmark (MonadBench(..))
import Agda.Utils.FileName
import Agda.Utils.HashMap (HashMap)
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Hash
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty hiding ((<>))
import Agda.Utils.Singleton
import Agda.Utils.Functor
#include "undefined.h"
import Agda.Utils.Impossible
data TCState = TCSt
{ stPreScopeState :: !PreScopeState
, stPostScopeState :: !PostScopeState
, stPersistentState :: !PersistentTCState
}
class Monad m => ReadTCState m where
getTCState :: m TCState
instance Show TCState where
show _ = "TCSt{}"
data PreScopeState = PreScopeState
{ stPreTokens :: !CompressedFile
, stPreImports :: !Signature
, stPreImportedModules :: !(Set ModuleName)
, stPreModuleToSource :: !ModuleToSource
, stPreVisitedModules :: !VisitedModules
, stPreScope :: !ScopeInfo
, stPrePatternSyns :: !A.PatternSynDefns
, stPrePatternSynImports :: !A.PatternSynDefns
, stPrePragmaOptions :: !PragmaOptions
, stPreImportedBuiltins :: !(BuiltinThings PrimFun)
, stPreImportedDisplayForms :: !DisplayForms
, stPreImportedInstanceDefs :: !InstanceTable
, stPreHaskellImports :: !(Set String)
, stPreHaskellImportsUHC :: !(Set String)
, stPreHaskellCode :: ![String]
, stPreFreshInteractionId :: !InteractionId
}
type DisambiguatedNames = IntMap A.QName
data PostScopeState = PostScopeState
{ stPostSyntaxInfo :: !CompressedFile
, stPostDisambiguatedNames :: !DisambiguatedNames
, stPostMetaStore :: !MetaStore
, stPostInteractionPoints :: !InteractionPoints
, stPostSolvedInteractionPoints :: !InteractionPoints
, stPostAwakeConstraints :: !Constraints
, stPostSleepingConstraints :: !Constraints
, stPostDirty :: !Bool
, stPostOccursCheckDefs :: !(Set QName)
, stPostSignature :: !Signature
, stPostModuleParameters :: !ModuleParamDict
, stPostImportsDisplayForms :: !DisplayForms
, stPostCurrentModule :: !(Maybe ModuleName)
, stPostInstanceDefs :: !TempInstanceTable
, stPostStatistics :: !Statistics
, stPostTCWarnings :: ![TCWarning]
, stPostMutualBlocks :: !(Map MutualId MutualBlock)
, stPostLocalBuiltins :: !(BuiltinThings PrimFun)
, stPostFreshMetaId :: !MetaId
, stPostFreshMutualId :: !MutualId
, stPostFreshCtxId :: !CtxId
, stPostFreshProblemId :: !ProblemId
, stPostFreshInt :: !Int
, stPostFreshNameId :: !NameId
}
data MutualBlock = MutualBlock
{ mutualInfo :: Info.MutualInfo
, mutualNames :: Set QName
} deriving (Show, Eq)
instance Null MutualBlock where
empty = MutualBlock empty empty
data PersistentTCState = PersistentTCSt
{ stDecodedModules :: DecodedModules
, stPersistentOptions :: CommandLineOptions
, stInteractionOutputCallback :: InteractionOutputCallback
, stBenchmark :: !Benchmark
, stAccumStatistics :: !Statistics
, stLoadedFileCache :: !(Maybe LoadedFileCache)
}
data LoadedFileCache = LoadedFileCache
{ lfcCached :: !CachedTypeCheckLog
, lfcCurrent :: !CurrentTypeCheckLog
}
type CachedTypeCheckLog = [(TypeCheckAction, PostScopeState)]
type CurrentTypeCheckLog = [(TypeCheckAction, PostScopeState)]
data TypeCheckAction
= EnterSection !Info.ModuleInfo !ModuleName ![A.TypedBindings]
| LeaveSection !ModuleName
| Decl !A.Declaration
| Pragmas !PragmaOptions
initPersistentState :: PersistentTCState
initPersistentState = PersistentTCSt
{ stPersistentOptions = defaultOptions
, stDecodedModules = Map.empty
, stInteractionOutputCallback = defaultInteractionOutputCallback
, stBenchmark = empty
, stAccumStatistics = Map.empty
, stLoadedFileCache = Nothing
}
initPreScopeState :: PreScopeState
initPreScopeState = PreScopeState
{ stPreTokens = mempty
, stPreImports = emptySignature
, stPreImportedModules = Set.empty
, stPreModuleToSource = Map.empty
, stPreVisitedModules = Map.empty
, stPreScope = emptyScopeInfo
, stPrePatternSyns = Map.empty
, stPrePatternSynImports = Map.empty
, stPrePragmaOptions = defaultInteractionOptions
, stPreImportedBuiltins = Map.empty
, stPreImportedDisplayForms = HMap.empty
, stPreImportedInstanceDefs = Map.empty
, stPreHaskellImports = Set.empty
, stPreHaskellImportsUHC = Set.empty
, stPreHaskellCode = []
, stPreFreshInteractionId = 0
}
initPostScopeState :: PostScopeState
initPostScopeState = PostScopeState
{ stPostSyntaxInfo = mempty
, stPostDisambiguatedNames = IntMap.empty
, stPostMetaStore = Map.empty
, stPostInteractionPoints = Map.empty
, stPostSolvedInteractionPoints = Map.empty
, stPostAwakeConstraints = []
, stPostSleepingConstraints = []
, stPostDirty = False
, stPostOccursCheckDefs = Set.empty
, stPostSignature = emptySignature
, stPostModuleParameters = Map.empty
, stPostImportsDisplayForms = HMap.empty
, stPostCurrentModule = Nothing
, stPostInstanceDefs = (Map.empty , Set.empty)
, stPostStatistics = Map.empty
, stPostTCWarnings = []
, stPostMutualBlocks = Map.empty
, stPostLocalBuiltins = Map.empty
, stPostFreshMetaId = 0
, stPostFreshMutualId = 0
, stPostFreshCtxId = 0
, stPostFreshProblemId = 1
, stPostFreshInt = 0
, stPostFreshNameId = NameId 0 0
}
initState :: TCState
initState = TCSt
{ stPreScopeState = initPreScopeState
, stPostScopeState = initPostScopeState
, stPersistentState = initPersistentState
}
stTokens :: Lens' CompressedFile TCState
stTokens f s =
f (stPreTokens (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreTokens = x}}
stImports :: Lens' Signature TCState
stImports f s =
f (stPreImports (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImports = x}}
stImportedModules :: Lens' (Set ModuleName) TCState
stImportedModules f s =
f (stPreImportedModules (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedModules = x}}
stModuleToSource :: Lens' ModuleToSource TCState
stModuleToSource f s =
f (stPreModuleToSource (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreModuleToSource = x}}
stVisitedModules :: Lens' VisitedModules TCState
stVisitedModules f s =
f (stPreVisitedModules (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreVisitedModules = x}}
stScope :: Lens' ScopeInfo TCState
stScope f s =
f (stPreScope (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreScope = x}}
stPatternSyns :: Lens' A.PatternSynDefns TCState
stPatternSyns f s =
f (stPrePatternSyns (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPrePatternSyns = x}}
stPatternSynImports :: Lens' A.PatternSynDefns TCState
stPatternSynImports f s =
f (stPrePatternSynImports (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPrePatternSynImports = x}}
stPragmaOptions :: Lens' PragmaOptions TCState
stPragmaOptions f s =
f (stPrePragmaOptions (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPrePragmaOptions = x}}
stImportedBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stImportedBuiltins f s =
f (stPreImportedBuiltins (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedBuiltins = x}}
stHaskellImports :: Lens' (Set String) TCState
stHaskellImports f s =
f (stPreHaskellImports (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreHaskellImports = x}}
stHaskellImportsUHC :: Lens' (Set String) TCState
stHaskellImportsUHC f s =
f (stPreHaskellImportsUHC (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreHaskellImportsUHC = x}}
stHaskellCode :: Lens' [String] TCState
stHaskellCode f s =
f (stPreHaskellCode (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreHaskellCode = x}}
stFreshInteractionId :: Lens' InteractionId TCState
stFreshInteractionId f s =
f (stPreFreshInteractionId (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreFreshInteractionId = x}}
stFreshNameId :: Lens' NameId TCState
stFreshNameId f s =
f (stPostFreshNameId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshNameId = x}}
stSyntaxInfo :: Lens' CompressedFile TCState
stSyntaxInfo f s =
f (stPostSyntaxInfo (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostSyntaxInfo = x}}
stDisambiguatedNames :: Lens' DisambiguatedNames TCState
stDisambiguatedNames f s =
f (stPostDisambiguatedNames (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostDisambiguatedNames = x}}
stMetaStore :: Lens' MetaStore TCState
stMetaStore f s =
f (stPostMetaStore (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostMetaStore = x}}
stInteractionPoints :: Lens' InteractionPoints TCState
stInteractionPoints f s =
f (stPostInteractionPoints (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostInteractionPoints = x}}
stSolvedInteractionPoints :: Lens' InteractionPoints TCState
stSolvedInteractionPoints f s =
f (stPostSolvedInteractionPoints (stPostScopeState s)) <&>
\ x -> s {stPostScopeState = (stPostScopeState s)
{stPostSolvedInteractionPoints = x}}
stAwakeConstraints :: Lens' Constraints TCState
stAwakeConstraints f s =
f (stPostAwakeConstraints (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostAwakeConstraints = x}}
stSleepingConstraints :: Lens' Constraints TCState
stSleepingConstraints f s =
f (stPostSleepingConstraints (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostSleepingConstraints = x}}
stDirty :: Lens' Bool TCState
stDirty f s =
f (stPostDirty (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostDirty = x}}
stOccursCheckDefs :: Lens' (Set QName) TCState
stOccursCheckDefs f s =
f (stPostOccursCheckDefs (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostOccursCheckDefs = x}}
stSignature :: Lens' Signature TCState
stSignature f s =
f (stPostSignature (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostSignature = x}}
stModuleParameters :: Lens' (ModuleParamDict) TCState
stModuleParameters f s =
f (stPostModuleParameters (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostModuleParameters = x}}
stImportsDisplayForms :: Lens' DisplayForms TCState
stImportsDisplayForms f s =
f (stPostImportsDisplayForms (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostImportsDisplayForms = x}}
stImportedDisplayForms :: Lens' DisplayForms TCState
stImportedDisplayForms f s =
f (stPreImportedDisplayForms (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedDisplayForms = x}}
stCurrentModule :: Lens' (Maybe ModuleName) TCState
stCurrentModule f s =
f (stPostCurrentModule (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostCurrentModule = x}}
stImportedInstanceDefs :: Lens' InstanceTable TCState
stImportedInstanceDefs f s =
f (stPreImportedInstanceDefs (stPreScopeState s)) <&>
\x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedInstanceDefs = x}}
stInstanceDefs :: Lens' TempInstanceTable TCState
stInstanceDefs f s =
f (stPostInstanceDefs (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostInstanceDefs = x}}
stStatistics :: Lens' Statistics TCState
stStatistics f s =
f (stPostStatistics (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostStatistics = x}}
stTCWarnings :: Lens' [TCWarning] TCState
stTCWarnings f s =
f (stPostTCWarnings (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostTCWarnings = x}}
stMutualBlocks :: Lens' (Map MutualId MutualBlock) TCState
stMutualBlocks f s =
f (stPostMutualBlocks (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostMutualBlocks = x}}
stLocalBuiltins :: Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins f s =
f (stPostLocalBuiltins (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostLocalBuiltins = x}}
stFreshMetaId :: Lens' MetaId TCState
stFreshMetaId f s =
f (stPostFreshMetaId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshMetaId = x}}
stFreshMutualId :: Lens' MutualId TCState
stFreshMutualId f s =
f (stPostFreshMutualId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshMutualId = x}}
stFreshCtxId :: Lens' CtxId TCState
stFreshCtxId f s =
f (stPostFreshCtxId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshCtxId = x}}
stFreshProblemId :: Lens' ProblemId TCState
stFreshProblemId f s =
f (stPostFreshProblemId (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshProblemId = x}}
stFreshInt :: Lens' Int TCState
stFreshInt f s =
f (stPostFreshInt (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostFreshInt = x}}
stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings s = (s^.stLocalBuiltins) `Map.union` (s^.stImportedBuiltins)
class Enum i => HasFresh i where
freshLens :: Lens' i TCState
nextFresh' :: i -> i
nextFresh' = succ
nextFresh :: HasFresh i => TCState -> (i, TCState)
nextFresh s =
let !c = s^.freshLens
in (c, set freshLens (nextFresh' c) s)
fresh :: (HasFresh i, MonadState TCState m) => m i
fresh =
do !s <- get
let (!c , !s') = nextFresh s
put s'
return c
instance HasFresh MetaId where
freshLens = stFreshMetaId
instance HasFresh MutualId where
freshLens = stFreshMutualId
instance HasFresh InteractionId where
freshLens = stFreshInteractionId
instance HasFresh NameId where
freshLens = stFreshNameId
nextFresh' = succ . succ
instance HasFresh CtxId where
freshLens = stFreshCtxId
instance HasFresh Int where
freshLens = stFreshInt
newtype ProblemId = ProblemId Nat
deriving (Typeable, Eq, Ord, Enum, Real, Integral, Num)
instance Show ProblemId where
show (ProblemId n) = show n
instance Pretty ProblemId where
pretty (ProblemId n) = pretty n
instance HasFresh ProblemId where
freshLens = stFreshProblemId
freshName :: (MonadState TCState m, HasFresh NameId) => Range -> String -> m Name
freshName r s = do
i <- fresh
return $ mkName r i s
freshNoName :: (MonadState TCState m, HasFresh NameId) => Range -> m Name
freshNoName r =
do i <- fresh
return $ Name i (C.NoName noRange i) r noFixity'
freshNoName_ :: (MonadState TCState m, HasFresh NameId) => m Name
freshNoName_ = freshNoName noRange
class FreshName a where
freshName_ :: (MonadState TCState m, HasFresh NameId) => a -> m Name
instance FreshName (Range, String) where
freshName_ = uncurry freshName
instance FreshName String where
freshName_ = freshName noRange
instance FreshName Range where
freshName_ = freshNoName
instance FreshName () where
freshName_ () = freshNoName_
type ModuleToSource = Map TopLevelModuleName AbsolutePath
type SourceToModule = Map AbsolutePath TopLevelModuleName
sourceToModule :: TCM SourceToModule
sourceToModule =
Map.fromList
. List.map (\(m, f) -> (f, m))
. Map.toList
<$> use stModuleToSource
lookupModuleFromSource :: AbsolutePath -> TCM (Maybe TopLevelModuleName)
lookupModuleFromSource f =
fmap fst . List.find ((f ==) . snd) . Map.toList <$> use stModuleToSource
data ModuleInfo = ModuleInfo
{ miInterface :: Interface
, miWarnings :: Bool
}
type VisitedModules = Map C.TopLevelModuleName ModuleInfo
type DecodedModules = Map C.TopLevelModuleName Interface
data Interface = Interface
{ iSourceHash :: Hash
, iImportedModules :: [(ModuleName, Hash)]
, iModuleName :: ModuleName
, iScope :: Map ModuleName Scope
, iInsideScope :: ScopeInfo
, iSignature :: Signature
, iDisplayForms :: DisplayForms
, iBuiltin :: BuiltinThings (String, QName)
, iHaskellImports :: Set String
, iHaskellImportsUHC :: Set String
, iHaskellCode :: [String]
, iHighlighting :: HighlightingInfo
, iPragmaOptions :: [OptionsPragma]
, iPatternSyns :: A.PatternSynDefns
}
deriving (Typeable, Show)
instance Pretty Interface where
pretty (Interface sourceH importedM moduleN scope insideS signature display builtin
haskellI haskellIUHC haskellCode highlighting pragmaO patternS) =
hang (text "Interface") 2 $ vcat
[ text "source hash:" <+> (pretty . show) sourceH
, text "imported modules:" <+> (pretty . show) importedM
, text "module name:" <+> pretty moduleN
, text "scope:" <+> (pretty . show) scope
, text "inside scope:" <+> (pretty . show) insideS
, text "signature:" <+> (pretty . show) signature
, text "display:" <+> (pretty . show) display
, text "builtin:" <+> (pretty . show) builtin
, text "Haskell imports:" <+> (pretty . show) haskellI
, text "Haskell imports UHC:" <+> (pretty . show) haskellIUHC
, text "Haskell code:" <+> (vcat $ map (vcat . map text . lines) $ reverse haskellCode)
, text "highlighting:" <+> (pretty . show) highlighting
, text "pragma options:" <+> (pretty . show) pragmaO
, text "pattern syns:" <+> (pretty . show) patternS
]
iFullHash :: Interface -> Hash
iFullHash i = combineHashes $ iSourceHash i : List.map snd (iImportedModules i)
data Closure a = Closure
{ clSignature :: Signature
, clEnv :: TCEnv
, clScope :: ScopeInfo
, clModuleParameters :: ModuleParamDict
, clValue :: a
}
deriving (Typeable, Functor, Foldable)
instance Show a => Show (Closure a) where
show cl = "Closure " ++ show (clValue cl)
instance HasRange a => HasRange (Closure a) where
getRange = getRange . clValue
buildClosure :: a -> TCM (Closure a)
buildClosure x = do
env <- ask
sig <- use stSignature
scope <- use stScope
pars <- use stModuleParameters
return $ Closure sig env scope pars x
type Constraints = [ProblemConstraint]
data ProblemConstraint = PConstr
{ constraintProblems :: [ProblemId]
, theConstraint :: Closure Constraint
}
deriving (Typeable, Show)
instance HasRange ProblemConstraint where
getRange = getRange . theConstraint
data Constraint
= ValueCmp Comparison Type Term Term
| ElimCmp [Polarity] Type Term [Elim] [Elim]
| TypeCmp Comparison Type Type
| TelCmp Type Type Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| LevelCmp Comparison Level Level
| UnBlock MetaId
| Guarded Constraint ProblemId
| IsEmpty Range Type
| CheckSizeLtSat Term
| FindInScope MetaId (Maybe MetaId) (Maybe [Candidate])
deriving (Typeable, Show)
instance HasRange Constraint where
getRange (IsEmpty r t) = r
getRange _ = noRange
instance Free' Constraint c where
freeVars' c =
case c of
ValueCmp _ t u v -> freeVars' (t, (u, v))
ElimCmp _ t u es es' -> freeVars' ((t, u), (es, es'))
TypeCmp _ t t' -> freeVars' (t, t')
TelCmp _ _ _ tel tel' -> freeVars' (tel, tel')
SortCmp _ s s' -> freeVars' (s, s')
LevelCmp _ l l' -> freeVars' (l, l')
UnBlock _ -> mempty
Guarded c _ -> freeVars' c
IsEmpty _ t -> freeVars' t
CheckSizeLtSat u -> freeVars' u
FindInScope _ _ cs -> freeVars' cs
instance TermLike Constraint where
foldTerm f = \case
ValueCmp _ t u v -> foldTerm f (t, u, v)
ElimCmp _ t u es es' -> foldTerm f (t, u, es, es')
TypeCmp _ t t' -> foldTerm f (t, t')
LevelCmp _ l l' -> foldTerm f (l, l')
IsEmpty _ t -> foldTerm f t
CheckSizeLtSat u -> foldTerm f u
TelCmp _ _ _ tel1 tel2 -> __IMPOSSIBLE__
SortCmp _ s1 s2 -> __IMPOSSIBLE__
UnBlock _ -> __IMPOSSIBLE__
Guarded c _ -> __IMPOSSIBLE__
FindInScope _ _ cs -> __IMPOSSIBLE__
traverseTerm f c = __IMPOSSIBLE__
traverseTermM f c = __IMPOSSIBLE__
data Comparison = CmpEq | CmpLeq
deriving (Eq, Typeable)
instance Show Comparison where
show CmpEq = "="
show CmpLeq = "=<"
instance Pretty Comparison where
pretty CmpEq = text "="
pretty CmpLeq = text "=<"
data CompareDirection = DirEq | DirLeq | DirGeq
deriving (Eq, Typeable)
instance Show CompareDirection where
show DirEq = "="
show DirLeq = "=<"
show DirGeq = ">="
fromCmp :: Comparison -> CompareDirection
fromCmp CmpEq = DirEq
fromCmp CmpLeq = DirLeq
flipCmp :: CompareDirection -> CompareDirection
flipCmp DirEq = DirEq
flipCmp DirLeq = DirGeq
flipCmp DirGeq = DirLeq
dirToCmp :: (Comparison -> a -> a -> c) -> CompareDirection -> a -> a -> c
dirToCmp cont DirEq = cont CmpEq
dirToCmp cont DirLeq = cont CmpLeq
dirToCmp cont DirGeq = flip $ cont CmpLeq
data Open a = OpenThing { openThingCtxIds :: [CtxId], openThing :: a }
deriving (Typeable, Show, Functor)
instance Decoration Open where
traverseF f (OpenThing cxt x) = OpenThing cxt <$> f x
data Local a = Local ModuleName a
| Global a
deriving (Typeable, Show, Functor, Foldable, Traversable)
isGlobal :: Local a -> Bool
isGlobal Global{} = True
isGlobal Local{} = False
instance Decoration Local where
traverseF f (Local m x) = Local m <$> f x
traverseF f (Global x) = Global <$> f x
data Judgement a
= HasType { jMetaId :: a, jMetaType :: Type }
| IsSort { jMetaId :: a, jMetaType :: Type }
deriving (Typeable)
instance Show a => Show (Judgement a) where
show (HasType a t) = show a ++ " : " ++ show t
show (IsSort a t) = show a ++ " :sort " ++ show t
data MetaVariable =
MetaVar { mvInfo :: MetaInfo
, mvPriority :: MetaPriority
, mvPermutation :: Permutation
, mvJudgement :: Judgement MetaId
, mvInstantiation :: MetaInstantiation
, mvListeners :: Set Listener
, mvFrozen :: Frozen
}
deriving (Typeable)
data Listener = EtaExpand MetaId
| CheckConstraint Nat ProblemConstraint
deriving (Typeable)
instance Eq Listener where
EtaExpand x == EtaExpand y = x == y
CheckConstraint x _ == CheckConstraint y _ = x == y
_ == _ = False
instance Ord Listener where
EtaExpand x `compare` EtaExpand y = x `compare` y
CheckConstraint x _ `compare` CheckConstraint y _ = x `compare` y
EtaExpand{} `compare` CheckConstraint{} = LT
CheckConstraint{} `compare` EtaExpand{} = GT
data Frozen
= Frozen
| Instantiable
deriving (Eq, Show)
data MetaInstantiation
= InstV [Arg String] Term
| Open
| OpenIFS
| BlockedConst Term
| PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)
deriving (Typeable)
data TypeCheckingProblem
= CheckExpr A.Expr Type
| CheckArgs ExpandHidden Range [NamedArg A.Expr] Type Type (Args -> Type -> TCM Term)
| CheckLambda (Arg ([WithHiding Name], Maybe Type)) A.Expr Type
| UnquoteTactic Term Term Type
deriving (Typeable)
instance Show MetaInstantiation where
show (InstV tel t) = "InstV " ++ show tel ++ " (" ++ show t ++ ")"
show Open = "Open"
show OpenIFS = "OpenIFS"
show (BlockedConst t) = "BlockedConst (" ++ show t ++ ")"
show (PostponedTypeCheckingProblem{}) = "PostponedTypeCheckingProblem (...)"
newtype MetaPriority = MetaPriority Int
deriving (Eq, Ord, Show)
data RunMetaOccursCheck
= RunMetaOccursCheck
| DontRunMetaOccursCheck
deriving (Eq, Ord, Show)
data MetaInfo = MetaInfo
{ miClosRange :: Closure Range
, miMetaOccursCheck :: RunMetaOccursCheck
, miNameSuggestion :: MetaNameSuggestion
}
type MetaNameSuggestion = String
data NamedMeta = NamedMeta
{ nmSuggestion :: MetaNameSuggestion
, nmid :: MetaId
}
instance Pretty NamedMeta where
pretty (NamedMeta "" x) = pretty x
pretty (NamedMeta s x) = text $ "_" ++ s ++ prettyShow x
type MetaStore = Map MetaId MetaVariable
instance HasRange MetaInfo where
getRange = clValue . miClosRange
instance HasRange MetaVariable where
getRange m = getRange $ getMetaInfo m
instance SetRange MetaInfo where
setRange r m = m { miClosRange = (miClosRange m) { clValue = r }}
instance SetRange MetaVariable where
setRange r m = m { mvInfo = setRange r (mvInfo m) }
normalMetaPriority :: MetaPriority
normalMetaPriority = MetaPriority 0
lowMetaPriority :: MetaPriority
lowMetaPriority = MetaPriority (10)
highMetaPriority :: MetaPriority
highMetaPriority = MetaPriority 10
getMetaInfo :: MetaVariable -> Closure Range
getMetaInfo = miClosRange . mvInfo
getMetaScope :: MetaVariable -> ScopeInfo
getMetaScope m = clScope $ getMetaInfo m
getMetaEnv :: MetaVariable -> TCEnv
getMetaEnv m = clEnv $ getMetaInfo m
getMetaSig :: MetaVariable -> Signature
getMetaSig m = clSignature $ getMetaInfo m
getMetaRelevance :: MetaVariable -> Relevance
getMetaRelevance = envRelevance . getMetaEnv
data InteractionPoint = InteractionPoint
{ ipRange :: Range
, ipMeta :: Maybe MetaId
, ipClause:: IPClause
}
instance Eq InteractionPoint where (==) = (==) `on` ipMeta
type InteractionPoints = Map InteractionId InteractionPoint
data IPClause = IPClause
{ ipcQName :: QName
, ipcClauseNo :: Int
, ipcClause :: A.RHS
}
| IPNoClause
instance Eq IPClause where
IPNoClause == IPNoClause = True
IPClause x i _ == IPClause x' i' _ = x == x' && i == i'
_ == _ = False
data Signature = Sig
{ _sigSections :: Sections
, _sigDefinitions :: Definitions
, _sigRewriteRules:: RewriteRuleMap
}
deriving (Typeable, Show)
sigSections :: Lens' Sections Signature
sigSections f s =
f (_sigSections s) <&>
\x -> s {_sigSections = x}
sigDefinitions :: Lens' Definitions Signature
sigDefinitions f s =
f (_sigDefinitions s) <&>
\x -> s {_sigDefinitions = x}
sigRewriteRules :: Lens' RewriteRuleMap Signature
sigRewriteRules f s =
f (_sigRewriteRules s) <&>
\x -> s {_sigRewriteRules = x}
type Sections = Map ModuleName Section
type Definitions = HashMap QName Definition
type RewriteRuleMap = HashMap QName RewriteRules
type DisplayForms = HashMap QName [LocalDisplayForm]
data Section = Section { _secTelescope :: Telescope }
deriving (Typeable, Show)
secTelescope :: Lens' Telescope Section
secTelescope f s =
f (_secTelescope s) <&>
\x -> s {_secTelescope = x}
emptySignature :: Signature
emptySignature = Sig Map.empty HMap.empty HMap.empty
data DisplayForm = Display
{ dfFreeVars :: Nat
, dfPats :: Elims
, dfRHS :: DisplayTerm
}
deriving (Typeable, Show)
type LocalDisplayForm = Local DisplayForm
data DisplayTerm
= DWithApp DisplayTerm [DisplayTerm] Elims
| DCon ConHead ConInfo [Arg DisplayTerm]
| DDef QName [Elim' DisplayTerm]
| DDot Term
| DTerm Term
deriving (Typeable, Show)
instance Free' DisplayForm c where
freeVars' (Display n ps t) = bind (freeVars' ps) `mappend` bind' n (freeVars' t)
instance Free' DisplayTerm c where
freeVars' (DWithApp t ws es) = freeVars' (t, (ws, es))
freeVars' (DCon _ _ vs) = freeVars' vs
freeVars' (DDef _ es) = freeVars' es
freeVars' (DDot v) = freeVars' v
freeVars' (DTerm v) = freeVars' v
defaultDisplayForm :: QName -> [LocalDisplayForm]
defaultDisplayForm c = []
defRelevance :: Definition -> Relevance
defRelevance = argInfoRelevance . defArgInfo
data NLPat
= PVar (Maybe CtxId) !Int [Arg Int]
| PWild
| PDef QName PElims
| PLam ArgInfo (Abs NLPat)
| PPi (Dom NLPType) (Abs NLPType)
| PBoundVar !Int PElims
| PTerm Term
deriving (Typeable, Show)
type PElims = [Elim' NLPat]
data NLPType = NLPType
{ nlpTypeLevel :: NLPat
, nlpTypeUnEl :: NLPat
} deriving (Typeable, Show)
type RewriteRules = [RewriteRule]
data RewriteRule = RewriteRule
{ rewName :: QName
, rewContext :: Telescope
, rewHead :: QName
, rewPats :: PElims
, rewRHS :: Term
, rewType :: Type
}
deriving (Typeable, Show)
data Definition = Defn
{ defArgInfo :: ArgInfo
, defName :: QName
, defType :: Type
, defPolarity :: [Polarity]
, defArgOccurrences :: [Occurrence]
, defDisplay :: [LocalDisplayForm]
, defMutual :: MutualId
, defCompiledRep :: CompiledRepresentation
, defInstance :: Maybe QName
, defCopy :: Bool
, defMatchable :: Bool
, theDef :: Defn
}
deriving (Typeable, Show)
theDefLens :: Lens' Defn Definition
theDefLens f d = f (theDef d) <&> \ df -> d { theDef = df }
defaultDefn :: ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn info x t def = Defn
{ defArgInfo = info
, defName = x
, defType = t
, defPolarity = []
, defArgOccurrences = []
, defDisplay = defaultDisplayForm x
, defMutual = 0
, defCompiledRep = noCompiledRep
, defInstance = Nothing
, defCopy = False
, defMatchable = False
, theDef = def
}
type HaskellCode = String
type HaskellType = String
type EpicCode = String
type JSCode = String
data HaskellRepresentation
= HsDefn HaskellType HaskellCode
| HsType HaskellType
deriving (Typeable, Show)
data HaskellExport = HsExport HaskellType String deriving (Show, Typeable)
data CoreRepresentation
= CrDefn CR.CoreExpr
| CrType CR.CoreType
| CrConstr CR.CoreConstr
deriving (Typeable, Show)
data Polarity
= Covariant
| Contravariant
| Invariant
| Nonvariant
deriving (Typeable, Show, Eq)
data CompiledRepresentation = CompiledRep
{ compiledHaskell :: Maybe HaskellRepresentation
, exportHaskell :: Maybe HaskellExport
, compiledEpic :: Maybe EpicCode
, compiledJS :: Maybe JSCode
, compiledCore :: Maybe CoreRepresentation
}
deriving (Typeable, Show)
noCompiledRep :: CompiledRepresentation
noCompiledRep = CompiledRep Nothing Nothing Nothing Nothing Nothing
data ExtLamInfo = ExtLamInfo
{ extLamNumHidden :: Int
, extLamNumNonHid :: Int
} deriving (Typeable, Eq, Ord, Show)
data Projection = Projection
{ projProper :: Bool
, projOrig :: QName
, projFromType :: Arg QName
, projIndex :: Int
, projLams :: ProjLams
} deriving (Typeable, Show)
newtype ProjLams = ProjLams { getProjLams :: [Arg ArgName] }
deriving (Typeable, Show, Null)
projDropPars :: Projection -> ProjOrigin -> Term
projDropPars (Projection True d _ _ lams) o =
case initLast $ getProjLams lams of
Nothing -> Def d []
Just (pars, Arg i y) ->
let core = Lam i $ Abs y $ Var 0 [Proj o d] in
List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) core pars
projDropPars (Projection False _ _ _ lams) o | null lams = __IMPOSSIBLE__
projDropPars (Projection False d _ _ lams) o =
List.foldr (\ (Arg ai x) -> Lam ai . NoAbs x) (Def d []) $ init $ getProjLams lams
projArgInfo :: Projection -> ArgInfo
projArgInfo (Projection _ _ _ _ lams) =
maybe __IMPOSSIBLE__ getArgInfo $ lastMaybe $ getProjLams lams
data EtaEquality
= Specified !Bool
| Inferred !Bool
deriving (Typeable, Show, Eq)
etaEqualityToBool :: EtaEquality -> Bool
etaEqualityToBool (Specified b) = b
etaEqualityToBool (Inferred b) = b
setEtaEquality :: EtaEquality -> Bool -> EtaEquality
setEtaEquality e@Specified{} _ = e
setEtaEquality _ b = Inferred b
data FunctionFlag
= FunStatic
| FunInline
| FunMacro
deriving (Typeable, Eq, Ord, Enum, Show)
data Defn = Axiom
| AbstractDefn
| Function
{ funClauses :: [Clause]
, funCompiled :: Maybe CompiledClauses
, funTreeless :: Maybe Compiled
, funInv :: FunctionInverse
, funMutual :: [QName]
, funAbstr :: IsAbstract
, funDelayed :: Delayed
, funProjection :: Maybe Projection
, funFlags :: Set FunctionFlag
, funTerminates :: Maybe Bool
, funExtLam :: Maybe ExtLamInfo
, funWith :: Maybe QName
, funCopatternLHS :: Bool
}
| Datatype
{ dataPars :: Nat
, dataSmallPars :: Permutation
, dataNonLinPars :: Drop Permutation
, dataIxs :: Nat
, dataInduction :: Induction
, dataClause :: (Maybe Clause)
, dataCons :: [QName]
, dataSort :: Sort
, dataMutual :: [QName]
, dataAbstr :: IsAbstract
}
| Record
{ recPars :: Nat
, recClause :: Maybe Clause
, recConHead :: ConHead
, recNamedCon :: Bool
, recFields :: [Arg QName]
, recTel :: Telescope
, recMutual :: [QName]
, recEtaEquality' :: EtaEquality
, recInduction :: Maybe Induction
, recRecursive :: Bool
, recAbstr :: IsAbstract
}
| Constructor
{ conPars :: Nat
, conSrcCon :: ConHead
, conData :: QName
, conAbstr :: IsAbstract
, conInd :: Induction
, conErased :: [Bool]
}
| Primitive
{ primAbstr :: IsAbstract
, primName :: String
, primClauses :: [Clause]
, primCompiled :: Maybe CompiledClauses
}
deriving (Typeable, Show)
recEtaEquality :: Defn -> Bool
recEtaEquality = etaEqualityToBool . recEtaEquality'
emptyFunction :: Defn
emptyFunction = Function
{ funClauses = []
, funCompiled = Nothing
, funTreeless = Nothing
, funInv = NotInjective
, funMutual = []
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Nothing
, funFlags = Set.empty
, funTerminates = Nothing
, funExtLam = Nothing
, funWith = Nothing
, funCopatternLHS = False
}
funFlag :: FunctionFlag -> Lens' Bool Defn
funFlag flag f def@Function{ funFlags = flags } =
f (Set.member flag flags) <&>
\ b -> def{ funFlags = (if b then Set.insert else Set.delete) flag flags }
funFlag _ f def = f False <&> const def
funStatic, funInline, funMacro :: Lens' Bool Defn
funStatic = funFlag FunStatic
funInline = funFlag FunInline
funMacro = funFlag FunMacro
isMacro :: Defn -> Bool
isMacro = (^. funMacro)
isEmptyFunction :: Defn -> Bool
isEmptyFunction def =
case def of
Function { funClauses = [] } -> True
_ -> False
isCopatternLHS :: [Clause] -> Bool
isCopatternLHS = List.any (List.any (isJust . A.isProjP) . namedClausePats)
recCon :: Defn -> QName
recCon Record{ recConHead } = conName recConHead
recCon _ = __IMPOSSIBLE__
defIsRecord :: Defn -> Bool
defIsRecord Record{} = True
defIsRecord _ = False
defIsDataOrRecord :: Defn -> Bool
defIsDataOrRecord Record{} = True
defIsDataOrRecord Datatype{} = True
defIsDataOrRecord _ = False
newtype Fields = Fields [(C.Name, Type)]
deriving (Typeable, Null)
data Simplification = YesSimplification | NoSimplification
deriving (Typeable, Eq, Show)
instance Null Simplification where
empty = NoSimplification
null = (== NoSimplification)
instance Semigroup Simplification where
YesSimplification <> _ = YesSimplification
NoSimplification <> s = s
instance Monoid Simplification where
mempty = NoSimplification
mappend = (<>)
data Reduced no yes = NoReduction no | YesReduction Simplification yes
deriving (Typeable, Functor)
data IsReduced
= NotReduced
| Reduced (Blocked ())
data MaybeReduced a = MaybeRed
{ isReduced :: IsReduced
, ignoreReduced :: a
}
deriving (Functor)
instance IsProjElim e => IsProjElim (MaybeReduced e) where
isProjElim = isProjElim . ignoreReduced
type MaybeReducedArgs = [MaybeReduced (Arg Term)]
type MaybeReducedElims = [MaybeReduced Elim]
notReduced :: a -> MaybeReduced a
notReduced x = MaybeRed NotReduced x
reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced b = case fmap ignoreSharing <$> b of
NotBlocked _ (Arg _ (MetaV x _)) -> MaybeRed (Reduced $ Blocked x ()) v
_ -> MaybeRed (Reduced $ () <$ b) v
where
v = ignoreBlocking b
data AllowedReduction
= ProjectionReductions
| InlineReductions
| CopatternReductions
| FunctionReductions
| LevelReductions
| NonTerminatingReductions
deriving (Show, Eq, Ord, Enum, Bounded)
type AllowedReductions = [AllowedReduction]
allReductions :: AllowedReductions
allReductions = [minBound..pred maxBound]
data PrimFun = PrimFun
{ primFunName :: QName
, primFunArity :: Arity
, primFunImplementation :: [Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term)
}
deriving (Typeable)
defClauses :: Definition -> [Clause]
defClauses Defn{theDef = Function{funClauses = cs}} = cs
defClauses Defn{theDef = Primitive{primClauses = cs}} = cs
defClauses Defn{theDef = Datatype{dataClause = Just c}} = [c]
defClauses Defn{theDef = Record{recClause = Just c}} = [c]
defClauses _ = []
defCompiled :: Definition -> Maybe CompiledClauses
defCompiled Defn{theDef = Function {funCompiled = mcc}} = mcc
defCompiled Defn{theDef = Primitive{primCompiled = mcc}} = mcc
defCompiled _ = Nothing
defParameters :: Definition -> Maybe Nat
defParameters Defn{theDef = Datatype{dataPars = n}} = Just n
defParameters Defn{theDef = Record {recPars = n}} = Just n
defParameters _ = Nothing
defJSDef :: Definition -> Maybe JSCode
defJSDef = compiledJS . defCompiledRep
defEpicDef :: Definition -> Maybe EpicCode
defEpicDef = compiledEpic . defCompiledRep
defCoreDef :: Definition -> Maybe CoreRepresentation
defCoreDef = compiledCore . defCompiledRep
defDelayed :: Definition -> Delayed
defDelayed Defn{theDef = Function{funDelayed = d}} = d
defDelayed _ = NotDelayed
defNonterminating :: Definition -> Bool
defNonterminating Defn{theDef = Function{funTerminates = Just False}} = True
defNonterminating _ = False
defAbstract :: Definition -> IsAbstract
defAbstract d = case theDef d of
Axiom{} -> ConcreteDef
AbstractDefn{} -> AbstractDef
Function{funAbstr = a} -> a
Datatype{dataAbstr = a} -> a
Record{recAbstr = a} -> a
Constructor{conAbstr = a} -> a
Primitive{primAbstr = a} -> a
type FunctionInverse = FunctionInverse' Clause
data FunctionInverse' c
= NotInjective
| Inverse (Map TermHead c)
deriving (Typeable, Show, Functor)
data TermHead = SortHead
| PiHead
| ConsHead QName
deriving (Typeable, Eq, Ord, Show)
newtype MutualId = MutId Int32
deriving (Typeable, Eq, Ord, Show, Num, Enum)
type Statistics = Map String Integer
data Call = CheckClause Type A.SpineClause
| CheckPattern A.Pattern Telescope Type
| CheckLetBinding A.LetBinding
| InferExpr A.Expr
| CheckExprCall A.Expr Type
| CheckDotPattern A.Expr Term
| CheckPatternShadowing A.SpineClause
| CheckProjection Range QName Type
| IsTypeCall A.Expr Sort
| IsType_ A.Expr
| InferVar Name
| InferDef QName
| CheckArguments Range [NamedArg A.Expr] Type Type
| CheckDataDef Range Name [A.LamBinding] [A.Constructor]
| CheckRecDef Range Name [A.LamBinding] [A.Constructor]
| CheckConstructor QName Telescope Sort A.Constructor
| CheckFunDef Range Name [A.Clause]
| CheckPragma Range A.Pragma
| CheckPrimitive Range Name A.Expr
| CheckIsEmpty Range Type
| CheckWithFunctionType A.Expr
| CheckSectionApplication Range ModuleName A.ModuleApplication
| ScopeCheckExpr C.Expr
| ScopeCheckDeclaration D.NiceDeclaration
| ScopeCheckLHS C.QName C.Pattern
| NoHighlighting
| ModuleContents
| SetRange Range
deriving (Typeable)
instance Pretty Call where
pretty CheckClause{} = text "CheckClause"
pretty CheckPattern{} = text "CheckPattern"
pretty InferExpr{} = text "InferExpr"
pretty CheckExprCall{} = text "CheckExprCall"
pretty CheckLetBinding{} = text "CheckLetBinding"
pretty CheckProjection{} = text "CheckProjection"
pretty IsTypeCall{} = text "IsTypeCall"
pretty IsType_{} = text "IsType_"
pretty InferVar{} = text "InferVar"
pretty InferDef{} = text "InferDef"
pretty CheckArguments{} = text "CheckArguments"
pretty CheckDataDef{} = text "CheckDataDef"
pretty CheckRecDef{} = text "CheckRecDef"
pretty CheckConstructor{} = text "CheckConstructor"
pretty CheckFunDef{} = text "CheckFunDef"
pretty CheckPragma{} = text "CheckPragma"
pretty CheckPrimitive{} = text "CheckPrimitive"
pretty CheckWithFunctionType{} = text "CheckWithFunctionType"
pretty ScopeCheckExpr{} = text "ScopeCheckExpr"
pretty ScopeCheckDeclaration{} = text "ScopeCheckDeclaration"
pretty ScopeCheckLHS{} = text "ScopeCheckLHS"
pretty CheckDotPattern{} = text "CheckDotPattern"
pretty CheckPatternShadowing{} = text "CheckPatternShadowing"
pretty SetRange{} = text "SetRange"
pretty CheckSectionApplication{} = text "CheckSectionApplication"
pretty CheckIsEmpty{} = text "CheckIsEmpty"
pretty NoHighlighting{} = text "NoHighlighting"
pretty ModuleContents{} = text "ModuleContents"
instance HasRange Call where
getRange (CheckClause _ c) = getRange c
getRange (CheckPattern p _ _) = getRange p
getRange (InferExpr e) = getRange e
getRange (CheckExprCall e _) = getRange e
getRange (CheckLetBinding b) = getRange b
getRange (CheckProjection r _ _) = r
getRange (IsTypeCall e s) = getRange e
getRange (IsType_ e) = getRange e
getRange (InferVar x) = getRange x
getRange (InferDef f) = getRange f
getRange (CheckArguments r _ _ _) = r
getRange (CheckDataDef i _ _ _) = getRange i
getRange (CheckRecDef i _ _ _) = getRange i
getRange (CheckConstructor _ _ _ c) = getRange c
getRange (CheckFunDef i _ _) = getRange i
getRange (CheckPragma r _) = r
getRange (CheckPrimitive i _ _) = getRange i
getRange CheckWithFunctionType{} = noRange
getRange (ScopeCheckExpr e) = getRange e
getRange (ScopeCheckDeclaration d) = getRange d
getRange (ScopeCheckLHS _ p) = getRange p
getRange (CheckDotPattern e _) = getRange e
getRange (CheckPatternShadowing c) = getRange c
getRange (SetRange r) = r
getRange (CheckSectionApplication r _ _) = r
getRange (CheckIsEmpty r _) = r
getRange NoHighlighting = noRange
getRange ModuleContents = noRange
type InstanceTable = Map QName (Set QName)
type TempInstanceTable = (InstanceTable , Set QName)
data BuiltinDescriptor
= BuiltinData (TCM Type) [String]
| BuiltinDataCons (TCM Type)
| BuiltinPrim String (Term -> TCM ())
| BuiltinPostulate Relevance (TCM Type)
| BuiltinUnknown (Maybe (TCM Type)) (Term -> Type -> TCM ())
data BuiltinInfo =
BuiltinInfo { builtinName :: String
, builtinDesc :: BuiltinDescriptor }
type BuiltinThings pf = Map String (Builtin pf)
data Builtin pf
= Builtin Term
| Prim pf
deriving (Typeable, Show, Functor, Foldable, Traversable)
data HighlightingLevel
= None
| NonInteractive
| Interactive
deriving (Eq, Ord, Show, Read)
data HighlightingMethod
= Direct
| Indirect
deriving (Eq, Show, Read)
ifTopLevelAndHighlightingLevelIs ::
MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs l m = do
e <- ask
when (envModuleNestingLevel e == 0 &&
envHighlightingLevel e >= l)
m
data ModuleParameters = ModuleParams
{ mpSubstitution :: Substitution
} deriving (Typeable, Show)
defaultModuleParameters :: ModuleParameters
defaultModuleParameters = ModuleParams IdS
type ModuleParamDict = Map ModuleName ModuleParameters
data TCEnv =
TCEnv { envContext :: Context
, envLetBindings :: LetBindings
, envCurrentModule :: ModuleName
, envCurrentPath :: Maybe AbsolutePath
, envAnonymousModules :: [(ModuleName, Nat)]
, envImportPath :: [C.TopLevelModuleName]
, envMutualBlock :: Maybe MutualId
, envTerminationCheck :: TerminationCheck ()
, envSolvingConstraints :: Bool
, envCheckingWhere :: Bool
, envAssignMetas :: Bool
, envActiveProblems :: [ProblemId]
, envAbstractMode :: AbstractMode
, envRelevance :: Relevance
, envDisplayFormsEnabled :: Bool
, envRange :: Range
, envHighlightingRange :: Range
, envClause :: IPClause
, envCall :: Maybe (Closure Call)
, envHighlightingLevel :: HighlightingLevel
, envHighlightingMethod :: HighlightingMethod
, envModuleNestingLevel :: !Int
, envAllowDestructiveUpdate :: Bool
, envExpandLast :: ExpandHidden
, envAppDef :: Maybe QName
, envSimplification :: Simplification
, envAllowedReductions :: AllowedReductions
, envCompareBlocked :: Bool
, envPrintDomainFreePi :: Bool
, envPrintMetasBare :: Bool
, envInsideDotPattern :: Bool
, envUnquoteFlags :: UnquoteFlags
, envInstanceDepth :: !Int
}
deriving (Typeable)
initEnv :: TCEnv
initEnv = TCEnv { envContext = []
, envLetBindings = Map.empty
, envCurrentModule = noModuleName
, envCurrentPath = Nothing
, envAnonymousModules = []
, envImportPath = []
, envMutualBlock = Nothing
, envTerminationCheck = TerminationCheck
, envSolvingConstraints = False
, envCheckingWhere = False
, envActiveProblems = [0]
, envAssignMetas = True
, envAbstractMode = ConcreteMode
, envRelevance = Relevant
, envDisplayFormsEnabled = True
, envRange = noRange
, envHighlightingRange = noRange
, envClause = IPNoClause
, envCall = Nothing
, envHighlightingLevel = None
, envHighlightingMethod = Indirect
, envModuleNestingLevel = 1
, envAllowDestructiveUpdate = True
, envExpandLast = ExpandLast
, envAppDef = Nothing
, envSimplification = NoSimplification
, envAllowedReductions = allReductions
, envCompareBlocked = False
, envPrintDomainFreePi = False
, envPrintMetasBare = False
, envInsideDotPattern = False
, envUnquoteFlags = defaultUnquoteFlags
, envInstanceDepth = 0
}
disableDestructiveUpdate :: TCM a -> TCM a
disableDestructiveUpdate = local $ \e -> e { envAllowDestructiveUpdate = False }
data UnquoteFlags = UnquoteFlags
{ _unquoteNormalise :: Bool }
deriving (Typeable)
defaultUnquoteFlags :: UnquoteFlags
defaultUnquoteFlags = UnquoteFlags
{ _unquoteNormalise = False }
unquoteNormalise :: Lens' Bool UnquoteFlags
unquoteNormalise f e = f (_unquoteNormalise e) <&> \ x -> e { _unquoteNormalise = x }
eUnquoteNormalise :: Lens' Bool TCEnv
eUnquoteNormalise = eUnquoteFlags . unquoteNormalise
eContext :: Lens' Context TCEnv
eContext f e = f (envContext e) <&> \ x -> e { envContext = x }
eLetBindings :: Lens' LetBindings TCEnv
eLetBindings f e = f (envLetBindings e) <&> \ x -> e { envLetBindings = x }
eCurrentModule :: Lens' ModuleName TCEnv
eCurrentModule f e = f (envCurrentModule e) <&> \ x -> e { envCurrentModule = x }
eCurrentPath :: Lens' (Maybe AbsolutePath) TCEnv
eCurrentPath f e = f (envCurrentPath e) <&> \ x -> e { envCurrentPath = x }
eAnonymousModules :: Lens' [(ModuleName, Nat)] TCEnv
eAnonymousModules f e = f (envAnonymousModules e) <&> \ x -> e { envAnonymousModules = x }
eImportPath :: Lens' [C.TopLevelModuleName] TCEnv
eImportPath f e = f (envImportPath e) <&> \ x -> e { envImportPath = x }
eMutualBlock :: Lens' (Maybe MutualId) TCEnv
eMutualBlock f e = f (envMutualBlock e) <&> \ x -> e { envMutualBlock = x }
eTerminationCheck :: Lens' (TerminationCheck ()) TCEnv
eTerminationCheck f e = f (envTerminationCheck e) <&> \ x -> e { envTerminationCheck = x }
eSolvingConstraints :: Lens' Bool TCEnv
eSolvingConstraints f e = f (envSolvingConstraints e) <&> \ x -> e { envSolvingConstraints = x }
eCheckingWhere :: Lens' Bool TCEnv
eCheckingWhere f e = f (envCheckingWhere e) <&> \ x -> e { envCheckingWhere = x }
eAssignMetas :: Lens' Bool TCEnv
eAssignMetas f e = f (envAssignMetas e) <&> \ x -> e { envAssignMetas = x }
eActiveProblems :: Lens' [ProblemId] TCEnv
eActiveProblems f e = f (envActiveProblems e) <&> \ x -> e { envActiveProblems = x }
eAbstractMode :: Lens' AbstractMode TCEnv
eAbstractMode f e = f (envAbstractMode e) <&> \ x -> e { envAbstractMode = x }
eRelevance :: Lens' Relevance TCEnv
eRelevance f e = f (envRelevance e) <&> \ x -> e { envRelevance = x }
eDisplayFormsEnabled :: Lens' Bool TCEnv
eDisplayFormsEnabled f e = f (envDisplayFormsEnabled e) <&> \ x -> e { envDisplayFormsEnabled = x }
eRange :: Lens' Range TCEnv
eRange f e = f (envRange e) <&> \ x -> e { envRange = x }
eHighlightingRange :: Lens' Range TCEnv
eHighlightingRange f e = f (envHighlightingRange e) <&> \ x -> e { envHighlightingRange = x }
eCall :: Lens' (Maybe (Closure Call)) TCEnv
eCall f e = f (envCall e) <&> \ x -> e { envCall = x }
eHighlightingLevel :: Lens' HighlightingLevel TCEnv
eHighlightingLevel f e = f (envHighlightingLevel e) <&> \ x -> e { envHighlightingLevel = x }
eHighlightingMethod :: Lens' HighlightingMethod TCEnv
eHighlightingMethod f e = f (envHighlightingMethod e) <&> \ x -> e { envHighlightingMethod = x }
eModuleNestingLevel :: Lens' Int TCEnv
eModuleNestingLevel f e = f (envModuleNestingLevel e) <&> \ x -> e { envModuleNestingLevel = x }
eAllowDestructiveUpdate :: Lens' Bool TCEnv
eAllowDestructiveUpdate f e = f (envAllowDestructiveUpdate e) <&> \ x -> e { envAllowDestructiveUpdate = x }
eExpandLast :: Lens' ExpandHidden TCEnv
eExpandLast f e = f (envExpandLast e) <&> \ x -> e { envExpandLast = x }
eAppDef :: Lens' (Maybe QName) TCEnv
eAppDef f e = f (envAppDef e) <&> \ x -> e { envAppDef = x }
eSimplification :: Lens' Simplification TCEnv
eSimplification f e = f (envSimplification e) <&> \ x -> e { envSimplification = x }
eAllowedReductions :: Lens' AllowedReductions TCEnv
eAllowedReductions f e = f (envAllowedReductions e) <&> \ x -> e { envAllowedReductions = x }
eCompareBlocked :: Lens' Bool TCEnv
eCompareBlocked f e = f (envCompareBlocked e) <&> \ x -> e { envCompareBlocked = x }
ePrintDomainFreePi :: Lens' Bool TCEnv
ePrintDomainFreePi f e = f (envPrintDomainFreePi e) <&> \ x -> e { envPrintDomainFreePi = x }
eInsideDotPattern :: Lens' Bool TCEnv
eInsideDotPattern f e = f (envInsideDotPattern e) <&> \ x -> e { envInsideDotPattern = x }
eUnquoteFlags :: Lens' UnquoteFlags TCEnv
eUnquoteFlags f e = f (envUnquoteFlags e) <&> \ x -> e { envUnquoteFlags = x }
eInstanceDepth :: Lens' Int TCEnv
eInstanceDepth f e = f (envInstanceDepth e) <&> \ x -> e { envInstanceDepth = x }
type Context = [ContextEntry]
data ContextEntry = Ctx { ctxId :: CtxId
, ctxEntry :: Dom (Name, Type)
}
deriving (Typeable)
newtype CtxId = CtxId Nat
deriving (Typeable, Eq, Ord, Show, Enum, Real, Integral, Num)
type LetBindings = Map Name (Open (Term, Dom Type))
data AbstractMode
= AbstractMode
| ConcreteMode
| IgnoreAbstractMode
deriving (Typeable, Show, Eq)
aDefToMode :: IsAbstract -> AbstractMode
aDefToMode AbstractDef = AbstractMode
aDefToMode ConcreteDef = ConcreteMode
aModeToDef :: AbstractMode -> IsAbstract
aModeToDef AbstractMode = AbstractDef
aModeToDef ConcreteMode = ConcreteDef
aModeToDef _ = __IMPOSSIBLE__
data ExpandHidden
= ExpandLast
| DontExpandLast
deriving (Eq)
data ExplicitToInstance
= ExplicitToInstance
| ExplicitStayExplicit
deriving (Eq, Show)
data Candidate = Candidate { candidateTerm :: Term
, candidateType :: Type
, candidateEti :: ExplicitToInstance
, candidateOverlappable :: Bool
}
deriving (Show)
instance Free' Candidate c where
freeVars' (Candidate t u _ _) = freeVars' (t, u)
data Warning =
TerminationIssue [TerminationError]
| NotStrictlyPositive QName OccursWhere
| UnsolvedMetaVariables [Range]
| UnsolvedInteractionMetas [Range]
| UnsolvedConstraints Constraints
| OldBuiltin String String
| EmptyRewritePragma
| ParseWarning ParseWarning
deriving Show
data TCWarning
= TCWarning
{ tcWarningState :: TCState
, tcWarningClosure :: Closure Warning
}
deriving Show
tcWarning :: TCWarning -> Warning
tcWarning = clValue . tcWarningClosure
data CallInfo = CallInfo
{ callInfoTarget :: QName
, callInfoRange :: Range
, callInfoCall :: Closure Term
} deriving Typeable
instance Show CallInfo where show = show . callInfoTarget
instance Pretty CallInfo where pretty = text . show
instance AllNames CallInfo where allNames = singleton . callInfoTarget
data TerminationError = TerminationError
{ termErrFunctions :: [QName]
, termErrCalls :: [CallInfo]
} deriving (Typeable, Show)
data SplitError
= NotADatatype (Closure Type)
| IrrelevantDatatype (Closure Type)
| CoinductiveDatatype (Closure Type)
| CantSplit
{ cantSplitConName :: QName
, cantSplitTel :: Telescope
, cantSplitConIdx :: Args
, cantSplitGivenIdx :: Args
}
| GenericSplitError String
deriving (Show)
instance Error SplitError where
strMsg = GenericSplitError
data UnquoteError
= BadVisibility String (Arg I.Term)
| ConInsteadOfDef QName String String
| DefInsteadOfCon QName String String
| NonCanonical String I.Term
| BlockedOnMeta TCState MetaId
| UnquotePanic String
deriving (Show)
instance Error UnquoteError where
strMsg msg = UnquotePanic msg
data TypeError
= InternalError String
| NotImplemented String
| NotSupported String
| CompilationError String
| TerminationCheckFailed [TerminationError]
| PropMustBeSingleton
| DataMustEndInSort Term
| ShouldEndInApplicationOfTheDatatype Type
| ShouldBeAppliedToTheDatatypeParameters Term Term
| ShouldBeApplicationOf Type QName
| ConstructorPatternInWrongDatatype QName QName
| IndicesNotConstructorApplications [Arg Term]
| IndexVariablesNotDistinct [Nat] [Arg Term]
| IndicesFreeInParameters [Nat] [Arg Term] [Arg Term]
| CantResolveOverloadedConstructorsTargetingSameDatatype QName [QName]
| DoesNotConstructAnElementOf QName Type
| DifferentArities
| WrongHidingInLHS
| WrongHidingInLambda Type
| WrongHidingInApplication Type
| WrongNamedArgument (NamedArg A.Expr)
| WrongIrrelevanceInLambda Type
| WrongInstanceDeclaration
| HidingMismatch Hiding Hiding
| RelevanceMismatch Relevance Relevance
| NotInductive Term
| UninstantiatedDotPattern A.Expr
| IlltypedPattern A.Pattern Type
| IllformedProjectionPattern A.Pattern
| CannotEliminateWithPattern (NamedArg A.Pattern) Type
| TooManyArgumentsInLHS Type
| WrongNumberOfConstructorArguments QName Nat Nat
| ShouldBeEmpty Type [DeBruijnPattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBeRecordType Type
| ShouldBeRecordPattern DeBruijnPattern
| NotAProjectionPattern (NamedArg A.Pattern)
| NotAProperTerm
| SetOmegaNotValidType
| InvalidTypeSort Sort
| InvalidType Term
| FunctionTypeInSizeUniv Term
| SplitOnIrrelevant A.Pattern (Dom Type)
| DefinitionIsIrrelevant QName
| VariableIsIrrelevant Name
| UnequalTerms Comparison Term Term Type
| UnequalTypes Comparison Type Type
| UnequalRelevance Comparison Term Term
| UnequalHiding Term Term
| UnequalSorts Sort Sort
| UnequalBecauseOfUniverseConflict Comparison Term Term
| HeterogeneousEquality Term Type Term Type
| NotLeqSort Sort Sort
| MetaCannotDependOn MetaId [Nat] Nat
| MetaOccursInItself MetaId
| GenericError String
| GenericDocError Doc
| BuiltinMustBeConstructor String A.Expr
| NoSuchBuiltinName String
| DuplicateBuiltinBinding String Term Term
| NoBindingForBuiltin String
| NoSuchPrimitiveFunction String
| ShadowedModule C.Name [A.ModuleName]
| BuiltinInParameterisedModule String
| IllegalLetInTelescope C.TypedBinding
| NoRHSRequiresAbsurdPattern [NamedArg A.Pattern]
| AbsurdPatternRequiresNoRHS [NamedArg A.Pattern]
| TooFewFields QName [C.Name]
| TooManyFields QName [C.Name]
| DuplicateFields [C.Name]
| DuplicateConstructors [C.Name]
| WithOnFreeVariable A.Expr Term
| UnexpectedWithPatterns [A.Pattern]
| WithClausePatternMismatch A.Pattern Pattern
| FieldOutsideRecord
| ModuleArityMismatch A.ModuleName Telescope [NamedArg A.Expr]
| IncompletePatternMatching Term [Elim]
| CoverageFailure QName [[NamedArg DeBruijnPattern]]
| UnreachableClauses QName [[NamedArg DeBruijnPattern]]
| CoverageCantSplitOn QName Telescope Args Args
| CoverageCantSplitIrrelevantType Type
| CoverageCantSplitType Type
| CoverageNoExactSplit QName Clause
| WithoutKError Type Term Term
| UnifyConflict ConHead ConHead
| UnifyCycle Int Term
| UnifyIndicesNotVars Type Term Term Args
| UnificationRecursiveEq Type Int Term
| UnificationStuck Telescope [Term] [Term]
| SplitError SplitError
| TooManyPolarities QName Integer
| LocalVsImportedModuleClash ModuleName
| SolvedButOpenHoles
| CyclicModuleDependency [C.TopLevelModuleName]
| FileNotFound C.TopLevelModuleName [AbsolutePath]
| OverlappingProjects AbsolutePath C.TopLevelModuleName C.TopLevelModuleName
| AmbiguousTopLevelModuleName C.TopLevelModuleName [AbsolutePath]
| ModuleNameUnexpected C.TopLevelModuleName C.TopLevelModuleName
| ModuleNameDoesntMatchFileName C.TopLevelModuleName [AbsolutePath]
| ClashingFileNamesFor ModuleName [AbsolutePath]
| ModuleDefinedInOtherFile C.TopLevelModuleName AbsolutePath AbsolutePath
| BothWithAndRHS
| NotInScope [C.QName]
| NoSuchModule C.QName
| AmbiguousName C.QName [A.QName]
| AmbiguousModule C.QName [A.ModuleName]
| UninstantiatedModule C.QName
| ClashingDefinition C.QName A.QName
| ClashingModule A.ModuleName A.ModuleName
| ClashingImport C.Name A.QName
| ClashingModuleImport C.Name A.ModuleName
| PatternShadowsConstructor A.Name A.QName
| ModuleDoesntExport C.QName [C.ImportedName]
| DuplicateImports C.QName [C.ImportedName]
| InvalidPattern C.Pattern
| RepeatedVariablesInPattern [C.Name]
| NotAModuleExpr C.Expr
| NotAnExpression C.Expr
| NotAValidLetBinding D.NiceDeclaration
| NotValidBeforeField D.NiceDeclaration
| NothingAppliedToHiddenArg C.Expr
| NothingAppliedToInstanceArg C.Expr
| BadArgumentsToPatternSynonym A.QName
| TooFewArgumentsToPatternSynonym A.QName
| UnusedVariableInPatternSynonym
| NoParseForApplication [C.Expr]
| AmbiguousParseForApplication [C.Expr] [C.Expr]
| NoParseForLHS LHSOrPatSyn C.Pattern
| AmbiguousParseForLHS LHSOrPatSyn C.Pattern [C.Pattern]
| OperatorInformation [NotationSection] TypeError
| OperatorChangeMessage TypeError
| IFSNoCandidateInScope Type
| UnquoteFailed UnquoteError
| DeBruijnIndexOutOfScope Nat Telescope [Name]
| SafeFlagPostulate C.Name
| SafeFlagPragma [String]
| SafeFlagNonTerminating
| SafeFlagTerminating
| SafeFlagPrimTrustMe
| SafeFlagNoPositivityCheck
| SafeFlagPolarity
| NeedOptionCopatterns
| NeedOptionRewriting
| NonFatalErrors [TCWarning]
| InstanceSearchDepthExhausted Term Type Int
deriving (Typeable, Show)
data LHSOrPatSyn = IsLHS | IsPatSyn deriving (Eq, Show)
#if !MIN_VERSION_transformers(0,4,1)
instance Error TypeError where
strMsg = GenericError
#endif
data TCErr
= TypeError
{ tcErrState :: TCState
, tcErrClosErr :: Closure TypeError
}
| Exception Range Doc
| IOException Range E.IOException
| PatternErr
deriving (Typeable)
instance Error TCErr where
strMsg = Exception noRange . text . strMsg
instance Show TCErr where
show (TypeError _ e) = show (envRange $ clEnv e) ++ ": " ++ show (clValue e)
show (Exception r d) = show r ++ ": " ++ render d
show (IOException r e) = show r ++ ": " ++ show e
show PatternErr{} = "Pattern violation (you shouldn't see this)"
instance HasRange TCErr where
getRange (TypeError _ cl) = envRange $ clEnv cl
getRange (Exception r _) = r
getRange (IOException r _) = r
getRange PatternErr{} = noRange
instance E.Exception TCErr
data ReduceEnv = ReduceEnv
{ redEnv :: TCEnv
, redSt :: TCState
}
mapRedEnv :: (TCEnv -> TCEnv) -> ReduceEnv -> ReduceEnv
mapRedEnv f s = s { redEnv = f (redEnv s) }
mapRedSt :: (TCState -> TCState) -> ReduceEnv -> ReduceEnv
mapRedSt f s = s { redSt = f (redSt s) }
mapRedEnvSt :: (TCEnv -> TCEnv) -> (TCState -> TCState) -> ReduceEnv
-> ReduceEnv
mapRedEnvSt f g (ReduceEnv e s) = ReduceEnv (f e) (g s)
newtype ReduceM a = ReduceM { unReduceM :: ReduceEnv -> a }
fmapReduce :: (a -> b) -> ReduceM a -> ReduceM b
fmapReduce f (ReduceM m) = ReduceM $ \ e -> f $! m e
apReduce :: ReduceM (a -> b) -> ReduceM a -> ReduceM b
apReduce (ReduceM f) (ReduceM x) = ReduceM $ \ e -> f e $! x e
bindReduce :: ReduceM a -> (a -> ReduceM b) -> ReduceM b
bindReduce (ReduceM m) f = ReduceM $ \ e -> unReduceM (f $! m e) e
instance Functor ReduceM where
fmap = fmapReduce
instance Applicative ReduceM where
pure x = ReduceM (const x)
(<*>) = apReduce
instance Monad ReduceM where
return = pure
(>>=) = bindReduce
(>>) = (*>)
instance ReadTCState ReduceM where
getTCState = ReduceM redSt
runReduceM :: ReduceM a -> TCM a
runReduceM m = do
e <- ask
s <- get
return $! unReduceM m (ReduceEnv e s)
runReduceF :: (a -> ReduceM b) -> TCM (a -> b)
runReduceF f = do
e <- ask
s <- get
return $ \x -> unReduceM (f x) (ReduceEnv e s)
instance MonadReader TCEnv ReduceM where
ask = ReduceM redEnv
local f (ReduceM m) = ReduceM (m . mapRedEnv f)
newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a }
instance MonadIO m => MonadReader TCEnv (TCMT m) where
ask = TCM $ \s e -> return e
local f (TCM m) = TCM $ \s e -> m s (f e)
instance MonadIO m => MonadState TCState (TCMT m) where
get = TCM $ \s _ -> liftIO (readIORef s)
put s = TCM $ \r _ -> liftIO (writeIORef r s)
type TCM = TCMT IO
class ( Applicative tcm, MonadIO tcm
, MonadReader TCEnv tcm
, MonadState TCState tcm
) => MonadTCM tcm where
liftTCM :: TCM a -> tcm a
instance MonadIO m => ReadTCState (TCMT m) where
getTCState = get
instance MonadError TCErr (TCMT IO) where
throwError = liftIO . E.throwIO
catchError m h = TCM $ \r e -> do
oldState <- liftIO (readIORef r)
unTCM m r e `E.catch` \err -> do
case err of
PatternErr -> return ()
_ ->
liftIO $ do
newState <- readIORef r
writeIORef r $ oldState { stPersistentState = stPersistentState newState }
unTCM (h err) r e
runPM :: PM a -> TCM a
runPM m = do
(res, ws) <- runPMIO m
mapM_ (warning . ParseWarning) ws
case res of
Left e -> throwError (Exception (getRange e) (pretty e))
Right a -> return a
type IM = TCMT (Haskeline.InputT IO)
runIM :: IM a -> TCM a
runIM = mapTCMT (Haskeline.runInputT Haskeline.defaultSettings)
instance MonadError TCErr IM where
throwError = liftIO . E.throwIO
catchError m h = mapTCMT liftIO $ runIM m `catchError` (runIM . h)
catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
catchError_ m h = TCM $ \r e ->
unTCM m r e
`E.catch` \err -> unTCM (h err) r e
finally_ :: TCM a -> TCM b -> TCM a
finally_ m f = do
x <- m `catchError_` \ err -> f >> throwError err
_ <- f
return x
mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
mapTCMT f (TCM m) = TCM $ \s e -> f (m s e)
pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
pureTCM f = TCM $ \r e -> do
s <- liftIO $ readIORef r
return (f s e)
instance MonadIO m => MonadTCM (TCMT m) where
liftTCM = mapTCMT liftIO
instance MonadTCM tcm => MonadTCM (MaybeT tcm) where
liftTCM = lift . liftTCM
instance MonadTCM tcm => MonadTCM (ListT tcm) where
liftTCM = lift . liftTCM
instance
#if !MIN_VERSION_transformers(0,4,1)
(Error err, MonadTCM tcm)
#else
MonadTCM tcm
#endif
=> MonadTCM (ExceptT err tcm) where
liftTCM = lift . liftTCM
instance (Monoid w, MonadTCM tcm) => MonadTCM (WriterT w tcm) where
liftTCM = lift . liftTCM
instance MonadTrans TCMT where
lift m = TCM $ \_ _ -> m
instance MonadIO m => Monad (TCMT m) where
return = pure
(>>=) = bindTCMT
(>>) = (*>)
fail = internalError
returnTCMT :: MonadIO m => a -> TCMT m a
returnTCMT = \x -> TCM $ \_ _ -> return x
bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b
bindTCMT = \(TCM m) k -> TCM $ \r e -> m r e >>= \x -> unTCM (k x) r e
thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b
thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e
instance MonadIO m => Functor (TCMT m) where
fmap = fmapTCMT
fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b
fmapTCMT = \f (TCM m) -> TCM $ \r e -> liftM f (m r e)
instance MonadIO m => Applicative (TCMT m) where
pure = returnTCMT
(<*>) = apTCMT
apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b
apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> ap (mf r e) (m r e)
instance MonadIO m => MonadIO (TCMT m) where
liftIO m = TCM $ \s e -> do
let r = envRange e
liftIO $ wrap r $ do
x <- m
x `seq` return x
where
wrap r m = E.catch m (handleIOException r)
handleIOException r e = E.throwIO $ IOException r e
instance MonadBench Phase TCM where
getBenchmark = liftIO $ getBenchmark
putBenchmark = liftIO . putBenchmark
finally = finally_
instance Null (TCM Doc) where
empty = return empty
null = __IMPOSSIBLE__
instance Semigroup (TCM Any) where
ma <> mb = Any <$> do (getAny <$> ma) `or2M` (getAny <$> mb)
instance Monoid (TCM Any) where
mempty = return mempty
mappend = (<>)
patternViolation :: TCM a
patternViolation = throwError PatternErr
internalError :: MonadTCM tcm => String -> tcm a
internalError s = typeError $ InternalError s
genericError :: MonadTCM tcm => String -> tcm a
genericError = typeError . GenericError
genericDocError :: MonadTCM tcm => Doc -> tcm a
genericDocError = typeError . GenericDocError
typeError :: MonadTCM tcm => TypeError -> tcm a
typeError err = liftTCM $ throwError =<< typeError_ err
typeError_ :: MonadTCM tcm => TypeError -> tcm TCErr
typeError_ err = liftTCM $ TypeError <$> get <*> buildClosure err
warning_ :: MonadTCM tcm => Warning -> tcm TCWarning
warning_ w = liftTCM $ TCWarning <$> get <*> buildClosure w
warning :: MonadTCM tcm => Warning -> tcm ()
warning w = do
tcwarn <- warning_ w
stTCWarnings %= (tcwarn :)
runTCM :: MonadIO m => TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM e s m = do
r <- liftIO $ newIORef s
a <- unTCM m r e
s <- liftIO $ readIORef r
return (a, s)
runTCMTop :: TCM a -> IO (Either TCErr a)
runTCMTop m = (Right <$> runTCMTop' m) `E.catch` (return . Left)
runTCMTop' :: MonadIO m => TCMT m a -> m a
runTCMTop' m = do
r <- liftIO $ newIORef initState
unTCM m r initEnv
runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
runSafeTCM m st = runTCM initEnv st m `E.catch` (\ (e :: TCErr) -> __IMPOSSIBLE__)
forkTCM :: TCM a -> TCM ()
forkTCM m = do
s <- get
e <- ask
liftIO $ void $ C.forkIO $ void $ runTCM e s m
extendedLambdaName :: String
extendedLambdaName = ".extendedlambda"
absurdLambdaName :: String
absurdLambdaName = ".absurdlambda"
isAbsurdLambdaName :: QName -> Bool
isAbsurdLambdaName = (absurdLambdaName ==) . prettyShow . qnameName
instance KillRange Signature where
killRange (Sig secs defs rews) = killRange2 Sig secs defs rews
instance KillRange Sections where
killRange = fmap killRange
instance KillRange Definitions where
killRange = fmap killRange
instance KillRange RewriteRuleMap where
killRange = fmap killRange
instance KillRange Section where
killRange (Section tel) = killRange1 Section tel
instance KillRange Definition where
killRange (Defn ai name t pols occs displ mut compiled inst copy ma def) =
killRange11 Defn ai name t pols occs displ mut compiled inst copy ma def
instance KillRange CtxId where
killRange (CtxId x) = killRange1 CtxId x
instance KillRange NLPat where
killRange (PVar x y z) = killRange3 PVar x y z
killRange (PWild) = PWild
killRange (PDef x y) = killRange2 PDef x y
killRange (PLam x y) = killRange2 PLam x y
killRange (PPi x y) = killRange2 PPi x y
killRange (PBoundVar x y) = killRange2 PBoundVar x y
killRange (PTerm x) = killRange1 PTerm x
instance KillRange NLPType where
killRange (NLPType s a) = killRange2 NLPType s a
instance KillRange RewriteRule where
killRange (RewriteRule q gamma f es rhs t) =
killRange6 RewriteRule q gamma f es rhs t
instance KillRange CompiledRepresentation where
killRange = id
instance KillRange EtaEquality where
killRange = id
instance KillRange ExtLamInfo where
killRange = id
instance KillRange FunctionFlag where
killRange = id
instance KillRange Defn where
killRange def =
case def of
Axiom -> Axiom
AbstractDefn -> __IMPOSSIBLE__
Function cls comp tt inv mut isAbs delayed proj flags term extlam with copat ->
killRange13 Function cls comp tt inv mut isAbs delayed proj flags term extlam with copat
Datatype a b c d e f g h i j -> killRange10 Datatype a b c d e f g h i j
Record a b c d e f g h i j k -> killRange11 Record a b c d e f g h i j k
Constructor a b c d e f -> killRange6 Constructor a b c d e f
Primitive a b c d -> killRange4 Primitive a b c d
instance KillRange MutualId where
killRange = id
instance KillRange c => KillRange (FunctionInverse' c) where
killRange NotInjective = NotInjective
killRange (Inverse m) = Inverse $ killRangeMap m
instance KillRange TermHead where
killRange SortHead = SortHead
killRange PiHead = PiHead
killRange (ConsHead q) = ConsHead $ killRange q
instance KillRange Projection where
killRange (Projection a b c d e) = killRange5 Projection a b c d e
instance KillRange ProjLams where
killRange = id
instance KillRange a => KillRange (Open a) where
killRange = fmap killRange
instance KillRange a => KillRange (Local a) where
killRange (Local a b) = killRange2 Local a b
killRange (Global a) = killRange1 Global a
instance KillRange DisplayForm where
killRange (Display n es dt) = killRange3 Display n es dt
instance KillRange Polarity where
killRange = id
instance KillRange DisplayTerm where
killRange dt =
case dt of
DWithApp dt dts es -> killRange3 DWithApp dt dts es
DCon q ci dts -> killRange3 DCon q ci dts
DDef q dts -> killRange2 DDef q dts
DDot v -> killRange1 DDot v
DTerm v -> killRange1 DTerm v