git.iko.soy/Idris-dev
on 0306e49 help sign in
Idris-dev/src/Core/CaseTree.hs
252 lines 9.3 kB history raw
1module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,
2 simpleCase, small, namesUsed) where
4import Core.TT
6import Control.Monad.State
7import Data.Maybe
8import Data.List hiding (partition)
9import Debug.Trace
11data CaseDef = CaseDef [Name] SC [Term]
12 deriving Show
14data SC = Case Name [CaseAlt] -- invariant: lowest tags first
15 | STerm Term
16 | UnmatchedCase String -- error message
17 deriving (Show, Eq, Ord)
18{-!
19deriving instance Binary SC
20!-}
22data CaseAlt = ConCase Name Int [Name] SC
23 | ConstCase Const SC
24 | DefaultCase SC
25 deriving (Show, Eq, Ord)
26{-!
27deriving instance Binary CaseAlt
28!-}
30type CaseTree = SC
31type Clause = ([Pat], (Term, Term))
32type CS = ([Term], Int)
34-- simple terms can be inlined trivially - good for primitives in particular
35small :: SC -> Bool
36-- small (STerm t) = True
37small _ = False
39namesUsed :: SC -> [Name]
40namesUsed sc = nub $ nu' [] sc where
41 nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]
42 nu' ps (STerm t) = nub $ nut ps t
43 nu' ps _ = []
45 nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args
46 nua ps (ConstCase _ sc) = nu' ps sc
47 nua ps (DefaultCase sc) = nu' ps sc
49 nut ps (P _ n _) | n `elem` ps = []
50 | otherwise = [n]
51 nut ps (App f a) = nut ps f ++ nut ps a
52 nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc
53 nut ps (Bind n b sc) = nut (n:ps) sc
54 nut ps _ = []
56simpleCase :: Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef
57simpleCase tc cover fc []
58 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []
59simpleCase tc cover fc cs
60 = let pats = map (\ (avs, l, r) -> (avs, toPats tc l, (l, r))) cs
61 chkPats = mapM chkAccessible pats in
62 case chkPats of
63 OK pats ->
64 let numargs = length (fst (head pats))
65 ns = take numargs args
66 (tree, st) = runState
67 (match ns pats (defaultCase cover)) ([], numargs) in
68 return $ CaseDef ns (prune tree) (fst st)
69 Error err -> Error (At fc err)
70 where args = map (\i -> MN i "e") [0..]
71 defaultCase True = STerm Erased
72 defaultCase False = UnmatchedCase "Error"
74 chkAccessible (avs, l, c) = do mapM_ (acc l) avs
75 return (l, c)
77 acc [] n = Error (Inaccessible n)
78 acc (PV x : xs) n | x == n = OK ()
79 acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n
80 acc (_ : xs) n = acc xs n
82data Pat = PCon Name Int [Pat]
83 | PConst Const
84 | PV Name
85 | PAny
86 deriving Show
88-- If there are repeated variables, take the *last* one (could be name shadowing
89-- in a where clause, so take the most recent).
91toPats :: Bool -> Term -> [Pat]
92toPats tc f = reverse (toPat tc (getArgs f)) where
93 getArgs (App f a) = a : getArgs f
94 getArgs _ = []
96toPat :: Bool -> [Term] -> [Pat]
97toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []
98 where
99 toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args
100 return $ PCon n t args'
101 -- Typecase
102 toPat' (P (TCon t a) n _) args | tc
103 = do args' <- mapM (\x -> toPat' x []) args
104 return $ PCon n t args'
105 toPat' (Constant IType) [] | tc = return $ PCon (UN "Int") 1 []
106 toPat' (Constant FlType) [] | tc = return $ PCon (UN "Float") 2 []
107 toPat' (Constant ChType) [] | tc = return $ PCon (UN "Char") 3 []
108 toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []
109 toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []
110 toPat' (Constant BIType) [] | tc = return $ PCon (UN "Integer") 6 []
112 toPat' (P Bound n _) [] = do ns <- get
113 if n `elem` ns
114 then return PAny
115 else do put (n : ns)
116 return (PV n)
117 toPat' (App f a) args = toPat' f (a : args)
118 toPat' (Constant (I c)) [] = return $ PConst (I c)
119 toPat' _ _ = return PAny
122data Partition = Cons [Clause]
123 | Vars [Clause]
125isVarPat (PV _ : ps , _) = True
126isVarPat (PAny : ps , _) = True
127isVarPat _ = False
129isConPat (PCon _ _ _ : ps, _) = True
130isConPat (PConst _ : ps, _) = True
131isConPat _ = False
133partition :: [Clause] -> [Partition]
134partition [] = []
135partition ms@(m : _)
136 | isVarPat m = let (vars, rest) = span isVarPat ms in
137 Vars vars : partition rest
138 | isConPat m = let (cons, rest) = span isConPat ms in
139 Cons cons : partition rest
140partition xs = error $ "Partition " ++ show xs
142match :: [Name] -> [Clause] -> SC -- error case
143 -> State CS SC
144match [] (([], ret) : xs) err
145 = do (ts, v) <- get
146 put (ts ++ (map (fst.snd) xs), v)
147 return $ STerm (snd ret) -- run out of arguments
148match vs cs err = do cs <- mixture vs (partition cs) err
149 return cs
151mixture :: [Name] -> [Partition] -> SC -> State CS SC
152mixture vs [] err = return err
153mixture vs (Cons ms : ps) err = do fallthrough <- mixture vs ps err
154 conRule vs ms fallthrough
155mixture vs (Vars ms : ps) err = do fallthrough <- mixture vs ps err
156 varRule vs ms fallthrough
158data ConType = CName Name Int -- named constructor
159 | CConst Const -- constant, not implemented yet
161data Group = ConGroup ConType -- Constructor
162 [([Pat], Clause)] -- arguments and rest of alternative
164conRule :: [Name] -> [Clause] -> SC -> State CS SC
165conRule (v:vs) cs err = do groups <- groupCons cs
166 caseGroups (v:vs) groups err
168caseGroups :: [Name] -> [Group] -> SC -> State CS SC
169caseGroups (v:vs) gs err = do g <- altGroups gs
170 return $ Case v (sort g)
171 where
172 altGroups [] = return [DefaultCase err]
173 altGroups (ConGroup (CName n i) args : cs)
174 = do g <- altGroup n i args
175 rest <- altGroups cs
176 return (g : rest)
177 altGroups (ConGroup (CConst c) args : cs)
178 = do g <- altConstGroup c args
179 rest <- altGroups cs
180 return (g : rest)
182 altGroup n i gs = do (newArgs, nextCs) <- argsToAlt gs
183 matchCs <- match (newArgs ++ vs) nextCs err
184 return $ ConCase n i newArgs matchCs
185 altConstGroup n gs = do (_, nextCs) <- argsToAlt gs
186 matchCs <- match vs nextCs err
187 return $ ConstCase n matchCs
189argsToAlt :: [([Pat], Clause)] -> State CS ([Name], [Clause])
190argsToAlt [] = return ([], [])
191argsToAlt rs@((r, m) : _)
192 = do newArgs <- getNewVars r
193 return (newArgs, addRs rs)
194 where
195 getNewVars [] = return []
196 getNewVars ((PV n) : ns) = do nsv <- getNewVars ns
197 return (n : nsv)
198 getNewVars (_ : ns) = do v <- getVar
199 nsv <- getNewVars ns
200 return (v : nsv)
201 addRs [] = []
202 addRs ((r, (ps, res)) : rs) = ((r++ps, res) : addRs rs)
204getVar :: State CS Name
205getVar = do (t, v) <- get; put (t, v+1); return (MN v "e")
207groupCons :: [Clause] -> State CS [Group]
208groupCons cs = gc [] cs
209 where
210 gc acc [] = return acc
211 gc acc ((p : ps, res) : cs) =
212 do acc' <- addGroup p ps res acc
213 gc acc' cs
214 addGroup p ps res acc = case p of
215 PCon con i args -> return $ addg con i args (ps, res) acc
216 PConst cval -> return $ addConG cval (ps, res) acc
217 pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"
219 addg con i conargs res [] = [ConGroup (CName con i) [(conargs, res)]]
220 addg con i conargs res (g@(ConGroup (CName n j) cs):gs)
221 | i == j = ConGroup (CName n i) (cs ++ [(conargs, res)]) : gs
222 | otherwise = g : addg con i conargs res gs
224 addConG con res [] = [ConGroup (CConst con) [([], res)]]
225 addConG con res (g@(ConGroup (CConst n) cs) : gs)
226 | con == n = ConGroup (CConst n) (cs ++ [([], res)]) : gs
227 | otherwise = g : addConG con res gs
229varRule :: [Name] -> [Clause] -> SC -> State CS SC
230varRule (v : vs) alts err =
231 do let alts' = map (repVar v) alts
232 match vs alts' err
233 where
234 repVar v (PV p : ps , (lhs, res)) = (ps, (lhs, subst p (P Bound v (V 0)) res))
235 repVar v (PAny : ps , res) = (ps, res)
237prune :: SC -> SC
238prune (Case n alts)
239 = let alts' = map pruneAlt $
240 filter notErased alts in
241 case alts' of
242 [] -> STerm Erased
243 as -> Case n as
244 where pruneAlt (ConCase cn i ns sc) = ConCase cn i ns (prune sc)
245 pruneAlt (ConstCase c sc) = ConstCase c (prune sc)
246 pruneAlt (DefaultCase sc) = DefaultCase (prune sc)
248 notErased (DefaultCase (STerm Erased)) = False
249 notErased _ = True
250prune t = t