idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of github.com:idris-lang/Idris2 into javascript

Browse Source
This commit is contained in:
Rui Barreiro 2020-06-20 15:11:08 +01:00
commit 1d2f3d8883
15 changed files with 99 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.github/workflows/ci-ubuntu-racket.yml vendored
View File

@ -17,6 +17,7 @@ jobs:
uses: actions/checkout@v2
- name: Install build dependencies
run: |
sudo apt-get update
sudo apt-get install -y racket
- name: Build from bootstrap
run: make bootstrap-racket

11
CHANGELOG.md
View File

@ -27,6 +27,17 @@ Library changes:
should be considered experimental with the API able to change at any time!
Further experiments in `Data.Linear` are welcome :).
Command-line options changes:
* Removed `--ide-mode-socket-with` option. `--ide-mode-socket` now accepts an
optional `host:port` argument.
Compiler changes:
* It is now possible to create new backends with minimal overhead. `Idris.Driver`
exposes the function `mainWithCodegens` that takes a list of codegens. The
feature in documented [here](https://idris2.readthedocs.io/en/latest/backends/custom.html).
Changes since Idris 2 v0.1.0
----------------------------

2
Makefile
View File

@ -101,7 +101,7 @@ clean: clean-libs support-clean
install: install-idris2 install-support install-libs
install-api:
install-api: src/IdrisPaths.idr
${IDRIS2_BOOT} --install idris2api.ipkg
install-idris2:

17
docs/source/backends/custom.rst
View File

@ -10,13 +10,12 @@ starting idris with these codegens in addition to the built-in ones.
Getting started
===============
To use Idris 2 as a library you need to install it with (the ipkg file
is at the top level of the Idris2 repo)
To use Idris 2 as a library you need to install it with (at the top level of the
Idris2 repo)
::
idris2 --build idris2api.ipkg
idris2 --install idris2api.ipkg
make install-api
Now create a file containing
@ -53,11 +52,11 @@ Now you have an idris2 with an added backend.
::
$ ./build/exec/lazy-idris2
____ __ _ ___
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.2.0-d8c7f08bd
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
/ // __ / ___/ / ___/ __/ / Version 0.2.0-bd9498c00
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/ Type :? for help
Welcome to Idris 2. Enjoy yourself!
With codegen for: lazy
@ -67,6 +66,6 @@ It will not be overly eager to actually compile any code with the new backend th
::
$ ./build/exec/lazy --cg lazy Hello.idr -o hello
$ ./build/exec/lazy-idris2 --cg lazy Hello.idr -o hello
I'd rather not.
$

2
docs/source/reference/literate.rst
View File

@ -52,4 +52,4 @@ CommonMark
Only code blocks denoted by standard code blocks labelled as idris are recognised.
We treat files with an extension of ``.md`` and ``.markdown`` as org-mode style literate files.
We treat files with an extension of ``.md`` and ``.markdown`` as CommonMark style literate files.

12
libs/base/Data/Bool.idr
View File

@ -97,3 +97,15 @@ export
notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
notOrIsAnd False _ = Refl
notOrIsAnd True _ = Refl
-- Interaction with typelevel `Not`
export
notTrueIsFalse : {1 x : Bool} -> Not (x = True) -> x = False
notTrueIsFalse {x=False} _ = Refl
notTrueIsFalse {x=True} f = absurd $ f Refl
export
notFalseIsTrue : {1 x : Bool} -> Not (x = False) -> x = True
notFalseIsTrue {x=True} _ = Refl
notFalseIsTrue {x=False} f = absurd $ f Refl

1
libs/base/base.ipkg
View File

@ -14,6 +14,7 @@ modules = Control.App,
Data.Buffer,
Data.Either,
Data.Fin,
Data.Fuel,
Data.IOArray,
Data.IOArray.Prims,
Data.IORef,

12
src/Compiler/Scheme/Chez.idr
View File

@ -366,17 +366,7 @@ startChezCmd chez appdir target = unlines
startChezWinSh : String -> String -> String -> String
startChezWinSh chez appdir target = unlines
[ "#!/bin/sh"
, ""
, "case `uname -s` in "
, " OpenBSD|FreeBSD|NetBSD) "
, " DIR=\"`grealpath $0`\""
, " ;; "
, " "
, " *) "
, " DIR=\"`realpath $0`\" "
, " ;; "
, "esac "
, ""
, "DIR=\"`realpath \"$0\"`\""
, "CHEZ=$(cygpath \"" ++ chez ++"\")"
, "export PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$PATH\""
, "$CHEZ --script \"$(dirname \"$DIR\")/" ++ target ++ "\" \"$@\""

8
src/Compiler/VMCode.idr
View File

@ -30,7 +30,7 @@ data VMInst : Type where
DECLARE : Reg -> VMInst
START : VMInst -- start of the main body of the function
ASSIGN : Reg -> Reg -> VMInst
MKCON : Reg -> (tag : Maybe Int) -> (args : List Reg) -> VMInst
MKCON : Reg -> (tag : Either Int Name) -> (args : List Reg) -> VMInst
MKCLOSURE : Reg -> Name -> (missing : Nat) -> (args : List Reg) -> VMInst
MKCONSTANT : Reg -> Constant -> VMInst
@ -117,8 +117,10 @@ toVM t res (AApp fc f a)
= [APPLY res (toReg f) (toReg a)]
toVM t res (ALet fc var val body)
= toVM False (Loc var) val ++ toVM t res body
toVM t res (ACon fc n tag args)
= [MKCON res tag (map toReg args)]
toVM t res (ACon fc n (Just tag) args)
= [MKCON res (Left tag) (map toReg args)]
toVM t res (ACon fc n Nothing args)
= [MKCON res (Right n) (map toReg args)]
toVM t res (AOp fc op args)
= [OP res op (map toReg args)]
toVM t res (AExtPrim fc p args)

3
src/Core/Context.idr
View File

@ -1747,6 +1747,9 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
addDataConstructors tag (MkCon fc n a ty :: cs) gam
= do let condef = newDef fc n top vars ty (conVisibility vis) (DCon tag a Nothing)
(idx, gam') <- addCtxt n condef gam
-- Check 'n' is undefined
Nothing <- lookupCtxtExact n gam
| Just gdef => throw (AlreadyDefined fc n)
addDataConstructors (tag + 1) cs gam'
-- Add a new nested namespace to the current namespace for new definitions

87
src/Idris/CommandLine.idr
View File

@ -112,32 +112,45 @@ ideSocketModeAddress (_ :: rest) = ideSocketModeAddress rest
formatSocketAddress : (String, Int) -> String
formatSocketAddress (host, port) = host ++ ":" ++ show port
ActType : List String -> Type
data OptType = Required String | Optional String
Show OptType where
show (Required a) = "<" ++ a ++ ">"
show (Optional a) = "[" ++ a ++ "]"
ActType : List OptType -> Type
ActType [] = List CLOpt
ActType (a :: as) = String -> ActType as
ActType (Required a :: as) = String -> ActType as
ActType (Optional a :: as) = Maybe String -> ActType as
record OptDesc where
constructor MkOpt
flags : List String
argdescs : List String
argdescs : List OptType
action : ActType argdescs
help : Maybe String
optSeparator : OptDesc
optSeparator = MkOpt [] [] [] Nothing
showDefault : Show a => a -> String
showDefault x = "(default " ++ show x ++ ")"
options : List OptDesc
options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Exit after checking source file"),
MkOpt ["--output", "-o"] ["file"] (\f => [OutputFile f, Quiet])
MkOpt ["--output", "-o"] [Required "file"] (\f => [OutputFile f, Quiet])
(Just "Specify output file"),
MkOpt ["--exec", "-x"] ["name"] (\f => [ExecFn f, Quiet])
MkOpt ["--exec", "-x"] [Required "name"] (\f => [ExecFn f, Quiet])
(Just "Execute function after checking source file"),
MkOpt ["--no-prelude"] [] [NoPrelude]
(Just "Don't implicitly import Prelude"),
MkOpt ["--codegen", "--cg"] ["backend"] (\f => [SetCG f])
(Just $ "Set code generator (default \""++ show (codegen defaultSession) ++ "\")"),
MkOpt ["--package", "-p"] ["package"] (\f => [PkgPath f])
MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f])
(Just $ "Set code generator " ++ showDefault (codegen defaultSession)),
MkOpt ["--package", "-p"] [Required "package"] (\f => [PkgPath f])
(Just "Add a package as a dependency"),
MkOpt [] [] [] Nothing,
optSeparator,
MkOpt ["--prefix"] [] [ShowPrefix]
(Just "Show installation prefix"),
MkOpt ["--paths"] [] [BlodwenPaths]
@ -145,33 +158,33 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
MkOpt ["--libdir"] [] [Directory LibDir]
(Just "Show library directory"),
MkOpt [] [] [] Nothing,
MkOpt ["--build"] ["package file"] (\f => [Package Build f])
optSeparator,
MkOpt ["--build"] [Required "package file"] (\f => [Package Build f])
(Just "Build modules/executable for the given package"),
MkOpt ["--install"] ["package file"] (\f => [Package Install f])
MkOpt ["--install"] [Required "package file"] (\f => [Package Install f])
(Just "Install the given package"),
MkOpt ["--clean"] ["package file"] (\f => [Package Clean f])
MkOpt ["--clean"] [Required "package file"] (\f => [Package Clean f])
(Just "Clean intermediate files/executables for the given package"),
MkOpt ["--repl"] ["package file"] (\f => [Package REPL f])
MkOpt ["--repl"] [Required "package file"] (\f => [Package REPL f])
(Just "Build the given package and launch a REPL instance."),
MkOpt ["--find-ipkg"] [] [FindIPKG]
(Just "Find and use an .ipkg file in a parent directory"),
MkOpt [] [] [] Nothing,
optSeparator,
MkOpt ["--ide-mode"] [] [IdeMode]
(Just "Run the REPL with machine-readable syntax"),
MkOpt ["--ide-mode-socket"] [] [IdeModeSocket $ formatSocketAddress (ideSocketModeAddress [])]
(Just $ "Run the ide socket mode on default host and port (" ++ formatSocketAddress (ideSocketModeAddress []) ++ ")"),
MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp])
(Just "Run the ide socket mode on given host and port"),
MkOpt ["--ide-mode-socket"] [Optional "host:port"]
(\hp => [IdeModeSocket $ fromMaybe (formatSocketAddress (ideSocketModeAddress [])) hp])
(Just $ "Run the ide socket mode on given host and port " ++
showDefault (formatSocketAddress (ideSocketModeAddress []))),
MkOpt [] [] [] Nothing,
MkOpt ["--client"] ["REPL command"] (\f => [RunREPL f])
optSeparator,
MkOpt ["--client"] [Required "REPL command"] (\f => [RunREPL f])
(Just "Run a REPL command then quit immediately"),
MkOpt ["--timing"] [] [Timing]
(Just "Display timing logs"),
MkOpt [] [] [] Nothing,
optSeparator,
MkOpt ["--no-banner"] [] [NoBanner]
(Just "Suppress the banner"),
MkOpt ["--quiet", "-q"] [] [Quiet]
@ -179,24 +192,24 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
MkOpt ["--verbose"] [] [Verbose]
(Just "Verbose mode (default)"),
MkOpt [] [] [] Nothing,
optSeparator,
MkOpt ["--version", "-v"] [] [Version]
(Just "Display version string"),
MkOpt ["--help", "-h", "-?"] [] [Help]
(Just "Display help text"),
-- Internal debugging options
MkOpt ["--yaffle", "--ttimp"] ["ttimp file"] (\f => [Yaffle f])
MkOpt ["--yaffle", "--ttimp"] [Required "ttimp file"] (\f => [Yaffle f])
Nothing, -- run ttimp REPL rather than full Idris
MkOpt ["--ttm" ] ["ttimp file"] (\f => [Metadata f])
MkOpt ["--ttm" ] [Required "ttimp file"] (\f => [Metadata f])
Nothing, -- dump metadata information from the given ttm file
MkOpt ["--dumpcases"] ["output file"] (\f => [DumpCases f])
MkOpt ["--dumpcases"] [Required "output file"] (\f => [DumpCases f])
Nothing, -- dump case trees to the given file
MkOpt ["--dumplifted"] ["output file"] (\f => [DumpLifted f])
MkOpt ["--dumplifted"] [Required "output file"] (\f => [DumpLifted f])
Nothing, -- dump lambda lifted trees to the given file
MkOpt ["--dumpanf"] ["output file"] (\f => [DumpANF f])
MkOpt ["--dumpanf"] [Required "output file"] (\f => [DumpANF f])
Nothing, -- dump ANF to the given file
MkOpt ["--dumpvmcode"] ["output file"] (\f => [DumpVMCode f])
MkOpt ["--dumpvmcode"] [Required "output file"] (\f => [DumpVMCode f])
Nothing, -- dump VM Code to the given file
MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
Nothing -- do more elaborator checks (currently conversion in LinearCheck)
@ -215,7 +228,7 @@ optsUsage options = let optsShow = map optShow options
optShow : OptDesc -> (String, Maybe String)
optShow (MkOpt [] _ _ _) = ("", Just "")
optShow (MkOpt flags argdescs action help) = (showSep ", " flags ++ " " ++
showSep " " (map (\x => "<" ++ x ++ ">") argdescs),
showSep " " (map show argdescs),
help)
optUsage : Nat -> (String, Maybe String) -> String
@ -237,13 +250,17 @@ usage = versionMsg ++ "\n" ++
"Available options:\n" ++
optsUsage options
processArgs : String -> (args : List String) -> List String -> ActType args ->
processArgs : String -> (args : List OptType) -> List String -> ActType args ->
Either String (List CLOpt, List String)
processArgs flag [] xs f = Right (f, xs)
processArgs flag (a :: as) [] f
= Left $ "Missing argument <" ++ a ++ "> for flag " ++ flag
processArgs flag (a :: as) (x :: xs) f
= processArgs flag as xs (f x)
processArgs flag (opt@(Required _) :: as) [] f =
Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
processArgs flag (Optional a :: as) [] f =
processArgs flag as [] (f Nothing)
processArgs flag (Required a :: as) (x :: xs) f =
processArgs flag as xs (f x)
processArgs flag (Optional a :: as) (x :: xs) f =
processArgs flag as xs (f $ toMaybe (not (isPrefixOf "-" x)) x)
matchFlag : (d : OptDesc) -> List String ->
Either String (Maybe (List CLOpt, List String))

2
src/Parser/Unlit.idr
View File

@ -24,7 +24,7 @@ styleOrg = MkLitStyle
export
styleCMark : LiterateStyle
styleCMark = MkLitStyle [("```idris", "```")] Nil [".md"]
styleCMark = MkLitStyle [("```idris", "```")] Nil [".md", ".markdown"]
export
isLitFile : String -> Maybe LiterateStyle

1
src/TTImp/ProcessData.idr
View File

@ -375,4 +375,3 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
traverse_ (\x => addHintFor fc (Resolved tidx) x True False) connames
traverse_ updateErasable (Resolved tidx :: connames)

2
tests/Main.idr
View File

@ -119,7 +119,7 @@ chezTests
nodeTests : List String
nodeTests
= [ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009"
, "node011", "node012", "node013", "node014", "node015", "node017", "node018", "node019"
, "node011", "node012", "node014", "node015", "node017", "node018", "node019"
, "node020", "node021"
, "reg001"
]

2
tests/idris2/coverage010/expected
View File

@ -3,4 +3,4 @@ casetot.idr:12:1--13:1:main is not covering at:
12 main : IO ()
13 main = do
Calls non covering function Main.case block in 2102(587)
Calls non covering function Main.case block in 2101(617)