{-# LANGUAGE CPP, ExistentialQuantification, FlexibleContexts, Rank2Types,
             TypeSynonymInstances, MultiParamTypeClasses, FlexibleInstances,
             UndecidableInstances, DeriveDataTypeable, GeneralizedNewtypeDeriving,
             DeriveFunctor, DeriveFoldable, DeriveTraversable
  #-}
module Agda.TypeChecking.Monad.Base where

import Control.Arrow
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.Applicative
import Data.Function
import Data.Int
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 Data.Hashable

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.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Utils.HashMap as HMap

import Agda.TypeChecking.CompiledClause

import Agda.Interaction.Exceptions
import {-# SOURCE #-} Agda.Interaction.FindFile
import Agda.Interaction.Options
import qualified Agda.Interaction.Highlighting.Range as R
import {-# SOURCE #-} Agda.Interaction.Response
  (InteractionOutputCallback, defaultInteractionOutputCallback)
import Agda.Interaction.Highlighting.Precise
  (CompressedFile, HighlightingInfo)
import Data.Monoid

import qualified Agda.Compiler.JS.Syntax as JS

import Agda.Utils.FileName
import Agda.Utils.Fresh
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Time

#include "../../undefined.h"
import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Type checking state
---------------------------------------------------------------------------

data TCState =
    TCSt { stFreshThings       :: FreshThings
         , stSyntaxInfo        :: CompressedFile
           -- ^ Highlighting info.
         , stTokens            :: CompressedFile
           -- ^ Highlighting info for tokens (but not those tokens for
           -- which highlighting exists in 'stSyntaxInfo').
         , stTermErrs          :: Seq TerminationError
	 , stMetaStore	       :: MetaStore
	 , stInteractionPoints :: InteractionPoints
	 , stAwakeConstraints    :: Constraints
	 , stSleepingConstraints :: Constraints
         , stDirty               :: Bool
         , stOccursCheckDefs   :: Set QName
           -- ^ Definitions to be considered during occurs check.
           --   Initialized to the current mutual block before the check.
	 , stSignature	       :: Signature
	 , stImports	       :: Signature
	 , stImportedModules   :: Set ModuleName
         , stModuleToSource    :: ModuleToSource
	 , stVisitedModules    :: VisitedModules
         , stCurrentModule     :: Maybe ModuleName
           -- ^ The current module is available after it has been type
           -- checked.
	 , stScope	       :: ScopeInfo
         , stPatternSyns       :: A.PatternSynDefns
         , stPatternSynImports :: A.PatternSynDefns
	 , stPragmaOptions     :: PragmaOptions
           -- ^ Options applying to the current file. @OPTIONS@
           -- pragmas only affect this field.
	 , stStatistics	       :: Statistics
         , stExtLambdaTele     :: Map QName (Int , Int)
	 , stMutualBlocks      :: Map MutualId (Set QName)
	 , stLocalBuiltins     :: BuiltinThings PrimFun
         , stImportedBuiltins  :: BuiltinThings PrimFun
         , stHaskellImports    :: Set String
           -- ^ Imports that should be generated by the compiler (this
           -- includes imports from imported modules).
         , stPersistent        :: PersistentTCState
         , stInteractionOutputCallback  :: InteractionOutputCallback
           -- ^ Callback fuction to call when there is a response
           --   to give to the interactive frontend.
           --   See the documentation of 'InteractionOutputCallback'.
	 }

-- | A part of the state which is not reverted when an error is thrown
-- or the state is reset.

data PersistentTCState = PersistentTCSt
  { stDecodedModules    :: DecodedModules
  , stPersistentOptions :: CommandLineOptions
    -- ^ Options which apply to all files, unless overridden.
  }

data FreshThings =
	Fresh { fMeta	     :: MetaId
	      , fInteraction :: InteractionId
	      , fMutual	     :: MutualId
	      , fName	     :: NameId
	      , fCtx	     :: CtxId
              , fProblem     :: ProblemId
              , fInt         :: Int
                -- ^ Can be used for various things.
	      }
    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
         , stExtLambdaTele     = Map.empty
	 , stMutualBlocks      = Map.empty
	 , stLocalBuiltins     = Map.empty
	 , stImportedBuiltins  = Map.empty
         , stHaskellImports    = Set.empty
         , stPersistent        = PersistentTCSt
           { stPersistentOptions = defaultOptions
	   , stDecodedModules    = Map.empty
           }
         , stInteractionOutputCallback = defaultInteractionOutputCallback
	 }

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

---------------------------------------------------------------------------
-- ** Interface
---------------------------------------------------------------------------

data ModuleInfo = ModuleInfo
  { miInterface  :: Interface
  , miWarnings   :: Bool
    -- ^ 'True' if warnings were encountered when the module was type
    -- checked.
  , miTimeStamp  :: ClockTime
    -- ^ The modification time stamp of the interface file when the
    -- interface was read or written. Alternatively, if warnings were
    -- encountered (in which case there may not be any up-to-date
    -- interface file), the time at which the interface was produced
    -- (approximately).
  }

-- Note that the use of 'C.TopLevelModuleName' here is a potential
-- performance problem, because these names do not contain unique
-- identifiers.

type VisitedModules = Map C.TopLevelModuleName ModuleInfo
type DecodedModules = Map C.TopLevelModuleName (Interface, ClockTime)

data Interface = Interface
	{ iImportedModules :: [ModuleName]
        , iModuleName      :: ModuleName
	, iScope	   :: Map ModuleName Scope
        , iInsideScope     :: ScopeInfo
	, iSignature	   :: Signature
	, iBuiltin	   :: BuiltinThings (String, QName)
        , iHaskellImports  :: Set String
                              -- ^ Haskell imports listed in
                              -- (transitively) imported modules are
                              -- not included here.
        , iHighlighting    :: HighlightingInfo
        , iPragmaOptions   :: [OptionsPragma]
                              -- ^ Pragma options set in the file.
        , iPatternSyns     :: A.PatternSynDefns
	}
    deriving (Typeable, Show)

---------------------------------------------------------------------------
-- ** Closure
---------------------------------------------------------------------------

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

---------------------------------------------------------------------------
-- ** Constraints
---------------------------------------------------------------------------

type Constraints = [ProblemConstraint]

data ProblemConstraint = PConstr
  { constraintProblem :: ProblemId
  , theConstraint     :: Closure Constraint
  }
  deriving (Typeable, Show)

data Constraint
  = ValueCmp Comparison Type Term Term
  | ElimCmp [Polarity] Type Term [Elim] [Elim]
  | TypeCmp Comparison Type Type
  | TelCmp Type Type Comparison Telescope Telescope -- ^ the two types are for the error message only
  | SortCmp Comparison Sort Sort
  | LevelCmp Comparison Level Level
--  | ShortCut MetaId Term Type
--    -- ^ A delayed instantiation.  Replaces @ValueCmp@ in 'postponeTypeCheckingProblem'.
  | UnBlock MetaId
  | Guarded Constraint ProblemId
  | IsEmpty Range Type
    -- ^ the range is the one of the absurd pattern
  | FindInScope MetaId [(Term, Type)]
  deriving (Typeable, Show)

data Comparison = CmpEq | CmpLeq
  deriving (Eq, Typeable)

instance Show Comparison where
  show CmpEq  = "="
  show CmpLeq = "=<"

---------------------------------------------------------------------------
-- * Open things
---------------------------------------------------------------------------

-- | A thing tagged with the context it came from.
data Open a = OpenThing [CtxId] a
    deriving (Typeable, Show, Functor)

---------------------------------------------------------------------------
-- * Judgements
--
-- Used exclusively for typing of meta variables.
---------------------------------------------------------------------------

data Judgement t a
	= HasType { jMetaId :: a, jMetaType :: t }
	| IsSort  { jMetaId :: a, jMetaType :: t } -- Andreas, 2011-04-26: type needed for higher-order sort metas
    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

---------------------------------------------------------------------------
-- ** Meta variables
---------------------------------------------------------------------------

data MetaVariable =
	MetaVar	{ mvInfo	  :: MetaInfo
		, mvPriority	  :: MetaPriority -- ^ some metavariables are more eager to be instantiated
                , mvPermutation   :: Permutation
                  -- ^ a metavariable doesn't have to depend on all variables
                  --   in the context, this "permutation" will throw away the
                  --   ones it does not depend on
		, mvJudgement	  :: Judgement Type MetaId
		, mvInstantiation :: MetaInstantiation
		, mvListeners	  :: Set Listener -- ^ meta variables scheduled for eta-expansion but blocked by this one
                , mvFrozen        :: Frozen -- ^ are we past the point where we can instantiate this meta variable?
		}
    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{} = Prelude.GT

-- | Frozen meta variable cannot be instantiated by unification.
--   This serves to prevent the completion of a definition by its use
--   outside of the current block.
--   (See issues 118, 288, 399).
data Frozen
  = Frozen        -- ^ Do not instantiate.
  | Instantiable
    deriving (Eq, Show)

data MetaInstantiation
	= InstV Term         -- ^ solved by term
	| InstS Term         -- ^ solved by @Lam .. Sort s@
	| Open               -- ^ unsolved
	| OpenIFS            -- ^ open, to be instantiated as "implicit from scope"
	| BlockedConst Term  -- ^ solution blocked by unsolved constraints
        | PostponedTypeCheckingProblem (Closure (A.Expr, Type, TCM Bool))
    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)

-- | @MetaInfo@ is cloned from one meta to the next during pruning.
data MetaInfo = MetaInfo
  { miClosRange       :: Closure Range -- TODO: Not so nice. But we want both to have the environment of the meta (Closure) and its range.
--  , miRelevance       :: Relevance          -- ^ Created in irrelevant position?
  , miMetaOccursCheck :: RunMetaOccursCheck -- ^ Run the extended occurs check that goes in definitions?
  , miNameSuggestion  :: MetaNameSuggestion
    -- ^ Used for printing.
    --   @Just x@ if meta-variable comes from omitted argument with name @x@.
  }

-- | Name suggestion for meta variable.  Empty string means no suggestion.
type MetaNameSuggestion = String

-- | For printing, we couple a meta with its name suggestion.
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 MetaVariable where
    getRange m = getRange $ getMetaInfo m

instance SetRange MetaVariable where
  setRange r m = m { mvInfo = (mvInfo m)
                     { miClosRange = (miClosRange (mvInfo m))
                       { clValue = r }}}

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

---------------------------------------------------------------------------
-- ** Interaction meta variables
---------------------------------------------------------------------------

type InteractionPoints = Map InteractionId MetaId

newtype InteractionId = InteractionId Nat
    deriving (Eq,Ord,Num,Integral,Real,Enum)

instance Show InteractionId where
    show (InteractionId x) = "?" ++ show x

---------------------------------------------------------------------------
-- ** Signature
---------------------------------------------------------------------------

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	    -- ^ This is the number of parameters when
				    --	 we're inside the section and 0
				    --	 outside. It's used to know how much of
				    --	 the context to apply function from the
				    --	 section to when translating from
				    --	 abstract to internal syntax.
      }
  deriving (Typeable, Show)

emptySignature :: Signature
emptySignature = Sig Map.empty HMap.empty

data DisplayForm = Display Nat [Term] DisplayTerm
		-- ^ The three arguments are:
		--
		--   * @n@: number of free variables;
		--
		--   * Patterns for arguments, one extra free var which
		--     represents pattern vars. There should @n@ of them.
		--
		--   * Display form. @n@ free variables.
  deriving (Typeable, Show)

data DisplayTerm = DWithApp [DisplayTerm] Args
                 | DCon QName [Arg DisplayTerm]
                 | DDef QName [Arg DisplayTerm]
                 | DDot Term
		 | DTerm Term
  deriving (Typeable, Show)

defaultDisplayForm :: QName -> [Open DisplayForm]
defaultDisplayForm c = []

data Definition = Defn
  { defRelevance      :: Relevance -- ^ Some defs can be irrelevant (but not hidden).
  , defName           :: QName
  , defType           :: Type	      -- ^ Type of the lifted definition.
  , defPolarity       :: [Polarity]
  , defArgOccurrences :: [Occurrence]
  , defDisplay        :: [Open DisplayForm]
  , defMutual         :: MutualId
  , defCompiledRep    :: CompiledRepresentation
  , theDef            :: Defn
  }
    deriving (Typeable, Show)

type HaskellCode = String
type HaskellType = String
type EpicCode    = String
type JSCode      = JS.Exp

data HaskellRepresentation
      = HsDefn HaskellType HaskellCode
      | HsType HaskellType
  deriving (Typeable, Show)

-- | Polarity for equality and subtype checking.
data Polarity
  = Covariant      -- ^ monotone
  | Contravariant  -- ^ antitone
  | Invariant      -- ^ no information (mixed variance)
  | Nonvariant     -- ^ constant
  deriving (Typeable, Show, Eq)

data CompiledRepresentation = CompiledRep
  { compiledHaskell :: Maybe HaskellRepresentation
  , compiledEpic    :: Maybe EpicCode
  , compiledJS      :: Maybe JSCode
  }
  deriving (Typeable, Show)

noCompiledRep :: CompiledRepresentation
noCompiledRep = CompiledRep Nothing Nothing Nothing

-- | Subterm occurrences for positivity checking.
--   The constructors are listed in increasing information they provide:
--   @Mixed <= JustPos <= StrictPos <= GuardPos <= Unused@
--   @Mixed <= JustNeg <= Unused@.
data Occurrence
  = Mixed     -- ^ Arbitrary occurrence (positive and negative).
  | JustNeg   -- ^ Negative occurrence.
  | JustPos   -- ^ Positive occurrence, but not strictly positive.
  | StrictPos -- ^ Strictly positive occurrence.
  | GuardPos  -- ^ Guarded strictly positive occurrence (i.e., under ∞).  For checking recursive records.
  | Unused    --  ^ No occurrence.
  deriving (Typeable, Show, Eq, Ord)

instance NFData Occurrence

data Defn = Axiom
	  | Function
            { funClauses        :: [Clause]
            , funCompiled       :: CompiledClauses
            , funInv            :: FunctionInverse
{- MOVED to Definition
            , funPolarity       :: [Polarity]
            , funArgOccurrences :: [Occurrence]
-}
            , funMutual         :: [QName]
              -- ^ Mutually recursive functions, @data@s and @record@s.
            , funAbstr          :: IsAbstract
            , funDelayed        :: Delayed
              -- ^ Are the clauses of this definition delayed?
            , funProjection     :: Maybe (QName, Int)
              -- ^ Is it a record projection?
              --   If yes, then return the name of the record type and index of
              --   the record argument.  Start counting with 1, because 0 means that
              --   it is already applied to the record. (Can happen in module
              --   instantiation.) This information is used in the termination
              --   checker.
            , funStatic         :: Bool
              -- ^ Should calls to this function be normalised at compile-time?
            , funCopy           :: Bool
              -- ^ Has this function been created by a module
                                   -- instantiation?
            , funTerminates     :: Maybe Bool
              -- ^ Has this function been termination checked?  Did it pass?
            }
	  | Datatype
            { dataPars           :: Nat           -- nof parameters
	    , dataIxs            :: Nat           -- nof indices
            , dataInduction      :: Induction  -- data or codata?
            , dataClause         :: (Maybe Clause) -- this might be in an instantiated module
            , dataCons           :: [QName]        -- constructor names
            , dataSort           :: Sort
{- MOVED
            , dataPolarity       :: [Polarity]
            , dataArgOccurrences :: [Occurrence]
-}
            , dataMutual         :: [QName]        -- ^ Mutually recursive functions, @data@s and @record@s.
            , dataAbstr          :: IsAbstract
            }
	  | Record
            { recPars           :: Nat                  -- ^ Number of parameters.
            , recClause         :: Maybe Clause
            , recCon            :: QName                -- ^ Constructor name.
            , recNamedCon       :: Bool
            , recConType        :: Type                 -- ^ The record constructor's type.
            , recFields         :: [Arg A.QName]
            , recTel            :: Telescope            -- ^ The record field telescope
{- MOVED
            , recPolarity       :: [Polarity]
            , recArgOccurrences :: [Occurrence]
-}
            , recMutual         :: [QName]              -- ^ Mutually recursive functions, @data@s and @record@s.
            , recEtaEquality    :: Bool                 -- ^ Eta-expand at this record type.  @False@ for unguarded recursive records.
            , recInduction      :: Induction            -- ^ 'Inductive' or 'Coinductive'?  Matters only for recursive records.
            , recRecursive      :: Bool                 -- ^ Recursive record.  Implies @recEtaEquality = False@.  Projections are not size-preserving.
            , recAbstr          :: IsAbstract
            }
	  | Constructor
            { conPars   :: Nat         -- nof parameters
	    , conSrcCon :: QName       -- original constructor (this might be in a module instance)
	    , conData   :: QName       -- name of datatype or record type
	    , conAbstr  :: IsAbstract
            , conInd    :: Induction   -- ^ Inductive or coinductive?
            }
	  | Primitive
            { primAbstr :: IsAbstract
            , primName  :: String
            , primClauses :: Maybe [Clause]
              -- ^ 'Nothing' for primitive functions, @'Just'
              -- something@ for builtin functions.
            , primCompiled :: Maybe CompiledClauses
              -- ^ 'Nothing' for primitive functions, @'Just'
              -- something@ for builtin functions.
            }
            -- ^ Primitive or builtin functions.
    deriving (Typeable, Show)

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 Reduced no yes = NoReduction no | YesReduction yes
    deriving (Typeable, Functor)

data IsReduced = NotReduced | Reduced (Blocked ())
data MaybeReduced a = MaybeRed
  { isReduced     :: IsReduced
  , ignoreReduced :: a
  }
  deriving (Functor)

type MaybeReducedArgs = [MaybeReduced (Arg Term)]

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 PrimFun = PrimFun
	{ primFunName		:: QName
	, primFunArity		:: Arity
	, primFunImplementation :: [Arg Term] -> TCM (Reduced MaybeReducedArgs Term)
	}
    deriving (Typeable)

defClauses :: Definition -> [Clause]
defClauses Defn{theDef = Function{funClauses = cs}}        = cs
defClauses Defn{theDef = Primitive{primClauses = Just 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 = cc}} = Just cc
defCompiled Defn{theDef = Primitive{primCompiled = mcc}} = mcc
defCompiled _ = Nothing

defJSDef :: Definition -> Maybe JSCode
defJSDef = compiledJS . defCompiledRep

defEpicDef :: Definition -> Maybe EpicCode
defEpicDef = compiledEpic . defCompiledRep

-- | Are the clauses of this definition delayed?
defDelayed :: Definition -> Delayed
defDelayed Defn{theDef = Function{funDelayed = d}} = d
defDelayed _                                       = NotDelayed

-- | Is the definition just a copy created by a module instantiation?
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

---------------------------------------------------------------------------
-- ** Injectivity
---------------------------------------------------------------------------

type FunctionInverse = FunctionInverse' Clause

data FunctionInverse' c
  = NotInjective
  | Inverse (Map TermHead c)
  deriving (Typeable, Show, Functor)

data TermHead = SortHead
              | PiHead
              | ConHead QName
  deriving (Typeable, Eq, Ord, Show)

---------------------------------------------------------------------------
-- ** Mutual blocks
---------------------------------------------------------------------------

newtype MutualId = MutId Int32
  deriving (Typeable, Eq, Ord, Show, Num)

---------------------------------------------------------------------------
-- ** Statistics
---------------------------------------------------------------------------

type Statistics = Map String Integer

---------------------------------------------------------------------------
-- ** Trace
---------------------------------------------------------------------------

data Call = CheckClause Type A.Clause (Maybe Clause)
	  | forall a. CheckPattern A.Pattern Telescope Type (Maybe a)
	  | CheckLetBinding A.LetBinding (Maybe ())
	  | InferExpr A.Expr (Maybe (Term, Type))
	  | CheckExpr A.Expr Type (Maybe Term)
	  | CheckDotPattern A.Expr Term (Maybe Constraints)
	  | CheckPatternShadowing A.Clause (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)	-- ^ used by 'setCurrentRange'
    deriving (Typeable)

instance HasRange Call where
    getRange (CheckClause _ c _)                   = getRange c
    getRange (CheckPattern p _ _ _)                = getRange p
    getRange (InferExpr e _)                       = getRange e
    getRange (CheckExpr 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

---------------------------------------------------------------------------
-- ** Builtin things
---------------------------------------------------------------------------

data BuiltinDescriptor = BuiltinData (TCM Type) [String]
                       | BuiltinDataCons (TCM Type)
                       | BuiltinPrim String (Term -> TCM ())
                       | BuiltinPostulate Relevance (TCM Type)
                       | BuiltinUnknown (Maybe (TCM Type)) (Term -> 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)

---------------------------------------------------------------------------
-- * Highlighting levels
---------------------------------------------------------------------------

-- | How much highlighting should be sent to the user interface?

data HighlightingLevel
  = None
  | NonInteractive
  | Interactive
    -- ^ This includes both non-interactive highlighting and
    -- interactive highlighting of the expression that is currently
    -- being type-checked.
    deriving (Eq, Ord, Show, Read)

-- | How should highlighting be sent to the user interface?

data HighlightingMethod
  = Direct
    -- ^ Via stdout.
  | Indirect
    -- ^ Both via files and via stdout.
    deriving (Eq, Show, Read)

-- | @ifTopLevelAndHighlightingLevelIs l m@ runs @m@ when we're
-- type-checking the top-level module and the highlighting level is
-- /at least/ @l@.

ifTopLevelAndHighlightingLevelIs ::
  MonadTCM tcm => HighlightingLevel -> tcm () -> tcm ()
ifTopLevelAndHighlightingLevelIs l m = do
  e <- ask
  when (envModuleNestingLevel e == 0 &&
        envHighlightingLevel e >= l)
       m

---------------------------------------------------------------------------
-- * Type checking environment
---------------------------------------------------------------------------

data TCEnv =
    TCEnv { envContext             :: Context
	  , envLetBindings         :: LetBindings
	  , envCurrentModule       :: ModuleName
	  , envCurrentPath         :: AbsolutePath
            -- ^ The path to the file that is currently being
            -- type-checked.
          , envAnonymousModules    :: [(ModuleName, Nat)] -- ^ anonymous modules and their number of free variables
	  , envImportPath          :: [C.TopLevelModuleName] -- ^ to detect import cycles
	  , envMutualBlock         :: Maybe MutualId -- ^ the current (if any) mutual block
          , envSolvingConstraints  :: Bool
                -- ^ Are we currently in the process of solving active constraints?
          , envAssignMetas         :: Bool
            -- ^ Are we allowed to assign metas?
          , envActiveProblems      :: [ProblemId]
	  , envAbstractMode        :: AbstractMode
		-- ^ When checking the typesignature of a public definition
		--   or the body of a non-abstract definition this is true.
		--   To prevent information about abstract things leaking
		--   outside the module.
          , envRelevance           :: Relevance
                -- ^ Are we checking an irrelevant argument? (=@Irrelevant@)
                -- Then top-level irrelevant declarations are enabled.
                -- Other value: @Relevant@, then only relevant decls. are avail.
          , envDisplayFormsEnabled :: Bool
                -- ^ Sometimes we want to disable display forms.
          , envReifyInteractionPoints :: Bool
                -- ^ should we try to recover interaction points when reifying?
                --   disabled when generating types for with functions
          , envEtaContractImplicit :: Bool
                -- ^ it's safe to eta contract implicit lambdas as long as we're
                --   not going to reify and retypecheck (like when doing with
                --   abstraction)
          , envRange :: Range
          , envHighlightingRange :: Range
                -- ^ Interactive highlighting uses this range rather
                --   than 'envRange'.
          , envCall  :: Maybe (Closure Call)
                -- ^ what we're doing at the moment
          , envEmacs :: Bool
                -- ^ True when called from the Emacs mode.
          , envHighlightingLevel  :: HighlightingLevel
                -- ^ Set to 'None' when imported modules are
                --   type-checked.
          , envHighlightingMethod :: HighlightingMethod
          , envModuleNestingLevel :: Integer
                -- ^ This number indicates how far away from the
                --   top-level module Agda has come when chasing
                --   modules. The level of a given module is not
                --   necessarily the same as the length, in the module
                --   dependency graph, of the shortest path from the
                --   top-level module; it depends on in which order
                --   Agda chooses to chase dependencies.
          , envAllowDestructiveUpdate :: Bool
                -- ^ When True, allows destructively shared updating terms
                --   during evaluation or unification. This is disabled when
                --   doing speculative checking, like solve instance metas, or
                --   when updating might break abstraction, as is the case when
                --   checking abstract definitions.
	  }
    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        = AbstractMode
                , envRelevance           = Relevant
                , envDisplayFormsEnabled = True
                , envReifyInteractionPoints = True
                , envEtaContractImplicit    = True
                , envRange                  = noRange
                , envHighlightingRange      = noRange
                , envCall                   = Nothing
                , envEmacs                  = False
                , envHighlightingLevel      = None
                , envHighlightingMethod     = Indirect
                , envModuleNestingLevel     = -1
                , envAllowDestructiveUpdate = True
		}

---------------------------------------------------------------------------
-- ** Context
---------------------------------------------------------------------------

-- | The @Context@ is a stack of 'ContextEntry's.
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)

---------------------------------------------------------------------------
-- ** Let bindings
---------------------------------------------------------------------------

type LetBindings = Map Name (Open (Term, Dom Type))

---------------------------------------------------------------------------
-- ** Abstract mode
---------------------------------------------------------------------------

data AbstractMode = AbstractMode       -- ^ abstract things in the current module can be accessed
		  | ConcreteMode       -- ^ no abstract things can be accessed
		  | IgnoreAbstractMode -- ^ all abstract things can be accessed
  deriving (Typeable)

---------------------------------------------------------------------------
-- ** Insertion of implicit arguments
---------------------------------------------------------------------------

data ExpandHidden
  = ExpandLast      -- ^ Add implicit arguments in the end until type is no longer hidden 'Pi'.
  | DontExpandLast  -- ^ Do not append implicit arguments.

data ExpandInstances
  = ExpandInstanceArguments
  | DontExpandInstanceArguments
    deriving (Eq)

---------------------------------------------------------------------------
-- * Type checking errors
---------------------------------------------------------------------------

-- Occurence of a name in a datatype definition
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)

-- | Information about a call.

data CallInfo = CallInfo
  { callInfoRange :: Range
    -- ^ Range of the head identifier.
  , callInfoCall :: String
    -- ^ Formatted representation of the call.
    --
    -- ('Doc' would perhaps be better here, but 'Doc' doesn't come
    -- with an 'Ord' instance.)
  } deriving (Eq, Ord, Typeable, Show)

-- | Information about a mutual block which did not pass the
-- termination checker.

data TerminationError = TerminationError
  { termErrFunctions :: [QName]
    -- ^ The functions which failed to check. (May not include
    -- automatically generated functions.)
  , termErrCalls :: [CallInfo]
    -- ^ The problematic call sites.
  } deriving (Typeable, Show, Eq)

{-
-- | We consider two 'TerminationError's equal if they report the same
--   invalid calls.
instance Eq TerminationError where
  (==) = (==) `on` termErrCalls
-}

data TypeError
	= InternalError String
	| NotImplemented String
	| NotSupported String
        | CompilationError String
	| TerminationCheckFailed [TerminationError]
	| PropMustBeSingleton
	| DataMustEndInSort Term
{- UNUSED
        | DataTooManyParameters
            -- ^ In @data D xs where@ the number of parameters @xs@ does not fit the
            --   the parameters given in the forward declaraion @data D Gamma : T@.
-}
	| ShouldEndInApplicationOfTheDatatype Type
	    -- ^ The target of a constructor isn't an application of its
	    -- datatype. The 'Type' records what it does target.
	| ShouldBeAppliedToTheDatatypeParameters Term Term
	    -- ^ The target of a constructor isn't its datatype applied to
	    --	 something that isn't the parameters. First term is the correct
	    --	 target and the second term is the actual target.
	| ShouldBeApplicationOf Type QName
	    -- ^ Expected a type to be an application of a particular datatype.
	| ConstructorPatternInWrongDatatype QName QName -- ^ constructor, datatype
        | IndicesNotConstructorApplications [Arg Term] -- ^ Indices.
        | IndexVariablesNotDistinct [Nat] [Arg Term] -- ^ Variables, indices.
        | IndicesFreeInParameters [Nat] [Arg Term] [Arg Term]
          -- ^ Indices (variables), index expressions (with
          -- constructors applied to reconstructed parameters),
          -- parameters.
        | DoesNotConstructAnElementOf QName Term -- ^ constructor, type
	| DifferentArities
	    -- ^ Varying number of arguments for a function.
	| WrongHidingInLHS Type
	    -- ^ The left hand side of a function definition has a hidden argument
	    --	 where a non-hidden was expected.
	| WrongHidingInLambda Type
	    -- ^ Expected a non-hidden function and found a hidden lambda.
	| WrongHidingInApplication Type
	    -- ^ A function is applied to a hidden argument where a non-hidden was expected.
	| WrongIrrelevanceInLambda Type
	    -- ^ Expected a relevant function and found an irrelevant lambda.
	| NotInductive Term
          -- ^ The term does not correspond to an inductive data type.
	| UninstantiatedDotPattern A.Expr
	| IlltypedPattern A.Pattern Type
	| TooManyArgumentsInLHS Type
	| WrongNumberOfConstructorArguments QName Nat Nat
	| ShouldBeEmpty Type [Pattern]
	| ShouldBeASort Type
	    -- ^ The given type should have been a sort.
	| ShouldBePi Type
	    -- ^ The given type should have been a pi.
	| ShouldBeRecordType Type
	| ShouldBeRecordPattern Pattern
	| NotAProperTerm
        | SetOmegaNotValidType
        | SplitOnIrrelevant A.Pattern (Dom Type)
        | DefinitionIsIrrelevant QName
        | VariableIsIrrelevant Name
        | UnequalLevel Comparison Term Term
	| UnequalTerms Comparison Term Term Type
	| UnequalTypes Comparison Type Type
	| UnequalTelescopes Comparison Telescope Telescope
	| UnequalRelevance Comparison Term Term
	    -- ^ The two function types have different relevance.
	| UnequalHiding Term Term
	    -- ^ The two function types have different hiding.
	| UnequalSorts Sort Sort
        | UnequalBecauseOfUniverseConflict Comparison Term Term
        | HeterogeneousEquality Term Type Term Type
            -- ^ We ended up with an equality constraint where the terms
            --   have different types.  This is not supported.
	| NotLeqSort Sort Sort
	| MetaCannotDependOn MetaId [Nat] Nat
	    -- ^ The arguments are the meta variable, the parameters it can
	    --	 depend on and the paratemeter that it wants to depend on.
	| 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
	| 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]
    -- Coverage errors
	| IncompletePatternMatching Term Args -- can only happen if coverage checking is switched off
        | CoverageFailure QName [[Arg Pattern]]
        | UnreachableClauses QName [[Arg Pattern]]
        | CoverageCantSplitOn QName Telescope Args Args
        | CoverageCantSplitIrrelevantType Type
        | CoverageCantSplitType Type
    -- Positivity errors
	| NotStrictlyPositive QName [Occ]
    -- Import errors
	| 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
          -- ^ Module name, file from which it was loaded, file which
          -- the include path says contains the module.
    -- Scope errors
	| 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]
    -- Concrete to Abstract errors
	| NotAModuleExpr C.Expr
	    -- ^ The expr was used in the right hand side of an implicit module
	    --	 definition, but it wasn't of the form @m Delta@.
	| NotAnExpression C.Expr
	| NotAValidLetBinding D.NiceDeclaration
	| NothingAppliedToHiddenArg C.Expr
	| NothingAppliedToInstanceArg C.Expr
        | UnusedVariableInPatternSynonym
        | PatternSynonymArityMismatch A.QName
    -- Operator errors
	| NoParseForApplication [C.Expr]
	| AmbiguousParseForApplication [C.Expr] [C.Expr]
	| NoParseForLHS LHSOrPatSyn C.Pattern
	| AmbiguousParseForLHS LHSOrPatSyn C.Pattern [C.Pattern]
{- UNUSED
	| NoParseForPatternSynonym C.Pattern
	| AmbiguousParseForPatternSynonym C.Pattern [C.Pattern]
-}
    -- Usage errors
    -- Implicit From Scope errors
        | IFSNoCandidateInScope Type
    -- Safe flag errors
        | SafeFlagPostulate C.Name
        | SafeFlagPragma [String]
        | SafeFlagNoTerminationCheck
        | SafeFlagPrimTrustMe
    -- Language option errors
        | NeedOptionCopatterns
          deriving (Typeable, Show)

-- | Distinguish error message when parsing lhs or pattern synonym, resp.
data LHSOrPatSyn = IsLHS | IsPatSyn deriving (Eq, Show)

-- instance Show TypeError where
--   show _ = "<TypeError>" -- TODO: more info?

instance Error TypeError where
    noMsg  = strMsg ""
    strMsg = GenericError

-- | Type-checking errors.

data TCErr = TypeError TCState (Closure TypeError)
	   | Exception Range String
           | IOException Range E.IOException
	   | PatternErr  TCState -- ^ for pattern violations
	   {- AbortAssign TCState -- ^ used to abort assignment to meta when there are instantiations -- UNUSED -}
  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)"
    {- show (AbortAssign _) = "Abort assignment (you shouldn't see this)" -- UNUSED -}

instance HasRange TCErr where
    getRange (TypeError _ cl)  = envRange $ clEnv cl
    getRange (Exception r _)   = r
    getRange (IOException r _) = r
    getRange (PatternErr s)    = noRange
    {- getRange (AbortAssign s)   = noRange -- UNUSED -}

instance Exception TCErr

---------------------------------------------------------------------------
-- * Type checking monad transformer
---------------------------------------------------------------------------

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
      -- Reset the state, but do not forget changes to the persistent
      -- component.
      liftIO $ do
        newState <- readIORef r
        writeIORef r $ oldState { stPersistent = stPersistent newState }
      unTCM (h err) r e

-- | Preserve the state of the failing computation.
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

{-# SPECIALIZE INLINE mapTCMT :: (forall a. IO a -> IO a) -> TCM a -> TCM a #-}
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)

{-# RULES "liftTCM/id" liftTCM = id #-}
instance MonadIO m => MonadTCM (TCMT m) where
    liftTCM = mapTCMT liftIO

instance (Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) where
  liftTCM = lift . liftTCM

instance MonadTrans TCMT where
    lift m = TCM $ \_ _ -> m

-- We want a special monad implementation of fail.
instance MonadIO m => Monad (TCMT m) where
    return = returnTCMT
    (>>=)  = bindTCMT
    (>>)   = thenTCMT
    fail   = internalError

-- One goal of the definitions and pragmas below is to inline the
-- monad operations as much as possible. This doesn't seem to have a
-- large effect on the performance of the normal executable, but (at
-- least on one machine/configuration) it has a massive effect on the
-- performance of the profiling executable [1], and reduces the time
-- attributed to bind from over 90% to about 25%.
--
-- [1] When compiled with -auto-all and run with -p: roughly 750%
-- faster for one example.

returnTCMT :: MonadIO m => a -> TCMT m a
returnTCMT = \x -> TCM $ \_ _ -> return x
{-# RULES "returnTCMT"
      returnTCMT = \x -> TCM $ \_ _ -> return x
  #-}
{-# INLINE returnTCMT #-}
{-# SPECIALIZE INLINE returnTCMT :: a -> TCM a #-}

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
{-# RULES "bindTCMT"
      bindTCMT = \(TCM m) k -> TCM $ \r e ->
                   m r e >>= \x -> unTCM (k x) r e
  #-}
{-# INLINE bindTCMT #-}
{-# SPECIALIZE INLINE bindTCMT :: TCM a -> (a -> TCM b) -> TCM b #-}

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
{-# RULES "thenTCMT"
      thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e
  #-}
{-# INLINE thenTCMT #-}
{-# SPECIALIZE INLINE thenTCMT :: TCM a -> TCM b -> TCM b #-}

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)
{-# RULES "fmapTCMT"
      fmapTCMT = \f (TCM m) -> TCM $ \r e -> liftM f (m r e)
  #-}
{-# INLINE fmapTCMT #-}
{-# SPECIALIZE INLINE fmapTCMT :: (a -> b) -> TCM a -> TCM b #-}

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)
{-# RULES "apTCMT"
      apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> ap (mf r e) (m r e)
  #-}
{-# INLINE apTCMT #-}
{-# SPECIALIZE INLINE apTCMT :: TCM (a -> b) -> TCM a -> TCM b #-}

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

-- | Running the type checking monad
runTCM :: TCMT IO a -> IO (Either TCErr a)
runTCM m = (Right <$> runTCM' m) `E.catch` (return . Left)

runTCM' :: MonadIO m => TCMT m a -> m a
runTCM' m = do
  r <- liftIO $ newIORef initState
  unTCM m r initEnv

-- | Runs the given computation in a separate thread, with /a copy/ of
-- the current state and environment.
--
-- Note that Agda sometimes uses actual, mutable state. If the
-- computation given to @forkTCM@ tries to /modify/ this state, then
-- bad things can happen, because accesses are not mutually exclusive.
-- The @forkTCM@ function has been added mainly to allow the thread to
-- /read/ (a snapshot of) the current state in a convenient way.
--
-- Note also that exceptions which are raised in the thread are not
-- propagated to the parent, so the thread should not do anything
-- important.

forkTCM :: TCM a -> TCM ()
forkTCM m = do
  s <- get
  e <- ask
  liftIO $ C.forkIO $ do
    runTCM $ local (\_ -> e) $ do
      put s
      m
    return ()
  return ()



-- | Base name for extended lambda patterns
extendlambdaname = ".extendedlambda"