[ breaking ] remove List1 related ambiguities (#690)

libs/base/Data/Either.idr

@@ -1,7 +1,24 @@
 module Data.Either
 
+import Data.List1
+
 %default total
 
+--------------------------------------------------------------------------------
+-- Checking for a specific constructor
+
+||| Extract the Left value, if possible
+public export
+getLeft : Either a b -> Maybe a
+getLeft (Left a) = Just a
+getLeft _ = Nothing
+
+||| Extract the Right value, if possible
+public export
+getRight : Either a b -> Maybe b
+getRight (Right b) = Just b
+getRight _ = Nothing
+
 ||| True if the argument is Left, False otherwise
 public export
 isLeft : Either a b -> Bool
@@ -14,6 +31,35 @@ isRight : Either a b -> Bool
 isRight (Left _)  = False
 isRight (Right _) = True
 
+--------------------------------------------------------------------------------
+-- Grouping values
+
+mutual
+
+  ||| Compress the list of Lefts and Rights by accumulating
+  ||| all of the lefts and rights into non-empty blocks.
+  export
+  compress : List (Either a b) -> List (Either (List1 a) (List1 b))
+  compress [] = []
+  compress (Left a :: abs) = compressLefts (singleton a) abs
+  compress (Right b :: abs) = compressRights (singleton b) abs
+
+  compressLefts : List1 a -> List (Either a b) -> List (Either (List1 a) (List1 b))
+  compressLefts acc (Left a :: abs) = compressLefts (cons a acc) abs
+  compressLefts acc abs = Left (reverse acc) :: compress abs
+
+  compressRights : List1 b -> List (Either a b) -> List (Either (List1 a) (List1 b))
+  compressRights acc (Right b :: abs) = compressRights (cons b acc) abs
+  compressRights acc abs = Right (reverse acc) :: compress abs
+
+||| Decompress a compressed list. This is the left inverse of `compress` but not its
+||| right inverse because nothing forces the input to be maximally compressed!
+export
+decompress : List (Either (List1 a) (List1 b)) -> List (Either a b)
+decompress = concatMap $ \ abs => case abs of
+  Left as => map Left  $ forget as
+  Right bs => map Right $ forget bs
+
 ||| Keep the payloads of all Left constructors in a list of Eithers
 public export
 lefts : List (Either a b) -> List a
@@ -45,6 +91,19 @@ mirror : Either a b -> Either b a
 mirror (Left  x) = Right x
 mirror (Right x) = Left x
 
+--------------------------------------------------------------------------------
+-- Bifunctor
+
+export
+bimap : (a -> c) -> (b -> d) -> Either a b -> Either c d
+bimap l r (Left a) = Left (l a)
+bimap l r (Right b) = Right (r b)
+
+export
+pushInto : c -> Either a b -> Either (c, a) (c, b)
+pushInto c = bimap (\ a => (c, a)) (\ b => (c, b))
+  -- ^ not using sections to keep it backwards compatible
+
 --------------------------------------------------------------------------------
 -- Conversions
 --------------------------------------------------------------------------------

libs/base/Data/List.idr

@@ -192,8 +192,8 @@ public export
 split : (a -> Bool) -> List a -> List1 (List a)
 split p xs =
   case break p xs of
-    (chunk, [])          => [chunk]
-    (chunk, (c :: rest)) => chunk :: toList (split p (assert_smaller xs rest))
+    (chunk, [])          => singleton chunk
+    (chunk, (c :: rest)) => cons chunk (split p (assert_smaller xs rest))
 
 public export
 splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
@@ -354,7 +354,7 @@ public export
 last : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
 last [] impossible
 last [x] = x
-last (x::y::ys) = last (y::ys)
+last (_::x::xs) = List.last (x::xs)
 
 ||| Return all but the last element of a non-empty list.
 ||| @ ok proof the list is non-empty
@@ -460,19 +460,19 @@ public export
 foldr1 : (a -> a -> a) -> (l : List a)  -> {auto 0 ok : NonEmpty l} -> a
 foldr1 f [] impossible
 foldr1 f [x] = x
-foldr1 f (x::y::ys) = f x (foldr1 f (y::ys))
+foldr1 f (x::y::ys) = f x (List.foldr1 f (y::ys))
 
 ||| Foldl without seeding the accumulator. If the list is empty, return `Nothing`.
 public export
 foldl1' : (a -> a -> a) -> List a -> Maybe a
 foldl1' f [] = Nothing
-foldl1' f xs@(_::_) = Just (foldl1 f xs)
+foldl1' f xs@(_::_) = Just (List.foldl1 f xs)
 
 ||| Foldr without seeding the accumulator. If the list is empty, return `Nothing`.
 public export
 foldr1' : (a -> a -> a) -> List a -> Maybe a
 foldr1' f [] = Nothing
-foldr1' f xs@(_::_) = Just (foldr1 f xs)
+foldr1' f xs@(_::_) = Just (List.foldr1 f xs)
 
 --------------------------------------------------------------------------------
 -- Sorting

libs/base/Data/List1.idr

@@ -2,72 +2,137 @@ module Data.List1
 
 %default total
 
+infixr 7 :::
+
 public export
 record List1 a where
-  constructor (::)
+  constructor (:::)
   head : a
   tail : List a
 
-public export
-toList : (1 xs : List1 a) -> List a
-toList (x :: xs) = x :: xs
+------------------------------------------------------------------------
+-- Conversion
 
+||| Forget that a list is non-empty
 public export
-reverseOnto : (1 acc : List1 a) -> (1 xs : List a) -> List1 a
-reverseOnto acc []        = acc
-reverseOnto acc (x :: xs) = reverseOnto (x :: toList acc) xs
-
-public export
-reverse : (1 xs : List1 a) -> List1 a
-reverse (x :: xs) = reverseOnto [x] xs
+forget : (1 xs : List1 a) -> List a
+forget (x ::: xs) = x :: xs
 
+||| Check whether a list is non-empty
 export
 fromList : (1 xs : List a) -> Maybe (List1 a)
 fromList [] = Nothing
-fromList (x :: xs) = Just (x :: xs)
+fromList (x :: xs) = Just (x ::: xs)
+
+------------------------------------------------------------------------
+-- Basic functions
+
+public export
+singleton : (1 x : a) -> List1 a
+singleton a = a ::: []
+
+export
+last : List1 a -> a
+last (x ::: xs) = loop x xs where
+
+  loop : a -> List a -> a
+  loop x [] = x
+  loop _ (x :: xs) = loop x xs
+
+export
+foldr1' : (a -> b -> b) -> (a -> b) -> List1 a -> b
+foldr1' c n (x ::: xs) = loop x xs where
+
+  loop : a -> List a -> b
+  loop a [] = n a
+  loop a (x :: xs) = c a (loop x xs)
+
+export
+foldr1 : (a -> a -> a) -> List1 a -> a
+foldr1 c = foldr1' c id
+
+export
+foldl1 : (a -> b) -> (b -> a -> b) -> List1 a -> b
+foldl1 n c (x ::: xs) = foldl c (n x) xs
+
+------------------------------------------------------------------------
+-- Append
 
 export
 appendl : (1 xs : List1 a) -> (1 ys : List a) -> List1 a
-appendl (x :: xs) ys = x :: xs ++ ys
+appendl (x ::: xs) ys = x ::: xs ++ ys
 
 export
 append : (1 xs, ys : List1 a) -> List1 a
-append xs ys = appendl xs (toList ys)
+append xs ys = appendl xs (forget ys)
 
 export
 lappend : (1 xs : List a) -> (1 ys : List1 a) -> List1 a
 lappend [] ys = ys
-lappend (x :: xs) ys = append (x :: xs) ys
+lappend (x :: xs) ys = append (x ::: xs) ys
+
+------------------------------------------------------------------------
+-- Cons/Snoc
+
+public export
+cons : (1 x : a) -> (1 xs : List1 a) -> List1 a
+cons x xs = x ::: forget xs
+
+export
+snoc : (1 xs : List1 a) -> (1 x : a) -> List1 a
+snoc xs x = append xs (singleton x)
+
+------------------------------------------------------------------------
+-- Reverse
+
+public export
+reverseOnto : (1 acc : List1 a) -> (1 xs : List a) -> List1 a
+reverseOnto acc [] = acc
+reverseOnto acc (x :: xs) = reverseOnto (x ::: forget acc) xs
+
+public export
+reverse : (1 xs : List1 a) -> List1 a
+reverse (x ::: xs) = reverseOnto (singleton x) xs
+
+------------------------------------------------------------------------
+-- Instances
+
+export
+Semigroup (List1 a) where
+  (<+>) = append
 
 export
 Functor List1 where
-  map f (x :: xs) = f x :: map f xs
-
-export
-Foldable List1 where
-  foldr c n (x :: xs) = c x (foldr c n xs)
-
-export
-Show a => Show (List1 a) where
-  show = show . toList
+  map f (x ::: xs) = f x ::: map f xs
 
 export
 Applicative List1 where
-  pure x = [x]
-  f :: fs <*> xs = appendl (map f xs) (fs <*> toList xs)
+  pure x = singleton x
+  f ::: fs <*> xs = appendl (map f xs) (fs <*> forget xs)
 
 export
 Monad List1 where
-  (x :: xs) >>= f = appendl (f x) (xs >>= toList . f)
+  (x ::: xs) >>= f = appendl (f x) (xs >>= forget . f)
+
+export
+Foldable List1 where
+  foldr c n (x ::: xs) = c x (foldr c n xs)
+
+export
+Show a => Show (List1 a) where
+  show = show . forget
 
 export
 Eq a => Eq (List1 a) where
-  (x :: xs) == (y :: ys) = x == y && xs == ys
+  (x ::: xs) == (y ::: ys) = x == y && xs == ys
 
 export
 Ord a => Ord (List1 a) where
-  compare xs ys = compare (toList xs) (toList ys)
+  compare xs ys = compare (forget xs) (forget ys)
+
+------------------------------------------------------------------------
+-- Properties
 
 export
-consInjective : the (List1 a) (x :: xs) === (y :: ys) -> (x === y, xs === ys)
+consInjective : the (List1 a) (x ::: xs) === (y ::: ys) -> (x === y, xs === ys)
 consInjective Refl = (Refl, Refl)

libs/base/Data/Strings.idr

@@ -301,29 +301,29 @@ parseDouble = mkDouble . wfe . trim
 
     wfe : String -> Maybe (Double, Double, Integer)
     wfe cs = case split (== '.') cs of
-               (wholeAndExp :: []) =>
+               (wholeAndExp ::: []) =>
                  case split (\c => c == 'e' || c == 'E') wholeAndExp of
-                   (whole::exp::[]) =>
+                   (whole:::exp::[]) =>
                      do
                        w <- cast {from=Integer} <$> parseInteger whole
                        e <- parseInteger exp
                        pure (w, 0, e)
-                   (whole::[]) =>
+                   (whole:::[]) =>
                      do
                        w <- cast {from=Integer} <$> parseInteger whole
                        pure (w, 0, 0)
                    _ => Nothing
-               (whole::fracAndExp::[]) =>
+               (whole:::fracAndExp::[]) =>
                  case split (\c => c == 'e' || c == 'E') fracAndExp of
-                   (""::exp::[]) => Nothing
-                   (frac::exp::[]) =>
+                   ("":::exp::[]) => Nothing
+                   (frac:::exp::[]) =>
                      do
                        w <- cast {from=Integer} <$> parseInteger whole
                        f <- (/ (natpow 10 (length frac))) <$>
                             (cast <$> parseNumWithoutSign (unpack frac) 0)
                        e <- parseInteger exp
                        pure (w, if w < 0 then (-f) else f, e)
-                   (frac::[]) =>
+                   (frac:::[]) =>
                      do
                        w <- cast {from=Integer} <$> parseInteger whole
                        f <- (/ (natpow 10 (length frac))) <$>

libs/base/Decidable/Equality.idr

@@ -143,11 +143,11 @@ DecEq a => DecEq (List a) where
 export
 DecEq a => DecEq (List1 a) where
 
-  decEq (x :: xs) (y :: ys) with (decEq x y)
-    decEq (x :: xs) (y :: ys) | No contra = No (contra . fst . consInjective)
-    decEq (x :: xs) (y :: ys) | Yes eqxy with (decEq xs ys)
-    decEq (x :: xs) (y :: ys) | Yes eqxy | No contra = No (contra . snd . consInjective)
-    decEq (x :: xs) (y :: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (::) eqxy eqxsys)
+  decEq (x ::: xs) (y ::: ys) with (decEq x y)
+    decEq (x ::: xs) (y ::: ys) | No contra = No (contra . fst . consInjective)
+    decEq (x ::: xs) (y ::: ys) | Yes eqxy with (decEq xs ys)
+    decEq (x ::: xs) (y ::: ys) | Yes eqxy | No contra = No (contra . snd . consInjective)
+    decEq (x ::: xs) (y ::: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (:::) eqxy eqxsys)
 
 -- TODO: Other prelude data types
 

libs/contrib/Data/List/TailRec.idr

@@ -122,7 +122,7 @@ break_ext p xs = span_ext (not . p) xs
 splitOnto : List (List a) -> (a -> Bool) -> List a -> List1 (List a)
 splitOnto acc p xs =
   case Data.List.break p xs of
-    (chunk, []       ) => reverseOnto [chunk] acc
+    (chunk, []       ) => reverseOnto (chunk ::: []) acc
     (chunk, (c::rest)) => splitOnto (chunk::acc) p rest
 
 export

libs/network/Network/Socket/Data.idr

@@ -186,8 +186,8 @@ export
 parseIPv4 : String -> SocketAddress
 parseIPv4 str =
     case splitted of
-      (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
-      otherwise                   => InvalidAddress
+      (i1 ::: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
+      _ => InvalidAddress
   where
     toInt' : String -> Integer
     toInt' = cast

src/Compiler/Scheme/Chez.idr

@@ -31,7 +31,7 @@ import System.Info
 pathLookup : IO String
 pathLookup
     = do path <- getEnv "PATH"
-         let pathList = List1.toList $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
+         let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
          let candidates = [p ++ "/" ++ x | p <- pathList,
                                            x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
          e <- firstExists candidates

src/Core/Core.idr

@@ -499,7 +499,7 @@ traverse f xs = traverse' f xs []
 
 export
 traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
-traverseList1 f (x :: xs) = [| f x :: traverse f xs |]
+traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |]
 
 export
 traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
@@ -520,7 +520,7 @@ traverse_ f (x :: xs)
 
 export
 traverseList1_ : (a -> Core b) -> List1 a -> Core ()
-traverseList1_ f (x :: xs) = do
+traverseList1_ f (x ::: xs) = do
   f x
   traverse_ f xs
 

src/Core/Hash.idr

@@ -47,7 +47,7 @@ Hashable a => Hashable (List a) where
 
 export
 Hashable a => Hashable (List1 a) where
-  hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs
+  hashWithSalt h (x ::: xs) = hashWithSalt (h * 33 + hash x) xs
 
 export
 Hashable a => Hashable (Maybe a) where

src/Core/Name/Namespace.idr

@@ -50,8 +50,8 @@ nsAsModuleIdent (MkNS ns) = MkMI ns
 export
 mkNamespacedIdent : String -> (Maybe Namespace, String)
 mkNamespacedIdent str = case reverse (split (== '.') str) of
-  [name]       => (Nothing, name)
-  (name :: ns) => (Just (MkNS ns), name)
+  (name ::: []) => (Nothing, name)
+  (name ::: ns) => (Just (MkNS ns), name)
 
 export
 mkNestedNamespace : Maybe Namespace -> String -> Namespace

src/Core/Options/Log.idr

@@ -44,7 +44,7 @@ data LogLevel : Type where
 ||| non-empty topics we can safely make a `LogLevel`.
 export
 mkLogLevel' : Maybe (List1 String) -> Nat -> LogLevel
-mkLogLevel' ps n = MkLogLevel (maybe [] List1.toList ps) n
+mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n
 
 ||| The smart constructor makes sure that the empty string is mapped to the empty
 ||| list. This bypasses the fact that the function `split` returns a non-empty
@@ -94,8 +94,8 @@ export
 parseLogLevel : String -> Maybe LogLevel
 parseLogLevel str = do
   (c, n) <- case split (== ':') str of
-             [n]    => pure (MkLogLevel [], n)
-             [ps,n] => pure (mkLogLevel ps, n)
+             n ::: [] => pure (MkLogLevel [], n)
+             ps ::: [n] => pure (mkLogLevel ps, n)
              _ => Nothing
   lvl <- parsePositive n
   pure $ c (fromInteger lvl)

src/Core/Reflect.idr

@@ -187,19 +187,19 @@ export
 Reify a => Reify (List1 a) where
   reify defs val@(NDCon _ n _ _ [_, x, xs])
       = case !(full (gamma defs) n) of
-             NS _ (UN "::")
+             NS _ (UN ":::")
                   => do x' <- reify defs !(evalClosure defs x)
                         xs' <- reify defs !(evalClosure defs xs)
-                        pure (x' :: xs')
+                        pure (x' ::: xs')
              _ => cantReify val "List1"
   reify defs val = cantReify val "List1"
 
 export
 Reflect a => Reflect (List1 a) where
-  reflect fc defs lhs env (x :: xs)
+  reflect fc defs lhs env (x ::: xs)
       = do x' <- reflect fc defs lhs env x
            xs' <- reflect fc defs lhs env xs
-           appCon fc defs (NS (mkNamespace "Data.List1") (UN "::")) [Erased fc False, x', xs']
+           appCon fc defs (NS (mkNamespace "Data.List1") (UN ":::")) [Erased fc False, x', xs']
 
 export
 Reify a => Reify (Maybe a) where

src/Idris/Parser.idr

@@ -391,7 +391,7 @@ mutual
     <|> do b <- bounds (pragma "runElab" *> expr pdef fname indents)
            pure (PRunElab (boundToFC fname b) b.val)
     <|> do b <- bounds $ do pragma "logging"
-                            topic <- optional ((::) <$> unqualifiedName <*> many aDotIdent)
+                            topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
                             lvl   <- intLit
                             e     <- expr pdef fname indents
                             pure (MkPair (mkLogLevel' topic (integerToNat lvl)) e)
@@ -994,7 +994,7 @@ directive fname indents
 --          atEnd indents
 --          pure (Hide True n)
   <|> do pragma "logging"
-         topic <- optional ((::) <$> unqualifiedName <*> many aDotIdent)
+         topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
          lvl <- intLit
          atEnd indents
          pure (Logging (mkLogLevel' topic (fromInteger lvl)))
@@ -1816,7 +1816,7 @@ loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, p
   parse = do
     symbol ":"
     runParseCmd parseCmd
-    topic <- optional ((::) <$> unqualifiedName <*> many aDotIdent)
+    topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
     lvl <- intLit
     pure (command (mkLogLevel' topic (fromInteger lvl)))
 

src/Parser/Lexer/Source.idr

@@ -125,7 +125,7 @@ mutual
   ||| comment unless the series of uninterrupted dashes is ended with
   ||| a closing brace in which case it is a closing delimiter.
   doubleDash : (k : Nat) -> Lexer
-  doubleDash k = many (is '-') <+> choice {t = List} -- absorb all dashes
+  doubleDash k = many (is '-') <+> choice            -- absorb all dashes
     [ is '}' <+> toEndComment k                      -- closing delimiter
     , many (isNot '\n') <+> toEndComment (S k)       -- line comment
     ]

src/Utils/Binary.idr

@@ -351,14 +351,14 @@ TTC a => TTC (List a) where
 
 export
 TTC a => TTC (List1 a) where
-  toBuf b (x :: xs)
+  toBuf b (x ::: xs)
      = do toBuf b x
           toBuf b xs
 
   fromBuf b = do
     x <- fromBuf b
     xs <- fromBuf b
-    pure (x :: xs)
+    pure (x ::: xs)
 
 export
 {n : Nat} -> TTC a => TTC (Vect n a) where

tests/Main.idr

@@ -281,7 +281,7 @@ firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
 pathLookup : List String -> IO (Maybe String)
 pathLookup names = do
   path <- getEnv "PATH"
-  let pathList = List1.toList $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
+  let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
   let candidates = [p ++ "/" ++ x | p <- pathList,
                                     x <- names]
   firstExists candidates
@@ -327,7 +327,7 @@ main
               | _ => do print args
                         putStrLn usage
          let filteredNonCGTests =
-              filterTests opts $ concat $ the (List (List String))
+              filterTests opts $ concat $
                  [ testPaths "ttimp" ttimpTests
                  , testPaths "idris2" idrisTests
                  , testPaths "typedd-book" typeddTests

tests/chez/chez020/Popen.idr

@@ -25,6 +25,6 @@ main = do
         | Left err => printLn err
     pclose fh
     putStrLn "closed"
-    let [idris2, _] = split ((==) ',') output
+    let (idris2 ::: _) = split ((==) ',') output
         | _ => printLn "Unexpected result"
     putStrLn idris2