{-|
Module      : Idris.Reflection
Description : Code related to Idris's reflection system. This module contains quoters and unquoters along with some supporting datatypes.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE CPP, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns -fwarn-unused-imports #-}
module Idris.Reflection (RConstructorDefn(..), RDataDefn(..),RFunArg(..),
                         RFunClause(..), RFunDefn(..), RTyDecl(..),
                         buildDatatypes, buildFunDefns, envTupleType, fromTTMaybe,
                         getArgs, mkList, rawList, rawPair, rawPairTy, reflect,
                         reflectArg, reflectDatatype, reflectEnv, reflectErr,
                         reflectFC, reflectFixity, reflectFunDefn, reflectList,
                         reflectName, reflectNameType, reflectRaw,
                         reflectRawQuotePattern, reflectRawQuote, reflectTTQuote,
                         reflectTTQuotePattern, reflm, reify, reifyBool, reifyEnv,
                         reifyFunDefn, reifyList, reifyRDataDefn, reifyRaw,
                         reifyReportPart, reifyReportParts, reifyTT, reifyTTName,
                         reifyTyDecl, rFunArgToPArg, tacN
                         ) where

import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,
                             movelast, runElab, solve)
import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact,
                            lookupTyExact)
import Idris.Core.TT

import Idris.AbsSyntaxTree (ArgOpt(..), ElabD, Fixity(..), IState(idris_datatypes, idris_implicits, idris_patdefs, tt_ctxt),
                            PArg, PArg'(..), PTactic, PTactic'(..), PTerm(..),
                            initEState, pairCon, pairTy)
import Idris.Delaborate (delab)

import Control.Monad (liftM, liftM2, liftM4)
import Control.Monad.State.Strict (lift)
import Data.List (findIndex, (\\))
import Data.Maybe (catMaybes)
import qualified Data.Text as T

data RErasure = RErased | RNotErased deriving Show

data RPlicity = RExplicit | RImplicit | RConstraint deriving Show

data RFunArg = RFunArg { argName    :: Name
                       , argTy      :: Raw
                       , argPlicity :: RPlicity
                       , erasure    :: RErasure
                       }
  deriving Show

data RTyDecl = RDeclare Name [RFunArg] Raw deriving Show

data RTyConArg = RParameter RFunArg
               | RIndex     RFunArg
  deriving Show

data RCtorArg = RCtorParameter RFunArg | RCtorField RFunArg deriving Show

data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Show

data RConstructorDefn = RConstructor Name [RFunArg] Raw

data RDataDefn = RDefineDatatype Name [RConstructorDefn]

rArgOpts :: RErasure -> [ArgOpt]
rArgOpts RErased = [InaccessibleArg]
rArgOpts _ = []

rFunArgToPArg :: RFunArg -> PArg
rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder
rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder
rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder

data RFunClause a = RMkFunClause a a
                  | RMkImpossibleClause a
                  deriving Show

data RFunDefn a = RDefineFun Name [RFunClause a] deriving Show

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

-- | Prefix a name with the "Language.Reflection.Elab" namespace
tacN :: String -> Name
tacN str = sNS (sUN str) ["Elab", "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 "Implementation" = return TCImplementation
reify _ (P _ n _) | n == reflm "Solve" = return Solve
reify _ (P _ n _) | n == reflm "Compute" = return Compute
reify _ (P _ n _) | n == reflm "Skip" = return Skip
reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
reify _ (P _ n _) | n == reflm "Unfocus" = return Unfocus
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 [Constant (I i)]
           | t == reflm "Search" = return (ProofSearch True True i Nothing [] [])
reifyApp _ t [x]
           | t == reflm "Refine" = do n <- reifyTTName x
                                      return $ Refine n []
reifyApp ist t [n, ty] | t == reflm "Claim" = do n' <- reifyTTName n
                                                 goal <- reifyTT ty
                                                 return $ Claim n' (delab ist goal)
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 [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName 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 ist t [errs]
             | t == reflm "Fail" = fmap TFail (reifyReportParts errs)
reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

reifyBool :: Term -> ElabD Bool
reifyBool (P _ n _) | n == sNS (sUN "True") ["Bool", "Prelude"] = return True
                    | n == sNS (sUN "False") ["Bool", "Prelude"] = return False
reifyBool tm = fail $ "Not a Boolean: " ++ show tm

reifyInt :: Term -> ElabD Int
reifyInt (Constant (I i)) = return i
reifyInt tm = fail $ "Not an Int: " ++ show tm

reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b)
reifyPair left right (App _ (App _ (App _ (App _ (P _ n _) _) _) x) y)
  | n == pairCon = liftM2 (,) (left x) (right y)
reifyPair left right tm = fail $ "Not a pair: " ++ show tm

reifyList :: (Term -> ElabD a) -> Term -> ElabD [a]
reifyList getElt lst =
  case unList lst of
    Nothing -> fail "Couldn't reify a list"
    Just xs -> mapM getElt xs

reifyReportParts :: Term -> ElabD [ErrorReportPart]
reifyReportParts errs =
  case unList errs of
    Nothing -> fail "Failed to reify errors"
    Just errs' ->
      let parts = mapM reifyReportPart errs' in
      case parts of
        Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
        Right errs'' ->
          return errs''

-- | 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 Complete 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 [tt]
           | t == reflm "UType" = liftM UType (reifyUniverse tt)
reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))

reifyUniverse :: Term -> ElabD Universe
reifyUniverse (P _ n _) | n == reflm "AllTypes" = return AllTypes
                        | n == reflm "UniqueType" = return UniqueType
                        | n == reflm "NullType" = return NullType
reifyUniverse tm = fail ("Unknown reflection universe: " ++ show tm)

-- | 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 in reifyRaw: " ++ 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 [c]
            | t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
reifyRawApp t args = fail ("Unknown reflection raw term in reifyRawApp: " ++ 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 [sn]
               | t == reflm "SN"
               , (P _ f _, args) <- unApply sn = SN <$> reifySN f args
  where reifySN :: Name -> [Term] -> ElabD SpecialName
        reifySN t [Constant (I i), n1, n2]
                | t == reflm "WhereN" = WhereN i <$> reifyTTName n1 <*> reifyTTName n2
        reifySN t [Constant (I i), n]
                | t == reflm "WithN" = WithN i <$> reifyTTName n
        reifySN t [n, ss]
                | t == reflm "ImplementationN" =
                  case unList ss of
                    Nothing -> fail "Can't reify ImplementationN strings"
                    Just ss' -> ImplementationN <$> reifyTTName n <*>
                                 pure [T.pack s | Constant (Str s) <- ss']
        reifySN t [n, Constant (Str s)]
                | t == reflm "ParentN" =
                  ParentN <$> reifyTTName n <*> pure (T.pack s)
        reifySN t [n]
                | t == reflm "MethodN" =
                  MethodN <$> reifyTTName n
        reifySN t [fc, n]
                | t == reflm "CaseN" =
                  CaseN <$> (FC' <$> reifyFC fc) <*> reifyTTName n
        reifySN t [n]
                | t == reflm "ImplementationCtorN" =
                  ImplementationCtorN <$> reifyTTName n
        reifySN t [n1, n2]
                | t == reflm "MetaN" =
                  MetaN <$> reifyTTName n1 <*> reifyTTName n2
        reifySN t args = fail $ "Can't reify special name " ++ show t ++ show args
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 False -- FIXME: Uniqueness!
           | 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 RigW) (reif t)
reifyTTBinderApp reif f [t, k]
                      | f == reflm "Pi" = liftM2 (Pi RigW Nothing) (reif t) (reif k)
reifyTTBinderApp reif f [x, y]
                      | f == reflm "Let" = liftM2 (Let RigW) (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 RigW) (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 "StrType"  = return StrType
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 aty
                | f == reflm "AType" = fmap AType (reifyArithTy aty)
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@(Ch _))
                | 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 v@(P _ _ _) =
    lift . tfail . Msg $
      "Can't reify the variable " ++
      show v ++
      " as a constant, because its value is not statically known."
reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))

reifyArithTy :: Term -> ElabD ArithTy
reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt"    = fmap ATInt (reifyIntTy intTy)
reifyArithTy (P _ n _)               | n == reflm "ATDouble" = return ATFloat
reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)

reifyNativeTy :: Term -> ElabD NativeTy
reifyNativeTy (P _ n _) | n == reflm "IT8"  = return IT8
reifyNativeTy (P _ n _) | n == reflm "IT16" = return IT16
reifyNativeTy (P _ n _) | n == reflm "IT32" = return IT32
reifyNativeTy (P _ n _) | n == reflm "IT64" = return IT64
reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x

reifyIntTy :: Term -> ElabD IntTy
reifyIntTy (App _ (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

reifyTTUExp :: Term -> ElabD UExp
reifyTTUExp t@(App _ _ _)
  = case unApply t of
      (P _ f _, [Constant (Str str), Constant (I i)])
           | f == reflm "UVar" -> return $ UVar str 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 = reflectTTQuote []

-- | Lift a term into its Language.Reflection.Raw representation
reflectRaw :: Raw -> Raw
reflectRaw = reflectRawQuote []

claimTy :: Name -> Raw -> ElabD Name
claimTy n ty = do n' <- getNameFrom n
                  claim n' ty
                  return n'

intToReflectedNat :: Int -> Raw
intToReflectedNat i = if i <= 0
                        then Var (natN "Z")
                        else RApp (Var (natN "S")) (intToReflectedNat (i - 1))
  where natN :: String -> Name
        natN n = sNS (sUN n) ["Nat", "Prelude"]

reflectFixity :: Fixity -> Raw
reflectFixity (Infixl  p) = RApp (Var (tacN "Infixl")) (intToReflectedNat p)
reflectFixity (Infixr  p) = RApp (Var (tacN "Infixr")) (intToReflectedNat p)
reflectFixity (InfixN  p) = RApp (Var (tacN "InfixN")) (intToReflectedNat p)
reflectFixity (PrefixN p) = RApp (Var (tacN "PrefixN")) (intToReflectedNat p)

-- | Convert a reflected term to a more suitable form for pattern-matching.
-- In particular, the less-interesting bits are elaborated to _ patterns. This
-- happens to NameTypes, universe levels, names that are bound but not used,
-- and the type annotation field of the P constructor.
reflectTTQuotePattern :: [Name] -> Term -> ElabD ()
reflectTTQuotePattern unq (P _ n _)
  | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
    do fill (Var n) ; solve
  | otherwise =
    do tyannot <- claimTy (sMN 0 "pTyAnnot") (Var (reflm "TT"))
       movelast tyannot  -- use a _ pattern here
       nt <- getNameFrom (sMN 0 "nt")
       claim nt (Var (reflm "NameType"))
       movelast nt       -- use a _ pattern here
       n' <- getNameFrom (sMN 0 "n")
       claim n' (Var (reflm "TTName"))
       fill $ reflCall "P" [Var nt, Var n', Var tyannot]
       solve
       focus n'; reflectNameQuotePattern n
reflectTTQuotePattern unq (V n)
  = do fill $ reflCall "V" [RConstant (I n)]
       solve
reflectTTQuotePattern unq (Bind n b x)
  = do x' <- claimTy (sMN 0 "sc") (Var (reflm "TT"))
       movelast x'
       b' <- getNameFrom (sMN 0 "binder")
       claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
                      (Var (sNS (sUN "TT") ["Reflection", "Language"])))
       if n `elem` freeNames x
         then do fill $ reflCall "Bind"
                                 [reflectName n,
                                  Var b',
                                  Var x']
                 solve
         else do any <- getNameFrom (sMN 0 "anyName")
                 claim any (Var (reflm "TTName"))
                 movelast any
                 fill $ reflCall "Bind"
                                 [Var any,
                                  Var b',
                                  Var x']
                 solve
       focus x'; reflectTTQuotePattern unq x
       focus b'; reflectBinderQuotePattern reflectTTQuotePattern (Var $ reflm "TT") unq b
reflectTTQuotePattern unq (App _ f x)
  = do f' <- claimTy (sMN 0 "f") (Var (reflm "TT")) ; movelast f'
       x' <- claimTy (sMN 0 "x") (Var (reflm "TT")) ; movelast x'
       fill $ reflCall "App" [Var f', Var x']
       solve
       focus f'; reflectTTQuotePattern unq f
       focus x'; reflectTTQuotePattern unq x
reflectTTQuotePattern unq (Constant c)
  = do fill $ reflCall "TConst" [reflectConstant c]
       solve
reflectTTQuotePattern unq (Proj t i)
  = lift . tfail . InternalMsg $
      "Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuotePattern unq Erased
  = do erased <- claimTy (sMN 0 "erased") (Var (reflm "TT"))
       movelast erased
       fill (Var erased)
reflectTTQuotePattern unq Impossible
  = lift . tfail . InternalMsg $
      "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuotePattern unq (Inferred t)
  = lift . tfail . InternalMsg $
      "Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."
reflectTTQuotePattern unq (TType exp)
  = do ue <- getNameFrom (sMN 0 "uexp")
       claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
       movelast ue
       fill $ reflCall "TType" [Var ue]
       solve
reflectTTQuotePattern unq (UType u)
  = do uH <- getNameFrom (sMN 0 "someUniv")
       claim uH (Var (reflm "Universe"))
       movelast uH
       fill $ reflCall "UType" [Var uH]
       solve
       focus uH
       fill (Var (reflm (case u of
                           NullType -> "NullType"
                           UniqueType -> "UniqueType"
                           AllTypes -> "AllTypes")))
       solve

reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()
reflectRawQuotePattern unq (Var n)
  -- the unquoted names already have types, just use them
  | n `elem` unq = do fill (Var n); solve
  | otherwise = do fill (reflCall "Var" [reflectName n]); solve
reflectRawQuotePattern unq (RBind n b sc) =
  do scH <- getNameFrom (sMN 0 "sc")
     claim scH (Var (reflm "Raw"))
     movelast scH
     bH <- getNameFrom (sMN 0 "binder")
     claim bH (RApp (Var (reflm "Binder"))
                    (Var (reflm "Raw")))
     if n `elem` freeNamesR sc
        then do fill $ reflCall "RBind" [reflectName n,
                                         Var bH,
                                         Var scH]
                solve
        else do any <- getNameFrom (sMN 0 "anyName")
                claim any (Var (reflm "TTName"))
                movelast any
                fill $ reflCall "RBind" [Var any, Var bH, Var scH]
                solve
     focus scH; reflectRawQuotePattern unq sc
     focus bH; reflectBinderQuotePattern reflectRawQuotePattern (Var $ reflm "Raw") unq b
  where freeNamesR (Var n) = [n]
        freeNamesR (RBind n (Let rc t v) body) = concat [freeNamesR v,
                                                         freeNamesR body \\ [n],
                                                         freeNamesR t]
        freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++
                                      (freeNamesR body \\ [n])
        freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x
        freeNamesR RType = []
        freeNamesR (RUType _) = []
        freeNamesR (RConstant _) = []
reflectRawQuotePattern unq (RApp f x) =
  do fH <- getNameFrom (sMN 0 "f")
     claim fH (Var (reflm "Raw"))
     movelast fH
     xH <- getNameFrom (sMN 0 "x")
     claim xH (Var (reflm "Raw"))
     movelast xH
     fill $ reflCall "RApp" [Var fH, Var xH]
     solve
     focus fH; reflectRawQuotePattern unq f
     focus xH; reflectRawQuotePattern unq x
reflectRawQuotePattern unq RType =
  do fill (Var (reflm "RType"))
     solve
reflectRawQuotePattern unq (RUType univ) =
  do uH <- getNameFrom (sMN 0 "universe")
     claim uH (Var (reflm "Universe"))
     movelast uH
     fill $ reflCall "RUType" [Var uH]
     solve
     focus uH; fill (reflectUniverse univ); solve
reflectRawQuotePattern unq (RConstant c) =
  do cH <- getNameFrom (sMN 0 "const")
     claim cH (Var (reflm "Constant"))
     movelast cH
     fill (reflCall "RConstant" [Var cH]); solve
     focus cH
     fill (reflectConstant c); solve

reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()
reflectBinderQuotePattern q ty unq (Lam _ t)
   = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
        fill $ reflCall "Lam" [ty, Var t']
        solve
        focus t'; q unq t
reflectBinderQuotePattern q ty unq (Pi _ _ t k)
   = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
        k' <- claimTy (sMN 0 "k") ty; movelast k';
        fill $ reflCall "Pi" [ty, Var t', Var k']
        solve
        focus t'; q unq t
reflectBinderQuotePattern q ty unq (Let rc x y)
   = do x' <- claimTy (sMN 0 "ty") ty; movelast x';
        y' <- claimTy (sMN 0 "v")ty; movelast y';
        fill $ reflCall "Let" [ty, Var x', Var y']
        solve
        focus x'; q unq x
        focus y'; q unq y
reflectBinderQuotePattern q ty unq (NLet x y)
   = do x' <- claimTy (sMN 0 "ty") ty; movelast x'
        y' <- claimTy (sMN 0 "v") ty; movelast y'
        fill $ reflCall "Let" [ty, Var x', Var y']
        solve
        focus x'; q unq x
        focus y'; q unq y
reflectBinderQuotePattern q ty unq (Hole t)
   = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
        fill $ reflCall "Hole" [ty, Var t']
        solve
        focus t'; q unq t
reflectBinderQuotePattern q ty unq (GHole _ _ t)
   = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
        fill $ reflCall "GHole" [ty, Var t']
        solve
        focus t'; q unq t
reflectBinderQuotePattern q ty unq (Guess x y)
   = do x' <- claimTy (sMN 0 "ty") ty; movelast x'
        y' <- claimTy (sMN 0 "v") ty; movelast y'
        fill $ reflCall "Guess" [ty, Var x', Var y']
        solve
        focus x'; q unq x
        focus y'; q unq y
reflectBinderQuotePattern q ty unq (PVar _ t)
   = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
        fill $ reflCall "PVar" [ty, Var t']
        solve
        focus t'; q unq t
reflectBinderQuotePattern q ty unq (PVTy t)
   = do t' <- claimTy (sMN 0 "ty") ty; movelast t'
        fill $ reflCall "PVTy" [ty, Var t']
        solve
        focus t'; q unq t

reflectUniverse :: Universe -> Raw
reflectUniverse u =
  (Var (reflm (case u of
                 NullType -> "NullType"
                 UniqueType -> "UniqueType"
                 AllTypes -> "AllTypes")))

-- | Create a reflected TT term, but leave refs to the provided name intact
reflectTTQuote :: [Name] -> Term -> Raw
reflectTTQuote unq (P nt n t)
  | n `elem` unq = Var n
  | otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectTTQuote unq t]
reflectTTQuote unq (V n)
  = reflCall "V" [RConstant (I n)]
reflectTTQuote unq (Bind n b x)
  = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
reflectTTQuote unq (App _ f x)
  = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
reflectTTQuote unq (Constant c)
  = reflCall "TConst" [reflectConstant c]
reflectTTQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
reflectTTQuote unq (UType u) = reflCall "UType" [reflectUniverse u]
reflectTTQuote _   (Proj _ _) =
  error "Phase error! The Proj constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuote unq Erased = Var (reflm "Erased")
reflectTTQuote _   Impossible =
  error "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."
reflectTTQuote _   (Inferred tm) =
  error "Phase error! The Inferred constructor is for coverage checking only and should not have been reflected during elaboration."

reflectRawQuote :: [Name] -> Raw -> Raw
reflectRawQuote unq (Var n)
  | n `elem` unq = Var n
  | otherwise = reflCall "Var" [reflectName n]
reflectRawQuote unq (RBind n b r) =
  reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
reflectRawQuote unq (RApp f x) =
  reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
reflectRawQuote unq RType = Var (reflm "RType")
reflectRawQuote unq (RUType u) =
  reflCall "RUType" [reflectUniverse u]
reflectRawQuote unq (RConstant cst) = reflCall "RConstant" [reflectConstant cst]

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)] -- FIXME: Uniqueness!
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 (SN sn) = raw_apply (Var (reflm "SN")) [reflectSpecialName sn]
reflectName (SymRef _) = error "The impossible happened: symbol table ref survived IBC loading"

reflectSpecialName :: SpecialName -> Raw
reflectSpecialName (WhereN i n1 n2) =
  reflCall "WhereN" [RConstant (I i), reflectName n1, reflectName n2]
reflectSpecialName (WithN i n) = reflCall "WithN" [ RConstant (I i)
                                                  , reflectName n
                                                  ]
reflectSpecialName (ImplementationN impl ss) =
  reflCall "ImplementationN" [ reflectName impl
                             , mkList (RConstant StrType) $
                                 map (RConstant . Str . T.unpack) ss
                             ]
reflectSpecialName (ParentN n s) =
  reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]
reflectSpecialName (MethodN n) =
  reflCall "MethodN" [reflectName n]
reflectSpecialName (CaseN fc n) =
  reflCall "CaseN" [reflectFC (unwrapFC fc), reflectName n]
reflectSpecialName (ImplementationCtorN n) =
  reflCall "ImplementationCtorN" [reflectName n]
reflectSpecialName (MetaN parent meta) =
  reflCall "MetaN" [reflectName parent, reflectName meta]

-- | Elaborate a name to a pattern.  This means that NS and UN will be intact.
-- MNs corresponding to will care about the string but not the number.  All
-- others become _.
reflectNameQuotePattern :: Name -> ElabD ()
reflectNameQuotePattern n@(UN s)
  = do fill $ reflectName n
       solve
reflectNameQuotePattern n@(NS _ _)
  = do fill $ reflectName n
       solve
reflectNameQuotePattern (MN _ n)
  = do i <- getNameFrom (sMN 0 "mnCounter")
       claim i (RConstant (AType (ATInt ITNative)))
       movelast i
       fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
       solve
reflectNameQuotePattern _ -- for all other names, match any
  = do nameHole <- getNameFrom (sMN 0 "name")
       claim nameHole (Var (reflm "TTName"))
       movelast nameHole
       fill (Var nameHole)
       solve

reflectBinder :: Binder Term -> Raw
reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
reflectBinderQuote q ty unq (Lam _ t)
   = reflCall "Lam" [Var ty, q unq t]
reflectBinderQuote q ty unq (Pi _ _ t k)
   = reflCall "Pi" [Var ty, q unq t, q unq k]
reflectBinderQuote q ty unq (Let rc x y)
   = reflCall "Let" [Var ty, q unq x, q unq y]
reflectBinderQuote q ty unq (NLet x y)
   = reflCall "Let" [Var ty, q unq x, q unq y]
reflectBinderQuote q ty unq (Hole t)
   = reflCall "Hole" [Var ty, q unq t]
reflectBinderQuote q ty unq (GHole _ _ t)
   = reflCall "GHole" [Var ty, q unq t]
reflectBinderQuote q ty unq (Guess x y)
   = reflCall "Guess" [Var ty, q unq x, q unq y]
reflectBinderQuote q ty unq (PVar _ t)
   = reflCall "PVar" [Var ty, q unq t]
reflectBinderQuote q ty unq (PVTy t)
   = reflCall "PVTy" [Var ty, q unq t]

mkList :: Raw -> [Raw] -> Raw
mkList ty []      = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
                              x)
                        (mkList ty xs)

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 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 ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATDouble")]
reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
reflectConstant StrType = Var (reflm "StrType")
reflectConstant (AType (ATInt (ITFixed IT8)))  = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
reflectConstant VoidType = Var (reflm "VoidType")
reflectConstant Forgot = Var (reflm "Forgot")
reflectConstant WorldType = Var (reflm "WorldType")
reflectConstant TheWorld = Var (reflm "TheWorld")

reflectUExp :: UExp -> Raw
reflectUExp (UVar ns i) = reflCall "UVar" [RConstant (Str ns), 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 . envBinders
  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]

-- Reflected environments don't get the RigCount (for the moment, at least)
reifyEnv :: Term -> ElabD Env
reifyEnv tm = do preEnv <- reifyList (reifyPair reifyTTName (reifyTTBinder reifyTT (reflm "TT"))) tm
                 return $ map (\(n, b) -> (n, RigW, b)) preEnv

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

-- | Idris tuples nest to the right
rawTripleTy :: Raw -> Raw -> Raw -> Raw
rawTripleTy a b c = rawPairTy a (rawPairTy b c)

rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw
rawTriple (a, b, c) (x, y, z) = rawPair (a, rawPairTy b c) (x, rawPair (b, c) (y, z))

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 (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
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 more)
   = raw_apply (Var $ reflErrName "CantResolve") [reflect t, reflectErr more]
reflectErr (InvalidTCArg n t) = raw_apply (Var $ reflErrName "InvalidTCArg") [reflectName n, reflect t]
reflectErr (CantResolveAlts ss) =
  raw_apply (Var $ reflErrName "CantResolveAlts")
            [rawList (Var $ reflm "TTName") (map reflectName ss)]
reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
reflectErr (UniverseError fc ue old new tys) =
  -- NB: loses information, but OK because this is not likely to be rewritten
  Var $ reflErrName "UniverseError"
reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
reflectErr (UnknownImplicit n f) = raw_apply (Var $ reflErrName "UnknownImplicit") [reflectName n, reflectName f]
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 l r tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect l, reflect r, 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]

-- | Reflect a file context
reflectFC :: FC -> Raw
reflectFC fc = raw_apply (Var (reflm "FileLoc"))
                         [ RConstant (Str (fc_fname fc))
                         , raw_apply (Var pairCon) $
                             [intTy, intTy] ++
                             map (RConstant . I)
                                 [ fst (fc_start fc)
                                 , snd (fc_start fc)
                                 ]
                         , raw_apply (Var pairCon) $
                             [intTy, intTy] ++
                             map (RConstant . I)
                                 [ fst (fc_end fc)
                                 , snd (fc_end fc)
                                 ]
                         ]
  where intTy = RConstant (AType (ATInt ITNative))

reifyFC :: Term -> ElabD FC
reifyFC tm
  | (P (DCon _ _ _) cn _, [Constant (Str fn), st, end]) <- unApply tm
  , cn == reflm "FileLoc" = FC fn <$> reifyPair reifyInt reifyInt st <*> reifyPair reifyInt reifyInt end
  | otherwise = fail $ "Not a source location: " ++ show tm

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 == reflm "TextPart" =
    Right (TextPart msg)
reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
  | n == reflm "NamePart" =
    case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 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 == reflm "TermPart" =
  case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 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 == reflm "RawPart" =
  case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") internalNS initContext emptyContext 0 Erased) of
    Error e -> Left . InternalMsg $
      "could not reify reflected raw term " ++
      show tm ++
      " when reflecting an error: " ++ show e
    OK (tm', _) -> Right $ RawPart tm'
reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
  | n == reflm "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

reifyErasure :: Term -> ElabD RErasure
reifyErasure (P (DCon _ _ _) n _)
  | n == tacN "Erased" = return RErased
  | n == tacN "NotErased" = return RNotErased
reifyErasure tm = fail $ "Can't reify " ++ show tm ++ " as erasure info."

reifyPlicity :: Term -> ElabD RPlicity
reifyPlicity (P (DCon _ _ _) n _)
  | n == tacN "Explicit" = return RExplicit
  | n == tacN "Implicit" = return RImplicit
  | n == tacN "Constraint" = return RConstraint
reifyPlicity tm = fail $ "Couldn't reify " ++ show tm ++ " as RPlicity."

reifyRFunArg :: Term -> ElabD RFunArg
reifyRFunArg (App _ (App _ (App _ (App _ (P (DCon _ _ _) n _) argN) argTy) argPl) argE)
  | n == tacN "MkFunArg" = liftM4 RFunArg
                             (reifyTTName argN)
                             (reifyRaw argTy)
                             (reifyPlicity argPl)
                             (reifyErasure argE)
reifyRFunArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

reifyTyDecl :: Term -> ElabD RTyDecl
reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)
  | n == tacN "Declare" =
  do tyN'  <- reifyTTName tyN
     args' <- case unList args of
                Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."
                Just xs -> mapM reifyRFunArg xs
     ret'  <- reifyRaw ret
     return $ RDeclare tyN' args' ret'
reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)
  | n == tacN "DefineFun" && t == reflm "Raw" =
  do fnN' <- reifyTTName fnN
     clauses' <- case unList clauses of
                   Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
                   Just cs -> mapM reifyC cs
     return $ RDefineFun fnN' clauses'
  where reifyC :: Term -> ElabD (RFunClause Raw)
        reifyC (App _ (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs) rhs)
          | n == tacN "MkFunClause" && t == reflm "Raw" = liftM2 RMkFunClause
                                             (reifyRaw lhs)
                                             (reifyRaw rhs)
        reifyC (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs)
          | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs
        reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

reifyRConstructorDefn :: Term -> ElabD RConstructorDefn
reifyRConstructorDefn (App _ (App _ (App _ (P _ n _) cn) args) retTy)
  | n == tacN "Constructor", Just args' <- unList args
  = RConstructor <$> reifyTTName cn <*> mapM reifyRFunArg args' <*> reifyRaw retTy
reifyRConstructorDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RConstructorDefn"

reifyRDataDefn :: Term -> ElabD RDataDefn
reifyRDataDefn (App _ (App _ (P _ n _) tyn) ctors)
  | n == tacN "DefineDatatype", Just ctors' <- unList ctors
  = RDefineDatatype <$> reifyTTName tyn <*> mapM reifyRConstructorDefn ctors'
reifyRDataDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RDataDefn"

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

reflectList :: Raw -> [Raw] -> Raw
reflectList ty []     = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
reflectList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
                                   x)
                             (reflectList ty xs)

-- | Apply Idris's implicit info to get a signature. The [PArg] should
-- come from a lookup in idris_implicits on IState.
getArgs :: [PArg] -> Raw -> ([RFunArg], Raw)
getArgs []     r = ([], r)
getArgs (a:as) (RBind n (Pi _ _ ty _) sc) =
  let (args, res) = getArgs as sc
      erased = if InaccessibleArg `elem` argopts a then RErased else RNotErased
      arg' = case a of
               PImp {} -> RFunArg n ty RImplicit erased
               PExp {} -> RFunArg n ty RExplicit erased
               PConstraint {} -> RFunArg n ty RConstraint erased
               PTacImplicit {} -> RFunArg n ty RImplicit erased
  in (arg':args, res)
getArgs _ r = ([], r)

unApplyRaw :: Raw -> (Raw, [Raw])
unApplyRaw tm = ua [] tm
  where
    ua args (RApp f a) = ua (a:args) f
    ua args t         = (t, args)

-- | Build the reflected function definition(s) that correspond(s) to
-- a provided unqualifed name
buildFunDefns :: IState -> Name -> [RFunDefn Term]
buildFunDefns ist n =
  [ mkFunDefn name clauses
  | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist
  ]

  where mkFunDefn name clauses = RDefineFun name (map mkFunClause clauses)

        mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs
        mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs
        mkFunClause (((n, ty) : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where
          bind Impossible = Impossible
          bind tm = Bind n (PVar RigW ty) tm

-- | Build the reflected datatype definition(s) that correspond(s) to
-- a provided unqualified name
buildDatatypes :: IState -> Name -> [RDatatype]
buildDatatypes ist n =
  catMaybes [ mkDataType dn ti
            | (dn, ti) <- lookupCtxtName n datatypes
            ]
  where datatypes = idris_datatypes ist
        ctxt      = tt_ctxt ist
        impls     = idris_implicits ist

        ctorSig params cn = do cty <- fmap forget (lookupTyExact cn ctxt)
                               argInfo <- lookupCtxtExact cn impls
                               let (args, res) = getArgs argInfo cty
                               return (cn, ctorArgsStatus args res params, res)

        argPos n [] res = findPos n res
          where findPos n app = case unApplyRaw app of
                                  (_, argL) -> findIndex (== Var n) argL
        argPos n (arg:args) res = if n == argName arg
                                     then Nothing
                                     else argPos n args res

        ctorArgsStatus :: [RFunArg] -> Raw -> [Int] -> [RCtorArg]
        ctorArgsStatus [] _ _ = []
        ctorArgsStatus (arg:args) res params =
          case argPos (argName arg) args res of
            Nothing -> RCtorField arg : ctorArgsStatus args res params
            Just i -> if i `elem` params
                         then RCtorParameter arg : ctorArgsStatus args res params
                         else RCtorField arg : ctorArgsStatus args res params

        mkDataType name (TI {param_pos = params, con_names = constrs}) =
          do (TyDecl (TCon _ _) ty) <- lookupDefExact name ctxt
             implInfo <- lookupCtxtExact name impls
             let (tcargs, tcres) = getTCArgs params implInfo (forget ty)
             ctors <- mapM (ctorSig params) constrs
             return $ RDatatype name tcargs tcres ctors

        getTCArgs :: [Int] -> [PArg] -> Raw -> ([RTyConArg], Raw)
        getTCArgs params implInfo tcTy =
          let (args, res) = getArgs implInfo tcTy
          in (tcArg args 0, res)
            where tcArg [] _ = []
                  tcArg (arg:args) i | i `elem` params = RParameter arg : tcArg args (i+1)
                                     | otherwise       = RIndex arg : tcArg args (i+1)


reflectErasure :: RErasure -> Raw
reflectErasure RErased    = Var (tacN "Erased")
reflectErasure RNotErased = Var (tacN "NotErased")

reflectPlicity :: RPlicity -> Raw
reflectPlicity RExplicit = Var (tacN "Explicit")
reflectPlicity RImplicit = Var (tacN "Implicit")
reflectPlicity RConstraint = Var (tacN "Constraint")

reflectArg :: RFunArg -> Raw
reflectArg (RFunArg n ty plic erasure) =
  RApp (RApp (RApp (RApp (Var $ tacN "MkFunArg") (reflectName n))
                   (reflectRaw ty))
              (reflectPlicity plic))
       (reflectErasure erasure)

reflectCtorArg :: RCtorArg -> Raw
reflectCtorArg (RCtorParameter arg) = RApp (Var $ tacN "CtorParameter") (reflectArg arg)
reflectCtorArg (RCtorField arg) = RApp (Var $ tacN "CtorField") (reflectArg arg)

reflectDatatype :: RDatatype -> Raw
reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =
  raw_apply (Var $ tacN "MkDatatype") [ reflectName tyn
                                      , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)
                                      , reflectRaw tyConRes
                                      , rawList (rawTripleTy (Var $ reflm "TTName")
                                                             (RApp (Var (sNS (sUN "List") ["List", "Prelude"]))
                                                                   (Var $ tacN "CtorArg"))
                                                             (Var $ reflm "Raw"))
                                                [ rawTriple ((Var $ reflm "TTName")
                                                            ,(RApp (Var (sNS (sUN "List") ["List", "Prelude"]))
                                                                   (Var $ tacN "CtorArg"))
                                                            ,(Var $ reflm "Raw"))
                                                            (reflectName cn
                                                            ,rawList (Var $ tacN "CtorArg")
                                                                     (map reflectCtorArg cargs)
                                                            ,reflectRaw cty)
                                                | (cn, cargs, cty) <- constrs
                                                ]
                                      ]
  where reflectConArg (RParameter a) =
          RApp (Var $ tacN "TyConParameter") (reflectArg a)
        reflectConArg (RIndex a) =
          RApp (Var $ tacN "TyConIndex") (reflectArg a)

reflectFunClause :: RFunClause Term -> Raw
reflectFunClause (RMkFunClause lhs rhs)    = raw_apply (Var $ tacN "MkFunClause")
                                                     $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]

reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause")
                                                       [ Var $ reflm "TT", reflect lhs ]

reflectFunDefn :: RFunDefn Term -> Raw
reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun")
                                                     [ Var $ reflm "TT"
                                                     , reflectName name
                                                     , rawList (RApp (Var $ tacN "FunClause")
                                                                     (Var $ reflm "TT"))
                                                               (map reflectFunClause clauses)
                                                     ]