{-# LANGUAGE CPP #-}

module Agda.TypeChecking.Monad.Builtin
  ( module Agda.TypeChecking.Monad.Builtin
  , module Agda.Syntax.Builtin  -- The names are defined here.
  ) where

#if __GLASGOW_HASKELL__ >= 800
import qualified Control.Monad.Fail as Fail
#endif

import Control.Monad.State
import Control.Monad.Trans.Maybe

import qualified Data.Map as Map
import Data.Function ( on )

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Builtin
import Agda.Syntax.Internal as I
import Agda.TypeChecking.Monad.Base
-- import Agda.TypeChecking.Functions  -- LEADS TO IMPORT CYCLE
import Agda.TypeChecking.Substitute

import Agda.Utils.Except
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Maybe
import Agda.Utils.Tuple

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

class ( Functor m
      , Applicative m
#if __GLASGOW_HASKELL__ < 800
      , Monad m
#else
      , Fail.MonadFail m
#endif
      ) => HasBuiltins m where
  getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))

instance HasBuiltins m => HasBuiltins (MaybeT m) where
  getBuiltinThing b = lift $ getBuiltinThing b

instance HasBuiltins m => HasBuiltins (ExceptT e m) where
  getBuiltinThing b = lift $ getBuiltinThing b

instance HasBuiltins m => HasBuiltins (StateT s m) where
  getBuiltinThing b = lift $ getBuiltinThing b

litType :: Literal -> TCM Type
litType l = case l of
  LitNat _ n    -> do
    _ <- primZero
    when (n > 0) $ void $ primSuc
    el <$> primNat
  LitWord64 _ _ -> el <$> primWord64
  LitFloat _ _  -> el <$> primFloat
  LitChar _ _   -> el <$> primChar
  LitString _ _ -> el <$> primString
  LitQName _ _  -> el <$> primQName
  LitMeta _ _ _ -> el <$> primAgdaMeta
  where
    el t = El (mkType 0) t

instance MonadIO m => HasBuiltins (TCMT m) where
  getBuiltinThing b = liftM2 mplus (Map.lookup b <$> useTC stLocalBuiltins)
                      (Map.lookup b <$> useTC stImportedBuiltins)

setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
setBuiltinThings b = stLocalBuiltins `setTCLens` 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          -> stLocalBuiltins `modifyTCLens` Map.insert b (Builtin x)

bindPrimitive :: String -> PrimFun -> TCM ()
bindPrimitive b pf = do
  builtin <- getBuiltinThing b
  case builtin of
    Just (Builtin _) -> typeError $ NoSuchPrimitiveFunction b
    Just (Prim x)    -> typeError $ (DuplicatePrimitiveBinding b `on` primFunName) x pf
    Nothing          -> stLocalBuiltins `modifyTCLens` Map.insert b (Prim pf)

getBuiltin :: String -> TCM Term
getBuiltin x =
  fromMaybeM (typeError $ NoBindingForBuiltin x) $ getBuiltin' x

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

getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' x = (getPrim =<<) <$> getBuiltinThing x
  where
    getPrim (Prim pf) = return pf
    getPrim _         = Nothing

getPrimitive :: String -> TCM PrimFun
getPrimitive x =
  fromMaybeM (typeError $ NoSuchPrimitiveFunction x) $ getPrimitive' x

getPrimitiveTerm :: String -> TCM Term
getPrimitiveTerm x = (`Def` []) <$> primFunName <$> getPrimitive x

getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term)
getPrimitiveTerm' x = fmap (`Def` []) <$> getPrimitiveName' x

getTerm' :: HasBuiltins m => String -> m (Maybe Term)
getTerm' x = mplus <$> getBuiltin' x <*> getPrimitiveTerm' x

getName' :: HasBuiltins m => String -> m (Maybe QName)
getName' x = mplus <$> getBuiltinName' x <*> getPrimitiveName' x

-- | @getTerm use name@ looks up @name@ as a primitive or builtin, and
-- throws an error otherwise.
-- The @use@ argument describes how the name is used for the sake of
-- the error message.
getTerm :: (HasBuiltins m) => String -> String -> m Term
getTerm use name = flip fromMaybeM (getTerm' name) $
  return $! (throwImpossible $ ImpMissingDefinitions [name] use)


-- | Rewrite a literal to constructor form if possible.
constructorForm :: Term -> TCM Term
constructorForm v = constructorForm' primZero primSuc v

constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
constructorForm' pZero pSuc v =
  case v of
    Lit (LitNat r n)
      | n == 0    -> pZero
      | n > 0     -> (`apply1` Lit (LitNat r $ n - 1)) <$> pSuc
      | otherwise -> pure v
    _ -> pure v

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

primInteger, primIntegerPos, primIntegerNegSuc,
    primFloat, primChar, primString, primUnit, primUnitUnit, primBool, primTrue, primFalse,
    primSigma,
    primList, primNil, primCons, primIO, primNat, primSuc, primZero,
    primPath, primPathP, primInterval, primIZero, primIOne, primPartial, primPartialP,
    primIMin, primIMax, primINeg,
    primIsOne, primItIsOne, primIsOne1, primIsOne2, primIsOneEmpty,
    primSub, primSubIn, primSubOut,
    primTrans, primHComp,
    primId, primConId, primIdElim,
    primEquiv, primEquivFun, primEquivProof, primPathToEquiv,
    primGlue, prim_glue, prim_unglue,
    primFaceForall,
    primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
    primNatEquality, primNatLess,
    -- Machine words
    primWord64,
    primSizeUniv, primSize, primSizeLt, primSizeSuc, primSizeInf, primSizeMax,
    primInf, primSharp, primFlat,
    primEquality, primRefl,
    primRewrite, -- Name of rewrite relation
    primLevel, primLevelZero, primLevelSuc, primLevelMax,
    primSetOmega,
    primFromNat, primFromNeg, primFromString,
    -- builtins for reflection:
    primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAbs, primAbsAbs, primAgdaTerm, primAgdaTermVar,
    primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
    primAgdaTermSort, primAgdaTermLit, primAgdaTermUnsupported, primAgdaTermMeta,
    primAgdaErrorPart, primAgdaErrorPartString, primAgdaErrorPartTerm, primAgdaErrorPartName,
    primHiding, primHidden, primInstance, primVisible,
    primRelevance, primRelevant, primIrrelevant,
    primAssoc, primAssocLeft, primAssocRight, primAssocNon,
    primPrecedence, primPrecRelated, primPrecUnrelated,
    primFixity, primFixityFixity,
    primAgdaLiteral, primAgdaLitNat, primAgdaLitWord64, primAgdaLitFloat, primAgdaLitString, primAgdaLitChar, primAgdaLitQName, primAgdaLitMeta,
    primAgdaSort, primAgdaSortSet, primAgdaSortLit, primAgdaSortUnsupported,
    primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef,
    primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor,
    primAgdaClause, primAgdaClauseClause, primAgdaClauseAbsurd,
    primAgdaPattern, primAgdaPatCon, primAgdaPatVar, primAgdaPatDot,
    primAgdaPatLit, primAgdaPatProj,
    primAgdaPatAbsurd,
    primAgdaMeta,
    primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify,
    primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType,
    primAgdaTCMNormalise, primAgdaTCMReduce,
    primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext,
    primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDefineFun,
    primAgdaTCMGetType, primAgdaTCMGetDefinition,
    primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm,
    primAgdaTCMBlockOnMeta, primAgdaTCMCommit, primAgdaTCMIsMacro,
    primAgdaTCMWithNormalisation, primAgdaTCMDebugPrint,
    primAgdaTCMNoConstraints,
    primAgdaTCMRunSpeculative
    :: TCM Term

primInteger      = getBuiltin builtinInteger
primIntegerPos   = getBuiltin builtinIntegerPos
primIntegerNegSuc = getBuiltin builtinIntegerNegSuc
primFloat        = getBuiltin builtinFloat
primChar         = getBuiltin builtinChar
primString       = getBuiltin builtinString
primBool         = getBuiltin builtinBool
primSigma        = getBuiltin builtinSigma
primUnit         = getBuiltin builtinUnit
primUnitUnit     = getBuiltin builtinUnitUnit
primTrue         = getBuiltin builtinTrue
primFalse        = getBuiltin builtinFalse
primList         = getBuiltin builtinList
primNil          = getBuiltin builtinNil
primCons         = getBuiltin builtinCons
primIO           = getBuiltin builtinIO
primId           = getBuiltin builtinId
primConId        = getBuiltin builtinConId
primIdElim       = getPrimitiveTerm builtinIdElim
primPath         = getBuiltin builtinPath
primPathP        = getBuiltin builtinPathP
primInterval     = getBuiltin builtinInterval
primIZero        = getBuiltin builtinIZero
primIOne         = getBuiltin builtinIOne
primIMin         = getPrimitiveTerm builtinIMin
primIMax         = getPrimitiveTerm builtinIMax
primINeg         = getPrimitiveTerm builtinINeg
primPartial      = getPrimitiveTerm "primPartial"
primPartialP     = getPrimitiveTerm "primPartialP"
primIsOne        = getBuiltin builtinIsOne
primItIsOne      = getBuiltin builtinItIsOne
primTrans        = getPrimitiveTerm builtinTrans
primHComp        = getPrimitiveTerm builtinHComp
primEquiv        = getBuiltin builtinEquiv
primEquivFun     = getBuiltin builtinEquivFun
primEquivProof   = getBuiltin builtinEquivProof
primPathToEquiv  = getBuiltin builtinPathToEquiv
primGlue         = getPrimitiveTerm builtinGlue
prim_glue        = getPrimitiveTerm builtin_glue
prim_unglue      = getPrimitiveTerm builtin_unglue
primFaceForall   = getPrimitiveTerm builtinFaceForall
primIsOne1       = getBuiltin builtinIsOne1
primIsOne2       = getBuiltin builtinIsOne2
primIsOneEmpty   = getBuiltin builtinIsOneEmpty
primSub          = getBuiltin builtinSub
primSubIn        = getBuiltin builtinSubIn
primSubOut       = getPrimitiveTerm builtinSubOut
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
primWord64       = getBuiltin builtinWord64
primSizeUniv     = getBuiltin builtinSizeUniv
primSize         = getBuiltin builtinSize
primSizeLt       = getBuiltin builtinSizeLt
primSizeSuc      = getBuiltin builtinSizeSuc
primSizeInf      = getBuiltin builtinSizeInf
primSizeMax      = getBuiltin builtinSizeMax
primInf          = getBuiltin builtinInf
primSharp        = getBuiltin builtinSharp
primFlat         = getBuiltin builtinFlat
primEquality     = getBuiltin builtinEquality
primRefl         = getBuiltin builtinRefl
primRewrite      = getBuiltin builtinRewrite
primLevel        = getBuiltin builtinLevel
primLevelZero    = getBuiltin builtinLevelZero
primLevelSuc     = getBuiltin builtinLevelSuc
primLevelMax     = getBuiltin builtinLevelMax
primSetOmega     = getBuiltin builtinSetOmega
primFromNat      = getBuiltin builtinFromNat
primFromNeg      = getBuiltin builtinFromNeg
primFromString   = getBuiltin builtinFromString
primQName        = getBuiltin builtinQName
primArg          = getBuiltin builtinArg
primArgArg       = getBuiltin builtinArgArg
primAbs          = getBuiltin builtinAbs
primAbsAbs       = getBuiltin builtinAbsAbs
primAgdaSort     = getBuiltin builtinAgdaSort
primHiding       = getBuiltin builtinHiding
primHidden       = getBuiltin builtinHidden
primInstance     = getBuiltin builtinInstance
primVisible      = getBuiltin builtinVisible
primRelevance    = getBuiltin builtinRelevance
primRelevant     = getBuiltin builtinRelevant
primIrrelevant   = getBuiltin builtinIrrelevant
primAssoc        = getBuiltin builtinAssoc
primAssocLeft    = getBuiltin builtinAssocLeft
primAssocRight   = getBuiltin builtinAssocRight
primAssocNon     = getBuiltin builtinAssocNon
primPrecedence    = getBuiltin builtinPrecedence
primPrecRelated   = getBuiltin builtinPrecRelated
primPrecUnrelated = getBuiltin builtinPrecUnrelated
primFixity        = getBuiltin builtinFixity
primFixityFixity  = getBuiltin builtinFixityFixity
primArgInfo      = getBuiltin builtinArgInfo
primArgArgInfo   = getBuiltin builtinArgArgInfo
primAgdaSortSet  = getBuiltin builtinAgdaSortSet
primAgdaSortLit  = getBuiltin builtinAgdaSortLit
primAgdaSortUnsupported = getBuiltin builtinAgdaSortUnsupported
primAgdaTerm         = getBuiltin builtinAgdaTerm
primAgdaTermVar      = getBuiltin builtinAgdaTermVar
primAgdaTermLam      = getBuiltin builtinAgdaTermLam
primAgdaTermExtLam   = getBuiltin builtinAgdaTermExtLam
primAgdaTermDef      = getBuiltin builtinAgdaTermDef
primAgdaTermCon      = getBuiltin builtinAgdaTermCon
primAgdaTermPi       = getBuiltin builtinAgdaTermPi
primAgdaTermSort     = getBuiltin builtinAgdaTermSort
primAgdaTermLit      = getBuiltin builtinAgdaTermLit
primAgdaTermUnsupported     = getBuiltin builtinAgdaTermUnsupported
primAgdaTermMeta  = getBuiltin builtinAgdaTermMeta
primAgdaErrorPart       = getBuiltin builtinAgdaErrorPart
primAgdaErrorPartString = getBuiltin builtinAgdaErrorPartString
primAgdaErrorPartTerm   = getBuiltin builtinAgdaErrorPartTerm
primAgdaErrorPartName   = getBuiltin builtinAgdaErrorPartName
primAgdaLiteral   = getBuiltin builtinAgdaLiteral
primAgdaLitNat    = getBuiltin builtinAgdaLitNat
primAgdaLitWord64 = getBuiltin builtinAgdaLitWord64
primAgdaLitFloat  = getBuiltin builtinAgdaLitFloat
primAgdaLitChar   = getBuiltin builtinAgdaLitChar
primAgdaLitString = getBuiltin builtinAgdaLitString
primAgdaLitQName  = getBuiltin builtinAgdaLitQName
primAgdaLitMeta   = getBuiltin builtinAgdaLitMeta
primAgdaPattern   = getBuiltin builtinAgdaPattern
primAgdaPatCon    = getBuiltin builtinAgdaPatCon
primAgdaPatVar    = getBuiltin builtinAgdaPatVar
primAgdaPatDot    = getBuiltin builtinAgdaPatDot
primAgdaPatLit    = getBuiltin builtinAgdaPatLit
primAgdaPatProj   = getBuiltin builtinAgdaPatProj
primAgdaPatAbsurd = getBuiltin builtinAgdaPatAbsurd
primAgdaClause    = getBuiltin builtinAgdaClause
primAgdaClauseClause = getBuiltin builtinAgdaClauseClause
primAgdaClauseAbsurd = getBuiltin builtinAgdaClauseAbsurd
primAgdaDefinitionFunDef          = getBuiltin builtinAgdaDefinitionFunDef
primAgdaDefinitionDataDef         = getBuiltin builtinAgdaDefinitionDataDef
primAgdaDefinitionRecordDef       = getBuiltin builtinAgdaDefinitionRecordDef
primAgdaDefinitionDataConstructor = getBuiltin builtinAgdaDefinitionDataConstructor
primAgdaDefinitionPostulate       = getBuiltin builtinAgdaDefinitionPostulate
primAgdaDefinitionPrimitive       = getBuiltin builtinAgdaDefinitionPrimitive
primAgdaDefinition                = getBuiltin builtinAgdaDefinition
primAgdaMeta                      = getBuiltin builtinAgdaMeta
primAgdaTCM           = getBuiltin builtinAgdaTCM
primAgdaTCMReturn     = getBuiltin builtinAgdaTCMReturn
primAgdaTCMBind       = getBuiltin builtinAgdaTCMBind
primAgdaTCMUnify      = getBuiltin builtinAgdaTCMUnify
primAgdaTCMTypeError  = getBuiltin builtinAgdaTCMTypeError
primAgdaTCMInferType  = getBuiltin builtinAgdaTCMInferType
primAgdaTCMCheckType  = getBuiltin builtinAgdaTCMCheckType
primAgdaTCMNormalise  = getBuiltin builtinAgdaTCMNormalise
primAgdaTCMReduce     = getBuiltin builtinAgdaTCMReduce
primAgdaTCMCatchError = getBuiltin builtinAgdaTCMCatchError
primAgdaTCMGetContext = getBuiltin builtinAgdaTCMGetContext
primAgdaTCMExtendContext = getBuiltin builtinAgdaTCMExtendContext
primAgdaTCMInContext     = getBuiltin builtinAgdaTCMInContext
primAgdaTCMFreshName     = getBuiltin builtinAgdaTCMFreshName
primAgdaTCMDeclareDef    = getBuiltin builtinAgdaTCMDeclareDef
primAgdaTCMDeclarePostulate   = getBuiltin builtinAgdaTCMDeclarePostulate
primAgdaTCMDefineFun     = getBuiltin builtinAgdaTCMDefineFun
primAgdaTCMGetType            = getBuiltin builtinAgdaTCMGetType
primAgdaTCMGetDefinition      = getBuiltin builtinAgdaTCMGetDefinition
primAgdaTCMQuoteTerm          = getBuiltin builtinAgdaTCMQuoteTerm
primAgdaTCMUnquoteTerm        = getBuiltin builtinAgdaTCMUnquoteTerm
primAgdaTCMBlockOnMeta        = getBuiltin builtinAgdaTCMBlockOnMeta
primAgdaTCMCommit             = getBuiltin builtinAgdaTCMCommit
primAgdaTCMIsMacro            = getBuiltin builtinAgdaTCMIsMacro
primAgdaTCMWithNormalisation  = getBuiltin builtinAgdaTCMWithNormalisation
primAgdaTCMDebugPrint         = getBuiltin builtinAgdaTCMDebugPrint
primAgdaTCMNoConstraints      = getBuiltin builtinAgdaTCMNoConstraints
primAgdaTCMRunSpeculative     = getBuiltin builtinAgdaTCMRunSpeculative

-- | The coinductive primitives.

data CoinductionKit = CoinductionKit
  { nameOfInf   :: QName
  , nameOfSharp :: QName
  , nameOfFlat  :: QName
  }

-- | Tries to build a 'CoinductionKit'.

coinductionKit' :: TCM CoinductionKit
coinductionKit' = do
  Def inf   _ <- primInf
  Def sharp _ <- primSharp
  Def flat  _ <- primFlat
  return $ CoinductionKit
    { nameOfInf   = inf
    , nameOfSharp = sharp
    , nameOfFlat  = flat
    }

coinductionKit :: TCM (Maybe CoinductionKit)
coinductionKit = tryMaybe coinductionKit'


------------------------------------------------------------------------
-- * Path equality
------------------------------------------------------------------------

getPrimName :: Term -> QName
getPrimName ty = do
  let lamV (Lam i b)  = mapFst (getHiding i :) $ lamV (unAbs b)
      lamV (Pi _ b)   = lamV (unEl $ unAbs b)
      lamV v          = ([], v)
  case lamV ty of
            (_, Def path _) -> path
            (_, Con nm _ _)   -> conName nm
            (_, _)          -> __IMPOSSIBLE__

getBuiltinName', getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' n = fmap getPrimName <$> getBuiltin' n
getPrimitiveName' n = fmap primFunName <$> getPrimitive' n

isPrimitive :: HasBuiltins m => String -> QName -> m Bool
isPrimitive n q = (Just q ==) <$> getPrimitiveName' n

intervalView' :: HasBuiltins m => m (Term -> IntervalView)
intervalView' = do
  iz <- getBuiltinName' builtinIZero
  io <- getBuiltinName' builtinIOne
  imax <- getPrimitiveName' "primIMax"
  imin <- getPrimitiveName' "primIMin"
  ineg <- getPrimitiveName' "primINeg"
  return $ \ t ->
    case t of
      Def q es ->
        case es of
          [Apply x,Apply y] | Just q == imin -> IMin x y
          [Apply x,Apply y] | Just q == imax -> IMax x y
          [Apply x]         | Just q == ineg -> INeg x
          _                 -> OTerm t
      Con q _ [] | Just (conName q) == iz -> IZero
                 | Just (conName q) == io -> IOne
      _ -> OTerm t

intervalView :: HasBuiltins m => Term -> m IntervalView
intervalView t = do
  f <- intervalView'
  return (f t)

intervalUnview :: HasBuiltins m => IntervalView -> m Term
intervalUnview t = do
  f <- intervalUnview'
  return (f t)

intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
intervalUnview' = do
  iz <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIZero -- should it be a type error instead?
  io <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIOne
  imin <- (`Def` []) <$> fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primIMin"
  imax <- (`Def` []) <$> fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primIMax"
  ineg <- (`Def` []) <$> fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' "primINeg"
  return $ \ v -> case v of
             IZero -> iz
             IOne  -> io
             IMin x y -> apply imin [x,y]
             IMax x y -> apply imax [x,y]
             INeg x   -> apply ineg [x]
             OTerm t -> t

------------------------------------------------------------------------
-- * Path equality
------------------------------------------------------------------------

-- | Check whether the type is actually an path (lhs ≡ rhs)
--   and extract lhs, rhs, and their type.
--
--   Precondition: type is reduced.

pathView :: HasBuiltins m => Type -> m PathView
pathView t0 = do
  view <- pathView'
  return $ view t0

pathView' :: HasBuiltins m => m (Type -> PathView)
pathView' = do
 mpath  <- getBuiltinName' builtinPath
 mpathp <- getBuiltinName' builtinPathP
 return $ \ t0@(El s t) ->
  case t of
    Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ]
      | Just path' == mpath, Just path <- mpathp -> PathType s path level (lam_i <$> typ) lhs rhs
      where lam_i = Lam defaultArgInfo . NoAbs "_"
    Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ]
      | Just path' == mpathp, Just path <- mpathp -> PathType s path level typ lhs rhs
    _ -> OType t0

-- | Non dependent Path
idViewAsPath :: HasBuiltins m => Type -> m PathView
idViewAsPath t0@(El s t) = do
  mid <- fmap getPrimName <$> getBuiltin' builtinId
  mpath <- fmap getPrimName <$> getBuiltin' builtinPath
  case mid of
   Just path | isJust mpath -> case t of
    Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ]
      | path' == path -> return $ PathType s (fromJust mpath) level typ lhs rhs
    _ -> return $ OType t0
   _ -> return $ OType t0

boldPathView :: Type -> PathView
boldPathView t0@(El s t) = do
  case t of
    Def path' [ Apply level , Apply typ , Apply lhs , Apply rhs ]
      -> PathType s path' level typ lhs rhs
    _ -> OType t0

-- | Revert the 'PathView'.
--
--   Postcondition: type is reduced.

pathUnview :: PathView -> Type
pathUnview (OType t) = t
pathUnview (PathType s path l t lhs rhs) =
  El s $ Def path $ map Apply [l, t, lhs, rhs]

------------------------------------------------------------------------
-- * Builtin equality
------------------------------------------------------------------------

-- | Get the name of the equality type.
primEqualityName :: TCM QName
-- primEqualityName = getDef =<< primEquality  -- LEADS TO IMPORT CYCLE
primEqualityName = do
  eq <- primEquality
  -- Andreas, 2014-05-17 moved this here from TC.Rules.Def
  -- Don't know why up to 2 hidden lambdas need to be stripped,
  -- but I left the code in place.
  -- Maybe it was intended that equality could be declared
  -- in three different ways:
  -- 1. universe and type polymorphic
  -- 2. type polymorphic only
  -- 3. monomorphic.
  let lamV (Lam i b)  = mapFst (getHiding i :) $ lamV (unAbs b)
      lamV v          = ([], v)
  return $ case lamV eq of
    (_, Def equality _) -> equality
    _                   -> __IMPOSSIBLE__

-- | Check whether the type is actually an equality (lhs ≡ rhs)
--   and extract lhs, rhs, and their type.
--
--   Precondition: type is reduced.

equalityView :: Type -> TCM EqualityView
equalityView t0@(El s t) = do
  equality <- primEqualityName
  case t of
    Def equality' es | equality' == equality -> do
      let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
      let n = length vs
      unless (n >= 3) __IMPOSSIBLE__
      let (pars, [ typ , lhs, rhs ]) = splitAt (n-3) vs
      return $ EqualityType s equality pars typ lhs rhs
    _ -> return $ OtherType t0

-- | Revert the 'EqualityView'.
--
--   Postcondition: type is reduced.

equalityUnview :: EqualityView -> Type
equalityUnview (OtherType t) = t
equalityUnview (EqualityType s equality l t lhs rhs) =
  El s $ Def equality $ map Apply (l ++ [t, lhs, rhs])

-- | Primitives with typechecking constrants.
constrainedPrims :: [String]
constrainedPrims =
  [ builtinConId
  , builtinPOr
  , builtinComp
  , builtinHComp
  , builtinTrans
  , builtin_glue
  ]

getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName)
getNameOfConstrained s = do
  unless (s `elem` constrainedPrims) __IMPOSSIBLE__
  getName' s