@@ -1,13 +1,15 @@
11{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}
22
3−module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),
3+module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo,
44 Phase(..), CaseTree,
55 simpleCase, small, namesUsed, findCalls, findUsedArgs,
66 substSC, substAlt, mkForce) where
77
88import Idris.Core.TT
99
10+import Control.Applicative hiding (Const)
1011import Control.Monad.State
12+import Control.Monad.Reader
1113import Data.Maybe
1214import Data.List hiding (partition)
1315import qualified Data.List(partition)
@@ -24,7 +26,7 @@ data CaseDef = CaseDef [Name] !SC [Term]
2426-- in the function `prune` as a means of optimisation
2527-- of already built case trees.
2628--
27−-- While the intermediate representation (follows in the pipeline)
29+-- While the intermediate representation (follows in the pipeline, named LExp)
2830-- allows casing on arbitrary terms, here we choose to maintain the distinction
2931-- in order to allow for better optimisation opportunities.
3032--
@@ -213,6 +215,11 @@ isUsed sc n = used sc where
213215 usedA (SucCase _ sc) = used sc
214216 usedA (DefaultCase sc) = used sc
215217
218+type ErasureInfo = Name -> [Int] -- name to list of inaccessible arguments; empty list if name not found
219+type CaseBuilder a = ReaderT ErasureInfo (State CS) a
220+
221+runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))
222+runCaseBuilder ei bld = runState $ runReaderT bld ei
216223
217224data Phase = CompileTime | RunTime
218225 deriving (Show, Eq)
@@ -223,8 +230,9 @@ data Phase = CompileTime | RunTime
223230simpleCase :: Bool -> Bool -> Bool ->
224231 Phase -> FC -> [Int] -> [Type] ->
225232 [([Name], Term, Term)] ->
233+ ErasureInfo ->
226234 TC CaseDef
227−simpleCase tc cover reflect phase fc inacc argtys cs
235+simpleCase tc cover reflect phase fc inacc argtys cs erInfo
228236 = sc' tc cover phase fc (filter (\(_, _, r) ->
229237 case r of
230238 Impossible -> False
@@ -243,7 +251,7 @@ simpleCase tc cover reflect phase fc inacc argtys cs
243251 let numargs = length (fst (head pats))
244252 ns = take numargs args
245253 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats
246− (tree, st) = runState
254+ (tree, st) = runCaseBuilder erInfo
247255 (match ns' ps' (defaultCase cover))
248256 ([], numargs, [])
249257 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
@@ -334,18 +342,20 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
334342 getArgs _ = []
335343
336344toPat :: Bool -> Bool -> [Term] -> [Pat]
337−toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
345+toPat reflect tc = map $ toPat' []
338346 where
339− toPat' (P (DCon t a) nm@(UN n) _) [_,_,arg]
340− | n == txt "Delay" = do arg' <- toPat' arg []
341− return $ PCon nm t [PAny, PAny, arg']
342− toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args
343− return $ PCon n t args'
347+ toPat' [_,_,arg](P (DCon t a) nm@(UN n) _)
348+ | n == txt "Delay"
349+ = PCon nm t [PAny, PAny, toPat' [] arg]
350+
351+ toPat' args (P (DCon t a) n _)
352+ = PCon n t $ map (toPat' []) args
353+
344354 -- n + 1
345− toPat' (P _ (UN pabi) _)
346− [p, Constant (BI 1)] | pabi == txt "prim__addBigInt"
347− = do p' <- toPat' p []
348− return $ PSuc p'
355+ toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)
356+ | pabi == txt "prim__addBigInt"
357+ = PSuc $ toPat' [] p
358+
349359 -- Typecase
350360-- toPat' (P (TCon t a) n _) args | tc
351361-- = do args' <- mapM (\x -> toPat' x []) args
@@ -360,26 +370,25 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
360370-- | tc = return $ PCon (UN "Integer") 6 []
361371-- toPat' (Constant (AType (ATInt (ITFixed n)))) []
362372-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive
363− toPat' (P Bound n ty) [] = -- trace (show (n, ty)) $
364− do ns <- get
365− if n `elem` ns
366− then return PAny
367− else do put (n : ns)
368− return (PV n ty)
369− toPat' (App f a) args = toPat' f (a : args)
370− toPat' (Constant (AType _)) [] = return PTyPat
371− toPat' (Constant StrType) [] = return PTyPat
372− toPat' (Constant PtrType) [] = return PTyPat
373− toPat' (Constant VoidType) [] = return PTyPat
374− toPat' (Constant x) [] = return $ PConst x
375− toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc
376− = do t' <- toPat' t []
377− sc' <- toPat' sc []
378− return $ PReflected (sUN "->") (t':sc':[])
379− toPat' (P _ n _) args | reflect
380− = do args' <- mapM (\x -> toPat' x []) args
381− return $ PReflected n args'
382− toPat' t _ = return PAny
373+--
374+
375+ toPat' [] (P Bound n ty) = PV n ty
376+ toPat' args (App f a) = toPat' (a : args) f
377+ toPat' [] (Constant (AType _)) = PTyPat
378+ toPat' [] (Constant StrType) = PTyPat
379+ toPat' [] (Constant PtrType) = PTyPat
380+ toPat' [] (Constant VoidType) = PTyPat
381+ toPat' [] (Constant x) = PConst x
382+
383+ toPat' [] (Bind n (Pi t) sc)
384+ | reflect && noOccurrence n sc
385+ = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]
386+
387+ toPat' args (P _ n _)
388+ | reflect
389+ = PReflected n $ map (toPat' []) args
390+
391+ toPat' _ t = PAny
383392
384393 fixedN IT8 = "Bits8"
385394 fixedN IT16 = "Bits16"
@@ -459,7 +468,7 @@ order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))
459468 numNames xs [] = length xs
460469
461470match :: [Name] -> [Clause] -> SC -- error case
462− -> State CS SC
471+ -> CaseBuilder SC
463472match [] (([], ret) : xs) err
464473 = do (ts, v, ntys) <- get
465474 put (ts ++ (map (fst.snd) xs), v, ntys)
@@ -469,13 +478,19 @@ match [] (([], ret) : xs) err
469478match vs cs err = do let ps = partition cs
470479 mixture vs ps err
471480
472−mixture :: [Name] -> [Partition] -> SC -> State CS SC
481+mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC
473482mixture vs [] err = return err
474483mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
475484 conRule vs ms fallthrough
476485mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
477486 varRule vs ms fallthrough
478487
488+-- Return the list of inaccessible arguments of a data constructor.
489+inaccessibleArgs :: Name -> CaseBuilder [Int]
490+inaccessibleArgs n = do
491+ getInaccessiblePositions <- ask -- this function is the only thing in the environment
492+ return $ getInaccessiblePositions n
493+
479494data ConType = CName Name Int -- named constructor
480495 | CFn Name -- reflected function name
481496 | CSuc -- n+1
@@ -486,76 +501,99 @@ data Group = ConGroup ConType -- Constructor
486501 [([Pat], Clause)] -- arguments and rest of alternative
487502 deriving Show
488503
489−conRule :: [Name] -> [Clause] -> SC -> State CS SC
504+conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
490505conRule (v:vs) cs err = do groups <- groupCons cs
491506 caseGroups (v:vs) groups err
492507
493−caseGroups :: [Name] -> [Group] -> SC -> State CS SC
508+caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC
494509caseGroups (v:vs) gs err = do g <- altGroups gs
495510 return $ Case v (sort g)
496511 where
497512 altGroups [] = return [DefaultCase err]
513+
498514 altGroups (ConGroup (CName n i) args : cs)
499− = do g <- altGroup n i args
500− rest <- altGroups cs
501− return (g : rest)
515+ = (:) <$> altGroup n i args <*> altGroups cs
516+
502517 altGroups (ConGroup (CFn n) args : cs)
503− = do g <- altFnGroup n args
504− rest <- altGroups cs
505− return (g : rest)
518+ = (:) <$> altFnGroup n args <*> altGroups cs
519+
506520 altGroups (ConGroup CSuc args : cs)
507− = do g <- altSucGroup args
508− rest <- altGroups cs
509− return (g : rest)
521+ = (:) <$> altSucGroup args <*> altGroups cs
522+
510523 altGroups (ConGroup (CConst c) args : cs)
511− = do g <- altConstGroup c args
512− rest <- altGroups cs
513− return (g : rest)
514−
515− altGroup n i gs = do (newArgs, nextCs) <- argsToAlt gs
516− matchCs <- match (newArgs ++ vs) nextCs err
517− return $ ConCase n i newArgs matchCs
518− altFnGroup n gs = do (newArgs, nextCs) <- argsToAlt gs
519− matchCs <- match (newArgs ++ vs) nextCs err
520− return $ FnCase n newArgs matchCs
521− altSucGroup gs = do ([newArg], nextCs) <- argsToAlt gs
522− matchCs <- match (newArg:vs) nextCs err
523− return $ SucCase newArg matchCs
524− altConstGroup n gs = do (_, nextCs) <- argsToAlt gs
525− matchCs <- match vs nextCs err
526− return $ ConstCase n matchCs
527−
528−argsToAlt :: [([Pat], Clause)] -> State CS ([Name], [Clause])
529−argsToAlt [] = return ([], [])
530−argsToAlt rs@((r, m) : rest)
531− = do newArgs <- getNewVars r
532− return (newArgs, addRs rs)
524+ = (:) <$> altConstGroup c args <*> altGroups cs
525+
526+ altGroup n i args = do inacc <- inaccessibleArgs n
527+ (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
528+ matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
529+ return $ ConCase n i newVars matchCs
530+
531+ altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args
532+ matchCs <- match (newVars ++ vs) nextCs err
533+ return $ FnCase n newVars matchCs
534+
535+ altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args
536+ matchCs <- match (newVar:vs) nextCs err
537+ return $ SucCase newVar matchCs
538+
539+ altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args
540+ matchCs <- match vs nextCs err
541+ return $ ConstCase n matchCs
542+
543+-- Returns:
544+-- * names of all variables arising from match
545+-- * names of accessible variables (subset of all variables)
546+-- * names of inaccessible variables (subset of all variables)
547+-- * clauses corresponding to (accVars ++ origVars ++ inaccVars)
548+argsToAlt :: [Int] -> [([Pat], Clause)] -> CaseBuilder ([Name], [Name], [Name], [Clause])
549+argsToAlt _ [] = return ([], [], [], [])
550+argsToAlt inacc rs@((r, m) : rest) = do
551+ newVars <- getNewVars r
552+ let (accVars, inaccVars) = partitionAcc newVars
553+ return (newVars, accVars, inaccVars, addRs rs)
533554 where
555+ -- Create names for new variables arising from the given patterns.
556+ getNewVars :: [Pat] -> CaseBuilder [Name]
534557 getNewVars [] = return []
535558 getNewVars ((PV n t) : ns) = do v <- getVar "e"
559+ nsv <- getNewVars ns
560+
561+ -- Record the type of the variable.
562+ --
563+ -- It seems that the ordering is not important
564+ -- and we can put (v,t) always in front of "ntys"
565+ -- (the varName-type pairs seem to represent a mapping).
566+ --
567+ -- The code that reads this is currently
568+ -- commented out, anyway.
536569 (cs, i, ntys) <- get
537570 put (cs, i, (v, t) : ntys)
538− nsv <- getNewVars ns
571+
539572 return (v : nsv)
540− getNewVars (PAny : ns) = do v <- getVar "i"
541− nsv <- getNewVars ns
542− return (v : nsv)
543− getNewVars (PTyPat : ns) = do v <- getVar "t"
544− nsv <- getNewVars ns
545− return (v : nsv)
546− getNewVars (_ : ns) = do v <- getVar "e"
547− nsv <- getNewVars ns
548− return (v : nsv)
573+
574+ getNewVars (PAny : ns) = (:) <$> getVar "i" <*> getNewVars ns
575+ getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns
576+ getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns
577+
578+ -- Partition a list of things into (accessible, inaccessible) things,
579+ -- according to the list of inaccessible indices.
580+ partitionAcc xs =
581+ ( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]
582+ , [x | (i,x) <- zip [0..] xs, i `elem` inacc]
583+ )
584+
549585 addRs [] = []
550− addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)
586+ addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)
587+ where
588+ (acc, inacc) = partitionAcc r
551589
552590 uniq i (UN n) = MN i n
553591 uniq i n = n
554592
555−getVar :: String -> State CS Name
593+getVar :: String -> CaseBuilder Name
556594getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)
557595
558−groupCons :: [Clause] -> State CS [Group]
596+groupCons :: [Clause] -> CaseBuilder [Group]
559597groupCons cs = gc [] cs
560598 where
561599 gc acc [] = return acc
@@ -581,7 +619,7 @@ groupCons cs = gc [] cs
581619-- | otherwise = g : addConG con res gs
582620 addConG con res (g : gs) = g : addConG con res gs
583621
584−varRule :: [Name] -> [Clause] -> SC -> State CS SC
622+varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
585623varRule (v : vs) alts err =
586624 do alts' <- mapM (repVar v) alts
587625 match vs alts' err