From 4d3b42747c618aa80e6f7e83b81a0f8e93d985ee Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Mon, 15 Jul 2019 14:36:54 +0300 Subject: [PATCH 1/2] add --clean option for ipkg --- idris2.ipkg | 2 + src/Core/Core.idr | 5 +++ src/Data/StringMap.idr | 4 ++ src/Data/StringTrie.idr | 55 +++++++++++++++++++++++++ src/Data/These.idr | 35 ++++++++++++++++ src/Idris/CommandLine.idr | 10 +++-- src/Idris/Package.idr | 85 ++++++++++++++++++++++++++++++++++++--- 7 files changed, 187 insertions(+), 9 deletions(-) create mode 100644 src/Data/StringTrie.idr create mode 100644 src/Data/These.idr diff --git a/idris2.ipkg b/idris2.ipkg index e9c42ac..baf8bcc 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -42,6 +42,8 @@ modules = Data.IOArray, Data.NameMap, Data.StringMap, + Data.These, + Data.StringTrie, Idris.CommandLine, Idris.Desugar, diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 72b5852..48d2bd7 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -348,6 +348,11 @@ Of course it would be a good idea to fix this in Idris, but it's not an urgent thing on the road to self hosting, and we can make sure this isn't a problem 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) + -- Monad (specialised) export %inline (>>=) : Core a -> (a -> Core b) -> Core b diff --git a/src/Data/StringMap.idr b/src/Data/StringMap.idr index f888e56..8dbacd7 100644 --- a/src/Data/StringMap.idr +++ b/src/Data/StringMap.idr @@ -208,6 +208,10 @@ export empty : StringMap v empty = Empty +export +singleton : String -> v -> StringMap v +singleton k v = M Z (Leaf k v) + export lookup : String -> StringMap v -> Maybe v lookup _ Empty = Nothing diff --git a/src/Data/StringTrie.idr b/src/Data/StringTrie.idr new file mode 100644 index 0000000..0d2cfbc --- /dev/null +++ b/src/Data/StringTrie.idr @@ -0,0 +1,55 @@ +module Data.StringTrie + +import Data.These +import Data.StringMap + +%access public export +%default total + +-- prefix tree specialised to use `String`s as keys + +record StringTrie a where + constructor MkStringTrie + node : These a (StringMap (StringTrie a)) + +Functor StringTrie where + map f (MkStringTrie node) = MkStringTrie $ assert_total $ bimap f (map (map f)) node + +empty : StringTrie a +empty = MkStringTrie $ That empty + +singleton : List String -> a -> StringTrie a +singleton [] v = MkStringTrie $ This v +singleton (k::ks) v = MkStringTrie $ That $ singleton k (singleton ks v) + +-- insert using supplied function to resolve clashes +insertWith : List String -> (Maybe a -> a) -> StringTrie a -> StringTrie a +insertWith [] f (MkStringTrie nd) = + MkStringTrie $ these (This . f . Just) (Both (f Nothing)) (Both . f . Just) nd +insertWith (k::ks) f (MkStringTrie nd) = + MkStringTrie $ these (\x => Both x (singleton k end)) (That . rec) (\x => Both x . rec) nd + where + end : StringTrie a + end = singleton ks (f Nothing) + rec : StringMap (StringTrie a) -> StringMap (StringTrie a) + rec sm = maybe (insert k end sm) (\tm => insert k (insertWith ks f tm) sm) (lookup k sm) + +insert : List String -> a -> StringTrie a -> StringTrie a +insert ks v = insertWith ks (const v) + +-- fold the trie in a depth-first fashion performing monadic actions on values, then keys +foldWithKeysM : (Monad m, Monoid b) => (List String -> m b) -> (List String -> a -> m b) -> StringTrie a -> m b +foldWithKeysM {a} {m} {b} fk fv = go [] + where + go : List String -> StringTrie a -> m b + go as (MkStringTrie nd) = + bifold <$> bitraverse + (fv as) + (\sm => foldlM + (\x, (k, vs) => do let as' = as ++ [k] + y <- assert_total $ go as' vs + z <- fk as' + pure $ x <+> y <+> z) + neutral + (toList sm)) + nd diff --git a/src/Data/These.idr b/src/Data/These.idr new file mode 100644 index 0000000..2f1ff6c --- /dev/null +++ b/src/Data/These.idr @@ -0,0 +1,35 @@ +module Data.These + +%access public export +%default total + +data These a b = This a | That b | Both a b + +fromEither : Either a b -> These a b +fromEither = either This That + +these : (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c +these l r lr (This a) = l a +these l r lr (That b) = r b +these l r lr (Both a b) = lr a b + +bimap : (f : a -> b) -> (g : c -> d) -> These a c -> These b d +bimap f g (This a) = This (f a) +bimap f g (That b) = That (g b) +bimap f g (Both a b) = Both (f a) (g b) + +Functor (These a) where + map = bimap id + +mapFst : (f : a -> b) -> These a c -> These b c +mapFst f = bimap f id + +bifold : Monoid m => These m m -> m +bifold (This a) = a +bifold (That b) = b +bifold (Both a b) = a <+> b + +bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> These a b -> f (These c d) +bitraverse f g (This a) = [| This (f a) |] +bitraverse f g (That b) = [| That (g b) |] +bitraverse f g (Both a b) = [| Both (f a) (g b) |] diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 168bc4a..5a3c883 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -6,6 +6,7 @@ public export data PkgCommand = Build | Install + | Clean | REPL @@ -13,6 +14,7 @@ export Show PkgCommand where show Build = "--build" show Install = "--install" + show Clean = "--clean" show REPL = "--repl" ||| CLOpt - possible command line options @@ -29,17 +31,17 @@ data CLOpt NoPrelude | ||| Show the installation prefix ShowPrefix | - ||| Display blodwen version + ||| Display Idris version Version | ||| Display help text Help | - ||| Run Blodwen in quiet mode + ||| Run Idris 2 in quiet mode Quiet | ||| Add a package as a dependency PkgPath String | ||| Build or install a given package, depending on PkgCommand Package PkgCommand String | - ||| The input Blodwen file + ||| The input Idris file InputFile String | ||| Whether or not to run in IdeMode (easily parsable for other tools) IdeMode | @@ -88,6 +90,8 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] (Just "Build modules/executable for the given package"), MkOpt ["--install"] ["package file"] (\f => [Package Install f]) (Just "Install the given package"), + MkOpt ["--clean"] ["package file"] (\f => [Package Clean f]) + (Just "Clean intermediate files/executables for the given package"), MkOpt ["--quiet", "-q"] [] [Quiet] (Just "Quiet mode; display fewer messages"), diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index e7243a9..a69f937 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -6,6 +6,10 @@ import Core.Directory import Core.Options import Core.Unify +import Data.These +import Data.StringMap +import Data.StringTrie + import Idris.CommandLine import Idris.ModTree import Idris.ProcessIdr @@ -192,9 +196,7 @@ installFrom : {auto c : Ref Ctxt Defs} -> String -> String -> String -> List String -> Core () installFrom _ _ _ [] = pure () installFrom pname builddir destdir ns@(m :: dns) - = do defs <- get Ctxt - let modname = showSep "." (reverse ns) - let ttcfile = showSep "/" (reverse ns) + = do let ttcfile = showSep "/" (reverse ns) let ttcPath = builddir ++ dirSep ++ ttcfile ++ ".ttc" let destPath = destdir ++ dirSep ++ showSep "/" (reverse dns) let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc" @@ -233,9 +235,80 @@ install pkg traverse (installFrom (name pkg) (srcdir ++ dirSep ++ build) (installPrefix ++ dirSep ++ name pkg)) toInstall - coreLift $ changeDir srcdir + coreLift $ changeDir srcdir runScript (postinstall pkg) +-- Data.These.bitraverse hand specialised for Core +bitraverseC : (a -> Core c) -> (b -> Core d) -> These a b -> Core (These c d) +bitraverseC f g (This a) = [| This (f a) |] +bitraverseC f g (That b) = [| That (g b) |] +bitraverseC f g (Both a b) = [| Both (f a) (g b) |] + +-- Prelude.Monad.foldlM hand specialised for Core +foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a +foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0) + +-- Data.StringTrie.foldWithKeysM hand specialised for Core +foldWithKeysC : Monoid b => (List String -> Core b) -> (List String -> a -> Core b) -> StringTrie a -> Core b +foldWithKeysC {a} {b} fk fv = go [] + where + go : List String -> StringTrie a -> Core b + go as (MkStringTrie nd) = + map bifold $ bitraverseC + (fv as) + (\sm => foldlC + (\x, (k, vs) => + do let as' = as ++ [k] + y <- assert_total $ go as' vs + z <- fk as' + pure $ x <+> y <+> z) + neutral + (toList sm)) + nd + +Semigroup () where + (<+>) _ _ = () + +Monoid () where + neutral = () + +clean : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + PkgDesc -> Core () +clean pkg + = do defs <- get Ctxt + let build = build_dir (dirs (options defs)) + let toClean = mapMaybe (\ks => [| MkPair (tail' ks) (head' ks) |]) $ + maybe (map fst (modules pkg)) + (\m => fst m :: map fst (modules pkg)) + (mainmod pkg) + srcdir <- coreLift currentDir + let builddir = srcdir ++ dirSep ++ build + -- the usual pair syntax breaks with `No such variable a` here for some reason + let pkgTrie = the (StringTrie (List String)) $ + foldl (\trie, ksv => + let ks = fst ksv + v = snd ksv + in + insertWith ks (maybe [v] (v::)) trie) empty toClean + foldWithKeysC (deleteFolder builddir) + (\ks => map concat . traverse (deleteBin builddir ks)) + pkgTrie + deleteFolder builddir [] + where + delete : String -> Core () + delete path = do True <- coreLift $ fRemove path + | False => do err <- coreLift getErrno + coreLift $ putStrLn $ path ++ ": " ++ show (GenericFileError err) + coreLift $ putStrLn $ "Removed: " ++ path + deleteFolder : String -> List String -> Core () + deleteFolder builddir ns = delete $ builddir ++ dirSep ++ showSep "/" (reverse ns) + deleteBin : String -> List String -> String -> Core () + deleteBin builddir ns mod + = do let ttFile = builddir ++ dirSep ++ showSep "/" (reverse ns) ++ dirSep ++ mod + delete $ ttFile ++ ".ttc" + delete $ ttFile ++ ".ttm" + -- Just load the 'Main' module, if it exists, which will involve building -- it if necessary runRepl : {auto c : Ref Ctxt Defs} -> @@ -264,11 +337,12 @@ processPackage cmd file Install => do [] <- build pkg | errs => coreLift (exit 1) install pkg + Clean => clean pkg REPL => runRepl pkg rejectPackageOpts : List CLOpt -> Core Bool rejectPackageOpts (Package cmd f :: _) - = do coreLift $ putStrLn ("Package commands (--build, --install --repl) must be the only option given") + = do coreLift $ putStrLn ("Package commands (--build, --install, --clean, --repl) must be the only option given") pure True -- Done, quit here rejectPackageOpts (_ :: xs) = rejectPackageOpts xs rejectPackageOpts [] = pure False @@ -284,4 +358,3 @@ processPackageOpts [Package cmd f] = do processPackage cmd f pure True processPackageOpts opts = rejectPackageOpts opts - From 8e37fe697aa62fb98d2922566725456e65b94f67 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Mon, 15 Jul 2019 14:37:05 +0300 Subject: [PATCH 2/2] blodwen -> idris2 --- src/Compiler/Common.idr | 4 ++-- src/Idris/IDEMode/Main.idr | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 8e06796..3fa91e6 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -14,10 +14,10 @@ import Data.NameMap public export record Codegen where constructor MkCG - ||| Compile a Blodwen expression, saving it to a file. + ||| Compile an Idris 2 expression, saving it to a file. compileExpr : Ref Ctxt Defs -> ClosedTerm -> (outfile : String) -> Core (Maybe String) - ||| Execute a Blodwen expression directly. + ||| Execute an Idris 2 expression directly. executeExpr : Ref Ctxt Defs -> ClosedTerm -> Core () ||| compile diff --git a/src/Idris/IDEMode/Main.idr b/src/Idris/IDEMode/Main.idr index d967cc5..8e8881b 100644 --- a/src/Idris/IDEMode/Main.idr +++ b/src/Idris/IDEMode/Main.idr @@ -132,7 +132,7 @@ stMain opts setOutput (IDEMode 0 file file) replIDE {c} {u} {m} else do - iputStrLn "Welcome to Blodwen. Good luck." + iputStrLn "Welcome to Idris 2. Good luck." repl {c} {u} {m} else -- exit with an error code if there was an error, otherwise