idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +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-25 13:01:15 +06:00
commit a3d57cd4fc
183 changed files with 11723 additions and 10037 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
.github/workflows/ci-macos.yml vendored Normal file
View File

@ -0,0 +1,24 @@
name: macOS
on:
push:
branches:
- '*'
tags:
- '*'
pull_request:
branches:
- master
jobs:
build:
runs-on: macos-latest
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Install build dependencies
run: |
brew install chezscheme
brew install coreutils
- name: Build and test Idris 2 from bootstrap
run: make bootstrap SCHEME=chez
shell: bash

24
.github/workflows/ci-ubuntu-racket.yml vendored Normal file
View File

@ -0,0 +1,24 @@
name: Ubuntu Racket
on:
push:
branches:
- '*'
tags:
- '*'
pull_request:
branches:
- master
jobs:
build:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Install build dependencies
run: |
sudo apt-get install -y racket
- name: Build from bootstrap
run: make bootstrap-racket
shell: bash

24
.github/workflows/ci-ubuntu.yml vendored Normal file
View File

@ -0,0 +1,24 @@
name: Ubuntu
on:
push:
branches:
- '*'
tags:
- '*'
pull_request:
branches:
- master
jobs:
build:
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Install build dependencies
run: |
sudo apt-get install -y chezscheme
- name: Build from bootstrap
run: make bootstrap SCHEME=scheme
shell: bash

40
.github/workflows/ci-windows.yml vendored Normal file
View File

@ -0,0 +1,40 @@
name: Windows
on:
push:
branches:
- '*'
tags:
- '*'
pull_request:
branches:
- master
env:
MSYS2_PATH_TYPE: inherit
jobs:
build:
runs-on: windows-latest
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
- name: Configure and Build Chez Scheme
run: msys2do cd ChezScheme; ./configure --threads; make; cd ..
shell: cmd
- name: Set Path
run: |
$chez="$(pwd)\ChezScheme\ta6nt\bin\ta6nt"
echo "::add-path::$chez"
echo "::set-env name=SCHEME::scheme"
- name: Test Scheme
run: scheme.exe --version
- name: Bootstrap
run: msys2do make bootstrap
shell: cmd

3
.gitignore vendored
View File

@ -1,3 +1,4 @@
idris2docs_venv
*~
*.ibc
*.ttc
@ -25,7 +26,7 @@
/bootstrap/bin/
/bootstrap/lib/
/bootstrap/idris2-0*/
/bootstrap/idris2_app/idris2-boot.*
/bootstrap/idris2_app/idris2-boot*
/bootstrap/idris2_app/libidris2_support.*
/bootstrap/idris2boot
/bootstrap/idris2boot.rkt

5
.travis.yml
View File

@ -1,5 +0,0 @@
dist: bionic
language: minimal
install: sudo apt-get install chezscheme9.5
script:
- make bootstrap SCHEME=chezscheme9.5

55
CHANGELOG.md
View File

@ -3,7 +3,37 @@ Changes since Idris 2 v0.1.0
The implementation is now self-hosted. To initialise the build, either use
the [bootstrapping version of Idris2](https://github.com/edwinb/Idris2-boot)
or build fromt the generated Scheme, using `make bootstrap`.
or build from the generated Scheme, using `make bootstrap`.
Language changes:
* `total`, `covering` and `partial` flags on functions now have an effect.
* `%default <totality status>` has been implemented. By default, functions must
be at least `covering`
+ That is, `%default covering` is the default status.
* Fields of records can be accessed (and updated) using the dot syntax,
such as `r.field1.field2` or `record { field1.field2 = 42 }`.
For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
* New function flag `%tcinline` which means that the function should be
inlined for the purposes of totality checking (but otherwise not inlined).
This can be used as a hint for totality checking, to make the checker look
inside functions that it otherwise might not.
* %transform directive, for declaring transformation rules on runtime
expressions. Transformation rules are automatically added for top level
implementations of interfaces.
* A %spec flag on functions which allows arguments to be marked for partial
evaluation, following the rules from "Scrapping Your Inefficient Engine"
(ICFP 2010, Brady & Hammond)
* To improve error messages, one can use `with NS.name <term>`
or `with [NS.name1, NS.name2, ...] <term>` to disable disambiguation
for the given names in `<term>`. Example: `with MyNS.(>>=) do ...`.
Library additions:
* Additional file management operations in `base`
* New module in `base` for time (`System.Clock`)
* New modules in `contrib` for JSON (`Language.JSON.*`); random numbers
(`System.Random`)
Compiler updates:
@ -17,38 +47,15 @@ Compiler updates:
* 0-multiplicity constructor arguments are now properly erased, not just
given a placeholder null value.
Language extensions:
* %transform directive, for declaring transformation rules on runtime
expressions. Transformation rules are automatically added for top level
implementations of interfaces.
* A %spec flag on functions which allows arguments to be marked for partial
evaluation, following the rules from "Scrapping Your Inefficient Engine"
(ICFP 2010, Brady & Hammond)
Library additions:
* Additional file management operations in `base`
* New module in `base` for time (`System.Clock`)
* New modules in `contrib` for JSON (`Language.JSON.*`); random numbers
(`System.Random`)
Other improvements:
* Various performance improvements in the typechecker:
+ Noting which metavariables are blocking unification constraints, so that
they only get retried if those metavariables make progress.
+ Evaluating `fromInteger` at compile time.
+ In the run-time, reuse the old heap after garbage collection if it
hasn't been resized, to avoid unnecessary system calls.
* Extend Idris2's literate mode to support reading Markdown and OrgMode files.
For more details see: https://idris2.readthedocs.io/en/latest/reference/literate.html
* Fields of records can be accessed (and updated) using the dot syntax,
such as `r.field1.field2` or `record { field1.field2 = 42 }`.
For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
Changes since Idris 1
---------------------

5
INSTALL.md
View File

@ -12,10 +12,7 @@ On Windows, it has been reported that installing via `MSYS2` works
(https://www.msys2.org/). On Raspberry Pi, you can bootstrap via Racket.
By default, code generation is via Chez Scheme. You can use Racket instead,
by passing `CG=racket` to `make` for the commands below.
[Note: a couple of tests are currently known to fail when installing via
Racket. This will be addressed soon!]
by setting the environment variable `IDRIS2_CG=racket` before running `make`.
1: Set the PREFIX
-----------------

27
Makefile
View File

@ -24,13 +24,7 @@ endif
export IDRIS2_VERSION := ${MAJOR}.${MINOR}.${PATCH}
IDRIS2_SUPPORT := libidris2_support${SHLIB_SUFFIX}
CG ?= ${IDRIS2_CG}
ifneq (${CG},racket)
IDRIS2_IPKG := idris2.ipkg
else
IDRIS2_IPKG := idris2rkt.ipkg
endif
IDRIS2_IPKG := idris2.ipkg
ifeq ($(OS), windows)
IDRIS2_PREFIX := $(shell cygpath -m ${PREFIX})
@ -47,7 +41,7 @@ endif
export SCHEME
.PHONY: all idris2-exec ${TARGET} support support-clean clean distclean
.PHONY: all idris2-exec ${TARGET} testbin support support-clean clean distclean
all: support ${TARGET} testbin libs
@ -107,12 +101,13 @@ install-api:
install-idris2:
mkdir -p ${PREFIX}/bin/
install ${TARGET} ${PREFIX}/bin
ifeq ($(OS), windows)
-install ${TARGET}.cmd ${PREFIX}/bin
endif
mkdir -p ${PREFIX}/lib/
install support/c/${IDRIS2_SUPPORT} ${PREFIX}/lib
ifneq ($(CG),racket)
mkdir -p ${PREFIX}/bin/${NAME}_app
install ${TARGETDIR}/${NAME}_app/* ${PREFIX}/bin/${NAME}_app
endif
install-support: support
mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
@ -126,7 +121,7 @@ install-support: support
install-libs: libs
${MAKE} -C libs/prelude install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/base install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_VERSION=${IDRIS2_VERSION}
${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
${MAKE} -C libs/contrib install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
@ -140,19 +135,15 @@ ifeq ($(OS), darwin)
else
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss
endif
ifeq ($(OS), windows)
sh ./bootstrap-win.sh
else
sh ./bootstrap.sh
endif
bootstrap-racket: support
cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
cp bootstrap/idris2.rkt bootstrap/idris2boot.rkt
cp bootstrap/idris2_app/idris2.rkt bootstrap/idris2_app/idris2-boot.rkt
ifeq ($(OS), darwin)
sed -i '' 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2boot.rkt
sed -i '' 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt
else
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2boot.rkt
sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt
endif
sh ./bootstrap-rkt.sh

6
README.md
View File

@ -1,9 +1,11 @@
Idris 2
=======
[![Build Status](https://travis-ci.org/idris-lang/Idris2.svg?branch=master)](https://travis-ci.org/idris-lang/Idris2)
[![Documentation Status](https://readthedocs.org/projects/idris2/badge/?version=latest)](https://idris2.readthedocs.io/en/latest/?badge=latest)
[![](https://github.com/idris-lang/Idris2/workflows/Windows/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Windows")
[![](https://github.com/idris-lang/Idris2/workflows/Ubuntu/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Ubuntu")
[![](https://github.com/idris-lang/Idris2/workflows/Ubuntu%20Racket/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Ubuntu+Racket")
[![](https://github.com/idris-lang/Idris2/workflows/macOS/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"macOS")
[Idris 2](https://idris-lang.org/) is a purely functional programming language
with first class types.

28
Release/mkdist.sh Normal file
View File

@ -0,0 +1,28 @@
#!/bin/sh
if [ $# -eq 0 ]
then
echo "No version number supplied"
exit 1
fi
git clone https://github.com/idris-lang/Idris2.git
mv Idris2 Idris2-$1
cd Idris2-$1
# Go to the tag for the release we're making
git checkout tags/v$1
# Remove the directories and files we don't want in the release
rm -rf .git
rm -rf .github
rm .git*
rm .travis*
rm -rf Release
find . -type f -name '.gitignore' -exec rm -f {} \;
cd ..
tar zcf idris2-$1.tgz Idris2-$1
echo "idris2-$1.tgz created."

14
bootstrap-rkt.sh
View File

@ -4,11 +4,13 @@
cd bootstrap
echo "Building idris2boot from idris2boot.rkt"
raco exe idris2boot.rkt
raco exe idris2_app/idris2-boot.rkt
# Put the result in the usual place where the target goes
mkdir -p ../build/exec
install idris2boot ../build/exec/idris2
mkdir -p ../build/exec/idris2_app
install idris2-rktboot ../build/exec/idris2
install idris2_app/* ../build/exec/idris2_app
cd ..
@ -21,8 +23,8 @@ 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"
make libs CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
make install CG=racket PREFIX=${PREFIX} LD_LIBRARY_PATH=${DYLIB_PATH}
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 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}
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}

35
bootstrap-win.sh
View File

@ -1,35 +0,0 @@
#!/bin/sh
if [ -z "$SCHEME" ]
then
echo "SCHEME not set. Invoke with SCHEME=[name of chez executable]"
exit 1
fi
# Compile the bootstrap scheme
cd bootstrap
${SCHEME} --script compile.ss
# Put the result in the usual place where the target goes
mkdir -p ../build/exec
mkdir -p ../build/exec/idris2_app
install idris2-boot ../build/exec/idris2
install idris2_app/* ../build/exec/idris2_app
cd ..
# Install with the bootstrap directory as the PREFIX
DIR="`realpath $0`"
PREFIX="`dirname $DIR`"/bootstrap
WIN_PREFIX=$(cygpath -m $PREFIX)
# Now rebuild everything properly
echo ${PREFIX}
IDRIS2_BOOT_PATH="${WIN_PREFIX}/idris2-0.2.0/prelude;${WIN_PREFIX}/idris2-0.2.0/base;${WIN_PREFIX}/idris2-0.2.0/contrib;${WIN_PREFIX}/idris2-0.2.0/network"
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}
make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_LIBS=${WIN_PREFIX}/idris2-0.2.0/lib IDRIS2_DATA=${WIN_PREFIX}/idris2-0.2.0/support

21
bootstrap.sh
View File

@ -22,17 +22,28 @@ cd ..
DIR="`realpath $0`"
PREFIX="`dirname $DIR`"/bootstrap
if [ ${OS} = "windows" ]; then
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"
# Now rebuild everything properly
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"
NEWPREFIX="`dirname $DIR`"
IDRIS2_NEW_PATH="${NEWPREFIX}/libs/prelude/build/ttc:${NEWPREFIX}/libs/base/build/ttc:${NEWPREFIX}/libs/network/build/ttc"
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=${PREFIX}/idris2-0.2.0/lib:${PREFIX}/idris2-0.2.0/network/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support
make test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_NEW_PATH} SCHEME=${SCHEME} IDRIS2_LIBS=${IDRIS2_TEST_LIBS} IDRIS2_DATA=${IDRIS2_TEST_DATA}

5
bootstrap/idris2-rktboot vendored Executable file
View File

@ -0,0 +1,5 @@
#!/bin/sh
DIR="`realpath $0`"
export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:`dirname "$DIR"`/"idris2_app""
export PATH="`dirname "$DIR"`/"idris2_app":$PATH"
"`dirname $DIR`"/"idris2_app/idris2-boot" "$@"

8885
bootstrap/idris2.rkt → bootstrap/idris2_app/idris2.rkt
View File

File diff suppressed because one or more lines are too long

8829
bootstrap/idris2_app/idris2.ss
View File

File diff suppressed because one or more lines are too long

2
config.mk
View File

@ -37,6 +37,8 @@ else
CFLAGS += -fPIC
endif
export OS
ifeq ($(OS),bsd)
MAKE := gmake
else

10
docs/source/backends/gambit.rst
View File

@ -8,9 +8,15 @@ The Gambit Scheme code generator can be accessed via the REPL command:
Main> :set cg gambit
Ergo, to run Idris programs with this generator, you will need to install
Alternatively, you can set it via the ``IDRIS2_CG`` environment variable:
::
$ export IDRIS2_CG=gambit
To run Idris programs with this generator, you will need to install
`Gambit Scheme <https://gambitscheme.org>`_. Gambit Scheme is free software,
and available via most pacakge managers.
and available via most package managers.
You can compile an expression ``expr`` of type ``IO ()`` to an executable as
follows, at the REPL:

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

@ -37,9 +37,22 @@ 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
the ``-o <output file>`` option:
::
$ idris2 hello.idr -o hello
This will compile the expression ``Main.main``, generating an executable
``hello`` (with an extension depending on the code generator) in the
``build/exec`` directory.
There are three code generators provided in Idris 2, and (later) there will be
a system for plugging in new code generators for a variety of targets. The
default is to compile via Chez Scheme, with an alternative via Racket or Gambit.
You can set the code generator at the REPL with the `:set codegen` command,
or via the `IDRIS2_CG` environment variable.
.. toctree::
:maxdepth: 1

36
docs/source/backends/racket.rst
View File

@ -8,4 +8,38 @@ The Racket code generator is accessed via a REPL command:
Main> :set cg racket
[More details TODO]
Alternatively, you can set it via the ``IDRIS2_CG`` environment variable:
::
$ export IDRIS2_CG=racket
You can compile an expression ``expr`` of type ``IO ()`` to an executable as
follows, at the REPL:
::
Main> :c execname expr
...where ``execname`` is the name of the executable file. This will generate
the following:
* A shell script ``build/exec/execname`` which invokes the program
* A subdirectory ``build/exec/execname_app`` which contains all the data necessary
to run the program. This includes the Racket source (``execname.rkt``),
the compiled Racket code (``execname`` or ``execname.exe`` on Windows)
and any shared libraries needed for foreign function definitions.
The executable ``execname`` is relocatable to any subdirectory, provided that
``execname_app`` is also in the same subdirectory.
You can also execute an expression directly:
::
Main> :exec expr
Again, ``expr`` must have type ``IO ()``. This will generate a temporary
executable script ``_tmpracket`` in the ``build/exec`` directory, and execute
that, without compiling to a binary first (so the resulting Racket code is
interpreted).

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

@ -5,8 +5,57 @@ Frequently Asked Questions
Can Idris 2 compile itself?
===========================
Not yet. Although it is written in Idris, there are several changes to the
language which are not fully backwards compatible (see Section
:ref:`updates-index`) so, although we hope to get there fairly soon - especially
since we are resisting using any of the more sophisticated language features -
it's not automatically the case that it will be able to compile itself.
Yes, Idris 2 is implemented in Idris 2. By default, it targets
`Chez Scheme <https://cisco.github.io/ChezScheme/>`_, so you can bootstrap
from the generated Scheme code, as described in Section :ref:`sect-starting`.
Why does Idris 2 target Scheme? Surely a dynamically typed target language is going to be slow?
===============================================================================================
You may be surprised at how fast Chez Scheme is :). `Racket <https://download.racket-lang.org/>`_,
as an alternative target, also performs well. Both perform better than the
Idris 1 back end, which is written in C but has not had the decades of
engineering effort by run time system specialists that Chez and Racket have.
Chez Scheme also allows us to turn off run time checks, which we do.
As anecdotal evidence of the performance improvement, as of 23rd May 2020, on a
Dell XPS 13 running Ubuntu, the performance is:
* Idris 2 (with the Chez Scheme runtime) checks its own source in 93 seconds.
* The bootstrapping Idris 2 (compiled with Idris 1) checks the same source in 125s.
* Idris 1 checks the bootstrapping Idris 2's source (the same as the above,
but with minor variations due to the syntax changes) in 768 seconds.
This is, nevertheless, not intended to be a long term solution, even if it
is a very convenient way to bootstrap.
Can Idris 2 generate Javascript? What about plug-in code generators?
====================================================================
Not yet, but there is a Javascript code generator in development.
Like Idris 1, Idris 2 will support plug-in code generation to allow you to
write a back end for the platform of your choice, but this is not yet
implemented.
What are the main differences between Idris 1 and Idris 2?
==========================================================
The most important difference is that Idris 2 explicitly represents *erasure*
in types, so that you can see at compile time which function and data type
arguments are erased, and which will be present at run time. You can see more
details in :ref:`sect-multiplicities`.
Idris 2 has significantly better type checking performance (perhaps even an
order of magnitude!) and generates significantly better code.
Also, being implemented in Idris, we've been able to take advantage of the
type system to remove some significant sources of bugs!
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
mostly still relevant.

4
docs/source/reference/envvars.rst
View File

@ -4,4 +4,6 @@
Environment Variables
*********************
[TODO: Fill in the environment variables recognised by Idris 2]
.. todo::
Fill in the environment variables recognised by Idris 2

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

@ -14,7 +14,7 @@ Lexical structure
constructor ``RF "foo"``)
* ``Foo.bar.baz`` starting with uppercase ``F`` is one lexeme, a namespaced
identifier: ``NSIdent ["baz", "bar", "Foo"]``
identifier: ``DotSepIdent ["baz", "bar", "Foo"]``
* ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
``.bar``, ``.baz``

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

@ -81,9 +81,9 @@ number as 0), we could write:
.. code-block:: idris
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
and will return the 5th fibonacci number. Note that while this works, this is not the
@ -114,7 +114,9 @@ any other character).
Cumulativity
============
[NOT YET IN IDRIS 2]
.. warning::
NOT YET IN IDRIS 2
Since values can appear in types and *vice versa*, it is natural that
types themselves have types. For example:

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

@ -64,7 +64,15 @@ the name of the module. The names defined in the ``BTree`` module are, in full:
If names are otherwise unambiguous, there is no need to give the fully
qualified name. Names can be disambiguated either by giving an explicit
qualification, or according to their type.
qualification, using the ``with`` keyword, or according to their type.
The ``with`` keyword in expressions comes in two variants:
* ``with BTree.insert (insert x empty)`` for one name
* ``with [BTree.insert, BTree.empty] (insert x empty)`` for multiple names
This is particularly useful with ``do`` notation, where it can often improve
error messages: ``with MyModule.(>>=) do ...``
There is no formal link between the module name and its filename,
although it is generally advisable to use the same name for each. An

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

@ -28,14 +28,14 @@ You can download the Idris 2 source from the `Idris web site
<https://www.idris-lang.org/pages/download.html>`_ or get the latest
development version from `idris-lang/Idris2
<https://github.com/idris-lang/Idris2>`_ on Github. This includes the Idris 2
source code and the Scheme code code generated from that. Once you have
source code and the Scheme code generated from that. Once you have
unpacked the source, you can install it as follows::
make bootstrap SCHEME=chez
Where `chez` is the executable name of the Chez Scheme compiler. This will
vary from system to system, but is often one of `scheme`, `chezscheme`, or
`chezscheme9.5`. If you are building via Racket, you can install it as
vary from system to system, but is often one of ``scheme``, ``chezscheme``, or
``chezscheme9.5``. If you are building via Racket, you can install it as
follows::
make bootstrap-racket

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

@ -126,7 +126,7 @@ To see more detail on what's going on, we can replace the recursive call to
``plusReducesZ`` with a hole:
.. code-block:: idris
plusReducesZ (S k) = cong S ?help
Then inspecting the type of the hole at the REPL shows us:
@ -361,7 +361,9 @@ total, a function ``f`` must:
Directives and Compiler Flags for Totality
------------------------------------------
[NOTE: Not all of this is implemented yet for Idris 2]
.. warning::
Not all of this is implemented yet for Idris 2
By default, Idris allows all well-typed definitions, whether total or not.
However, it is desirable for functions to be total as far as possible, as this

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

@ -234,6 +234,37 @@ of how this works in practice:
.. _sect-holes:
Totality and Covering
---------------------
By default, functions in Idris must be ``covering``. That is, there must be
patterns which cover all possible values of the inputs types. For example,
the following definition will give an error:
.. code-block:: idris
fromMaybe : Maybe a -> a
fromMaybe (Just x) = x
This gives an error because ``fromMaybe Nothing`` is not defined. Idris
reports:
::
frommaybe.idr:1:1--2:1:fromMaybe is not covering. Missing cases:
fromMaybe Nothing
You can override this with a ``partial`` annotation:
.. code-block:: idris
partial fromMaybe : Maybe a -> a
fromMaybe (Just x) = x
However, this is not advisable, and in general you should only do this during
the initial development of a function, or during debugging. If you try to
evaluate ``fromMaybe Nothing`` at run time you will get a run time error.
Holes
-----

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

@ -4,7 +4,9 @@
Views and the “``with``” rule
*****************************
[NOT UPDATED FOR IDRIS 2 YET]
.. warning::
NOT UPDATED FOR IDRIS 2 YET
Dependent pattern matching
==========================

12
docs/source/typedd/typedd.rst
View File

@ -77,6 +77,9 @@ confusing and potentially error prone. Instead, there is ``stringToNatOrZ`` in
In ``Loops.idr`` and ``ReadNum.idr`` add ``import Data.Strings`` and change ``cast`` to
``stringToNatOrZ``
In ``ReadNum.idr``, since functions must now be ``covering`` by default, add
a ``partial`` annotation to ``readNumber_v2``.
Chapter 6
---------
@ -137,6 +140,9 @@ longer part of the prelude, so add ``import Decidable.Equality``.
In ``ReverseVec.idr``, add ``import Data.Nat`` for the ``Nat`` proofs.
In ``Void.idr``, since functions must now be ``covering`` by default, add
a ``partial`` annotation to ``nohead`` and its helper function ``getHead``.
Chapter 9
---------
@ -306,6 +312,8 @@ In ``ArithCmd.idr``, update ``DivBy`` and ``import Data.Strings`` as above. Also
since export rules are per-namespace now, rather than per-file, you need to
export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
In ``StreamFail.idr``, add a ``partial`` annotation to ``labelWith``.
Chapter 12
----------
@ -453,4 +461,6 @@ In ``ATM.idr``, add:
Chapter 15
----------
TODO
.. todo::
This chapter.

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

@ -425,11 +425,29 @@ can see if we try evaluating ``myShow True`` at the REPL:
In fact, this is how interfaces are elaborated. However, ``%hint`` should be
used with care. Too many hints can lead to a large search space!
Record fields
-------------
Record fields can now be accessed via a ``.``. For example, if you have:
.. code-block:: idris
record Person where
constructor MkPerson
firstName, middleName, lastName : String
age : Int
and you have a record ``fred : Person``, then you can use ``fred.firstName``
to access the ``firstName`` field.
Totality and Coverage
---------------------
``%default covering`` is now the default status [Actually still TODO, but
planned soon!]
``%default covering`` is now the default status, so all functions must cover
all their inputs unless stated otherwise with a ``partial`` annotation, or
switching to ``%default partial`` (which is not recommended - use a ``partial``
annotation instead to have the smallest possible place where functions are
partial).
Build artefacts
---------------

3
idris2.ipkg
View File

@ -81,9 +81,12 @@ modules =
Idris.Version,
Parser.Lexer.Common,
Parser.Lexer.Package,
Parser.Lexer.Source,
Parser.Rule.Common,
Parser.Rule.Package,
Parser.Rule.Source,
Parser.Package,
Parser.Source,
Parser.Support,
Parser.Unlit,

3
idris2api.ipkg
View File

@ -81,9 +81,12 @@ modules =
Idris.Version,
Parser.Lexer.Common,
Parser.Lexer.Package,
Parser.Lexer.Source,
Parser.Rule.Common,
Parser.Rule.Package,
Parser.Rule.Source,
Parser.Package,
Parser.Source,
Parser.Support,
Parser.Unlit,

154
idris2rkt.ipkg
View File

@ -1,154 +0,0 @@
package idris2
modules =
Algebra,
Algebra.Preorder,
Algebra.Semiring,
Algebra.ZeroOneOmega,
Compiler.ANF,
Compiler.Common,
Compiler.CompileExpr,
Compiler.Inline,
Compiler.LambdaLift,
Compiler.Scheme.Chez,
Compiler.Scheme.Racket,
Compiler.Scheme.Gambit,
Compiler.Scheme.Common,
Compiler.VMCode,
Core.AutoSearch,
Core.Binary,
Core.CaseBuilder,
Core.CaseTree,
Core.Context,
Core.CompileExpr,
Core.Core,
Core.Coverage,
Core.Directory,
Core.Env,
Core.FC,
Core.GetType,
Core.Hash,
Core.InitPrimitives,
Core.LinearCheck,
Core.Metadata,
Core.Name,
Core.Normalise,
Core.Options,
Core.Primitives,
-- Core.Reflect,
Core.Termination,
Core.Transform,
Core.TT,
Core.TTC,
Core.Unify,
Core.UnifyState,
Core.Value,
Data.ANameMap,
Data.Bool.Extra,
Data.IntMap,
Data.LengthMatch,
Data.NameMap,
Data.StringMap,
Data.These,
Data.StringTrie,
IdrisPaths,
Idris.CommandLine,
Idris.Desugar,
Idris.Elab.Implementation,
Idris.Elab.Interface,
Idris.Error,
Idris.IDEMode.CaseSplit,
Idris.IDEMode.Commands,
Idris.IDEMode.MakeClause,
Idris.IDEMode.Parser,
Idris.IDEMode.REPL,
Idris.IDEMode.TokenLine,
Idris.ModTree,
Idris.Package,
Idris.Parser,
Idris.ProcessIdr,
Idris.REPL,
Idris.REPLCommon,
Idris.REPLOpts,
Idris.Resugar,
Idris.SetOptions,
Idris.Syntax,
Idris.Version,
Parser.Lexer.Common,
Parser.Lexer.Source,
Parser.Rule.Common,
Parser.Rule.Source,
Parser.Source,
Parser.Support,
Parser.Unlit,
Text.Lexer,
Text.Lexer.Core,
Text.Literate,
Text.Parser,
Text.Parser.Core,
Text.Quantity,
Text.Token,
TTImp.BindImplicits,
TTImp.Elab,
TTImp.Elab.Ambiguity,
TTImp.Elab.App,
TTImp.Elab.As,
TTImp.Elab.Binders,
TTImp.Elab.Case,
TTImp.Elab.Check,
TTImp.Elab.Delayed,
TTImp.Elab.Dot,
TTImp.Elab.Hole,
TTImp.Elab.ImplicitBind,
TTImp.Elab.Lazy,
TTImp.Elab.Local,
TTImp.Elab.Prim,
-- TTImp.Elab.Quote,
TTImp.Elab.Record,
TTImp.Elab.Rewrite,
TTImp.Elab.Term,
TTImp.Elab.Utils,
TTImp.Impossible,
TTImp.Interactive.CaseSplit,
TTImp.Interactive.ExprSearch,
TTImp.Interactive.GenerateDef,
TTImp.Interactive.MakeLemma,
TTImp.Parser,
TTImp.PartialEval,
TTImp.ProcessData,
TTImp.ProcessDecls,
TTImp.ProcessDef,
TTImp.ProcessParams,
TTImp.ProcessRecord,
TTImp.ProcessTransform,
TTImp.ProcessType,
-- TTImp.Reflect,
TTImp.TTImp,
TTImp.Unelab,
TTImp.Utils,
TTImp.WithClause,
Utils.Binary,
Utils.Hex,
Utils.Octal,
Utils.Shunting,
Utils.String,
Yaffle.Main,
Yaffle.REPL
opts = "--codegen racket"
depends = contrib, network
sourcedir = "src"
main = Idris.Main
executable = idris2

13
libs/base/Data/Buffer.idr
View File

@ -1,5 +1,6 @@
module Data.Buffer
import System.Directory
import System.File
export
@ -149,7 +150,7 @@ copyData src start len dest loc
-- else pure (Left FileReadError)
%foreign "scheme:blodwen-read-bytevec"
prim__readBufferFromFile : String -> PrimIO Buffer
prim__readBufferFromFile : String -> String -> PrimIO Buffer
%foreign "scheme:blodwen-isbytevec"
prim__isBuffer : Buffer -> Int
@ -159,20 +160,24 @@ prim__isBuffer : Buffer -> Int
export
createBufferFromFile : String -> IO (Either FileError Buffer)
createBufferFromFile fn
= do buf <- primIO (prim__readBufferFromFile fn)
= do Just cwd <- currentDir
| Nothing => pure (Left FileReadError)
buf <- primIO (prim__readBufferFromFile cwd fn)
if prim__isBuffer buf /= 0
then pure (Left FileReadError)
else do let sz = prim__bufferSize buf
pure (Right buf)
%foreign "scheme:blodwen-write-bytevec"
prim__writeBuffer : String -> Buffer -> Int -> PrimIO Int
prim__writeBuffer : String -> String -> Buffer -> Int -> PrimIO Int
export
writeBufferToFile : String -> Buffer -> (maxbytes : Int) ->
IO (Either FileError ())
writeBufferToFile fn buf max
= do res <- primIO (prim__writeBuffer fn buf max)
= do Just cwd <- currentDir
| Nothing => pure (Left FileReadError)
res <- primIO (prim__writeBuffer cwd fn buf max)
if res /= 0
then pure (Left FileWriteError)
else pure (Right ())

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

@ -159,7 +159,7 @@ split : (a -> Bool) -> List a -> List (List a)
split p xs =
case break p xs of
(chunk, []) => [chunk]
(chunk, (c :: rest)) => chunk :: split p rest
(chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)
public export
splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)

94
libs/base/Data/Nat.idr
View File

@ -170,7 +170,7 @@ export
SIsNotZ : (S x = Z) -> Void
SIsNotZ Refl impossible
export
export partial
modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
modNatNZ left Z p = void (p Refl)
modNatNZ left (S right) _ = mod' left left right
@ -183,11 +183,11 @@ modNatNZ left (S right) _ = mod' left left right
else
mod' left (minus centre (S right)) right
export
export partial
modNat : Nat -> Nat -> Nat
modNat left (S right) = modNatNZ left (S right) SIsNotZ
export
export partial
divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
divNatNZ left Z p = void (p Refl)
divNatNZ left (S right) _ = div' left left right
@ -200,17 +200,17 @@ divNatNZ left (S right) _ = div' left left right
else
S (div' left (minus centre (S right)) right)
export
export partial
divNat : Nat -> Nat -> Nat
divNat left (S right) = divNatNZ left (S right) SIsNotZ
export
export partial
divCeilNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
divCeilNZ x y p = case (modNatNZ x y p) of
Z => divNatNZ x y p
S _ => S (divNatNZ x y p)
export
export partial
divCeil : Nat -> Nat -> Nat
divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
@ -225,7 +225,7 @@ gcd a Z = a
gcd Z b = b
gcd a (S b) = gcd (S b) (modNatNZ a (S b) SIsNotZ)
export
export partial
lcm : Nat -> Nat -> Nat
lcm _ Z = Z
lcm Z _ = Z
@ -415,3 +415,83 @@ multOneRightNeutral (S left) =
let inductiveHypothesis = multOneRightNeutral left in
rewrite inductiveHypothesis in
Refl
-- Proofs on -
export
minusSuccSucc : (left : Nat) -> (right : Nat) -> minus (S left) (S right) = minus left right
minusSuccSucc left right = Refl
export
minusZeroLeft : (right : Nat) -> minus 0 right = Z
minusZeroLeft right = Refl
export
minusZeroRight : (left : Nat) -> minus left 0 = left
minusZeroRight Z = Refl
minusZeroRight (S left) = Refl
export
minusZeroN : (n : Nat) -> Z = minus n n
minusZeroN Z = Refl
minusZeroN (S n) = minusZeroN n
export
minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
minusOneSuccN Z = Refl
minusOneSuccN (S n) = minusOneSuccN n
export
minusSuccOne : (n : Nat) -> minus (S n) 1 = n
minusSuccOne Z = Refl
minusSuccOne (S n) = Refl
export
minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z
minusPlusZero Z m = Refl
minusPlusZero (S n) m = minusPlusZero n m
export
minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
minus (minus left centre) right = minus left (centre + right)
minusMinusMinusPlus Z Z right = Refl
minusMinusMinusPlus (S left) Z right = Refl
minusMinusMinusPlus Z (S centre) right = Refl
minusMinusMinusPlus (S left) (S centre) right =
let inductiveHypothesis = minusMinusMinusPlus left centre right in
rewrite inductiveHypothesis in
Refl
export
plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
minus (left + right) (left + right') = minus right right'
plusMinusLeftCancel Z right right' = Refl
plusMinusLeftCancel (S left) right right' =
let inductiveHypothesis = plusMinusLeftCancel left right right' in
rewrite inductiveHypothesis in
Refl
export
multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
(minus left centre) * right = minus (left * right) (centre * right)
multDistributesOverMinusLeft Z Z right = Refl
multDistributesOverMinusLeft (S left) Z right =
rewrite (minusZeroRight (plus right (mult left right))) in Refl
multDistributesOverMinusLeft Z (S centre) right = Refl
multDistributesOverMinusLeft (S left) (S centre) right =
let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
rewrite inductiveHypothesis in
rewrite plusMinusLeftCancel right (mult left right) (mult centre right) in
Refl
export
multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
left * (minus centre right) = minus (left * centre) (left * right)
multDistributesOverMinusRight left centre right =
rewrite multCommutative left (minus centre right) in
rewrite multDistributesOverMinusLeft centre right left in
rewrite multCommutative centre left in
rewrite multCommutative right left in
Refl

4
libs/base/Data/Strings.idr
View File

@ -167,11 +167,11 @@ export
toLower : String -> String
toLower str = pack (map toLower (unpack str))
export
export partial
strIndex : String -> Int -> Char
strIndex = prim__strIndex
export
export partial
strTail : String -> String
strTail = prim__strTail

20
libs/base/System/Directory.idr
View File

@ -35,14 +35,14 @@ prim_changeDir : String -> PrimIO Int
%foreign support "idris2_createDir"
prim_createDir : String -> PrimIO Int
%foreign support "idris2_dirOpen"
%foreign support "idris2_openDir"
prim_openDir : String -> PrimIO DirPtr
%foreign support "idris2_dirClose"
%foreign support "idris2_closeDir"
prim_closeDir : DirPtr -> PrimIO ()
%foreign support "idris2_rmDir"
prim_rmDir : String -> PrimIO ()
%foreign support "idris2_removeDir"
prim_removeDir : String -> PrimIO ()
%foreign support "idris2_nextDirEntry"
prim_dirEntry : DirPtr -> PrimIO (Ptr String)
@ -74,20 +74,20 @@ currentDir
else pure (Just (prim__getString res))
export
dirOpen : String -> IO (Either FileError Directory)
dirOpen d
openDir : String -> IO (Either FileError Directory)
openDir d
= do res <- primIO (prim_openDir d)
if prim__nullAnyPtr res /= 0
then returnError
else ok (MkDir res)
export
dirClose : Directory -> IO ()
dirClose (MkDir d) = primIO (prim_closeDir d)
closeDir : Directory -> IO ()
closeDir (MkDir d) = primIO (prim_closeDir d)
export
rmDir : String -> IO ()
rmDir dirName = primIO (prim_rmDir dirName)
removeDir : String -> IO ()
removeDir dirName = primIO (prim_removeDir dirName)
export
dirEntry : Directory -> IO (Either FileError String)

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

@ -31,7 +31,7 @@ prim__readLine : FilePtr -> PrimIO (Ptr String)
%foreign support "idris2_readChars"
prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
%foreign support "fgetc"
prim__readChar : FilePtr -> PrimIO Char
prim__readChar : FilePtr -> PrimIO Int
%foreign support "idris2_writeLine"
prim__writeLine : FilePtr -> String -> PrimIO Int
%foreign support "idris2_eof"
@ -39,8 +39,8 @@ prim__eof : FilePtr -> PrimIO Int
%foreign "C:fflush,libc 6"
prim__flush : FilePtr -> PrimIO Int
%foreign support "idris2_fileRemove"
prim__fileRemove : String -> PrimIO Int
%foreign support "idris2_removeFile"
prim__removeFile : String -> PrimIO Int
%foreign support "idris2_fileSize"
prim__fileSize : FilePtr -> PrimIO Int
%foreign support "idris2_fileSize"
@ -159,7 +159,7 @@ fGetChar (FHandle h)
ferr <- primIO (prim_error h)
if (ferr /= 0)
then returnError
else ok c
else ok (cast c)
export
fPutStr : (h : File) -> String -> IO (Either FileError ())
@ -210,9 +210,9 @@ fileStatusTime (FHandle f)
else returnError
export
fileRemove : String -> IO (Either FileError ())
fileRemove fname
= do res <- primIO (prim__fileRemove fname)
removeFile : String -> IO (Either FileError ())
removeFile fname
= do res <- primIO (prim__removeFile fname)
if res == 0
then ok ()
else returnError
@ -265,7 +265,7 @@ writeFile fn contents = do
closeFile h
pure (Right ())
namespace FileMode
namespace FileMode
public export
data FileMode = Read | Write | Execute

3
libs/contrib/Language/JSON/Data.idr
View File

@ -38,7 +38,8 @@ intToHexString n =
13 => "D"
14 => "E"
15 => "F"
other => intToHexString (shiftR n 4) ++ intToHexString (mod n 16)
other => assert_total $
intToHexString (shiftR n 4) ++ intToHexString (mod n 16)
private
showChar : Char -> String

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

@ -349,7 +349,7 @@ unc = do count (exactly 2) $ match $ PTPunct '\\'
server <- match PTText
bodySeparator
share <- match PTText
pure $ UNC server share
Core.pure $ UNC server share
-- Example: \\?\server\share
private
@ -358,7 +358,7 @@ verbatimUnc = do verbatim
server <- match PTText
bodySeparator
share <- match PTText
pure $ UNC server share
Core.pure $ UNC server share
-- Example: C:
private

2
libs/contrib/Text/Parser/Core.idr
View File

@ -29,7 +29,7 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
||| guaranteed to consume some input. If the first one consumes input, the
||| second is allowed to be recursive (because it means some input has been
||| consumed and therefore the input is smaller)
public export %inline
public export %inline %tcinline
(>>=) : {c1, c2 : Bool} ->
Grammar tok c1 a ->
inf c1 (a -> Grammar tok c2 b) ->

58
libs/network/Echo.idr
View File

@ -1,58 +0,0 @@
module Main
import System
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw
%cg chez libidris_net
runServer : IO (Either String (Port, ThreadID))
runServer = do
Right sock <- socket AF_INET Stream 0
| Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
res <- bind sock (Just (Hostname "localhost")) 0
if res /= 0
then pure (Left $ "Failed to bind socket with error: " ++ show res)
else do
port <- getSockPort sock
res <- listen sock
if res /= 0
then pure (Left $ "Failed to listen on socket with error: " ++ show res)
else do
forked <- fork (serve port sock)
pure $ Right (port, forked)
where
serve : Port -> Socket -> IO ()
serve port sock = do
Right (s, _) <- accept sock
| Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
Right (str, _) <- recv s 1024
| Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
putStrLn ("Received: " ++ str)
Right n <- send s ("echo: " ++ str)
| Left err => putStrLn ("Server failed to send data with error: " ++ show err)
pure ()
runClient : Port -> IO ()
runClient serverPort = do
Right sock <- socket AF_INET Stream 0
| Left fail => putStrLn ("Failed to open socket: " ++ show fail)
res <- connect sock (Hostname "localhost") serverPort
if res /= 0
then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res)
else do
Right n <- send sock ("hello world!")
| Left err => putStrLn ("Client failed to send data with error: " ++ show err)
Right (str, _) <- recv sock 1024
| Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
-- assuming that stdout buffers get flushed in between system calls, this is "guaranteed"
-- to be printed after the server prints its own message
putStrLn ("Received: " ++ str)
main : IO ()
main = do
Right (serverPort, tid) <- runServer
| Left err => putStrLn $ "[server] " ++ err
runClient serverPort

56
libs/network/Makefile
View File

@ -1,58 +1,8 @@
include ../../config.mk
INSTALLDIR = ${PREFIX}/idris2-${IDRIS2_VERSION}/network/lib
IDRIS_SRCS = Network/Socket.idr Network/Socket/Data.idr Network/Socket/Raw.idr
TARGET = idris_net
SRCS = idris_net.c
OBJS = $(SRCS:.c=.o)
DEPS = $(OBJS:.o=.d)
ifeq ($(OS), windows)
LDFLAGS += -lws2_32
endif
all: $(TARGET)$(SHLIB_SUFFIX)
all:
${IDRIS2} --build network.ipkg
build: $(TARGET)$(SHLIB_SUFFIX) $(IDRIS_SRCS)
@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
${IDRIS2} --build network.ipkg
$(TARGET)$(SHLIB_SUFFIX): $(OBJS)
$(CC) -shared -o $@ $^ $(LDFLAGS)
-include $(DEPS)
%.d: %.c
@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@
.PHONY: clean
clean :
$(RM) $(OBJS) $(TARGET)$(SHLIB_SUFFIX)
$(RM) -r build
cleandep: clean
$(RM) $(DEPS)
.PHONY: install
install:
@if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi
${IDRIS2} --install network.ipkg
@if ! [ -d $(INSTALLDIR) ]; then mkdir -p $(INSTALLDIR); fi
install $(TARGET)$(SHLIB_SUFFIX) $(wildcard *.h) $(INSTALLDIR)
test: build test.c
$(CC) -o network-tests -L. -I. test.c $(TARGET)$(SHLIB_SUFFIX)
LD_LIBRARY_PATH=. ./network-tests
@$(RM) ./network-tests test.o
clean:
$(RM) -r build

64
libs/network/Network/FFI.idr
View File

@ -7,143 +7,143 @@ import Network.Socket.Data
-- From sys/socket.h
%foreign "C:close,idris_net"
%foreign "C:close,libidris2_support"
export
socket_close : (sockdes : SocketDescriptor) -> PrimIO Int
%foreign "C:listen,idris_net"
%foreign "C:listen,libidris2_support"
export
socket_listen : (sockfd : SocketDescriptor) -> (backlog : Int) -> PrimIO Int
-- From idris_net.h
%foreign "C:idrnet_socket,idris_net"
%foreign "C:idrnet_socket,libidris2_support"
export
idrnet_socket : (domain, type, protocol : Int) -> PrimIO Int
%foreign "C:idrnet_bind,idris_net"
%foreign "C:idrnet_bind,libidris2_support"
export
idrnet_bind : (sockfd : SocketDescriptor) -> (family, socket_type : Int) -> (host : String)
-> (port : Port) -> PrimIO Int
%foreign "C:idrnet_connect,idris_net"
%foreign "C:idrnet_connect,libidris2_support"
export
idrnet_connect : (sockfd : SocketDescriptor) -> (family, socket_type : Int) -> (host : String)
-> (port : Port) -> PrimIO Int
%foreign "C:idrnet_sockaddr_family,idris_net"
%foreign "C:idrnet_sockaddr_family,libidris2_support"
export
idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_sockaddr_ipv4,idris_net"
%foreign "C:idrnet_sockaddr_ipv4,libidris2_support"
export
idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String
%foreign "C:idrnet_sockaddr_ipv4_port,idris_net"
%foreign "C:idrnet_sockaddr_ipv4_port,libidris2_support"
export
idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_sockaddr_port,idris_net"
%foreign "C:idrnet_sockaddr_port,libidris2_support"
export
idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int
%foreign "C:idrnet_create_sockaddr,idris_net"
%foreign "C:idrnet_create_sockaddr,libidris2_support"
export
idrnet_create_sockaddr : PrimIO AnyPtr
%foreign "C:idrnet_accept,idris_net"
%foreign "C:idrnet_accept,libidris2_support"
export
idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_send,idris_net"
%foreign "C:idrnet_send,libidris2_support"
export
idrnet_send : (sockfd : SocketDescriptor) -> (dataString : String) -> PrimIO Int
%foreign "C:idrnet_send_buf,idris_net"
%foreign "C:idrnet_send_buf,libidris2_support"
export
idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int
%foreign "C:idrnet_recv,idris_net"
%foreign "C:idrnet_recv,libidris2_support"
export
idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
%foreign "C:idrnet_recv_buf,idris_net"
%foreign "C:idrnet_recv_buf,libidris2_support"
export
idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int)
-> PrimIO Int
%foreign "C:idrnet_sendto,idris_net"
%foreign "C:idrnet_sendto,libidris2_support"
export
idrnet_sendto : (sockfd : SocketDescriptor) -> (dataString,host : String)
-> (port : Port) -> (family : Int) -> PrimIO Int
%foreign "C:idrnet_sendto_buf,idris_net"
%foreign "C:idrnet_sendto_buf,libidris2_support"
export
idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) -> (buf_len : Int)
-> (host : String) -> (port : Port) -> (family : Int) -> PrimIO Int
%foreign "C:idrnet_recvfrom,idris_net"
%foreign "C:idrnet_recvfrom,libidris2_support"
export
idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
%foreign "C:idrnet_recvfrom_buf,idris_net"
%foreign "C:idrnet_recvfrom_buf,libidris2_support"
export
idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int)
-> PrimIO AnyPtr
%foreign "C:idrnet_get_recv_res,idris_net"
%foreign "C:idrnet_get_recv_res,libidris2_support"
export
idrnet_get_recv_res : (res_struct : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_get_recv_payload,idris_net"
%foreign "C:idrnet_get_recv_payload,libidris2_support"
export
idrnet_get_recv_payload : (res_struct : AnyPtr) -> PrimIO String
%foreign "C:idrnet_free_recv_struct,idris_net"
%foreign "C:idrnet_free_recv_struct,libidris2_support"
export
idrnet_free_recv_struct : (res_struct : AnyPtr) -> PrimIO ()
%foreign "C:idrnet_get_recvfrom_res,idris_net"
%foreign "C:idrnet_get_recvfrom_res,libidris2_support"
export
idrnet_get_recvfrom_res : (res_struct : AnyPtr) -> PrimIO Int
%foreign "C:idrnet_get_recvfrom_payload,idris_net"
%foreign "C:idrnet_get_recvfrom_payload,libidris2_support"
export
idrnet_get_recvfrom_payload : (res_struct : AnyPtr) -> PrimIO String
%foreign "C:idrnet_get_recvfrom_sockaddr,idris_net"
%foreign "C:idrnet_get_recvfrom_sockaddr,libidris2_support"
export
idrnet_get_recvfrom_sockaddr : (res_struct : AnyPtr) -> PrimIO AnyPtr
%foreign "C:idrnet_free_recvfrom_struct,idris_net"
%foreign "C:idrnet_free_recvfrom_struct,libidris2_support"
export
idrnet_free_recvfrom_struct : (res_struct : AnyPtr) -> PrimIO ()
%foreign "C:idrnet_geteagain,idris_net"
%foreign "C:idrnet_geteagain,libidris2_support"
export
idrnet_geteagain : PrimIO Int
%foreign "C:idrnet_errno,idris_net"
%foreign "C:idrnet_errno,libidris2_support"
export
idrnet_errno : PrimIO Int
%foreign "C:idrnet_malloc,idris_net"
%foreign "C:idrnet_malloc,libidris2_support"
export
idrnet_malloc : (size : Int) -> PrimIO AnyPtr
%foreign "C:idrnet_free,idris_net"
%foreign "C:idrnet_free,libidris2_support"
export
idrnet_free : (ptr : AnyPtr) -> PrimIO ()
%foreign "C:idrnet_peek,idris_net"
%foreign "C:idrnet_peek,libidris2_support"
export
idrnet_peek : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> PrimIO {-Unsigned-} Int
%foreign "C:idrnet_poke,idris_net"
%foreign "C:idrnet_poke,libidris2_support"
export
idrnet_poke : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> (val : Int {- should be Char? -})
-> PrimIO ()

8
libs/network/Network/Socket/Data.idr
View File

@ -10,8 +10,6 @@ import Data.Strings
-- ------------------------------------------------------------ [ Type Aliases ]
%cg chez "libidris_net"
public export
ByteLength : Type
ByteLength = Int
@ -49,7 +47,7 @@ BACKLOG : Int
BACKLOG = 20
-- Repeat to avoid a dependency cycle
%foreign "C:idrnet_geteagain,idris_net"
%foreign "C:idrnet_geteagain,libidris2_support"
idrnet_geteagain : PrimIO Int
export
@ -62,10 +60,10 @@ EAGAIN =
-- ---------------------------------------------------------------- [ Error Code ]
-- repeat without export to avoid dependency cycles
%foreign "C:idrnet_errno,idris_net"
%foreign "C:idrnet_errno,libidris2_support"
idrnet_errno : PrimIO Int
%foreign "C:isNull,idris_net"
%foreign "C:isNull,libidris2_support"
idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int

2
libs/network/expected
View File

@ -1,2 +0,0 @@
Received: hello world!
Received: echo: hello world!

58
libs/network/test.c
View File

@ -1,58 +0,0 @@
#include <assert.h>
#include <stdio.h>
#ifndef _WIN32
#include <netinet/in.h>
#include <arpa/inet.h>
#endif
#include "idris_net.h"
void test_sockaddr_port_returns_random_port_when_bind_port_is_0() {
int sock = idrnet_socket(AF_INET, 1, 0);
assert(sock > 0);
int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 0);
assert(res == 0);
res = idrnet_sockaddr_port(sock);
assert(res > 0);
close(sock);
}
void test_sockaddr_port_returns_explicitly_assigned_port() {
int sock = idrnet_socket(AF_INET, 1, 0);
assert(sock > 0);
int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 34567);
assert(res == 0);
res = idrnet_sockaddr_port(sock);
assert(res == 34567);
close(sock);
}
void test_peek_and_poke_buffer() {
void *buf = idrnet_malloc(100);
assert(buf > 0);
for (int i = 0; i < 100; i++) {
idrnet_poke(buf,i,7*i);
}
for(int i = 0; i < 100; i++) {
assert (idrnet_peek(buf,i) == (0xff & 7*i));
}
idrnet_free(buf);
}
int main(void) {
test_sockaddr_port_returns_explicitly_assigned_port();
test_sockaddr_port_returns_random_port_when_bind_port_is_0();
test_peek_and_poke_buffer();
printf("network library tests SUCCESS\n");
return 0;
}

3
libs/prelude/Builtin.idr
View File

@ -6,6 +6,9 @@ module Builtin
||| Assert to the totality checker that the given expression will always
||| terminate.
||| Note: assert_total can reduce at compile time, if required for unification,
||| which might mean that it's no longer guarded a subexpression. Therefore,
||| it is best to use it around the smallest possible subexpression.
%inline
public export
assert_total : {0 a : _} -> a -> a

10
libs/prelude/Prelude.idr
View File

@ -117,7 +117,7 @@ public export
||| Equality is a congruence.
public export
cong : (f : t -> u) -> (1 p : a = b) -> f a = f b
cong : (0 f : t -> u) -> (1 p : a = b) -> f a = f b
cong f Refl = Refl
||| A canonical proof that some type is empty.
@ -353,14 +353,18 @@ interface Num ty => Abs ty where
public export
interface Num ty => Fractional ty where
partial
(/) : ty -> ty -> ty
partial
recip : ty -> ty
recip x = 1 / x
public export
interface Num ty => Integral ty where
partial
div : ty -> ty -> ty
partial
mod : ty -> ty -> ty
----- Instances for primitives
@ -1117,13 +1121,13 @@ fastPack xs
||| ```
public export
unpack : String -> List Char
unpack str = assert_total $ unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
unpack str = unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
where
unpack' : Int -> Int -> String -> List Char
unpack' pos len str
= if pos >= len
then []
else (prim__strIndex str pos) :: unpack' (pos + 1) len str
else assert_total (prim__strIndex str pos) :: assert_total (unpack' (pos + 1) len str)
public export
Semigroup String where

10
src/Compiler/Common.idr
View File

@ -145,6 +145,11 @@ getAllDesc (n@(Resolved i) :: rest) arr defs
getAllDesc (n :: rest) arr defs
= getAllDesc rest arr defs
warnIfHole : Name -> NamedDef -> Core ()
warnIfHole n (MkNmError _)
= coreLift $ putStrLn $ "Warning: compiling hole " ++ show n
warnIfHole n _ = pure ()
getNamedDef : {auto c : Ref Ctxt Defs} ->
Name -> Core (Maybe (Name, FC, NamedDef))
getNamedDef n
@ -153,7 +158,8 @@ getNamedDef n
Nothing => pure Nothing
Just def => case namedcompexpr def of
Nothing => pure Nothing
Just d => pure (Just (n, location def, d))
Just d => do warnIfHole n d
pure (Just (n, location def, d))
replaceEntry : {auto c : Ref Ctxt Defs} ->
(Int, Maybe Binary) -> Core ()
@ -391,7 +397,7 @@ copyLib (lib, fullname)
= if lib == fullname
then pure ()
else do Right bin <- coreLift $ readFromFile fullname
| Left err => throw (FileErr fullname err)
| Left err => pure () -- assume a system library installed globally
Right _ <- coreLift $ writeToFile lib bin
| Left err => throw (FileErr lib err)
pure ()

2
src/Compiler/CompileExpr.idr
View File

@ -438,7 +438,7 @@ mutual
= toCExpTree n sc
toCExpTree' n (Case _ x scTy [])
= pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n
toCExpTree' n (STerm tm) = toCExp n tm
toCExpTree' n (STerm _ tm) = toCExp n tm
toCExpTree' n (Unmatched msg)
= pure $ CCrash emptyFC msg
toCExpTree' n Impossible

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

@ -55,11 +55,13 @@ findLibs ds
then Just (trim (substr 3 (length d) d))
else Nothing
escapeQuotes : String -> String
escapeQuotes s = pack $ foldr escape [] $ unpack s
escapeString : String -> String
escapeString s = pack $ foldr escape [] $ unpack s
where
escape : Char -> List Char -> List Char
escape '"' cs = '\\' :: '\"' :: cs
escape '\\' cs = '\\' :: '\\' :: cs
escape c cs = c :: cs
schHeader : String -> List String -> String
@ -69,9 +71,10 @@ schHeader chez libs
"(case (machine-type)\n" ++
" [(i3le ti3le a6le ta6le) (load-shared-object \"libc.so.6\")]\n" ++
" [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++
" [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++
" [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")" ++
" (load-shared-object \"ws2_32.dll\")]\n" ++
" [else (load-shared-object \"libc.so\")])\n\n" ++
showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeQuotes x ++ "\")") libs) ++ "\n\n" ++
showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeString x ++ "\")") libs) ++ "\n\n" ++
"(let ()\n"
schFooter : String
@ -181,7 +184,7 @@ cCall appdir fc cfn clib args ret
copyLib (appdir ++ dirSep ++ fname, fullname)
put Loaded (clib :: loaded)
pure $ "(load-shared-object \""
++ escapeQuotes fname
++ escapeString fname
++ "\")\n"
argTypes <- traverse (\a => cftySpec fc (snd a)) args
retType <- cftySpec fc ret
@ -320,17 +323,17 @@ startChezCmd : String -> String -> String -> String
startChezCmd chez appdir target = unlines
[ "@echo off"
, "set APPDIR=%~dp0"
, "set PATH=%APPDIR%;%PATH%"
, chez ++ " --script %APPDIR%/" ++ target ++ " %*"
, "set PATH=%APPDIR%\\" ++ appdir ++ ";%PATH%"
, "\"" ++ chez ++ "\" --script \"%APPDIR%/" ++ target ++ "\" %*"
]
startChezWinSh : String -> String -> String -> String
startChezWinSh chez appdir target = unlines
[ "#!/bin/sh"
, "DIR=\"`realpath $0`\""
, "DIR=\"`realpath \"$0\"`\""
, "CHEZ=$(cygpath \"" ++ chez ++"\")"
, "export PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$PATH\""
, "$CHEZ --script \"`dirname \"$DIR\"`\"/\"" ++ target ++ "\" \"$@\""
, "$CHEZ --script \"$(dirname \"$DIR\")/" ++ target ++ "\" \"$@\""
]
||| Compile a TT expression to Chez Scheme
@ -372,7 +375,7 @@ compileToSO chez appDirRel outSsAbs
Right () <- coreLift $ writeFile tmpFileAbs build
| Left err => throw (FileErr tmpFileAbs err)
coreLift $ chmodRaw tmpFileAbs 0o755
coreLift $ system (chez ++ " --script " ++ tmpFileAbs)
coreLift $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
pure ()
makeSh : String -> String -> String -> Core ()

2
src/Compiler/Scheme/Common.idr
View File

@ -131,7 +131,7 @@ schOp (Cast IntegerType DoubleType) [x] = op "exact->inexact" [x]
schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x]
schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x]
schOp (Cast IntType CharType) [x] = op "integer->char" [x]
schOp (Cast IntType CharType) [x] = op "cast-int-char" [x]
schOp (Cast from to) [x] = "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")"

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

@ -152,9 +152,9 @@ handleRet ret op = mkWorld (cToRkt ret op)
cCall : {auto f : Ref Done (List String) } ->
{auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
FC -> (cfn : String) -> (clib : String) ->
String -> FC -> (cfn : String) -> (clib : String) ->
List (Name, CFType) -> CFType -> Core (String, String)
cCall fc cfn libspec args ret
cCall appdir fc cfn libspec args ret
= do loaded <- get Loaded
bound <- get Done
@ -162,8 +162,8 @@ cCall fc cfn libspec args ret
lib <- if libn `elem` loaded
then pure ""
else do put Loaded (libn :: loaded)
ldata <- locate libspec
copyLib ldata
(fname, fullname) <- locate libspec
copyLib (appdir ++ dirSep ++ fname, fullname)
pure (loadlib libn vers)
argTypes <- traverse (\a => do s <- cftySpec fc (snd a)
@ -230,18 +230,18 @@ schemeCall fc sfn argns ret
useCC : {auto f : Ref Done (List String) } ->
{auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
useCC fc [] args ret
String -> FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
useCC appdir fc [] args ret
= throw (GenericMsg fc "No recognised foreign calling convention")
useCC fc (cc :: ccs) args ret
useCC appdir fc (cc :: ccs) args ret
= case parseCC cc of
Nothing => useCC fc ccs args ret
Nothing => useCC appdir fc ccs args ret
Just ("scheme", [sfn]) =>
do body <- schemeCall fc sfn (map fst args) ret
pure ("", body)
Just ("C", [cfn, clib]) => cCall fc cfn clib args ret
Just ("C", [cfn, clib, chdr]) => cCall fc cfn clib args ret
_ => useCC fc ccs args ret
Just ("C", [cfn, clib]) => cCall appdir fc cfn clib args ret
Just ("C", [cfn, clib, chdr]) => cCall appdir fc cfn clib args ret
_ => useCC appdir fc ccs args ret
-- For every foreign arg type, return a name, and whether to pass it to the
-- foreign call (we don't pass '%World')
@ -271,31 +271,56 @@ schFgnDef : {auto f : Ref Done (List String) } ->
{auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
{auto s : Ref Structs (List String)} ->
FC -> Name -> NamedDef -> Core (String, String)
schFgnDef fc n (MkNmForeign cs args ret)
String -> FC -> Name -> NamedDef -> Core (String, String)
schFgnDef appdir fc n (MkNmForeign cs args ret)
= do let argns = mkArgs 0 args
let allargns = map fst argns
let useargns = map fst (filter snd argns)
argStrs <- traverse mkStruct args
retStr <- mkStruct ret
(load, body) <- useCC fc cs (zip useargns args) ret
(load, body) <- useCC appdir fc cs (zip useargns args) ret
defs <- get Ctxt
pure (concat argStrs ++ retStr ++ load,
"(define " ++ schName !(full (gamma defs) n) ++
" (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
body ++ "))\n")
schFgnDef _ _ _ = pure ("", "")
schFgnDef _ _ _ _ = pure ("", "")
getFgnCall : {auto f : Ref Done (List String) } ->
{auto c : Ref Ctxt Defs} ->
{auto l : Ref Loaded (List String)} ->
{auto s : Ref Structs (List String)} ->
(Name, FC, NamedDef) -> Core (String, String)
getFgnCall (n, fc, d) = schFgnDef fc n d
String -> (Name, FC, NamedDef) -> Core (String, String)
getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d
startRacket : String -> String -> String -> String
startRacket racket appdir target = unlines
[ "#!/bin/sh"
, ""
, "DIR=\"`realpath $0`\""
, "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" ++ appdir ++ "\"\""
, racket ++ "\"`dirname \"$DIR\"`\"/\"" ++ target ++ "\" \"$@\""
]
startRacketCmd : String -> String -> String -> String
startRacketCmd racket appdir target = unlines
[ "@echo off"
, "set APPDIR=%~dp0"
, "set PATH=%APPDIR%\\" ++ appdir ++ ";%PATH%"
, racket ++ "\"" ++ target ++ "\" %*"
]
startRacketWinSh : String -> String -> String -> String
startRacketWinSh racket appdir target = unlines
[ "#!/bin/sh"
, "DIR=\"`realpath \"$0\"`\""
, "export PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$PATH\""
, racket ++ "\"" ++ target ++ "\" \"$@\""
]
compileToRKT : Ref Ctxt Defs ->
ClosedTerm -> (outfile : String) -> Core ()
compileToRKT c tm outfile
String -> ClosedTerm -> (outfile : String) -> Core ()
compileToRKT c appdir tm outfile
= do cdata <- getCompileData Cases tm
let ndefs = namedDefs cdata
let ctm = forget (mainExpr cdata)
@ -304,7 +329,7 @@ compileToRKT c tm outfile
f <- newRef {t = List String} Done empty
l <- newRef {t = List String} Loaded []
s <- newRef {t = List String} Structs []
fgndefs <- traverse getFgnCall ndefs
fgndefs <- traverse (getFgnCall appdir) ndefs
compdefs <- traverse (getScheme racketPrim racketString) ndefs
let code = fastAppend (map snd fgndefs ++ compdefs)
main <- schExp racketPrim racketString 0 ctm
@ -318,28 +343,68 @@ compileToRKT c tm outfile
coreLift $ chmodRaw outfile 0o755
pure ()
compileExpr : Ref Ctxt Defs -> (execDir : String) ->
makeSh : String -> String -> String -> String -> Core ()
makeSh racket outShRel appdir outAbs
= do Right () <- coreLift $ writeFile outShRel (startRacket racket appdir outAbs)
| Left err => throw (FileErr outShRel err)
pure ()
||| Make Windows start scripts, one for bash environments and one batch file
makeShWindows : String -> String -> String -> String -> Core ()
makeShWindows racket outShRel appdir outAbs
= do let cmdFile = outShRel ++ ".cmd"
Right () <- coreLift $ writeFile cmdFile (startRacketCmd racket appdir outAbs)
| Left err => throw (FileErr cmdFile err)
Right () <- coreLift $ writeFile outShRel (startRacketWinSh racket appdir outAbs)
| Left err => throw (FileErr outShRel err)
pure ()
compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr c execDir tm outfile
= do let outSs = execDir ++ dirSep ++ outfile ++ ".rkt"
let outBin = execDir ++ dirSep ++ outfile
compileToRKT c tm outSs
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)
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
compileToRKT c appDirGen tm outRktAbs
raco <- coreLift findRacoExe
ok <- coreLift $ system (raco ++ " -o " ++ outBin ++ " " ++ outSs)
racket <- coreLift findRacket
ok <- the (Core Int) $ if mkexec
then logTime "Build racket" $
coreLift $
system (raco ++ " -o " ++ outBinAbs ++ " " ++ outRktAbs)
else pure 0
if ok == 0
then pure (Just outfile)
then do -- TODO: add launcher script
let outShRel = execDir ++ dirSep ++ outfile
the (Core ()) $ if isWindows
then if mkexec
then makeShWindows "" outShRel appDirRel outBinFile
else makeShWindows (racket ++ " ") outShRel appDirRel outRktFile
else if mkexec
then makeSh "" outShRel appDirRel outBinFile
else makeSh (racket ++ " ") outShRel appDirRel outRktFile
coreLift $ chmodRaw outShRel 0o755
pure (Just outShRel)
else pure Nothing
executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()
executeExpr c execDir tm
= do let tmp = execDir ++ dirSep ++ "_tmpracket"
let outn = tmp ++ ".rkt"
compileToRKT c tm outn
racket <- coreLift findRacket
coreLift $ system (racket ++ " " ++ outn)
= do Just sh <- compileExpr False c execDir tm "_tmpracket"
| Nothing => throw (InternalError "compileExpr returned Nothing")
coreLift $ system sh
pure ()
export
codegenRacket : Codegen
codegenRacket = MkCG compileExpr executeExpr
codegenRacket = MkCG (compileExpr True) executeExpr

2
src/Core/Binary.idr
View File

@ -28,7 +28,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 28
ttcVersion = 29
export
checkTTCVersion : String -> Int -> Int -> Core ()

198
src/Core/CaseBuilder.idr
View File

@ -188,22 +188,22 @@ take (x :: xs) (p :: ps) = p :: take xs ps
data PatClause : (vars : List Name) -> (todo : List Name) -> Type where
MkPatClause : List Name -> -- names matched so far (from original lhs)
NamedPats vars todo ->
(rhs : Term vars) -> PatClause vars todo
Int -> (rhs : Term vars) -> PatClause vars todo
getNPs : PatClause vars todo -> NamedPats vars todo
getNPs (MkPatClause _ lhs rhs) = lhs
getNPs (MkPatClause _ lhs pid rhs) = lhs
{vars : _} -> {todo : _} -> Show (PatClause vars todo) where
show (MkPatClause _ ps rhs)
show (MkPatClause _ ps pid rhs)
= show ps ++ " => " ++ show rhs
substInClause : {a, vars, todo : _} ->
{auto c : Ref Ctxt Defs} ->
FC -> PatClause vars (a :: todo) ->
Core (PatClause vars (a :: todo))
substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs)
substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs)
= do pats' <- substInPats fc a (mkTerm vars pat) pats
pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') rhs)
pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') pid rhs)
data Partitions : List (PatClause vars todo) -> Type where
ConClauses : {todo, vars, ps : _} ->
@ -244,7 +244,7 @@ clauseType : Phase -> PatClause vars (a :: as) -> ClauseType
-- and don't see later, treat it as a variable
-- Or, if we're compiling for runtime we won't be able to split on it, so
-- also treat it as a variable
clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) rhs)
clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) pid rhs)
= getClauseType phase arg ty
where
-- used to get the remaining clause types
@ -324,25 +324,25 @@ data Group : List Name -> -- variables in scope
data GroupMatch : ConType -> List Pat -> Group vars todo -> Type where
ConMatch : LengthMatch ps newargs ->
GroupMatch (CName n tag) ps
(ConGroup {newargs} n tag (MkPatClause pvs pats rhs :: rest))
(ConGroup {newargs} n tag (MkPatClause pvs pats pid rhs :: rest))
DelayMatch : GroupMatch CDelay []
(DelayGroup {tyarg} {valarg} (MkPatClause pvs pats rhs :: rest))
(DelayGroup {tyarg} {valarg} (MkPatClause pvs pats pid rhs :: rest))
ConstMatch : GroupMatch (CConst c) []
(ConstGroup c (MkPatClause pvs pats rhs :: rest))
(ConstGroup c (MkPatClause pvs pats pid rhs :: rest))
NoMatch : GroupMatch ct ps g
checkGroupMatch : (c : ConType) -> (ps : List Pat) -> (g : Group vars todo) ->
GroupMatch c ps g
checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats rhs :: rest))
checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats pid rhs :: rest))
= case checkLengthMatch ps newargs of
Nothing => NoMatch
Just prf => case (nameEq x x', decEq tag tag') of
(Just Refl, Yes Refl) => ConMatch prf
_ => NoMatch
checkGroupMatch (CName x tag) ps _ = NoMatch
checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats rhs :: rest))
checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats pid rhs :: rest))
= DelayMatch
checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats rhs :: rest))
checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats pid rhs :: rest))
= case constantEq c c' of
Nothing => NoMatch
Just Refl => ConstMatch
@ -434,14 +434,14 @@ groupCons fc fn pvars cs
addConG : {vars', todo' : _} ->
Name -> (tag : Int) ->
List Pat -> NamedPats vars' todo' ->
(rhs : Term vars') ->
Int -> (rhs : Term vars') ->
(acc : List (Group vars' todo')) ->
Core (List (Group vars' todo'))
-- Group all the clauses that begin with the same constructor, and
-- add new pattern arguments for each of that constructor's arguments.
-- The type of 'ConGroup' ensures that we refer to the arguments by
-- the same name in each of the clauses
addConG {vars'} {todo'} n tag pargs pats rhs []
addConG {vars'} {todo'} n tag pargs pats pid rhs []
= do cty <- the (Core (NF vars')) $ if n == UN "->"
then pure $ NBind fc (MN "_" 0) (Pi top Explicit (NType fc)) $
(\d, a => pure $ NBind fc (MN "_" 1) (Pi top Explicit (NErased fc False))
@ -458,11 +458,11 @@ groupCons fc fn pvars cs
let clause = MkPatClause {todo = patnames ++ todo'}
pvars
(newargs ++ pats')
(weakenNs patnames rhs)
pid (weakenNs patnames rhs)
pure [ConGroup n tag [clause]]
addConG {vars'} {todo'} n tag pargs pats rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g)
addConG {vars'} {todo'} n tag pargs pats rhs
((ConGroup {newargs} n tag ((MkPatClause pvars ps tm) :: rest)) :: gs)
addConG {vars'} {todo'} n tag pargs pats pid rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g)
addConG {vars'} {todo'} n tag pargs pats pid rhs
((ConGroup {newargs} n tag ((MkPatClause pvars ps tid tm) :: rest)) :: gs)
| (ConMatch {newargs} lprf)
= do let newps = newPats pargs lprf ps
let pats' = updatePatNames (updateNames (zip newargs pargs))
@ -470,13 +470,14 @@ groupCons fc fn pvars cs
let newclause : PatClause (newargs ++ vars') (newargs ++ todo')
= MkPatClause pvars
(newps ++ pats')
pid
(weakenNs newargs rhs)
-- put the new clause at the end of the group, since we
-- match the clauses top to bottom.
pure ((ConGroup n tag (MkPatClause pvars ps tm :: rest ++ [newclause]))
pure ((ConGroup n tag (MkPatClause pvars ps tid tm :: rest ++ [newclause]))
:: gs)
addConG n tag pargs pats rhs (g :: gs) | NoMatch
= do gs' <- addConG n tag pargs pats rhs gs
addConG n tag pargs pats pid rhs (g :: gs) | NoMatch
= do gs' <- addConG n tag pargs pats pid rhs gs
pure (g :: gs')
-- This rather ugly special case is to deal with laziness, where Delay
@ -485,10 +486,10 @@ groupCons fc fn pvars cs
-- and compiler)
addDelayG : {vars', todo' : _} ->
Pat -> Pat -> NamedPats vars' todo' ->
(rhs : Term vars') ->
Int -> (rhs : Term vars') ->
(acc : List (Group vars' todo')) ->
Core (List (Group vars' todo'))
addDelayG {vars'} {todo'} pty parg pats rhs []
addDelayG {vars'} {todo'} pty parg pats pid rhs []
= do let dty = NBind fc (MN "a" 0) (Pi erased Explicit (NType fc)) $
(\d, a =>
do a' <- evalClosure d a
@ -502,11 +503,11 @@ groupCons fc fn pvars cs
(weakenNs [tyname, argname] pats)
let clause = MkPatClause {todo = tyname :: argname :: todo'}
pvars (newargs ++ pats')
(weakenNs [tyname, argname] rhs)
pid (weakenNs [tyname, argname] rhs)
pure [DelayGroup [clause]]
addDelayG {vars'} {todo'} pty parg pats rhs (g :: gs) with (checkGroupMatch CDelay [] g)
addDelayG {vars'} {todo'} pty parg pats rhs
((DelayGroup {tyarg} {valarg} ((MkPatClause pvars ps tm) :: rest)) :: gs)
addDelayG {vars'} {todo'} pty parg pats pid rhs (g :: gs) with (checkGroupMatch CDelay [] g)
addDelayG {vars'} {todo'} pty parg pats pid rhs
((DelayGroup {tyarg} {valarg} ((MkPatClause pvars ps tid tm) :: rest)) :: gs)
| (DelayMatch {tyarg} {valarg})
= do let newps = newPats [pty, parg] (ConsMatch (ConsMatch NilMatch)) ps
let pats' = updatePatNames (updateNames [(tyarg, pty),
@ -514,56 +515,56 @@ groupCons fc fn pvars cs
(weakenNs [tyarg, valarg] pats)
let newclause : PatClause (tyarg :: valarg :: vars')
(tyarg :: valarg :: todo')
= MkPatClause pvars (newps ++ pats')
= MkPatClause pvars (newps ++ pats') pid
(weakenNs [tyarg, valarg] rhs)
pure ((DelayGroup (MkPatClause pvars ps tm :: rest ++ [newclause]))
pure ((DelayGroup (MkPatClause pvars ps tid tm :: rest ++ [newclause]))
:: gs)
addDelayG pty parg pats rhs (g :: gs) | NoMatch
= do gs' <- addDelayG pty parg pats rhs gs
addDelayG pty parg pats pid rhs (g :: gs) | NoMatch
= do gs' <- addDelayG pty parg pats pid rhs gs
pure (g :: gs')
addConstG : {vars', todo' : _} ->
Constant -> NamedPats vars' todo' ->
(rhs : Term vars') ->
Int -> (rhs : Term vars') ->
(acc : List (Group vars' todo')) ->
Core (List (Group vars' todo'))
addConstG c pats rhs []
= pure [ConstGroup c [MkPatClause pvars pats rhs]]
addConstG {todo'} {vars'} c pats rhs (g :: gs) with (checkGroupMatch (CConst c) [] g)
addConstG {todo'} {vars'} c pats rhs
((ConstGroup c ((MkPatClause pvars ps tm) :: rest)) :: gs) | ConstMatch
addConstG c pats pid rhs []
= pure [ConstGroup c [MkPatClause pvars pats pid rhs]]
addConstG {todo'} {vars'} c pats pid rhs (g :: gs) with (checkGroupMatch (CConst c) [] g)
addConstG {todo'} {vars'} c pats pid rhs
((ConstGroup c ((MkPatClause pvars ps tid tm) :: rest)) :: gs) | ConstMatch
= let newclause : PatClause vars' todo'
= MkPatClause pvars pats rhs in
= MkPatClause pvars pats pid rhs in
pure ((ConstGroup c
(MkPatClause pvars ps tm :: rest ++ [newclause])) :: gs)
addConstG c pats rhs (g :: gs) | NoMatch
= do gs' <- addConstG c pats rhs gs
(MkPatClause pvars ps tid tm :: rest ++ [newclause])) :: gs)
addConstG c pats pid rhs (g :: gs) | NoMatch
= do gs' <- addConstG c pats pid rhs gs
pure (g :: gs')
addGroup : {vars, todo, idx : _} ->
Pat -> (0 p : IsVar name idx vars) ->
NamedPats vars todo -> Term vars ->
NamedPats vars todo -> Int -> Term vars ->
List (Group vars todo) ->
Core (List (Group vars todo))
-- In 'As' replace the name on the RHS with a reference to the
-- variable we're doing the case split on
addGroup (PAs fc n p) pprf pats rhs acc
= addGroup p pprf pats (substName n (Local fc (Just True) _ pprf) rhs) acc
addGroup (PCon cfc n t a pargs) pprf pats rhs acc
addGroup (PAs fc n p) pprf pats pid rhs acc
= addGroup p pprf pats pid (substName n (Local fc (Just True) _ pprf) rhs) acc
addGroup (PCon cfc n t a pargs) pprf pats pid rhs acc
= if a == length pargs
then addConG n t pargs pats rhs acc
then addConG n t pargs pats pid rhs acc
else throw (CaseCompile cfc fn (NotFullyApplied n))
addGroup (PTyCon _ n a pargs) pprf pats rhs acc
= addConG n 0 pargs pats rhs acc
addGroup (PArrow _ _ s t) pprf pats rhs acc
= addConG (UN "->") 0 [s, t] pats rhs acc
addGroup (PTyCon _ n a pargs) pprf pats pid rhs acc
= addConG n 0 pargs pats pid rhs acc
addGroup (PArrow _ _ s t) pprf pats pid rhs acc
= addConG (UN "->") 0 [s, t] pats pid rhs acc
-- Go inside the delay; we'll flag the case as needing to force its
-- scrutinee (need to check in 'caseGroups below)
addGroup (PDelay _ _ pty parg) pprf pats rhs acc
= addDelayG pty parg pats rhs acc
addGroup (PConst _ c) pprf pats rhs acc
= addConstG c pats rhs acc
addGroup _ pprf pats rhs acc = pure acc -- Can't happen, not a constructor
addGroup (PDelay _ _ pty parg) pprf pats pid rhs acc
= addDelayG pty parg pats pid rhs acc
addGroup (PConst _ c) pprf pats pid rhs acc
= addConstG c pats pid rhs acc
addGroup _ pprf pats pid rhs acc = pure acc -- Can't happen, not a constructor
-- -- FIXME: Is this possible to rule out with a type? Probably.
gc : {a, vars, todo : _} ->
@ -571,8 +572,8 @@ groupCons fc fn pvars cs
List (PatClause vars (a :: todo)) ->
Core (List (Group vars todo))
gc acc [] = pure acc
gc {a} acc ((MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs) :: cs)
= do acc' <- addGroup pat pprf pats rhs acc
gc {a} acc ((MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs) :: cs)
= do acc' <- addGroup pat pprf pats pid rhs acc
gc acc' cs
getFirstPat : NamedPats ns (p :: ps) -> Pat
@ -614,13 +615,10 @@ sameType {ns} fc phase fn env (p :: xs)
sameTypeAs : Phase -> NF ns -> List (ArgType ns) -> Core ()
sameTypeAs _ ty [] = pure ()
sameTypeAs ph ty (Known r t :: xs) =
if ph == RunTime && isErased r
-- Can't match on erased thing
then throw (CaseCompile fc fn (MatchErased (_ ** (env, mkTerm _ (firstPat p)))))
else do defs <- get Ctxt
if headEq ty !(nf defs env t) phase
then sameTypeAs ph ty xs
else throw (CaseCompile fc fn DifferingTypes)
do defs <- get Ctxt
if headEq ty !(nf defs env t) phase
then sameTypeAs ph ty xs
else throw (CaseCompile fc fn DifferingTypes)
sameTypeAs p ty _ = throw (CaseCompile fc fn DifferingTypes)
-- Check whether all the initial patterns are the same, or are all a variable.
@ -731,7 +729,8 @@ moveFirst el nps = getPat el nps :: dropPat el nps
shuffleVars : {idx : Nat} -> (0 el : IsVar name idx todo) -> PatClause vars todo ->
PatClause vars (name :: dropVar todo el)
shuffleVars el (MkPatClause pvars lhs rhs) = MkPatClause pvars (moveFirst el lhs) rhs
shuffleVars el (MkPatClause pvars lhs pid rhs)
= MkPatClause pvars (moveFirst el lhs) pid rhs
mutual
{- 'PatClause' contains a list of patterns still to process (that's the
@ -759,10 +758,10 @@ mutual
match {todo = []} fc fn phase [] err
= maybe (pure (Unmatched "No patterns"))
pure err
match {todo = []} fc fn phase ((MkPatClause pvars [] (Erased _ True)) :: _) err
match {todo = []} fc fn phase ((MkPatClause pvars [] pid (Erased _ True)) :: _) err
= pure Impossible
match {todo = []} fc fn phase ((MkPatClause pvars [] rhs) :: _) err
= pure $ STerm rhs
match {todo = []} fc fn phase ((MkPatClause pvars [] pid rhs) :: _) err
= pure $ STerm pid rhs
caseGroups : {pvar, vars, todo : _} ->
{auto i : Ref PName Int} ->
@ -804,7 +803,7 @@ mutual
-- the same variable (pprf) for the first argument. If not, the result
-- will be a broken case tree... so we should find a way to express this
-- in the type if we can.
conRule {a} fc fn phase cs@(MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs :: rest) err
conRule {a} fc fn phase cs@(MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs :: rest) err
= do refinedcs <- traverse (substInClause fc) cs
groups <- groupCons fc fn pvars refinedcs
ty <- case fty of
@ -825,21 +824,21 @@ mutual
where
updateVar : PatClause vars (a :: todo) -> Core (PatClause vars todo)
-- replace the name with the relevant variable on the rhs
updateVar (MkPatClause pvars (MkInfo (PLoc pfc n) prf fty :: pats) rhs)
updateVar (MkPatClause pvars (MkInfo (PLoc pfc n) prf fty :: pats) pid rhs)
= pure $ MkPatClause (n :: pvars)
!(substInPats fc a (Local pfc (Just False) _ prf) pats)
(substName n (Local pfc (Just False) _ prf) rhs)
pid (substName n (Local pfc (Just False) _ prf) rhs)
-- If it's an as pattern, replace the name with the relevant variable on
-- the rhs then continue with the inner pattern
updateVar (MkPatClause pvars (MkInfo (PAs pfc n pat) prf fty :: pats) rhs)
updateVar (MkPatClause pvars (MkInfo (PAs pfc n pat) prf fty :: pats) pid rhs)
= do pats' <- substInPats fc a (mkTerm _ pat) pats
let rhs' = substName n (Local pfc (Just True) _ prf) rhs
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats') rhs')
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats') pid rhs')
-- match anything, name won't appear in rhs but need to update
-- LHS pattern types based on what we've learned
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats) rhs)
updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats) pid rhs)
= pure $ MkPatClause pvars
!(substInPats fc a (mkTerm vars pat) pats) rhs
!(substInPats fc a (mkTerm vars pat) pats) pid rhs
mixture : {a, vars, todo : _} ->
{auto i : Ref PName Int} ->
@ -860,17 +859,18 @@ mutual
mkPatClause : {auto c : Ref Ctxt Defs} ->
FC -> Name ->
(args : List Name) -> ClosedTerm -> (List Pat, ClosedTerm) ->
(args : List Name) -> ClosedTerm ->
Int -> (List Pat, ClosedTerm) ->
Core (PatClause args args)
mkPatClause fc fn args ty (ps, rhs)
mkPatClause fc fn args ty pid (ps, rhs)
= maybe (throw (CaseCompile fc fn DifferingArgNumbers))
(\eq =>
do defs <- get Ctxt
nty <- nf defs [] ty
ns <- mkNames args ps eq (Just nty)
pure (MkPatClause [] ns
(rewrite sym (appendNilRightNeutral args) in
(weakenNs args rhs))))
pure (MkPatClause [] ns pid
(rewrite sym (appendNilRightNeutral args) in
(weakenNs args rhs))))
(checkLengthMatch args ps)
where
mkNames : (vars : List Name) -> (ps : List Pat) ->
@ -906,7 +906,7 @@ patCompile fc fn phase ty [] def
def
patCompile fc fn phase ty (p :: ps) def
= do let ns = getNames 0 (fst p)
pats <- traverse (mkPatClause fc fn ns ty) (p :: ps)
pats <- mkPatClausesFrom 0 ns (p :: ps)
log 5 $ "Pattern clauses " ++ show pats
i <- newRef PName (the Int 0)
cases <- match fc fn phase pats
@ -914,6 +914,15 @@ patCompile fc fn phase ty (p :: ps) def
map (TT.weakenNs ns) def)
pure (_ ** cases)
where
mkPatClausesFrom : Int -> (args : List Name) ->
List (List Pat, ClosedTerm) ->
Core (List (PatClause args args))
mkPatClausesFrom i ns [] = pure []
mkPatClausesFrom i ns (p :: ps)
= do p' <- mkPatClause fc fn ns ty i p
ps' <- mkPatClausesFrom (i + 1) ns ps
pure (p' :: ps')
getNames : Int -> List Pat -> List Name
getNames i [] = []
getNames i (x :: xs) = MN "arg" i :: getNames (i + 1) xs
@ -950,16 +959,28 @@ simpleCase fc phase fn ty def clauses
defs <- get Ctxt
patCompile fc fn phase ty ps def
findReached : CaseTree ns -> List Int
findReached (Case _ _ _ alts) = concatMap findRAlts alts
where
findRAlts : CaseAlt ns' -> List Int
findRAlts (ConCase _ _ _ t) = findReached t
findRAlts (DelayCase _ _ t) = findReached t
findRAlts (ConstCase _ t) = findReached t
findRAlts (DefaultCase t) = findReached t
findReached (STerm i _) = [i]
findReached _ = []
-- Returns the case tree, and a list of the clauses that aren't reachable
export
getPMDef : {auto c : Ref Ctxt Defs} ->
FC -> Phase -> Name -> ClosedTerm -> List Clause ->
Core (args ** CaseTree args)
Core (args ** (CaseTree args, List Clause))
-- If there's no clauses, make a definition with the right number of arguments
-- for the type, which we can use in coverage checking to ensure that one of
-- the arguments has an empty type
getPMDef fc phase fn ty []
= do defs <- get Ctxt
pure (!(getArgs 0 !(nf defs [] ty)) ** Unmatched "No clauses")
pure (!(getArgs 0 !(nf defs [] ty)) ** (Unmatched "No clauses", []))
where
getArgs : Int -> NF [] -> Core (List Name)
getArgs i (NBind fc x (Pi _ _ _) sc)
@ -970,8 +991,17 @@ getPMDef fc phase fn ty []
getPMDef fc phase fn ty clauses
= do defs <- get Ctxt
let cs = map (toClosed defs) (labelPat 0 clauses)
simpleCase fc phase fn ty Nothing cs
(_ ** t) <- simpleCase fc phase fn ty Nothing cs
let reached = findReached t
pure (_ ** (t, getUnreachable 0 reached clauses))
where
getUnreachable : Int -> List Int -> List Clause -> List Clause
getUnreachable i is [] = []
getUnreachable i is (c :: cs)
= if i `elem` is
then getUnreachable (i + 1) is cs
else c :: getUnreachable (i + 1) is cs
labelPat : Int -> List a -> List (String, a)
labelPat i [] = []
labelPat i (x :: xs) = ("pat" ++ show i ++ ":", x) :: labelPat (i + 1) xs

14
src/Core/CaseTree.idr
View File

@ -20,7 +20,9 @@ mutual
(scTy : Term vars) -> List (CaseAlt vars) ->
CaseTree vars
||| RHS: no need for further inspection
STerm : Term vars -> CaseTree vars
||| The Int is a clause id that allows us to see which of the
||| initial clauses are reached in the tree
STerm : Int -> Term vars -> CaseTree vars
||| error from a partial match
Unmatched : (msg : String) -> CaseTree vars
||| Absurd context
@ -60,7 +62,7 @@ mutual
show (Case {name} idx prf ty alts)
= "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of { " ++
showSep " | " (assert_total (map show alts)) ++ " }"
show (STerm tm) = show tm
show (STerm i tm) = "[" ++ show i ++ "] " ++ show tm
show (Unmatched msg) = "Error: " ++ show msg
show Impossible = "Impossible"
@ -83,7 +85,7 @@ mutual
= i == i
&& length alts == length alts
&& allTrue (zipWith eqAlt alts alts')
eqTree (STerm t) (STerm t') = eqTerm t t'
eqTree (STerm _ t) (STerm _ t') = eqTerm t t'
eqTree (Unmatched _) (Unmatched _) = True
eqTree Impossible Impossible = True
eqTree _ _ = False
@ -118,7 +120,7 @@ mutual
= let MkNVar prf' = insertNVarNames {outer} {inner} {ns} _ prf in
Case _ prf' (insertNames {outer} ns scTy)
(map (insertCaseAltNames {outer} {inner} ns) alts)
insertCaseNames {outer} ns (STerm x) = STerm (insertNames {outer} ns x)
insertCaseNames {outer} ns (STerm i x) = STerm i (insertNames {outer} ns x)
insertCaseNames ns (Unmatched msg) = Unmatched msg
insertCaseNames ns Impossible = Impossible
@ -146,7 +148,7 @@ thinTree : {outer, inner : _} ->
thinTree n (Case idx prf scTy alts)
= let MkNVar prf' = insertNVar {n} _ prf in
Case _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts)
thinTree n (STerm tm) = STerm (thin n tm)
thinTree n (STerm i tm) = STerm i (thin n tm)
thinTree n (Unmatched msg) = Unmatched msg
thinTree n Impossible = Impossible
@ -172,7 +174,7 @@ getNames add ns sc = getSet ns sc
getSet : NameMap Bool -> CaseTree vs -> NameMap Bool
getSet ns (Case _ x ty xs) = getAltSets ns xs
getSet ns (STerm tm) = add ns tm
getSet ns (STerm i tm) = add ns tm
getSet ns (Unmatched msg) = ns
getSet ns Impossible = ns

36
src/Core/Context.idr
View File

@ -170,6 +170,9 @@ data DefFlag
-- should evaluate the RHS, with reduction limits on the given names,
-- and ensure the name has made progress in doing so (i.e. has reduced
-- at least once)
| AllGuarded -- safe to treat as a constructor for the purposes of
-- productivity checking. All clauses are guarded by constructors,
-- and there are no other function applications
export
Eq DefFlag where
@ -181,6 +184,7 @@ Eq DefFlag where
(==) BlockedHint BlockedHint = True
(==) Macro Macro = True
(==) (PartialEval x) (PartialEval y) = x == y
(==) AllGuarded AllGuarded = True
(==) _ _ = False
export
@ -193,6 +197,7 @@ Show DefFlag where
show BlockedHint = "blockedhint"
show Macro = "macro"
show (PartialEval _) = "partialeval"
show AllGuarded = "allguarded"
public export
data SizeChange = Smaller | Same | Unknown
@ -612,14 +617,14 @@ mutual
HasNames (CaseTree vars) where
full gam (Case i v ty alts)
= pure $ Case i v !(full gam ty) !(traverse (full gam) alts)
full gam (STerm tm)
= pure $ STerm !(full gam tm)
full gam (STerm i tm)
= pure $ STerm i !(full gam tm)
full gam t = pure t
resolved gam (Case i v ty alts)
= pure $ Case i v !(resolved gam ty) !(traverse (resolved gam) alts)
resolved gam (STerm tm)
= pure $ STerm !(resolved gam tm)
resolved gam (STerm i tm)
= pure $ STerm i !(resolved gam tm)
resolved gam t = pure t
export
@ -854,6 +859,8 @@ record Defs where
-- again
timings : StringMap (Bool, Integer)
-- ^ record of timings from logTimeRecord
warnings : List Warning
-- ^ as yet unreported warnings
-- Label for context references
export
@ -871,7 +878,7 @@ initDefs
= do gam <- initCtxt
pure (MkDefs gam [] ["Main"] [] defaults empty 100
empty empty empty [] [] empty []
empty 5381 [] [] [] [] [] empty empty empty empty)
empty 5381 [] [] [] [] [] empty empty empty empty [])
-- Reset the context, except for the options
export
@ -885,6 +892,9 @@ clearCtxt
resetElab : Options -> Options
resetElab = record { elabDirectives = defaultElab }
-- Beware: if your hashable thing contains (potentially resolved) names,
-- it'll be better to use addHashWithNames to make the hash independent
-- of the internal numbering of names.
export
addHash : {auto c : Ref Ctxt Defs} ->
Hashable a => a -> Core ()
@ -1181,6 +1191,15 @@ prettyName (WithBlock outer idx)
prettyName (NS ns n) = prettyName n
prettyName n = pure (show n)
-- Add a hash of a thing that contains names,
-- but convert the internal numbers to full names first.
-- This makes the hash not depend on the internal numbering,
-- which is unstable.
export
addHashWithNames : {auto c : Ref Ctxt Defs} ->
Hashable a => HasNames a => a -> Core ()
addHashWithNames x = toFullNames x >>= addHash
export
setFlag : {auto c : Ref Ctxt Defs} ->
FC -> Name -> DefFlag -> Core ()
@ -2161,6 +2180,13 @@ setSession sopts
= do defs <- get Ctxt
put Ctxt (record { options->session = sopts } defs)
export
recordWarning : {auto c : Ref Ctxt Defs} ->
Warning -> Core ()
recordWarning w
= do defs <- get Ctxt
put Ctxt (record { warnings $= (w ::) } defs)
-- Log message with a term, translating back to human readable names first
export
logTerm : {vars : _} ->

12
src/Core/Core.idr
View File

@ -119,7 +119,8 @@ data Error : Type where
GenericMsg : FC -> String -> Error
TTCError : TTCErrorMsg -> Error
FileErr : String -> FileError -> Error
ParseFail : FC -> ParseError -> Error
ParseFail : Show token =>
FC -> ParseError token -> Error
ModuleNotFound : FC -> List String -> Error
CyclicImports : List (List String) -> Error
ForceNeeded : Error
@ -130,6 +131,11 @@ data Error : Type where
InLHS : FC -> Name -> Error -> Error
InRHS : FC -> Name -> Error -> Error
public export
data Warning : Type where
UnreachableClause : {vars : _} ->
FC -> Env Term vars -> Term vars -> Warning
export
Show TTCErrorMsg where
show (Format file ver exp) =
@ -361,6 +367,10 @@ getErrorLoc (InCon _ _ err) = getErrorLoc err
getErrorLoc (InLHS _ _ err) = getErrorLoc err
getErrorLoc (InRHS _ _ err) = getErrorLoc err
export
getWarningLoc : Warning -> Maybe FC
getWarningLoc (UnreachableClause fc _ _) = Just fc
-- Core is a wrapper around IO that is specialised for efficiency.
export
record Core t where

123
src/Core/Coverage.idr
View File

@ -7,59 +7,132 @@ import Core.Normalise
import Core.TT
import Core.Value
import Data.Bool.Extra
import Data.List
import Data.NameMap
%default covering
-- Return whether any of the name matches conflict
conflictMatch : {vars : _} -> List (Name, Term vars) -> Bool
conflictMatch [] = False
conflictMatch ((x, tm) :: ms)
= if conflictArgs x tm ms
then True
else conflictMatch ms
where
clash : Term vars -> Term vars -> Bool
clash (Ref _ (DataCon t _) _) (Ref _ (DataCon t' _) _)
= t /= t'
clash _ _ = False
findN : Nat -> Term vars -> Bool
findN i (Local _ _ i' _) = i == i'
findN i tm
= let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
| _ => False in
anyTrue (map (findN i) args)
-- Assuming in normal form. Look for: mismatched constructors, or
-- a name appearing strong rigid in the other term
conflictTm : Term vars -> Term vars -> Bool
conflictTm (Local _ _ i _) tm
= let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
| _ => False in
anyTrue (map (findN i) args)
conflictTm tm (Local _ _ i _)
= let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
| _ => False in
anyTrue (map (findN i) args)
conflictTm tm tm'
= let (f, args) = getFnArgs tm
(f', args') = getFnArgs tm' in
if clash f f'
then True
else anyTrue (zipWith conflictTm args args')
conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool
conflictArgs n tm [] = False
conflictArgs n tm ((x, tm') :: ms)
= if n == x && conflictTm tm tm'
then True
else conflictArgs n tm ms
-- Return whether any part of the type conflicts in such a way that they
-- can't possibly be equal (i.e. mismatched constructor)
conflict : {vars : _} ->
Defs -> NF vars -> Name -> Core Bool
conflict defs nfty n
{auto c : Ref Ctxt Defs} ->
Defs -> Env Term vars -> NF vars -> Name -> Core Bool
conflict defs env nfty n
= do Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure False
case (definition gdef, type gdef) of
(DCon t arity _, dty)
=> conflictNF nfty !(nf defs [] dty)
=> do Nothing <- conflictNF 0 nfty !(nf defs [] dty)
| Just ms => pure $ conflictMatch ms
pure True
_ => pure False
where
mutual
conflictArgs : List (Closure vars) -> List (Closure []) -> Core Bool
conflictArgs [] [] = pure False
conflictArgs (c :: cs) (c' :: cs')
conflictArgs : Int -> List (Closure vars) -> List (Closure []) ->
Core (Maybe (List (Name, Term vars)))
conflictArgs _ [] [] = pure (Just [])
conflictArgs i (c :: cs) (c' :: cs')
= do cnf <- evalClosure defs c
cnf' <- evalClosure defs c'
pure $ !(conflictNF cnf cnf') || !(conflictArgs cs cs')
conflictArgs _ _ = pure False
Just ms <- conflictNF i cnf cnf'
| Nothing => pure Nothing
Just ms' <- conflictArgs i cs cs'
| Nothing => pure Nothing
pure (Just (ms ++ ms'))
conflictArgs _ _ _ = pure (Just [])
conflictNF : NF vars -> NF [] -> Core Bool
conflictNF t (NBind fc x b sc)
= conflictNF t !(sc defs (toClosure defaultOpts [] (Erased fc False)))
conflictNF (NDCon _ n t a args) (NDCon _ n' t' a' args')
-- If the constructor type (the NF []) matches the variable type,
-- then there may be a way to construct it, so return the matches in
-- the indices.
-- If any of those matches clash, the constructor is not valid
-- e.g, Eq x x matches Eq Z (S Z), with x = Z and x = S Z
-- conflictNF returns the list of matches, for checking
conflictNF : Int -> NF vars -> NF [] ->
Core (Maybe (List (Name, Term vars)))
conflictNF i t (NBind fc x b sc)
-- invent a fresh name, in case a user has bound the same name
-- twice somehow both references appear in the result it's unlikely
-- put posslbe
= let x' = MN (show x) i in
conflictNF (i + 1) t
!(sc defs (toClosure defaultOpts [] (Ref fc Bound x')))
conflictNF i nf (NApp _ (NRef Bound n) [])
= do empty <- clearDefs defs
pure (Just [(n, !(quote empty env nf))])
conflictNF i (NDCon _ n t a args) (NDCon _ n' t' a' args')
= if t == t'
then conflictArgs args args'
else pure True
conflictNF (NTCon _ n t a args) (NTCon _ n' t' a' args')
then conflictArgs i args args'
else pure Nothing
conflictNF i (NTCon _ n t a args) (NTCon _ n' t' a' args')
= if n == n'
then conflictArgs args args'
else pure True
conflictNF (NPrimVal _ c) (NPrimVal _ c') = pure (c /= c')
conflictNF _ _ = pure False
then conflictArgs i args args'
else pure Nothing
conflictNF i (NPrimVal _ c) (NPrimVal _ c')
= if c == c'
then pure (Just [])
else pure Nothing
conflictNF _ _ _ = pure (Just [])
-- Return whether the given type is definitely empty (due to there being
-- no constructors which can possibly match it.)
export
isEmpty : {vars : _} ->
Defs -> NF vars -> Core Bool
isEmpty defs (NTCon fc n t a args)
{auto c : Ref Ctxt Defs} ->
Defs -> Env Term vars -> NF vars -> Core Bool
isEmpty defs env (NTCon fc n t a args)
= case !(lookupDefExact n (gamma defs)) of
Just (TCon _ _ _ _ flags _ cons _)
=> if not (external flags)
then allM (conflict defs (NTCon fc n t a args)) cons
then allM (conflict defs env (NTCon fc n t a args)) cons
else pure False
_ => pure False
isEmpty defs _ = pure False
isEmpty defs env _ = pure False
-- Need this to get a NF from a Term; the names are free in any case
freeEnv : FC -> (vs : List Name) -> Env Term vs
@ -95,7 +168,7 @@ emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts)
emptyRHSalt (DelayCase c arg sc) = DelayCase c arg (emptyRHS fc sc)
emptyRHSalt (ConstCase c sc) = ConstCase c (emptyRHS fc sc)
emptyRHSalt (DefaultCase sc) = DefaultCase (emptyRHS fc sc)
emptyRHS fc (STerm s) = STerm (Erased fc False)
emptyRHS fc (STerm i s) = STerm i (Erased fc False)
emptyRHS fc sc = sc
mkAlt : {vars : _} ->
@ -284,7 +357,7 @@ buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn)
buildArgsAlt not' (c :: cs)
= pure $ !(buildArgAlt not' c) ++ !(buildArgsAlt not' cs)
buildArgs fc defs known not ps (STerm vs)
buildArgs fc defs known not ps (STerm _ vs)
= pure [] -- matched, so return nothing
buildArgs fc defs known not ps (Unmatched msg)
= pure [ps] -- unmatched, so return it

13
src/Core/Directory.idr
View File

@ -13,7 +13,7 @@ import System.Directory
import System.File
import System.Info
%default total
%default covering
fullPath : String -> List String
fullPath fp = filter (/="") $ split (==sep) fp
@ -200,10 +200,10 @@ getEntries d
dirEntries : String -> IO (Either FileError (List String))
dirEntries dir
= do Right d <- dirOpen dir
= do Right d <- openDir dir
| Left err => pure (Left err)
ds <- getEntries d
dirClose d
closeDir d
pure (Right ds)
findIpkg : List String -> Maybe String
@ -215,10 +215,13 @@ findIpkg (f :: fs)
allDirs : String -> List String -> List (String, List String)
allDirs path [] = []
allDirs path ("" :: ds) = ("/", ds) :: allDirs path ds
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
(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

1
src/Core/GetType.idr
View File

@ -59,6 +59,7 @@ mutual
NDelayed fc _ fty =>
do defs <- get Ctxt
pure $ glueBack defs env fty
_ => throw (GenericMsg fc "Not a delayed type")
chk env (PrimVal fc x) = pure $ gnf env (chkConstant fc x)
chk env (TType fc) = pure (gType fc)
chk env (Erased fc _) = pure (gErased fc)

2
src/Core/Hash.idr
View File

@ -152,7 +152,7 @@ mutual
Hashable (CaseTree vars) where
hashWithSalt h (Case idx x scTy xs)
= h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs
hashWithSalt h (STerm x)
hashWithSalt h (STerm _ x)
= h `hashWithSalt` 1 `hashWithSalt` x
hashWithSalt h (Unmatched msg)
= h `hashWithSalt` 2

7
src/Core/LinearCheck.idr
View File

@ -222,8 +222,9 @@ mutual
rig
logC 10 $ do
def <- the (Core String) $ case definition gdef of
PMDef _ _ (STerm tm) _ _ => do tm' <- toFullNames tm
pure (show tm')
PMDef _ _ (STerm _ tm) _ _ =>
do tm' <- toFullNames tm
pure (show tm')
_ => pure ""
pure (show rig ++ ": " ++ show n ++ " " ++ show fc ++ "\n"
++ show def)
@ -614,7 +615,7 @@ mutual
RigCount -> (erase : Bool) -> Env Term vars ->
Name -> Int -> Def -> List (Term vars) ->
Core (Term vars, Glued vars, Usage vars)
expandMeta rig erase env n idx (PMDef _ [] (STerm fn) _ _) args
expandMeta rig erase env n idx (PMDef _ [] (STerm _ fn) _ _) args
= do tm <- substMeta (embed fn) args []
lcheck rig erase env tm
where

10
src/Core/Normalise.idr
View File

@ -107,7 +107,7 @@ parameters (defs : Defs, topopts : EvalOpts)
eval env locs (Bind fc x (Lam r _ ty) scope) (thunk :: stk)
= eval env (thunk :: locs) scope stk
eval env locs (Bind fc x b@(Let r val ty) scope) stk
= if holesOnly topopts || argHolesOnly topopts
= if holesOnly topopts || argHolesOnly topopts && not (tcInline topopts)
then do b' <- traverse (\tm => eval env locs tm []) b
pure $ NBind fc x b'
(\defs', arg => evalWithOpts defs' topopts
@ -326,7 +326,7 @@ parameters (defs : Defs, topopts : EvalOpts)
= do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
let loc' = updateLocal idx (varExtend x) loc xval
findAlt env loc' opts fc stk xval alts def
evalTree env loc opts fc stk (STerm tm) def
evalTree env loc opts fc stk (STerm _ tm) def
= case fuel opts of
Nothing => evalWithOpts defs opts env loc (embed tm) stk
Just Z => def
@ -595,8 +595,10 @@ mutual
pure (TDelay fc r tyQ argQ)
where
toHolesOnly : Closure vs -> Closure vs
toHolesOnly (MkClosure _ locs env tm)
= MkClosure withHoles locs env tm
toHolesOnly (MkClosure opts locs env tm)
= MkClosure (record { holesOnly = True,
argHolesOnly = True } opts)
locs env tm
toHolesOnly c = c
quoteGenNF q defs bound env (NForce fc r arg args)
= do args' <- quoteArgs q defs bound env args

2
src/Core/Options.idr
View File

@ -159,7 +159,7 @@ defaultSession = MkSessionOpts False False False Chez 0 False False
export
defaultElab : ElabDirectives
defaultElab = MkElabDirectives True True PartialOK 3 True
defaultElab = MkElabDirectives True True CoveringOnly 3 True
export
defaults : Options

6
src/Core/TTC.idr
View File

@ -343,7 +343,7 @@ mutual
{vars : _} -> TTC (CaseTree vars) where
toBuf b (Case {name} idx x scTy xs)
= do tag 0; toBuf b name; toBuf b idx; toBuf b xs
toBuf b (STerm x)
toBuf b (STerm _ x)
= do tag 1; toBuf b x
toBuf b (Unmatched msg)
= do tag 2; toBuf b msg
@ -355,7 +355,7 @@ mutual
xs <- fromBuf b
pure (Case {name} idx (mkPrf idx) (Erased emptyFC False) xs)
1 => do x <- fromBuf b
pure (STerm x)
pure (STerm 0 x)
2 => do msg <- fromBuf b
pure (Unmatched msg)
3 => pure Impossible
@ -865,6 +865,7 @@ TTC DefFlag where
toBuf b BlockedHint = tag 7
toBuf b Macro = tag 8
toBuf b (PartialEval x) = tag 9 -- names not useful any more
toBuf b AllGuarded = tag 10
fromBuf b
= case !getTag of
@ -876,6 +877,7 @@ TTC DefFlag where
7 => pure BlockedHint
8 => pure Macro
9 => pure (PartialEval [])
10 => pure AllGuarded
_ => corrupt "DefFlag"
export

121
src/Core/Termination.idr
View File

@ -34,6 +34,55 @@ totRefsIn : {auto c : Ref Ctxt Defs} ->
Defs -> Term vars -> Core Terminating
totRefsIn defs ty = totRefs defs (keys (getRefs (Resolved (-1)) ty))
-- Check if all branches end up as constructor arguments, with no other
-- function application, and set 'AllGuarded' if so.
-- This is to check whether a function can be considered a constructor form
-- for the sake of termination checking (and might have other uses...)
export
checkIfGuarded : {auto c : Ref Ctxt Defs} ->
FC -> Name -> Core ()
checkIfGuarded fc n
= do defs <- get Ctxt
Just (PMDef _ _ _ _ pats) <- lookupDefExact n (gamma defs)
| _ => pure ()
t <- allGuarded pats
when t $ setFlag fc n AllGuarded
where
guardedNF : {vars : _} -> Defs -> Env Term vars -> NF vars -> Core Bool
guardedNF defs env (NDCon _ _ _ _ args) = pure True
guardedNF defs env (NApp _ (NRef _ n) args)
= do Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure False
pure (AllGuarded `elem` flags gdef)
guardedNF defs env _ = pure False
checkNotFn : Defs -> Name -> Core Bool
checkNotFn defs n
= do Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure False
case definition gdef of
DCon _ _ _ => pure True
_ => pure (multiplicity gdef == erased
|| (AllGuarded `elem` flags gdef))
guarded : {vars : _} -> Env Term vars -> Term vars -> Core Bool
guarded env tm
= do defs <- get Ctxt
empty <- clearDefs defs
tmnf <- nf empty env tm
if !(guardedNF defs env tmnf)
then do Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure False
allM (checkNotFn defs) (keys (refersTo gdef))
else pure False
allGuarded : List (vs ** (Env Term vs, Term vs, Term vs)) -> Core Bool
allGuarded [] = pure True
allGuarded ((_ ** (env, lhs, rhs)) :: ps)
= if !(guarded env rhs)
then allGuarded ps
else pure False
-- Equal for the purposes of size change means, ignoring as patterns, all
-- non-metavariable positions are equal
scEq : Term vars -> Term vars -> Bool
@ -61,6 +110,31 @@ Show Guardedness where
show Guarded = "Guarded"
show InDelay = "InDelay"
-- Remove all force and delay annotations which are nothing to do with
-- coinduction meaning that all Delays left guard coinductive calls.
delazy : Defs -> Term vars -> Term vars
delazy defs (TDelayed fc r tm)
= let tm' = delazy defs tm in
case r of
LInf => TDelayed fc r tm'
_ => tm'
delazy defs (TDelay fc r ty tm)
= let ty' = delazy defs ty
tm' = delazy defs tm in
case r of
LInf => TDelay fc r ty' tm'
_ => tm'
delazy defs (TForce fc r t)
= case r of
LInf => TForce fc r (delazy defs t)
_ => delazy defs t
delazy defs (Meta fc n i args) = Meta fc n i (map (delazy defs) args)
delazy defs (Bind fc x b sc)
= Bind fc x (map (delazy defs) b) (delazy defs sc)
delazy defs (App fc f a) = App fc (delazy defs f) (delazy defs a)
delazy defs (As fc s a p) = As fc s (delazy defs a) (delazy defs p)
delazy defs tm = tm
mutual
findSC : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -79,8 +153,13 @@ mutual
-- If we're Guarded and find a Delay, continue with the argument as InDelay
findSC defs env Guarded pats (TDelay _ _ _ tm)
= findSC defs env InDelay pats tm
findSC defs env g pats (TDelay _ _ _ tm)
= findSC defs env g pats tm
findSC defs env g pats tm
= case (g, getFnArgs tm) of
= do let (fn, args) = getFnArgs tm
fn' <- conIfGuarded fn -- pretend it's a data constructor if
-- it has the AllGuarded flag
case (g, fn', args) of
-- If we're InDelay and find a constructor (or a function call which is
-- guaranteed to return a constructor; AllGuarded set), continue as InDelay
(InDelay, Ref fc (DataCon _ _) cn, args) =>
@ -91,6 +170,9 @@ mutual
(InDelay, _, args) =>
do scs <- traverse (findSC defs env Unguarded pats) args
pure (concat scs)
(Guarded, Ref fc (DataCon _ _) cn, args) =>
do scs <- traverse (findSC defs env Guarded pats) args
pure (concat scs)
(Toplevel, Ref fc (DataCon _ _) cn, args) =>
do scs <- traverse (findSC defs env Guarded pats) args
pure (concat scs)
@ -103,6 +185,16 @@ mutual
(_, f, args) =>
do scs <- traverse (findSC defs env Unguarded pats) args
pure (concat scs)
where
conIfGuarded : Term vars -> Core (Term vars)
conIfGuarded (Ref fc Func n)
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => pure $ Ref fc Func n
if AllGuarded `elem` flags gdef
then pure $ Ref fc (DataCon 0 0) n
else pure $ Ref fc Func n
conIfGuarded tm = pure tm
-- Expand the size change argument list with 'Nothing' to match the given
-- arity (i.e. the arity of the function we're calling) to ensure that
@ -279,32 +371,7 @@ mutual
pure ("Looking in case args " ++ show ps))
logTermNF 10 " =" env tm
rhs <- normaliseOpts tcOnly defs env tm
findSC defs env g pats rhs
-- Remove all force and delay annotations which are nothing to do with
-- coinduction meaning that all Delays left guard coinductive calls.
delazy : Defs -> Term vars -> Term vars
delazy defs (TDelayed fc r tm)
= let tm' = delazy defs tm in
case r of
LInf => TDelayed fc r tm'
_ => tm'
delazy defs (TDelay fc r ty tm)
= let ty' = delazy defs ty
tm' = delazy defs tm in
case r of
LInf => TDelay fc r ty' tm'
_ => tm'
delazy defs (TForce fc r t)
= case r of
LInf => TForce fc r (delazy defs t)
_ => delazy defs t
delazy defs (Meta fc n i args) = Meta fc n i (map (delazy defs) args)
delazy defs (Bind fc x b sc)
= Bind fc x (map (delazy defs) b) (delazy defs sc)
delazy defs (App fc f a) = App fc (delazy defs f) (delazy defs a)
delazy defs (As fc s a p) = As fc s (delazy defs a) (delazy defs p)
delazy defs tm = tm
findSC defs env g pats (delazy defs rhs)
findCalls : {auto c : Ref Ctxt Defs} ->
Defs -> (vars ** (Env Term vars, Term vars, Term vars)) ->

14
src/Core/Unify.idr
View File

@ -202,7 +202,7 @@ chaseMetas (n :: ns) all
= case lookup n all of
Just _ => chaseMetas ns all
_ => do defs <- get Ctxt
Just (PMDef _ _ (STerm soln) _ _) <-
Just (PMDef _ _ (STerm _ soln) _ _) <-
lookupDefExact n (gamma defs)
| _ => chaseMetas ns (insert n () all)
let sns = keys (getMetas soln)
@ -472,7 +472,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
logTerm 5 "Definition" rhs
let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs)
let newdef = record { definition =
PMDef simpleDef [] (STerm rhs) (STerm rhs) []
PMDef simpleDef [] (STerm 0 rhs) (STerm 0 rhs) []
} mdef
addDef (Resolved mref) newdef
removeHole mref
@ -1359,7 +1359,7 @@ retryGuess mode smode (hid, (loc, hname))
handleUnify
(do tm <- search loc rig (smode == Defaults) depth defining
(type def) []
let gdef = record { definition = PMDef defaultPI [] (STerm tm) (STerm tm) [] } def
let gdef = record { definition = PMDef defaultPI [] (STerm 0 tm) (STerm 0 tm) [] } def
logTermNF 5 ("Solved " ++ show hname) [] tm
addDef (Resolved hid) gdef
removeGuess hid
@ -1390,7 +1390,7 @@ retryGuess mode smode (hid, (loc, hname))
logTerm 5 "Retry Delay" tm
pure $ delayMeta r envb !(getTerm ty) tm
let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
[] (STerm tm') (STerm tm') [] } def
[] (STerm 0 tm') (STerm 0 tm') [] } def
logTerm 5 ("Resolved " ++ show hname) tm'
addDef (Resolved hid) gdef
removeGuess hid
@ -1416,7 +1416,7 @@ retryGuess mode smode (hid, (loc, hname))
-- proper definition and remove it from the
-- hole list
[] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True)
[] (STerm tm) (STerm tm) [] } def
[] (STerm 0 tm) (STerm 0 tm) [] } def
logTerm 5 ("Resolved " ++ show hname) tm
addDef (Resolved hid) gdef
removeGuess hid
@ -1479,7 +1479,7 @@ checkArgsSame : {auto u : Ref UST UState} ->
checkArgsSame [] = pure False
checkArgsSame (x :: xs)
= do defs <- get Ctxt
Just (PMDef _ [] (STerm def) _ _) <-
Just (PMDef _ [] (STerm 0 def) _ _) <-
lookupDefExact (Resolved x) (gamma defs)
| _ => checkArgsSame xs
s <- anySame def xs
@ -1491,7 +1491,7 @@ checkArgsSame (x :: xs)
anySame tm [] = pure False
anySame tm (t :: ts)
= do defs <- get Ctxt
Just (PMDef _ [] (STerm def) _ _) <-
Just (PMDef _ [] (STerm 0 def) _ _) <-
lookupDefExact (Resolved t) (gamma defs)
| _ => anySame tm ts
if !(convert defs [] tm def)

2
src/Idris/Desugar.idr
View File

@ -353,6 +353,8 @@ mutual
= desugarB side ps $
PLam fc top Explicit (PRef fc (MN "rec" 0)) (PImplicit fc) $
foldl (\r, f => PApp fc (PRef fc f) r) (PRef fc (MN "rec" 0)) fields
desugarB side ps (PWithUnambigNames fc ns rhs)
= IWithUnambigNames fc ns <$> desugarB side ps rhs
desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
{auto b : Ref Bang BangData} ->

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

@ -185,7 +185,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
fns <- topMethTypes [] impName methImps impsp (params cdata)
(map fst (methods cdata))
(methods cdata)
traverse (processDecl [] nest env) (map mkTopMethDecl fns)
traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)
-- 3. Build the record for the implementation
let mtops = map (Builtin.fst . snd) fns

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

@ -245,9 +245,7 @@ updateIfaceSyn iname cn ps cs ms ds
totMeth : (Name, RigCount, List FnOpt, (Bool, RawImp)) ->
Core (Name, RigCount, TotalReq, (Bool, RawImp))
totMeth (n, c, opts, t)
= do let treq = fromMaybe PartialOK (findSetTotal opts)
-- = do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts)
-- TODO: Put the above back when totality checker is properly working
= do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts)
pure (n, c, treq, t)
export
@ -395,6 +393,9 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
changeName : Name -> ImpClause -> ImpClause
changeName dn (PatClause fc lhs rhs)
= PatClause fc (changeNameTerm dn lhs) rhs
changeName dn (WithClause fc lhs wval cs)
= WithClause fc (changeNameTerm dn lhs) wval
(map (changeName dn) cs)
changeName dn (ImpossibleClause fc lhs)
= ImpossibleClause fc (changeNameTerm dn lhs)

15
src/Idris/Error.idr
View File

@ -258,6 +258,13 @@ perror (InRHS fc n err)
= pure $ "While processing right hand side of " ++ !(prettyName n) ++
" at " ++ show fc ++ ":\n" ++ !(perror err)
export
pwarning : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Warning -> Core String
pwarning (UnreachableClause fc env tm)
= pure $ "Warning: unreachable clause: " ++ !(pshow env tm)
export
display : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
@ -265,3 +272,11 @@ display : {auto c : Ref Ctxt Defs} ->
display err
= pure $ maybe "" (\f => show f ++ ":") (getErrorLoc err) ++
!(perror err)
export
displayWarning : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
Warning -> Core String
displayWarning w
= pure $ maybe "" (\f => show f ++ ":") (getWarningLoc w) ++
!(pwarning w)

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

@ -164,7 +164,7 @@ fnName lhs (UN n)
else "op"
fnName lhs (NS _ n) = fnName lhs n
fnName lhs (DN s _) = s
fnName lhs n = show n
fnName lhs n = nameRoot n
export

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

@ -15,6 +15,9 @@ data SExp = SExpList (List SExp)
| IntegerAtom Integer
| SymbolAtom String
public export
data DocMode = Overview | Full
public export
data IDECommand
= Interpret String
@ -22,12 +25,25 @@ data IDECommand
| TypeOf String (Maybe (Integer, Integer))
| CaseSplit Integer Integer String
| AddClause Integer String
-- deprecated: | AddProofClause
| AddMissing Integer String
| ExprSearch Integer String (List String) Bool
| GenerateDef Integer String
| MakeLemma Integer String
| MakeCase Integer String
| MakeWith Integer String
| DocsFor String (Maybe DocMode)
| Apropos String
| Metavariables Integer
| WhoCalls String
| CallsWho String
| BrowseNamespace String
| NormaliseTerm String -- TODO: implement a Binary lib
| ShowTermImplicits String -- and implement Binary (Term)
| HideTermImplicits String -- for these four defintions,
| ElaborateTerm String -- then change String to Term, as in idris1
| PrintDefinition String
| ReplCompletions String
| Version
| GetOptions
@ -58,6 +74,8 @@ getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])
= Just $ CaseSplit l 0 n
getIDECommand (SExpList [SymbolAtom "add-clause", IntegerAtom l, StringAtom n])
= Just $ AddClause l n
getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
= Just $ AddMissing line n
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n])
= Just $ ExprSearch l n [] False
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, SExpList hs])
@ -79,8 +97,36 @@ getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])
= Just $ MakeCase l n
getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
= Just $ MakeWith l n
getIDECommand (SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail))
= do -- Maybe monad
modeOpt <- case modeTail of
[] => Just Nothing
[SymbolAtom "overview"] => Just $ Just Overview
[SymbolAtom "full" ] => Just $ Just Full
_ => Nothing
Just $ DocsFor n modeOpt
getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n])
= Just $ Apropos n
getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n])
= Just $ Metavariables n
getIDECommand (SExpList [SymbolAtom "who-calls", StringAtom n])
= Just $ WhoCalls n
getIDECommand (SExpList [SymbolAtom "calls-who", StringAtom n])
= Just $ CallsWho n
getIDECommand (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
= Just $ BrowseNamespace ns
getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])
= Just $ NormaliseTerm tm
getIDECommand (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
= Just $ ShowTermImplicits tm
getIDECommand (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
= Just $ HideTermImplicits tm
getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
= Just $ ElaborateTerm tm
getIDECommand (SExpList [SymbolAtom "print-definition", StringAtom n])
= Just $ PrintDefinition n
getIDECommand (SExpList [SymbolAtom "repl-completions", StringAtom n])
= Just $ ReplCompletions n
getIDECommand (SymbolAtom "version") = Just Version
getIDECommand (SExpList [SymbolAtom "get-options"]) = Just GetOptions
getIDECommand _ = Nothing
@ -94,6 +140,7 @@ putIDECommand (TypeOf cmd Nothing) = (SExpList [SymbolAtom "type-of",
putIDECommand (TypeOf cmd (Just (line, col))) = (SExpList [SymbolAtom "type-of", StringAtom cmd, IntegerAtom line, IntegerAtom col])
putIDECommand (CaseSplit line col n) = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n])
putIDECommand (AddClause line n) = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n])
putIDECommand (AddMissing line n) = (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
putIDECommand (ExprSearch line n exprs mode) = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, SExpList $ map StringAtom exprs, getMode mode])
where
getMode : Bool -> SExp
@ -103,7 +150,22 @@ putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-
putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
putIDECommand (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
putIDECommand (DocsFor n modeOpt) = let modeTail = case modeOpt of
Nothing => []
Just Overview => [SymbolAtom "overview"]
Just Full => [SymbolAtom "full"] in
(SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail))
putIDECommand (Apropos n) = (SExpList [SymbolAtom "apropos", StringAtom n])
putIDECommand (Metavariables n) = (SExpList [SymbolAtom "metavariables", IntegerAtom n])
putIDECommand (WhoCalls n) = (SExpList [SymbolAtom "who-calls", StringAtom n])
putIDECommand (CallsWho n) = (SExpList [SymbolAtom "calls-who", StringAtom n])
putIDECommand (BrowseNamespace ns) = (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
putIDECommand (NormaliseTerm tm) = (SExpList [SymbolAtom "normalise-term", StringAtom tm])
putIDECommand (ShowTermImplicits tm) = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
putIDECommand (HideTermImplicits tm) = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
putIDECommand (ElaborateTerm tm) = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
putIDECommand (PrintDefinition n) = (SExpList [SymbolAtom "print-definition", StringAtom n])
putIDECommand (ReplCompletions n) = (SExpList [SymbolAtom "repl-completions", StringAtom n])
putIDECommand GetOptions = (SExpList [SymbolAtom "get-options"])
putIDECommand Version = SymbolAtom "version"

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

@ -5,31 +5,30 @@ module Idris.IDEMode.Parser
import Idris.IDEMode.Commands
import Text.Parser
import Data.List
import Data.Strings
import Parser.Lexer.Source
import Parser.Source
import Text.Lexer
import Text.Parser
import Utils.Either
import Utils.String
import Data.List
import Data.Strings
%hide Text.Lexer.symbols
%hide Parser.Lexer.Source.symbols
symbols : List String
symbols = ["(", ":", ")"]
ideTokens : TokenMap SourceToken
ideTokens : TokenMap Token
ideTokens =
map (\x => (exact x, Symbol)) symbols ++
[(digits, \x => Literal (cast x)),
(stringLit, \x => StrLit (stripQuotes x)),
(identAllowDashes, \x => NSIdent [x]),
[(digits, \x => IntegerLit (cast x)),
(stringLit, \x => StringLit (stripQuotes x)),
(identAllowDashes, \x => Ident x),
(space, Comment)]
idelex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
idelex : String -> Either (Int, Int, String) (List (TokenData Token))
idelex str
= case lex ideTokens str of
-- Add the EndInput token so that we'll have a line and column
@ -38,12 +37,12 @@ idelex str
[MkToken l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData SourceToken -> Bool
notComment : TokenData Token -> Bool
notComment t = case tok t of
Comment _ => False
_ => True
sexp : SourceRule SExp
sexp : Rule SExp
sexp
= do symbol ":"; exactIdent "True"
pure (BoolAtom True)
@ -60,15 +59,14 @@ sexp
symbol ")"
pure (SExpList xs)
ideParser : {e : _} ->
String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
ideParser : {e : _} -> String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty
ideParser str p
= do toks <- mapError LexFail $ idelex str
parsed <- mapError mapParseError $ parse p toks
parsed <- mapError toGenericParsingError $ parse p toks
Right (fst parsed)
export
parseSExp : String -> Either ParseError SExp
parseSExp : String -> Either (ParseError Token) SExp
parseSExp inp
= ideParser inp (do c <- sexp; eoi; pure c)

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

@ -119,49 +119,99 @@ getInput f
do inp <- getNChars f (integerToNat (cast num))
pure (pack inp)
||| Do nothing and tell the user to wait for us to implmement this (or join the effort!)
todoCmd : {auto o : Ref ROpts REPLOpts} ->
String -> Core ()
todoCmd cmdName = iputStrLn $ cmdName ++ ": command not yet implemented. Hopefully soon!"
data IDEResult
= REPL REPLResult
| NameList (List Name)
| Term String -- should be a PTerm + metadata, or SExp.
| TTTerm String -- should be a TT Term + metadata, or perhaps SExp
replWrap : Core REPLResult -> Core IDEResult
replWrap m = pure $ REPL !m
process : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
IDECommand -> Core REPLResult
IDECommand -> Core IDEResult
process (Interpret cmd)
= interpret cmd
= replWrap $ interpret cmd
process (LoadFile fname _)
= Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
= replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
process (TypeOf n Nothing)
= Idris.REPL.process (Check (PRef replFC (UN n)))
= replWrap $ Idris.REPL.process (Check (PRef replFC (UN n)))
process (TypeOf n (Just (l, c)))
= Idris.REPL.process (Editing (TypeAt (fromInteger l) (fromInteger c) (UN n)))
= replWrap $ Idris.REPL.process (Editing (TypeAt (fromInteger l) (fromInteger c) (UN n)))
process (CaseSplit l c n)
= Idris.REPL.process (Editing (CaseSplit False (fromInteger l) (fromInteger c) (UN n)))
= replWrap $ Idris.REPL.process (Editing (CaseSplit False (fromInteger l) (fromInteger c) (UN n)))
process (AddClause l n)
= Idris.REPL.process (Editing (AddClause False (fromInteger l) (UN n)))
= replWrap $ Idris.REPL.process (Editing (AddClause False (fromInteger l) (UN n)))
process (AddMissing l n)
= do todoCmd "add-missing"
pure $ REPL $ Edited $ DisplayEdit []
process (ExprSearch l n hs all)
= Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n)
= replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n)
(map UN hs) all))
process (GenerateDef l n)
= Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n)))
= replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n)))
process (MakeLemma l n)
= Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n)))
= replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n)))
process (MakeCase l n)
= Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN n)))
= replWrap $ Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN n)))
process (MakeWith l n)
= Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n)))
= replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n)))
process (DocsFor n modeOpt)
= do todoCmd "docs-for"
pure $ REPL $ Printed []
process (Apropos n)
= do todoCmd "apropros"
pure $ REPL $ Printed []
process (WhoCalls n)
= do todoCmd "who-calls"
pure $ NameList []
process (CallsWho n)
= do todoCmd "calls-who"
pure $ NameList []
process (BrowseNamespace ns)
= do todoCmd "browse-namespace"
pure $ NameList []
process (NormaliseTerm tm)
= do todoCmd "normalise-term"
pure $ Term tm
process (ShowTermImplicits tm)
= do todoCmd "show-term-implicits"
pure $ Term tm
process (HideTermImplicits tm)
= do todoCmd "hide-term-implicits"
pure $ Term tm
process (ElaborateTerm tm)
= do todoCmd "elaborate-term"
pure $ TTTerm tm
process (PrintDefinition n)
= do todoCmd "print-definition"
pure $ REPL $ Printed [n]
process (ReplCompletions n)
= do todoCmd "repl-completions"
pure $ NameList []
process Version
= Idris.REPL.process ShowVersion
= replWrap $ Idris.REPL.process ShowVersion
process (Metavariables _)
= Idris.REPL.process Metavars
= replWrap $ Idris.REPL.process Metavars
process GetOptions
= Idris.REPL.process GetOpts
= replWrap $ Idris.REPL.process GetOpts
processCatch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
IDECommand -> Core REPLResult
IDECommand -> Core IDEResult
processCatch cmd
= do c' <- branch
u' <- get UST
@ -175,7 +225,7 @@ processCatch cmd
put Syn s'
put ROpts o'
msg <- perror err
pure $ REPLError msg)
pure $ REPL $ REPLError msg)
idePutStrLn : File -> Integer -> String -> Core ()
idePutStrLn outf i msg
@ -212,41 +262,79 @@ SExpable REPLOpt where
sexpName : Name -> SExp
sexpName n = SExpList [ StringAtom (show n), SExpList [], SExpList [] ]
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} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
File -> Integer -> REPLResult -> Core ()
displayIDEResult outf i (REPLError err) = printIDEError outf i err
displayIDEResult outf i (Evaluated x Nothing) = printIDEResultWithHighlight outf i $ StringAtom $ show x
displayIDEResult outf i (Evaluated x (Just y)) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y
displayIDEResult outf i (Printed xs) = printIDEResultWithHighlight outf i $ StringAtom $ showSep "\n" xs
displayIDEResult outf i (TermChecked x y) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y
displayIDEResult outf i (FileLoaded x) = printIDEResult outf i $ SExpList []
displayIDEResult outf i (ErrorLoadingFile x err) = printIDEError outf i $ "Error loading file " ++ x ++ ": " ++ show err
displayIDEResult outf i (ErrorsBuildingFile x errs) = printIDEError outf i $ "Error(s) building file " ++ x ++ ": " ++ (showSep "\n" $ map show errs)
displayIDEResult outf i NoFileLoaded = printIDEError outf i "No file can be reloaded"
displayIDEResult outf i (CurrentDirectory dir) = printIDEResult outf i $ StringAtom $ "Current working directory is '" ++ dir ++ "'"
displayIDEResult outf i CompilationFailed = printIDEError outf i "Compilation failed"
displayIDEResult outf i (Compiled f) = printIDEResult outf i $ StringAtom $ "File " ++ f ++ " written"
displayIDEResult outf i (ProofFound x) = printIDEResult outf i $ StringAtom $ show x
--displayIDEResult outf i (Missed cases) = printIDEResult outf i $ showSep "\n" $ map handleMissing cases
displayIDEResult outf i (CheckedTotal xs) = printIDEResult outf i $ StringAtom $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs
displayIDEResult outf i (FoundHoles []) = printIDEResult outf i $ SExpList []
displayIDEResult outf i (FoundHoles xs) = printIDEResult outf i $ holesSexp
File -> Integer -> IDEResult -> Core ()
displayIDEResult outf i (REPL $ REPLError err)
= printIDEError outf i err
displayIDEResult outf i (REPL RequestedHelp )
= printIDEResult outf i
$ StringAtom $ displayHelp
displayIDEResult outf i (REPL $ Evaluated x Nothing)
= printIDEResultWithHighlight outf i
$ StringAtom $ show x
displayIDEResult outf i (REPL $ Evaluated x (Just y))
= printIDEResultWithHighlight outf i
$ StringAtom $ show x ++ " : " ++ show y
displayIDEResult outf i (REPL $ Printed xs)
= printIDEResultWithHighlight outf i
$ StringAtom $ showSep "\n" xs
displayIDEResult outf i (REPL $ TermChecked x y)
= printIDEResultWithHighlight outf i
$ StringAtom $ show x ++ " : " ++ show y
displayIDEResult outf i (REPL $ FileLoaded x)
= printIDEResult outf i $ SExpList []
displayIDEResult outf i (REPL $ ErrorLoadingFile x err)
= printIDEError outf i
$ "Error loading file " ++ x ++ ": " ++ show err
displayIDEResult outf i (REPL $ ErrorsBuildingFile x errs)
= printIDEError outf i
$ "Error(s) building file " ++ x ++ ": " ++
(showSep "\n" $ map show errs)
displayIDEResult outf i (REPL $ NoFileLoaded)
= printIDEError outf i "No file can be reloaded"
displayIDEResult outf i (REPL $ CurrentDirectory dir)
= printIDEResult outf i
$ StringAtom $ "Current working directory is '" ++ dir ++ "'"
displayIDEResult outf i (REPL CompilationFailed)
= printIDEError outf i "Compilation failed"
displayIDEResult outf i (REPL $ Compiled f)
= printIDEResult outf i $ StringAtom
$ "File " ++ f ++ " written"
displayIDEResult outf i (REPL $ ProofFound x)
= printIDEResult outf i
$ StringAtom $ show x
displayIDEResult outf i (REPL $ Missed cases)
= printIDEResult outf i
$ StringAtom $ showSep "\n"
$ map handleMissing cases
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 (LogLevelSet k) = printIDEResult outf i $ StringAtom $ "Set loglevel to " ++ show k
displayIDEResult outf i (OptionsSet opts) = printIDEResult outf i optionsSexp
displayIDEResult outf i (REPL $ LogLevelSet k)
= printIDEResult outf i
$ StringAtom $ "Set loglevel to " ++ show k
displayIDEResult outf i (REPL $ OptionsSet opts)
= printIDEResult outf i optionsSexp
where
optionsSexp : SExp
optionsSexp = SExpList $ map toSExp opts
displayIDEResult outf i (VersionIs x) = printIDEResult outf i versionSExp
displayIDEResult outf i (REPL $ VersionIs x)
= printIDEResult outf i versionSExp
where
semverSexp : SExp
semverSexp = case (semVer x) of
@ -258,11 +346,19 @@ displayIDEResult outf i (VersionIs x) = printIDEResult outf i versionSExp
versionSExp : SExp
versionSExp = SExpList [ semverSexp, tagSexp ]
displayIDEResult outf i (Edited (DisplayEdit xs)) = printIDEResult outf i $ StringAtom $ showSep "\n" xs
displayIDEResult outf i (Edited (EditError x)) = printIDEError outf i x
displayIDEResult outf i (Edited (MadeLemma lit name pty pappstr)) =
printIDEResult outf i $ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr
displayIDEResult outf i (REPL $ Edited (DisplayEdit xs))
= printIDEResult outf i $ StringAtom $ showSep "\n" xs
displayIDEResult outf i (REPL $ Edited (EditError x))
= printIDEError outf i x
displayIDEResult outf i (REPL $ Edited (MadeLemma lit name pty pappstr))
= printIDEResult outf i
$ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr
displayIDEResult outf i (NameList ns)
= printIDEResult outf i $ SExpList $ map toSExp ns
displayIDEResult outf i (Term t)
= printIDEResult outf i $ StringAtom t
displayIDEResult outf i (TTTerm t)
= printIDEResult outf i $ StringAtom t
displayIDEResult outf i _ = pure ()
@ -271,8 +367,8 @@ handleIDEResult : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
File -> Integer -> REPLResult -> Core ()
handleIDEResult outf i Exited = idePutStrLn outf i "Bye for now!"
File -> Integer -> IDEResult -> Core ()
handleIDEResult outf i (REPL Exited) = idePutStrLn outf i "Bye for now!"
handleIDEResult outf i other = displayIDEResult outf i other
loop : {auto c : Ref Ctxt Defs} ->

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

@ -58,6 +58,7 @@ SExpable Highlight where
inFile : String -> (FC, (Name, Nat, ClosedTerm)) -> Bool
inFile fname (MkFC file _ _, _) = file == fname
inFile _ (EmptyFC, _) = False
||| Output some data using current dialog index
export

39
src/Idris/Main.idr
View File

@ -37,11 +37,10 @@ findInput [] = Nothing
findInput (InputFile f :: fs) = Just f
findInput (_ :: fs) = findInput fs
-- Add extra library directories from the "BLODWEN_PATH"
-- environment variable
updatePaths : {auto c : Ref Ctxt Defs} ->
Core ()
updatePaths
-- Add extra data from the "IDRIS2_x" environment variables
updateEnv : {auto c : Ref Ctxt Defs} ->
Core ()
updateEnv
= do bprefix <- coreLift $ getEnv "IDRIS2_PREFIX"
the (Core ()) $ case bprefix of
Just p => setPrefix p
@ -58,6 +57,13 @@ updatePaths
the (Core ()) $ case blibs of
Just path => do traverse_ addLibDir (map trim (split (==pathSep) path))
Nothing => pure ()
cg <- coreLift $ getEnv "IDRIS2_CG"
the (Core ()) $ case cg of
Just e => case getCG e of
Just cg => setCG cg
Nothing => throw (InternalError ("Unknown code generator " ++ show e))
Nothing => pure ()
-- IDRIS2_PATH goes first so that it overrides this if there's
-- any conflicts. In particular, that means that setting IDRIS2_PATH
-- for the tests means they test the local version not the installed
@ -78,7 +84,7 @@ updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
updateREPLOpts
= do opts <- get ROpts
ed <- coreLift $ getEnv "EDITOR"
case ed of
the (Core ()) $ case ed of
Just e => put ROpts (record { editor = e } opts)
Nothing => pure ()
@ -133,7 +139,7 @@ stMain opts
addPrimitives
setWorkingDir "."
updatePaths
updateEnv
let ide = ideMode opts
let ideSocket = ideModeSocket opts
let outmode = if ide then IDEMode 0 stdin stdout else REPL False
@ -177,16 +183,15 @@ stMain opts
setOutput (IDEMode 0 stdin stdout)
replIDE {c} {u} {m}
else do
throw (InternalError "Not implemeted yet")
-- let (host, port) = ideSocketModeHostPort opts
-- f <- coreLift $ initIDESocketFile host port
-- case f of
-- Left err => do
-- coreLift $ putStrLn err
-- coreLift $ exit 1
-- Right file => do
-- setOutput (IDEMode 0 file file)
-- replIDE {c} {u} {m}
let (host, port) = ideSocketModeHostPort opts
f <- coreLift $ initIDESocketFile host port
case f of
Left err => do
coreLift $ putStrLn err
coreLift $ exitWith (ExitFailure 1)
Right file => do
setOutput (IDEMode 0 file file)
replIDE {c} {u} {m}
else do
repl {c} {u} {m}
showTimeRecord

8
src/Idris/ModTree.idr
View File

@ -20,6 +20,7 @@ import Idris.Syntax
import Data.List
import Data.StringMap
import System.Directory
import System.File
%default covering
@ -183,11 +184,14 @@ buildMod loc num len mod
": Building " ++ showMod ++
" (" ++ src ++ ")"
[] <- process {u} {m} msg src
| errs => do traverse emitError errs
| errs => do emitWarnings
traverse emitError errs
pure (ferrs ++ errs)
emitWarnings
traverse_ emitError ferrs
pure ferrs
else do traverse_ emitError ferrs
else do emitWarnings
traverse_ emitError ferrs
pure ferrs
where
getEithers : List (Either a b) -> (List a, List b)

73
src/Idris/Package.idr
View File

@ -15,6 +15,12 @@ import Data.Strings
import Data.StringTrie
import Data.These
import Parser.Package
import System
import Text.Parser
import Utils.Binary
import Utils.String
import Idris.CommandLine
import Idris.ModTree
import Idris.ProcessIdr
@ -23,13 +29,6 @@ import Idris.REPLOpts
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import Parser.Lexer.Source
import Parser.Source
import Utils.Binary
import System
import Text.Parser
import IdrisPaths
%default covering
@ -114,7 +113,7 @@ data DescField : Type where
PPreclean : FC -> String -> DescField
PPostclean : FC -> String -> DescField
field : String -> SourceRule DescField
field : String -> Rule DescField
field fname
= strField PVersion "version"
<|> strField PAuthors "authors"
@ -134,43 +133,41 @@ field fname
<|> strField PPostinstall "postinstall"
<|> strField PPreclean "preclean"
<|> strField PPostclean "postclean"
<|> do exactIdent "depends"; symbol "="
ds <- sepBy1 (symbol ",") unqualifiedName
<|> do exactProperty "depends"
equals
ds <- sep packageName
pure (PDepends ds)
<|> do exactIdent "modules"; symbol "="
ms <- sepBy1 (symbol ",")
(do start <- location
ns <- nsIdent
end <- location
pure (MkFC fname start end, ns))
<|> do exactProperty "modules"
equals
ms <- sep (do start <- location
m <- moduleIdent
end <- location
pure (MkFC fname start end, m))
pure (PModules ms)
<|> do exactIdent "main"; symbol "="
<|> do exactProperty "main"
equals
start <- location
m <- nsIdent
m <- namespacedIdent
end <- location
pure (PMainMod (MkFC fname start end) m)
<|> do exactIdent "executable"; symbol "="
e <- unqualifiedName
<|> do exactProperty "executable"
equals
e <- (stringLit <|> packageName)
pure (PExec e)
where
getStr : (FC -> String -> DescField) -> FC ->
String -> Constant -> SourceEmptyRule DescField
getStr p fc fld (Str s) = pure (p fc s)
getStr p fc fld _ = fail $ fld ++ " field must be a string"
strField : (FC -> String -> DescField) -> String -> SourceRule DescField
strField p f
strField : (FC -> String -> DescField) -> String -> Rule DescField
strField fieldConstructor fieldName
= do start <- location
exactIdent f
symbol "="
c <- constant
exactProperty fieldName
equals
str <- stringLit
end <- location
getStr p (MkFC fname start end) f c
pure $ fieldConstructor (MkFC fname start end) str
parsePkgDesc : String -> SourceRule (String, List DescField)
parsePkgDesc : String -> Rule (String, List DescField)
parsePkgDesc fname
= do exactIdent "package"
name <- unqualifiedName
= do exactProperty "package"
name <- packageName
fields <- many (field fname)
pure (name, fields)
@ -412,7 +409,7 @@ clean pkg
runScript (postclean pkg)
where
delete : String -> Core ()
delete path = do Right () <- coreLift $ fileRemove path
delete path = do Right () <- coreLift $ removeFile path
| Left err => pure ()
coreLift $ putStrLn $ "Removed: " ++ path
@ -425,6 +422,12 @@ clean pkg
delete $ ttFile ++ ".ttc"
delete $ ttFile ++ ".ttm"
getParseErrorLoc : String -> ParseError Token -> FC
getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
getParseErrorLoc fname (LitFail _) = MkFC fname (0, 0) (0, 0) -- TODO: Remove this unused case
getParseErrorLoc fname _ = replFC
-- Just load the 'Main' module, if it exists, which will involve building
-- it if necessary
runRepl : {auto c : Ref Ctxt Defs} ->

237
src/Idris/Parser.idr
View File

@ -14,7 +14,7 @@ import Data.Strings
%default covering
-- Forward declare since they're used in the parser
topDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
topDecl : FileName -> IndentInfo -> Rule (List PDecl)
collectDefs : List PDecl -> List PDecl
-- Some context for the parser
@ -46,7 +46,7 @@ plhs = MkParseOpts False False
%hide Prelude.pure
%hide Core.Core.pure
atom : FileName -> SourceRule PTerm
atom : FileName -> Rule PTerm
atom fname
= do start <- location
x <- constant
@ -85,30 +85,30 @@ atom fname
end <- location
pure (PRef (MkFC fname start end) x)
whereBlock : FileName -> Int -> SourceRule (List PDecl)
whereBlock : FileName -> Int -> Rule (List PDecl)
whereBlock fname col
= do keyword "where"
ds <- blockAfter col (topDecl fname)
pure (collectDefs (concat ds))
-- Expect a keyword, but if we get anything else it's a fatal error
commitKeyword : IndentInfo -> String -> SourceRule ()
commitKeyword : IndentInfo -> String -> Rule ()
commitKeyword indents req
= do mustContinue indents (Just req)
keyword req
mustContinue indents Nothing
commitSymbol : String -> SourceRule ()
commitSymbol : String -> Rule ()
commitSymbol req
= symbol req
<|> fatalError ("Expected '" ++ req ++ "'")
continueWith : IndentInfo -> String -> SourceRule ()
continueWith : IndentInfo -> String -> Rule ()
continueWith indents req
= do mustContinue indents (Just req)
symbol req
iOperator : SourceRule Name
iOperator : Rule Name
iOperator
= operator
<|> do symbol "`"
@ -122,12 +122,13 @@ data ArgType
| WithArg PTerm
mutual
appExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
appExpr q fname indents
= case_ fname indents
<|> lambdaCase fname indents
<|> lazy fname indents
<|> if_ fname indents
<|> with_ fname indents
<|> doBlock fname indents
<|> do start <- location
f <- simpleExpr fname indents
@ -152,7 +153,7 @@ mutual
applyExpImp start end f (WithArg exp :: args)
= applyExpImp start end (PWithApp (MkFC fname start end) f exp) args
argExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule ArgType
argExpr : ParseOpts -> FileName -> IndentInfo -> Rule ArgType
argExpr q fname indents
= do continue indents
arg <- simpleExpr fname indents
@ -169,7 +170,7 @@ mutual
pure (WithArg arg)
else fail "| not allowed here"
implicitArg : FileName -> IndentInfo -> SourceRule (Maybe Name, PTerm)
implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, PTerm)
implicitArg fname indents
= do start <- location
symbol "{"
@ -188,7 +189,30 @@ mutual
symbol "}"
pure (Nothing, tm)
opExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
with_ : FileName -> IndentInfo -> Rule PTerm
with_ fname indents
= do start <- location
keyword "with"
commit
ns <- singleName <|> nameList
end <- location
rhs <- expr pdef fname indents
pure (PWithUnambigNames (MkFC fname start end) ns rhs)
where
singleName : Rule (List Name)
singleName = do
n <- name
pure [n]
nameList : Rule (List Name)
nameList = do
symbol "["
commit
ns <- sepBy1 (symbol ",") name
symbol "]"
pure ns
opExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
opExpr q fname indents
= do start <- location
l <- appExpr q fname indents
@ -208,7 +232,7 @@ mutual
pure (POp (MkFC fname start end) op l r))
<|> pure l
dpair : FileName -> FilePos -> IndentInfo -> SourceRule PTerm
dpair : FileName -> FilePos -> IndentInfo -> Rule PTerm
dpair fname start indents
= do x <- unqualifiedName
symbol ":"
@ -231,7 +255,7 @@ mutual
(PImplicit (MkFC fname start end))
rest)
bracketedExpr : FileName -> FilePos -> IndentInfo -> SourceRule PTerm
bracketedExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm
bracketedExpr fname start indents
-- left section. This may also be a prefix operator, but we'll sort
-- that out when desugaring: if the operator is infix, treat it as a
@ -263,7 +287,7 @@ mutual
getInitRange [x, y] = pure (x, Just y)
getInitRange _ = fatalError "Invalid list range syntax"
listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> SourceRule PTerm
listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> Rule PTerm
listRange fname start indents xs
= do symbol "]"
end <- location
@ -277,7 +301,7 @@ mutual
rstate <- getInitRange xs
pure (PRange fc (fst rstate) (snd rstate) y)
listExpr : FileName -> FilePos -> IndentInfo -> SourceRule PTerm
listExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm
listExpr fname start indents
= do ret <- expr pnowith fname indents
symbol "|"
@ -293,7 +317,7 @@ mutual
pure (PList (MkFC fname start end) xs))
-- A pair, dependent pair, or just a single expression
tuple : FileName -> FilePos -> IndentInfo -> PTerm -> SourceRule PTerm
tuple : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PTerm
tuple fname start indents e
= do rest <- some (do symbol ","
estart <- location
@ -313,7 +337,7 @@ mutual
mergePairs end ((estart, exp) :: rest)
= PPair (MkFC fname estart end) exp (mergePairs end rest)
simpleExpr : FileName -> IndentInfo -> SourceRule PTerm
simpleExpr : FileName -> IndentInfo -> Rule PTerm
simpleExpr fname indents
= do
start <- location
@ -329,7 +353,7 @@ mutual
[] => root
fs => PRecordFieldAccess (MkFC fname start end) root recFields
simplerExpr : FileName -> IndentInfo -> SourceRule PTerm
simplerExpr : FileName -> IndentInfo -> Rule PTerm
simplerExpr fname indents
= do start <- location
x <- unqualifiedName
@ -405,7 +429,7 @@ mutual
= PPi fc rig p n ty (pibindAll fc p rest scope)
bindList : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, PTerm, PTerm))
Rule (List (RigCount, PTerm, PTerm))
bindList fname start indents
= sepBy1 (symbol ",")
(do rigc <- multiplicity
@ -418,7 +442,7 @@ mutual
pure (rig, pat, ty))
pibindListName : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, Name, PTerm))
Rule (List (RigCount, Name, PTerm))
pibindListName fname start indents
= do rigc <- multiplicity
ns <- sepBy1 (symbol ",") unqualifiedName
@ -436,12 +460,12 @@ mutual
pure (rig, n, ty))
pibindList : FileName -> FilePos -> IndentInfo ->
SourceRule (List (RigCount, Maybe Name, PTerm))
Rule (List (RigCount, Maybe Name, PTerm))
pibindList fname start indents
= do params <- pibindListName fname start indents
pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params
bindSymbol : SourceRule (PiInfo PTerm)
bindSymbol : Rule (PiInfo PTerm)
bindSymbol
= do symbol "->"
pure Explicit
@ -449,7 +473,7 @@ mutual
pure AutoImplicit
explicitPi : FileName -> IndentInfo -> SourceRule PTerm
explicitPi : FileName -> IndentInfo -> Rule PTerm
explicitPi fname indents
= do start <- location
symbol "("
@ -460,7 +484,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) exp binders scope)
autoImplicitPi : FileName -> IndentInfo -> SourceRule PTerm
autoImplicitPi : FileName -> IndentInfo -> Rule PTerm
autoImplicitPi fname indents
= do start <- location
symbol "{"
@ -473,7 +497,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
defaultImplicitPi : FileName -> IndentInfo -> SourceRule PTerm
defaultImplicitPi : FileName -> IndentInfo -> Rule PTerm
defaultImplicitPi fname indents
= do start <- location
symbol "{"
@ -487,7 +511,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) (DefImplicit t) binders scope)
forall_ : FileName -> IndentInfo -> SourceRule PTerm
forall_ : FileName -> IndentInfo -> Rule PTerm
forall_ fname indents
= do start <- location
keyword "forall"
@ -503,7 +527,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
implicitPi : FileName -> IndentInfo -> SourceRule PTerm
implicitPi : FileName -> IndentInfo -> Rule PTerm
implicitPi fname indents
= do start <- location
symbol "{"
@ -514,7 +538,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
lam : FileName -> IndentInfo -> SourceRule PTerm
lam : FileName -> IndentInfo -> Rule PTerm
lam fname indents
= do start <- location
symbol "\\"
@ -531,7 +555,7 @@ mutual
= PLam fc rig Explicit pat ty (bindAll fc rest scope)
letBinder : FileName -> IndentInfo ->
SourceRule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
letBinder fname indents
= do start <- location
rigc <- multiplicity
@ -570,7 +594,7 @@ mutual
= let fc = MkFC fname start end in
DoLetPat fc pat ty val alts :: buildDoLets fname rest
let_ : FileName -> IndentInfo -> SourceRule PTerm
let_ : FileName -> IndentInfo -> Rule PTerm
let_ fname indents
= do start <- location
keyword "let"
@ -589,7 +613,7 @@ mutual
end <- location
pure (PLocal (MkFC fname start end) (collectDefs (concat ds)) scope)
case_ : FileName -> IndentInfo -> SourceRule PTerm
case_ : FileName -> IndentInfo -> Rule PTerm
case_ fname indents
= do start <- location
keyword "case"
@ -599,7 +623,7 @@ mutual
end <- location
pure (PCase (MkFC fname start end) scr alts)
lambdaCase : FileName -> IndentInfo -> SourceRule PTerm
lambdaCase : FileName -> IndentInfo -> Rule PTerm
lambdaCase fname indents
= do start <- location
symbol "\\" *> keyword "case"
@ -614,13 +638,13 @@ mutual
PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
PCase fc (PRef fcCase n) alts)
caseAlt : FileName -> IndentInfo -> SourceRule PClause
caseAlt : FileName -> IndentInfo -> Rule PClause
caseAlt fname indents
= do start <- location
lhs <- opExpr plhs fname indents
caseRHS fname start indents lhs
caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> SourceRule PClause
caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PClause
caseRHS fname start indents lhs
= do symbol "=>"
mustContinue indents Nothing
@ -633,7 +657,7 @@ mutual
end <- location
pure (MkImpossible (MkFC fname start end) lhs)
if_ : FileName -> IndentInfo -> SourceRule PTerm
if_ : FileName -> IndentInfo -> Rule PTerm
if_ fname indents
= do start <- location
keyword "if"
@ -646,7 +670,7 @@ mutual
end <- location
pure (PIfThenElse (MkFC fname start end) x t e)
record_ : FileName -> IndentInfo -> SourceRule PTerm
record_ : FileName -> IndentInfo -> Rule PTerm
record_ fname indents
= do start <- location
keyword "record"
@ -657,7 +681,7 @@ mutual
end <- location
pure (PUpdate (MkFC fname start end) fs)
field : FileName -> IndentInfo -> SourceRule PFieldUpdate
field : FileName -> IndentInfo -> Rule PFieldUpdate
field fname indents
= do path <- map fieldName <$> [| name :: many recFieldCompat |]
upd <- (do symbol "="; pure PSetField)
@ -673,10 +697,10 @@ mutual
-- this allows the dotted syntax .field
-- but also the arrowed syntax ->field for compatibility with Idris 1
recFieldCompat : SourceRule Name
recFieldCompat : Rule Name
recFieldCompat = recField <|> (symbol "->" *> name)
rewrite_ : FileName -> IndentInfo -> SourceRule PTerm
rewrite_ : FileName -> IndentInfo -> Rule PTerm
rewrite_ fname indents
= do start <- location
keyword "rewrite"
@ -686,7 +710,7 @@ mutual
end <- location
pure (PRewrite (MkFC fname start end) rule tm)
doBlock : FileName -> IndentInfo -> SourceRule PTerm
doBlock : FileName -> IndentInfo -> Rule PTerm
doBlock fname indents
= do start <- location
keyword "do"
@ -704,7 +728,7 @@ mutual
else fail "Not a pattern variable"
validPatternVar _ = fail "Not a pattern variable"
doAct : FileName -> IndentInfo -> SourceRule (List PDo)
doAct : FileName -> IndentInfo -> Rule (List PDo)
doAct fname indents
= do start <- location
n <- name
@ -744,12 +768,12 @@ mutual
end <- location
pure [DoBindPat (MkFC fname start end) e val alts])
patAlt : FileName -> IndentInfo -> SourceRule PClause
patAlt : FileName -> IndentInfo -> Rule PClause
patAlt fname indents
= do symbol "|"
caseAlt fname indents
lazy : FileName -> IndentInfo -> SourceRule PTerm
lazy : FileName -> IndentInfo -> Rule PTerm
lazy fname indents
= do start <- location
exactIdent "Lazy"
@ -772,7 +796,7 @@ mutual
end <- location
pure (PForce (MkFC fname start end) tm)
binder : FileName -> IndentInfo -> SourceRule PTerm
binder : FileName -> IndentInfo -> Rule PTerm
binder fname indents
= let_ fname indents
<|> autoImplicitPi fname indents
@ -782,7 +806,7 @@ mutual
<|> explicitPi fname indents
<|> lam fname indents
typeExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
typeExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
typeExpr q fname indents
= do start <- location
arg <- opExpr q fname indents
@ -801,10 +825,10 @@ mutual
(mkPi start end a as)
export
expr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
expr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
expr = typeExpr
visOption : SourceRule Visibility
visOption : Rule Visibility
visOption
= do keyword "public"
keyword "export"
@ -819,7 +843,7 @@ visibility
= visOption
<|> pure Private
tyDecl : FileName -> IndentInfo -> SourceRule PTypeDecl
tyDecl : FileName -> IndentInfo -> Rule PTypeDecl
tyDecl fname indents
= do start <- location
n <- name
@ -833,7 +857,7 @@ tyDecl fname indents
mutual
parseRHS : (withArgs : Nat) ->
FileName -> FilePos -> Int ->
IndentInfo -> (lhs : PTerm) -> SourceRule PClause
IndentInfo -> (lhs : PTerm) -> Rule PClause
parseRHS withArgs fname start col indents lhs
= do symbol "="
mustWork $
@ -858,7 +882,7 @@ mutual
ifThenElse True t e = t
ifThenElse False t e = e
clause : Nat -> FileName -> IndentInfo -> SourceRule PClause
clause : Nat -> FileName -> IndentInfo -> Rule PClause
clause withArgs fname indents
= do start <- location
col <- column
@ -874,7 +898,7 @@ mutual
applyArgs f [] = f
applyArgs f ((fc, a) :: args) = applyArgs (PApp fc f a) args
parseWithArg : SourceRule (FC, PTerm)
parseWithArg : Rule (FC, PTerm)
parseWithArg
= do symbol "|"
start <- location
@ -903,7 +927,7 @@ mkDataConType fc ret (WithArg a :: xs)
= PImplicit fc -- This can't happen because we parse constructors without
-- withOK set
simpleCon : FileName -> PTerm -> IndentInfo -> SourceRule PTypeDecl
simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
simpleCon fname ret indents
= do start <- location
cname <- name
@ -913,7 +937,7 @@ simpleCon fname ret indents
pure (let cfc = MkFC fname start end in
MkPTy cfc cname (mkDataConType cfc ret params))
simpleData : FileName -> FilePos -> Name -> IndentInfo -> SourceRule PDataDecl
simpleData : FileName -> FilePos -> Name -> IndentInfo -> Rule PDataDecl
simpleData fname start n indents
= do params <- many name
tyend <- location
@ -927,7 +951,7 @@ simpleData fname start n indents
pure (MkPData (MkFC fname start end) n
(mkTyConType tyfc params) [] cons)
dataOpt : SourceRule DataOpt
dataOpt : Rule DataOpt
dataOpt
= do exactIdent "noHints"
pure NoHints
@ -956,14 +980,14 @@ dataBody fname mincol start n indents ty
end <- location
pure (MkPData (MkFC fname start end) n ty opts cs)
gadtData : FileName -> Int -> FilePos -> Name -> IndentInfo -> SourceRule PDataDecl
gadtData : FileName -> Int -> FilePos -> Name -> IndentInfo -> Rule PDataDecl
gadtData fname mincol start n indents
= do symbol ":"
commit
ty <- expr pdef fname indents
dataBody fname mincol start n indents ty
dataDeclBody : FileName -> IndentInfo -> SourceRule PDataDecl
dataDeclBody : FileName -> IndentInfo -> Rule PDataDecl
dataDeclBody fname indents
= do start <- location
col <- column
@ -972,7 +996,7 @@ dataDeclBody fname indents
simpleData fname start n indents
<|> gadtData fname col start n indents
dataDecl : FileName -> IndentInfo -> SourceRule PDecl
dataDecl : FileName -> IndentInfo -> Rule PDecl
dataDecl fname indents
= do start <- location
vis <- visibility
@ -987,19 +1011,19 @@ stripBraces str = pack (drop '{' (reverse (drop '}' (reverse (unpack str)))))
drop c [] = []
drop c (c' :: xs) = if c == c' then drop c xs else c' :: xs
onoff : SourceRule Bool
onoff : Rule Bool
onoff
= do exactIdent "on"
pure True
<|> do exactIdent "off"
pure False
extension : SourceRule LangExt
extension : Rule LangExt
extension
= do exactIdent "Borrowing"
pure Borrowing
totalityOpt : SourceRule TotalReq
totalityOpt : Rule TotalReq
totalityOpt
= do keyword "partial"
pure PartialOK
@ -1008,7 +1032,7 @@ totalityOpt
<|> do keyword "covering"
pure CoveringOnly
directive : FileName -> IndentInfo -> SourceRule Directive
directive : FileName -> IndentInfo -> Rule Directive
directive fname indents
= do pragma "hide"
n <- name
@ -1083,21 +1107,21 @@ directive fname indents
atEnd indents
pure (DefaultTotality tot)
fix : SourceRule Fixity
fix : Rule Fixity
fix
= do keyword "infixl"; pure InfixL
<|> do keyword "infixr"; pure InfixR
<|> do keyword "infix"; pure Infix
<|> do keyword "prefix"; pure Prefix
namespaceHead : SourceRule (List String)
namespaceHead : Rule (List String)
namespaceHead
= do keyword "namespace"
commit
ns <- nsIdent
ns <- namespacedIdent
pure ns
namespaceDecl : FileName -> IndentInfo -> SourceRule PDecl
namespaceDecl : FileName -> IndentInfo -> Rule PDecl
namespaceDecl fname indents
= do start <- location
ns <- namespaceHead
@ -1105,7 +1129,7 @@ namespaceDecl fname indents
ds <- assert_total (nonEmptyBlock (topDecl fname))
pure (PNamespace (MkFC fname start end) ns (concat ds))
transformDecl : FileName -> IndentInfo -> SourceRule PDecl
transformDecl : FileName -> IndentInfo -> Rule PDecl
transformDecl fname indents
= do start <- location
pragma "transform"
@ -1116,7 +1140,7 @@ transformDecl fname indents
end <- location
pure (PTransform (MkFC fname start end) n lhs rhs)
mutualDecls : FileName -> IndentInfo -> SourceRule PDecl
mutualDecls : FileName -> IndentInfo -> Rule PDecl
mutualDecls fname indents
= do start <- location
keyword "mutual"
@ -1125,7 +1149,7 @@ mutualDecls fname indents
end <- location
pure (PMutual (MkFC fname start end) (concat ds))
paramDecls : FileName -> IndentInfo -> SourceRule PDecl
paramDecls : FileName -> IndentInfo -> Rule PDecl
paramDecls fname indents
= do start <- location
keyword "parameters"
@ -1141,7 +1165,7 @@ paramDecls fname indents
end <- location
pure (PParameters (MkFC fname start end) ps (collectDefs (concat ds)))
usingDecls : FileName -> IndentInfo -> SourceRule PDecl
usingDecls : FileName -> IndentInfo -> Rule PDecl
usingDecls fname indents
= do start <- location
keyword "using"
@ -1159,11 +1183,11 @@ usingDecls fname indents
end <- location
pure (PUsing (MkFC fname start end) us (collectDefs (concat ds)))
fnOpt : SourceRule PFnOpt
fnOpt : Rule PFnOpt
fnOpt = do x <- totalityOpt
pure $ IFnOpt (Totality x)
fnDirectOpt : FileName -> SourceRule PFnOpt
fnDirectOpt : FileName -> Rule PFnOpt
fnDirectOpt fname
= do pragma "hint"
pure $ IFnOpt (Hint True)
@ -1174,6 +1198,9 @@ fnDirectOpt fname
<|> do pragma "inline"
commit
pure $ IFnOpt Inline
<|> do pragma "tcinline"
commit
pure $ IFnOpt TCInline
<|> do pragma "extern"
pure $ IFnOpt ExternFn
<|> do pragma "macro"
@ -1185,7 +1212,7 @@ fnDirectOpt fname
cs <- block (expr pdef fname)
pure $ PForeign cs
visOpt : FileName -> SourceRule (Either Visibility PFnOpt)
visOpt : FileName -> Rule (Either Visibility PFnOpt)
visOpt fname
= do vis <- visOption
pure (Left vis)
@ -1237,7 +1264,7 @@ implBinds fname indents
pure ((n, rig, tm) :: more)
<|> pure []
ifaceParam : FileName -> IndentInfo -> SourceRule (Name, PTerm)
ifaceParam : FileName -> IndentInfo -> Rule (Name, PTerm)
ifaceParam fname indents
= do symbol "("
n <- name
@ -1250,7 +1277,7 @@ ifaceParam fname indents
end <- location
pure (n, PInfer (MkFC fname start end))
ifaceDecl : FileName -> IndentInfo -> SourceRule PDecl
ifaceDecl : FileName -> IndentInfo -> Rule PDecl
ifaceDecl fname indents
= do start <- location
vis <- visibility
@ -1271,7 +1298,7 @@ ifaceDecl fname indents
pure (PInterface (MkFC fname start end)
vis cons n params det dc (collectDefs (concat body)))
implDecl : FileName -> IndentInfo -> SourceRule PDecl
implDecl : FileName -> IndentInfo -> Rule PDecl
implDecl fname indents
= do start <- location
visOpts <- many (visOpt fname)
@ -1298,7 +1325,7 @@ implDecl fname indents
vis opts Single impls cons n params iname nusing
(map (collectDefs . concat) body))
fieldDecl : FileName -> IndentInfo -> SourceRule (List PField)
fieldDecl : FileName -> IndentInfo -> Rule (List PField)
fieldDecl fname indents
= do symbol "{"
commit
@ -1310,7 +1337,7 @@ fieldDecl fname indents
atEnd indents
pure fs
where
fieldBody : PiInfo PTerm -> SourceRule (List PField)
fieldBody : PiInfo PTerm -> Rule (List PField)
fieldBody p
= do start <- location
m <- multiplicity
@ -1322,7 +1349,7 @@ fieldDecl fname indents
end <- location
pure (map (\n => MkField (MkFC fname start end)
rig p n ty) ns)
recordParam : FileName -> IndentInfo -> SourceRule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam fname indents
= do symbol "("
start <- location
@ -1347,7 +1374,7 @@ recordParam fname indents
end <- location
pure [(n, top, Explicit, PInfer (MkFC fname start end))]
recordDecl : FileName -> IndentInfo -> SourceRule PDecl
recordDecl : FileName -> IndentInfo -> Rule PDecl
recordDecl fname indents
= do start <- location
vis <- visibility
@ -1362,13 +1389,13 @@ recordDecl fname indents
pure (PRecord (MkFC fname start end)
vis n params (fst dcflds) (concat (snd dcflds)))
where
ctor : IndentInfo -> SourceRule Name
ctor : IndentInfo -> Rule Name
ctor idt = do exactIdent "constructor"
n <- name
atEnd idt
pure n
claim : FileName -> IndentInfo -> SourceRule PDecl
claim : FileName -> IndentInfo -> Rule PDecl
claim fname indents
= do start <- location
visOpts <- many (visOpt fname)
@ -1380,14 +1407,14 @@ claim fname indents
end <- location
pure (PClaim (MkFC fname start end) rig vis opts cl)
definition : FileName -> IndentInfo -> SourceRule PDecl
definition : FileName -> IndentInfo -> Rule PDecl
definition fname indents
= do start <- location
nd <- clause 0 fname indents
end <- location
pure (PDef (MkFC fname start end) [nd])
fixDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
fixDecl : FileName -> IndentInfo -> Rule (List PDecl)
fixDecl fname indents
= do start <- location
fixity <- fix
@ -1397,7 +1424,7 @@ fixDecl fname indents
end <- location
pure (map (PFixity (MkFC fname start end) fixity (fromInteger prec)) ops)
directiveDecl : FileName -> IndentInfo -> SourceRule PDecl
directiveDecl : FileName -> IndentInfo -> Rule PDecl
directiveDecl fname indents
= do start <- location
(do d <- directive fname indents
@ -1411,7 +1438,7 @@ directiveDecl fname indents
pure (PReflect (MkFC fname start end) tm))
-- Declared at the top
-- topDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
-- topDecl : FileName -> IndentInfo -> Rule (List PDecl)
topDecl fname indents
= do d <- dataDecl fname indents
pure [d]
@ -1480,15 +1507,15 @@ collectDefs (d :: ds)
= d :: collectDefs ds
export
import_ : FileName -> IndentInfo -> SourceRule Import
import_ : FileName -> IndentInfo -> Rule Import
import_ fname indents
= do start <- location
keyword "import"
reexp <- option False (do keyword "public"
pure True)
ns <- nsIdent
ns <- namespacedIdent
nsAs <- option ns (do exactIdent "as"
nsIdent)
namespacedIdent)
end <- location
atEnd indents
pure (MkImport (MkFC fname start end) reexp ns nsAs)
@ -1499,7 +1526,7 @@ prog fname
= do start <- location
nspace <- option ["Main"]
(do keyword "module"
nsIdent)
namespacedIdent)
end <- location
imports <- block (import_ fname)
ds <- block (topDecl fname)
@ -1512,13 +1539,13 @@ progHdr fname
= do start <- location
nspace <- option ["Main"]
(do keyword "module"
nsIdent)
namespacedIdent)
end <- location
imports <- block (import_ fname)
pure (MkModule (MkFC fname start end)
nspace imports [])
parseMode : SourceRule REPLEval
parseMode : Rule REPLEval
parseMode
= do exactIdent "typecheck"
pure EvalTC
@ -1533,7 +1560,7 @@ parseMode
<|> do exactIdent "exec"
pure Execute
setVarOption : SourceRule REPLOpt
setVarOption : Rule REPLOpt
setVarOption
= do exactIdent "eval"
mode <- parseMode
@ -1545,7 +1572,7 @@ setVarOption
c <- unqualifiedName
pure (CG c)
setOption : Bool -> SourceRule REPLOpt
setOption : Bool -> Rule REPLOpt
setOption set
= do exactIdent "showimplicits"
pure (ShowImplicits set)
@ -1555,7 +1582,7 @@ setOption set
pure (ShowTypes set)
<|> if set then setVarOption else fatalError "Unrecognised option"
replCmd : List String -> SourceRule ()
replCmd : List String -> Rule ()
replCmd [] = fail "Unrecognised command"
replCmd (c :: cs)
= exactIdent c
@ -1563,7 +1590,7 @@ replCmd (c :: cs)
<|> replCmd cs
export
editCmd : SourceRule EditCmd
editCmd : Rule EditCmd
editCmd
= do replCmd ["typeat"]
line <- intLit
@ -1649,7 +1676,7 @@ data ParseCmd : Type where
ParseIdentCmd : String -> ParseCmd
CommandDefinition : Type
CommandDefinition = (List String, CmdArg, String, SourceRule REPLCmd)
CommandDefinition = (List String, CmdArg, String, Rule REPLCmd)
CommandTable : Type
CommandTable = List CommandDefinition
@ -1659,7 +1686,7 @@ extractNames (ParseREPLCmd names) = names
extractNames (ParseKeywordCmd keyword) = [keyword]
extractNames (ParseIdentCmd ident) = [ident]
runParseCmd : ParseCmd -> SourceRule ()
runParseCmd : ParseCmd -> Rule ()
runParseCmd (ParseREPLCmd names) = replCmd names
runParseCmd (ParseKeywordCmd keyword') = keyword keyword'
runParseCmd (ParseIdentCmd ident) = exactIdent ident
@ -1670,7 +1697,7 @@ noArgCmd parseCmd command doc = (names, NoArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1682,7 +1709,7 @@ nameArgCmd parseCmd command doc = (names, NameArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1695,7 +1722,7 @@ exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1708,7 +1735,7 @@ optArgCmd parseCmd command set doc = (names, OptionArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1721,7 +1748,7 @@ numberArgCmd parseCmd command doc = (names, NumberArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1734,7 +1761,7 @@ compileArgsCmd parseCmd command doc = (names, FileArg, doc, parse)
names : List String
names = extractNames parseCmd
parse : SourceRule REPLCmd
parse : Rule REPLCmd
parse = do
symbol ":"
runParseCmd parseCmd
@ -1770,11 +1797,11 @@ help = (["<expr>"], NoArg, "Evaluate an expression") ::
map (\ (names, args, text, _) =>
(map (":" ++) names, args, text)) parserCommandsForHelp
nonEmptyCommand : SourceRule REPLCmd
nonEmptyCommand : Rule REPLCmd
nonEmptyCommand =
choice (map (\ (_, _, _, parser) => parser) parserCommandsForHelp)
eval : SourceRule REPLCmd
eval : Rule REPLCmd
eval = do
tm <- expr pdef "(interactive)" init
pure (Eval tm)

4
src/Idris/ProcessIdr.idr
View File

@ -177,7 +177,7 @@ modTime fname
pure (cast t)
export
getParseErrorLoc : String -> ParseError -> FC
getParseErrorLoc : String -> ParseError Token -> FC
getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
getParseErrorLoc fname (LitFail (MkLitErr l c _)) = MkFC fname (l, 0) (l, 0)
@ -195,7 +195,7 @@ readHeader path
where
-- Stop at the first :, that's definitely not part of the header, to
-- save lexing the whole file unnecessarily
isColon : TokenData SourceToken -> Bool
isColon : TokenData Token -> Bool
isColon t
= case tok t of
Symbol ":" => True

7
src/Idris/REPL.idr
View File

@ -69,6 +69,7 @@ showInfo (n, idx, d)
show !(traverse getFullName (keys (refersTo d))))
coreLift $ putStrLn ("Refers to (runtime): " ++
show !(traverse getFullName (keys (refersToRuntime d))))
coreLift $ putStrLn ("Flags: " ++ show (flags d))
when (not (isNil (sizeChange d))) $
let scinfo = map (\s => show (fnCall s) ++ ": " ++
show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in
@ -398,7 +399,7 @@ processEdit (ExprSearch upd line name hints all)
if upd
then updateFile (proofSearch name res (integerToNat (cast (line - 1))))
else pure $ DisplayEdit [res]
[(n, nidx, PMDef pi [] (STerm tm) _ _)] =>
[(n, nidx, PMDef pi [] (STerm _ tm) _ _)] =>
case holeInfo pi of
NotHole => pure $ EditError "Not a searchable hole"
SolvedHole locs =>
@ -748,7 +749,7 @@ parseCmd : SourceEmptyRule (Maybe REPLCmd)
parseCmd = do c <- command; eoi; pure $ Just c
export
parseRepl : String -> Either ParseError (Maybe REPLCmd)
parseRepl : String -> Either (ParseError Token) (Maybe REPLCmd)
parseRepl inp
= case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd)
@ -819,6 +820,7 @@ mutual
prompt NormaliseAll = ""
prompt Execute = "[exec] "
export
handleMissing : MissedResult -> String
handleMissing (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs
handleMissing (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function"
@ -871,6 +873,7 @@ mutual
displayResult (OptionsSet opts) = printResult $ showSep "\n" $ map show opts
displayResult _ = pure ()
export
displayHelp : String
displayHelp =
showSep "\n" $ map cmdInfo help

39
src/Idris/REPLCommon.idr
View File

@ -11,6 +11,7 @@ import Idris.IDEMode.Commands
import public Idris.REPLOpts
import Idris.Syntax
import Data.List
-- Output informational messages, unless quiet flag is set
export
@ -74,6 +75,44 @@ emitError err
addOne : (Int, Int) -> (Int, Int)
addOne (l, c) = (l + 1, c + 1)
export
emitWarning : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
{auto s : Ref Syn SyntaxInfo} ->
Warning -> Core ()
emitWarning w
= do opts <- get ROpts
case idemode opts of
REPL _ =>
do msg <- displayWarning w
coreLift $ putStrLn msg
IDEMode i _ f =>
do msg <- pwarning w
case getWarningLoc w of
Nothing => iputStrLn msg
Just fc =>
send f (SExpList [SymbolAtom "warning",
SExpList [toSExp (file fc),
toSExp (addOne (startPos fc)),
toSExp (addOne (endPos fc)),
toSExp msg,
-- highlighting; currently blank
SExpList []],
toSExp i])
where
addOne : (Int, Int) -> (Int, Int)
addOne (l, c) = (l + 1, c + 1)
export
emitWarnings : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
{auto s : Ref Syn SyntaxInfo} ->
Core ()
emitWarnings
= do defs <- get Ctxt
traverse_ emitWarning (reverse (warnings defs))
put Ctxt (record { warnings = [] } defs)
getFCLine : FC -> Int
getFCLine fc = fst (startPos fc)

3
src/Idris/Resugar.idr
View File

@ -252,6 +252,9 @@ mutual
toPTerm p (Implicit fc True) = pure (PImplicit fc)
toPTerm p (Implicit fc False) = pure (PInfer fc)
toPTerm p (IWithUnambigNames fc ns rhs) =
PWithUnambigNames fc ns <$> toPTerm startPrec rhs
mkApp : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
PTerm -> List (FC, Maybe (Maybe Name), PTerm) -> Core PTerm

8
src/Idris/Syntax.idr
View File

@ -96,7 +96,8 @@ mutual
-- Debugging
PUnifyLog : FC -> Nat -> PTerm -> PTerm
-- TODO: 'with' disambiguation
-- with-disambiguation
PWithUnambigNames : FC -> List Name -> PTerm -> PTerm
public export
data PFieldUpdate : Type where
@ -493,6 +494,8 @@ mutual
= showPrec d rec ++ concatMap show fields
showPrec d (PRecordProjection fc fields)
= concatMap show fields
showPrec d (PWithUnambigNames fc ns rhs)
= "with " ++ show ns ++ " " ++ showPrec d rhs
public export
record IFaceInfo where
@ -776,6 +779,9 @@ mapPTermM f = goPTerm where
>>= f
goPTerm (PRecordProjection fc fields) =
f (PRecordProjection fc fields)
goPTerm (PWithUnambigNames fc ns rhs) =
PWithUnambigNames fc ns <$> goPTerm rhs
>>= f
goPFieldUpdate : PFieldUpdate -> Core PFieldUpdate
goPFieldUpdate (PSetField p t) = PSetField p <$> goPTerm t

27
src/Parser/Lexer/Common.idr
View File

@ -18,15 +18,13 @@ comment
-- There are multiple variants.
public export
data Flavour = Capitalised | AllowDashes | Normal
data Flavour = AllowDashes | Capitalised | Normal
export
isIdentStart : Flavour -> Char -> Bool
isIdentStart _ '_' = True
isIdentStart Capitalised x = isUpper x || x > chr 160
isIdentStart _ x = isAlpha x || x > chr 160
export
isIdentTrailing : Flavour -> Char -> Bool
isIdentTrailing AllowDashes '-' = True
isIdentTrailing _ '\'' = True
@ -45,3 +43,26 @@ ident : Flavour -> Lexer
ident flavour =
(pred $ isIdentStart flavour) <+>
(many . pred $ isIdentTrailing flavour)
export
isIdentNormal : String -> Bool
isIdentNormal = isIdent Normal
export
identNormal : Lexer
identNormal = ident Normal
export
identAllowDashes : Lexer
identAllowDashes = ident AllowDashes
namespaceIdent : Lexer
namespaceIdent = ident Capitalised <+> many (is '.' <+> ident Capitalised <+> expect (is '.'))
export
namespacedIdent : Lexer
namespacedIdent = namespaceIdent <+> opt (is '.' <+> identNormal)
export
spacesOrNewlines : Lexer
spacesOrNewlines = some (space <|> newline)

65
src/Parser/Lexer/Package.idr Normal file
View File

@ -0,0 +1,65 @@
module Parser.Lexer.Package
import public Parser.Lexer.Common
import public Text.Lexer
import public Text.Parser
import Data.List
import Data.Strings
import Data.String.Extra
import Utils.String
%default total
public export
data Token
= Comment String
| EndOfInput
| Equals
| DotSepIdent (List String)
| Separator
| Space
| StringLit String
public export
Show Token where
show (Comment str) = "Comment: " ++ str
show EndOfInput = "EndOfInput"
show Equals = "Equals"
show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep dsid
show Separator = "Separator"
show Space = "Space"
show (StringLit s) = "StringLit: " ++ s
equals : Lexer
equals = is '='
separator : Lexer
separator = is ','
rawTokens : TokenMap Token
rawTokens =
[ (equals, const Equals)
, (comment, Comment . drop 2)
, (namespacedIdent, DotSepIdent . splitNamespace)
, (identAllowDashes, DotSepIdent . pure)
, (separator, const Separator)
, (spacesOrNewlines, const Space)
, (stringLit, \s => StringLit (stripQuotes s))
]
where
splitNamespace : String -> List String
splitNamespace = Data.Strings.split (== '.')
export
lex : String -> Either (Int, Int, String) (List (TokenData Token))
lex str =
case lexTo (const False) rawTokens str of
(tokenData, (l, c, "")) =>
Right $ (filter (useful . tok) tokenData) ++ [MkToken l c EndOfInput]
(_, fail) => Left fail
where
useful : Token -> Bool
useful (Comment c) = False
useful Space = False
useful _ = True

115
src/Parser/Lexer/Source.idr
View File

@ -12,46 +12,50 @@ import Utils.String
%default total
public export
data SourceToken
= NSIdent (List String)
| HoleIdent String
| Literal Integer
| StrLit String
| CharLit String
data Token
-- Literals
= CharLit String
| DoubleLit Double
| IntegerLit Integer
| StringLit String
-- Identifiers
| HoleIdent String
| Ident String
| DotSepIdent (List String)
| RecordField String
| Symbol String
| Keyword String
| Unrecognised String
-- Comments
| Comment String
| DocComment String
-- Special
| CGDirective String
| RecordField String
| Pragma String
| EndInput
| Keyword String
| Pragma String
| Unrecognised String
export
Show SourceToken where
show (HoleIdent x) = "hole identifier " ++ x
show (Literal x) = "literal " ++ show x
show (StrLit x) = "string " ++ show x
Show Token where
-- Literals
show (CharLit x) = "character " ++ show x
show (DoubleLit x) = "double " ++ show x
show (IntegerLit x) = "literal " ++ show x
show (StringLit x) = "string " ++ show x
-- Identifiers
show (HoleIdent x) = "hole identifier " ++ x
show (Ident x) = "identifier " ++ x
show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (reverse xs)
show (RecordField x) = "record field " ++ x
show (Symbol x) = "symbol " ++ x
show (Keyword x) = x
show (Unrecognised x) = "Unrecognised " ++ x
-- Comments
show (Comment _) = "comment"
show (DocComment _) = "doc comment"
-- Special
show (CGDirective x) = "CGDirective " ++ x
show (RecordField x) = "record field " ++ x
show (Pragma x) = "pragma " ++ x
show EndInput = "end of input"
show (NSIdent [x]) = "identifier " ++ x
show (NSIdent xs) = "namespaced identifier " ++ dotSep (reverse xs)
where
dotSep : List String -> String
dotSep [] = ""
dotSep [x] = x
dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs]
show (Keyword x) = x
show (Pragma x) = "pragma " ++ x
show (Unrecognised x) = "Unrecognised " ++ x
mutual
||| The mutually defined functions represent different states in a
@ -102,29 +106,14 @@ blockComment = is '{' <+> is '-' <+> toEndComment 1
docComment : Lexer
docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')
export
isIdentNormal : String -> Bool
isIdentNormal = isIdent Normal
export
identNormal : Lexer
identNormal = ident Normal
export
identAllowDashes : Lexer
identAllowDashes = ident AllowDashes
holeIdent : Lexer
holeIdent = is '?' <+> ident Normal
nsIdent : Lexer
nsIdent = ident Capitalised <+> many (is '.' <+> ident Normal)
holeIdent = is '?' <+> identNormal
recField : Lexer
recField = is '.' <+> ident Normal
recField = is '.' <+> identNormal
pragma : Lexer
pragma = is '%' <+> ident Normal
pragma = is '%' <+> identNormal
doubleLit : Lexer
doubleLit
@ -142,7 +131,7 @@ cgDirective
is '}')
<|> many (isNot '\n'))
mkDirective : String -> SourceToken
mkDirective : String -> Token
mkDirective str = CGDirective (trim (substr 3 (length str) str))
-- Reserved words
@ -171,7 +160,6 @@ symbols
"(", ")", "{", "}", "[", "]", ",", ";", "_",
"`(", "`"]
export
isOpChar : Char -> Bool
isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
@ -205,7 +193,7 @@ fromOctLit str
Nothing => 0 -- can't happen if the literal lexed correctly
Just n => cast n
rawTokens : TokenMap SourceToken
rawTokens : TokenMap Token
rawTokens =
[(comment, Comment),
(blockComment, Comment),
@ -214,31 +202,30 @@ rawTokens =
(holeIdent, \x => HoleIdent (assert_total (strTail x)))] ++
map (\x => (exact x, Symbol)) symbols ++
[(doubleLit, \x => DoubleLit (cast x)),
(hexLit, \x => Literal (fromHexLit x)),
(octLit, \x => Literal (fromOctLit x)),
(digits, \x => Literal (cast x)),
(stringLit, \x => StrLit (stripQuotes x)),
(hexLit, \x => IntegerLit (fromHexLit x)),
(octLit, \x => IntegerLit (fromOctLit x)),
(digits, \x => IntegerLit (cast x)),
(stringLit, \x => StringLit (stripQuotes x)),
(charLit, \x => CharLit (stripQuotes x)),
(recField, \x => RecordField (assert_total $ strTail x)),
(nsIdent, parseNSIdent),
(ident Normal, parseIdent),
(namespacedIdent, parseNamespace),
(identNormal, parseIdent),
(pragma, \x => Pragma (assert_total $ strTail x)),
(space, Comment),
(validSymbol, Symbol),
(symbol, Unrecognised)]
where
parseNSIdent : String -> SourceToken
parseNSIdent = NSIdent . reverse . split (== '.')
parseIdent : String -> SourceToken
parseIdent x =
if x `elem` keywords
then Keyword x
else NSIdent [x]
parseIdent : String -> Token
parseIdent x = if x `elem` keywords then Keyword x
else Ident x
parseNamespace : String -> Token
parseNamespace ns = case Data.List.reverse . split (== '.') $ ns of
[ident] => parseIdent ident
ns => DotSepIdent ns
export
lexTo : (TokenData SourceToken -> Bool) ->
String -> Either (Int, Int, String) (List (TokenData SourceToken))
lexTo : (TokenData Token -> Bool) ->
String -> Either (Int, Int, String) (List (TokenData Token))
lexTo pred str
= case lexTo pred rawTokens str of
-- Add the EndInput token so that we'll have a line and column
@ -247,12 +234,12 @@ lexTo pred str
[MkToken l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData SourceToken -> Bool
notComment : TokenData Token -> Bool
notComment t = case tok t of
Comment _ => False
DocComment _ => False -- TODO!
_ => True
export
lex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
lex : String -> Either (Int, Int, String) (List (TokenData Token))
lex = lexTo (const False)

24
src/Parser/Package.idr Normal file
View File

@ -0,0 +1,24 @@
module Parser.Package
import public Parser.Lexer.Package
import public Parser.Rule.Package
import public Text.Lexer
import public Text.Parser
import public Parser.Support
import System.File
import Utils.Either
export
runParser : String -> Rule ty -> Either (ParseError Token) ty
runParser str p
= do toks <- mapError LexFail $ lex str
parsed <- mapError toGenericParsingError $ parse p toks
Right (fst parsed)
export
parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty)
parseFile fn p
= do Right str <- readFile fn
| Left err => pure (Left (FileFail err))
pure (runParser str p)

79
src/Parser/Rule/Package.idr Normal file
View File

@ -0,0 +1,79 @@
module Parser.Rule.Package
import public Parser.Lexer.Package
import public Parser.Rule.Common
import Data.List
%default total
public export
Rule : Type -> Type
Rule = Rule Token
public export
PackageEmptyRule : Type -> Type
PackageEmptyRule = EmptyRule Token
export
equals : Rule ()
equals = terminal "Expected equals"
(\x => case tok x of
Equals => Just ()
_ => Nothing)
export
eoi : Rule ()
eoi = terminal "Expected end of input"
(\x => case tok x of
EndOfInput => Just ()
_ => Nothing)
export
exactProperty : String -> Rule String
exactProperty p = terminal ("Expected property " ++ p)
(\x => case tok x of
DotSepIdent [p'] =>
if p == p' then Just p
else Nothing
_ => Nothing)
export
stringLit : Rule String
stringLit = terminal "Expected string"
(\x => case tok x of
StringLit str => Just str
_ => Nothing)
export
namespacedIdent : Rule (List String)
namespacedIdent = terminal "Expected namespaced identifier"
(\x => case tok x of
DotSepIdent nsid => Just $ reverse nsid
_ => Nothing)
export
moduleIdent : Rule (List String)
moduleIdent = terminal "Expected module identifier"
(\x => case tok x of
DotSepIdent m => Just $ reverse m
_ => Nothing)
export
packageName : Rule String
packageName = terminal "Expected package name"
(\x => case tok x of
DotSepIdent [str] =>
if isIdent AllowDashes str then Just str
else Nothing
_ => Nothing)
sep' : Rule ()
sep' = terminal "Expected separator"
(\x => case tok x of
Separator => Just ()
_ => Nothing)
export
sep : Rule t -> Rule (List t)
sep rule = sepBy1 sep' rule

99
src/Parser/Rule/Source.idr
View File

@ -9,12 +9,12 @@ import Core.TT
%default total
public export
SourceRule : Type -> Type
SourceRule = Rule SourceToken
Rule : Type -> Type
Rule = Rule Token
public export
SourceEmptyRule : Type -> Type
SourceEmptyRule = EmptyRule SourceToken
SourceEmptyRule = EmptyRule Token
export
eoi : SourceEmptyRule ()
@ -22,48 +22,48 @@ eoi
= do nextIs "Expected end of input" (isEOI . tok)
pure ()
where
isEOI : SourceToken -> Bool
isEOI : Token -> Bool
isEOI EndInput = True
isEOI _ = False
export
constant : SourceRule Constant
constant : Rule Constant
constant
= terminal "Expected constant"
(\x => case tok x of
Literal i => Just (BI i)
StrLit s => case escape s of
Nothing => Nothing
Just s' => Just (Str s')
CharLit c => case getCharLit c of
Nothing => Nothing
Just c' => Just (Ch c')
DoubleLit d => Just (Db d)
NSIdent ["Int"] => Just IntType
NSIdent ["Integer"] => Just IntegerType
NSIdent ["String"] => Just StringType
NSIdent ["Char"] => Just CharType
NSIdent ["Double"] => Just DoubleType
DoubleLit d => Just (Db d)
IntegerLit i => Just (BI i)
StringLit s => case escape s of
Nothing => Nothing
Just s' => Just (Str s')
Ident "Char" => Just CharType
Ident "Double" => Just DoubleType
Ident "Int" => Just IntType
Ident "Integer" => Just IntegerType
Ident "String" => Just StringType
_ => Nothing)
export
intLit : SourceRule Integer
intLit : Rule Integer
intLit
= terminal "Expected integer literal"
(\x => case tok x of
Literal i => Just i
IntegerLit i => Just i
_ => Nothing)
export
strLit : SourceRule String
strLit : Rule String
strLit
= terminal "Expected string literal"
(\x => case tok x of
StrLit s => Just s
StringLit s => Just s
_ => Nothing)
export
recField : SourceRule Name
recField : Rule Name
recField
= terminal "Expected record field"
(\x => case tok x of
@ -71,7 +71,7 @@ recField
_ => Nothing)
export
symbol : String -> SourceRule ()
symbol : String -> Rule ()
symbol req
= terminal ("Expected '" ++ req ++ "'")
(\x => case tok x of
@ -80,7 +80,7 @@ symbol req
_ => Nothing)
export
keyword : String -> SourceRule ()
keyword : String -> Rule ()
keyword req
= terminal ("Expected '" ++ req ++ "'")
(\x => case tok x of
@ -89,16 +89,16 @@ keyword req
_ => Nothing)
export
exactIdent : String -> SourceRule ()
exactIdent : String -> Rule ()
exactIdent req
= terminal ("Expected " ++ req)
(\x => case tok x of
NSIdent [s] => if s == req then Just ()
else Nothing
Ident s => if s == req then Just ()
else Nothing
_ => Nothing)
export
pragma : String -> SourceRule ()
pragma : String -> Rule ()
pragma n =
terminal ("Expected pragma " ++ n)
(\x => case tok x of
@ -109,7 +109,7 @@ pragma n =
_ => Nothing)
export
operator : SourceRule Name
operator : Rule Name
operator
= terminal "Expected operator"
(\x => case tok x of
@ -119,27 +119,28 @@ operator
else Just (UN s)
_ => Nothing)
identPart : SourceRule String
identPart : Rule String
identPart
= terminal "Expected name"
(\x => case tok x of
NSIdent [str] => Just str
Ident str => Just str
_ => Nothing)
export
nsIdent : SourceRule (List String)
nsIdent
namespacedIdent : Rule (List String)
namespacedIdent
= terminal "Expected namespaced name"
(\x => case tok x of
NSIdent ns => Just ns
DotSepIdent ns => Just ns
Ident i => Just $ [i]
_ => Nothing)
export
unqualifiedName : SourceRule String
unqualifiedName : Rule String
unqualifiedName = identPart
export
holeName : SourceRule String
holeName : Rule String
holeName
= terminal "Expected hole name"
(\x => case tok x of
@ -152,17 +153,17 @@ reservedNames
"Lazy", "Inf", "Force", "Delay"]
export
name : SourceRule Name
name : Rule Name
name = opNonNS <|> do
ns <- nsIdent
ns <- namespacedIdent
opNS ns <|> nameNS ns
where
reserved : String -> Bool
reserved n = n `elem` reservedNames
nameNS : List String -> Grammar (TokenData SourceToken) False Name
nameNS : List String -> SourceEmptyRule Name
nameNS [] = pure $ UN "IMPOSSIBLE"
nameNS [x] =
nameNS [x] =
if reserved x
then fail $ "can't use reserved name " ++ x
else pure $ UN x
@ -171,10 +172,10 @@ name = opNonNS <|> do
then fail $ "can't use reserved name " ++ x
else pure $ NS xs (UN x)
opNonNS : SourceRule Name
opNonNS : Rule Name
opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")"
opNS : List String -> SourceRule Name
opNS : List String -> Rule Name
opNS ns = do
symbol ".("
n <- (operator <|> recField)
@ -238,7 +239,7 @@ checkValid (AfterPos x) c = if c >= x
checkValid EndOfBlock c = fail "End of block"
||| Any token which indicates the end of a statement/block
isTerminator : SourceToken -> Bool
isTerminator : Token -> Bool
isTerminator (Symbol ",") = True
isTerminator (Symbol "]") = True
isTerminator (Symbol ";") = True
@ -318,8 +319,8 @@ terminator valid laststart
afterDedent EndOfBlock col = pure EndOfBlock
-- Parse an entry in a block
blockEntry : ValidIndent -> (IndentInfo -> SourceRule ty) ->
SourceRule (ty, ValidIndent)
blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->
Rule (ty, ValidIndent)
blockEntry valid rule
= do col <- column
checkValid valid col
@ -327,7 +328,7 @@ blockEntry valid rule
valid' <- terminator valid col
pure (p, valid')
blockEntries : ValidIndent -> (IndentInfo -> SourceRule ty) ->
blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
SourceEmptyRule (List ty)
blockEntries valid rule
= do eoi; pure []
@ -337,7 +338,7 @@ blockEntries valid rule
<|> pure []
export
block : (IndentInfo -> SourceRule ty) -> SourceEmptyRule (List ty)
block : (IndentInfo -> Rule ty) -> SourceEmptyRule (List ty)
block item
= do symbol "{"
commit
@ -353,7 +354,7 @@ block item
||| by curly braces). `rule` is a function of the actual indentation
||| level.
export
blockAfter : Int -> (IndentInfo -> SourceRule ty) -> SourceEmptyRule (List ty)
blockAfter : Int -> (IndentInfo -> Rule ty) -> SourceEmptyRule (List ty)
blockAfter mincol item
= do symbol "{"
commit
@ -366,7 +367,7 @@ blockAfter mincol item
else blockEntries (AtPos col) item
export
blockWithOptHeaderAfter : Int -> (IndentInfo -> SourceRule hd) -> (IndentInfo -> SourceRule ty) -> SourceEmptyRule (Maybe hd, List ty)
blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> SourceEmptyRule (Maybe hd, List ty)
blockWithOptHeaderAfter {ty} mincol header item
= do symbol "{"
commit
@ -379,7 +380,7 @@ blockWithOptHeaderAfter {ty} mincol header item
ps <- blockEntries (AtPos col) item
pure (map fst hidt, ps)
where
restOfBlock : Maybe (hd, ValidIndent) -> SourceRule (Maybe hd, List ty)
restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)
restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
symbol "}"
pure (Just h, ps)
@ -388,7 +389,7 @@ blockWithOptHeaderAfter {ty} mincol header item
pure (Nothing, ps)
export
nonEmptyBlock : (IndentInfo -> SourceRule ty) -> SourceRule (List ty)
nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
nonEmptyBlock item
= do symbol "{"
commit

14
src/Parser/Source.idr
View File

@ -3,8 +3,6 @@ module Parser.Source
import public Parser.Lexer.Source
import public Parser.Rule.Source
import public Parser.Unlit
import public Text.Lexer
import public Text.Parser
import System.File
import Utils.Either
@ -13,21 +11,21 @@ import Utils.Either
export
runParserTo : {e : _} ->
Maybe LiterateStyle -> (TokenData SourceToken -> Bool) ->
String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
Maybe LiterateStyle -> (TokenData Token -> Bool) ->
String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty
runParserTo lit pred str p
= do str <- mapError LitFail $ unlit lit str
toks <- mapError LexFail $ lexTo pred str
parsed <- mapError mapParseError $ parse p toks
parsed <- mapError toGenericParsingError $ parse p toks
Right (fst parsed)
export
runParser : {e : _} ->
Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
Maybe LiterateStyle -> String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty
runParser lit = runParserTo lit (const False)
export
parseFile : (fn : String) -> SourceRule ty -> IO (Either ParseError ty)
export covering
parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty)
parseFile fn p
= do Right str <- readFile fn
| Left err => pure (Left (FileFail err))

18
src/Parser/Support.idr
View File

@ -1,6 +1,5 @@
module Parser.Support
import public Parser.Lexer.Source
import public Text.Lexer
import public Text.Parser
@ -13,13 +12,14 @@ import System.File
%default total
public export
data ParseError = ParseFail String (Maybe (Int, Int)) (List SourceToken)
| LexFail (Int, Int, String)
| FileFail FileError
| LitFail LiterateError
data ParseError tok
= ParseFail String (Maybe (Int, Int)) (List tok)
| LexFail (Int, Int, String)
| FileFail FileError
| LitFail LiterateError
export
Show ParseError where
Show tok => Show (ParseError tok) where
show (ParseFail err loc toks)
= "Parse error: " ++ err ++ " (next tokens: "
++ show (take 10 toks) ++ ")"
@ -31,9 +31,9 @@ Show ParseError where
= "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str
export
mapParseError : ParseError (TokenData SourceToken) -> ParseError
mapParseError (Error err []) = ParseFail err Nothing []
mapParseError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts))
toGenericParsingError : ParsingError (TokenData token) -> ParseError token
toGenericParsingError (Error err []) = ParseFail err Nothing []
toGenericParsingError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts))
export
hex : Char -> Maybe Int

30
src/TTImp/Elab/Ambiguity.idr
View File

@ -15,6 +15,7 @@ import TTImp.TTImp
import Data.Bool.Extra
import Data.List
import Data.StringMap
%default covering
@ -49,17 +50,26 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
ci <- fromCharName
let prims = mapMaybe id [fi, si, ci]
let primApp = isPrimName prims x
ns <- lookupCtxtName x (gamma defs)
ns' <- filterM visible ns
case ns' of
[] => do log 10 $ "Failed to find " ++ show orig
pure orig
[nalt] =>
do log 10 $ "Only one " ++ show (fst nalt)
pure $ mkAlt primApp est nalt
nalts => pure $ IAlternative fc (uniqType fi si ci x args)
(map (mkAlt primApp est) nalts)
case lookupUN (userNameRoot x) (unambiguousNames est) of
Just xr => do
log 10 $ "unambiguous: " ++ show (fst xr)
pure $ mkAlt primApp est xr
Nothing => do
ns <- lookupCtxtName x (gamma defs)
ns' <- filterM visible ns
case ns' of
[] => do log 10 $ "Failed to find " ++ show orig
pure orig
[nalt] =>
do log 10 $ "Only one " ++ show (fst nalt)
pure $ mkAlt primApp est nalt
nalts => pure $ IAlternative fc (uniqType fi si ci x args)
(map (mkAlt primApp est) nalts)
where
lookupUN : Maybe String -> StringMap a -> Maybe a
lookupUN Nothing _ = Nothing
lookupUN (Just n) sm = lookup n sm
visible : (Name, Int, GlobalDef) -> Core Bool
visible (n, i, def)
= do let NS ns x = fullname def

9
src/TTImp/Elab/App.idr
View File

@ -649,11 +649,12 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
isPrimName (p :: ps) fn
= dropNS fn == p || isPrimName ps fn
boundSafe : Constant -> Bool
boundSafe (BI x) = abs x < 100 -- only do this for relatively small bounds.
boundSafe : Constant -> ElabMode -> Bool
boundSafe _ (InLHS _) = True -- always need to expand on LHS
boundSafe (BI x) _ = abs x < 100 -- only do this for relatively small bounds.
-- Once it gets too big, we might be making the term
-- bigger than it would have been without evaluating!
boundSafe _ = True
boundSafe _ _ = True
-- If the term is an application of a primitive conversion (fromInteger etc)
-- and it's applied to a constant, fully normalise the term.
@ -665,7 +666,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
= if isPrimName prims !(getFullName n)
then case reverse expargs of
(IPrimVal _ c :: _) =>
if boundSafe c
if boundSafe c (elabMode elabinfo)
then do defs <- get Ctxt
tm <- normalise defs env (fst res)
pure (tm, snd res)

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