@@ -110,12 +110,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
110110 >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
111111 _ -> return ()
112112
113− -- create an eliminator
114− when (DefaultEliminator `elem` opts) $
115− evalStateT (elabCaseFun True params n t dcons info) Map.empty
116− -- create a case function
117− when (DefaultCaseFun `elem` opts) $
118− evalStateT (elabCaseFun False params n t dcons info) Map.empty
119113 -- create a rewriting lemma
120114 when (n /= sUN "=") $
121115 elabRewriteLemma info n cty
@@ -312,244 +306,3 @@ addParamConstraints fc ps cty cons
312306 addIBC (IBCConstraint fc con)
313307 _ -> return ()
314308 constraintTy t = return ()
315−
316−type EliminatorState = StateT (Map.Map String Int) Idris
317−
318−-- -- Issue #1616 in the issue tracker.
319−-- https://github.com/idris-lang/Idris-dev/issues/1616
320−--
321−-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)
322−-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function
323−-- rename to caseFun to match updated intend
324−elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->
325− [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])] ->
326− ElabInfo -> EliminatorState ()
327−elabCaseFun ind paramPos n ty cons info = do
328− elimLog "Elaborating case function"
329− put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
330− let (cnstrs, _) = splitPi ty
331− let (pms, idxs) = splitPms cnstrs
332− generalParams <- namePis False pms
333− motiveIdxs <- namePis False idxs
334− let motive = mkMotive n paramPos generalParams motiveIdxs
335− consTerms <- mapM (\(c@(_, _, cnm, _, _, _, _)) -> do
336− let casefunt = if ind then "elim_" else "case_"
337− name <- freshName $ casefunt ++ simpleName cnm
338− consTerm <- extractConsTerm c generalParams
339− return (name, expl, consTerm)) cons
340− scrutineeIdxs <- namePis False idxs
341− let motiveConstr = [(motiveName, expl, motive)]
342− let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
343− let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC [] n) scrutineeIdxs) (PRef elimFC [] scrutineeName))
344− let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName elimFC eliminatorTy
345− let clauseConsElimArgs = map getPiName consTerms
346− let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
347− let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC [] arg)) clauseGeneralArgs'
348− let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy
349− elimLog elimSig
350− eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
351− let eliminatorDef = PClauses elimFC [TotalFn] elimDeclName eliminatorClauses
352− elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
353− State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)
354− (ierror . Elaborating "type declaration of " elimDeclName Nothing)
355− -- Do not elaborate clauses if there aren't any
356− case eliminatorClauses of
357− [] -> State.lift $ solveDeferred elimFC elimDeclName -- Remove meta-variable for type
358− _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
359− (ierror . Elaborating "clauses of " elimDeclName Nothing)
360− where elimLog :: String -> EliminatorState ()
361− elimLog s = State.lift (logElab 2 s)
362−
363− elimFC :: FC
364− elimFC = fileFC $ "(casefun " ++ show n ++ ")"
365−
366− elimDeclName :: Name
367− elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n
368−
369− splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
370− splitPi = splitPi' []
371− where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
372− splitPi' acc (PPi pl n _ tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
373− splitPi' acc t = (reverse acc, t)
374−
375− splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])
376− splitPms cnstrs = (map fst pms, map fst idxs)
377− where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
378−
379− isMachineGenerated :: Name -> Bool
380− isMachineGenerated (MN _ _) = True
381− isMachineGenerated _ = False
382−
383− namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]
384− namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms
385− let oldNames = map fst names
386− let params = map snd names
387− return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params
388−
389− mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))
390− mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))
391− mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg
392− return (oldName, (name, pl, piarg))
393− where keyOf :: PTerm -> String
394− keyOf (PRef _ _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"
395− keyOf (PApp _ tyf _) = keyOf tyf
396− keyOf (PType _) = "ty__"
397− keyOf _ = "carg__"
398− nameStart :: Name -> Char
399− nameStart n = nameStart' (simpleName n)
400− where nameStart' :: String -> Char
401− nameStart' "" = ' '
402− nameStart' ns = head ns
403−
404− simpleName :: Name -> String
405− simpleName (NS n _) = simpleName n
406− simpleName (MN i n) = str n ++ show i
407− simpleName n = show n
408−
409− freshName :: String -> EliminatorState Name
410− freshName key = do
411− nameMap <- get
412− let i = fromMaybe 0 (Map.lookup key nameMap)
413− let name = uniqueName (sUN (key ++ show i)) (map (\(nm, nb) -> sUN (nm ++ show nb)) $ Map.toList nameMap)
414− put $ Map.insert key (i+1) nameMap
415− return name
416−
417− scrutineeName :: Name
418− scrutineeName = sUN "scrutinee"
419−
420− scrutineeArgName :: Name
421− scrutineeArgName = sUN "scrutineeArg"
422−
423− motiveName :: Name
424− motiveName = sUN "prop"
425−
426− mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
427− mkMotive n paramPos params indicies =
428− let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))
429− in piConstr (indicies ++ [scrutineeTy]) (PType elimFC)
430−
431− piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm
432− piConstr [] ty = ty
433− piConstr ((n, pl, tyb):tyr) ty = PPi pl n elimFC tyb (piConstr tyr ty)
434−
435− interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]
436− interlievePos idxs [] l2 i = l2
437− interlievePos idxs l1 [] i = l1
438− interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))
439− interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))
440−
441− replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
442− replaceParams paramPos params cns =
443− let (_, cnsResTy) = splitPi cns
444− in case cnsResTy of
445− PApp _ _ args ->
446− let oldParams = paramNamesOf 0 paramPos args
447− in removeParamPis oldParams params cns
448− _ -> cns
449−
450− removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
451− removeParamPis oldParams params (PPi pl n fc tyb tyr) =
452− case findIndex (== n) oldParams of
453− Nothing -> (PPi pl n fc (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
454− Just i -> (removeParamPis oldParams params tyr)
455− removeParamPis oldParams params (PRef _ _ n) =
456− case findIndex (== n) oldParams of
457− Nothing -> (PRef elimFC [] n)
458− Just i -> let (newname,_,_) = params !! i in (PRef elimFC [] (newname))
459− removeParamPis oldParams params (PApp _ cns args) =
460− PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args
461− where replaceParamArgs :: [PArg] -> [PArg]
462− replaceParamArgs [] = []
463− replaceParamArgs (arg:args) =
464− case extractName (getTm arg) of
465− [] -> arg:replaceParamArgs args
466− [n] ->
467− case findIndex (== n) oldParams of
468− Nothing -> arg:replaceParamArgs args
469− Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC [] newname}:replaceParamArgs args
470− removeParamPis oldParams params t = t
471−
472− paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]
473− paramNamesOf i paramPos [] = []
474− paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args
475−
476− extractName :: PTerm -> [Name]
477− extractName (PRef _ _ n) = [n]
478− extractName _ = []
479−
480− splitArgPms :: PTerm -> ([PTerm], [PTerm])
481− splitArgPms (PApp _ f args) = splitArgPms' args
482− where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])
483− splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)
484− where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
485− splitArgPms _ = ([],[])
486−
487−
488− implicitIndexes :: (Docstring (Either Err PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]
489− implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do
490− i <- State.lift getIState
491− implargs' <- case lookupCtxt cnm (idris_implicits i) of
492− [] -> do fail $ "Error while showing implicits for " ++ show cnm
493− [args] -> do return args
494− _ -> do fail $ "Ambigous name for " ++ show cnm
495− let implargs = mapMaybe convertImplPi implargs'
496− let (_, cnsResTy) = splitPi ty
497− case cnsResTy of
498− PApp _ _ args ->
499− let oldParams = paramNamesOf 0 paramPos args
500− in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
501− _ -> return implargs
502−
503− extractConsTerm :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
504− extractConsTerm (doc, argDocs, cnm, _, ty, fc, fs) generalParameters = do
505− let cons' = replaceParams paramPos generalParameters ty
506− let (args, resTy) = splitPi cons'
507− implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
508− consArgs <- namePis False args
509− let recArgs = findRecArgs consArgs
510− let recMotives = if ind then map applyRecMotive recArgs else []
511− let (_, consIdxs) = splitArgPms resTy
512− return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
513− where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
514− applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC [] n))
515− where (_, idxs) = splitArgPms ty
516−
517− findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
518− findRecArgs [] = []
519− findRecArgs (ty@(_,_,PRef _ _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
520− findRecArgs (ty@(_,_,PApp _ (PRef _ _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
521− findRecArgs (ty:rs) = findRecArgs rs
522−
523− applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm
524− applyCons tn targs = PApp elimFC (PRef elimFC [] tn) (map convertArg targs)
525−
526− convertArg :: (Name, Plicity, PTerm) -> PArg
527− convertArg (n, _, _) = pexp (PRef elimFC [] n)
528−
529− applyMotive :: [PTerm] -> PTerm -> PTerm
530− applyMotive idxs t = PApp elimFC (PRef elimFC [] motiveName) (map pexp idxs ++ [pexp t])
531−
532− getPiName :: (Name, Plicity, PTerm) -> Name
533− getPiName (name,_,_) = name
534−
535− convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)
536− convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
537− convertImplPi _ = Nothing
538−
539− generateEliminatorClauses :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
540− generateEliminatorClauses (doc, _, cnm, _, ty, fc, fs) cnsElim generalArgs generalParameters = do
541− let cons' = replaceParams paramPos generalParameters ty
542− let (args, resTy) = splitPi cons'
543− i <- State.lift getIState
544− implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)
545− let (_, generalIdxs') = splitArgPms resTy
546− let generalIdxs = map pexp generalIdxs'
547− consArgs <- namePis False args
548− let lhsPattern = PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
549− let recArgs = findRecArgs consArgs
550− let recElims = if ind then map applyRecElim recArgs else []
551− let rhsExpr = PApp elimFC (PRef elimFC [] cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)
552− return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []
553− where applyRecElim :: (Name, Plicity, PTerm) -> PArg
554− applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC [] recCnm])
555− where (_, idxs) = splitArgPms recTy