mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-08-17 03:40:33 +03:00
Merge pull request #16 from clayrat/clean-ipkg
Add --clean option for ipkg
This commit is contained in:
commit
36b5081a4e
@ -42,6 +42,8 @@ modules =
|
||||
Data.IOArray,
|
||||
Data.NameMap,
|
||||
Data.StringMap,
|
||||
Data.These,
|
||||
Data.StringTrie,
|
||||
|
||||
Idris.CommandLine,
|
||||
Idris.Desugar,
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
55
src/Data/StringTrie.idr
Normal file
55
src/Data/StringTrie.idr
Normal file
@ -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
|
35
src/Data/These.idr
Normal file
35
src/Data/These.idr
Normal file
@ -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) |]
|
@ -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"),
|
||||
|
@ -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
|
||||
|
@ -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
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user