{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
             TypeSynonymInstances, PatternGuards #-}

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

import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Typecheck
import Idris.AbsSyntaxTree
import Idris.Colours
import Idris.IdeSlave
import IRTS.CodegenCommon
import Util.DynamicLinker

import Paths_idris

import System.Console.Haskeline
import System.IO

import Control.Monad.State
import Control.Monad.Error(throwError)

import Data.List
import Data.Char
import qualified Data.Text as T
import Data.Either
import qualified Data.Map as M
import Data.Maybe
import qualified Data.Set as S
import Data.Word (Word)

import Debug.Trace

import Control.Monad.Error (throwError, catchError)
import System.IO.Error(isUserError, ioeGetErrorString, tryIOError)

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, tgt == tgt']

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 $ (tgt, f) : idris_objs i }

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 $ (tgt, f) : idris_libs i }

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 $ (tgt, f) : idris_cgflags i }

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


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

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

addTrans :: (Term, Term) -> Idris ()
addTrans t = do i <- getIState
                putIState $ i { idris_transforms = t : idris_transforms i }

addErrRev :: (Term, Term) -> Idris ()
addErrRev t = do i <- getIState
                 putIState $ i { idris_errRev = t : idris_errRev i }

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

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

setTotality :: Name -> Totality -> Idris ()
setTotality n a
         = do i <- getIState
              let ctxt = setTotal 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 t [] = []
          findCoercions t (n : ns) =
             let ps = case lookupTy n (tt_ctxt i) of
                        [ty'] -> case unApply (getRetTy ty') of
                                   (t', _) ->
                                      if t == t' then [n] else []
                        _ -> [] 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) }

-- | Adds error handlers for a particular function and argument. If names are is 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 }

getFunctionErrorHandlers :: Name -> Name -> Idris [Name]
getFunctionErrorHandlers f arg = do i <- getIState
                                    return . maybe [] S.toList $
                                     undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)


-- Trace all the names in a call graph starting at the given name
getAllNames :: Name -> Idris [Name]
getAllNames n = allNames [] n

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

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

addDocStr :: Name -> String -> Idris ()
addDocStr n doc
   = do i <- getIState
        putIState $ i { idris_docstrings = addDef n doc (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 show (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 i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]
getNameHints i n =
        case lookupCtxt n (idris_namehints i) of
             [ns] -> ns
             _ -> []

addToCalledG :: Name -> [Name] -> Idris ()
addToCalledG n ns = return () -- TODO

-- Add a class instance function. Dodgy hack: Put integer instances first in the
-- list so they are resolved by default.
-- Dodgy hack 2: put constraint chasers (@@) last

addInstance :: Bool -> Name -> Name -> Idris ()
addInstance int n i
    = do ist <- getIState
         case lookupCtxt n (idris_classes ist) of
                [CI a b c d e ins] ->
                     do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
                        putIState $ ist { idris_classes = cs }
                _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)
                        putIState $ ist { idris_classes = cs }
  where addI i ins | int = i : ins
                   | chaser n = ins ++ [i]
                   | otherwise = insI i ins
        insI i [] = [i]
        insI i (n : ns) | chaser n = i : n : ns
                        | otherwise = n : insI i ns

        chaser (UN nm) 
             | ('@':'@':_) <- str nm = True
        chaser (NS n _) = chaser n
        chaser _ = False

addClass :: Name -> ClassInfo -> Idris ()
addClass n i
   = do ist <- getIState
        let i' = case lookupCtxt n (idris_classes ist) of
                      [c] -> c { class_instances = class_instances i }
                      _ -> i
        putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

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': is) | 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 = [] }

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

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

setErrLine :: Int -> Idris ()
setErrLine x = do i <- getIState;
                  case (errLine i) of
                      Nothing -> putIState $ i { errLine = Just x }
                      Just _ -> return ()

clearErr :: Idris ()
clearErr = do i <- getIState
              putIState $ i { errLine = 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

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

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

addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
addInternalApp fp l t
    = do i <- getIState
         putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })

getInternalApp :: FilePath -> Int -> Idris PTerm
getInternalApp fp l = do i <- getIState
                         case lookup (fp, l) (idris_lineapps i) of
                              Just n' -> return n'
                              Nothing -> return Placeholder
                              -- TODO: What if it's not there?

-- 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 tot 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' c' 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 fc n
    = do i <- getContext
         case lookupTy n i of
             (_:_)  -> 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 i <- getIState
         let ctxt = tt_ctxt i
         let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
                            next_tvar = v }
         let ics = zip cs (repeat fc) ++ idris_constraints i
         putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

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

addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
addDeferred' nt ns
  = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns
       i <- getIState
       putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++
                                            idris_metavars i }
  where tidyNames used (Bind (MN i x) b sc)
            = let n' = uniqueName (UN x) used in
                  Bind n' b $ tidyNames (n':used) sc
        tidyNames used (Bind n b sc)
            = let n' = uniqueName n used in
                  Bind n' b $ tidyNames (n':used) sc
        tidyNames used b = b

solveDeferred :: Name -> Idris ()
solveDeferred n = do i <- getIState
                     putIState $ i { idris_metavars =
                                       filter (\(n', _) -> n/=n')
                                          (idris_metavars i) }

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

ihPrintResult :: Handle -> String -> Idris ()
ihPrintResult h s = do i <- getIState
                       case idris_outputmode i of
                         RawOutput -> case s of
                                        "" -> return ()
                                        s  -> runIO $ hPutStrLn h s
                         IdeSlave n ->
                             let good = SexpList [SymbolAtom "ok", toSExp s] in
                             runIO $ hPutStrLn h $ convSExp "return" good n

-- | Write a pretty-printed term to the console with semantic coloring
consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
consoleDisplayAnnotated h output = do ist <- getIState
                                      runIO . hPutStrLn h .
                                        displayDecorated (consoleDecorate ist) .
                                        renderCompact $ output

-- | Write pretty-printed output to IDESlave with semantic annotations
ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
ideSlaveReturnAnnotated n h out = do ist <- getIState
                                     let (str, spans) = displaySpans .
                                                        renderCompact .
                                                        fmap (fancifyAnnots ist) $
                                                        out
                                         good = [SymbolAtom "ok", toSExp str, toSExp spans]
                                     runIO . hPutStrLn h $ convSExp "return" good n

ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
ihPrintTermWithType h tm ty = do ist <- getIState
                                 let output = tm <+> colon <+> ty
                                 case idris_outputmode ist of
                                   RawOutput -> consoleDisplayAnnotated h output
                                   IdeSlave n -> ideSlaveReturnAnnotated n h output

-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()
ihPrintFunTypes h n []        = ihPrintError h $ "No such variable " ++ show n
ihPrintFunTypes h n overloads = do imp <- impShow
                                   ist <- getIState
                                   let output = vsep (map (uncurry (ppOverload imp)) overloads)
                                   case idris_outputmode ist of
                                     RawOutput -> consoleDisplayAnnotated h output
                                     IdeSlave n -> ideSlaveReturnAnnotated n h output
  where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
        ppOverload imp n tm = fullName n <+> colon <+> prettyImp imp tm

fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
fancifyAnnots ist annot@(AnnName n _ _) =
  do let ctxt = tt_ctxt ist
     case () of
       _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
       _ | isFnName   n ctxt -> AnnName n (Just FunOutput) Nothing
       _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
       _ | otherwise         -> annot
fancifyAnnots _ annot = annot

type1Doc :: Doc OutputAnnotation
type1Doc = (annotate AnnConstType $ text "Type 1")

ihPrintError :: Handle -> String -> Idris ()
ihPrintError h s = do i <- getIState
                      case idris_outputmode i of
                        RawOutput -> case s of
                                          "" -> return ()
                                          s  -> runIO $ hPutStrLn h s
                        IdeSlave n ->
                          let good = SexpList [SymbolAtom "error", toSExp s] in
                          runIO . hPutStrLn h $ convSExp "return" good n

ihputStrLn :: Handle -> String -> Idris ()
ihputStrLn h s = do i <- getIState
                    case idris_outputmode i of
                      RawOutput -> runIO $ hPutStrLn h s
                      IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n

iputStrLn = ihputStrLn stdout
iPrintError = ihPrintError stdout
iPrintResult = ihPrintResult stdout
iWarn = ihWarn stdout

ideslavePutSExp :: SExpable a => String -> a -> Idris ()
ideslavePutSExp cmd info = do i <- getIState
                              case idris_outputmode i of
                                   IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
                                   _ -> return ()

-- this needs some typing magic and more structured output towards emacs
iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
iputGoal g = do i <- getIState
                case idris_outputmode i of
                  RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
                  IdeSlave n -> runIO . putStrLn $
                                convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

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

ihWarn :: Handle -> FC -> String -> Idris ()
ihWarn h fc err = do i <- getIState
                     case idris_outputmode i of
                       RawOutput -> runIO $ hPutStrLn h (show fc ++ ":" ++ err)
                       IdeSlave n -> runIO $ hPutStrLn h $ convSExp "warning" (fc_fname fc, fc_line fc, fc_column fc, err) n

setLogLevel :: Int -> Idris ()
setLogLevel l = do i <- getIState
                   let opts = idris_options i
                   let opt' = opts { opt_logLevel = l }
                   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))

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

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

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

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

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)

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

setIdeSlave :: Bool -> Idris ()
setIdeSlave True  = do i <- getIState
                       putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }
setIdeSlave 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))

setOptLevel :: Word -> Idris ()
setOptLevel t = do i <- getIState
                   let opts = idris_options i
                       opt' = opts { opt_optLevel = t }
                   putIState $ i { idris_options = opt' }

optLevel :: Idris Word
optLevel = do i <- getIState
              return (opt_optLevel (idris_options i))

verbose :: Idris Bool
verbose = do i <- getIState
             return (opt_verbose (idris_options i))

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

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

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

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

setOutH :: Handle -> Idris ()
setOutH h = do i <- getIState
               putIState $ i { idris_outh = h }

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 }

logLvl :: Int -> String -> Idris ()
logLvl l str = do i <- getIState
                  let lvl = opt_logLevel (idris_options i)
                  when (lvl >= l) $
                    case idris_outputmode i of
                      RawOutput -> do runIO $ putStrLn str
                      IdeSlave n ->
                        do let good = SexpList [IntegerAtom (toInteger l), toSExp str]
                           runIO $ putStrLn $ convSExp "log" good n

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

iLOG :: String -> Idris ()
iLOG = logLvl 1

noErrors :: Idris Bool
noErrors = do i <- getIState
              case errLine 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' }


-- 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 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 (PLam n t s)
       | n `elem` (map fst ps ++ ns)
               = let n' = mkShadow n in
                     PLam n' (en t) (en (shadow n n' s))
       | otherwise = PLam n (en t) (en s)
    en (PPi p n t s)
       | n `elem` (map fst ps ++ ns)
               = let n' = mkShadow n in
                     PPi p n' (en t) (en (shadow n n' s))
       | otherwise = PPi p n (en t) (en s)
    en (PLet n ty v s)
       | n `elem` (map fst ps ++ ns)
               = let n' = mkShadow n in
                     PLet n' (en ty) (en v) (en (shadow n n' s))
       | otherwise = PLet n (en ty) (en v) (en s)
    -- FIXME: Should only do this in a type signature!
    en (PDPair f (PRef f' n) t r)
       | n `elem` (map fst ps ++ ns) && t /= Placeholder
           = let n' = mkShadow n in
                 PDPair f (PRef f' n') (en t) (en (shadow n n' r))
    en (PEq f l r) = PEq f (en l) (en r)
    en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
    en (PTyped l r) = PTyped (en l) (en r)
    en (PPair f l r) = PPair f (en l) (en r)
    en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
    en (PAlternative a as) = PAlternative a (map en as)
    en (PHidden t) = PHidden (en t)
    en (PUnifyLog t) = PUnifyLog (en t)
    en (PNoImplicits t) = PNoImplicits (en t)
    en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
    en (PProof ts)   = PProof (map (fmap en) ts)
    en (PTactics ts) = PTactics (map (fmap en) ts)

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

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

    nseq x y = nsroot x == nsroot y

expandParamsD :: Bool -> -- True = RHS only
                 IState ->
                 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
    = if n `elem` ns && (not rhsonly)
         then -- trace (show (n, expandParams dec ps ns ty)) $
              PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))
         else --trace (show (n, expandParams dec ps ns ty)) $
              PTy doc syn fc o n (expandParams dec ps ns [] ty)
expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)
    = if n `elem` ns && (not rhsonly)
         then -- trace (show (n, expandParams dec ps ns ty)) $
              PPostulate doc syn fc o (dec n) (piBind ps
                            (expandParams dec ps ns [] ty))
         else --trace (show (n, expandParams dec ps ns ty)) $
              PPostulate doc syn fc 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 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)
                          (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 n ++ "_u"), t) : updateps yn nm as

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

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

expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)
    = PData doc syn fc co (expandPData pd)
  where
    -- just do the type decl, leave constructors alone (parameters will be
    -- added implicitly)
    expandPData (PDatadecl n ty cons)
       = if n `elem` ns
            then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))
                           (map econ cons)
            else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
    econ (doc, n, t, fc, fs)
       = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
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 (PClass doc info f cs n params decls)
   = PClass doc info f
           (map (expandParams dec ps ns []) cs)
           n
           (map (mapsnd (expandParams dec ps ns [])) params)
           (map (expandParamsD rhs ist dec ps ns) decls)
expandParamsD rhs ist dec ps ns (PInstance info f cs n params ty cn decls)
   = PInstance info f
           (map (expandParams dec ps ns []) cs)
           n
           (map (expandParams dec ps ns []) params)
           (expandParams dec ps ns [] ty)
           cn
           (map (expandParamsD rhs ist dec ps ns) decls)
expandParamsD rhs ist dec ps ns d = d

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

-- 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 -- pri tm
  where
    pri (PRef _ n) =
        case lookupP n (tt_ctxt i) of
            ((P (DCon _ _) _ _):_) -> 1
            ((P (TCon _ _) _ _):_) -> 1
            ((P Ref _ _):_) -> 1
            [] -> 0 -- must be locally bound, if it's not an error...
    pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
    pri (PTrue _) = 0
    pri (PFalse _) = 0
    pri (PRefl _ _) = 1
    pri (PEq _ l r) = max 1 (max (pri l) (pri r))
    pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))
    pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
    pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
    pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
    pri (PTyped l r) = pri l
    pri (PPair _ l r) = max 1 (max (pri l) (pri r))
    pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
    pri (PAlternative a as) = maximum (map pri as)
    pri (PConstant _) = 0
    pri Placeholder = 1
    pri _ = 3

addStatics :: Name -> Term -> PTerm -> Idris ()
addStatics n tm ptm =
    do let (statics, dynamics) = initStatics tm ptm
       let stnames = nub $ concatMap freeArgNames (map snd statics)
       let dnames = nub $ concatMap freeArgNames (map snd dynamics)
       -- also get the arguments which are 'uniquely inferrable' from
       -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")
       let statics' = nub $ map fst statics ++
                              filter (\x -> not (elem x dnames)) stnames
       let stpos = staticList statics' tm
       i <- getIState
       when (not (null statics)) $
          logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics
                        ++ "\n" ++ show stnames ++ "\n" ++ show dnames
       putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
       addIBC (IBCStatic n)
  where
    initStatics (Bind n (Pi ty) sc) (PPi p _ _ 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 = ([], [])

    freeArgNames (Bind n (Pi ty) sc) 
          = nub $ freeArgNames ty 
    freeArgNames tm = let (_, args) = unApply tm in
                          concatMap freeNames args

    -- if a name appears in a type class 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 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
        -- if all names in the arguments of addconsts appear in ns,
        -- add the constraint implicitly
        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 "") (sMN 0 "cu")
                         (mkConst c args) (doAdd cs ns t)
             | otherwise = doAdd cs ns t

         mkConst c args = PApp fc (PRef fc c)
                             (map (\n -> PExp 0 [] (PRef fc n) "") 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 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...

implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
implicit syn n ptm = implicit' syn [] n ptm

implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
implicit' syn ignore n ptm
    = do i <- getIState
         let (tm', impdata) = implicitise syn ignore i ptm
--          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'

implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
      let (declimps, ns') = execState (imps True [] tm) ([], [])
          ns = filter (\n -> 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 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 = []

    imps top env (PApp _ f as)
       = do (decls, ns) <- get
            let isn = concatMap (namesIn uvars ist) (map getTm as)
            put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
    imps top env (PPi (Imp l _ doc _) n ty sc)
        = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]
             (decls , ns) <- get
             put (PImp (getPriority ist ty) True l n Placeholder doc : decls,
                  nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
             imps True (n:env) sc
    imps top env (PPi (Exp l _ doc _) n ty sc)
        = do let isn = nub (namesIn uvars ist 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 Placeholder doc : decls,
                  nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
             imps True (n:env) sc
    imps top env (PPi (Constraint l _ doc) n ty sc)
        = do let isn = nub (namesIn uvars ist ty ++ case sc of
                            (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
                            _ -> [])
             (decls, ns) <- get -- ignore decls in HO types
             put (PConstraint 10 l Placeholder doc : decls,
                  nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
             imps True (n:env) sc
    imps top env (PPi (TacImp l _ scr doc) n ty sc)
        = do let isn = nub (namesIn uvars ist 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 doc : decls,
                  nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
             imps True (n:env) sc
    imps top env (PEq _ 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 (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 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 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 _               = return ()

    pibind using []     sc = sc
    pibind using (n:ns) sc
      = case lookup n using of
            Just ty -> PPi (Imp [] Dynamic "" False) n ty (pibind using ns sc)
            Nothing -> PPi (Imp [] Dynamic "" False) n 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

addImpl :: 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] -> IState -> PTerm -> PTerm
addImpl' inpat env infns ist ptm 
         = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)
  where
    ai env ds (PRef fc f)
        | f `elem` infns = PInferRef fc f
        | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []
    ai env ds (PHidden (PRef fc f))
        | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []
    ai env ds (PEq fc l r)   
      = let l' = ai env ds l
            r' = ai env ds r in
            PEq fc l' r'
    ai env ds (PRewrite fc l r g)   
       = let l' = ai env ds l
             r' = ai env ds r
             g' = fmap (ai env ds) g in
         PRewrite fc l' r' g'
    ai env ds (PTyped l r) 
      = let l' = ai env ds l
            r' = ai env ds r in
            PTyped l' r'
    ai env ds (PPair fc l r) 
      = let l' = ai env ds l
            r' = ai env ds r in
            PPair fc l' r'
    ai env ds (PDPair fc l t r)
         = let l' = ai env ds l
               t' = ai env ds t
               r' = ai env ds r in
           PDPair fc l' t' r'
    ai env ds (PAlternative a as) 
           = let as' = map (ai env ds) as in
                 PAlternative a as'
    ai env _ (PDisamb ds' as) = ai env ds' as
    ai env ds (PApp fc (PInferRef _ f) as)
        = let as' = map (fmap (ai env ds)) as in
              PApp fc (PInferRef fc f) as'
    ai env ds (PApp fc ftm@(PRef _ f) as)
        | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)
        | not (f `elem` map fst env)
                          = let as' = map (fmap (ai env ds)) as in
                                handleErr $ aiFn inpat False ist fc f ds as'
        | Just (Just ty) <- lookup f env =
             let as' = map (fmap (ai env ds)) as
                 arity = getPArity ty in
              mkPApp fc arity ftm as'
    ai env ds (PApp fc f as) 
      = let f' = ai env ds f
            as' = map (fmap (ai env ds)) as in
         mkPApp fc 1 f' as'
    ai env ds (PCase fc c os) 
      = let c' = ai env ds c
            os' = map (pmap (ai env ds)) os in
            PCase fc c' os'
    ai env ds (PLam n ty sc) 
      = let ty' = ai env ds ty
            sc' = ai ((n, Just ty):env) ds sc in
            PLam n ty' sc'
    ai env ds (PLet n ty val sc)
      = let ty' = ai env ds ty
            val' = ai env ds val
            sc' = ai ((n, Just ty):env) ds sc in
            PLet n ty' val' sc'
    ai env ds (PPi p n ty sc) 
      = let ty' = ai env ds ty
            sc' = ai ((n, Just ty):env) ds sc in
            PPi p n ty' sc'
    ai env ds (PGoal fc r n sc) 
      = let r' = ai env ds r
            sc' = ai ((n, Nothing):env) ds sc in
            PGoal fc r' n sc'
    ai env ds (PHidden tm) = PHidden (ai env ds tm)
    ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)
    ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)
    ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)
    ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)
    ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)
    ai env ds tm = tm

    handleErr (Left err) = PElabError err
    handleErr (Right x) = x

-- if in a pattern, and there are no arguments, and there's no possible
-- names with zero explicit arguments, don't add implicits.

aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
aiFn inpat True ist fc f ds []
  = case lookupDef f (tt_ctxt ist) of
        [] -> Right $ PPatvar fc f
        alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
                    -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
                    if (not (vname f) || tcname f
                           || any (conCaf (tt_ctxt ist)) ialts)
--                            any constructor alts || any allImp ialts))
                        then aiFn inpat False ist fc f ds [] -- use it as a constructor
                        else Right $ PPatvar fc f
    where imp (PExp _ _ _ _) = False
          imp _ = True
--           allImp [] = False
          allImp xs = all imp xs
          constructor (TyDecl (DCon _ _) _) = True
          constructor _ = False

          conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia

          vname (UN n) = True -- non qualified
          vname _ = False

aiFn inpat expat ist fc f ds as
    | f `elem` primNames = Right $ PApp fc (PRef fc f) as
aiFn inpat expat ist fc f ds as
          -- This is where namespaces get resolved by adding PAlternative
     = do let ns = lookupCtxtName f (idris_implicits ist)
          let nh = filter (\(n, _) -> notHidden n) ns
          let ns' = case trimAlts ds nh of
                         [] -> nh
                         x -> x 
          case ns' of
            [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
            [] -> if f `elem` (map fst (idris_metavars ist))
                    then Right $ PApp fc (PRef fc f) as
                    else Right $ mkPApp fc (length as) (PRef fc f) as
            alts -> Right $
                         PAlternative True $
                           map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
                                                  (insertImpl ns as)) alts
  where
    trimAlts [] alts = alts
    trimAlts ns alts 
        = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

    nspace (NS _ s) = s
    nspace _ = []

    notHidden n = case getAccessibility n of
                        Hidden -> False
                        _ -> True

    getAccessibility n
             = case lookupDefAcc n False (tt_ctxt ist) of
                    [(n,t)] -> t
                    _ -> Public


    insertImpl :: [PArg] -> [PArg] -> [PArg]
    insertImpl (PExp p l ty _ : ps) (PExp _ _ tm d : given) =
                                 PExp p l tm d : insertImpl ps given
    insertImpl (PConstraint p l ty _ : ps) (PConstraint _ _ tm d : given) =
                                 PConstraint p l tm d : insertImpl ps given
    insertImpl (PConstraint p l ty d : ps) given =
                 PConstraint p l (PResolveTC fc) d : insertImpl ps given
    insertImpl (PImp p _ l n ty d : ps) given =
        case find n given [] of
            Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'
            Nothing ->           PImp p True l n Placeholder "" : insertImpl ps given
    insertImpl (PTacImplicit p l n sc' ty d : ps) given =
      let sc = addImpl ist sc' in
        case find n given [] of
            Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'
            Nothing -> if inpat
                          then PTacImplicit p l n sc Placeholder "" : insertImpl ps given
                          else PTacImplicit p l n sc sc "" : insertImpl ps given
    insertImpl expected [] = []
    insertImpl _        given  = given

    find n []               acc = Nothing
    find n (PImp _ _ _ n' t _ : gs) acc
         | n == n' = Just (t, reverse acc ++ gs)
    find n (PTacImplicit _ _ n' _ t _ : gs) acc
         | n == n' = Just (t, reverse acc ++ gs)
    find n (g : gs) acc = find n gs (g : acc)

-- replace non-linear occurrences with _
-- ASSUMPTION: This is called before adding 'alternatives' because otherwise
-- it is hard to get right!

stripLinear :: IState -> PTerm -> PTerm
stripLinear i tm = evalState (sl tm) [] where
    sl :: PTerm -> State [Name] PTerm
    sl (PRef fc f)
         | (_:_) <- lookupTy f (tt_ctxt i)
              = return $ PRef fc f
         | otherwise = do ns <- get
                          if (f `elem` ns)
                             then return Placeholder
                             else do put (f : ns)
                                     return (PRef fc f)
    sl (PPatvar fc f)
                     = do ns <- get
                          if (f `elem` ns)
                             then return Placeholder
                             else do put (f : ns)
                                     return (PPatvar fc f)
    sl (PApp fc fn args) = do fn' <- sl fn
                              args' <- mapM slA args
                              return $ PApp fc fn' args'
       where slA (PImp p m l n t d) = do t' <- sl t
                                         return $ PImp p m l n t' d
             slA (PExp p l t d) = do t' <- sl t
                                     return $ PExp p l t' d
             slA (PConstraint p l t d)
                                = do t' <- sl t
                                     return $ PConstraint p l t' d
             slA (PTacImplicit p l n sc t d)
                                = do t' <- sl t
                                     return $ PTacImplicit p l n sc t' d
    sl x = return x

-- Remove functions which aren't applied to anything, which must then
-- be resolved by unification. Assume names resolved and alternatives
-- filled in (so no ambiguity).

stripUnmatchable :: IState -> PTerm -> PTerm
stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
    su :: PTerm -> PTerm
    su (PRef fc f)
       | (Bind n (Pi t) sc :_) <- lookupTy f (tt_ctxt i) 
          = Placeholder
    su (PApp fc fn args) 
       = PApp fc fn (fmap (fmap su) args)
    su (PAlternative b alts) 
       = let alts' = filter (/= Placeholder) (map su alts) in
             if null alts' then Placeholder
                           else PAlternative b alts'
    su (PPair fc l r) = PPair fc (su l) (su r)
    su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
    su t = t
stripUnmatchable i tm = tm

mkPApp fc a f [] = f
mkPApp fc a f as = let rest = drop a as in
                       appRest fc (PApp fc f (take a as)) rest
  where
    appRest fc f [] = f
    appRest fc f (a : as) = appRest fc (PApp fc f [a]) as

-- Find 'static' argument positions
-- (the declared ones, plus any names in argument position in the declared
-- statics)
-- FIXME: It's possible that this really has to happen after elaboration

findStatics :: IState -> PTerm -> (PTerm, [Bool])
findStatics ist tm = trace (show tm) $
                      let (ns, ss) = fs tm in
                         runState (pos ns ss tm) []
  where fs (PPi p n t sc)
            | Static <- pstatic p
                        = let (ns, ss) = fs sc in
                              (namesIn [] ist t : ns, n : ss)
            | otherwise = let (ns, ss) = fs sc in
                              (ns, ss)
        fs _ = ([], [])

        inOne n ns = length (filter id (map (elem n) ns)) == 1

        pos ns ss (PPi p n t sc)
            | elem n ss = do sc' <- pos ns ss sc
                             spos <- get
                             put (True : spos)
                             return (PPi (p { pstatic = Static }) n t sc')
            | otherwise = do sc' <- pos ns ss sc
                             spos <- get
                             put (False : spos)
                             return (PPi p n t sc')
        pos ns ss t = return t

-- for 6.12/7 compatibility
data EitherErr a b = LeftErr a | RightOK b

instance Monad (EitherErr a) where
    return = RightOK

    (LeftErr e) >>= k = LeftErr e
    RightOK v   >>= k = k v

toEither (LeftErr e)  = Left e
toEither (RightOK ho) = Right ho

-- syntactic match of a against b, returning pair of variables in a
-- and what they match. Returns the pair that failed if not a match.

matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause = matchClause' False

matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
    matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))

    fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
    fullApp x = x

    match' x y = match (fullApp x) (fullApp y)
    match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'
        | fi == txt "fromInteger" && b == txt "builtins",
          PConstant (I _) <- getTm x = match (getTm x) x'
    match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])
        | fi == txt "fromInteger" && b == txt "builtins",
          PConstant (I _) <- getTm x = match (getTm x) x'
    match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'
    match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')
    match (PApp _ f args) (PApp _ f' args')
        | length args == length args'
            = do mf <- match' f f'
                 ms <- zipWithM matchArg args args'
                 return (mf ++ concat ms)
--     match (PRef _ n) (PRef _ n') | n == n' = return []
--                                  | otherwise = Nothing
    match (PRef f n) (PApp _ x []) = match (PRef f n) x
    match (PPatvar f n) xr = match (PRef f n) xr
    match xr (PPatvar f n) = match xr (PRef f n)
    match (PApp _ x []) (PRef f n) = match x (PRef f n)
    match (PRef _ n) tm@(PRef _ n')
        | n == n' && not names &&
          (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i)) 
                || tm == Placeholder)
            = return [(n, tm)]
        | n == n' = return []
    match (PRef _ n) tm
        | not names && (not (isConName n (tt_ctxt i) ||
                             isFnName n (tt_ctxt i)) || tm == Placeholder)
            = return [(n, tm)]
    match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
                                         mr <- match' r r'
                                         return (ml ++ mr)
    match (PRewrite _ l r _) (PRewrite _ l' r' _)
                                    = do ml <- match' l l'
                                         mr <- match' r r'
                                         return (ml ++ mr)
    match (PTyped l r) (PTyped l' r') = do ml <- match l l'
                                           mr <- match r r'
                                           return (ml ++ mr)
    match (PTyped l r) x = match l x
    match x (PTyped l r) = match x l
    match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
                                             mr <- match' r r'
                                             return (ml ++ mr)
    match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
                                                    mt <- match' t t'
                                                    mr <- match' r r'
                                                    return (ml ++ mt ++ mr)
    match (PAlternative a as) (PAlternative a' as')
        = do ms <- zipWithM match' as as'
             return (concat ms)
    match a@(PAlternative _ as) b
        = do let ms = zipWith match' as (repeat b)
             case (rights (map toEither ms)) of
                (x: _) -> return x
                _ -> LeftErr (a, b)
    match (PCase _ _ _) _ = return [] -- lifted out
    match (PMetavar _) _ = return [] -- modified
    match (PInferRef _ _) _ = return [] -- modified
    match (PQuote _) _ = return []
    match (PProof _) _ = return []
    match (PTactics _) _ = return []
    match (PRefl _ _) (PRefl _ _) = return []
    match (PResolveTC _) (PResolveTC _) = return []
    match (PTrue _) (PTrue _) = return []
    match (PFalse _) (PFalse _) = return []
    match (PReturn _) (PReturn _) = return []
    match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
                                             ms <- match' s s'
                                             return (mt ++ ms)
    match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'
                                           ms <- match' s s'
                                           return (mt ++ ms)
    match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'
                                                  mty <- match' ty ty'
                                                  ms <- match' s s'
                                                  return (mt ++ mty ++ ms)
    match (PHidden x) (PHidden y) = match' x y
    match (PUnifyLog x) y = match' x y
    match x (PUnifyLog y) = match' x y
    match (PNoImplicits x) y = match' x y
    match x (PNoImplicits y) = match' x y
    match Placeholder _ = return []
    match _ Placeholder = return []
    match (PResolveTC _) _ = return []
    match a b | a == b = return []
              | otherwise = LeftErr (a, b)

    checkRpts (RightOK ms) = check ms where
        check ((n,t):xs)
            | Just t' <- lookup n xs = if t/=t' && t/=Placeholder && t'/=Placeholder
                                                then Left (t, t')
                                                else check xs
        check (_:xs) = check xs
        check [] = Right ms
    checkRpts (LeftErr x) = Left x

substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
substMatches ms = substMatchesShadow ms []

substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
substMatchesShadow [] shs t = t
substMatchesShadow ((n,tm):ns) shs t
   = substMatchShadow n shs tm (substMatchesShadow ns shs t)

substMatch :: Name -> PTerm -> PTerm -> PTerm
substMatch n = substMatchShadow n []

substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
substMatchShadow n shs tm t = sm shs t where
    sm xs (PRef _ n') | n == n' = tm
    sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)
    sm xs (PPi p x t sc)
         | x `elem` xs
             = let x' = nextName x in
                   PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
                            (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
         | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
    sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
    sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
    sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)
    sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
                                           (fmap (sm xs) tm)
    sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
    sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
    sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
    sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
    sm xs (PHidden x) = PHidden (sm xs x)
    sm xs (PUnifyLog x) = PUnifyLog (sm xs x)
    sm xs (PNoImplicits x) = PNoImplicits (sm xs x)
    sm xs x = x

    fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
    fullApp x = x

shadow :: Name -> Name -> PTerm -> PTerm
shadow n n' t = sm t where
    sm (PRef fc x) | n == x = PRef fc n'
    sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)
    sm (PPi p x t sc) | n /=x = PPi p x (sm t) (sm sc)
    sm (PLet x t v sc) | n /= x = PLet x (sm t) (sm v) (sm sc)
    sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)
    sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)
    sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)
    sm (PEq f x y) = PEq f (sm x) (sm y)
    sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
    sm (PTyped x y) = PTyped (sm x) (sm y)
    sm (PPair f x y) = PPair f (sm x) (sm y)
    sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
    sm (PAlternative a as) = PAlternative a (map sm as)
    sm (PTactics ts) = PTactics (map (fmap sm) ts)
    sm (PProof ts) = PProof (map (fmap sm) ts)
    sm (PHidden x) = PHidden (sm x)
    sm (PUnifyLog x) = PUnifyLog (sm x)
    sm (PNoImplicits x) = PNoImplicits (sm x)
    sm x = x

-- Rename any binders which are repeated (so that we don't have to mess
-- about with shadowing anywhere else).

mkUniqueNames :: [Name] -> PTerm -> PTerm
mkUniqueNames env tm = evalState (mkUniq tm) env where
  inScope = boundNamesIn tm

  mkUniqA arg = do t' <- mkUniq (getTm arg)
                   return (arg { getTm = t' })

  -- FIXME: Probably ought to do this for completeness! It's fine as
  -- long as there are no bindings inside tactics though.
  mkUniqT tac = return tac 

  mkUniq :: PTerm -> State [Name] PTerm
  mkUniq (PLam n ty sc)
         = do env <- get
              (n', sc') <- 
                    if n `elem` env 
                       then do let n' = uniqueName n (env ++ inScope)
                               return (n', shadow n n' sc)
                       else return (n, sc)
              put (n' : env)
              ty' <- mkUniq ty
              sc'' <- mkUniq sc'
              return $! PLam n' ty' sc''
  mkUniq (PPi p n ty sc)
         = do env <- get
              (n', sc') <- 
                    if n `elem` env 
                       then do let n' = uniqueName n (env ++ inScope)
                               return (n', shadow n n' sc)
                       else return (n, sc)
              put (n' : env)
              ty' <- mkUniq ty
              sc'' <- mkUniq sc'
              return $! PPi p n' ty' sc''
  mkUniq (PLet n ty val sc)
         = do env <- get
              (n', sc') <- 
                    if n `elem` env 
                       then do let n' = uniqueName n (env ++ inScope)
                               return (n', shadow n n' sc)
                       else return (n, sc)
              put (n' : env)
              ty' <- mkUniq ty; val' <- mkUniq val
              sc'' <- mkUniq sc'
              return $! PLet n' ty' val' sc''
  mkUniq (PApp fc t args) 
         = do t' <- mkUniq t
              args' <- mapM mkUniqA args
              return $! PApp fc t' args'
  mkUniq (PAppBind fc t args) 
         = do t' <- mkUniq t
              args' <- mapM mkUniqA args
              return $! PAppBind fc t' args'
  mkUniq (PCase fc t alts) 
         = do t' <- mkUniq t
              alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
                                         return (x', y')) alts
              return $! PCase fc t' alts'
  mkUniq (PPair fc l r) 
         = do l' <- mkUniq l; r' <- mkUniq r
              return $! PPair fc l' r'                                                      
  mkUniq (PDPair fc l t r) 
         = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
              return $! PDPair fc l' t' r'                                                      
  mkUniq (PAlternative b as) 
         = liftM (PAlternative b) (mapM mkUniq as)
  mkUniq (PHidden t) = liftM PHidden (mkUniq t)
  mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)
  mkUniq (PDisamb n t) = liftM (PDisamb n) (mkUniq t)
  mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
  mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
  mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
  mkUniq t = return t


