@@ -1,6 +1,6 @@
11{-# LANGUAGE PatternGuards #-}
22
3−module Idris.CaseSplit(split, splitOnLine) where
3+module Idris.CaseSplit(split, splitOnLine, replaceSplits) where
44
55-- splitting a variable in a pattern clause
66
@@ -16,6 +16,7 @@ import Core.Typecheck
1616import Core.Evaluate
1717
1818import Data.Maybe
19+import Data.Char
1920import Control.Monad
2021import Control.Monad.State.Strict
2122
@@ -25,6 +26,8 @@ import Text.Trifecta(Result(..), parseString)
2526import Text.Trifecta.Delta
2627import qualified Data.ByteString.UTF8 as UTF8
2728
29+import Debug.Trace
30+
2831{-
2932
3033Given a pattern clause and a variable 'n', elaborate the cluse and find the
@@ -71,7 +74,11 @@ data MergeState = MS { namemap :: [(Name, Name)],
7174 updates :: [(Name, PTerm)] }
7275
7376addUpdate 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
7582
7683mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]
7784mergeAllPats ctxt t [] = []
@@ -169,9 +176,8 @@ replaceVar ctxt n t pat = pat
169176splitOnLine :: Int -- ^ line number
170177 -> Name -- ^ variable
171178 -> FilePath -- ^ name of file
172− -> String -- ^ file contents
173179 -> Idris [[(Name, PTerm)]]
174−splitOnLine l n fn inp = do
180+splitOnLine l n fn = do
175181-- let (before, later) = splitAt (l-1) (lines inp)
176182-- i <- getIState
177183 cl <- getInternalApp fn l
@@ -180,7 +186,43 @@ splitOnLine l n fn inp = do
180186-- iputStrLn (showSep "\n" (map show tms))
181187 return tms -- "" -- not yet done...
182188
183−getFnName (PClause _ n _ _ _ _) = n
184−getFnName (PWith _ n _ _ _ _) = n
189+replaceSplits :: String -> [[(Name, PTerm)]] -> [String]
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+
185227
186228