git.iko.soy/Idris-dev
on 5cf643e help sign in
Idris-dev/src/Idris/Core/CaseTree.hs
817 lines 32 kB history raw
1{-|
2Module : Idris.Core.CaseTree
3Description : Module to define and interact with case trees.
4Copyright :
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-}
21{-# LANGUAGE DeriveFunctor, DeriveGeneric, PatternGuards, TypeSynonymInstances
22 #-}
24module Idris.Core.CaseTree (
25 CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
26 , Phase(..), CaseTree, CaseType(..)
27 , simpleCase, small, namesUsed, findCalls, findCalls', findUsedArgs
28 , substSC, substAlt, mkForce
29 ) where
31import Idris.Core.TT
33import Control.Applicative hiding (Const)
34import Control.Monad.Reader
35import Control.Monad.State
36import Data.List hiding (partition)
37import qualified Data.List (partition)
38import Data.Maybe
39import Debug.Trace
40import GHC.Generics (Generic)
42data CaseDef = CaseDef [Name] !SC [Term]
43 deriving Show
45data SC' t = Case CaseType Name [CaseAlt' t] -- ^ invariant: lowest tags first
46 | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection
47 | STerm !t
48 | UnmatchedCase String -- ^ error message
49 | ImpossibleCase -- ^ already checked to be impossible
50 deriving (Eq, Ord, Functor, Generic)
51{-!
52deriving instance Binary SC'
53!-}
55data CaseType = Updatable | Shared
56 deriving (Eq, Ord, Show, Generic)
58type SC = SC' Term
60data CaseAlt' t = ConCase Name Int [Name] !(SC' t)
61 | FnCase Name [Name] !(SC' t) -- ^ reflection function
62 | ConstCase Const !(SC' t)
63 | SucCase Name !(SC' t)
64 | DefaultCase !(SC' t)
65 deriving (Show, Eq, Ord, Functor, Generic)
66{-!
67deriving instance Binary CaseAlt'
68!-}
70type CaseAlt = CaseAlt' Term
72instance Show t => Show (SC' t) where
73 show sc = show' 1 sc
74 where
75 show' i (Case up n alts) = "case" ++ u ++ show n ++ " of\n" ++ indent i ++
76 showSep ("\n" ++ indent i) (map (showA i) alts)
77 where u = case up of
78 Updatable -> "! "
79 Shared -> " "
80 show' i (ProjCase tm alts) = "case " ++ show tm ++ " of " ++
81 showSep ("\n" ++ indent i) (map (showA i) alts)
82 show' i (STerm tm) = show tm
83 show' i (UnmatchedCase str) = "error " ++ show str
84 show' i ImpossibleCase = "impossible"
86 indent i = concat $ take i (repeat " ")
88 showA i (ConCase n t args sc)
89 = show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
90 ++ show' (i+1) sc
91 showA i (FnCase n args sc)
92 = "FN " ++ show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
93 ++ show' (i+1) sc
94 showA i (ConstCase t sc)
95 = show t ++ " => " ++ show' (i+1) sc
96 showA i (SucCase n sc)
97 = show n ++ "+1 => " ++ show' (i+1) sc
98 showA i (DefaultCase sc)
99 = "_ => " ++ show' (i+1) sc
102type CaseTree = SC
103type Clause = ([Pat], (Term, Term))
104type CS = ([Term], Int, [(Name, Type)])
106instance TermSize SC where
107 termsize n (Case _ n' as) = termsize n as
108 termsize n (ProjCase n' as) = termsize n as
109 termsize n (STerm t) = termsize n t
110 termsize n _ = 1
112instance TermSize CaseAlt where
113 termsize n (ConCase _ _ _ s) = termsize n s
114 termsize n (FnCase _ _ s) = termsize n s
115 termsize n (ConstCase _ s) = termsize n s
116 termsize n (SucCase _ s) = termsize n s
117 termsize n (DefaultCase s) = termsize n s
119-- simple terms can be inlined trivially - good for primitives in particular
120-- To avoid duplicating work, don't inline something which uses one
121-- of its arguments in more than one place
123small :: Name -> [Name] -> SC -> Bool
124small n args t = let as = findAllUsedArgs t args in
125 length as == length (nub as) &&
126 termsize n t < 10
128namesUsed :: SC -> [Name]
129namesUsed sc = nub $ nu' [] sc where
130 nu' ps (Case _ n alts) = nub (concatMap (nua ps) alts) \\ [n]
131 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts
132 nu' ps (STerm t) = nub $ nut ps t
133 nu' ps _ = []
135 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args
136 nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc) \\ args
137 nua ps (ConstCase _ sc) = nu' ps sc
138 nua ps (SucCase _ sc) = nu' ps sc
139 nua ps (DefaultCase sc) = nu' ps sc
141 nut ps (P _ n _) | n `elem` ps = []
142 | otherwise = [n]
143 nut ps (App _ f a) = nut ps f ++ nut ps a
144 nut ps (Proj t _) = nut ps t
145 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc
146 nut ps (Bind n b sc) = nut (n:ps) sc
147 nut ps _ = []
149-- | Return all called functions, and which arguments are used
150-- in each argument position for the call, in order to help reduce
151-- compilation time, and trace all unused arguments
152findCalls :: SC -> [Name] -> [(Name, [[Name]])]
153findCalls = findCalls' False
155findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]
156findCalls' ignoreasserts sc topargs = nub $ nu' topargs sc where
157 nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)
158 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts
159 nu' ps (STerm t) = nub $ nut ps t
160 nu' ps _ = []
162 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc)
163 nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc)
164 nua ps (ConstCase _ sc) = nu' ps sc
165 nua ps (SucCase _ sc) = nu' ps sc
166 nua ps (DefaultCase sc) = nu' ps sc
168 nut ps (P _ n _) | n `elem` ps = []
169 | otherwise = [(n, [])] -- tmp
170 nut ps fn@(App _ f a)
171 | (P _ n _, args) <- unApply fn
172 = if ignoreasserts && n == sUN "assert_total"
173 then []
174 else if n `elem` ps
175 then nut ps f ++ nut ps a
176 else [(n, map argNames args)] ++ concatMap (nut ps) args
177 | (P (TCon _ _) n _, _) <- unApply fn = []
178 | otherwise = nut ps f ++ nut ps a
179 nut ps (Bind n (Let t v) sc) = 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 _ = []
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 = CompileTime | RunTime
246 deriving (Show, Eq)
248-- Generate a simple case tree
249-- Work Right to Left
251simpleCase :: Bool -> SC -> Bool ->
252 Phase -> FC -> [Int] ->
253 [(Type, Bool)] -> -- (Argument type, whether it's canonical)
254 [([Name], Term, Term)] ->
255 ErasureInfo ->
256 TC CaseDef
257simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
258 = sc' tc defcase phase fc (filter (\(_, _, r) ->
259 case r of
260 Impossible -> False
261 _ -> True) cs)
262 where
263 sc' tc defcase phase fc []
264 = return $ CaseDef [] (UnmatchedCase (show fc ++ ":No pattern clauses")) []
265 sc' tc defcase phase fc cs
266 = let proj = phase == RunTime
267 vnames = fstT (head cs)
268 pats = map (\ (avs, l, r) ->
269 (avs, toPats reflect tc l, (l, r))) cs
270 chkPats = mapM chkAccessible pats in
271 case chkPats of
272 OK pats ->
273 let numargs = length (fst (head pats))
274 ns = take numargs args
275 (ns', ps') = order phase [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats (map snd argtys)
276 (tree, st) = runCaseBuilder erInfo
277 (match ns' ps' defcase)
278 ([], numargs, [])
279 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
280 if proj then return (stripLambdas t)
281 else return t
282 Error err -> Error (At fc err)
283 where args = map (\i -> sMN i "e") [0..]
284 defaultCase True = STerm Erased
285 defaultCase False = UnmatchedCase "Error"
286 fstT (x, _, _) = x
287 lstT (_, _, 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 == RunTime || 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
302-- For each 'Case', make sure every choice is in the same type family,
303-- as directed by the variable type (i.e. there is no implicit type casing
304-- going on).
306checkSameTypes :: [(Name, Type)] -> SC -> Bool
307checkSameTypes tys (Case _ n alts)
308 = case lookup n tys of
309 Just t -> and (map (checkAlts t) alts)
310 _ -> and (map ((checkSameTypes tys).getSC) alts)
311 where
312 checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc
313 checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc
314 checkAlts _ (ConstCase c sc) = False
315 checkAlts _ _ = True
317 getSC (ConCase _ _ _ sc) = sc
318 getSC (FnCase _ _ sc) = sc
319 getSC (ConstCase _ sc) = sc
320 getSC (SucCase _ sc) = sc
321 getSC (DefaultCase sc) = sc
322checkSameTypes _ _ = True
324-- FIXME: All we're actually doing here is checking that we haven't arrived
325-- at a specific constructor for a polymorphic argument. I *think* this
326-- is sufficient, but if it turns out not to be, fix it!
327--
328-- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718
329isType n t | (P (TCon _ _) _ _, _) <- unApply t = True
330isType n t | (P Ref _ _, _) <- unApply t = True
331isType n t = False
333isConstType (I _) (AType (ATInt ITNative)) = True
334isConstType (BI _) (AType (ATInt ITBig)) = True
335isConstType (Fl _) (AType ATFloat) = True
336isConstType (Ch _) (AType (ATInt ITChar)) = True
337isConstType (Str _) StrType = True
338isConstType (B8 _) (AType (ATInt _)) = True
339isConstType (B16 _) (AType (ATInt _)) = True
340isConstType (B32 _) (AType (ATInt _)) = True
341isConstType (B64 _) (AType (ATInt _)) = True
342isConstType _ _ = False
344data Pat = PCon Bool Name Int [Pat]
345 | PConst Const
346 | PV Name Type
347 | PSuc Pat -- special case for n+1 on Integer
348 | PReflected Name [Pat]
349 | PAny
350 | PTyPat -- typecase, not allowed, inspect last
351 deriving Show
353-- If there are repeated variables, take the *last* one (could be name shadowing
354-- in a where clause, so take the most recent).
356toPats :: Bool -> Bool -> Term -> [Pat]
357toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
358 getArgs (App _ f a) = a : getArgs f
359 getArgs _ = []
361toPat :: Bool -> Bool -> [Term] -> [Pat]
362toPat reflect tc = map $ toPat' []
363 where
364 toPat' [_,_,arg] (P (DCon t a uniq) nm@(UN n) _)
365 | n == txt "Delay"
366 = PCon uniq nm t [PAny, PAny, toPat' [] arg]
368 toPat' args (P (DCon t a uniq) nm@(NS (UN n) [own]) _)
369 | n == txt "Read" && own == txt "Ownership"
370 = PCon False nm t (map shareCons (map (toPat' []) args))
371 where shareCons (PCon _ n i ps) = PCon False n i (map shareCons ps)
372 shareCons p = p
374 toPat' args (P (DCon t a uniq) n _)
375 = PCon uniq n t $ map (toPat' []) args
377 -- n + 1
378 toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)
379 | pabi == txt "prim__addBigInt"
380 = PSuc $ toPat' [] p
382 toPat' [] (P Bound n ty) = PV n ty
383 toPat' args (App _ f a) = toPat' (a : args) f
384 toPat' [] (Constant x) | isTypeConst x = PTyPat
385 | otherwise = PConst x
387 toPat' [] (Bind n (Pi _ t _) sc)
388 | reflect && noOccurrence n sc
389 = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]
391 toPat' args (P _ n _)
392 | reflect
393 = PReflected n $ map (toPat' []) args
395 toPat' _ t = PAny
397 fixedN IT8 = "Bits8"
398 fixedN IT16 = "Bits16"
399 fixedN IT32 = "Bits32"
400 fixedN IT64 = "Bits64"
403data Partition = Cons [Clause]
404 | Vars [Clause]
405 deriving Show
407isVarPat (PV _ _ : ps , _) = True
408isVarPat (PAny : ps , _) = True
409isVarPat (PTyPat : ps , _) = True
410isVarPat _ = False
412isConPat (PCon _ _ _ _ : ps, _) = True
413isConPat (PReflected _ _ : ps, _) = True
414isConPat (PSuc _ : ps, _) = True
415isConPat (PConst _ : ps, _) = True
416isConPat _ = False
418partition :: [Clause] -> [Partition]
419partition [] = []
420partition ms@(m : _)
421 | isVarPat m = let (vars, rest) = span isVarPat ms in
422 Vars vars : partition rest
423 | isConPat m = let (cons, rest) = span isConPat ms in
424 Cons cons : partition rest
425partition xs = error $ "Partition " ++ show xs
427-- reorder the patterns so that the one with most distinct names
428-- comes next. Take rightmost first, otherwise (i.e. pick value rather
429-- than dependency)
430--
431-- The first argument means [(Name, IsInaccessible)].
433order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
434-- do nothing at compile time: FIXME (EB): Put this in after checking
435-- implications for Franck's reflection work... see issue 3233
436-- order CompileTime ns cs _ = (map fst ns, cs)
437order _ [] cs cans = ([], cs)
438order _ ns' [] cans = (map fst ns', [])
439order phase ns' cs cans
440 = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))
441 -- only sort the arguments where there is no clash in
442 -- constructor tags between families, the argument type is canonical,
443 -- and no constructor/constant
444 -- clash, because otherwise we can't reliable make the
445 -- case distinction on evaluation
446 (patnames_ord, patnames_rest)
447 = Data.List.partition (noClash . map snd) patnames
448 patnames_ord' = case phase of
449 CompileTime -> patnames_ord
450 -- reversing tends to make better case trees
451 -- and helps erasure
452 RunTime -> reverse patnames_ord
453 pats' = transpose (sortBy moreDistinct patnames_ord'
454 ++ patnames_rest) in
455 (getNOrder pats', zipWith rebuild pats' cs)
456 where
457 getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)
458 getNOrder (c : _) = map (fst . fst) c
460 rebuild patnames clause = (map (snd . snd) patnames, snd clause)
462 noClash [] = True
463 noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))
464 && noClash ps
466 clashPat (PCon _ _ _ _) (PConst _) = True
467 clashPat (PConst _) (PCon _ _ _ _) = True
468 clashPat (PCon _ _ _ _) (PSuc _) = True
469 clashPat (PSuc _) (PCon _ _ _ _) = True
470 clashPat (PCon _ n i _) (PCon _ n' i' _) | i == i' = n /= n'
471 clashPat _ _ = False
473 -- this compares (+isInaccessible, -numberOfCases)
474 moreDistinct xs ys
475 = compare (snd . fst . head $ xs, numNames [] (map snd ys))
476 (snd . fst . head $ ys, numNames [] (map snd xs))
478 numNames xs ((_, PCon _ n _ _) : ps)
479 | not (Left n `elem` xs) = numNames (Left n : xs) ps
480 numNames xs ((_, PConst c) : ps)
481 | not (Right c `elem` xs) = numNames (Right c : xs) ps
482 numNames xs (_ : ps) = numNames xs ps
483 numNames xs [] = length xs
485match :: [Name] -> [Clause] -> SC -- error case
486 -> CaseBuilder SC
487match [] (([], ret) : xs) err
488 = do (ts, v, ntys) <- get
489 put (ts ++ (map (fst.snd) xs), v, ntys)
490 case snd ret of
491 Impossible -> return ImpossibleCase
492 tm -> return $ STerm tm -- run out of arguments
493match vs cs err = do let ps = partition cs
494 mixture vs ps err
496mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC
497mixture vs [] err = return err
498mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
499 conRule vs ms fallthrough
500mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
501 varRule vs ms fallthrough
503-- Return the list of inaccessible arguments of a data constructor.
504inaccessibleArgs :: Name -> CaseBuilder [Int]
505inaccessibleArgs n = do
506 getInaccessiblePositions <- ask -- this function is the only thing in the environment
507 return $ getInaccessiblePositions n
509data ConType = CName Name Int -- named constructor
510 | CFn Name -- reflected function name
511 | CSuc -- n+1
512 | CConst Const -- constant, not implemented yet
513 deriving (Show, Eq)
515data Group = ConGroup Bool -- Uniqueness flag
516 ConType -- Constructor
517 [([Pat], Clause)] -- arguments and rest of alternative
518 deriving Show
520conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
521conRule (v:vs) cs err = do groups <- groupCons cs
522 caseGroups (v:vs) groups err
524caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC
525caseGroups (v:vs) gs err = do g <- altGroups gs
526 return $ Case (getShared gs) v (sort g)
527 where
528 getShared (ConGroup True _ _ : _) = Updatable
529 getShared _ = Shared
531 altGroups [] = return [DefaultCase err]
533 altGroups (ConGroup _ (CName n i) args : cs)
534 = (:) <$> altGroup n i args <*> altGroups cs
536 altGroups (ConGroup _ (CFn n) args : cs)
537 = (:) <$> altFnGroup n args <*> altGroups cs
539 altGroups (ConGroup _ CSuc args : cs)
540 = (:) <$> altSucGroup args <*> altGroups cs
542 altGroups (ConGroup _ (CConst c) args : cs)
543 = (:) <$> altConstGroup c args <*> altGroups cs
545 altGroup n i args
546 = do inacc <- inaccessibleArgs n
547 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
548 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
549 return $ ConCase n i newVars matchCs
551 altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args
552 matchCs <- match (newVars ++ vs) nextCs err
553 return $ FnCase n newVars matchCs
555 altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args
556 matchCs <- match (newVar:vs) nextCs err
557 return $ SucCase newVar matchCs
559 altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args
560 matchCs <- match vs nextCs err
561 return $ ConstCase n matchCs
563-- Returns:
564-- * names of all variables arising from match
565-- * names of accessible variables (subset of all variables)
566-- * names of inaccessible variables (subset of all variables)
567-- * clauses corresponding to (accVars ++ origVars ++ inaccVars)
568argsToAlt :: [Int] -> [([Pat], Clause)] -> CaseBuilder ([Name], [Name], [Name], [Clause])
569argsToAlt _ [] = return ([], [], [], [])
570argsToAlt inacc rs@((r, m) : rest) = do
571 newVars <- getNewVars r
572 let (accVars, inaccVars) = partitionAcc newVars
573 return (newVars, accVars, inaccVars, addRs rs)
574 where
575 -- Create names for new variables arising from the given patterns.
576 getNewVars :: [Pat] -> CaseBuilder [Name]
577 getNewVars [] = return []
578 getNewVars ((PV n t) : ns) = do v <- getVar "e"
579 nsv <- getNewVars ns
581 -- Record the type of the variable.
582 --
583 -- It seems that the ordering is not important
584 -- and we can put (v,t) always in front of "ntys"
585 -- (the varName-type pairs seem to represent a mapping).
586 --
587 -- The code that reads this is currently
588 -- commented out, anyway.
589 (cs, i, ntys) <- get
590 put (cs, i, (v, t) : ntys)
592 return (v : nsv)
594 getNewVars (PAny : ns) = (:) <$> getVar "i" <*> getNewVars ns
595 getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns
596 getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns
598 -- Partition a list of things into (accessible, inaccessible) things,
599 -- according to the list of inaccessible indices.
600 partitionAcc xs =
601 ( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]
602 , [x | (i,x) <- zip [0..] xs, i `elem` inacc]
603 )
605 addRs [] = []
606 addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)
607 where
608 (acc, inacc) = partitionAcc r
610 uniq i (UN n) = MN i n
611 uniq i n = n
613getVar :: String -> CaseBuilder Name
614getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)
616groupCons :: [Clause] -> CaseBuilder [Group]
617groupCons cs = gc [] cs
618 where
619 gc acc [] = return acc
620 gc acc ((p : ps, res) : cs) =
621 do acc' <- addGroup p ps res acc
622 gc acc' cs
623 addGroup p ps res acc = case p of
624 PCon uniq con i args -> return $ addg uniq (CName con i) args (ps, res) acc
625 PConst cval -> return $ addConG cval (ps, res) acc
626 PSuc n -> return $ addg False CSuc [n] (ps, res) acc
627 PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc
628 pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"
630 addg uniq c conargs res []
631 = [ConGroup uniq c [(conargs, res)]]
632 addg uniq c conargs res (g@(ConGroup _ c' cs):gs)
633 | c == c' = ConGroup uniq c (cs ++ [(conargs, res)]) : gs
634 | otherwise = g : addg uniq c conargs res gs
636 addConG con res [] = [ConGroup False (CConst con) [([], res)]]
637 addConG con res (g@(ConGroup False (CConst n) cs) : gs)
638 | con == n = ConGroup False (CConst n) (cs ++ [([], res)]) : gs
639-- | otherwise = g : addConG con res gs
640 addConG con res (g : gs) = g : addConG con res gs
642varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
643varRule (v : vs) alts err =
644 do alts' <- mapM (repVar v) alts
645 match vs alts' err
646 where
647 repVar v (PV p ty : ps , (lhs, res))
648 = do (cs, i, ntys) <- get
649 put (cs, i, (v, ty) : ntys)
650 return (ps, (lhs, subst p (P Bound v ty) res))
651 repVar v (PAny : ps , res) = return (ps, res)
652 repVar v (PTyPat : ps , res) = return (ps, res)
654-- fix: case e of S k -> f (S k) ==> case e of S k -> f e
656depatt :: [Name] -> SC -> SC
657depatt ns tm = dp [] tm
658 where
659 dp ms (STerm tm) = STerm (applyMaps ms tm)
660 dp ms (Case up x alts) = Case up x (map (dpa ms x) alts)
661 dp ms sc = sc
663 dpa ms x (ConCase n i args sc)
664 = ConCase n i args (dp ((x, (n, args)) : ms) sc)
665 dpa ms x (FnCase n args sc)
666 = FnCase n args (dp ((x, (n, args)) : ms) sc)
667 dpa ms x (ConstCase c sc) = ConstCase c (dp ms sc)
668 dpa ms x (SucCase n sc) = SucCase n (dp ms sc)
669 dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)
671 applyMaps ms f@(App _ _ _)
672 | (P nt cn pty, args) <- unApply f
673 = let args' = map (applyMaps ms) args in
674 applyMap ms nt cn pty args'
675 where
676 applyMap [] nt cn pty args' = mkApp (P nt cn pty) args'
677 applyMap ((x, (n, args)) : ms) nt cn pty args'
678 | and ((length args == length args') :
679 (n == cn) : zipWith same args args') = P Ref x Erased
680 | otherwise = applyMap ms nt cn pty args'
681 same n (P _ n' _) = n == n'
682 same _ _ = False
684 applyMaps ms (App s f a) = App s (applyMaps ms f) (applyMaps ms a)
685 applyMaps ms t = t
687-- FIXME: Do this for SucCase too
688-- Issue #1719 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1719
689prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)
690 -> SC -> SC
691prune proj (Case up n alts) = case alts' of
692 [] -> ImpossibleCase
694 -- Projection transformations prevent us from seeing some uses of ctor fields
695 -- because they delete information about which ctor is being used.
696 -- Consider:
697 -- f (X x) = ... x ...
698 -- vs.
699 -- f x = ... x!0 ...
700 --
701 -- Hence, we disable this step.
702 -- TODO: re-enable this in toIR
703 --
704 -- as@[ConCase cn i args sc]
705 -- | proj -> mkProj n 0 args (prune proj sc)
706 -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs
708 -- If none of the args are used in the sc, however, we can just replace it
709 -- with sc
710 as@[ConCase cn i args sc]
711 | proj -> let sc' = prune proj sc in
712 if any (isUsed sc') args
713 then Case up n [ConCase cn i args sc']
714 else sc'
716 [SucCase cn sc]
717 | proj
718 -> projRep cn n (-1) $ prune proj sc
720 [ConstCase _ sc]
721 -> prune proj sc
723 -- Bit of a hack here! The default case will always be 0, make sure
724 -- it gets caught first.
725 [s@(SucCase _ _), DefaultCase dc]
726 -> Case up n [ConstCase (BI 0) dc, s]
728 as -> Case up n as
729 where
730 alts' = filter (not . erased) $ map pruneAlt alts
732 pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)
733 pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)
734 pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)
735 pruneAlt (SucCase n sc) = SucCase n (prune proj sc)
736 pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)
738 erased (DefaultCase (STerm Erased)) = True
739 erased (DefaultCase ImpossibleCase) = True
740 erased _ = False
742 projRep :: Name -> Name -> Int -> SC -> SC
743 projRep arg n i (Case up x alts) | x == arg
744 = ProjCase (Proj (P Bound n Erased) i) $ map (projRepAlt arg n i) alts
745 projRep arg n i (Case up x alts)
746 = Case up x (map (projRepAlt arg n i) alts)
747 projRep arg n i (ProjCase t alts)
748 = ProjCase (projRepTm arg n i t) $ map (projRepAlt arg n i) alts
749 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)
750 projRep arg n i c = c
752 projRepAlt arg n i (ConCase cn t args rhs)
753 = ConCase cn t args (projRep arg n i rhs)
754 projRepAlt arg n i (FnCase cn args rhs)
755 = FnCase cn args (projRep arg n i rhs)
756 projRepAlt arg n i (ConstCase t rhs)
757 = ConstCase t (projRep arg n i rhs)
758 projRepAlt arg n i (SucCase sn rhs)
759 = SucCase sn (projRep arg n i rhs)
760 projRepAlt arg n i (DefaultCase rhs)
761 = DefaultCase (projRep arg n i rhs)
763 projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t
765prune _ t = t
767stripLambdas :: CaseDef -> CaseDef
768stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)
769 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
770stripLambdas x = x
772substSC :: Name -> Name -> SC -> SC
773substSC n repl (Case up n' alts)
774 | n == n' = Case up repl (map (substAlt n repl) alts)
775 | otherwise = Case up n' (map (substAlt n repl) alts)
776substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
777substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg
778substSC n repl ImpossibleCase = ImpossibleCase
779substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
781substAlt :: Name -> Name -> CaseAlt -> CaseAlt
782substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
783substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
784substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
785substAlt n repl (SucCase n' sc)
786 | n == n' = SucCase n (substSC n repl sc)
787 | otherwise = SucCase n' (substSC n repl sc)
788substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
790-- mkForce n' n t updates the tree t under the assumption that
791-- n' = force n (so basically updating n to n')
792mkForce :: Name -> Name -> SC -> SC
793mkForce = mkForceSC
794 where
795 mkForceSC n arg (Case up x alts) | x == arg
796 = Case up n $ map (mkForceAlt n arg) alts
798 mkForceSC n arg (Case up x alts)
799 = Case up x (map (mkForceAlt n arg) alts)
801 mkForceSC n arg (ProjCase t alts)
802 = ProjCase t $ map (mkForceAlt n arg) alts
804 mkForceSC n arg c = c
806 mkForceAlt n arg (ConCase cn t args rhs)
807 = ConCase cn t args (mkForceSC n arg rhs)
808 mkForceAlt n arg (FnCase cn args rhs)
809 = FnCase cn args (mkForceSC n arg rhs)
810 mkForceAlt n arg (ConstCase t rhs)
811 = ConstCase t (mkForceSC n arg rhs)
812 mkForceAlt n arg (SucCase sn rhs)
813 = SucCase sn (mkForceSC n arg rhs)
814 mkForceAlt n arg (DefaultCase rhs)
815 = DefaultCase (mkForceSC n arg rhs)
817 forceTm n arg t = subst n arg t