edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-03 02:03:20 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of github.com:edwinb/Idris2

Browse Source
This commit is contained in:
Edwin Brady 2019-08-29 11:10:44 +01:00
commit ea75fd21a1
19 changed files with 346 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
docs/index.rst
View File

@ -21,3 +21,4 @@ This is a placeholder, to get set up with readthedocs.
:maxdepth: 1
faq/faq
reference/index

19
docs/reference/index.rst Normal file
View File

@ -0,0 +1,19 @@
**********************
Idris2 Reference Guide
**********************
.. note::
The documentation for Idris 2 has been published under the Creative
Commons CC0 License. As such to the extent possible under law, *The
Idris Community* has waived all copyright and related or neighboring
rights to Documentation for Idris.
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
This is a placeholder, to get set up with readthedocs.
.. toctree::
:maxdepth: 1
packages

102
docs/reference/packages.rst Normal file
View File

@ -0,0 +1,102 @@
.. _ref-sect-packages:
********
Packages
********
Idris includes a simple system for building packages from a package
description file. These files can be used with the Idris compiler to
manage the development process of your Idris programmes and packages.
Package Descriptions
====================
A package description includes the following:
+ A header, consisting of the keyword package followed by the package
name. Package names can be any valid Idris identifier. The iPKG
format also takes a quoted version that accepts any valid filename.
+ Fields describing package contents, ``<field> = <value>``
At least one field must be the modules field, where the value is a
comma separated list of modules. For example, a library test which
has two modules ``Foo.idr`` and ``Bar.idr`` as source files would be
written as follows::
package test
modules = Foo, Bar
Other examples of package files can be found in the ``libs`` directory
of the main Idris repository, and in `third-party libraries <https://github.com/idris-lang/Idris-dev/wiki/Libraries>`_.
Metadata
--------
The `iPKG` format supports additional metadata associated with the package.
The added fields are:
+ ``brief = "<text>"``, a string literal containing a brief description
of the package.
+ ``version = "<text>""``, a version string to associate with the package.
+ ``readme = "<file>""``, location of the README file.
+ ``license = "<text>"``, a string description of the licensing
information.
+ ``authors = "<text>"``, the author information.
+ ``maintainers = "<text>"``, Maintainer information.
+ ``homepage = "<url>"``, the website associated with the package.
+ ``sourceloc = "<url>"``, the location of the DVCS where the source
can be found.
+ ``bugtracker = "<url>"``, the location of the project's bug tracker.
Common Fields
-------------
Other common fields which may be present in an ``ipkg`` file are:
+ ``executable = <output>``, which takes the name of the executable
file to generate. Executable names can be any valid Idris
identifier. the iPKG format also takes a quoted version that accepts
any valid filename.
+ ``main = <module>``, which takes the name of the main module, and
must be present if the executable field is present.
+ ``opts = "<idris options>"``, which allows options to be passed to
Idris.
+ ``depends = <pkg name> (',' <pkg name>)+``, a comma separated list of
package names that the Idris package requires.
Comments
---------
Package files support comments using the standard Idris singleline ``--`` and multiline ``{- -}`` format.
Using Package files
===================
Given an Idris package file ``test.ipkg`` it can be used with the Idris compiler as follows:
+ ``idris2 --build test.ipkg`` will build all modules in the package
+ ``idris2 --install test.ipkg`` will install the package, making it
accessible by other Idris libraries and programs.
+ ``idris2 --clean test.ipkg`` will clean the intermediate build files.
Once the test package has been installed, the command line option
``--package test`` makes it accessible (abbreviated to ``-p test``).
For example::
idris -p test Main.idr

8
libs/network/.gitignore vendored Normal file
View File

@ -0,0 +1,8 @@
network-tests
*.o
*.so
*.dylib
*.dll

2
libs/prelude/Prelude.idr
View File

@ -564,7 +564,7 @@ data Nat = Z | S Nat
public export
integerToNat : Integer -> Nat
integerToNat x
= if intToBool (prim__eq_Integer x 0)
= if intToBool (prim__lte_Integer x 0)
then Z
else S (assert_total (integerToNat (prim__sub_Integer x 1)))

4
src/Idris/CommandLine.idr
View File

@ -23,6 +23,8 @@ data CLOpt
=
||| Only typecheck the given file
CheckOnly |
||| The output file from the code generator
OutputFile String |
||| Execute a given function after checking the source file
ExecFn String |
||| Use a specific code generator (default chez)
@ -67,6 +69,8 @@ record OptDesc where
options : List OptDesc
options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Exit after checking source file"),
MkOpt ["--output", "-o"] ["file"] (\f => [OutputFile f, Quiet])
(Just "Specify output file"),
MkOpt ["--exec", "-x"] ["name"] (\f => [ExecFn f, Quiet])
(Just "Execute function after checking source file"),
MkOpt ["--no-prelude"] [] [NoPrelude]

3
src/Idris/ModTree.idr
View File

@ -129,7 +129,8 @@ fnameModified fname
= do Right f <- coreLift $ openFile fname Read
| Left err => throw (FileErr fname err)
Right t <- coreLift $ fileModifiedTime f
| Left err => throw (FileErr fname err)
| Left err => do coreLift $ closeFile f
throw (FileErr fname err)
coreLift $ closeFile f
pure t

108
src/Idris/Package.idr
View File

@ -30,6 +30,13 @@ record PkgDesc where
name : String
version : String
authors : String
maintainers : Maybe String
license : Maybe String
brief : Maybe String
readme : Maybe String
homepage : Maybe String
sourceloc : Maybe String
bugtracker : Maybe String
depends : List String -- packages to add to search path
modules : List (List String, String) -- modules to install (namespace, filename)
mainmod : Maybe (List String, String) -- main file (i.e. file to load at REPL)
@ -44,6 +51,13 @@ Show PkgDesc where
show pkg = "Package: " ++ name pkg ++ "\n" ++
"Version: " ++ version pkg ++ "\n" ++
"Authors: " ++ authors pkg ++ "\n" ++
maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
maybe "" (\m => "License: " ++ m ++ "\n") (license pkg) ++
maybe "" (\m => "Brief: " ++ m ++ "\n") (brief pkg) ++
maybe "" (\m => "ReadMe: " ++ m ++ "\n") (readme pkg) ++
maybe "" (\m => "HomePage: " ++ m ++ "\n") (homepage pkg) ++
maybe "" (\m => "SourceLoc: " ++ m ++ "\n") (sourceloc pkg) ++
maybe "" (\m => "BugTracker: " ++ m ++ "\n") (bugtracker pkg) ++
"Depends: " ++ show (depends pkg) ++ "\n" ++
"Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
@ -56,26 +70,42 @@ Show PkgDesc where
initPkgDesc : String -> PkgDesc
initPkgDesc pname
= MkPkgDesc pname "0" "Anonymous" [] []
= MkPkgDesc pname "0" "Anonymous" Nothing Nothing
Nothing Nothing Nothing Nothing Nothing
[] []
Nothing Nothing Nothing Nothing Nothing Nothing Nothing
data DescField : Type where
PVersion : FC -> String -> DescField
PAuthors : FC -> String -> DescField
PDepends : List String -> DescField
PModules : List (FC, List String) -> DescField
PMainMod : FC -> List String -> DescField
PExec : String -> DescField
POpts : FC -> String -> DescField
PPrebuild : FC -> String -> DescField
PPostbuild : FC -> String -> DescField
PPreinstall : FC -> String -> DescField
PVersion : FC -> String -> DescField
PAuthors : FC -> String -> DescField
PMaintainers : FC -> String -> DescField
PLicense : FC -> String -> DescField
PBrief : FC -> String -> DescField
PReadMe : FC -> String -> DescField
PHomePage : FC -> String -> DescField
PSourceLoc : FC -> String -> DescField
PBugTracker : FC -> String -> DescField
PDepends : List String -> DescField
PModules : List (FC, List String) -> DescField
PMainMod : FC -> List String -> DescField
PExec : String -> DescField
POpts : FC -> String -> DescField
PPrebuild : FC -> String -> DescField
PPostbuild : FC -> String -> DescField
PPreinstall : FC -> String -> DescField
PPostinstall : FC -> String -> DescField
field : String -> Rule DescField
field fname
= strField PVersion "version"
<|> strField PAuthors "authors"
<|> strField PMaintainers "maintainers"
<|> strField PLicense "license"
<|> strField PBrief "brief"
<|> strField PReadMe "readme"
<|> strField PHomePage "homepage"
<|> strField PSourceLoc "sourceloc"
<|> strField PBugTracker "bugtracker"
<|> strField POpts "options"
<|> strField POpts "opts"
<|> strField PPrebuild "prebuild"
@ -86,7 +116,7 @@ field fname
ds <- sepBy1 (symbol ",") unqualifiedName
pure (PDepends ds)
<|> do exactIdent "modules"; symbol "="
ms <- sepBy1 (symbol ",")
ms <- sepBy1 (symbol ",")
(do start <- location
ns <- namespace_
end <- location
@ -126,8 +156,16 @@ addField : {auto c : Ref Ctxt Defs} ->
DescField -> PkgDesc -> Core PkgDesc
addField (PVersion fc n) pkg = pure (record { version = n } pkg)
addField (PAuthors fc a) pkg = pure (record { authors = a } pkg)
addField (PMaintainers fc a) pkg = pure (record { maintainers = Just a } pkg)
addField (PLicense fc a) pkg = pure (record { license = Just a } pkg)
addField (PBrief fc a) pkg = pure (record { brief = Just a } pkg)
addField (PReadMe fc a) pkg = pure (record { readme = Just a } pkg)
addField (PHomePage fc a) pkg = pure (record { homepage = Just a } pkg)
addField (PSourceLoc fc a) pkg = pure (record { sourceloc = Just a } pkg)
addField (PBugTracker fc a) pkg = pure (record { bugtracker = Just a } pkg)
addField (PDepends ds) pkg = pure (record { depends = ds } pkg)
addField (PModules ms) pkg
addField (PModules ms) pkg
= pure (record { modules = !(traverse toSource ms) } pkg)
where
toSource : (FC, List String) -> Core (List String, String)
@ -148,7 +186,7 @@ addFields (x :: xs) desc = addFields xs !(addField x desc)
runScript : Maybe (FC, String) -> Core ()
runScript Nothing = pure ()
runScript (Just (fc, s))
runScript (Just (fc, s))
= do res <- coreLift $ system s
when (res /= 0) $
throw (GenericMsg fc "Script failed")
@ -167,7 +205,7 @@ processOptions Nothing = pure ()
processOptions (Just (fc, opts))
= do let Right clopts = getOpts (words opts)
| Left err => throw (GenericMsg fc err)
preOptions clopts
preOptions clopts
build : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -200,7 +238,7 @@ installFrom pname builddir destdir ns@(m :: dns)
let ttcPath = builddir ++ dirSep ++ ttcfile ++ ".ttc"
let destPath = destdir ++ dirSep ++ showSep "/" (reverse dns)
let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc"
Right _ <- coreLift $ mkdirs (reverse dns)
Right _ <- coreLift $ mkdirs (reverse dns)
| Left err => throw (FileErr pname err)
coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
Right _ <- coreLift $ copyFile ttcPath destFile
@ -210,10 +248,10 @@ installFrom pname builddir destdir ns@(m :: dns)
-- Install all the built modules in prefix/package/
-- We've already built and checked for success, so if any don't exist that's
-- an internal error.
install : {auto c : Ref Ctxt Defs} ->
install : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc -> Core ()
install pkg
install pkg
= do defs <- get Ctxt
let build = build_dir (dirs (options defs))
runScript (preinstall pkg)
@ -230,12 +268,12 @@ install pkg
True <- coreLift $ changeDir (name pkg)
| False => throw (FileErr (name pkg) FileReadError)
-- We're in that directory now, so copy the files from
-- We're in that directory now, so copy the files from
-- srcdir/build into it
traverse (installFrom (name pkg)
(srcdir ++ dirSep ++ build)
(srcdir ++ dirSep ++ build)
(installPrefix ++ dirSep ++ name pkg)) toInstall
coreLift $ changeDir srcdir
coreLift $ changeDir srcdir
runScript (postinstall pkg)
-- Data.These.bitraverse hand specialised for Core
@ -257,10 +295,10 @@ foldWithKeysC {a} {b} fk fv = go []
map bifold $ bitraverseC
(fv as)
(\sm => foldlC
(\x, (k, vs) =>
(\x, (k, vs) =>
do let as' = as ++ [k]
y <- assert_total $ go as' vs
z <- fk as'
z <- fk as'
pure $ x <+> y <+> z)
neutral
(toList sm))
@ -272,10 +310,10 @@ Semigroup () where
Monoid () where
neutral = ()
clean : {auto c : Ref Ctxt Defs} ->
clean : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc -> Core ()
clean pkg
clean pkg
= do defs <- get Ctxt
let build = build_dir (dirs (options defs))
let toClean = mapMaybe (\ks => [| MkPair (tail' ks) (head' ks) |]) $
@ -286,12 +324,12 @@ clean pkg
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 =>
foldl (\trie, ksv =>
let ks = fst ksv
v = snd ksv
in
v = snd ksv
in
insertWith ks (maybe [v] (v::)) trie) empty toClean
foldWithKeysC (deleteFolder builddir)
foldWithKeysC (deleteFolder builddir)
(\ks => map concat . traverse (deleteBin builddir ks))
pkgTrie
deleteFolder builddir []
@ -311,11 +349,11 @@ clean pkg
-- Just load the 'Main' module, if it exists, which will involve building
-- it if necessary
runRepl : {auto c : Ref Ctxt Defs} ->
runRepl : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc -> Core ()
runRepl pkg
= do addDeps pkg
runRepl pkg
= do addDeps pkg
processOptions (options pkg)
throw (InternalError "Not implemented")
@ -323,8 +361,8 @@ processPackage : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
PkgCommand -> String -> Core ()
processPackage cmd file
= do Right (pname, fs) <- coreLift $ parseFile file
processPackage cmd file
= do Right (pname, fs) <- coreLift $ parseFile file
(do desc <- parsePkgDesc file
eoi
pure desc)
@ -354,7 +392,7 @@ processPackageOpts : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
List CLOpt -> Core Bool
processPackageOpts [Package cmd f]
processPackageOpts [Package cmd f]
= do processPackage cmd f
pure True
processPackageOpts opts = rejectPackageOpts opts

11
src/Idris/Parser.idr
View File

@ -1395,9 +1395,8 @@ editCmd
pure (MakeWith (fromInteger line) n)
<|> fatalError "Unrecognised command"
export
command : Rule REPLCmd
command
nonEmptyCommand : Rule REPLCmd
nonEmptyCommand
= do symbol ":"; replCmd ["t", "type"]
tm <- expr pdef "(interactive)" init
pure (Check tm)
@ -1445,3 +1444,9 @@ command
<|> do tm <- expr pdef "(interactive)" init
pure (Eval tm)
export
command : EmptyRule REPLCmd
command
= do eoi
pure NOP
<|> nonEmptyCommand

3
src/Idris/ProcessIdr.idr
View File

@ -157,7 +157,8 @@ modTime fname
= do Right f <- coreLift $ openFile fname Read
| Left err => pure 0 -- Beginning of Time :)
Right t <- coreLift $ fileModifiedTime f
| Left err => pure 0
| Left err => do coreLift $ closeFile f
pure 0
coreLift $ closeFile f
pure t

35
src/Idris/REPL.idr
View File

@ -218,6 +218,24 @@ findCG
Chicken => pure codegenChicken
Racket => pure codegenRacket
export
compileExp : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
PTerm -> String -> Core ()
compileExp ctm outfile
= do inidx <- resolveName (UN "[input]")
ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
(tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC Rig1 True [] tm
ok <- compile !findCG tm_erased outfile
maybe (pure ())
(\fname => iputStrLn (outfile ++ " written"))
ok
export
execExp : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
@ -467,15 +485,7 @@ process Edit
loadMainFile f
pure True
process (Compile ctm outfile)
= do inidx <- resolveName (UN "[input]")
ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
(tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC Rig1 True [] tm
ok <- compile !findCG tm_erased outfile
maybe (pure ())
(\fname => iputStrLn (outfile ++ " written"))
ok
= do compileExp ctm outfile
pure True
process (Exec ctm)
= do execExp ctm
@ -551,6 +561,8 @@ process (Editing cmd)
process Quit
= do iputStrLn "Bye for now!"
pure False
process NOP
= pure True
processCatch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
@ -619,7 +631,10 @@ repl
inp <- coreLift getLine
end <- coreLift $ fEOF stdin
if end
then iputStrLn "Bye for now!"
then do
-- start a new line in REPL mode (not relevant in IDE mode)
coreLift $ putStrLn ""
iputStrLn "Bye for now!"
else if !(interpret inp)
then repl
else pure ()

5
src/Idris/SetOptions.idr
View File

@ -56,8 +56,13 @@ postOptions : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
List CLOpt -> Core Bool
postOptions [] = pure True
postOptions (OutputFile outfile :: rest)
= do compileExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN "main")) outfile
postOptions rest
pure False
postOptions (ExecFn str :: rest)
= do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
postOptions rest

1
src/Idris/Syntax.idr
View File

@ -280,6 +280,7 @@ data REPLCmd : Type where
Metavars : REPLCmd
Editing : EditCmd -> REPLCmd
Quit : REPLCmd
NOP : REPLCmd
public export
record Import where

7
src/Utils/Binary.idr
View File

@ -79,10 +79,13 @@ readFromFile fname
= do Right h <- openFile fname Read
| Left err => pure (Left err)
Right fsize <- fileSize h
| Left err => pure (Left err)
| Left err => do closeFile h
pure (Left err)
Just b <- newBuffer fsize
| Nothing => pure (Left (GenericFileError 0)) --- um, not really
| Nothing => do closeFile h
pure (Left (GenericFileError 0)) --- um, not really
b <- readBufferFromFile h b fsize
closeFile h
pure (Right (MkBin b 0 fsize fsize))
public export

9
tests/Main.idr
View File

@ -46,6 +46,7 @@ idrisTests
"perf001", "perf002",
"perror001", "perror002", "perror003", "perror004", "perror005",
"perror006",
"pkg001",
"record001", "record002",
"reg001",
"total001", "total002", "total003", "total004", "total005",
@ -84,9 +85,15 @@ runTest prog testPath
Right exp <- readFile "expected"
| Left err => do print err
pure False
if (out == exp)
then putStrLn "success"
else putStrLn "FAILURE"
else do
putStrLn "FAILURE"
putStrLn "Expected:"
printLn exp
putStrLn "Given:"
printLn out
chdir "../.."
pure (out == exp)

69
tests/idris2/pkg001/Dummy.idr Normal file
View File

@ -0,0 +1,69 @@
module Dummy
import Data.Vect
namespace DList
||| A list construct for dependent types.
|||
||| @aTy The type of the value contained within the list element type.
||| @elemTy The type of the elements within the list
||| @as The List used to contain the different values within the type.
public export
data DList : (aTy : Type)
-> (elemTy : aTy -> Type)
-> (as : List aTy)
-> Type where
||| Create an empty List
Nil : DList aTy elemTy Nil
||| Cons
|||
||| @elem The element to add
||| @rest The list for `elem` to be added to.
(::) : (elem : elemTy x)
-> (rest : DList aTy elemTy xs)
-> DList aTy elemTy (x::xs)
namespace DVect
||| A list construct for dependent types.
|||
||| @aTy The type of the value contained within the list element type.
||| @elemTy The type of the elements within the list
||| @len The length of the list.
||| @as The List used to contain the different values within the type.
public export
data DVect : (aTy : Type)
-> (elemTy : aTy -> Type)
-> (len : Nat)
-> (as : Vect len aTy)
-> Type where
||| Create an empty List
Nil : DVect aTy elemTy Z Nil
||| Cons
|||
||| @ex The element to add
||| @rest The list for `elem` to be added to.
(::) : (ex : elemTy x)
-> (rest : DVect aTy elemTy n xs)
-> DVect aTy elemTy (S n) (x::xs)
namespace PList
public export
data PList : (aTy : Type)
-> (elemTy : aTy -> Type)
-> (predTy : aTy -> Type)
-> (as : List aTy)
-> (prf : DList aTy predTy as)
-> Type
where
||| Create an empty List
Nil : PList aTy elemTy predTy Nil Nil
||| Cons
|||
||| @elem The element to add and proof that the element's type satisfies a certain predicate.
||| @rest The list for `elem` to be added to.
(::) : (elem : elemTy x)
-> {prf : predTy x}
-> (rest : PList aTy elemTy predTy xs prfs)
-> PList aTy elemTy predTy (x :: xs) (prf :: prfs)

9
tests/idris2/pkg001/dummy.ipkg Normal file
View File

@ -0,0 +1,9 @@
package dummy
authors = "Joe Bloggs"
maintainers = "Joe Bloggs"
license = "BSD3 but see LICENSE for more information"
brief = "This is a dummy package."
readme = "README.md"
modules = Dummy

1
tests/idris2/pkg001/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Dummy (Dummy.idr)

3
tests/idris2/pkg001/run Executable file
View File

@ -0,0 +1,3 @@
$1 --build dummy.ipkg
rm -rf build