Merge pull request #156 from clayrat/misc-fixes

Misc fixes and additions

libs/base/Data/List.idr

@@ -194,6 +194,16 @@ tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
 tail [] impossible
 tail (x :: xs) = xs
 
+||| Attempt to get the head of a list. If the list is empty, return `Nothing`.
+head' : List a -> Maybe a
+head' []      = Nothing
+head' (x::xs) = Just x
+
+||| Attempt to get the tail of a list. If the list is empty, return `Nothing`.
+tail' : List a -> Maybe (List a)
+tail' []      = Nothing
+tail' (x::xs) = Just xs
+
 ||| Convert any Foldable structure to a list.
 export
 toList : Foldable t => t a -> List a

libs/base/Data/Strings.idr

@@ -2,6 +2,10 @@ module Data.Strings
 
 import Data.List
 
+export
+singleton : Char -> String
+singleton c = strCons c ""
+
 partial
 foldr1 : (a -> a -> a) -> List a -> a
 foldr1 _ [x] = x

libs/prelude/Prelude.idr

@@ -435,7 +435,7 @@ shiftR : Int -> Int -> Int
 shiftR = prim__shr_Int
 
 ---------------------------------
--- FUNCTOR, APPLICATIVE, MONAD --
+-- FUNCTOR, APPLICATIVE, ALTERNATIVE, MONAD --
 ---------------------------------
 
 public export
@@ -446,6 +446,10 @@ public export
 (<$>) : Functor f => (func : a -> b) -> f a -> f b
 (<$>) func x = map func x
 
+public export
+ignore : Functor f => f a -> f ()
+ignore = map (const ())
+
 public export
 interface Functor f => Applicative f where
   pure : a -> f a
@@ -465,8 +469,8 @@ a *> b = map (const id) a <*> b
 
 public export
 interface Applicative f => Alternative f where
-    empty : f a
-    (<|>) : f a -> f a -> f a
+  empty : f a
+  (<|>) : f a -> f a -> f a
 
 public export
 interface Applicative m => Monad m where
@@ -544,6 +548,35 @@ public export
 for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
 for_ = flip traverse_
 
+||| Fold using Alternative
+|||
+||| If you have a left-biased alternative operator `<|>`, then `choice`
+||| performs left-biased choice from a list of alternatives, which means that
+||| it evaluates to the left-most non-`empty` alternative.
+|||
+||| If the list is empty, or all values in it are `empty`, then it
+||| evaluates to `empty`.
+|||
+||| Example:
+|||
+||| ```
+||| -- given a parser expression like:
+||| expr = literal <|> keyword <|> funcall
+|||
+||| -- choice lets you write this as:
+||| expr = choice [literal, keyword, funcall]
+||| ```
+|||
+||| Note: In Haskell, `choice` is called `asum`.
+public export
+choice : (Foldable t, Alternative f) => t (f a) -> f a
+choice = foldr (<|>) empty
+
+||| A fused version of `choice` and `map`.
+public export
+choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b
+choiceMap f = foldr (\e, a => f e <|> a) empty
+
 public export
 interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
   ||| Map each element of a structure to a computation, evaluate those
@@ -618,6 +651,18 @@ natToInteger : Nat -> Integer
 natToInteger Z = 0
 natToInteger (S k) = 1 + natToInteger k
 
+-----------
+-- PAIRS --
+-----------
+
+public export
+Functor (Pair a) where
+  map f (x, y) = (x, f y)
+
+public export
+mapFst : (a -> c) -> (a, b) -> (c, b)
+mapFst f (x, y) = (f x, y)
+
 -----------
 -- MAYBE --
 -----------

src/Core/FC.idr

@@ -11,6 +11,7 @@ public export
 FileName : Type
 FileName = String
 
+||| A file context is a filename together with starting and ending positions
 public export
 data FC = MkFC FileName FilePos FilePos
         | EmptyFC

src/Idris/CommandLine.idr

@@ -101,7 +101,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
               (Just "Run the REPL with machine-readable syntax"),
 
            MkOpt ["--ide-mode-socket"] [] [IdeModeSocket "localhost:38398"]
-              (Just "Run the ide socket mode on default host and port (localhost:38398"),
+              (Just "Run the ide socket mode on default host and port (localhost:38398)"),
 
            MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp])
               (Just "Run the ide socket mode on given host and port"),

src/Idris/IDEMode/REPL.idr

@@ -32,6 +32,8 @@ import TTImp.Elab
 import TTImp.TTImp
 import TTImp.ProcessDecls
 
+import Utils.Hex
+
 import Control.Catchable
 import System
 import Idris.Socket
@@ -100,38 +102,12 @@ getNChars i (S k)
          xs <- getNChars i k
          pure (x :: xs)
 
-hex : Char -> Maybe Int
-hex '0' = Just 0
-hex '1' = Just 1
-hex '2' = Just 2
-hex '3' = Just 3
-hex '4' = Just 4
-hex '5' = Just 5
-hex '6' = Just 6
-hex '7' = Just 7
-hex '8' = Just 8
-hex '9' = Just 9
-hex 'a' = Just 10
-hex 'b' = Just 11
-hex 'c' = Just 12
-hex 'd' = Just 13
-hex 'e' = Just 14
-hex 'f' = Just 15
-hex _ = Nothing
-
-export
-toHex : Int -> List Char -> Maybe Int
-toHex _ [] = Just 0
-toHex m (d :: ds)
-    = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds)
-
-
 -- Read 6 characters. If they're a hex number, read that many characters.
 -- Otherwise, just read to newline
 getInput : File -> IO String
 getInput f
     = do x <- getNChars f 6
-         case toHex 1 (reverse x) of
+         case fromHexChars (reverse x) of
               Nothing =>
                 do rest <- getFLine f
                    pure (pack x ++ rest)

src/Idris/Package.idr

@@ -67,6 +67,7 @@ Show PkgDesc where
              maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
              maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
              maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
+             maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
              maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
              maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
              maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg)

src/Utils/Hex.idr

@@ -31,3 +31,34 @@ asHex n = pack $ asHex' n []
     asHex' n hex with (n `divides` 16)
       asHex' (16 * div + rem) hex | DivBy {div} {rem} _ = asHex' div (hexDigit rem :: hex)
 
+export
+fromHexDigit : Char -> Maybe Int
+fromHexDigit '0' = Just 0
+fromHexDigit '1' = Just 1
+fromHexDigit '2' = Just 2
+fromHexDigit '3' = Just 3
+fromHexDigit '4' = Just 4
+fromHexDigit '5' = Just 5
+fromHexDigit '6' = Just 6
+fromHexDigit '7' = Just 7
+fromHexDigit '8' = Just 8
+fromHexDigit '9' = Just 9
+fromHexDigit 'a' = Just 10
+fromHexDigit 'b' = Just 11
+fromHexDigit 'c' = Just 12
+fromHexDigit 'd' = Just 13
+fromHexDigit 'e' = Just 14
+fromHexDigit 'f' = Just 15
+fromHexDigit _ = Nothing
+
+export
+fromHexChars : List Char -> Maybe Int
+fromHexChars = fromHexChars' 1
+  where
+    fromHexChars' : Int -> List Char -> Maybe Int
+    fromHexChars' _ [] = Just 0
+    fromHexChars' m (d :: ds) = pure $ !(fromHexDigit (toLower d)) * m + !(fromHexChars' (m*16) ds)
+
+export
+fromHex : String -> Maybe Int
+fromHex = fromHexChars . unpack

tests/idris2/total006/expected

@@ -1,6 +1,6 @@
 1/1: Building Total (Total.idr)
 Main> Main.count is total
-Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:824:1--828:1 -> Prelude.map
+Main> Main.badCount is not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:869:1--873:1 -> Prelude.map
 Main> Main.process is total
 Main> Main.badProcess is not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
 Main> Main.doubleInt is total