git.iko.soy/Idris-dev
on fadbbc8 help sign in
Idris-dev/src/Idris/CaseSplit.hs
310 lines 12 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.CaseSplit(splitOnLine, replaceSplits,
4 getClause, getProofClause,
5 mkWith,
6 getUniq, nameRoot) where
8-- splitting a variable in a pattern clause
10import Idris.AbsSyntax
11import Idris.ElabDecls
12import Idris.ElabTerm
13import Idris.Delaborate
14import Idris.Parser
15import Idris.Error
17import Core.TT
18import Core.Typecheck
19import Core.Evaluate
21import Data.Maybe
22import Data.Char
23import Control.Monad
24import Control.Monad.State.Strict
26import Text.Parser.Combinators
27import Text.Parser.Char(anyChar)
28import Text.Trifecta(Result(..), parseString)
29import Text.Trifecta.Delta
30import qualified Data.ByteString.UTF8 as UTF8
32import Debug.Trace
34{-
36Given a pattern clause and a variable 'n', elaborate the clause and find the
37type of 'n'.
39Make new pattern clauses by replacing 'n' with all the possibly constructors
40applied to '_', and replacing all other variables with '_' in order to
41resolve other dependencies.
43Finally, merge the generated patterns with the original, by matching.
44Always take the "more specific" argument when there is a discrepancy, i.e.
45names over '_', patterns over names, etc.
46-}
48-- Given a variable to split, and a term application, return a list of
49-- variable updates
50split :: Name -> PTerm -> Idris [[(Name, PTerm)]]
51split n t'
52 = do ist <- getIState
53 (tm, ty, pats) <- elabValBind toplevel True (addImplPat ist t')
54 logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
55-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
56-- iputStrLn (show pats)
57 let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
58 let ctxt = tt_ctxt ist
59 case lookup n pats of
60 Nothing -> fail $ show n ++ " is not a pattern variable"
61 Just ty ->
62 do let splits = findPats ist ty
63 iLOG ("New patterns " ++ showSep ", "
64 (map (showImp Nothing True False) splits))
65 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
66 logLvl 4 ("Working from " ++ show t)
67 logLvl 4 ("Trying " ++ showSep "\n"
68 (map (showImp Nothing True False) newPats_in))
69 newPats <- mapM elabNewPat newPats_in
70 logLvl 3 ("Original:\n" ++ show t)
71 logLvl 3 ("Split:\n" ++
72 (showSep "\n" (map show (mapMaybe id newPats))))
73 logLvl 3 "----"
74 let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)
75 iLOG ("Name updates " ++ showSep "\n"
76 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))
77 return (map snd newPats')
79data MergeState = MS { namemap :: [(Name, Name)],
80 updates :: [(Name, PTerm)] }
82addUpdate n tm = do ms <- get
83 put (ms { updates = ((n, stripNS tm) : updates ms) } )
85stripNS tm = mapPT dens tm where
86 dens (PRef fc n) = PRef fc (nsroot n)
87 dens t = t
89mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
90mergeAllPats ctxt t [] = []
91mergeAllPats ctxt t (p : ps)
92 = let (p', MS _ u) = runState (mergePat ctxt t p) (MS [] [])
93 ps' = mergeAllPats ctxt t ps in
94 ((p, u) : ps')
96mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm
97-- If any names are unified, make sure they stay unified. Always prefer
98-- user provided name (first pattern)
99mergePat ctxt (PPatvar fc n) new
100 = mergePat ctxt (PRef fc n) new
101mergePat ctxt old (PPatvar fc n)
102 = mergePat ctxt old (PRef fc n)
103mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
104 | isDConName n' ctxt = do addUpdate n new;
105 return new
106 | otherwise
107 = do ms <- get
108 case lookup n' (namemap ms) of
109 Just x -> do addUpdate n (PRef fc x)
110 return (PRef fc x)
111 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })
112 return (PRef fc n)
113mergePat ctxt (PApp _ _ args) (PApp fc f args')
114 = do newArgs <- zipWithM mergeArg args args'
115 return (PApp fc f newArgs)
116 where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)
117 case x of
118 (PImp _ _ _ _ _ _) ->
119 return (y { machine_inf = machine_inf x,
120 getTm = tm' })
121 _ -> return (y { getTm = tm' })
122mergePat ctxt (PRef fc n) t = do tm <- tidy t
123 addUpdate n tm
124 return tm
125mergePat ctxt x y = return y
127mergeUserImpl :: PTerm -> PTerm -> PTerm
128mergeUserImpl x y = x
130tidy orig@(PRef fc n)
131 = do ms <- get
132 case lookup n (namemap ms) of
133 Just x -> return (PRef fc x)
134 Nothing -> case n of
135 (UN _) -> return orig
136 _ -> return Placeholder
137tidy (PApp fc f args)
138 = do args' <- mapM tidyArg args
139 return (PApp fc f args')
140 where tidyArg x = do tm' <- tidy (getTm x)
141 return (x { getTm = tm' })
142tidy tm = return tm
145-- mapPT tidyVar tm
146-- where tidyVar (PRef _ _) = Placeholder
147-- tidyVar t = t
149elabNewPat :: PTerm -> Idris (Maybe PTerm)
150elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t
151 i <- getIState
152 return (Just (delab i tm)))
153 (\e -> do i <- getIState
154 logLvl 5 $ "Not a valid split:\n" ++ pshow i e
155 return Nothing)
157findPats :: IState -> Type -> [PTerm]
158findPats ist t | (P _ n _, _) <- unApply t
159 = case lookupCtxt n (idris_datatypes ist) of
160 [ti] -> map genPat (con_names ti)
161 _ -> [Placeholder]
162 where genPat n = case lookupCtxt n (idris_implicits ist) of
163 [args] -> PApp emptyFC (PRef emptyFC n)
164 (map toPlaceholder args)
165 _ -> error $ "Can't happen (genPat) " ++ show n
166 toPlaceholder tm = tm { getTm = Placeholder }
167findPats ist t = [Placeholder]
169replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
170replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
171 where subst :: PTerm -> PTerm
172 subst orig@(PPatvar _ v) | v == n = t
173 | otherwise = Placeholder
174 subst orig@(PRef _ v) | v == n = t
175 | isDConName v ctxt = orig
176 subst (PRef _ _) = Placeholder
177 subst (PApp fc (PRef _ t) pats)
178 | isTConName t ctxt = Placeholder -- infer types
179 subst (PApp fc f pats) = PApp fc f (map substArg pats)
180 subst (PEq fc l r) = PEq fc (subst l) (subst r)
181 subst x = x
183 substArg arg = arg { getTm = subst (getTm arg) }
185replaceVar ctxt n t pat = pat
187splitOnLine :: Int -- ^ line number
188 -> Name -- ^ variable
189 -> FilePath -- ^ name of file
190 -> Idris [[(Name, PTerm)]]
191splitOnLine l n fn = do
192-- let (before, later) = splitAt (l-1) (lines inp)
193-- i <- getIState
194 cl <- getInternalApp fn l
195 logLvl 3 ("Working with " ++ showImp Nothing True False cl)
196 tms <- split n cl
197-- iputStrLn (showSep "\n" (map show tms))
198 return tms -- "" -- not yet done...
200replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
201replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
202 where
203 rep str [] = str ++ "\n"
204 rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow False tm) str) ups
206 updateRHSs i [] = return []
207 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
208 xs' <- updateRHSs i' xs
209 return (x' : xs')
211 updateRHS i ('?':'=':xs) = do (xs', i') <- updateRHS i xs
212 return ("?=" ++ xs', i')
213 updateRHS i ('?':xs) = do let (nm, rest) = span (not . isSpace) xs
214 (nm', i') <- getUniq nm i
215 return ('?':nm' ++ rest, i')
216 updateRHS i (x : xs) = do (xs', i') <- updateRHS i xs
217 return (x : xs', i')
218 updateRHS i [] = return ("", i)
221 -- TMP HACK: If there are Nats, we don't want to show as numerals since
222 -- this isn't supported in a pattern, so special case here
223 nshow brack (PRef _ (UN "Z")) = "Z"
224 nshow brack (PApp _ (PRef _ (UN "S")) [x]) =
225 if brack then "(S " else "S " ++ nshow True (getTm x) ++
226 if brack then ")" else ""
227 nshow _ t = show t
229 -- if there's any {n} replace with {n=n}
230 expandBraces ('{' : xs)
231 = let (brace, (_:rest)) = span (/= '}') xs in
232 if (not ('=' `elem` brace))
233 then ('{' : brace ++ " = " ++ brace ++ "}") ++
234 expandBraces rest
235 else ('{' : brace ++ "}") ++ expandBraces rest
236 expandBraces (x : xs) = x : expandBraces xs
237 expandBraces [] = []
239 updatePat start n tm [] = []
240 updatePat start n tm ('{':rest) =
241 let (space, rest') = span isSpace rest in
242 '{' : space ++ updatePat False n tm rest'
243 updatePat True n tm xs@(c:rest) | length xs > length n
244 = let (before, after@(next:_)) = splitAt (length n) xs in
245 if (before == n && not (isAlpha next))
246 then addBrackets tm ++ updatePat False n tm after
247 else c : updatePat (not (isAlpha c)) n tm rest
248 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest
250 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"
251 | otherwise = tm
253getUniq nm i
254 = do ist <- getIState
255 let n = nameRoot [] nm ++ "_" ++ show i
256 case lookupTy (UN n) (tt_ctxt ist) of
257 [] -> return (n, i+1)
258 _ -> getUniq nm (i+1)
260nameRoot acc nm | all isDigit nm = showSep "_" acc
261nameRoot acc nm =
262 case span (/='_') nm of
263 (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
264 _ -> showSep "_" (acc ++ [nm])
266getClause :: Int -> -- ^ Line type is declared on
267 Name -> -- ^ Function name
268 FilePath -> -- ^ Source file name
269 Idris String
270getClause l fn fp = do ty <- getInternalApp fp l
271 let ap = mkApp ty [1..]
272 return (show fn ++ " " ++ ap ++
273 "= ?" ++ show fn ++ "_rhs")
274 where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)
275 = "x" ++ show n ++ " " ++ mkApp sc ns
276 mkApp (PPi (Exp _ _ _ False) n _ sc) ns
277 = show n ++ " " ++ mkApp sc ns
278 mkApp (PPi _ _ _ sc) ns = mkApp sc ns
279 mkApp _ _ = ""
281getProofClause :: Int -> -- ^ Line type is declared on
282 Name -> -- ^ Function name
283 FilePath -> -- ^ Source file name
284 Idris String
285getProofClause l fn fp
286 = do ty <- getInternalApp fp l
287 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
288 where mkApp (PPi _ _ _ sc) = mkApp sc
289 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
291-- Purely syntactic - turn a pattern match clause into a with and a new
292-- match clause
294mkWith :: String -> Name -> String
295mkWith str n = let ind = getIndent str
296 str' = replicate ind ' ' ++
297 replaceRHS str "with (_)"
298 newpat = replicate (ind + 2) ' ' ++
299 replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in
300 str' ++ "\n" ++ newpat
302 where getIndent s = length (takeWhile isSpace s)
304 replaceRHS [] str = str
305 replaceRHS ('?':'=': rest) str = str
306 replaceRHS ('=': rest) str
307 | not ('=' `elem` rest) = str
308 replaceRHS (x : rest) str = x : replaceRHS rest str