{-| Module : Idris.Elab.Data Description : Code to elaborate data structures. Copyright : License : BSD3 Maintainer : The Idris Community. -} {-# 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.Rewrite 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 logElab 1 (show (fc, doc)) checkUndefined fc n when (implicitable (nsroot 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 logElab 1 (show fc) undef <- isUndefined fc n when (implicitable (nsroot 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 let as = map (const (Left (Msg ""))) (getArgTys cty) ctxt <- getContext let params = findParams n (normalise ctxt [] cty) (map snd cons) logElab 2 $ "Parameters : " ++ show params addParamConstraints fc params cty cons i <- getIState -- 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 -- create a rewriting lemma when (n /= sUN "=") $ elabRewriteLemma info n cty -- Emit highlighting info sendHighlighting $ [(nfc, AnnName n Nothing Nothing Nothing)] ++ map (\(_, _, n, nfc, _, _, _) -> (nfc, AnnName n Nothing Nothing Nothing)) dcons where 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 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 (nsroot n)) $ warnLC fc n logElab 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 -- Check that the constructor type is, in fact, a part of the family being defined tyIs n cty' logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t logElab 5 $ "Inaccessible args: " ++ show inacc logElab 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 (substV (P Bound n Erased) sc) tyIs con t | (P Bound n' _, _) <- unApply t = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con Nothing (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn)))) else return () 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 "Delayed")) [pexp (PRef fc [] (sUN "Infinite")), 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 () addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris () addParamConstraints fc ps cty cons = case getRetTy cty of TType cvar -> mapM_ (addConConstraint ps cvar) (map getParamNames cons) _ -> return () where getParamNames (n, ty) = (ty, getPs ty) getPs (Bind n (Pi _ _ _) sc) = getPs (substV (P Ref n Erased) sc) getPs t | (f, args) <- unApply t = paramArgs 0 args paramArgs i (P _ n _ : args) | i `elem` ps = n : paramArgs (i + 1) args paramArgs i (_ : args) = paramArgs (i + 1) args paramArgs i [] = [] addConConstraint ps cvar (ty, pnames) = constraintTy ty where constraintTy (Bind n (Pi _ ty _) sc) = case getRetTy ty of TType avar -> do tit <- typeInType when (not tit) $ do ctxt <- getContext let tv = next_tvar ctxt let con = if n `elem` pnames then ULE avar cvar else ULT avar cvar addConstraints fc (tv, [con]) addIBC (IBCConstraint fc con) _ -> return () constraintTy t = 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 elimFC 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 elimFC [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 elimFC 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 (logElab 2 s) elimFC :: FC elimFC = fileFC $ "(casefun " ++ show n ++ ")" elimDeclName :: Name elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ 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 elimFC 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