Git.idr

module Libgit.Git

import Control.Monad.Reader

||| An abstract token representing the initialized libgit2 state. Its
||| constructor is purposefully not exported, a context can only be created
||| via `runGitT`.
export
data GitContext : (i : Type) -> Type where
  MkGitContext : GitContext i

public export
data GitT : (i : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
  MkGitT : ReaderT (GitContext i) m a -> GitT i m a

unGitT : GitT i m a -> ReaderT (GitContext i) m a
unGitT (MkGitT x) = x

public export
implementation Functor m => Functor (GitT i m) where
  map f (MkGitT x) = MkGitT (f <$> x)

public export
implementation Applicative m => Applicative (GitT i m) where
  pure x = MkGitT (pure x)

  MkGitT f <*> MkGitT x = MkGitT (f <*> x)

public export
implementation Monad m => Monad (GitT i m) where
  MkGitT x >>= f = MkGitT $ x >>= unGitT . f

public export
implementation HasIO m => HasIO (GitT i m) where
  liftIO action = MkGitT $ liftIO action

Reader.idr

module Control.Monad.Reader

public export
record ReaderT (stateType : Type) (m: Type -> Type) (a: Type) where
  constructor MkReaderT
  runReaderT : stateType -> m a

public export
implementation Functor f => Functor (ReaderT stateType f) where
  map f (MkReaderT g) = MkReaderT (\st => map f (g st))

public export
implementation Applicative f => Applicative (ReaderT stateType f) where
  pure x = MkReaderT (\st => pure x)

  (MkReaderT f) <*> (MkReaderT a) =
    MkReaderT (\st =>
      let f' = f st in
      let a' = a st in
      f' <*> a')

public export
implementation Monad m => Monad (ReaderT stateType m) where
  (MkReaderT f) >>= k =
    MkReaderT (\st => do v <- f st
                         let MkReaderT kv = k v
                         kv st)

public export
implementation HasIO m => HasIO (ReaderT stateType m) where
  liftIO f = MkReaderT (\_ => liftIO f)

3/5: Building Libgit.Git (src/Libgit/Git.idr)
src/Libgit/Git.idr:67:35--67:41:While processing right hand side of liftIO at src/Libgit/Git.idr:67:3--69:1:
Trying to use linear name action in non-linear context at:
67        liftIO action = MkGitT $ liftIO action