From 626245e629546aa3c740cd1cb86643db5342b406 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 02:24:14 -0500 Subject: [PATCH] Add slurp utility function --- src/SSG/Djot/Lines.idr | 44 ++++++++++++++++++++++++++++++------------ 1 file changed, 32 insertions(+), 12 deletions(-) diff --git a/src/SSG/Djot/Lines.idr b/src/SSG/Djot/Lines.idr index f8fa26d..4bd9483 100644 --- a/src/SSG/Djot/Lines.idr +++ b/src/SSG/Djot/Lines.idr @@ -8,9 +8,9 @@ import Control.Eff -- Only for iutils unit tests import System ---********************* ---* Effect Definition * ---********************* +--************************ +--* Effect Definition * +--************************ export data Lines : Type -> Type where @@ -19,9 +19,9 @@ data Lines : Type -> Type where ||| Take the next line Take : Lines (Maybe String) ---********************* ---* Effect Actions * ---********************* +--************************ +--* Effect Actions * +--************************ export peek : Has Lines fs => Eff fs (Maybe String) @@ -31,9 +31,29 @@ export take : Has Lines fs => Eff fs (Maybe String) take = send Take ---********************* ---* Effect Handlers * ---********************* +--************************ +--* Extra Effect Actions * +--************************ + +||| Take lines until a line matching the given predicate is encountered, dropping the +||| matching line +export +slurp : Has Lines fs => (predicate : String -> Bool) -> Eff fs (List String) +slurp predicate = do + Just line <- peek + | _ => pure [] + if predicate line + then do + _ <- take + pure [] + else do + Just x <- take + | _ => pure [] + map (x ::) (slurp predicate) + +--************************ +--* Effect Handlers * +--************************ ||| Split the next line from a string nextLine : String -> Maybe (String, String) @@ -79,9 +99,9 @@ runLines input = let (vv, input3) = unLines input2 lns in f input3 vv ---********************* ---* Unit Tests * ---********************* +--************************ +--* Unit Tests * +--************************ -- @@test runLines Smoke Test runLinesSmoke : IO Bool