~cypheon/Idris2

2d3f113833e04aa4bf069c3eea6b66b3099e4266 — Johann Rudloff a month ago 91be635 + 18f9c54
Merge branch 'lambdalift-opt'
256 files changed, 6470 insertions(+), 1576 deletions(-)

M .github/workflows/ci-windows.yml
M .gitignore
M CHANGELOG.md
M INSTALL.md
M Makefile
M README.md
M config.mk
A docs/source/backends/backend-cookbook.rst
M docs/source/backends/custom.rst
M docs/source/backends/index.rst
A docs/source/reference/builtins.rst
M docs/source/reference/index.rst
M docs/source/updates/updates.rst
M idris2api.ipkg
M libs/base/Control/App.idr
A libs/base/Control/Applicative/Const.idr
M libs/base/Control/Monad/Identity.idr
A libs/base/Data/Bifoldable.idr
M libs/base/Data/Bool.idr
A libs/base/Data/Contravariant.idr
M libs/base/Data/Fin.idr
M libs/base/Data/Maybe.idr
M libs/base/Data/Morphisms.idr
M libs/base/Data/Primitives/Views.idr
M libs/base/Data/These.idr
M libs/base/System.idr
M libs/base/System/Directory.idr
M libs/base/System/File.idr
M libs/base/base.ipkg
M libs/contrib/Control/Linear/LIO.idr
M libs/contrib/Data/Fin/Extra.idr
M libs/contrib/Data/String/Extra.idr
M libs/contrib/Data/Validated.idr
M libs/contrib/Language/JSON/Data.idr
M libs/contrib/Language/JSON/String/Tokens.idr
A libs/contrib/System/Directory/Tree.idr
M libs/contrib/System/Path.idr
M libs/contrib/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr
M libs/contrib/contrib.ipkg
M libs/network/Control/Linear/Network.idr
M libs/network/Network/FFI.idr
M libs/network/Network/Socket/Raw.idr
M libs/prelude/Prelude/Cast.idr
M libs/prelude/Prelude/Interfaces.idr
M libs/prelude/Prelude/Ops.idr
M libs/prelude/Prelude/Show.idr
M libs/prelude/Prelude/Types.idr
M libs/test/Test/Golden.idr
M nix/package.nix
M nix/test.nix
M src/Compiler/Common.idr
M src/Compiler/CompileExpr.idr
M src/Compiler/ES/Node.idr
M src/Compiler/LambdaLift.idr
A src/Compiler/RefC/CC.idr
M src/Compiler/RefC/RefC.idr
M src/Compiler/Scheme/Chez.idr
M src/Compiler/Scheme/Racket.idr
M src/Core/Binary.idr
M src/Core/Context.idr
M src/Core/Core.idr
M src/Core/Env.idr
M src/Core/Metadata.idr
M src/Core/Name/Namespace.idr
M src/Core/Normalise.idr
M src/Core/TT.idr
M src/Core/TTC.idr
M src/Core/UnifyState.idr
M src/Idris/CommandLine.idr
M src/Idris/Desugar.idr
M src/Idris/DocString.idr
M src/Idris/Driver.idr
M src/Idris/Error.idr
M src/Idris/IDEMode/CaseSplit.idr
M src/Idris/IDEMode/Commands.idr
M src/Idris/ModTree.idr
M src/Idris/Package.idr
A src/Idris/Package/Init.idr
A src/Idris/Package/Types.idr
M src/Idris/Parser.idr
M src/Idris/Pretty.idr
A src/Idris/Pretty/Render.idr
M src/Idris/ProcessIdr.idr
M src/Idris/REPL.idr
R src/Idris/{REPLCommon.idr => REPL/Common.idr}
A src/Idris/REPL/FuzzySearch.idr
R src/Idris/{REPLOpts.idr => REPL/Opts.idr}
M src/Idris/Resugar.idr
M src/Idris/SetOptions.idr
M src/Idris/Syntax.idr
M src/Libraries/Data/ANameMap.idr
M src/Libraries/Data/List/Extra.idr
M src/Libraries/Data/NameMap.idr
A src/Libraries/Data/PosMap.idr
M src/Libraries/Data/StringMap.idr
A src/Libraries/System/Directory/Tree.idr
M src/Libraries/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr
M src/Libraries/Utils/Binary.idr
M src/Libraries/Utils/Path.idr
M src/Parser/Lexer/Package.idr
M src/Parser/Lexer/Source.idr
M src/TTImp/Elab.idr
M src/TTImp/Elab/App.idr
M src/TTImp/Elab/Case.idr
M src/TTImp/Elab/Hole.idr
M src/TTImp/Elab/ImplicitBind.idr
M src/TTImp/Elab/Quote.idr
M src/TTImp/Parser.idr
A src/TTImp/ProcessBuiltin.idr
M src/TTImp/ProcessDecls.idr
M src/TTImp/ProcessDef.idr
M src/TTImp/ProcessParams.idr
M src/TTImp/ProcessRecord.idr
M src/TTImp/Reflect.idr
M src/TTImp/TTImp.idr
M src/TTImp/Unelab.idr
M support/c/idris_net.c
M support/c/idris_net.h
M support/chez/support.ss
M support/gambit/support.scm
M support/js/support_system_directory.js
M support/js/support_system_file.js
M support/racket/support.rkt
M tests/Main.idr
M tests/base/data_bits001/expected
M tests/base/system_file001/expected
M tests/chez/chez001/expected
M tests/chez/chez002/expected
M tests/chez/chez003/expected
M tests/chez/chez004/expected
M tests/chez/chez005/expected
M tests/chez/chez006/expected
M tests/chez/chez007/expected
M tests/chez/chez008/expected
M tests/chez/chez009/expected
M tests/chez/chez010/expected
M tests/chez/chez011/expected
M tests/chez/chez012/expected
M tests/chez/chez013/expected
M tests/chez/chez014/Echo.idr
M tests/chez/chez014/expected
M tests/chez/chez015/expected
M tests/chez/chez016/expected
M tests/chez/chez016/run
M tests/chez/chez017/expected.in
M tests/chez/chez018/expected
M tests/chez/chez019/expected
M tests/chez/chez020/expected
M tests/chez/chez021/expected
M tests/chez/chez022/expected
M tests/chez/chez023/expected
M tests/chez/chez024/expected
M tests/chez/chez025/expected
M tests/chez/chez027/expected
M tests/chez/chez028/expected
M tests/chez/chez029/expected
M tests/chez/chez032/expected
A tests/codegen/builtin001/CatCases.idr
A tests/codegen/builtin001/Main.idr
A tests/codegen/builtin001/expected
A tests/codegen/builtin001/run
M tests/codegen/con001/expected
M tests/codegen/con001/run
A tests/contrib/json_001/CharEncoding.idr
A tests/contrib/json_001/expected
A tests/contrib/json_001/input
A tests/contrib/json_001/run
M tests/idris2/basic029/Params.idr
M tests/idris2/basic044/expected
M tests/idris2/basic044/run
M tests/idris2/basic055/expected
M tests/idris2/basic056/expected
A tests/idris2/basic059/MultiClaim.idr
A tests/idris2/basic059/expected
A tests/idris2/basic059/run
A tests/idris2/builtin001/Test.idr
A tests/idris2/builtin001/expected
A tests/idris2/builtin001/input
A tests/idris2/builtin001/run
A tests/idris2/builtin002/Test.idr
A tests/idris2/builtin002/expected
A tests/idris2/builtin002/input
A tests/idris2/builtin002/run
A tests/idris2/builtin003/Test.idr
A tests/idris2/builtin003/expected
A tests/idris2/builtin003/input
A tests/idris2/builtin003/run
A tests/idris2/builtin004/Test.idr
A tests/idris2/builtin004/expected
A tests/idris2/builtin004/input
A tests/idris2/builtin004/run
M tests/idris2/docs001/expected
M tests/idris2/error007/CongErr.idr
M tests/idris2/error007/expected
M tests/idris2/error011/expected
A tests/idris2/error017/Issue962-case.idr
A tests/idris2/error017/Issue962.idr
A tests/idris2/error017/expected
A tests/idris2/error017/run
M tests/idris2/interactive019/expected
A tests/idris2/interactive030/expected
A tests/idris2/interactive030/input
A tests/idris2/interactive030/run
M tests/idris2/interpreter007/expected
A tests/idris2/params002/ParamsPrint.idr
A tests/idris2/params002/expected
A tests/idris2/params002/input
A tests/idris2/params002/run
M tests/idris2/pkg002/run
A tests/idris2/pkg007/A/Path/Of/Dires/First.idr
A tests/idris2/pkg007/A/Path/Of/Dires/Second.idr
A tests/idris2/pkg007/Another/Fourth.idr
A tests/idris2/pkg007/Another/One/Third.idr
A tests/idris2/pkg007/expected
A tests/idris2/pkg007/input
A tests/idris2/pkg007/input2
A tests/idris2/pkg007/run
A tests/idris2/pkg007/src/And/A/Proof.idr
A tests/idris2/pkg007/src/Yet/Another/Path.idr
A tests/idris2/pkg008/Bar.idr
A tests/idris2/pkg008/Foo.idr
A tests/idris2/pkg008/bar.ipkg
A tests/idris2/pkg008/expected
A tests/idris2/pkg008/foo.ipkg
A tests/idris2/pkg008/run
A tests/idris2/pkg009/expected
A tests/idris2/pkg009/run
A tests/idris2/pkg009/testpkg/Main.idr
A tests/idris2/pkg009/testpkg/testpkg.ipkg
A tests/idris2/pretty001/Issue1328A.idr
A tests/idris2/pretty001/expected
A tests/idris2/pretty001/input
A tests/idris2/pretty001/run
M tests/idris2/reflection001/expected
M tests/idris2/reg023/expected
M tests/node/node001/expected
M tests/node/node002/expected
M tests/node/node003/expected
M tests/node/node004/expected
M tests/node/node005/expected
M tests/node/node006/expected
M tests/node/node007/expected
M tests/node/node008/expected
M tests/node/node009/expected
M tests/node/node011/expected
M tests/node/node012/expected
M tests/node/node015/expected
M tests/node/node017/expected.in
M tests/node/node018/expected
M tests/node/node019/expected
M tests/node/node021/expected
M tests/node/node022/expected
M tests/node/node023/expected
M tests/node/node024/expected
M tests/node/node025/expected
M tests/tests.ipkg
M .github/workflows/ci-windows.yml => .github/workflows/ci-windows.yml +1 -1
@@ 45,4 45,4 @@ jobs:
        run: |
          scheme --version
      - name: Bootstrap and install
        run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make bootstrap && make install"
        run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make bootstrap && make bootstrap-test && make install"

M .gitignore => .gitignore +2 -0
@@ 9,6 9,8 @@

/build

/lib

idris2docs_venv
/docs/build


M CHANGELOG.md => CHANGELOG.md +7 -12
@@ 13,6 13,13 @@ REPL/IDE mode changes:
* Added `:search` command, which searches for functions by type
* `:load`/`:l` and `:cd` commands now only accept paths surrounded by double quotes

Syntax changes:

* The syntax for parameter blocks has been updated. It now allows to declare
  implicit parameters and give multiplicities for parameters. The old syntax
  is still available for compatibility purposes but will be removed in the
  future.

Compiler changes:

* Racket codegen now always uses `blodwen-sleep` instead of `idris2_sleep` in


@@ 39,18 46,6 @@ Other changes:
* Added an environment variable `IDRIS2_PACKAGE_PATH` for extending where to
  look for packages.

Other changes:

* The `version` field in `.ipkg` files is now used. Packages are installed into
  a directory which includes its version number, and dependencies can have
  version number ranges using `<=`, `<`, `>=`, `>`, `==` to express version
  constraints. Version numbers must be in the form of integers, separated by
  dots (e.g. `1.0`, `0.3.0`, `3.1.4.1.5` etc)
* Idris now looks in the current working directory, under a subdirectory
  `depends` for local installations of packages before looking globally.
* Added an environment variable `IDRIS2_PACKAGE_PATH` for extending where to
  look for packages.

Changes since Idris 2 v0.2.1
----------------------------


M INSTALL.md => INSTALL.md +4 -3
@@ 32,7 32,7 @@ of `make` in the following steps.
**NOTE**: If you're running macOS on Apple Silicon (arm64) you may need to run
"`arch -x86_64 make ...`" instead of `make` in the following steps.

### 1: Set the PREFIX
### 1: Set installation target directory

- Change the `PREFIX` in `config.mk`. The default is to install in
  `$HOME/.idris2`


@@ 95,8 95,9 @@ code generator. To do so, once everything is successfully installed, type:

- `make install-api`

The API will only work if you've completed the self-hosting step, step 3, since
the intermediate code versions need to be consistent throughout.
The API will only work if you've completed the self-hosting step, step 4, since
the intermediate code versions need to be consistent throughout. Otherwise, you
will get an `Error in TTC: TTC data is in an older format` error.

### Troubleshooting


M Makefile => Makefile +49 -43
@@ 5,7 5,7 @@ export IDRIS2_BOOT ?= idris2

# Idris 2 executable we're building
NAME = idris2
TARGETDIR = build/exec
TARGETDIR = ${CURDIR}/build/exec
TARGET = ${TARGETDIR}/${NAME}

MAJOR=0


@@ 22,6 22,7 @@ ifeq ($(shell git status >/dev/null 2>&1; echo $$?), 0)
endif

export IDRIS2_VERSION := ${MAJOR}.${MINOR}.${PATCH}
NAME_VERSION := ${NAME}-${IDRIS2_VERSION}
IDRIS2_SUPPORT := libidris2_support${SHLIB_SUFFIX}
IDRIS2_APP_IPKG := idris2.ipkg
IDRIS2_LIB_IPKG := idris2api.ipkg


@@ 37,13 38,10 @@ else
	SEP := :
endif

# Library and data paths for test
IDRIS2_TEST_LIBS ?= ${IDRIS2_CURDIR}/lib
IDRIS2_TEST_DATA ?= ${IDRIS2_CURDIR}/support
TEST_PREFIX ?= ${IDRIS2_CURDIR}/build/env

# Library and data paths for bootstrap-test
IDRIS2_BOOT_TEST_LIBS := ${IDRIS2_CURDIR}/bootstrap/${NAME}-${IDRIS2_VERSION}/lib
IDRIS2_BOOT_TEST_DATA := ${IDRIS2_CURDIR}/bootstrap/${NAME}-${IDRIS2_VERSION}/support
IDRIS2_BOOT_PREFIX := ${IDRIS2_CURDIR}/bootstrap

# These are the library path in the build dir to be used during build
export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS2_CURDIR}/libs/base/build/ttc${SEP}${IDRIS2_CURDIR}/libs/contrib/build/ttc${SEP}${IDRIS2_CURDIR}/libs/network/build/ttc${SEP}${IDRIS2_CURDIR}/libs/test/build/ttc"


@@ 51,19 49,15 @@ export IDRIS2_BOOT_PATH := "${IDRIS2_CURDIR}/libs/prelude/build/ttc${SEP}${IDRIS
export SCHEME


.PHONY: all idris2-exec ${TARGET} testbin support support-lib support-clean clean distclean FORCE
.PHONY: all idris2-exec testenv testenv-clean support support-clean clean FORCE

all: support ${TARGET} support-lib libs
all: support ${TARGET} libs

idris2-exec: ${TARGET}

${TARGET}: src/IdrisPaths.idr
	${IDRIS2_BOOT} --build ${IDRIS2_APP_IPKG}

support-lib:
	mkdir -p lib
	install support/c/${IDRIS2_SUPPORT} lib

# We use FORCE to always rebuild IdrisPath so that the git SHA1 info is always up to date
src/IdrisPaths.idr: FORCE
	echo '-- @generated' > src/IdrisPaths.idr


@@ 74,31 68,44 @@ src/IdrisPaths.idr: FORCE
FORCE:

prelude:
	${MAKE} -C libs/prelude IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/prelude IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

base: prelude
	${MAKE} -C libs/base IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/base IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

network: prelude
	${MAKE} -C libs/network IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/network IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

contrib: base
	${MAKE} -C libs/contrib IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/contrib IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

test-lib: contrib
	${MAKE} -C libs/test IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/test IDRIS2=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

libs : prelude base contrib network test-lib

testbin:
	@${MAKE} -C tests testbin IDRIS2=../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_DATA=${IDRIS2_TEST_DATA} IDRIS2_LIBS=${IDRIS2_TEST_LIBS}
${TEST_PREFIX}/${NAME_VERSION} :
	${MAKE} install-support PREFIX=${TEST_PREFIX}
	ln -s ${IDRIS2_CURDIR}/libs/prelude/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/prelude-${IDRIS2_VERSION}
	ln -s ${IDRIS2_CURDIR}/libs/base/build/ttc    ${TEST_PREFIX}/${NAME_VERSION}/base-${IDRIS2_VERSION}
	ln -s ${IDRIS2_CURDIR}/libs/test/build/ttc    ${TEST_PREFIX}/${NAME_VERSION}/test-${IDRIS2_VERSION}
	ln -s ${IDRIS2_CURDIR}/libs/contrib/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/contrib-${IDRIS2_VERSION}
	ln -s ${IDRIS2_CURDIR}/libs/network/build/ttc ${TEST_PREFIX}/${NAME_VERSION}/network-${IDRIS2_VERSION}

testenv:
	@${MAKE} ${TEST_PREFIX}/${NAME_VERSION}
	@${MAKE} -C tests testbin IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}

test: testbin
testenv-clean:
	$(RM) -r ${TEST_PREFIX}/${NAME_VERSION}

test: testenv
	@echo
	@echo "NOTE: \`${MAKE} test\` does not rebuild Idris or the libraries packaged with it; to do that run \`${MAKE}\`"
	@if [ ! -x "${TARGET}" ]; then echo "ERROR: Missing IDRIS2 executable. Cannot run tests!\n"; exit 1; fi
	@echo
	@${MAKE} -C tests only=$(only) IDRIS2=../../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_DATA=${IDRIS2_TEST_DATA} IDRIS2_LIBS=${IDRIS2_TEST_LIBS}
	@${MAKE} -C tests only=$(only) IDRIS2=${TARGET} IDRIS2_PREFIX=${TEST_PREFIX}


support:
	@${MAKE} -C support/c


@@ 115,12 122,11 @@ clean-libs:
	${MAKE} -C libs/network clean
	${MAKE} -C libs/test clean

clean: clean-libs support-clean
clean: clean-libs support-clean testenv-clean
	-${IDRIS2_BOOT} --clean ${IDRIS2_APP_IPKG}
	$(RM) src/IdrisPaths.idr
	${MAKE} -C tests clean
	$(RM) -r build
	$(RM) -r lib

install: install-idris2 install-support install-libs



@@ 134,55 140,55 @@ ifeq ($(OS), windows)
	-install ${TARGET}.cmd ${PREFIX}/bin
endif
	mkdir -p ${PREFIX}/lib/
	install lib/${IDRIS2_SUPPORT} ${PREFIX}/lib
	install support/c/${IDRIS2_SUPPORT} ${PREFIX}/lib
	mkdir -p ${PREFIX}/bin/${NAME}_app
	install ${TARGETDIR}/${NAME}_app/* ${PREFIX}/bin/${NAME}_app

install-support:
	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/racket
	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/gambit
	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/js
	install support/chez/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
	install support/racket/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/racket
	install support/gambit/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/gambit
	install support/js/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/js
	mkdir -p ${PREFIX}/${NAME_VERSION}/support/chez
	mkdir -p ${PREFIX}/${NAME_VERSION}/support/racket
	mkdir -p ${PREFIX}/${NAME_VERSION}/support/gambit
	mkdir -p ${PREFIX}/${NAME_VERSION}/support/js
	install support/chez/* ${PREFIX}/${NAME_VERSION}/support/chez
	install support/racket/* ${PREFIX}/${NAME_VERSION}/support/racket
	install support/gambit/* ${PREFIX}/${NAME_VERSION}/support/gambit
	install support/js/* ${PREFIX}/${NAME_VERSION}/support/js
	@${MAKE} -C support/c install
	@${MAKE} -C support/refc install

install-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/contrib install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/network install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/test install IDRIS2?=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${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/contrib install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/network install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
	${MAKE} -C libs/test  install IDRIS2?=${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}


.PHONY: bootstrap bootstrap-build bootstrap-racket bootstrap-racket-build bootstrap-test bootstrap-clean

# Bootstrapping using SCHEME
bootstrap: support support-lib
bootstrap: support
	cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
	sed 's/libidris2_support.so/${IDRIS2_SUPPORT}/g; s|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' \
	sed 's/libidris2_support.so/${IDRIS2_SUPPORT}/g; s|__PREFIX__|${IDRIS2_BOOT_PREFIX}|g' \
		bootstrap/idris2_app/idris2.ss \
		> bootstrap/idris2_app/idris2-boot.ss
	$(SHELL) ./bootstrap-stage1-chez.sh
	IDRIS2_CG="chez" $(SHELL) ./bootstrap-stage2.sh

# Bootstrapping using racket
bootstrap-racket: support support-lib
bootstrap-racket: support
	cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
	sed 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' \
	sed 's|__PREFIX__|${IDRIS2_BOOT_PREFIX}|g' \
		bootstrap/idris2_app/idris2.rkt \
		> bootstrap/idris2_app/idris2-boot.rkt
	$(SHELL) ./bootstrap-stage1-racket.sh
	IDRIS2_CG="racket" $(SHELL) ./bootstrap-stage2.sh

bootstrap-test:
	$(MAKE) test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_TEST_DATA=${IDRIS2_BOOT_TEST_DATA} IDRIS2_TEST_LIBS=${IDRIS2_BOOT_TEST_LIBS}
	$(MAKE) test INTERACTIVE='' IDRIS2_PREFIX=${IDRIS2_BOOT_PREFIX}

bootstrap-clean:
	$(RM) -r bootstrap/bin bootstrap/lib bootstrap/idris2-${IDRIS2_VERSION}
	$(RM) -r bootstrap/bin bootstrap/lib bootstrap/${NAME_VERSION}
	$(RM) bootstrap/idris2boot* bootstrap/idris2_app/idris2-boot.* bootstrap/idris2_app/${IDRIS2_SUPPORT}



M README.md => README.md +5 -6
@@ 2,12 2,10 @@ Idris 2
=======

[![Documentation Status](https://readthedocs.org/projects/idris2/badge/?version=latest)](https://idris2.readthedocs.io/en/latest/?badge=latest)
[![Windows Status](https://github.com/idris-lang/Idris2/workflows/Windows/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Windows")
[![Ubuntu Status](https://github.com/idris-lang/Idris2/workflows/Ubuntu/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Ubuntu")
[![Ubuntu Racket Status](https://github.com/idris-lang/Idris2/workflows/Ubuntu%20Racket/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Ubuntu+Racket")
[![MacOS Status](https://github.com/idris-lang/Idris2/workflows/macOS/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"macOS")
[![API Status](https://github.com/idris-lang/Idris2/workflows/API/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"API")
[![Nix Status](https://github.com/idris-lang/Idris2/workflows/Nix/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Nix")
[![Windows Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-windows.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-windows.yml)
[![Ubuntu Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-ubuntu-combined.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-ubuntu-combined.yml)
[![MacOS Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-macos-combined.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-macos-combined.yml)
[![Nix Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-nix.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-nix.yml)

[Idris 2](https://idris-lang.org/) is a purely functional programming language
with first class types.


@@ 45,6 43,7 @@ exceptions. The most notable user visible differences, which might cause Idris
  Notably, elaborator reflection will exist, but most likely in a slightly
  different form because the internal details of the elaborator are different.
+ The `Prelude` is much smaller (and easier to replace with an alternative).
  Command-line option `--no-prelude` can be used to not implicitly import `Prelude`.
+ `let x = val in e` no longer computes with `x` in `e`, instead being
  essentially equivalent to `(\x => e) val`. This is to make the
  behaviour of `let` consistent in the presence of `case` and `with` (where

M config.mk => config.mk +1 -0
@@ 1,5 1,6 @@
##### Options which a user might set before building go here #####

# Where to install idris2 binaries and libraries
PREFIX ?= $(HOME)/.idris2

# For Windows targets. Set to 1 to support Windows 7.

A docs/source/backends/backend-cookbook.rst => docs/source/backends/backend-cookbook.rst +762 -0
@@ 0,0 1,762 @@
Custom backend cookbook
=======================

This document addresses the details on how to implement a custom code generation
backend for the Idris compiler.

This part has no insights about how to implement the dependently typed bits.
For that part of the compiler Edwin Brady gave lectures at SPLV20_ which are
available online.

The architecture of the Idris2 compiler makes it easy to implement a custom code
generation back-end.

The way to extend Idris with new back-ends is to use it as a library.
The module ``Idris.Driver`` exports the function ``mainWithCodegens``,
that takes a list of ``(String, Codegen)``, starting idris with these codegens
in addition to the built-in ones.
The first codegen in the list will be set as the default codegen.

Anyone who is interested in implementing a custom back-end needs to answer the
following questions:

- Which Intermediate Representation (IR) should be consumed by the custom back-end?
- How to represent primitive values defined by the ``Core.TT.Constant`` type?
- How to represent Algebraic Data Types?
- How to implement special values?
- How to implement primitive operations?
- How to compile IR expressions?
- How to compile Definitions?
- How to implement Foreign Function Interface?
- How to compile modules?
- How to embed code snippets?
- What should the runtime system support?

First of all, we should know that Idris2 is not an optimizing compiler.
Currently its focus is only to compile dependently typed functional code
in a timely manner.
Its main purpose is to check if the given program is correct in a dependently
typed setting and generate code in form of a lambda-calculus like IR where
higher-order functions are present.
Idris has 3 intermediate representations for code generation.
At every level we get a simpler representation, closer to machine code, but it
should be stressed that all the aggressive code optimizations should happen in
the custom back-ends.
The quality and readability of the generated back-end code is on the shoulders
of the implementor of the back-end. Idris erases type information, in the IRs as
it compiles to scheme by default, and there is no need to keep the type
information around.
With this in mind let's answer the questions above.

The architecture of an Idris back-end
-------------------------------------

Idris compiles its dependently typed front-end language into a representation
which is called ``Compile.TT.Term`` .
This data type has a few constructors and it represents a dependently typed
term.
This ``Term`` is transformed to ``Core.CompileExpr.CExp`` which has more
constructors than ``Term`` and it is a very similar construct to a lambda
calculus with let bindings, structured and tagged data representation,
primitive operations, external operations, and case expressions.
The ``CExp`` is closer in the compiling process to code generation.

The custom code generation back-end gets
a context of definitions,
a template directory and an an output directory,
a ``Core.TT.ClosedTerm`` to compile and a path to an output file.

.. code-block:: idris

   compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String)
           -> ClosedTerm -> (outfile : String) -> Core (Maybe String)
   compile defs tmpDir outputDir term file = ?

The ``ClosedTerm`` is a special ``Term`` where the list of the unbound
variables is empty.
This technicality is not important for the code generation of the custom
back-end as the back-end needs to call the ``getCompileData`` function
which produces the ``Compiler.Common.CompileData`` record.

The ``CompileData`` contains:

- A main expression that will be the entry point for the program in ``CExp``
- A list of ``Core.CompileExpr.NamedDef``
- A list of lambda-lifted definitions ``Compiler.LambdaLift.LiftedDef``
- A list of ``Compiler.ANF.ANFDef``
- A list of ``Compiler.VMCode.VMDef`` definitions

These lists contain:

- Functions
- Top-level data definitions
- Runtime crashes which represent unfilled holes,
  explicit calls by the user to ``idris_crash``,
  and unreachable branches in case trees
- Foreign call constructs

The job of the custom code generation back-end is to transform one of the phase
encoded definitions (``NamedDef``, ``LiftedDef``, ``CExp``, ``ANF``, or ``VM``)
into the intermediate representation of the code generator.
It can then run optimizations and generate some form of executable.
In summary, the code generator has to understand how to represent tagged data
and function applications (even if the function application is partial), how
to handle let expressions, how to implement and invoke primitive operations,
how to handle ``Erased`` arguments, and how to do runtime crashes.

The implementor of the custom back-end should pick the closest Idris IR which
fits to the abstraction of the technology that is aimed to compile to.
The implementor should also consider how to transform the simple main expression
which is represented in CExp.
As Idris does not focus on memory management and threading. The custom back-end
should model these concepts for the program that is compiled.
One possible approach is to target a fairly high level language and reuse as
much as possible from it for the custom back-end.
Another possibility is to implement a runtime that is capable of handling memory
management and threading.

Which Intermediate Representation (IR) should be consumed by the custom back-end?
---------------------------------------------------------------------------------

Now lets turn our attention to the different intermediate representations (IRs)
that Idris provides.
When the ``getCompiledData`` function is invoked with the ``Phase`` parameter
it will produce a ``CompileData`` record, which will contain lists of top-level
definitions that needs to be compiled. These are:

- ``NamedDef``
- ``LiftedDef``
- ``ANFDef``
- ``VMDef``

The question to answer here is: Which one should be picked?
Which one fits to the custom back-end?

How to represent primitive values defined by the ``Core.TT.Constant`` type?
---------------------------------------------------------------------------

After one selects the IR to be used during code generation, the next question
to answer is how primitive types should be represented in the back-end.
Idris has the following primitive types:

- ``Int``
- ``Integer`` (arbitrary precision)
- ``Bits(8/16/32/64)``
- ``Char``
- ``String``
- ``Double``
- ``WorldVal`` (token for IO computations)

And as Idris allows pattern matching on types all the primitive types have
their primitive counterpart for describing a type:

- ``IntType``
- ``IntegerType``
- ``Bits(8/16/32/64)Type``
- ``StringType``
- ``CharType``
- ``DoubleType``
- ``WorldType``

The representation of these primitive types should be a well-thought out
design decision as it affects many parts of the code generation, such as
conversion from the back-end values when FFI is involved, big part of the
data during the runtime is represented in these forms.
Representation of primitive types affect the possible optimisation techniques,
and they also affect the memory management and garbage collection.

There are two special primitive types: String and World.

**String**

As its name suggest this type represent a string of characters. As mentioned in
`Primitive FFI Types <https://idris2.readthedocs.io/en/latest/ffi/ffi.html#primitive-ffi-types>`_,
Strings are encoded in UTF-8.

It is not always clear who is responsible for freeing up a ``String`` created by
a component other than the Idris runtime. Strings created in Idris will
always have value, unlike possible String representation of the host technology,
where for example NULL pointer can be a value, which can not happen on the Idris side.
This creates constraints on the possible representations of the Strings in the
custom back-end and diverging from the Idris representation is not a good idea.
The best approach here is to build a conversion layer between the string
representation of the custom back-end and the runtime.

**World**

In pure functional programming, causality needs to be represented whenever we
want to maintain the order in which subexpressions are executed.
In Idris a token is used to chain IO function calls.
This is an abstract notion about the state of the world. For example this
information could be the information that the runtime needs for bookkeeping
of the running program.

The ``WorldVal`` value in Idris programs is accessed via the ``primIO``
construction which leads us to the ``PrimIO`` module.
Let's see the relevant snippets:

.. code-block:: idris

   data IORes : Type -> Type where
        MkIORes : (result : a) -> (1 x : %World) -> IORes a

   fromPrim : (1 fn : (1 x : %World) -> IORes a) -> IO a
   fromPrim op = MkIO op

   primIO : HasIO io => (1 fn : (1 x : %World) -> IORes a) -> io a
   primIO op = liftIO (fromPrim op)

The world value is referenced as ``%World`` in Idris.
It is created by the runtime when the program starts.
Its content is changed by the custom runtime.
More precisely, the World is created when the ``WorldVal`` is evaluated during
the execution of the program.
This can happen when the program gets initialized or when an ``unsafePerformIO``
function is executed.

How to represent Algebraic Data Types?
--------------------------------------

In Idris there are two different ways to define a data type: tagged unions are
introduced using the ``data`` keyword while structs are declared via the
``record`` keyword.
Declaring a ``record`` amounts to defining a named collection of fields.
Let's see examples for both:

.. code-block:: idris

   data Either a b
     = Left  a
     | Right b

.. code-block:: idris

   record Pair a b
     constructor MkPair
     fst : a
     snd : b

Idris offers not only algebraic data types but also indexed families. These
are tagged union where different constructors may have different return types.
Here is ``Vect`` an example of a data type which is an indexed family
corresponding to a linked-list whose length is known at compile time.
It has one index (of type ``Nat``) representing the length of the list (the
value of this index is therefore different for the ``[]`` and ``(::)``
constructors) and a parameter (of type ``Type``) corresponding to the type
of values stored in the list.

.. code-block:: idris

   data Vect : (size : Nat) -> Type -> Type where
     Nil  : Vect 0 a                         -- empty list: size is 0
     (::) : a -> Vect n a -> Vect (1 + n) a  -- extending a list of size n: size is 1+n

Both data and record are compiled to constructors in the intermediate
representations. Two examples of such Constructors are
``Core.CompileExpr.CExp.CCon`` and ``Core.CompileExpr.CDef.MkCon``.

Compiling the ``Either`` data type will produce three constructor definitions
in the IR:

- One for the ``Either`` type itself, with the arity of two.
  Arity tells how many parameters of the constructor should have.
  Two is reasonable in this case as the original Idris ``Either`` type has
  two parameters.
- One for the ``Left`` constructor with arity of three.
  Three may be surprising, as the constructor only has one argument in Idris,
  but we should keep in mind the type parameters for the data type too.
- One for the ``Right`` constructor with arity of three.

In the IR constructors have unique names. For efficiency reasons,
Idris assigns a unique integer tag to each data constructors so that constructor
matching is reduced to comparisons of integers instead of strings.
In the ``Either`` example above ``Left`` gets tag 0 and ``Right`` gets tag 1.

Constructors can be considered structured information: a name
together with parameters.
The custom back-end needs to decide how to represent such data.
For example using ``Dict`` in Python, ``JSON`` in JavaScript, etc.
The most important aspect to consider is that these structured values
are heap related values, which should be created and stored dynamically.
If there is an easy way to map in the host technology, the memory management
for these values could be inherited. If not, then the host technology is
responsible for implementing an appropriate memory management.
For example ``RefC`` is a C backend that implements its own memory management
based on reference counting.

How to implement special values?
--------------------------------

Apart from the data constructors there are two special kind of values present
in the Idris IRs: type constructors and ``Erased``.

Type constructors
~~~~~~~~~~~~~~~~~

Type and data constructors that are not relevant for the program's runtime
behaviour may be used at compile butand will be erased from the intermediate
representation.

However some type constructors need to be kept around even at runtime
because pattern matching on types is allowed in Idris:

.. code-block:: idris

   notId : {a : Type} -> a -> a
   notId {a=Int} x = x + 1
   notId x = x

Here we can pattern match on ``a`` and ensure that ``notId`` behaves differently
on ``Int`` than all the other types.
This will generate an IR that will contain a ``Case`` expression with two
branches:
one ``Alt`` matching on the ``Int`` type constructor
and a default for the non-``Int`` matching part of the ``notId`` function.

This is not that special: ``Type`` is a bit like an infinite data type that
contains all of the types a user may ever declare or use.
This can be handled in the back-end and host language using the same mechanisms
that were mobilised to deal with data constructors.
The reason for using the same approach is that in dependently typed languages,
the same language is used to form both type and value level expressions.
Compilation of type level terms will be the same as that of value level terms.
This is one of the things that make dependently typed abstraction elegant.

``Erased``
~~~~~~~~~~

The other kind of special value is ``Erased``.
This is generated by the Idris compiler and part of the IR if the original value
is only needed during the type elaboration process. For example:

.. code-block:: idris

   data Subset : (type : Type)
              -> (pred : type -> Type)
              -> Type
     where
       Element : (value : type)
              -> (0 prf : pred value)
              -> Subset type pred

Because ``prf`` has quantity ``0``, it is guaranteed to be erased during
compilation and thus not present at runtime.
Therefore ``prf`` will be represented as ``Erased`` in the IR.
The custom back-end needs to represent this value too as any other data value,
as it could occur in place of normal values.
The simplest approach is to implement it as a special data constructor and let
the host technology provided optimizations take care of its removal.

How to implement primitive operations?
--------------------------------------

Primitive operations are defined in the module ``Core.TT.PrimFn``.
The constructors of this data type represent the primitive operations that
the custom back-end needs to implement.
These primitive operations can be grouped as:

- Arithmetic operations (``Add``, ``Sub``, ``Mul``, ``Div``, ``Mod``, ``Neg``)
- Bit operations (``ShiftL``, ``ShiftR``, ``BAnd``, ``BOr``, ``BXor``)
- Comparison operations (``LT``, ``LTE``, ``EQ``, ``GTE``, ``GT``)
- String operations
  (``Length``, ``Head``, ``Tail``, ``Index``, ``Cons``, ``Append``,
  ``Reverse``, ``Substr``)
- Double precision floating point operations
  (``Exp``, ``Log``, ``Sin``, ``Cos``, ``Tan``, ``ASin``, ``ACos``, ``ATan``,
  ``Sqrt``, ``Floor``, ``Ceiling``)
- Casting of numeric and string values
- An unsafe  cast operation ``BelieveMe``
- A ``Crash`` operation taking a type and a string and creating a value at that
  type by raising an error.

BelieveMe
~~~~~~~~~

The primitive ``believe_me`` is an unsafe cast that allows users to bypass the
typechecker when they know something to be true even though it cannot be proven.

For instance, assuming that Idris' primitives are correctly implemented, it
should be true that if a boolean equality test on two ``Int`` ``i`` and ``j``
returns ``True`` then ``i`` and ``j`` are equal.
Such a theorem can be implemented by using ``believe_me`` to caset ``Refl``
(the constructor for proofs of a propositional equality) from ``i === i`` to
``i === j``. In this case, it should be safe to implement

Boxing
~~~~~~

Idris assumes that the back-end representation of the data is not strongly typed
and that all the data type have the same kind of representation.
This could introduce a constraint on the representation of the primitives and
constructor represented data types.
One possible solution is that the custom back-end should represent primitive
data types the same way it does constructors, using special tags.
This is called boxing.

Official backends represent primitive data types as boxed ones.
- RefC: Boxes the primitives, which makes them easy to put on the heap.
- Scheme: Prints the values that are a ``Constant`` as Scheme literals.

How to compile top-level definitions?
-------------------------------------

As mentioned earlier, Idris has 4 different IRs that are available in
the ``CompileData`` record: ``Named``, ``LambdaLifted``, ``ANF``, and ``VMDef``.
When assembling the ``CompileData`` we have to tell the Idris compiler which
level we are interested in.
The ``CompileData`` contains lists of definitions that can be considered as top
level definitions that the custom back-end need to generate functions for.

There are four types of top-level definitions that the code generation back-end
needs to support:

- Function
- Constructor
- Foreign call
- Error

**Function** contains a lambda calculus like expression.

**Constructor** represents a data or a type constructor, and it should
be implemented as a function creating the corresponding data structure
in the custom back-end.

A top-level **foreign call** defines an entry point for calling functions
implemented outside the Idris program under compilation.
The Foreign construction contains a list of Strings which are the snippets
defined by the programmer, the type of the arguments and the return type of
the foreign function. The custom back-end should generate a wrapper function.
More on this on the 'How to do do FFI' section.

A top-level **error** definition represents holes in Idris programs, uses of
``idris_crash``, or unreachable branches in a case tree.
Users may want to execute incomplete programs for testing purposes which is
fine as long as we never actually need the value of any of the holes.
Library writers may want to raise an exception if an unrecoverable error has
happened.
Finally, Idris compiles the unreachable branches of a case tree to runtime
error as it is dead code anyway.


How to compile IR expressions?
------------------------------

The custom back-end should decide which intermediate representation
is used as a starting point. The result of the transformation should be
expressions and functions of the host technology.

Definitions in ``ANF`` and ``Lifted`` are represented as a tree like expression,
where control flow is based on the ``Let`` and ``Case`` expressions.

Case expressions
~~~~~~~~~~~~~~~~

There are two types of case expressions,
one for matching and branching on primitive values such as ``Int``,
and the second one is matching and branching on constructor values.
The two types of case expressions will have two different representation for
alternatives of the cases. These are ``ConstCase`` (for matching on constant
values) and ``ConCase`` (for matching on constructors).

Matching on constructors can be implemented as matching on their tags or,
less efficiently, as matching on the name of the constructor. In both cases
a match should bind the values of the constructor's arguments to variables
in the body of the matching branch.
This can be implemented in various ways depending on the host technology:
switch expressions, case with pattern matching, or if-then-else chains.

When pattern matching binds variables, the number of arguments can be different
from the arity of the constructor defined in top-level definitions and in
``GlobalDef``. This is because all the arguments are kept around at typechecking
time, but the code generator for the case tree removes the ones which are marked
as erased. The code generator of the custom back-end also needs to remove the
erased arguments in the constructor implementation.
In ``GlobalDef``, ``eraseArg`` contains this information, which can be used to
extract the number of arguments which needs to be kept around.


Creating values
~~~~~~~~~~~~~~~

Values can be created in two ways.

If the value is a primitive value, it will be handed to the back-end as
a ``PrimVal``. It should be compiled to a constant in the host language
following the  design decisions made in
the 'How to represent primitive values?' section.

If it is a structured value (i.e. a ``Con``) it should be compiled to a function
in the host language which creates a dynamic value. Design decisions made for
'How to represent constructor values?' is going to have effect here.

Function calls
~~~~~~~~~~~~~~

There are four types of function calls:
- Saturated function calls (all the arguments are there)
- Under-applied function calls (some arguments are missing)
- Primitive function calls (necessarily saturated, ``PrimFn`` constructor)
- Foreign Function calls (referred to by its name)

The ``ANF`` and ``Lifted`` intermediate representations support under-applied
function calls (using the ``UnderApp`` constructor in both IR).
The custom back-end needs to support partial application of functions and
creating closures in the host technology.
This is not a problem with back-ends like Scheme where we get the partial
application of a function for free.
But if the host language does not have this tool in its toolbox, the custom
back-end needs to simulate closures.
One possible solution is to manufacture a closure as a special object storing
the function and the values it is currently applied to and wait until all the
necessary arguments have been received before evaluating it.
The same approach is needed if the ``VMCode`` IR was chosen for code generation.

Let bindings
~~~~~~~~~~~~

Both the ``ANF`` and ``Lifted`` intermediate representations have a
``Let`` construct that lets users assign values to local variables.
These two IRs differ in their representation of bound variables.

``Lifted`` is a type family indexed by the ``List Name`` of local variables
in scope. A variable is represented using ``LLocal``, a constructor that
stores a ``Nat`` together with a proof that it points to a valid name in
the local scope.

``ANF`` is a lower level representation where this kind of guarantees are not
present anymore. A local variable is represented using the ``AV`` constructor
which stores an ``AVar`` whose definition we include below.
The ``ALocal`` constructor stores an ``Int`` that corresponds to the ``Nat``
we would have seen in ``Lifted``.
The ``ANull`` constructor refers to an erased variable and its representation
in the host language will depend on the design choices made in
the 'How to represent ``Erased`` values' section.

.. .code-block:: idri
  data AVar : Type where
     ALocal : Int -> AVar
     ANull : AVar

VMDef specificities
~~~~~~~~~~~~~~~~~~~

``VMDef`` is meant to be the closest IR to machine code.
In ``VMDef``, all the definitions have been compiled to instructions for a small
virtual machine with registers and closures.

Instead of ``Let`` expressions, there only are ``ASSIGN`` statements
at this level.

Instead of ``Case`` expressions binding variables when they successfully match
on a data constructor, ``CASE`` picks a branch based on the constructor itself.
An extra operation called ``PROJECT`` is introduced to explicitly extract a
constructor's argument based on their position.

There are no ``App`` or ``UnderApp``. Both are replaced by ``APPLY`` which
applies only one value and creates a closure from the application. For erased
values the operation ``NULL`` assigns an empty/null value for the register.

How to implement the Foreign Function Interface?
------------------------------------------------

The Foreign Function Interface (FFI) plays a big role in running Idris programs.
The primitive operations which are mentioned above are functions for
manipulating values and those functions aren't meant for complex interaction
with the runtime system.
Many of the primitive types can be thought of as abstract types provided via
``external`` and foreign functions to manipulate them.

The responsibility of the custom back-end and the host technology is
to represent these computations the operationally correct way.
The design decisions with respect to representing primitive types in the host
technology will inevitably have effects on the design of the FFI.

Foreign Types
~~~~~~~~~~~~~

Originally Idris had an official back-end implementation in C. Even though
this has changed, the names in the types for the FFI kept their C prefix.
The ``Core.CompileExpr.CFType`` contains the following definitions, many of
them one-to-one mapping from the corresponding primitive type, but some of
them needs explanation.

The foreign types are:

- ``CFUnit``
- ``CFInt``
- ``CFUnsigned(8/16/32/64)``
- ``CFString``
- ``CFDouble``
- ``CFChar``
- ``CFFun`` of type  ``CFType -> CFType -> CFType``
  Callbacks can be registered in the host technology via parameters that have
  CFFun type. The back-end should be able to handle functions that are
  defined in Idris side and compiled to the host technology. If the custom
  back-end supports higher order functions then it should
  be used to implement the support for this kind of FFI type.
- ``CFIORes`` of type ``CFType -> CFType``
  Any ``PrimIO`` defined computation will have this extra layer.
  Pure functions shouldn't have any observable IO effect on the program state
  in the host technology implemented runtime.
  NOTE: ``IORes`` is also used when callback functions are registered in the
  host technology.
- ``CFWorld``
  Represents the current state of the world. This should refer to a token that
  is passed around between function calls.
  The implementation of the World value should contain back-end
  specific values and information about the state of the Idris runtime.
- ``CFStruct`` of type ``String -> List (String, CFType) -> CFType`` is the
  foreign type associated with the ``System.FFI.Struct``.
  It represents a C like structure in the custom back-end.
  ``prim__getField`` and ``prim__setField`` primitives should be implemented
  to support this CFType.
- ``CFUser`` of type ``Name -> List CFType -> CFType``
  Types defined with [external] are represented with ``CFUser``. For example
  ``data MyType : Type where [external]`` will be represented as
  ``CFUser Module.MyType []``
- ``CFBuffer``
  Foreign type defined for ``Data.Buffer``.
  Although this is an external type, Idris builds on a random access buffer.
- ``CFPtr`` The ``Ptr t`` and ``AnyPtr`` are compiled to ``CFPtr``
  Any complex structured data that can not be represented as a simple primitive
  can use this CFPtr to keep track where the value is used.
  In Idris ``Ptr t`` is defined as external type.
- ``CFGCPtr`` The ``GCPtr t`` and ``GCAnyPtr`` are compiled to ``CFGCPtr``.
  ``GCPtr`` is inferred from a Ptr value calling the ``onCollect`` function and
  has a special property. The ``onCollect`` attaches a finalizer for the pointer
  which should run when the pointer is freed.

Examples
~~~~~~~~

Let's step back and look into how this is represented at the Idris source level.
The simplest form of a definition involving the FFI a function definition with
a ``%foreign`` pragma. The pragma is passed a list of strings corresponding to
a mapping from backends to names for the foreign calls. For instance:

.. .code-block:: idris

  %foreign "C:add,libsmallc"
  prim__add : Int -> Int -> Int

this function should be translated by the C back end as a call to the ``add``
function defined in the ``smallc.c`` file. In the FFI, ``Int`` is translated to
``CFInt``. The back-end assumes that the data representation specified in the
library file correspond to that of normal Idris values.

We can also define ``external`` types like in the following examples:

.. .code-block:: idris

  data ThreadID : Type where [external]

  %foreign "scheme:blodwen-thread"
  prim__fork : (1 prog : PrimIO ()) -> PrimIO ThreadID

Here ``ThreadID`` is defined as an external type and this type will be
represented as ``CFUser "ThreadID" []`` internally. The value which is
created by the scheme runtime will be considered as a black box.

The type of ``prim__fork``, once translated as a foreign type, is
``[%World -> IORes Unit, %World] -> IORes Main.ThreadID``
Here we see that the ``%World`` is added to the IO computations.
The ``%World`` parameter is always the last in the argument list.

For the FFI functions, the type information and the user defined string can
be found in the top-level definitions.
The custom back-end should use the definitions to generate wrapper code,
which should convert the types that are described by the ``CFType`` to the
types that the function in the ``%foreign`` directive needs..

How to compile modules?
-----------------------

The Idris compiler generates intermediate files for modules, the content of
the files are neither part of ``Lifted``, ``ANF``, nor ``VMCode``.
Because of this, when the compilation pipeline enters the stage of code
generation, all the information will be in one instance of the ``CompileData``
record and the custom code generator back-end can process them as it would
see the whole program.

The custom back-end has the option to introduce some hierarchy for the functions
in different namespaces and organize some module structure to let the host
technology process the bits and pieces in different sized chunks.
However, this feature is not in the scope of the Idris compiler.

It is worth noting that modules can be mutually recursive in Idris.
So a direct compilation of Idris modules to modules in the host language
may be unsuccessful.

How to embed code snippets?
---------------------------

A possible motivation for implementing a custom back-end for Idris is to
generate code that is meant to be used in a larger project. This project
may be bound to another language that has many useful librarie  but could
benefit from relying on Idris' strong type system in places.

When writing a code generator for this purpose, the interoperability of the
host technology and Idris based on the Foreign Interface can be inconvenient.
In this situation, the need to embed code of the host technology arises
naturally. Elaboration can be an answer for that.

Elaboration is a typechecking time code generation technique.
It relies on the ``Elab`` monad to write scripts that can interact with the
typechecking machinery to generate Idris code in ``Core.TT``.

When code snippets need to be embedded a custom library should be provided
with the custom back-end to turn the valid code snippets into their
representation in ``Core.TT``.

What should the runtime system support?
---------------------------------------

As a summary, a custom back-end for the Idris compiler should create an environment
in the host technology that is able to run Idris programs. As Idris is part of
the family of functional programming languages, its computation model is based
on graph reduction. Programs represented as simple graphs in the memory are based
on the closure creation mechanism during evaluation. Closure creation exist even
on the lowest levels of IRs. For that reason any runtime in
any host technology needs to support some kind of representation of closures
and be able to store them on the heap, thus the responsibility of memory management
falls on the lap of the implementor of the custom back-end. If the host technology
has memory management, the problem is not difficult. It is also likely
that storing closures can be easily implemented via the tools of the host technology.

Although it is not clear how much functionality a back-end should support.
Tools from the Scheme back-end are brought into the Idris world via external types and primitive operations
around them. This is a good practice and gives the community the ability to focus on
the implementation of a quick compiler for a dependently typed language.
One of these hidden features is the concurrency primitives. These are part of the
different libraries that could be part of the compiler or part of the
contribution package. If the threading model is different for the host technology
that the Idris default back-end inherits currently from the Scheme technology it could be a bigger
piece of work.

IO in Idris is implemented using an abstract ``%World`` value, which serves as token for
functions that operate interactively with the World through simple calls to the
underlying runtime system. The entry point of the program is the main function, which
has the type of the IO unit, such as ``main : IO ()``. This means that every
program which runs, starts its part of some IO computation. Under the hood this is
implemented via the creation of the ``%World`` abstract value, and invoking the main
function, which is compiled to pass the abstract %World value for IO related
foreign or external operations.

There is an operation called ``unsafePerformIO`` in the ``PrimIO`` module.
The type signature of ``unsafePerformIO`` tells us that it is capable of
evaluating an ``IO`` computation in a pure context.
Under the hood it is run in exactly the same way the ``main`` function is.
It manufactures a fresh ``%World`` token and passes it to the ``IO`` computations.
This leads to a design decision: How to
represent the state of the World, and how to
represent the world that is instantiated for the sake of the ``unsafePerformIO`` operation via the
``unsafeCreateWorld``? Both the mechanisms of ``main`` and ``unsafeCreateWorld``
use the ``%MkWorld`` constructor, which will be compiled to ``WorldVal`` and
its type to ``WorldType``, which means the implementation of the runtime
is responsible for creating the abstraction around the World. Implementation of an
abstract World value could be based on a singleton pattern, where we can have
just one world, or we could have more than one world, resulting in parallel
universes for ``unsafePerformIO``.

.. _SPLV20: https://www.youtube.com/playlist?list=PLmYPUe8PWHKqBRJfwBr4qga7WIs7r60Ql
.. _Elaboration: https://github.com/stefan-hoeck/idris2-elab-util/blob/main/src/Doc/Index.md

M docs/source/backends/custom.rst => docs/source/backends/custom.rst +2 -2
@@ 11,8 11,8 @@ codegen in the list will be set as the default codegen.
Getting started
===============

To use Idris 2 as a library you need to install it with (at the top level of the
Idris2 repo)
To use Idris 2 as a library you need a self-hosting installation and
then install the `idris2api` library (at the top level of the Idris2 repo)

::


M docs/source/backends/index.rst => docs/source/backends/index.rst +1 -0
@@ 63,6 63,7 @@ or via the `IDRIS2_CG` environment variable.
   javascript
   refc
   custom
   backend-cookbook

There are also external code generators that aren't part of the main Idris 2
repository and can be found on Idris 2 wiki:

A docs/source/reference/builtins.rst => docs/source/reference/builtins.rst +72 -0
@@ 0,0 1,72 @@
********
Builtins
********

.. role:: idris(code)
    :language: idris

Idris2 supports an optimised runtime representation of some types,
using the ``%builtin`` pragma.
For now only ``Nat``-like types has been implemented.

``%builtin Natural``
====================

I suggest having a look at the source for ``Nat`` (in ``Prelude.Types``) before reading this section.

The ``%builtin Natural`` pragma converts recursive/unary representations of natural numbers
into primitive ``Integer`` representations.
This massively reduces the memory usage and offers a small speed improvement,
for example with the unary representation ``the Nat 1000`` would take up about 2000 * 8 bytes
(1000 for the tag, 1000 for the pointers) whereas the ``Integer`` representation takes about 8 to 16 bytes.

Here's an example:

.. code-block:: idris

    data Nat
        = Z
        | S Nat
    
    %builtin Natural Nat

Note that the order of the constructors doesn't matter.
Furthermore this pragma supports GADTs
so long as any extra arguments are erased.

For example:

.. code-block:: idris
    
    data Fin : Nat -> Type where
        FZ : Fin (S k)
        FS : Fin k -> Fin (S k)
    
    %builtin Natural Fin

works because the ``k`` is always erased.

This doesn't work if the argument to the ``S``-like constructor
is ``Inf`` (sometime known as ``CoNat``) as these can be infinite
or is ``Lazy`` as it wouldn't preserve laziness semantics.

During codegen any occurance of ``Nat`` will be converted to the faster ``Integer`` implementation.
Here are the specifics for the conversion:

``Z`` => ``0``

``S k`` => ``1 + k``

.. code-block:: idris

    case k of
        Z => zexp
        S k' => sexp
    
=>

.. code-block:: idris

    case k of
        0 => zexp
        _ => let k' = k - 1 in sexp
\ No newline at end of file

M docs/source/reference/index.rst => docs/source/reference/index.rst +1 -0
@@ 21,3 21,4 @@ This is a placeholder, to get set up with readthedocs.
   records
   literate
   overloadedlit
   builtins

M docs/source/updates/updates.rst => docs/source/updates/updates.rst +3 -2
@@ 858,8 858,9 @@ Chez Scheme target

The default code generator is, for the moment, `Chez Scheme
<https://www.scheme.com/>`_. Racket and Gambit code generators are also
available. There is not yet a way to plug in code generators as in Idris 1,
but this is coming.
available.  Like Idris 1, Idris 2 `supports plug-in code generation
<https://idris2.readthedocs.io/en/latest/backends/custom.html>`_
to allow you to write a back end for the platform of your choice.
To change the code generator, you can use the ``:set cg`` command:

::

M idris2api.ipkg => idris2api.ipkg +14 -2
@@ 22,6 22,7 @@ modules =
    Compiler.ES.RemoveUnused,
    Compiler.ES.TailRec,

    Compiler.RefC.CC,
    Compiler.RefC.RefC,

    Compiler.Scheme.Chez,


@@ 71,14 72,17 @@ modules =
    Idris.Driver,
    Idris.Error,
    Idris.ModTree,

    Idris.Package,
    Idris.Package.Init,
    Idris.Package.Types,

    Idris.Parser,
    Idris.Parser.Let,
    Idris.Pretty,
    Idris.Pretty.Render,
    Idris.ProcessIdr,
    Idris.REPL,
    Idris.REPLCommon,
    Idris.REPLOpts,
    Idris.Resugar,
    Idris.SetOptions,
    Idris.Syntax,


@@ 96,6 100,10 @@ modules =
    Idris.IDEMode.SyntaxHighlight,
    Idris.IDEMode.TokenLine,

    Idris.REPL.Common,
    Idris.REPL.Opts,
    Idris.REPL.FuzzySearch,

    Libraries.Control.ANSI,
    Libraries.Control.ANSI.CSI,
    Libraries.Control.ANSI.SGR,


@@ 112,6 120,7 @@ modules =
    Libraries.Data.List.Lazy,
    Libraries.Data.List1,
    Libraries.Data.NameMap,
    Libraries.Data.PosMap,
    Libraries.Data.SortedMap,
    Libraries.Data.SortedSet,
    Libraries.Data.String.Extra,


@@ 119,6 128,8 @@ modules =
    Libraries.Data.StringMap,
    Libraries.Data.StringTrie,

    Libraries.System.Directory.Tree,

    Libraries.Text.Bounded,
    Libraries.Text.Distance.Levenshtein,
    Libraries.Text.Lexer,


@@ 164,6 175,7 @@ modules =
    TTImp.Impossible,
    TTImp.Parser,
    TTImp.PartialEval,
    TTImp.ProcessBuiltin,
    TTImp.ProcessData,
    TTImp.ProcessDecls,
    TTImp.ProcessDef,

M libs/base/Control/App.idr => libs/base/Control/App.idr +19 -2
@@ 2,6 2,7 @@ module Control.App

import Data.IORef

||| `Error` is a type synonym for `Type`, specify for exception handling.
public export
Error : Type
Error = Type


@@ 11,6 12,8 @@ data HasErr : Error -> List Error -> Type where
     Here : HasErr e (e :: es)
     There : HasErr e es -> HasErr e (e' :: es)

||| States whether the program's execution path is linear or might throw exceptions so that we can know
||| whether it is safe to reference linear resources.
public export
data Path = MayThrow | NoThrow



@@ 86,6 89,11 @@ prim_app1_bind : (1 act : PrimApp1 Any a) ->
prim_app1_bind fn k w
    = let MkApp1ResW x' w' = fn w in k x' w'

||| A type supports throwing and catching exceptions. See `interface Exception err e` for details.
||| @ l  An implicit Path states whether the program's execution path is linear or might throw
|||      exceptions. The default value is `MayThrow` which represents that the program might throw.
||| @ es A list of exception types that can be thrown. Constrained interfaces can be defined by
|||      parameterising with a list of errors `es`.
export
data App : {default MayThrow l : Path} ->
           (es : List Error) -> Type -> Type where


@@ 255,8 263,15 @@ new val prog

public export
interface Exception err e where
  throw : err -> App e a
  catch : App e a -> (err -> App e a) -> App e a
  ||| Throw an exception.
  ||| @ ev Value of the exception.
  throw : (ev : err) -> App e a
  ||| Use with a given computation to do exception-catching.
  ||| If any exception is raised then the handler is executed.
  ||| @ act The computation to run.
  ||| @ k   Handler to invoke if an exception is raised.
  ||| @ ev  Value of the exception passed as an argument to the handler.
  catch : (act : App e a) -> (k : (ev : err) -> App e a) -> App e a

findException : HasErr e es -> e -> OneOf es MayThrow
findException Here err = First err


@@ 313,6 328,8 @@ public export
Init : List Error
Init = [AppHasIO]

||| The only way provided by `Control.App` to run an App.
||| @ Init A concrete list of errors.
export
run : App {l} Init a -> IO a
run (MkApp prog)

A libs/base/Control/Applicative/Const.idr => libs/base/Control/Applicative/Const.idr +112 -0
@@ 0,0 1,112 @@
module Control.Applicative.Const

import Data.Contravariant
import Data.Bits

public export
record Const (a : Type) (b : Type) where
  constructor MkConst
  runConst : a

public export
Eq a => Eq (Const a b) where
  (==) = (==) `on` runConst

public export
Ord a => Ord (Const a b) where
  compare = compare `on` runConst

export
Show a => Show (Const a b) where
  showPrec p (MkConst v) = showCon p "MkConst" (showArg v)

public export
Semigroup a => Semigroup (Const a b) where
  MkConst x <+> MkConst y = MkConst (x <+> y)

public export
Monoid a => Monoid (Const a b) where
  neutral = MkConst neutral

public export
Num a => Num (Const a b) where
  MkConst x + MkConst y = MkConst (x + y)
  MkConst x * MkConst y = MkConst (x * y)
  fromInteger = MkConst . fromInteger

public export
Neg a => Neg (Const a b) where
  negate (MkConst x)    = MkConst (negate x)
  MkConst x - MkConst y = MkConst (x - y)

public export
Abs a => Abs (Const a b) where
  abs (MkConst x)    = MkConst (abs x)

public export
Fractional a => Fractional (Const a b) where
  recip (MkConst x)     = MkConst (recip x)
  MkConst x / MkConst y = MkConst (x / y)

public export
Integral a => Integral (Const a b) where
  MkConst x `div` MkConst y = MkConst (x `div` y)
  MkConst x `mod` MkConst y = MkConst (x `mod` y)

public export
Bits a => Bits (Const a b) where
  Index = Index {a}
  MkConst x .&. MkConst y = MkConst (x .&. y)
  MkConst x .|. MkConst y = MkConst (x .|. y)
  MkConst x `xor` MkConst y = MkConst (x `xor` y)
  shiftL (MkConst v) ix = MkConst (shiftL v ix)
  shiftR (MkConst v) ix = MkConst (shiftR v ix)
  bit = MkConst . bit
  zeroBits = MkConst zeroBits
  complement (MkConst v) = MkConst (complement v)
  oneBits = MkConst oneBits
  complementBit (MkConst v) ix = MkConst (complementBit v ix)
  clearBit (MkConst v) ix = MkConst (clearBit v ix)
  testBit (MkConst v) ix = testBit v ix
  setBit (MkConst v) ix = MkConst (setBit v ix)

public export
FromString a => FromString (Const a b) where
  fromString = MkConst . fromString

public export
Functor (Const a) where
  map _ (MkConst v) = MkConst v

public export
Contravariant (Const a) where
  contramap _ (MkConst v) = MkConst v

public export
Monoid a => Applicative (Const a) where
  pure _ = MkConst neutral
  MkConst x <*> MkConst y = MkConst (x <+> y)

public export
Foldable (Const a) where
  foldr _ acc _ = acc
  foldl _ acc _ = acc
  null _ = True

public export
Traversable (Const a) where
  traverse _ (MkConst v) = pure (MkConst v)

public export
Bifunctor Const where
  bimap f _ (MkConst v) = MkConst (f v)

public export
Bifoldable Const where
  bifoldr f _ acc (MkConst v) = f v acc
  bifoldl f _ acc (MkConst v) = f acc v
  binull _ = False

public export
Bitraversable Const where
  bitraverse f _ (MkConst v) = MkConst <$> f v

M libs/base/Control/Monad/Identity.idr => libs/base/Control/Monad/Identity.idr +48 -0
@@ 1,5 1,7 @@
module Control.Monad.Identity

import Data.Bits

public export
record Identity (a : Type) where
  constructor Id


@@ 43,3 45,49 @@ public export
public export
(Monoid a) => Monoid (Identity a) where
  neutral = Id (neutral)

public export
Num a => Num (Identity a) where
  Id x + Id y = Id (x + y)
  Id x * Id y = Id (x * y)
  fromInteger = Id . fromInteger

public export
Neg a => Neg (Identity a) where
  negate (Id x)    = Id (negate x)
  Id x - Id y = Id (x - y)

public export
Abs a => Abs (Identity a) where
  abs (Id x)    = Id (abs x)

public export
Fractional a => Fractional (Identity a) where
  recip (Id x)     = Id (recip x)
  Id x / Id y = Id (x / y)

public export
Integral a => Integral (Identity a) where
  Id x `div` Id y = Id (x `div` y)
  Id x `mod` Id y = Id (x `mod` y)

public export
Bits a => Bits (Identity a) where
  Index = Index {a}
  Id x .&. Id y = Id (x .&. y)
  Id x .|. Id y = Id (x .|. y)
  Id x `xor` Id y = Id (x `xor` y)
  shiftL (Id v) ix = Id (shiftL v ix)
  shiftR (Id v) ix = Id (shiftR v ix)
  bit = Id . bit
  zeroBits = Id zeroBits
  complement (Id v) = Id (complement v)
  oneBits = Id oneBits
  complementBit (Id v) ix = Id (complementBit v ix)
  clearBit (Id v) ix = Id (clearBit v ix)
  testBit (Id v) ix = testBit v ix
  setBit (Id v) ix = Id (setBit v ix)

public export
FromString a => FromString (Identity a) where
  fromString = Id . fromString

A libs/base/Data/Bifoldable.idr => libs/base/Data/Bifoldable.idr +128 -0
@@ 0,0 1,128 @@
||| Additional utility functions for the `Bifoldable` interface.
module Data.Bifoldable

||| Left associative monadic bifold over a structure.
public export
bifoldlM :  (Bifoldable p, Monad m)
         => (f: a -> b -> m a)
         -> (g: a -> c -> m a)
         -> (init: a)
         -> (input: p b c) -> m a
bifoldlM f g a0 = bifoldl (\ma,b => ma >>= flip f b)
                          (\ma,c => ma >>= flip g c)
                          (pure a0)

||| Combines the elements of a structure,
||| given ways of mapping them to a common monoid.
public export
bifoldMap : (Bifoldable p, Monoid m) => (a -> m) -> (b -> m) -> p a b -> m
bifoldMap f g = bifoldr ((<+>) . f) ((<+>) . g) neutral

||| Combines the elements of a structure using a monoid.
public export
biconcat : (Bifoldable p, Monoid m) => p m m -> m
biconcat = bifoldr (<+>) (<+>) neutral

||| Combines the elements of a structure,
||| given ways of mapping them to a common monoid.
public export
biconcatMap : (Bifoldable p, Monoid m) => (a -> m) -> (b -> m) -> p a b -> m
biconcatMap f g = bifoldr ((<+>) . f) ((<+>) . g) neutral

||| The conjunction of all elements of a structure containing lazy boolean
||| values.  `biand` short-circuits from left to right, evaluating until either an
||| element is `False` or no elements remain.
public export
biand : Bifoldable p => p (Lazy Bool) (Lazy Bool) -> Bool
biand = bifoldl (&&) (&&) True

||| The disjunction of all elements of a structure containing lazy boolean
||| values.  `bior` short-circuits from left to right, evaluating either until an
||| element is `True` or no elements remain.
public export
bior : Bifoldable p => p (Lazy Bool) (Lazy Bool) -> Bool
bior = bifoldl (||) (||) False

||| The disjunction of the collective results of applying a predicate to all
||| elements of a structure. `biany` short-circuits from left to right.
public export
biany : Bifoldable p => (a -> Bool) -> (b -> Bool) -> p a b -> Bool
biany f g = bifoldl (\x,y => x || f y) (\x,y => x || g y) False

||| The disjunction of the collective results of applying a predicate to all
||| elements of a structure.  `biall` short-circuits from left to right.
public export
biall : Bifoldable p => (a -> Bool) -> (b -> Bool) -> p a b -> Bool
biall f g = bifoldl (\x,y => x && f y) (\x,y => x && g y) True

||| Add together all the elements of a structure.
public export
bisum : (Bifoldable p, Num a) => p a a -> a
bisum = bifoldr (+) (+) 0

||| Add together all the elements of a structure.
||| Same as `bisum` but tail recursive.
export
bisum' : (Bifoldable p, Num a) => p a a -> a
bisum' = bifoldl (+) (+) 0

||| Multiply together all elements of a structure.
public export
biproduct : (Bifoldable p, Num a) => p a a -> a
biproduct = bifoldr (*) (*) 1

||| Multiply together all elements of a structure.
||| Same as `product` but tail recursive.
export
biproduct' : (Bifoldable p, Num a) => p a a -> a
biproduct' = bifoldl (*) (*) 1

||| Map each element of a structure to a computation, evaluate those
||| computations and discard the results.
public export
bitraverse_ :  (Bifoldable p, Applicative f)
            => (a -> f x)
            -> (b -> f y)
            -> p a b
            -> f ()
bitraverse_ f g = bifoldr ((*>) . f) ((*>) . g) (pure ())

||| Evaluate each computation in a structure and discard the results.
public export
bisequence_ : (Bifoldable p, Applicative f) => p (f a) (f b) -> f ()
bisequence_ = bifoldr (*>) (*>) (pure ())

||| Like `bitraverse_` but with the arguments flipped.
public export
bifor_ :  (Bifoldable p, Applicative f)
       => p a b
       -> (a -> f x)
       -> (b -> f y)
       -> f ()
bifor_ p f g = bitraverse_ f g p

||| Bifold using Alternative.
|||
||| If you have a left-biased alternative operator `<|>`, then `choice` performs
||| left-biased choice from a list of alternatives, which means that it
||| evaluates to the left-most non-`empty` alternative.
public export
bichoice : (Bifoldable p, Alternative f) => p (Lazy (f a)) (Lazy (f a)) -> f a
bichoice t = bifoldr {a = Lazy (f a)} {b = Lazy (f a)} {acc = Lazy (f a)}
                 (\ x, xs => x <|> xs)
                 (\ x, xs => x <|> xs)
                 empty
                 t

||| A fused version of `bichoice` and `bimap`.
public export
bichoiceMap : (Bifoldable p, Alternative f)
            => (a -> f x)
            -> (b -> f x)
            -> p a b ->
            f x
bichoiceMap fa fb t = bifoldr {a} {b} {acc = Lazy (f x)}
                        (\e, fx => fa e <|> fx)
                        (\e, fx => fb e <|> fx)
                        empty
                        t

M libs/base/Data/Bool.idr => libs/base/Data/Bool.idr +13 -0
@@ 109,3 109,16 @@ export
notFalseIsTrue : {1 x : Bool} -> Not (x = False) -> x = True
notFalseIsTrue {x=True} _  = Refl
notFalseIsTrue {x=False} f = absurd $ f Refl

--------------------------------------------------------------------------------
-- Decidability specialized on bool
--------------------------------------------------------------------------------

||| You can reverse decidability when bool is involved.
-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
invertContraBool False True contra = Refl
invertContraBool True False contra = Refl
invertContraBool True True contra = absurd $ contra Refl

A libs/base/Data/Contravariant.idr => libs/base/Data/Contravariant.idr +48 -0
@@ 0,0 1,48 @@
module Data.Contravariant

infixl 4 >$, >$<, >&<, $<

||| Contravariant functors
public export
interface Contravariant (0 f : Type -> Type) where
  contramap : (a -> b) -> f b -> f a

  (>$) : b -> f b -> f a
  v >$ fb = contramap (const v) fb

||| If `f` is both `Functor` and `Contravariant` then by the time you factor in the
||| laws of each of those classes, it can't actually use its argument in any
||| meaningful capacity.
public export %inline
phantom : (Functor f, Contravariant f) => f a -> f b
phantom fa = () >$ (fa $> ())

||| This is an infix alias for `contramap`.
public export %inline
(>$<) : Contravariant f => (a -> b) -> f b -> f a
(>$<) = contramap

||| This is an infix version of `contramap` with the arguments flipped.
public export %inline
(>&<) : Contravariant f => f b -> (a -> b) -> f a
(>&<) = flip contramap

||| This is `>$` with its arguments flipped.
public export %inline
($<) : Contravariant f => f b -> b -> f a
($<) = flip (>$)

||| Composition of `Contravariant` is a `Functor`.
public export
[Compose] (Contravariant f, Contravariant g) => Functor (f . g) where
  map = contramap . contramap

||| Composition of a `Functor` and a `Contravariant` is a `Contravariant`.
public export
[ComposeFC] (Functor f, Contravariant g) => Contravariant (f . g) where
  contramap = map . contramap

||| Composition of a `Contravariant` and a `Functor` is a `Contravariant`.
public export
[ComposeCF] (Contravariant f, Functor g) => Contravariant (f . g) where
  contramap = contramap . map

M libs/base/Data/Fin.idr => libs/base/Data/Fin.idr +104 -0
@@ 17,6 17,14 @@ data Fin : (n : Nat) -> Type where
    FZ : Fin (S k)
    FS : Fin k -> Fin (S k)

||| Cast between Fins with equal indices
public export
cast : {n : Nat} -> (0 eq : m = n) -> Fin m -> Fin n
cast {n = S _} eq FZ = FZ
cast {n = Z} eq FZ impossible
cast {n = S _} eq (FS k) = FS (cast (succInjective _ _ eq) k)
cast {n = Z} eq (FS k) impossible

export
Uninhabited (Fin Z) where
  uninhabited FZ impossible


@@ 176,3 184,99 @@ DecEq (Fin n) where
      = case decEq f f' of
             Yes p => Yes $ cong FS p
             No p => No $ p . fsInjective

namespace Equality

  ||| Pointwise equality of Fins
  ||| It is sometimes complicated to prove equalities on type-changing
  ||| operations on Fins.
  ||| This inductive definition can be used to simplify proof. We can
  ||| recover proofs of equalities by using `homoPointwiseIsEqual`.
  public export
  data Pointwise : Fin m -> Fin n -> Type where
    FZ : Pointwise FZ FZ
    FS : Pointwise k l -> Pointwise (FS k) (FS l)

  infix 6 ~~~
  ||| Convenient infix notation for the notion of pointwise equality of Fins
  public export
  (~~~) : Fin m -> Fin n -> Type
  (~~~) = Pointwise

  ||| Pointwise equality is reflexive
  export
  reflexive : {k : Fin m} -> k ~~~ k
  reflexive {k = FZ} = FZ
  reflexive {k = FS k} = FS reflexive

  ||| Pointwise equality is symmetric
  export
  symmetric : k ~~~ l -> l ~~~ k
  symmetric FZ = FZ
  symmetric (FS prf) = FS (symmetric prf)

  ||| Pointwise equality is transitive
  export
  transitive : j ~~~ k -> k ~~~ l -> j ~~~ l
  transitive FZ FZ = FZ
  transitive (FS prf) (FS prg) = FS (transitive prf prg)

  ||| Pointwise equality is compatible with cast
  export
  castEq : {k : Fin m} -> (0 eq : m = n) -> cast eq k ~~~ k
  castEq {k = FZ} Refl = FZ
  castEq {k = FS k} Refl = FS (castEq _)

  ||| The actual proof used by cast is irrelevant
  export
  congCast : {n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
             {0 eq1 : m = n} -> {0 eq2 : p = q} ->
             k ~~~ l ->
             cast eq1 k ~~~ cast eq2 l
  congCast eq = transitive (castEq _) (transitive eq $ symmetric $ castEq _)

  ||| Last is congruent wrt index equality
  export
  congLast : {m, n : Nat} -> (0 _ : m = n) -> last {n=m} ~~~ last {n}
  congLast {m = Z} {n = Z} eq = reflexive
  congLast {m = S _} {n = S _} eq = FS (congLast (succInjective _ _ eq))

  export
  congShift : (m : Nat) -> k ~~~ l -> shift m k ~~~ shift m l
  congShift Z prf = prf
  congShift (S m) prf = FS (congShift m prf)

  ||| WeakenN is congruent wrt pointwise equality
  export
  congWeakenN : k ~~~ l -> weakenN n k ~~~ weakenN n l
  congWeakenN FZ = FZ
  congWeakenN (FS prf) = FS (congWeakenN prf)

  ||| Pointwise equality is propositional equality on Fins that have the same type
  export
  homoPointwiseIsEqual : {0 k, l : Fin m} -> k ~~~ l -> k === l
  homoPointwiseIsEqual FZ = Refl
  homoPointwiseIsEqual (FS prf) = cong FS (homoPointwiseIsEqual prf)

  ||| Pointwise equality is propositional equality modulo transport on Fins that
  ||| have provably equal types
  export
  hetPointwiseIsTransport :
     {0 k : Fin m} -> {0 l : Fin n} ->
     (eq : m === n) -> k ~~~ l -> k === rewrite eq in l
  hetPointwiseIsTransport Refl = homoPointwiseIsEqual

  export
  finToNatQuotient : k ~~~ l -> finToNat k === finToNat l
  finToNatQuotient FZ = Refl
  finToNatQuotient (FS prf) = cong S (finToNatQuotient prf)

  export
  weakenNeutral : (k : Fin n) -> weaken k ~~~ k
  weakenNeutral FZ = FZ
  weakenNeutral (FS k) = FS (weakenNeutral k)

  export
  weakenNNeutral : (0 m : Nat) -> (k : Fin n) -> weakenN m k ~~~ k
  weakenNNeutral m FZ = FZ
  weakenNNeutral m (FS k) = FS (weakenNNeutral m k)

M libs/base/Data/Maybe.idr => libs/base/Data/Maybe.idr +5 -0
@@ 60,3 60,8 @@ lowerMaybe (Just x) = x
export
raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a
raiseToMaybe x = if x == neutral then Nothing else Just x

public export
filter : (a -> Bool) -> Maybe a -> Maybe a
filter _ Nothing = Nothing
filter f (Just x) = toMaybe (f x) x

M libs/base/Data/Morphisms.idr => libs/base/Data/Morphisms.idr +36 -0
@@ 1,5 1,7 @@
module Data.Morphisms

import Data.Contravariant

public export
record Morphism a b where
  constructor Mor


@@ 21,6 23,11 @@ record Kleislimorphism (f : Type -> Type) a b where
  constructor Kleisli
  applyKleisli : a -> f b

public export
record Op b a where
  constructor MkOp
  applyOp : a -> b

export
Functor (Morphism r) where
  map f (Mor a) = Mor $ f . a


@@ 65,6 72,11 @@ Monad f => Monad (Kleislimorphism f a) where
    k1 <- f r
    applyKleisli (g k1) r

public export
Contravariant (Op b) where
  contramap f (MkOp g) = MkOp (g . f)
  v >$ (MkOp f) = MkOp \_ => f v

-- Applicative is a bit too strong, but there is no suitable superclass
export
(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a) where


@@ 89,3 101,27 @@ Cast (Morphism a (f b)) (Kleislimorphism f a b) where
export
Cast (Kleislimorphism f a b) (Morphism a (f b)) where
  cast (Kleisli f) = Mor f

export
Cast (Endomorphism a) (Op a a) where
  cast (Endo f) = MkOp f

export
Cast (Op a a) (Endomorphism a) where
  cast (MkOp f) = Endo f

export
Cast (Op (f b) a) (Kleislimorphism f a b) where
  cast (MkOp f) = Kleisli f

export
Cast (Kleislimorphism f a b) (Op (f b) a) where
  cast (Kleisli f) = MkOp f

export
Cast (Morphism a b) (Op b a) where
  cast (Mor f) = MkOp f

export
Cast (Op b a) (Morphism a b) where
  cast (MkOp f) = Mor f

M libs/base/Data/Primitives/Views.idr => libs/base/Data/Primitives/Views.idr +16 -8
@@ 30,16 30,20 @@ namespace IntegerV
  public export
  data IntegerRec : Integer -> Type where
       IntegerZ : IntegerRec 0
       IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
       IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
       -- adding the constant (-1 or 1) on the left keeps the view
       -- similar to the inductive definition of natural numbers, and
       -- is usually compatible with pattern matching on arguments
       -- left-to-right.
       IntegerSucc : IntegerRec (-1 + n) -> IntegerRec n
       IntegerPred : IntegerRec (1 + (-n)) -> IntegerRec (-n)

  ||| Covering function for `IntegerRec`
  public export
  integerRec : (x : Integer) -> IntegerRec x
  integerRec 0 = IntegerZ
  integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
  integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (-1 + x)))
                      else believe_me (IntegerPred {n = -x}
                                (assert_total (believe_me (integerRec (x + 1)))))
                                (assert_total (believe_me (integerRec (1 + x)))))

namespace IntV
  ||| View for expressing a number as a multiplication + a remainder


@@ 70,13 74,17 @@ namespace IntV
  public export
  data IntRec : Int -> Type where
       IntZ : IntRec 0
       IntSucc : IntRec (n - 1) -> IntRec n
       IntPred : IntRec ((-n) + 1) -> IntRec (-n)
       -- adding the constant (-1 or 1) on the left keeps the view
       -- similar to the inductive definition of natural numbers, and
       -- is usually compatible with pattern matching on arguments
       -- left-to-right.
       IntSucc : IntRec (-1 + n) -> IntRec n
       IntPred : IntRec (1 + (-n)) -> IntRec (-n)

  ||| Covering function for `IntRec`
  public export
  intRec : (x : Int) -> IntRec x
  intRec 0 = IntZ
  intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
  intRec x = if x > 0 then IntSucc (assert_total (intRec (-1 + x)))
                      else believe_me (IntPred {n = -x}
                                (assert_total (believe_me (intRec (x + 1)))))
                                (assert_total (believe_me (intRec (1 + x)))))

M libs/base/Data/These.idr => libs/base/Data/These.idr +20 -6
@@ 42,6 42,26 @@ Bifunctor These where

%inline
public export
Bifoldable These where
  bifoldr f _ acc (This a)   = f a acc
  bifoldr _ g acc (That b)   = g b acc
  bifoldr f g acc (Both a b) = f a (g b acc)

  bifoldl f _ acc (This a)   = f acc a
  bifoldl _ g acc (That b)   = g acc b
  bifoldl f g acc (Both a b) = g (f acc a) b

  binull _ = False

%inline
public export
Bitraversable These where
  bitraverse f _ (This a)   = This <$> f a
  bitraverse _ g (That b)   = That <$> g b
  bitraverse f g (Both a b) = [| Both (f a) (g b) |]

%inline
public export
Functor (These a) where
  map = mapSnd



@@ 50,9 70,3 @@ bifold : Monoid m => These m m -> m
bifold (This a)   = a
bifold (That b)   = b
bifold (Both a b) = a <+> b

public export
bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> These a b -> f (These c d)
bitraverse f g (This a)   = [| This (f a) |]
bitraverse f g (That b)   = [| That (g b) |]
bitraverse f g (Both a b) = [| Both (f a) (g b) |]

M libs/base/System.idr => libs/base/System.idr +14 -6
@@ 31,15 31,23 @@ export
usleep : HasIO io => (x : Int) -> So (x >= 0) => io ()
usleep sec = primIO (prim__usleep sec)

-- This one is going to vary for different back ends. Probably needs a
-- better convention. Will revisit...
%foreign "scheme:blodwen-args"
         "node:lambda:() => __prim_js2idris_array(process.argv.slice(1))"
prim__getArgs : PrimIO (List String)
-- Get the number of arguments
%foreign "scheme:blodwen-arg-count"
         "node:lambda:() => process.argv.length"
prim__getArgCount : PrimIO Int

-- Get argument number `n`
%foreign "scheme:blodwen-arg"
         "node:lambda:n => process.argv[n]"
prim__getArg : Int -> PrimIO String

export
getArgs : HasIO io => io (List String)
getArgs = primIO prim__getArgs
getArgs = do
            n <- primIO prim__getArgCount
            if n > 0
              then for [0..n-1] (\x => primIO $ prim__getArg x)
              else pure []

%foreign libc "getenv"
         "node:lambda: n => process.env[n]"

M libs/base/System/Directory.idr => libs/base/System/Directory.idr +1 -1
@@ 10,7 10,7 @@ support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support"

%foreign support "idris2_fileErrno"
         "node:support:fileErrno,support_system_directory"
         "node:support:fileErrno,support_system_file"
prim__fileErrno : PrimIO Int

returnError : HasIO io => io (Either FileError a)

M libs/base/System/File.idr => libs/base/System/File.idr +1 -1
@@ 34,7 34,7 @@ prim__close : FilePtr -> PrimIO ()
prim__error : FilePtr -> PrimIO Int

%foreign support "idris2_fileErrno"
         "node:lambda:()=>-BigInt(process.__lasterr.errno)"
         "node:support:fileErrno,support_system_file"
prim__fileErrno : PrimIO Int

%foreign support "idris2_seekLine"

M libs/base/base.ipkg => libs/base/base.ipkg +4 -0
@@ 7,6 7,8 @@ modules = Control.App,
          Control.App.Console,
          Control.App.FileIO,

          Control.Applicative.Const,

          Control.Monad.Either,
          Control.Monad.Error.Either,
          Control.Monad.Error.Interface,


@@ 28,12 30,14 @@ modules = Control.App,
          Control.Monad.Writer.Interface,
          Control.WellFounded,

          Data.Bifoldable,
          Data.Bits,
          Data.Bool,
          Data.Bool.Xor,
          Data.Buffer,
          Data.Colist,
          Data.Colist1,
          Data.Contravariant,
          Data.DPair,
          Data.Either,
          Data.Fin,

M libs/contrib/Control/Linear/LIO.idr => libs/contrib/Control/Linear/LIO.idr +8 -0
@@ 49,6 49,14 @@ data L : (io : Type -> Type) ->
            (1 _ : ContType io u_act u_k a b) ->
            L io {use=u_k} b

public export
L0 : (io : Type -> Type) -> (ty : Type) -> Type
L0 io ty = L io {use = 0} ty

public export
L1 : (io : Type -> Type) -> (ty : Type) -> Type
L1 io ty = L io {use = 1} ty

ContType io None u_k a b = (0 _ : a) -> L io {use=u_k} b
ContType io Linear u_k a b = (1 _ : a) -> L io {use=u_k} b
ContType io Unrestricted u_k a b = a -> L io {use=u_k} b

M libs/contrib/Data/Fin/Extra.idr => libs/contrib/Data/Fin/Extra.idr +361 -38
@@ 3,77 3,130 @@ module Data.Fin.Extra
import Data.Fin
import Data.Nat

import Syntax.WithProof
import Syntax.PreorderReasoning

%default total

||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
-------------------------------
--- `finToNat`'s properties ---
-------------------------------

||| A Fin's underlying natural number is smaller than the bound
export
elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
elemSmallerThanBound FZ = LTESucc LTEZero
elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)

||| Proof that application of finToNat the last element of Fin **S n** gives **n**.
||| Last's underlying natural number is the bound's predecessor
export
finToNatLastIsBound : {n : Nat} -> finToNat (Fin.last {n}) = n
finToNatLastIsBound {n=Z} = Refl
finToNatLastIsBound {n=S k} = rewrite finToNatLastIsBound {n=k} in Refl
finToNatLastIsBound {n=S k} = cong S finToNatLastIsBound

||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
||| Weaken does not modify the underlying natural number
export
finToNatWeakenNeutral : {m : Nat} -> {n : Fin m} -> finToNat (weaken n) = finToNat n
finToNatWeakenNeutral {n=FZ} = Refl
finToNatWeakenNeutral {m=S (S _)} {n=FS _} = cong S finToNatWeakenNeutral
finToNatWeakenNeutral : {n : Fin m} -> finToNat (weaken n) = finToNat n
finToNatWeakenNeutral = finToNatQuotient (weakenNeutral n)

-- ||| Proof that it's possible to strengthen a weakened element of Fin **m**.
-- export
-- strengthenWeakenNeutral : {m : Nat} -> (n : Fin m) -> strengthen (weaken n) = Right n
-- strengthenWeakenNeutral {m=S _} FZ = Refl
-- strengthenWeakenNeutral {m=S (S _)} (FS k) = rewrite strengthenWeakenNeutral k in Refl
||| WeakenN does not modify the underlying natural number
export
finToNatWeakenNNeutral : (0 m : Nat) -> (k : Fin n) ->
                         finToNat (weakenN m k) = finToNat k
finToNatWeakenNNeutral m k = finToNatQuotient (weakenNNeutral m k)

||| Proof that it's not possible to strengthen the last element of Fin **n**.
||| `Shift k` shifts the underlying natural number by `k`.
export
strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Left (Fin.last {n})
strengthenLastIsLeft {n=Z} = Refl
strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl
finToNatShift : (k : Nat) -> (a : Fin n) -> finToNat (shift k a) = k + finToNat a
finToNatShift Z     a = Refl
finToNatShift (S k) a = cong S (finToNatShift k a)

||| Enumerate elements of Fin **n** backwards.
-------------------------------------------------
--- Inversion function and related properties ---
-------------------------------------------------

||| Compute the Fin such that `k + invFin k = n - 1`
export
invFin : {n : Nat} -> Fin n -> Fin n
invFin FZ = last
invFin {n=S (S _)} (FS k) = weaken (invFin k)
invFin (FS k) = weaken (invFin k)

||| The inverse of a weakened element is the successor of its inverse
export
invFinWeakenIsFS : {n : Nat} -> (m : Fin n) -> invFin (weaken m) = FS (invFin m)
invFinWeakenIsFS FZ = Refl
invFinWeakenIsFS (FS k) = cong weaken (invFinWeakenIsFS k)

export
invFinLastIsFZ : {n : Nat} -> invFin (last {n}) = FZ
invFinLastIsFZ {n = Z} = Refl
invFinLastIsFZ {n = S n} = cong weaken (invFinLastIsFZ {n})

||| `invFin` is involutive (i.e. applied twice it is the identity)
export
invFinInvolutive : {n : Nat} -> (m : Fin n) -> invFin (invFin m) = m
invFinInvolutive FZ = invFinLastIsFZ
invFinInvolutive (FS k) = Calc $
   |~ invFin (invFin (FS k))
   ~~ invFin (weaken (invFin k)) ...( Refl )
   ~~ FS (invFin (invFin k))     ...( invFinWeakenIsFS (invFin k) )
   ~~ FS k                       ...( cong FS (invFinInvolutive k) )

--------------------------------
--- Strengthening properties ---
--------------------------------

||| Proof that an inverse of a weakened element of Fin **n** is a successive of an inverse of an original element.
||| It's possible to strengthen a weakened element of Fin **m**.
export
invWeakenIsSucc : {n : Nat} -> (m : Fin n) -> invFin (weaken m) = FS (invFin m)
invWeakenIsSucc FZ = Refl
invWeakenIsSucc {n=S (S _)} (FS k) = rewrite invWeakenIsSucc k in Refl
strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Right n
strengthenWeakenIsRight FZ = Refl
strengthenWeakenIsRight (FS k) = rewrite strengthenWeakenIsRight k in Refl

||| Proof that double inversion of Fin **n** gives the original.
||| It's not possible to strengthen the last element of Fin **n**.
export
doubleInvFinSame : {n : Nat} -> (m : Fin n) -> invFin (invFin m) = m
doubleInvFinSame {n=S Z} FZ = Refl
doubleInvFinSame {n=S (S k)} FZ = rewrite doubleInvFinSame {n=S k} FZ in Refl
doubleInvFinSame {n=S (S _)} (FS x) = trans (invWeakenIsSucc $ invFin x) (cong FS $ doubleInvFinSame x)
strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Left (Fin.last {n})
strengthenLastIsLeft {n=Z} = Refl
strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl

||| Proof that an inverse of the last element of Fin (S **n**) in FZ.
||| It's possible to strengthen the inverse of a succesor
export
invLastIsFZ : {n : Nat} -> invFin (Fin.last {n}) = FZ
invLastIsFZ {n=Z} = Refl
invLastIsFZ {n=S k} = rewrite invLastIsFZ {n=k} in Refl
strengthenNotLastIsRight : {n : Nat} -> (m : Fin n) -> strengthen (invFin (FS m)) = Right (invFin m)
strengthenNotLastIsRight m = strengthenWeakenIsRight (invFin m)

-- ||| Proof that it's possible to strengthen an inverse of a succesive element of Fin **n**.
-- export
-- strengthenNotLastIsRight : (m : Fin (S n)) -> strengthen (invFin (FS m)) = Right (invFin m)
-- strengthenNotLastIsRight m = strengthenWeakenNeutral (invFin m)
--
||| Either tightens the bound on a Fin or proves that it's the last.
export
strengthen' : {n : Nat} -> (m : Fin (S n)) -> Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
strengthen' : {n : Nat} -> (m : Fin (S n)) ->
              Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
strengthen' {n = Z} FZ = Left Refl
strengthen' {n = S k} FZ = Right (FZ ** Refl)
strengthen' {n = S k} (FS m) = case strengthen' m of
    Left eq => Left $ cong FS eq
    Right (m' ** eq) => Right (FS m' ** cong S eq)

----------------------------
--- Weakening properties ---
----------------------------

export
weakenNZeroIdentity : (k : Fin n) ->  weakenN 0 k ~~~ k
weakenNZeroIdentity FZ = FZ
weakenNZeroIdentity (FS k) = FS (weakenNZeroIdentity k)

export
shiftFSLinear : (m : Nat) -> (f : Fin n) -> shift m (FS f) ~~~ FS (shift m f)
shiftFSLinear Z     f = reflexive
shiftFSLinear (S m) f = FS (shiftFSLinear m f)

export
shiftLastIsLast : (m : Nat) -> {n : Nat} ->
                  shift m (Fin.last {n}) ~~~ Fin.last {n=m+n}
shiftLastIsLast Z = reflexive
shiftLastIsLast (S m) = FS (shiftLastIsLast m)

-----------------------------------
--- Division-related properties ---
-----------------------------------

||| A view of Nat as a quotient of some number and a finite remainder.
public export
data FractionView : (n : Nat) -> (d : Nat) -> Type where


@@ 98,6 151,9 @@ divMod {ok=_} (S n) (S d) =
            rewrite sym $ plusSuccRightSucc (q * S d) (finToNat r') in
                cong S $ trans (sym $ cong (plus (q * S d)) eq') eq

-------------------
--- Conversions ---
-------------------

||| Total function to convert a nat to a Fin, given a proof
||| that it is less than the bound.


@@ 113,4 169,271 @@ natToFinToNat :
  -> (lte : LT n m)
  -> finToNat (natToFinLTE n lte) = n
natToFinToNat 0 (LTESucc lte) = Refl
natToFinToNat (S k) (LTESucc lte) = rewrite natToFinToNat k lte in Refl
natToFinToNat (S k) (LTESucc lte) = cong S (natToFinToNat k lte)

----------------------------------------
--- Result-type changing arithmetics ---
----------------------------------------

||| Addition of `Fin`s as bounded naturals.
||| The resulting type has the smallest possible bound
||| as illustated by the relations with the `last` function.
public export
(+) : {m, n : Nat} -> Fin m -> Fin (S n) -> Fin (m + n)
(+) FZ y = cast (cong S $ plusCommutative n (pred m)) (weakenN (pred m) y)
(+) (FS x) y = FS (x + y)

||| Multiplication of `Fin`s as bounded naturals.
||| The resulting type has the smallest possible bound
||| as illustated by the relations with the `last` function.
public export
(*) : {m, n : Nat} -> Fin (S m) -> Fin (S n) -> Fin (S (m * n))
(*) FZ _ = FZ
(*) {m = S _} (FS x) y = y + x * y

--- Properties ---

-- Relation between `+` and `*` and their counterparts on `Nat`

export
finToNatPlusHomo : {m, n : Nat} -> (x : Fin m) -> (y : Fin (S n)) ->
                   finToNat (x + y) = finToNat x + finToNat y
finToNatPlusHomo FZ _
  = finToNatQuotient $ transitive
     (castEq _)
     (weakenNNeutral _ _)
finToNatPlusHomo (FS x) y = cong S (finToNatPlusHomo x y)

export
finToNatMultHomo : {m, n : Nat} -> (x : Fin (S m)) -> (y : Fin (S n)) ->
                   finToNat (x * y) = finToNat x * finToNat y
finToNatMultHomo FZ _ = Refl
finToNatMultHomo {m = S _} (FS x) y = Calc $
  |~ finToNat (FS x * y)
  ~~ finToNat (y + x * y)                 ...( Refl )
  ~~ finToNat y + finToNat (x * y)        ...( finToNatPlusHomo y (x * y) )
  ~~ finToNat y + finToNat x * finToNat y ...( cong (finToNat y +) (finToNatMultHomo x y) )
  ~~ finToNat (FS x) * finToNat y         ...( Refl)

-- Relations to `Fin`'s `last`

export
plusPreservesLast : (m, n : Nat) -> Fin.last {n=m} + Fin.last {n} = Fin.last
plusPreservesLast Z     n
  = homoPointwiseIsEqual $ transitive
      (castEq _)
      (weakenNNeutral _ _)
plusPreservesLast (S m) n = cong FS (plusPreservesLast m n)

export
multPreservesLast : (m, n : Nat) -> Fin.last {n=m} * Fin.last {n} = Fin.last
multPreservesLast Z n = Refl
multPreservesLast (S m) n = Calc $
  |~ last + (last * last)
  ~~ last + last          ...( cong (last +) (multPreservesLast m n) )
  ~~ last                 ...( plusPreservesLast n (m * n) )

-- General addition properties

export
plusSuccRightSucc : {m, n : Nat} -> (left : Fin m) -> (right : Fin (S n)) ->
                    FS (left + right) ~~~ left + FS right
plusSuccRightSucc FZ        right = FS $ congCast reflexive
plusSuccRightSucc (FS left) right = FS $ plusSuccRightSucc left right

-- Relations to `Fin`-specific `shift` and `weaken`

export
shiftAsPlus : {m, n : Nat} -> (k : Fin (S m)) ->
              shift n k ~~~ last {n} + k
shiftAsPlus {n=Z}   k =
  symmetric $ transitive (castEq _) (weakenNNeutral _ _)
shiftAsPlus {n=S n} k = FS (shiftAsPlus k)

export
weakenNAsPlusFZ : {m, n : Nat} -> (k : Fin n) ->
                  weakenN m k = k + the (Fin (S m)) FZ
weakenNAsPlusFZ FZ = Refl
weakenNAsPlusFZ (FS k) = cong FS (weakenNAsPlusFZ k)

export
weakenNPlusHomo : {0 m, n : Nat} -> (k : Fin p) ->
                  weakenN n (weakenN m k) ~~~ weakenN (m + n) k
weakenNPlusHomo FZ = FZ
weakenNPlusHomo (FS k) = FS (weakenNPlusHomo k)

export
weakenNOfPlus :
  {m, n : Nat} -> (k : Fin m) -> (l : Fin (S n)) ->
  weakenN w (k + l) ~~~ weakenN w k + l
weakenNOfPlus FZ l
  = transitive (congWeakenN (castEq _))
  $ transitive (weakenNPlusHomo l)
  $ symmetric (castEq _)
weakenNOfPlus (FS k) l = FS (weakenNOfPlus k l)
-- General addition properties (continued)

export
plusZeroLeftNeutral : (k : Fin (S n)) -> FZ + k ~~~ k
plusZeroLeftNeutral k = transitive (castEq _) (weakenNNeutral _ k)

export
congPlusLeft : {m, n, p : Nat} -> {k : Fin m} -> {l : Fin n} ->
               (c : Fin (S p)) -> k ~~~ l -> k + c ~~~ l + c
congPlusLeft c FZ
  = transitive (plusZeroLeftNeutral c)
               (symmetric $ plusZeroLeftNeutral c)
congPlusLeft c (FS prf) = FS (congPlusLeft c prf)

export
plusZeroRightNeutral : (k : Fin m) -> k + FZ ~~~ k
plusZeroRightNeutral FZ = FZ
plusZeroRightNeutral (FS k) = FS (plusZeroRightNeutral k)

export
congPlusRight : {m, n, p : Nat} -> {k : Fin (S n)} -> {l : Fin (S p)} ->
               (c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
congPlusRight c FZ
  = transitive (plusZeroRightNeutral c)
               (symmetric $ plusZeroRightNeutral c)
congPlusRight {n = S _} {p = S _} c (FS prf)
  = transitive (symmetric $ plusSuccRightSucc c _)
  $ transitive (FS $ congPlusRight c prf)
               (plusSuccRightSucc c _)
congPlusRight {p = Z} c (FS prf) impossible

export
plusCommutative : {m, n : Nat} -> (left : Fin (S m)) -> (right : Fin (S n)) ->
                  left + right ~~~ right + left
plusCommutative FZ        right
  = transitive (plusZeroLeftNeutral right)
               (symmetric $ plusZeroRightNeutral right)
plusCommutative {m = S _} (FS left) right
  = transitive (FS (plusCommutative left right))
               (plusSuccRightSucc right left)

export
plusAssociative :
  {m, n, p : Nat} ->
  (left : Fin m) -> (centre : Fin (S n)) -> (right : Fin (S p)) ->
  left + (centre + right) ~~~ (left + centre) + right
plusAssociative FZ centre right
  = transitive (plusZeroLeftNeutral (centre + right))
               (congPlusLeft right (symmetric $ plusZeroLeftNeutral centre))
plusAssociative (FS left) centre right = FS (plusAssociative left centre right)

-------------------------------------------------
--- Splitting operations and their properties ---
-------------------------------------------------

||| Converts `Fin`s that are used as indexes of parts to an index of a sum.
|||
||| For example, if you have a `Vect` that is a concatenation of two `Vect`s and
||| you have an index either in the first or the second of the original `Vect`s,
||| using this function you can get an index in the concatenated one.
public export
indexSum : {m : Nat} -> Either (Fin m) (Fin n) -> Fin (m + n)
indexSum (Left  l) = weakenN n l
indexSum (Right r) = shift m r

||| Extracts an index of the first or the second part from the index of a sum.
|||
||| For example, if you have a `Vect` that is a concatenation of the `Vect`s and
||| you have an index of this `Vect`, you have get an index of either left or right
||| original `Vect` using this function.
public export
splitSum : {m : Nat} -> Fin (m + n) -> Either (Fin m) (Fin n)
splitSum {m=Z}   k      = Right k
splitSum {m=S m} FZ     = Left FZ
splitSum {m=S m} (FS k) = mapFst FS $ splitSum k

||| Calculates the index of a square matrix of size `a * b` by indices of each side.
public export
indexProd : {n : Nat} -> Fin m -> Fin n -> Fin (m * n)
indexProd FZ     = weakenN $ mult (pred m) n
indexProd (FS k) = shift n . indexProd k

||| Splits the index of a square matrix of size `a * b` to indices of each side.
public export
splitProd : {m, n : Nat} -> Fin (m * n) -> (Fin m, Fin n)
splitProd {m=S _} p = case splitSum p of
  Left  k => (FZ, k)
  Right l => mapFst FS $ splitProd l

--- Properties ---

export
indexSumPreservesLast :
  (m, n : Nat) -> indexSum {m} (Right $ Fin.last {n}) ~~~ Fin.last {n=m+n}
indexSumPreservesLast Z     n = reflexive
indexSumPreservesLast (S m) n = FS (shiftLastIsLast m)

export
indexProdPreservesLast : (m, n : Nat) ->
         indexProd (Fin.last {n=m}) (Fin.last {n}) = Fin.last
indexProdPreservesLast Z n = homoPointwiseIsEqual
  $ transitive (weakenNZeroIdentity last)
               (congLast (sym $ plusZeroRightNeutral n))
indexProdPreservesLast (S m) n = Calc $
  |~ indexProd (last {n=S m}) (last {n})
  ~~ FS (shift n (indexProd last last)) ...( Refl )
  ~~ FS (shift n last)                  ...( cong (FS . shift n) (indexProdPreservesLast m n ) )
  ~~ last                               ...( homoPointwiseIsEqual prf )

  where

    prf : shift (S n) (Fin.last {n = n + m * S n}) ~~~ Fin.last {n = n + S (n + m * S n)}
    prf = transitive (shiftLastIsLast (S n))
                     (congLast (plusSuccRightSucc n (n + m * S n)))

export
splitSumOfWeakenN : (k : Fin m) -> splitSum {m} {n} (weakenN n k) = Left k
splitSumOfWeakenN FZ = Refl
splitSumOfWeakenN (FS k) = cong (mapFst FS) $ splitSumOfWeakenN k

export
splitSumOfShift : {m : Nat} -> (k : Fin n) -> splitSum {m} {n} (shift m k) = Right k
splitSumOfShift {m=Z}   k = Refl
splitSumOfShift {m=S m} k = cong (mapFst FS) $ splitSumOfShift k

export
splitOfIndexSumInverse : {m : Nat} -> (e : Either (Fin m) (Fin n)) -> splitSum (indexSum e) = e
splitOfIndexSumInverse (Left l) = splitSumOfWeakenN l
splitOfIndexSumInverse (Right r) = splitSumOfShift r

export
indexOfSplitSumInverse : {m, n : Nat} -> (f : Fin (m + n)) -> indexSum (splitSum {m} {n} f) = f
indexOfSplitSumInverse {m=Z}   f  = Refl
indexOfSplitSumInverse {m=S _} FZ = Refl
indexOfSplitSumInverse {m=S _} (FS f) with (indexOfSplitSumInverse f)
  indexOfSplitSumInverse {m=S _} (FS f) | eq with (splitSum f)
    indexOfSplitSumInverse {m=S _} (FS _) | eq | Left  _ = cong FS eq
    indexOfSplitSumInverse {m=S _} (FS _) | eq | Right _ = cong FS eq


export
splitOfIndexProdInverse : {m : Nat} -> (k : Fin m) -> (l : Fin n) ->
                          splitProd (indexProd k l) = (k, l)
splitOfIndexProdInverse FZ     l
   = rewrite splitSumOfWeakenN {n = mult (pred m) n} l in Refl
splitOfIndexProdInverse (FS k) l
   = rewrite splitSumOfShift {m=n} $ indexProd k l in
     cong (mapFst FS) $ splitOfIndexProdInverse k l

export
indexOfSplitProdInverse : {m, n : Nat} -> (f : Fin (m * n)) ->
                          uncurry (indexProd {m} {n}) (splitProd {m} {n} f) = f
indexOfSplitProdInverse {m = S _} f with (@@ splitSum f)
  indexOfSplitProdInverse {m = S _} f | (Left l ** eq) = rewrite eq in Calc $
    |~ indexSum (Left l)
    ~~ indexSum (splitSum f) ...( cong indexSum (sym eq) )
    ~~ f                     ...( indexOfSplitSumInverse f )
  indexOfSplitProdInverse f | (Right r ** eq) with (@@ splitProd r)
    indexOfSplitProdInverse f | (Right r ** eq) | ((p, q) ** eq2)
      = rewrite eq in rewrite eq2 in Calc $
        |~ indexProd (FS p) q
        ~~ shift n (indexProd p q)                   ...( Refl )
        ~~ shift n (uncurry indexProd (splitProd r)) ...( cong (shift n . uncurry indexProd) (sym eq2) )
        ~~ shift n r                                 ...( cong (shift n) (indexOfSplitProdInverse r) )
        ~~ indexSum (splitSum f)                     ...( sym (cong indexSum eq) )
        ~~ f                                         ...( indexOfSplitSumInverse f )

M libs/contrib/Data/String/Extra.idr => libs/contrib/Data/String/Extra.idr +18 -0
@@ 103,3 103,21 @@ indent n x = replicate n ' ' ++ x
public export
indentLines : (n : Nat) -> String -> String
indentLines n str = unlines $ map (indent n) $ forget $ lines str

||| Return a string of the given character repeated
||| `n` times.
export
fastReplicate : (n : Nat) -> Char -> String
fastReplicate n c = fastPack $ replicate n c

||| Left-justify a string to the given length, using the
||| specified fill character on the right.
export
justifyLeft : Nat -> Char -> String -> String
justifyLeft n c s = s ++ fastReplicate (n `minus` length s) c

||| Right-justify a string to the given length, using the
||| specified fill character on the left.
export
justifyRight : Nat -> Char -> String -> String
justifyRight n c s = fastReplicate (n `minus` length s) c ++ s

M libs/contrib/Data/Validated.idr => libs/contrib/Data/Validated.idr +15 -0
@@ 33,6 33,21 @@ Bifunctor Validated where
  bimap _ s $ Valid x   = Valid   $ s x
  bimap f _ $ Invalid e = Invalid $ f e

public export
Bifoldable Validated where
  bifoldr _ g acc (Valid a)   = g a acc
  bifoldr f _ acc (Invalid e) = f e acc

  bifoldl _ g acc (Valid a)   = g acc a
  bifoldl f _ acc (Invalid e) = f acc e

  binull _ = False

public export
Bitraversable Validated where
  bitraverse _ g (Valid a)   = Valid <$> g a
  bitraverse f _ (Invalid e) = Invalid <$> f e

||| Applicative composition preserves invalidity sequentially accumulating all errors.
public export
Semigroup e => Applicative (Validated e) where

M libs/contrib/Language/JSON/Data.idr => libs/contrib/Language/JSON/Data.idr +2 -1
@@ 56,7 56,8 @@ showChar c
         '\\' => "\\\\"
         '"'  => "\\\""
         c => if isControl c || c >= '\127'
                 then "\\u" ++ b16ToHexString (cast $ ord c)
                 then let hex = b16ToHexString (cast $ ord c)
                       in "\\u" ++ justifyRight 4 '0' hex
                 else singleton c

private

M libs/contrib/Language/JSON/String/Tokens.idr => libs/contrib/Language/JSON/String/Tokens.idr +11 -1
@@ 1,5 1,7 @@
module Language.JSON.String.Tokens

import Data.List
import Data.String
import Data.String.Extra
import Text.Token



@@ 48,7 50,15 @@ simpleEscapeValue x

private
unicodeEscapeValue : String -> Char
unicodeEscapeValue x = chr $ cast ("0x" ++ drop 2 x)
unicodeEscapeValue x = fromHex (drop 2 $ fastUnpack x) 0
  where hexVal : Char -> Int
        hexVal c = if c >= 'A'
                      then ord c - ord 'A' + 10
                      else ord c - ord '0'

        fromHex : List Char -> Int -> Char
        fromHex       [] acc = chr acc
        fromHex (h :: t) acc = fromHex t (hexVal h + 16 * acc)

public export
TokenKind JSONStringTokenKind where

A libs/contrib/System/Directory/Tree.idr => libs/contrib/System/Directory/Tree.idr +201 -0
@@ 0,0 1,201 @@
module System.Directory.Tree

import Data.DPair
import Data.List
import Data.Nat
import Data.Strings
import System.Directory
import System.Path

%default total

------------------------------------------------------------------------------
-- Filenames

||| A `Filename root` is anchored in `root`.
||| We use a `data` type so that Idris can easily infer `root` when passing
||| a `FileName` around. We do not use a `record` because we do not want to
||| allow users to manufacture their own `FileName`.
||| To get an absolute path, we need to append said filename to the root.
export
data FileName : Path -> Type where
  MkFileName : String -> FileName root

||| Project the string out of a `FileName`.
export
fileName : FileName root -> String
fileName (MkFileName str) = str

namespace FileName
  export
  toRelative : FileName root -> FileName (parse "")
  toRelative (MkFileName x) = MkFileName x

||| Convert a filename anchored in `root` to a filepath by appending the name
||| to the root path.
export
toFilePath : {root : Path} -> FileName root -> Path
toFilePath file = root /> fileName file

export
directoryExists : {root : Path} -> FileName root -> IO Bool
directoryExists fp = do
  Right dir <- openDir (show $ toFilePath fp)
    | Left _ => pure False
  closeDir dir
  pure True

------------------------------------------------------------------------------
-- Directory trees

||| A `Tree root` is the representation of a directory tree anchored in `root`.
||| Each directory contains a list of files and a list of subtrees waiting to be
||| explored. The fact these subtrees are IO-bound means the subtrees will be
||| lazily constructed on demand.
public export
SubTree : Path -> Type

public export
record Tree (root : Path) where
  constructor MkTree
  files    : List (FileName root)
  subTrees : List (SubTree root)

SubTree root = (dir : FileName root ** IO (Tree (root /> fileName dir)))

||| An empty tree contains no files and has no sub-directories.
export
emptyTree : Tree root
emptyTree = MkTree [] []

namespace Tree
  ||| No run time information is changed,
  ||| so we assert the identity.
  export
  toRelative : Tree root -> Tree (parse "")
  toRelative x = believe_me x

||| Filter out files and directories that do not satisfy a given predicate.
export
filter : (filePred, dirPred : {root : _} -> FileName root -> Bool) ->
         {root : _} -> Tree root -> Tree root
filter filePred dirPred (MkTree files dirs) = MkTree files' dirs' where

  files' : List (FileName root)
  files' = filter filePred files

  dirs' : List (SubTree root)
  dirs' = flip mapMaybe dirs $ \ (dname ** iot) => do
            guard (dirPred dname)
            pure (dname ** map (assert_total (filter filePred dirPred)) iot)

||| Sort the lists of files and directories using the given comparison functions
export
sortBy : (fileCmp, dirCmp : {root : _} -> FileName root -> FileName root -> Ordering) ->
         {root : _} -> Tree root -> Tree root
sortBy fileCmp dirCmp (MkTree files dirs) = MkTree files' dirs' where

  files' : List (FileName root)
  files' = sortBy fileCmp files

  dirs' : List (SubTree root)
  dirs' = sortBy (\ d1, d2 => dirCmp (fst d1) (fst d2))
        $ flip map dirs $ \ (dname ** iot) =>
          (dname ** map (assert_total (sortBy fileCmp dirCmp)) iot)

||| Sort the list of files and directories alphabetically
export
sort : {root : _} -> Tree root -> Tree root
sort = sortBy cmp cmp where

  cmp : {root : _} -> FileName root -> FileName root -> Ordering
  cmp a b = compare (fileName a) (fileName b)


||| Exploring a filesystem from a given root to produce a tree
export
explore : (root : Path) -> IO (Tree root)

go : {root : Path} -> Directory -> Tree root -> IO (Tree root)

explore root = do
  Right dir <- openDir (show root)
    | Left err => pure emptyTree
  assert_total (go dir emptyTree)

go dir acc = case !(dirEntry dir) of
  -- If there is no next entry then we are done and can return the accumulator.
  Left err => acc <$ closeDir dir
  -- Otherwise we have an entry and need to categorise it
  Right entry => do
    -- ignore aliases for current and parent directories
    let False = elem entry [".", ".."]
         | _ => assert_total (go dir acc)
    -- if the entry is a directory, add it to the (lazily explored)
    -- list of subdirectories
    let entry : FileName root = MkFileName entry
    let acc = if !(directoryExists entry)
                then { subTrees $= ((entry ** explore _) ::) } acc
                else { files    $= (entry                ::) } acc
    assert_total (go dir acc)

||| Depth first traversal of all of the files in a tree
export
covering
depthFirst : ({root : Path} -> FileName root -> Lazy (IO a) -> IO a) ->
             {root : Path} -> Tree root -> IO a -> IO a
depthFirst check t k =
  let next = foldr (\ (dir ** iot), def => depthFirst check !iot def) k t.subTrees in
  foldr (\ fn, def => check fn def) next t.files

||| Finding a file in a tree (depth first search)
export
covering
findFile : {root : Path} -> String -> Tree root -> IO (Maybe Path)
findFile needle t = depthFirst check t (pure Nothing) where

  check : {root : Path} -> FileName root ->
          Lazy (IO (Maybe Path)) -> IO (Maybe Path)
  check fn next = if fileName fn == needle
                    then pure (Just (toFilePath fn))
                    else next

||| Display a tree by printing it procedurally. Note that because directory
||| trees contain suspended computations corresponding to their subtrees this
||| has to be an `IO` function. We make it return Unit rather than a String
||| because we do not want to assume that the tree is finite.
export
covering
print : Tree root -> IO ()
print t = go [([], ".", Evidence root (pure t))] where

  -- This implementation is unadulterated black magic.
  -- Do NOT touch it if nothing is broken.

  padding : Bool -> List Bool -> String
  padding isDir = fastConcat . go [] where

    go : List String -> List Bool -> List String
    go acc [] = acc
    go acc (b :: bs) = go (hd :: acc) bs where
      hd : String
      hd = if isDir && isNil acc
           then if b then " ├ " else " └ "
           else if b then " │"  else "  "

  prefixes : Nat -> List Bool
  prefixes n = snoc (replicate (pred n) True) False

  covering
  go : List (List Bool, String, Exists (IO . Tree)) -> IO ()
  go [] = pure ()
  go ((bs, fn, Evidence _ iot) :: iots) = do
    t <- iot
    putStrLn (padding True bs ++ fn)
    let pad = padding False bs
    let pads = prefixes (length t.files + length t.subTrees)
    for_ (zip pads t.files) $ \ (b, fp) =>
      putStrLn (pad ++ (if b then " ├ " else " └ ") ++ fileName fp)
    let bss = map (:: bs) (prefixes (length t.subTrees))
    go (zipWith (\ bs, (dir ** iot) => (bs, fileName dir, Evidence _ iot)) bss t.subTrees)
    go iots

M libs/contrib/System/Path.idr => libs/contrib/System/Path.idr +23 -4
@@ 13,7 13,7 @@ import Text.Quantity

import System.Info

infixr 5 </>
infixr 5 </>, />
infixr 7 <.>




@@ 344,6 344,7 @@ setFileName' name path =
  else
    append' path (parse name)

export
splitFileName : String -> (String, String)
splitFileName name =
  case break (== '.') $ reverse $ unpack name of


@@ 384,11 385,28 @@ isRelative = not . isAbsolute
||| - If the right path has a volume but no root, it replaces left.
|||
||| ```idris example
||| parse "/usr" /> "local/etc" == "/usr/local/etc"
||| ```
export
(/>) : (left : Path) -> (right : String) -> Path
(/>) left right = append' left (parse right)

||| Appends the right path to the left path.
|||
||| If the path on the right is absolute, it replaces the left path.
|||
||| On Windows:
|||
||| - If the right path has a root but no volume (e.g., `\windows`), it replaces
|||   everything except for the volume (if any) of left.
||| - If the right path has a volume but no root, it replaces left.
|||
||| ```idris example
||| "/usr" </> "local/etc" == "/usr/local/etc"
||| ```
export
(</>) : (left : String) -> (right : String) -> String
(</>) left right = show $ append' (parse left) (parse right)
(</>) left right = show $ parse left /> right

||| Joins path components into one.
|||


@@ 397,7 415,7 @@ export
||| ```
export
joinPath : List String -> String
joinPath xs = foldl (</>) "" xs
joinPath xs = show $ foldl (/>) (parse "") xs

||| Splits path into components.
|||


@@ 505,7 523,8 @@ fileStem path = pure $ fst $ splitFileName !(fileName path)
||| - Otherwise, the portion of the file name after the last ".".
export
extension : String -> Maybe String
extension path = pure $ snd $ splitFileName !(fileName path)
extension path = fileName path >>=
  filter (/= "") . Just . snd . splitFileName

||| Updates the file name in the path.
|||

M libs/contrib/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr => libs/contrib/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr +1 -1
@@ 87,7 87,7 @@ fromStream sdoc = case sdocToTreeParser sdoc of
    flatten (STConcat [x, STEmpty]) = flatten x
    flatten (STConcat [x, STConcat xs]) = case flatten (STConcat xs) of
      (STConcat xs') => STConcat (x :: xs')
      y => y
      y => STConcat [x, y]
    flatten x = x

    internalError : SimpleDocTree ann

M libs/contrib/contrib.ipkg => libs/contrib/contrib.ipkg +10 -0
@@ 69,6 69,7 @@ modules = Control.ANSI,
          Data.Nat.Ack,
          Data.Nat.Division,
          Data.Nat.Equational,
          Data.Nat.Exponentiation,
          Data.Nat.Fact,
          Data.Nat.Factor,
          Data.Nat.Fib,


@@ 76,15 77,23 @@ modules = Control.ANSI,
          Data.Nat.Order.Properties,
          Data.Nat.Properties,

          Data.Num.Implementations,

          Data.OpenUnion,

          Data.Order,

          Data.Path,

          Data.Recursion.Free,

          Data.Rel.Complement,

          Data.SortedMap,
          Data.SortedSet,

          Data.Stream.Extra,

          Data.String.Extra,
          Data.String.Interpolation,
          Data.String.Iterator,


@@ 136,6 145,7 @@ modules = Control.ANSI,
          Syntax.PreorderReasoning.Generic,

          System.Console.GetOpt,
          System.Directory.Tree,
          System.Future,
          System.Random,
          System.Path,

M libs/network/Control/Linear/Network.idr => libs/network/Control/Linear/Network.idr +80 -46
@@ 2,6 2,9 @@ module Control.Linear.Network

-- An experimental linear type based API to sockets

import public Data.Either
import public Data.Maybe

import Control.Linear.LIO

import public Network.Socket.Data


@@ 10,16 13,42 @@ import Network.Socket
public export
data SocketState = Ready | Bound | Listening | Open | Closed

||| Define the domain of SocketState transitions.
||| Label every such transition.
public export
data Action : SocketState -> Type where
  Bind    : Action Ready
  Listen  : Action Bound
  Accept  : Action Listening
  Send    : Action Open
  Receive : Action Open
  Close   : Action st

export
data Socket : SocketState -> Type where
     MkSocket : Socket.Data.Socket -> Socket st

||| For every label of a SocketState transition
||| and a success value of the transition,
||| define its result.
public export
Next : (action : Action st)
    -> (success : Bool)
    -> Type
Next Bind    True  = Socket Bound
Next Listen  True  = Socket Listening
Next Accept  True  = LPair (Socket Listening) (Socket Open)
Next Send    True  = Socket Open
Next Receive True  = Socket Open
Next Close   True  = Socket Closed
Next _       False = Socket Closed

export
newSocket : LinearIO io
      => (fam  : SocketFamily)
      -> (ty   : SocketType)
      -> (pnum : ProtocolNumber)
      -> (success : (1 _ : Socket Ready) -> L io ())
      -> (success : (1 sock : Socket Ready) -> L io ())
      -> (fail : SocketError -> L io ())
      -> L io ()
newSocket fam ty pnum success fail


@@ 28,93 57,98 @@ newSocket fam ty pnum success fail
         success (MkSocket rawsock)

export
close : LinearIO io => (1 _ : Socket st) -> L io {use=1} (Socket Closed)
close : LinearIO io => (1 sock : Socket st) -> L1 io (Socket Closed)
close (MkSocket sock)
    = do Socket.close sock
         pure1 (MkSocket sock)

export
done : LinearIO io => (1 _ : Socket Closed) -> L io ()
done : LinearIO io => (1 sock : Socket Closed) -> L io ()
done (MkSocket sock) = pure ()

export
bind : LinearIO io =>
       (1 _ : Socket Ready) ->
       (1 sock : Socket Ready) ->
       (addr : Maybe SocketAddress) ->
       (port : Port) ->
       L io {use=1} (Res Bool (\res => Socket (case res of
                                                    False => Closed
                                                    True => Bound)))
       L1 io (Res (Maybe SocketError)
         (\res => Next Bind (isNothing res)))
bind (MkSocket sock) addr port
    = do ok <- Socket.bind sock addr port
         pure1 $ ok == 0 # MkSocket sock
    = do code <- Socket.bind sock addr port
         case code of
           0 =>
             pure1 $ Nothing # MkSocket sock
           err =>
             pure1 $ Just err # MkSocket sock

export
connect : LinearIO io =>
          (sock : Socket) ->
          (addr : SocketAddress) ->
          (port : Port) ->
          L io {use=1} (Res Bool (\res => Socket (case res of
                                                       False => Closed
                                                       True => Open)))
          L1 io (Res (Maybe SocketError)
            (\case Nothing => Socket Ready
                   Just _  => Socket Closed))
connect sock addr port
    = do ok <- Socket.connect sock addr port
         pure1 $ ok == 0 # MkSocket sock
    = do code <- Socket.connect sock addr port
         case code of
           0 =>
             pure1 $ Nothing # MkSocket sock
           err =>
             pure1 $ Just err # MkSocket sock

export
listen : LinearIO io =>
         (1 _ : Socket Bound) ->
         L io {use=1} (Res Bool (\res => Socket (case res of
                                                      False => Closed
                                                      True => Listening)))
         (1 sock : Socket Bound) ->
         L1 io (Res (Maybe SocketError)
           (\res => Next Listen (isNothing res)))
listen (MkSocket sock)
    = do ok <- Socket.listen sock
         pure1 $ ok == 0 # MkSocket sock
    = do code <- Socket.listen sock
         case code of
           0 =>
             pure1 $ Nothing # MkSocket sock
           err =>
             pure1 $ Just err # MkSocket sock


export
accept : LinearIO io =>
         (1 _ : Socket Listening) ->
         L io {use=1} (Res Bool (\case
                                    False => Socket Listening
                                    True => (Socket Listening, Socket Open)))
         (1 sock : Socket Listening) ->
         L1 io (Res (Maybe SocketError)
           (\res => Next Accept (isNothing res)))
accept (MkSocket sock)
    = do Right (sock', sockaddr) <- Socket.accept sock
             | Left err => pure1 (False # MkSocket sock)
         pure1 (True # (MkSocket sock, MkSocket sock'))
             | Left err => pure1 (Just err # MkSocket sock)
         pure1 (Nothing # (MkSocket sock # MkSocket sock'))

export
send : LinearIO io =>
       (1 _ : Socket Open) ->
       (1 sock : Socket Open) ->
       (msg : String) ->
       L io {use=1} (Res Bool (\res => Socket (case res of
                                                    False => Closed
                                                    True => Open)))
       L1 io (Res (Maybe SocketError)
         (\res => Next Send (isNothing res)))
send (MkSocket sock) msg
    = do Right c <- Socket.send sock msg
             | Left err => pure1 (False # MkSocket sock)
         pure1 (True # MkSocket sock)
             | Left err => pure1 (Just err # MkSocket sock)
         pure1 (Nothing # MkSocket sock)

export
recv : LinearIO io =>
       (1 _ : Socket Open) ->
       (1 sock : Socket Open) ->
       (len : ByteLength) ->
       L io {use=1} (Res (Maybe (String, ResultCode))
                         (\res => Socket (case res of
                                               Nothing => Closed
                                               Just msg => Open)))
       L1 io (Res (Either SocketError (String, ResultCode))
         (\res => Next Receive (isRight res)))
recv (MkSocket sock) len
    = do Right msg <- Socket.recv sock len
             | Left err => pure1 (Nothing # MkSocket sock)
         pure1 (Just msg # MkSocket sock)
             | Left err => pure1 (Left err # MkSocket sock)
         pure1 (Right msg # MkSocket sock)

export
recvAll : LinearIO io =>
          (1 _ : Socket Open) ->
          L io {use=1} (Res (Maybe String)
                            (\res => Socket (case res of
                                                  Nothing => Closed
                                                  Just msg => Open)))
          (1 sock : Socket Open) ->
          L1 io (Res (Either SocketError String)
            (\res => Next Receive (isRight res)))
recvAll (MkSocket sock)
    = do Right msg <- Socket.recvAll sock
             | Left err => pure1 (Nothing # MkSocket sock)
         pure1 (Just msg # MkSocket sock)
             | Left err => pure1 (Left err # MkSocket sock)
         pure1 (Right msg # MkSocket sock)

M libs/network/Network/FFI.idr => libs/network/Network/FFI.idr +4 -0
@@ 40,6 40,10 @@ prim__idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int
export
prim__idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String

%foreign "C:idrnet_sockaddr_unix,libidris2_support"
export
prim__idrnet_sockaddr_unix : (sockaddr : AnyPtr) -> PrimIO String

%foreign "C:idrnet_sockaddr_ipv4_port,libidris2_support"
export
prim__idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int

M libs/network/Network/Socket/Raw.idr => libs/network/Network/Socket/Raw.idr +1 -0
@@ 70,6 70,7 @@ getSockAddr (SAPtr ptr) = do

      pure $ parseIPv4 ipv4_addr
    Just AF_INET6 => pure IPv6Addr
    Just AF_UNIX => map Hostname $ primIO (prim__idrnet_sockaddr_unix ptr)
    Just AF_UNSPEC => pure InvalidAddress)

export

M libs/prelude/Prelude/Cast.idr => libs/prelude/Prelude/Cast.idr +4 -0
@@ 18,6 18,10 @@ interface Cast from to where
  ||| @ orig The original type
  cast : (orig : from) -> to

export
Cast a a where
  cast = id

-- To String

export

M libs/prelude/Prelude/Interfaces.idr => libs/prelude/Prelude/Interfaces.idr +41 -0
@@ 81,6 81,14 @@ public export
(<$>) : Functor f => (func : a -> b) -> f a -> f b
(<$>) func x = map func x

||| Flipped version of `<$>`, an infix alias for `map`, applying a function across
||| everything of type 'a' in a parameterised type.
||| @ f the parameterised type
||| @ func the function to apply
public export
(<&>) : Functor f => f a -> (func : a -> b) -> f b
(<&>) x func = map func x

||| Run something for effects, replacing the return value with a given parameter.
public export
(<$) : Functor f => b -> f a -> f b


@@ 372,6 380,19 @@ namespace Foldable
    foldl = foldl . foldl
    null tf = null tf || all (force . null) tf

||| `Bifoldable` identifies foldable structures with two different varieties
||| of elements (as opposed to `Foldable`, which has one variety of element).
||| Common examples are `Either` and `Pair`.
public export
interface Bifoldable p where
  bifoldr : (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc

  bifoldl : (acc -> a -> acc) -> (acc -> b -> acc) -> acc -> p a b -> acc
  bifoldl f g z t = bifoldr (flip (.) . flip f) (flip (.) . flip g) id t z

  binull : p a b -> Lazy Bool
  binull = bifoldr {acc = Lazy Bool} (\ _,_ => False) (\ _,_ => False) True

public export
interface (Functor t, Foldable t) => Traversable t where
  ||| Map each element of a structure to a computation, evaluate those


@@ 388,6 409,26 @@ public export
for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
for = flip traverse

public export
interface (Bifunctor p, Bifoldable p) => Bitraversable p where
  ||| Map each element of a structure to a computation, evaluate those
  ||| computations and combine the results.
  bitraverse : Applicative f => (a -> f c) -> (b -> f d) -> p a b -> f (p c d)

||| Evaluate each computation in a structure and collect the results.
public export
bisequence : (Bitraversable p, Applicative f) => p (f a) (f b) -> f (p a b)
bisequence = bitraverse id id

||| Like `bitraverse` but with the arguments flipped.
public export
bifor :  (Bitraversable p, Applicative f)
      => p a b
      -> (a -> f c)
      -> (b -> f d)
      -> f (p c d)
bifor t f g = bitraverse f g t

namespace Traversable
  ||| Composition of traversables is traversable.
  public export

M libs/prelude/Prelude/Ops.idr => libs/prelude/Prelude/Ops.idr +1 -1
@@ 13,7 13,7 @@ infixr 4 ||
infixr 7 ::, ++

-- Functor/Applicative/Monad/Algebra operators
infixl 1 >>=, =<<, >>, >=>, <=<
infixl 1 >>=, =<<, >>, >=>, <=<, <&>
infixr 2 <|>
infixl 3 <*>, *>, <*
infixr 4 <$>, $>, <$

M libs/prelude/Prelude/Show.idr => libs/prelude/Prelude/Show.idr +0 -5
@@ 155,11 155,6 @@ showLitChar c
           "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
           "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US"]

    getAt : Nat -> List String -> Maybe String
    getAt Z     (x :: xs) = Just x
    getAt (S k) (x :: xs) = getAt k xs
    getAt _     []        = Nothing

showLitString : List Char -> String -> String
showLitString []        = id
showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs

M libs/prelude/Prelude/Types.idr => libs/prelude/Prelude/Types.idr +36 -0
@@ 104,6 104,18 @@ Bifunctor Pair where

%inline
public export
Bifoldable Pair where
  bifoldr f g acc (x, y) = f x (g y acc)
  bifoldl f g acc (x, y) = g (f acc x) y
  binull _ = False

%inline
public export
Bitraversable Pair where
  bitraverse f g (a,b) = [| (,) (f a) (g b) |]

%inline
public export
Functor (Pair a) where
  map = mapSnd



@@ 274,6 286,23 @@ Bifunctor Either where

%inline
public export
Bifoldable Either where
  bifoldr f _ acc (Left a)  = f a acc
  bifoldr _ g acc (Right b) = g b acc

  bifoldl f _ acc (Left a)  = f acc a
  bifoldl _ g acc (Right b) = g acc b

  binull _ = False

%inline
public export
Bitraversable Either where
  bitraverse f _ (Left a)  = Left <$> f a
  bitraverse _ g (Right b) = Right <$> g b

%inline
public export
Applicative (Either e) where
  pure = Right



@@ 389,6 418,13 @@ elem : Eq a => a -> List a -> Bool
x `elem` [] = False
x `elem` (y :: ys) = x == y ||  elem x ys

||| Lookup a value at a given position
export
getAt : Nat -> List a -> Maybe a
getAt Z     (x :: xs) = Just x
getAt (S k) (x :: xs) = getAt k xs
getAt _     []        = Nothing

-------------
-- STREAMS --
-------------

M libs/test/Test/Golden.idr => libs/test/Test/Golden.idr +14 -7
@@ 240,9 240,11 @@ export
pathLookup : List String -> IO (Maybe String)
pathLookup names = do
  path <- getEnv "PATH"
  let extensions = if isWindows then [".exe", ".cmd", ".bat", ""] else [""]
  let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
  let candidates = [p ++ "/" ++ x | p <- pathList,
                                    x <- names]
  let candidates = [p ++ "/" ++ x ++ y | p <- pathList,
                                         x <- names,
                                         y <- extensions]
  firstExists candidates




@@ 262,17 264,22 @@ Show Requirement where
export
checkRequirement : Requirement -> IO (Maybe String)
checkRequirement req
  = do let (envvar, paths) = requirement req
       Just exec <- getEnv envvar | Nothing => pathLookup paths
       pure (Just exec)

  = if platformSupport req
      then do let (envvar, paths) = requirement req
              Just exec <- getEnv envvar | Nothing => pathLookup paths
              pure (Just exec)
      else pure Nothing
  where
    requirement : Requirement -> (String, List String)
    requirement C = ("CC", ["cc"])
    requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "scheme", "scheme.exe"])
    requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "scheme"])
    requirement Node = ("NODE", ["node"])
    requirement Racket = ("RACKET", ["racket"])
    requirement Gambit = ("GAMBIT", ["gsc"])
    platformSupport : Requirement -> Bool
    platformSupport C = not isWindows
    platformSupport Racket = not isWindows
    platformSupport _ = True

export
findCG : IO (Maybe String)

M nix/package.nix => nix/package.nix +5 -1
@@ 5,6 5,9 @@
, fetchFromGitHub
, makeWrapper
, idris2-version
, racket
, gambit
, nodejs
}:

# Uses scheme to bootstrap the build of idris2


@@ 28,7 31,8 @@ stdenv.mkDerivation rec {
  # The name of the main executable of pkgs.chez is `scheme`
  buildFlags = [ "bootstrap" "SCHEME=scheme" ];

  checkTarget = "test";
  checkInputs = [ gambit nodejs ]; # racket ];
  checkFlags = [ "INTERACTIVE=" ];

  # TODO: Move this into its own derivation, such that this can be changed
  #       without having to recompile idris2 every time.

M nix/test.nix => nix/test.nix +1 -0
@@ 42,3 42,4 @@ let
in
withTests testsTemplate templateBuildDefault
// withTests testsTemplateWithDeps templateBuildWithDeps
// { idris2Tests = idris.defaultPackage.${system}.overrideAttrs (a: { doCheck = true; }); }

M src/Compiler/Common.idr => src/Compiler/Common.idr +26 -9
@@ 1,5 1,6 @@
module Compiler.Common


import Compiler.ANF
import Compiler.CompileExpr
import Compiler.Inline


@@ 13,11 14,15 @@ import Core.Options
import Core.TT
import Core.TTC
import Libraries.Utils.Binary
import Libraries.Utils.Path

import Data.IOArray
import Data.List
import Data.List1
import Libraries.Data.NameMap
import Data.Strings
import Data.Strings as String

import Idris.Env

import System.Directory
import System.Info


@@ 86,7 91,7 @@ compile {c} cg tm out
         let outputDir = outputDirWithDefault d
         ensureDirectoryExists tmpDir
         ensureDirectoryExists outputDir
         logTime "Code generation overall" $
         logTime "+ Code generation overall" $
             compileExpr cg c tmpDir outputDir tm out

||| execute


@@ 261,7 266,7 @@ getCompileData doLazyAnnots phase tm_in
         -- to check than a NameMap!)
         asize <- getNextEntry
         arr <- coreLift $ newArray asize
         logTime "Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs
         logTime "++ Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs

         let entries = mapMaybe id !(coreLift (toList arr))
         let allNs = map (Resolved . fst) entries


@@ 271,9 276,9 @@ getCompileData doLazyAnnots phase tm_in
         -- unknown due to cyclic modules (i.e. declared in one, defined in
         -- another)
         rcns <- filterM nonErased cns
         logTime "Merge lambda" $ traverse_ mergeLamDef rcns
         logTime "Fix arity" $ traverse_ fixArityDef rcns
         logTime "Forget names" $ traverse_ mkForgetDef rcns
         logTime "++ Merge lambda" $ traverse_ mergeLamDef rcns
         logTime "++ Fix arity" $ traverse_ fixArityDef rcns
         logTime "++ Forget names" $ traverse_ mkForgetDef rcns

         compiledtm <- fixArityExp !(compileExp tm)
         let mainname = MN "__mainExpression" 0


@@ 281,17 286,17 @@ getCompileData doLazyAnnots phase tm_in

         namedefs <- traverse getNamedDef rcns
         lifted_in <- if phase >= Lifted
                         then logTime "Lambda lift" $ traverse (lambdaLift doLazyAnnots) rcns
                         then logTime "++ Lambda lift" $ traverse (lambdaLift doLazyAnnots) rcns
                         else pure []

         let lifted = (mainname, MkLFun [] [] liftedtm) ::
                      ldefs ++ concat lifted_in

         anf <- if phase >= ANF
                   then logTime "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
                   then logTime "++ Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
                   else pure []
         vmcode <- if phase >= VMCode
                      then logTime "Get VM Code" $ pure (allDefs anf)
                      then logTime "++ Get VM Code" $ pure (allDefs anf)
                      else pure []

         defs <- get Ctxt


@@ 432,3 437,15 @@ getExtraRuntime directives
      Right contents <- coreLift $ readFile p
        | Left err => throw (FileErr p err)
      pure contents

||| Looks up an executable from a list of candidate names in the PATH
export
pathLookup : List String -> IO (Maybe String)
pathLookup candidates
    = do path <- idrisGetEnv "PATH"
         let extensions = if isWindows then [".exe", ".cmd", ".bat", ""] else [""]
         let pathList = forget $ String.split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
         let candidates = [p ++ "/" ++ x ++ y | p <- pathList,
                                                x <- candidates,
                                                y <- extensions ]
         firstExists candidates

M src/Compiler/CompileExpr.idr => src/Compiler/CompileExpr.idr +129 -88
@@ 127,7 127,7 @@ mkDropSubst i es rest (x :: xs)
             then (vs ** DropCons sub)
             else (x :: vs ** KeepCons sub)

-- Rewrite applications of Nat constructors and functions to more optimal
-- Rewrite applications of Nat-like constructors and functions to more optimal
-- versions using Integer

-- None of these should be hard coded, but we'll do it this way until we


@@ 136,10 136,10 @@ mkDropSubst i es rest (x :: xs)
-- Common.idr, so that they get compiled, as they won't be spotted by the
-- usual calls to 'getRefs'.
data Magic : Type where
  MagicCCon : Namespace -> String -> (arity : Nat) -> -- checks
  MagicCCon : Name -> (arity : Nat) -> -- checks
              (FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> -- translation
              Magic
  MagicCRef : Namespace -> String -> (arity : Nat) -> -- checks
  MagicCRef : Name -> (arity : Nat) -> -- checks
              (FC -> FC -> forall vars. Vect arity (CExp vars) -> CExp vars) -> --translation
              Magic



@@ 148,11 148,11 @@ magic ms (CLam fc x exp) = CLam fc x (magic ms exp)
magic ms e = go ms e where

  fire : Magic -> CExp vars -> Maybe (CExp vars)
  fire (MagicCCon ns n arity f) (CCon fc (NS ns' (UN n')) _ es)
    = do guard (n == n' && ns == ns')
  fire (MagicCCon n arity f) (CCon fc n' _ es)
    = do guard (n == n')
         map (f fc) (toVect arity es)
  fire (MagicCRef ns n arity f) (CApp fc (CRef fc' (NS ns' (UN n'))) es)
    = do guard (n == n' && ns == ns')
  fire (MagicCRef n arity f) (CApp fc (CRef fc' n') es)
    = do guard (n == n')
         map (f fc fc') (toVect arity es)
  fire _ _ = Nothing



@@ 165,63 165,99 @@ magic ms e = go ms e where
natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
natMinus fc fc' [m,n] = CApp fc (CRef fc' (UN "prim__sub_Integer")) [m, n]

natHack : CExp vars -> CExp vars
natHack = magic
    [ MagicCCon typesNS "Z" 0
         (\ fc, [] => CPrimVal fc (BI 0))
    , MagicCCon typesNS "S" 1
         (\ fc, [k] => CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k])
    , MagicCRef typesNS "natToInteger" 1
-- TODO: next release remove this and use %builtin pragma
natHack : List Magic
natHack =
    [ MagicCRef (NS typesNS (UN "natToInteger")) 1
         (\ _, _, [k] => k)
    , MagicCRef typesNS "integerToNat" 1
    , MagicCRef (NS typesNS (UN "integerToNat")) 1
         (\ fc, fc', [k] => CApp fc (CRef fc' (NS typesNS (UN "prim__integerToNat"))) [k])
    , MagicCRef typesNS "plus" 2
    , MagicCRef (NS typesNS (UN "plus")) 2
         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n])
    , MagicCRef typesNS "mult" 2
    , MagicCRef (NS typesNS (UN "mult")) 2
         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__mul_Integer")) [m, n])
    , MagicCRef natNS "minus" 2 natMinus
    , MagicCRef (NS natNS (UN "minus")) 2 natMinus
    ]


isNatCon : Name -> Bool
isNatCon (NS ns (UN n))
   = (n == "Z" || n == "S") && ns == typesNS
isNatCon _ = False

natBranch : CConAlt vars -> Bool
natBranch (MkConAlt n _ _ _) = isNatCon n

trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
trySBranch n (MkConAlt (NS ns (UN nm)) _ [arg] sc)
  = do guard (nm == "S" && ns == typesNS)
-- get all transformation from %builtin pragmas
builtinMagic : Ref Ctxt Defs => Core (forall vars. CExp vars -> CExp vars)
builtinMagic = do
    defs <- get Ctxt
    let b = defs.builtinTransforms
    let nats = concatMap builtinMagicNat $ values $ natTyNames b
    pure $ magic $ natHack ++ nats
  where
    builtinMagicNat : NatBuiltin -> List Magic
    builtinMagicNat cons =
        [ MagicCCon cons.zero 0
             (\ fc, [] => CPrimVal fc (BI 0))
        , MagicCCon cons.succ 1
             (\ fc, [k] => CApp fc (CRef fc (UN "prim__add_Integer")) [CPrimVal fc (BI 1), k])
        ] -- TODO: add builtin pragmas for Nat related functions (to/from Integer, add, mult, minus, compare)

isNatCon : (zeroMap : NameMap ZERO) ->
           (succMap : NameMap SUCC) ->
           Name -> Bool
isNatCon zs ss n = isJust (lookup n zs) || isJust (lookup n ss)

natBranch : (zeroMap : NameMap ZERO) ->
           (succMap : NameMap SUCC) ->
           CConAlt vars -> Bool
natBranch zs ss (MkConAlt n _ _ _) = isNatCon zs ss n

trySBranch :
    (succMap : NameMap SUCC) ->
    CExp vars ->
    CConAlt vars ->
    Maybe (CExp vars)
trySBranch ss n (MkConAlt nm _ [arg] sc)
  = do guard $ isJust $ lookup nm ss
       let fc = getFC n
       pure (CLet fc arg True (natMinus fc fc [n, CPrimVal fc (BI 1)]) sc)
trySBranch _ _ = Nothing

tryZBranch : CConAlt vars -> Maybe (CExp vars)
tryZBranch (MkConAlt (NS ns (UN n)) _ [] sc)
   = do guard (n == "Z" && ns == typesNS)
trySBranch _ _ _ = Nothing

tryZBranch :
    (zeroMap : NameMap ZERO) ->
    CConAlt vars ->
    Maybe (CExp vars)
tryZBranch zs (MkConAlt n _ [] sc)
   = do guard $ isJust $ lookup n zs
        pure sc
tryZBranch _ = Nothing

getSBranch : CExp vars -> List (CConAlt vars) -> Maybe (CExp vars)
getSBranch n [] = Nothing
getSBranch n (x :: xs) = trySBranch n x <+> getSBranch n xs

getZBranch : List (CConAlt vars) -> Maybe (CExp vars)
getZBranch [] = Nothing
getZBranch (x :: xs) = tryZBranch x <+> getZBranch xs
tryZBranch _ _ = Nothing

getSBranch :
    (succMap : NameMap SUCC) ->
    CExp vars ->
    List (CConAlt vars) ->
    Maybe (CExp vars)
getSBranch ss n [] = Nothing
getSBranch ss n (x :: xs) = trySBranch ss n x <+> getSBranch ss n xs

getZBranch :
    (zeroMap : NameMap ZERO) ->
    List (CConAlt vars) ->
    Maybe (CExp vars)
getZBranch zs [] = Nothing
getZBranch zs (x :: xs) = tryZBranch zs x <+> getZBranch zs xs

-- Rewrite case trees on Nat to be case trees on Integer
natHackTree : CExp vars -> CExp vars
natHackTree (CConCase fc sc alts def)
   = if any natBranch alts
builtinNatTree' : (zeroMap : NameMap ZERO) ->
                  (succMap : NameMap SUCC) ->
                  CExp vars -> CExp vars
builtinNatTree' zs ss (CConCase fc sc alts def)
   = if any (natBranch zs ss) alts
        then let defb = maybe (CCrash fc "Nat case not covered") id def
                 scase = maybe defb id (getSBranch sc alts)
                 zcase = maybe defb id (getZBranch alts) in
                 scase = maybe defb id (getSBranch ss sc alts)
                 zcase = maybe defb id (getZBranch zs alts) in
                 CConstCase fc sc [MkConstAlt (BI 0) zcase] (Just scase)
        else CConCase fc sc alts def
natHackTree t = t
builtinNatTree' zs ss t = t

builtinNatTree : Ref Ctxt Defs => Core (CExp vars -> CExp vars)
builtinNatTree = do
    defs <- get Ctxt
    let b = defs.builtinTransforms
    pure $ builtinNatTree' b.natZNames b.natSNames

-- Rewrite case trees on Bool/Ord to be case trees on Integer
-- TODO: Generalise to all finite enumerations


@@ 248,71 284,75 @@ boolHackTree t = t
mutual
  toCExpTm : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             Name -> Term vars -> Core (CExp vars)
  toCExpTm n (Local fc _ _ prf)
             (magic : forall vars. CExp vars -> CExp vars) ->
             Name -> Term vars ->
             Core (CExp vars)
  toCExpTm m n (Local fc _ _ prf)
      = pure $ CLocal fc prf
  -- TMP HACK: extend this to all types which look like enumerations after erasure
  toCExpTm n (Ref fc (DataCon tag arity) fn)
  toCExpTm m n (Ref fc (DataCon tag arity) fn)
      = if arity == Z && isFiniteEnum fn
        then pure $ CPrimVal fc (I tag)
        else -- get full name for readability, and the Nat hack
        else -- get full name for readability, and %builtin Natural
             pure $ CCon fc !(getFullName fn) (Just tag) []
  toCExpTm n (Ref fc (TyCon tag arity) fn)
  toCExpTm m n (Ref fc (TyCon tag arity) fn)
      = pure $ CCon fc fn Nothing []
  toCExpTm n (Ref fc _ fn)
  toCExpTm m n (Ref fc _ fn)
      = do full <- getFullName fn
               -- ^ For readability of output code, and the Nat hack,
           pure $ CApp fc (CRef fc full) []
  toCExpTm n (Meta fc mn i args)
      = pure $ CApp fc (CRef fc mn) !(traverse (toCExp n) args)
  toCExpTm n (Bind fc x (Lam _ _ _ _) sc)
      = pure $ CLam fc x !(toCExp n sc)
  toCExpTm n (Bind fc x (Let _ rig val _) sc)
      = do sc' <- toCExp n sc
  toCExpTm m n (Meta fc mn i args)
      = pure $ CApp fc (CRef fc mn) !(traverse (toCExp m n) args)
  toCExpTm m n (Bind fc x (Lam _ _ _ _) sc)
      = pure $ CLam fc x !(toCExp m n sc)
  toCExpTm m n (Bind fc x (Let _ rig val _) sc)
      = do sc' <- toCExp m n sc
           pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
                          (CLet fc x True !(toCExp n val) sc')
                          (CLet fc x True !(toCExp m n val) sc')
                          rig
  toCExpTm n (Bind fc x (Pi _ c e ty) sc)
      = pure $ CCon fc (UN "->") Nothing [!(toCExp n ty),
                                    CLam fc x !(toCExp n sc)]
  toCExpTm n (Bind fc x b tm) = pure $ CErased fc
  toCExpTm m n (Bind fc x (Pi _ c e ty) sc)
      = pure $ CCon fc (UN "->") Nothing [!(toCExp m n ty),
                                    CLam fc x !(toCExp m n sc)]
  toCExpTm m n (Bind fc x b tm) = pure $ CErased fc
  -- We'd expect this to have been dealt with in toCExp, but for completeness...
  toCExpTm n (App fc tm arg)
      = pure $ CApp fc !(toCExp n tm) [!(toCExp n arg)]
  toCExpTm m n (App fc tm arg)
      = pure $ CApp fc !(toCExp m n tm) [!(toCExp m n arg)]
  -- This shouldn't be in terms any more, but here for completeness
  toCExpTm n (As _ _ _ p) = toCExpTm n p
  toCExpTm m n (As _ _ _ p) = toCExpTm m n p
  -- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase
  toCExpTm n (TDelayed fc _ _) = pure $ CErased fc
  toCExpTm n (TDelay fc lr _ arg)
      = pure (CDelay fc lr !(toCExp n arg))
  toCExpTm n (TForce fc lr arg)
      = pure (CForce fc lr !(toCExp n arg))
  toCExpTm n (PrimVal fc c)
  toCExpTm m n (TDelayed fc _ _) = pure $ CErased fc
  toCExpTm m n (TDelay fc lr _ arg)
      = pure (CDelay fc lr !(toCExp m n arg))
  toCExpTm m n (TForce fc lr arg)
      = pure (CForce fc lr !(toCExp m n arg))
  toCExpTm m n (PrimVal fc c)
      = let t = constTag c in
            if t == 0
               then pure $ CPrimVal fc c
               else pure $ CCon fc (UN (show c)) Nothing []
  toCExpTm n (Erased fc _) = pure $ CErased fc
  toCExpTm n (TType fc) = pure $ CCon fc (UN "Type") Nothing []
  toCExpTm m n (Erased fc _) = pure $ CErased fc
  toCExpTm m n (TType fc) = pure $ CCon fc (UN "Type") Nothing []

  toCExp : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           Name -> Term vars -> Core (CExp vars)
  toCExp n tm
           (magic : forall vars. CExp vars -> CExp vars) ->
           Name -> Term vars ->
           Core (CExp vars)
  toCExp m n tm
      = case getFnArgs tm of
             (f, args) =>
                do args' <- traverse (toCExp n) args
                do args' <- traverse (toCExp m n) args
                   defs <- get Ctxt
                   f' <- toCExpTm n f
                   f' <- toCExpTm m n f
                   Arity a <- numArgs defs f
                      | NewTypeBy arity pos =>
                            do let res = applyNewType arity pos f' args'
                               pure $ natHack res
                               pure $ m res
                      | EraseArgs arity epos =>
                            do let res = eraseConArgs arity epos f' args'
                               pure $ natHack res
                               pure $ m res
                   let res = expandToArity a f' args'
                   pure $ natHack res
                   pure $ m res

mutual
  conCases : {vars : _} ->


@@ 448,7 488,7 @@ mutual
               def <- getDef n alts
               if isNil cases
                  then pure (fromMaybe (CErased fc) def)
                  else pure $ boolHackTree $ natHackTree $
                  else pure $ boolHackTree $ !builtinNatTree $
                            CConCase fc (CLocal fc x) cases def
  toCExpTree' n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
      = throw (InternalError "Unexpected DelayCase")


@@ 463,7 503,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 !builtinMagic n tm
  toCExpTree' n (Unmatched msg)
      = pure $ CCrash emptyFC msg
  toCExpTree' n Impossible


@@ 658,7 698,8 @@ export
compileExp : {auto c : Ref Ctxt Defs} ->
             ClosedTerm -> Core (CExp [])
compileExp tm
    = do exp <- toCExp (UN "main") tm
    = do m <- builtinMagic
         exp <- toCExp m (UN "main") tm
         pure exp

||| Given a name, look up an expression, and compile it to a CExp in the environment

M src/Compiler/ES/Node.idr => src/Compiler/ES/Node.idr +7 -4
@@ 17,9 17,11 @@ import System.File
import Data.Maybe

findNode : IO String
findNode =
  do env <- idrisGetEnv "NODE"
     pure $ fromMaybe "/usr/bin/env node" env
findNode = do
   Nothing <- idrisGetEnv "NODE"
      | Just node => pure node
   path <- pathLookup ["node"]
   pure $ fromMaybe "/usr/bin/env node" path

||| Compile a TT expression to Node
compileToNode : Ref Ctxt Defs ->


@@ 45,7 47,8 @@ executeExpr c tmpDir tm
     Right () <- coreLift $ writeFile outn js
        | Left err => throw (FileErr outn err)
     node <- coreLift findNode
     coreLift_ $ system (node ++ " " ++ outn)
     quoted_node <- pure $ "\"" ++ node ++ "\"" -- Windows often have a space in the path.
     coreLift_ $ system (quoted_node ++ " " ++ outn)
     pure ()

||| Codegen wrapper for Node implementation.

M src/Compiler/LambdaLift.idr => src/Compiler/LambdaLift.idr +180 -11
@@ 158,6 158,61 @@ unload fc _ f [] = pure f
-- only outermost LApp must be lazy as rest will be closures
unload fc lazy f (a :: as) = unload fc Nothing (LApp fc lazy f a) as

record Used (vars : List Name) where
  constructor MkUsed
  used : Vect (length vars) Bool

initUsed : {vars : _} -> Used vars
initUsed {vars} = MkUsed (replicate (length vars) False)

lengthDistributesOverAppend
  : (xs, ys : List a)
  -> length (xs ++ ys) = length xs + length ys
lengthDistributesOverAppend [] ys = Refl
lengthDistributesOverAppend (x :: xs) ys =
  cong S $ lengthDistributesOverAppend xs ys

weakenUsed : {outer : _} -> Used vars -> Used (outer ++ vars)
weakenUsed {outer} (MkUsed xs) =
  MkUsed (rewrite lengthDistributesOverAppend outer vars in
         (replicate (length outer) False ++ xs))

contractUsed : (Used (x::vars)) -> Used vars
contractUsed (MkUsed xs) = MkUsed (tail xs)

contractUsedMany : {remove : _} ->
                   (Used (remove ++ vars)) ->
                   Used vars
contractUsedMany {remove=[]} x = x
contractUsedMany {remove=(r::rs)} x = contractUsedMany {remove=rs} (contractUsed x)

markUsed : {vars : _} ->
           (idx : Nat) ->
           {0 prf : IsVar x idx vars} ->
           Used vars ->
           Used vars
markUsed {vars} {prf} idx (MkUsed us) =
  let newUsed = replaceAt (finIdx prf) True us in
  MkUsed newUsed
    where
    finIdx : {vars : _} -> {idx : _} ->
               (0 prf : IsVar x idx vars) ->
               Fin (length vars)
    finIdx {idx=Z} First = FZ
    finIdx {idx=S x} (Later l) = FS (finIdx l)

getUnused : Used vars ->
            Vect (length vars) Bool
getUnused (MkUsed uv) = map not uv

total
dropped : (vars : List Name) ->
          (drop : Vect (length vars) Bool) ->
          List Name
dropped [] _ = []
dropped (x::xs) (False::us) = x::(dropped xs us)
dropped (x::xs) (True::us) = dropped xs us

mutual
  makeLam : {auto l : Ref Lifts LDefs} ->
            {vars : _} ->


@@ 168,24 223,27 @@ mutual
  makeLam fc bound (CLam _ x sc') = makeLam fc {doLazyAnnots} {lazy} (x :: bound) sc'
  makeLam {vars} fc bound sc
      = do scl <- liftExp {doLazyAnnots} {lazy} sc
           -- Find out which variables aren't used in the new definition, and
           -- do not abstract over them in the new definition.
           let scUsedL = usedVars initUsed scl
               unusedContracted = contractUsedMany {remove=bound} scUsedL
               unused = getUnused unusedContracted
               scl' = dropUnused {outer=bound} unused scl
           n <- genName
           ldefs <- get Lifts
           put Lifts (record { defs $= ((n, MkLFun vars bound scl) ::) } ldefs)
           -- TODO: an optimisation here would be to spot which variables
           -- aren't used in the new definition, and not abstract over them
           -- in the new definition. Given that we have to do some messing
           -- about with indices anyway, it's probably not costly to do.
           pure $ LUnderApp fc n (length bound) (allVars fc vars)
           put Lifts (record { defs $= ((n, MkLFun (dropped vars unused) bound scl') ::) } ldefs)
           pure $ LUnderApp fc n (length bound) (allVars fc vars unused)
    where
        allPrfs : (vs : List Name) -> List (Var vs)
        allPrfs [] = []
        allPrfs (v :: vs) = MkVar First :: map weaken (allPrfs vs)
        allPrfs : (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Var vs)
        allPrfs [] _ = []
        allPrfs (v :: vs) (False::uvs) = MkVar First :: map weaken (allPrfs vs uvs)
        allPrfs (v :: vs) (True::uvs) = map weaken (allPrfs vs uvs)

        -- apply to all the variables. 'First' will be first in the last, which
        -- is good, because the most recently bound name is the first argument to
        -- the resulting function
        allVars : FC -> (vs : List Name) -> List (Lifted vs)
        allVars fc vs = map (\ (MkVar p) => LLocal fc p) (allPrfs vs)
        allVars : FC -> (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Lifted vs)
        allVars fc vs unused = map (\ (MkVar p) => LLocal fc p) (allPrfs vs unused)

-- if doLazyAnnots = True then annotate function application with laziness
-- otherwise use old behaviour (thunk is a function)


@@ 234,6 292,117 @@ mutual
  liftExp (CErased fc) = pure $ LErased fc
  liftExp (CCrash fc str) = pure $ LCrash fc str

  usedVars : {vars : _} ->
             {auto l : Ref Lifts LDefs} ->
             Used vars ->
             Lifted vars ->
             Used vars
  usedVars used (LLocal {idx} fc prf) =
    markUsed {prf} idx used
  usedVars used (LAppName fc lazy n args) =
    foldl (usedVars {vars}) used args
  usedVars used (LUnderApp fc n miss args) =
    foldl (usedVars {vars}) used args
  usedVars used (LApp fc lazy c arg) =
    usedVars (usedVars used arg) c
  usedVars used (LLet fc x val sc) =
    let innerUsed = contractUsed $ usedVars (weakenUsed {outer=[x]} used) sc in
        usedVars innerUsed val
  usedVars used (LCon fc n tag args) =
    foldl (usedVars {vars}) used args
  usedVars used (LOp fc lazy fn args) =
    foldl (usedVars {vars}) used args
  usedVars used (LExtPrim fc lazy fn args) =
    foldl (usedVars {vars}) used args
  usedVars used (LConCase fc sc alts def) =
      let defUsed = maybe used (usedVars used {vars}) def
          scDefUsed = usedVars defUsed sc in
          foldl usedConAlt scDefUsed alts
    where
      usedConAlt : {default Nothing lazy : Maybe LazyReason} ->
                   Used vars -> LiftedConAlt vars -> Used vars
      usedConAlt used (MkLConAlt n tag args sc) =
        contractUsedMany {remove=args} (usedVars (weakenUsed used) sc)

  usedVars used (LConstCase fc sc alts def) =
      let defUsed = maybe used (usedVars used {vars}) def
          scDefUsed = usedVars defUsed sc in
          foldl usedConstAlt scDefUsed alts
    where
      usedConstAlt : {default Nothing lazy : Maybe LazyReason} ->
                     Used vars -> LiftedConstAlt vars -> Used vars
      usedConstAlt used (MkLConstAlt c sc) = usedVars used sc

  usedVars used (LPrimVal _ _) = used
  usedVars used (LErased _) = used
  usedVars used (LCrash _ _) = used

  dropIdx : {vars : _} ->
            {idx : _} ->
            (outer : List Name) ->
            (unused : Vect (length vars) Bool) ->
            (0 p : IsVar x idx (outer ++ vars)) ->
            Var (outer ++ (dropped vars unused))
  dropIdx [] (False::_) First = MkVar First
  dropIdx [] (True::_) First = assert_total $
    idris_crash "INTERNAL ERROR: Referenced variable marked as unused"
  dropIdx [] (False::rest) (Later p) = Var.later $ dropIdx [] rest p
  dropIdx [] (True::rest) (Later p) = dropIdx [] rest p
  dropIdx (_::xs) unused First = MkVar First
  dropIdx (_::xs) unused (Later p) = Var.later $ dropIdx xs unused p

  dropUnused : {vars : _} ->
               {auto l : Ref Lifts LDefs} ->
               {outer : List Name} ->
               (unused : Vect (length vars) Bool) ->
               (l : Lifted (outer ++ vars)) ->
               Lifted (outer ++ (dropped vars unused))
  dropUnused _ (LPrimVal fc val) = LPrimVal fc val
  dropUnused _ (LErased fc) = LErased fc
  dropUnused _ (LCrash fc msg) = LCrash fc msg
  dropUnused {outer} unused (LLocal fc p) =
    let (MkVar p') = dropIdx outer unused p in LLocal fc p'
  dropUnused unused (LCon fc n tag args) =
    let args' = map (dropUnused unused) args in
        LCon fc n tag args'
  dropUnused {outer} unused (LLet fc n val sc) =
    let val' = dropUnused unused val
        sc' = dropUnused {outer=n::outer} (unused) sc in
        LLet fc n val' sc'
  dropUnused unused (LApp fc lazy c arg) =
    let c' = dropUnused unused c
        arg' = dropUnused unused arg in
        LApp fc lazy c' arg'
  dropUnused unused (LOp fc lazy fn args) =
    let args' = map (dropUnused unused) args in
        LOp fc lazy fn args'
  dropUnused unused (LExtPrim fc lazy n args) =
    let args' = map (dropUnused unused) args in
        LExtPrim fc lazy n args'
  dropUnused unused (LAppName fc lazy n args) =
    let args' = map (dropUnused unused) args in
        LAppName fc lazy n args'
  dropUnused unused (LUnderApp fc n miss args) =
    let args' = map (dropUnused unused) args in
        LUnderApp fc n miss args'
  dropUnused {vars} {outer} unused (LConCase fc sc alts def) =
    let alts' = map dropConCase alts in
        LConCase fc (dropUnused unused sc) alts' (map (dropUnused unused) def)
    where
      dropConCase : LiftedConAlt (outer ++ vars) ->
                    LiftedConAlt (outer ++ (dropped vars unused))
      dropConCase (MkLConAlt n t args sc) =
        let sc' = (rewrite sym $ appendAssociative args outer vars in sc)
            droppedSc = dropUnused {vars=vars} {outer=args++outer} unused sc' in
        MkLConAlt n t args (rewrite appendAssociative args outer (dropped vars unused) in droppedSc)
  dropUnused {vars} {outer} unused (LConstCase fc sc alts def) =
    let alts' = map dropConstCase alts in
        LConstCase fc (dropUnused unused sc) alts' (map (dropUnused unused) def)
    where
      dropConstCase : LiftedConstAlt (outer ++ vars) ->
                      LiftedConstAlt (outer ++ (dropped vars unused))
      dropConstCase (MkLConstAlt c val) = MkLConstAlt c (dropUnused unused val)

export
liftBody : {vars : _} -> {doLazyAnnots : Bool} ->
           Name -> CExp vars -> Core (Lifted vars, List (Name, LiftedDef))

A src/Compiler/RefC/CC.idr => src/Compiler/RefC/CC.idr +74 -0
@@ 0,0 1,74 @@
module Compiler.RefC.CC

import Core.Context
import Core.Context.Log
import Core.Options

import System

import Idris.Version
import Libraries.Utils.Path

findCC : IO String
findCC
    = do Nothing <- getEnv "IDRIS2_CC"
           | Just cc => pure cc
         Nothing <- getEnv "CC"
           | Just cc => pure cc
         pure "cc"

fullprefix_dir : Dirs -> String -> String
fullprefix_dir dirs sub
    = prefix_dir dirs </> "idris2-" ++ showVersion False version </> sub

export
compileCObjectFile : {auto c : Ref Ctxt Defs}
                  -> {default False asLibrary : Bool}
                  -> (sourceFile : String)
                  -> (objectFile : String)
                  -> Core (Maybe String)
compileCObjectFile {asLibrary} sourceFile objectFile =
  do cc <- coreLift findCC
     dirs <- getDirs

     let libraryFlag = if asLibrary then "-fpic " else ""

     let runccobj = cc ++ " -c " ++ libraryFlag ++ sourceFile ++
                       " -o " ++ objectFile ++ " " ++
                       "-I" ++ fullprefix_dir dirs "refc " ++
                       "-I" ++ fullprefix_dir dirs "include"

     log "compiler.refc.cc" 10 runccobj
     0 <- coreLift $ system runccobj
       | _ => pure Nothing

     pure (Just objectFile)

export
compileCFile : {auto c : Ref Ctxt Defs}
            -> {default False asShared : Bool}
            -> (objectFile : String)
            -> (outFile : String)
            -> Core (Maybe String)
compileCFile {asShared} objectFile outFile =
  do cc <- coreLift findCC
     dirs <- getDirs

     let sharedFlag = if asShared then "-shared " else ""

     let runcc = cc ++ " " ++ sharedFlag ++ objectFile ++
                       " -o " ++ outFile ++ " " ++
                       fullprefix_dir dirs "lib" </> "libidris2_support.a" ++ " " ++
                       "-lidris2_refc " ++
                       "-L" ++ fullprefix_dir dirs "refc " ++
                       clibdirs (lib_dirs dirs)

     log "compiler.refc.cc" 10 runcc
     0 <- coreLift $ system runcc
       | _ => pure Nothing

     pure (Just outFile)

  where
    clibdirs : List String -> String
    clibdirs ds = concat (map (\d => "-L" ++ d ++ " ") ds)

M src/Compiler/RefC/RefC.idr => src/Compiler/RefC/RefC.idr +32 -61
@@ 1,42 1,27 @@
module Compiler.RefC.RefC

import Compiler.RefC.CC

import Compiler.Common
import Compiler.CompileExpr
import Compiler.LambdaLift
import Compiler.ANF
import Compiler.Inline

import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Name
import Core.Options
import Core.TT

import Data.IORef
import Data.List
import Libraries.Data.DList
import Libraries.Data.NameMap
import Data.Nat
import Data.Strings
import Data.Vect

import System
import System.Info
import System.File

import Idris.Env
import Idris.Version
import Libraries.Utils.Hex
import Libraries.Utils.Path

findCC : IO String
findCC
    = do Nothing <- idrisGetEnv "IDRIS2_CC"
           | Just cc => pure cc
         Nothing <- idrisGetEnv "CC"
           | Just cc => pure cc
         pure "cc"

showcCleanStringChar : Char -> String -> String
showcCleanStringChar '+' = ("_plus" ++)
showcCleanStringChar '-' = ("__" ++)


@@ 1011,7 996,8 @@ createCFunctions n (MkAError exp) = do
    pure ()


header : {auto f : Ref FunctionDefinitions (List String)}
header : {auto c : Ref Ctxt Defs}
      -> {auto f : Ref FunctionDefinitions (List String)}
      -> {auto o : Ref OutfileText Output}
      -> {auto il : Ref IndentLevel Nat}
      -> {auto e : Ref ExternalLibs (List String)}


@@ 1022,7 1008,7 @@ header = do
                    , "#include <idris_support.h> // for libidris2_support"]
    extLibs <- get ExternalLibs
    let extLibLines = map (\lib => "// add header(s) for library: " ++ lib ++ "\n") extLibs
    traverse_ (\l => coreLift (putStrLn $ " header for " ++ l ++ " needed")) extLibs
    traverse_ (\l => log "compiler.refc" 20 $ " header for " ++ l ++ " needed") extLibs
    fns <- get FunctionDefinitions
    update OutfileText (appendL (initLines ++ extLibLines ++ ["\n// function definitions"] ++ fns))



@@ 1044,6 1030,27 @@ executeExpr c _ tm
         coreLift_ $ system "false"

export
generateCSourceFile : {auto c : Ref Ctxt Defs}
                   -> List (Name, ANFDef)
                   -> (outn : String)
                   -> Core ()
generateCSourceFile defs outn =
  do _ <- newRef ArgCounter 0
     _ <- newRef FunctionDefinitions []
     _ <- newRef TemporaryVariableTracker []
     _ <- newRef OutfileText DList.Nil
     _ <- newRef ExternalLibs []
     _ <- newRef IndentLevel 0
     traverse_ (uncurry createCFunctions) defs
     header -- added after the definition traversal in order to add all encountered function defintions
     footer
     fileContent <- get OutfileText
     let code = fastAppend (map (++ "\n") (reify fileContent))

     coreLift_ $ writeFile outn code
     log "compiler.refc" 10 $ "Generated C file " ++ outn

export
compileExpr : UsePhase
           -> Ref Ctxt Defs
           -> (tmpDir : String)


@@ 1055,52 1062,16 @@ compileExpr ANF c _ outputDir tm outfile =
  do let outn = outputDir </> outfile ++ ".c"
     let outobj = outputDir </> outfile ++ ".o"
     let outexec = outputDir </> outfile

     coreLift_ $ mkdirAll outputDir
     cdata <- getCompileData False ANF tm
     let defs = anf cdata
     _ <- newRef ArgCounter 0
     _ <- newRef FunctionDefinitions []
     _ <- newRef TemporaryVariableTracker []
     _ <- newRef OutfileText DList.Nil
     _ <- newRef ExternalLibs []
     _ <- newRef IndentLevel 0
     traverse_ (\(n, d) => createCFunctions n d) defs
     header -- added after the definition traversal in order to add all encountered function defintions
     footer
     fileContent <- get OutfileText
     let code = fastAppend (map (++ "\n") (reify fileContent))

     coreLift_ $ writeFile outn code
     coreLift_ $ putStrLn $ "Generated C file " ++ outn

     cc <- coreLift findCC
     dirs <- getDirs

     let runccobj = cc ++ " -c " ++ outn ++ " -o " ++ outobj ++ " " ++
                       "-I" ++ fullprefix_dir dirs "refc " ++
                       "-I" ++ fullprefix_dir dirs "include"

     let runcc = cc ++ " " ++ outobj ++ " -o " ++ outexec ++ " " ++
                       fullprefix_dir dirs "lib" </> "libidris2_support.a" ++ " " ++
                       "-lidris2_refc " ++
                       "-L" ++ fullprefix_dir dirs "refc " ++
                       clibdirs (lib_dirs dirs)

     coreLift $ putStrLn runccobj
     0 <- coreLift $ system runccobj
       | _ => pure Nothing
     coreLift $ putStrLn runcc
     0 <- coreLift $ system runcc
       | _ => pure Nothing
     pure (Just outexec)

  where
    fullprefix_dir : Dirs -> String -> String
    fullprefix_dir dirs sub
        = prefix_dir dirs </> "idris2-" ++ showVersion False version </> sub
     generateCSourceFile defs outn
     Just _ <- compileCObjectFile outn outobj
       | Nothing => pure Nothing
     compileCFile outobj outexec

    clibdirs : List String -> String
    clibdirs ds = concat (map (\d => "-L" ++ d ++ " ") ds)
compileExpr _ _ _ _ _ _ = pure Nothing

export

M src/Compiler/Scheme/Chez.idr => src/Compiler/Scheme/Chez.idr +5 -12
@@ 30,19 30,12 @@ import System.Info

%default covering

pathLookup : IO String
pathLookup
    = do path <- idrisGetEnv "PATH"
         let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
         let candidates = [p ++ "/" ++ x | p <- pathList,
                                           x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
         e <- firstExists candidates
         pure $ fromMaybe "/usr/bin/env scheme" e

findChez : IO String
findChez
    = do Just chez <- idrisGetEnv "CHEZ" | Nothing => pathLookup
         pure chez
    = do Nothing <- idrisGetEnv "CHEZ"
            | Just chez => pure chez
         path <- pathLookup ["chez", "chezscheme9.5", "scheme"]
         pure $ fromMaybe "/usr/bin/env scheme" path

-- Given the chez compiler directives, return a list of pairs of:
--   - the library file name


@@ 459,7 452,7 @@ compileExpr makeitso c tmpDir outputDir tm outfile
         let outSoAbs = cwd </> outputDir </> outSoFile
         chez <- coreLift $ findChez
         compileToSS c appDirGen tm outSsAbs
         logTime "Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
         logTime "++ Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
         let outShRel = outputDir </> outfile
         if isWindows
            then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)

M src/Compiler/Scheme/Racket.idr => src/Compiler/Scheme/Racket.idr +1 -1
@@ 431,7 431,7 @@ compileExpr mkexec c tmpDir outputDir tm outfile
         racket <- coreLift findRacket

         ok <- the (Core Int) $ if mkexec
                  then logTime "Build racket" $
                  then logTime "+ Build racket" $
                         coreLift $
                           system (raco ++ " -o " ++ outBinAbs ++ " " ++ outRktAbs)
                  else pure 0

M src/Core/Binary.idr => src/Core/Binary.idr +1 -1
@@ 31,7 31,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 47
ttcVersion = 48

export
checkTTCVersion : String -> Int -> Int -> Core ()

M src/Core/Context.idr => src/Core/Context.idr +68 -0
@@ 645,6 645,61 @@ data Transform : Type where
                   Name -> -- name for identifying the rule
                   Env Term vars -> Term vars -> Term vars -> Transform

||| Types that are transformed into a faster representation
||| during codegen.
public export
data BuiltinType : Type where
    ||| A built-in 'Nat'-like type
    ||| 'NatLike : [index ->] Type'
    ||| 'SLike : {0 _ : index} -> NatLike [index] -> NatLike [f index]'
    ||| 'ZLike : {0 _ : index} -> NatLike [index]'
    BuiltinNatural : BuiltinType
    -- All the following aren't implemented yet
    -- but are here to reduce number of TTC version changes
    NaturalPlus : BuiltinType
    NaturalMult : BuiltinType
    NaturalToInteger : BuiltinType
    IntegerToNatural : BuiltinType

export
Show BuiltinType where
    show BuiltinNatural = "Natural"
    show _ = "Not yet implemented"

-- Token types to make it harder to get the constructor names
-- the wrong way round.
public export data ZERO = MkZERO
public export data SUCC = MkSUCC

||| Record containing names of 'Nat'-like constructors.
public export
record NatBuiltin where
    constructor MkNatBuiltin
    zero : Name
    succ : Name

||| Rewrite rules for %builtin pragmas
||| Seperate to 'Transform' because it must also modify case statements
||| behaviour should remain the same after this transform
public export
record BuiltinTransforms where
    constructor MkBuiltinTransforms
    natTyNames : NameMap NatBuiltin -- map from Nat-like names to their constructors
    natZNames : NameMap ZERO -- map from Z-like names to their type constructor
    natSNames : NameMap SUCC -- map from S-like names to their type constructor

-- TODO: After next release remove nat from here and use %builtin pragma instead
initBuiltinTransforms : BuiltinTransforms
initBuiltinTransforms =
    let type = NS typesNS (UN "Nat")
        zero = NS typesNS (UN "Z")
        succ = NS typesNS (UN "S")
    in MkBuiltinTransforms
        { natTyNames = singleton type (MkNatBuiltin {zero, succ})
        , natZNames = singleton zero MkZERO
        , natSNames = singleton succ MkSUCC
        }

export
getFnName : Transform -> Maybe Name
getFnName (MkTransform _ _ app _)


@@ 987,6 1042,10 @@ record Defs where
     -- ^ A mapping from names to transformation rules which update applications
     -- of that name
  saveTransforms : List (Name, Transform)
  builtinTransforms : BuiltinTransforms
     -- ^ A mapping from names to transformations resulting from a %builtin pragma
     -- seperate to `transforms` because these must always fire globally so run these
     -- when compiling to `CExp`.
  namedirectives : NameMap (List String)
  ifaceHash : Int
  importHashes : List (Namespace, Int)


@@ 1046,6 1105,7 @@ initDefs
           , saveAutoHints = []
           , transforms = empty
           , saveTransforms = []
           , builtinTransforms = initBuiltinTransforms
           , namedirectives = empty
           , ifaceHash = 5381
           , importHashes = []


@@ 2144,6 2204,14 @@ getWorkingDir
         pure d

export
withCtxt : {auto c : Ref Ctxt Defs} -> Core a -> Core a
withCtxt = wrapRef Ctxt resetCtxt
  where
    resetCtxt : Defs -> Core ()
    resetCtxt defs = do let dir = defs.options.dirs.working_dir
                        coreLift_ $ changeDir dir

export
setPrefix : {auto c : Ref Ctxt Defs} -> String -> Core ()
setPrefix dir
    = do defs <- get Ctxt

M src/Core/Core.idr => src/Core/Core.idr +32 -0
@@ 492,6 492,18 @@ export %inline
(=<<) : (a -> Core b) -> Core a -> Core b
(=<<) = flip (>>=)

-- Kleisli compose
infixr 1 >=>
export %inline
(>=>) : (a -> Core b) -> (b -> Core c) -> (a -> Core c)
f >=> g = (g =<<) . f

-- Flipped kleisli compose
infixr 1 <=<
export %inline
(<=<) : (b -> Core c) -> (a -> Core b) -> (a -> Core c)
(<=<) = flip (>=>)

-- Applicative (specialised)
export %inline
pure : a -> Core a


@@ 554,6 566,11 @@ Catchable Core Error where
                         Right val => pure (Right val))
  throw = coreFail

-- Prelude.Monad.foldlM hand specialised for Core
export
foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)

-- Traversable (specialised)
traverse' : (a -> Core b) -> List a -> List b -> Core (List b)
traverse' f [] acc = pure (reverse acc)


@@ 706,6 723,21 @@ update x f
       put x (f v)

export
wrapRef : (x : label) -> {auto ref : Ref x a} ->
          (a -> Core ()) ->
          Core b ->
          Core b
wrapRef x onClose op
  = do v <- get x
       o <- catch op $ \err =>
              do onClose v
                 put x v
                 throw err
       onClose v
       put x v
       pure o

export
cond : List (Lazy Bool, Lazy a) -> a -> a
cond [] def = def
cond ((x, y) :: xs) def = if x then y else cond xs def

M src/Core/Env.idr => src/Core/Env.idr +6 -6
@@ 59,7 59,7 @@ revOnto xs [] = Refl
revOnto xs (v :: vs)
    = rewrite revOnto (v :: xs) vs in
        rewrite appendAssociative (reverse vs) [v] xs in
				  rewrite revOnto [v] vs in Refl
          rewrite revOnto [v] vs in Refl

revNs : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)
revNs [] ns = rewrite appendNilRightNeutral (reverse ns) in Refl


@@ 141,7 141,7 @@ letToLam (Let fc c val ty :: env) = Lam fc c Explicit ty :: letToLam env
letToLam (b :: env) = b :: letToLam env

mutual
	-- Quicker, if less safe, to store variables as a Nat, for quick comparison
  -- Quicker, if less safe, to store variables as a Nat, for quick comparison
  findUsed : {vars : _} ->
             Env Term vars -> List Nat -> Term vars -> List Nat
  findUsed env used (Local fc r idx p)


@@ 216,9 216,9 @@ mkShrinkSub [] els
         else (_ ** DropCons SubRefl)
mkShrinkSub (x :: xs) els
    = let (_ ** subRest) = mkShrinkSub xs (dropFirst els) in
					if isUsed 0 els
				     then (_ ** KeepCons subRest)
				     else (_ ** DropCons subRest)
      if isUsed 0 els
        then (_ ** KeepCons subRest)
        else (_ ** DropCons subRest)

mkShrink : {vars : _} ->