From 252b31579eb4b148666e91888ad21400af19c747 Mon Sep 17 00:00:00 2001
From: Alexander Carter <alrunner4@gmail.com>
Date: Thu, 9 Jan 2020 16:36:27 -0800
Subject: [PATCH 1/2] typo on showing builtin arity

---
 src/Core/Context.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 9c2b5cfa2..937d3d801 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -77,7 +77,7 @@ Show Def where
   show (ExternDef arity) = "<external def with arity " ++ show arity ++ ">"
   show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++
                            " " ++ show cs ++">"
-  show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"
+  show (Builtin {arity} _) = "<builtin with arity " ++ show arity ++ ">"
   show (Hole _ p) = "Hole" ++ if p then " [impl]" else ""
   show (BySearch c depth def) = "Search in " ++ show def
   show (Guess tm _ cs) = "Guess " ++ show tm ++ " when " ++ show cs

From 6a1ddb84b68dd28e5031587bd05b92fe9c7492d6 Mon Sep 17 00:00:00 2001
From: Alexander Carter <alrunner4@gmail.com>
Date: Wed, 15 Jan 2020 13:21:58 -0800
Subject: [PATCH 2/2] define MonadError in base

---
 libs/base/Control/Monad/Error.idr       | 49 +++++++++++++++++++++++++
 libs/base/Control/Monad/Error/IORef.idr | 11 ++++++
 libs/base/base.ipkg                     |  2 +
 libs/prelude/Prelude.idr                | 10 +++++
 4 files changed, 72 insertions(+)
 create mode 100644 libs/base/Control/Monad/Error.idr
 create mode 100644 libs/base/Control/Monad/Error/IORef.idr

diff --git a/libs/base/Control/Monad/Error.idr b/libs/base/Control/Monad/Error.idr
new file mode 100644
index 000000000..9de966b47
--- /dev/null
+++ b/libs/base/Control/Monad/Error.idr
@@ -0,0 +1,49 @@
+module Control.Monad.Error
+import Control.Monad.Trans
+
+public export
+interface Monad m => MonadError e m where
+    throw : e -> m a
+    catch : m a -> ( e -> m a ) -> m a
+
+public export
+data ErrorT : Type -> ( Type -> Type ) -> Type -> Type where
+    RunErrorT : m ( Either e a ) -> ErrorT e m a
+
+public export
+IOError : Type -> Type -> Type
+IOError e a = ErrorT e IO a
+
+public export
+Functor m => Functor( ErrorT e m ) where
+    map f ( RunErrorT op ) = RunErrorT( map ( map f ) op )
+
+public export
+Monad m => Applicative( ErrorT e m ) where
+    pure x = RunErrorT( pure ( Right x ) )
+    RunErrorT f <*> RunErrorT op = RunErrorT $
+        op >>= \ e_val => map ( <*> e_val ) f
+
+public export
+Monad m => Monad( ErrorT e m ) where
+    RunErrorT op >>= f = RunErrorT $ op >>= \ e_val =>
+        case e_val of
+            Left  err => pure( Left err )
+            Right val => let RunErrorT op = f val in op
+
+public export
+Monad m => MonadError e ( ErrorT e m ) where
+    throw = RunErrorT . pure . Left
+    catch( RunErrorT op ) handler = RunErrorT $ op >>= \ e_val => case e_val of
+        Left  err => let RunErrorT op' = handler err in op'
+        Right val => pure( Right val )
+
+public export
+MonadTrans( ErrorT e ) where
+--  lift : Monad m => m a -> ErrorT e m a
+    lift op = RunErrorT( map Right op )
+
+throwIf : MonadError e m => Bool -> Lazy e -> m ()
+throwIf test err = if test
+    then throw err
+    else pure ()
diff --git a/libs/base/Control/Monad/Error/IORef.idr b/libs/base/Control/Monad/Error/IORef.idr
new file mode 100644
index 000000000..dd4aed974
--- /dev/null
+++ b/libs/base/Control/Monad/Error/IORef.idr
@@ -0,0 +1,11 @@
+module Control.Monad.Error.IORef
+import Control.Monad.Error
+import Data.IORef
+
+public export
+overIORef : IORef a -> ( a -> IOError e a ) -> IOError e a
+overIORef ref xform = do
+    val <- lift( readIORef ref )
+    newval <- xform val
+    lift( writeIORef ref newval )
+    pure newval
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index c54b0d66b..d2a0893fa 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -3,6 +3,8 @@ package base
 modules = Control.Monad.Identity,
           Control.Monad.State,
           Control.Monad.Trans,
+		  Control.Monad.Error,
+		  Control.Monad.Error.IORef,
           Control.WellFounded,
 
           Data.Buffer,
diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr
index 3b7d45b63..6e33e3d3c 100644
--- a/libs/prelude/Prelude.idr
+++ b/libs/prelude/Prelude.idr
@@ -736,6 +736,16 @@ Monad (Either e) where
     (Left n) >>= _ = Left n
     (Right r) >>= f = f r
 
+public export
+Foldable (Either e) where
+	foldr _ z ( Left  _ ) = z
+	foldr f z ( Right x ) = f x z
+
+public export
+Traversable (Either e) where
+	traverse _ ( Left  e ) = pure( Left e )
+	traverse f ( Right x ) = map Right ( f x )
+
 -----------
 -- LISTS --
 -----------