git.iko.soy/Idris-dev
on master help sign in
Add replaceSplits to generate new definition
bba09bdEdwin Brady
src/Idris/CaseSplit.hs+48−6
compare with master
unifiedsplit
@@ -1,6 +1,6 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2
2
3−module Idris.CaseSplit(split, splitOnLine) where
3+module Idris.CaseSplit(split, splitOnLine, replaceSplits) where
4
4
5-- splitting a variable in a pattern clause
5-- splitting a variable in a pattern clause
6
6
@@ -16,6 +16,7 @@ import Core.Typecheck
16import Core.Evaluate
16import Core.Evaluate
17
17
18import Data.Maybe
18import Data.Maybe
19+import Data.Char
19import Control.Monad
20import Control.Monad
20import Control.Monad.State.Strict
21import Control.Monad.State.Strict
21
22
@@ -25,6 +26,8 @@ import Text.Trifecta(Result(..), parseString)
25import Text.Trifecta.Delta
26import Text.Trifecta.Delta
26import qualified Data.ByteString.UTF8 as UTF8
27import qualified Data.ByteString.UTF8 as UTF8
27
28
29+import Debug.Trace
30+
28{-
31{-
29
32
30Given a pattern clause and a variable 'n', elaborate the cluse and find the
33Given a pattern clause and a variable 'n', elaborate the cluse and find the
@@ -71,7 +74,11 @@ data MergeState = MS { namemap :: [(Name, Name)],
71 updates :: [(Name, PTerm)] }
74 updates :: [(Name, PTerm)] }
72
75
73addUpdate n tm = do ms <- get
76addUpdate n tm = do ms <- get
74− put (ms { updates = ((n, tm) : updates ms) } )
77+ put (ms { updates = ((n, stripNS tm) : updates ms) } )
78+
79+stripNS tm = mapPT dens tm where
80+ dens (PRef fc n) = PRef fc (nsroot n)
81+ dens t = t
75
82
76mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
83mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
77mergeAllPats ctxt t [] = []
84mergeAllPats ctxt t [] = []
@@ -169,9 +176,8 @@ replaceVar ctxt n t pat = pat
169splitOnLine :: Int -- ^ line number
176splitOnLine :: Int -- ^ line number
170 -> Name -- ^ variable
177 -> Name -- ^ variable
171 -> FilePath -- ^ name of file
178 -> FilePath -- ^ name of file
172− -> String -- ^ file contents
173 -> Idris [[(Name, PTerm)]]
179 -> Idris [[(Name, PTerm)]]
174−splitOnLine l n fn inp = do
180+splitOnLine l n fn = do
175-- let (before, later) = splitAt (l-1) (lines inp)
181-- let (before, later) = splitAt (l-1) (lines inp)
176-- i <- getIState
182-- i <- getIState
177 cl <- getInternalApp fn l
183 cl <- getInternalApp fn l
@@ -180,7 +186,43 @@ splitOnLine l n fn inp = do
180-- iputStrLn (showSep "\n" (map show tms))
186-- iputStrLn (showSep "\n" (map show tms))
181 return tms -- "" -- not yet done...
187 return tms -- "" -- not yet done...
182
188
183−getFnName (PClause _ n _ _ _ _) = n
189+replaceSplits :: String -> [[(Name, PTerm)]] -> [String]
184−getFnName (PWith _ n _ _ _ _) = n
190+replaceSplits l ups = map (rep (expandBraces l)) ups
191+ where
192+ rep str [] = str
193+ rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow False tm) str) ups
194+
195+ -- TMP HACK: If there are Nats, we don't want to show as numerals since
196+ -- this isn't supported in a pattern, so special case here
197+ nshow brack (PRef _ (UN "Z")) = "Z"
198+ nshow brack (PApp _ (PRef _ (UN "S")) [x]) =
199+ if brack then "(S " else "S " ++ nshow True (getTm x) ++
200+ if brack then ")" else ""
201+ nshow _ t = show t
202+
203+ -- if there's any {n} replace with {n=n}
204+ expandBraces ('{' : xs)
205+ = let (brace, (_:rest)) = span (/= '}') xs in
206+ if (not ('=' `elem` brace))
207+ then ('{' : brace ++ " = " ++ brace ++ "}") ++
208+ expandBraces rest
209+ else ('{' : brace ++ "}") ++ expandBraces rest
210+ expandBraces (x : xs) = x : expandBraces xs
211+ expandBraces [] = []
212+
213+ updatePat start n tm [] = []
214+ updatePat start n tm ('{':rest) =
215+ let (space, rest') = span isSpace rest in
216+ '{' : space ++ updatePat False n tm rest'
217+ updatePat True n tm xs@(c:rest) | length xs > length n
218+ = let (before, after@(next:_)) = splitAt (length n) xs in
219+ if (before == n && not (isAlpha next))
220+ then addBrackets tm ++ updatePat False n tm after
221+ else c : updatePat (not (isAlpha c)) n tm rest
222+ updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest
223+
224+ addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"
225+ | otherwise = tm
226+
185
227
186
228
src/Idris/REPL.hs+6−2
@@ -428,8 +428,12 @@ process fn (CaseSplit n t)
428 iputStrLn (showSep "\n" (map show tms))
428 iputStrLn (showSep "\n" (map show tms))
429process fn (CaseSplitAt l n)
429process fn (CaseSplitAt l n)
430 = do src <- runIO $ readFile fn
430 = do src <- runIO $ readFile fn
431− res <- splitOnLine l n fn src
431+ res <- splitOnLine l n fn
432+ iLOG (showSep "\n" (map show res))
433+ let (before, (ap : later)) = splitAt (l-1) (lines src)
432− iputStrLn (showSep "\n" (map show res))
434+ iputStrLn (showSep "\n" (replaceSplits ap res))
435+
436+
433process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
437process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t
434 ctxt <- getContext
438 ctxt <- getContext
435 ist <- getIState
439 ist <- getIState