git.iko.soy/Idris-dev
on master help sign in
Make ProjCase take exactly one alternative. (TODO: is this safe?)
59c3cd1Matus Tejiscak
src/IRTS/Compiler.hs+3−3
compare with master
unifiedsplit
@@ -370,9 +370,9 @@ instance ToIR SC where
370
370
371 ir' (STerm t) = ir t
371 ir' (STerm t) = ir t
372 ir' (UnmatchedCase str) = return $ LError str
372 ir' (UnmatchedCase str) = return $ LError str
373− ir' (ProjCase tm alts) = do tm' <- ir tm
373+ ir' (ProjCase tm alt) = do tm' <- ir tm
374− alts' <- mapM (mkIRAlt tm') alts
374+ alt' <- mkIRAlt tm' alt
375− return $ LCase tm' alts'
375+ return $ LCase tm' [alt']
376 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
376 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
377 return $ LCase (LV (Glob n)) alts'
377 return $ LCase (LV (Glob n)) alts'
378 ir' ImpossibleCase = return LNothing
378 ir' ImpossibleCase = return LNothing
src/Idris/Core/CaseTree.hs+12−13
@@ -14,8 +14,8 @@ import Debug.Trace
14data CaseDef = CaseDef [Name] !SC [Term]
14data CaseDef = CaseDef [Name] !SC [Term]
15 deriving Show
15 deriving Show
16
16
17−data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first
17+data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first
18− | ProjCase t [CaseAlt' t] -- ^ special case for projections
18+ | ProjCase t (CaseAlt' t) -- ^ special case for projections
19 | STerm !t
19 | STerm !t
20 | UnmatchedCase String -- ^ error message
20 | UnmatchedCase String -- ^ error message
21 | ImpossibleCase -- ^ already checked to be impossible
21 | ImpossibleCase -- ^ already checked to be impossible
@@ -45,8 +45,8 @@ instance Show t => Show (SC' t) where
45 where
45 where
46 show' i (Case n alts) = "case " ++ show n ++ " of\n" ++ indent i ++
46 show' i (Case n alts) = "case " ++ show n ++ " of\n" ++ indent i ++
47 showSep ("\n" ++ indent i) (map (showA i) alts)
47 showSep ("\n" ++ indent i) (map (showA i) alts)
48− show' i (ProjCase tm alts) = "case " ++ show tm ++ " of " ++
48+ show' i (ProjCase tm alt) = "case " ++ show tm ++ " of " ++
49− showSep ("\n" ++ indent i) (map (showA i) alts)
49+ showSep ("\n" ++ indent i) (map (showA i) [alt])
50 show' i (STerm tm) = show tm
50 show' i (STerm tm) = show tm
51 show' i (UnmatchedCase str) = "error " ++ show str
51 show' i (UnmatchedCase str) = "error " ++ show str
52 show' i ImpossibleCase = "impossible"
52 show' i ImpossibleCase = "impossible"
@@ -96,8 +96,7 @@ small n args t = let as = findAllUsedArgs t args in
96namesUsed :: SC -> [Name]
96namesUsed :: SC -> [Name]
97namesUsed sc = nub $ nu' [] sc where
97namesUsed sc = nub $ nu' [] sc where
98 nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]
98 nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]
99− nu' ps (ProjCase t alts) = nub $ (nut ps t ++
99+ nu' ps (ProjCase t alt) = nub $ nut ps t ++ nua ps alt
100− (concatMap (nua ps) alts))
101 nu' ps (STerm t) = nub $ nut ps t
100 nu' ps (STerm t) = nub $ nut ps t
102 nu' ps _ = []
101 nu' ps _ = []
103
102
@@ -122,7 +121,7 @@ namesUsed sc = nub $ nu' [] sc where
122findCalls :: SC -> [Name] -> [(Name, [[Name]])]
121findCalls :: SC -> [Name] -> [(Name, [[Name]])]
123findCalls sc topargs = nub $ nu' topargs sc where
122findCalls sc topargs = nub $ nu' topargs sc where
124 nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)
123 nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)
125− nu' ps (ProjCase t alts) = nub (nut ps t ++ concatMap (nua ps) alts)
124+ nu' ps (ProjCase t alt) = nub (nut ps t ++ nua ps alt)
126 nu' ps (STerm t) = nub $ nut ps t
125 nu' ps (STerm t) = nub $ nut ps t
127 nu' ps _ = []
126 nu' ps _ = []
128
127
@@ -175,7 +174,7 @@ findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)
175
174
176findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where
175findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where
177 nu' (Case n alts) = n : concatMap nua alts
176 nu' (Case n alts) = n : concatMap nua alts
178− nu' (ProjCase t alts) = directUse t ++ concatMap nua alts
177+ nu' (ProjCase t alt) = directUse t ++ nua alt
179 nu' (STerm t) = directUse t
178 nu' (STerm t) = directUse t
180 nu' _ = []
179 nu' _ = []
181
180
@@ -640,12 +639,12 @@ prune proj (Case n alts)
640-- projn t = t
639-- projn t = t
641
640
642 projRep :: Name -> Name -> Int -> SC -> SC
641 projRep :: Name -> Name -> Int -> SC -> SC
642+ projRep arg n i (Case x [alt]) | x == arg
643+ = ProjCase (Proj (P Bound n Erased) i) (projRepAlt arg n i alt)
643 projRep arg n i (Case x alts)
644 projRep arg n i (Case x alts)
644− | x == arg = ProjCase (Proj (P Bound n Erased) i)
645− (map (projRepAlt arg n i) alts)
646− | otherwise = Case x (map (projRepAlt arg n i) alts)
645+ = Case x (map (projRepAlt arg n i) alts)
647− projRep arg n i (ProjCase t alts)
646+ projRep arg n i (ProjCase t alt)
648− = ProjCase (projRepTm arg n i t) (map (projRepAlt arg n i) alts)
647+ = ProjCase (projRepTm arg n i t) (projRepAlt arg n i alt)
649 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)
648 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)
650 projRep arg n i c = c -- unmatched
649 projRep arg n i c = c -- unmatched
651
650
src/Idris/Core/Evaluate.hs+2−2
@@ -389,9 +389,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
389 etm' <- ev ntimes stk (not (conHeaded tm))
389 etm' <- ev ntimes stk (not (conHeaded tm))
390 (amap ++ env) etm
390 (amap ++ env) etm
391 return $ Just etm'
391 return $ Just etm'
392− evTree ntimes stk top env amap (ProjCase t alts)
392+ evTree ntimes stk top env amap (ProjCase t alt)
393 = do t' <- ev ntimes stk top env t
393 = do t' <- ev ntimes stk top env t
394− doCase ntimes stk top env amap t' alts
394+ doCase ntimes stk top env amap t' [alt]
395 evTree ntimes stk top env amap (Case n alts)
395 evTree ntimes stk top env amap (Case n alts)
396 = case lookup n amap of
396 = case lookup n amap of
397 Just v -> doCase ntimes stk top env amap v alts
397 Just v -> doCase ntimes stk top env amap v alts
src/Idris/Erasure.hs+1−1
@@ -44,7 +44,7 @@ findUsed ctx cg ns = union $ map (findUsedDef cg . getDef ctx) ns
44 findUsedSC cg vars ImpossibleCase = M.empty
44 findUsedSC cg vars ImpossibleCase = M.empty
45 findUsedSC cg vars (UnmatchedCase msg) = M.empty
45 findUsedSC cg vars (UnmatchedCase msg) = M.empty
46 findUsedSC cg vars (Case n alts) = undefined
46 findUsedSC cg vars (Case n alts) = undefined
47− findUsedSC cg vars (ProjCase t alts) = undefined
47+ findUsedSC cg vars (ProjCase t alt) = undefined
48 findUsedSC cg vars (STerm t) = undefined
48 findUsedSC cg vars (STerm t) = undefined
49
49
50findUnusedArgs :: [Name] -> Idris ()
50findUnusedArgs :: [Name] -> Idris ()