Merge pull request #31 from stefan-hoeck/style

[ style ] adhere to style guide

src/Control/RIO.idr

@@ -32,12 +32,14 @@ data Stack : (x1,x2,a,b : Type) -> Type where
 export
 eval : RIO x a -> IO (Either x a)
 eval app = fromPrim $ go app []
-  where go : RIO x1 v -> Stack x1 x2 v w -> PrimIO (Either x2 w)
-        go (Chain z f) st       w = go z (f :: st) w
-        go (Lift run) []        w = run w
-        go (Lift run) (f :: fs) w =
-          let MkIORes ei w2 = run w
-           in assert_total $ go (f ei) fs w2
+
+  where
+    go : RIO x1 v -> Stack x1 x2 v w -> PrimIO (Either x2 w)
+    go (Chain z f) st       w = go z (f :: st) w
+    go (Lift run) []        w = run w
+    go (Lift run) (f :: fs) w =
+      let MkIORes ei w2 = run w
+       in assert_total $ go (f ei) fs w2
 
 ||| Tail-recursively evaluate a `RIO` computation,
 ||| which cannot fail with an exception.

src/Control/RIO/App.idr

@@ -60,9 +60,11 @@ Handler a x = x -> RIO Void a
 ||| in the resulting `App` type.
 export
 handle : (prf : Has x xs) => Handler a x -> App xs a -> App (xs - x) a
-handle f = catch $ \u => case map f (decomp @{prf} u) of
-  Left y  => fail y
-  Right y => lift y
+handle f =
+  catch $ \u =>
+    case map f (decomp @{prf} u) of
+      Left y  => fail y
+      Right y => lift y
 
 hall : (prf : All (Handler a) ts) => HSum ts -> RIO Void a
 hall @{h :: t} (Here v)  = h v

src/Control/RIO/File.idr

@@ -156,11 +156,12 @@ chgDir dir = injectIO (changeDir_ %search t dir)
 ||| Runs an action in the given directory, changing back
 ||| to the current directory afterwards.
 export
-inDir :  FS
-      => Has FileErr xs
-      => (dir : Path t)
-      -> (act : App xs a)
-      -> App xs a
+inDir :
+     {auto _ : FS}
+  -> {auto _ : Has FileErr xs}
+  -> (dir : Path t)
+  -> (act : App xs a)
+  -> App xs a
 inDir dir act = do
   cur <- curDir
   finally (chgDir cur) (chgDir dir >> act)
@@ -179,9 +180,11 @@ mkDir dir = injectIO (mkDir_ %search t dir)
 export
 mkDirP : FS => Has FileErr xs => Path t -> App xs ()
 mkDirP dir = go (parentDirs dir) >> mkDir dir
-  where go : List (Path t) -> App xs ()
-        go []        = pure ()
-        go (x :: xs) = when !(missing x) $ go xs >> mkDir x
+
+  where
+    go : List (Path t) -> App xs ()
+    go []        = pure ()
+    go (x :: xs) = when !(missing x) $ go xs >> mkDir x
 
 ||| Creates the parent directory of the given file
 export %inline
@@ -238,15 +241,16 @@ mkDirImpl _ dir = mapFst (MkDir dir) <$> createDir "\{dir}"
 ||| A computer's local file system
 export
 local : FS
-local = MkFS {
-    write_      = writeImpl
-  , append_     = appendImpl
-  , removeFile_ = removeFileImpl
-  , removeDir_  = removeDirImpl
-  , exists_     = \_,fp => exists "\{fp}"
-  , read_       = readImpl
-  , curDir_     = curDirImpl
-  , changeDir_  = changeDirImpl
-  , listDir_    = listDirImpl
-  , mkDir_      = mkDirImpl
-  }
+local =
+  MkFS
+    { write_      = writeImpl
+    , append_     = appendImpl
+    , removeFile_ = removeFileImpl
+    , removeDir_  = removeDirImpl
+    , exists_     = \_,fp => exists "\{fp}"
+    , read_       = readImpl
+    , curDir_     = curDirImpl
+    , changeDir_  = changeDirImpl
+    , listDir_    = listDirImpl
+    , mkDir_      = mkDirImpl
+    }

src/Control/RIO/Logging.idr

@@ -135,7 +135,7 @@ syslogLogger : Facility -> ConsoleOut -> Logger
 syslogLogger f c =
   consoleLogger c $
     \l,s =>
-      let lvl = 8 * facility f + severity l
+      let lvl := 8 * facility f + severity l
        in "<\{show lvl}> \{s}"
 
 --------------------------------------------------------------------------------

src/Control/RIO/Mock/Console.idr

@@ -23,8 +23,9 @@ mkMockOut = [| MkMockOut (newIORef [<]) (newIORef [<]) |]
 export
 consoleOut : MockOut -> ConsoleOut
 consoleOut m =
-  MkConsoleOut (\s => modifyIORef m.stdOut (:< s))
-            (\s => modifyIORef m.errOut (:< s))
+  MkConsoleOut
+    (\s => modifyIORef m.stdOut (:< s))
+    (\s => modifyIORef m.errOut (:< s))
 
 ||| A mock console where err out and std out are mutable refs
 ||| of snoc lists and `getChar` and `getLine` are simulated
@@ -48,5 +49,6 @@ getHead ref = readIORef ref >>= \(h :: t) => writeIORef ref t $> h
 export
 console : MockIn -> ConsoleIn
 console m =
-  MkConsoleIn (getHead m.charIn)
-              (getHead m.lineIn)
+  MkConsoleIn
+    (getHead m.charIn)
+    (getHead m.lineIn)

src/Control/RIO/Mock/File.idr

@@ -28,11 +28,13 @@ unFocus (MkCtxt sp n ps) x = sp <>> ((n,x) :: ps)
 export
 focus : Eq k => k -> List (k,v) -> Maybe (Ctxt k v, v)
 focus key = go [<]
-  where go : SnocList (k,v) -> List (k,v) -> Maybe (Ctxt k v, v)
-        go sx []        = Nothing
-        go sx (x :: xs) = case fst x == key of
-          True  => Just (MkCtxt sx (fst x) xs, snd x)
-          False => go (sx :< x) xs
+
+  where
+    go : SnocList (k,v) -> List (k,v) -> Maybe (Ctxt k v, v)
+    go sx []        = Nothing
+    go sx (x :: xs) = case fst x == key of
+      True  => Just (MkCtxt sx (fst x) xs, snd x)
+      False => go (sx :< x) xs
 
 --------------------------------------------------------------------------------
 --          Mock FS
@@ -55,20 +57,23 @@ AFile = Either MockFile MockDir
 
 public export
 data Focus : Type where
-  FileF :  MockFile
-        -> Ctxt Body AFile
-        -> SnocList (Ctxt Body AFile)
-        -> Focus
-  DirF  :  MockDir
-        -> SnocList (Ctxt Body AFile)
-        -> Focus
+  FileF :
+       MockFile
+    -> Ctxt Body AFile
+    -> SnocList (Ctxt Body AFile)
+    -> Focus
+  DirF :
+       MockDir
+    -> SnocList (Ctxt Body AFile)
+    -> Focus
 
 public export
 data PCFocus : Type where
-  Parent :  (child     : Body)
-         -> (parendDir : MockDir)
-         -> (context   : SnocList (Ctxt Body AFile))
-         -> PCFocus
+  Parent :
+       (child     : Body)
+    -> (parendDir : MockDir)
+    -> (context   : SnocList (Ctxt Body AFile))
+    -> PCFocus
   Exists :  Focus -> PCFocus
 
 selfOrParent : Path t -> Path t
@@ -77,38 +82,45 @@ selfOrParent fp = maybe fp fst $ split fp
 export
 mkdirFocus : MockDir -> Path Abs -> Maybe Focus
 mkdirFocus (MkMD ps) (PAbs sx) = go [<] ps (sx <>> [])
-  where go :  SnocList (Ctxt Body AFile)
-           -> List (Body,AFile)
-           -> List Body
-           -> Maybe Focus
-        go sx ps []        = Just $ DirF (MkMD ps) sx
-        go sx ps (x :: xs) = case focus x ps of
-          Nothing          =>
-            let c = MkCtxt Lin x Nil
-             in go (sx :< c) [] xs
-          Just (c, Left f) => case xs of
-            Nil => Just $ FileF f c sx
-            _   => Nothing
-          Just (c, Right $ MkMD ps2) => go (sx :< c) ps2 xs
+
+  where
+    go :
+         SnocList (Ctxt Body AFile)
+      -> List (Body,AFile)
+      -> List Body
+      -> Maybe Focus
+    go sx ps []        = Just $ DirF (MkMD ps) sx
+    go sx ps (x :: xs) = case focus x ps of
+      Nothing          =>
+        let c := MkCtxt Lin x Nil
+         in go (sx :< c) [] xs
+      Just (c, Left f) => case xs of
+        Nil => Just $ FileF f c sx
+        _   => Nothing
+      Just (c, Right $ MkMD ps2) => go (sx :< c) ps2 xs
 
 export
 dirFocus : MockDir -> Path Abs -> Maybe Focus
 dirFocus (MkMD ps) (PAbs sx) = go [<] ps (sx <>> [])
-  where go :  SnocList (Ctxt Body AFile)
-           -> List (Body,AFile)
-           -> List Body
-           -> Maybe Focus
-        go sx ps []        = Just $ DirF (MkMD ps) sx
-        go sx ps (x :: xs) = case focus x ps of
-          Nothing          => Nothing
-          Just (c, Left f)           => case xs of
-            Nil => Just $ FileF f c sx
-            _   => Nothing
-          Just (c, Right $ MkMD ps2) => go (sx :< c) ps2 xs
-
-unDirFocus' :  List (Body, AFile)
-            -> SnocList (Ctxt Body AFile)
-            -> MockDir
+
+  where
+    go :
+         SnocList (Ctxt Body AFile)
+      -> List (Body,AFile)
+      -> List Body
+      -> Maybe Focus
+    go sx ps []        = Just $ DirF (MkMD ps) sx
+    go sx ps (x :: xs) = case focus x ps of
+      Nothing          => Nothing
+      Just (c, Left f) => case xs of
+        Nil => Just $ FileF f c sx
+        _   => Nothing
+      Just (c, Right $ MkMD ps2) => go (sx :< c) ps2 xs
+
+unDirFocus' :
+     List (Body, AFile)
+  -> SnocList (Ctxt Body AFile)
+  -> MockDir
 unDirFocus' xs [<]       = MkMD xs
 unDirFocus' xs (sx :< x) = unDirFocus' (unFocus x . Right $ MkMD xs) sx
 
@@ -162,10 +174,11 @@ mkDirP fp fs = case mkdirFocus fs.root (absPath fs fp) of
   Just (FileF {})  => Left (MkDir fp FileExists)
   Nothing => Left (MkDir fp FileExists)
 
-writeImpl :  File t
-          -> String
-          -> (String -> String)
-          -> MockFS -> Either FileErr MockFS
+writeImpl :
+     File t
+  -> String
+  -> (String -> String)
+  -> MockFS -> Either FileErr MockFS
 writeImpl fp s f fs = case pcFocus fs $ toPath fp of
   Just (Parent c d sx) =>
     let empty := (c, Left $ Regular s)
@@ -237,15 +250,16 @@ mock ref f = do
 ||| A mock file system
 export
 fs : IORef MockFS -> FS
-fs ref = MkFS {
-    write_      = \_,fp,s => mock ref (write fp s)
-  , append_     = \_,fp,s => mock ref (append fp s)
-  , removeFile_ = \_,fp => mock ref (removeFile fp)
-  , removeDir_  = \_,fp => mock ref (removeDir fp)
-  , exists_     = \_,fp => exists fp <$> readIORef ref
-  , read_       = \_,fp,l => read fp l <$> readIORef ref
-  , curDir_     = Right . curDir <$> readIORef ref
-  , changeDir_  = \_,fp => mock ref (changeDir fp)
-  , listDir_    = \_,fp => listDir fp <$> readIORef ref
-  , mkDir_      = \_,fp => mock ref (mkDir fp)
-  }
+fs ref =
+  MkFS
+    { write_      = \_,fp,s => mock ref (write fp s)
+    , append_     = \_,fp,s => mock ref (append fp s)
+    , removeFile_ = \_,fp => mock ref (removeFile fp)
+    , removeDir_  = \_,fp => mock ref (removeDir fp)
+    , exists_     = \_,fp => exists fp <$> readIORef ref
+    , read_       = \_,fp,l => read fp l <$> readIORef ref
+    , curDir_     = Right . curDir <$> readIORef ref
+    , changeDir_  = \_,fp => mock ref (changeDir fp)
+    , listDir_    = \_,fp => listDir fp <$> readIORef ref
+    , mkDir_      = \_,fp => mock ref (mkDir fp)
+    }

src/Control/RIO/State.idr

@@ -38,10 +38,11 @@ namespace Read
 public export
 data ST : (lbl : l) -> (a : Type) -> Type where
   [search lbl]
-  MkST :  (read_  : IO a)
-       -> (write_ : a -> IO ())
-       -> (mod_   : (a -> a) -> IO ())
-       -> ST lbl a
+  MkST :
+       (read_  : IO a)
+    -> (write_ : a -> IO ())
+    -> (mod_   : (a -> a) -> IO ())
+    -> ST lbl a
 
 export
 mkST : HasIO io => a -> io (ST lbl a)

test/src/FSProps.idr

@@ -74,11 +74,13 @@ relativeFile = MkF neutral <$> fileBody
 
 mockFS : Gen MockFS
 mockFS = toFS (MkMockFS (MkMD []) root) <$> list (linear 0 20) dir
-  where toFS : MockFS -> List FilePath -> MockFS
-        toFS fs []        = fs
-        toFS fs (FP p :: ps) = case mkDirP p fs of
-          Right fs2 => toFS fs2 ps
-          Left  _   => toFS fs ps
+
+  where
+    toFS : MockFS -> List FilePath -> MockFS
+    toFS fs []        = fs
+    toFS fs (FP p :: ps) = case mkDirP p fs of
+      Right fs2 => toFS fs2 ps
+      Left  _   => toFS fs ps
 
 anyString : Gen String
 anyString = string (linear 0 20) unicode
@@ -103,7 +105,9 @@ prop_readWrite = property $ do
 
 export
 props : Group
-props = MkGroup "MockFS" [
-        ("prop_rootExists", prop_rootExists)
-      , ("prop_readWrite", prop_readWrite)
-      ]
+props =
+  MkGroup
+    "MockFS"
+    [ ("prop_rootExists", prop_rootExists)
+    , ("prop_readWrite", prop_readWrite)
+    ]