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

Merge branch 'master' into use-contrib

Browse Source
This commit is contained in:
Kamil Shakirov 2020-05-29 15:05:18 +06:00
commit d43850d86e
158 changed files with 12784 additions and 10737 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
.github/workflows/ci-macos.yml vendored
View File

@ -8,7 +8,8 @@ on:
pull_request:
branches:
- master
env:
SCHEME: chez
jobs:
build:
runs-on: macos-latest
@ -19,6 +20,10 @@ jobs:
run: |
brew install chezscheme
brew install coreutils
echo "::add-path::$HOME/.idris2/bin"
- name: Build and test Idris 2 from bootstrap
run: make bootstrap SCHEME=chez
run: make bootstrap && make install
shell: bash
- name: Build and test self-hosted
run: make clean && make all && make test INTERACTIVE=''
shell: bash

8
.github/workflows/ci-ubuntu.yml vendored
View File

@ -9,6 +9,8 @@ on:
branches:
- master
env:
SCHEME: scheme
jobs:
build:
runs-on: ubuntu-latest
@ -18,7 +20,11 @@ jobs:
- name: Install build dependencies
run: |
sudo apt-get install -y chezscheme
echo "::add-path::$HOME/.idris2/bin"
- name: Build from bootstrap
run: make bootstrap SCHEME=scheme
run: make bootstrap && make install
shell: bash
- name: Build and test self-hosted
run: make clean && make all && make test INTERACTIVE=''
shell: bash

27
.github/workflows/ci-windows.yml vendored
View File

@ -9,7 +9,10 @@ on:
branches:
- master
env:
MSYSTEM: MINGW64
MSYS2_PATH_TYPE: inherit
SCHEME: scheme
CC: gcc
jobs:
build:
@ -17,24 +20,24 @@ jobs:
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Install MSYS2
uses: eine/setup-msys2@v0
with:
update: true
install: make mingw-w64-x86_64-clang tar
- name: Get Chez Scheme
run: |
git clone --depth 1 https://github.com/cisco/ChezScheme
c:\msys64\usr\bin\bash -l -c "pacman -S --noconfirm tar make"
echo "::set-env name=PWD::$(c:\msys64\usr\bin\cygpath -u $(pwd))"
- name: Configure and Build Chez Scheme
run: msys2do cd ChezScheme; ./configure --threads; make; cd ..
shell: cmd
run: |
c:\msys64\usr\bin\bash -l -c "cd $env:PWD && cd ChezScheme && ./configure --threads && make"
- name: Set Path
run: |
$chez="$(pwd)\ChezScheme\ta6nt\bin\ta6nt"
$idris="$(pwd)\.idris2"
echo "::add-path::$chez"
echo "::set-env name=SCHEME::scheme"
echo "::add-path::$idris\bin"
echo "::set-env name=IDRIS_PREFIX::$idris"
echo "::set-env name=PREFIX::$(c:\msys64\usr\bin\cygpath -u $idris)"
- name: Test Scheme
run: scheme.exe --version
- name: Bootstrap
run: msys2do make bootstrap
shell: cmd
run: |
scheme --version
- name: Bootstrap and install
run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make bootstrap && make install"

10
CONTRIBUTING.md
View File

@ -4,7 +4,6 @@ Contributing to Idris 2
Contributions are welcome! The most important things needed at this stage,
beyond work on the language core, are (in no particular order):
* CI integration.
* Documentation string support (at the REPL and IDE mode).
* Generating HTML documentation from documentation strings (and possibly other
formations)
@ -22,8 +21,6 @@ beyond work on the language core, are (in no particular order):
- (Not really part of Idris 2, but an editing mode for vim would be lovely!)
* Some parts of the Idris 1 Prelude are not yet implemented and should be
added to base/
* Partial evaluation, especially for specialisation of interface
implementations.
* The lexer and parser are quite slow, new and faster versions with better
errors would be good.
- In particular, large sections commented out with {- -} can take a while
@ -47,8 +44,6 @@ notably:
- This will necessarily be slightly different from Idris 1 since the
elaborator works differently. It would also be nice to extend it with
libraries and perhaps syntax for deriving implementations of interfaces.
* `%default` directives, since coverage and totality checking have not been well
tested yet.
Other contributions are also welcome, but I (@edwinb) will need to be
confident that I'll be able to maintain them!
@ -74,11 +69,6 @@ behaviour might be useful in a proof (so very small definitions) are
Syntax
------
Some syntax that hasn't yet been implemented but will be:
* Idiom brackets
* !-notation [needs some thought about the exact rules]
Some things from Idris 1 definitely won't be implemented:
* `%access` directives, because it's too easy to export things by accident

28
Makefile
View File

@ -27,16 +27,22 @@ IDRIS2_SUPPORT := libidris2_support${SHLIB_SUFFIX}
IDRIS2_IPKG := idris2.ipkg
ifeq ($(OS), windows)
# This produces D:/../.. style paths
IDRIS2_PREFIX := $(shell cygpath -m ${PREFIX})
IDRIS2_CURDIR := $(shell cygpath -m ${CURDIR})
export IDRIS2_BOOT_PATH = "${IDRIS2_CURDIR}/libs/prelude/build/ttc;${IDRIS2_CURDIR}/libs/base/build/ttc;${IDRIS2_CURDIR}/libs/network/build/ttc"
SEP := ;
else
IDRIS2_PREFIX := ${PREFIX}
IDRIS2_CURDIR := ${CURDIR}
export IDRIS2_BOOT_PATH = ${IDRIS2_CURDIR}/libs/prelude/build/ttc:${IDRIS2_CURDIR}/libs/base/build/ttc:${IDRIS2_CURDIR}/libs/network/build/ttc
SEP := :
endif
# Library and data paths for bootstrap-test
IDRIS2_BOOT_TEST_LIBS := ${IDRIS2_CURDIR}/bootstrap/${NAME}-${IDRIS2_VERSION}/lib
IDRIS2_BOOT_TEST_DATA := ${IDRIS2_CURDIR}/bootstrap/${NAME}-${IDRIS2_VERSION}/support
# These are the library path in the build dir to be used during build
export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS2_CURDIR}/libs/base/build/ttc${SEP}${IDRIS2_CURDIR}/libs/network/build/ttc"
export SCHEME
@ -125,9 +131,12 @@ install-libs: libs
${MAKE} -C libs/contrib install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
.PHONY: bootstrap bootstrap-racket bootstrap-clean
.PHONY: bootstrap bootstrap-build bootstrap-racket bootstrap-racket-build bootstrap-test bootstrap-clean
bootstrap: support
# Bootstrapping using SCHEME
bootstrap: bootstrap-build bootstrap-test
bootstrap-build: support
cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
sed s/libidris2_support.so/${IDRIS2_SUPPORT}/g bootstrap/idris2_app/idris2.ss > bootstrap/idris2_app/idris2-boot.ss
ifeq ($(OS), darwin)
@ -135,9 +144,14 @@ ifeq ($(OS), darwin)
else
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss
endif
SCHEME=${SCHEME} \
IDRIS2_VERSION=${IDRIS2_VERSION} \
sh ./bootstrap.sh
bootstrap-racket: support
# Bootstrapping using racket
bootstrap-racket: bootstrap-racket-build bootstrap-test
bootstrap-racket-build: support
cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
cp bootstrap/idris2_app/idris2.rkt bootstrap/idris2_app/idris2-boot.rkt
ifeq ($(OS), darwin)
@ -145,8 +159,12 @@ ifeq ($(OS), darwin)
else
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt
endif
IDRIS2_VERSION=${IDRIS2_VERSION} \
sh ./bootstrap-rkt.sh
bootstrap-test:
$(MAKE) test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_DATA=${IDRIS2_BOOT_TEST_DATA} IDRIS2_LIBS=${IDRIS2_BOOT_TEST_LIBS}
bootstrap-clean:
$(RM) -r bootstrap/bin bootstrap/lib bootstrap/idris2-${IDRIS2_VERSION}
$(RM) bootstrap/idris2boot* bootstrap/idris2_app/idris2-boot.* bootstrap/idris2_app/${IDRIS2_SUPPORT}

34
bootstrap-rkt.sh
View File

@ -1,9 +1,17 @@
#!/bin/sh
set -e # Exit on any error
echo "bootstrapping IDRIS2_VERSION=$IDRIS2_VERSION"
if [ -z "$IDRIS2_VERSION" ]
then
echo "Required ENV not set."
exit 1
fi
# Compile the bootstrap scheme
cd bootstrap
echo "Building idris2boot from idris2boot.rkt"
echo "Building idris2-boot from idris2-boot.rkt"
raco exe idris2_app/idris2-boot.rkt
# Put the result in the usual place where the target goes
@ -14,17 +22,27 @@ install idris2_app/* ../build/exec/idris2_app
cd ..
# Install with the bootstrap directory as the PREFIX
DIR="`realpath $0`"
PREFIX="`dirname $DIR`"/bootstrap
PREFIX=${PWD}/bootstrap
if [ ${OS} = "windows" ]; then
# IDRIS_PREFIX is only used to build IDRIS2_BOOT_PATH
IDRIS_PREFIX=$(cygpath -m $PREFIX)
SEP=";"
else
IDRIS_PREFIX=${PREFIX}
SEP=":"
fi
BOOT_PATH_BASE=${IDRIS_PREFIX}/idris2-${IDRIS2_VERSION}
IDRIS2_BOOT_PATH="${BOOT_PATH_BASE}/prelude${SEP}${BOOT_PATH_BASE}/base${SEP}${BOOT_PATH_BASE}/contrib${SEP}${BOOT_PATH_BASE}/network"
# Now rebuild everything properly
# PREFIX must be the "clean" build root, without cygpath -m
# Otherwise, we get 'git: Bad address'
echo ${PREFIX}
IDRIS2_BOOT_PATH="${PREFIX}/idris2-0.2.0/prelude:${PREFIX}/idris2-0.2.0/base:${PREFIX}/idris2-0.2.0/contrib:${PREFIX}/idris2-0.2.0/network"
DYLIB_PATH="${PREFIX}/lib"
DYLIB_PATH="${PREFIX}/lib"
make libs IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
make install IDRIS2_CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
make clean IDRIS2_BOOT=${PREFIX}/bin/idris2 LD_LIBRARY_PATH=${DYLIB_PATH}
make all IDRIS2_BOOT=${PREFIX}/bin/idris2 IDRIS2_CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} LD_LIBRARY_PATH=${DYLIB_PATH}
make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2 CG=racket IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib LD_LIBRARY_PATH=${DYLIB_PATH}

32
bootstrap.sh
View File

@ -1,13 +1,22 @@
#!/bin/sh
if [ -z "$SCHEME" ]
set -e # Exit on any error
echo "bootstrapping SCHEME=$SCHEME IDRIS2_VERSION=$IDRIS2_VERSION"
if [ -z "$SCHEME" ] || [ -z "$IDRIS2_VERSION" ]
then
echo "SCHEME not set. Invoke with SCHEME=[name of chez executable]"
echo "Required ENV not set."
if [ -z "$SCHEME" ]
then
echo "Invoke with SCHEME=[name of chez scheme executable]"
fi
exit 1
fi
# Compile the bootstrap scheme
# TODO: Move boot-build to Makefile in bootstrap/Makefile
cd bootstrap
echo "Building idris2-boot from idris2-boot.ss"
${SCHEME} --script compile.ss
# Put the result in the usual place where the target goes
@ -18,32 +27,27 @@ install idris2_app/* ../build/exec/idris2_app
cd ..
# Install with the bootstrap directory as the PREFIX
DIR="`realpath $0`"
PREFIX="`dirname $DIR`"/bootstrap
# TODO: Unify with bootstrap-rkt
PREFIX=${PWD}/bootstrap
if [ ${OS} = "windows" ]; then
# IDRIS_PREFIX is only used to build IDRIS2_BOOT_PATH
IDRIS_PREFIX=$(cygpath -m $PREFIX)
SEP=";"
NEW_PREFIX=$(cygpath -m $(dirname "$DIR"))
else
IDRIS_PREFIX=${PREFIX}
SEP=":"
NEW_PREFIX="`dirname $DIR`"
fi
IDRIS2_BOOT_PATH="${IDRIS_PREFIX}/idris2-0.2.0/prelude${SEP}${IDRIS_PREFIX}/idris2-0.2.0/base${SEP}${IDRIS_PREFIX}/idris2-0.2.0/contrib${SEP}${IDRIS_PREFIX}/idris2-0.2.0/network"
IDRIS2_TEST_LIBS="${IDRIS_PREFIX}/idris2-0.2.0/lib"
IDRIS2_TEST_DATA="${IDRIS_PREFIX}/idris2-0.2.0/support"
IDRIS2_NEW_PATH="${NEW_PREFIX}/libs/prelude/build/ttc${SEP}${NEW_PREFIX}/libs/base/build/ttc${SEP}${NEW_PREFIX}/libs/network/build/ttc"
BOOT_PATH_BASE=${IDRIS_PREFIX}/idris2-${IDRIS2_VERSION}
IDRIS2_BOOT_PATH="${BOOT_PATH_BASE}/prelude${SEP}${BOOT_PATH_BASE}/base${SEP}${BOOT_PATH_BASE}/contrib${SEP}${BOOT_PATH_BASE}/network"
# Now rebuild everything properly
# PREFIX must be the "clean" build root, without cygpath -m
# Otherwise, we get 'git: Bad address'
echo ${PREFIX}
make libs SCHEME=${SCHEME} PREFIX=${PREFIX}
make install SCHEME=${SCHEME} PREFIX=${PREFIX}
make clean IDRIS2_BOOT=${PREFIX}/bin/idris2
make all IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
echo "Testing using libraries in ${IDRIS2_NEW_PATH}"
make test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_NEW_PATH} SCHEME=${SCHEME} IDRIS2_LIBS=${IDRIS2_TEST_LIBS} IDRIS2_DATA=${IDRIS2_TEST_DATA}

10296
bootstrap/idris2_app/idris2.rkt
View File

File diff suppressed because one or more lines are too long

10292
bootstrap/idris2_app/idris2.ss
View File

File diff suppressed because one or more lines are too long

3
config.mk
View File

@ -2,8 +2,7 @@
PREFIX ?= $(HOME)/.idris2
# clang compiles the output much faster than gcc!
CC := clang
CC ?= clang
##################################################################

2
docs/make.bat
View File

@ -21,7 +21,7 @@ if errorlevel 9009 (
echo.may add the Sphinx directory to PATH.
echo.
echo.If you don't have Sphinx installed, grab it from
echo.http://sphinx-doc.org/
echo.https://www.sphinx-doc.org/
exit /b 1
)

88
docs/source/app/exceptionsstate.rst Normal file
View File

@ -0,0 +1,88 @@
Exceptions and State
====================
``Control.App`` is primarily intended to make it easier to manage the common
cases of applications with exceptions and state. We can throw and catch
exceptions listed in the environment (the ``e`` parameter to ``App``) and
introduce new global state.
Exceptions
----------
The ``Environment`` is a list of error types, usable via the
``Exception`` interface defined in ``Control.App``:
.. code-block:: idris
interface Exception err e where
throw : err -> App e a
catch : App e a -> (err -> App e a) -> App e a
We can use ``throw`` and ``catch`` for some exception type
``err`` as long as the exception type exists in the environment. This is
checked with the ``HasErr`` predicate, also defined in ``Control.App``:
.. code-block:: idris
data HasErr : Type -> Environment -> Type where
Here : HasErr e (e :: es)
There : HasErr e es -> HasErr e (e' :: es)
HasErr err e => Exception err e where ...
Note the ``HasErr`` constraint on ``Exception``: this is one place
where it is notationally convenient that the ``auto`` implicit mechanism
and the interface resolution mechanism are identical in Idris 2.
Finally, we can introduce new exception types via ``handle``, which runs a
block of code which might throw, handling any exceptions:
.. code-block:: idris
handle : App (err :: e) a -> (onok : a -> App e b) ->
(onerr : err -> App e b) -> App e b
Adding State
------------
Applications will typically need to keep track of state, and we support
this primitively in ``App`` using a ``State`` type, defined in
``Control.App``:
.. code-block:: idris
data State : (tag : a) -> Type -> Environment -> Type
The ``tag`` is used purely to distinguish between different states,
and is not required at run-time, as explicitly stated in the types of
``get`` and ``put``, which are used to access and update a state:
.. code-block:: idris
get : (0 tag : a) -> State tag t e => App {l} e t
put : (0 tag : a) -> State tag t e => t -> App {l} e ()
These use an ``auto``-implicit to pass around
a ``State`` with the relevant ``tag`` implicitly, so we refer
to states by tag alone. In ``helloCount`` earlier, we used an empty type
``Counter`` as the tag:
.. code-block:: idris
data Counter : Type where -- complete definition
The environment ``e`` is used to ensure that
states are only usable in the environment in which they are introduced.
States are introduced using ``new``:
.. code-block:: idris
new : t -> (1 p : State tag t e => App {l} e a) -> App {l} e a
Note that the type tells us ``new`` runs the program with the state
exactly once.
Rather than using ``State`` and ``Exception`` directly, however,
we typically use interfaces to constrain the operations which are allowed
in an environment. Internally, ``State`` is implemented via an
``IORef``, primarily for performance reasons.

9
docs/source/app/index.rst
View File

@ -46,4 +46,11 @@ We begin by introducing ``App``, with some small example
programs, then show how to extend it with exceptions, state, and other
interfaces.
[To be continued...]
.. toctree::
:maxdepth: 1
introapp
exceptionsstate
interfaces
linear

148
docs/source/app/interfaces.rst Normal file
View File

@ -0,0 +1,148 @@
Defining Interfaces
===================
The only way provided by ``Control.App`` to run an ``App`` is
via the ``run`` function, which takes a concrete environment
``Init``.
All concrete extensions to this environment are via either ``handle``,
to introduce a new exception, or ``new``, to introduce a new state.
In order to compose ``App`` programs effectively, rather than
introducing concrete exceptions and state in general, we define interfaces for
collections of operations which work in a specific environment.
Example: Console I/O
--------------------
We have seen an initial example using the ``Console`` interface,
which is declared as follows, in ``Control.App.Console``:
.. code-block:: idris
interface Console e where
putStr : String -> App {l} e ()
getStr : App {l} e String
It provides primitives for writing to and reading from the console, and
generalising the path parameter to ``l`` means that neither can
throw an exception, because they have to work in both the ``NoThrow``
and ``MayThrow`` contexts.
To implement this for use in a top level ``IO``
program, we need access to primitive ``IO`` operations.
The ``Control.App`` library defines a primitive interface for this:
.. code-block:: idris
interface PrimIO e where
primIO : IO a -> App {l} e a
fork : (forall e' . PrimIO e' => App {l} e' ()) -> App e ()
We use ``primIO`` to invoke an ``IO`` function. We also have a ``fork``
primitive, which starts a new thread in a new environment supporting
``PrimIO``. Note that ``fork`` starts a new environment ``e'`` so that states
are only available in a single thread.
There is an implementation of ``PrimIO`` for an environment which can
throw the empty type as an exception. This means that if ``PrimIO``
is the only interface available, we cannot throw an exception, which is
consistent with the definition of ``IO``. This also allows us to
use ``PrimIO`` in the initial environment ``Init``.
.. code-block:: idris
HasErr Void e => PrimIO e where ...
Given this, we can implement \texttt{Console} and run our \texttt{hello}
program in ``IO``. It is implemented as follows in ``Control.App.Console``:
.. code-block:: idris
PrimIO e => Console e where
putStr str = primIO $ putStr str
getStr = primIO $ getLine
Example: File I/O
-----------------
Console I/O can be implemented directly, but most I/O operations can fail.
For example, opening a file can fail for several reasons: the file does not
exist; the user has the wrong permissions, etc. In Idris, the ``IO``
primitive reflects this in its type:
.. code-block:: idris
openFile : String -> Mode -> IO (Either FileError File)
While precise, this becomes unwieldy when there are long sequences of
``IO`` operations. Using ``App``, we can provide an interface
which throws an exception when an operation fails, and guarantee that any
exceptions are handled at the top level using ``handle``.
We begin by defining the ``FileIO`` interface, in ``Control.App.FileIO``:
.. code-block:: idris
interface Has [Exception IOError] e => FileIO e where
withFile : String -> Mode -> (onError : IOError -> App e a) ->
(onOpen : File -> App e a) -> App e a
fGetStr : File -> App e String
fPutStr : File -> String -> App e ()
fEOF : File -> App e Bool
We use resource bracketing - passing a function to ``withFile`` for working
with the opened file - rather than an explicit ``open`` operation,
to open a file, to ensure that the file handle is cleaned up on
completion.
One could also imagine an interface using a linear resource for the file, which
might be appropriate in some safety critical contexts, but for most programming
tasks, exceptions should suffice.
All of the operations can fail, and the interface makes this explicit by
saying we can only implement ``FileIO`` if the environment supports
throwing and catching the ``IOError`` exception. ``IOError`` is defined
in ``Control.App``.
For example, we can use this interface to implement ``readFile``, throwing
an exception if opening the file fails in ``withFile``:
.. code-block:: idris
readFile : FileIO e => String -> App e String
readFile f = withFile f Read throw $ \h =>
do content <- read [] h
pure (concat content)
where
read : List String -> File -> App e (List String)
read acc h = do eof <- fEOF h
if eof then pure (reverse acc)
else do str <- fGetStr h
read (str :: acc) h
Again, this is defined in ``Control.App.FileIO``.
To implement ``FileIO``, we need access to the primitive operations
via ``PrimIO``, and the ability to throw exceptions if any of the
operations fail. With this, we can implement ``withFile`` as follows,
for example:
.. code-block:: idris
Has [PrimIO, Exception IOError] e => FileIO e where
withFile fname m onError proc
= do Right h <- primIO $ openFile fname m
| Left err => onError (FileErr (toFileEx err))
res <- catch (proc h) onError
pure res
...
Given this implementation of ``FileIO``, we can run ``readFile``,
provided that we wrap it in a top level ``handle`` function to deal
with any errors thrown by ``readFile``:
.. code-block:: idris
readMain : String -> App Init ()
readMain fname = handle (readFile fname)
(\str => putStrLn $ "Success:\n" ++ show str)
(\err : IOError => putStrLn $ "Error: " ++ show err)

108
docs/source/app/introapp.rst Normal file
View File

@ -0,0 +1,108 @@
Introducing App
===============
``App`` is declared as below, in a module ``Control.App``, which is part of
the ``base`` libraries.
It is parameterised by an implicit
``Path`` (which states whether the program's execution path
is linear or might throw
exceptions), which has a ``default`` value that the program
might throw, and an ``Environment``
(which gives a list of exception types which can be thrown, and is
a synonym for ``List Type``):
.. code-block:: idris
data App : {default MayThrow l : Path} ->
(e : Environment) -> Type -> Type
It serves the same purpose as ``IO``, but supports throwing and catching
exceptions, and allows us to define more constrained interfaces parameterised
by the environment ``e``.
e.g. a program which supports console IO:
.. code-block:: idris
hello : Console e => App e ()
hello = putStrLn "Hello, App world!"
We can use this in a complete program as follows:
.. code-block:: idris
module Main
import Control.App
import Control.App.Console
hello : Console e => App e ()
hello = putStrLn "Hello, App world!"
main : IO ()
main = run hello
Or, a program which supports console IO and carries an ``Int`` state,
labelled ``Counter``:
.. code-block:: idris
data Counter : Type where
helloCount : (Console e, State Counter Int e) => App e ()
helloCount = do c <- get Counter
put Counter (c + 1)
putStrLn "Hello, counting world"
c <- get Counter
putStrLn ("Counter " ++ show c)
To run this as part of a complete program, we need to initialise the state.
.. code-block:: idris
main : IO ()
main = run (new 93 helloCount)
For convenience, we can list multiple interfaces in one go, using a function
``Has``, defined in ``Control.App``, to compute the interface constraints:
.. code-block:: idris
helloCount : Has [Console, State Counter Int] e => App e ()
0 Has : List (a -> Type) -> a -> Type
Has [] es = ()
Has (e :: es') es = (e es, Has es' es)
The purpose of ``Path`` is to state whether a program can throw
exceptions, so that we can know where it is safe to reference linear
resources. It is declared as follows:
.. code-block:: idris
data Path = MayThrow | NoThrow
The type of ``App`` states that ``MayThrow`` is the default.
We expect this to be the most
common case. After all, realistically, most operations have possible failure
modes, especially those which interact with the outside world.
The ``0`` on the declaration of ``Has`` indicates that it can only
be run in an erased context, so it will never be run at run-time.
To run an ``App`` inside ``IO``, we use an initial
environment ``Init`` (recall that an ``Environment`` is a
``List Type``):
.. code-block:: idris
Init : Environment
Init = [Void]
run : App {l} Init a -> IO a
Generalising the ``Path`` parameter with ``l``
means that we can invoke ``run`` for any application, whether the ``Path``
is ``NoThrow`` or ``MayThrow``. But, in practice, all applications
given to ``run`` will not throw at the top level, because the only
exception type available is the empty type ``Void``. Any exceptions
will have been introduced and handled inside the ``App``.

253
docs/source/app/linear.rst Normal file
View File

@ -0,0 +1,253 @@
Linear Resources
================
We have introduced ``App`` for writing
interactive programs, using interfaces to constrain which operations are
permitted, but have not yet seen the ``Path`` parameter in action.
Its purpose is to constrain when programs can throw exceptions,
to know where linear resource usage is allowed. The bind operator
for ``App`` is defined as follows (not via ``Monad``):
.. code-block:: idris
data SafeBind : Path -> (l' : Path) -> Type where
SafeSame : SafeBind l l
SafeToThrow : SafeBind NoThrow MayThrow
(>>=) : SafeBind l l' =>
App {l} e a -> (a -> App {l=l'} e b) -> App {l=l'} e b
The intuition behind this type is that, when sequencing two ``App``
programs:
* if the first action might throw an exception, then the whole program might
throw.
* if the first action cannot throw an exception, the second action can still
throw, and the program as a whole can throw.
* if neither action can throw an exception, the program as a whole cannot
throw.
The reason for the detail in the type is that it is useful to be able to
sequence programs with a different ``Path``, but in doing so, we must
calculate the resulting ``Path`` accurately.
Then, if we want to sequence subprograms with linear variables,
we can use an alternative bind operator which guarantees to run the
continuation exactly once:
.. code-block:: idris
bindL : App {l=NoThrow} e a ->
(1 k : a -> App {l} e b) -> App {l} e b
To illustrate the need for ``bindL``, we can try writing a program which
tracks the state of a secure data store, which requires logging in before
reading the data.
Example: a data store requiring a login
---------------------------------------
Many software components rely on some form of state, and there may be
operations which are only valid in specific states. For example, consider
a secure data store in which a user must log in before getting access to
some secret data. This system can be in one of two states:
* ``LoggedIn``, in which the user is allowed to read the secret
* ``LoggedOut``, in which the user has no access to the secret
We can provide commands to log in, log out, and read the data, as illustrated
in the following diagram:
|login|
The ``login`` command, if it succeeds, moves the overall system state from
``LoggedOut`` to ``LoggedIn``. The ``logout`` command moves the state from
``LoggedIn`` to ``LoggedOut``. Most importantly, the ``readSecret`` command
is only valid when the system is in the ``LoggedIn`` state.
We can represent the state transitions using functions with linear types.
To begin, we define an interface for connecting to and disconnecting from
a store:
.. code-block:: idris
interface StoreI e where
connect : (1 prog : (1 d : Store LoggedOut) ->
App {l} e ()) -> App {l} e ()
disconnect : (1 d : Store LoggedOut) -> App {l} e ()
Neither ``connect`` nor ``disconnect`` throw, as shown by
generalising over ``l``. Once we
have a connection, we can use the following functions to
access the resource directly:
.. code-block:: idris
data Res : (a : Type) -> (a -> Type) -> Type where
(@@) : (val : a) -> (1 resource : r val) -> Res a r
login : (1 s : Store LoggedOut) -> (password : String) ->
Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
logout : (1 s : Store LoggedIn) -> Store LoggedOut
readSecret : (1 s : Store LoggedIn) ->
Res String (const (Store LoggedIn))
``Res`` is defined in ``Control.App`` since it is commonly useful. It is a
dependent pair type, which associates a value with a linear resource.
We'll leave the other definitions abstract, for the purposes of this
introductory example.
The following listing shows a complete program accessing the store, which
reads a password, accesses the store if the password is correct and prints the
secret data. It uses ``let (>>=) = bindL`` to redefine
``do``-notation locally.
.. code-block:: idris
storeProg : Has [Console, StoreI] e => App e ()
storeProg = let (>>=) = bindL in
do putStr "Password: "
password <- getStr
connect $ \s =>
do let True @@ s = login s password
| False @@ s => do putStrLn "Wrong password"
disconnect s
let str @@ s = readSecret s
putStrLn $ "Secret: " ++ show str
let s = logout s
disconnect s
If we omit the ``let (>>=) = bindL``, it will use the default
``(>>=)`` operator, which allows the continuation to be run multiple
times, which would mean that ``s`` is not guaranteed to be accessed
linearly, and ``storeProg`` would not type check.
We can safely use ``getStr`` and ``putStr`` because they
are guaranteed not to throw by the ``Path`` parameter in their types.
.. |login| image:: ../image/login.png
:width: 500px
App1: Linear Interfaces
-----------------------
Adding the ``bindL`` function to allow locally rebinding the
``(>>=)`` operator allows us to combine existing linear resource
programs with operations in ``App`` - at least, those that don't throw.
It would nevertheless be nice to interoperate more directly with ``App``.
One advantage of defining interfaces is that we can provide multiple
implementations for different contexts, but our implementation of the
data store uses primitive functions (which we left undefined in any case)
to access the store.
To allow control over linear resources, ``Control.App`` provides an alternative
parameterised type ``App1``:
.. code-block:: idris
data App1 : {default One u : Usage} ->
(e : Environment) -> Type -> Type
There is no need for a ``Path`` argument, since linear programs can
never throw. The ``Usage`` argument states whether the value
returned is to be used once, or has unrestricted usage, with
the default in ``App1`` being to use once:
.. code-block:: idris
data Usage = One | Any
The main difference from ``App`` is the ``(>>=)`` operator, which
has a different multiplicity for the variable bound by the continuation
depending on the usage of the first action:
.. code-block:: idris
Cont1Type : Usage -> Type -> Usage -> Environment ->
Type -> Type
Cont1Type One a u e b = (1 x : a) -> App1 {u} e b
Cont1Type Any a u e b = (x : a) -> App1 {u} e b
(>>=) : {u : _} -> (1 act : App1 {u} e a) ->
(1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b
``Cont1Type`` returns a continuation which uses the argument linearly,
if the first ``App1`` program has usage ``One``, otherwise it
returns a continuation where argument usage is unrestricted. Either way,
because there may be linear resources in scope, the continuation is
run exactly once and there can be no exceptions thrown.
Using ``App1``, we can define all of the data store operations in a
single interface, as shown in the following listing.
Each operation other than ``disconnect`` returns a `linear` resource.
.. code-block:: idris
interface StoreI e where
connect : App1 e (Store LoggedOut)
login : (1 d : Store LoggedOut) -> (password : String) ->
App1 e (Res Bool (\ok => Store (if ok then LoggedIn
else LoggedOut))
logout : (1 d : Store LoggedIn) -> App1 e (Store LoggedOut)
readSecret : (1 d : Store LoggedIn) ->
App1 e (Res String (const (Store LoggedIn)))
disconnect : (1 d : Store LoggedOut) -> App {l} e ()
We can explicitly move between ``App`` and ``App1``:
.. code-block:: idris
app : (1 p : App {l=NoThrow} e a) -> App1 {u=Any} e a
app1 : (1 p : App1 {u=Any} e a) -> App {l} e a
We can run an ``App`` program using ``app``, inside ``App1``,
provided that it is guaranteed not to throw. Similarly, we can run an
``App1`` program using ``app1``, inside ``App``, provided that
the value it returns has unrestricted usage. So, for example, we can
write:
.. code-block:: idris
storeProg : Has [Console, StoreI] e => App e ()
storeProg = app1 $ do
store <- connect
app $ putStr "Password: "
?what_next
This uses ``app1`` to state that the body of the program is linear,
then ``app`` to state that the ``putStr`` operation is in
``App``. We can see that ``connect`` returns a linear resource
by inspecting the hole ``what_next``, which also shows that we are
running inside ``App1``:
.. code-block:: idris
0 e : List Type
1 store : Store LoggedOut
-------------------------------------
what_next : App1 e ()
For completeness, one way to implement the interface is as follows, with
hard coded password and internal data:
.. code-block:: idris
Has [Console] e => StoreI e where
connect
= do app $ putStrLn "Connect"
pure1 (MkStore "xyzzy")
login (MkStore str) pwd
= if pwd == "Mornington Crescent"
then pure1 (True @@ MkStore str)
else pure1 (False @@ MkStore str)
logout (MkStore str) = pure1 (MkStore str)
readSecret (MkStore str) = pure1 (str @@ MkStore str)
disconnect (MkStore _)
= putStrLn "Door destroyed"
Then we can run it in ``main``:
.. code-block:: idris
main : IO ()
main = run storeProg

3
docs/source/backends/index.rst
View File

@ -37,7 +37,7 @@ You can also execute expressions directly:
Again, ``expr`` must have type ``IO ()``.
Finally, you can compile to an exectuable from the command line by adding
Finally, you can compile to an executable from the command line by adding
the ``-o <output file>`` option:
::
@ -60,4 +60,3 @@ or via the `IDRIS2_CG` environment variable.
chez
racket
gambit

2
docs/source/faq/faq.rst
View File

@ -57,5 +57,5 @@ You can find more details in Section :ref:`updates-index`.
Where can I find more answers?
==============================
The `Idris 1 FAQ <http://docs.idris-lang.org/en/latest/faq/faq.html>`_ is
The `Idris 1 FAQ <https://docs.idris-lang.org/en/latest/faq/faq.html>`_ is
mostly still relevant.

BIN
docs/source/image/login.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 9.9 KiB

10
docs/source/tutorial/conclusions.rst
View File

@ -10,7 +10,7 @@ dependent types in general, can be obtained from various sources:
* `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
by Edwin Brady, available from `Manning <https://www.manning.com>`_.
* The Idris web site (http://www.idris-lang.org/) and by asking
* The Idris web site (https://www.idris-lang.org/) and by asking
questions on the mailing list.
* The IRC channel ``#idris``, on
@ -30,7 +30,7 @@ dependent types in general, can be obtained from various sources:
* Existing projects on the ``Idris Hackers`` web space:
* http://idris-hackers.github.io.
* https://idris-hackers.github.io.
* Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_). Although these mostly
describe older versions of Idris.
@ -41,14 +41,14 @@ dependent types in general, can be obtained from various sources:
Aspects of Declarative Languages (PADL'12), Claudio Russo and
Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
242-257. DOI=10.1007/978-3-642-27694-1_18
http://dx.doi.org/10.1007/978-3-642-27694-1_18
https://dx.doi.org/10.1007/978-3-642-27694-1_18
.. [#Brady] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
dependent types. In Proceedings of the 5th ACM workshop on
Programming languages meets program verification (PLPV
'11). ACM, New York, NY, USA,
43-54. DOI=10.1145/1929529.1929536
http://doi.acm.org/10.1145/1929529.1929536
https://doi.acm.org/10.1145/1929529.1929536
.. [#BradyHammond2010] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
inefficient engine: using partial evaluation to improve
@ -56,4 +56,4 @@ dependent types in general, can be obtained from various sources:
15th ACM SIGPLAN international conference on Functional
programming (ICFP '10). ACM, New York, NY, USA,
297-308. DOI=10.1145/1863543.1863587
http://doi.acm.org/10.1145/1863543.1863587
https://doi.acm.org/10.1145/1863543.1863587

2
docs/source/tutorial/interactive.rst
View File

@ -252,5 +252,5 @@ for other editors can be added in a relatively straightforward manner
by using ``idris2 -–client``.
More sophisticated support can be added by using the IDE protocol (yet to
be documented for Idris 2, but which mostly extends to protocol documented for
`Idris 1 <http://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.
`Idris 1 <https://docs.idris-lang.org/en/latest/reference/ide-protocol.html>`_.

2
docs/source/tutorial/interfaces.rst
View File

@ -658,4 +658,4 @@ parameter used to find an implementation.
.. [#ConorRoss] Conor McBride and Ross Paterson. 2008. Applicative programming
with effects. J. Funct. Program. 18, 1 (January 2008),
1-13. DOI=10.1017/S0956796807006326
http://dx.doi.org/10.1017/S0956796807006326
https://dx.doi.org/10.1017/S0956796807006326

4
docs/source/tutorial/introduction.rst
View File

@ -6,7 +6,7 @@ Introduction
In conventional programming languages, there is a clear distinction
between *types* and *values*. For example, in `Haskell
<http://www.haskell.org>`_, the following are types, representing
<https://www.haskell.org>`_, the following are types, representing
integers, characters, lists of characters, and lists of any value
respectively:
@ -49,7 +49,7 @@ Intended Audience
This tutorial is intended as a brief introduction to the language, and
is aimed at readers already familiar with a functional language such
as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
as `Haskell <https://www.haskell.org>`_ or `OCaml <https://ocaml.org>`_.
In particular, a certain amount of familiarity with Haskell syntax is
assumed, although most concepts will at least be explained
briefly. The reader is also assumed to have some interest in using

2
docs/source/tutorial/miscellany.rst
View File

@ -136,7 +136,7 @@ But what about the type of ``Type``? If we ask Idris it reports:
Type : Type 1
If ``Type`` were its own type, it would lead to an inconsistency due to
`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
`Girard’s paradox <https://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
so internally there is a *hierarchy* of types (or *universes*):
.. code-block:: idris

22
docs/source/tutorial/multiplicities.rst
View File

@ -109,7 +109,17 @@ If we use ``x`` for one part of the pair...
-------------------------------------
help : a
The same happens if we try defining ``duplicate x = (?help, x)`` (try it!)
The same happens if we try defining ``duplicate x = (?help, x)`` (try it!).
In order to avoid parsing ambiguities, if you give an explicit multiplicity
for a variable as with the argument to ``duplicate``, you need to give it
a name too. But, if the name isn't used in the scope of the type, you
can use ``_`` instead of a name, as follows:
.. code-block:: idris
duplicate : (1 _ : a) -> (a, a)
The intution behind multiplicity ``1`` is that if we have a function with
a type of the following form...
@ -135,10 +145,10 @@ wraps an argument with unrestricted use
.. code-block:: idris
data Lin : Type -> Type where
MkLin : (1 x : a) -> Lin a
MkLin : (1 _ : a) -> Lin a
data Unr : Type -> Type where
MkUnr : (x : a) -> Unr a
MkUnr : a -> Unr a
If ``MkLin x`` is used once, then ``x`` is used once. But if ``MkUnr x`` is
used once, there is no guarantee on how often ``x`` is used. We can see this a
@ -147,10 +157,10 @@ bit more clearly by starting to write projection functions for ``Lin`` and
.. code-block:: idris
getLin : (1 val : Lin a) -> a
getLin : (1 _ : Lin a) -> a
getLin (MkLin x) = ?howmanyLin
getUnr : (1 val : Unr a) -> a
getUnr : (1 _ : Unr a) -> a
getUnr (MkUnr x) = ?howmanyUnr
Checking the types of the holes shows us that, for ``getLin``, we must use
@ -178,7 +188,7 @@ If ``getLin`` has an unrestricted argument...
.. code-block:: idris
getLin : (val : Lin a) -> a
getLin : Lin a -> a
getLin (MkLin x) = ?howmanyLin
...then ``x`` is unrestricted in ``howmanyLin``::

8
docs/source/tutorial/starting.rst
View File

@ -40,9 +40,11 @@ follows::
make bootstrap-racket
This will, by default, install into ``${HOME}/.idris2``. You can change this
by editing the options in ``config.mk``. For example,
to install into ``/usr/local``, you can edit the ``PREFIX`` as follows::
Once you've successfully bootstrapped with any of the above commands, you can
install with the command ``make install``. This will, by default, install into
``${HOME}/.idris2``. You can change this by editing the options in
``config.mk``. For example, to install into ``/usr/local``, you can edit the
``PREFIX`` as follows::
PREFIX ?= /usr/local

2
docs/source/tutorial/theorems.rst
View File

@ -456,4 +456,4 @@ argument.
control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
symposium on Principles of programming languages (POPL
'90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
http://doi.acm.org/10.1145/96709.96714
https://doi.acm.org/10.1145/96709.96714

2
docs/source/tutorial/typesfuns.rst
View File

@ -20,7 +20,7 @@ into the Idris interactive environment by typing ``idris2 Prims.idr``:
module Prims
x : Int
x = 42
x = 94
foo : String
foo = "Sausage machine"

3
docs/source/updates/updates.rst
View File

@ -334,6 +334,9 @@ There are several ``%language`` pragmas in Idris 1, which define various
experimental extensions. None of these are available in Idris 2, although
extensions may be defined in the future.
Also removed was the ``%access`` pragma for default visibility, use visibility
modifiers on each declaration instead.
``let`` bindings
----------------

2
idris2.ipkg
View File

@ -69,6 +69,7 @@ modules =
Idris.IDEMode.Parser,
Idris.IDEMode.REPL,
Idris.IDEMode.TokenLine,
Idris.IDEMode.Holes,
Idris.ModTree,
Idris.Package,
Idris.Parser,
@ -145,6 +146,7 @@ modules =
Utils.Octal,
Utils.Shunting,
Utils.String,
Utils.Path,
Yaffle.Main,
Yaffle.REPL

3
idris2api.ipkg
View File

@ -50,6 +50,7 @@ modules =
Data.Bool.Extra,
Data.IntMap,
Data.LengthMatch,
Data.List.Extra,
Data.NameMap,
Data.StringMap,
Data.These,
@ -68,6 +69,7 @@ modules =
Idris.IDEMode.Parser,
Idris.IDEMode.REPL,
Idris.IDEMode.TokenLine,
Idris.IDEMode.Holes,
Idris.ModTree,
Idris.Package,
Idris.Parser,
@ -144,6 +146,7 @@ modules =
Utils.Octal,
Utils.Shunting,
Utils.String,
Utils.Path,
Yaffle.Main,
Yaffle.REPL

2
libs/base/Data/Fin.idr
View File

@ -1,6 +1,6 @@
module Data.Fin
import Data.Maybe
import public Data.Maybe
import Data.Nat
import Decidable.Equality

6
libs/base/Data/List.idr
View File

@ -56,6 +56,12 @@ filter p (x :: xs)
then x :: filter p xs
else filter p xs
||| Find the first element of the list that satisfies the predicate.
public export
find : (p : a -> Bool) -> (xs : List a) -> Maybe a
find p [] = Nothing
find p (x::xs) = if p x then Just x else find p xs
||| Find associated information in a list using a custom comparison.
public export
lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b

80
libs/base/Data/List/Quantifiers.idr Normal file
View File

@ -0,0 +1,80 @@
module Data.List.Quantifiers
import Data.List
import Data.List.Elem
||| A proof that some element of a list satisfies some property
|||
||| @ p the property to be satisfied
public export
data Any : (0 p : a -> Type) -> List a -> Type where
||| A proof that the satisfying element is the first one in the `List`
Here : {0 xs : List a} -> p x -> Any p (x :: xs)
||| A proof that the satisfying element is in the tail of the `List`
There : {0 xs : List a} -> Any p xs -> Any p (x :: xs)
export
Uninhabited (Any p Nil) where
uninhabited (Here _) impossible
uninhabited (There _) impossible
||| Given a decision procedure for a property, determine if an element of a
||| list satisfies it.
|||
||| @ p the property to be satisfied
||| @ dec the decision procedure
||| @ xs the list to examine
export
any : (dec : (x : a) -> Dec (p x)) -> (xs : List a) -> Dec (Any p xs)
any _ Nil = No uninhabited
any p (x::xs) with (p x)
any p (x::xs) | Yes prf = Yes (Here prf)
any p (x::xs) | No ctra =
case any p xs of
Yes prf' => Yes (There prf')
No ctra' => No $ \case
Here px => ctra px
There pxs => ctra' pxs
||| A proof that all elements of a list satisfy a property. It is a list of
||| proofs, corresponding element-wise to the `List`.
public export
data All : (0 p : a -> Type) -> List a -> Type where
Nil : All p Nil
(::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs)
||| Given a decision procedure for a property, decide whether all elements of
||| a list satisfy it.
|||
||| @ p the property
||| @ dec the decision procedure
||| @ xs the list to examine
export
all : (dec : (x : a) -> Dec (p x)) -> (xs : List a) -> Dec (All p xs)
all _ Nil = Yes Nil
all d (x::xs) with (d x)
all d (x::xs) | No ctra = No $ \(p::_) => ctra p
all d (x::xs) | Yes prf =
case all d xs of
Yes prf' => Yes (prf :: prf')
No ctra' => No $ \(_::ps) => ctra' ps
||| If there does not exist an element that satifies the property, then it is
||| the case that all elements do not satisfy it.
export
negAnyAll : {xs : List a} -> Not (Any p xs) -> All (Not . p) xs
negAnyAll {xs=Nil} _ = Nil
negAnyAll {xs=x::xs} f = (f . Here) :: negAnyAll (f . There)
||| If there exists an element that doesn't satify the property, then it is
||| not the case that all elements satisfy it.
export
anyNegAll : Any (Not . p) xs -> Not (All p xs)
anyNegAll (Here ctra) (p::_) = ctra p
anyNegAll (There np) (_::ps) = anyNegAll np ps
||| Given a proof of membership for some element, extract the property proof for it
export
indexAll : Elem x xs -> All p xs -> p x
indexAll Here (p::_ ) = p
indexAll (There e) ( _::ps) = indexAll e ps

1
libs/base/Data/List/Views.idr
View File

@ -2,6 +2,7 @@ module Data.List.Views
import Control.WellFounded
import Data.List
import Data.Nat
import Data.Nat.Views
lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->

1
libs/base/Data/Nat/Views.idr
View File

@ -1,6 +1,7 @@
module Data.Nat.Views
import Control.WellFounded
import Data.Nat
||| View for dividing a Nat in half
public export

2
libs/base/System.idr
View File

@ -1,6 +1,6 @@
module System
import Data.So
import public Data.So
import Data.List
import Data.Strings

16
libs/base/System/File.idr
View File

@ -38,6 +38,10 @@ prim__writeLine : FilePtr -> String -> PrimIO Int
prim__eof : FilePtr -> PrimIO Int
%foreign "C:fflush,libc 6"
prim__flush : FilePtr -> PrimIO Int
%foreign support "idris2_popen"
prim__popen : String -> String -> PrimIO FilePtr
%foreign support "idris2_pclose"
prim__pclose : FilePtr -> PrimIO ()
%foreign support "idris2_removeFile"
prim__removeFile : String -> PrimIO Int
@ -185,6 +189,18 @@ fflush (FHandle f)
= do primIO (prim__flush f)
pure ()
export
popen : String -> Mode -> IO (Either FileError File)
popen f m = do
ptr <- primIO (prim__popen f (modeStr m))
if prim__nullAnyPtr ptr /= 0
then returnError
else pure (Right (FHandle ptr))
export
pclose : File -> IO ()
pclose (FHandle h) = primIO (prim__pclose h)
export
fileAccessTime : (h : File) -> IO (Either FileError Int)
fileAccessTime (FHandle f)

4
libs/base/System/Info.idr
View File

@ -10,3 +10,7 @@ os = prim__os
export
codegen : String
codegen = prim__codegen
export
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]

1
libs/base/base.ipkg
View File

@ -17,6 +17,7 @@ modules = Control.App,
Data.List,
Data.List.Elem,
Data.List.Views,
Data.List.Quantifiers,
Data.Maybe,
Data.Morphisms,
Data.Nat,

2
libs/contrib/Data/String/Extra.idr
View File

@ -1,5 +1,7 @@
module Data.String.Extra
import Data.List
import Data.Nat
import Data.Strings
%default total

1
libs/contrib/Language/JSON/String/Lexer.idr
View File

@ -1,5 +1,6 @@
module Language.JSON.String.Lexer
import Data.Nat
import Language.JSON.String.Tokens
import Text.Lexer

6
libs/contrib/System/Path.idr
View File

@ -1,7 +1,9 @@
module System.Path
import Control.Delayed
import Data.List
import Data.Maybe
import Data.Nat
import Data.Strings
import Data.String.Extra
import System.Info
@ -10,10 +12,6 @@ import Text.Lexer
import Text.Parser
import Text.Quantity
private
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
||| The character that separates directories in the path.
export
dirSeparator : Char

15
libs/prelude/Prelude.idr
View File

@ -3,6 +3,8 @@ module Prelude
import public Builtin
import public PrimIO
%default total
{-
The Prelude is minimal (since it is effectively part of the language
specification, this seems to be desirable - we should, nevertheless, aim to
@ -632,11 +634,23 @@ public export
sum : (Foldable t, Num a) => t a -> a
sum = foldr (+) 0
||| Add together all the elements of a structure.
||| Same as `sum` but tail recursive.
export
sum' : (Foldable t, Num a) => t a -> a
sum' = foldl (+) 0
||| Multiply together all elements of a structure.
public export
product : (Foldable t, Num a) => t a -> a
product = foldr (*) 1
||| Multiply together all elements of a structure.
||| Same as `product` but tail recursive.
export
product' : (Foldable t, Num a) => t a -> a
product' = foldl (*) 1
||| Map each element of a structure to a computation, evaluate those
||| computations and discard the results.
public export
@ -1427,6 +1441,7 @@ public export
Functor IO where
map f io = io_bind io (\b => io_pure (f b))
%inline
public export
Applicative IO where
pure x = io_pure x

2
src/Algebra.idr
View File

@ -4,6 +4,8 @@ import public Algebra.ZeroOneOmega
import public Algebra.Semiring
import public Algebra.Preorder
%default total
public export
RigCount : Type
RigCount = ZeroOneOmega

2
src/Algebra/Preorder.idr
View File

@ -1,5 +1,7 @@
module Algebra.Preorder
%default total
||| Preorder defines a binary relation using the `<=` operator
public export
interface Preorder a where

2
src/Algebra/ZeroOneOmega.idr
View File

@ -3,6 +3,8 @@ module Algebra.ZeroOneOmega
import Algebra.Semiring
import Algebra.Preorder
%default total
export
data ZeroOneOmega = Rig0 | Rig1 | RigW

2
src/Compiler/Common.idr
View File

@ -22,6 +22,8 @@ import System.Directory
import System.Info
import System.File
%default covering
||| Generic interface to some code generator
public export
record Codegen where

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

@ -11,13 +11,17 @@ import Core.Name
import Core.Options
import Core.TT
import Utils.Hex
import Utils.Path
import Data.List
import Data.Maybe
import Data.NameMap
import Data.Strings
import Data.Vect
import System
import System.Directory
import System.File
import System.Info
%default covering
@ -26,7 +30,7 @@ import System.Info
pathLookup : IO String
pathLookup
= do path <- getEnv "PATH"
let pathList = split (== pathSep) $ fromMaybe "/usr/bin:/usr/local/bin" path
let pathList = split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
let candidates = [p ++ "/" ++ x | p <- pathList,
x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
e <- firstExists candidates
@ -181,7 +185,7 @@ cCall appdir fc cfn clib args ret
lib <- if clib `elem` loaded
then pure ""
else do (fname, fullname) <- locate clib
copyLib (appdir ++ dirSep ++ fname, fullname)
copyLib (appdir </> fname, fullname)
put Loaded (clib :: loaded)
pure $ "(load-shared-object \""
++ escapeString fname
@ -369,7 +373,7 @@ compileToSS c appdir tm outfile
compileToSO : {auto c : Ref Ctxt Defs} ->
String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
compileToSO chez appDirRel outSsAbs
= do let tmpFileAbs = appDirRel ++ dirSep ++ "compileChez"
= do let tmpFileAbs = appDirRel </> "compileChez"
let build= "(parameterize ([optimize-level 3]) (compile-program " ++
show outSsAbs ++ "))"
Right () <- coreLift $ writeFile tmpFileAbs build
@ -399,18 +403,18 @@ compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c execDir tm outfile
= do let appDirRel = outfile ++ "_app" -- relative to build dir
let appDirGen = execDir ++ dirSep ++ appDirRel -- relative to here
coreLift $ mkdirs (splitDir appDirGen)
let appDirGen = execDir </> appDirRel -- relative to here
coreLift $ mkdirAll appDirGen
Just cwd <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
let outSsFile = appDirRel ++ dirSep ++ outfile ++ ".ss"
let outSoFile = appDirRel ++ dirSep ++ outfile ++ ".so"
let outSsAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSsFile
let outSoAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSoFile
let outSsFile = appDirRel </> outfile <.> "ss"
let outSoFile = appDirRel </> outfile <.> "so"
let outSsAbs = cwd </> execDir </> outSsFile
let outSoAbs = cwd </> execDir </> outSoFile
chez <- coreLift $ findChez
compileToSS c appDirGen tm outSsAbs
logTime "Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
let outShRel = execDir ++ dirSep ++ outfile
let outShRel = execDir </> outfile
if isWindows
then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)
else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)

10
src/Compiler/Scheme/Gambit.idr
View File

@ -11,13 +11,17 @@ import Core.Name
import Core.Options
import Core.TT
import Utils.Hex
import Utils.Path
import Data.List
import Data.Maybe
import Data.NameMap
import Data.Strings
import Data.Vect
import System
import System.Directory
import System.File
import System.Info
%default covering
@ -292,16 +296,16 @@ compileToSCM c tm outfile
compileExpr : Ref Ctxt Defs -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr c execDir tm outfile
= do let outn = execDir ++ dirSep ++ outfile ++ ".scm"
= do let outn = execDir </> outfile <.> "scm"
libsname <- compileToSCM c tm outn
libsfile <- traverse findLibraryFile $ nub $ map (++ ".a") libsname
libsfile <- traverse findLibraryFile $ map (<.> "a") (nub libsname)
gsc <- coreLift findGSC
let cmd = gsc ++
" -exe -cc-options \"-Wno-implicit-function-declaration\" -ld-options \"" ++
(showSep " " libsfile) ++ "\" " ++ outn
ok <- coreLift $ system cmd
if ok == 0
then pure (Just (execDir ++ dirSep ++ outfile))
then pure (Just (execDir </> outfile))
else pure Nothing
executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()

20
src/Compiler/Scheme/Racket.idr
View File

@ -11,6 +11,7 @@ import Core.Directory
import Core.Name
import Core.TT
import Utils.Hex
import Utils.Path
import Data.List
import Data.Maybe
@ -18,7 +19,10 @@ import Data.NameMap
import Data.Nat
import Data.Strings
import Data.Vect
import System
import System.Directory
import System.File
import System.Info
%default covering
@ -163,7 +167,7 @@ cCall appdir fc cfn libspec args ret
then pure ""
else do put Loaded (libn :: loaded)
(fname, fullname) <- locate libspec
copyLib (appdir ++ dirSep ++ fname, fullname)
copyLib (appdir </> fname, fullname)
pure (loadlib libn vers)
argTypes <- traverse (\a => do s <- cftySpec fc (snd a)
@ -363,16 +367,16 @@ compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr mkexec c execDir tm outfile
= do let appDirRel = outfile ++ "_app" -- relative to build dir
let appDirGen = execDir ++ dirSep ++ appDirRel -- relative to here
coreLift $ mkdirs (splitDir appDirGen)
let appDirGen = execDir </> appDirRel -- relative to here
coreLift $ mkdirAll appDirGen
Just cwd <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
let ext = if isWindows then ".exe" else ""
let outRktFile = appDirRel ++ dirSep ++ outfile ++ ".rkt"
let outBinFile = appDirRel ++ dirSep ++ outfile ++ ext
let outRktAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outRktFile
let outBinAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outBinFile
let outRktFile = appDirRel </> outfile <.> "rkt"
let outBinFile = appDirRel </> outfile <.> ext
let outRktAbs = cwd </> execDir </> outRktFile
let outBinAbs = cwd </> execDir </> outBinFile
compileToRKT c appDirGen tm outRktAbs
raco <- coreLift findRacoExe
@ -385,7 +389,7 @@ compileExpr mkexec c execDir tm outfile
else pure 0
if ok == 0
then do -- TODO: add launcher script
let outShRel = execDir ++ dirSep ++ outfile
let outShRel = execDir </> outfile
the (Core ()) $ if isWindows
then if mkexec
then makeShWindows "" outShRel appDirRel outBinFile

18
src/Core/Binary.idr
View File

@ -13,6 +13,8 @@ import Data.IntMap
import Data.List
import Data.NameMap
import System.File
-- Reading and writing 'Defs' from/to a binary file
-- In order to be saved, a name must have been flagged using 'toSave'.
-- (Otherwise we'd save out everything, not just the things in the current
@ -28,7 +30,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 29
ttcVersion = 31
export
checkTTCVersion : String -> Int -> Int -> Core ()
@ -322,7 +324,11 @@ addTypeHint fc (tyn, hintn, d)
addAutoHint : {auto c : Ref Ctxt Defs} ->
(Name, Bool) -> Core ()
addAutoHint (hintn, d) = addGlobalHint hintn d
addAutoHint (hintn_in, d)
= do defs <- get Ctxt
hintn <- toResolvedNames hintn_in
put Ctxt (record { autoHints $= insert hintn d } defs)
export
updatePair : {auto c : Ref Ctxt Defs} ->
@ -400,13 +406,15 @@ export
readFromTTC : TTC extra =>
{auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
FC -> Bool ->
Bool -> -- set nested namespaces (for records, to use at the REPL)
FC ->
Bool -> -- importing as public
(fname : String) -> -- file containing the module
(modNS : List String) -> -- module namespace
(importAs : List String) -> -- namespace to import as
Core (Maybe (extra, Int,
List (List String, Bool, List String)))
readFromTTC loc reexp fname modNS importAs
readFromTTC nestedns loc reexp fname modNS importAs
= do defs <- get Ctxt
-- If it's already in the context, with the same visibility flag,
-- don't load it again (we do need to load it again if it's visible
@ -434,7 +442,7 @@ readFromTTC loc reexp fname modNS importAs
traverse (addGlobalDef modNS as) (context ttc)
traverse_ addUserHole (userHoles ttc)
setNS (currentNS ttc)
setNestedNS (nestedNS ttc)
when nestedns $ setNestedNS (nestedNS ttc)
-- Set up typeHints and autoHints based on the loaded data
traverse_ (addTypeHint loc) (typeHints ttc)
traverse_ addAutoHint (autoHints ttc)

16
src/Core/Context.idr
View File

@ -149,6 +149,11 @@ data Clause : Type where
(env : Env Term vars) ->
(lhs : Term vars) -> (rhs : Term vars) -> Clause
export
Show Clause where
show (MkClause {vars} env lhs rhs)
= show vars ++ ": " ++ show lhs ++ " = " ++ show rhs
public export
data DefFlag
= Inline
@ -208,6 +213,13 @@ Show SizeChange where
show Same = "Same"
show Unknown = "Unknown"
export
Eq SizeChange where
Smaller == Smaller = True
Same == Same = True
Unknown == Unknown = True
_ == _ = False
public export
record SCCall where
constructor MkSCCall
@ -222,6 +234,10 @@ export
Show SCCall where
show c = show (fnCall c) ++ ": " ++ show (fnArgs c)
export
Eq SCCall where
x == y = fnCall x == fnCall y && fnArgs x == fnArgs y
public export
record GlobalDef where
constructor MkGlobalDef

1
src/Core/Core.idr
View File

@ -8,6 +8,7 @@ import Parser.Source
import public Data.IORef
import System
import System.File
%default covering

160
src/Core/Directory.idr
View File

@ -5,27 +5,17 @@ import Core.Core
import Core.FC
import Core.Name
import Core.Options
import Utils.Path
import Data.List
import Data.Strings
import Data.Maybe
import System.Directory
import System.File
import System.Info
%default covering
fullPath : String -> List String
fullPath fp = filter (/="") $ split (==sep) fp
dropExtension : String -> String
dropExtension fname
= case span (/= '.') (reverse fname) of
(all, "") => -- no extension
reverse all
(ext, root) =>
-- assert that root can't be empty
reverse (assert_total (strTail root))
%default total
-- Return the name of the first file available in the list
firstAvailable : List String -> Core (Maybe String)
@ -37,11 +27,12 @@ firstAvailable (f :: fs)
pure (Just f)
export
covering
readDataFile : {auto c : Ref Ctxt Defs} ->
String -> Core String
readDataFile fname
= do d <- getDirs
let fs = map (\p => p ++ dirSep ++ fname) (data_dirs d)
let fs = map (\p => p </> fname) (data_dirs d)
Just f <- firstAvailable fs
| Nothing => throw (InternalError ("Can't find data file " ++ fname ++
" in any of " ++ show fs))
@ -57,8 +48,8 @@ findLibraryFile : {auto c : Ref Ctxt Defs} ->
String -> Core String
findLibraryFile fname
= do d <- getDirs
let fs = map (\p => p ++ dirSep ++ fname)
(lib_dirs d ++ map (\x => x ++ dirSep ++ "lib")
let fs = map (\p => p </> fname)
(lib_dirs d ++ map (\x => x </> "lib")
(extra_dirs d))
Just f <- firstAvailable fs
| Nothing => throw (InternalError ("Can't find library " ++ fname))
@ -71,9 +62,9 @@ nsToPath : {auto c : Ref Ctxt Defs} ->
FC -> List String -> Core (Either Error String)
nsToPath loc ns
= do d <- getDirs
let fnameBase = showSep dirSep (reverse ns)
let fs = map (\p => p ++ dirSep ++ fnameBase ++ ".ttc")
((build_dir d ++ dirSep ++ "ttc") :: extra_dirs d)
let fnameBase = joinPath (reverse ns)
let fs = map (\p => p </> fnameBase <.> "ttc")
((build_dir d </> "ttc") :: extra_dirs d)
Just f <- firstAvailable fs
| Nothing => pure (Left (ModuleNotFound loc ns))
pure (Right f)
@ -85,9 +76,9 @@ nsToSource : {auto c : Ref Ctxt Defs} ->
FC -> List String -> Core String
nsToSource loc ns
= do d <- getDirs
let fnameOrig = showSep dirSep (reverse ns)
let fnameBase = maybe fnameOrig (\srcdir => srcdir ++ dirSep ++ fnameOrig) (source_dir d)
let fs = map (\ext => fnameBase ++ ext)
let fnameOrig = joinPath (reverse ns)
let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
let fs = map (\ext => fnameBase <.> ext)
[".idr", ".lidr", ".yaff", ".org", ".md"]
Just f <- firstAvailable fs
| Nothing => throw (ModuleNotFound loc ns)
@ -98,75 +89,53 @@ nsToSource loc ns
export
pathToNS : String -> Maybe String -> String -> List String
pathToNS wdir sdir fname
= let wsplit = splitSep wdir
ssplit = maybe [] splitSep sdir
fsplit = splitSep fname
wdrop = dropDir wsplit fsplit fsplit
in
dropDir ssplit wdrop wdrop
where
dropDir : List String -> List String -> List String -> List String
dropDir dir orig [] = []
dropDir dir orig (x :: xs)
= if dir == xs
then [x]
else x :: dropDir dir orig xs
= let sdir = fromMaybe "" sdir in
case stripPrefix sdir fname of
Nothing => []
Just p => map show $ reverse $ (parse (p <.> "")).body
splitSep : String -> List String
splitSep fname
= case span (/=sep) fname of
(end, "") => [dropExtension end]
(mod, rest) => assert_total (splitSep (strTail rest)) ++ [mod]
dirExists : String -> IO Bool
dirExists dir = do Right d <- openDir dir
| Left _ => pure False
closeDir d
pure True
-- Create subdirectories, if they don't exist
export
mkdirs : List String -> IO (Either FileError ())
mkdirs [] = pure (Right ())
mkdirs ("." :: ds) = mkdirs ds
mkdirs ("" :: ds) = mkdirs ds
mkdirs (d :: ds)
= do ok <- changeDir d
if ok
then do mkdirs ds
changeDir ".."
pure (Right ())
else do Right _ <- createDir d
| Left err => pure (Left err)
ok <- changeDir d
mkdirs ds
changeDir ".."
pure (Right ())
isDirSep : Char -> Bool
isDirSep c = cast c == dirSep
export
splitDir : String -> List String
splitDir = split isDirSep
covering
mkdirAll : String -> IO (Either FileError ())
mkdirAll dir = if parse dir == emptyPath
then pure (Right ())
else do exist <- dirExists dir
if exist
then pure (Right ())
else do case parent dir of
Just parent => mkdirAll parent
Nothing => pure (Right ())
createDir dir
-- Given a namespace (i.e. a module name), make the build directory for the
-- corresponding ttc file
export
covering
makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
List String -> Core ()
makeBuildDirectory ns
= do d <- getDirs
let bdir = splitDir $ build_dir d
let ndirs = case ns of
[] => []
(n :: ns) => ns -- first item is file name
let fname = showSep dirSep (reverse ndirs)
Right _ <- coreLift $ mkdirs (bdir ++ "ttc" :: reverse ndirs)
| Left err => throw (FileErr (build_dir d ++ dirSep ++ fname) err)
let bdir = build_dir d </> "ttc"
let ns = reverse $ fromMaybe [] (tail' ns) -- first item is file name
let ndir = joinPath ns
Right _ <- coreLift $ mkdirAll (bdir </> ndir)
| Left err => throw (FileErr (build_dir d </> ndir) err)
pure ()
export
covering
makeExecDirectory : {auto c : Ref Ctxt Defs} ->
Core ()
makeExecDirectory
= do d <- getDirs
let edir = splitDir $ exec_dir d
Right _ <- coreLift $ mkdirs edir
Right _ <- coreLift $ mkdirAll (exec_dir d)
| Left err => throw (FileErr (exec_dir d) err)
pure ()
@ -180,16 +149,16 @@ getTTCFileName inp ext
-- Get its namespace from the file relative to the working directory
-- and generate the ttc file from that
let ns = pathToNS (working_dir d) (source_dir d) inp
let fname = showSep dirSep (reverse ns) ++ ext
let fname = joinPath (reverse ns) <.> ext
let bdir = build_dir d
pure $ bdir ++ dirSep ++ "ttc" ++ dirSep ++ fname
pure $ bdir </> "ttc" </> fname
-- Given a root executable name, return the name in the build directory
export
getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String
getExecFileName efile
= do d <- getDirs
pure $ build_dir d ++ dirSep ++ efile
pure $ build_dir d </> efile
getEntries : Directory -> IO (List String)
getEntries d
@ -206,42 +175,25 @@ dirEntries dir
closeDir d
pure (Right ds)
findIpkg : List String -> Maybe String
findIpkg [] = Nothing
findIpkg (f :: fs)
= if isSuffixOf ".ipkg" f
then Just f
else findIpkg fs
allDirs : String -> List String -> List (String, List String)
allDirs path [] = []
allDirs path ("" :: ds) = (dirSep, ds) ::allDirs path ds
allDirs "" (d :: ds)
= let d' = if isWindows then d ++ dirSep else strCons sep d in
(d', ds) :: allDirs d' ds
allDirs path (d :: ds)
= let d' = path ++ strCons sep d in
(d', ds) :: allDirs d' ds
-- Find an ipkg file in any of the directories above this one
-- returns the directory, the ipkg file name, and the directories we've
-- gone up
export
findIpkgFile : IO (Maybe (String, String, List String))
covering
findIpkgFile : IO (Maybe (String, String, String))
findIpkgFile
= do Just dir <- currentDir
| Nothing => pure Nothing
-- 'paths' are the paths to look for an .ipkg, in order
let paths = reverse (allDirs "" (splitDir dir))
res <- firstIpkg paths
res <- findIpkgFile' dir ""
pure res
where
firstIpkg : List (String, List String) ->
IO (Maybe (String, String, List String))
firstIpkg [] = pure Nothing
firstIpkg ((d, up) :: ds)
= do Right files <- dirEntries d
covering
findIpkgFile' : String -> String -> IO (Maybe (String, String, String))
findIpkgFile' dir up
= do Right files <- dirEntries dir
| Left err => pure Nothing
let Just f = findIpkg files
| Nothing => firstIpkg ds
pure $ Just (d, f, up)
let Just f = find (\f => extension f == Just "ipkg") files
| Nothing => case splitParent dir of
Just (parent, end) => findIpkgFile' parent (end </> up)
Nothing => pure Nothing
pure $ Just (dir, f, up)

4
src/Core/Env.idr
View File

@ -3,6 +3,8 @@ module Core.Env
import Core.TT
import Data.List
%default total
-- Environment containing types and values of local variables
public export
data Env : (tm : List Name -> Type) -> List Name -> Type where
@ -119,6 +121,8 @@ export
abstractFullEnvType : {vars : _} ->
FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
abstractFullEnvType fc [] tm = tm
abstractFullEnvType fc (Pi c e ty :: env) tm
= abstractFullEnvType fc env (Bind fc _ (Pi c e ty) tm)
abstractFullEnvType fc (b :: env) tm
= abstractFullEnvType fc env (Bind fc _
(Pi (multiplicity b) Explicit (binderType b)) tm)

2
src/Core/FC.idr
View File

@ -1,5 +1,7 @@
module Core.FC
%default total
public export
FilePos : Type
FilePos = (Int, Int)

17
src/Core/LinearCheck.idr
View File

@ -215,7 +215,9 @@ mutual
Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
| _ => throw (UndefinedName fc n)
let expand = branchZero
False
(case type gdef of
Erased _ _ => True -- defined elsewhere, need to expand
_ => False)
(case definition gdef of
(PMDef _ _ _ _ _) => True
_ => False)
@ -330,6 +332,13 @@ mutual
pure (App fc f' aerased,
glueBack defs env sc',
fused ++ aused)
NApp _ (NRef _ n) _ =>
do Just _ <- lookupCtxtExact n (gamma defs)
| _ => throw (UndefinedName fc n)
tfty <- getTerm gfty
throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++
" (" ++ show tfty ++ " not a function type)"))
_ => do tfty <- getTerm gfty
throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++
" (" ++ show tfty ++ " not a function type)"))
@ -567,14 +576,14 @@ mutual
lcheckDef fc rig True env n
= do defs <- get Ctxt
Just def <- lookupCtxtExact n (gamma defs)
| Nothing => throw (InternalError ("Linearity checking failed on " ++ show n))
| Nothing => throw (UndefinedName fc n)
pure (type def)
lcheckDef fc rig False env n
= do defs <- get Ctxt
let Just idx = getNameID n (gamma defs)
| Nothing => throw (InternalError ("Linearity checking failed on " ++ show n))
| Nothing => throw (UndefinedName fc n)
Just def <- lookupCtxtExact (Resolved idx) (gamma defs)
| Nothing => throw (InternalError ("Linearity checking failed on " ++ show n))
| Nothing => throw (UndefinedName fc n)
rigSafe (multiplicity def) rig
if linearChecked def
then pure (type def)

4
src/Core/Metadata.idr
View File

@ -10,9 +10,11 @@ import Core.TT
import Core.TTC
import Data.List
import System.File
import Utils.Binary
%default covering
-- Additional data we keep about the context to support interactive editing
public export

1
src/Core/Normalise.idr
View File

@ -969,6 +969,7 @@ logEnv lvl msg env
dumpEnv bs
dumpEnv {vs = x :: _} (b :: bs)
= do logTermNF lvl (msg ++ ":" ++ show (multiplicity b) ++ " " ++
show (piInfo b) ++ " " ++
show x) bs (binderType b)
dumpEnv bs

21
src/Core/Options.idr
View File

@ -4,12 +4,15 @@ import Core.Core
import Core.Name
import Core.TT
import Utils.Binary
import Utils.Path
import Data.List
import Data.Strings
import System.Info
%default total
public export
record Dirs where
constructor MkDirs
@ -129,25 +132,9 @@ record Options where
primnames : PrimNames
extensions : List LangExt
export
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
export
sep : Char
sep = if isWindows then '\\' else '/'
export
dirSep : String
dirSep = cast sep
export
pathSep : Char
pathSep = if isWindows then ';' else ':'
defaultDirs : Dirs
defaultDirs = MkDirs "." Nothing "build"
("build" ++ dirSep ++ "exec")
("build" </> "exec")
"/usr/local" ["."] [] []
defaultPPrint : PPrinter

9
src/Core/TT.idr
View File

@ -256,6 +256,15 @@ multiplicity (PVar c p ty) = c
multiplicity (PLet c val ty) = c
multiplicity (PVTy c ty) = c
export
piInfo : Binder tm -> PiInfo tm
piInfo (Lam c x ty) = x
piInfo (Let c val ty) = Explicit
piInfo (Pi c x ty) = x
piInfo (PVar c p ty) = p
piInfo (PLet c val ty) = Explicit
piInfo (PVTy c ty) = Explicit
export
setMultiplicity : Binder tm -> RigCount -> Binder tm
setMultiplicity (Lam c x ty) c' = Lam c' x ty

8
src/Core/TTC.idr
View File

@ -788,7 +788,7 @@ export
TTC Def where
toBuf b None = tag 0
toBuf b (PMDef pi args ct rt pats)
= do tag 1; toBuf b pi; toBuf b args; toBuf b ct; toBuf b rt; toBuf b pats
= do tag 1; toBuf b pi; toBuf b args; toBuf b ct; toBuf b pats
toBuf b (ExternDef a)
= do tag 2; toBuf b a
toBuf b (ForeignDef a cs)
@ -815,9 +815,8 @@ TTC Def where
1 => do pi <- fromBuf b
args <- fromBuf b
ct <- fromBuf b
rt <- fromBuf b
pats <- fromBuf b
pure (PMDef pi args ct rt pats)
pure (PMDef pi args ct (Unmatched "") pats)
2 => do a <- fromBuf b
pure (ExternDef a)
3 => do a <- fromBuf b
@ -945,7 +944,8 @@ TTC GlobalDef where
let refs = map fromList refsList
def <- fromBuf b
if isUserName name
then do ty <- fromBuf b; eargs <- fromBuf b;
then do ty <- fromBuf b
eargs <- fromBuf b;
seargs <- fromBuf b; specargs <- fromBuf b
iargs <- fromBuf b;
vars <- fromBuf b

9
src/Core/Termination.idr
View File

@ -386,7 +386,7 @@ getSC : {auto c : Ref Ctxt Defs} ->
Defs -> Def -> Core (List SCCall)
getSC defs (PMDef _ args _ _ pats)
= do sc <- traverse (findCalls defs) pats
pure (concat sc)
pure $ nub (concat sc)
getSC defs _ = pure []
export
@ -421,8 +421,6 @@ initArgs (S k)
-- Traverse the size change graph. When we reach a point we've seen before,
-- at least one of the arguments must have got smaller, otherwise it's
-- potentially non-terminating
-- TODO: If we encounter a name where we already know its termination status,
-- use that rather than continuing to traverse the graph!
checkSC : {auto a : Ref APos Arg} ->
{auto c : Ref Ctxt Defs} ->
Defs ->
@ -467,6 +465,11 @@ checkSC defs f args path
checkCall : List (Name, List (Maybe Arg)) -> SCCall -> Core Terminating
checkCall path sc
= do let inpath = fnCall sc `elem` map fst path
Just gdef <- lookupCtxtExact (fnCall sc) (gamma defs)
| Nothing => pure IsTerminating -- nothing to check
let Unchecked = isTerminating (totality gdef)
| IsTerminating => pure IsTerminating
| _ => pure (NotTerminating (BadCall [fnCall sc]))
term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path
if not inpath
then case term of

7
src/Core/Transform.idr
View File

@ -7,6 +7,8 @@ import Core.TT
import Data.NameMap
%default total
unload : List (FC, Term vars) -> Term vars -> Term vars
unload [] fn = fn
unload ((fc, arg) :: args) fn = unload args (App fc fn arg)
@ -48,6 +50,7 @@ match ms x y
then Just ms
else Nothing
covering
tryReplace : MatchVars vars vs -> Term vars -> Maybe (Term vs)
tryReplace ms (Local _ _ idx p) = lookupMatch idx p ms
tryReplace ms (Ref fc nt n) = pure (Ref fc nt n)
@ -80,6 +83,7 @@ tryReplace ms (PrimVal fc c) = pure (PrimVal fc c)
tryReplace ms (Erased fc i) = pure (Erased fc i)
tryReplace ms (TType fc) = pure (TType fc)
covering
tryApply : Transform -> Term vs -> Maybe (Term vs)
tryApply trans@(MkTransform {vars} n _ lhs rhs) tm
= case match None lhs tm of
@ -100,6 +104,7 @@ apply (t :: ts) tm
data Upd : Type where
covering
trans : {auto c : Ref Ctxt Defs} ->
{auto u : Ref Upd Bool} ->
Env Term vars -> List (FC, Term vars) -> Term vars ->
@ -135,6 +140,7 @@ trans env stk (TForce fc r tm)
pure $ unload stk (TForce fc r tm')
trans env stk tm = pure $ unload stk tm
covering
transLoop : {auto c : Ref Ctxt Defs} ->
Nat -> Env Term vars -> Term vars -> Core (Term vars)
transLoop Z env tm = pure tm
@ -148,6 +154,7 @@ transLoop (S k) env tm
else pure tm'
export
covering
applyTransforms : {auto c : Ref Ctxt Defs} ->
Env Term vars -> Term vars -> Core (Term vars)
applyTransforms env tm = transLoop 5 env tm

23
src/Core/Unify.idr
View File

@ -230,6 +230,11 @@ postpone blockedMetas loc mode logstr env x y
yq <- quote defs env y
pure (logstr ++ ": " ++ show !(toFullNames xq) ++
" =?= " ++ show !(toFullNames yq))
-- If we're blocked because a name is undefined, give up
checkDefined defs x
checkDefined defs y
xtm <- quote empty env x
ytm <- quote empty env y
-- Need to find all the metas in the constraint since solving any one
@ -249,6 +254,13 @@ postpone blockedMetas loc mode logstr env x y
logTerm 10 "Y" ytm
pure (constrain c)
where
checkDefined : Defs -> NF vars -> Core ()
checkDefined defs (NApp _ (NRef _ n) _)
= do Just _ <- lookupCtxtExact n (gamma defs)
| _ => throw (UndefinedName loc n)
pure ()
checkDefined _ _ = pure ()
undefinedN : Name -> Core Bool
undefinedN n
= do defs <- get Ctxt
@ -567,11 +579,11 @@ solveIfUndefined env metavar soln
= pure False
isDefInvertible : {auto c : Ref Ctxt Defs} ->
Int -> Core Bool
isDefInvertible i
FC -> Int -> Core Bool
isDefInvertible fc i
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
| Nothing => pure False
| Nothing => throw (UndefinedName fc (Resolved i))
pure (invertible gdef)
mutual
@ -906,7 +918,7 @@ mutual
(NApp yfc (NLocal yr y yp) yargs)
-- If they're both holes, solve the one with the bigger context
unifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc (NMeta yn yi yargs) yargs'
= do invx <- isDefInvertible xi
= do invx <- isDefInvertible loc xi
if xi == yi && (invx || umode mode == InSearch)
-- Invertible, (from auto implicit search)
-- so we can also unify the arguments.
@ -1323,7 +1335,7 @@ retry mode c
_ => pure cs
where
definedN : Name -> Core Bool
definedN n
definedN n@(NS _ (MN _ _)) -- a metavar will only ever be a MN
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| _ => pure False
@ -1332,6 +1344,7 @@ retry mode c
BySearch _ _ _ => pure False
Guess _ _ _ => pure False
_ => pure True
definedN _ = pure True
delayMeta : {vars : _} ->
LazyReason -> Nat -> Term vars -> Term vars -> Term vars

2
src/Core/Value.idr
View File

@ -7,6 +7,8 @@ import Core.TT
import Data.IntMap
%default covering
public export
record EvalOpts where
constructor MkEvalOpts

4
src/Data/ANameMap.idr
View File

@ -2,9 +2,13 @@
module Data.ANameMap
import Core.Name
import Data.List
import Data.NameMap
import Data.StringMap
%default total
export
record ANameMap a where
constructor MkANameMap

2
src/Data/Bool/Extra.idr
View File

@ -1,5 +1,7 @@
module Data.Bool.Extra
%default total
public export
andSameNeutral : (x : Bool) -> x && x = x
andSameNeutral False = Refl

2
src/Data/IntMap.idr
View File

@ -2,7 +2,7 @@ module Data.IntMap
-- Hand specialised map, for efficiency...
%default covering
%default total
Key : Type
Key = Int

2
src/Data/LengthMatch.idr
View File

@ -1,5 +1,7 @@
module Data.LengthMatch
%default total
public export
data LengthMatch : List a -> List b -> Type where
NilMatch : LengthMatch [] []

2
src/Data/List/Extra.idr
View File

@ -1,6 +1,6 @@
module Data.List.Extra
%default covering
%default total
||| Fetches the element at a given position.
||| Returns `Nothing` if the position beyond the list's end.

2
src/Data/NameMap.idr
View File

@ -4,7 +4,7 @@ import Core.Name
-- Hand specialised map, for efficiency...
%default covering
%default total
Key : Type
Key = Name

2
src/Data/StringMap.idr
View File

@ -2,7 +2,7 @@ module Data.StringMap
-- Hand specialised map, for efficiency...
%default covering
%default total
Key : Type
Key = String

4
src/Idris/CommandLine.idr
View File

@ -130,6 +130,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
(Just "Show installation prefix"),
MkOpt ["--paths"] [] [BlodwenPaths]
(Just "Show paths"),
MkOpt ["--build"] ["package file"] (\f => [Package Build f])
(Just "Build modules/executable for the given package"),
MkOpt ["--install"] ["package file"] (\f => [Package Install f])
@ -137,6 +138,9 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
MkOpt ["--clean"] ["package file"] (\f => [Package Clean f])
(Just "Clean intermediate files/executables for the given package"),
MkOpt ["--repl"] ["package file"] (\f => [Package REPL f])
(Just "Build the given package and launch a REPL instance."),
MkOpt ["--libdir"] [] [Directory LibDir]
(Just "Show library directory"),
MkOpt ["--no-banner"] [] [NoBanner]

25
src/Idris/Elab/Implementation.idr
View File

@ -215,6 +215,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
unsetFlag fc impName BlockedHint
setFlag fc impName TCInline
-- it's the methods we're interested in, not the implementation
setFlag fc impName (SetTotal PartialOK)
-- 4. (TODO: Order method bodies to be in declaration order, in
-- case of dependencies)
@ -225,9 +227,13 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
log 10 $ "Implementation body: " ++ show body'
traverse (processDecl [] nest env) body'
-- 6. Add transnformation rules for top level methods
-- 6. Add transformation rules for top level methods
traverse (addTransform impName upds) (methods cdata)
-- inline flag has done its job, and outside the interface
-- it can hurt, so unset it now
unsetFlag fc impName TCInline
-- Reset the open hints (remove the named implementation)
setOpenHints hs
pure ()) mbody
@ -270,7 +276,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
-- inserted in the right place
mkMethField : List (Name, RigCount, RawImp) ->
List (Name, List (Name, RigCount, PiInfo RawImp)) ->
(Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> RawImp
(Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> RawImp
mkMethField methImps fldTys (topn, n, upds, c, treq, ty)
= let argns = map applyUpdate (maybe [] id (lookup (dropNS topn) fldTys))
imps = map fst methImps in
@ -311,8 +317,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
topMethType : List (Name, RawImp) ->
Name -> List (Name, RigCount, RawImp) ->
List String -> List Name -> List Name ->
(Name, RigCount, TotalReq, (Bool, RawImp)) ->
Core ((Name, Name, List (String, String), RigCount, TotalReq, RawImp),
(Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
Core ((Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp),
List (Name, RawImp))
topMethType methupds impName methImps impsp pnames allmeths (mn, c, treq, (d, mty_in))
= do -- Get the specialised type by applying the method to the
@ -353,17 +359,18 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
topMethTypes : List (Name, RawImp) ->
Name -> List (Name, RigCount, RawImp) ->
List String -> List Name -> List Name ->
List (Name, RigCount, TotalReq, (Bool, RawImp)) ->
Core (List (Name, Name, List (String, String), RigCount, TotalReq, RawImp))
List (Name, RigCount, Maybe TotalReq, (Bool, RawImp)) ->
Core (List (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp))
topMethTypes upds impName methImps impsp pnames allmeths [] = pure []
topMethTypes upds impName methImps impsp pnames allmeths (m :: ms)
= do (m', newupds) <- topMethType upds impName methImps impsp pnames allmeths m
ms' <- topMethTypes (newupds ++ upds) impName methImps impsp pnames allmeths ms
pure (m' :: ms')
mkTopMethDecl : (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> ImpDecl
mkTopMethDecl : (Name, Name, List (String, String), RigCount, Maybe TotalReq, RawImp) -> ImpDecl
mkTopMethDecl (mn, n, upds, c, treq, mty)
= IClaim fc c vis (Totality treq :: opts_in) (MkImpTy fc n mty)
= let opts = maybe opts_in (\t => Totality t :: opts_in) treq in
IClaim fc c vis opts (MkImpTy fc n mty)
-- Given the method type (result of topMethType) return the mapping from
-- top level method name to current implementation's method name
@ -414,7 +421,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
"Implementation body can only contain definitions")
addTransform : Name -> List (Name, Name) ->
(Name, RigCount, TotalReq, Bool, RawImp) ->
(Name, RigCount, Maybe TotalReq, Bool, RawImp) ->
Core ()
addTransform iname ns (top, _, _, _, ty)
= do log 3 $ "Adding transform for " ++ show top ++ " : " ++ show ty ++

6
src/Idris/Elab/Interface.idr
View File

@ -23,6 +23,8 @@ import Data.ANameMap
import Data.List
import Data.Maybe
%default covering
-- TODO: Check all the parts of the body are legal
-- TODO: Deal with default superclass implementations
@ -243,9 +245,9 @@ updateIfaceSyn iname cn ps cs ms ds
findSetTotal (_ :: xs) = findSetTotal xs
totMeth : (Name, RigCount, List FnOpt, (Bool, RawImp)) ->
Core (Name, RigCount, TotalReq, (Bool, RawImp))
Core (Name, RigCount, Maybe TotalReq, (Bool, RawImp))
totMeth (n, c, opts, t)
= do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts)
= do let treq = findSetTotal opts
pure (n, c, treq, t)
export

1
src/Idris/Error.idr
View File

@ -12,6 +12,7 @@ import Idris.Syntax
import Parser.Source
import Data.List
import System.File
%default covering

4
src/Idris/IDEMode/Commands.idr
View File

@ -6,7 +6,7 @@ import public Idris.REPLOpts
import System.File
%default covering
%default total
public export
data SExp = SExpList (List SExp)
@ -186,7 +186,7 @@ escape = pack . concatMap escapeChar . unpack
export
Show SExp where
show (SExpList xs) = "(" ++ showSep " " (map show xs) ++ ")"
show (SExpList xs) = assert_total $ "(" ++ showSep " " (map show xs) ++ ")"
show (StringAtom str) = "\"" ++ escape str ++ "\""
show (BoolAtom b) = ":" ++ show b
show (IntegerAtom i) = show i

148
src/Idris/IDEMode/Holes.idr Normal file
View File

@ -0,0 +1,148 @@
module Idris.IDEMode.Holes
import Core.Env
import Idris.Resugar
import Idris.Syntax
import Idris.IDEMode.Commands
%default covering
public export
record HolePremise where
constructor MkHolePremise
name : Name
type : PTerm
multiplicity : RigCount
isImplicit : Bool
public export
record HoleData where
constructor MkHoleData
name : Name
type : PTerm
context : List HolePremise
||| If input is a hole, return number of locals in scope at binding
||| point
export
isHole : GlobalDef -> Maybe Nat
isHole def
= case definition def of
Hole locs _ => Just locs
PMDef pi _ _ _ _ =>
case holeInfo pi of
NotHole => Nothing
SolvedHole n => Just n
None => Just 0
_ => Nothing
-- Bring these back into REPL.idr
showName : Name -> Bool
showName (UN "_") = False
showName (MN _ _) = False
showName _ = True
showCount : RigCount -> String
showCount = elimSemi
" 0 "
" 1 "
(const " ")
impBracket : Bool -> String -> String
impBracket False str = str
impBracket True str = "{" ++ str ++ "}"
tidy : Name -> String
tidy (MN n _) = n
tidy n = show n
export
extractHoleData : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Core HoleData
extractHoleData defs env fn (S args) (Bind fc x (Let c val ty) sc)
= extractHoleData defs env fn args (subst val sc)
extractHoleData defs env fn (S args) (Bind fc x b sc)
= do rest <- extractHoleData defs (b :: env) fn args sc
let True = showName x
| False => pure rest
ity <- resugar env !(normalise defs env (binderType b))
let premise = MkHolePremise x ity (multiplicity b) (implicitBind b)
pure $ record { context $= (premise ::) } rest
where
implicitBind : Binder (Term vars) -> Bool
implicitBind (Pi _ Explicit _) = False
implicitBind (Pi _ _ _) = True
implicitBind (Lam _ Explicit _) = False
implicitBind (Lam _ _ _) = True
implicitBind _ = False
extractHoleData defs env fn args ty
= do ity <- resugar env !(normalise defs env ty)
pure $ MkHoleData fn ity []
export
holeData : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Core HoleData
holeData gam env fn args ty
= do hdata <- extractHoleData gam env fn args ty
pp <- getPPrint
pure $ if showImplicits pp
then hdata
else record { context $= dropShadows } hdata
where
dropShadows : List HolePremise -> List HolePremise
dropShadows [] = []
dropShadows (premise :: rest)
= if premise.name `elem` map name rest
then dropShadows rest
else premise :: dropShadows rest
export
showHole : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Core String
showHole defs env fn args ty
= do hdata <- holeData defs env fn args ty
case hdata.context of
[] => pure $ show (hdata.name) ++ " : " ++ show hdata.type
_ => pure $ concat
(map (\premise => showCount premise.multiplicity
++ (impBracket premise.isImplicit $
tidy premise.name ++ " : " ++ (show premise.type) ++ "\n" )
) hdata.context)
++ "-------------------------------------\n"
++ nameRoot (hdata.name) ++ " : " ++ show hdata.type
sexpPremise : HolePremise -> SExp
sexpPremise premise =
SExpList [StringAtom $ showCount premise.multiplicity
++ (impBracket premise.isImplicit $
tidy premise.name)
,StringAtom $ show premise.type
,SExpList [] -- TODO: metadata
]
export
sexpHole : HoleData -> SExp
sexpHole hole = SExpList
[ StringAtom (show hole.name)
, SExpList $ map sexpPremise hole.context -- Premises
, SExpList [ StringAtom $ show hole.type -- Conclusion
, SExpList[]] -- TODO: Highlighting information
]

2
src/Idris/IDEMode/MakeClause.idr
View File

@ -8,6 +8,8 @@ import Data.List
import Data.Nat
import Data.Strings
%default total
-- Implement make-with and make-case from the IDE mode
showRHSName : Name -> String

4
src/Idris/IDEMode/Parser.idr
View File

@ -14,6 +14,8 @@ import Text.Parser
import Utils.Either
import Utils.String
%default total
%hide Text.Lexer.symbols
%hide Parser.Lexer.Source.symbols
@ -42,6 +44,7 @@ idelex str
Comment _ => False
_ => True
covering
sexp : Rule SExp
sexp
= do symbol ":"; exactIdent "True"
@ -67,6 +70,7 @@ ideParser str p
export
covering
parseSExp : String -> Either (ParseError Token) SExp
parseSExp inp
= ideParser inp (do c <- sexp; eoi; pure c)

21
src/Idris/IDEMode/REPL.idr
View File

@ -15,6 +15,8 @@ import Core.Options
import Core.TT
import Core.Unify
import Data.So
import Idris.Desugar
import Idris.Error
import Idris.ModTree
@ -24,8 +26,9 @@ import Idris.REPL
import Idris.Syntax
import Idris.Version
import Idris.IDEMode.Parser
import Idris.IDEMode.Commands
import Idris.IDEMode.Holes
import Idris.IDEMode.Parser
import Idris.IDEMode.SyntaxHighlight
import TTImp.Interactive.CaseSplit
@ -37,10 +40,13 @@ import Utils.Hex
import Data.List
import System
import System.File
import Network.Socket
import Network.Socket.Data
%default covering
%foreign "C:fdopen,libc 6"
prim__fdopen : Int -> String -> PrimIO AnyPtr
@ -261,9 +267,6 @@ SExpable REPLOpt where
toSExp (CG str) = SExpList [ SymbolAtom "cg", toSExp str ]
sexpName : Name -> SExp
sexpName n = SExpList [ StringAtom (show n), SExpList [], SExpList [StringAtom "?", SExpList[]]]
displayIDEResult : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -317,14 +320,8 @@ displayIDEResult outf i (REPL $ CheckedTotal xs)
= printIDEResult outf i
$ StringAtom $ showSep "\n"
$ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
displayIDEResult outf i (REPL $ FoundHoles [])
= printIDEResult outf i $ SExpList []
displayIDEResult outf i (REPL $ FoundHoles xs)
= printIDEResult outf i $ holesSexp
where
holesSexp : SExp
holesSexp = SExpList $ map sexpName xs
displayIDEResult outf i (REPL $ FoundHoles holes)
= printIDEResult outf i $ SExpList $ map sexpHole holes
displayIDEResult outf i (REPL $ LogLevelSet k)
= printIDEResult outf i
$ StringAtom $ "Set loglevel to " ++ show k

2
src/Idris/IDEMode/SyntaxHighlight.idr
View File

@ -10,6 +10,8 @@ import Idris.IDEMode.Commands
import Data.List
%default covering
data Decoration : Type where
Typ : Decoration
Function : Decoration

2
src/Idris/IDEMode/TokenLine.idr
View File

@ -4,6 +4,8 @@ module Idris.IDEMode.TokenLine
import Parser.Lexer.Source
import Text.Lexer
%default total
public export
RawName : Type
RawName = String

32
src/Idris/Main.idr
View File

@ -1,35 +1,31 @@
module Main
import Core.Binary
import Core.Context
import Core.Core
import Core.Directory
import Core.InitPrimitives
import Core.Metadata
import Core.Options
import Core.Unify
import Idris.CommandLine
import Idris.Desugar
import Idris.IDEMode.REPL
import Idris.ModTree
import Idris.Package
import Idris.Parser
import Idris.ProcessIdr
import Idris.REPL
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import Data.List
import IdrisPaths
import Data.So
import Data.Strings
import Data.Vect
import System
import System.Directory
import System.File
import Utils.Path
import Yaffle.Main
import IdrisPaths
%default covering
findInput : List CLOpt -> Maybe String
@ -47,15 +43,15 @@ updateEnv
Nothing => setPrefix yprefix
bpath <- coreLift $ getEnv "IDRIS2_PATH"
the (Core ()) $ case bpath of
Just path => do traverse_ addExtraDir (map trim (split (==pathSep) path))
Just path => do traverse_ addExtraDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
bdata <- coreLift $ getEnv "IDRIS2_DATA"
the (Core ()) $ case bdata of
Just path => do traverse_ addDataDir (map trim (split (==pathSep) path))
Just path => do traverse_ addDataDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
blibs <- coreLift $ getEnv "IDRIS2_LIBS"
the (Core ()) $ case blibs of
Just path => do traverse_ addLibDir (map trim (split (==pathSep) path))
Just path => do traverse_ addLibDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
cg <- coreLift $ getEnv "IDRIS2_CG"
the (Core ()) $ case cg of
@ -71,10 +67,10 @@ updateEnv
defs <- get Ctxt
addPkgDir "prelude"
addPkgDir "base"
addDataDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"idris2-" ++ showVersion False version ++ dirSep ++ "support")
addLibDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"idris2-" ++ showVersion False version ++ dirSep ++ "lib")
addDataDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "support")
addLibDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "lib")
Just cwd <- coreLift $ currentDir
| Nothing => throw (InternalError "Can't get current directory")
addLibDir cwd
@ -171,7 +167,7 @@ stMain opts
the (Core ()) $ case fname of
Nothing => logTime "Loading prelude" $
when (not $ noprelude session) $
readPrelude
readPrelude True
Just f => logTime "Loading main file" $
(loadMainFile f >>= displayErrors)

152
src/Idris/Package.idr
View File

@ -10,6 +10,8 @@ import Core.Options
import Core.Unify
import Data.List
import Data.Maybe
import Data.So
import Data.StringMap
import Data.Strings
import Data.StringTrie
@ -17,9 +19,13 @@ import Data.These
import Parser.Package
import System
import System.Directory
import System.File
import Text.Parser
import Utils.Binary
import Utils.String
import Utils.Path
import Idris.CommandLine
import Idris.ModTree
@ -263,11 +269,14 @@ compileMain mainn mmod exec
build : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc -> Core (List Error)
build pkg
PkgDesc ->
List CLOpt ->
Core (List Error)
build pkg opts
= do defs <- get Ctxt
addDeps pkg
processOptions (options pkg)
preOptions opts
runScript (prebuild pkg)
let toBuild = maybe (map snd (modules pkg))
(\m => snd m :: map snd (modules pkg))
@ -295,11 +304,11 @@ installFrom : {auto c : Ref Ctxt Defs} ->
String -> String -> String -> List String -> Core ()
installFrom _ _ _ [] = pure ()
installFrom pname builddir destdir ns@(m :: dns)
= do let ttcfile = showSep dirSep (reverse ns)
let ttcPath = builddir ++ dirSep ++ "ttc" ++ dirSep ++ ttcfile ++ ".ttc"
let destPath = destdir ++ dirSep ++ showSep dirSep (reverse dns)
let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc"
Right _ <- coreLift $ mkdirs (reverse dns)
= do let ttcfile = joinPath (reverse ns)
let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"
let destPath = destdir </> joinPath (reverse dns)
let destFile = destdir </> ttcfile <.> "ttc"
Right _ <- coreLift $ mkdirAll $ joinPath (reverse dns)
| Left err => throw (InternalError ("Can't make directories " ++ show (reverse dns)))
coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
Right _ <- coreLift $ copyFile ttcPath destFile
@ -311,8 +320,10 @@ installFrom pname builddir destdir ns@(m :: dns)
-- an internal error.
install : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc -> Core ()
install pkg
PkgDesc ->
List CLOpt ->
Core ()
install pkg opts -- not used but might be in the future
= do defs <- get Ctxt
let build = build_dir (dirs (options defs))
runScript (preinstall pkg)
@ -322,11 +333,11 @@ install pkg
Just srcdir <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
-- Make the package installation directory
let installPrefix = dir_prefix (dirs (options defs)) ++
dirSep ++ "idris2-" ++ showVersion False version
let installPrefix = dir_prefix (dirs (options defs)) </>
"idris2-" ++ showVersion False version
True <- coreLift $ changeDir installPrefix
| False => throw (InternalError ("Can't change directory to " ++ installPrefix))
Right _ <- coreLift $ mkdirs [name pkg]
Right _ <- coreLift $ mkdirAll (name pkg)
| Left err => throw (InternalError ("Can't make directory " ++ name pkg))
True <- coreLift $ changeDir (name pkg)
| False => throw (InternalError ("Can't change directory to " ++ name pkg))
@ -334,8 +345,8 @@ install pkg
-- We're in that directory now, so copy the files from
-- srcdir/build into it
traverse (installFrom (name pkg)
(srcdir ++ dirSep ++ build)
(installPrefix ++ dirSep ++ name pkg)) toInstall
(srcdir </> build)
(installPrefix </> name pkg)) toInstall
coreLift $ changeDir srcdir
runScript (postinstall pkg)
@ -375,8 +386,10 @@ Monoid () where
clean : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc -> Core ()
clean pkg
PkgDesc ->
List CLOpt ->
Core ()
clean pkg opts -- `opts` is not used but might be in the future
= do defs <- get Ctxt
let build = build_dir (dirs (options defs))
let exec = exec_dir (dirs (options defs))
@ -391,8 +404,8 @@ clean pkg
(x :: xs) => Just (xs, x)) pkgmods
Just srcdir <- coreLift currentDir
| Nothing => throw (InternalError "Can't get current directory")
let builddir = srcdir ++ dirSep ++ build ++ dirSep ++ "ttc"
let execdir = srcdir ++ dirSep ++ exec
let builddir = srcdir </> build </> "ttc"
let execdir = srcdir </> exec
-- the usual pair syntax breaks with `No such variable a` here for some reason
let pkgTrie = the (StringTrie (List String)) $
foldl (\trie, ksv =>
@ -404,7 +417,7 @@ clean pkg
(\ks => map concat . traverse (deleteBin builddir ks))
pkgTrie
deleteFolder builddir []
maybe (pure ()) (\e => delete (execdir ++ dirSep ++ e))
maybe (pure ()) (\e => delete (execdir </> e))
(executable pkg)
runScript (postclean pkg)
where
@ -414,13 +427,13 @@ clean pkg
coreLift $ putStrLn $ "Removed: " ++ path
deleteFolder : String -> List String -> Core ()
deleteFolder builddir ns = delete $ builddir ++ dirSep ++ showSep dirSep ns
deleteFolder builddir ns = delete $ builddir </> joinPath ns
deleteBin : String -> List String -> String -> Core ()
deleteBin builddir ns mod
= do let ttFile = builddir ++ dirSep ++ showSep dirSep ns ++ dirSep ++ mod
delete $ ttFile ++ ".ttc"
delete $ ttFile ++ ".ttm"
= do let ttFile = builddir </> joinPath ns </> mod
delete $ ttFile <.> "ttc"
delete $ ttFile <.> "ttm"
getParseErrorLoc : String -> ParseError Token -> FC
getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
@ -432,39 +445,78 @@ getParseErrorLoc fname _ = replFC
-- it if necessary
runRepl : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgDesc -> Core ()
runRepl pkg
PkgDesc ->
List CLOpt ->
Core ()
runRepl pkg opts
= do addDeps pkg
processOptions (options pkg)
preOptions opts
throw (InternalError "Not implemented")
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
PkgCommand ->
String ->
List CLOpt ->
Core ()
processPackage cmd file opts
= if not (isSuffixOf ".ipkg" file)
then do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")
coreLift (exitWith (ExitFailure 1))
else do Right (pname, fs) <- coreLift $ parseFile file
(do desc <- parsePkgDesc file
eoi
pure desc)
| Left (FileFail err) => throw (FileErr file err)
| Left err => throw (ParseFail (getParseErrorLoc file err) err)
pkg <- addFields fs (initPkgDesc pname)
case cmd of
Build => do [] <- build pkg
Build => do [] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
pure ()
Install => do [] <- build pkg
Install => do [] <- build pkg opts
| errs => coreLift (exitWith (ExitFailure 1))
install pkg
Clean => clean pkg
REPL => runRepl pkg
install pkg opts
Clean => clean pkg opts
REPL => runRepl pkg opts
rejectPackageOpts : List CLOpt -> Core Bool
rejectPackageOpts (Package cmd f :: _)
= 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
record POptsFilterResult where
constructor MkPFR
pkgDetails : Maybe (PkgCommand, String)
oopts : List CLOpt
hasError : Bool
errorMsg : String
errorMsg = unlines
[ "Not all command line options can be used to override package options.\n"
, "Overridable options are:"
, " --quiet"
, " --verbose"
, " --timing"
, " --dumpcases <file>"
, " --dumplifted <file>"
, " --dumpvmcode <file>"
, " --debug-elab-check"
, " --codegen <cg>"
]
filterPackageOpts : POptsFilterResult -> List CLOpt -> Core (POptsFilterResult)
filterPackageOpts acc Nil = pure acc
filterPackageOpts acc (Package cmd f ::xs) = filterPackageOpts (record {pkgDetails = Just (cmd, f)} acc) xs
filterPackageOpts acc (SetCG f ::xs) = filterPackageOpts (record {oopts $= (SetCG f::)} acc) xs
filterPackageOpts acc (Quiet ::xs) = filterPackageOpts (record {oopts $= (Quiet::)} acc) xs
filterPackageOpts acc (Verbose ::xs) = filterPackageOpts (record {oopts $= (Verbose::)} acc) xs
filterPackageOpts acc (Timing ::xs) = filterPackageOpts (record {oopts $= (Timing::)} acc) xs
filterPackageOpts acc (DumpCases f ::xs) = filterPackageOpts (record {oopts $= (DumpCases f::)} acc) xs
filterPackageOpts acc (DumpLifted f ::xs) = filterPackageOpts (record {oopts $= (DumpLifted f::)} acc) xs
filterPackageOpts acc (DumpVMCode f ::xs) = filterPackageOpts (record {oopts $= (DumpVMCode f::)} acc) xs
filterPackageOpts acc (DebugElabCheck::xs) = filterPackageOpts (record {oopts $= (DebugElabCheck::)} acc) xs
filterPackageOpts acc (x::xs) = pure (record {hasError = True} acc)
-- If there's a package option, it must be the only option, so reject if
-- it's not
@ -472,11 +524,22 @@ export
processPackageOpts : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
List CLOpt -> Core Bool
processPackageOpts [Package cmd f]
= do processPackage cmd f
List CLOpt ->
Core Bool
processPackageOpts Nil = pure False
processPackageOpts [Package cmd f] = do processPackage cmd f Nil
pure True
processPackageOpts opts = rejectPackageOpts opts
processPackageOpts opts
= do (MkPFR (Just (cmd, f)) opts' err) <- filterPackageOpts (MkPFR Nothing Nil False) opts
| (MkPFR Nothing opts _) => pure False
if err
then do coreLift (putStrLn errorMsg)
pure True
else do processPackage cmd f opts'
pure True
-- find an ipkg file in one of the parent directories
-- If it exists, read it, set the current directory to the root of the source
@ -493,6 +556,7 @@ findIpkg fname
(do desc <- parsePkgDesc ipkgn
eoi
pure desc)
| Left (FileFail err) => throw (FileErr ipkgn err)
| Left err => throw (ParseFail (getParseErrorLoc ipkgn err) err)
pkg <- addFields fs (initPkgDesc pname)
setSourceDir (sourcedir pkg)
@ -501,7 +565,7 @@ findIpkg fname
case fname of
Nothing => pure Nothing
Just src =>
do let src' = showSep dirSep (up ++ [src])
do let src' = up </> src
setSource src'
opts <- get ROpts
put ROpts (record { mainfile = Just src' } opts)

26
src/Idris/Parser.idr
View File

@ -49,13 +49,17 @@ plhs = MkParseOpts False False
atom : FileName -> Rule PTerm
atom fname
= do start <- location
x <- constant
end <- location
pure (PPrimVal (MkFC fname start end) x)
<|> do start <- location
exactIdent "Type"
end <- location
pure (PType (MkFC fname start end))
<|> do start <- location
x <- name
end <- location
pure (PRef (MkFC fname start end) x)
<|> do start <- location
x <- constant
end <- location
pure (PPrimVal (MkFC fname start end) x)
<|> do start <- location
symbol "_"
end <- location
@ -80,10 +84,6 @@ atom fname
pragma "search"
end <- location
pure (PSearch (MkFC fname start end) 50)
<|> do start <- location
x <- name
end <- location
pure (PRef (MkFC fname start end) x)
whereBlock : FileName -> Int -> Rule (List PDecl)
whereBlock fname col
@ -445,7 +445,7 @@ mutual
Rule (List (RigCount, Name, PTerm))
pibindListName fname start indents
= do rigc <- multiplicity
ns <- sepBy1 (symbol ",") unqualifiedName
ns <- sepBy1 (symbol ",") binderName
symbol ":"
ty <- expr pdef fname indents
atEnd indents
@ -453,11 +453,15 @@ mutual
pure (map (\n => (rig, UN n, ty)) ns)
<|> sepBy1 (symbol ",")
(do rigc <- multiplicity
n <- name
n <- binderName
symbol ":"
ty <- expr pdef fname indents
rig <- getMult rigc
pure (rig, n, ty))
pure (rig, UN n, ty))
where
-- _ gets treated specially here, it means "I don't care about the name"
binderName : Rule String
binderName = unqualifiedName <|> do symbol "_"; pure "_"
pibindList : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Maybe Name, PTerm))

51
src/Idris/ProcessIdr.idr
View File

@ -28,6 +28,8 @@ import Data.NameMap
import System.File
%default covering
processDecl : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -57,20 +59,20 @@ processDecls decls
readModule : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
(top : Bool) ->
(full : Bool) -> -- load everything transitively (needed for REPL and compiling)
FC ->
(visible : Bool) -> -- Is import visible to top level module?
(reexp : Bool) -> -- Should the module be reexported?
(imp : List String) -> -- Module name to import
(as : List String) -> -- Namespace to import into
Core ()
readModule top loc vis reexp imp as
readModule full loc vis reexp imp as
= do defs <- get Ctxt
let False = (imp, vis, as) `elem` map snd (allImported defs)
| True => when vis (setVisible imp)
Right fname <- nsToPath loc imp
| Left err => throw err
Just (syn, hash, more) <- readFromTTC {extra = SyntaxInfo}
Just (syn, hash, more) <- readFromTTC False {extra = SyntaxInfo}
loc vis fname imp as
| Nothing => when vis (setVisible imp) -- already loaded, just set visibility
extendAs imp as syn
@ -82,30 +84,25 @@ readModule top loc vis reexp imp as
do let m = fst mimp
let reexp = fst (snd mimp)
let as = snd (snd mimp)
readModule False loc (vis && reexp) reexp m as) more
when (reexp || full) $ readModule full loc (vis && reexp) reexp m as) more
setNS modNS
readImport : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
Import -> Core ()
readImport imp
= do readModule True (loc imp) True (reexport imp) (path imp) (nameAs imp)
Bool -> Import -> Core ()
readImport full imp
= do readModule full (loc imp) True (reexport imp) (path imp) (nameAs imp)
addImported (path imp, reexport imp, nameAs imp)
readHash : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
Import -> Core (List String, Int)
Import -> Core (Bool, (List String, Int))
readHash imp
= do Right fname <- nsToPath (loc imp) (path imp)
| Left err => throw err
h <- readIFaceHash fname
-- If the import is a 'public' import, then it forms part of
-- our own interface so add its hash to our hash
when (reexport imp) $
do log 5 $ "Reexporting " ++ show (path imp) ++ " hash " ++ show h
addHash h
pure (nameAs imp, h)
pure (reexport imp, (nameAs imp, h))
prelude : Import
prelude = MkImport (MkFC "(implicit)" (0, 0) (0, 0)) False
@ -115,8 +112,9 @@ export
readPrelude : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
Core ()
readPrelude = do readImport prelude
Bool -> Core ()
readPrelude full
= do readImport full prelude
setNS ["Main"]
-- Import a TTC for use as the main file (e.g. at the REPL)
@ -127,7 +125,7 @@ readAsMain : {auto c : Ref Ctxt Defs} ->
(fname : String) -> Core ()
readAsMain fname
= do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo}
toplevelFC True fname [] []
True toplevelFC True fname [] []
| Nothing => throw (InternalError "Already loaded")
replNS <- getNS
replNestedNS <- getNestedNS
@ -139,13 +137,13 @@ readAsMain fname
traverse_ (\ mimp =>
do let m = fst mimp
let as = snd (snd mimp)
readModule False emptyFC True True m as
readModule True emptyFC True True m as
addImported (m, True, as)) more
-- also load the prelude, if required, so that we have access to it
-- at the REPL.
when (not (noprelude !getSession)) $
readModule False emptyFC True True ["Prelude"] ["Prelude"]
readModule True emptyFC True True ["Prelude"] ["Prelude"]
-- We're in the namespace from the first TTC, so use the next name
-- from that for the fresh metavariable name generation
@ -207,6 +205,12 @@ prim__gc : Int -> PrimIO ()
gc : IO ()
gc = primIO $ prim__gc 4
export
addPublicHash : {auto c : Ref Ctxt Defs} ->
(Bool, (List String, Int)) -> Core ()
addPublicHash (True, (mod, h)) = do addHash mod; addHash h
addPublicHash _ = pure ()
-- Process everything in the module; return the syntax information which
-- needs to be written to the TTC (e.g. exported infix operators)
-- Returns 'Nothing' if it didn't reload anything
@ -233,7 +237,7 @@ processMod srcf ttcf msg sourcecode
defs <- get Ctxt
log 5 $ "Current hash " ++ show (ifaceHash defs)
log 5 $ show (moduleNS modh) ++ " hashes:\n" ++
show (sort hs)
show (sort (map snd hs))
imphs <- readImportHashes ttcf
log 5 $ "Old hashes from " ++ ttcf ++ ":\n" ++ show (sort imphs)
@ -245,7 +249,7 @@ processMod srcf ttcf msg sourcecode
let ns = moduleNS modh
if (sort hs == sort imphs && srctime <= ttctime)
if (sort (map snd hs) == sort imphs && srctime <= ttctime)
then -- Hashes the same, source up to date, just set the namespace
-- for the REPL
do setNS ns
@ -256,6 +260,7 @@ processMod srcf ttcf msg sourcecode
pure (runParser (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p))
| Left err => pure (Just [ParseFail (getParseErrorLoc srcf err) err])
initHash
traverse addPublicHash (sort hs)
resetNextVar
when (ns /= ["Main"]) $
do let MkFC fname _ _ = headerloc mod
@ -271,7 +276,7 @@ processMod srcf ttcf msg sourcecode
-- (also that we only build child dependencies if rebuilding
-- changes the interface - will need to store a hash in .ttc!)
logTime "Reading imports" $
traverse_ readImport imps
traverse_ (readImport False) imps
-- Before we process the source, make sure the "hide_everywhere"
-- names are set to private (TODO, maybe if we want this?)
@ -288,7 +293,7 @@ processMod srcf ttcf msg sourcecode
-- If they haven't changed next time, and the source
-- file hasn't changed, no need to rebuild.
defs <- get Ctxt
put Ctxt (record { importHashes = hs } defs)
put Ctxt (record { importHashes = map snd hs } defs)
pure (Just errs))
(\err => pure (Just [err]))

101
src/Idris/REPL.idr
View File

@ -26,6 +26,7 @@ import Idris.Error
import Idris.IDEMode.CaseSplit
import Idris.IDEMode.Commands
import Idris.IDEMode.MakeClause
import Idris.IDEMode.Holes
import Idris.ModTree
import Idris.Parser
import Idris.Resugar
@ -49,6 +50,7 @@ import Data.Stream
import Data.Strings
import System
import System.File
%default covering
@ -76,82 +78,6 @@ showInfo (n, idx, d)
coreLift $ putStrLn $
"Size change: " ++ showSep ", " scinfo
isHole : GlobalDef -> Maybe Nat
isHole def
= case definition def of
Hole locs _ => Just locs
PMDef pi _ _ _ _ =>
case holeInfo pi of
NotHole => Nothing
SolvedHole n => Just n
_ => Nothing
showCount : RigCount -> String
showCount = elimSemi
" 0 "
" 1 "
(const " ")
impBracket : Bool -> String -> String
impBracket False str = str
impBracket True str = "{" ++ str ++ "}"
showName : Name -> Bool
showName (UN "_") = False
showName (MN _ _) = False
showName _ = True
tidy : Name -> String
tidy (MN n _) = n
tidy n = show n
showEnv : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Core (List (Name, String), String)
showEnv defs env fn (S args) (Bind fc x (Let c val ty) sc)
= showEnv defs env fn args (subst val sc)
showEnv defs env fn (S args) (Bind fc x b sc)
= do ity <- resugar env !(normalise defs env (binderType b))
let pre = if showName x
then REPL.showCount (multiplicity b) ++
impBracket (implicitBind b) (tidy x ++ " : " ++ show ity) ++ "\n"
else ""
(envstr, ret) <- showEnv defs (b :: env) fn args sc
pure ((x, pre) :: envstr, ret)
where
implicitBind : Binder (Term vars) -> Bool
implicitBind (Pi _ Explicit _) = False
implicitBind (Pi _ _ _) = True
implicitBind (Lam _ Explicit _) = False
implicitBind (Lam _ _ _) = True
implicitBind _ = False
showEnv defs env fn args ty
= do ity <- resugar env !(normalise defs env ty)
pure ([], "-------------------------------------\n" ++
nameRoot fn ++ " : " ++ show ity)
showHole : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> Env Term vars -> Name -> Nat -> Term vars ->
Core String
showHole gam env fn args ty
= do (envs, ret) <- showEnv gam env fn args ty
pp <- getPPrint
let envs' = if showImplicits pp
then envs
else dropShadows envs
pure (concat (map snd envs') ++ ret)
where
dropShadows : List (Name, a) -> List (Name, a)
dropShadows [] = []
dropShadows ((n, ty) :: ns)
= if n `elem` map fst ns
then dropShadows ns
else (n, ty) :: dropShadows ns
displayType : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Defs -> (Name, Int, GlobalDef) ->
@ -494,7 +420,7 @@ data REPLResult : Type where
ProofFound : PTerm -> REPLResult
Missed : List MissedResult -> REPLResult
CheckedTotal : List (Name, Totality) -> REPLResult
FoundHoles : List Name -> REPLResult
FoundHoles : List HoleData -> REPLResult
OptionsSet : List REPLOpt -> REPLResult
LogLevelSet : Nat -> REPLResult
VersionIs : Version -> REPLResult
@ -702,8 +628,21 @@ process (SetLog lvl)
= do setLogLevel lvl
pure $ LogLevelSet lvl
process Metavars
= do ms <- getUserHoles
pure $ FoundHoles ms
= do defs <- get Ctxt
let ctxt = gamma defs
ms <- getUserHoles
let globs = concat !(traverse (\n => lookupCtxtName n ctxt) ms)
let holesWithArgs = mapMaybe (\(n, i, gdef) => do args <- isHole gdef
pure (n, gdef, args))
globs
hData <- the (Core $ List HoleData) $
traverse (\n_gdef_args =>
-- Inference can't deal with this for now :/
let (n, gdef, args) = the (Name, GlobalDef, Nat) n_gdef_args in
holeData defs [] n args (type gdef))
holesWithArgs
pure $ FoundHoles hData
process (Editing cmd)
= do ppopts <- getPPrint
-- Since we're working in a local environment, don't do the usual
@ -860,9 +799,9 @@ mutual
displayResult (Missed cases) = printResult $ showSep "\n" $ map handleMissing cases
displayResult (CheckedTotal xs) = printResult $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
displayResult (FoundHoles []) = printResult $ "No holes"
displayResult (FoundHoles [x]) = printResult $ "1 hole: " ++ show x
displayResult (FoundHoles [x]) = printResult $ "1 hole: " ++ show x.name
displayResult (FoundHoles xs) = printResult $ show (length xs) ++ " holes: " ++
showSep ", " (map show xs)
showSep ", " (map (show . name) xs)
displayResult (LogLevelSet k) = printResult $ "Set loglevel to " ++ show k
displayResult (VersionIs x) = printResult $ showVersion True x
displayResult (RequestedHelp) = printResult displayHelp

2
src/Idris/REPLCommon.idr
View File

@ -13,6 +13,8 @@ import Idris.Syntax
import Data.List
%default covering
-- Output informational messages, unless quiet flag is set
export
iputStrLn : {auto o : Ref ROpts REPLOpts} ->

2
src/Idris/REPLOpts.idr
View File

@ -5,6 +5,8 @@ import Idris.Syntax
import Data.Strings
import System.File
%default total
public export
data OutputMode
= IDEMode Integer File File

10
src/Idris/SetOptions.idr
View File

@ -5,6 +5,7 @@ import Core.Directory
import Core.Metadata
import Core.Options
import Core.Unify
import Utils.Path
import Idris.CommandLine
import Idris.REPL
@ -13,21 +14,24 @@ import Idris.Version
import IdrisPaths
import Data.So
import System
%default covering
-- TODO: Version numbers on dependencies
export
addPkgDir : {auto c : Ref Ctxt Defs} ->
String -> Core ()
addPkgDir p
= do defs <- get Ctxt
addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++
"idris2-" ++ showVersion False version ++ dirSep ++ p)
addExtraDir (dir_prefix (dirs (options defs)) </>
"idris2-" ++ showVersion False version </> p)
dirOption : Dirs -> DirCommand -> Core ()
dirOption dirs LibDir
= coreLift $ putStrLn
(dir_prefix dirs ++ dirSep ++ "idris2-" ++ showVersion False version ++ dirSep)
(dir_prefix dirs </> "idris2-" ++ showVersion False version)
-- Options to be processed before type checking. Return whether to continue.
export

2
src/Idris/Syntax.idr
View File

@ -503,7 +503,7 @@ record IFaceInfo where
iconstructor : Name
params : List Name
parents : List RawImp
methods : List (Name, RigCount, TotalReq, Bool, RawImp)
methods : List (Name, RigCount, Maybe TotalReq, Bool, RawImp)
-- ^ name, whether a data method, and desugared type (without constraint)
defaults : List (Name, List ImpClause)

2
src/Idris/Version.idr
View File

@ -4,6 +4,8 @@ module Idris.Version
import IdrisPaths
import Data.List
%default total
||| Semantic versioning with optional tag
||| See [semver](https://semver.org/) for proper definition of semantic versioning
public export

3
src/Parser/Package.idr
View File

@ -9,6 +9,8 @@ import public Parser.Support
import System.File
import Utils.Either
%default total
export
runParser : String -> Rule ty -> Either (ParseError Token) ty
runParser str p
@ -17,6 +19,7 @@ runParser str p
Right (fst parsed)
export
covering
parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty)
parseFile fn p
= do Right str <- readFile fn

10
src/Parser/Support.idr
View File

@ -155,23 +155,23 @@ escape' ('\\' :: 'o' :: xs)
escape' ('\\' :: xs)
= case span isDigit xs of
([], (a :: b :: c :: rest)) =>
case getEsc (pack (the (List _) [a, b, c])) of
case getEsc (fastPack (the (List _) [a, b, c])) of
Just v => Just (v :: !(assert_total (escape' rest)))
Nothing => case getEsc (pack (the (List _) [a, b])) of
Nothing => case getEsc (fastPack (the (List _) [a, b])) of
Just v => Just (v :: !(assert_total (escape' (c :: rest))))
Nothing => escape' xs
([], (a :: b :: [])) =>
case getEsc (pack (the (List _) [a, b])) of
case getEsc (fastPack (the (List _) [a, b])) of
Just v => Just (v :: [])
Nothing => escape' xs
([], rest) => assert_total (escape' rest)
(ds, rest) => Just $ cast (cast {to=Int} (pack ds)) ::
(ds, rest) => Just $ cast (cast {to=Int} (fastPack ds)) ::
!(assert_total (escape' rest))
escape' (x :: xs) = Just $ x :: !(escape' xs)
export
escape : String -> Maybe String
escape x = pure $ pack !(escape' (unpack x))
escape x = pure $ fastPack !(escape' (unpack x))
export
getCharLit : String -> Maybe Char

2
src/TTImp/Elab.idr
View File

@ -19,6 +19,8 @@ import Data.IntMap
import Data.List
import Data.NameMap
%default covering
findPLetRenames : {vars : _} ->
Term vars -> List (Name, (RigCount, Name))
findPLetRenames (Bind fc n (PLet c (Local _ _ idx p) ty) sc)

8
src/TTImp/Elab/Case.idr
View File

@ -61,6 +61,12 @@ toRig0 : {idx : Nat} -> (0 p : IsVar name idx vs) -> Env Term vs -> Env Term vs
toRig0 First (b :: bs) = setMultiplicity b erased :: bs
toRig0 (Later p) (b :: bs) = b :: toRig0 p bs
-- When we abstract over the evironment, pi needs to be explicit
explicitPi : Env Term vs -> Env Term vs
explicitPi (Pi c _ ty :: env) = Pi c Explicit ty :: explicitPi env
explicitPi (b :: env) = b :: explicitPi env
explicitPi [] = []
allow : Maybe (Var vs) -> Env Term vs -> Env Term vs
allow Nothing env = env
allow (Just (MkVar p)) env = toRig1 p env
@ -187,7 +193,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
(caseretty, _) <- bindImplicits fc (implicitMode elabinfo) defs env
fullImps caseretty_in (TType fc)
let casefnty
= abstractFullEnvType fc (allow splitOn env)
= abstractFullEnvType fc (allow splitOn (explicitPi env))
(maybe (Bind fc scrn (Pi caseRig Explicit scrty)
(weaken caseretty))
(const caseretty) splitOn)

2
src/TTImp/Elab/Check.idr
View File

@ -21,6 +21,8 @@ import Data.List
import Data.NameMap
import Data.StringMap
%default covering
public export
data ElabMode = InType | InLHS RigCount | InExpr | InTransform

Some files were not shown because too many files have changed in this diff Show More