@@ -7,6 +7,7 @@ module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), Eras
77
88import Idris.Core.TT
99
10+import Control.Applicative hiding (Const)
1011import Control.Monad.State
1112import Control.Monad.Reader
1213import Data.Maybe
@@ -483,6 +484,12 @@ mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
483484mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
484485 varRule vs ms fallthrough
485486
487+-- Return the list of inaccessible arguments of a data constructor.
488+inaccessibleArgs :: Name -> CaseBuilder [Int]
489+inaccessibleArgs n = do
490+ getInaccessiblePositions <- ask -- this function is the only thing in the environment
491+ return $ getInaccessiblePositions n
492+
486493data ConType = CName Name Int -- named constructor
487494 | CFn Name -- reflected function name
488495 | CSuc -- n+1
@@ -502,41 +509,44 @@ caseGroups (v:vs) gs err = do g <- altGroups gs
502509 return $ Case v (sort g)
503510 where
504511 altGroups [] = return [DefaultCase err]
512+
505513 altGroups (ConGroup (CName n i) args : cs)
506− = do g <- altGroup n i args
507− rest <- altGroups cs
508− return (g : rest)
514+ = (:) <$> altGroup n i args <*> altGroups cs
515+
509516 altGroups (ConGroup (CFn n) args : cs)
510− = do g <- altFnGroup n args
511− rest <- altGroups cs
512− return (g : rest)
517+ = (:) <$> altFnGroup n args <*> altGroups cs
518+
513519 altGroups (ConGroup CSuc args : cs)
514− = do g <- altSucGroup args
515− rest <- altGroups cs
516− return (g : rest)
520+ = (:) <$> altSucGroup args <*> altGroups cs
521+
517522 altGroups (ConGroup (CConst c) args : cs)
518− = do g <- altConstGroup c args
519− rest <- altGroups cs
520− return (g : rest)
521−
522− altGroup n i gs = do (newArgs, nextCs) <- argsToAlt gs
523− matchCs <- match (newArgs ++ vs) nextCs err
524− return $ ConCase n i newArgs matchCs
525− altFnGroup n gs = do (newArgs, nextCs) <- argsToAlt gs
526− matchCs <- match (newArgs ++ vs) nextCs err
527− return $ FnCase n newArgs matchCs
528− altSucGroup gs = do ([newArg], nextCs) <- argsToAlt gs
529− matchCs <- match (newArg:vs) nextCs err
530− return $ SucCase newArg matchCs
531− altConstGroup n gs = do (_, nextCs) <- argsToAlt gs
532− matchCs <- match vs nextCs err
533− return $ ConstCase n matchCs
534−
535−argsToAlt :: [([Pat], Clause)] -> CaseBuilder ([Name], [Clause])
536−argsToAlt [] = return ([], [])
523+ = (:) <$> altConstGroup c args <*> altGroups cs
524+
525+ altGroup n i args = do inacc <- inaccessibleArgs n
526+ (newArgs, nextCs, [], []) <- argsToAlt args
527+ matchCs <- match (newArgs ++ vs) nextCs err
528+ return $ ConCase n i newArgs matchCs
529+
530+ altFnGroup n args = do (newArgs, nextCs, [], []) <- argsToAlt args
531+ matchCs <- match (newArgs ++ vs) nextCs err
532+ return $ FnCase n newArgs matchCs
533+
534+ altSucGroup args = do ([newArg], nextCs, [], []) <- argsToAlt args
535+ matchCs <- match (newArg:vs) nextCs err
536+ return $ SucCase newArg matchCs
537+
538+ altConstGroup n args = do (_, nextCs, [], []) <- argsToAlt args
539+ matchCs <- match vs nextCs err
540+ return $ ConstCase n matchCs
541+
542+-- Returns:
543+-- * names of accessible variables + corresponding clauses
544+-- * names of inaccessible variables + corresponding clauses
545+argsToAlt :: [([Pat], Clause)] -> CaseBuilder ([Name], [Clause], [Name], [Clause])
546+argsToAlt [] = return ([], [], [], [])
537547argsToAlt rs@((r, m) : rest)
538548 = do newArgs <- getNewVars r
539− return (newArgs, addRs rs)
549+ return (newArgs, addRs rs, [], [])
540550 where
541551 getNewVars [] = return []
542552 getNewVars ((PV n t) : ns) = do v <- getVar "e"