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
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.Typeable (Typeable)
import Data.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.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.Interaction.Exceptions
import Agda.Interaction.Options
import Agda.Interaction.Response
(InteractionOutputCallback, defaultInteractionOutputCallback)
import Agda.Interaction.Highlighting.Precise
(CompressedFile, HighlightingInfo)
import qualified Agda.Compiler.JS.Syntax as JS
import qualified Agda.Compiler.UHC.Pragmas.Base as CR
import Agda.Utils.Except
( Error(strMsg)
, ExceptT
, MonadError(catchError, throwError)
)
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.ListT
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Singleton
#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
, 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
, stPostAwakeConstraints :: Constraints
, stPostSleepingConstraints :: Constraints
, stPostDirty :: Bool
, stPostOccursCheckDefs :: Set QName
, stPostSignature :: Signature
, stPostImportsDisplayForms :: !DisplayForms
, stPostImportedDisplayForms :: !DisplayForms
, stPostCurrentModule :: Maybe ModuleName
, stPostInstanceDefs :: TempInstanceTable
, stPostStatistics :: Statistics
, stPostMutualBlocks :: Map MutualId (Set QName)
, stPostLocalBuiltins :: BuiltinThings PrimFun
, stPostFreshMetaId :: MetaId
, stPostFreshMutualId :: MutualId
, stPostFreshCtxId :: CtxId
, stPostFreshProblemId :: ProblemId
, stPostFreshInt :: Int
, stPostFreshNameId :: NameId
}
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
, stPreHaskellImports = Set.empty
, stPreHaskellImportsUHC = Set.empty
, stPreHaskellCode = []
, stPreFreshInteractionId = 0
}
initPostScopeState :: PostScopeState
initPostScopeState = PostScopeState
{ stPostSyntaxInfo = mempty
, stPostDisambiguatedNames = IntMap.empty
, stPostMetaStore = Map.empty
, stPostInteractionPoints = Map.empty
, stPostAwakeConstraints = []
, stPostSleepingConstraints = []
, stPostDirty = False
, stPostOccursCheckDefs = Set.empty
, stPostSignature = emptySignature
, stPostImportsDisplayForms = HMap.empty
, stPostImportedDisplayForms = HMap.empty
, stPostCurrentModule = Nothing
, stPostInstanceDefs = (Map.empty , [])
, stPostStatistics = Map.empty
, 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}}
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}}
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 (stPostImportedDisplayForms (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostImportedDisplayForms = x}}
stCurrentModule :: Lens' (Maybe ModuleName) TCState
stCurrentModule f s =
f (stPostCurrentModule (stPostScopeState s)) <&>
\x -> s {stPostScopeState = (stPostScopeState s) {stPostCurrentModule = 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}}
stMutualBlocks :: Lens' (Map MutualId (Set QName)) 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
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
, clValue :: a
}
deriving (Typeable)
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
return $ Closure sig env scope 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
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)
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
| InstS 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 (InstS s) = "InstS (" ++ show s ++ ")"
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
}
instance Eq InteractionPoint where (==) = (==) `on` ipMeta
type InteractionPoints = Map InteractionId InteractionPoint
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 [Open DisplayForm]
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 :: [Term]
, dfRHS :: DisplayTerm
}
deriving (Typeable, Show)
data DisplayTerm
= DWithApp DisplayTerm [DisplayTerm] Args
| DCon ConHead [Arg DisplayTerm]
| DDef QName [Elim' DisplayTerm]
| DDot Term
| DTerm Term
deriving (Typeable, Show)
defaultDisplayForm :: QName -> [Open DisplayForm]
defaultDisplayForm c = []
defRelevance :: Definition -> Relevance
defRelevance = argInfoRelevance . defArgInfo
data NLPat
= PVar (Maybe CtxId) !Int
| PWild
| PDef QName PElims
| PLam ArgInfo (Abs NLPat)
| PPi (Dom (Type' NLPat)) (Abs (Type' NLPat))
| PBoundVar !Int PElims
| PTerm Term
deriving (Typeable, Show)
type PElims = [Elim' NLPat]
type RewriteRules = [RewriteRule]
data RewriteRule = RewriteRule
{ rewName :: QName
, rewContext :: Telescope
, rewLHS :: NLPat
, rewRHS :: Term
, rewType :: Type
}
deriving (Typeable, Show)
data Definition = Defn
{ defArgInfo :: ArgInfo
, defName :: QName
, defType :: Type
, defPolarity :: [Polarity]
, defArgOccurrences :: [Occurrence]
, defDisplay :: [Open DisplayForm]
, defMutual :: MutualId
, defCompiledRep :: CompiledRepresentation
, defInstance :: Maybe QName
, defCopy :: Bool
, theDef :: Defn
}
deriving (Typeable, Show)
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
, theDef = def
}
type HaskellCode = String
type HaskellType = String
type EpicCode = String
type JSCode = JS.Exp
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 :: Maybe QName
, projFromType :: QName
, projIndex :: Int
, projDropPars :: Term
, projArgInfo :: ArgInfo
} deriving (Typeable, Show)
data EtaEquality = Specified !Bool | Inferred !Bool deriving (Typeable,Show)
etaEqualityToBool :: EtaEquality -> Bool
etaEqualityToBool (Specified b) = b
etaEqualityToBool (Inferred b) = b
setEtaEquality :: EtaEquality -> Bool -> EtaEquality
setEtaEquality e@Specified{} _ = e
setEtaEquality _ b = Inferred b
data Defn = Axiom
| Function
{ funClauses :: [Clause]
, funCompiled :: Maybe CompiledClauses
, funTreeless :: Maybe Compiled
, funInv :: FunctionInverse
, funMutual :: [QName]
, funAbstr :: IsAbstract
, funDelayed :: Delayed
, funProjection :: Maybe Projection
, funStatic :: Bool
, funInline :: Bool
, funSmashable :: Bool
, 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
, recConType :: Type
, 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
}
| 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
, funStatic = False
, funInline = False
, funSmashable = True
, funTerminates = Nothing
, funExtLam = Nothing
, funWith = Nothing
, funCopatternLHS = False
}
isEmptyFunction :: Defn -> Bool
isEmptyFunction def =
case def of
Function { funClauses = [] } -> True
_ -> False
isCopatternLHS :: [Clause] -> Bool
isCopatternLHS = List.any (List.any (isJust . A.isProjP) . clausePats)
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 Monoid Simplification where
mempty = NoSimplification
mappend YesSimplification _ = YesSimplification
mappend NoSimplification s = s
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
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 Range 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 [QName]
type TempInstanceTable = (InstanceTable , [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 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
, envReifyInteractionPoints :: Bool
, envEtaContractImplicit :: Bool
, envRange :: Range
, envHighlightingRange :: Range
, envCall :: Maybe (Closure Call)
, envHighlightingLevel :: HighlightingLevel
, envHighlightingMethod :: HighlightingMethod
, envModuleNestingLevel :: Integer
, envAllowDestructiveUpdate :: Bool
, envExpandLast :: ExpandHidden
, envAppDef :: Maybe QName
, envSimplification :: Simplification
, envAllowedReductions :: AllowedReductions
, envCompareBlocked :: Bool
, envPrintDomainFreePi :: Bool
, envInsideDotPattern :: Bool
}
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
, envReifyInteractionPoints = True
, envEtaContractImplicit = True
, envRange = noRange
, envHighlightingRange = noRange
, envCall = Nothing
, envHighlightingLevel = None
, envHighlightingMethod = Indirect
, envModuleNestingLevel = 1
, envAllowDestructiveUpdate = True
, envExpandLast = ExpandLast
, envAppDef = Nothing
, envSimplification = NoSimplification
, envAllowedReductions = allReductions
, envCompareBlocked = False
, envPrintDomainFreePi = False
, envInsideDotPattern = False
}
disableDestructiveUpdate :: TCM a -> TCM a
disableDestructiveUpdate = local $ \e -> e { envAllowDestructiveUpdate = False }
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)
data ExpandHidden
= ExpandLast
| DontExpandLast
deriving (Eq)
data ExplicitToInstance
= ExplicitToInstance
| ExplicitStayExplicit
deriving (Eq, Show)
data Candidate = Candidate { candidateTerm :: Term
, candidateType :: Type
, candidateEti :: ExplicitToInstance
}
deriving (Show)
data Occ = OccCon { occDatatype :: QName
, occConstructor :: QName
, occPosition :: OccPos
}
| OccClause { occFunction :: QName
, occClause :: Int
, occPosition :: OccPos
}
deriving (Show)
data OccPos = NonPositively | ArgumentTo Nat QName
deriving (Show)
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 [Pattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBeRecordType Type
| ShouldBeRecordPattern Pattern
| 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
| UnexpectedWithPatterns [A.Pattern]
| WithClausePatternMismatch A.Pattern Pattern
| FieldOutsideRecord
| ModuleArityMismatch A.ModuleName Telescope [NamedArg A.Expr]
| IncompletePatternMatching Term [Elim]
| CoverageFailure QName [[Arg DeBruijnPattern]]
| UnreachableClauses QName [[Arg 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
| NotStrictlyPositive QName [Occ]
| LocalVsImportedModuleClash ModuleName
| UnsolvedMetas [Range]
| UnsolvedConstraints Constraints
| SolvedButOpenHoles
| CyclicModuleDependency [C.TopLevelModuleName]
| FileNotFound C.TopLevelModuleName [AbsolutePath]
| OverlappingProjects AbsolutePath C.TopLevelModuleName C.TopLevelModuleName
| AmbiguousTopLevelModuleName C.TopLevelModuleName [AbsolutePath]
| 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
| 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
| SafeFlagPostulate C.Name
| SafeFlagPragma [String]
| SafeFlagNonTerminating
| SafeFlagTerminating
| SafeFlagPrimTrustMe
| SafeFlagNoPositivityCheck
| NeedOptionCopatterns
| NeedOptionRewriting
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 TCState (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 }
instance Functor ReduceM where
fmap f (ReduceM m) = ReduceM $ \ e -> f $! m e
instance Applicative ReduceM where
pure x = ReduceM (const x)
ReduceM f <*> ReduceM x = ReduceM $ \ e -> f e $! x e
instance Monad ReduceM where
return = pure
ReduceM m >>= f = ReduceM $ \ e -> unReduceM (f $! m e) e
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
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 = failOnException handleException
$ E.catch m (handleIOException r)
handleIOException r e = E.throwIO $ IOException r e
handleException r s = E.throwIO $ Exception r s
instance MonadBench Phase TCM where
getBenchmark = liftIO $ getBenchmark
putBenchmark = liftIO . putBenchmark
finally = finally_
instance Null (TCM Doc) where
empty = return empty
null = __IMPOSSIBLE__
instance Monoid (TCM Any) where
mempty = return mempty
ma `mappend` mb = Any <$> do (getAny <$> ma) `or2M` (getAny <$> mb)
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
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
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 def) =
killRange11 Defn ai name t pols occs displ mut compiled inst copy def
instance KillRange CtxId where
killRange (CtxId x) = killRange1 CtxId x
instance KillRange NLPat where
killRange (PVar x y) = killRange1 PVar x y
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 RewriteRule where
killRange (RewriteRule q gamma lhs rhs t) =
killRange5 RewriteRule q gamma lhs rhs t
instance KillRange CompiledRepresentation where
killRange = id
instance KillRange EtaEquality where
killRange = id
instance KillRange ExtLamInfo where
killRange = id
instance KillRange Defn where
killRange def =
case def of
Axiom -> Axiom
Function cls comp tt inv mut isAbs delayed proj static inline smash term extlam with cop ->
killRange15 Function cls comp tt inv mut isAbs delayed proj static inline smash term extlam with cop
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 l -> killRange12 Record a b c d e f g h i j k l
Constructor a b c d e -> killRange5 Constructor a b c d e
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) = killRange4 Projection a b c d e
instance KillRange a => KillRange (Open a) where
killRange = fmap killRange
instance KillRange DisplayForm where
killRange (Display n vs dt) = killRange3 Display n vs dt
instance KillRange Polarity where
killRange = id
instance KillRange DisplayTerm where
killRange dt =
case dt of
DWithApp dt dts args -> killRange3 DWithApp dt dts args
DCon q dts -> killRange2 DCon q dts
DDef q dts -> killRange2 DDef q dts
DDot v -> killRange1 DDot v
DTerm v -> killRange1 DTerm v