{-# LANGUAGE PatternGuards #-}

module Idris.ElabTerm where

import Idris.AbsSyntax
import Idris.DSL
import Idris.Delaborate
import Idris.Error
import Idris.ProofSearch

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

import Control.Applicative ((<$>))
import Control.Monad
import Control.Monad.State.Strict
import Data.List
import qualified Data.Map as M
import Data.Maybe (mapMaybe)
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
         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
         when (not pattern) $ do matchProblems; unifyProblems
         probs <- get_probs
         case probs of
            [] -> return ()
            ((_,_,_,e):es) -> 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
         initNextNameFrom ns
         elab ist info pattern opts fn tm
         probs <- get_probs
         tm <- get_term
         case probs of
            [] -> return ()
            ((_,_,_,e):es) -> 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
                  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
                 tm <- get_term
                 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
                    $ -}
                  do t' <- insertCoerce ina t
                     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') $ 
                     elab' ina t'

    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 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 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
             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 ()
                    -- 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' (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 tcArg (n, PConstraint _ _ Placeholder _) = True
            tcArg _ = False
            
            -- normal < tactic < default tactic
            cmpArg (_, x) (_, y)
                   = compare (priority x + alt x) (priority y + alt y)
                where alt t = case getTm t of
                                   PAlternative False _ -> 5
                                   _ -> 0

            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) ts
    elab' ina (PTactics ts)
        | not pattern = do mapM_ (runTac False ist) 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 " ++ show 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

    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, PTerm)] -- ^ (Laziness, argument)
             -> ElabD ()
    elabArgs ist ina failed fc retry f [] _
--         | retry = let (ns, ts) = unzip (reverse failed) in
--                       elabArgs ina [] False ns ts
        | otherwise = return ()
    elabArgs ist ina failed fc r f (n:ns) ((_, Placeholder) : args)
        = elabArgs ist ina failed fc r f ns args
    elabArgs ist ina failed fc r f ((argName, holeName):ns) ((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 =
              reflectFunctionErrors ist f argName $
              do hs <- get_holes
                 tm <- get_term
                 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; elabE ina t; return failed
                              False -> return failed
                 elabArgs ist ina failed fc r f ns args

-- | Perform error reflection for function applicaitons with specific error handlers
reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a
reflectFunctionErrors ist f arg action =
  do elabState <- get
     (result, newState) <- case runStateT action elabState of
                             OK (res, newState) -> return (res, newState)
                             Error e@(ReflectionError _ _) -> (lift . tfail) e
                             Error e@(ReflectionFailed _ _) -> (lift . tfail) e
                             Error e -> handle e >>= lift . tfail
     put newState
     return result
  where handle :: Err -> ElabD Err
        handle e = do let funhandlers = (maybe M.empty id . lookupCtxtExact f . idris_function_errorhandlers) ist
                          handlers = (maybe [] S.toList . M.lookup arg) funhandlers
                          reports  = map (\n -> RApp (Var n) (reflectErr e)) handlers


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

                      -- Normalize error handler terms to produce the new messages
                      let ctxt    = tt_ctxt ist
                          results = map (normalise ctxt []) (map fst handlers)

                      -- 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 -> lift (tfail err)
                                      Right ok -> return ok
                      return $ case errorparts of
                                   []    -> e
                                   parts -> ReflectionError errorparts e

-- 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 0 topg fn ist = fail $ "Can't resolve type class"
resolveTC 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
resolveTC 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 depth' = if t == t' then depth - 1 else depth
                                     resolveTC 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
       when (not (n `elem` map fst ds)) $ put ((n, (i, top, t)) : ds)
       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 -> PTactic -> ElabD ()
runTac autoSolve ist tac
    = do env <- get_env
         g <- goal
         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 (ProofSearch top n hints)
         = do proofSearch' ist top n 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 (sUN "__pi_arg")
                                (Pi (RApp listTy envTupleType))
                                    (RBind (sUN "__pi_arg1")
                                           (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 (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 (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 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 "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 _ 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 (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err]
           where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc")
                                                            [ RConstant (Str source)
                                                            , RConstant (I line)
                                                            , RConstant (I col)
                                                            ]
reflectErr (Elaborating str n e) =
  raw_apply (Var $ reflErrName "Elaborating")
            [ RConstant (Str str)
            , reflectName n
            , reflectErr e
            ]
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]


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
          handle e = do ist <- getIState
                        logLvl 2 "Starting error reflection"
                        let handlers = idris_errorhandlers ist
                        logLvl 3 $ "Using reflection handlers " ++ concat (intersperse ", " (map show handlers))
                        let reports = map (\n -> RApp (Var n) (reflectErr e)) 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 ())

