git.iko.soy/Idris-dev
on master help sign in
Make ProjCase take exactly one alternative. (TODO: is this safe?)
commit59c3cd1466a33fe077bb601d612c5e1ded001f43 authorMatus Tejiscak <ziman@functor.sk> dateMon 16 Dec 2013, 18:10 (13 years ago) parent437322c
4 files changed+18−19
compare with master
unifiedsplit
src/IRTS/Compiler.hs+3−3 src/Idris/Core/CaseTree.hs+12−13 src/Idris/Core/Evaluate.hs+2−2 src/Idris/Erasure.hs+1−1
src/IRTS/Compiler.hs+3−3
@@ -370,9 +370,9 @@ instance ToIR SC where
370370
371371 ir' (STerm t) = ir t
372372 ir' (UnmatchedCase str) = return $ LError str
373− ir' (ProjCase tm alts) = do tm' <- ir tm
374− alts' <- mapM (mkIRAlt tm') alts
375− return $ LCase tm' alts'
373+ ir' (ProjCase tm alt) = do tm' <- ir tm
374+ alt' <- mkIRAlt tm' alt
375+ return $ LCase tm' [alt']
376376 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
377377 return $ LCase (LV (Glob n)) alts'
378378 ir' ImpossibleCase = return LNothing
src/Idris/Core/CaseTree.hs+12−13
@@ -14,8 +14,8 @@ import Debug.Trace
1414data CaseDef = CaseDef [Name] !SC [Term]
1515 deriving Show
1616
17−data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first
18− | ProjCase t [CaseAlt' t] -- ^ special case for projections
17+data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first
18+ | ProjCase t (CaseAlt' t) -- ^ special case for projections
1919 | STerm !t
2020 | UnmatchedCase String -- ^ error message
2121 | ImpossibleCase -- ^ already checked to be impossible
@@ -45,8 +45,8 @@ instance Show t => Show (SC' t) where
4545 where
4646 show' i (Case n alts) = "case " ++ show n ++ " of\n" ++ indent i ++
4747 showSep ("\n" ++ indent i) (map (showA i) alts)
48− show' i (ProjCase tm alts) = "case " ++ show tm ++ " of " ++
49− showSep ("\n" ++ indent i) (map (showA i) alts)
48+ show' i (ProjCase tm alt) = "case " ++ show tm ++ " of " ++
49+ showSep ("\n" ++ indent i) (map (showA i) [alt])
5050 show' i (STerm tm) = show tm
5151 show' i (UnmatchedCase str) = "error " ++ show str
5252 show' i ImpossibleCase = "impossible"
@@ -96,8 +96,7 @@ small n args t = let as = findAllUsedArgs t args in
9696namesUsed :: SC -> [Name]
9797namesUsed sc = nub $ nu' [] sc where
9898 nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]
99− nu' ps (ProjCase t alts) = nub $ (nut ps t ++
100− (concatMap (nua ps) alts))
99+ nu' ps (ProjCase t alt) = nub $ nut ps t ++ nua ps alt
101100 nu' ps (STerm t) = nub $ nut ps t
102101 nu' ps _ = []
103102
@@ -122,7 +121,7 @@ namesUsed sc = nub $ nu' [] sc where
122121findCalls :: SC -> [Name] -> [(Name, [[Name]])]
123122findCalls sc topargs = nub $ nu' topargs sc where
124123 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)
126125 nu' ps (STerm t) = nub $ nut ps t
127126 nu' ps _ = []
128127
@@ -175,7 +174,7 @@ findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)
175174
176175findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where
177176 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
179178 nu' (STerm t) = directUse t
180179 nu' _ = []
181180
@@ -640,12 +639,12 @@ prune proj (Case n alts)
640639-- projn t = t
641640
642641 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)
643644 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)
647− projRep arg n i (ProjCase t alts)
648− = ProjCase (projRepTm arg n i t) (map (projRepAlt arg n i) alts)
645+ = Case x (map (projRepAlt arg n i) alts)
646+ projRep arg n i (ProjCase t alt)
647+ = ProjCase (projRepTm arg n i t) (projRepAlt arg n i alt)
649648 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)
650649 projRep arg n i c = c -- unmatched
651650
src/Idris/Core/Evaluate.hs+2−2
@@ -389,9 +389,9 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
389389 etm' <- ev ntimes stk (not (conHeaded tm))
390390 (amap ++ env) etm
391391 return $ Just etm'
392− evTree ntimes stk top env amap (ProjCase t alts)
392+ evTree ntimes stk top env amap (ProjCase t alt)
393393 = 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]
395395 evTree ntimes stk top env amap (Case n alts)
396396 = case lookup n amap of
397397 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
4444 findUsedSC cg vars ImpossibleCase = M.empty
4545 findUsedSC cg vars (UnmatchedCase msg) = M.empty
4646 findUsedSC cg vars (Case n alts) = undefined
47− findUsedSC cg vars (ProjCase t alts) = undefined
47+ findUsedSC cg vars (ProjCase t alt) = undefined
4848 findUsedSC cg vars (STerm t) = undefined
4949
5050findUnusedArgs :: [Name] -> Idris ()