git.iko.soy/Idris-dev
on 593cade help sign in
Idris-dev/src/Idris/Core/CaseTree.hs
867 lines 34 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 sc = removeUnreachable (prune proj (depatt ns' tree))
283 t = CaseDef ns sc (fstT st) in
284 if proj then return (stripLambdas t)
285 else return t
286 Error err -> Error (At fc err)
287 where args = map (\i -> sMN i "e") [0..]
288 fstT (x, _, _) = x
290 -- Check that all pattern variables are reachable by a case split
291 -- Otherwise, they won't make sense on the RHS.
292 chkAccessible (avs, l, c)
293 | phase /= CompileTime || reflect = return (l, c)
294 | otherwise = do mapM_ (acc l) avs
295 return (l, c)
297 acc [] n = Error (Inaccessible n)
298 acc (PV x t : xs) n | x == n = OK ()
299 acc (PCon _ _ _ ps : xs) n = acc (ps ++ xs) n
300 acc (PSuc p : xs) n = acc (p : xs) n
301 acc (_ : xs) n = acc xs n
303data Pat = PCon Bool Name Int [Pat]
304 | PConst Const
305 | PInferred Pat
306 | PV Name Type
307 | PSuc Pat -- special case for n+1 on Integer
308 | PReflected Name [Pat]
309 | PAny
310 | PTyPat -- typecase, not allowed, inspect last
311 deriving Show
313-- If there are repeated variables, take the *last* one (could be name shadowing
314-- in a where clause, so take the most recent).
316toPats :: Bool -> Bool -> Term -> [Pat]
317toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
318 getArgs (App _ f a) = a : getArgs f
319 getArgs _ = []
321toPat :: Bool -> Bool -> [Term] -> [Pat]
322toPat reflect tc = map $ toPat' []
323 where
324 toPat' [_,_,arg] (P (DCon t a uniq) nm@(UN n) _)
325 | n == txt "Delay"
326 = PCon uniq nm t [PAny, PAny, toPat' [] arg]
328 toPat' args (P (DCon t a uniq) nm@(NS (UN n) [own]) _)
329 | n == txt "Read" && own == txt "Ownership"
330 = PCon False nm t (map shareCons (map (toPat' []) args))
331 where shareCons (PCon _ n i ps) = PCon False n i (map shareCons ps)
332 shareCons p = p
334 toPat' args (P (DCon t a uniq) n _)
335 = PCon uniq n t $ map (toPat' []) args
337 -- n + 1
338 toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)
339 | pabi == txt "prim__addBigInt"
340 = PSuc $ toPat' [] p
342 toPat' [] (P Bound n ty) = PV n ty
343 toPat' args (App _ f a) = toPat' (a : args) f
344 toPat' args (Inferred tm) = PInferred (toPat' args tm)
345 toPat' [] (Constant x) | isTypeConst x = PTyPat
346 | otherwise = PConst x
348 toPat' [] (Bind n (Pi _ _ t _) sc)
349 | reflect && noOccurrence n sc
350 = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]
352 toPat' args (P _ n _)
353 | reflect
354 = PReflected n $ map (toPat' []) args
356 toPat' _ t = PAny
358data Partition = Cons [Clause]
359 | Vars [Clause]
360 deriving Show
362isVarPat (PV _ _ : ps , _) = True
363isVarPat (PAny : ps , _) = True
364isVarPat (PTyPat : ps , _) = True
365isVarPat _ = False
367isConPat (PCon _ _ _ _ : ps, _) = True
368isConPat (PReflected _ _ : ps, _) = True
369isConPat (PSuc _ : ps, _) = True
370isConPat (PConst _ : ps, _) = True
371isConPat _ = False
373partition :: [Clause] -> [Partition]
374partition [] = []
375partition ms@(m : _)
376 | isVarPat m = let (vars, rest) = span isVarPat ms in
377 Vars vars : partition rest
378 | isConPat m = let (cons, rest) = span isConPat ms in
379 Cons cons : partition rest
380partition xs = error $ "Partition " ++ show xs
382-- reorder the patterns so that the one with most distinct names
383-- comes next. Take rightmost first, otherwise (i.e. pick value rather
384-- than dependency)
385--
386-- The first argument means [(Name, IsInaccessible)].
388order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
389-- do nothing at compile time: FIXME (EB): Put this in after checking
390-- implications for Franck's reflection work... see issue 3233
391-- order CompileTime ns cs _ = (map fst ns, cs)
392order _ [] cs cans = ([], cs)
393order _ ns' [] cans = (map fst ns', [])
394order (CoverageCheck pos) ns' cs cans
395 = let ns_out = pick 0 [] (map fst ns')
396 cs_out = map pickClause cs in
397 (ns_out, cs_out)
398 where
399 pickClause (pats, def) = (pick 0 [] pats, def)
401 -- Order the list so that things in a position in 'pos' are in the first
402 -- part, then all the other things later. Otherwise preserve order.
403 pick i skipped [] = reverse skipped
404 pick i skipped (x : xs)
405 | i `elem` pos = x : pick (i + 1) skipped xs
406 | otherwise = pick (i + 1) (x : skipped) xs
408order phase ns' cs cans
409 = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))
410 -- only sort the arguments where there is no clash in
411 -- constructor tags between families, the argument type is canonical,
412 -- and no constructor/constant
413 -- clash, because otherwise we can't reliable make the
414 -- case distinction on evaluation
415 (patnames_ord, patnames_rest)
416 = Data.List.partition (noClash . map snd) patnames
417 patnames_ord' = case phase of
418 CompileTime -> patnames_ord
419 -- reversing tends to make better case trees
420 -- and helps erasure
421 RunTime -> reverse patnames_ord
422 pats' = transpose (sortBy moreDistinct patnames_ord'
423 ++ patnames_rest) in
424 (getNOrder pats', zipWith rebuild pats' cs)
425 where
426 getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)
427 getNOrder (c : _) = map (fst . fst) c
429 rebuild patnames clause = (map (snd . snd) patnames, snd clause)
431 noClash [] = True
432 noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))
433 && noClash ps
435 clashPat (PCon _ _ _ _) (PConst _) = True
436 clashPat (PConst _) (PCon _ _ _ _) = True
437 clashPat (PCon _ _ _ _) (PSuc _) = True
438 clashPat (PSuc _) (PCon _ _ _ _) = True
439 clashPat (PCon _ n i _) (PCon _ n' i' _) | i == i' = n /= n'
440 clashPat _ _ = False
442 -- this compares (+isInaccessible, -numberOfCases)
443 moreDistinct xs ys
444 = compare (snd . fst . head $ xs, numNames [] (map snd ys))
445 (snd . fst . head $ ys, numNames [] (map snd xs))
447 numNames xs ((_, PCon _ n _ _) : ps)
448 | not (Left n `elem` xs) = numNames (Left n : xs) ps
449 numNames xs ((_, PConst c) : ps)
450 | not (Right c `elem` xs) = numNames (Right c : xs) ps
451 numNames xs (_ : ps) = numNames xs ps
452 numNames xs [] = length xs
454-- Reorder the patterns in the clause so that the PInferred patterns come
455-- last. Also strip 'PInferred' from the top level patterns so that we can
456-- go ahead and match.
457orderByInf :: [Name] -> [Clause] -> ([Name], [Clause])
458orderByInf vs cs = let alwaysInf = getInf cs in
459 (selectInf alwaysInf vs,
460 map deInf (map (selectExp alwaysInf) cs))
461 where
462 getInf [] = []
463 getInf [(pats, def)] = infPos 0 pats
464 getInf ((pats, def) : cs) = infPos 0 pats `intersect` getInf cs
466 selectExp :: [Int] -> Clause -> Clause
467 selectExp infs (pats, def)
468 = let (notInf, inf) = splitPats 0 infs [] [] pats in
469 (notInf ++ inf, def)
471 selectInf :: [Int] -> [a] -> [a]
472 selectInf infs ns = let (notInf, inf) = splitPats 0 infs [] [] ns in
473 notInf ++ inf
475 splitPats i infpos notInf inf [] = (reverse notInf, reverse inf)
476 splitPats i infpos notInf inf (p : ps)
477 | i `elem` infpos = splitPats (i + 1) infpos notInf (p : inf) ps
478 | otherwise = splitPats (i + 1) infpos (p : notInf) inf ps
480 infPos i [] = []
481 infPos i (PInferred p : ps) = i : infPos (i + 1) ps
482 infPos i (_ : ps) = infPos (i + 1) ps
484 deInf (pats, def) = (map deInfPat pats, def)
486 deInfPat (PInferred p) = p
487 deInfPat p = p
489match :: [Name] -> [Clause] -> SC -- error case
490 -> CaseBuilder SC
491match [] (([], ret) : xs) err
492 = do (ts, v, ntys) <- get
493 put (ts ++ (map (fst.snd) xs), v, ntys)
494 case snd ret of
495 Impossible -> return ImpossibleCase
496 tm -> return $ STerm tm -- run out of arguments
497match vs cs err = do let (vs', de_inf) = orderByInf vs cs
498 ps = partition de_inf
499 mixture vs' ps err
501mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC
502mixture vs [] err = return err
503mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
504 conRule vs ms fallthrough
505mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
506 varRule vs ms fallthrough
508-- Return the list of inaccessible arguments of a data constructor.
509inaccessibleArgs :: Name -> CaseBuilder [Int]
510inaccessibleArgs n = do
511 getInaccessiblePositions <- ask -- this function is the only thing in the environment
512 return $ getInaccessiblePositions n
514data ConType = CName Name Int -- named constructor
515 | CFn Name -- reflected function name
516 | CSuc -- n+1
517 | CConst Const -- constant, not implemented yet
518 deriving (Show, Eq)
520data Group = ConGroup Bool -- Uniqueness flag
521 ConType -- Constructor
522 [([Pat], Clause)] -- arguments and rest of alternative
523 deriving Show
525conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
526conRule (v:vs) cs err = do groups <- groupCons cs
527 caseGroups (v:vs) groups err
529caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC
530caseGroups (v:vs) gs err = do g <- altGroups gs
531 return $ Case (getShared gs) v (sort g)
532 where
533 getShared (ConGroup True _ _ : _) = Updatable
534 getShared _ = Shared
536 altGroups [] = return [DefaultCase err]
538 altGroups (ConGroup _ (CName n i) args : cs)
539 = (:) <$> altGroup n i args <*> altGroups cs
541 altGroups (ConGroup _ (CFn n) args : cs)
542 = (:) <$> altFnGroup n args <*> altGroups cs
544 altGroups (ConGroup _ CSuc args : cs)
545 = (:) <$> altSucGroup args <*> altGroups cs
547 altGroups (ConGroup _ (CConst c) args : cs)
548 = (:) <$> altConstGroup c args <*> altGroups cs
550 altGroup n i args
551 = do inacc <- inaccessibleArgs n
552 ~(newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
553 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
554 return $ ConCase n i newVars matchCs
556 altFnGroup n args = do ~(newVars, _, [], nextCs) <- argsToAlt [] args
557 matchCs <- match (newVars ++ vs) nextCs err
558 return $ FnCase n newVars matchCs
560 altSucGroup args = do ~([newVar], _, [], nextCs) <- argsToAlt [] args
561 matchCs <- match (newVar:vs) nextCs err
562 return $ SucCase newVar matchCs
564 altConstGroup n args = do ~(_, _, [], nextCs) <- argsToAlt [] args
565 matchCs <- match vs nextCs err
566 return $ ConstCase n matchCs
568-- Returns:
569-- * names of all variables arising from match
570-- * names of accessible variables (subset of all variables)
571-- * names of inaccessible variables (subset of all variables)
572-- * clauses corresponding to (accVars ++ origVars ++ inaccVars)
573argsToAlt :: [Int] -> [([Pat], Clause)] -> CaseBuilder ([Name], [Name], [Name], [Clause])
574argsToAlt _ [] = return ([], [], [], [])
575argsToAlt inacc rs@((r, m) : rest) = do
576 newVars <- getNewVars r
577 let (accVars, inaccVars) = partitionAcc newVars
578 return (newVars, accVars, inaccVars, addRs rs)
579 where
580 -- Create names for new variables arising from the given patterns.
581 getNewVars :: [Pat] -> CaseBuilder [Name]
582 getNewVars [] = return []
583 getNewVars ((PV n t) : ns) = do v <- getVar "e"
584 nsv <- getNewVars ns
586 -- Record the type of the variable.
587 --
588 -- It seems that the ordering is not important
589 -- and we can put (v,t) always in front of "ntys"
590 -- (the varName-type pairs seem to represent a mapping).
591 --
592 -- The code that reads this is currently
593 -- commented out, anyway.
594 (cs, i, ntys) <- get
595 put (cs, i, (v, t) : ntys)
597 return (v : nsv)
599 getNewVars (PAny : ns) = (:) <$> getVar "i" <*> getNewVars ns
600 getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns
601 getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns
603 -- Partition a list of things into (accessible, inaccessible) things,
604 -- according to the list of inaccessible indices.
605 partitionAcc xs =
606 ( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]
607 , [x | (i,x) <- zip [0..] xs, i `elem` inacc]
608 )
610 addRs [] = []
611 addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)
612 where
613 (acc, inacc) = partitionAcc r
615getVar :: String -> CaseBuilder Name
616getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)
618groupCons :: [Clause] -> CaseBuilder [Group]
619groupCons cs = gc [] cs
620 where
621 gc acc [] = return acc
622 gc acc ((p : ps, res) : cs) =
623 do acc' <- addGroup p ps res acc
624 gc acc' cs
625 addGroup p ps res acc = case p of
626 PCon uniq con i args -> return $ addg uniq (CName con i) args (ps, res) acc
627 PConst cval -> return $ addConG cval (ps, res) acc
628 PSuc n -> return $ addg False CSuc [n] (ps, res) acc
629 PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc
630 pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"
632 addg uniq c conargs res []
633 = [ConGroup uniq c [(conargs, res)]]
634 addg uniq c conargs res (g@(ConGroup _ c' cs):gs)
635 | c == c' = ConGroup uniq c (cs ++ [(conargs, res)]) : gs
636 | otherwise = g : addg uniq c conargs res gs
638 addConG con res [] = [ConGroup False (CConst con) [([], res)]]
639 addConG con res (g@(ConGroup False (CConst n) cs) : gs)
640 | con == n = ConGroup False (CConst n) (cs ++ [([], res)]) : gs
641-- | otherwise = g : addConG con res gs
642 addConG con res (g : gs) = g : addConG con res gs
644varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
645varRule (v : vs) alts err =
646 do alts' <- mapM (repVar v) alts
647 match vs alts' err
648 where
649 repVar v (PV p ty : ps , (lhs, res))
650 = do (cs, i, ntys) <- get
651 put (cs, i, (v, ty) : ntys)
652 return (ps, (lhs, subst p (P Bound v ty) res))
653 repVar v (PAny : ps , res) = return (ps, res)
654 repVar v (PTyPat : ps , res) = return (ps, res)
656-- fix: case e of S k -> f (S k) ==> case e of S k -> f e
658depatt :: [Name] -> SC -> SC
659depatt ns tm = dp [] tm
660 where
661 dp ms (STerm tm) = STerm (applyMaps ms tm)
662 dp ms (Case up x alts) = Case up x (map (dpa ms x) alts)
663 dp ms sc = sc
665 dpa ms x (ConCase n i args sc)
666 = ConCase n i args (dp ((x, (n, args)) : ms) sc)
667 dpa ms x (FnCase n args sc)
668 = FnCase n args (dp ((x, (n, args)) : ms) sc)
669 dpa ms x (ConstCase c sc) = ConstCase c (dp ms sc)
670 dpa ms x (SucCase n sc) = SucCase n (dp ms sc)
671 dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)
673 applyMaps ms f@(App _ _ _)
674 | (P nt cn pty, args) <- unApply f
675 = let args' = map (applyMaps ms) args in
676 applyMap ms nt cn pty args'
677 where
678 applyMap [] nt cn pty args' = mkApp (P nt cn pty) args'
679 applyMap ((x, (n, args)) : ms) nt cn pty args'
680 | and ((length args == length args') :
681 (n == cn) : zipWith same args args') = P Ref x Erased
682 | otherwise = applyMap ms nt cn pty args'
683 same n (P _ n' _) = n == n'
684 same _ _ = False
686 applyMaps ms (App s f a) = App s (applyMaps ms f) (applyMaps ms a)
687 applyMaps ms t = t
689-- FIXME: Do this for SucCase too
690-- Issue #1719 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1719
691prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)
692 -> SC -> SC
693prune proj (Case up n alts) = case alts' of
694 [] -> ImpossibleCase
696 -- Projection transformations prevent us from seeing some uses of ctor fields
697 -- because they delete information about which ctor is being used.
698 -- Consider:
699 -- f (X x) = ... x ...
700 -- vs.
701 -- f x = ... x!0 ...
702 --
703 -- Hence, we disable this step.
704 -- TODO: re-enable this in toIR
705 --
706 -- as@[ConCase cn i args sc]
707 -- | proj -> mkProj n 0 args (prune proj sc)
708 -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs
710 -- If none of the args are used in the sc, however, we can just replace it
711 -- with sc
712 as@[ConCase cn i args sc]
713 | proj -> let sc' = prune proj sc in
714 if any (isUsed sc') args
715 then Case up n [ConCase cn i args sc']
716 else sc'
718 [SucCase cn sc]
719 | proj
720 -> projRep cn n (-1) $ prune proj sc
722 [ConstCase _ sc]
723 -> prune proj sc
725 -- Bit of a hack here! The default case will always be 0, make sure
726 -- it gets caught first.
727 [s@(SucCase _ _), DefaultCase dc]
728 -> Case up n [ConstCase (BI 0) dc, s]
730 as -> Case up n as
731 where
732 alts' = filter (not . erased) $ map pruneAlt alts
734 pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)
735 pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)
736 pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)
737 pruneAlt (SucCase n sc) = SucCase n (prune proj sc)
738 pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)
740 erased (DefaultCase (STerm Erased)) = True
741 erased (DefaultCase ImpossibleCase) = True
742 erased _ = False
744 projRep :: Name -> Name -> Int -> SC -> SC
745 projRep arg n i (Case up x alts) | x == arg
746 = ProjCase (Proj (P Bound n Erased) i) $ map (projRepAlt arg n i) alts
747 projRep arg n i (Case up x alts)
748 = Case up x (map (projRepAlt arg n i) alts)
749 projRep arg n i (ProjCase t alts)
750 = ProjCase (projRepTm arg n i t) $ map (projRepAlt arg n i) alts
751 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)
752 projRep arg n i c = c
754 projRepAlt arg n i (ConCase cn t args rhs)
755 = ConCase cn t args (projRep arg n i rhs)
756 projRepAlt arg n i (FnCase cn args rhs)
757 = FnCase cn args (projRep arg n i rhs)
758 projRepAlt arg n i (ConstCase t rhs)
759 = ConstCase t (projRep arg n i rhs)
760 projRepAlt arg n i (SucCase sn rhs)
761 = SucCase sn (projRep arg n i rhs)
762 projRepAlt arg n i (DefaultCase rhs)
763 = DefaultCase (projRep arg n i rhs)
765 projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t
767prune _ t = t
769-- Remove any branches we can't reach because of variables we've already
770-- tested
771removeUnreachable :: SC -> SC
772removeUnreachable sc = ru [] sc
773 where
774 -- keep a mapping from variable names, to the constructor tag we've
775 -- already checked it as in this branch
776 ru :: [(Name, Int)] -> SC -> SC
777 ru checked (Case t n alts)
778 = let alts' = map (ruAlt checked n) (dropImpossible (lookup n checked) alts) in
779 Case t n alts'
780 ru checked t = t
782 dropImpossible Nothing alts = alts
783 dropImpossible (Just t) [] = []
784 dropImpossible (Just t) (ConCase con tag args sc : rest)
785 | t == tag = [ConCase con tag args sc] -- must be this case
786 | otherwise = dropImpossible (Just t) rest -- can't be this case
787 dropImpossible (Just t) (c : rest)
788 = c : dropImpossible (Just t) rest
790 ruAlt :: [(Name, Int)] -> Name -> CaseAlt -> CaseAlt
791 ruAlt checked var (ConCase con tag args sc)
792 = let checked' = dropChecked args (updateChecked var tag checked)
793 sc' = ru checked' sc in
794 ConCase con tag args sc'
795 ruAlt checked var (FnCase n args sc)
796 = let checked' = dropChecked [var] checked
797 sc' = ru checked' sc in
798 FnCase n args sc'
799 ruAlt checked var (ConstCase c sc)
800 = let checked' = dropChecked [var] checked
801 sc' = ru checked' sc in
802 ConstCase c sc'
803 ruAlt checked var (SucCase n sc)
804 = let checked' = dropChecked [var] checked
805 sc' = ru checked' sc in
806 SucCase n sc'
807 ruAlt checked var (DefaultCase sc)
808 = let checked' = dropChecked [var] checked
809 sc' = ru checked' sc in
810 DefaultCase sc'
812 updateChecked :: Name -> Int -> [(Name, Int)] -> [(Name, Int)]
813 updateChecked n i checked
814 = (n, i) : filter (\x -> fst x /= n) checked
816 dropChecked :: [Name] -> [(Name, Int)] -> [(Name, Int)]
817 dropChecked ns checked = filter (\x -> fst x `notElem` ns) checked
819stripLambdas :: CaseDef -> CaseDef
820stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)
821 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
822stripLambdas x = x
824substSC :: Name -> Name -> SC -> SC
825substSC n repl (Case up n' alts)
826 | n == n' = Case up repl (map (substAlt n repl) alts)
827 | otherwise = Case up n' (map (substAlt n repl) alts)
828substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
829substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg
830substSC n repl ImpossibleCase = ImpossibleCase
831substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
833substAlt :: Name -> Name -> CaseAlt -> CaseAlt
834substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
835substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
836substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
837substAlt n repl (SucCase n' sc)
838 | n == n' = SucCase n (substSC n repl sc)
839 | otherwise = SucCase n' (substSC n repl sc)
840substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
842-- mkForce n' n t updates the tree t under the assumption that
843-- n' = force n (so basically updating n to n')
844mkForce :: Name -> Name -> SC -> SC
845mkForce = mkForceSC
846 where
847 mkForceSC n arg (Case up x alts) | x == arg
848 = Case up n $ map (mkForceAlt n arg) alts
850 mkForceSC n arg (Case up x alts)
851 = Case up x (map (mkForceAlt n arg) alts)
853 mkForceSC n arg (ProjCase t alts)
854 = ProjCase t $ map (mkForceAlt n arg) alts
856 mkForceSC n arg c = c
858 mkForceAlt n arg (ConCase cn t args rhs)
859 = ConCase cn t args (mkForceSC n arg rhs)
860 mkForceAlt n arg (FnCase cn args rhs)
861 = FnCase cn args (mkForceSC n arg rhs)
862 mkForceAlt n arg (ConstCase t rhs)
863 = ConstCase t (mkForceSC n arg rhs)
864 mkForceAlt n arg (SucCase sn rhs)
865 = SucCase sn (mkForceSC n arg rhs)
866 mkForceAlt n arg (DefaultCase rhs)
867 = DefaultCase (mkForceSC n arg rhs)