{-# LANGUAGE PatternGuards #-}
module Idris.Elab.Data(elabData) where

import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.DSL
import Idris.Error
import Idris.Delaborate
import Idris.Imports
import Idris.Elab.Term
import Idris.Coverage
import Idris.DataOpts
import Idris.Providers
import Idris.Primitives
import Idris.Inliner
import Idris.PartialEval
import Idris.DeepSeq
import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)
import IRTS.Lang

import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Elab.Value

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

import Idris.Docstrings

import Prelude hiding (id, (.))
import Control.Category

import Control.Applicative hiding (Const)
import Control.DeepSeq
import Control.Monad
import Control.Monad.State.Strict as State
import Data.List
import Data.Maybe
import Debug.Trace

import qualified Data.Map as Map
import qualified Data.Set as S
import qualified Data.Text as T
import Data.Char(isLetter, toLower)
import Data.List.Split (splitOn)

import Util.Pretty

warnLC :: FC -> Name -> Idris ()
warnLC fc n 
   = iWarn fc $ annName n <+> text "has a name which may be implicitly bound."
           <> line <> text "This is likely to lead to problems!"

elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()
elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)
    = do let codata = Codata `elem` opts
         logLvl 1 (show (fc, doc))
         checkUndefined fc n
         when (implicitable n) $ warnLC fc n
         (cty, _, t, inacc) <- buildType info syn fc [] n t_in

         addIBC (IBCDef n)
         updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
         sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
    = do let codata = Codata `elem` opts
         logLvl 1 (show fc)
         undef <- isUndefined fc n
         when (implicitable n) $ warnLC fc n
         (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in
         -- if n is defined already, make sure it is just a type declaration
         -- with the same type we've just elaborated, and no constructors
         -- yet
         i <- getIState
         checkDefinedAs fc n cty i
         -- temporary, to check cons
         when undef $ updateContext (addTyDecl n (TCon 0 0) cty)
         let cnameinfo = cinfo info (map cname dcons)
         unique <- case getRetTy (normalise (tt_ctxt i) [] cty) of
                        UType UniqueType -> return True
                        UType _ -> return False
                        TType _ -> return False
                        rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))
         cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
         ttag <- getName
         i <- getIState
         let as = map (const (Left (Msg ""))) (getArgTys cty)
         let params = findParams  (map snd cons)
         logLvl 2 $ "Parameters : " ++ show params
         -- TI contains information about mutually declared types - this will
         -- be updated when the mutual block is complete
         putIState (i { idris_datatypes =
                          addDef n (TI (map fst cons) codata opts params [n])
                                             (idris_datatypes i) })
         addIBC (IBCDef n)
         addIBC (IBCData n)
         checkDocs fc argDocs t
         doc' <- elabDocTerms info doc
         argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
                                         return (n, d')) argDocs
         addDocStr n doc' argDocs'
         addIBC (IBCDoc n)
         let metainf = DataMI params
         addIBC (IBCMetaInformation n metainf)
         -- TMP HACK! Make this a data option
         updateContext (addDatatype (Data n ttag cty unique cons))
         updateContext (setMetaInformation n metainf)
         mapM_ totcheck (zip (repeat fc) (map fst cons))
--          mapM_ (checkPositive n) cons

         -- if there's exactly one constructor,
         -- mark both the type and the constructor as detaggable
         case cons of
            [(cn,ct)] -> setDetaggable cn >> setDetaggable n
                >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
            _ -> return ()

         -- create an eliminator
         when (DefaultEliminator `elem` opts) $
            evalStateT (elabCaseFun True params n t dcons info) Map.empty
         -- create a case function
         when (DefaultCaseFun `elem` opts) $
            evalStateT (elabCaseFun False params n t dcons info) Map.empty
         -- Emit highlighting info
         sendHighlighting $ [(nfc, AnnName n Nothing Nothing Nothing)] ++
           map (\(_, _, n, nfc, _, _, _) ->
                 (nfc, AnnName n Nothing Nothing Nothing))
               dcons
  where
        setDetaggable :: Name -> Idris ()
        setDetaggable n = do
            ist <- getIState
            let opt = idris_optimisation ist
            case lookupCtxt n opt of
                [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
                _    -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }

        checkDefinedAs fc n t i
            = let defined = tclift $ tfail (At fc (AlreadyDefined n))
                  ctxt = tt_ctxt i in
                case lookupDef n ctxt of
                   [] -> return ()
                   [TyDecl _ ty] ->
                      case converts ctxt [] t ty of
                           OK () -> case lookupCtxtExact n (idris_datatypes i) of
                                         Nothing -> return ()
                                         _ -> defined
                           _ -> defined
                   _ -> defined
        -- parameters are names which are unchanged across the structure,
        -- which appear exactly once in the return type of a constructor

        -- First, find all applications of the constructor, then check over
        -- them for repeated arguments

        findParams :: [Type] -> [Int]
        findParams ts = let allapps = map getDataApp ts
           -- do each constructor separately, then merge the results (names
           -- may change between constructors)
                            conParams = map paramPos allapps in
                            inAll conParams

        inAll :: [[Int]] -> [Int]
        inAll [] = []
        inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x

        paramPos [] = []
        paramPos (args : rest)
              = dropNothing $ keepSame (zip [0..] args) rest

        dropNothing [] = []
        dropNothing ((x, Nothing) : ts) = dropNothing ts
        dropNothing ((x, _) : ts) = x : dropNothing ts

        keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
                    [(Int, Maybe Name)]
        keepSame as [] = as
        keepSame as (args : rest) = keepSame (update as args) rest
          where
            update [] _ = []
            update _ [] = []
            update ((n, Just x) : as) (Just x' : args)
                | x == x' = (n, Just x) : update as args
            update ((n, _) : as) (_ : args) = (n, Nothing) : update as args

        getDataApp :: Type -> [[Maybe Name]]
        getDataApp f@(App _ _ _)
            | (P _ d _, args) <- unApply f
                   = if (d == n) then [mParam args args] else []
        getDataApp (Bind n (Pi _ t _) sc)
            = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
        getDataApp _ = []

        -- keep the arguments which are single names, which don't appear
        -- elsewhere

        mParam args [] = []
        mParam args (P Bound n _ : rest)
               | count n args == 1
                  = Just n : mParam args rest
            where count n [] = 0
                  count n (t : ts)
                       | n `elem` freeNames t = 1 + count n ts
                       | otherwise = count n ts
        mParam args (_ : rest) = Nothing : mParam args rest

        cname (_, _, n, _, _, _, _) = n

        -- Abuse of ElabInfo.
        -- TODO Contemplate whether the ElabInfo type needs modification.
        cinfo :: ElabInfo -> [Name] -> ElabInfo
        cinfo info ds
          = let newps = params info
                dsParams = map (\n -> (n, [])) ds
                newb = addAlist dsParams (inblock info)
                l = liftname info in
                info { params = newps,
                       inblock = newb,
                       liftname = id -- Is this appropriate?
                     }

elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
           Type -> -- for unique kind checking
           Type -> -- data type's kind
           (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) ->
           Idris (Name, Type)
elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcenames)
    = do checkUndefined fc n
         when (implicitable n) $ warnLC fc n
         logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
         (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
         ctxt <- getContext
         let cty' = normalise ctxt [] cty
         checkUniqueKind ckind expkind
         addDataConstraint ckind dkind

         -- Check that the constructor type is, in fact, a part of the family being defined
         tyIs n cty'

         logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t
         logLvl 5 $ "Inaccessible args: " ++ show inacc
         logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

         -- Add to the context (this is temporary, so that later constructors
         -- can be indexed by it)
         updateContext (addTyDecl n (DCon 0 0 False) cty) 

         addIBC (IBCDef n)
         checkDocs fc argDocs t
         doc' <- elabDocTerms info doc
         argDocs' <- mapM (\(n, d) -> do d' <- elabDocTerms info d
                                         return (n, d')) argDocs
         addDocStr n doc' argDocs'
         addIBC (IBCDoc n)
         fputState (opt_inaccessible . ist_optimisation n) inacc
         addIBC (IBCOpt n)
         return (n, cty')
  where
    tyIs con (Bind n b sc) = tyIs con sc
    tyIs con t | (P _ n' _, _) <- unApply t
        = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show n' ++ " is not " ++ show tn))))
             else return ()
    tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg (show t ++ " is not " ++ show tn))))

    mkLazy (PPi pl n nfc ty sc)
        = let ty' = if getTyName ty
                       then PApp fc (PRef fc [] (sUN "Lazy'"))
                            [pexp (PRef fc [] (sUN "LazyCodata")),
                             pexp ty]
                       else ty in
              PPi pl n nfc ty' (mkLazy sc)
    mkLazy t = t

    getTyName (PApp _ (PRef _ _ n) _) = n == nsroot tn
    getTyName (PRef _ _ n) = n == nsroot tn
    getTyName _ = False


    getNamePos :: Int -> PTerm -> Name -> Maybe Int
    getNamePos i (PPi _ n _ _ sc) x | n == x = Just i
                                    | otherwise = getNamePos (i + 1) sc x
    getNamePos _ _ _ = Nothing

    -- if the constructor is a UniqueType, the datatype must be too
    -- (AnyType is fine, since that is checked for uniqueness too)
    -- if hte contructor is AnyType, the datatype must be at least AnyType
    checkUniqueKind (UType NullType) (UType NullType) = return ()
    checkUniqueKind (UType NullType) _
        = tclift $ tfail (At fc (UniqueKindError NullType n))
    checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()
    checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()
    checkUniqueKind (UType UniqueType) _
        = tclift $ tfail (At fc (UniqueKindError UniqueType n))
    checkUniqueKind (UType AllTypes) (UType AllTypes) = return ()
    checkUniqueKind (UType AllTypes) (UType UniqueType) = return ()
    checkUniqueKind (UType AllTypes) _ 
        = tclift $ tfail (At fc (UniqueKindError AllTypes n))
    checkUniqueKind _ _ = return ()

    -- Constructor's kind must be <= expected kind
    addDataConstraint (TType con) (TType exp) 
       = do ctxt <- getContext
            let v = next_tvar ctxt
            addConstraints fc (v, [ULT con exp])
    addDataConstraint _ _ = return ()

type EliminatorState = StateT (Map.Map String Int) Idris

-- -- Issue #1616 in the issue tracker.
--     https://github.com/idris-lang/Idris-dev/issues/1616
--
-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function
-- rename to caseFun to match updated intend
elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->
                  [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])] ->
                  ElabInfo -> EliminatorState ()
elabCaseFun ind paramPos n ty cons info = do
  elimLog $ "Elaborating case function"
  put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
  let (cnstrs, _) = splitPi ty
  let (splittedTy@(pms, idxs)) = splitPms cnstrs
  generalParams <- namePis False pms
  motiveIdxs    <- namePis False idxs
  let motive = mkMotive n paramPos generalParams motiveIdxs
  consTerms <- mapM (\(c@(_, _, cnm, _, _, _, _)) -> do
                               let casefunt = if ind then "elim_" else "case_"
                               name <- freshName $ casefunt ++ simpleName cnm
                               consTerm <- extractConsTerm c generalParams
                               return (name, expl, consTerm)) cons
  scrutineeIdxs <- namePis False idxs
  let motiveConstr = [(motiveName, expl, motive)]
  let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
  let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC [] n) scrutineeIdxs) (PRef elimFC [] scrutineeName))
  let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName NoFC eliminatorTy
  let clauseConsElimArgs = map getPiName consTerms
  let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
  let clauseGeneralArgs  = map (\arg -> pexp (PRef elimFC [] arg)) clauseGeneralArgs'
  let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy
  elimLog elimSig
  eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
  let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
  elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
  State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)
                    (ierror . Elaborating "type declaration of " elimDeclName Nothing)
  -- Do not elaborate clauses if there aren't any
  case eliminatorClauses of
    [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
    _  -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
                    (ierror . Elaborating "clauses of " elimDeclName Nothing)
  where elimLog :: String -> EliminatorState ()
        elimLog s = State.lift (logLvl 2 s)

        elimFC :: FC
        elimFC = fileFC "(casefun)"

        elimDeclName :: Name
        elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' emptyFC) $ n

        applyNS :: Name -> [String] -> Name
        applyNS n []  = n
        applyNS n ns  = sNS n ns

        splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
        splitPi = splitPi' []
          where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
                splitPi' acc (PPi pl n _ tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
                splitPi' acc t                    = (reverse acc, t)

        splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])
        splitPms cnstrs = (map fst pms, map fst idxs)
           where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])

        isMachineGenerated :: Name -> Bool
        isMachineGenerated (MN _ _) = True
        isMachineGenerated _        = False

        namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]
        namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms
                                 let oldNames = map fst names
                                 let params   = map snd names
                                 return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params

        mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))
        mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))
        mkPiName _ (oldName, pl, piarg) =  do name <- freshName $ keyOf piarg
                                              return (oldName, (name, pl, piarg))
          where keyOf :: PTerm -> String
                keyOf (PRef _ _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"
                keyOf (PApp _ tyf _) = keyOf tyf
                keyOf (PType _) = "ty__"
                keyOf _     = "carg__"
                nameStart :: Name -> Char
                nameStart n = nameStart' (simpleName n)
                  where nameStart' :: String -> Char
                        nameStart' "" = ' '
                        nameStart' ns = head ns

        simpleName :: Name -> String
        simpleName (NS n _) = simpleName n
        simpleName (MN i n) = str n ++ show i
        simpleName n        = show n

        nameSpaces :: Name -> [String]
        nameSpaces (NS _ ns) = map str ns
        nameSpaces _         = []

        freshName :: String -> EliminatorState Name
        freshName key = do
          nameMap <- get
          let i = fromMaybe 0 (Map.lookup key nameMap)
          let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)
          put $ Map.insert key (i+1) nameMap
          return name

        scrutineeName :: Name
        scrutineeName = sUN "scrutinee"

        scrutineeArgName :: Name
        scrutineeArgName = sUN "scrutineeArg"

        motiveName :: Name
        motiveName = sUN "prop"

        mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
        mkMotive n paramPos params indicies =
          let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))
          in piConstr (indicies ++ [scrutineeTy]) (PType elimFC)

        piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm
        piConstr [] ty = ty
        piConstr ((n, pl, tyb):tyr) ty = PPi pl n NoFC tyb (piConstr tyr ty)

        interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]
        interlievePos idxs []     l2     i = l2
        interlievePos idxs l1     []     i = l1
        interlievePos idxs (x:xs) l2     i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))
        interlievePos idxs l1     (y:ys) i = y:(interlievePos idxs l1 ys (i+1))

        replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
        replaceParams paramPos params cns =
          let (_, cnsResTy) = splitPi cns
          in case cnsResTy of
               PApp _ _ args ->
                let oldParams = paramNamesOf 0 paramPos args
                in removeParamPis oldParams params cns
               _ -> cns

        removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
        removeParamPis oldParams params (PPi pl n fc tyb tyr) =
          case findIndex (== n) oldParams of
            Nothing -> (PPi pl n fc (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
            Just i  -> (removeParamPis oldParams params tyr)
        removeParamPis oldParams params (PRef _ _ n) =
          case findIndex (== n) oldParams of
               Nothing -> (PRef elimFC [] n)
               Just i  -> let (newname,_,_) = params !! i in (PRef elimFC [] (newname))
        removeParamPis oldParams params (PApp _ cns args) =
          PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args
            where replaceParamArgs :: [PArg] -> [PArg]
                  replaceParamArgs []          = []
                  replaceParamArgs (arg:args)  =
                    case extractName (getTm arg) of
                      []   -> arg:replaceParamArgs args
                      [n]  ->
                        case findIndex (== n) oldParams of
                          Nothing -> arg:replaceParamArgs args
                          Just i  -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC [] newname}:replaceParamArgs args
        removeParamPis oldParams params t = t

        paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]
        paramNamesOf i paramPos []          = []
        paramNamesOf i paramPos (arg:args)  = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args

        extractName :: PTerm -> [Name]
        extractName (PRef _ _ n) = [n]
        extractName _            = []

        splitArgPms :: PTerm -> ([PTerm], [PTerm])
        splitArgPms (PApp _ f args) = splitArgPms' args
          where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])
                splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)
                    where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
        splitArgPms _                 = ([],[])


        implicitIndexes :: (Docstring (Either Err PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
        implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
          i <-  State.lift getIState
          implargs' <- case lookupCtxt cnm (idris_implicits i) of
            [] -> do fail $ "Error while showing implicits for " ++ show cnm
            [args] -> do return args
            _ -> do fail $ "Ambigous name for " ++ show cnm
          let implargs = mapMaybe convertImplPi implargs'
          let (_, cnsResTy) = splitPi ty
          case cnsResTy of
             PApp _ _ args ->
              let oldParams = paramNamesOf 0 paramPos args
              in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
             _ -> return implargs

        extractConsTerm :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
        extractConsTerm (doc, argDocs, cnm, _, ty, fc, fs) generalParameters = do
          let cons' = replaceParams paramPos generalParameters ty
          let (args, resTy) = splitPi cons'
          implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
          consArgs <- namePis False args
          let recArgs = findRecArgs consArgs
          let recMotives = if ind then map applyRecMotive recArgs else []
          let (_, consIdxs) = splitArgPms resTy
          return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
            where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
                  applyRecMotive (n,_,ty)  = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC [] n))
                      where (_, idxs) = splitArgPms ty

        findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
        findRecArgs []                            = []
        findRecArgs (ty@(_,_,PRef _ _ tn):rs)            | simpleName tn == simpleName n = ty:findRecArgs rs
        findRecArgs (ty@(_,_,PApp _ (PRef _ _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
        findRecArgs (ty:rs)                                                              = findRecArgs rs

        applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm
        applyCons tn targs = PApp elimFC (PRef elimFC [] tn) (map convertArg targs)

        convertArg :: (Name, Plicity, PTerm) -> PArg
        convertArg (n, _, _)      = pexp (PRef elimFC [] n)

        applyMotive :: [PTerm] -> PTerm -> PTerm
        applyMotive idxs t = PApp elimFC (PRef elimFC [] motiveName) (map pexp idxs ++ [pexp t])

        getPiName :: (Name, Plicity, PTerm) -> Name
        getPiName (name,_,_) = name

        convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)
        convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
        convertImplPi _                             = Nothing

        generateEliminatorClauses :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
        generateEliminatorClauses (doc, _, cnm, _, ty, fc, fs) cnsElim generalArgs generalParameters = do
          let cons' = replaceParams paramPos generalParameters ty
          let (args, resTy) = splitPi cons'
          i <- State.lift getIState
          implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
          let (_, generalIdxs') = splitArgPms resTy
          let generalIdxs = map pexp generalIdxs'
          consArgs <- namePis False args
          let lhsPattern = PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
          let recArgs = findRecArgs consArgs
          let recElims = if ind then map applyRecElim recArgs else []
          let rhsExpr    = PApp elimFC (PRef elimFC [] cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)
          return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []
            where applyRecElim :: (Name, Plicity, PTerm) -> PArg
                  applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC [] recCnm])
                    where (_, idxs) = splitArgPms recTy