From b3320e9e5fa44b9a86a225660653330eed81b17a Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 9 Dec 2024 16:40:07 +0300 Subject: [PATCH] [ cleanup ] Small cleanup `Core` code --- src/Compiler/RefC/RefC.idr | 16 ++++----- src/Core/Context.idr | 7 ++-- src/Core/Core.idr | 69 +++++++++++++------------------------- src/Idris/Driver.idr | 6 ++-- src/Idris/Package.idr | 8 ++--- 5 files changed, 38 insertions(+), 68 deletions(-) diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 9a3369e557..04be10007b 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -593,11 +593,9 @@ mutual decreaseIndentation pure "} else ") "" alts - case mDef of - Nothing => pure () - Just body => do - emit emptyFC "} else {" - concaseBody env switchReturnVar "" [] body tailPosition + whenJust mDef $ \body => do + emit emptyFC "} else {" + concaseBody env switchReturnVar "" [] body tailPosition emit emptyFC "}" pure switchReturnVar @@ -626,11 +624,9 @@ mutual pure "} else ") "" alts pure () - case def of - Nothing => pure () - Just body => do - emit emptyFC "} else {" - concaseBody env switchReturnVar "" [] body tailPosition + whenJust def $ \body => do + emit emptyFC "} else {" + concaseBody env switchReturnVar "" [] body tailPosition emit emptyFC "}" pure switchReturnVar diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 5c2ff1e0f5..b569c99cb1 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -1385,10 +1385,9 @@ updateDef n fdef = do defs <- get Ctxt Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => pure () - case fdef (definition gdef) of - Nothing => pure () - Just def' => ignore $ addDef n ({ definition := def', - schemeExpr := Nothing } gdef) + whenJust (fdef $ definition gdef) $ \def' => + ignore $ addDef n $ { definition := def', + schemeExpr := Nothing } gdef export updateTy : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/Core.idr b/src/Core/Core.idr index ade5f7363a..48c8a61b4b 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -670,14 +670,12 @@ record Core t where runCore : IO (Either Error t) export -coreRun : Core a -> - (Error -> IO b) -> (a -> IO b) -> IO b -coreRun (MkCore act) err ok - = either err ok !act +coreRun : Core a -> (Error -> IO b) -> (a -> IO b) -> IO b +coreRun (MkCore act) err ok = either err ok !act export coreFail : Error -> Core a -coreFail e = MkCore (pure (Left e)) +coreFail = MkCore . pure . Left export wrapError : (Error -> Error) -> Core a -> Core a @@ -687,8 +685,7 @@ wrapError fe (MkCore prog) = MkCore $ mapFst fe <$> prog export %inline coreLift : IO a -> Core a -coreLift op = MkCore (do op' <- op - pure (Right op')) +coreLift = MkCore . map Right {- Monad, Applicative, Traversable are specialised by hand for Core. In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn't @@ -702,11 +699,11 @@ in the next version (i.e., in this project...)! -} -- Functor (specialised) export %inline map : (a -> b) -> Core a -> Core b -map f (MkCore a) = MkCore (map (map f) a) +map f (MkCore a) = MkCore $ map (map f) a export %inline (<$>) : (a -> b) -> Core a -> Core b -(<$>) f (MkCore a) = MkCore (map (map f) a) +(<$>) = map export %inline (<$) : b -> Core a -> Core b @@ -718,7 +715,7 @@ export %inline export %inline ignore : Core a -> Core () -ignore = map (const ()) +ignore = map $ const () -- This would be better if we restrict it to a limited set of IO operations export @@ -729,11 +726,9 @@ coreLift_ op = ignore (coreLift op) -- Monad (specialised) export %inline (>>=) : Core a -> (a -> Core b) -> Core b -(>>=) (MkCore act) f - = MkCore (act >>= - \case - Left err => pure $ Left err - Right val => runCore $ f val) +MkCore act >>= f = MkCore $ act >>= \case + Left err => pure $ Left err + Right val => runCore $ f val export %inline (>>) : Core () -> Core a -> Core a @@ -757,26 +752,25 @@ export %inline -- Applicative (specialised) export %inline pure : a -> Core a -pure x = MkCore (pure (pure x)) +pure = MkCore . pure . Right export (<*>) : Core (a -> b) -> Core a -> Core b -(<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |] +MkCore f <*> MkCore a = MkCore [| f <*> a |] export (*>) : Core a -> Core b -> Core b -(*>) (MkCore a) (MkCore b) = MkCore [| a *> b |] +MkCore a *> MkCore b = MkCore [| a *> b |] export (<*) : Core a -> Core b -> Core a -(<*) (MkCore a) (MkCore b) = MkCore [| a <* b |] +MkCore a <* MkCore b = MkCore [| a <* b |] export %inline when : Bool -> Lazy (Core ()) -> Core () when True f = f when False f = pure () - export %inline unless : Bool -> Lazy (Core ()) -> Core () unless = when . not @@ -811,11 +805,9 @@ interface Catchable m t | m where export Catchable Core Error where - catch (MkCore prog) h - = MkCore ( do p' <- prog - case p' of - Left e => let MkCore he = h e in he - Right val => pure (Right val)) + catch (MkCore prog) h = MkCore $ prog >>= \case + Left e => runCore (h e) + Right val => pure (Right val) breakpoint (MkCore prog) = MkCore (pure <$> prog) throw = coreFail @@ -827,8 +819,7 @@ foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0) -- Traversable (specialised) traverse' : (a -> Core b) -> List a -> List b -> Core (List b) traverse' f [] acc = pure (reverse acc) -traverse' f (x :: xs) acc - = traverse' f xs (!(f x) :: acc) +traverse' f (x :: xs) acc = traverse' f xs (!(f x) :: acc) %inline export @@ -851,15 +842,12 @@ for = flip traverse export traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b) -traverseList1 f xxs - = let x = head xxs - xs = tail xxs in - [| f x ::: traverse f xs |] +traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |] export traverseSnocList : (a -> Core b) -> SnocList a -> Core (SnocList b) traverseSnocList f [<] = pure [<] -traverseSnocList f (as :< a) = (:<) <$> traverseSnocList f as <*> f a +traverseSnocList f (as :< a) = [| traverseSnocList f as :< f a |] export traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b) @@ -879,9 +867,8 @@ traversePair f (w, a) = (w,) <$> f a export traverse_ : (a -> Core b) -> List a -> Core () traverse_ f [] = pure () -traverse_ f (x :: xs) - = Core.do ignore (f x) - traverse_ f xs +traverse_ f (x :: xs) = ignore (f x) >> traverse_ f xs + %inline export for_ : List a -> (a -> Core ()) -> Core () @@ -890,20 +877,12 @@ for_ = flip traverse_ %inline export sequence : List (Core a) -> Core (List a) -sequence (x :: xs) - = do - x' <- x - xs' <- sequence xs - pure (x' :: xs') +sequence (x :: xs) = [| x :: sequence xs |] sequence [] = pure [] export traverseList1_ : (a -> Core b) -> List1 a -> Core () -traverseList1_ f xxs - = do let x = head xxs - let xs = tail xxs - ignore (f x) - traverse_ f xs +traverseList1_ f (x ::: xs) = ignore (f x) >> traverse_ f xs %inline export traverseFC : (a -> Core b) -> WithFC a -> Core (WithFC b) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 7bfe9acc31..fb9a152afb 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -97,8 +97,7 @@ updateREPLOpts tryYaffle : List CLOpt -> Core Bool tryYaffle [] = pure False -tryYaffle (Yaffle f :: _) = do yaffleMain f [] - pure True +tryYaffle (Yaffle f :: _) = yaffleMain f [] $> True tryYaffle (c :: cs) = tryYaffle cs ignoreMissingIpkg : List CLOpt -> Bool @@ -108,8 +107,7 @@ ignoreMissingIpkg (c :: cs) = ignoreMissingIpkg cs tryTTM : List CLOpt -> Core Bool tryTTM [] = pure False -tryTTM (Metadata f :: _) = do dumpTTM f - pure True +tryTTM (Metadata f :: _) = dumpTTM f $> True tryTTM (c :: cs) = tryTTM cs diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index b04033b0a7..019c7cf219 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -889,11 +889,9 @@ runRepl fname = do pure (PhysicalIdrSrc modIdent) ) fname m <- newRef MD (initMetadata origin) - case fname of - Nothing => pure () - Just fn => do - errs <- loadMainFile fn - displayErrors errs + whenJust fname $ \fn => do + errs <- loadMainFile fn + displayErrors errs repl {u} {s} ||| If the user did not provide a package file we can look in the working