git.iko.soy/Idris-dev
on ff7ea9d help sign in
Idris-dev/src/Idris/Core/CaseTree.hs
819 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 PatternGuards, DeriveFunctor, TypeSynonymInstances,
22 DeriveGeneric #-}
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.State
35import Control.Monad.Reader
36import Data.Maybe
37import Data.List hiding (partition)
38import qualified Data.List(partition)
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'
53deriving instance NFData SC'
54!-}
56data CaseType = Updatable | Shared
57 deriving (Eq, Ord, Show, Generic)
59type SC = SC' Term
61data CaseAlt' t = ConCase Name Int [Name] !(SC' t)
62 | FnCase Name [Name] !(SC' t) -- ^ reflection function
63 | ConstCase Const !(SC' t)
64 | SucCase Name !(SC' t)
65 | DefaultCase !(SC' t)
66 deriving (Show, Eq, Ord, Functor, Generic)
67{-!
68deriving instance Binary CaseAlt'
69deriving instance NFData CaseAlt'
70!-}
72type CaseAlt = CaseAlt' Term
74instance Show t => Show (SC' t) where
75 show sc = show' 1 sc
76 where
77 show' i (Case up n alts) = "case" ++ u ++ show n ++ " of\n" ++ indent i ++
78 showSep ("\n" ++ indent i) (map (showA i) alts)
79 where u = case up of
80 Updatable -> "! "
81 Shared -> " "
82 show' i (ProjCase tm alts) = "case " ++ show tm ++ " of " ++
83 showSep ("\n" ++ indent i) (map (showA i) alts)
84 show' i (STerm tm) = show tm
85 show' i (UnmatchedCase str) = "error " ++ show str
86 show' i ImpossibleCase = "impossible"
88 indent i = concat $ take i (repeat " ")
90 showA i (ConCase n t args sc)
91 = show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
92 ++ show' (i+1) sc
93 showA i (FnCase n args sc)
94 = "FN " ++ show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
95 ++ show' (i+1) sc
96 showA i (ConstCase t sc)
97 = show t ++ " => " ++ show' (i+1) sc
98 showA i (SucCase n sc)
99 = show n ++ "+1 => " ++ show' (i+1) sc
100 showA i (DefaultCase sc)
101 = "_ => " ++ show' (i+1) sc
104type CaseTree = SC
105type Clause = ([Pat], (Term, Term))
106type CS = ([Term], Int, [(Name, Type)])
108instance TermSize SC where
109 termsize n (Case _ n' as) = termsize n as
110 termsize n (ProjCase n' as) = termsize n as
111 termsize n (STerm t) = termsize n t
112 termsize n _ = 1
114instance TermSize CaseAlt where
115 termsize n (ConCase _ _ _ s) = termsize n s
116 termsize n (FnCase _ _ s) = termsize n s
117 termsize n (ConstCase _ s) = termsize n s
118 termsize n (SucCase _ s) = termsize n s
119 termsize n (DefaultCase s) = termsize n s
121-- simple terms can be inlined trivially - good for primitives in particular
122-- To avoid duplicating work, don't inline something which uses one
123-- of its arguments in more than one place
125small :: Name -> [Name] -> SC -> Bool
126small n args t = let as = findAllUsedArgs t args in
127 length as == length (nub as) &&
128 termsize n t < 10
130namesUsed :: SC -> [Name]
131namesUsed sc = nub $ nu' [] sc where
132 nu' ps (Case _ n alts) = nub (concatMap (nua ps) alts) \\ [n]
133 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts
134 nu' ps (STerm t) = nub $ nut ps t
135 nu' ps _ = []
137 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args
138 nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc) \\ args
139 nua ps (ConstCase _ sc) = nu' ps sc
140 nua ps (SucCase _ sc) = nu' ps sc
141 nua ps (DefaultCase sc) = nu' ps sc
143 nut ps (P _ n _) | n `elem` ps = []
144 | otherwise = [n]
145 nut ps (App _ f a) = nut ps f ++ nut ps a
146 nut ps (Proj t _) = nut ps t
147 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc
148 nut ps (Bind n b sc) = nut (n:ps) sc
149 nut ps _ = []
151-- | Return all called functions, and which arguments are used
152-- in each argument position for the call, in order to help reduce
153-- compilation time, and trace all unused arguments
154findCalls :: SC -> [Name] -> [(Name, [[Name]])]
155findCalls = findCalls' False
157findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]
158findCalls' ignoreasserts sc topargs = nub $ nu' topargs sc where
159 nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)
160 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts
161 nu' ps (STerm t) = nub $ nut ps t
162 nu' ps _ = []
164 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc)
165 nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc)
166 nua ps (ConstCase _ sc) = nu' ps sc
167 nua ps (SucCase _ sc) = nu' ps sc
168 nua ps (DefaultCase sc) = nu' ps sc
170 nut ps (P _ n _) | n `elem` ps = []
171 | otherwise = [(n, [])] -- tmp
172 nut ps fn@(App _ f a)
173 | (P _ n _, args) <- unApply fn
174 = if ignoreasserts && n == sUN "assert_total"
175 then []
176 else if n `elem` ps
177 then nut ps f ++ nut ps a
178 else [(n, map argNames args)] ++ concatMap (nut ps) args
179 | (P (TCon _ _) n _, _) <- unApply fn = []
180 | otherwise = nut ps f ++ nut ps a
181 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc
182 nut ps (Proj t _) = nut ps t
183 nut ps (Bind n b sc) = nut (n:ps) sc
184 nut ps _ = []
186 argNames tm = let ns = directUse tm in
187 filter (\x -> x `elem` ns) topargs
189-- Find names which are used directly (i.e. not in a function call) in a term
191directUse :: TT Name -> [Name]
192directUse (P _ n _) = [n]
193directUse (Bind n (Let t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])
194 ++ directUse t
195directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])
196directUse fn@(App _ f a)
197 | (P Ref (UN pfk) _, [App _ e w]) <- unApply fn,
198 pfk == txt "prim_fork"
199 = directUse e ++ directUse w -- HACK so that fork works
200 | (P Ref (UN fce) _, [_, _, a]) <- unApply fn,
201 fce == txt "Force"
202 = directUse a -- forcing a value counts as a use
203 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them
204 | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime
205 | otherwise = nub $ directUse f ++ directUse a
206directUse (Proj x i) = nub $ directUse x
207directUse _ = []
209-- Find all directly used arguments (i.e. used but not in function calls)
211findUsedArgs :: SC -> [Name] -> [Name]
212findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)
214findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where
215 nu' (Case _ n alts) = n : concatMap nua alts
216 nu' (ProjCase t alts) = directUse t ++ concatMap nua alts
217 nu' (STerm t) = directUse t
218 nu' _ = []
220 nua (ConCase n i args sc) = nu' sc
221 nua (FnCase n args sc) = nu' sc
222 nua (ConstCase _ sc) = nu' sc
223 nua (SucCase _ sc) = nu' sc
224 nua (DefaultCase sc) = nu' sc
226-- Return whether name is used anywhere in a case tree
227isUsed :: SC -> Name -> Bool
228isUsed sc n = used sc where
230 used (Case _ n' alts) = n == n' || any usedA alts
231 used (ProjCase t alts) = n `elem` freeNames t || any usedA alts
232 used (STerm t) = n `elem` freeNames t
233 used _ = False
235 usedA (ConCase _ _ args sc) = used sc
236 usedA (FnCase _ args sc) = used sc
237 usedA (ConstCase _ sc) = used sc
238 usedA (SucCase _ sc) = used sc
239 usedA (DefaultCase sc) = used sc
241type ErasureInfo = Name -> [Int] -- name to list of inaccessible arguments; empty list if name not found
242type CaseBuilder a = ReaderT ErasureInfo (State CS) a
244runCaseBuilder :: ErasureInfo -> CaseBuilder a -> (CS -> (a, CS))
245runCaseBuilder ei bld = runState $ runReaderT bld ei
247data Phase = CompileTime | RunTime
248 deriving (Show, Eq)
250-- Generate a simple case tree
251-- Work Right to Left
253simpleCase :: Bool -> SC -> Bool ->
254 Phase -> FC -> [Int] ->
255 [(Type, Bool)] -> -- (Argument type, whether it's canonical)
256 [([Name], Term, Term)] ->
257 ErasureInfo ->
258 TC CaseDef
259simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
260 = sc' tc defcase phase fc (filter (\(_, _, r) ->
261 case r of
262 Impossible -> False
263 _ -> True) cs)
264 where
265 sc' tc defcase phase fc []
266 = return $ CaseDef [] (UnmatchedCase (show fc ++ ":No pattern clauses")) []
267 sc' tc defcase phase fc cs
268 = let proj = phase == RunTime
269 vnames = fstT (head cs)
270 pats = map (\ (avs, l, r) ->
271 (avs, toPats reflect tc l, (l, r))) cs
272 chkPats = mapM chkAccessible pats in
273 case chkPats of
274 OK pats ->
275 let numargs = length (fst (head pats))
276 ns = take numargs args
277 (ns', ps') = order phase [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats (map snd argtys)
278 (tree, st) = runCaseBuilder erInfo
279 (match ns' ps' defcase)
280 ([], numargs, [])
281 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
282 if proj then return (stripLambdas t)
283 else return t
284 Error err -> Error (At fc err)
285 where args = map (\i -> sMN i "e") [0..]
286 defaultCase True = STerm Erased
287 defaultCase False = UnmatchedCase "Error"
288 fstT (x, _, _) = x
289 lstT (_, _, x) = x
291 -- Check that all pattern variables are reachable by a case split
292 -- Otherwise, they won't make sense on the RHS.
293 chkAccessible (avs, l, c)
294 | phase == RunTime || reflect = return (l, c)
295 | otherwise = do mapM_ (acc l) avs
296 return (l, c)
298 acc [] n = Error (Inaccessible n)
299 acc (PV x t : xs) n | x == n = OK ()
300 acc (PCon _ _ _ ps : xs) n = acc (ps ++ xs) n
301 acc (PSuc p : xs) n = acc (p : xs) n
302 acc (_ : xs) n = acc xs n
304-- For each 'Case', make sure every choice is in the same type family,
305-- as directed by the variable type (i.e. there is no implicit type casing
306-- going on).
308checkSameTypes :: [(Name, Type)] -> SC -> Bool
309checkSameTypes tys (Case _ n alts)
310 = case lookup n tys of
311 Just t -> and (map (checkAlts t) alts)
312 _ -> and (map ((checkSameTypes tys).getSC) alts)
313 where
314 checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc
315 checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc
316 checkAlts _ (ConstCase c sc) = False
317 checkAlts _ _ = True
319 getSC (ConCase _ _ _ sc) = sc
320 getSC (FnCase _ _ sc) = sc
321 getSC (ConstCase _ sc) = sc
322 getSC (SucCase _ sc) = sc
323 getSC (DefaultCase sc) = sc
324checkSameTypes _ _ = True
326-- FIXME: All we're actually doing here is checking that we haven't arrived
327-- at a specific constructor for a polymorphic argument. I *think* this
328-- is sufficient, but if it turns out not to be, fix it!
329--
330-- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718
331isType n t | (P (TCon _ _) _ _, _) <- unApply t = True
332isType n t | (P Ref _ _, _) <- unApply t = True
333isType n t = False
335isConstType (I _) (AType (ATInt ITNative)) = True
336isConstType (BI _) (AType (ATInt ITBig)) = True
337isConstType (Fl _) (AType ATFloat) = True
338isConstType (Ch _) (AType (ATInt ITChar)) = True
339isConstType (Str _) StrType = True
340isConstType (B8 _) (AType (ATInt _)) = True
341isConstType (B16 _) (AType (ATInt _)) = True
342isConstType (B32 _) (AType (ATInt _)) = True
343isConstType (B64 _) (AType (ATInt _)) = True
344isConstType _ _ = False
346data Pat = PCon Bool Name Int [Pat]
347 | PConst Const
348 | PV Name Type
349 | PSuc Pat -- special case for n+1 on Integer
350 | PReflected Name [Pat]
351 | PAny
352 | PTyPat -- typecase, not allowed, inspect last
353 deriving Show
355-- If there are repeated variables, take the *last* one (could be name shadowing
356-- in a where clause, so take the most recent).
358toPats :: Bool -> Bool -> Term -> [Pat]
359toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
360 getArgs (App _ f a) = a : getArgs f
361 getArgs _ = []
363toPat :: Bool -> Bool -> [Term] -> [Pat]
364toPat reflect tc = map $ toPat' []
365 where
366 toPat' [_,_,arg] (P (DCon t a uniq) nm@(UN n) _)
367 | n == txt "Delay"
368 = PCon uniq nm t [PAny, PAny, toPat' [] arg]
370 toPat' args (P (DCon t a uniq) nm@(NS (UN n) [own]) _)
371 | n == txt "Read" && own == txt "Ownership"
372 = PCon False nm t (map shareCons (map (toPat' []) args))
373 where shareCons (PCon _ n i ps) = PCon False n i (map shareCons ps)
374 shareCons p = p
376 toPat' args (P (DCon t a uniq) n _)
377 = PCon uniq n t $ map (toPat' []) args
379 -- n + 1
380 toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)
381 | pabi == txt "prim__addBigInt"
382 = PSuc $ toPat' [] p
384 toPat' [] (P Bound n ty) = PV n ty
385 toPat' args (App _ f a) = toPat' (a : args) f
386 toPat' [] (Constant x) | isTypeConst x = PTyPat
387 | otherwise = PConst x
389 toPat' [] (Bind n (Pi _ t _) sc)
390 | reflect && noOccurrence n sc
391 = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]
393 toPat' args (P _ n _)
394 | reflect
395 = PReflected n $ map (toPat' []) args
397 toPat' _ t = PAny
399 fixedN IT8 = "Bits8"
400 fixedN IT16 = "Bits16"
401 fixedN IT32 = "Bits32"
402 fixedN IT64 = "Bits64"
405data Partition = Cons [Clause]
406 | Vars [Clause]
407 deriving Show
409isVarPat (PV _ _ : ps , _) = True
410isVarPat (PAny : ps , _) = True
411isVarPat (PTyPat : ps , _) = True
412isVarPat _ = False
414isConPat (PCon _ _ _ _ : ps, _) = True
415isConPat (PReflected _ _ : ps, _) = True
416isConPat (PSuc _ : ps, _) = True
417isConPat (PConst _ : ps, _) = True
418isConPat _ = False
420partition :: [Clause] -> [Partition]
421partition [] = []
422partition ms@(m : _)
423 | isVarPat m = let (vars, rest) = span isVarPat ms in
424 Vars vars : partition rest
425 | isConPat m = let (cons, rest) = span isConPat ms in
426 Cons cons : partition rest
427partition xs = error $ "Partition " ++ show xs
429-- reorder the patterns so that the one with most distinct names
430-- comes next. Take rightmost first, otherwise (i.e. pick value rather
431-- than dependency)
432--
433-- The first argument means [(Name, IsInaccessible)].
435order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
436-- do nothing at compile time: FIXME (EB): Put this in after checking
437-- implications for Franck's reflection work... see issue 3233
438-- order CompileTime ns cs _ = (map fst ns, cs)
439order _ [] cs cans = ([], cs)
440order _ ns' [] cans = (map fst ns', [])
441order phase ns' cs cans
442 = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))
443 -- only sort the arguments where there is no clash in
444 -- constructor tags between families, the argument type is canonical,
445 -- and no constructor/constant
446 -- clash, because otherwise we can't reliable make the
447 -- case distinction on evaluation
448 (patnames_ord, patnames_rest)
449 = Data.List.partition (noClash . map snd) patnames
450 patnames_ord' = case phase of
451 CompileTime -> patnames_ord
452 -- reversing tends to make better case trees
453 -- and helps erasure
454 RunTime -> reverse patnames_ord
455 pats' = transpose (sortBy moreDistinct patnames_ord'
456 ++ patnames_rest) in
457 (getNOrder pats', zipWith rebuild pats' cs)
458 where
459 getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)
460 getNOrder (c : _) = map (fst . fst) c
462 rebuild patnames clause = (map (snd . snd) patnames, snd clause)
464 noClash [] = True
465 noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))
466 && noClash ps
468 clashPat (PCon _ _ _ _) (PConst _) = True
469 clashPat (PConst _) (PCon _ _ _ _) = True
470 clashPat (PCon _ _ _ _) (PSuc _) = True
471 clashPat (PSuc _) (PCon _ _ _ _) = True
472 clashPat (PCon _ n i _) (PCon _ n' i' _) | i == i' = n /= n'
473 clashPat _ _ = False
475 -- this compares (+isInaccessible, -numberOfCases)
476 moreDistinct xs ys
477 = compare (snd . fst . head $ xs, numNames [] (map snd ys))
478 (snd . fst . head $ ys, numNames [] (map snd xs))
480 numNames xs ((_, PCon _ n _ _) : ps)
481 | not (Left n `elem` xs) = numNames (Left n : xs) ps
482 numNames xs ((_, PConst c) : ps)
483 | not (Right c `elem` xs) = numNames (Right c : xs) ps
484 numNames xs (_ : ps) = numNames xs ps
485 numNames xs [] = length xs
487match :: [Name] -> [Clause] -> SC -- error case
488 -> CaseBuilder SC
489match [] (([], ret) : xs) err
490 = do (ts, v, ntys) <- get
491 put (ts ++ (map (fst.snd) xs), v, ntys)
492 case snd ret of
493 Impossible -> return ImpossibleCase
494 tm -> return $ STerm tm -- run out of arguments
495match vs cs err = do let ps = partition cs
496 mixture vs ps err
498mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC
499mixture vs [] err = return err
500mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
501 conRule vs ms fallthrough
502mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
503 varRule vs ms fallthrough
505-- Return the list of inaccessible arguments of a data constructor.
506inaccessibleArgs :: Name -> CaseBuilder [Int]
507inaccessibleArgs n = do
508 getInaccessiblePositions <- ask -- this function is the only thing in the environment
509 return $ getInaccessiblePositions n
511data ConType = CName Name Int -- named constructor
512 | CFn Name -- reflected function name
513 | CSuc -- n+1
514 | CConst Const -- constant, not implemented yet
515 deriving (Show, Eq)
517data Group = ConGroup Bool -- Uniqueness flag
518 ConType -- Constructor
519 [([Pat], Clause)] -- arguments and rest of alternative
520 deriving Show
522conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
523conRule (v:vs) cs err = do groups <- groupCons cs
524 caseGroups (v:vs) groups err
526caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC
527caseGroups (v:vs) gs err = do g <- altGroups gs
528 return $ Case (getShared gs) v (sort g)
529 where
530 getShared (ConGroup True _ _ : _) = Updatable
531 getShared _ = Shared
533 altGroups [] = return [DefaultCase err]
535 altGroups (ConGroup _ (CName n i) args : cs)
536 = (:) <$> altGroup n i args <*> altGroups cs
538 altGroups (ConGroup _ (CFn n) args : cs)
539 = (:) <$> altFnGroup n args <*> altGroups cs
541 altGroups (ConGroup _ CSuc args : cs)
542 = (:) <$> altSucGroup args <*> altGroups cs
544 altGroups (ConGroup _ (CConst c) args : cs)
545 = (:) <$> altConstGroup c args <*> altGroups cs
547 altGroup n i args
548 = do inacc <- inaccessibleArgs n
549 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
550 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
551 return $ ConCase n i newVars matchCs
553 altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args
554 matchCs <- match (newVars ++ vs) nextCs err
555 return $ FnCase n newVars matchCs
557 altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args
558 matchCs <- match (newVar:vs) nextCs err
559 return $ SucCase newVar matchCs
561 altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args
562 matchCs <- match vs nextCs err
563 return $ ConstCase n matchCs
565-- Returns:
566-- * names of all variables arising from match
567-- * names of accessible variables (subset of all variables)
568-- * names of inaccessible variables (subset of all variables)
569-- * clauses corresponding to (accVars ++ origVars ++ inaccVars)
570argsToAlt :: [Int] -> [([Pat], Clause)] -> CaseBuilder ([Name], [Name], [Name], [Clause])
571argsToAlt _ [] = return ([], [], [], [])
572argsToAlt inacc rs@((r, m) : rest) = do
573 newVars <- getNewVars r
574 let (accVars, inaccVars) = partitionAcc newVars
575 return (newVars, accVars, inaccVars, addRs rs)
576 where
577 -- Create names for new variables arising from the given patterns.
578 getNewVars :: [Pat] -> CaseBuilder [Name]
579 getNewVars [] = return []
580 getNewVars ((PV n t) : ns) = do v <- getVar "e"
581 nsv <- getNewVars ns
583 -- Record the type of the variable.
584 --
585 -- It seems that the ordering is not important
586 -- and we can put (v,t) always in front of "ntys"
587 -- (the varName-type pairs seem to represent a mapping).
588 --
589 -- The code that reads this is currently
590 -- commented out, anyway.
591 (cs, i, ntys) <- get
592 put (cs, i, (v, t) : ntys)
594 return (v : nsv)
596 getNewVars (PAny : ns) = (:) <$> getVar "i" <*> getNewVars ns
597 getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns
598 getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns
600 -- Partition a list of things into (accessible, inaccessible) things,
601 -- according to the list of inaccessible indices.
602 partitionAcc xs =
603 ( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]
604 , [x | (i,x) <- zip [0..] xs, i `elem` inacc]
605 )
607 addRs [] = []
608 addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)
609 where
610 (acc, inacc) = partitionAcc r
612 uniq i (UN n) = MN i n
613 uniq i n = n
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
769stripLambdas :: CaseDef -> CaseDef
770stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)
771 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
772stripLambdas x = x
774substSC :: Name -> Name -> SC -> SC
775substSC n repl (Case up n' alts)
776 | n == n' = Case up repl (map (substAlt n repl) alts)
777 | otherwise = Case up n' (map (substAlt n repl) alts)
778substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
779substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg
780substSC n repl ImpossibleCase = ImpossibleCase
781substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
783substAlt :: Name -> Name -> CaseAlt -> CaseAlt
784substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
785substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
786substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
787substAlt n repl (SucCase n' sc)
788 | n == n' = SucCase n (substSC n repl sc)
789 | otherwise = SucCase n' (substSC n repl sc)
790substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
792-- mkForce n' n t updates the tree t under the assumption that
793-- n' = force n (so basically updating n to n')
794mkForce :: Name -> Name -> SC -> SC
795mkForce = mkForceSC
796 where
797 mkForceSC n arg (Case up x alts) | x == arg
798 = Case up n $ map (mkForceAlt n arg) alts
800 mkForceSC n arg (Case up x alts)
801 = Case up x (map (mkForceAlt n arg) alts)
803 mkForceSC n arg (ProjCase t alts)
804 = ProjCase t $ map (mkForceAlt n arg) alts
806 mkForceSC n arg c = c
808 mkForceAlt n arg (ConCase cn t args rhs)
809 = ConCase cn t args (mkForceSC n arg rhs)
810 mkForceAlt n arg (FnCase cn args rhs)
811 = FnCase cn args (mkForceSC n arg rhs)
812 mkForceAlt n arg (ConstCase t rhs)
813 = ConstCase t (mkForceSC n arg rhs)
814 mkForceAlt n arg (SucCase sn rhs)
815 = SucCase sn (mkForceSC n arg rhs)
816 mkForceAlt n arg (DefaultCase rhs)
817 = DefaultCase (mkForceSC n arg rhs)
819 forceTm n arg t = subst n arg t