module Agda.TypeChecking.Monad.Builtin where

import Data.Functor
import Control.Monad.State
import qualified Data.Map as Map

import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base

getBuiltinThing :: String -> TCM (Maybe (Builtin PrimFun))
getBuiltinThing b = liftM2 mplus (Map.lookup b <$> gets stLocalBuiltins)
                    (Map.lookup b <$> gets stImportedBuiltins)

setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
setBuiltinThings b = modify $ \s -> s { stLocalBuiltins = b }

bindBuiltinName :: String -> Term -> TCM ()
bindBuiltinName b x = do
	builtin <- getBuiltinThing b
	case builtin of
	    Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x
	    Just (Prim _)    -> typeError $ NoSuchBuiltinName b
	    Nothing	     -> modify $ \st ->
              st { stLocalBuiltins =
                    Map.insert b (Builtin x) $ stLocalBuiltins st
                 }

bindPrimitive :: String -> PrimFun -> TCM ()
bindPrimitive b pf = do
  builtin <- gets stLocalBuiltins
  setBuiltinThings $ Map.insert b (Prim pf) builtin


getBuiltin :: String -> TCM Term
getBuiltin x = do
    mt <- getBuiltin' x
    case mt of
        Nothing -> typeError $ NoBindingForBuiltin x
        Just t  -> return t

getBuiltin' :: String -> TCM (Maybe Term)
getBuiltin' x = do
    builtin <- getBuiltinThing x
    case builtin of
	Just (Builtin t) -> return $ Just (killRange t)
	_		 -> return Nothing

getPrimitive :: String -> TCM PrimFun
getPrimitive x = do
    builtin <- getBuiltinThing x
    case builtin of
	Just (Prim pf) -> return pf
	_	       -> typeError $ NoSuchPrimitiveFunction x

---------------------------------------------------------------------------
-- * The names of built-in things
---------------------------------------------------------------------------

primInteger, primFloat, primChar, primString, primBool, primTrue, primFalse,
    primList, primNil, primCons, primIO, primNat, primSuc, primZero,
    primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
    primNatEquality, primNatLess, primSize, primSizeSuc, primSizeInf,
    primInf, primSharp, primFlat,
    primEquality, primRefl,
    primLevel, primLevelZero, primLevelSuc, primLevelMax,
    -- builtins for reflection:
    primQName, primArg, primArgArg, primAgdaTerm, primAgdaTermVar,
    primAgdaTermLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
    primAgdaTermSort, primAgdaTermUnsupported,
    primAgdaType, primAgdaTypeEl,
    primHiding, primHidden, primInstance, primVisible,
    primRelvance, primRelevant, primIrrelevant,
    primAgdaSort, primAgdaSortSet, primAgdaSortLit, primAgdaSortUnsupported,
    primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef,
    primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor,
    primAgdaFunDef, primAgdaDataDef, primAgdaRecordDef
    :: TCM Term
primInteger      = getBuiltin builtinInteger
primFloat        = getBuiltin builtinFloat
primChar         = getBuiltin builtinChar
primString       = getBuiltin builtinString
primBool         = getBuiltin builtinBool
primTrue         = getBuiltin builtinTrue
primFalse        = getBuiltin builtinFalse
primList         = getBuiltin builtinList
primNil          = getBuiltin builtinNil
primCons         = getBuiltin builtinCons
primIO           = getBuiltin builtinIO
primNat          = getBuiltin builtinNat
primSuc          = getBuiltin builtinSuc
primZero         = getBuiltin builtinZero
primNatPlus      = getBuiltin builtinNatPlus
primNatMinus     = getBuiltin builtinNatMinus
primNatTimes     = getBuiltin builtinNatTimes
primNatDivSucAux = getBuiltin builtinNatDivSucAux
primNatModSucAux = getBuiltin builtinNatModSucAux
primNatEquality  = getBuiltin builtinNatEquals
primNatLess      = getBuiltin builtinNatLess
primSize         = getBuiltin builtinSize
primSizeSuc      = getBuiltin builtinSizeSuc
primSizeInf      = getBuiltin builtinSizeInf
primInf          = getBuiltin builtinInf
primSharp        = getBuiltin builtinSharp
primFlat         = getBuiltin builtinFlat
primEquality     = getBuiltin builtinEquality
primRefl         = getBuiltin builtinRefl
primLevel        = getBuiltin builtinLevel
primLevelZero    = getBuiltin builtinLevelZero
primLevelSuc     = getBuiltin builtinLevelSuc
primLevelMax     = getBuiltin builtinLevelMax
primQName        = getBuiltin builtinQName
primArg          = getBuiltin builtinArg
primArgArg       = getBuiltin builtinArgArg
primAgdaSort     = getBuiltin builtinAgdaSort
primAgdaType     = getBuiltin builtinAgdaType
primAgdaTypeEl   = getBuiltin builtinAgdaTypeEl
primHiding       = getBuiltin builtinHiding
primHidden       = getBuiltin builtinHidden
primInstance     = getBuiltin builtinInstance
primVisible      = getBuiltin builtinVisible
primRelvance     = getBuiltin builtinRelevance
primRelevant     = getBuiltin builtinRelevant
primIrrelevant   = getBuiltin builtinIrrelevant
primAgdaSortSet  = getBuiltin builtinAgdaSortSet
primAgdaSortLit  = getBuiltin builtinAgdaSortLit
primAgdaSortUnsupported = getBuiltin builtinAgdaSortUnsupported
primAgdaTerm         = getBuiltin builtinAgdaTerm
primAgdaTermVar      = getBuiltin builtinAgdaTermVar
primAgdaTermLam      = getBuiltin builtinAgdaTermLam
primAgdaTermDef      = getBuiltin builtinAgdaTermDef
primAgdaTermCon      = getBuiltin builtinAgdaTermCon
primAgdaTermPi       = getBuiltin builtinAgdaTermPi
primAgdaTermSort     = getBuiltin builtinAgdaTermSort
primAgdaTermUnsupported     = getBuiltin builtinAgdaTermUnsupported
primAgdaFunDef                    = getBuiltin builtinAgdaFunDef
primAgdaDataDef                   = getBuiltin builtinAgdaDataDef
primAgdaRecordDef                 = getBuiltin builtinAgdaRecordDef
primAgdaDefinitionFunDef          = getBuiltin builtinAgdaDefinitionFunDef
primAgdaDefinitionDataDef         = getBuiltin builtinAgdaDefinitionDataDef
primAgdaDefinitionRecordDef       = getBuiltin builtinAgdaDefinitionRecordDef
primAgdaDefinitionDataConstructor = getBuiltin builtinAgdaDefinitionDataConstructor
primAgdaDefinitionPostulate       = getBuiltin builtinAgdaDefinitionPostulate
primAgdaDefinitionPrimitive       = getBuiltin builtinAgdaDefinitionPrimitive
primAgdaDefinition                = getBuiltin builtinAgdaDefinition
builtinNat          = "NATURAL"
builtinSuc          = "SUC"
builtinZero         = "ZERO"
builtinNatPlus      = "NATPLUS"
builtinNatMinus     = "NATMINUS"
builtinNatTimes     = "NATTIMES"
builtinNatDivSucAux = "NATDIVSUCAUX"
builtinNatModSucAux = "NATMODSUCAUX"
builtinNatEquals    = "NATEQUALS"
builtinNatLess      = "NATLESS"
builtinInteger      = "INTEGER"
builtinFloat        = "FLOAT"
builtinChar         = "CHAR"
builtinString       = "STRING"
builtinBool         = "BOOL"
builtinTrue         = "TRUE"
builtinFalse        = "FALSE"
builtinList         = "LIST"
builtinNil          = "NIL"
builtinCons         = "CONS"
builtinIO           = "IO"
builtinSize         = "SIZE"
builtinSizeSuc      = "SIZESUC"
builtinSizeInf      = "SIZEINF"
builtinInf          = "INFINITY"
builtinSharp        = "SHARP"
builtinFlat         = "FLAT"
builtinEquality     = "EQUALITY"
builtinRefl         = "REFL"
builtinLevelMax     = "LEVELMAX"
builtinLevel        = "LEVEL"
builtinLevelZero    = "LEVELZERO"
builtinLevelSuc     = "LEVELSUC"
builtinQName        = "QNAME"
builtinAgdaSort     = "AGDASORT"
builtinAgdaSortSet  = "AGDASORTSET"
builtinAgdaSortLit  = "AGDASORTLIT"
builtinAgdaSortUnsupported = "AGDASORTUNSUPPORTED"
builtinAgdaType     = "AGDATYPE"
builtinAgdaTypeEl   = "AGDATYPEEL"
builtinHiding       = "HIDING"
builtinHidden       = "HIDDEN"
builtinInstance     = "INSTANCE"
builtinVisible      = "VISIBLE"
builtinRelevance    = "RELEVANCE"
builtinRelevant     = "RELEVANT"
builtinIrrelevant   = "IRRELEVANT"
builtinArg          = "ARG"
builtinArgArg       = "ARGARG"
builtinAgdaTerm         = "AGDATERM"
builtinAgdaTermVar      = "AGDATERMVAR"
builtinAgdaTermLam      = "AGDATERMLAM"
builtinAgdaTermDef      = "AGDATERMDEF"
builtinAgdaTermCon      = "AGDATERMCON"
builtinAgdaTermPi       = "AGDATERMPI"
builtinAgdaTermSort     = "AGDATERMSORT"
builtinAgdaTermUnsupported = "AGDATERMUNSUPPORTED"
builtinAgdaFunDef                    = "AGDAFUNDEF"
builtinAgdaDataDef                   = "AGDADATADEF"
builtinAgdaRecordDef                 = "AGDARECORDDEF"
builtinAgdaDefinitionFunDef          = "AGDADEFINITIONFUNDEF"
builtinAgdaDefinitionDataDef         = "AGDADEFINITIONDATADEF"
builtinAgdaDefinitionRecordDef       = "AGDADEFINITIONRECORDDEF"
builtinAgdaDefinitionDataConstructor = "AGDADEFINITIONDATACONSTRUCTOR"
builtinAgdaDefinitionPostulate       = "AGDADEFINITIONPOSTULATE"
builtinAgdaDefinitionPrimitive       = "AGDADEFINITIONPRIMITIVE"
builtinAgdaDefinition                = "AGDADEFINITION"