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

import Control.Arrow
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.Generics
import Data.Foldable
import Data.Traversable
import Data.IORef
import System.Time

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.TypeChecking.CompiledClause

import Agda.Interaction.Exceptions
import {-# SOURCE #-} Agda.Interaction.FindFile
import Agda.Interaction.Options
import qualified Agda.Interaction.Highlighting.Range as R
import Agda.Interaction.Highlighting.Precise (HighlightingInfo)

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

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

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

data TCState =
    TCSt { stFreshThings       :: FreshThings
	 , stMetaStore	       :: MetaStore
	 , stInteractionPoints :: InteractionPoints
	 , stAwakeConstraints    :: Constraints
	 , stSleepingConstraints :: Constraints
	 , 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
	 , 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
	 }

-- | 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
              , fInteger     :: Integer
                -- ^ 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
	 , stInteractionPoints = Map.empty
	 , stAwakeConstraints    = []
	 , stSleepingConstraints = []
	 , stSignature	       = emptySignature
	 , stImports	       = emptySignature
	 , stImportedModules   = Set.empty
         , stModuleToSource    = Map.empty
	 , stVisitedModules    = Map.empty
         , stCurrentModule     = Nothing
	 , stScope	       = emptyScopeInfo
	 , stPragmaOptions     = optPragmaOptions $ defaultOptions
	 , 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
           }
	 }

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 Integer FreshThings where
    nextFresh s = (i, s { fInteger = succ i })
	where
	    i = fInteger s

newtype ProblemId = ProblemId Nat
  deriving (Typeable, Data, 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
        , iHaskellImports  :: Set String
                              -- ^ Haskell imports listed in
                              -- (transitively) imported modules are
                              -- not included here.
        , iHighlighting    :: HighlightingInfo
        , iPragmaOptions   :: [OptionsPragma]
                              -- ^ Pragma options set in the file.
	}
    deriving (Typeable, Data, Show)

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

data Closure a = Closure { clSignature  :: Signature
			 , clEnv	:: TCEnv
			 , clScope	:: ScopeInfo
			 , clValue	:: a
			 }
    deriving (Typeable, Data)

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
  | UnBlock MetaId
  | Guarded Constraint ProblemId
  | IsEmpty Type
  | FindInScope MetaId
  deriving (Typeable, Show)

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

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

-- | A thing tagged with the context it came from.
data Open a = OpenThing [CtxId] a
    deriving (Typeable, Data, 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, Data, 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)

-- | TODO: Not so nice.
type MetaInfo = Closure Range

type MetaStore = Map MetaId MetaVariable

instance HasRange MetaVariable where
    getRange m = getRange $ getMetaInfo m

instance SetRange MetaVariable where
  setRange r (MetaVar mi p perm j inst ls frozen) =
    MetaVar (mi {clValue = r}) p perm j inst ls frozen

normalMetaPriority :: MetaPriority
normalMetaPriority = MetaPriority 0

lowMetaPriority :: MetaPriority
lowMetaPriority = MetaPriority (-10)

highMetaPriority :: MetaPriority
highMetaPriority = MetaPriority 10

getMetaInfo :: MetaVariable -> MetaInfo
getMetaInfo = 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

---------------------------------------------------------------------------
-- ** 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, Data, Show)

type Sections	 = Map ModuleName Section
type Definitions = Map 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, Data, Show)

emptySignature :: Signature
emptySignature = Sig Map.empty Map.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, Data, Show)

data DisplayTerm = DWithApp [DisplayTerm] Args
                 | DCon QName [Arg DisplayTerm]
                 | DDef QName [Arg DisplayTerm]
                 | DDot Term
		 | DTerm Term
  deriving (Typeable, Data, 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.
  , defDisplay     :: [Open DisplayForm]
  , defMutual      :: MutualId
  , defCompiledRep :: CompiledRepresentation
  , theDef         :: Defn
  }
    deriving (Typeable, Data, Show)

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

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

data Polarity = Covariant | Contravariant | Invariant
  deriving (Typeable, Data, Show, Eq)

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

noCompiledRep :: CompiledRepresentation
noCompiledRep = CompiledRep Nothing Nothing Nothing

-- | 'Positive' means strictly positive and 'Negative' means not strictly
-- positive.
data Occurrence = Positive | Negative | Unused
  deriving (Typeable, Data, Show, Eq, Ord)

data Defn = Axiom
	  | Function
            { funClauses        :: [Clause]
            , funCompiled       :: CompiledClauses
            , funInv            :: FunctionInverse
            , funPolarity       :: [Polarity]
            , funArgOccurrences :: [Occurrence]
            , 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?
            }
	  | 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
            , dataPolarity       :: [Polarity]
            , dataArgOccurrences :: [Occurrence]
            , dataAbstr          :: IsAbstract
            }
	  | Record
            { recPars           :: Nat
            , 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
            , recPolarity       :: [Polarity]
            , recArgOccurrences :: [Occurrence]
            , recEtaEquality    :: Bool
            , 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, Data, Show)

defIsRecord :: Defn -> Bool
defIsRecord Record{} = True
defIsRecord _        = False

newtype Fields = Fields [(C.Name, Type)]
  deriving (Typeable, Data)

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 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

-- | Used to specify whether something should be delayed.
data Delayed = Delayed | NotDelayed
  deriving (Typeable, Data, Show, Eq)

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

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
---------------------------------------------------------------------------

data FunctionInverse = NotInjective
                     | Inverse (Map TermHead Clause)
  deriving (Typeable, Data, Show)

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

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

newtype MutualId = MutId Int32
  deriving (Typeable, Data, 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 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. TermFunDef Range Name [A.Clause] (Maybe a)
	  | forall a. SetRange Range (Maybe a)	-- ^ used by 'setCurrentRange'
            -- actually, 'a' is Agda.Termination.TermCheck.CallGraph
            -- but I was to lazy to import the stuff here --Andreas,2007-5-29

    deriving (Typeable)

-- Dummy instance
instance Data Call where
  dataTypeOf _  = mkDataType "Call" []
  toConstr   x  = mkConstr (dataTypeOf x) "Dummy" [] Prefix
  gunfold k z _ = __IMPOSSIBLE__

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 (TermFunDef i _ _ _)                  = getRange i
    getRange (SetRange r _)                        = r
    getRange (CheckSectionApplication r _ _ _)     = r
    getRange (CheckIsEmpty _ _)                    = noRange

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

data BuiltinDescriptor = BuiltinData (TCM Type) [String]
                       | BuiltinDataCons (TCM Type)
                       | BuiltinPrim String (Term -> TCM ())
                       | BuiltinPostulate (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, Data, Show, Functor, Foldable, Traversable)

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

data TCEnv =
    TCEnv { envContext             :: Context
	  , envLetBindings         :: LetBindings
	  , envCurrentModule       :: ModuleName
          , 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?
          , 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.
          , envTopLevel            :: Bool
                -- ^ Are we at the top level when checking a declaration?
                --   In this case, we will freeze metas afterwards.
          , 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
          , envCall  :: Maybe (Closure Call)
                -- ^ what we're doing at the moment
	  }
    deriving (Typeable, Data)

initEnv :: TCEnv
initEnv = TCEnv { envContext	         = []
		, envLetBindings         = Map.empty
		, envCurrentModule       = noModuleName
                , envAnonymousModules    = []
		, envImportPath          = []
		, envMutualBlock         = Nothing
                , envSolvingConstraints  = False
                , envActiveProblems      = [0]
		, envAbstractMode        = AbstractMode
                , envTopLevel            = True
                , envRelevance           = Relevant
                , envDisplayFormsEnabled = True
                , envReifyInteractionPoints = True
                , envEtaContractImplicit    = True
                , envRange                  = noRange
                , envCall                   = Nothing
		}

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

type Context	  = [ContextEntry]
data ContextEntry = Ctx { ctxId	   :: CtxId
			, ctxEntry :: Arg (Name, Type)
			}
  deriving (Typeable, Data)

newtype CtxId	  = CtxId Nat
  deriving (Typeable, Data, Eq, Ord, Show, Enum, Real, Integral, Num)

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

type LetBindings = Map Name (Open (Term, Arg 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, Data)

---------------------------------------------------------------------------
-- * 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)

data TypeError
	= InternalError String
	| NotImplemented String
	| NotSupported String
        | CompilationError String
	| TerminationCheckFailed [TerminationError]
	| PropMustBeSingleton
	| DataMustEndInSort Term
	| 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 [Arg Term] -- ^ Indices.
        | IndexFreeInParameter Nat [Arg Term] -- ^ Index (a variable), 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 Nat 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
	| NotAProperTerm
        | SplitOnIrrelevant A.Pattern (Arg Type)
        | DefinitionIsIrrelevant QName
        | VariableIsIrrelevant Name
        | UnequalLevel Comparison Term Term
	| UnequalTerms Comparison Term Term Type
	| UnequalTypes Comparison Type Type
	| UnequalTelescopes Comparison Telescope Telescope
	| UnequalRelevance Type Type
	    -- ^ The two function types have different relevance.
	| UnequalHiding Type Type
	    -- ^ The two function types have different hiding.
	| UnequalSorts Sort Sort
        | 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
        | BuiltinMustBeConstructor String A.Expr
	| NoSuchBuiltinName String
	| DuplicateBuiltinBinding String Term Term
	| NoBindingForBuiltin String
	| NoSuchPrimitiveFunction String
        | ShadowedModule [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
    -- Operator errors
	| NoParseForApplication [C.Expr]
	| AmbiguousParseForApplication [C.Expr] [C.Expr]
	| NoParseForLHS C.Pattern
	| AmbiguousParseForLHS C.Pattern [C.Pattern]
    -- Usage errors
    -- Implicit From Scope errors
        | IFSNoCandidateInScope Type
    -- Safe flag errors
        | SafeFlagPostulate C.Name
        | SafeFlagPragma [String]
        | SafeFlagPrimTrustMe
          deriving (Typeable, 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)

-- | Type-checking errors, potentially paired with relevant syntax
-- highlighting information.

data TCErr =
  TCErr { errHighlighting :: Maybe (HighlightingInfo, ModuleToSource)
          -- ^ The 'ModuleToSource' can be used to map the module
          -- names in the 'HighlightingInfo' to file names.
        , errError        :: TCErr'
        }
  deriving (Typeable)

instance Error TCErr where
    noMsg  = strMsg ""
    strMsg = TCErr Nothing . Exception noRange . strMsg

instance Show TCErr where
  show = show . errError

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 HasRange TCErr where
    getRange = getRange . errError

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 x = TCM $ \_ _ -> return x
    TCM m >>= k = TCM $ \r e -> do
        x <- m r e
        let TCM m' = k x in m' r e
    TCM m1 >> TCM m2 = TCM $ \r e -> m1 r e >> m2 r e
    fail    = internalError

    {-# SPECIALIZE instance Monad TCM #-}

instance MonadIO m => Functor (TCMT m) where
    fmap = liftM

instance MonadIO m => Applicative (TCMT m) where
    pure = return
    (<*>) = ap

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 $ TCErr Nothing $ IOException r e
      handleException   r s = throwIO $ TCErr Nothing $ Exception r s

patternViolation :: TCM a
patternViolation = do
    s <- get
    throwError $ TCErr Nothing $ 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 $ TCErr Nothing $ 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




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