{-# LANGUAGE PatternGuards #-}

module Idris.ElabTerm where

import Idris.AbsSyntax
import Idris.DSL
import Idris.Delaborate
import Idris.Error
import Idris.ProofSearch
import Idris.Output (pshow)

import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Core.Unify
import Idris.Core.Typecheck (check)
import Idris.ErrReverse (errReverse)

import Control.Applicative ((<$>))
import Control.Monad
import Control.Monad.State.Strict
import Data.List
import qualified Data.Map as M
import Data.Maybe (mapMaybe, fromMaybe)
import qualified Data.Set as S
import qualified Data.Text as T

import Debug.Trace

-- Data to pass to recursively called elaborators; e.g. for where blocks,
-- paramaterised declarations, etc.

data ElabInfo = EInfo { params :: [(Name, PTerm)],
                        inblock :: Ctxt [Name], -- names in the block, and their params
                        liftname :: Name -> Name,
                        namespace :: Maybe [String] }

toplevel = EInfo [] emptyContext id Nothing

-- Using the elaborator, convert a term in raw syntax to a fully
-- elaborated, typechecked term.
--
-- If building a pattern match, we convert undeclared variables from
-- holes to pattern bindings.

-- Also find deferred names in the term and their types

build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
         ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
build ist info pattern opts fn tm
    = do elab ist info pattern opts fn tm
         let tmIn = tm
         let inf = case lookupCtxt fn (idris_tyinfodata ist) of
                        [TIPartial] -> True
                        _ -> False
         ivs <- get_instances
         hs <- get_holes
         ptm <- get_term
         -- Resolve remaining type classes. Two passes - first to get the
         -- default Num instances, second to clean up the rest
         when (not pattern) $
              mapM_ (\n -> when (n `elem` hs) $
                             do focus n
                                g <- goal
                                try (resolveTC 7 g fn ist)
                                    (movelast n)) ivs
         ivs <- get_instances
         hs <- get_holes
         when (not pattern) $
              mapM_ (\n -> when (n `elem` hs) $
                             do focus n
                                g <- goal
                                resolveTC 7 g fn ist) ivs
         tm <- get_term
         ctxt <- get_context
         probs <- get_probs
         u <- getUnifyLog

         when (not pattern) $ 
           traceWhen u ("Remaining problems:\n" ++ show probs) $ 
             do matchProblems True; unifyProblems
         probs <- get_probs
         case probs of
            [] -> return ()
            ((_,_,_,e,_,_):es) -> if inf then return ()
                                         else lift (Error e)
         is <- getAux
         tt <- get_term
         let (tm, ds) = runState (collectDeferred (Just fn) tt) []
         log <- getLog
         if (log /= "") then trace log $ return (tm, ds, is)
            else return (tm, ds, is)

-- Build a term autogenerated as a typeclass method definition
-- (Separate, so we don't go overboard resolving things that we don't
-- know about yet on the LHS of a pattern def)

buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
         ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
buildTC ist info pattern opts fn tm
    = do -- set name supply to begin after highest index in tm
         let ns = allNamesIn tm
         let tmIn = tm
         let inf = case lookupCtxt fn (idris_tyinfodata ist) of
                        [TIPartial] -> True
                        _ -> False
         initNextNameFrom ns
         elab ist info pattern opts fn tm
         probs <- get_probs
         tm <- get_term
         case probs of
            [] -> return ()
            ((_,_,_,e,_,_):es) -> if inf then return ()
                                         else lift (Error e)
         is <- getAux
         tt <- get_term
         let (tm, ds) = runState (collectDeferred (Just fn) tt) []
         log <- getLog
         if (log /= "") then trace log $ return (tm, ds, is)
            else return (tm, ds, is)

-- Returns the set of declarations we need to add to complete the definition
-- (most likely case blocks to elaborate)

elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->
        ElabD ()
elab ist info pattern opts fn tm
    = do let loglvl = opt_logLevel (idris_options ist)
         when (loglvl > 5) $ unifyLog True
         compute -- expand type synonyms, etc
         elabE (False, False, False) tm -- (in argument, guarded, in type)
         end_unify
         when pattern -- convert remaining holes to pattern vars
              (do update_term orderPats
                  matchProblems False -- only the ones we matched earlier
                  unifyProblems
                  mkPat)
  where
    tcgen = Dictionary `elem` opts
    reflect = Reflection `elem` opts

    isph arg = case getTm arg of
        Placeholder -> (True, priority arg)
        _ -> (False, priority arg)

    toElab ina arg = case getTm arg of
        Placeholder -> Nothing
        v -> Just (priority arg, elabE ina v)

    toElab' ina arg = case getTm arg of
        Placeholder -> Nothing
        v -> Just (elabE ina v)

    mkPat = do hs <- get_holes
               tm <- get_term
               case hs of
                  (h: hs) -> do patvar h; mkPat
                  [] -> return ()

    elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
    elabE ina t = 
               --do g <- goal
                  --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
                  do ct <- insertCoerce ina t
                     t' <- insertLazy ct
                     g <- goal
                     tm <- get_term
                     ps <- get_probs
                     hs <- get_holes
                     --trace ("Elaborating " ++ show t' ++ " in " ++ show g
                     --         ++ "\n" ++ show tm
                     --         ++ "\nholes " ++ show hs
                     --         ++ "\nproblems " ++ show ps
                     --         ++ "\n-----------\n") $
                     --trace ("ELAB " ++ show t') $ 
                     let fc = fileFC "Force"
                     env <- get_env
                     handleError (forceErr env)
                         (elab' ina t')
                         (elab' ina (PApp fc (PRef fc (sUN "Force"))
                                       [pimp (sUN "t") Placeholder True,
                                        pimp (sUN "a") Placeholder True, 
                                        pexp ct])) True

    forceErr env (CantUnify _ t t' _ _ _)
       | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
            ht == txt "Lazy'" = True
    forceErr env (CantUnify _ t t' _ _ _)
       | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
            ht == txt "Lazy'" = True
    forceErr env (InfiniteUnify _ t _)
       | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
            ht == txt "Lazy'" = True
    forceErr env (Elaborating _ _ t) = forceErr env t
    forceErr env (ElaboratingArg _ _ _ t) = forceErr env t
    forceErr env (At _ t) = forceErr env t
    forceErr env t = False

    local f = do e <- get_env
                 return (f `elem` map fst e)

    -- | Is a constant a type?
    constType :: Const -> Bool
    constType (AType _) = True
    constType StrType = True
    constType PtrType = True
    constType VoidType = True
    constType _ = False

    elab' :: (Bool, Bool, Bool)  -- ^ (in an argument, guarded, in a type)
          -> PTerm -- ^ The term to elaborate
          -> ElabD ()
    elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
    elab' ina PType           = do apply RType []; solve
--  elab' (_,_,inty) (PConstant c) 
--     | constType c && pattern && not reflect && not inty
--       = lift $ tfail (Msg "Typecase is not allowed") 
    elab' ina (PConstant c)  = do apply (RConstant c) []; solve
    elab' ina (PQuote r)     = do fill r; solve
    elab' ina (PTrue fc _)   = try (elab' ina (PRef fc unitCon))
                                    (elab' ina (PRef fc unitTy))
    elab' ina (PFalse fc)    = elab' ina (PRef fc falseTy)
    elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
       = do g <- goal; resolveTC 5 g fn ist
    elab' ina (PResolveTC fc)
        | True = do c <- getNameFrom (sMN 0 "class")
                    instanceArg c
        | otherwise = do g <- goal
                         try (resolveTC 2 g fn ist)
                          (do c <- getNameFrom (sMN 0 "class")
                              instanceArg c)
    elab' ina (PRefl fc t)
        = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
                                              pimp (sMN 0 "x") t False])
    elab' ina (PEq fc l r)   = elab' ina (PApp fc (PRef fc eqTy)
                                    [pimp (sMN 0 "A") Placeholder True,
                                     pimp (sMN 0 "B") Placeholder False,
                                     pexp l, pexp r])
    elab' ina@(_, a, inty) (PPair fc _ l r)
        = do hnf_compute
             g <- goal
             case g of
                TType _ -> elabE (True, a,inty) (PApp fc (PRef fc pairTy)
                                                  [pexp l,pexp r])
                _ -> elabE (True, a, inty) (PApp fc (PRef fc pairCon)
                                            [pimp (sMN 0 "A") Placeholder True,
                                             pimp (sMN 0 "B") Placeholder True,
                                             pexp l, pexp r])
    elab' ina (PDPair fc p l@(PRef _ n) t r)
            = case t of
                Placeholder ->
                   do hnf_compute
                      g <- goal
                      case g of
                         TType _ -> asType
                         _ -> asValue
                _ -> asType
         where asType = elab' ina (PApp fc (PRef fc sigmaTy)
                                        [pexp t,
                                         pexp (PLam n Placeholder r)])
               asValue = elab' ina (PApp fc (PRef fc existsCon)
                                         [pimp (sMN 0 "a") t False,
                                          pimp (sMN 0 "P") Placeholder True,
                                          pexp l, pexp r])
    elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon)
                                              [pimp (sMN 0 "a") t False,
                                               pimp (sMN 0 "P") Placeholder True,
                                               pexp l, pexp r])
    elab' ina (PAlternative True as)
        = do hnf_compute
             ty <- goal
             ctxt <- get_context
             let (tc, _) = unApply ty
             let as' = pruneByType tc ctxt as
--              trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $
             tryAll (zip (map (elab' ina) as') (map showHd as'))
        where showHd (PApp _ (PRef _ n) _) = show n
              showHd (PRef _ n) = show n
              showHd (PApp _ h _) = show h
              showHd x = show x
    elab' ina (PAlternative False as)
        = trySeq as
        where -- if none work, take the error from the first
              trySeq (x : xs) = let e1 = elab' ina x in
                                    try' e1 (trySeq' e1 xs) True
              trySeq' deferr [] = proofFail deferr
              trySeq' deferr (x : xs)
                  = try' (elab' ina x) (trySeq' deferr xs) True
    elab' ina (PPatvar fc n) | pattern = patvar n
--    elab' (_, _, inty) (PRef fc f)
--       | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
--          = lift $ tfail (Msg "Typecase is not allowed") 
    elab' (ina, guarded, inty) (PRef fc n) | pattern && not (inparamBlock n)
        = do ctxt <- get_context
             let defined = case lookupTy n ctxt of
                               [] -> False
                               _ -> True
           -- this is to stop us resolve type classes recursively
             -- trace (show (n, guarded)) $
             if (tcname n && ina) then erun fc $ patvar n
               else if (defined && not guarded)
                       then do apply (Var n) []; solve
                       else try (do apply (Var n) []; solve)
                                (patvar n)
      where inparamBlock n = case lookupCtxtName n (inblock info) of
                                [] -> False
                                _ -> True
    elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
    elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
    elab' ina@(_, a, inty) (PLam n Placeholder sc)
          = do -- if n is a type constructor name, this makes no sense...
               ctxt <- get_context
               when (isTConName n ctxt) $
                    lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")  
               checkPiGoal n
               attack; intro (Just n);
               -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
               elabE (True, a, inty) sc; solve
    elab' ina@(_, a, inty) (PLam n ty sc)
          = do tyn <- getNameFrom (sMN 0 "lamty")
               -- if n is a type constructor name, this makes no sense...
               ctxt <- get_context
               when (isTConName n ctxt) $
                    lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")  
               checkPiGoal n
               claim tyn RType
               explicit tyn
               attack
               ptm <- get_term
               hs <- get_holes
               introTy (Var tyn) (Just n)
               focus tyn
               elabE (True, a, True) ty
               elabE (True, a, inty) sc
               solve
    elab' ina@(_, a, _) (PPi _ n Placeholder sc)
          = do attack; arg n (sMN 0 "ty"); elabE (True, a, True) sc; solve
    elab' ina@(_, a, _) (PPi _ n ty sc)
          = do attack; tyn <- getNameFrom (sMN 0 "ty")
               claim tyn RType
               n' <- case n of
                        MN _ _ -> unique_hole n
                        _ -> return n
               forall n' (Var tyn)
               focus tyn
               elabE (True, a, True) ty
               elabE (True, a, True) sc
               solve
    elab' ina@(_, a, inty) (PLet n ty val sc)
          = do attack;
               tyn <- getNameFrom (sMN 0 "letty")
               claim tyn RType
               valn <- getNameFrom (sMN 0 "letval")
               claim valn (Var tyn)
               explicit valn
               letbind n (Var tyn) (Var valn)
               case ty of
                   Placeholder -> return ()
                   _ -> do focus tyn
                           explicit tyn
                           elabE (True, a, True) ty
               focus valn
               elabE (True, a, True) val
               env <- get_env
               elabE (True, a, inty) sc
               -- HACK: If the name leaks into its type, it may leak out of
               -- scope outside, so substitute in the outer scope.
               expandLet n (case lookup n env of
                                 Just (Let t v) -> v)
               solve
    elab' ina@(_, a, inty) (PGoal fc r n sc) = do
         rty <- goal
         attack
         tyn <- getNameFrom (sMN 0 "letty")
         claim tyn RType
         valn <- getNameFrom (sMN 0 "letval")
         claim valn (Var tyn)
         letbind n (Var tyn) (Var valn)
         focus valn
         elabE (True, a, True) (PApp fc r [pexp (delab ist rty)])
         env <- get_env
         computeLet n
         elabE (True, a, inty) sc
         solve
--          elab' ina (PLet n Placeholder
--              (PApp fc r [pexp (delab ist rty)]) sc)
    elab' ina tm@(PApp fc (PInferRef _ f) args) = do
         rty <- goal
         ds <- get_deferred
         ctxt <- get_context
         -- make a function type a -> b -> c -> ... -> rty for the
         -- new function name
         env <- get_env
         argTys <- claimArgTys env args
         fn <- getNameFrom (sMN 0 "inf_fn")
         let fty = fnTy argTys rty
--             trace (show (ptm, map fst argTys)) $ focus fn
            -- build and defer the function application
         attack; deferType (mkN f) fty (map fst argTys); solve
         -- elaborate the arguments, to unify their types. They all have to
         -- be explicit.
         mapM_ elabIArg (zip argTys args)
       where claimArgTys env [] = return []
             claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)
                                  = do nty <- get_type (Var n)
                                       ans <- claimArgTys env xs
                                       return ((n, (False, forget nty)) : ans)
             claimArgTys env (_ : xs)
                                  = do an <- getNameFrom (sMN 0 "inf_argTy")
                                       aval <- getNameFrom (sMN 0 "inf_arg")
                                       claim an RType
                                       claim aval (Var an)
                                       ans <- claimArgTys env xs
                                       return ((aval, (True, (Var an))) : ans)
             fnTy [] ret  = forget ret
             fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi xt) (fnTy xs ret)

             localVar env (PRef _ x)
                           = case lookup x env of
                                  Just _ -> Just x
                                  _ -> Nothing
             localVar env _ = Nothing

             elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)
             elabIArg _ = return () -- already done, just a name

             mkN n@(NS _ _) = n
             mkN n@(SN _) = n
             mkN n = case namespace info of
                        Just xs@(_:_) -> sNS n xs
                        _ -> n

    elab' ina (PMatchApp fc fn)
       = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
                             [(n, args)] -> return (n, map (const True) args)
                             _ -> lift $ tfail (NoSuchVariable fn)
            ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
            solve
    elab' (_, _, inty) (PApp fc (PRef _ f) args')
       | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty
          = lift $ tfail (Msg "Typecase is not allowed")
    -- if f is local, just do a simple_app
    elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)
       = do env <- get_env
            if (f `elem` map fst env && length args == 1)
               then -- simple app, as below
                    do simple_app (elabE (ina, g, inty) (PRef fc f))
                                  (elabE (True, g, inty) (getTm (head args)))
                                  (show tm)
                       solve
               else
                 do ivs <- get_instances
                    ps <- get_probs
                    -- HACK: we shouldn't resolve type classes if we're defining an instance
                    -- function or default definition.
                    let isinf = f == inferCon || tcname f
                    -- if f is a type class, we need to know its arguments so that
                    -- we can unify with them
                    case lookupCtxt f (idris_classes ist) of
                        [] -> return ()
                        _ -> mapM_ setInjective (map getTm args)
                    ctxt <- get_context
                    let guarded = isConName f ctxt
--                    trace ("args is " ++ show args) $ return ()
                    ns <- apply (Var f) (map isph args)
--                    trace ("ns is " ++ show ns) $ return ()
                    -- mark any type class arguments as injective
                    mapM_ checkIfInjective (map snd ns)
                    unifyProblems -- try again with the new information,
                                  -- to help with disambiguation
                    -- Sort so that the implicit tactics and alternatives go last
                    let (ns', eargs) = unzip $
                             sortBy cmpArg (zip ns args)
                    elabArgs ist (ina || not isinf, guarded, inty)
                           [] fc False f ns' 
                             (f == sUN "Force")
                             (map (\x -> (lazyarg x, getTm x)) eargs)
                    solve
                    ivs' <- get_instances
                    -- Attempt to resolve any type classes which have 'complete' types,
                    -- i.e. no holes in them
                    when (not pattern || (ina && not tcgen && not guarded)) $
                        mapM_ (\n -> do focus n
                                        g <- goal
                                        env <- get_env
                                        hs <- get_holes
                                        if all (\n -> not (n `elem` hs)) (freeNames g)
                                        -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
                                         then try (resolveTC 7 g fn ist)
                                                  (movelast n)
                                         else movelast n)
                              (ivs' \\ ivs)
      where -- normal < alternatives < lambdas < rewrites < tactic < default tactic
            -- reason for lambdas after alternatives is that having 
            -- the alternative resolved can help with typechecking the lambda
            -- or the rewrite. Rewrites/tactics need as much information
            -- as possible about the type.
            -- FIXME: Better would be to allow alternative resolution to be
            -- retried after more information is in.
            cmpArg (_, x) (_, y)
                   = compare (conDepth 0 (getTm x) + priority x + alt x) 
                             (conDepth 0 (getTm y) + priority y + alt y)
                where alt t = case getTm t of
                                   PAlternative False _ -> 5
                                   PAlternative True _ -> 1
                                   PLam _ _ _ -> 2
                                   PRewrite _ _ _ _ -> 3
                                   _ -> 0

            -- Score a point for every level where there is a non-constructor
            -- function (so higher score --> done later)
            -- Only relevant when on lhs
            conDepth d t | not pattern = 0
            conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0
                                  | otherwise = max (100 - d) 1
            conDepth d (PApp _ f as) 
               = conDepth d f + sum (map (conDepth (d+1)) (map getTm as))
            conDepth d (PPatvar _ _) = 0
            conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
            conDepth d Placeholder = 0
            conDepth d t = max (100 - d) 1

            checkIfInjective n = do
                env <- get_env
                case lookup n env of
                     Nothing -> return ()
                     Just b ->
                       case unApply (binderTy b) of
                            (P _ c _, args) -> 
                                case lookupCtxt c (idris_classes ist) of
                                   [] -> return ()
                                   _ -> -- type class, set as injective
                                        mapM_ setinjArg args
                            _ -> return ()
                     
            setinjArg (P _ n _) = setinj n
            setinjArg _ = return ()

            tacTm (PTactics _) = True
            tacTm (PProof _) = True
            tacTm _ = False

            setInjective (PRef _ n) = setinj n
            setInjective (PApp _ (PRef _ n) _) = setinj n
            setInjective _ = return ()

    elab' ina@(_, a, inty) tm@(PApp fc f [arg])
          = erun fc $
             do simple_app (elabE ina f) (elabE (True, a, inty) (getTm arg))
                           (show tm)
                solve
    elab' ina Placeholder = do (h : hs) <- get_holes
                               movelast h
    elab' ina (PMetavar n) = let n' = mkN n in
                                 do attack; defer n'; solve
        where mkN n@(NS _ _) = n
              mkN n = case namespace info of
                        Just xs@(_:_) -> sNS n xs
                        _ -> n
    elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts
    elab' ina (PTactics ts)
        | not pattern = do mapM_ (runTac False ist fn) ts
        | otherwise = elab' ina Placeholder
    elab' ina (PElabError e) = fail (pshow ist e)
    elab' ina (PRewrite fc r sc newg)
        = do attack
             tyn <- getNameFrom (sMN 0 "rty")
             claim tyn RType
             valn <- getNameFrom (sMN 0 "rval")
             claim valn (Var tyn)
             letn <- getNameFrom (sMN 0 "rewrite_rule")
             letbind letn (Var tyn) (Var valn)
             focus valn
             elab' ina r
             compute
             g <- goal
             rewrite (Var letn)
             g' <- goal
             when (g == g') $ lift $ tfail (NoRewriting g)
             case newg of
                 Nothing -> elab' ina sc
                 Just t -> doEquiv t sc
             solve
        where doEquiv t sc =
                do attack
                   tyn <- getNameFrom (sMN 0 "ety")
                   claim tyn RType
                   valn <- getNameFrom (sMN 0 "eqval")
                   claim valn (Var tyn)
                   letn <- getNameFrom (sMN 0 "equiv_val")
                   letbind letn (Var tyn) (Var valn)
                   focus tyn
                   elab' ina t
                   focus valn
                   elab' ina sc
                   elab' ina (PRef fc letn)
                   solve
    elab' ina@(_, a, inty) c@(PCase fc scr opts)
        = do attack
             tyn <- getNameFrom (sMN 0 "scty")
             claim tyn RType
             valn <- getNameFrom (sMN 0 "scval")
             scvn <- getNameFrom (sMN 0 "scvar")
             claim valn (Var tyn)
             letbind scvn (Var tyn) (Var valn)
             focus valn
             elabE (True, a, inty) scr
             args <- get_env
             cname <- unique_hole' True (mkCaseName fn)
             let cname' = mkN cname
             elab' ina (PMetavar cname')
             -- if the scrutinee is one of the 'args' in env, we should
             -- inspect it directly, rather than adding it as a new argument
             let newdef = PClauses fc [] cname'
                             (caseBlock fc cname'
                                (map (isScr scr) (reverse args)) opts)
             -- elaborate case
             env <- get_env
             updateAux (newdef : )
             -- if we haven't got the type yet, hopefully we'll get it later!
             movelast tyn
             solve
        where mkCaseName (NS n ns) = NS (mkCaseName n) ns
              mkCaseName n = SN (CaseN n)
--               mkCaseName (UN x) = UN (x ++ "_case")
--               mkCaseName (MN i x) = MN i (x ++ "_case")
              mkN n@(NS _ _) = n
              mkN n = case namespace info of
                        Just xs@(_:_) -> sNS n xs
                        _ -> n
    elab' ina (PUnifyLog t) = do unifyLog True
                                 elab' ina t
                                 unifyLog False
    elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

    isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
    isScr (PRef _ n) (n', b) = (n', (n == n', b))
    isScr _ (n', b) = (n', (False, b))

    caseBlock :: FC -> Name -> 
                 [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
    caseBlock fc n env opts
        = let args' = findScr env
              args = map mkarg (map getNmScr args') in
              map (mkClause args) opts

       where -- Find the variable we want as the scrutinee and mark it as
             -- 'True'. If the scrutinee is in the environment, match on that
             -- otherwise match on the new argument we're adding.
             findScr ((n, (True, t)) : xs) 
                        = (n, (True, t)) : scrName n xs
             findScr [(n, (_, t))] = [(n, (True, t))] 
             findScr (x : xs) = x : findScr xs
             -- [] can't happen since scrutinee is in the environment!
             
             -- To make sure top level pattern name remains in scope, put
             -- it at the end of the environment
             scrName n []  = []
             scrName n [(_, t)] = [(n, t)]
             scrName n (x : xs) = x : scrName n xs

             getNmScr (n, (s, _)) = (n, s)

             mkarg (n, s) = (PRef fc n, s)
             -- may be shadowed names in the new pattern - so replace the
             -- old ones with an _
             mkClause args (l, r)
                   = let args' = map (shadowed (allNamesIn l)) args
                         lhs = PApp (getFC fc l) (PRef (getFC fc l) n)
                                 (map (mkLHSarg l) args') in
                            PClause (getFC fc l) n lhs [] r []

             mkLHSarg l (tm, True) = pexp l
             mkLHSarg l (tm, False) = pexp tm

             shadowed new (PRef _ n, s) | n `elem` new = (Placeholder, s)
             shadowed new t = t

    getFC d (PApp fc _ _) = fc
    getFC d (PRef fc _) = fc
    getFC d (PAlternative _ (x:_)) = getFC d x
    getFC d x = d

    insertLazy :: PTerm -> ElabD PTerm
    insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t
    insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t
    insertLazy (PCoerced t) = return t
    insertLazy t =
        do ty <- goal
           env <- get_env
           let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
           let tries = if pattern then [t, mkDelay t] else [mkDelay t, t]
           case tyh of
                P _ (UN l) _ | l == txt "Lazy'"
                    -> return (PAlternative False tries)
                _ -> return t
      where
        mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)
        mkDelay t = let fc = fileFC "Delay" in
                        addImpl ist (PApp fc (PRef fc (sUN "Delay")) 
                                          [pexp t])

    insertCoerce ina t =
        do ty <- goal
           -- Check for possible coercions to get to the goal
           -- and add them as 'alternatives'
           env <- get_env
           let ty' = normalise (tt_ctxt ist) env ty
           let cs = getCoercionsTo ist ty'
           let t' = case (t, cs) of
                         (PCoerced tm, _) -> tm
                         (_, []) -> t
                         (_, cs) -> PAlternative False [t ,
                                       PAlternative True (map (mkCoerce t) cs)]
           return t'
       where
         mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!
                            addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

    -- | Elaborate the arguments to a function
    elabArgs :: IState -- ^ The current Idris state
             -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
             -> [Bool]
             -> FC -- ^ Source location
             -> Bool
             -> Name -- ^ Name of the function being applied
             -> [(Name, Name)] -- ^ (Argument Name, Hole Name)
             -> Bool -- ^ under a 'force'
             -> [(Bool, PTerm)] -- ^ (Laziness, argument)
             -> ElabD ()
    elabArgs ist ina failed fc retry f [] force _ = return ()
    elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)
        = elabArgs ist ina failed fc r f ns force args
    elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)
        | lazy && not pattern
          = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))
                                           [pimp (sUN "a") Placeholder True,
                                            pexp t])
        | otherwise = elabArg argName holeName t
      where elabArg argName holeName t =
              do now_elaborating fc f argName
                 wrapErr f argName $ do
                   hs <- get_holes
                   tm <- get_term
                   -- No coercing under an explicit Force (or it can Force/Delay
                   -- recursively!)
                   let elab = if force then elab' else elabE
                   failed' <- -- trace (show (n, t, hs, tm)) $
                              -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
                              case holeName `elem` hs of
                                True -> do focus holeName; elab ina t; return failed
                                False -> return failed
                   done_elaborating_arg f argName
                   elabArgs ist ina failed fc r f ns force args
            wrapErr f argName action =
              do elabState <- get
                 while <- elaborating_app
                 let while' = map (\(x, y, z)-> (y, z)) while
                 (result, newState) <- case runStateT action elabState of
                                         OK (res, newState) -> return (res, newState)
                                         Error e -> do done_elaborating_arg f argName
                                                       lift (tfail (elaboratingArgErr while' e))
                 put newState
                 return result


-- For every alternative, look at the function at the head. Automatically resolve
-- any nested alternatives where that function is also at the head

pruneAlt :: [PTerm] -> [PTerm]
pruneAlt xs = map prune xs
  where
    prune (PApp fc1 (PRef fc2 f) as)
        = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)
    prune t = t

    choose f (PAlternative a as)
        = let as' = fmap (choose f) as
              fs = filter (headIs f) as' in
              case fs of
                 [a] -> a
                 _ -> PAlternative a as'

    choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)
    choose f t = t

    headIs f (PApp _ (PRef _ f') _) = f == f'
    headIs f (PApp _ f' _) = headIs f f'
    headIs f _ = True -- keep if it's not an application

-- Rule out alternatives that don't return the same type as the head of the goal
-- (If there are none left as a result, do nothing)
pruneByType :: Term -> Context -> [PTerm] -> [PTerm]
pruneByType (P _ n _) c as
-- if the goal type is polymorphic, keep e
   | [] <- lookupTy n c = as
   | otherwise
       = let asV = filter (headIs True n) as
             as' = filter (headIs False n) as in
             case as' of
               [] -> case asV of
                        [] -> as
                        _ -> asV
               _ -> as'
  where
    headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'
    headIs var f (PApp _ f' _) = headIs var f f'
    headIs var f (PPi _ _ _ sc) = headIs var f sc
    headIs _ _ _ = True -- keep if it's not an application

    typeHead var f f'
        = case lookupTy f' c of
                       [ty] -> let ty' = normalise c [] ty in
                                   case unApply (getRetTy ty') of
                                    (P _ ftyn _, _) -> ftyn == f
                                    (V _, _) -> var -- keep, variable
                                    _ -> False
                       _ -> False

pruneByType t _ as = as

findInstances :: IState -> Term -> [Name]
findInstances ist t
    | (P _ n _, _) <- unApply t
        = case lookupCtxt n (idris_classes ist) of
            [CI _ _ _ _ _ ins] -> ins
            _ -> []
    | otherwise = []

trivial' ist
    = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist
proofSearch' ist top n hints
    = proofSearch (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist


resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
resolveTC = resTC' [] 

resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class"
resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
resTC' tcs depth topg fn ist
      = do hnf_compute
           g <- goal
           ptm <- get_term
           ulog <- getUnifyLog
           hs <- get_holes
           traceWhen ulog ("Resolving class " ++ show g) $ 
            try' (trivial' ist)
                (do t <- goal
                    let (tc, ttypes) = unApply t
                    scopeOnly <- needsDefault t tc ttypes
                    let insts_in = findInstances ist t
                    let insts = if scopeOnly then filter chaser insts_in
                                    else insts_in
                    tm <- get_term
                    let depth' = if scopeOnly then 2 else depth
                    blunderbuss t depth' insts) True
  where
    elabTC n | n /= fn && tcname n = (resolve n depth, show n)
             | otherwise = (fail "Can't resolve", show n)

    -- HACK! Rather than giving a special name, better to have some kind
    -- of flag in ClassInfo structure
    chaser (UN nm) 
        | ('@':'@':_) <- str nm = True -- old way
    chaser (SN (ParentN _ _)) = True
    chaser (NS n _) = chaser n
    chaser _ = False

    numclass = sNS (sUN "Num") ["Classes","Prelude"]

    needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass
        = do focus a
             fill (RConstant (AType (ATInt ITBig))) -- default Integer
             solve
             return False
    needsDefault t f as
          | all boundVar as = return True -- fail $ "Can't resolve " ++ show t
    needsDefault t f a = return False -- trace (show t) $ return ()

    boundVar (P Bound _ _) = True
    boundVar _ = False

    blunderbuss t d [] = do -- c <- get_env
                            -- ps <- get_probs
                            lift $ tfail $ CantResolve topg
    blunderbuss t d (n:ns)
        | n /= fn && tcname n = try' (resolve n d)
                                     (blunderbuss t d ns) True
        | otherwise = blunderbuss t d ns

    resolve n depth
       | depth == 0 = fail $ "Can't resolve type class"
       | otherwise
           = do t <- goal
                let (tc, ttypes) = unApply t
--                 if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
--                   else do
                   -- if there's a hole in the goal, don't even try
                let imps = case lookupCtxtName n (idris_implicits ist) of
                                [] -> []
                                [args] -> map isImp (snd args) -- won't be overloaded!
                ps <- get_probs
                tm <- get_term
                args <- map snd <$> try' (apply (Var n) imps)
                                         (match_apply (Var n) imps) True
                ps' <- get_probs
                when (length ps < length ps') $ fail "Can't apply type class"
--                 traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
                mapM_ (\ (_,n) -> do focus n
                                     t' <- goal
                                     let (tc', ttype) = unApply t'
                                     let got = fst (unApply t)
                                     let depth' = if tc' `elem` tcs
                                                     then depth - 1 else depth 
                                     resTC' (got : tcs)  depth' topg fn ist)
                      (filter (\ (x, y) -> not x) (zip (map fst imps) args))
                -- if there's any arguments left, we've failed to resolve
                hs <- get_holes
                ulog <- getUnifyLog
                solve
                traceWhen ulog ("Got " ++ show n) $ return ()
       where isImp (PImp p _ _ _ _) = (True, p)
             isImp arg = (False, priority arg)

collectDeferred :: Maybe Name ->
                   Term -> State [(Name, (Int, Maybe Name, Type))] Term
collectDeferred top (Bind n (GHole i t) app) =
    do ds <- get
       t' <- collectDeferred top t
       when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
       collectDeferred top app
collectDeferred top (Bind n b t) = do b' <- cdb b
                                      t' <- collectDeferred top t
                                      return (Bind n b' t')
  where
    cdb (Let t v)   = liftM2 Let (collectDeferred top t) (collectDeferred top v)
    cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)
    cdb b           = do ty' <- collectDeferred top (binderTy b)
                         return (b { binderTy = ty' })
collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)
collectDeferred top t = return t

-- Running tactics directly
-- if a tactic adds unification problems, return an error

runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
runTac autoSolve ist fn tac 
    = do env <- get_env
         g <- goal
         if autoSolve 
            then runT (fmap (addImplBound ist (map fst env)) tac)
            else no_errors (runT (fmap (addImplBound ist (map fst env)) tac))
                   (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
  where
    runT (Intro []) = do g <- goal
                         attack; intro (bname g)
      where
        bname (Bind n _ _) = Just n
        bname _ = Nothing
    runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
    runT Intros = do g <- goal
                     attack; intro (bname g)
                     try' (runT Intros)
                          (return ()) True
      where
        bname (Bind n _ _) = Just n
        bname _ = Nothing
    runT (Exact tm) = do elab ist toplevel False [] (sMN 0 "tac") tm
                         when autoSolve solveAll
    runT (MatchRefine fn)
        = do fnimps <-
               case lookupCtxtName fn (idris_implicits ist) of
                    [] -> do a <- envArgs fn
                             return [(fn, a)]
                    ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
             let tacs = map (\ (fn', imps) ->
                                 (match_apply (Var fn') (map (\x -> (x, 0)) imps),
                                     show fn')) fnimps
             tryAll tacs
             when autoSolve solveAll
       where envArgs n = do e <- get_env
                            case lookup n e of
                               Just t -> return $ map (const False)
                                                      (getArgTys (binderTy t))
                               _ -> return []
    runT (Refine fn [])
        = do fnimps <-
               case lookupCtxtName fn (idris_implicits ist) of
                    [] -> do a <- envArgs fn
                             return [(fn, a)]
                    ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
             let tacs = map (\ (fn', imps) ->
                                 (apply (Var fn') (map (\x -> (x, 0)) imps),
                                     show fn')) fnimps
             tryAll tacs
             when autoSolve solveAll
       where isImp (PImp _ _ _ _ _) = True
             isImp _ = False
             envArgs n = do e <- get_env
                            case lookup n e of
                               Just t -> return $ map (const False)
                                                      (getArgTys (binderTy t))
                               _ -> return []
    runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)
                               when autoSolve solveAll
    runT (Equiv tm) -- let bind tm, then
              = do attack
                   tyn <- getNameFrom (sMN 0 "ety")
                   claim tyn RType
                   valn <- getNameFrom (sMN 0 "eqval")
                   claim valn (Var tyn)
                   letn <- getNameFrom (sMN 0 "equiv_val")
                   letbind letn (Var tyn) (Var valn)
                   focus tyn
                   elab ist toplevel False [] (sMN 0 "tac") tm
                   focus valn
                   when autoSolve solveAll
    runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
              = do attack; -- (h:_) <- get_holes
                   tyn <- getNameFrom (sMN 0 "rty")
                   -- start_unify h
                   claim tyn RType
                   valn <- getNameFrom (sMN 0 "rval")
                   claim valn (Var tyn)
                   letn <- getNameFrom (sMN 0 "rewrite_rule")
                   letbind letn (Var tyn) (Var valn)
                   focus valn
                   elab ist toplevel False [] (sMN 0 "tac") tm
                   rewrite (Var letn)
                   when autoSolve solveAll
    runT (Induction nm)
              = do induction nm
                   when autoSolve solveAll
    runT (LetTac n tm)
              = do attack
                   tyn <- getNameFrom (sMN 0 "letty")
                   claim tyn RType
                   valn <- getNameFrom (sMN 0 "letval")
                   claim valn (Var tyn)
                   letn <- unique_hole n
                   letbind letn (Var tyn) (Var valn)
                   focus valn
                   elab ist toplevel False [] (sMN 0 "tac") tm
                   when autoSolve solveAll
    runT (LetTacTy n ty tm)
              = do attack
                   tyn <- getNameFrom (sMN 0 "letty")
                   claim tyn RType
                   valn <- getNameFrom (sMN 0 "letval")
                   claim valn (Var tyn)
                   letn <- unique_hole n
                   letbind letn (Var tyn) (Var valn)
                   focus tyn
                   elab ist toplevel False [] (sMN 0 "tac") ty
                   focus valn
                   elab ist toplevel False [] (sMN 0 "tac") tm
                   when autoSolve solveAll
    runT Compute = compute
    runT Trivial = do trivial' ist; when autoSolve solveAll
    runT TCInstance = runT (Exact (PResolveTC emptyFC))
    runT (ProofSearch top hints)
         = do proofSearch' ist top fn hints; when autoSolve solveAll
    runT (Focus n) = focus n
    runT Solve = solve
    runT (Try l r) = do try' (runT l) (runT r) True
    runT (TSeq l r) = do runT l; runT r
    runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
                               tgoal <- goal -- store the goal
                               attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
                               script <- getNameFrom (sMN 0 "script")
                               claim script scriptTy
                               scriptvar <- getNameFrom (sMN 0 "scriptvar" )
                               letbind scriptvar scriptTy (Var script)
                               focus script
                               elab ist toplevel False [] (sMN 0 "tac") tm
                               (script', _) <- get_type_val (Var scriptvar)
                               -- now that we have the script apply
                               -- it to the reflected goal and context
                               restac <- getNameFrom (sMN 0 "restac")
                               claim restac tacticTy
                               focus restac
                               fill (raw_apply (forget script')
                                               [reflectEnv tenv, reflect tgoal])
                               restac' <- get_guess
                               solve
                               -- normalise the result in order to
                               -- reify it
                               ctxt <- get_context
                               env <- get_env
                               let tactic = normalise ctxt env restac'
                               runReflected tactic
        where tacticTy = Var (reflm "Tactic")
              listTy = Var (sNS (sUN "List") ["List", "Prelude"])
              scriptTy = (RBind (sMN 0 "__pi_arg")
                                (Pi (RApp listTy envTupleType))
                                    (RBind (sMN 1 "__pi_arg")
                                           (Pi (Var $ reflm "TT")) tacticTy))
    runT (ByReflection tm) -- run the reflection function 'tm' on the
                           -- goal, then apply the resulting reflected Tactic
        = do tgoal <- goal
             attack
             script <- getNameFrom (sMN 0 "script")
             claim script scriptTy
             scriptvar <- getNameFrom (sMN 0 "scriptvar" )
             letbind scriptvar scriptTy (Var script)
             focus script
             ptm <- get_term
             elab ist toplevel False [] (sMN 0 "tac") 
                  (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
             (script', _) <- get_type_val (Var scriptvar)
             -- now that we have the script apply
             -- it to the reflected goal 
             restac <- getNameFrom (sMN 0 "restac")
             claim restac tacticTy
             focus restac
             fill (forget script')
             restac' <- get_guess
             solve
             -- normalise the result in order to
             -- reify it
             ctxt <- get_context
             env <- get_env
             let tactic = normalise ctxt env restac'
             runReflected tactic
      where tacticTy = Var (reflm "Tactic")
            scriptTy = tacticTy

    runT (Reflect v) = do attack -- let x = reflect v in ...
                          tyn <- getNameFrom (sMN 0 "letty")
                          claim tyn RType
                          valn <- getNameFrom (sMN 0 "letval")
                          claim valn (Var tyn)
                          letn <- getNameFrom (sMN 0 "letvar")
                          letbind letn (Var tyn) (Var valn)
                          focus valn
                          elab ist toplevel False [] (sMN 0 "tac") v
                          (value, _) <- get_type_val (Var letn)
                          ctxt <- get_context
                          env <- get_env
                          let value' = hnf ctxt env value
                          runTac autoSolve ist fn (Exact $ PQuote (reflect value'))
    runT (Fill v) = do attack -- let x = fill x in ...
                       tyn <- getNameFrom (sMN 0 "letty")
                       claim tyn RType
                       valn <- getNameFrom (sMN 0 "letval")
                       claim valn (Var tyn)
                       letn <- getNameFrom (sMN 0 "letvar")
                       letbind letn (Var tyn) (Var valn)
                       focus valn
                       elab ist toplevel False [] (sMN 0 "tac") v
                       (value, _) <- get_type_val (Var letn)
                       ctxt <- get_context
                       env <- get_env
                       let value' = normalise ctxt env value
                       rawValue <- reifyRaw value'
                       runTac autoSolve ist fn (Exact $ PQuote rawValue)
    runT (GoalType n tac) = do g <- goal
                               case unApply g of
                                    (P _ n' _, _) ->
                                       if nsroot n' == sUN n
                                          then runT tac
                                          else fail "Wrong goal type"
                                    _ -> fail "Wrong goal type"
    runT ProofState = do g <- goal
                         return ()
    runT x = fail $ "Not implemented " ++ show x

    runReflected t = do t' <- reify ist t
                        runTac autoSolve ist fn t'

-- | Prefix a name with the "Language.Reflection" namespace
reflm :: String -> Name
reflm n = sNS (sUN n) ["Reflection", "Language"]


-- | Reify tactics from their reflected representation
reify :: IState -> Term -> ElabD PTactic
reify _ (P _ n _) | n == reflm "Intros" = return Intros
reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
reify _ (P _ n _) | n == reflm "Solve" = return Solve
reify _ (P _ n _) | n == reflm "Compute" = return Compute
reify ist t@(App _ _)
          | (P _ f _, args) <- unApply t = reifyApp ist f args
reify _ t = fail ("Unknown tactic " ++ show t)

reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
reifyApp _ t [x]
           | t == reflm "Refine" = do n <- reifyTTName x
                                      return $ Refine n []
reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
reifyApp ist t [Constant (Str n), x]
             | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
reifyApp _ t [Constant (Str n)]
           | t == reflm "Intro" = return $ Intro [sUN n]
reifyApp ist t [t']
             | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
reifyApp ist t [t']
             | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
reifyApp ist t [t']
             | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
reifyApp _ t [t']
           | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
reifyApp ist t [t']
             | t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
reifyApp ist t [x]
             | t == reflm "Focus" = liftM Focus (reifyTTName x)
reifyApp ist t [t']
             | t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
reifyApp ist t [n, t']
             | t == reflm "LetTac" = do n'  <- reifyTTName n
                                        t'' <- reifyTT t'
                                        return $ LetTac n' (delab ist t')
reifyApp ist t [n, tt', t']
             | t == reflm "LetTacTy" = do n'   <- reifyTTName n
                                          tt'' <- reifyTT tt'
                                          t''  <- reifyTT t'
                                          return $ LetTacTy n' (delab ist tt'') (delab ist t'')
reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

-- | Reify terms from their reflected representation
reifyTT :: Term -> ElabD Term
reifyTT t@(App _ _)
        | (P _ f _, args) <- unApply t = reifyTTApp f args
reifyTT t@(P _ n _)
        | n == reflm "Erased" = return $ Erased
reifyTT t@(P _ n _)
        | n == reflm "Impossible" = return $ Impossible
reifyTT t = fail ("Unknown reflection term: " ++ show t)

reifyTTApp :: Name -> [Term] -> ElabD Term
reifyTTApp t [nt, n, x]
           | t == reflm "P" = do nt' <- reifyTTNameType nt
                                 n'  <- reifyTTName n
                                 x'  <- reifyTT x
                                 return $ P nt' n' x'
reifyTTApp t [Constant (I i)]
           | t == reflm "V" = return $ V i
reifyTTApp t [n, b, x]
           | t == reflm "Bind" = do n' <- reifyTTName n
                                    b' <- reifyTTBinder reifyTT (reflm "TT") b
                                    x' <- reifyTT x
                                    return $ Bind n' b' x'
reifyTTApp t [f, x]
           | t == reflm "App" = do f' <- reifyTT f
                                   x' <- reifyTT x
                                   return $ App f' x'
reifyTTApp t [c]
           | t == reflm "TConst" = liftM Constant (reifyTTConst c)
reifyTTApp t [t', Constant (I i)]
           | t == reflm "Proj" = do t'' <- reifyTT t'
                                    return $ Proj t'' i
reifyTTApp t [tt]
           | t == reflm "TType" = liftM TType (reifyTTUExp tt)
reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

-- | Reify raw terms from their reflected representation
reifyRaw :: Term -> ElabD Raw
reifyRaw t@(App _ _)
         | (P _ f _, args) <- unApply t = reifyRawApp f args
reifyRaw t@(P _ n _)
         | n == reflm "RType" = return $ RType
reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)

reifyRawApp :: Name -> [Term] -> ElabD Raw
reifyRawApp t [n]
            | t == reflm "Var" = liftM Var (reifyTTName n)
reifyRawApp t [n, b, x]
            | t == reflm "RBind" = do n' <- reifyTTName n
                                      b' <- reifyTTBinder reifyRaw (reflm "Raw") b
                                      x' <- reifyRaw x
                                      return $ RBind n' b' x'
reifyRawApp t [f, x]
            | t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
reifyRawApp t [t']
            | t == reflm "RForce" = liftM RForce (reifyRaw t')
reifyRawApp t [c]
            | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))

reifyTTName :: Term -> ElabD Name
reifyTTName t
            | (P _ f _, args) <- unApply t = reifyTTNameApp f args
reifyTTName t = fail ("Unknown reflection term name: " ++ show t)

reifyTTNameApp :: Name -> [Term] -> ElabD Name
reifyTTNameApp t [Constant (Str n)]
               | t == reflm "UN" = return $ sUN n
reifyTTNameApp t [n, ns]
               | t == reflm "NS" = do n'  <- reifyTTName n
                                      ns' <- reifyTTNamespace ns
                                      return $ sNS n' ns'
reifyTTNameApp t [Constant (I i), Constant (Str n)]
               | t == reflm "MN" = return $ sMN i n
reifyTTNameApp t []
               | t == reflm "NErased" = return NErased
reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))

reifyTTNamespace :: Term -> ElabD [String]
reifyTTNamespace t@(App _ _)
  = case unApply t of
      (P _ f _, [Constant StrType])
           | f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
      (P _ f _, [Constant StrType, Constant (Str n), ns])
           | f == sNS (sUN "::")  ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
      _ -> fail ("Unknown reflection namespace arg: " ++ show t)
reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)

reifyTTNameType :: Term -> ElabD NameType
reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
reifyTTNameType t@(App _ _)
  = case unApply t of
      (P _ f _, [Constant (I tag), Constant (I num)])
           | f == reflm "DCon" -> return $ DCon tag num
           | f == reflm "TCon" -> return $ TCon tag num
      _ -> fail ("Unknown reflection name type: " ++ show t)
reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder reificator binderType t@(App _ _)
  = case unApply t of
     (P _ f _, bt:args) | forget bt == Var binderType
       -> reifyTTBinderApp reificator f args
     _ -> fail ("Mismatching binder reflection: " ++ show t)
reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)

reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
reifyTTBinderApp reif f [t]
                      | f == reflm "Lam" = liftM Lam (reif t)
reifyTTBinderApp reif f [t]
                      | f == reflm "Pi" = liftM Pi (reif t)
reifyTTBinderApp reif f [x, y]
                      | f == reflm "Let" = liftM2 Let (reif x) (reif y)
reifyTTBinderApp reif f [x, y]
                      | f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
reifyTTBinderApp reif f [t]
                      | f == reflm "Hole" = liftM Hole (reif t)
reifyTTBinderApp reif f [t]
                      | f == reflm "GHole" = liftM (GHole 0) (reif t)
reifyTTBinderApp reif f [x, y]
                      | f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
reifyTTBinderApp reif f [t]
                      | f == reflm "PVar" = liftM PVar (reif t)
reifyTTBinderApp reif f [t]
                      | f == reflm "PVTy" = liftM PVTy (reif t)
reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

reifyTTConst :: Term -> ElabD Const
reifyTTConst (P _ n _) | n == reflm "IType"    = return (AType (ATInt ITNative))
reifyTTConst (P _ n _) | n == reflm "BIType"   = return (AType (ATInt ITBig))
reifyTTConst (P _ n _) | n == reflm "FlType"   = return (AType ATFloat)
reifyTTConst (P _ n _) | n == reflm "ChType"   = return (AType (ATInt ITChar))
reifyTTConst (P _ n _) | n == reflm "StrType"  = return $ StrType
reifyTTConst (P _ n _) | n == reflm "B8Type"   = return (AType (ATInt (ITFixed IT8)))
reifyTTConst (P _ n _) | n == reflm "B16Type"  = return (AType (ATInt (ITFixed IT16)))
reifyTTConst (P _ n _) | n == reflm "B32Type"  = return (AType (ATInt (ITFixed IT32)))
reifyTTConst (P _ n _) | n == reflm "B64Type"  = return (AType (ATInt (ITFixed IT64)))
reifyTTConst (P _ n _) | n == reflm "PtrType"  = return $ PtrType
reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
reifyTTConst (P _ n _) | n == reflm "Forgot"   = return $ Forgot
reifyTTConst t@(App _ _)
             | (P _ f _, [arg]) <- unApply t   = reifyTTConstApp f arg
reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

reifyTTConstApp :: Name -> Term -> ElabD Const
reifyTTConstApp f (Constant c@(I _))
                | f == reflm "I"   = return $ c
reifyTTConstApp f (Constant c@(BI _))
                | f == reflm "BI"  = return $ c
reifyTTConstApp f (Constant c@(Fl _))
                | f == reflm "Fl"  = return $ c
reifyTTConstApp f (Constant c@(I _))
                | f == reflm "Ch"  = return $ c
reifyTTConstApp f (Constant c@(Str _))
                | f == reflm "Str" = return $ c
reifyTTConstApp f (Constant c@(B8 _))
                | f == reflm "B8"  = return $ c
reifyTTConstApp f (Constant c@(B16 _))
                | f == reflm "B16" = return $ c
reifyTTConstApp f (Constant c@(B32 _))
                | f == reflm "B32" = return $ c
reifyTTConstApp f (Constant c@(B64 _))
                | f == reflm "B64" = return $ c
reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

reifyTTUExp :: Term -> ElabD UExp
reifyTTUExp t@(App _ _)
  = case unApply t of
      (P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
      (P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
      _ -> fail ("Unknown reflection type universe expression: " ++ show t)
reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

-- | Create a reflected call to a named function/constructor
reflCall :: String -> [Raw] -> Raw
reflCall funName args
  = raw_apply (Var (reflm funName)) args

-- | Lift a term into its Language.Reflection.TT representation
reflect :: Term -> Raw
reflect (P nt n t)
  = reflCall "P" [reflectNameType nt, reflectName n, reflect t]
reflect (V n)
  = reflCall "V" [RConstant (I n)]
reflect (Bind n b x)
  = reflCall "Bind" [reflectName n, reflectBinder b, reflect x]
reflect (App f x)
  = reflCall "App" [reflect f, reflect x]
reflect (Constant c)
  = reflCall "TConst" [reflectConstant c]
reflect (Proj t i)
  = reflCall "Proj" [reflect t, RConstant (I i)]
reflect (Erased) = Var (reflm "Erased")
reflect (Impossible) = Var (reflm "Impossible")
reflect (TType exp) = reflCall "TType" [reflectUExp exp]

reflectNameType :: NameType -> Raw
reflectNameType (Bound) = Var (reflm "Bound")
reflectNameType (Ref) = Var (reflm "Ref")
reflectNameType (DCon x y)
  = reflCall "DCon" [RConstant (I x), RConstant (I y)]
reflectNameType (TCon x y)
  = reflCall "TCon" [RConstant (I x), RConstant (I y)]

reflectName :: Name -> Raw
reflectName (UN s)
  = reflCall "UN" [RConstant (Str (str s))]
reflectName (NS n ns)
  = reflCall "NS" [ reflectName n
                  , foldr (\ n s ->
                             raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
                                       [ RConstant StrType, RConstant (Str n), s ])
                             ( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
                                         [ RConstant StrType ])
                             (map str ns)
                  ]
reflectName (MN i n)
  = reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
reflectName (NErased) = Var (reflm "NErased")
reflectName n = Var (reflm "NErased") -- special name, not yet implemented

reflectBinder :: Binder Term -> Raw
reflectBinder (Lam t)
   = reflCall "Lam" [Var (reflm "TT"), reflect t]
reflectBinder (Pi t)
   = reflCall "Pi" [Var (reflm "TT"), reflect t]
reflectBinder (Let x y)
   = reflCall "Let" [Var (reflm "TT"), reflect x, reflect y]
reflectBinder (NLet x y)
   = reflCall "NLet" [Var (reflm "TT"), reflect x, reflect y]
reflectBinder (Hole t)
   = reflCall "Hole" [Var (reflm "TT"), reflect t]
reflectBinder (GHole _ t)
   = reflCall "GHole" [Var (reflm "TT"), reflect t]
reflectBinder (Guess x y)
   = reflCall "Guess" [Var (reflm "TT"), reflect x, reflect y]
reflectBinder (PVar t)
   = reflCall "PVar" [Var (reflm "TT"), reflect t]
reflectBinder (PVTy t)
   = reflCall "PVTy" [Var (reflm "TT"), reflect t]

reflectConstant :: Const -> Raw
reflectConstant c@(I  _) = reflCall "I"  [RConstant c]
reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
reflectConstant (AType (ATInt ITNative)) = Var (reflm "IType")
reflectConstant (AType (ATInt ITBig)) = Var (reflm "BIType")
reflectConstant (AType ATFloat) = Var (reflm "FlType")
reflectConstant (AType (ATInt ITChar)) = Var (reflm "ChType")
reflectConstant (StrType) = Var (reflm "StrType")
reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
reflectConstant (AType (ATInt (ITFixed IT8)))  = Var (reflm "B8Type")
reflectConstant (AType (ATInt (ITFixed IT16))) = Var (reflm "B16Type")
reflectConstant (AType (ATInt (ITFixed IT32))) = Var (reflm "B32Type")
reflectConstant (AType (ATInt (ITFixed IT64))) = Var (reflm "B64Type")
reflectConstant (PtrType) = Var (reflm "PtrType")
reflectConstant (VoidType) = Var (reflm "VoidType")
reflectConstant (Forgot) = Var (reflm "Forgot")

reflectUExp :: UExp -> Raw
reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

-- | Reflect the environment of a proof into a List (TTName, Binder TT)
reflectEnv :: Env -> Raw
reflectEnv = foldr consToEnvList emptyEnvList
  where
    consToEnvList :: (Name, Binder Term) -> Raw -> Raw
    consToEnvList (n, b) l
      = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
                  [ envTupleType
                  , raw_apply (Var pairCon) [ (Var $ reflm "TTName")
                                            , (RApp (Var $ reflm "Binder")
                                                    (Var $ reflm "TT"))
                                            , reflectName n
                                            , reflectBinder b
                                            ]
                  , l
                  ]

    emptyEnvList :: Raw
    emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
                             [envTupleType]

-- | Reflect an error into the internal datatype of Idris -- TODO
rawBool :: Bool -> Raw
rawBool True  = Var (sNS (sUN "True") ["Bool", "Prelude"])
rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])

rawNil :: Raw -> Raw
rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]

rawCons :: Raw -> Raw -> Raw -> Raw
rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]

rawList :: Raw -> [Raw] -> Raw
rawList ty = foldr (rawCons ty) (rawNil ty)

rawPairTy :: Raw -> Raw -> Raw
rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]

rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]

reflectCtxt :: [(Name, Type)] -> Raw
reflectCtxt ctxt = rawList (rawPairTy  (Var $ reflm "TTName") (Var $ reflm "TT"))
                           (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
                                                      (reflectName n, reflect t)))
                                ctxt)

reflectErr :: Err -> Raw
reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
reflectErr (CantUnify b t1 t2 e ctxt i) =
  raw_apply (Var $ reflErrName "CantUnify")
            [ rawBool b
            , reflect t1
            , reflect t2
            , reflectErr e
            , reflectCtxt ctxt
            , RConstant (I i)]
reflectErr (InfiniteUnify n tm ctxt) =
  raw_apply (Var $ reflErrName "InfiniteUnify")
            [ reflectName n
            , reflect tm
            , reflectCtxt ctxt
            ]
reflectErr (CantConvert t t' ctxt) =
  raw_apply (Var $ reflErrName "CantConvert")
            [ reflect t
            , reflect t'
            , reflectCtxt ctxt
            ]
reflectErr (CantSolveGoal t ctxt) =
  raw_apply (Var $ reflErrName "CantSolveGoal")
            [ reflect t
            , reflectCtxt ctxt
            ]
reflectErr (UnifyScope n n' t ctxt) =
  raw_apply (Var $ reflErrName "UnifyScope")
            [ reflectName n
            , reflectName n'
            , reflect t
            , reflectCtxt ctxt
            ]
reflectErr (CantInferType str) =
  raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
reflectErr (NonFunctionType t t') =
  raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
reflectErr (NotEquality t t') =
  raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
reflectErr (NotInjective t1 t2 t3) =
  raw_apply (Var $ reflErrName "NotInjective")
            [ reflect t1
            , reflect t2
            , reflect t3
            ]
reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
reflectErr (CantResolveAlts ss) =
  raw_apply (Var $ reflErrName "CantResolve")
            [rawList (Var $ (sUN "String")) (map (RConstant . Str) ss)]
reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
reflectErr UniverseError = Var $ reflErrName "UniverseError"
reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
reflectErr (ProviderError str) =
  raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
reflectErr (LoadingFailed str err) =
  raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

elaboratingArgErr :: [(Name, Name)] -> Err -> Err
elaboratingArgErr [] err = err
elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
  where rewrite (ElaboratingArg _ _ _ _) = Nothing
        rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)
        rewrite (At fc e) = fmap (At fc) (rewrite e)
        rewrite err = Just (ElaboratingArg f x during err)


withErrorReflection :: Idris a -> Idris a
withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
    where handle :: Err -> Idris Err
          handle e@(ReflectionError _ _)  = do logLvl 3 "Skipping reflection of error reflection result"
                                               return e -- Don't do meta-reflection of errors
          handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
                                               return e
          -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
          handle e@(At fc err) = do logLvl 3 "Reflecting body of At"
                                    err' <- handle err
                                    return (At fc err')
          handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
                                                 err' <- handle err
                                                 return (Elaborating what n err')
          handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
                                                      hs <- getFnHandlers f a
                                                      err' <- if null hs
                                                                 then handle err
                                                                 else applyHandlers err hs
                                                      return (ElaboratingArg f a prev err')
          -- TODO: argument-specific error handlers go here for ElaboratingArg
          handle e = do ist <- getIState
                        logLvl 2 "Starting error reflection"
                        let handlers = idris_errorhandlers ist
                        applyHandlers e handlers
          getFnHandlers :: Name -> Name -> Idris [Name]
          getFnHandlers f arg = do ist <- getIState
                                   let funHandlers = maybe M.empty id .
                                                     lookupCtxtExact f .
                                                     idris_function_errorhandlers $ ist
                                   return . maybe [] S.toList . M.lookup arg $ funHandlers


          applyHandlers e handlers =
                      do ist <- getIState
                         let err = fmap (errReverse ist) e
                         logLvl 3 $ "Using reflection handlers " ++
                                    concat (intersperse ", " (map show handlers))
                         let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers

                         -- Typecheck error handlers - if this fails, then something else was wrong earlier!
                         handlers <- case mapM (check (tt_ctxt ist) []) reports of
                                       Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
                                       OK hs   -> return hs

                         -- Normalize error handler terms to produce the new messages
                         ctxt <- getContext
                         let results = map (normalise ctxt []) (map fst handlers)
                         logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))

                         -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
                         let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
                         errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
                                         Left err -> ierror err
                                         Right ok -> return ok
                         return $ case errorparts of
                                    []    -> e
                                    parts -> ReflectionError errorparts e

fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)
  | just == txt "Just" = Just tm
fromTTMaybe x          = Nothing

reflErrName :: String -> Name
reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

-- | Attempt to reify a report part from TT to the internal
-- representation. Not in Idris or ElabD monads because it should be usable
-- from either.
reifyReportPart :: Term -> Either Err ErrorReportPart
reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =
    Right (TextPart msg)
reifyReportPart (App (P (DCon _ _) n _) ttn)
  | n == reflErrName "NamePart" =
    case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of
      Error e -> Left . InternalMsg $
       "could not reify name term " ++
       show ttn ++
       " when reflecting an error:" ++ show e
      OK (n', _)-> Right $ NamePart n'
reifyReportPart (App (P (DCon _ _) n _) tm)
  | n == reflErrName "TermPart" =
  case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of
    Error e -> Left . InternalMsg $
      "could not reify reflected term " ++
      show tm ++
      " when reflecting an error:" ++ show e
    OK (tm', _) -> Right $ TermPart tm'
reifyReportPart (App (P (DCon _ _) n _) tm)
  | n == reflErrName "SubReport" =
  case unList tm of
    Just xs -> do subParts <- mapM reifyReportPart xs
                  Right (SubReport subParts)
    Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

envTupleType :: Raw
envTupleType
  = raw_apply (Var pairTy) [ (Var $ reflm "TTName")
                           , (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
                           ]

solveAll = try (do solve; solveAll) (return ())