{-|
Module      : Idris.AbsSyntax
Description : Provides Idris' core data definitions and utility code.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}

module Idris.AbsSyntax(
    module Idris.AbsSyntax
  , module Idris.AbsSyntaxTree
  ) where

import Idris.AbsSyntaxTree
import Idris.Colours
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Docstrings
import Idris.IdeMode hiding (Opt(..))
import Idris.Options
import IRTS.CodegenCommon

import System.Directory (canonicalizePath, doesFileExist)
import System.IO

import Control.Applicative
import Control.Monad.State
import Prelude hiding (Applicative, Foldable, Traversable, (<$>))

import Data.Char
import Data.Either
import Data.List hiding (insert, union)
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
import System.IO.Error (tryIOError)

import Data.Generics.Uniplate.Data (descend, descendM)

import Util.DynamicLinker
import Util.Pretty
import Util.System

getContext :: Idris Context
getContext = do i <- getIState; return (tt_ctxt i)

forCodegen :: Codegen -> [(Codegen, a)] -> [a]
forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']
    where
        eqLang (Via _ x) (Via _ y) = x == y
        eqLang Bytecode Bytecode = True
        eqLang _ _ = False

getObjectFiles :: Codegen -> Idris [FilePath]
getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)

addObjectFile :: Codegen -> FilePath -> Idris ()
addObjectFile tgt f = do i <- getIState; putIState $ i { idris_objs = nub $ idris_objs i ++ [(tgt, f)] }

getLibs :: Codegen -> Idris [String]
getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)

addLib :: Codegen -> String -> Idris ()
addLib tgt f = do i <- getIState; putIState $ i { idris_libs = nub $ idris_libs i ++ [(tgt, f)] }

getFlags :: Codegen -> Idris [String]
getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)

addFlag :: Codegen -> String -> Idris ()
addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = nub $ idris_cgflags i ++ [(tgt, f)] }

addDyLib :: [String] -> Idris (Either DynamicLib String)
addDyLib libs = do i <- getIState
                   let ls = idris_dynamic_libs i
                   let importdirs = opt_importdirs (idris_options i)
                   case mapMaybe (findDyLib ls) libs of
                     x:_ -> return (Left x)
                     [] -> do
                       handle <- lift . lift .
                                 mapM (\l -> catchIO (tryLoadLib importdirs l)
                                                     (\_ -> return Nothing)) $ libs
                       case msum handle of
                         Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
                                                    intercalate "," libs ++ "\"")
                         Just x -> do putIState $ i { idris_dynamic_libs = x:ls }
                                      return (Left x)
    where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib
          findDyLib []         _                     = Nothing
          findDyLib (lib:libs') l | l == lib_name lib = Just lib
                                  | otherwise         = findDyLib libs' l

getAutoImports :: Idris [FilePath]
getAutoImports = do i <- getIState
                    return (opt_autoImport (idris_options i))

addAutoImport :: FilePath -> Idris ()
addAutoImport fp = do i <- getIState
                      let opts = idris_options i
                      put (i { idris_options = opts { opt_autoImport =
                                                       fp : opt_autoImport opts } } )

addDefinedName :: Name -> Idris ()
addDefinedName n = do ist <- getIState
                      putIState $ ist { idris_inmodule = S.insert n (idris_inmodule ist) }

getDefinedNames :: Idris [Name]
getDefinedNames = do ist <- getIState
                     return (S.toList (idris_inmodule ist))

addTT :: Term -> Idris (Maybe Term)
addTT t = do ist <- getIState
             case M.lookup t (idris_ttstats ist) of
                  Nothing -> do let tt' = M.insert t (1, t) (idris_ttstats ist)
                                putIState $ ist { idris_ttstats = tt' }
                                return Nothing
                  Just (i, t') -> do let tt' = M.insert t' (i + 1, t') (idris_ttstats ist)
                                     putIState $ ist { idris_ttstats = tt' }
                                     return (Just t')

dumpTT :: Idris ()
dumpTT = do ist <- get
            let sts = sortBy count (M.toList (idris_ttstats ist))
            mapM_ dump sts
            return ()
  where
    count (_,x) (_,y) = compare y x
    dump (tm, val) = runIO $ putStrLn (show val ++ ": " ++ show tm)

addHdr :: Codegen -> String -> Idris ()
addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

addImported :: Bool -> FilePath -> Idris ()
addImported pub f
     = do i <- getIState
          putIState $ i { idris_imported = nub $ (f, pub) : idris_imported i }

addLangExt :: LanguageExt -> Idris ()
addLangExt e = do i <- getIState
                  putIState $ i {
                    idris_language_extensions = e : idris_language_extensions i
                  }

dropLangExt :: LanguageExt -> Idris ()
dropLangExt e = do i <- getIState
                   putIState $ i {
                     idris_language_extensions = idris_language_extensions i \\ [e]
                   }

-- | Transforms are organised by the function being applied on the lhs
-- of the transform, to make looking up appropriate transforms quicker
addTrans :: Name -> (Term, Term) -> Idris ()
addTrans basefn t
           = do i <- getIState
                let t' = case lookupCtxtExact basefn (idris_transforms i) of
                              Just def -> (t : def)
                              Nothing -> [t]
                putIState $ i { idris_transforms = addDef basefn t'
                                                          (idris_transforms i) }

-- | Add transformation rules from a definition, which will reverse the
-- definition for an error to make it more readable
addErrRev :: (Term, Term) -> Idris ()
addErrRev t = do i <- getIState
                 putIState $ i { idris_errRev = t : idris_errRev i }

-- | Say that the name should always be reduced in error messages, to
-- help readability/error reflection
addErrReduce :: Name -> Idris ()
addErrReduce t = do i <- getIState
                    putIState $ i { idris_errReduce = t : idris_errReduce i }

addErasureUsage :: Name -> Int -> Idris ()
addErasureUsage n i = do ist <- getIState
                         putIState $ ist { idris_erasureUsed = (n, i) : idris_erasureUsed ist }

addExport :: Name -> Idris ()
addExport n = do ist <- getIState
                 putIState $ ist { idris_exports = n : idris_exports ist }

addUsedName :: FC -> Name -> Name -> Idris ()
addUsedName fc n arg
    = do ist <- getIState
         case lookupTyName n (tt_ctxt ist) of
              [(n', ty)] -> addUsage n' 0 ty
              [] -> throwError (At fc (NoSuchVariable n))
              xs -> throwError (At fc (CantResolveAlts (map fst xs)))
  where addUsage n i (Bind x _ sc) | x == arg = do addIBC (IBCUsage (n, i))
                                                   addErasureUsage n i
                                   | otherwise = addUsage n (i + 1) sc
        addUsage _ _ _ = throwError (At fc (Msg ("No such argument name " ++ show arg)))

getErasureUsage :: Idris [(Name, Int)]
getErasureUsage = do ist <- getIState;
                     return (idris_erasureUsed ist)

getExports :: Idris [Name]
getExports = do ist <- getIState
                return (idris_exports ist)

totcheck :: (FC, Name) -> Idris ()
totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

defer_totcheck :: (FC, Name) -> Idris ()
defer_totcheck n
   = do i <- getIState;
        putIState $ i { idris_defertotcheck = nub (idris_defertotcheck i ++ [n]) }

clear_totcheck :: Idris ()
clear_totcheck  = do i <- getIState; putIState $ i { idris_totcheck = [] }

setFlags :: Name -> [FnOpt] -> Idris ()
setFlags n fs = do i <- getIState; putIState $ i { idris_flags = addDef n fs (idris_flags i) }

addFnOpt :: Name -> FnOpt -> Idris ()
addFnOpt n f = do i <- getIState
                  let fls = case lookupCtxtExact n (idris_flags i) of
                                 Nothing -> []
                                 Just x -> x
                  setFlags n (f : fls)

setFnInfo :: Name -> FnInfo -> Idris ()
setFnInfo n fs = do i <- getIState; putIState $ i { idris_fninfo = addDef n fs (idris_fninfo i) }

setAccessibility :: Name -> Accessibility -> Idris ()
setAccessibility n a
         = do i <- getIState
              let ctxt = setAccess n a (tt_ctxt i)
              putIState $ i { tt_ctxt = ctxt }

-- | get the accessibility of a name outside this module
getFromHideList :: Name -> Idris (Maybe Accessibility)
getFromHideList n = do i <- getIState
                       return $ lookupCtxtExact n (hide_list i)

setTotality :: Name -> Totality -> Idris ()
setTotality n a
         = do i <- getIState
              let ctxt = setTotal n a (tt_ctxt i)
              putIState $ i { tt_ctxt = ctxt }

setInjectivity :: Name -> Injectivity -> Idris ()
setInjectivity n a
         = do i <- getIState
              let ctxt = setInjective n a (tt_ctxt i)
              putIState $ i { tt_ctxt = ctxt }

getTotality :: Name -> Idris Totality
getTotality n
         = do i <- getIState
              case lookupTotal n (tt_ctxt i) of
                [t] -> return t
                _ -> return (Total [])

-- Get coercions which might return the required type
getCoercionsTo :: IState -> Type -> [Name]
getCoercionsTo i ty =
    let cs = idris_coercions i
        (fn,_) = unApply (getRetTy ty) in
        findCoercions fn cs
    where findCoercions _ [] = []
          findCoercions t (n : ns) =
             let ps = case lookupTy n (tt_ctxt i) of
                        [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
                                   (t', _) -> [n | t == t']
                        _ -> [] in
                 ps ++ findCoercions t ns

addToCG :: Name -> CGInfo -> Idris ()
addToCG n cg
   = do i <- getIState
        putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

addCalls :: Name -> [Name] -> Idris ()
addCalls n calls
   = do i <- getIState
        case lookupCtxtExact n (idris_callgraph i) of
             Nothing -> addToCG n (CGInfo calls Nothing [] [])
             Just (CGInfo cs ans scg used) ->
                addToCG n (CGInfo (nub (calls ++ cs)) ans scg used)

addTyInferred :: Name -> Idris ()
addTyInferred n
   = do i <- getIState
        putIState $ i { idris_tyinfodata =
                        addDef n TIPartial (idris_tyinfodata i) }

addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
                               mapM_ addConstraint ts
                               return ()
    where addConstraint (x, y) = findMVApps x y

          findMVApps x y
             = do let (fx, argsx) = unApply x
                  let (fy, argsy) = unApply y
                  if (fx /= fy)
                     then do
                       tryAddMV fx y
                       tryAddMV fy x
                     else mapM_ addConstraint (zip argsx argsy)

          tryAddMV (P _ mv _) y =
               do ist <- get
                  case lookup mv (idris_metavars ist) of
                       Just _ -> addConstraintRule mv y
                       _ -> return ()
          tryAddMV _ _ = return ()

          addConstraintRule :: Name -> Term -> Idris ()
          addConstraintRule n t
             = do ist <- get
                  logLvl 1 $ "TI constraint: " ++ show (n, t)
                  case lookupCtxt n (idris_tyinfodata ist) of
                     [TISolution ts] ->
                         do mapM_ (checkConsistent t) ts
                            let ti' = addDef n (TISolution (t : ts))
                                               (idris_tyinfodata ist)
                            put $ ist { idris_tyinfodata = ti' }
                     _ ->
                         do let ti' = addDef n (TISolution [t])
                                               (idris_tyinfodata ist)
                            put $ ist { idris_tyinfodata = ti' }

          -- Check a solution is consistent with previous solutions
          -- Meaning: If heads are both data types, they had better be the
          -- same.
          checkConsistent :: Term -> Term -> Idris ()
          checkConsistent x y =
              do let (fx, _) = unApply x
                 let (fy, _) = unApply y
                 case (fx, fy) of
                      (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n')
                      (P (TCon _ _) n _, Constant _) -> errWhen True
                      (Constant _, P (TCon _ _) n' _) -> errWhen True
                      (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n')
                      _ -> return ()

              where errWhen True
                       = throwError (At fc
                            (CantUnify False (x, Nothing) (y, Nothing) (Msg "") [] 0))
                    errWhen False = return ()

isTyInferred :: Name -> Idris Bool
isTyInferred n
   = do i <- getIState
        case lookupCtxt n (idris_tyinfodata i) of
             [TIPartial] -> return True
             _ -> return False

-- | Adds error handlers for a particular function and argument. If
-- names are ambiguous, all matching handlers are updated.
addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
addFunctionErrorHandlers f arg hs =
 do i <- getIState
    let oldHandlers = idris_function_errorhandlers i
    let newHandlers = flip (addDef f) oldHandlers $
                      case lookupCtxtExact f oldHandlers of
                        Nothing            -> M.singleton arg (S.fromList hs)
                        Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers
                        -- will always be one of those two, thus no extra case
    putIState $ i { idris_function_errorhandlers = newHandlers }

-- | Trace all the names in a call graph starting at the given name
getAllNames :: Name -> Idris [Name]
getAllNames n = do i <- getIState
                   case getCGAllNames i n of
                        Just ns -> return ns
                        Nothing -> do ns <- allNames [] n
                                      addCGAllNames i n ns
                                      return ns

getCGAllNames :: IState -> Name -> Maybe [Name]
getCGAllNames i n = case lookupCtxtExact n (idris_callgraph i) of
                         Just ci -> allCalls ci
                         _ -> Nothing

addCGAllNames :: IState -> Name -> [Name] -> Idris ()
addCGAllNames i n ns
      = case lookupCtxtExact n (idris_callgraph i) of
             Just ci -> addToCG n (ci { allCalls = Just ns })
             _ -> addToCG n (CGInfo [] (Just ns) [] [])

allNames :: [Name] -> Name -> Idris [Name]
allNames ns n | n `elem` ns = return []
allNames ns n = do i <- getIState
                   case getCGAllNames i n of
                        Just ns -> return ns
                        Nothing -> case lookupCtxtExact n (idris_callgraph i) of
                                        Just ci ->
                                          do more <- mapM (allNames (n:ns)) (calls ci)
                                             let ns' = nub (n : concat more)
                                             addCGAllNames i n ns'
                                             return ns'
                                        _ -> return [n]

addCoercion :: Name -> Idris ()
addCoercion n = do i <- getIState
                   putIState $ i { idris_coercions = nub $ n : idris_coercions i }

addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addDocStr n doc args
   = do i <- getIState
        putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

addNameHint :: Name -> Name -> Idris ()
addNameHint ty n
   = do i <- getIState
        ty' <- case lookupCtxtName ty (idris_implicits i) of
                       [(tyn, _)] -> return tyn
                       [] -> throwError (NoSuchVariable ty)
                       tyns -> throwError (CantResolveAlts (map fst tyns))
        let ns' = case lookupCtxt ty' (idris_namehints i) of
                       [ns] -> ns ++ [n]
                       _ -> [n]
        putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }

getNameHints :: IState -> Name -> [Name]
getNameHints _ (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
getNameHints i n =
        case lookupCtxt n (idris_namehints i) of
             [ns] -> ns
             _ -> []

addDeprecated :: Name -> String -> Idris ()
addDeprecated n reason = do
  i <- getIState
  putIState $ i { idris_deprecated = addDef n reason (idris_deprecated i) }

getDeprecated :: Name -> Idris (Maybe String)
getDeprecated n = do
  i <- getIState
  return $ lookupCtxtExact n (idris_deprecated i)

addFragile :: Name -> String -> Idris ()
addFragile n reason = do
  i <- getIState
  putIState $ i { idris_fragile = addDef n reason (idris_fragile i) }

getFragile :: Name -> Idris (Maybe String)
getFragile n = do
  i <- getIState
  return $ lookupCtxtExact n (idris_fragile i)

push_estack :: Name -> Bool -> Idris ()
push_estack n implementation
    = do i <- getIState
         putIState (i { elab_stack = (n, implementation) : elab_stack i })

pop_estack :: Idris ()
pop_estack = do i <- getIState
                putIState (i { elab_stack = ptail (elab_stack i) })
    where ptail [] = []
          ptail (_ : xs) = xs

-- | Add an interface implementation function.
--
-- Precondition: the implementation should have the correct type.
--
-- Dodgy hack 1: Put integer implementations first in the list so they are
-- resolved by default.
--
-- Dodgy hack 2: put constraint chasers (ParentN) last
addImplementation :: Bool -- ^ whether the name is an Integer implementation
                  -> Bool -- ^ whether to include the implementation in implementation search
                  -> Name -- ^ the name of the interface
                  -> Name -- ^ the name of the implementation
                  -> Idris ()
addImplementation int res n i
    = do ist <- getIState
         case lookupCtxt n (idris_interfaces ist) of
                [CI a b c d e f g ins fds] ->
                     do let cs = addDef n (CI a b c d e f g (addI i ins) fds) (idris_interfaces ist)
                        putIState $ ist { idris_interfaces = cs }
                _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [] [] [(i, res)] []) (idris_interfaces ist)
                        putIState $ ist { idris_interfaces = cs }
  where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]
        addI i ins | int = (i, res) : ins
                   | chaser n = ins ++ [(i, res)]
                   | otherwise = insI i ins
        insI i [] = [(i, res)]
        insI i (n : ns) | chaser (fst n) = (i, res) : n : ns
                        | otherwise = n : insI i ns

        chaser (SN (ParentN _ _)) = True
        chaser (NS n _) = chaser n
        chaser _ = False

-- | Add a privileged implementation - one which implementation search will
-- happily resolve immediately if it is type correct This is used for
-- naming parent implementations when defining an implementation with
-- constraints.  Returns the old list, so we can revert easily at the
-- end of a block
addOpenImpl :: [Name] -> Idris [Name]
addOpenImpl ns = do ist <- getIState
                    ns' <- mapM (checkValid ist) ns
                    let open = idris_openimpls ist
                    putIState $ ist { idris_openimpls = nub (ns' ++ open) }
                    return open
  where
    checkValid ist n
      = case lookupCtxtName n (idris_implicits ist) of
             [(n', _)] -> return n'
             []        -> throwError (NoSuchVariable n)
             more      -> throwError (CantResolveAlts (map fst more))

setOpenImpl :: [Name] -> Idris ()
setOpenImpl ns = do ist <- getIState
                    putIState $ ist { idris_openimpls = ns }

getOpenImpl :: Idris [Name]
getOpenImpl = do ist <- getIState
                 return (idris_openimpls ist)

addInterface :: Name -> InterfaceInfo -> Idris ()
addInterface n i
   = do ist <- getIState
        let i' = case lookupCtxt n (idris_interfaces ist) of
                      [c] -> i { interface_implementations = interface_implementations c ++
                                                             interface_implementations i }
                      _ -> i
        putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }

updateIMethods :: Name -> [(Name, PTerm)] -> Idris ()
updateIMethods n meths
   = do ist <- getIState
        let i = case lookupCtxtExact n (idris_interfaces ist) of
                     Just c -> c { interface_methods = update (interface_methods c) }
                     Nothing -> error "Can't happen updateIMethods"
        putIState $ ist { idris_interfaces = addDef n i (idris_interfaces ist) }
  where
    update [] = []
    update (m@(n, (b, opts, t)) : rest)
        | Just ty <- lookup n meths
             = (n, (b, opts, ty)) : update rest
        | otherwise = m : update rest

addRecord :: Name -> RecordInfo -> Idris ()
addRecord n ri = do ist <- getIState
                    putIState $ ist { idris_records = addDef n ri (idris_records ist) }

addAutoHint :: Name -> Name -> Idris ()
addAutoHint n hint =
    do ist <- getIState
       case lookupCtxtExact n (idris_autohints ist) of
            Nothing ->
                 do let hs = addDef n [hint] (idris_autohints ist)
                    putIState $ ist { idris_autohints = hs }
            Just nhints ->
                 do let hs = addDef n (hint : nhints) (idris_autohints ist)
                    putIState $ ist { idris_autohints = hs }

getAutoHints :: Name -> Idris [Name]
getAutoHints n = do ist <- getIState
                    case lookupCtxtExact n (idris_autohints ist) of
                         Nothing -> return []
                         Just ns -> return ns

addIBC :: IBCWrite -> Idris ()
addIBC ibc@(IBCDef n)
           = do i <- getIState
                when (notDef (ibc_write i)) $
                  putIState $ i { ibc_write = ibc : ibc_write i }
   where notDef [] = True
         notDef (IBCDef n': _) | n == n' = False
         notDef (_ : is) = notDef is
addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

clearIBC :: Idris ()
clearIBC = do i <- getIState; putIState $ i { ibc_write = [],
                                              idris_inmodule = S.empty }

resetNameIdx :: Idris ()
resetNameIdx = do i <- getIState
                  put (i { idris_nameIdx = (0, emptyContext) })

-- | Used to preserve sharing of names
addNameIdx :: Name -> Idris (Int, Name)
addNameIdx n = do i <- getIState
                  let (i', x) = addNameIdx' i n
                  putIState i'
                  return x

addNameIdx' :: IState -> Name -> (IState, (Int, Name))
addNameIdx' i n
   = let idxs = snd (idris_nameIdx i) in
         case lookupCtxt n idxs of
            [x] -> (i, x)
            _ -> let i' = fst (idris_nameIdx i) + 1 in
                    (i { idris_nameIdx = (i', addDef n (i', n) idxs) }, (i', n))

getSymbol :: Name -> Idris Name
getSymbol n = do i <- getIState
                 case M.lookup n (idris_symbols i) of
                      Just n' -> return n'
                      Nothing -> do let sym' = M.insert n n (idris_symbols i)
                                    put (i { idris_symbols = sym' })
                                    return n

getHdrs :: Codegen -> Idris [String]
getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

getImported ::  Idris [(FilePath, Bool)]
getImported = idris_imported `fmap` getIState

setErrSpan :: FC -> Idris ()
setErrSpan x = do i <- getIState;
                  case (errSpan i) of
                      Nothing -> putIState $ i { errSpan = Just x }
                      Just _ -> return ()

clearErr :: Idris ()
clearErr = do i <- getIState
              putIState $ i { errSpan = Nothing }

getSO :: Idris (Maybe String)
getSO = do i <- getIState
           return (compiled_so i)

setSO :: Maybe String -> Idris ()
setSO s = do i <- getIState
             putIState (i { compiled_so = s })

getIState :: Idris IState
getIState = get

putIState :: IState -> Idris ()
putIState = put

updateIState :: (IState -> IState) -> Idris ()
updateIState f = do i <- getIState
                    putIState $ f i

withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b
withContext ctx name dflt action = do
    ist <- getIState
    case lookupCtxt name (ctx ist) of
        [x] -> action x
        _   -> return dflt

withContext_ :: (IState -> Ctxt a) -> Name -> (a -> Idris ()) -> Idris ()
withContext_ ctx name action = withContext ctx name () action

-- | A version of liftIO that puts errors into the exception type of
-- the Idris monad
runIO :: IO a -> Idris a
runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return
-- TODO: create specific Idris exceptions for specific IO errors such as "openFile: does not exist"
--
-- Issue #1738 on the issue tracker.
--     https://github.com/idris-lang/Idris-dev/issues/1738

getName :: Idris Int
getName = do i <- getIState;
             let idx = idris_name i;
             putIState (i { idris_name = idx + 1 })
             return idx

-- | InternalApp keeps track of the real function application for
-- making case splits from, not the application the programmer wrote,
-- which doesn't have the whole context in any case other than top
-- level definitions
addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
addInternalApp fp l t
    = do i <- getIState
         -- We canonicalise the path to make "./Test/Module.idr" equal
         -- to "Test/Module.idr"
         exists <- runIO $ doesFileExist fp
         when exists $
           do fp' <- runIO $ canonicalizePath fp
              putIState (i { idris_lineapps = ((fp', l), t) : idris_lineapps i })

getInternalApp :: FilePath -> Int -> Idris PTerm
getInternalApp fp l = do i <- getIState
                         -- We canonicalise the path to make
                         -- "./Test/Module.idr" equal to
                         -- "Test/Module.idr"
                         exists <- runIO $ doesFileExist fp
                         if exists
                           then do fp' <- runIO $ canonicalizePath fp
                                   case lookup (fp', l) (idris_lineapps i) of
                                     Just n' -> return n'
                                     Nothing -> return Placeholder
                                     -- TODO: What if it's not there?
                           else return Placeholder

-- | Pattern definitions are only used for coverage checking, so erase
-- them when we're done
clearOrigPats :: Idris ()
clearOrigPats = do i <- get
                   let ps = idris_patdefs i
                   let ps' = mapCtxt (\ (_,miss) -> ([], miss)) ps
                   put (i { idris_patdefs = ps' })

-- | Erase types from Ps in the context (basically ending up with
-- what's in the .ibc, which is all we need after all the analysis is
-- done)
clearPTypes :: Idris ()
clearPTypes = do i <- get
                 let ctxt = tt_ctxt i
                 put (i { tt_ctxt = mapDefCtxt pErase ctxt })
   where pErase (CaseOp c t tys orig _ cds)
            = CaseOp c t tys orig [] (pErase' cds)
         pErase x = x
         pErase' (CaseDefs (cs, c) rs)
             = let c' = (cs, fmap pEraseType c) in
                   CaseDefs c' rs

checkUndefined :: FC -> Name -> Idris ()
checkUndefined fc n
    = do i <- getContext
         case lookupTy n i of
             (_:_)  -> throwError . Msg $ show fc ++ ":" ++
                                          show n ++ " already defined"
             _ -> return ()

isUndefined :: FC -> Name -> Idris Bool
isUndefined _ n
    = do i <- getContext
         case lookupTyExact n i of
             Just _ -> return False
             _ -> return True

setContext :: Context -> Idris ()
setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )

updateContext :: (Context -> Context) -> Idris ()
updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )

addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
addConstraints fc (v, cs)
    = do tit <- typeInType
         when (not tit) $ do
             i <- getIState
             let ctxt = tt_ctxt i
             let ctxt' = ctxt { next_tvar = v }
             let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)
             putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }
  where
    insertAll [] c = c
    insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics
    insertAll ((ULE x y, fc) : cs) ics | x == y = insertAll cs ics
    insertAll ((c, fc) : cs) ics
       = insertAll cs $ S.insert (ConstraintFC c fc) ics

addDeferred = addDeferred' Ref
addDeferredTyCon = addDeferred' (TCon 0 0)

-- | Save information about a name that is not yet defined
addDeferred' :: NameType
             -> [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))]
                -- ^ The Name is the name being made into a metavar,
                -- the Int is the number of vars that are part of a
                -- putative proof context, the Maybe Name is the
                -- top-level function containing the new metavariable,
                -- the Type is its type, and the Bool is whether :p is
                -- allowed
             -> Idris ()
addDeferred' nt ns
  = do mapM_ (\(n, (i, _, t, _, _, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns
       mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns
       i <- getIState
       putIState $ i { idris_metavars = map (\(n, (i, top, _, ns, isTopLevel, isDefinable)) ->
                                                  (n, (top, i, ns, isTopLevel, isDefinable))) ns ++
                                            idris_metavars i }
  where
        -- 'tidyNames' is to generate user accessible names in case they are
        -- needed in tactic scripts
        tidyNames used (Bind (MN i x) b sc)
            = let n' = uniqueNameSet (UN x) used in
                  Bind n' b $ tidyNames (S.insert n' used) sc
        tidyNames used (Bind n b sc)
            = let n' = uniqueNameSet n used in
                  Bind n' b $ tidyNames (S.insert n' used) sc
        tidyNames _    b = b

solveDeferred :: FC -> Name -> Idris ()
solveDeferred fc n
    = do i <- getIState
         case lookup n (idris_metavars i) of
              Just (_, _, _, _, False) ->
                   throwError $ At fc $ Msg ("Can't define hole " ++ show n ++ " as it depends on other holes")
              _ -> putIState $ i { idris_metavars =
                                       filter (\(n', _) -> n/=n')
                                          (idris_metavars i),
                                     ibc_write =
                                       filter (notMV n) (ibc_write i)
                                          }
    where notMV n (IBCMetavar n') = not (n == n')
          notMV n _ = True

getUndefined :: Idris [Name]
getUndefined = do i <- getIState
                  return (map fst (idris_metavars i) \\ primDefs)

isMetavarName :: Name -> IState -> Bool
isMetavarName n ist
     = case lookupNames n (tt_ctxt ist) of
            (t:_) -> isJust $ lookup t (idris_metavars ist)
            _     -> False

getWidth :: Idris ConsoleWidth
getWidth = fmap idris_consolewidth getIState

setWidth :: ConsoleWidth -> Idris ()
setWidth w = do ist <- getIState
                put ist { idris_consolewidth = w }

setDepth :: Maybe Int -> Idris ()
setDepth d = do ist <- getIState
                put ist { idris_options = (idris_options ist) { opt_printdepth = d } }

typeDescription :: String
typeDescription = "The type of types"


type1Doc :: Doc OutputAnnotation
type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")


isetPrompt :: String -> Idris ()
isetPrompt p = do i <- getIState
                  case idris_outputmode i of
                    IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n

-- | Tell clients how much was parsed and loaded
isetLoadedRegion :: Idris ()
isetLoadedRegion = do i <- getIState
                      let span = idris_parsedSpan i
                      case span of
                        Just fc ->
                          case idris_outputmode i of
                            IdeMode n h ->
                              runIO . hPutStrLn h $
                                convSExp "set-loaded-region" fc n
                        Nothing -> return ()

setLogLevel :: Int -> Idris ()
setLogLevel l = do i <- getIState
                   let opts = idris_options i
                   let opt' = opts { opt_logLevel = l }
                   putIState $ i { idris_options = opt' }

setLogCats :: [LogCat] -> Idris ()
setLogCats cs = do
  i <- getIState
  let opts = idris_options i
  let opt' = opts { opt_logcats = cs }
  putIState $ i { idris_options = opt' }

setCmdLine :: [Opt] -> Idris ()
setCmdLine opts = do i <- getIState
                     let iopts = idris_options i
                     putIState $ i { idris_options = iopts { opt_cmdline = opts } }

getCmdLine :: Idris [Opt]
getCmdLine = do i <- getIState
                return (opt_cmdline (idris_options i))

getDumpHighlighting :: Idris Bool
getDumpHighlighting = do ist <- getIState
                         return (findC (opt_cmdline (idris_options ist)))
  where findC = elem DumpHighlights

getDumpDefun :: Idris (Maybe FilePath)
getDumpDefun = do i <- getIState
                  return $ findC (opt_cmdline (idris_options i))
    where findC [] = Nothing
          findC (DumpDefun x : _) = Just x
          findC (_ : xs) = findC xs

getDumpCases :: Idris (Maybe FilePath)
getDumpCases = do i <- getIState
                  return $ findC (opt_cmdline (idris_options i))
    where findC [] = Nothing
          findC (DumpCases x : _) = Just x
          findC (_ : xs) = findC xs

logLevel :: Idris Int
logLevel = do i <- getIState
              return (opt_logLevel (idris_options i))

setAutoImpls :: Bool -> Idris ()
setAutoImpls b = do i <- getIState
                    let opts = idris_options i
                    let opt' = opts { opt_autoimpls = b }
                    putIState $ i { idris_options = opt' }

getAutoImpls :: Idris Bool
getAutoImpls = do i <- getIState
                  return (opt_autoimpls (idris_options i))

setErrContext :: Bool -> Idris ()
setErrContext t = do i <- getIState
                     let opts = idris_options i
                     let opts' = opts { opt_errContext = t }
                     putIState $ i { idris_options = opts' }

errContext :: Idris Bool
errContext = do i <- getIState
                return (opt_errContext (idris_options i))

getOptimise :: Idris [Optimisation]
getOptimise = do i <- getIState
                 return (opt_optimise (idris_options i))

setOptimise :: [Optimisation] -> Idris ()
setOptimise newopts = do i <- getIState
                         let opts = idris_options i
                         let opts' = opts { opt_optimise = newopts }
                         putIState $ i { idris_options = opts' }

addOptimise :: Optimisation -> Idris ()
addOptimise opt = do opts <- getOptimise
                     setOptimise (nub (opt : opts))

removeOptimise :: Optimisation -> Idris ()
removeOptimise opt = do opts <- getOptimise
                        setOptimise ((nub opts) \\ [opt])

-- | Set appropriate optimisation set for the given level. We only
-- have one optimisation that is configurable at the moment, however!
setOptLevel :: Int -> Idris ()
setOptLevel n | n <= 0 = setOptimise []
setOptLevel 1          = setOptimise []
setOptLevel 2          = setOptimise [PETransform]
setOptLevel n | n >= 3 = setOptimise [PETransform]

useREPL :: Idris Bool
useREPL = do i <- getIState
             return (opt_repl (idris_options i))

setREPL :: Bool -> Idris ()
setREPL t = do i <- getIState
               let opts = idris_options i
               let opt' = opts { opt_repl = t }
               putIState $ i { idris_options = opt' }

showOrigErr :: Idris Bool
showOrigErr = do i <- getIState
                 return (opt_origerr (idris_options i))

setShowOrigErr :: Bool -> Idris ()
setShowOrigErr b = do i <- getIState
                      let opts = idris_options i
                      let opt' = opts { opt_origerr = b }
                      putIState $ i { idris_options = opt' }

setAutoSolve :: Bool -> Idris ()
setAutoSolve b = do i <- getIState
                    let opts = idris_options i
                    let opt' = opts { opt_autoSolve = b }
                    putIState $ i { idris_options = opt' }

setNoBanner :: Bool -> Idris ()
setNoBanner n = do i <- getIState
                   let opts = idris_options i
                   let opt' = opts { opt_nobanner = n }
                   putIState $ i { idris_options = opt' }

getNoBanner :: Idris Bool
getNoBanner = do i <- getIState
                 let opts = idris_options i
                 return (opt_nobanner opts)

setEvalTypes :: Bool -> Idris ()
setEvalTypes n = do i <- getIState
                    let opts = idris_options i
                    let opt' = opts { opt_evaltypes = n }
                    putIState $ i { idris_options = opt' }

getDesugarNats :: Idris Bool
getDesugarNats = do i <- getIState
                    let opts = idris_options i
                    return (opt_desugarnats opts)


setDesugarNats :: Bool -> Idris ()
setDesugarNats n = do i <- getIState
                      let opts = idris_options i
                      let opt' = opts { opt_desugarnats = n }
                      putIState $ i { idris_options = opt' }

setQuiet :: Bool -> Idris ()
setQuiet q = do i <- getIState
                let opts = idris_options i
                let opt' = opts { opt_quiet = q }
                putIState $ i { idris_options = opt' }

getQuiet :: Idris Bool
getQuiet = do i <- getIState
              let opts = idris_options i
              return (opt_quiet opts)

setCodegen :: Codegen -> Idris ()
setCodegen t = do i <- getIState
                  let opts = idris_options i
                  let opt' = opts { opt_codegen = t }
                  putIState $ i { idris_options = opt' }

codegen :: Idris Codegen
codegen = do i <- getIState
             return (opt_codegen (idris_options i))


setOutputTy :: OutputType -> Idris ()
setOutputTy t = do i <- getIState
                   let opts = idris_options i
                   let opt' = opts { opt_outputTy = t }
                   putIState $ i { idris_options = opt' }

outputTy :: Idris OutputType
outputTy = do i <- getIState
              return $ opt_outputTy $ idris_options i

setIdeMode :: Bool -> Handle -> Idris ()
setIdeMode True  h = do i <- getIState
                        putIState $ i { idris_outputmode = IdeMode 0 h
                                      , idris_colourRepl = False
                                      }
setIdeMode False _ = return ()

setTargetTriple :: String -> Idris ()
setTargetTriple t = do i <- getIState
                       let opts = idris_options i
                           opt' = opts { opt_triple = t }
                       putIState $ i { idris_options = opt' }

targetTriple :: Idris String
targetTriple = do i <- getIState
                  return (opt_triple (idris_options i))

setTargetCPU :: String -> Idris ()
setTargetCPU t = do i <- getIState
                    let opts = idris_options i
                        opt' = opts { opt_cpu = t }
                    putIState $ i { idris_options = opt' }

targetCPU :: Idris String
targetCPU = do i <- getIState
               return (opt_cpu (idris_options i))

verbose :: Idris Int
verbose = do
  i <- getIState
  -- Quietness overrides verbosity
  let quiet = opt_quiet   $ idris_options i
  if quiet
    then return $ 0
    else return $ (opt_verbose $ idris_options i)

setVerbose :: Int -> Idris ()
setVerbose t = do
  i <- getIState
  let opts = idris_options i
  let opt' = opts { opt_verbose = t }
  putIState $ i { idris_options = opt' }

iReport :: Int -> String -> Idris ()
iReport level msg = do
  verbosity <- verbose
  i <- getIState
  when (level <= verbosity) $
    case idris_outputmode i of
      RawOutput h -> runIO $ hPutStrLn h msg
      IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" msg n
  return ()

typeInType :: Idris Bool
typeInType = do i <- getIState
                return (opt_typeintype (idris_options i))

setTypeInType :: Bool -> Idris ()
setTypeInType t = do i <- getIState
                     let opts = idris_options i
                     let opt' = opts { opt_typeintype = t }
                     putIState $ i { idris_options = opt' }

coverage :: Idris Bool
coverage = do i <- getIState
              return (opt_coverage (idris_options i))

setCoverage :: Bool -> Idris ()
setCoverage t = do i <- getIState
                   let opts = idris_options i
                   let opt' = opts { opt_coverage = t }
                   putIState $ i { idris_options = opt' }

setIBCSubDir :: FilePath -> Idris ()
setIBCSubDir fp = do i <- getIState
                     let opts = idris_options i
                     let opt' = opts { opt_ibcsubdir = fp }
                     putIState $ i { idris_options = opt' }

valIBCSubDir :: IState -> Idris FilePath
valIBCSubDir i = return (opt_ibcsubdir (idris_options i))

addImportDir :: FilePath -> Idris ()
addImportDir fp = do i <- getIState
                     let opts = idris_options i
                     let opt' = opts { opt_importdirs = nub $ fp : opt_importdirs opts }
                     putIState $ i { idris_options = opt' }

setImportDirs :: [FilePath] -> Idris ()
setImportDirs fps = do i <- getIState
                       let opts = idris_options i
                       let opt' = opts { opt_importdirs = fps }
                       putIState $ i { idris_options = opt' }

allImportDirs :: Idris [FilePath]
allImportDirs = do i <- getIState
                   let optdirs = opt_importdirs (idris_options i)
                   return ("." : reverse optdirs)

-- Like allImportDirs but the dirs that are a prefix of
-- the files path first. This makes it look in the current
-- package first.
rankedImportDirs :: FilePath -> Idris [FilePath]
rankedImportDirs fp = do ids <- allImportDirs
                         let (prefixes, rest) = partition (`isPrefixOf`fp) ids
                         return $ prefixes ++ rest

addSourceDir :: FilePath -> Idris ()
addSourceDir fp = do i <- getIState
                     let opts = idris_options i
                     let opts' = opts { opt_sourcedirs = nub $ fp : opt_sourcedirs opts  }
                     putIState $ i { idris_options = opts' }

setSourceDirs :: [FilePath] -> Idris ()
setSourceDirs fps = do i <- getIState
                       let opts = idris_options i
                       let opts' = opts { opt_sourcedirs = nub $ fps  }
                       putIState $ i { idris_options = opts' }

allSourceDirs :: Idris [FilePath]
allSourceDirs = do i <- getIState
                   let optdirs = opt_sourcedirs (idris_options i)
                   return ("." : reverse optdirs)

colourise :: Idris Bool
colourise = do i <- getIState
               return $ idris_colourRepl i

setColourise :: Bool -> Idris ()
setColourise b = do i <- getIState
                    putIState $ i { idris_colourRepl = b }

impShow :: Idris Bool
impShow = do i <- getIState
             return (opt_showimp (idris_options i))

setImpShow :: Bool -> Idris ()
setImpShow t = do i <- getIState
                  let opts = idris_options i
                  let opt' = opts { opt_showimp = t }
                  putIState $ i { idris_options = opt' }

setColour :: ColourType -> IdrisColour -> Idris ()
setColour ct c = do i <- getIState
                    let newTheme = setColour' ct c (idris_colourTheme i)
                    putIState $ i { idris_colourTheme = newTheme }
    where setColour' KeywordColour   c t = t { keywordColour = c }
          setColour' BoundVarColour  c t = t { boundVarColour = c }
          setColour' ImplicitColour  c t = t { implicitColour = c }
          setColour' FunctionColour  c t = t { functionColour = c }
          setColour' TypeColour      c t = t { typeColour = c }
          setColour' DataColour      c t = t { dataColour = c }
          setColour' PromptColour    c t = t { promptColour = c }
          setColour' PostulateColour c t = t { postulateColour = c }

logLvl :: Int -> String -> Idris ()
logLvl = logLvlCats []

logCoverage :: Int -> String -> Idris ()
logCoverage = logLvlCats [ICoverage]

logErasure :: Int -> String -> Idris ()
logErasure = logLvlCats [IErasure]

-- | Log an action of the parser
logParser :: Int -> String -> Idris ()
logParser = logLvlCats parserCats

-- | Log an action of the elaborator.
logElab :: Int -> String -> Idris ()
logElab = logLvlCats elabCats

-- | Log an action of the compiler.
logCodeGen :: Int -> String -> Idris ()
logCodeGen = logLvlCats codegenCats

logIBC :: Int -> String -> Idris ()
logIBC = logLvlCats [IIBC]

-- | Log aspect of Idris execution
--
-- An empty set of logging levels is used to denote all categories.
--
-- @TODO update IDE protocol
logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.
           -> Int      -- ^ The Logging level the message should appear.
           -> String   -- ^ The message to show the developer.
           -> Idris ()
logLvlCats cs l msg = do
    i <- getIState
    let lvl  = opt_logLevel (idris_options i)
    let cats = opt_logcats (idris_options i)
    when (lvl >= l) $
      when (inCat cs cats || null cats) $
        case idris_outputmode i of
          RawOutput h -> do
            runIO $ hPutStrLn h msg
          IdeMode n h -> do
            let good = SexpList [IntegerAtom (toInteger l), toSExp msg]
            runIO . hPutStrLn h $ convSExp "log" good n
  where
    inCat :: [LogCat] -> [LogCat] -> Bool
    inCat cs cats = any (`elem` cats) cs

cmdOptType :: Opt -> Idris Bool
cmdOptType x = do i <- getIState
                  return $ x `elem` opt_cmdline (idris_options i)

noErrors :: Idris Bool
noErrors = do i <- getIState
              case errSpan i of
                Nothing -> return True
                _       -> return False

setTypeCase :: Bool -> Idris ()
setTypeCase t = do i <- getIState
                   let opts = idris_options i
                   let opt' = opts { opt_typecase = t }
                   putIState $ i { idris_options = opt' }

getIndentWith :: Idris Int
getIndentWith = do
  i <- getIState
  return $ interactiveOpts_indentWith (idris_interactiveOpts i)

setIndentWith :: Int -> Idris ()
setIndentWith indentWith = do
  i <- getIState
  let opts = idris_interactiveOpts i
  let opts' = opts { interactiveOpts_indentWith = indentWith }
  putIState $ i { idris_interactiveOpts = opts' }

getIndentClause :: Idris Int
getIndentClause = do
  i <- getIState
  return $ interactiveOpts_indentClause (idris_interactiveOpts i)

setIndentClause :: Int -> Idris ()
setIndentClause indentClause = do
  i <- getIState
  let opts = idris_interactiveOpts i
  let opts' = opts { interactiveOpts_indentClause = indentClause }
  putIState $ i { idris_interactiveOpts = opts' }

-- Dealing with parameters

expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
                [Name] -> -- all names
                [Name] -> -- names with no declaration
                PTerm -> PTerm
expandParams dec ps ns infs tm = en 0 tm
  where
    -- if we shadow a name (say in a lambda binding) that is used in a call to
    -- a lifted function, we need access to both names - once in the scope of the
    -- binding and once to call the lifted functions. So we'll explicitly shadow
    -- it. (Yes, it's a hack. The alternative would be to resolve names earlier
    -- but we didn't...)

    mkShadow (UN n) = MN 0 n
    mkShadow (MN i n) = MN (i+1) n
    mkShadow (NS x s) = NS (mkShadow x) s

    en :: Int -- ^ The quotation level - only transform terms that are used, not terms
              -- that are merely mentioned.
        -> PTerm -> PTerm
    en 0 (PLam fc n nfc t s)
       | n `elem` (map fst ps ++ ns)
               = let n' = mkShadow n in
                     PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
       | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
    en 0 (PPi p n nfc t s)
       | n `elem` (map fst ps ++ ns)
               = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
                     PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
       | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
    en 0 (PLet fc rc n nfc ty v s)
       | n `elem` (map fst ps ++ ns)
               = let n' = mkShadow n in
                     PLet fc rc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
       | otherwise = PLet fc rc n nfc (en 0 ty) (en 0 v) (en 0 s)
    -- FIXME: Should only do this in a type signature!
    en 0 (PDPair f hls p (PRef f' fcs n) t r)
       | n `elem` (map fst ps ++ ns) && t /= Placeholder
           = let n' = mkShadow n in
                 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
    en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)
    en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
    en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
    en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
    en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
    en 0 (PHidden t) = PHidden (en 0 t)
    en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
    en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
    en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
    en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
    en 0 (PProof ts)   = PProof (map (fmap (en 0)) ts)
    en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)

    en 0 (PQuote (Var n))
        | n `nselem` ns = PQuote (Var (dec n))
    en 0 (PApp fc (PInferRef fc' hl n) as)
        | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
                           (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
    en 0 (PApp fc (PRef fc' hl n) as)
        | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
                           (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
        | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
                           (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
    en 0 (PAppBind fc (PRef fc' hl n) as)
        | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
                           (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
        | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
                           (map ((pexp . (PRef fc hl)) . fst) ps ++ (map (fmap (en 0)) as))
    en 0 (PRef fc hl n)
        | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
                           (map ((pexp . (PRef fc hl)) . fst) ps)
        | n `nselem` ns = PApp fc (PRef fc hl (dec n))
                           (map ((pexp . (PRef fc hl)) . fst) ps)
    en 0 (PInferRef fc hl n)
        | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
                           (map ((pexp . (PRef fc hl)) . fst) ps)
    en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
    en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
    en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
    en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
    en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
    en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)

    en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
    en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)

    en ql t = descend (en ql) t

    nselem x [] = False
    nselem x (y : xs) | nseq x y = True
                      | otherwise = nselem x xs

    nseq x y = nsroot x == nsroot y

    enTacImp ql (TacImp aos st scr rig) = TacImp aos st (en ql scr) rig
    enTacImp ql other                   = other

expandParamsD :: Bool -> -- True = RHS only
                 IState ->
                 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)
    = if n `elem` ns && (not rhsonly)
         then -- trace (show (n, expandParams dec ps ns ty)) $
              PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))
         else --trace (show (n, expandParams dec ps ns ty)) $
              PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)
expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc nfc o n ty)
    = if n `elem` ns && (not rhsonly)
         then -- trace (show (n, expandParams dec ps ns ty)) $
              PPostulate e doc syn fc nfc o (dec n)
                         (piBind ps (expandParams dec ps ns [] ty))
         else --trace (show (n, expandParams dec ps ns ty)) $
              PPostulate e doc syn fc nfc o n (expandParams dec ps ns [] ty)
expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
    = let n' = if n `elem` ns then dec n else n in
          PClauses fc opts n' (map expandParamsC cs)
  where
    expandParamsC (PClause fc n lhs ws rhs ds)
        = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])
              ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
              lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
              n' = if n `elem` ns then dec n else n
              -- names bound on the lhs should not be expanded on the rhs
              ns' = removeBound lhs ns in
              PClause fc n' lhs'
                            (map (expandParams dec ps'' ns' []) ws)
                            (expandParams dec ps'' ns' [] rhs)
                            (map (expandParamsD True ist dec ps'' ns') ds)
    expandParamsC (PWith fc n lhs ws wval pn ds)
        = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])
              ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])
              lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)
              n' = if n `elem` ns then dec n else n
              ns' = removeBound lhs ns in
              PWith fc n' lhs'
                          (map (expandParams dec ps'' ns' []) ws)
                          (expandParams dec ps'' ns' [] wval)
                          pn
                          (map (expandParamsD rhsonly ist dec ps'' ns') ds)
    updateps yn nm [] = []
    updateps yn nm (((a, t), i):as)
        | (a `elem` nm) == yn = (a, t) : updateps yn nm as
        | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as

    removeBound lhs ns = ns \\ nub (bnames lhs)

    bnames (PRef _ _ n) = [n]
    bnames (PApp _ _ args) = concatMap (bnames . getTm) args
    bnames (PPair _ _ _ l r) = bnames l ++ bnames r
    bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r
    bnames _ = []

-- | Expands parameters defined in parameter and where blocks inside of declarations
expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
    = PData doc argDocs syn fc co (expandPData pd)
  where
    -- just do the type decl, leave constructors alone (parameters will be
    -- added implicitly)
    expandPData (PDatadecl n nfc ty cons)
       = if n `elem` ns
            then PDatadecl (dec n) nfc (piBind ps (expandParams dec ps ns [] ty))
                           (map econ cons)
            else PDatadecl n nfc (expandParams dec ps ns [] ty) (map econ cons)
    econ (doc, argDocs, n, nfc, t, fc, fs)
       = (doc, argDocs, dec n, nfc, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name nfc prs pdocs fls cn cdoc csyn)
  = d
expandParamsD rhs ist dec ps ns (PParams f params pds)
   = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
               (map (expandParamsD True ist dec ps ns) pds)
--                (map (expandParamsD ist dec ps ns) pds)
expandParamsD rhs ist dec ps ns (PMutual f pds)
   = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)
expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd)
   = PInterface doc info f
           (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
           n nfc
           (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)
           pDocs
           fds
           (map (expandParamsD rhs ist dec ps ns) decls)
           cn
           cd
expandParamsD rhs ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
   = let cn' = case cn of
                    Just n -> if n `elem` ns then Just (dec n) else Just n
                    Nothing -> Nothing in
     PImplementation doc argDocs info f
                     (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
                     pnames acc opts n
                     nfc
                     (map (expandParams dec ps ns []) params)
                     (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
                     (expandParams dec ps ns [] ty)
                     cn'
                     (map (expandParamsD True ist dec ps ns) decls)
expandParamsD rhs ist dec ps ns d = d

mapsnd f (x, t) = (x, f t)

expandImplementationScope ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
    = PImplementation doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
                      ty cn decls
expandImplementationScope ist dec ps ns d = d

-- | Calculate a priority for a type, for deciding elaboration order
-- * if it's just a type variable or concrete type, do it early (0)
-- * if there's only type variables and injective constructors, do it next (1)
-- * if there's a function type, next (2)
-- * finally, everything else (3)
getPriority :: IState -> PTerm -> Int
getPriority i tm = 1

addStatics :: Name -> Term -> PTerm -> Idris ()
addStatics n tm ptm =
    do let (statics, dynamics) = initStatics tm ptm
       ist <- getIState
       let paramnames
              = nub $ case lookupCtxtExact n (idris_fninfo ist) of
                           Just p -> getNamesFrom 0 (fn_params p) tm ++
                                     concatMap (getParamNames ist . snd) statics
                           _ -> concatMap (getParamNames ist . snd) statics

       let stnames = nub $ concatMap (freeArgNames . snd) statics
       let dnames = (nub $ concatMap (freeArgNames . snd) dynamics)
                             \\ paramnames
       -- also get the arguments which are 'uniquely inferrable' from
       -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
       -- or parameters to the type of a static
       let statics' = nub $ map fst statics ++
                              filter (\x -> not (elem x dnames)) stnames
       let stpos = staticList statics' tm
       i <- getIState
       unless (null statics) $
          logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ "\n"
                        ++ showTmImpls ptm ++ "\n"
                        ++ show statics ++ "\n" ++ show dynamics
                        ++ "\n" ++ show paramnames
                        ++ "\n" ++ show stpos
       putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
       addIBC (IBCStatic n)
  where
    initStatics (Bind n (Pi _ _ ty _) sc) (PPi p n' fc t s)
            | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
                            (static, (n, ty) : dynamic)
    initStatics (Bind n (Pi _ _ ty _) sc) (PPi p n' fc _ s)
            = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
                  if pstatic p == Static then ((n, ty) : static, dynamic)
                    else if (not (searchArg p))
                            then (static, (n, ty) : dynamic)
                            else (static, dynamic)
    initStatics t pt = ([], [])

    getParamNames ist tm | (P _ n _ , args) <- unApply tm
       = case lookupCtxtExact n (idris_datatypes ist) of
              Just ti -> getNamePos 0 (param_pos ti) args
              Nothing -> []
      where getNamePos i ps [] = []
            getNamePos i ps (P _ n _ : as)
                 | i `elem` ps = n : getNamePos (i + 1) ps as
            getNamePos i ps (_ : as) = getNamePos (i + 1) ps as
    getParamNames ist (Bind t (Pi _ _ (P _ n _) _) sc)
       = n : getParamNames ist sc
    getParamNames ist _ = []

    getNamesFrom i ps (Bind n (Pi _ _ _ _) sc)
       | i `elem` ps = n : getNamesFrom (i + 1) ps sc
       | otherwise = getNamesFrom (i + 1) ps sc
    getNamesFrom i ps sc = []

    freeArgNames (Bind n (Pi _ _ ty _) sc)
          = nub $ freeNames ty ++ freeNames sc -- treat '->' as fn here
    freeArgNames tm = let (_, args) = unApply tm in
                          concatMap freeNames args

    -- if a name appears in an interface or tactic implicit index, it doesn't
    -- affect its 'uniquely inferrable' from a static status since these are
    -- resolved by searching.
    searchArg (Constraint _ _ _) = True
    searchArg (TacImp _ _ _ _) = True
    searchArg _ = False

    staticList sts (Bind n (Pi _ _ _ _) sc) = (n `elem` sts) : staticList sts sc
    staticList _ _ = []

-- Dealing with implicit arguments

-- Add some bound implicits to the using block if they aren't there already

addToUsing :: [Using] -> [(Name, PTerm)] -> [Using]
addToUsing us [] = us
addToUsing us ((n, t) : ns)
   | n `notElem` mapMaybe impName us = addToUsing (us ++ [UImplicit n t]) ns
   | otherwise = addToUsing us ns
  where impName (UImplicit n _) = Just n
        impName _ = Nothing

-- Add constraint bindings from using block

addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
addUsingConstraints syn fc t
   = do ist <- get
        let ns = namesIn [] ist t
        let cs = getConstraints t -- check declared constraints
        let addconsts = uconsts \\ cs
        return (doAdd addconsts ns t)
   where uconsts = filter uconst (using syn)
         uconst (UConstraint _ _) = True
         uconst _ = False

         doAdd [] _ t = t
         -- if all of args in ns, then add it
         doAdd (UConstraint c args : cs) ns t
             | all (\n -> elem n ns) args
                   = PPi (Constraint [] Dynamic RigW) (sMN 0 "cu") NoFC
                         (mkConst c args) (doAdd cs ns t)
             | otherwise = doAdd cs ns t

         mkConst c args = PApp fc (PRef fc [] c)
                           (map (PExp 0 [] (sMN 0 "carg") . PRef fc []) args)

         getConstraints (PPi (Constraint _ _ _) _ _ c sc)
             = getcapp c ++ getConstraints sc
         getConstraints (PPi _ _ _ c sc) = getConstraints sc
         getConstraints _ = []

         getcapp (PApp _ (PRef _ _ c) args)
             = do ns <- mapM getName args
                  return (UConstraint c ns)
         getcapp _ = []

         getName (PExp _ _ _ (PRef _ _ n)) = return n
         getName _ = []

-- | Add implicit bindings from using block, and bind any missing names
addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm
addUsingImpls syn n fc t
   = do ist <- getIState
        autoimpl <- getAutoImpls
        let ns_in = implicitNamesIn (map iname uimpls) ist t
        let ns = if autoimpl then ns_in
                    else filter (\n -> n `elem` (map iname uimpls)) ns_in

        let badnames = filter (\n -> not (implicitable n) &&
                                     n `notElem` (map iname uimpls)) ns
        unless (null badnames) $
           throwError (At fc (Elaborating "type of " n Nothing
                         (NoSuchVariable (head badnames))))
        let cs = getArgnames t -- get already bound names
        let addimpls = filter (\n -> iname n `notElem` cs) uimpls
        -- if all names in the arguments of addconsts appear in ns,
        -- add the constraint implicitly
        return (bindFree ns (doAdd addimpls ns t))
   where uimpls = filter uimpl (using syn)
         uimpl (UImplicit _ _) = True
         uimpl _ = False

         iname (UImplicit n _) = n
         iname (UConstraint _ _) = error "Can't happen addUsingImpls"

         doAdd [] _ t = t
         -- if all of args in ns, then add it
         doAdd (UImplicit n ty : cs) ns t
             | elem n ns
                   = PPi impl_gen n NoFC ty (doAdd cs ns t)
             | otherwise = doAdd cs ns t

         -- bind the free names which weren't in the using block
         bindFree [] tm = tm
         bindFree (n:ns) tm
             | elem n (map iname uimpls) = bindFree ns tm
             | otherwise
                    = PPi (impl_gen { pargopts = [InaccessibleArg] }) n NoFC Placeholder (bindFree ns tm)

         getArgnames (PPi _ n _ c sc)
             = n : getArgnames sc
         getArgnames _ = []

-- Given the original type and the elaborated type, return the implicitness
-- status of each pi-bound argument, and whether it's inaccessible (True) or not.

getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
getUnboundImplicits i t tm = getImps t (collectImps tm)
  where collectImps (PPi p n _ t sc)
            = (n, (p, t)) : collectImps sc
        collectImps _ = []

        scopedimpl (Just i) = not (toplevel_imp i)
        scopedimpl _ = False

        getImps (Bind n (Pi _ i _ _) sc) imps
             | scopedimpl i = getImps sc imps
        getImps (Bind n (Pi _ _ t _) sc) imps
            | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps
         where
            argInfo n (Imp opt _ _ _ _ _) Placeholder
                   = (True, PImp 0 True opt n Placeholder)
            argInfo n (Imp opt _ _ _ _ _) t'
                   = (InaccessibleArg `elem` opt,
                          PImp (getPriority i t') True opt n t')
            argInfo n (Exp opt _ _ _) t'
                   = (InaccessibleArg `elem` opt,
                          PExp (getPriority i t') opt n t')
            argInfo n (Constraint opt _ _) t'
                   = (InaccessibleArg `elem` opt,
                          PConstraint 10 opt n t')
            argInfo n (TacImp opt _ scr _) t'
                   = (InaccessibleArg `elem` opt,
                          PTacImplicit 10 opt n scr t')
        getImps (Bind n (Pi _ _ t _) sc) imps = impBind n t : getImps sc imps
           where impBind n t = (True, PImp 1 True [] n Placeholder)
        getImps sc tm = []

-- Add implicit Pi bindings for any names in the term which appear in an
-- argument position.

-- This has become a right mess already. Better redo it some time...
-- TODO: This is obsoleted by the new way of elaborating types, (which
-- calls addUsingImpls) but there's still a couple of places which use
-- it. Clean them up!
--
-- Issue 1739 in the issue tracker
--     https://github.com/idris-lang/Idris-dev/issues/1739
implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm
implicit info syn n ptm = implicit' info syn [] n ptm

implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
implicit' info syn ignore n ptm
    = do i <- getIState
         auto <- getAutoImpls
         let (tm', impdata) = implicitise auto syn ignore i ptm
         defaultArgCheck (eInfoNames info ++ M.keys (idris_implicits i)) impdata
--          let (tm'', spos) = findStatics i tm'
         putIState $ i { idris_implicits = addDef n impdata (idris_implicits i) }
         addIBC (IBCImp n)
         logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)
--          i <- get
--          putIState $ i { idris_statics = addDef n spos (idris_statics i) }
         return tm'
  where
    --  Detect unknown names in default arguments and throw error if found.
    defaultArgCheck :: [Name] -> [PArg] -> Idris ()
    defaultArgCheck knowns params = foldM_ notFoundInDefault knowns params

    notFoundInDefault :: [Name] -> PArg -> Idris [Name]
    notFoundInDefault kns (PTacImplicit _ _ n script _)
      = do  i <- getIState
            case notFound kns (namesIn [] i script) of
              Nothing     -> return (n:kns)
              Just name   -> throwError (NoSuchVariable name)
    notFoundInDefault kns p = return ((pname p):kns)

    notFound :: [Name] -> [Name] -> Maybe Name
    notFound kns [] = Nothing
    notFound kns (SN (WhereN _ _ _) : ns) = notFound kns ns --  Known already
    notFound kns (n:ns) = if elem n kns then notFound kns ns else Just n

-- | Even if auto_implicits is off, we need to call this so we record
-- which arguments are implicit
implicitise :: Bool -> SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
      let (declimps, ns') = execState (imps True [] tm) ([], [])
          ns = filter (\n -> auto && implicitable n || elem n (map fst uvars)) $
                  ns' \\ (map fst pvars ++ no_imp syn ++ ignore)
          nsOrder = filter (not . inUsing) ns ++ filter inUsing ns in
          if null ns
            then (tm, reverse declimps)
            else implicitise auto syn ignore ist (pibind uvars nsOrder tm)
  where
    uvars = map ipair (filter uimplicit (using syn))
    pvars = syn_params syn

    inUsing n = n `elem` map fst uvars

    ipair (UImplicit x y) = (x, y)
    uimplicit (UImplicit _ _) = True
    uimplicit _ = False

    dropAll (x:xs) ys | x `elem` ys = dropAll xs ys
                      | otherwise   = x : dropAll xs ys
    dropAll [] ys = []

    -- Find names in argument position in a type, suitable for implicit
    -- binding
    -- Not the function position, but do everything else...
    implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
    implNamesIn uv t = implicitNamesIn (map fst uv) ist t

    imps top env ty@(PApp _ f as)
       = do (decls, ns) <- get
            let isn = nub (implNamesIn uvars ty)
            put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
    imps top env (PPi (Imp l _ _ _ _ _) n _ ty sc)
        = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
             (decls , ns) <- get
             put (PImp (getPriority ist ty) True l n Placeholder : decls,
                  nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
             imps True (n:env) sc
    imps top env (PPi (Exp l _ _ _) n _ ty sc)
        = do let isn = nub (implNamesIn uvars ty ++ case sc of
                            (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
                            _ -> [])
             (decls, ns) <- get -- ignore decls in HO types
             put (PExp (getPriority ist ty) l n Placeholder : decls,
                  nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
             imps True (n:env) sc
    imps top env (PPi (Constraint l _ _) n _ ty sc)
        = do let isn = nub (implNamesIn uvars ty ++ case sc of
                            (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
                            _ -> [])
             (decls, ns) <- get -- ignore decls in HO types
             put (PConstraint 10 l n Placeholder : decls,
                  nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
             imps True (n:env) sc
    imps top env (PPi (TacImp l _ scr _) n _ ty sc)
        = do let isn = nub (implNamesIn uvars ty ++ case sc of
                            (PRef _ _ x) -> namesIn uvars ist sc `dropAll` [n]
                            _ -> [])
             (decls, ns) <- get -- ignore decls in HO types
             put (PTacImplicit 10 l n scr Placeholder : decls,
                  nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
             imps True (n:env) sc
    imps top env (PRewrite _ _ l r _)
        = do (decls, ns) <- get
             let isn = namesIn uvars ist l ++ namesIn uvars ist r
             put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
    imps top env (PTyped l r)
        = imps top env l
    imps top env (PPair _ _ _ l r)
        = do (decls, ns) <- get
             let isn = namesIn uvars ist l ++ namesIn uvars ist r
             put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
    imps top env (PDPair _ _ _ (PRef _ _ n) t r)
        = do (decls, ns) <- get
             let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]
             put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
    imps top env (PDPair _ _ _ l t r)
        = do (decls, ns) <- get
             let isn = namesIn uvars ist l ++ namesIn uvars ist t ++
                       namesIn uvars ist r
             put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))
    imps top env (PAlternative ms a as)
        = do (decls, ns) <- get
             let isn = concatMap (namesIn uvars ist) as
             put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
    imps top env (PLam fc n _ ty sc)
        = do imps False env ty
             imps False (n:env) sc
    imps top env (PHidden tm)    = imps False env tm
    imps top env (PUnifyLog tm)  = imps False env tm
    imps top env (PNoImplicits tm)  = imps False env tm
    imps top env (PRunElab fc tm ns) = imps False env tm
    imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!
    imps top env _               = return ()

    pibind using []     sc = sc
    pibind using (n:ns) sc
      = case lookup n using of
            Just ty -> PPi impl_gen
                           n NoFC ty (pibind using ns sc)
            Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })
                           n NoFC Placeholder (pibind using ns sc)

-- | Add implicit arguments in function calls
addImplPat :: IState -> PTerm -> PTerm
addImplPat = addImpl' True [] [] []

addImplBound :: IState -> [Name] -> PTerm -> PTerm
addImplBound ist ns = addImpl' False ns [] [] ist

addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
addImplBoundInf ist ns inf = addImpl' False ns inf [] ist

-- | Add the implicit arguments to applications in the term [Name]
-- gives the names to always expend, even when under a binder of that
-- name (this is to expand methods with implicit arguments in
-- dependent interfaces).
addImpl :: [Name] -> IState -> PTerm -> PTerm
addImpl = addImpl' False [] []

-- TODO: in patterns, don't add implicits to function names guarded by constructors
-- and *not* inside a PHidden

addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
addImpl' inpat env infns imp_meths ist ptm
   = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
  where
    allowcap = AllowCapitalizedPatternVariables `elem` opt_cmdline (idris_options ist)

    topname = case ptm of
                   PRef _ _ n -> n
                   PApp _ (PRef _ _ n) _ -> n
                   _ -> sUN "" -- doesn't matter then

    ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
    ai inpat qq env ds (PRef fc fcs f)
        | f `elem` infns = PInferRef fc fcs f
        | not (f `elem` map fst env) = handleErr $ aiFn topname allowcap inpat inpat qq imp_meths ist fc f fc ds []
    ai inpat qq env ds (PHidden (PRef fc hl f))
        | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname allowcap inpat False qq imp_meths ist fc f fc ds [])
    ai inpat qq env ds (PRewrite fc by l r g)
       = let l' = ai inpat qq env ds l
             r' = ai inpat qq env ds r
             g' = fmap (ai inpat qq env ds) g in
         PRewrite fc by l' r' g'
    ai inpat qq env ds (PTyped l r)
      = let l' = ai inpat qq env ds l
            r' = ai inpat qq env ds r in
            PTyped l' r'
    ai inpat qq env ds (PPair fc hls p l r)
      = let l' = ai inpat qq env ds l
            r' = ai inpat qq env ds r in
            PPair fc hls p l' r'
    ai inpat qq env ds (PDPair fc hls p l t r)
         = let l' = ai inpat qq env ds l
               t' = ai inpat qq env ds t
               r'