Merge branch 'master' into better-names

.github/workflows/ci-windows.yml

@@ -0,0 +1,40 @@
+name: Windows CI
+on:
+  push:
+    branches:
+      - '*'
+    tags:
+      - '*'
+  pull_request:
+    branches:
+      - master
+env:
+  MSYS2_PATH_TYPE: inherit
+
+jobs:
+  build:
+    runs-on: windows-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+      - name: Install MSYS2
+        uses: eine/setup-msys2@v0
+        with:
+          update: true
+          install: make mingw-w64-x86_64-clang tar
+      - name: Get Chez Scheme
+        run: | 
+          git clone --depth 1 https://github.com/cisco/ChezScheme
+      - name: Configure and Build Chez Scheme
+        run: msys2do cd ChezScheme; ./configure --threads; make; cd ..
+        shell: cmd
+      - name: Set Path
+        run: |
+          $chez="$(pwd)\ChezScheme\ta6nt\bin\ta6nt"
+          echo "::add-path::$chez"
+          echo "::set-env name=SCHEME::scheme"
+      - name: Test Scheme
+        run: scheme.exe --version
+      - name: Bootstrap
+        run: msys2do make bootstrap
+        shell: cmd

CHANGELOG.md

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

Makefile

@@ -12,6 +12,7 @@ MAJOR=0
 MINOR=2
 PATCH=0
 
+
 GIT_SHA1=
 ifeq ($(shell git status >/dev/null 2>&1; echo $$?), 0)
     # inside a git repo
@@ -31,14 +32,24 @@ else
     IDRIS2_IPKG := idris2rkt.ipkg
 endif
 
-export IDRIS2_BOOT_PATH = ${CURDIR}/libs/prelude/build/ttc:${CURDIR}/libs/base/build/ttc:${CURDIR}/libs/network/build/ttc
+ifeq ($(OS), windows)
+	IDRIS2_PREFIX := $(shell cygpath -m ${PREFIX})
+	IDRIS2_CURDIR := $(shell cygpath -m ${CURDIR})
+	export IDRIS2_BOOT_PATH = "${IDRIS2_CURDIR}/libs/prelude/build/ttc;${IDRIS2_CURDIR}/libs/base/build/ttc;${IDRIS2_CURDIR}/libs/network/build/ttc"
+else
+	IDRIS2_PREFIX := ${PREFIX}
+	IDRIS2_CURDIR := ${CURDIR}
+	export IDRIS2_BOOT_PATH = ${IDRIS2_CURDIR}/libs/prelude/build/ttc:${IDRIS2_CURDIR}/libs/base/build/ttc:${IDRIS2_CURDIR}/libs/network/build/ttc
+endif
+
+
 
 export SCHEME
 
 
-.PHONY: all idris2-exec ${TARGET} support support-clean clean distclean
+.PHONY: all idris2-exec ${TARGET} testbin support support-clean clean distclean
 
-all: support ${TARGET} libs
+all: support ${TARGET} testbin libs
 
 idris2-exec: ${TARGET}
 
@@ -48,7 +59,7 @@ ${TARGET}: src/IdrisPaths.idr
 src/IdrisPaths.idr:
 	echo 'module IdrisPaths' > src/IdrisPaths.idr
 	echo 'export idrisVersion : ((Nat,Nat,Nat), String); idrisVersion = ((${MAJOR},${MINOR},${PATCH}), "${GIT_SHA1}")' >> src/IdrisPaths.idr
-	echo 'export yprefix : String; yprefix="${PREFIX}"' >> src/IdrisPaths.idr
+	echo 'export yprefix : String; yprefix="${IDRIS2_PREFIX}"' >> src/IdrisPaths.idr
 
 prelude:
 	${MAKE} -C libs/prelude IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
@@ -64,6 +75,9 @@ contrib: prelude
 
 libs : prelude base network contrib
 
+testbin:
+	@${MAKE} -C tests testbin
+
 test:
 	@${MAKE} -C tests only=$(only) IDRIS2=../../../${TARGET}
 
@@ -93,12 +107,13 @@ install-api:
 install-idris2:
 	mkdir -p ${PREFIX}/bin/
 	install ${TARGET} ${PREFIX}/bin
+ifeq ($(OS), windows)
+	-install ${TARGET}.cmd ${PREFIX}/bin
+endif
 	mkdir -p ${PREFIX}/lib/
 	install support/c/${IDRIS2_SUPPORT} ${PREFIX}/lib
-ifneq ($(CG),racket)
 	mkdir -p ${PREFIX}/bin/${NAME}_app
 	install ${TARGETDIR}/${NAME}_app/* ${PREFIX}/bin/${NAME}_app
-endif
 
 install-support: support
 	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/support/chez
@@ -112,7 +127,7 @@ install-support: support
 install-libs: libs
 	${MAKE} -C libs/prelude install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 	${MAKE} -C libs/base install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
-	${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_VERSION=${IDRIS2_VERSION}
+	${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 	${MAKE} -C libs/contrib install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 
 
@@ -122,19 +137,19 @@ bootstrap: support
 	cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
 	sed s/libidris2_support.so/${IDRIS2_SUPPORT}/g bootstrap/idris2_app/idris2.ss > bootstrap/idris2_app/idris2-boot.ss
 ifeq ($(OS), darwin)
-	sed -i '' 's|__PREFIX__|${CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss
+	sed -i '' 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss
 else
-	sed -i 's|__PREFIX__|${CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss
+	sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss
 endif
 	sh ./bootstrap.sh
 
 bootstrap-racket: support
 	cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app
-	cp bootstrap/idris2.rkt bootstrap/idris2boot.rkt
+	cp bootstrap/idris2_app/idris2.rkt bootstrap/idris2_app/idris2-boot.rkt
 ifeq ($(OS), darwin)
-	sed -i '' 's|__PREFIX__|${CURDIR}/bootstrap|g' bootstrap/idris2boot.rkt
+	sed -i '' 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt
 else
-	sed -i 's|__PREFIX__|${CURDIR}/bootstrap|g' bootstrap/idris2boot.rkt
+	sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt
 endif
 	sh ./bootstrap-rkt.sh
 

README.md

@@ -3,7 +3,7 @@ Idris 2
 
 [![Build Status](https://travis-ci.org/idris-lang/Idris2.svg?branch=master)](https://travis-ci.org/idris-lang/Idris2)
 [![Documentation Status](https://readthedocs.org/projects/idris2/badge/?version=latest)](https://idris2.readthedocs.io/en/latest/?badge=latest)
-      
+![](https://github.com/idris-lang/Idris2/workflows/Windows%20CI/badge.svg)
 
 [Idris 2](https://idris-lang.org/) is a purely functional programming language
 with first class types.
@@ -16,8 +16,8 @@ you have Chez Scheme installed, with the executable name `chez`, type:
 
 You may need to change `chez` to be the local name of your Chez Scheme. This
 is often one of `scheme`, `chezscheme` or `chezscheme9.5` (depending on the
-version). On a modern desktop machine, this process should take no more than
-2 or 3 minutes.
+version). On a modern desktop machine, this process (including tests)
+should take less than 5 minutes.
 
 Idris 2 is mostly backwards compatible with Idris 1, with some minor
 exceptions. The most notable user visible differences, which might cause Idris

bootstrap-rkt.sh

@@ -4,11 +4,13 @@
 cd bootstrap
 echo "Building idris2boot from idris2boot.rkt"
 
-raco exe idris2boot.rkt
+raco exe idris2_app/idris2-boot.rkt
 
 # Put the result in the usual place where the target goes
 mkdir -p ../build/exec
-install idris2boot ../build/exec/idris2
+mkdir -p ../build/exec/idris2_app
+install idris2-rktboot ../build/exec/idris2
+install idris2_app/* ../build/exec/idris2_app
 
 cd ..
 

bootstrap.sh

@@ -22,13 +22,28 @@ cd ..
 DIR="`realpath $0`"
 PREFIX="`dirname $DIR`"/bootstrap
 
+if [ ${OS} = "windows" ]; then
+    IDRIS_PREFIX=$(cygpath -m $PREFIX)
+    IDRIS2_BOOT_PATH="${IDRIS_PREFIX}/idris2-0.2.0/prelude;${IDRIS_PREFIX}/idris2-0.2.0/base;${IDRIS_PREFIX}/idris2-0.2.0/contrib;${IDRIS_PREFIX}/idris2-0.2.0/network"
+    NEW_PREFIX=$(cygpath -m $(dirname "$DIR"))
+    IDRIS2_NEW_PATH="${NEW_PREFIX}/libs/prelude/build/ttc;${NEW_PREFIX}/libs/base/build/ttc;${NEW_PREFIX}/libs/network/build/ttc"
+    IDRIS2_TEST_LIBS="${IDRIS_PREFIX}/idris2-0.2.0/lib"
+    IDRIS2_TEST_DATA=${IDRIS_PREFIX}/idris2-0.2.0/support
+else
+    IDRIS2_BOOT_PATH="${PREFIX}/idris2-0.2.0/prelude:${PREFIX}/idris2-0.2.0/base:${PREFIX}/idris2-0.2.0/contrib:${PREFIX}/idris2-0.2.0/network"
+    NEWPREFIX="`dirname $DIR`"
+    IDRIS2_NEW_PATH="${NEWPREFIX}/libs/prelude/build/ttc:${NEWPREFIX}/libs/base/build/ttc:${NEWPREFIX}/libs/network/build/ttc"
+    IDRIS2_TEST_LIBS="${PREFIX}/idris2-0.2.0/lib" IDRIS2_TEST_DATA=${PREFIX}/idris2-0.2.0/support
+fi
+
 # Now rebuild everything properly
 echo ${PREFIX}
 
-IDRIS2_BOOT_PATH="${PREFIX}/idris2-0.2.0/prelude:${PREFIX}/idris2-0.2.0/base:${PREFIX}/idris2-0.2.0/contrib:${PREFIX}/idris2-0.2.0/network"
 
 make libs SCHEME=${SCHEME} PREFIX=${PREFIX}
 make install SCHEME=${SCHEME} PREFIX=${PREFIX}
 make clean IDRIS2_BOOT=${PREFIX}/bin/idris2
 make all IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
-make test INTERACTIVE='' IDRIS2_BOOT=${PREFIX}/bin/idris2 SCHEME=${SCHEME} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_LIBS=${PREFIX}/idris2-0.2.0/lib IDRIS2_DATA=${PREFIX}/idris2-0.2.0/support
+
+echo "Testing using libraries in ${IDRIS2_NEW_PATH}"
+make test INTERACTIVE='' IDRIS2_PATH=${IDRIS2_NEW_PATH} SCHEME=${SCHEME} IDRIS2_LIBS=${IDRIS2_TEST_LIBS} IDRIS2_DATA=${IDRIS2_TEST_DATA}

bootstrap/idris2-boot

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

bootstrap/idris2-rktboot

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

config.mk

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

docs/source/backends/racket.rst

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

docs/source/faq/faq.rst

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

docs/source/tutorial/modules.rst

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

idris2.ipkg

@@ -82,8 +82,10 @@ modules =
     Idris.Syntax,
     Idris.Version,
 
-    Parser.Lexer,
-    Parser.Rule,
+    Parser.Lexer.Common,
+    Parser.Lexer.Source,
+    Parser.Rule.Common,
+    Parser.Rule.Source,
     Parser.Source,
     Parser.Support,
     Parser.Unlit,

idris2api.ipkg

@@ -82,8 +82,10 @@ modules =
     Idris.Syntax,
     Idris.Version,
 
-    Parser.Lexer,
-    Parser.Rule,
+    Parser.Lexer.Common,
+    Parser.Lexer.Source,
+    Parser.Rule.Common,
+    Parser.Rule.Source,
     Parser.Source,
     Parser.Support,
     Parser.Unlit,

idris2rkt.ipkg

@@ -82,8 +82,10 @@ modules =
     Idris.Syntax,
     Idris.Version,
 
-    Parser.Lexer,
-    Parser.Rule,
+    Parser.Lexer.Common,
+    Parser.Lexer.Source,
+    Parser.Rule.Common,
+    Parser.Rule.Source,
     Parser.Source,
     Parser.Support,
     Parser.Unlit,

libs/base/Data/Nat.idr

@@ -415,3 +415,83 @@ multOneRightNeutral (S left) =
   let inductiveHypothesis = multOneRightNeutral left in
     rewrite inductiveHypothesis in
             Refl
+
+
+-- Proofs on -
+
+export
+minusSuccSucc : (left : Nat) -> (right : Nat) -> minus (S left) (S right) = minus left right
+minusSuccSucc left right = Refl
+
+export
+minusZeroLeft : (right : Nat) -> minus 0 right = Z
+minusZeroLeft right = Refl
+
+export
+minusZeroRight : (left : Nat) -> minus left 0 = left
+minusZeroRight Z        = Refl
+minusZeroRight (S left) = Refl
+
+export
+minusZeroN : (n : Nat) -> Z = minus n n
+minusZeroN Z     = Refl
+minusZeroN (S n) = minusZeroN n
+
+export
+minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
+minusOneSuccN Z     = Refl
+minusOneSuccN (S n) = minusOneSuccN n
+
+export
+minusSuccOne : (n : Nat) -> minus (S n) 1 = n
+minusSuccOne Z     = Refl
+minusSuccOne (S n) = Refl
+
+export
+minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z
+minusPlusZero Z     m = Refl
+minusPlusZero (S n) m = minusPlusZero n m
+
+export
+minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+  minus (minus left centre) right = minus left (centre + right)
+minusMinusMinusPlus Z        Z          right = Refl
+minusMinusMinusPlus (S left) Z          right = Refl
+minusMinusMinusPlus Z        (S centre) right = Refl
+minusMinusMinusPlus (S left) (S centre) right =
+  let inductiveHypothesis = minusMinusMinusPlus left centre right in
+      rewrite inductiveHypothesis in
+              Refl
+
+export
+plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
+  minus (left + right) (left + right') = minus right right'
+plusMinusLeftCancel Z right right'        = Refl
+plusMinusLeftCancel (S left) right right' =
+  let inductiveHypothesis = plusMinusLeftCancel left right right' in
+      rewrite inductiveHypothesis in
+              Refl
+
+export
+multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+                               (minus left centre) * right = minus (left * right) (centre * right)
+multDistributesOverMinusLeft Z        Z          right = Refl
+multDistributesOverMinusLeft (S left) Z          right =
+  rewrite (minusZeroRight (plus right (mult left right))) in Refl
+multDistributesOverMinusLeft Z        (S centre) right = Refl
+multDistributesOverMinusLeft (S left) (S centre) right =
+  let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
+      rewrite inductiveHypothesis in
+      rewrite plusMinusLeftCancel right (mult left right) (mult centre right) in
+              Refl
+
+export
+multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+                                left * (minus centre right) = minus (left * centre) (left * right)
+multDistributesOverMinusRight left centre right =
+  rewrite multCommutative left (minus centre right) in
+  rewrite multDistributesOverMinusLeft centre right left in
+  rewrite multCommutative centre left in
+  rewrite multCommutative right left in
+          Refl
+

libs/base/base.ipkg

@@ -37,6 +37,7 @@ modules = Control.App,
 
           System,
           System.Concurrency.Raw,
+          System.Clock,
           System.Directory,
           System.File,
           System.FFI,

libs/contrib/System/Clock.idr

@@ -1,150 +0,0 @@
-module System.Clock
-
-import PrimIO
-
-||| The various types of system clock available.
-public export
-data ClockType
-  = UTC       -- The time elapsed since the "epoch:" 00:00:00 UTC, January 1, 1970
-  | Monotonic -- The time elapsed since some arbitrary point in the past
-  | Duration  -- Representing a time duration.
-  | Process   -- The amount of CPU time used by the current process.
-  | Thread    -- The amount of CPU time used by the current thread.
-  | GCCPU     -- The current process's CPU time consumed by the garbage collector.
-  | GCReal    -- The current process's real time consumed by the garbage collector.
-
-export
-Show ClockType where
-  show UTC       = "UTC"
-  show Monotonic = "monotonic"
-  show Duration  = "duration"
-  show Process   = "process"
-  show Thread    = "thread"
-  show GCCPU     = "gcCPU"
-  show GCReal    = "gcReal"
-
-public export
-data Clock : (type : ClockType) -> Type where
-  MkClock
-    : {type : ClockType}
-    -> (seconds : Integer)
-    -> (nanoseconds : Integer)
-    -> Clock type
-
-public export
-Eq (Clock type) where
-  (MkClock seconds1 nanoseconds1) == (MkClock seconds2 nanoseconds2) =
-    seconds1 == seconds2 && nanoseconds1 == nanoseconds2
-
-public export
-Ord (Clock type) where
-  compare (MkClock seconds1 nanoseconds1) (MkClock seconds2 nanoseconds2) =
-  case compare seconds1 seconds2 of
-    LT => LT
-    GT => GT
-    EQ => compare nanoseconds1 nanoseconds2
-
-public export
-Show (Clock type) where
-  show (MkClock {type} seconds nanoseconds) =
-    show type ++ ": " ++ show seconds ++ "s " ++ show nanoseconds ++ "ns"
-
-||| A helper to deconstruct a Clock.
-public export
-seconds : Clock type -> Integer
-seconds (MkClock s _) = s
-
-||| A helper to deconstruct a Clock.
-public export
-nanoseconds : Clock type -> Integer
-nanoseconds (MkClock _ ns) = ns
-
-||| Make a duration value.
-public export
-makeDuration : Integer -> Integer -> Clock Duration
-makeDuration = MkClock
-
-||| Opaque clock value manipulated by the back-end.
-data OSClock : Type where [external]
-
-||| Note: Back-ends are required to implement UTC, monotonic time, CPU time
-||| in current process/thread, and time duration; the rest are optional.
-data ClockTypeMandatory
-  = Mandatory
-  | Optional
-
-public export
-isClockMandatory : ClockType -> ClockTypeMandatory
-isClockMandatory GCCPU  = Optional
-isClockMandatory GCReal = Optional
-isClockMandatory _      = Mandatory
-
-prim_clockTimeMonotonic : IO OSClock
-prim_clockTimeMonotonic = schemeCall OSClock "blodwen-clock-time-monotonic" []
-
-fetchOSClock : ClockType -> IO OSClock
-fetchOSClock UTC       = schemeCall OSClock "blodwen-clock-time-utc" []
-fetchOSClock Monotonic = prim_clockTimeMonotonic
-fetchOSClock Process   = schemeCall OSClock "blodwen-clock-time-process" []
-fetchOSClock Thread    = schemeCall OSClock "blodwen-clock-time-thread" []
-fetchOSClock GCCPU     = schemeCall OSClock "blodwen-clock-time-gccpu" []
-fetchOSClock GCReal    = schemeCall OSClock "blodwen-clock-time-gcreal" []
-fetchOSClock Duration  = prim_clockTimeMonotonic
-
-||| A test to determine the status of optional clocks.
-osClockValid : OSClock -> IO Int
-osClockValid clk = schemeCall Int "blodwen-is-time?" [clk]
-
-fromOSClock : {type : ClockType} -> OSClock -> IO (Clock type)
-fromOSClock clk =
-  pure $
-    MkClock
-      {type}
-      !(schemeCall Integer "blodwen-clock-second" [clk])
-      !(schemeCall Integer "blodwen-clock-nanosecond" [clk])
-
-public export
-clockTimeReturnType : (typ : ClockType) -> Type
-clockTimeReturnType typ with (isClockMandatory typ)
-  clockTimeReturnType typ | Optional = Maybe (Clock typ)
-  clockTimeReturnType typ | Mandatory = Clock typ
-
-||| Fetch the system clock of a given kind. If the clock is mandatory,
-||| we return a (Clock type) else (Maybe (Clock type)).
-public export
-clockTime : (typ : ClockType) -> IO (clockTimeReturnType typ)
-clockTime clockType with (isClockMandatory clockType)
-  clockTime clockType | Mandatory = fetchOSClock clockType >>= fromOSClock
-  clockTime clockType | Optional = do
-    clk <- fetchOSClock clockType
-    valid <- map (== 1) $ osClockValid clk
-    if valid
-      then map Just $ fromOSClock clk
-      else pure Nothing
-
-toNano : Clock type -> Integer
-toNano (MkClock seconds nanoseconds) =
-  let scale = 1000000000
-   in scale * seconds + nanoseconds
-
-fromNano : {type : ClockType} -> Integer -> Clock type
-fromNano n =
-  let scale       = 1000000000
-      seconds     = n `div` scale
-      nanoseconds = n `mod` scale
-   in MkClock seconds nanoseconds
-
-||| Compute difference between two clocks of the same type.
-public export
-timeDifference : Clock type -> Clock type -> Clock Duration
-timeDifference clock duration = fromNano $ toNano clock - toNano duration
-
-||| Add a duration to a clock value.
-public export
-addDuration : {type : ClockType} -> Clock type -> Clock Duration -> Clock type
-addDuration clock duration = fromNano $ toNano clock + toNano duration
-
-||| Subtract a duration from a clock value.
-public export
-subtractDuration : {type : ClockType} -> Clock type -> Clock Duration -> Clock type
-subtractDuration clock duration = fromNano $ toNano clock - toNano duration

libs/contrib/System/Path.idr

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

libs/contrib/Text/Parser/Core.idr

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

libs/contrib/contrib.ipkg

@@ -25,7 +25,6 @@ modules = Control.Delayed,
           Text.Parser.Core,
           Text.Lexer.Core,
 
-          System.Clock,
           System.Random,
           System.Path,
           Syntax.WithProof,

libs/network/Echo.idr

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

libs/network/Makefile

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

libs/network/Network/FFI.idr

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

libs/network/Network/Socket/Data.idr

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

libs/network/expected

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

libs/network/test.c

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

libs/prelude/Prelude.idr

@@ -1093,7 +1093,7 @@ strCons = prim__strCons
 public export
 strUncons : String -> Maybe (Char, String)
 strUncons "" = Nothing
-strUncons str = Just (prim__strHead str, prim__strTail str)
+strUncons str = assert_total $ Just (prim__strHead str, prim__strTail str)
 
 ||| Turns a list of characters into a string.
 public export
@@ -1117,7 +1117,7 @@ fastPack xs
 ||| ```
 public export
 unpack : String -> List Char
-unpack str = unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
+unpack str = assert_total $ unpack' 0 (prim__cast_IntegerInt (natToInteger (length str))) str
   where
     unpack' : Int -> Int -> String -> List Char
     unpack' pos len str

src/Compiler/Common.idr

@@ -391,7 +391,7 @@ copyLib (lib, fullname)
     = if lib == fullname
          then pure ()
          else do Right bin <- coreLift $ readFromFile fullname
-                    | Left err => throw (FileErr fullname err)
+                    | Left err => pure () -- assume a system library installed globally
                  Right _ <- coreLift $ writeToFile lib bin
                     | Left err => throw (FileErr lib err)
                  pure ()

src/Compiler/Scheme/Chez.idr

@@ -26,9 +26,9 @@ import System.Info
 pathLookup : IO String
 pathLookup
     = do path <- getEnv "PATH"
-         let pathList = split (== ':') $ fromMaybe "/usr/bin:/usr/local/bin" path
+         let pathList = split (== pathSep) $ fromMaybe "/usr/bin:/usr/local/bin" path
          let candidates = [p ++ "/" ++ x | p <- pathList,
-                                           x <- ["chez", "chezscheme9.5", "scheme"]]
+                                           x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
          e <- firstExists candidates
          pure $ fromMaybe "/usr/bin/env scheme" e
 
@@ -55,11 +55,13 @@ findLibs ds
              then Just (trim (substr 3 (length d) d))
              else Nothing
 
-escapeQuotes : String -> String
-escapeQuotes s = pack $ foldr escape [] $ unpack s
+
+escapeString : String -> String
+escapeString s = pack $ foldr escape [] $ unpack s
   where
     escape : Char -> List Char -> List Char
     escape '"' cs = '\\' :: '\"' :: cs
+    escape '\\' cs = '\\' :: '\\' :: cs
     escape c   cs = c :: cs
 
 schHeader : String -> List String -> String
@@ -71,7 +73,7 @@ schHeader chez libs
     "  [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++
     "  [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")]\n" ++
     "  [else (load-shared-object \"libc.so\")])\n\n" ++
-    showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeQuotes x ++ "\")") libs) ++ "\n\n" ++
+    showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeString x ++ "\")") libs) ++ "\n\n" ++
     "(let ()\n"
 
 schFooter : String
@@ -181,7 +183,7 @@ cCall appdir fc cfn clib args ret
                            copyLib (appdir ++ dirSep ++ fname, fullname)
                            put Loaded (clib :: loaded)
                            pure $ "(load-shared-object \""
-                                    ++ escapeQuotes fname
+                                    ++ escapeString fname
                                     ++ "\")\n"
          argTypes <- traverse (\a => cftySpec fc (snd a)) args
          retType <- cftySpec fc ret
@@ -316,6 +318,23 @@ startChez appdir target = unlines
     , "\"`dirname \"$DIR\"`\"/\"" ++ target ++ "\" \"$@\""
     ]
 
+startChezCmd : String -> String -> String -> String
+startChezCmd chez appdir target = unlines
+    [ "@echo off"
+    , "set APPDIR=%~dp0"
+    , "set PATH=%APPDIR%\\" ++ appdir ++ ";%PATH%"
+    , "\"" ++ chez ++ "\" --script \"%APPDIR%/" ++ target ++ "\" %*"
+    ]
+
+startChezWinSh : String -> String -> String -> String
+startChezWinSh chez appdir target = unlines
+    [ "#!/bin/sh"
+    , "DIR=\"`realpath \"$0\"`\""
+    , "CHEZ=$(cygpath \"" ++ chez ++"\")"
+    , "export PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$PATH\""
+    , "\"$CHEZ\" --script \"$(dirname \"$DIR\")/" ++ target ++ "\" \"$@\""
+    ]
+
 ||| Compile a TT expression to Chez Scheme
 compileToSS : Ref Ctxt Defs ->
               String -> ClosedTerm -> (outfile : String) -> Core ()
@@ -347,17 +366,15 @@ compileToSS c appdir tm outfile
 
 ||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off.
 compileToSO : {auto c : Ref Ctxt Defs} ->
-              (appDirRel : String) -> (outSsAbs : String) -> Core ()
-compileToSO appDirRel outSsAbs
+              String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
+compileToSO chez appDirRel outSsAbs
     = do let tmpFileAbs = appDirRel ++ dirSep ++ "compileChez"
-         chez <- coreLift $ findChez
-         let build= "#!" ++ chez ++ " --script\n" ++
-                    "(parameterize ([optimize-level 3]) (compile-program \"" ++
-                    outSsAbs ++ "\"))"
+         let build= "(parameterize ([optimize-level 3]) (compile-program " ++
+                    show outSsAbs ++ "))"
          Right () <- coreLift $ writeFile tmpFileAbs build
             | Left err => throw (FileErr tmpFileAbs err)
          coreLift $ chmodRaw tmpFileAbs 0o755
-         coreLift $ system tmpFileAbs
+         coreLift $ system ("\"" ++ chez ++ "\" --script \"" ++ tmpFileAbs ++ "\"")
          pure ()
 
 makeSh : String -> String -> String -> Core ()
@@ -366,13 +383,22 @@ makeSh outShRel appdir outAbs
             | Left err => throw (FileErr outShRel err)
          pure ()
 
+||| Make Windows start scripts, one for bash environments and one batch file
+makeShWindows : String -> String -> String -> String -> Core ()
+makeShWindows chez outShRel appdir outAbs
+    = do let cmdFile = outShRel ++ ".cmd"
+         Right () <- coreLift $ writeFile cmdFile (startChezCmd chez appdir outAbs)
+            | Left err => throw (FileErr cmdFile err)
+         Right () <- coreLift $ writeFile outShRel (startChezWinSh chez appdir outAbs)
+            | Left err => throw (FileErr outShRel err)
+         pure ()
+
 ||| Chez Scheme implementation of the `compileExpr` interface.
 compileExpr : Bool -> Ref Ctxt Defs -> (execDir : String) ->
               ClosedTerm -> (outfile : String) -> Core (Maybe String)
 compileExpr makeitso c execDir tm outfile
     = do let appDirRel = outfile ++ "_app" -- relative to build dir
          let appDirGen = execDir ++ dirSep ++ appDirRel -- relative to here
-
          coreLift $ mkdirs (splitDir appDirGen)
          Just cwd <- coreLift currentDir
               | Nothing => throw (InternalError "Can't get current directory")
@@ -380,11 +406,13 @@ compileExpr makeitso c execDir tm outfile
          let outSoFile = appDirRel ++ dirSep ++ outfile ++ ".so"
          let outSsAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSsFile
          let outSoAbs = cwd ++ dirSep ++ execDir ++ dirSep ++ outSoFile
-
+         chez <- coreLift $ findChez
          compileToSS c appDirGen tm outSsAbs
-         logTime "Make SO" $ when makeitso $ compileToSO appDirGen outSsAbs
+         logTime "Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
          let outShRel = execDir ++ dirSep ++ outfile
-         makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)
+         if isWindows
+            then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile) 
+            else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)
          coreLift $ chmodRaw outShRel 0o755
          pure (Just outShRel)
 

src/Compiler/Scheme/Racket.idr

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

src/Core/Binary.idr

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

src/Core/Context.idr

@@ -170,6 +170,9 @@ data DefFlag
          -- should evaluate the RHS, with reduction limits on the given names,
          -- and ensure the name has made progress in doing so (i.e. has reduced
          -- at least once)
+    | AllGuarded -- safe to treat as a constructor for the purposes of
+         -- productivity checking. All clauses are guarded by constructors,
+         -- and there are no other function applications
 
 export
 Eq DefFlag where
@@ -181,8 +184,21 @@ Eq DefFlag where
     (==) BlockedHint BlockedHint = True
     (==) Macro Macro = True
     (==) (PartialEval x) (PartialEval y) = x == y
+    (==) AllGuarded AllGuarded = True
     (==) _ _ = False
 
+export
+Show DefFlag where
+  show Inline = "inline"
+  show Invertible = "invertible"
+  show Overloadable = "overloadable"
+  show TCInline = "tcinline"
+  show (SetTotal x) = show x
+  show BlockedHint = "blockedhint"
+  show Macro = "macro"
+  show (PartialEval _) = "partialeval"
+  show AllGuarded = "allguarded"
+
 public export
 data SizeChange = Smaller | Same | Unknown
 
@@ -868,9 +884,15 @@ clearCtxt : {auto c : Ref Ctxt Defs} ->
             Core ()
 clearCtxt
     = do defs <- get Ctxt
-         put Ctxt (record { options = options defs,
+         put Ctxt (record { options = resetElab (options defs),
                             timings = timings defs } !initDefs)
+  where
+    resetElab : Options -> Options
+    resetElab = record { elabDirectives = defaultElab }
 
+-- Beware: if your hashable thing contains (potentially resolved) names,
+-- it'll be better to use addHashWithNames to make the hash independent
+-- of the internal numbering of names.
 export
 addHash : {auto c : Ref Ctxt Defs} ->
           Hashable a => a -> Core ()
@@ -1167,6 +1189,15 @@ prettyName (WithBlock outer idx)
 prettyName (NS ns n) = prettyName n
 prettyName n = pure (show n)
 
+-- Add a hash of a thing that contains names,
+-- but convert the internal numbers to full names first.
+-- This makes the hash not depend on the internal numbering,
+-- which is unstable.
+export
+addHashWithNames : {auto c : Ref Ctxt Defs} ->
+  Hashable a => HasNames a => a -> Core ()
+addHashWithNames x = toFullNames x >>= addHash
+
 export
 setFlag : {auto c : Ref Ctxt Defs} ->
         FC -> Name -> DefFlag -> Core ()

src/Core/Coverage.idr

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

src/Core/Directory.idr

@@ -215,10 +215,13 @@ findIpkg (f :: fs)
 
 allDirs : String -> List String -> List (String, List String)
 allDirs path [] = []
-allDirs path ("" :: ds) = ("/", ds) :: allDirs path ds
+allDirs path ("" :: ds) = (dirSep, ds) ::allDirs path ds
+allDirs "" (d :: ds)
+    = let d' = if isWindows then d ++ dirSep else strCons sep d in 
+                (d', ds) :: allDirs d' ds
 allDirs path (d :: ds)
     = let d' = path ++ strCons sep d in
-          (d', ds) :: allDirs d' ds
+                (d', ds) :: allDirs d' ds
 
 -- Find an ipkg file in any of the directories above this one
 -- returns the directory, the ipkg file name, and the directories we've

src/Core/Hash.idr

@@ -64,6 +64,8 @@ Hashable String where
 export
 Hashable Name where
   hashWithSalt h (MN s _) = hashWithSalt h s
+  hashWithSalt h (DN _ n) = hashWithSalt h n
+  hashWithSalt h (NS ns n) = hashWithSalt (hashWithSalt h ns) n
   hashWithSalt h (Resolved i) = hashWithSalt h i
   hashWithSalt h n = hashWithSalt h (show n)
 

src/Core/Normalise.idr

@@ -107,7 +107,7 @@ parameters (defs : Defs, topopts : EvalOpts)
     eval env locs (Bind fc x (Lam r _ ty) scope) (thunk :: stk)
         = eval env (thunk :: locs) scope stk
     eval env locs (Bind fc x b@(Let r val ty) scope) stk
-        = if holesOnly topopts || argHolesOnly topopts
+        = if holesOnly topopts || argHolesOnly topopts && not (tcInline topopts)
              then do b' <- traverse (\tm => eval env locs tm []) b
                      pure $ NBind fc x b'
                         (\defs', arg => evalWithOpts defs' topopts
@@ -595,8 +595,10 @@ mutual
            pure (TDelay fc r tyQ argQ)
     where
       toHolesOnly : Closure vs -> Closure vs
-      toHolesOnly (MkClosure _ locs env tm)
-          = MkClosure withHoles locs env tm
+      toHolesOnly (MkClosure opts locs env tm)
+          = MkClosure (record { holesOnly = True,
+                                argHolesOnly = True } opts)
+                      locs env tm
       toHolesOnly c = c
   quoteGenNF q defs bound env (NForce fc r arg args)
       = do args' <- quoteArgs q defs bound env args

src/Core/Options.idr

@@ -129,12 +129,13 @@ record Options where
   primnames : PrimNames
   extensions : List LangExt
 
+export
 isWindows : Bool
 isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
 
 export
 sep : Char
-sep = '/'
+sep = if isWindows then '\\' else '/'
 
 export
 dirSep : String
@@ -156,6 +157,7 @@ defaultSession : Session
 defaultSession = MkSessionOpts False False False Chez 0 False False
                                Nothing Nothing Nothing Nothing
 
+export
 defaultElab : ElabDirectives
 defaultElab = MkElabDirectives True True PartialOK 3 True
 

src/Core/Primitives.idr

@@ -403,12 +403,12 @@ allPrimitives =
     map (\t => MkPrim (Div t) (arithTy t) notCovering) [IntType, IntegerType, DoubleType] ++
     map (\t => MkPrim (Mod t) (arithTy t) notCovering) [IntType, IntegerType] ++
     map (\t => MkPrim (Neg t) (predTy t t) isTotal) [IntType, IntegerType, DoubleType] ++
-    map (\t => MkPrim (ShiftL t) (arithTy t) notCovering) [IntType, IntegerType] ++
-    map (\t => MkPrim (ShiftR t) (arithTy t) notCovering) [IntType, IntegerType] ++
+    map (\t => MkPrim (ShiftL t) (arithTy t) isTotal) [IntType, IntegerType] ++
+    map (\t => MkPrim (ShiftR t) (arithTy t) isTotal) [IntType, IntegerType] ++
 
-    map (\t => MkPrim (BAnd t) (arithTy t) notCovering) [IntType, IntegerType] ++
-    map (\t => MkPrim (BOr t) (arithTy t) notCovering) [IntType, IntegerType] ++
-    map (\t => MkPrim (BXOr t) (arithTy t) notCovering) [IntType] ++
+    map (\t => MkPrim (BAnd t) (arithTy t) isTotal) [IntType, IntegerType] ++
+    map (\t => MkPrim (BOr t) (arithTy t) isTotal) [IntType, IntegerType] ++
+    map (\t => MkPrim (BXOr t) (arithTy t) isTotal) [IntType] ++
 
     map (\t => MkPrim (LT t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++
     map (\t => MkPrim (LTE t) (cmpTy t) isTotal) [IntType, IntegerType, CharType, DoubleType, StringType] ++

src/Core/TT.idr

@@ -526,6 +526,12 @@ Eq TotalReq where
     (==) PartialOK PartialOK = True
     (==) _ _ = False
 
+export
+Show TotalReq where
+    show Total = "total"
+    show CoveringOnly = "covering"
+    show PartialOK = "partial"
+
 public export
 data PartialReason
        = NotStrictlyPositive

src/Core/TTC.idr

@@ -843,6 +843,7 @@ TTC Def where
              10 => pure Context.Delayed
              _ => corrupt "Def"
 
+export
 TTC TotalReq where
   toBuf b Total = tag 0
   toBuf b CoveringOnly = tag 1
@@ -864,6 +865,7 @@ TTC DefFlag where
   toBuf b BlockedHint = tag 7
   toBuf b Macro = tag 8
   toBuf b (PartialEval x) = tag 9 -- names not useful any more
+  toBuf b AllGuarded = tag 10
 
   fromBuf b
       = case !getTag of
@@ -875,6 +877,7 @@ TTC DefFlag where
              7 => pure BlockedHint
              8 => pure Macro
              9 => pure (PartialEval [])
+             10 => pure AllGuarded
              _ => corrupt "DefFlag"
 
 export

src/Core/Termination.idr

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

src/Idris/Desugar.idr

@@ -17,7 +17,7 @@ import Idris.Syntax
 import Idris.Elab.Implementation
 import Idris.Elab.Interface
 
-import Parser.Lexer
+import Parser.Lexer.Source
 
 import TTImp.BindImplicits
 import TTImp.Parser
@@ -353,6 +353,8 @@ mutual
       = desugarB side ps $
           PLam fc top Explicit (PRef fc (MN "rec" 0)) (PImplicit fc) $
             foldl (\r, f => PApp fc (PRef fc f) r) (PRef fc (MN "rec" 0)) fields
+  desugarB side ps (PWithUnambigNames fc ns rhs)
+      = IWithUnambigNames fc ns <$> desugarB side ps rhs
 
   desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
                   {auto b : Ref Bang BangData} ->
@@ -600,12 +602,6 @@ mutual
                 List Name -> PDecl -> Core (List ImpDecl)
   desugarDecl ps (PClaim fc rig vis fnopts ty)
       = do opts <- traverse (desugarFnOpt ps) fnopts
-           opts <- if (isTotalityOption `any` opts)
-                   then pure opts
-                   else do PartialOK <- getDefaultTotalityOption
-                           | tot => pure (Totality tot :: opts)
-                           -- We assume PartialOK by default internally
-                           pure opts
            pure [IClaim fc rig vis opts !(desugarType ps ty)]
         where
           isTotalityOption : FnOpt -> Bool

src/Idris/Elab/Implementation.idr

@@ -185,7 +185,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                fns <- topMethTypes [] impName methImps impsp (params cdata)
                                       (map fst (methods cdata))
                                       (methods cdata)
-               traverse (processDecl [] nest env) (map mkTopMethDecl fns)
+               traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)
 
                -- 3. Build the record for the implementation
                let mtops = map (Builtin.fst . snd) fns
@@ -270,8 +270,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     -- inserted in the right place
     mkMethField : List (Name, RigCount, RawImp) ->
                   List (Name, List (Name, RigCount, PiInfo RawImp)) ->
-                  (Name, Name, List (String, String), RigCount, RawImp) -> RawImp
-    mkMethField methImps fldTys (topn, n, upds, c, ty)
+                  (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> RawImp
+    mkMethField methImps fldTys (topn, n, upds, c, treq, ty)
         = let argns = map applyUpdate (maybe [] id (lookup (dropNS topn) fldTys))
               imps = map fst methImps in
               -- Pass through implicit arguments to the function which are also
@@ -311,10 +311,10 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
     topMethType : List (Name, RawImp) ->
                   Name -> List (Name, RigCount, RawImp) ->
                   List String -> List Name -> List Name ->
-                  (Name, RigCount, (Bool, RawImp)) ->
-                  Core ((Name, Name, List (String, String), RigCount, RawImp),
+                  (Name, RigCount, TotalReq, (Bool, RawImp)) ->
+                  Core ((Name, Name, List (String, String), RigCount, TotalReq, RawImp),
                            List (Name, RawImp))
-    topMethType methupds impName methImps impsp pnames allmeths (mn, c, (d, mty_in))
+    topMethType methupds impName methImps impsp pnames allmeths (mn, c, treq, (d, mty_in))
         = do -- Get the specialised type by applying the method to the
              -- parameters
              n <- inCurrentNS (methName mn)
@@ -348,22 +348,22 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
              let methupds' = if isNil ibinds then []
                              else [(n, impsApply (IVar fc n)
                                      (map (\x => (x, IBindVar fc (show x))) ibinds))]
-             pure ((mn, n, upds, c, mty), methupds')
+             pure ((mn, n, upds, c, treq, mty), methupds')
 
     topMethTypes : List (Name, RawImp) ->
                    Name -> List (Name, RigCount, RawImp) ->
                    List String -> List Name -> List Name ->
-                   List (Name, RigCount, (Bool, RawImp)) ->
-                   Core (List (Name, Name, List (String, String), RigCount, RawImp))
+                   List (Name, RigCount, TotalReq, (Bool, RawImp)) ->
+                   Core (List (Name, Name, List (String, String), RigCount, TotalReq, RawImp))
     topMethTypes upds impName methImps impsp pnames allmeths [] = pure []
     topMethTypes upds impName methImps impsp pnames allmeths (m :: ms)
         = do (m', newupds) <- topMethType upds impName methImps impsp pnames allmeths m
              ms' <- topMethTypes (newupds ++ upds) impName methImps impsp pnames allmeths ms
              pure (m' :: ms')
 
-    mkTopMethDecl : (Name, Name, List (String, String), RigCount, RawImp) -> ImpDecl
-    mkTopMethDecl (mn, n, upds, c, mty)
-        = IClaim fc c vis opts_in (MkImpTy fc n mty)
+    mkTopMethDecl : (Name, Name, List (String, String), RigCount, TotalReq, RawImp) -> ImpDecl
+    mkTopMethDecl (mn, n, upds, c, treq, mty)
+        = IClaim fc c vis (Totality treq :: opts_in) (MkImpTy fc n mty)
 
     -- Given the method type (result of topMethType) return the mapping from
     -- top level method name to current implementation's method name
@@ -414,9 +414,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                    "Implementation body can only contain definitions")
 
     addTransform : Name -> List (Name, Name) ->
-                   (Name, RigCount, Bool, RawImp) ->
+                   (Name, RigCount, TotalReq, Bool, RawImp) ->
                    Core ()
-    addTransform iname ns (top, _, _, ty)
+    addTransform iname ns (top, _, _, _, ty)
         = do log 3 $ "Adding transform for " ++ show top ++ " : " ++ show ty ++
                      "\n\tfor " ++ show iname ++ " in " ++ show ns
              let lhs = IImplicitApp fc (IVar fc top)

src/Idris/Elab/Interface.idr

@@ -21,6 +21,7 @@ import TTImp.Utils
 
 import Data.ANameMap
 import Data.List
+import Data.Maybe
 
 -- TODO: Check all the parts of the body are legal
 -- TODO: Deal with default superclass implementations
@@ -225,14 +226,29 @@ mkCon loc (NS ns (UN n))
 mkCon loc n
    = DN (show n ++ " at " ++ show loc) (UN ("__mk" ++ show n))
 
-updateIfaceSyn : {auto s : Ref Syn SyntaxInfo} ->
+updateIfaceSyn : {auto c : Ref Ctxt Defs} ->
+                 {auto s : Ref Syn SyntaxInfo} ->
                  Name -> Name -> List Name -> List RawImp ->
-                 List (Name, RigCount, (Bool, RawImp)) -> List (Name, List ImpClause) ->
+                 List (Name, RigCount, List FnOpt, (Bool, RawImp)) -> List (Name, List ImpClause) ->
                  Core ()
 updateIfaceSyn iname cn ps cs ms ds
     = do syn <- get Syn
-         let info = MkIFaceInfo cn ps cs ms ds
+         ms' <- traverse totMeth ms
+         let info = MkIFaceInfo cn ps cs ms' ds
          put Syn (record { ifaces $= addName iname info } syn)
+ where
+    findSetTotal : List FnOpt -> Maybe TotalReq
+    findSetTotal [] = Nothing
+    findSetTotal (Totality t :: _) = Just t
+    findSetTotal (_ :: xs) = findSetTotal xs
+
+    totMeth : (Name, RigCount, List FnOpt, (Bool, RawImp)) ->
+              Core (Name, RigCount, TotalReq, (Bool, RawImp))
+    totMeth (n, c, opts, t)
+        = do let treq = fromMaybe PartialOK (findSetTotal opts)
+--         = do let treq = fromMaybe !getDefaultTotalityOption (findSetTotal opts)
+-- TODO: Put the above back when totality checker is properly working
+             pure (n, c, treq, t)
 
 export
 elabInterface : {vars : _} ->
@@ -255,7 +271,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
          -- Machine generated names need to be qualified when looking them up
          conName <- inCurrentNS conName_in
          let meth_sigs = mapMaybe getSig body -- (FC, RigCount, List FnOpt, Name, (Bool, RawImp))
-         let meth_decls = map (\ (f, c, o, n, b, ty) => (n, c, b, ty)) meth_sigs
+         let meth_decls = map (\ (f, c, o, n, b, ty) => (n, c, o, b, ty)) meth_sigs
          let meth_names = map fst meth_decls
          let defaults = mapMaybe getDefault body
 
@@ -321,7 +337,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
     -- Check that a default definition is correct. We just discard it here once
     -- we know it's okay, since we'll need to re-elaborate it for each
     -- instance, to specialise it
-    elabDefault : List (Name, RigCount, (Bool, RawImp)) ->
+    elabDefault : List (Name, RigCount, List FnOpt, Bool, RawImp) ->
                   (FC, List FnOpt, Name, List ImpClause) ->
                   Core (Name, List ImpClause)
     elabDefault tydecls (fc, opts, n, cs)
@@ -332,7 +348,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
              (rig, dty) <-
                    the (Core (RigCount, RawImp)) $
                        case lookup n tydecls of
-                          Just (r, (_, t)) => pure (r, t)
+                          Just (r, _, _, t) => pure (r, t)
                           Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname))
 
              let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))

src/Idris/Error.idr

@@ -83,7 +83,7 @@ perror (NotCovering fc n (NonCoveringCall ns))
                            [fn] => " " ++ show fn
                            _ => "s: " ++ showSep ", " (map show ns)
 perror (NotTotal fc n r)
-    = pure $ !(prettyName n) ++ " is not total"
+    = pure $ !(prettyName n) ++ " is not total:\n\t" ++ show r
 perror (LinearUsed fc count n)
     = pure $ "There are " ++ show count ++ " uses of linear name " ++ sugarName n
 perror (LinearMisuse fc n exp ctx)

src/Idris/IDEMode/CaseSplit.idr

@@ -6,7 +6,7 @@ import Core.Metadata
 import Core.TT
 import Core.Value
 
-import Parser.Lexer
+import Parser.Lexer.Source
 import Parser.Unlit
 
 import TTImp.Interactive.CaseSplit
@@ -164,7 +164,7 @@ fnName lhs (UN n)
       else "op"
 fnName lhs (NS _ n) = fnName lhs n
 fnName lhs (DN s _) = s
-fnName lhs n = show n
+fnName lhs n = nameRoot n
 
 
 export

src/Idris/IDEMode/Commands.idr

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

src/Idris/IDEMode/MakeClause.idr

@@ -1,7 +1,7 @@
 module Idris.IDEMode.MakeClause
 
 import Core.Name
-import Parser.Lexer
+import Parser.Lexer.Source
 import Parser.Unlit
 
 import Data.List

src/Idris/IDEMode/Parser.idr

@@ -6,7 +6,7 @@ module Idris.IDEMode.Parser
 import Idris.IDEMode.Commands
 
 import Text.Parser
-import Parser.Lexer
+import Parser.Lexer.Source
 import Parser.Source
 import Text.Lexer
 import Utils.Either
@@ -16,7 +16,7 @@ import Data.List
 import Data.Strings
 
 %hide Text.Lexer.symbols
-%hide Parser.Lexer.symbols
+%hide Parser.Lexer.Source.symbols
 
 symbols : List String
 symbols = ["(", ":", ")"]
@@ -43,7 +43,7 @@ idelex str
                           Comment _ => False
                           _ => True
 
-sexp : Rule SExp
+sexp : SourceRule SExp
 sexp
     = do symbol ":"; exactIdent "True"
          pure (BoolAtom True)

src/Idris/IDEMode/REPL.idr

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

src/Idris/IDEMode/SyntaxHighlight.idr

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

src/Idris/IDEMode/TokenLine.idr

@@ -1,7 +1,7 @@
 ||| Tokenise a source line for easier processing
 module Idris.IDEMode.TokenLine
 
-import Parser.Lexer
+import Parser.Lexer.Source
 import Text.Lexer
 
 public export

src/Idris/Main.idr

@@ -177,16 +177,15 @@ stMain opts
                        setOutput (IDEMode 0 stdin stdout)
                        replIDE {c} {u} {m}
                      else do
-                       throw (InternalError "Not implemeted yet")
---                        let (host, port) = ideSocketModeHostPort opts
---                        f <- coreLift $ initIDESocketFile host port
---                        case f of
---                          Left err => do
---                            coreLift $ putStrLn err
---                            coreLift $ exit 1
---                          Right file => do
---                            setOutput (IDEMode 0 file file)
---                            replIDE {c} {u} {m}
+                       let (host, port) = ideSocketModeHostPort opts
+                       f <- coreLift $ initIDESocketFile host port
+                       case f of
+                         Left err => do
+                           coreLift $ putStrLn err
+                           coreLift $ exitWith (ExitFailure 1)
+                         Right file => do
+                           setOutput (IDEMode 0 file file)
+                           replIDE {c} {u} {m}
                    else do
                        repl {c} {u} {m}
                        showTimeRecord

src/Idris/Package.idr

@@ -23,7 +23,7 @@ import Idris.REPLOpts
 import Idris.SetOptions
 import Idris.Syntax
 import Idris.Version
-import Parser.Lexer
+import Parser.Lexer.Source
 import Parser.Source
 import Utils.Binary
 
@@ -114,7 +114,7 @@ data DescField : Type where
   PPreclean    : FC -> String -> DescField
   PPostclean   : FC -> String -> DescField
 
-field : String -> Rule DescField
+field : String -> SourceRule DescField
 field fname
       = strField PVersion "version"
     <|> strField PAuthors "authors"
@@ -142,23 +142,23 @@ field fname
                       (do start <- location
                           ns <- nsIdent
                           end <- location
-                          pure (MkFC fname start end, ns))
-           pure (PModules ms)
+                          Parser.Core.pure (MkFC fname start end, ns))
+           Parser.Core.pure (PModules ms)
     <|> do exactIdent "main"; symbol "="
            start <- location
            m <- nsIdent
            end <- location
-           pure (PMainMod (MkFC fname start end) m)
+           Parser.Core.pure (PMainMod (MkFC fname start end) m)
     <|> do exactIdent "executable"; symbol "="
            e <- unqualifiedName
-           pure (PExec e)
+           Parser.Core.pure (PExec e)
   where
     getStr : (FC -> String -> DescField) -> FC ->
-             String -> Constant -> EmptyRule DescField
+             String -> Constant -> SourceEmptyRule DescField
     getStr p fc fld (Str s) = pure (p fc s)
     getStr p fc fld _ = fail $ fld ++ " field must be a string"
 
-    strField : (FC -> String -> DescField) -> String -> Rule DescField
+    strField : (FC -> String -> DescField) -> String -> SourceRule DescField
     strField p f
         = do start <- location
              exactIdent f
@@ -167,7 +167,7 @@ field fname
              end <- location
              getStr p (MkFC fname start end) f c
 
-parsePkgDesc : String -> Rule (String, List DescField)
+parsePkgDesc : String -> SourceRule (String, List DescField)
 parsePkgDesc fname
     = do exactIdent "package"
          name <- unqualifiedName

src/Idris/Parser.idr

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

src/Idris/ProcessIdr.idr

@@ -14,6 +14,7 @@ import Core.Unify
 import Parser.Unlit
 
 import TTImp.Elab.Check
+import TTImp.ProcessDecls
 import TTImp.TTImp
 
 import Idris.Desugar
@@ -50,7 +51,8 @@ processDecls decls
              | Just err => pure (case mapMaybe id xs of
                                       [] => [err]
                                       errs => errs)
-         pure (mapMaybe id xs)
+         errs <- getTotalityErrors
+         pure (mapMaybe id xs ++ errs)
 
 readModule : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->

src/Idris/REPL.idr

@@ -69,6 +69,7 @@ showInfo (n, idx, d)
                                show !(traverse getFullName (keys (refersTo d))))
          coreLift $ putStrLn ("Refers to (runtime): " ++
                                show !(traverse getFullName (keys (refersToRuntime d))))
+         coreLift $ putStrLn ("Flags: " ++ show (flags d))
          when (not (isNil (sizeChange d))) $
             let scinfo = map (\s => show (fnCall s) ++ ": " ++
                                     show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in
@@ -741,10 +742,10 @@ processCatch cmd
                            pure $ REPLError !(display err)
                            )
 
-parseEmptyCmd : EmptyRule (Maybe REPLCmd)
+parseEmptyCmd : SourceEmptyRule (Maybe REPLCmd)
 parseEmptyCmd = eoi *> (pure Nothing)
 
-parseCmd : EmptyRule (Maybe REPLCmd)
+parseCmd : SourceEmptyRule (Maybe REPLCmd)
 parseCmd = do c <- command; eoi; pure $ Just c
 
 export
@@ -819,6 +820,7 @@ mutual
       prompt NormaliseAll = ""
       prompt Execute = "[exec] "
 
+  export
   handleMissing : MissedResult -> String
   handleMissing (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs
   handleMissing (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function"
@@ -871,6 +873,7 @@ mutual
   displayResult  (OptionsSet opts) = printResult $ showSep "\n" $ map show opts
   displayResult  _ = pure ()
 
+  export
   displayHelp : String
   displayHelp =
     showSep "\n" $ map cmdInfo help

src/Idris/Resugar.idr

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

src/Idris/Syntax.idr

@@ -96,7 +96,8 @@ mutual
        -- Debugging
        PUnifyLog : FC -> Nat -> PTerm -> PTerm
 
-       -- TODO: 'with' disambiguation
+       -- with-disambiguation
+       PWithUnambigNames : FC -> List Name -> PTerm -> PTerm
 
   public export
   data PFieldUpdate : Type where
@@ -493,6 +494,8 @@ mutual
         = showPrec d rec ++ concatMap show fields
     showPrec d (PRecordProjection fc fields)
         = concatMap show fields
+    showPrec d (PWithUnambigNames fc ns rhs)
+        = "with " ++ show ns ++ " " ++ showPrec d rhs
 
 public export
 record IFaceInfo where
@@ -500,7 +503,7 @@ record IFaceInfo where
   iconstructor : Name
   params : List Name
   parents : List RawImp
-  methods : List (Name, RigCount, Bool, RawImp)
+  methods : List (Name, RigCount, TotalReq, Bool, RawImp)
      -- ^ name, whether a data method, and desugared type (without constraint)
   defaults : List (Name, List ImpClause)
 
@@ -776,6 +779,9 @@ mapPTermM f = goPTerm where
       >>= f
     goPTerm (PRecordProjection fc fields) =
       f (PRecordProjection fc fields)
+    goPTerm (PWithUnambigNames fc ns rhs) =
+      PWithUnambigNames fc ns <$> goPTerm rhs
+      >>= f
 
     goPFieldUpdate : PFieldUpdate -> Core PFieldUpdate
     goPFieldUpdate (PSetField p t)    = PSetField p <$> goPTerm t

src/Parser/Lexer/Common.idr

@@ -0,0 +1,47 @@
+module Parser.Lexer.Common
+
+import public Text.Lexer
+
+%default total
+
+||| In `comment` we are careful not to parse closing delimiters as
+||| valid comments. i.e. you may not write many dashes followed by
+||| a closing brace and call it a valid comment.
+export
+comment : Lexer
+comment
+   =  is '-' <+> is '-'                  -- comment opener
+  <+> many (is '-') <+> reject (is '}')  -- not a closing delimiter
+  <+> many (isNot '\n')                  -- till the end of line
+
+-- Identifier Lexer
+-- There are multiple variants.
+
+public export
+data Flavour = Capitalised | AllowDashes | Normal
+
+export
+isIdentStart : Flavour -> Char -> Bool
+isIdentStart _           '_' = True
+isIdentStart Capitalised  x  = isUpper x || x > chr 160
+isIdentStart _            x  = isAlpha x || x > chr 160
+
+export
+isIdentTrailing : Flavour -> Char -> Bool
+isIdentTrailing AllowDashes '-'  = True
+isIdentTrailing _           '\'' = True
+isIdentTrailing _           '_'  = True
+isIdentTrailing _            x   = isAlphaNum x || x > chr 160
+
+export %inline
+isIdent : Flavour -> String -> Bool
+isIdent flavour string =
+  case unpack string of
+    []      => False
+    (x::xs) => isIdentStart flavour x && all (isIdentTrailing flavour) xs
+
+export %inline
+ident : Flavour -> Lexer
+ident flavour =
+  (pred $ isIdentStart flavour) <+>
+    (many . pred $ isIdentTrailing flavour)

src/Parser/Lexer/Source.idr

@@ -1,9 +1,10 @@
-module Parser.Lexer
+module Parser.Lexer.Source
+
+import public Parser.Lexer.Common
 
 import Data.List
 import Data.Strings
 
-import public Text.Lexer
 import Utils.Hex
 import Utils.Octal
 import Utils.String
@@ -52,17 +53,7 @@ Show SourceToken where
       dotSep [x] = x
       dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs]
 
-||| In `comment` we are careful not to parse closing delimiters as
-||| valid comments. i.e. you may not write many dashes followed by
-||| a closing brace and call it a valid comment.
-comment : Lexer
-comment
-   =  is '-' <+> is '-'                  -- comment opener
-  <+> many (is '-') <+> reject (is '}')  -- not a closing delimiter
-  <+> many (isNot '\n')                  -- till the end of line
-
 mutual
-
   ||| The mutually defined functions represent different states in a
   ||| small automaton.
   ||| `toEndComment` is the default state and it will munch through
@@ -111,35 +102,6 @@ blockComment = is '{' <+> is '-' <+> toEndComment 1
 docComment : Lexer
 docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')
 
--- Identifier Lexer
--- There are multiple variants.
-
-data Flavour = Capitalised | AllowDashes | Normal
-
-isIdentStart : Flavour -> Char -> Bool
-isIdentStart _           '_' = True
-isIdentStart Capitalised  x  = isUpper x || x > chr 160
-isIdentStart _            x  = isAlpha x || x > chr 160
-
-isIdentTrailing : Flavour -> Char -> Bool
-isIdentTrailing AllowDashes '-'  = True
-isIdentTrailing _           '\'' = True
-isIdentTrailing _           '_'  = True
-isIdentTrailing _            x   = isAlphaNum x || x > chr 160
-
-%inline
-isIdent : Flavour -> String -> Bool
-isIdent flavour string =
-  case unpack string of
-    []      => False
-    (x::xs) => isIdentStart flavour x && all (isIdentTrailing flavour) xs
-
-%inline
-ident : Flavour -> Lexer
-ident flavour =
-  (pred $ isIdentStart flavour) <+>
-    (many . pred $ isIdentTrailing flavour)
-
 export
 isIdentNormal : String -> Bool
 isIdentNormal = isIdent Normal

src/Parser/Rule/Common.idr

@@ -0,0 +1,26 @@
+module Parser.Rule.Common
+
+import public Text.Lexer
+import public Text.Parser
+
+%default total
+
+public export
+Rule : Type -> Type -> Type
+Rule token ty = Grammar (TokenData token) True ty
+
+public export
+EmptyRule : Type -> Type -> Type
+EmptyRule token ty = Grammar (TokenData token) False ty
+
+export
+location : {token : _} -> EmptyRule token (Int, Int)
+location
+    = do tok <- peek
+         pure (line tok, col tok)
+
+export
+column : {token : _ } -> EmptyRule token Int
+column
+    = do (line, col) <- location
+         pure col

src/Parser/Rule/Source.idr

@@ -1,38 +1,23 @@
-module Parser.Rule
+module Parser.Rule.Source
 
-import public Parser.Lexer
+import public Parser.Lexer.Source
+import public Parser.Rule.Common
 import public Parser.Support
-import public Text.Lexer
-import public Text.Parser
 
 import Core.TT
 
 %default total
 
 public export
-Rule : Type -> Type
-Rule ty = Grammar (TokenData SourceToken) True ty
+SourceRule : Type -> Type
+SourceRule = Rule SourceToken
 
 public export
-EmptyRule : Type -> Type
-EmptyRule ty = Grammar (TokenData SourceToken) False ty
-
--- Some basic parsers used by all the intermediate forms
+SourceEmptyRule : Type -> Type
+SourceEmptyRule = EmptyRule SourceToken
 
 export
-location : EmptyRule (Int, Int)
-location
-    = do tok <- peek
-         pure (line tok, col tok)
-
-export
-column : EmptyRule Int
-column
-    = do (line, col) <- location
-         pure col
-
-export
-eoi : EmptyRule ()
+eoi : SourceEmptyRule ()
 eoi
     = do nextIs "Expected end of input" (isEOI . tok)
          pure ()
@@ -42,7 +27,7 @@ eoi
     isEOI _ = False
 
 export
-constant : Rule Constant
+constant : SourceRule Constant
 constant
     = terminal "Expected constant"
                (\x => case tok x of
@@ -62,7 +47,7 @@ constant
                            _ => Nothing)
 
 export
-intLit : Rule Integer
+intLit : SourceRule Integer
 intLit
     = terminal "Expected integer literal"
                (\x => case tok x of
@@ -70,7 +55,7 @@ intLit
                            _ => Nothing)
 
 export
-strLit : Rule String
+strLit : SourceRule String
 strLit
     = terminal "Expected string literal"
                (\x => case tok x of
@@ -78,7 +63,7 @@ strLit
                            _ => Nothing)
 
 export
-recField : Rule Name
+recField : SourceRule Name
 recField
     = terminal "Expected record field"
                (\x => case tok x of
@@ -86,7 +71,7 @@ recField
                            _ => Nothing)
 
 export
-symbol : String -> Rule ()
+symbol : String -> SourceRule ()
 symbol req
     = terminal ("Expected '" ++ req ++ "'")
                (\x => case tok x of
@@ -95,7 +80,7 @@ symbol req
                            _ => Nothing)
 
 export
-keyword : String -> Rule ()
+keyword : String -> SourceRule ()
 keyword req
     = terminal ("Expected '" ++ req ++ "'")
                (\x => case tok x of
@@ -104,7 +89,7 @@ keyword req
                            _ => Nothing)
 
 export
-exactIdent : String -> Rule ()
+exactIdent : String -> SourceRule ()
 exactIdent req
     = terminal ("Expected " ++ req)
                (\x => case tok x of
@@ -113,7 +98,7 @@ exactIdent req
                            _ => Nothing)
 
 export
-pragma : String -> Rule ()
+pragma : String -> SourceRule ()
 pragma n =
   terminal ("Expected pragma " ++ n)
     (\x => case tok x of
@@ -124,7 +109,7 @@ pragma n =
       _ => Nothing)
 
 export
-operator : Rule Name
+operator : SourceRule Name
 operator
     = terminal "Expected operator"
                (\x => case tok x of
@@ -134,7 +119,7 @@ operator
                                    else Just (UN s)
                            _ => Nothing)
 
-identPart : Rule String
+identPart : SourceRule String
 identPart
     = terminal "Expected name"
                (\x => case tok x of
@@ -142,7 +127,7 @@ identPart
                            _ => Nothing)
 
 export
-nsIdent : Rule (List String)
+nsIdent : SourceRule (List String)
 nsIdent
     = terminal "Expected namespaced name"
         (\x => case tok x of
@@ -150,11 +135,11 @@ nsIdent
             _ => Nothing)
 
 export
-unqualifiedName : Rule String
+unqualifiedName : SourceRule String
 unqualifiedName = identPart
 
 export
-holeName : Rule String
+holeName : SourceRule String
 holeName
     = terminal "Expected hole name"
                (\x => case tok x of
@@ -167,7 +152,7 @@ reservedNames
        "Lazy", "Inf", "Force", "Delay"]
 
 export
-name : Rule Name
+name : SourceRule Name
 name = opNonNS <|> do
   ns <- nsIdent
   opNS ns <|> nameNS ns
@@ -186,10 +171,10 @@ name = opNonNS <|> do
       then fail $ "can't use reserved name " ++ x
       else pure $ NS xs (UN x)
 
-  opNonNS : Rule Name
+  opNonNS : SourceRule Name
   opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")"
 
-  opNS : List String -> Rule Name
+  opNS : List String -> SourceRule Name
   opNS ns = do
     symbol ".("
     n <- (operator <|> recField)
@@ -204,23 +189,23 @@ export
 init : IndentInfo
 init = 0
 
-continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule ()
+continueF : SourceEmptyRule () -> (indent : IndentInfo) -> SourceEmptyRule ()
 continueF err indent
     = do eoi; err
   <|> do keyword "where"; err
-  <|> do col <- Rule.column
+  <|> do col <- Common.column
          if col <= indent
             then err
             else pure ()
 
 ||| Fail if this is the end of a block entry or end of file
 export
-continue : (indent : IndentInfo) -> EmptyRule ()
+continue : (indent : IndentInfo) -> SourceEmptyRule ()
 continue = continueF (fail "Unexpected end of expression")
 
 ||| As 'continue' but failing is fatal (i.e. entire parse fails)
 export
-mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule ()
+mustContinue : (indent : IndentInfo) -> Maybe String -> SourceEmptyRule ()
 mustContinue indent Nothing
    = continueF (fatalError "Unexpected end of expression") indent
 mustContinue indent (Just req)
@@ -242,7 +227,7 @@ Show ValidIndent where
   show (AfterPos i) = "[after " ++ show i ++ "]"
   show EndOfBlock = "[EOB]"
 
-checkValid : ValidIndent -> Int -> EmptyRule ()
+checkValid : ValidIndent -> Int -> SourceEmptyRule ()
 checkValid AnyIndent c = pure ()
 checkValid (AtPos x) c = if c == x
                             then pure ()
@@ -272,22 +257,22 @@ isTerminator _ = False
 ||| It's the end if we have a terminating token, or the next token starts
 ||| in or before indent. Works by looking ahead but not consuming.
 export
-atEnd : (indent : IndentInfo) -> EmptyRule ()
+atEnd : (indent : IndentInfo) -> SourceEmptyRule ()
 atEnd indent
     = eoi
   <|> do nextIs "Expected end of block" (isTerminator . tok)
          pure ()
-  <|> do col <- Rule.column
+  <|> do col <- Common.column
          if (col <= indent)
             then pure ()
             else fail "Not the end of a block entry"
 
 -- Check we're at the end, but only by looking at indentation
 export
-atEndIndent : (indent : IndentInfo) -> EmptyRule ()
+atEndIndent : (indent : IndentInfo) -> SourceEmptyRule ()
 atEndIndent indent
     = eoi
-  <|> do col <- Rule.column
+  <|> do col <- Common.column
          if col <= indent
             then pure ()
             else fail "Not the end of a block entry"
@@ -295,7 +280,7 @@ atEndIndent indent
 
 -- Parse a terminator, return where the next block entry
 -- must start, given where the current block entry started
-terminator : ValidIndent -> Int -> EmptyRule ValidIndent
+terminator : ValidIndent -> Int -> SourceEmptyRule ValidIndent
 terminator valid laststart
     = do eoi
          pure EndOfBlock
@@ -317,7 +302,7 @@ terminator valid laststart
    -- Expected indentation for the next token can either be anything (if
    -- we're inside a brace delimited block) or in exactly the initial column
    -- (if we're inside an indentation delimited block)
-   afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent
+   afterDedent : ValidIndent -> Int -> SourceEmptyRule ValidIndent
    afterDedent AnyIndent col
        = if col <= laststart
             then pure AnyIndent
@@ -333,8 +318,8 @@ terminator valid laststart
    afterDedent EndOfBlock col = pure EndOfBlock
 
 -- Parse an entry in a block
-blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->
-             Rule (ty, ValidIndent)
+blockEntry : ValidIndent -> (IndentInfo -> SourceRule ty) ->
+             SourceRule (ty, ValidIndent)
 blockEntry valid rule
     = do col <- column
          checkValid valid col
@@ -342,8 +327,8 @@ blockEntry valid rule
          valid' <- terminator valid col
          pure (p, valid')
 
-blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
-               EmptyRule (List ty)
+blockEntries : ValidIndent -> (IndentInfo -> SourceRule ty) ->
+               SourceEmptyRule (List ty)
 blockEntries valid rule
      = do eoi; pure []
    <|> do res <- blockEntry valid rule
@@ -352,7 +337,7 @@ blockEntries valid rule
    <|> pure []
 
 export
-block : (IndentInfo -> Rule ty) -> EmptyRule (List ty)
+block : (IndentInfo -> SourceRule ty) -> SourceEmptyRule (List ty)
 block item
     = do symbol "{"
          commit
@@ -368,33 +353,33 @@ block item
 ||| by curly braces). `rule` is a function of the actual indentation
 ||| level.
 export
-blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty)
+blockAfter : Int -> (IndentInfo -> SourceRule ty) -> SourceEmptyRule (List ty)
 blockAfter mincol item
     = do symbol "{"
          commit
          ps <- blockEntries AnyIndent item
          symbol "}"
          pure ps
-  <|> do col <- Rule.column
+  <|> do col <- Common.column
          if col <= mincol
             then pure []
             else blockEntries (AtPos col) item
 
 export
-blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty)
+blockWithOptHeaderAfter : Int -> (IndentInfo -> SourceRule hd) -> (IndentInfo -> SourceRule ty) -> SourceEmptyRule (Maybe hd, List ty)
 blockWithOptHeaderAfter {ty} mincol header item
     = do symbol "{"
          commit
          hidt <- optional $ blockEntry AnyIndent header
          restOfBlock hidt
-  <|> do col <- Rule.column
+  <|> do col <- Common.column
          if col <= mincol
             then pure (Nothing, [])
             else do hidt <- optional $ blockEntry (AtPos col) header
                     ps <- blockEntries (AtPos col) item
                     pure (map fst hidt, ps)
   where
-  restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)
+  restOfBlock : Maybe (hd, ValidIndent) -> SourceRule (Maybe hd, List ty)
   restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
                                    symbol "}"
                                    pure (Just h, ps)
@@ -403,7 +388,7 @@ blockWithOptHeaderAfter {ty} mincol header item
                            pure (Nothing, ps)
 
 export
-nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
+nonEmptyBlock : (IndentInfo -> SourceRule ty) -> SourceRule (List ty)
 nonEmptyBlock item
     = do symbol "{"
          commit

src/Parser/Source.idr

@@ -1,7 +1,7 @@
 module Parser.Source
 
-import public Parser.Lexer
-import public Parser.Rule
+import public Parser.Lexer.Source
+import public Parser.Rule.Source
 import public Parser.Unlit
 import public Text.Lexer
 import public Text.Parser
@@ -27,7 +27,7 @@ runParser : {e : _} ->
 runParser lit = runParserTo lit (const False)
 
 export
-parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty)
+parseFile : (fn : String) -> SourceRule ty -> IO (Either ParseError ty)
 parseFile fn p
     = do Right str <- readFile fn
              | Left err => pure (Left (FileFail err))

src/Parser/Support.idr

@@ -1,6 +1,6 @@
 module Parser.Support
 
-import public Parser.Lexer
+import public Parser.Lexer.Source
 import public Text.Lexer
 import public Text.Parser
 

src/TTImp/Elab/Ambiguity.idr

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

src/TTImp/Elab/App.idr

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

src/TTImp/Elab/Case.idr

@@ -226,7 +226,15 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- Start with empty nested names, since we've extended the rhs with
          -- ICaseLocal so they'll get rebuilt with the right environment
          let nest' = MkNested []
+         ust <- get UST
+         -- We don't want to keep rechecking delayed elaborators in the
+         -- case block, because they're not going to make progress until
+         -- we come out again, so save them
+         let olddelayed = delayedElab ust
+         put UST (record { delayedElab = [] } ust)
          processDecl [InCase] nest' [] (IDef fc casen alts')
+         ust <- get UST
+         put UST (record { delayedElab = olddelayed } ust)
 
          pure (appTm, gnf env caseretty)
   where

src/TTImp/Elab/Check.idr

@@ -127,17 +127,22 @@ record EState (vars : List Name) where
   allPatVars : List Name
                   -- Holes standing for pattern variables, which we'll delete
                   -- once we're done elaborating
-  allowDelay : Bool -- Delaying elaborators is okay. We can't nest delays.
+  delayDepth : Nat -- if it gets too deep, it gets slow, so fail quicker
   linearUsed : List (Var vars)
   saveHoles : NameMap () -- things we'll need to save to TTC, even if solved
 
+  unambiguousNames : StringMap (Name, Int, GlobalDef)
+                  -- Mapping from userNameRoot to fully resolved names.
+                  -- For names in this mapping, we don't run disambiguation.
+                  -- Used in with-expressions.
+
 export
 data EST : Type where
 
 export
 initEStateSub : {outer : _} ->
                 Int -> Env Term outer -> SubVars outer vars -> EState vars
-initEStateSub n env sub = MkEState n env sub [] [] [] [] [] True [] empty
+initEStateSub n env sub = MkEState n env sub [] [] [] [] [] Z [] empty empty
 
 export
 initEState : {vars : _} ->
@@ -165,9 +170,10 @@ weakenedEState {e}
                               (bindIfUnsolved est)
                               (lhsPatVars est)
                               (allPatVars est)
-                              (allowDelay est)
+                              (delayDepth est)
                               (map weaken (linearUsed est))
-                              (saveHoles est))
+                              (saveHoles est)
+                              (unambiguousNames est))
          pure eref
   where
     wknTms : (Name, ImplBinding vs) ->
@@ -197,9 +203,10 @@ strengthenedEState {n} {vars} c e fc env
                         (bindIfUnsolved est)
                         (lhsPatVars est)
                         (allPatVars est)
-                        (allowDelay est)
+                        (delayDepth est)
                         (mapMaybe dropTop (linearUsed est))
-                        (saveHoles est))
+                        (saveHoles est)
+                        (unambiguousNames est))
   where
     dropSub : SubVars xs (y :: ys) -> Core (SubVars xs ys)
     dropSub (DropCons sub) = pure sub
@@ -290,9 +297,10 @@ updateEnv env sub bif st
                (boundNames st) (toBind st) bif
                (lhsPatVars st)
                (allPatVars st)
-               (allowDelay st)
+               (delayDepth st)
                (linearUsed st)
                (saveHoles st)
+               (unambiguousNames st)
 
 export
 addBindIfUnsolved : {vars : _} ->
@@ -306,9 +314,10 @@ addBindIfUnsolved hn r p env tm ty st
                ((hn, r, (_ ** (env, p, tm, ty, subEnv st))) :: bindIfUnsolved st)
                (lhsPatVars st)
                (allPatVars st)
-               (allowDelay st)
+               (delayDepth st)
                (linearUsed st)
                (saveHoles st)
+               (unambiguousNames st)
 
 clearBindIfUnsolved : EState vars -> EState vars
 clearBindIfUnsolved st
@@ -317,9 +326,10 @@ clearBindIfUnsolved st
                (boundNames st) (toBind st) []
                (lhsPatVars st)
                (allPatVars st)
-               (allowDelay st)
+               (delayDepth st)
                (linearUsed st)
                (saveHoles st)
+               (unambiguousNames st)
 
 -- Clear the 'toBind' list, except for the names given
 export

src/TTImp/Elab/Delayed.idr

@@ -40,6 +40,17 @@ mkClosedElab {vars = x :: vars} fc (b :: env) elab
     newBinder (Let c val ty) = Let c val ty
     newBinder b = Lam (multiplicity b) Explicit (binderType b)
 
+deeper : {auto e : Ref EST (EState vars)} ->
+         Core a -> Core a
+deeper elab
+    = do est <- get EST
+         let d = delayDepth est
+         put EST (record { delayDepth = 1 + d } est)
+         res <- elab
+         est <- get EST
+         put EST (record { delayDepth = d } est)
+         pure res
+
 -- Try the given elaborator; if it fails, and the error matches the
 -- predicate, make a hole and try it again later when more holes might
 -- have been resolved
@@ -57,10 +68,10 @@ delayOnFailure : {vars : _} ->
                  Core (Term vars, Glued vars)
 delayOnFailure fc rig env expected pred pri elab
     = do est <- get EST
-         handle (elab (not (allowDelay est)))
+         handle (elab False)
           (\err =>
               do est <- get EST
-                 if pred err && allowDelay est
+                 if pred err
                     then
                       do nm <- genName "delayed"
                          (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
@@ -70,7 +81,7 @@ delayOnFailure fc rig env expected pred pri elab
                          log 10 ("Due to error " ++ show err)
                          ust <- get UST
                          put UST (record { delayedElab $=
-                                 ((pri, ci, mkClosedElab fc env (elab True)) :: ) }
+                                 ((pri, ci, mkClosedElab fc env (deeper (elab True))) :: ) }
                                          ust)
                          pure (dtm, expected)
                     else throw err)
@@ -88,19 +99,16 @@ delayElab : {vars : _} ->
             Core (Term vars, Glued vars)
 delayElab {vars} fc rig env exp pri elab
     = do est <- get EST
-         if not (allowDelay est)
-            then elab
-            else do
-             nm <- genName "delayed"
-             expected <- mkExpected exp
-             (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
-             logGlueNF 5 ("Postponing elaborator " ++ show nm ++
-                          " for") env expected
-             ust <- get UST
-             put UST (record { delayedElab $=
-                     ((pri, ci, mkClosedElab fc env elab) :: ) }
-                             ust)
-             pure (dtm, expected)
+         nm <- genName "delayed"
+         expected <- mkExpected exp
+         (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
+         logGlueNF 5 ("Postponing elaborator " ++ show nm ++
+                      " for") env expected
+         ust <- get UST
+         put UST (record { delayedElab $=
+                 ((pri, ci, mkClosedElab fc env elab) :: ) }
+                         ust)
+         pure (dtm, expected)
   where
     mkExpected : Maybe (Glued vars) -> Core (Glued vars)
     mkExpected (Just ty) = pure ty
@@ -121,18 +129,74 @@ ambiguous (InRHS _ _ err) = ambiguous err
 ambiguous (WhenUnifying _ _ _ _ err) = ambiguous err
 ambiguous _ = False
 
+mutual
+  mismatchNF : {vars : _} ->
+               Defs -> NF vars -> NF vars -> Core Bool
+  mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)
+      = if xn /= yn
+           then pure True
+           else anyM (mismatch defs) (zip xargs yargs)
+  mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
+      = if xt /= yt
+           then pure True
+           else anyM (mismatch defs) (zip xargs yargs)
+  mismatchNF defs (NPrimVal _ xc) (NPrimVal _ yc) = pure (xc /= yc)
+  mismatchNF defs (NDelayed _ _ x) (NDelayed _ _ y) = mismatchNF defs x y
+  mismatchNF defs (NDelay _ _ _ x) (NDelay _ _ _ y)
+      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
+  mismatchNF _ _ _ = pure False
+
+  mismatch : {vars : _} ->
+             Defs -> (Closure vars, Closure vars) -> Core Bool
+  mismatch defs (x, y)
+      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
+
+contra : {vars : _} ->
+               Defs -> NF vars -> NF vars -> Core Bool
+-- Unlike 'impossibleOK', any mismatch indicates an unrecoverable error
+contra defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
+    = if xn /= yn
+         then pure True
+         else anyM (mismatch defs) (zip xargs yargs)
+contra defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
+    = if xt /= yt
+         then pure True
+         else anyM (mismatch defs) (zip xargs yargs)
+contra defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)
+contra defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure True
+contra defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure True
+contra defs x y = pure False
+
+-- Errors that might be recoverable later if we try again. Generally -
+-- ambiguity errors, type inference errors
+export
+recoverable : {auto c : Ref Ctxt Defs} ->
+              Error -> Core Bool
+recoverable (CantConvert _ env l r)
+   = do defs <- get Ctxt
+        pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
+recoverable (CantSolveEq _ env l r)
+   = do defs <- get Ctxt
+        pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
+recoverable (UndefinedName _ _) = pure False
+recoverable (InType _ _ err) = recoverable err
+recoverable (InCon _ _ err) = recoverable err
+recoverable (InLHS _ _ err) = recoverable err
+recoverable (InRHS _ _ err) = recoverable err
+recoverable (WhenUnifying _ _ _ _ err) = recoverable err
+recoverable _ = pure True
+
 data RetryError
-     = NoError
-     | AmbigError
+     = RecoverableErrors
      | AllErrors
 
 Show RetryError where
-  show NoError = "NoError"
-  show AmbigError = "AmbigError"
+  show RecoverableErrors = "RecoverableErrors"
   show AllErrors = "AllErrors"
 
 -- Try all the delayed elaborators. If there's a failure, we want to
 -- show the ambiguity errors first (since that's the likely cause)
+-- Return all the ones that need trying again
 retryDelayed' : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
@@ -140,14 +204,16 @@ retryDelayed' : {vars : _} ->
                 {auto e : Ref EST (EState vars)} ->
                 RetryError ->
                 List (Nat, Int, Core ClosedTerm) ->
-                Core ()
-retryDelayed' errmode [] = pure ()
-retryDelayed' errmode ((_, i, elab) :: ds)
+                List (Nat, Int, Core ClosedTerm) ->
+                Core (List (Nat, Int, Core ClosedTerm))
+retryDelayed' errmode acc [] = pure (reverse acc)
+retryDelayed' errmode acc (d@(_, i, elab) :: ds)
     = do defs <- get Ctxt
          Just Delayed <- lookupDefExact (Resolved i) (gamma defs)
-              | _ => retryDelayed' errmode ds
+              | _ => retryDelayed' errmode acc ds
          handle
-           (do log 5 ("Retrying delayed hole " ++ show !(getFullName (Resolved i)))
+           (do est <- get EST
+               log 5 (show (delayDepth est) ++ ": Retrying delayed hole " ++ show !(getFullName (Resolved i)))
                -- elab itself might have delays internally, so keep track of them
                ust <- get UST
                put UST (record { delayedElab = [] } ust)
@@ -160,15 +226,14 @@ retryDelayed' errmode ((_, i, elab) :: ds)
                logTerm 5 ("Resolved delayed hole " ++ show i) tm
                logTermNF 5 ("Resolved delayed hole NF " ++ show i) [] tm
                removeHole i
-               retryDelayed' errmode ds')
+               retryDelayed' errmode acc ds')
            (\err => do log 5 $ show errmode ++ ":Error in " ++ show !(getFullName (Resolved i))
                                 ++ "\n" ++ show err
                        case errmode of
-                         NoError => retryDelayed' errmode ds
-                         AmbigError =>
-                            if ambiguous err -- give up on ambiguity
+                         RecoverableErrors =>
+                            if not !(recoverable err)
                                then throw err
-                               else retryDelayed' errmode ds
+                               else retryDelayed' errmode (d :: acc) ds
                          AllErrors => throw err)
 
 export
@@ -180,9 +245,10 @@ retryDelayed : {vars : _} ->
                List (Nat, Int, Core ClosedTerm) ->
                Core ()
 retryDelayed ds
-    = do retryDelayed' NoError ds -- try everything again
-         retryDelayed' AmbigError ds -- fail on ambiguity error
-         retryDelayed' AllErrors ds -- fail on all errors
+    = do est <- get EST
+         ds <- retryDelayed' RecoverableErrors [] ds -- try everything again
+         retryDelayed' AllErrors [] ds -- fail on all errors
+         pure ()
 
 -- Run an elaborator, then all the delayed elaborators arising from it
 export
@@ -199,8 +265,9 @@ runDelays pri elab
          tm <- elab
          ust <- get UST
          log 2 $ "Rerunning delayed in elaborator"
-         handle (retryDelayed' AllErrors
-                     (reverse (filter hasPri (delayedElab ust))))
+         handle (do retryDelayed' AllErrors []
+                       (reverse (filter hasPri (delayedElab ust)))
+                    pure ())
                 (\err => do put UST (record { delayedElab = olddelayed } ust)
                             throw err)
          ust <- get UST

src/TTImp/Elab/Local.idr

@@ -37,7 +37,15 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
                                            -- fixes bug #115
          let nest' = record { names $= (names' ++) } nest
          let env' = dropLinear env
+         -- We don't want to keep rechecking delayed elaborators in the
+         -- locals  block, because they're not going to make progress until
+         -- we come out again, so save them
+         ust <- get UST
+         let olddelayed = delayedElab ust
+         put UST (record { delayedElab = [] } ust)
          traverse (processDecl [] nest' env') (map (updateName nest') nestdecls)
+         ust <- get UST
+         put UST (record { delayedElab = olddelayed } ust)
          check rig elabinfo nest' env scope expty
   where
     -- For the local definitions, don't allow access to linear things

src/TTImp/Elab/Term.idr

@@ -1,5 +1,7 @@
 module TTImp.Elab.Term
 
+import Data.StringMap
+
 import Core.Context
 import Core.Core
 import Core.Env
@@ -215,6 +217,36 @@ checkTerm rig elabinfo nest env (Implicit fc b) Nothing
             do est <- get EST
                put EST (addBindIfUnsolved nm rig Explicit env metaval ty est)
          pure (metaval, gnf env ty)
+checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
+    = do -- enter the scope -> add unambiguous names
+         est <- get EST
+         rns <- resolveNames fc ns
+         put EST $ record { unambiguousNames = mergeLeft rns (unambiguousNames est) } est
+
+         -- inside the scope -> check the RHS
+         result <- check rig elabinfo nest env rhs exp
+
+         -- exit the scope -> restore unambiguous names
+         newEST <- get EST
+         put EST $ record { unambiguousNames = unambiguousNames est } newEST
+
+         pure result
+  where
+    resolveNames : FC -> List Name -> Core (StringMap (Name, Int, GlobalDef))
+    resolveNames fc [] = pure empty
+    resolveNames fc (n :: ns) =
+      case userNameRoot n of
+        -- should never happen
+        Nothing => throw $ InternalError $ "non-UN in \"with\" LHS: " ++ show n
+        Just nRoot => do
+          -- this will always be a global name
+          -- so we lookup only among the globals
+          ctxt <- get Ctxt
+          rns <- lookupCtxtName n (gamma ctxt)
+          case rns of
+            []   => throw $ UndefinedName fc n
+            [rn] => insert nRoot rn <$> resolveNames fc ns
+            _    => throw $ AmbiguousName fc (map fst rns)
 
 -- Declared in TTImp.Elab.Check
 -- check : {vars : _} ->

src/TTImp/Elab/Utils.idr

@@ -7,6 +7,7 @@ import Core.Normalise
 import Core.TT
 import Core.Value
 
+import TTImp.Elab.Check
 import TTImp.TTImp
 
 detagSafe : Defs -> NF [] -> Core Bool
@@ -64,3 +65,9 @@ updateErasable n
          addDef n (record { eraseArgs = es,
                             safeErase = dtes } gdef)
          pure ()
+export
+wrapErrorC : List ElabOpt -> (Error -> Error) -> Core a -> Core a
+wrapErrorC opts err
+    = if InCase `elem` opts
+         then id
+         else wrapError err

src/TTImp/Interactive/GenerateDef.idr

@@ -10,7 +10,7 @@ import Core.TT
 import Core.Unify
 import Core.Value
 
-import Parser.Lexer
+import Parser.Lexer.Source
 
 import TTImp.Elab
 import TTImp.Elab.Check
@@ -33,7 +33,7 @@ fnName lhs (UN n)
       else "op"
 fnName lhs (NS _ n) = fnName lhs n
 fnName lhs (DN s _) = s
-fnName lhs n = show n
+fnName lhs n = nameRoot n
 
 -- Make the hole on the RHS have a unique name
 uniqueRHS : {auto c : Ref Ctxt Defs} ->

src/TTImp/Parser.idr

@@ -12,7 +12,7 @@ import        Data.List
 import        Data.List.Views
 import        Data.Strings
 
-topDecl : FileName -> IndentInfo -> Rule ImpDecl
+topDecl : FileName -> IndentInfo -> SourceRule ImpDecl
 -- All the clauses get parsed as one-clause definitions. Collect any
 -- neighbouring clauses with the same function name into one definition.
 export
@@ -26,7 +26,7 @@ collectDefs : List ImpDecl -> List ImpDecl
 %hide Lexer.Core.(<|>)
 %hide Prelude.(<|>)
 
-atom : FileName -> Rule RawImp
+atom : FileName -> SourceRule RawImp
 atom fname
     = do start <- location
          x <- constant
@@ -62,7 +62,7 @@ atom fname
          end <- location
          pure (IHole (MkFC fname start end) x)
 
-visOption : Rule Visibility
+visOption : SourceRule Visibility
 visOption
     = do keyword "public"
          keyword "export"
@@ -72,12 +72,12 @@ visOption
   <|> do keyword "private"
          pure Private
 
-visibility : EmptyRule Visibility
+visibility : SourceEmptyRule Visibility
 visibility
     = visOption
   <|> pure Private
 
-totalityOpt : Rule TotalReq
+totalityOpt : SourceRule TotalReq
 totalityOpt
     = do keyword "partial"
          pure PartialOK
@@ -86,11 +86,11 @@ totalityOpt
   <|> do keyword "covering"
          pure CoveringOnly
 
-fnOpt : Rule FnOpt
+fnOpt : SourceRule FnOpt
 fnOpt = do x <- totalityOpt
            pure $ Totality x
 
-fnDirectOpt : Rule FnOpt
+fnDirectOpt : SourceRule FnOpt
 fnDirectOpt
     = do pragma "hint"
          pure (Hint True)
@@ -105,7 +105,7 @@ fnDirectOpt
   <|> do pragma "extern"
          pure ExternFn
 
-visOpt : Rule (Either Visibility FnOpt)
+visOpt : SourceRule (Either Visibility FnOpt)
 visOpt
     = do vis <- visOption
          pure (Left vis)
@@ -115,7 +115,7 @@ visOpt
          pure (Right opt)
 
 getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) ->
-                EmptyRule Visibility
+               SourceEmptyRule Visibility
 getVisibility Nothing [] = pure Private
 getVisibility (Just vis) [] = pure vis
 getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs
@@ -127,7 +127,7 @@ getRight : Either a b -> Maybe b
 getRight (Left _) = Nothing
 getRight (Right v) = Just v
 
-bindSymbol : Rule (PiInfo RawImp)
+bindSymbol : SourceRule (PiInfo RawImp)
 bindSymbol
     = do symbol "->"
          pure Explicit
@@ -135,7 +135,7 @@ bindSymbol
          pure AutoImplicit
 
 mutual
-  appExpr : FileName -> IndentInfo -> Rule RawImp
+  appExpr : FileName -> IndentInfo -> SourceRule RawImp
   appExpr fname indents
       = case_ fname indents
     <|> lazy fname indents
@@ -155,7 +155,7 @@ mutual
           = applyExpImp start end (IImplicitApp (MkFC fname start end) f n imp) args
 
   argExpr : FileName -> IndentInfo ->
-            Rule (Either RawImp (Maybe Name, RawImp))
+            SourceRule (Either RawImp (Maybe Name, RawImp))
   argExpr fname indents
       = do continue indents
            arg <- simpleExpr fname indents
@@ -164,7 +164,7 @@ mutual
            arg <- implicitArg fname indents
            pure (Right arg)
 
-  implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, RawImp)
+  implicitArg : FileName -> IndentInfo -> SourceRule (Maybe Name, RawImp)
   implicitArg fname indents
       = do start <- location
            symbol "{"
@@ -183,7 +183,7 @@ mutual
            symbol "}"
            pure (Nothing, tm)
 
-  as : FileName -> IndentInfo -> Rule RawImp
+  as : FileName -> IndentInfo -> SourceRule RawImp
   as fname indents
       = do start <- location
            x <- unqualifiedName
@@ -192,7 +192,7 @@ mutual
            end <- location
            pure (IAs (MkFC fname start end) UseRight (UN x) pat)
 
-  simpleExpr : FileName -> IndentInfo -> Rule RawImp
+  simpleExpr : FileName -> IndentInfo -> SourceRule RawImp
   simpleExpr fname indents
       = as fname indents
     <|> atom fname
@@ -204,13 +204,13 @@ mutual
            symbol ")"
            pure e
 
-  multiplicity : EmptyRule (Maybe Integer)
+  multiplicity : SourceEmptyRule (Maybe Integer)
   multiplicity
       = do c <- intLit
            pure (Just c)
     <|> pure Nothing
 
-  getMult : Maybe Integer -> EmptyRule RigCount
+  getMult : Maybe Integer -> SourceEmptyRule RigCount
   getMult (Just 0) = pure erased
   getMult (Just 1) = pure linear
   getMult Nothing = pure top
@@ -223,7 +223,7 @@ mutual
            = IPi fc rig p n ty (pibindAll fc p rest scope)
 
   bindList : FileName -> FilePos -> IndentInfo ->
-             Rule (List (RigCount, Name, RawImp))
+             SourceRule (List (RigCount, Name, RawImp))
   bindList fname start indents
       = sepBy1 (symbol ",")
                (do rigc <- multiplicity
@@ -238,7 +238,7 @@ mutual
 
 
   pibindListName : FileName -> FilePos -> IndentInfo ->
-                   Rule (List (RigCount, Name, RawImp))
+                   SourceRule (List (RigCount, Name, RawImp))
   pibindListName fname start indents
        = do rigc <- multiplicity
             ns <- sepBy1 (symbol ",") unqualifiedName
@@ -256,13 +256,13 @@ mutual
                     pure (rig, n, ty))
 
   pibindList : FileName -> FilePos -> IndentInfo ->
-               Rule (List (RigCount, Maybe Name, RawImp))
+               SourceRule (List (RigCount, Maybe Name, RawImp))
   pibindList fname start indents
     = do params <- pibindListName fname start indents
          pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params
 
 
-  autoImplicitPi : FileName -> IndentInfo -> Rule RawImp
+  autoImplicitPi : FileName -> IndentInfo -> SourceRule RawImp
   autoImplicitPi fname indents
       = do start <- location
            symbol "{"
@@ -275,7 +275,7 @@ mutual
            end <- location
            pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
 
-  forall_ : FileName -> IndentInfo -> Rule RawImp
+  forall_ : FileName -> IndentInfo -> SourceRule RawImp
   forall_ fname indents
       = do start <- location
            keyword "forall"
@@ -290,7 +290,7 @@ mutual
            end <- location
            pure (pibindAll (MkFC fname start end) Implicit binders scope)
 
-  implicitPi : FileName -> IndentInfo -> Rule RawImp
+  implicitPi : FileName -> IndentInfo -> SourceRule RawImp
   implicitPi fname indents
       = do start <- location
            symbol "{"
@@ -301,7 +301,7 @@ mutual
            end <- location
            pure (pibindAll (MkFC fname start end) Implicit binders scope)
 
-  explicitPi : FileName -> IndentInfo -> Rule RawImp
+  explicitPi : FileName -> IndentInfo -> SourceRule RawImp
   explicitPi fname indents
       = do start <- location
            symbol "("
@@ -312,7 +312,7 @@ mutual
            end <- location
            pure (pibindAll (MkFC fname start end) exp binders scope)
 
-  lam : FileName -> IndentInfo -> Rule RawImp
+  lam : FileName -> IndentInfo -> SourceRule RawImp
   lam fname indents
       = do start <- location
            symbol "\\"
@@ -328,7 +328,7 @@ mutual
        bindAll fc ((rig, n, ty) :: rest) scope
            = ILam fc rig Explicit (Just n) ty (bindAll fc rest scope)
 
-  let_ : FileName -> IndentInfo -> Rule RawImp
+  let_ : FileName -> IndentInfo -> SourceRule RawImp
   let_ fname indents
       = do start <- location
            keyword "let"
@@ -353,7 +353,7 @@ mutual
            end <- location
            pure (ILocal (MkFC fname start end) (collectDefs ds) scope)
 
-  case_ : FileName -> IndentInfo -> Rule RawImp
+  case_ : FileName -> IndentInfo -> SourceRule RawImp
   case_ fname indents
       = do start <- location
            keyword "case"
@@ -364,14 +364,14 @@ mutual
            pure (let fc = MkFC fname start end in
                      ICase fc scr (Implicit fc False) alts)
 
-  caseAlt : FileName -> IndentInfo -> Rule ImpClause
+  caseAlt : FileName -> IndentInfo -> SourceRule ImpClause
   caseAlt fname indents
       = do start <- location
            lhs <- appExpr fname indents
            caseRHS fname indents start lhs
 
   caseRHS : FileName -> IndentInfo -> (Int, Int) -> RawImp ->
-            Rule ImpClause
+            SourceRule ImpClause
   caseRHS fname indents start lhs
       = do symbol "=>"
            continue indents
@@ -384,7 +384,7 @@ mutual
            end <- location
            pure (ImpossibleClause (MkFC fname start end) lhs)
 
-  record_ : FileName -> IndentInfo -> Rule RawImp
+  record_ : FileName -> IndentInfo -> SourceRule RawImp
   record_ fname indents
       = do start <- location
            keyword "record"
@@ -396,7 +396,7 @@ mutual
            end <- location
            pure (IUpdate (MkFC fname start end) fs sc)
 
-  field : FileName -> IndentInfo -> Rule IFieldUpdate
+  field : FileName -> IndentInfo -> SourceRule IFieldUpdate
   field fname indents
       = do path <- sepBy1 (symbol "->") unqualifiedName
            upd <- (do symbol "="; pure ISetField)
@@ -405,7 +405,7 @@ mutual
            val <- appExpr fname indents
            pure (upd path val)
 
-  rewrite_ : FileName -> IndentInfo -> Rule RawImp
+  rewrite_ : FileName -> IndentInfo -> SourceRule RawImp
   rewrite_ fname indents
       = do start <- location
            keyword "rewrite"
@@ -415,7 +415,7 @@ mutual
            end <- location
            pure (IRewrite (MkFC fname start end) rule tm)
 
-  lazy : FileName -> IndentInfo -> Rule RawImp
+  lazy : FileName -> IndentInfo -> SourceRule RawImp
   lazy fname indents
       = do start <- location
            exactIdent "Lazy"
@@ -439,7 +439,7 @@ mutual
            pure (IForce (MkFC fname start end) tm)
 
 
-  binder : FileName -> IndentInfo -> Rule RawImp
+  binder : FileName -> IndentInfo -> SourceRule RawImp
   binder fname indents
       = autoImplicitPi fname indents
     <|> forall_ fname indents
@@ -448,7 +448,7 @@ mutual
     <|> lam fname indents
     <|> let_ fname indents
 
-  typeExpr : FileName -> IndentInfo -> Rule RawImp
+  typeExpr : FileName -> IndentInfo -> SourceRule RawImp
   typeExpr fname indents
       = do start <- location
            arg <- appExpr fname indents
@@ -467,10 +467,10 @@ mutual
                   (mkPi start end a as)
 
   export
-  expr : FileName -> IndentInfo -> Rule RawImp
+  expr : FileName -> IndentInfo -> SourceRule RawImp
   expr = typeExpr
 
-tyDecl : FileName -> IndentInfo -> Rule ImpTy
+tyDecl : FileName -> IndentInfo -> SourceRule ImpTy
 tyDecl fname indents
     = do start <- location
          n <- name
@@ -483,7 +483,7 @@ tyDecl fname indents
 mutual
   parseRHS : (withArgs : Nat) ->
              FileName -> IndentInfo -> (Int, Int) -> RawImp ->
-             Rule (Name, ImpClause)
+             SourceRule (Name, ImpClause)
   parseRHS withArgs fname indents start lhs
       = do symbol "="
            commit
@@ -508,7 +508,7 @@ mutual
            let fc = MkFC fname start end
            pure (!(getFn lhs), ImpossibleClause fc lhs)
     where
-      getFn : RawImp -> EmptyRule Name
+      getFn : RawImp -> SourceEmptyRule Name
       getFn (IVar _ n) = pure n
       getFn (IApp _ f a) = getFn f
       getFn (IImplicitApp _ f _ a) = getFn f
@@ -518,7 +518,7 @@ mutual
   ifThenElse True t e = t
   ifThenElse False t e = e
 
-  clause : Nat -> FileName -> IndentInfo -> Rule (Name, ImpClause)
+  clause : Nat -> FileName -> IndentInfo -> SourceRule (Name, ImpClause)
   clause withArgs fname indents
       = do start <- location
            lhs <- expr fname indents
@@ -531,7 +531,7 @@ mutual
       applyArgs f [] = f
       applyArgs f ((fc, a) :: args) = applyArgs (IApp fc f a) args
 
-      parseWithArg : Rule (FC, RawImp)
+      parseWithArg : SourceRule (FC, RawImp)
       parseWithArg
           = do symbol "|"
                start <- location
@@ -539,14 +539,14 @@ mutual
                end <- location
                pure (MkFC fname start end, tm)
 
-definition : FileName -> IndentInfo -> Rule ImpDecl
+definition : FileName -> IndentInfo -> SourceRule ImpDecl
 definition fname indents
     = do start <- location
          nd <- clause 0 fname indents
          end <- location
          pure (IDef (MkFC fname start end) (fst nd) [snd nd])
 
-dataOpt : Rule DataOpt
+dataOpt : SourceRule DataOpt
 dataOpt
     = do exactIdent "noHints"
          pure NoHints
@@ -556,7 +556,7 @@ dataOpt
          ns <- some name
          pure (SearchBy ns)
 
-dataDecl : FileName -> IndentInfo -> Rule ImpData
+dataDecl : FileName -> IndentInfo -> SourceRule ImpData
 dataDecl fname indents
     = do start <- location
          keyword "data"
@@ -572,7 +572,7 @@ dataDecl fname indents
          end <- location
          pure (MkImpData (MkFC fname start end) n ty opts cs)
 
-recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp))
+recordParam : FileName -> IndentInfo -> SourceRule (List (Name, RigCount, PiInfo RawImp, RawImp))
 recordParam fname indents
     = do symbol "("
          start <- location
@@ -582,7 +582,7 @@ recordParam fname indents
   <|> do symbol "{"
          commit
          start <- location
-         info <- the (EmptyRule (PiInfo RawImp))
+         info <- the (SourceEmptyRule (PiInfo RawImp))
                  (pure  AutoImplicit <* keyword "auto"
               <|>(do
                   keyword "default"
@@ -597,7 +597,7 @@ recordParam fname indents
          end <- location
          pure [(n, top, Explicit, Implicit (MkFC fname start end) False)]
 
-fieldDecl : FileName -> IndentInfo -> Rule (List IField)
+fieldDecl : FileName -> IndentInfo -> SourceRule (List IField)
 fieldDecl fname indents
       = do symbol "{"
            commit
@@ -609,7 +609,7 @@ fieldDecl fname indents
            atEnd indents
            pure fs
   where
-    fieldBody : PiInfo RawImp -> Rule (List IField)
+    fieldBody : PiInfo RawImp -> SourceRule (List IField)
     fieldBody p
         = do start <- location
              ns <- sepBy1 (symbol ",") unqualifiedName
@@ -619,7 +619,7 @@ fieldDecl fname indents
              pure (map (\n => MkIField (MkFC fname start end)
                                        linear p (UN n) ty) ns)
 
-recordDecl : FileName -> IndentInfo -> Rule ImpDecl
+recordDecl : FileName -> IndentInfo -> SourceRule ImpDecl
 recordDecl fname indents
     = do start <- location
          vis <- visibility
@@ -638,14 +638,14 @@ recordDecl fname indents
                    IRecord fc Nothing vis
                            (MkImpRecord fc n params dc (concat flds)))
 
-namespaceDecl : Rule (List String)
+namespaceDecl : SourceRule (List String)
 namespaceDecl
     = do keyword "namespace"
          commit
          ns <- nsIdent
          pure ns
 
-directive : FileName -> IndentInfo -> Rule ImpDecl
+directive : FileName -> IndentInfo -> SourceRule ImpDecl
 directive fname indents
     = do pragma "logging"
          commit
@@ -672,7 +672,7 @@ directive fname indents
                    IPragma (\c, nest, env => setRewrite {c} fc eq rw))
     -}
 -- Declared at the top
--- topDecl : FileName -> IndentInfo -> Rule ImpDecl
+-- topDecl : FileName -> IndentInfo -> SourceRule ImpDecl
 topDecl fname indents
     = do start <- location
          vis <- visibility
@@ -720,14 +720,14 @@ collectDefs (d :: ds)
 
 -- full programs
 export
-prog : FileName -> Rule (List ImpDecl)
+prog : FileName -> SourceRule (List ImpDecl)
 prog fname
     = do ds <- nonEmptyBlock (topDecl fname)
          pure (collectDefs ds)
 
 -- TTImp REPL commands
 export
-command : Rule ImpREPL
+command : SourceRule ImpREPL
 command
     = do symbol ":"; exactIdent "t"
          tm <- expr "(repl)" init

src/TTImp/ProcessData.idr

@@ -92,7 +92,7 @@ checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc cn_in ty_raw)
          Nothing <- lookupCtxtExact cn (gamma defs)
              | Just gdef => throw (AlreadyDefined fc cn)
          ty <-
-             wrapError (InCon fc cn) $
+             wrapErrorC opts (InCon fc cn) $
                    checkTerm !(resolveName cn) InType opts nest env
                               (IBindHere fc (PI erased) ty_raw)
                               (gType fc)
@@ -107,8 +107,8 @@ checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc cn_in ty_raw)
          log 10 $ "Saving from " ++ show cn ++ ": " ++ show (keys (getMetas ty))
 
          case vis of
-              Public => do addHash cn
-                           addHash fullty
+              Public => do addHashWithNames cn
+                           addHashWithNames fullty
               _ => pure ()
          pure (MkCon fc cn !(getArity defs [] fullty) fullty)
 
@@ -255,7 +255,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
              | Just gdef => throw (AlreadyDefined fc n)
 
          (ty, _) <-
-             wrapError (InCon fc n) $
+             wrapErrorC eopts (InCon fc n) $
                     elabTerm !(resolveName n) InType eopts nest env
                               (IBindHere fc (PI erased) ty_raw)
                               (Just (gType dfc))
@@ -278,8 +278,8 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
 
          case vis of
               Private => pure ()
-              _ => do addHash n
-                      addHash fullty
+              _ => do addHashWithNames n
+                      addHashWithNames fullty
          pure ()
 
 processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
@@ -289,7 +289,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
          log 1 $ "Processing " ++ show n
          defs <- get Ctxt
          (ty, _) <-
-             wrapError (InCon fc n) $
+             wrapErrorC eopts (InCon fc n) $
                     elabTerm !(resolveName n) InType eopts nest env
                               (IBindHere fc (PI erased) ty_raw)
                               (Just (gType dfc))
@@ -323,8 +323,8 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
                           (TCon 0 arity [] [] defaultFlags [] [] Nothing))
          case vis of
               Private => pure ()
-              _ => do addHash n
-                      addHash fullty
+              _ => do addHashWithNames n
+                      addHashWithNames fullty
 
          -- Constructors are private if the data type as a whole is
          -- export

src/TTImp/ProcessDecls.idr

@@ -4,6 +4,7 @@ import Core.Context
 import Core.Core
 import Core.Env
 import Core.Metadata
+import Core.Termination
 import Core.UnifyState
 
 import Parser.Source
@@ -20,6 +21,8 @@ import TTImp.ProcessType
 import TTImp.TTImp
 
 import Data.List
+import Data.Maybe
+import Data.NameMap
 
 -- Implements processDecl, declared in TTImp.Elab.Check
 process : {vars : _} ->
@@ -54,6 +57,58 @@ process eopts nest env (ILog n)
 
 TTImp.Elab.Check.processDecl = process
 
+export
+checkTotalityOK : {auto c : Ref Ctxt Defs} ->
+                  Name -> Core (Maybe Error)
+checkTotalityOK n
+-- checkTotalityOK (NS _ n@(UN _)) -- top level user defined names only
+    = do defs <- get Ctxt
+         Just gdef <- lookupCtxtExact n (gamma defs)
+              | Nothing => pure Nothing
+--          let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
+-- TODO: Put the above back when totality checker is properly working
+         let treq = fromMaybe PartialOK (findSetTotal (flags gdef))
+         let tot = totality gdef
+         let fc = location gdef
+         log 3 $ show n ++ " must be: " ++ show treq
+         case treq of
+              PartialOK => pure Nothing
+              CoveringOnly => checkCovering fc (isCovering tot)
+              Total => checkTotality fc
+  where
+    checkCovering : FC -> Covering -> Core (Maybe Error)
+    checkCovering fc IsCovering = pure Nothing
+    checkCovering fc cov
+        = pure (Just (NotCovering fc n cov))
+
+    checkTotality : FC -> Core (Maybe Error)
+    checkTotality fc
+        = do checkTotal fc n -- checked lazily, so better calculate here
+             t <- getTotality fc n
+             err <- checkCovering fc (isCovering t)
+             maybe (case isTerminating t of
+                         NotTerminating p => pure (Just (NotTotal fc n p))
+                         _ => pure Nothing)
+                   (pure . Just) err
+
+    findSetTotal : List DefFlag -> Maybe TotalReq
+    findSetTotal [] = Nothing
+    findSetTotal (SetTotal t :: _) = Just t
+    findSetTotal (_ :: xs) = findSetTotal xs
+
+-- Check totality of all the names added in the file, and return a list of
+-- totality errors.
+-- Do this at the end of processing a file (or a batch of definitions) since
+-- they might be mutually dependent so we need all the definitions to be able
+-- to check accurately.
+export
+getTotalityErrors : {auto c : Ref Ctxt Defs} ->
+                    Core (List Error)
+getTotalityErrors
+    = do defs <- get Ctxt
+         errs <- traverse checkTotalityOK (keys (toSave defs))
+         pure (mapMaybe id errs)
+
 export
 processDecls : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->

src/TTImp/ProcessDef.idr

@@ -18,6 +18,7 @@ import Core.UnifyState
 import TTImp.BindImplicits
 import TTImp.Elab
 import TTImp.Elab.Check
+import TTImp.Elab.Utils
 import TTImp.Impossible
 import TTImp.PartialEval
 import TTImp.TTImp
@@ -252,7 +253,7 @@ checkLHS {vars} trans mult hashit n opts nest env fc lhs_in
                           then InTransform
                           else InLHS mult
          (lhstm, lhstyg) <-
-             wrapError (InLHS fc !(getFullName (Resolved n))) $
+             wrapErrorC opts (InLHS fc !(getFullName (Resolved n))) $
                      elabTerm n lhsMode opts nest env
                                 (IBindHere fc PATTERN lhs) Nothing
          logTerm 5 "Checked LHS term" lhstm
@@ -328,9 +329,10 @@ bindReq fc (b :: env) (DropCons p) ns tm
 --  * Every constructor of the family has a return type which conflicts with
 --    the given constructor's type
 hasEmptyPat : {vars : _} ->
+              {auto c : Ref Ctxt Defs} ->
               Defs -> Env Term vars -> Term vars -> Core Bool
 hasEmptyPat defs env (Bind fc x (PVar c p ty) sc)
-   = pure $ !(isEmpty defs !(nf defs env ty))
+   = pure $ !(isEmpty defs env !(nf defs env ty))
             || !(hasEmptyPat defs (PVar c p ty :: env) sc)
 hasEmptyPat defs env _ = pure False
 
@@ -387,14 +389,14 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
          log 5 $ "Checking RHS " ++ show rhs
          logEnv 5 "In env" env'
 
-         rhstm <- wrapError (InRHS fc !(getFullName (Resolved n))) $
+         rhstm <- wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
                        checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
          clearHoleLHS
 
          logTerm 3 "RHS term" rhstm
          when hashit $
-           do addHash lhstm'
-              addHash rhstm
+           do addHashWithNames lhstm'
+              addHashWithNames rhstm
 
          -- If the rhs is a hole, record the lhs in the metadata because we
          -- might want to split it interactively
@@ -411,7 +413,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
          let wmode
                = if isErased mult then InType else InExpr
 
-         (wval, gwvalTy) <- wrapError (InRHS fc !(getFullName (Resolved n))) $
+         (wval, gwvalTy) <- wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
                 elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing
          clearHoleLHS
 
@@ -471,7 +473,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
                          map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)
 
          log 3 $ "Applying to with argument " ++ show rhs_in
-         rhs <- wrapError (InRHS fc !(getFullName (Resolved n))) $
+         rhs <- wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
              checkTermSub n wmode opts nest' env' env sub' rhs_in
                           (gnf env' reqty)
 
@@ -720,6 +722,7 @@ processDef opts nest env fc n_in cs_in
              do calcRefs False atotal (Resolved nidx)
                 sc <- calculateSizeChange fc n
                 setSizeChange fc n sc
+                checkIfGuarded fc n
 
          md <- get MD -- don't need the metadata collected on the coverage check
          cov <- checkCoverage nidx ty mult cs
@@ -729,8 +732,7 @@ processDef opts nest env fc n_in cs_in
          -- If we're not in a case tree, compile all the outstanding case
          -- trees.
          when (not (elem InCase opts)) $
-           compileRunTime fc cov atotal
-
+              compileRunTime fc cov atotal
   where
     simplePat : forall vars . Term vars -> Bool
     simplePat (Local _ _ _ _) = True

src/TTImp/ProcessType.idr

@@ -33,6 +33,8 @@ processFnOpt : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> FnOpt -> Core ()
 processFnOpt fc ndef Inline
     = setFlag fc ndef Inline
+processFnOpt fc ndef TCInline
+    = setFlag fc ndef TCInline
 processFnOpt fc ndef (Hint d)
     = do defs <- get Ctxt
          Just ty <- lookupTyExact ndef (gamma defs)
@@ -264,7 +266,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
               | Just _ => throw (AlreadyDefined fc n)
 
          ty <-
-             wrapError (InType fc n) $
+             wrapErrorC eopts (InType fc n) $
                    checkTerm idx InType (HolesOkay :: eopts) nest env
                              (IBindHere fc (PI erased) ty_raw)
                              (gType fc)
@@ -301,5 +303,5 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))
 
          when (vis /= Private) $
-              do addHash n
-                 addHash ty
+              do addHashWithNames n
+                 addHashWithNames ty

src/TTImp/TTImp.idr

@@ -105,6 +105,9 @@ mutual
        -- at the end of elaborator
        Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp
 
+       -- with-disambiguation
+       IWithUnambigNames : FC -> List Name -> RawImp -> RawImp
+
   public export
   data IFieldUpdate : Type where
        ISetField : (path : List String) -> RawImp -> IFieldUpdate
@@ -170,6 +173,7 @@ mutual
       show (IType fc) = "%type"
       show (Implicit fc True) = "_"
       show (Implicit fc False) = "?"
+      show (IWithUnambigNames fc ns rhs) = "(%with " ++ show ns ++ " " ++ show rhs ++ ")"
 
   export
   Show IFieldUpdate where
@@ -179,6 +183,7 @@ mutual
   public export
   data FnOpt : Type where
        Inline : FnOpt
+       TCInline : FnOpt
        -- Flag means the hint is a direct hint, not a function which might
        -- find the result (e.g. chasing parent interface dictionaries)
        Hint : Bool -> FnOpt
@@ -196,6 +201,7 @@ mutual
   export
   Show FnOpt where
     show Inline = "%inline"
+    show TCInline = "%tcinline"
     show (Hint t) = "%hint " ++ show t
     show (GlobalHint t) = "%globalhint " ++ show t
     show ExternFn = "%extern"
@@ -210,6 +216,7 @@ mutual
   export
   Eq FnOpt where
     Inline == Inline = True
+    TCInline == TCInline = True
     (Hint x) == (Hint y) = x == y
     (GlobalHint x) == (GlobalHint y) = x == y
     ExternFn == ExternFn = True
@@ -587,6 +594,7 @@ getFC (IUnquote x _) = x
 getFC (IRunElab x _) = x
 getFC (IAs x _ _ _) = x
 getFC (Implicit x _) = x
+getFC (IWithUnambigNames x _ _) = x
 
 export
 apply : RawImp -> List RawImp -> RawImp
@@ -676,6 +684,8 @@ mutual
 
     toBuf b (Implicit fc i)
         = do tag 28; toBuf b fc; toBuf b i
+    toBuf b (IWithUnambigNames fc ns rhs)
+        = do tag 29; toBuf b ns; toBuf b rhs
 
     fromBuf b
         = case !getTag of
@@ -760,6 +770,10 @@ mutual
                28 => do fc <- fromBuf b
                         i <- fromBuf b
                         pure (Implicit fc i)
+               29 => do fc <- fromBuf b
+                        ns <- fromBuf b
+                        rhs <- fromBuf b
+                        pure (IWithUnambigNames fc ns rhs)
                _ => corrupt "RawImp"
 
   export
@@ -895,6 +909,7 @@ mutual
   export
   TTC FnOpt where
     toBuf b Inline = tag 0
+    toBuf b TCInline = tag 11
     toBuf b (Hint t) = do tag 1; toBuf b t
     toBuf b (GlobalHint t) = do tag 2; toBuf b t
     toBuf b ExternFn = tag 3
@@ -919,6 +934,7 @@ mutual
                8 => pure (Totality PartialOK)
                9 => pure Macro
                10 => do ns <- fromBuf b; pure (SpecArgs ns)
+               11 => pure TCInline
                _ => corrupt "FnOpt"
 
   export

support/c/Makefile

@@ -9,7 +9,8 @@ CFLAGS += -O2
 
 SRCS = $(wildcard *.c)
 ifeq ($(OS), windows)
-	SRCS += windows/win_utils.c
+	SRCS += windows/win_utils.c windows/win_hack.c
+	LDFLAGS += -lws2_32
 endif
 OBJS = $(SRCS:.c=.o)
 DEPS = $(OBJS:.o=.d)
@@ -26,7 +27,7 @@ $(LIBTARGET): $(OBJS)
 	$(RANLIB) $@
 
 $(DYLIBTARGET): $(OBJS)
-	$(CC) -shared $(LDFLAGS) -o $@ $^
+	$(CC) -shared -o $@ $^ $(LDFLAGS)
 
 
 -include $(DEPS)

support/c/windows/win_hack.c

@@ -0,0 +1,3 @@
+int chmod(char** str, int perm) {
+    return 0;
+}

support/gambit/support.scm

@@ -1,3 +1,12 @@
+;; Inspired by:
+;; https://github.com/gambit/gambit/blob/master/gsc/_t-x86.scm#L1106 #L1160
+(define (blodwen-os)
+  (cond
+    [(memq (cadr (system-type)) '(apple)) "darwin"]
+    [(memq (caddr (system-type)) '(linux-gnu)) "unix"]
+    [(memq (caddr (system-type)) '(mingw32 mingw64)) "windows"]
+    [else "unknown"]))
+
 ;; TODO Convert to macro
 (define (blodwen-read-args desc)
   (if (fx= (vector-ref desc 0) 0)

support/racket/support.rkt

@@ -127,7 +127,7 @@
 
 (define (blodwen-read-bytevec fname)
   (with-handlers
-    ([(lambda (x) #t) (lambda (exn) (make-bytevector 0))])
+    ([(lambda (x) #t) (lambda (exn) #f)])
     (let* [(h (open-file-input-port fname
                                     (file-options)
                                     (buffer-mode line) #f))

tests/Main.idr

@@ -7,6 +7,8 @@ import Data.Strings
 import System
 import System.Directory
 import System.File
+import System.Info
+import System.Path
 
 %default covering
 
@@ -40,7 +42,7 @@ idrisTests
        "basic036", "basic037", "basic038", "basic039", "basic040",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
-       "coverage005", "coverage006",
+       "coverage005", "coverage006", "coverage007",
        -- Error messages
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",
@@ -84,12 +86,14 @@ idrisTests
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
-       "reg015", "reg016", "reg017", "reg018", "reg019",
+       "reg015", "reg016", "reg017", "reg018", "reg019", "reg020",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
-       "total006",
+       "total006", "total007", "total008",
        -- The 'with' rule
-       "with001", "with002"]
+       "with001", "with002",
+       -- with-disambiguation
+       "with003"]
 
 typeddTests : List String
 typeddTests
@@ -147,6 +151,19 @@ fail err
     = do putStrLn err
          exitWith (ExitFailure 1)
 
+
+isWindows : Bool
+isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
+
+-- on Windows, we just ignore backslashes and slashes when comparing,
+-- similarity up to that is good enough. Leave errors that depend
+-- on the confusion of slashes and backslashes to unix machines.
+normalize : String -> String
+normalize str =
+    if isWindows
+      then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
+      else str
+
 runTest : Options -> String -> IO Bool
 runTest opts testPath
     = do changeDir testPath
@@ -186,8 +203,7 @@ runTest opts testPath
           b <- getAnswer
           when b $ do Right _ <- writeFile "expected" out
                           | Left err => print err
-                      pure ()
-
+                      pure () 
         runTest' : IO Bool
         runTest'
             = do putStr $ testPath ++ ": "
@@ -202,9 +218,9 @@ runTest opts testPath
                            else print FileNotFound
                          pure False
                      | Left err => do print err
-                                      pure False
-
-                 if (out == exp)
+                                      pure False 
+                 let result = normalize out == normalize exp
+                 if normalize out == normalize exp 
                     then putStrLn "success"
                     else do
                       putStrLn "FAILURE"
@@ -212,7 +228,7 @@ runTest opts testPath
                          then mayOverwrite (Just exp) out
                          else printExpectedVsOutput exp out
 
-                 pure (out == exp)
+                 pure result
 
 exists : String -> IO Bool
 exists f
@@ -228,9 +244,9 @@ firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
 pathLookup : IO (Maybe String)
 pathLookup = do
   path <- getEnv "PATH"
-  let pathList = split (== ':') $ fromMaybe "/usr/bin:/usr/local/bin" path
+  let pathList = split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
   let candidates = [p ++ "/" ++ x | p <- pathList,
-                                    x <- ["chez", "chezscheme9.5", "scheme"]]
+                                    x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
   firstExists candidates
 
 findChez : IO (Maybe String)

tests/Makefile

@@ -1,8 +1,12 @@
 INTERACTIVE ?= --interactive
 
-test: clean
+.PHONY: testbin test
+
+test:
+	./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --only $(only)
+
+testbin:
 	${IDRIS2_BOOT} --build tests.ipkg
-	@./build/exec/runtests $(IDRIS2) $(INTERACTIVE) --only $(only)
 
 clean:
 	$(RM) -r build

tests/chez/chez014/Echo.idr

@@ -1,12 +1,11 @@
 module Main
 
 import System
+import System.Info
 import Network.Socket
 import Network.Socket.Data
 import Network.Socket.Raw
 
-%cg chez libidris_net
-
 runServer : IO (Either String (Port, ThreadID))
 runServer = do
   Right sock <- socket AF_INET Stream 0
@@ -53,6 +52,7 @@ runClient serverPort = do
 
 main : IO ()
 main = do
+  when (os == "windows") (schemeCall () "load-shared-object" ["ws2_32"])
   Right (serverPort, tid) <- runServer
     | Left err => putStrLn $ "[server] " ++ err
   runClient serverPort

tests/chez/chez017/expected.in

@@ -1,7 +1,7 @@
 File Exists
 False
 True
-Just "__PWD__/testdir"
+Just "__PWD__testdir"
 1/1: Building dir (dir.idr)
 Main> Main> Bye for now!
 hello

tests/chez/chez017/gen_expected.sh

@@ -1,3 +1,8 @@
 #!/usr/bin/env sh
+if [ $OS = "windows" ]; then
+    MY_PWD="$(cygpath -m $(pwd))\\\\" 
+else
+    MY_PWD=$(pwd)/
+fi
 
-sed -e "s|__PWD__|$(pwd)|g" expected.in > expected
+sed -e "s|__PWD__|${MY_PWD}|g" expected.in > expected

tests/idris2/basic039/expected

@@ -8,6 +8,7 @@ Inferrable args: []
 Compiled: Constructor tag Just 0 arity 1 (newtype by 0)
 Refers to: []
 Refers to (runtime): []
+Flags: []
 Main> Main.MkBar ==> DataCon 0 1
 RigW
 Erasable args: []
@@ -17,4 +18,5 @@ Inferrable args: []
 Compiled: Constructor tag Just 0 arity 1
 Refers to: []
 Refers to (runtime): []
+Flags: []
 Main> Bye for now!

tests/idris2/coverage005/expected

@@ -1,7 +1,6 @@
 1/1: Building Cover (Cover.idr)
 Main> Main.zsym is total
-Main> Main.zsym':
-zsym' (NS _) _
+Main> Main.zsym': All cases covered
 Main> Main.foo is total
 Main> Main.bar is total
 Main> Bye for now!

tests/idris2/coverage006/Cover.idr

@@ -1,20 +0,0 @@
-import Data.Fin
-
-data NNat = NZ | NS NNat
-
-zsym : (x : NNat) -> x = NZ -> NZ = x
-zsym NZ Refl = Refl
-zsym (NS _) Refl impossible
-
-zsym' : (x : NNat) -> x = NZ -> NZ = x
-zsym' NZ Refl = Refl
-
-foo : Nat -> String
-foo 0 = "zero"
-foo 1 = "one"
-foo x = "something else"
-
-bar : Fin (S (S (S Z))) -> String
-bar 0 = "a"
-bar 1 = "b"
-bar 2 = "c"

tests/idris2/coverage007/eq.idr

@@ -0,0 +1,30 @@
+
+eq1 : (x : Nat) -> (x = S x) -> Nat
+eq1 x p impossible
+  
+eq2 : (x : Nat) -> (S x = Z) -> Nat
+eq2 x p impossible
+  
+eq3 : (x : Nat) -> (S (S x) = (S x)) -> Nat
+eq3 x p impossible
+  
+eq4 : (x : Nat) -> (S x = x) -> Nat
+eq4 x p impossible
+  
+eq5 : (x : Nat) -> (Z = S x) -> Nat
+eq5 x p impossible
+  
+eq6 : (x : Nat) -> (S x = (S (S x))) -> Nat
+eq6 x p impossible
+
+eqL1 : (xs : List a) -> (x :: xs = []) -> Nat
+eqL1 xs p impossible
+
+eqL2 : (xs : List a) -> (x :: xs = x :: y :: xs) -> Nat
+eqL2 xs p impossible
+
+badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
+badeq x y p impossible
+
+badeqL : (xs : List a) -> (ys : List a) -> (x :: xs = x :: y :: ys) -> Nat
+badeqL xs ys p impossible

tests/idris2/coverage007/expected

@@ -0,0 +1,3 @@
+1/1: Building eq (eq.idr)
+eq.idr:27:1--29:1:badeq x y p is not a valid impossible case
+eq.idr:30:1--31:1:badeqL xs ys p is not a valid impossible case

tests/idris2/coverage007/run

@@ -0,0 +1,3 @@
+$1 --no-banner eq.idr --check
+
+rm -rf build