module Agda.TypeChecking.Monad.Base where
import Control.Arrow ((***), first, second)
import qualified Control.Concurrent as C
import Control.DeepSeq
import Control.Exception as E
import Control.Monad.Error
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.Trans.Maybe
import Control.Applicative
import Data.Function
import Data.Int
import qualified Data.List as List
import Data.Map as Map
import Data.Set as Set
import Data.Sequence as Seq
import Data.Typeable (Typeable)
import Data.Foldable
import Data.Traversable
import Data.IORef
import Agda.Syntax.Concrete (TopLevelModuleName)
import Agda.Syntax.Common hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as 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.Internal as I
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.CompiledClause
import Agda.Interaction.Exceptions
import Agda.Interaction.Options
import Agda.Interaction.Response
(InteractionOutputCallback, defaultInteractionOutputCallback, Response)
import Agda.Interaction.Highlighting.Precise
(CompressedFile, HighlightingInfo)
import qualified Agda.Compiler.JS.Syntax as JS
import Agda.TypeChecking.Monad.Base.Benchmark (Benchmark)
import qualified Agda.TypeChecking.Monad.Base.Benchmark as Benchmark
import Agda.Utils.FileName
import Agda.Utils.Fresh
import Agda.Utils.HashMap as HMap
import Agda.Utils.Hash
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Time
#include "../../undefined.h"
import Agda.Utils.Impossible
data TCState =
TCSt { stFreshThings :: FreshThings
, stSyntaxInfo :: CompressedFile
, stTokens :: CompressedFile
, stTermErrs :: Seq TerminationError
, stMetaStore :: MetaStore
, stInteractionPoints :: InteractionPoints
, stAwakeConstraints :: Constraints
, stSleepingConstraints :: Constraints
, stDirty :: Bool
, stOccursCheckDefs :: Set QName
, stSignature :: Signature
, stImports :: Signature
, stImportedModules :: Set ModuleName
, stModuleToSource :: ModuleToSource
, stVisitedModules :: VisitedModules
, stCurrentModule :: Maybe ModuleName
, stScope :: ScopeInfo
, stPatternSyns :: A.PatternSynDefns
, stPatternSynImports :: A.PatternSynDefns
, stPragmaOptions :: PragmaOptions
, stStatistics :: Statistics
, stMutualBlocks :: Map MutualId (Set QName)
, stLocalBuiltins :: BuiltinThings PrimFun
, stImportedBuiltins :: BuiltinThings PrimFun
, stHaskellImports :: Set String
, stPersistent :: PersistentTCState
}
data PersistentTCState = PersistentTCSt
{ stDecodedModules :: DecodedModules
, stPersistentOptions :: CommandLineOptions
, stInteractionOutputCallback :: InteractionOutputCallback
, stBenchmark :: !Benchmark
}
initPersistentState :: PersistentTCState
initPersistentState = PersistentTCSt
{ stPersistentOptions = defaultOptions
, stDecodedModules = Map.empty
, stInteractionOutputCallback = defaultInteractionOutputCallback
, stBenchmark = Benchmark.empty
}
data FreshThings =
Fresh { fMeta :: MetaId
, fInteraction :: InteractionId
, fMutual :: MutualId
, fName :: NameId
, fCtx :: CtxId
, fProblem :: ProblemId
, fInt :: Int
}
deriving (Show)
initState :: TCState
initState = TCSt
{ stFreshThings = (Fresh 0 0 0 (NameId 0 0) 0 0 0) { fProblem = 1 }
, stMetaStore = Map.empty
, stSyntaxInfo = mempty
, stTokens = mempty
, stTermErrs = Seq.empty
, stInteractionPoints = Map.empty
, stAwakeConstraints = []
, stSleepingConstraints = []
, stDirty = False
, stOccursCheckDefs = Set.empty
, stSignature = emptySignature
, stImports = emptySignature
, stImportedModules = Set.empty
, stModuleToSource = Map.empty
, stVisitedModules = Map.empty
, stCurrentModule = Nothing
, stScope = emptyScopeInfo
, stPatternSyns = Map.empty
, stPatternSynImports = Map.empty
, stPragmaOptions = defaultInteractionOptions
, stStatistics = Map.empty
, stMutualBlocks = Map.empty
, stLocalBuiltins = Map.empty
, stImportedBuiltins = Map.empty
, stHaskellImports = Set.empty
, stPersistent = initPersistentState
}
stBuiltinThings :: TCState -> BuiltinThings PrimFun
stBuiltinThings s = stLocalBuiltins s `Map.union` stImportedBuiltins s
instance HasFresh MetaId FreshThings where
nextFresh s = (i, s { fMeta = i + 1 })
where
i = fMeta s
instance HasFresh MutualId FreshThings where
nextFresh s = (i, s { fMutual = i + 1 })
where
i = fMutual s
instance HasFresh InteractionId FreshThings where
nextFresh s = (i, s { fInteraction = i + 1 })
where
i = fInteraction s
instance HasFresh NameId FreshThings where
nextFresh s = (i, s { fName = succ i })
where
i = fName s
instance HasFresh CtxId FreshThings where
nextFresh s = (i, s { fCtx = succ i })
where
i = fCtx s
instance HasFresh Int FreshThings where
nextFresh s = (i, s { fInt = succ i })
where
i = fInt s
newtype ProblemId = ProblemId Nat
deriving (Typeable, Eq, Ord, Enum, Real, Integral, Num)
instance Show ProblemId where
show (ProblemId n) = show n
instance HasFresh ProblemId FreshThings where
nextFresh s = (i, s { fProblem = succ i })
where i = fProblem s
instance HasFresh i FreshThings => HasFresh i TCState where
nextFresh s = ((,) $! i) $! s { stFreshThings = f }
where
(i, f) = nextFresh $ stFreshThings s
type ModuleToSource = Map TopLevelModuleName AbsolutePath
type SourceToModule = Map AbsolutePath TopLevelModuleName
sourceToModule :: TCM SourceToModule
sourceToModule =
Map.fromList
. List.map (\(m, f) -> (f, m))
. Map.toList
. stModuleToSource
<$> get
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
, iBuiltin :: BuiltinThings (String, QName)
, iHaskellImports :: Set String
, iHighlighting :: HighlightingInfo
, iPragmaOptions :: [OptionsPragma]
, iPatternSyns :: A.PatternSynDefns
}
deriving (Typeable, Show)
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 <- gets stSignature
scope <- gets stScope
return $ Closure sig env scope x
type Constraints = [ProblemConstraint]
data ProblemConstraint = PConstr
{ constraintProblem :: 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
| FindInScope MetaId [(Term, Type)]
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 = "=<"
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 t a
= HasType { jMetaId :: a, jMetaType :: t }
| IsSort { jMetaId :: a, jMetaType :: t }
deriving (Typeable, Functor, Foldable, Traversable)
instance (Show t, Show a) => Show (Judgement t 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 Type 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 Term
| InstS Term
| Open
| OpenIFS
| BlockedConst Term
| PostponedTypeCheckingProblem (Closure TypeCheckingProblem) (TCM Bool)
deriving (Typeable)
data TypeCheckingProblem
= CheckExpr A.Expr Type
| CheckArgs ExpandHidden ExpandInstances Range [I.NamedArg A.Expr] Type Type (Args -> Type -> TCM Term)
deriving (Typeable)
instance Show MetaInstantiation where
show (InstV t) = "InstV (" ++ 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 Show NamedMeta where
show (NamedMeta "" x) = show x
show (NamedMeta s x) = "_" ++ s ++ show 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
getMetaColors :: MetaVariable -> [Color]
getMetaColors = envColors . 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
}
deriving (Typeable, Show)
type Sections = Map ModuleName Section
type Definitions = HashMap QName Definition
data Section = Section
{ secTelescope :: Telescope
, secFreeVars :: Nat
}
deriving (Typeable, Show)
emptySignature :: Signature
emptySignature = Sig Map.empty HMap.empty
data DisplayForm = Display
{ dfFreeVars :: Nat
, dfPats :: [Term]
, dfRHS :: DisplayTerm
}
deriving (Typeable, Show)
data DisplayTerm
= DWithApp DisplayTerm [DisplayTerm] Args
| DCon QName [Arg DisplayTerm]
| DDef QName [Arg DisplayTerm]
| DDot Term
| DTerm Term
deriving (Typeable, Show)
defaultDisplayForm :: QName -> [Open DisplayForm]
defaultDisplayForm c = []
defRelevance = argInfoRelevance . defArgInfo
defColors = argInfoColors . defArgInfo
data Definition = Defn
{ defArgInfo :: ArgInfo
, defName :: QName
, defType :: Type
, defPolarity :: [Polarity]
, defArgOccurrences :: [Occurrence]
, defDisplay :: [Open DisplayForm]
, defMutual :: MutualId
, defCompiledRep :: CompiledRepresentation
, 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
, 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 Polarity
= Covariant
| Contravariant
| Invariant
| Nonvariant
deriving (Typeable, Show, Eq)
data CompiledRepresentation = CompiledRep
{ compiledHaskell :: Maybe HaskellRepresentation
, exportHaskell :: Maybe HaskellExport
, compiledEpic :: Maybe EpicCode
, compiledJS :: Maybe JSCode
}
deriving (Typeable, Show)
noCompiledRep :: CompiledRepresentation
noCompiledRep = CompiledRep Nothing Nothing Nothing Nothing
data Occurrence
= Mixed
| JustNeg
| JustPos
| StrictPos
| GuardPos
| Unused
deriving (Typeable, Show, Eq, Ord)
instance NFData Occurrence
data Projection = Projection
{ projProper :: Maybe QName
, projFromType :: QName
, projIndex :: Int
, projDropPars :: Term
, projArgInfo :: I.ArgInfo
} deriving (Typeable, Show)
data Defn = Axiom
| Function
{ funClauses :: [Clause]
, funCompiled :: Maybe CompiledClauses
, funInv :: FunctionInverse
, funMutual :: [QName]
, funAbstr :: IsAbstract
, funDelayed :: Delayed
, funProjection :: Maybe Projection
, funStatic :: Bool
, funCopy :: Bool
, funTerminates :: Maybe Bool
, funExtLam :: Maybe (Int,Int)
, funWith :: Maybe QName
}
| 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 :: Bool
, recInduction :: 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)
emptyFunction :: Defn
emptyFunction = Function
{ funClauses = []
, funCompiled = Nothing
, funInv = NotInjective
, funMutual = []
, funAbstr = ConcreteDef
, funDelayed = NotDelayed
, funProjection = Nothing
, funStatic = False
, funCopy = False
, funTerminates = Nothing
, funExtLam = Nothing
, funWith = Nothing
}
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)
data Simplification = YesSimplification | NoSimplification
deriving (Typeable, Eq, Show)
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 (Common.Arg _ (MetaV x _)) -> MaybeRed (Reduced $ Blocked x ()) v
_ -> MaybeRed (Reduced $ () <$ b) v
where
v = ignoreBlocking b
data AllowedReduction
= ProjectionReductions
| FunctionReductions
| LevelReductions
deriving (Show, Eq, Ord, Enum, Bounded)
type AllowedReductions = [AllowedReduction]
allReductions = [minBound..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
defJSDef :: Definition -> Maybe JSCode
defJSDef = compiledJS . defCompiledRep
defEpicDef :: Definition -> Maybe EpicCode
defEpicDef = compiledEpic . 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
defCopy :: Definition -> Bool
defCopy Defn{theDef = Function{funCopy = b}} = b
defCopy _ = 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)
type Statistics = Map String Integer
data Call = CheckClause Type A.SpineClause (Maybe Clause)
| forall a. CheckPattern A.Pattern Telescope Type (Maybe a)
| CheckLetBinding A.LetBinding (Maybe ())
| InferExpr A.Expr (Maybe (Term, Type))
| CheckExprCall A.Expr Type (Maybe Term)
| CheckDotPattern A.Expr Term (Maybe Constraints)
| CheckPatternShadowing A.SpineClause (Maybe ())
| IsTypeCall A.Expr Sort (Maybe Type)
| IsType_ A.Expr (Maybe Type)
| InferVar Name (Maybe (Term, Type))
| InferDef Range QName (Maybe (Term, Type))
| CheckArguments Range [NamedArg A.Expr] Type Type (Maybe (Args, Type))
| CheckDataDef Range Name [A.LamBinding] [A.Constructor] (Maybe ())
| CheckRecDef Range Name [A.LamBinding] [A.Constructor] (Maybe ())
| CheckConstructor QName Telescope Sort A.Constructor (Maybe ())
| CheckFunDef Range Name [A.Clause] (Maybe ())
| CheckPragma Range A.Pragma (Maybe ())
| CheckPrimitive Range Name A.Expr (Maybe ())
| CheckIsEmpty Range Type (Maybe ())
| CheckWithFunctionType A.Expr (Maybe ())
| CheckSectionApplication Range ModuleName A.ModuleApplication (Maybe ())
| ScopeCheckExpr C.Expr (Maybe A.Expr)
| ScopeCheckDeclaration D.NiceDeclaration (Maybe [A.Declaration])
| ScopeCheckLHS C.Name C.Pattern (Maybe A.LHS)
| forall a. NoHighlighting (Maybe a)
| forall a. SetRange Range (Maybe a)
deriving (Typeable)
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 (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
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 :: AbsolutePath
, envAnonymousModules :: [(ModuleName, Nat)]
, envImportPath :: [C.TopLevelModuleName]
, envMutualBlock :: Maybe MutualId
, envSolvingConstraints :: Bool
, envAssignMetas :: Bool
, envActiveProblems :: [ProblemId]
, envAbstractMode :: AbstractMode
, envRelevance :: Relevance
, envColors :: [Color]
, 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
, envPrintDomainFreePi :: Bool
, envInsideDotPattern :: Bool
}
deriving (Typeable)
initEnv :: TCEnv
initEnv = TCEnv { envContext = []
, envLetBindings = Map.empty
, envCurrentModule = noModuleName
, envCurrentPath = __IMPOSSIBLE__
, envAnonymousModules = []
, envImportPath = []
, envMutualBlock = Nothing
, envSolvingConstraints = False
, envActiveProblems = [0]
, envAssignMetas = True
, envAbstractMode = ConcreteMode
, envRelevance = Relevant
, envColors = []
, 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
, envPrintDomainFreePi = False
, envInsideDotPattern = 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 ExpandInstances
= ExpandInstanceArguments
| DontExpandInstanceArguments
deriving (Eq)
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 . callInfoTarget
data TerminationError = TerminationError
{ termErrFunctions :: [QName]
, termErrCalls :: [CallInfo]
} deriving (Typeable, Show)
data SplitError = NotADatatype (Closure Type)
| IrrelevantDatatype (Closure Type)
| CoinductiveDatatype (Closure Type)
| CantSplit QName Telescope Args Args [Term]
| GenericSplitError String
deriving (Show)
instance Error SplitError where
noMsg = strMsg ""
strMsg = GenericSplitError
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 (I.NamedArg A.Expr)
| WrongIrrelevanceInLambda Type
| HidingMismatch Hiding Hiding
| RelevanceMismatch Relevance Relevance
| ColorMismatch [Color] [Color]
| NotInductive Term
| UninstantiatedDotPattern A.Expr
| IlltypedPattern A.Pattern Type
| IllformedProjectionPattern A.Pattern
| CannotEliminateWithPattern (A.NamedArg A.Pattern) Type
| TooManyArgumentsInLHS Type
| WrongNumberOfConstructorArguments QName Nat Nat
| ShouldBeEmpty Type [Pattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBeRecordType Type
| ShouldBeRecordPattern Pattern
| NotAProjectionPattern (A.NamedArg A.Pattern)
| NotAProperTerm
| SetOmegaNotValidType
| InvalidType 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
| UnequalColors 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]
| UnexpectedWithPatterns [A.Pattern]
| WithClausePatternMismatch A.Pattern Pattern
| FieldOutsideRecord
| ModuleArityMismatch A.ModuleName Telescope [NamedArg A.Expr]
| IncompletePatternMatching Term [Elim]
| CoverageFailure QName [[Arg Pattern]]
| UnreachableClauses QName [[Arg Pattern]]
| CoverageCantSplitOn QName Telescope Args Args
| CoverageCantSplitIrrelevantType Type
| CoverageCantSplitType Type
| WithoutKError Type Term Term
| SplitError SplitError
| NotStrictlyPositive QName [Occ]
| LocalVsImportedModuleClash ModuleName
| UnsolvedMetas [Range]
| UnsolvedConstraints Constraints
| 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
| UnusedVariableInPatternSynonym
| PatternSynonymArityMismatch A.QName
| NoParseForApplication [C.Expr]
| AmbiguousParseForApplication [C.Expr] [C.Expr]
| NoParseForLHS LHSOrPatSyn C.Pattern
| AmbiguousParseForLHS LHSOrPatSyn C.Pattern [C.Pattern]
| IFSNoCandidateInScope Type
| SafeFlagPostulate C.Name
| SafeFlagPragma [String]
| SafeFlagNoTerminationCheck
| SafeFlagPrimTrustMe
| NeedOptionCopatterns
deriving (Typeable, Show)
data LHSOrPatSyn = IsLHS | IsPatSyn deriving (Eq, Show)
instance Error TypeError where
noMsg = strMsg ""
strMsg = GenericError
data TCErr = TypeError TCState (Closure TypeError)
| Exception Range String
| IOException Range E.IOException
| PatternErr TCState
deriving (Typeable)
instance Error TCErr where
noMsg = strMsg ""
strMsg = Exception noRange . strMsg
instance Show TCErr where
show (TypeError _ e) = show (envRange $ clEnv e) ++ ": " ++ show (clValue e)
show (Exception r s) = show r ++ ": " ++ s
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 s) = noRange
instance 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 :: Reader ReduceEnv a }
deriving (Functor, Applicative, Monad)
runReduceM :: ReduceM a -> TCM a
runReduceM m = do
e <- ask
s <- get
return $ runReader (unReduceM m) (ReduceEnv e s)
instance MonadReader TCEnv ReduceM where
ask = redEnv <$> ReduceM ask
local f = ReduceM . local (mapRedEnv f) . unReduceM
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 MonadError TCErr (TCMT IO) where
throwError = liftIO . throwIO
catchError m h = TCM $ \r e -> do
oldState <- liftIO (readIORef r)
unTCM m r e `E.catch` \err -> do
liftIO $ do
newState <- readIORef r
writeIORef r $ oldState { stPersistent = stPersistent newState }
unTCM (h err) r e
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
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 (Error err, MonadTCM tcm) => MonadTCM (ErrorT 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 = returnTCMT
(>>=) = bindTCMT
(>>) = thenTCMT
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 = throwIO $ IOException r e
handleException r s = throwIO $ Exception r s
patternViolation :: TCM a
patternViolation = do
s <- get
throwError $ PatternErr s
internalError :: MonadTCM tcm => String -> tcm a
internalError s = typeError $ InternalError s
typeError :: MonadTCM tcm => TypeError -> tcm a
typeError err = liftTCM $ do
cl <- buildClosure err
s <- get
throwError $ TypeError s cl
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
extendlambdaname = ".extendedlambda"
absurdLambdaName = ".absurdlambda"
isAbsurdLambdaName :: QName -> Bool
isAbsurdLambdaName (QName _ x) | show x == absurdLambdaName = True
isAbsurdLambdaName _ = False