Repl prints listy things with sugar

Searches for applications of "Nil" and "::" and prints them accordingly.

src/Idris/AbsSyntaxTree.hs

@@ -1014,6 +1014,8 @@ showImp impl tm = se 10 tm where
         = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
     se p (PPi (TacImp _ _ s _) n ty sc)
         = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
+    se p e
+        | Just str <- slist p e = str
     se p (PApp _ (PRef _ f) [])
         | not impl = show f
     se p (PApp _ (PRef _ op@(UN (f:_))) args)
@@ -1052,6 +1054,25 @@ showImp impl tm = se 10 tm where
     se p (PCoerced t) = se p t
 --     se p x = "Not implemented"
 
+    slist' p (PApp _ (PRef _ nil) _)
+      | nsroot nil == UN "Nil" = Just []
+    slist' p (PApp _ (PRef _ cons) args)
+      | nsroot cons == UN "::",
+        (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
+        all isImp imps,
+        Just tl' <- slist' p tl
+      = Just (hd:tl')
+      where
+        isImp (PImp {}) = True
+        isImp _         = False
+    slist' _ _ = Nothing
+
+    slist p e | Just es <- slist' p e = Just $
+      case es of []  -> "[]"
+                 [x] -> "[" ++ se p x ++ "]"
+                 xs  -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
+    slist _ _ = Nothing
+
     sArg (PImp _ _ n tm _) = siArg (n, tm)
     sArg (PExp _ _ tm _) = seArg tm
     sArg (PConstraint _ _ tm _) = scArg tm