git.iko.soy/Idris-dev
on master help sign in
Extend argsToAlt to return a quadruple.
747aaf5Matus Tejiscak
src/Idris/Core/CaseTree.hs+39−29
compare with master
unifiedsplit
@@ -7,6 +7,7 @@ module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), Eras
7
7
8import Idris.Core.TT
8import Idris.Core.TT
9
9
10+import Control.Applicative hiding (Const)
10import Control.Monad.State
11import Control.Monad.State
11import Control.Monad.Reader
12import Control.Monad.Reader
12import Data.Maybe
13import Data.Maybe
@@ -483,6 +484,12 @@ mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
483mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
484mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
484 varRule vs ms fallthrough
485 varRule vs ms fallthrough
485
486
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+
486data ConType = CName Name Int -- named constructor
493data ConType = CName Name Int -- named constructor
487 | CFn Name -- reflected function name
494 | CFn Name -- reflected function name
488 | CSuc -- n+1
495 | CSuc -- n+1
@@ -502,41 +509,44 @@ caseGroups (v:vs) gs err = do g <- altGroups gs
502 return $ Case v (sort g)
509 return $ Case v (sort g)
503 where
510 where
504 altGroups [] = return [DefaultCase err]
511 altGroups [] = return [DefaultCase err]
512+
505 altGroups (ConGroup (CName n i) args : cs)
513 altGroups (ConGroup (CName n i) args : cs)
506− = do g <- altGroup n i args
514+ = (:) <$> altGroup n i args <*> altGroups cs
507− rest <- altGroups cs
515+
508− return (g : rest)
509 altGroups (ConGroup (CFn n) args : cs)
516 altGroups (ConGroup (CFn n) args : cs)
510− = do g <- altFnGroup n args
517+ = (:) <$> altFnGroup n args <*> altGroups cs
511− rest <- altGroups cs
518+
512− return (g : rest)
513 altGroups (ConGroup CSuc args : cs)
519 altGroups (ConGroup CSuc args : cs)
514− = do g <- altSucGroup args
520+ = (:) <$> altSucGroup args <*> altGroups cs
515− rest <- altGroups cs
521+
516− return (g : rest)
517 altGroups (ConGroup (CConst c) args : cs)
522 altGroups (ConGroup (CConst c) args : cs)
518− = do g <- altConstGroup c args
523+ = (:) <$> altConstGroup c args <*> altGroups cs
519− rest <- altGroups cs
524+
520− return (g : rest)
525+ altGroup n i args = do inacc <- inaccessibleArgs n
521−
522− altGroup n i gs = do (newArgs, nextCs) <- argsToAlt gs
526+ (newArgs, nextCs, [], []) <- argsToAlt args
523− matchCs <- match (newArgs ++ vs) nextCs err
527+ matchCs <- match (newArgs ++ vs) nextCs err
524− return $ ConCase n i newArgs matchCs
528+ return $ ConCase n i newArgs matchCs
529+
525− altFnGroup n gs = do (newArgs, nextCs) <- argsToAlt gs
530+ altFnGroup n args = do (newArgs, nextCs, [], []) <- argsToAlt args
526− matchCs <- match (newArgs ++ vs) nextCs err
531+ matchCs <- match (newArgs ++ vs) nextCs err
527− return $ FnCase n newArgs matchCs
532+ return $ FnCase n newArgs matchCs
533+
528− altSucGroup gs = do ([newArg], nextCs) <- argsToAlt gs
534+ altSucGroup args = do ([newArg], nextCs, [], []) <- argsToAlt args
529− matchCs <- match (newArg:vs) nextCs err
535+ matchCs <- match (newArg:vs) nextCs err
530− return $ SucCase newArg matchCs
536+ return $ SucCase newArg matchCs
537+
531− altConstGroup n gs = do (_, nextCs) <- argsToAlt gs
538+ altConstGroup n args = do (_, nextCs, [], []) <- argsToAlt args
532− matchCs <- match vs nextCs err
539+ matchCs <- match vs nextCs err
533− return $ ConstCase n matchCs
540+ return $ ConstCase n matchCs
534−
541+
542+-- Returns:
543+-- * names of accessible variables + corresponding clauses
544+-- * names of inaccessible variables + corresponding clauses
535−argsToAlt :: [([Pat], Clause)] -> CaseBuilder ([Name], [Clause])
545+argsToAlt :: [([Pat], Clause)] -> CaseBuilder ([Name], [Clause], [Name], [Clause])
536−argsToAlt [] = return ([], [])
546+argsToAlt [] = return ([], [], [], [])
537argsToAlt rs@((r, m) : rest)
547argsToAlt rs@((r, m) : rest)
538 = do newArgs <- getNewVars r
548 = do newArgs <- getNewVars r
539− return (newArgs, addRs rs)
549+ return (newArgs, addRs rs, [], [])
540 where
550 where
541 getNewVars [] = return []
551 getNewVars [] = return []
542 getNewVars ((PV n t) : ns) = do v <- getVar "e"
552 getNewVars ((PV n t) : ns) = do v <- getVar "e"