git.iko.soy/Idris-dev
on f92ecd2 help sign in
Idris-dev/src/Idris/Core/CaseTree.hs
816 lines 32 kB history raw
1{-|
2Module : Idris.Core.CaseTree
3Description : Module to define and interact with case trees.
5License : BSD3
6Maintainer : The Idris Community.
8Note: The case-tree elaborator only produces (Case n alts)-cases;
9in other words, it never inspects anything else than variables.
11ProjCase is a special powerful case construct that allows inspection
12of compound terms. Occurrences of ProjCase arise no earlier than
13in the function `prune` as a means of optimisation
14of already built case trees.
16While the intermediate representation (follows in the pipeline, named LExp)
17allows casing on arbitrary terms, here we choose to maintain the distinction
18in order to allow for better optimisation opportunities.
20-}
22{-# LANGUAGE DeriveFunctor, DeriveGeneric, FlexibleContexts, FlexibleInstances,
23 PatternGuards, TypeSynonymInstances #-}
25module Idris.Core.CaseTree (
26 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
27 , Phase(..), CaseTree, CaseType(..)
28 , simpleCase, small, namesUsed, findCalls, findCalls', findUsedArgs
29 , substSC, substAlt, mkForce
30 ) where
32import Idris.Core.TT
34import Control.Monad.Reader
35import Control.Monad.State
36import Data.List hiding (partition)
37import qualified Data.List (partition)
38import qualified Data.Set as S
39import GHC.Generics (Generic)
41data CaseDef = CaseDef [Name] !SC [Term]
42 deriving Show
44data SC' t = Case CaseType Name [CaseAlt' t] -- ^ invariant: lowest tags first
45 | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection
46 | STerm !t
47 | UnmatchedCase String -- ^ error message
48 | ImpossibleCase -- ^ already checked to be impossible
49 deriving (Eq, Ord, Functor, Generic)
50{-!
51deriving instance Binary SC'
52!-}
54data CaseType = Updatable | Shared
55 deriving (Eq, Ord, Show, Generic)
57type SC = SC' Term
59data CaseAlt' t = ConCase Name Int [Name] !(SC' t)
60 | FnCase Name [Name] !(SC' t) -- ^ reflection function
61 | ConstCase Const !(SC' t)
62 | SucCase Name !(SC' t)
63 | DefaultCase !(SC' t)
64 deriving (Show, Eq, Ord, Functor, Generic)
65{-!
66deriving instance Binary CaseAlt'
67!-}
69type CaseAlt = CaseAlt' Term
71instance Show t => Show (SC' t) where
72 show sc = show' 1 sc
73 where
74 show' i (Case up n alts) = "case" ++ u ++ show n ++ " of\n" ++ indent i ++
75 showSep ("\n" ++ indent i) (map (showA i) alts)
76 where u = case up of
77 Updatable -> "! "
78 Shared -> " "
79 show' i (ProjCase tm alts) = "case " ++ show tm ++ " of " ++
80 showSep ("\n" ++ indent i) (map (showA i) alts)
81 show' i (STerm tm) = show tm
82 show' i (UnmatchedCase str) = "error " ++ show str
83 show' i ImpossibleCase = "impossible"
85 indent i = concat $ take i (repeat " ")
87 showA i (ConCase n t args sc)
88 = show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
89 ++ show' (i+1) sc
90 showA i (FnCase n args sc)
91 = "FN " ++ show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
92 ++ show' (i+1) sc
93 showA i (ConstCase t sc)
94 = show t ++ " => " ++ show' (i+1) sc
95 showA i (SucCase n sc)
96 = show n ++ "+1 => " ++ show' (i+1) sc
97 showA i (DefaultCase sc)
98 = "_ => " ++ show' (i+1) sc
101type CaseTree = SC
102type Clause = ([Pat], (Term, Term))
103type CS = ([Term], Int, [(Name, Type)])
105instance TermSize SC where
106 termsize n (Case _ n' as) = termsize n as
107 termsize n (ProjCase n' as) = termsize n as
108 termsize n (STerm t) = termsize n t
109 termsize n _ = 1
111instance TermSize CaseAlt where
112 termsize n (ConCase _ _ _ s) = termsize n s
113 termsize n (FnCase _ _ s) = termsize n s
114 termsize n (ConstCase _ s) = termsize n s
115 termsize n (SucCase _ s) = termsize n s
116 termsize n (DefaultCase s) = termsize n s
118-- simple terms can be inlined trivially - good for primitives in particular
119-- To avoid duplicating work, don't inline something which uses one
120-- of its arguments in more than one place
122small :: Name -> [Name] -> SC -> Bool
123small n args t = let as = findAllUsedArgs t args in
124 length as == length (nub as) &&
125 termsize n t < 20
127namesUsed :: SC -> [Name]
128namesUsed sc = nub $ nu' [] sc where
129 nu' ps (Case _ n alts) = nub (concatMap (nua ps) alts) \\ [n]
130 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts
131 nu' ps (STerm t) = nub $ nut ps t
132 nu' ps _ = []
134 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args
135 nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc) \\ args
136 nua ps (ConstCase _ sc) = nu' ps sc
137 nua ps (SucCase _ sc) = nu' ps sc
138 nua ps (DefaultCase sc) = nu' ps sc
140 nut ps (P _ n _) | n `elem` ps = []
141 | otherwise = [n]
142 nut ps (App _ f a) = nut ps f ++ nut ps a
143 nut ps (Proj t _) = nut ps t
144 nut ps (Bind n (Let _ t v) sc) = nut ps v ++ nut (n:ps) sc
145 nut ps (Bind n b sc) = nut (n:ps) sc
146 nut ps _ = []
148-- | Return all called functions, and which arguments are used
149-- in each argument position for the call, in order to help reduce
150-- compilation time, and trace all unused arguments
151findCalls :: SC -> [Name] -> [(Name, [[Name]])]
152findCalls = findCalls' False
154findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]
155findCalls' ignoreasserts sc topargs = S.toList $ nu' topargs sc where
156 nu' ps (Case _ n alts) = S.unions $ map (nua (n : ps)) alts
157 nu' ps (ProjCase t alts) = S.unions $ nut ps t : map (nua ps) alts
158 nu' ps (STerm t) = nut ps t
159 nu' ps _ = S.empty
161 nua ps (ConCase n i args sc) = nu' (ps ++ args) sc
162 nua ps (FnCase n args sc) = nu' (ps ++ args) sc
163 nua ps (ConstCase _ sc) = nu' ps sc
164 nua ps (SucCase _ sc) = nu' ps sc
165 nua ps (DefaultCase sc) = nu' ps sc
167 nut ps (P _ n _) | n `elem` ps = S.empty
168 | otherwise = S.singleton (n, [])
169 nut ps fn@(App _ f a)
170 | (P _ n _, args) <- unApply fn
171 = if ignoreasserts && n == sUN "assert_total"
172 then S.empty
173 else if n `elem` ps
174 then S.union (nut ps f) (nut ps a)
175 else S.insert (n, map argNames args)
176 (S.unions $ map (nut ps) args)
177 | (P (TCon _ _) n _, _) <- unApply fn = S.empty
178 | otherwise = S.union (nut ps f) (nut ps a)
179 nut ps (Bind n (Let _ t v) sc) = S.union (nut ps v) (nut (n:ps) sc)
180 nut ps (Proj t _) = nut ps t
181 nut ps (Bind n b sc) = nut (n:ps) sc
182 nut ps _ = S.empty
184 argNames tm = let ns = directUse tm in
185 filter (\x -> x `elem` ns) topargs
187-- Find names which are used directly (i.e. not in a function call) in a term
189directUse :: TT Name -> [Name]
190directUse (P _ n _) = [n]
191directUse (Bind n (Let _ t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])
192 ++ directUse t
193directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])
194directUse fn@(App _ f a)
195 | (P Ref (UN pfk) _, [App _ e w]) <- unApply fn,
196 pfk == txt "prim_fork"
197 = directUse e ++ directUse w -- HACK so that fork works
198 | (P Ref (UN fce) _, [_, _, a]) <- unApply fn,
199 fce == txt "Force"
200 = directUse a -- forcing a value counts as a use
201 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them
202 | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime
203 | otherwise = nub $ directUse f ++ directUse a
204directUse (Proj x i) = nub $ directUse x
205directUse _ = []
207-- Find all directly used arguments (i.e. used but not in function calls)
209findUsedArgs :: SC -> [Name] -> [Name]
210findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)
212findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where
213 nu' (Case _ n alts) = n : concatMap nua alts
214 nu' (ProjCase t alts) = directUse t ++ concatMap nua alts
215 nu' (STerm t) = directUse t
216 nu' _ = []
218 nua (ConCase n i args sc) = nu' sc
219 nua (FnCase n args sc) = nu' sc
220 nua (ConstCase _ sc) = nu' sc
221 nua (SucCase _ sc) = nu' sc
222 nua (DefaultCase sc) = nu' sc
224-- Return whether name is used anywhere in a case tree
225isUsed :: SC -> Name -> Bool
226isUsed sc n = used sc where
228 used (Case _ n' alts) = n == n' || any usedA alts
229 used (ProjCase t alts) = n `elem` freeNames t || any usedA alts
230 used (STerm t) = n `elem` freeNames t
231 used _ = False
233 usedA (ConCase _ _ args sc) = used sc
234 usedA (FnCase _ args sc) = used sc
235 usedA (ConstCase _ sc) = used sc
236 usedA (SucCase _ sc) = used sc
237 usedA (DefaultCase sc) = used sc
239type ErasureInfo = Name -> [Int] -- name to list of inaccessible arguments; empty list if name not found
240type CaseBuilder a = ReaderT ErasureInfo (State CS) a
242runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))
243runCaseBuilder ei bld = runState $ runReaderT bld ei
245data Phase = CoverageCheck [Int] -- list of positions explicitly given
246 | CompileTime
247 | RunTime
248 deriving (Show, Eq)
250-- Generate a simple case tree
251-- Work Right to Left
253simpleCase :: Bool -> SC -> Bool ->
254 Phase -> FC ->
255 -- Following two can be empty lists when Phase = CoverageCheck
256 [Int] -> -- Inaccessible argument positions
257 [(Type, Bool)] -> -- (Argument type, whether it's canonical)
258 [([Name], Term, Term)] ->
259 ErasureInfo ->
260 TC CaseDef
261simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
262 = sc' tc defcase phase fc (filter (\(_, _, r) ->
263 case r of
264 Impossible -> False
265 _ -> True) cs)
266 where
267 sc' tc defcase phase fc []
268 = return $ CaseDef [] (UnmatchedCase (show fc ++ ":No pattern clauses")) []
269 sc' tc defcase phase fc cs
270 = let proj = phase == RunTime
271 pats = map (\ (avs, l, r) ->
272 (avs, toPats reflect tc l, (l, r))) cs
273 chkPats = mapM chkAccessible pats in
274 case chkPats of
275 OK pats ->
276 let numargs = length (fst (head pats))
277 ns = take numargs args
278 (ns', ps') = order phase [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats (map snd argtys)
279 (tree, st) = runCaseBuilder erInfo
280 (match ns' ps' defcase)
281 ([], numargs, [])
282 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
283 if proj then return (stripLambdas t)
284 else return t
285 Error err -> Error (At fc err)
286 where args = map (\i -> sMN i "e") [0..]
287 fstT (x, _, _) = x
289 -- Check that all pattern variables are reachable by a case split
290 -- Otherwise, they won't make sense on the RHS.
291 chkAccessible (avs, l, c)
292 | phase /= CompileTime || reflect = return (l, c)
293 | otherwise = do mapM_ (acc l) avs
294 return (l, c)
296 acc [] n = Error (Inaccessible n)
297 acc (PV x t : xs) n | x == n = OK ()
298 acc (PCon _ _ _ ps : xs) n = acc (ps ++ xs) n
299 acc (PSuc p : xs) n = acc (p : xs) n
300 acc (_ : xs) n = acc xs n
302data Pat = PCon Bool Name Int [Pat]
303 | PConst Const
304 | PInferred Pat
305 | PV Name Type
306 | PSuc Pat -- special case for n+1 on Integer
307 | PReflected Name [Pat]
308 | PAny
309 | PTyPat -- typecase, not allowed, inspect last
310 deriving Show
312-- If there are repeated variables, take the *last* one (could be name shadowing
313-- in a where clause, so take the most recent).
315toPats :: Bool -> Bool -> Term -> [Pat]
316toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
317 getArgs (App _ f a) = a : getArgs f
318 getArgs _ = []
320toPat :: Bool -> Bool -> [Term] -> [Pat]
321toPat reflect tc = map $ toPat' []
322 where
323 toPat' [_,_,arg] (P (DCon t a uniq) nm@(UN n) _)
324 | n == txt "Delay"
325 = PCon uniq nm t [PAny, PAny, toPat' [] arg]
327 toPat' args (P (DCon t a uniq) nm@(NS (UN n) [own]) _)
328 | n == txt "Read" && own == txt "Ownership"
329 = PCon False nm t (map shareCons (map (toPat' []) args))
330 where shareCons (PCon _ n i ps) = PCon False n i (map shareCons ps)
331 shareCons p = p
333 toPat' args (P (DCon t a uniq) n _)
334 = PCon uniq n t $ map (toPat' []) args
336 -- n + 1
337 toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)
338 | pabi == txt "prim__addBigInt"
339 = PSuc $ toPat' [] p
341 toPat' [] (P Bound n ty) = PV n ty
342 toPat' args (App _ f a) = toPat' (a : args) f
343 toPat' args (Inferred tm) = PInferred (toPat' args tm)
344 toPat' [] (Constant x) | isTypeConst x = PTyPat
345 | otherwise = PConst x
347 toPat' [] (Bind n (Pi _ _ t _) sc)
348 | reflect && noOccurrence n sc
349 = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]
351 toPat' args (P _ n _)
352 | reflect
353 = PReflected n $ map (toPat' []) args
355 toPat' _ t = PAny
357data Partition = Cons [Clause]
358 | Vars [Clause]
359 deriving Show
361isVarPat (PV _ _ : ps , _) = True
362isVarPat (PAny : ps , _) = True
363isVarPat (PTyPat : ps , _) = True
364isVarPat _ = False
366isConPat (PCon _ _ _ _ : ps, _) = True
367isConPat (PReflected _ _ : ps, _) = True
368isConPat (PSuc _ : ps, _) = True
369isConPat (PConst _ : ps, _) = True
370isConPat _ = False
372partition :: [Clause] -> [Partition]
373partition [] = []
374partition ms@(m : _)
375 | isVarPat m = let (vars, rest) = span isVarPat ms in
376 Vars vars : partition rest
377 | isConPat m = let (cons, rest) = span isConPat ms in
378 Cons cons : partition rest
379partition xs = error $ "Partition " ++ show xs
381-- reorder the patterns so that the one with most distinct names
382-- comes next. Take rightmost first, otherwise (i.e. pick value rather
383-- than dependency)
384--
385-- The first argument means [(Name, IsInaccessible)].
387order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
388-- do nothing at compile time: FIXME (EB): Put this in after checking
389-- implications for Franck's reflection work... see issue 3233
390-- order CompileTime ns cs _ = (map fst ns, cs)
391order _ [] cs cans = ([], cs)
392order _ ns' [] cans = (map fst ns', [])
393order (CoverageCheck pos) ns' cs cans
394 = let ns_out = pick 0 [] (map fst ns')
395 cs_out = map pickClause cs in
396 (ns_out, cs_out)
397 where
398 pickClause (pats, def) = (pick 0 [] pats, def)
400 -- Order the list so that things in a position in 'pos' are in the first
401 -- part, then all the other things later. Otherwise preserve order.
402 pick i skipped [] = reverse skipped
403 pick i skipped (x : xs)
404 | i `elem` pos = x : pick (i + 1) skipped xs
405 | otherwise = pick (i + 1) (x : skipped) xs
407order phase ns' cs cans
408 = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))
409 -- only sort the arguments where there is no clash in
410 -- constructor tags between families, the argument type is canonical,
411 -- and no constructor/constant
412 -- clash, because otherwise we can't reliable make the
413 -- case distinction on evaluation
414 (patnames_ord, patnames_rest)
415 = Data.List.partition (noClash . map snd) patnames
416 patnames_ord' = case phase of
417 CompileTime -> patnames_ord
418 -- reversing tends to make better case trees
419 -- and helps erasure
420 RunTime -> reverse patnames_ord
421 pats' = transpose (sortBy moreDistinct patnames_ord'
422 ++ patnames_rest) in
423 (getNOrder pats', zipWith rebuild pats' cs)
424 where
425 getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)
426 getNOrder (c : _) = map (fst . fst) c
428 rebuild patnames clause = (map (snd . snd) patnames, snd clause)
430 noClash [] = True
431 noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))
432 && noClash ps
434 clashPat (PCon _ _ _ _) (PConst _) = True
435 clashPat (PConst _) (PCon _ _ _ _) = True
436 clashPat (PCon _ _ _ _) (PSuc _) = True
437 clashPat (PSuc _) (PCon _ _ _ _) = True
438 clashPat (PCon _ n i _) (PCon _ n' i' _) | i == i' = n /= n'
439 clashPat _ _ = False
441 -- this compares (+isInaccessible, -numberOfCases)
442 moreDistinct xs ys
443 = compare (snd . fst . head $ xs, numNames [] (map snd ys))
444 (snd . fst . head $ ys, numNames [] (map snd xs))
446 numNames xs ((_, PCon _ n _ _) : ps)
447 | not (Left n `elem` xs) = numNames (Left n : xs) ps
448 numNames xs ((_, PConst c) : ps)
449 | not (Right c `elem` xs) = numNames (Right c : xs) ps
450 numNames xs (_ : ps) = numNames xs ps
451 numNames xs [] = length xs
453-- Reorder the patterns in the clause so that the PInferred patterns come
454-- last. Also strip 'PInferred' from the top level patterns so that we can
455-- go ahead and match.
456orderByInf :: [Name] -> [Clause] -> ([Name], [Clause])
457orderByInf vs cs = let alwaysInf = getInf cs in
458 (selectInf alwaysInf vs,
459 map deInf (map (selectExp alwaysInf) cs))
460 where
461 getInf [] = []
462 getInf [(pats, def)] = infPos 0 pats
463 getInf ((pats, def) : cs) = infPos 0 pats `intersect` getInf cs
465 selectExp :: [Int] -> Clause -> Clause
466 selectExp infs (pats, def)
467 = let (notInf, inf) = splitPats 0 infs [] [] pats in
468 (notInf ++ inf, def)
470 selectInf :: [Int] -> [a] -> [a]
471 selectInf infs ns = let (notInf, inf) = splitPats 0 infs [] [] ns in
472 notInf ++ inf
474 splitPats i infpos notInf inf [] = (reverse notInf, reverse inf)
475 splitPats i infpos notInf inf (p : ps)
476 | i `elem` infpos = splitPats (i + 1) infpos notInf (p : inf) ps
477 | otherwise = splitPats (i + 1) infpos (p : notInf) inf ps
479 infPos i [] = []
480 infPos i (PInferred p : ps) = i : infPos (i + 1) ps
481 infPos i (_ : ps) = infPos (i + 1) ps
483 deInf (pats, def) = (map deInfPat pats, def)
485 deInfPat (PInferred p) = p
486 deInfPat p = p
488match :: [Name] -> [Clause] -> SC -- error case
489 -> CaseBuilder SC
490match [] (([], ret) : xs) err
491 = do (ts, v, ntys) <- get
492 put (ts ++ (map (fst.snd) xs), v, ntys)
493 case snd ret of
494 Impossible -> return ImpossibleCase
495 tm -> return $ STerm tm -- run out of arguments
496match vs cs err = do let (vs', de_inf) = orderByInf vs cs
497 ps = partition de_inf
498 mixture vs' ps err
500mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC
501mixture vs [] err = return err
502mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
503 conRule vs ms fallthrough
504mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
505 varRule vs ms fallthrough
507-- Return the list of inaccessible arguments of a data constructor.
508inaccessibleArgs :: Name -> CaseBuilder [Int]
509inaccessibleArgs n = do
510 getInaccessiblePositions <- ask -- this function is the only thing in the environment
511 return $ getInaccessiblePositions n
513data ConType = CName Name Int -- named constructor
514 | CFn Name -- reflected function name
515 | CSuc -- n+1
516 | CConst Const -- constant, not implemented yet
517 deriving (Show, Eq)
519data Group = ConGroup Bool -- Uniqueness flag
520 ConType -- Constructor
521 [([Pat], Clause)] -- arguments and rest of alternative
522 deriving Show
524conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
525conRule (v:vs) cs err = do groups <- groupCons cs
526 caseGroups (v:vs) groups err
528caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC
529caseGroups (v:vs) gs err = do g <- altGroups gs
530 return $ Case (getShared gs) v (sort g)
531 where
532 getShared (ConGroup True _ _ : _) = Updatable
533 getShared _ = Shared
535 altGroups [] = return [DefaultCase err]
537 altGroups (ConGroup _ (CName n i) args : cs)
538 = (:) <$> altGroup n i args <*> altGroups cs
540 altGroups (ConGroup _ (CFn n) args : cs)
541 = (:) <$> altFnGroup n args <*> altGroups cs
543 altGroups (ConGroup _ CSuc args : cs)
544 = (:) <$> altSucGroup args <*> altGroups cs
546 altGroups (ConGroup _ (CConst c) args : cs)
547 = (:) <$> altConstGroup c args <*> altGroups cs
549 altGroup n i args
550 = do inacc <- inaccessibleArgs n
551 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
552 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
553 return $ ConCase n i newVars matchCs
555 altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args
556 matchCs <- match (newVars ++ vs) nextCs err
557 return $ FnCase n newVars matchCs
559 altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args
560 matchCs <- match (newVar:vs) nextCs err
561 return $ SucCase newVar matchCs
563 altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args
564 matchCs <- match vs nextCs err
565 return $ ConstCase n matchCs
567-- Returns:
568-- * names of all variables arising from match
569-- * names of accessible variables (subset of all variables)
570-- * names of inaccessible variables (subset of all variables)
571-- * clauses corresponding to (accVars ++ origVars ++ inaccVars)
572argsToAlt :: [Int] -> [([Pat], Clause)] -> CaseBuilder ([Name], [Name], [Name], [Clause])
573argsToAlt _ [] = return ([], [], [], [])
574argsToAlt inacc rs@((r, m) : rest) = do
575 newVars <- getNewVars r
576 let (accVars, inaccVars) = partitionAcc newVars
577 return (newVars, accVars, inaccVars, addRs rs)
578 where
579 -- Create names for new variables arising from the given patterns.
580 getNewVars :: [Pat] -> CaseBuilder [Name]
581 getNewVars [] = return []
582 getNewVars ((PV n t) : ns) = do v <- getVar "e"
583 nsv <- getNewVars ns
585 -- Record the type of the variable.
586 --
587 -- It seems that the ordering is not important
588 -- and we can put (v,t) always in front of "ntys"
589 -- (the varName-type pairs seem to represent a mapping).
590 --
591 -- The code that reads this is currently
592 -- commented out, anyway.
593 (cs, i, ntys) <- get
594 put (cs, i, (v, t) : ntys)
596 return (v : nsv)
598 getNewVars (PAny : ns) = (:) <$> getVar "i" <*> getNewVars ns
599 getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns
600 getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns
602 -- Partition a list of things into (accessible, inaccessible) things,
603 -- according to the list of inaccessible indices.
604 partitionAcc xs =
605 ( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]
606 , [x | (i,x) <- zip [0..] xs, i `elem` inacc]
607 )
609 addRs [] = []
610 addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)
611 where
612 (acc, inacc) = partitionAcc r
614getVar :: String -> CaseBuilder Name
615getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)
617groupCons :: [Clause] -> CaseBuilder [Group]
618groupCons cs = gc [] cs
619 where
620 gc acc [] = return acc
621 gc acc ((p : ps, res) : cs) =
622 do acc' <- addGroup p ps res acc
623 gc acc' cs
624 addGroup p ps res acc = case p of
625 PCon uniq con i args -> return $ addg uniq (CName con i) args (ps, res) acc
626 PConst cval -> return $ addConG cval (ps, res) acc
627 PSuc n -> return $ addg False CSuc [n] (ps, res) acc
628 PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc
629 pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"
631 addg uniq c conargs res []
632 = [ConGroup uniq c [(conargs, res)]]
633 addg uniq c conargs res (g@(ConGroup _ c' cs):gs)
634 | c == c' = ConGroup uniq c (cs ++ [(conargs, res)]) : gs
635 | otherwise = g : addg uniq c conargs res gs
637 addConG con res [] = [ConGroup False (CConst con) [([], res)]]
638 addConG con res (g@(ConGroup False (CConst n) cs) : gs)
639 | con == n = ConGroup False (CConst n) (cs ++ [([], res)]) : gs
640-- | otherwise = g : addConG con res gs
641 addConG con res (g : gs) = g : addConG con res gs
643varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
644varRule (v : vs) alts err =
645 do alts' <- mapM (repVar v) alts
646 match vs alts' err
647 where
648 repVar v (PV p ty : ps , (lhs, res))
649 = do (cs, i, ntys) <- get
650 put (cs, i, (v, ty) : ntys)
651 return (ps, (lhs, subst p (P Bound v ty) res))
652 repVar v (PAny : ps , res) = return (ps, res)
653 repVar v (PTyPat : ps , res) = return (ps, res)
655-- fix: case e of S k -> f (S k) ==> case e of S k -> f e
657depatt :: [Name] -> SC -> SC
658depatt ns tm = dp [] tm
659 where
660 dp ms (STerm tm) = STerm (applyMaps ms tm)
661 dp ms (Case up x alts) = Case up x (map (dpa ms x) alts)
662 dp ms sc = sc
664 dpa ms x (ConCase n i args sc)
665 = ConCase n i args (dp ((x, (n, args)) : ms) sc)
666 dpa ms x (FnCase n args sc)
667 = FnCase n args (dp ((x, (n, args)) : ms) sc)
668 dpa ms x (ConstCase c sc) = ConstCase c (dp ms sc)
669 dpa ms x (SucCase n sc) = SucCase n (dp ms sc)
670 dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)
672 applyMaps ms f@(App _ _ _)
673 | (P nt cn pty, args) <- unApply f
674 = let args' = map (applyMaps ms) args in
675 applyMap ms nt cn pty args'
676 where
677 applyMap [] nt cn pty args' = mkApp (P nt cn pty) args'
678 applyMap ((x, (n, args)) : ms) nt cn pty args'
679 | and ((length args == length args') :
680 (n == cn) : zipWith same args args') = P Ref x Erased
681 | otherwise = applyMap ms nt cn pty args'
682 same n (P _ n' _) = n == n'
683 same _ _ = False
685 applyMaps ms (App s f a) = App s (applyMaps ms f) (applyMaps ms a)
686 applyMaps ms t = t
688-- FIXME: Do this for SucCase too
689-- Issue #1719 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1719
690prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)
691 -> SC -> SC
692prune proj (Case up n alts) = case alts' of
693 [] -> ImpossibleCase
695 -- Projection transformations prevent us from seeing some uses of ctor fields
696 -- because they delete information about which ctor is being used.
697 -- Consider:
698 -- f (X x) = ... x ...
699 -- vs.
700 -- f x = ... x!0 ...
701 --
702 -- Hence, we disable this step.
703 -- TODO: re-enable this in toIR
704 --
705 -- as@[ConCase cn i args sc]
706 -- | proj -> mkProj n 0 args (prune proj sc)
707 -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs
709 -- If none of the args are used in the sc, however, we can just replace it
710 -- with sc
711 as@[ConCase cn i args sc]
712 | proj -> let sc' = prune proj sc in
713 if any (isUsed sc') args
714 then Case up n [ConCase cn i args sc']
715 else sc'
717 [SucCase cn sc]
718 | proj
719 -> projRep cn n (-1) $ prune proj sc
721 [ConstCase _ sc]
722 -> prune proj sc
724 -- Bit of a hack here! The default case will always be 0, make sure
725 -- it gets caught first.
726 [s@(SucCase _ _), DefaultCase dc]
727 -> Case up n [ConstCase (BI 0) dc, s]
729 as -> Case up n as
730 where
731 alts' = filter (not . erased) $ map pruneAlt alts
733 pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)
734 pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)
735 pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)
736 pruneAlt (SucCase n sc) = SucCase n (prune proj sc)
737 pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)
739 erased (DefaultCase (STerm Erased)) = True
740 erased (DefaultCase ImpossibleCase) = True
741 erased _ = False
743 projRep :: Name -> Name -> Int -> SC -> SC
744 projRep arg n i (Case up x alts) | x == arg
745 = ProjCase (Proj (P Bound n Erased) i) $ map (projRepAlt arg n i) alts
746 projRep arg n i (Case up x alts)
747 = Case up x (map (projRepAlt arg n i) alts)
748 projRep arg n i (ProjCase t alts)
749 = ProjCase (projRepTm arg n i t) $ map (projRepAlt arg n i) alts
750 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)
751 projRep arg n i c = c
753 projRepAlt arg n i (ConCase cn t args rhs)
754 = ConCase cn t args (projRep arg n i rhs)
755 projRepAlt arg n i (FnCase cn args rhs)
756 = FnCase cn args (projRep arg n i rhs)
757 projRepAlt arg n i (ConstCase t rhs)
758 = ConstCase t (projRep arg n i rhs)
759 projRepAlt arg n i (SucCase sn rhs)
760 = SucCase sn (projRep arg n i rhs)
761 projRepAlt arg n i (DefaultCase rhs)
762 = DefaultCase (projRep arg n i rhs)
764 projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t
766prune _ t = t
768stripLambdas :: CaseDef -> CaseDef
769stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)
770 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
771stripLambdas x = x
773substSC :: Name -> Name -> SC -> SC
774substSC n repl (Case up n' alts)
775 | n == n' = Case up repl (map (substAlt n repl) alts)
776 | otherwise = Case up n' (map (substAlt n repl) alts)
777substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
778substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg
779substSC n repl ImpossibleCase = ImpossibleCase
780substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
782substAlt :: Name -> Name -> CaseAlt -> CaseAlt
783substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
784substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
785substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
786substAlt n repl (SucCase n' sc)
787 | n == n' = SucCase n (substSC n repl sc)
788 | otherwise = SucCase n' (substSC n repl sc)
789substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
791-- mkForce n' n t updates the tree t under the assumption that
792-- n' = force n (so basically updating n to n')
793mkForce :: Name -> Name -> SC -> SC
794mkForce = mkForceSC
795 where
796 mkForceSC n arg (Case up x alts) | x == arg
797 = Case up n $ map (mkForceAlt n arg) alts
799 mkForceSC n arg (Case up x alts)
800 = Case up x (map (mkForceAlt n arg) alts)
802 mkForceSC n arg (ProjCase t alts)
803 = ProjCase t $ map (mkForceAlt n arg) alts
805 mkForceSC n arg c = c
807 mkForceAlt n arg (ConCase cn t args rhs)
808 = ConCase cn t args (mkForceSC n arg rhs)
809 mkForceAlt n arg (FnCase cn args rhs)
810 = FnCase cn args (mkForceSC n arg rhs)
811 mkForceAlt n arg (ConstCase t rhs)
812 = ConstCase t (mkForceSC n arg rhs)
813 mkForceAlt n arg (SucCase sn rhs)
814 = SucCase sn (mkForceSC n arg rhs)
815 mkForceAlt n arg (DefaultCase rhs)
816 = DefaultCase (mkForceSC n arg rhs)