git.iko.soy/Idris-dev
on ea65347 help sign in
Idris-dev/src/Idris/Core/CaseTree.hs
875 lines 34 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 qualified Data.Set as S
40import Debug.Trace
41import GHC.Generics (Generic)
43data CaseDef = CaseDef [Name] !SC [Term]
44 deriving Show
46data SC' t = Case CaseType Name [CaseAlt' t] -- ^ invariant: lowest tags first
47 | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection
48 | STerm !t
49 | UnmatchedCase String -- ^ error message
50 | ImpossibleCase -- ^ already checked to be impossible
51 deriving (Eq, Ord, Functor, Generic)
52{-!
53deriving instance Binary 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'
69!-}
71type CaseAlt = CaseAlt' Term
73instance Show t => Show (SC' t) where
74 show sc = show' 1 sc
75 where
76 show' i (Case up n alts) = "case" ++ u ++ show n ++ " of\n" ++ indent i ++
77 showSep ("\n" ++ indent i) (map (showA i) alts)
78 where u = case up of
79 Updatable -> "! "
80 Shared -> " "
81 show' i (ProjCase tm alts) = "case " ++ show tm ++ " of " ++
82 showSep ("\n" ++ indent i) (map (showA i) alts)
83 show' i (STerm tm) = show tm
84 show' i (UnmatchedCase str) = "error " ++ show str
85 show' i ImpossibleCase = "impossible"
87 indent i = concat $ take i (repeat " ")
89 showA i (ConCase n t args sc)
90 = show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
91 ++ show' (i+1) sc
92 showA i (FnCase n args sc)
93 = "FN " ++ show n ++ "(" ++ showSep (", ") (map show args) ++ ") => "
94 ++ show' (i+1) sc
95 showA i (ConstCase t sc)
96 = show t ++ " => " ++ show' (i+1) sc
97 showA i (SucCase n sc)
98 = show n ++ "+1 => " ++ show' (i+1) sc
99 showA i (DefaultCase sc)
100 = "_ => " ++ show' (i+1) sc
103type CaseTree = SC
104type Clause = ([Pat], (Term, Term))
105type CS = ([Term], Int, [(Name, Type)])
107instance TermSize SC where
108 termsize n (Case _ n' as) = termsize n as
109 termsize n (ProjCase n' as) = termsize n as
110 termsize n (STerm t) = termsize n t
111 termsize n _ = 1
113instance TermSize CaseAlt where
114 termsize n (ConCase _ _ _ s) = termsize n s
115 termsize n (FnCase _ _ s) = termsize n s
116 termsize n (ConstCase _ s) = termsize n s
117 termsize n (SucCase _ s) = termsize n s
118 termsize n (DefaultCase s) = termsize n s
120-- simple terms can be inlined trivially - good for primitives in particular
121-- To avoid duplicating work, don't inline something which uses one
122-- of its arguments in more than one place
124small :: Name -> [Name] -> SC -> Bool
125small n args t = let as = findAllUsedArgs t args in
126 length as == length (nub as) &&
127 termsize n t < 10
129namesUsed :: SC -> [Name]
130namesUsed sc = nub $ nu' [] sc where
131 nu' ps (Case _ n alts) = nub (concatMap (nua ps) alts) \\ [n]
132 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts
133 nu' ps (STerm t) = nub $ nut ps t
134 nu' ps _ = []
136 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args
137 nua ps (FnCase n args sc) = nub (nu' (ps ++ args) sc) \\ args
138 nua ps (ConstCase _ sc) = nu' ps sc
139 nua ps (SucCase _ sc) = nu' ps sc
140 nua ps (DefaultCase sc) = nu' ps sc
142 nut ps (P _ n _) | n `elem` ps = []
143 | otherwise = [n]
144 nut ps (App _ f a) = nut ps f ++ nut ps a
145 nut ps (Proj t _) = nut ps t
146 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc
147 nut ps (Bind n b sc) = nut (n:ps) sc
148 nut ps _ = []
150-- | Return all called functions, and which arguments are used
151-- in each argument position for the call, in order to help reduce
152-- compilation time, and trace all unused arguments
153findCalls :: SC -> [Name] -> [(Name, [[Name]])]
154findCalls = findCalls' False
156findCalls' :: Bool -> SC -> [Name] -> [(Name, [[Name]])]
157findCalls' ignoreasserts sc topargs = S.toList $ nu' topargs sc where
158 nu' ps (Case _ n alts) = S.unions $ map (nua (n : ps)) alts
159 nu' ps (ProjCase t alts) = S.unions $ nut ps t : map (nua ps) alts
160 nu' ps (STerm t) = nut ps t
161 nu' ps _ = S.empty
163 nua ps (ConCase n i args sc) = nu' (ps ++ args) sc
164 nua ps (FnCase n args sc) = nu' (ps ++ args) sc
165 nua ps (ConstCase _ sc) = nu' ps sc
166 nua ps (SucCase _ sc) = nu' ps sc
167 nua ps (DefaultCase sc) = nu' ps sc
169 nut ps (P _ n _) | n `elem` ps = S.empty
170 | otherwise = S.singleton (n, [])
171 nut ps fn@(App _ f a)
172 | (P _ n _, args) <- unApply fn
173 = if ignoreasserts && n == sUN "assert_total"
174 then S.empty
175 else if n `elem` ps
176 then S.union (nut ps f) (nut ps a)
177 else S.insert (n, map argNames args)
178 (S.unions $ map (nut ps) args)
179 | (P (TCon _ _) n _, _) <- unApply fn = S.empty
180 | otherwise = S.union (nut ps f) (nut ps a)
181 nut ps (Bind n (Let t v) sc) = S.union (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 _ = S.empty
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 = CoverageCheck [Int] -- list of positions explicitly given
248 | CompileTime
249 | RunTime
250 deriving (Show, Eq)
252-- Generate a simple case tree
253-- Work Right to Left
255simpleCase :: Bool -> SC -> Bool ->
256 Phase -> FC ->
257 -- Following two can be empty lists when Phase = CoverageCheck
258 [Int] -> -- Inaccessible argument positions
259 [(Type, Bool)] -> -- (Argument type, whether it's canonical)
260 [([Name], Term, Term)] ->
261 ErasureInfo ->
262 TC CaseDef
263simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
264 = sc' tc defcase phase fc (filter (\(_, _, r) ->
265 case r of
266 Impossible -> False
267 _ -> True) cs)
268 where
269 sc' tc defcase phase fc []
270 = return $ CaseDef [] (UnmatchedCase (show fc ++ ":No pattern clauses")) []
271 sc' tc defcase phase fc cs
272 = let proj = phase == RunTime
273 vnames = fstT (head cs)
274 pats = map (\ (avs, l, r) ->
275 (avs, toPats reflect tc l, (l, r))) cs
276 chkPats = mapM chkAccessible pats in
277 case chkPats of
278 OK pats ->
279 let numargs = length (fst (head pats))
280 ns = take numargs args
281 (ns', ps') = order phase [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats (map snd argtys)
282 (tree, st) = runCaseBuilder erInfo
283 (match ns' ps' defcase)
284 ([], numargs, [])
285 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in
286 if proj then return (stripLambdas t)
287 else return t
288 Error err -> Error (At fc err)
289 where args = map (\i -> sMN i "e") [0..]
290 defaultCase True = STerm Erased
291 defaultCase False = UnmatchedCase "Error"
292 fstT (x, _, _) = x
293 lstT (_, _, x) = x
295 -- Check that all pattern variables are reachable by a case split
296 -- Otherwise, they won't make sense on the RHS.
297 chkAccessible (avs, l, c)
298 | phase /= CompileTime || reflect = return (l, c)
299 | otherwise = do mapM_ (acc l) avs
300 return (l, c)
302 acc [] n = Error (Inaccessible n)
303 acc (PV x t : xs) n | x == n = OK ()
304 acc (PCon _ _ _ ps : xs) n = acc (ps ++ xs) n
305 acc (PSuc p : xs) n = acc (p : xs) n
306 acc (_ : xs) n = acc xs n
308-- For each 'Case', make sure every choice is in the same type family,
309-- as directed by the variable type (i.e. there is no implicit type casing
310-- going on).
312checkSameTypes :: [(Name, Type)] -> SC -> Bool
313checkSameTypes tys (Case _ n alts)
314 = case lookup n tys of
315 Just t -> and (map (checkAlts t) alts)
316 _ -> and (map ((checkSameTypes tys).getSC) alts)
317 where
318 checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc
319 checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc
320 checkAlts _ (ConstCase c sc) = False
321 checkAlts _ _ = True
323 getSC (ConCase _ _ _ sc) = sc
324 getSC (FnCase _ _ sc) = sc
325 getSC (ConstCase _ sc) = sc
326 getSC (SucCase _ sc) = sc
327 getSC (DefaultCase sc) = sc
328checkSameTypes _ _ = True
330-- FIXME: All we're actually doing here is checking that we haven't arrived
331-- at a specific constructor for a polymorphic argument. I *think* this
332-- is sufficient, but if it turns out not to be, fix it!
333--
334-- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718
335isType n t | (P (TCon _ _) _ _, _) <- unApply t = True
336isType n t | (P Ref _ _, _) <- unApply t = True
337isType n t = False
339isConstType (I _) (AType (ATInt ITNative)) = True
340isConstType (BI _) (AType (ATInt ITBig)) = True
341isConstType (Fl _) (AType ATFloat) = True
342isConstType (Ch _) (AType (ATInt ITChar)) = True
343isConstType (Str _) StrType = True
344isConstType (B8 _) (AType (ATInt _)) = True
345isConstType (B16 _) (AType (ATInt _)) = True
346isConstType (B32 _) (AType (ATInt _)) = True
347isConstType (B64 _) (AType (ATInt _)) = True
348isConstType _ _ = False
350data Pat = PCon Bool Name Int [Pat]
351 | PConst Const
352 | PInferred Pat
353 | PV Name Type
354 | PSuc Pat -- special case for n+1 on Integer
355 | PReflected Name [Pat]
356 | PAny
357 | PTyPat -- typecase, not allowed, inspect last
358 deriving Show
360-- If there are repeated variables, take the *last* one (could be name shadowing
361-- in a where clause, so take the most recent).
363toPats :: Bool -> Bool -> Term -> [Pat]
364toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
365 getArgs (App _ f a) = a : getArgs f
366 getArgs _ = []
368toPat :: Bool -> Bool -> [Term] -> [Pat]
369toPat reflect tc = map $ toPat' []
370 where
371 toPat' [_,_,arg] (P (DCon t a uniq) nm@(UN n) _)
372 | n == txt "Delay"
373 = PCon uniq nm t [PAny, PAny, toPat' [] arg]
375 toPat' args (P (DCon t a uniq) nm@(NS (UN n) [own]) _)
376 | n == txt "Read" && own == txt "Ownership"
377 = PCon False nm t (map shareCons (map (toPat' []) args))
378 where shareCons (PCon _ n i ps) = PCon False n i (map shareCons ps)
379 shareCons p = p
381 toPat' args (P (DCon t a uniq) n _)
382 = PCon uniq n t $ map (toPat' []) args
384 -- n + 1
385 toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)
386 | pabi == txt "prim__addBigInt"
387 = PSuc $ toPat' [] p
389 toPat' [] (P Bound n ty) = PV n ty
390 toPat' args (App _ f a) = toPat' (a : args) f
391 toPat' args (Inferred tm) = PInferred (toPat' args tm)
392 toPat' [] (Constant x) | isTypeConst x = PTyPat
393 | otherwise = PConst x
395 toPat' [] (Bind n (Pi _ _ t _) sc)
396 | reflect && noOccurrence n sc
397 = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]
399 toPat' args (P _ n _)
400 | reflect
401 = PReflected n $ map (toPat' []) args
403 toPat' _ t = PAny
405 fixedN IT8 = "Bits8"
406 fixedN IT16 = "Bits16"
407 fixedN IT32 = "Bits32"
408 fixedN IT64 = "Bits64"
411data Partition = Cons [Clause]
412 | Vars [Clause]
413 deriving Show
415isVarPat (PV _ _ : ps , _) = True
416isVarPat (PAny : ps , _) = True
417isVarPat (PTyPat : ps , _) = True
418isVarPat _ = False
420isConPat (PCon _ _ _ _ : ps, _) = True
421isConPat (PReflected _ _ : ps, _) = True
422isConPat (PSuc _ : ps, _) = True
423isConPat (PConst _ : ps, _) = True
424isConPat _ = False
426partition :: [Clause] -> [Partition]
427partition [] = []
428partition ms@(m : _)
429 | isVarPat m = let (vars, rest) = span isVarPat ms in
430 Vars vars : partition rest
431 | isConPat m = let (cons, rest) = span isConPat ms in
432 Cons cons : partition rest
433partition xs = error $ "Partition " ++ show xs
435-- reorder the patterns so that the one with most distinct names
436-- comes next. Take rightmost first, otherwise (i.e. pick value rather
437-- than dependency)
438--
439-- The first argument means [(Name, IsInaccessible)].
441order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
442-- do nothing at compile time: FIXME (EB): Put this in after checking
443-- implications for Franck's reflection work... see issue 3233
444-- order CompileTime ns cs _ = (map fst ns, cs)
445order _ [] cs cans = ([], cs)
446order _ ns' [] cans = (map fst ns', [])
447order (CoverageCheck pos) ns' cs cans
448 = let ns_out = pick 0 [] (map fst ns')
449 cs_out = map pickClause cs in
450 (ns_out, cs_out)
451 where
452 pickClause (pats, def) = (pick 0 [] pats, def)
454 -- Order the list so that things in a position in 'pos' are in the first
455 -- part, then all the other things later. Otherwise preserve order.
456 pick i skipped [] = reverse skipped
457 pick i skipped (x : xs)
458 | i `elem` pos = x : pick (i + 1) skipped xs
459 | otherwise = pick (i + 1) (x : skipped) xs
461order phase ns' cs cans
462 = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))
463 -- only sort the arguments where there is no clash in
464 -- constructor tags between families, the argument type is canonical,
465 -- and no constructor/constant
466 -- clash, because otherwise we can't reliable make the
467 -- case distinction on evaluation
468 (patnames_ord, patnames_rest)
469 = Data.List.partition (noClash . map snd) patnames
470 patnames_ord' = case phase of
471 CompileTime -> patnames_ord
472 -- reversing tends to make better case trees
473 -- and helps erasure
474 RunTime -> reverse patnames_ord
475 pats' = transpose (sortBy moreDistinct patnames_ord'
476 ++ patnames_rest) in
477 (getNOrder pats', zipWith rebuild pats' cs)
478 where
479 getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)
480 getNOrder (c : _) = map (fst . fst) c
482 rebuild patnames clause = (map (snd . snd) patnames, snd clause)
484 noClash [] = True
485 noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps))
486 && noClash ps
488 clashPat (PCon _ _ _ _) (PConst _) = True
489 clashPat (PConst _) (PCon _ _ _ _) = True
490 clashPat (PCon _ _ _ _) (PSuc _) = True
491 clashPat (PSuc _) (PCon _ _ _ _) = True
492 clashPat (PCon _ n i _) (PCon _ n' i' _) | i == i' = n /= n'
493 clashPat _ _ = False
495 -- this compares (+isInaccessible, -numberOfCases)
496 moreDistinct xs ys
497 = compare (snd . fst . head $ xs, numNames [] (map snd ys))
498 (snd . fst . head $ ys, numNames [] (map snd xs))
500 numNames xs ((_, PCon _ n _ _) : ps)
501 | not (Left n `elem` xs) = numNames (Left n : xs) ps
502 numNames xs ((_, PConst c) : ps)
503 | not (Right c `elem` xs) = numNames (Right c : xs) ps
504 numNames xs (_ : ps) = numNames xs ps
505 numNames xs [] = length xs
507-- Reorder the patterns in the clause so that the PInferred patterns come
508-- last. Also strip 'PInferred' from the top level patterns so that we can
509-- go ahead and match.
510orderByInf :: [Name] -> [Clause] -> ([Name], [Clause])
511orderByInf vs cs = let alwaysInf = getInf cs in
512 (selectInf alwaysInf vs,
513 map deInf (map (selectExp alwaysInf) cs))
514 where
515 getInf [] = []
516 getInf [(pats, def)] = infPos 0 pats
517 getInf ((pats, def) : cs) = infPos 0 pats `intersect` getInf cs
519 selectExp :: [Int] -> Clause -> Clause
520 selectExp infs (pats, def)
521 = let (notInf, inf) = splitPats 0 infs [] [] pats in
522 (notInf ++ inf, def)
524 selectInf :: [Int] -> [a] -> [a]
525 selectInf infs ns = let (notInf, inf) = splitPats 0 infs [] [] ns in
526 notInf ++ inf
528 splitPats i infpos notInf inf [] = (reverse notInf, reverse inf)
529 splitPats i infpos notInf inf (p : ps)
530 | i `elem` infpos = splitPats (i + 1) infpos notInf (p : inf) ps
531 | otherwise = splitPats (i + 1) infpos (p : notInf) inf ps
533 infPos i [] = []
534 infPos i (PInferred p : ps) = i : infPos (i + 1) ps
535 infPos i (_ : ps) = infPos (i + 1) ps
537 deInf (pats, def) = (map deInfPat pats, def)
539 deInfPat (PInferred p) = p
540 deInfPat p = p
542match :: [Name] -> [Clause] -> SC -- error case
543 -> CaseBuilder SC
544match [] (([], ret) : xs) err
545 = do (ts, v, ntys) <- get
546 put (ts ++ (map (fst.snd) xs), v, ntys)
547 case snd ret of
548 Impossible -> return ImpossibleCase
549 tm -> return $ STerm tm -- run out of arguments
550match vs cs err = do let (vs', de_inf) = orderByInf vs cs
551 ps = partition de_inf
552 mixture vs' ps err
554mixture :: [Name] -> [Partition] -> SC -> CaseBuilder SC
555mixture vs [] err = return err
556mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
557 conRule vs ms fallthrough
558mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
559 varRule vs ms fallthrough
561-- Return the list of inaccessible arguments of a data constructor.
562inaccessibleArgs :: Name -> CaseBuilder [Int]
563inaccessibleArgs n = do
564 getInaccessiblePositions <- ask -- this function is the only thing in the environment
565 return $ getInaccessiblePositions n
567data ConType = CName Name Int -- named constructor
568 | CFn Name -- reflected function name
569 | CSuc -- n+1
570 | CConst Const -- constant, not implemented yet
571 deriving (Show, Eq)
573data Group = ConGroup Bool -- Uniqueness flag
574 ConType -- Constructor
575 [([Pat], Clause)] -- arguments and rest of alternative
576 deriving Show
578conRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
579conRule (v:vs) cs err = do groups <- groupCons cs
580 caseGroups (v:vs) groups err
582caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC
583caseGroups (v:vs) gs err = do g <- altGroups gs
584 return $ Case (getShared gs) v (sort g)
585 where
586 getShared (ConGroup True _ _ : _) = Updatable
587 getShared _ = Shared
589 altGroups [] = return [DefaultCase err]
591 altGroups (ConGroup _ (CName n i) args : cs)
592 = (:) <$> altGroup n i args <*> altGroups cs
594 altGroups (ConGroup _ (CFn n) args : cs)
595 = (:) <$> altFnGroup n args <*> altGroups cs
597 altGroups (ConGroup _ CSuc args : cs)
598 = (:) <$> altSucGroup args <*> altGroups cs
600 altGroups (ConGroup _ (CConst c) args : cs)
601 = (:) <$> altConstGroup c args <*> altGroups cs
603 altGroup n i args
604 = do inacc <- inaccessibleArgs n
605 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args
606 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err
607 return $ ConCase n i newVars matchCs
609 altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args
610 matchCs <- match (newVars ++ vs) nextCs err
611 return $ FnCase n newVars matchCs
613 altSucGroup args = do ([newVar], _, [], nextCs) <- argsToAlt [] args
614 matchCs <- match (newVar:vs) nextCs err
615 return $ SucCase newVar matchCs
617 altConstGroup n args = do (_, _, [], nextCs) <- argsToAlt [] args
618 matchCs <- match vs nextCs err
619 return $ ConstCase n matchCs
621-- Returns:
622-- * names of all variables arising from match
623-- * names of accessible variables (subset of all variables)
624-- * names of inaccessible variables (subset of all variables)
625-- * clauses corresponding to (accVars ++ origVars ++ inaccVars)
626argsToAlt :: [Int] -> [([Pat], Clause)] -> CaseBuilder ([Name], [Name], [Name], [Clause])
627argsToAlt _ [] = return ([], [], [], [])
628argsToAlt inacc rs@((r, m) : rest) = do
629 newVars <- getNewVars r
630 let (accVars, inaccVars) = partitionAcc newVars
631 return (newVars, accVars, inaccVars, addRs rs)
632 where
633 -- Create names for new variables arising from the given patterns.
634 getNewVars :: [Pat] -> CaseBuilder [Name]
635 getNewVars [] = return []
636 getNewVars ((PV n t) : ns) = do v <- getVar "e"
637 nsv <- getNewVars ns
639 -- Record the type of the variable.
640 --
641 -- It seems that the ordering is not important
642 -- and we can put (v,t) always in front of "ntys"
643 -- (the varName-type pairs seem to represent a mapping).
644 --
645 -- The code that reads this is currently
646 -- commented out, anyway.
647 (cs, i, ntys) <- get
648 put (cs, i, (v, t) : ntys)
650 return (v : nsv)
652 getNewVars (PAny : ns) = (:) <$> getVar "i" <*> getNewVars ns
653 getNewVars (PTyPat : ns) = (:) <$> getVar "t" <*> getNewVars ns
654 getNewVars (_ : ns) = (:) <$> getVar "e" <*> getNewVars ns
656 -- Partition a list of things into (accessible, inaccessible) things,
657 -- according to the list of inaccessible indices.
658 partitionAcc xs =
659 ( [x | (i,x) <- zip [0..] xs, i `notElem` inacc]
660 , [x | (i,x) <- zip [0..] xs, i `elem` inacc]
661 )
663 addRs [] = []
664 addRs ((r, (ps, res)) : rs) = ((acc++ps++inacc, res) : addRs rs)
665 where
666 (acc, inacc) = partitionAcc r
668 uniq i (UN n) = MN i n
669 uniq i n = n
671getVar :: String -> CaseBuilder Name
672getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)
674groupCons :: [Clause] -> CaseBuilder [Group]
675groupCons cs = gc [] cs
676 where
677 gc acc [] = return acc
678 gc acc ((p : ps, res) : cs) =
679 do acc' <- addGroup p ps res acc
680 gc acc' cs
681 addGroup p ps res acc = case p of
682 PCon uniq con i args -> return $ addg uniq (CName con i) args (ps, res) acc
683 PConst cval -> return $ addConG cval (ps, res) acc
684 PSuc n -> return $ addg False CSuc [n] (ps, res) acc
685 PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc
686 pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"
688 addg uniq c conargs res []
689 = [ConGroup uniq c [(conargs, res)]]
690 addg uniq c conargs res (g@(ConGroup _ c' cs):gs)
691 | c == c' = ConGroup uniq c (cs ++ [(conargs, res)]) : gs
692 | otherwise = g : addg uniq c conargs res gs
694 addConG con res [] = [ConGroup False (CConst con) [([], res)]]
695 addConG con res (g@(ConGroup False (CConst n) cs) : gs)
696 | con == n = ConGroup False (CConst n) (cs ++ [([], res)]) : gs
697-- | otherwise = g : addConG con res gs
698 addConG con res (g : gs) = g : addConG con res gs
700varRule :: [Name] -> [Clause] -> SC -> CaseBuilder SC
701varRule (v : vs) alts err =
702 do alts' <- mapM (repVar v) alts
703 match vs alts' err
704 where
705 repVar v (PV p ty : ps , (lhs, res))
706 = do (cs, i, ntys) <- get
707 put (cs, i, (v, ty) : ntys)
708 return (ps, (lhs, subst p (P Bound v ty) res))
709 repVar v (PAny : ps , res) = return (ps, res)
710 repVar v (PTyPat : ps , res) = return (ps, res)
712-- fix: case e of S k -> f (S k) ==> case e of S k -> f e
714depatt :: [Name] -> SC -> SC
715depatt ns tm = dp [] tm
716 where
717 dp ms (STerm tm) = STerm (applyMaps ms tm)
718 dp ms (Case up x alts) = Case up x (map (dpa ms x) alts)
719 dp ms sc = sc
721 dpa ms x (ConCase n i args sc)
722 = ConCase n i args (dp ((x, (n, args)) : ms) sc)
723 dpa ms x (FnCase n args sc)
724 = FnCase n args (dp ((x, (n, args)) : ms) sc)
725 dpa ms x (ConstCase c sc) = ConstCase c (dp ms sc)
726 dpa ms x (SucCase n sc) = SucCase n (dp ms sc)
727 dpa ms x (DefaultCase sc) = DefaultCase (dp ms sc)
729 applyMaps ms f@(App _ _ _)
730 | (P nt cn pty, args) <- unApply f
731 = let args' = map (applyMaps ms) args in
732 applyMap ms nt cn pty args'
733 where
734 applyMap [] nt cn pty args' = mkApp (P nt cn pty) args'
735 applyMap ((x, (n, args)) : ms) nt cn pty args'
736 | and ((length args == length args') :
737 (n == cn) : zipWith same args args') = P Ref x Erased
738 | otherwise = applyMap ms nt cn pty args'
739 same n (P _ n' _) = n == n'
740 same _ _ = False
742 applyMaps ms (App s f a) = App s (applyMaps ms f) (applyMaps ms a)
743 applyMaps ms t = t
745-- FIXME: Do this for SucCase too
746-- Issue #1719 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1719
747prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)
748 -> SC -> SC
749prune proj (Case up n alts) = case alts' of
750 [] -> ImpossibleCase
752 -- Projection transformations prevent us from seeing some uses of ctor fields
753 -- because they delete information about which ctor is being used.
754 -- Consider:
755 -- f (X x) = ... x ...
756 -- vs.
757 -- f x = ... x!0 ...
758 --
759 -- Hence, we disable this step.
760 -- TODO: re-enable this in toIR
761 --
762 -- as@[ConCase cn i args sc]
763 -- | proj -> mkProj n 0 args (prune proj sc)
764 -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs
766 -- If none of the args are used in the sc, however, we can just replace it
767 -- with sc
768 as@[ConCase cn i args sc]
769 | proj -> let sc' = prune proj sc in
770 if any (isUsed sc') args
771 then Case up n [ConCase cn i args sc']
772 else sc'
774 [SucCase cn sc]
775 | proj
776 -> projRep cn n (-1) $ prune proj sc
778 [ConstCase _ sc]
779 -> prune proj sc
781 -- Bit of a hack here! The default case will always be 0, make sure
782 -- it gets caught first.
783 [s@(SucCase _ _), DefaultCase dc]
784 -> Case up n [ConstCase (BI 0) dc, s]
786 as -> Case up n as
787 where
788 alts' = filter (not . erased) $ map pruneAlt alts
790 pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune proj sc)
791 pruneAlt (FnCase cn ns sc) = FnCase cn ns (prune proj sc)
792 pruneAlt (ConstCase c sc) = ConstCase c (prune proj sc)
793 pruneAlt (SucCase n sc) = SucCase n (prune proj sc)
794 pruneAlt (DefaultCase sc) = DefaultCase (prune proj sc)
796 erased (DefaultCase (STerm Erased)) = True
797 erased (DefaultCase ImpossibleCase) = True
798 erased _ = False
800 projRep :: Name -> Name -> Int -> SC -> SC
801 projRep arg n i (Case up x alts) | x == arg
802 = ProjCase (Proj (P Bound n Erased) i) $ map (projRepAlt arg n i) alts
803 projRep arg n i (Case up x alts)
804 = Case up x (map (projRepAlt arg n i) alts)
805 projRep arg n i (ProjCase t alts)
806 = ProjCase (projRepTm arg n i t) $ map (projRepAlt arg n i) alts
807 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)
808 projRep arg n i c = c
810 projRepAlt arg n i (ConCase cn t args rhs)
811 = ConCase cn t args (projRep arg n i rhs)
812 projRepAlt arg n i (FnCase cn args rhs)
813 = FnCase cn args (projRep arg n i rhs)
814 projRepAlt arg n i (ConstCase t rhs)
815 = ConstCase t (projRep arg n i rhs)
816 projRepAlt arg n i (SucCase sn rhs)
817 = SucCase sn (projRep arg n i rhs)
818 projRepAlt arg n i (DefaultCase rhs)
819 = DefaultCase (projRep arg n i rhs)
821 projRepTm arg n i t = subst arg (Proj (P Bound n Erased) i) t
823prune _ t = t
825stripLambdas :: CaseDef -> CaseDef
826stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)
827 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
828stripLambdas x = x
830substSC :: Name -> Name -> SC -> SC
831substSC n repl (Case up n' alts)
832 | n == n' = Case up repl (map (substAlt n repl) alts)
833 | otherwise = Case up n' (map (substAlt n repl) alts)
834substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
835substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg
836substSC n repl ImpossibleCase = ImpossibleCase
837substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
839substAlt :: Name -> Name -> CaseAlt -> CaseAlt
840substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
841substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
842substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
843substAlt n repl (SucCase n' sc)
844 | n == n' = SucCase n (substSC n repl sc)
845 | otherwise = SucCase n' (substSC n repl sc)
846substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
848-- mkForce n' n t updates the tree t under the assumption that
849-- n' = force n (so basically updating n to n')
850mkForce :: Name -> Name -> SC -> SC
851mkForce = mkForceSC
852 where
853 mkForceSC n arg (Case up x alts) | x == arg
854 = Case up n $ map (mkForceAlt n arg) alts
856 mkForceSC n arg (Case up x alts)
857 = Case up x (map (mkForceAlt n arg) alts)
859 mkForceSC n arg (ProjCase t alts)
860 = ProjCase t $ map (mkForceAlt n arg) alts
862 mkForceSC n arg c = c
864 mkForceAlt n arg (ConCase cn t args rhs)
865 = ConCase cn t args (mkForceSC n arg rhs)
866 mkForceAlt n arg (FnCase cn args rhs)
867 = FnCase cn args (mkForceSC n arg rhs)
868 mkForceAlt n arg (ConstCase t rhs)
869 = ConstCase t (mkForceSC n arg rhs)
870 mkForceAlt n arg (SucCase sn rhs)
871 = SucCase sn (mkForceSC n arg rhs)
872 mkForceAlt n arg (DefaultCase rhs)
873 = DefaultCase (mkForceSC n arg rhs)
875 forceTm n arg t = subst n arg t