Merge branch 'master' into master

.github/workflows/ci-lint.yml

@@ -9,9 +9,6 @@ on:
     branches:
       - master
 
-env:
-  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
-
 jobs:
   build:
     runs-on: ubuntu-latest

.github/workflows/ci-macos-combined.yml

@@ -12,7 +12,6 @@ on:
 env:
   SCHEME: chez
   IDRIS2_TESTS_CG: chez
-  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
 
 jobs:
 
@@ -27,7 +26,7 @@ jobs:
         run: |
           brew install chezscheme
           brew install coreutils
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
       - name: Build Idris 2 from bootstrap
         run: make bootstrap && make install
         shell: bash
@@ -54,7 +53,7 @@ jobs:
         run: |
           brew install chezscheme
           brew install coreutils
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
           chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
       - name: Build self-hosted
         run: make all && make install
@@ -83,7 +82,7 @@ jobs:
   #         brew install gambit-scheme
   #         CURRENTDIR=$(find /usr/local/Cellar/gambit-scheme -type l -name current)
   #         echo "::add-path::${CURRENTDIR}/bin"
-  #         echo "::add-path::$HOME/.idris2/bin"
+  #         echo "$HOME/.idris2/bin" >> $GITHUB_PATH
   #         chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
   #     - name: Test gambit
   #       run: cd tests/gambit/bitops001/ && ./run idris2

.github/workflows/ci-super-linter.yml

@@ -51,6 +51,7 @@ jobs:
         uses: github/super-linter@v3
         env:
           VALIDATE_ALL_CODEBASE: false
+          VALIDATE_CPP: false # C files predate linting
           VALIDATE_JSCPD: false  # erroneously complains about docs/requirements.txt
           VALIDATE_JAVASCRIPT_STANDARD: false #requires camel-casing
           DEFAULT_BRANCH: master

.github/workflows/ci-ubuntu-combined.yml

@@ -12,7 +12,6 @@ on:
       - main
 
 env:
-  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
   IDRIS2_VERSION: 0.3.0 # For previous-version build
   SCHEME: scheme
 
@@ -33,7 +32,7 @@ jobs:
       - name: Install build dependencies
         run: |
           sudo apt-get install -y chezscheme
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
       - name: Build from bootstrap
         run: make bootstrap && make install
       - name: Artifact Bootstrapped Idris2
@@ -53,7 +52,7 @@ jobs:
       - name: Install build dependencies
         run: |
           sudo apt-get install -y racket
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
       - name: Build from bootstrap
         run: make bootstrap-racket && make install
       - name: Artifact Bootstrapped Idris2
@@ -73,7 +72,7 @@ jobs:
       - name: Install build dependencies
         run: |
           sudo apt-get install -y chezscheme
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
       - name: Cache Chez Previous Version
         id: previous-version-cache
         uses: actions/cache@v2
@@ -120,7 +119,7 @@ jobs:
       - name: Install build dependencies
         run: |
           sudo apt-get install -y chezscheme
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
           chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
       - name: Build self-hosted
         run: make all && make install
@@ -144,7 +143,7 @@ jobs:
       - name: Install build dependencies
         run: |
           sudo apt-get install -y racket
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
           chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
       - name: Build self-hosted
         run: make all && make install
@@ -168,7 +167,7 @@ jobs:
       - name: Install build dependencies
         run: |
           sudo apt-get install -y chezscheme
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
           chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
       - name: Build from previous version
         run: make all && make install && make clean
@@ -199,7 +198,7 @@ jobs:
       - name: Install build dependencies
         run: |
           sudo apt-get install -y chezscheme
-          echo "::add-path::$HOME/.idris2/bin"
+          echo "$HOME/.idris2/bin" >> $GITHUB_PATH
           chmod +x $HOME/.idris2/bin/idris2 $HOME/.idris2/bin/idris2_app/*
       - name: Build API
         run: make install-api

.github/workflows/ci-windows.yml

@@ -14,7 +14,6 @@ env:
   SCHEME: scheme
   IDRIS2_TESTS_CG: chez
   CC: gcc
-  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
 
 jobs:
   build:
@@ -29,7 +28,7 @@ jobs:
         run: |
           git clone --depth 1 https://github.com/cisco/ChezScheme
           c:\msys64\usr\bin\bash -l -c "pacman -S --noconfirm tar make"
-          echo "::set-env name=PWD::$(c:\msys64\usr\bin\cygpath -u $(pwd))"
+          echo "PWD=$(c:\msys64\usr\bin\cygpath -u $(pwd))" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
       - name: Configure and Build Chez Scheme
         run: |
           c:\msys64\usr\bin\bash -l -c "cd $env:PWD && cd ChezScheme && ./configure --threads && make"
@@ -37,10 +36,10 @@ jobs:
         run: |
           $chez="$(pwd)\ChezScheme\ta6nt\bin\ta6nt"
           $idris="$(pwd)\.idris2"
-          echo "::add-path::$chez"
+          echo "$chez" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append
-          echo "::add-path::$idris\bin"
+          echo "$idris\bin" | Out-File -FilePath $env:GITHUB_PATH -Encoding utf8 -Append
-          echo "::set-env name=IDRIS_PREFIX::$idris"
+          echo "IDRIS_PREFIX=$idris" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
-          echo "::set-env name=PREFIX::$(c:\msys64\usr\bin\cygpath -u $idris)"
+          echo "PREFIX=$(c:\msys64\usr\bin\cygpath -u $idris)" | Out-File -FilePath $env:GITHUB_ENV -Encoding utf8 -Append
       - name: Test Scheme
         run: |
           scheme --version

CHANGELOG.md

@@ -11,7 +11,8 @@ Library changes:
   command line options, to `contrib`.
 * Monad transformers in `Control.Monad` where restructured
   and several new transformer types where added.
-* `Data.Colist` and `Data.Colist1` where added to `base`.
+* `Data.Colist` and `Data.Colist1` were added to `base`.
+* Add `Data.SnocList` to base and `data SnocList` to `Prelude.Types`.
 * `Data.Bits`, an interface for bitwise operations, was added to `base`.
 * Interfaces `Bifoldable` and `Bitraversable` were added to the `prelude`.
 * Interface `Data.Contravariant` for contravariant functors was added
@@ -29,6 +30,8 @@ Syntax changes:
   implicit parameters and give multiplicities for parameters. The old syntax
   is still available for compatibility purposes but will be removed in the
   future.
+* Add support for SnocList syntax: `[< 1, 2, 3]` desugars into `Lin :< 1 :< 2 :< 3`
+  and their semantic highlighting.
 
 Compiler changes:
 

INSTALL.md

@@ -10,7 +10,7 @@ The requirements are:
 
 - A Scheme compiler; either Chez Scheme (default), or Racket.
 - `bash`, with `realpath`. On Linux, you probably already have this.
-  On a Mac, you can install this with `brew install coreutils`.
+  On a macOS, you can install this with `brew install coreutils`.
   On FreeBSD, OpenBSD and NetBSD, you can install `realpath` and `GNU make`
   using a package manager.  For instance, on OpenBSD you can install all of them
   with `pkg_add coreutils gmake` command.

README.md

@@ -4,7 +4,7 @@ Idris 2
 [![Documentation Status](https://readthedocs.org/projects/idris2/badge/?version=latest)](https://idris2.readthedocs.io/en/latest/?badge=latest)
 [![Windows Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-windows.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-windows.yml)
 [![Ubuntu Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-ubuntu-combined.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-ubuntu-combined.yml)
-[![MacOS Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-macos-combined.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-macos-combined.yml)
+[![macOS Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-macos-combined.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-macos-combined.yml)
 [![Nix Status](https://github.com/idris-lang/Idris2/actions/workflows/ci-nix.yml/badge.svg)](https://github.com/idris-lang/Idris2/actions/workflows/ci-nix.yml)
 
 [Idris 2](https://idris-lang.org/) is a purely functional programming language

bootstrap/idris2-boot.sh

@@ -7,22 +7,12 @@ if [ -z "$SCHEME" ]; then
     exit 1
 fi
 
-case $(uname -s) in
+if [ "$(uname)" = Darwin ]; then
-    OpenBSD | FreeBSD | NetBSD)
+    DIR=$(zsh -c 'printf %s "$0:A:h"' "$0")
-        REALPATH="grealpath"
+else
-        ;;
+    DIR=$(dirname "$(readlink -f -- "$0")")
-
-    *)
-        REALPATH="realpath"
-        ;;
-esac
-
-if ! command -v "$REALPATH" >/dev/null; then
-    echo "$REALPATH is required for Chez code generator."
-    exit 1
 fi
 
-DIR=$(dirname "$($REALPATH "$0")")
 LD_LIBRARY_PATH="$DIR/idris2_app":$LD_LIBRARY_PATH
 PATH="$DIR/idris2_app":$PATH
 export LD_LIBRARY_PATH PATH

bootstrap/idris2-rktboot.sh

@@ -2,28 +2,12 @@
 
 set -e # exit on any error
 
-if [ -z "$IDRIS2_VERSION" ]; then
+if [ "$(uname)" = Darwin ]; then
-    echo "Required IDRIS2_VERSION env is not set."
+    DIR=$(zsh -c 'printf %s "$0:A:h"' "$0")
-    exit 1
+else
-fi
+    DIR=$(dirname "$(readlink -f -- "$0")")
-echo "Bootstrapping IDRIS2_VERSION=$IDRIS2_VERSION"
-
-case $(uname -s) in
-    OpenBSD | FreeBSD | NetBSD)
-        REALPATH="grealpath"
-        ;;
-
-    *)
-        REALPATH="realpath"
-        ;;
-esac
-
-if ! command -v "$REALPATH" >/dev/null; then
-    echo "$REALPATH is required for Racket code generator."
-    exit 1
 fi
 
-DIR=$(dirname "$($REALPATH "$0")")
 LD_LIBRARY_PATH="$DIR/idris2_app":$LD_LIBRARY_PATH
 PATH="$DIR/idris2_app":$PATH
 export LD_LIBRARY_PATH PATH

docs/source/reference/debugging.rst

@@ -0,0 +1,106 @@
+**********************
+Debugging The Compiler
+**********************
+
+Performance
+===========
+
+The compiler has the ``--timing`` flag to dump timing information collected during operation.
+
+The output documents, in reverse chronological order, the cumulative time taken for the operation (and sub operations) to complete.
+Sub levels are indicated by successive repetitions of ``+``.
+
+
+Logging
+=======
+
+The compiler logs various categories of information during operation at various levels.
+
+Log levels are characterised by two things:
+
++ a dot-separated path of ever finer topics of interest e.g. scope.let
++ a natural number corresponding to the verbosity level e.g. 5
+
+If the user asks for some logs by writing::
+
+    %logging "scope" 5
+
+they will get all of the logs whose path starts with `scope` and whose
+verbosity level is less or equal to `5`. By combining different logging
+directives, users can request information about everything (with a low
+level of details) and at the same time focus on a particular subsystem
+they want to get a lot of information about. For instance:::
+
+    %logging 1
+    %logging "scope.let" 10
+
+will deliver basic information about the various phases the compiler goes
+through and deliver a lot of information about scope-checking let binders.
+
+
+You can set the logging level at the command line using::
+
+    --log <level>
+
+and through the REPL using::
+
+    :log <string category> <level>
+
+    :logging <string category> <level>
+
+The supported logging categories can be found using the command line flag::
+
+    --help logging
+
+REPL Commands
+=============
+
+To see more debug information from the REPL there are several options one can set.
+
+.. csv-table:: Logging Categories
+   :header: "command", "description"
+   :widths: 20, 20
+
+   ``:di <name>``, show debugging information for a name
+   ``:set showimplicits``, show values of implicit arguments
+
+Compiler Flags
+==============
+
+There are several 'hidden' compiler flags that can help expose Idris' inner workings.
+
+.. csv-table:: Logging Categories
+   :header: "command", "description"
+   :widths: 20, 20
+
+   ``--dumpcases <file>``, dump case trees to the given file
+   ``--dumplifted <file>``, dump lambda lifted trees to the given file
+   ``--dumpanf <file>``, dump ANF to the given file
+   ``--dumpvmcode <file>``, dump VM Code to the given file
+   ``--debug-elab-check``, do more elaborator checks (currently conversion in LinearCheck)
+
+
+Output Formats
+==============
+
+Debug Output
+------------
+
+Calling ``:di <name>`` dumps debugging information about the selected term.
+Specifically dumped are:
+
+.. csv-table:: Debugging Information
+   :header: "topic", "description"
+   :widths: 20, 20
+
+   Full Name(s), The fully qualified name of the term.
+   Multiplicity, The terms multiplicity.
+   Erasable Arguments, Things that are erased.
+   Detaggable argument types,
+   Specialised arguments,
+   Inferrable arguments,
+   Compiled version,
+   Compile time linked terms,
+   Runtime linked terms,
+   Flags,
+   Size change graph,

docs/source/reference/index.rst

@@ -22,3 +22,4 @@ This is a placeholder, to get set up with readthedocs.
    literate
    overloadedlit
    builtins
+   debugging

docs/source/tutorial/starting.rst

@@ -90,7 +90,7 @@ which you can run:
     $ ./build/exec/hello
     Hello world
 
-(On Macos you may first need to install realpath: ```brew install coreutils```)
+(On macOS you may first need to install realpath: ```brew install coreutils```)
 
 Please note that the dollar sign ``$`` indicates the shell prompt!
 Some useful options to the Idris command are:

docs/source/tutorial/typesfuns.rst

@@ -737,13 +737,26 @@ Note that the constructor names are the same for each — constructor
 names (in fact, names in general) can be overloaded, provided that
 they are declared in different namespaces (see Section
 :ref:`sect-namespaces`), and will typically be resolved according to
-their type. As syntactic sugar, any type with the constructor names
+their type. As syntactic sugar, any implementation of the names
 ``Nil`` and ``::`` can be written in list form. For example:
 
 -  ``[]`` means ``Nil``
 
 -  ``[1,2,3]`` means ``1 :: 2 :: 3 :: Nil``
 
+Similarly, any implementation of the names ``Lin`` and ``:<`` can be
+written in **snoc**-list form:
+
+- ``[<]`` mean ``Lin``
+- ``[< 1, 2, 3]`` means ``Lin :< 1 :< 2 :< 3``.
+
+and the prelude includes a pre-defined datatype for snoc-lists:
+
+.. code-block:: idris
+
+    data SnocList a = Lin | (:<) (SnocList a) a
+
+
 The library also defines a number of functions for manipulating these
 types. ``map`` is overloaded both for ``List`` and ``Vect`` (we'll see more
 details of precisely how later when we cover interfaces in

idris2api.ipkg

@@ -73,7 +73,7 @@ modules =
     Idris.Desugar.Mutual,
     Idris.Env,
     Idris.Doc.HTML,
-    Idris.DocString,
+    Idris.Doc.String,
     Idris.Driver,
     Idris.Error,
     Idris.ModTree,

libs/base/Data/Buffer.idr

@@ -16,6 +16,7 @@ export
 data Buffer : Type where [external]
 
 %foreign "scheme:blodwen-buffer-size"
+         "C:idris2_getBufferSize, libidris2_support, idris_buffer.h"
          "node:lambda:b => BigInt(b.length)"
 prim__bufferSize : Buffer -> Int
 
@@ -24,6 +25,7 @@ rawSize : HasIO io => Buffer -> io Int
 rawSize buf = pure (prim__bufferSize buf)
 
 %foreign "scheme:blodwen-new-buffer"
+         "C:idris2_newBuffer, libidris2_support, idris_buffer.h"
          "node:lambda:s=>Buffer.alloc(Number(s))"
 prim__newBuffer : Int -> PrimIO Buffer
 
@@ -36,16 +38,22 @@ newBuffer size
 --             then pure Nothing
 --             else pure $ Just $ MkBuffer buf size 0
 
--- might be needed if we do this in C...
+%foreign "scheme:blodwen-buffer-free"
+         "C:idris2_freeBuffer, libidris2_support, idris_buffer.h"
+         "node:lambda:buf=>undefined"
+prim__freeBuffer : Buffer -> PrimIO ()
+
 export
 freeBuffer : HasIO io => Buffer -> io ()
-freeBuffer buf = pure ()
+freeBuffer buf = primIO (prim__freeBuffer buf)
 
 %foreign "scheme:blodwen-buffer-setbyte"
+         "C:idris2_setBufferByte, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset,value)=>buf.writeUInt8(Number(value), Number(offset))"
 prim__setByte : Buffer -> Int -> Int -> PrimIO ()
 
 %foreign "scheme:blodwen-buffer-setbyte"
+         "C:idris2_setBufferByte, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset,value)=>buf.writeUInt8(Number(value), Number(offset))"
 prim__setBits8 : Buffer -> Int -> Bits8 -> PrimIO ()
 
@@ -61,10 +69,12 @@ setBits8 buf loc val
     = primIO (prim__setBits8 buf loc val)
 
 %foreign "scheme:blodwen-buffer-getbyte"
+         "C:idris2_getBufferByte, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset)=>BigInt(buf.readUInt8(Number(offset)))"
 prim__getByte : Buffer -> Int -> PrimIO Int
 
 %foreign "scheme:blodwen-buffer-getbyte"
+         "C:idris2_getBufferByte, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset)=>BigInt(buf.readUInt8(Number(offset)))"
 prim__getBits8 : Buffer -> Int -> PrimIO Bits8
 
@@ -149,6 +159,7 @@ getInt32 buf loc
     = primIO (prim__getInt32 buf loc)
 
 %foreign "scheme:blodwen-buffer-setint"
+         "C:idris2_setBufferInt, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset,value)=>buf.writeInt64(Number(value), Number(offset))"
 prim__setInt : Buffer -> Int -> Int -> PrimIO ()
 
@@ -158,6 +169,7 @@ setInt buf loc val
     = primIO (prim__setInt buf loc val)
 
 %foreign "scheme:blodwen-buffer-getint"
+         "C:idris2_getBufferInt, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset)=>BigInt(buf.readInt64(Number(offset)))"
 prim__getInt : Buffer -> Int -> PrimIO Int
 
@@ -167,6 +179,7 @@ getInt buf loc
     = primIO (prim__getInt buf loc)
 
 %foreign "scheme:blodwen-buffer-setdouble"
+         "C:idris2_setBufferDouble, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, Number(offset))"
 prim__setDouble : Buffer -> Int -> Double -> PrimIO ()
 
@@ -176,6 +189,7 @@ setDouble buf loc val
     = primIO (prim__setDouble buf loc val)
 
 %foreign "scheme:blodwen-buffer-getdouble"
+         "C:idris2_getBufferDouble, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset)=>buf.readDoubleLE(Number(offset))"
 prim__getDouble : Buffer -> Int -> PrimIO Double
 
@@ -190,6 +204,7 @@ export
 stringByteLength : String -> Int
 
 %foreign "scheme:blodwen-buffer-setstring"
+         "C:idris2_setBufferString, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset,value)=>buf.write(value, Number(offset),buf.length - Number(offset), 'utf-8')"
 prim__setString : Buffer -> Int -> String -> PrimIO ()
 
@@ -199,6 +214,7 @@ setString buf loc val
     = primIO (prim__setString buf loc val)
 
 %foreign "scheme:blodwen-buffer-getstring"
+         "C:idris2_getBufferString, libidris2_support, idris_buffer.h"
          "node:lambda:(buf,offset,len)=>buf.slice(Number(offset), Number(offset+len)).toString('utf-8')"
 prim__getString : Buffer -> Int -> Int -> PrimIO String
 
@@ -221,6 +237,7 @@ bufferData buf
 
 
 %foreign "scheme:blodwen-buffer-copydata"
+         "C:idris2_copyBuffer, libidris2_support, idris_buffer.h"
          "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,Number(o2), Number(o1), Number(o1+length))"
 prim__copyData : Buffer -> Int -> Int -> Buffer -> Int -> PrimIO ()
 
@@ -230,11 +247,11 @@ copyData : HasIO io => (src : Buffer) -> (start, len : Int) ->
 copyData src start len dest loc
     = primIO (prim__copyData src start len dest loc)
 
-%foreign "C:idris2_readBufferData,libidris2_support"
+%foreign "C:idris2_readBufferData, libidris2_support, idris_buffer.h"
          "node:lambda:(f,b,l,m) => BigInt(require('fs').readSync(f.fd,b,Number(l), Number(m)))"
 prim__readBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
 
-%foreign "C:idris2_writeBufferData,libidris2_support"
+%foreign "C:idris2_writeBufferData, libidris2_support, idris_buffer.h"
          "node:lambda:(f,b,l,m) => BigInt(require('fs').writeSync(f.fd,b,Number(l), Number(m)))"
 prim__writeBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
 

libs/base/Data/Fin.idr

@@ -17,13 +17,15 @@ data Fin : (n : Nat) -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)
 
-||| Cast between Fins with equal indices
+||| Coerce between Fins with equal indices
 public export
-cast : {n : Nat} -> (0 eq : m = n) -> Fin m -> Fin n
+coerce : {n : Nat} -> (0 eq : m = n) -> Fin m -> Fin n
-cast {n = S _} eq FZ = FZ
+coerce {n = S _} eq FZ = FZ
-cast {n = Z} eq FZ impossible
+coerce {n = Z} eq FZ impossible
-cast {n = S _} eq (FS k) = FS (cast (succInjective _ _ eq) k)
+coerce {n = S _} eq (FS k) = FS (coerce (succInjective _ _ eq) k)
-cast {n = Z} eq (FS k) impossible
+coerce {n = Z} eq (FS k) impossible
+
+%transform "coerce-identity" coerce = replace {p = Fin}
 
 export
 Uninhabited (Fin Z) where
@@ -221,19 +223,21 @@ namespace Equality
   transitive FZ FZ = FZ
   transitive (FS prf) (FS prg) = FS (transitive prf prg)
 
-  ||| Pointwise equality is compatible with cast
+  ||| Pointwise equality is compatible with coerce
   export
-  castEq : {k : Fin m} -> (0 eq : m = n) -> cast eq k ~~~ k
+  coerceEq : {k : Fin m} -> (0 eq : m = n) -> coerce eq k ~~~ k
-  castEq {k = FZ} Refl = FZ
+  coerceEq {k = FZ} Refl = FZ
-  castEq {k = FS k} Refl = FS (castEq _)
+  coerceEq {k = FS k} Refl = FS (coerceEq _)
 
-  ||| The actual proof used by cast is irrelevant
+  ||| The actual proof used by coerce is irrelevant
   export
-  congCast : {0 n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
+  congCoerce : {0 n, q : Nat} -> {k : Fin m} -> {l : Fin p} ->
                {0 eq1 : m = n} -> {0 eq2 : p = q} ->
                k ~~~ l ->
-             cast eq1 k ~~~ cast eq2 l
+               coerce eq1 k ~~~ coerce eq2 l
-  congCast eq = transitive (castEq _) (transitive eq $ symmetric $ castEq _)
+  congCoerce eq
+    = transitive (coerceEq _)
+    $ transitive eq $ symmetric $ coerceEq _
 
   ||| Last is congruent wrt index equality
   export

libs/base/Data/SnocList.idr

@@ -0,0 +1,104 @@
+||| A Reversed List
+module Data.SnocList
+
+import Decidable.Equality
+import Data.List
+
+%default total
+
+infixl 7 <><
+infixr 6 <>>
+
+||| 'fish': Action of lists on snoc-lists
+public export
+(<><) : SnocList a -> List a -> SnocList a
+sx <>< [] = sx
+sx <>< (x :: xs) = sx :< x <>< xs
+
+||| 'chips': Action of snoc-lists on lists
+public export
+(<>>) : SnocList a -> List a -> List a
+Lin       <>> xs = xs
+(sx :< x) <>> xs = sx <>> x :: xs
+
+Cast (SnocList a) (List a) where
+  cast sx = sx <>> []
+
+Cast (List a) (SnocList a) where
+  cast xs = Lin <>< xs
+
+||| Transform to a list but keeping the contents in the spine order (term depth).
+public export
+asList : SnocList type -> List type
+asList = (reverse . cast)
+
+
+public export
+Eq a => Eq (SnocList a) where
+  (==) Lin Lin = True
+  (==) (sx :< x) (sy :< y) = x == y && sx == sy
+  (==) _ _ = False
+
+
+public export
+Ord a => Ord (SnocList a) where
+  compare Lin Lin = EQ
+  compare Lin (sx :< x) = LT
+  compare (sx :< x) Lin = GT
+  compare (sx :< x) (sy :< y)
+    = case compare sx sy of
+        EQ => compare x y
+        c  => c
+
+||| True iff input is Lin
+public export
+isLin : SnocList a -> Bool
+isLin Lin = True
+isLin (sx :< x) = False
+
+||| True iff input is (:<)
+public export
+isSnoc : SnocList a -> Bool
+isSnoc Lin     = False
+isSnoc (sx :< x) = True
+
+public export
+(++) : (sx, sy : SnocList a) -> SnocList a
+(++) sx Lin = sx
+(++) sx (sy :< y) = (sx ++ sy) :< y
+
+public export
+length : SnocList a -> Nat
+length Lin = Z
+length (sx :< x) = length sx + 1
+
+export
+Show a => Show (SnocList a) where
+  show xs = "[< " ++ show' "" xs ++ "]"
+    where
+      show' : String -> SnocList a -> String
+      show' acc Lin       = acc
+      show' acc (Lin :< x)= show x ++ acc
+      show' acc (xs :< x) = show' (", " ++ show x ++ acc) xs
+
+
+public export
+Functor SnocList where
+  map f Lin = Lin
+  map f (sx :< x) = (map f sx) :< (f x)
+
+
+public export
+Semigroup (SnocList a) where
+  (<+>) = (++)
+
+public export
+Monoid (SnocList a) where
+  neutral = Lin
+
+
+||| Check if something is a member of a list using the default Boolean equality.
+public export
+elem : Eq a => a -> SnocList a -> Bool
+elem x Lin = False
+elem x (sx :< y) = x == y || elem x sx

libs/base/System.idr

@@ -5,7 +5,7 @@ import Data.List
 import Data.Strings
 
 support : String -> String
-support fn = "C:" ++ fn ++ ", libidris2_support"
+support fn = "C:" ++ fn ++ ", libidris2_support, idris_support.h"
 
 libc : String -> String
 libc fn = "C:" ++ fn ++ ", libc 6"
@@ -15,12 +15,10 @@ libc fn = "C:" ++ fn ++ ", libc 6"
 
 %foreign "scheme,racket:blodwen-sleep"
          support "idris2_sleep"
---         "C:idris2_sleep, libidris2_support"
 prim__sleep : Int -> PrimIO ()
 
 %foreign "scheme,racket:blodwen-usleep"
          support "idris2_usleep"
---         "C:idris2_usleep, libidris2_support"
 prim__usleep : Int -> PrimIO ()
 
 export
@@ -33,12 +31,14 @@ usleep sec = primIO (prim__usleep sec)
 
 -- Get the number of arguments
 %foreign "scheme:blodwen-arg-count"
-         "node:lambda:() => process.argv.length"
+         support "idris2_getArgCount"
+         "node:lambda:() => BigInt(process.argv.length)"
 prim__getArgCount : PrimIO Int
 
 -- Get argument number `n`
 %foreign "scheme:blodwen-arg"
-         "node:lambda:n => process.argv[n]"
+         support "idris2_getArg"
+         "node:lambda:n => process.argv[(Number(n))]"
 prim__getArg : Int -> PrimIO String
 
 export
@@ -113,6 +113,14 @@ export
 time : HasIO io => io Integer
 time = pure $ cast !(primIO prim__time)
 
+%foreign support "idris2_getPID"
+prim__getPID : PrimIO Int
+
+||| Get the ID of the currently running process.
+export
+getPID : HasIO io => io Int
+getPID = primIO prim__getPID
+
 %foreign libc "exit"
          "node:lambda:c => process.exit(Number(c))"
 prim__exit : Int -> PrimIO ()

libs/base/System/Clock.idr

@@ -81,36 +81,42 @@ isClockMandatory GCReal = Optional
 isClockMandatory _      = Mandatory
 
 %foreign "scheme:blodwen-clock-time-monotonic"
+         "C:clockTimeMonotonic"
 prim__clockTimeMonotonic : PrimIO OSClock
 
 clockTimeMonotonic : IO OSClock
 clockTimeMonotonic = fromPrim prim__clockTimeMonotonic
 
 %foreign "scheme:blodwen-clock-time-utc"
+         "C:clockTimeUtc"
 prim__clockTimeUtc : PrimIO OSClock
 
 clockTimeUtc : IO OSClock
 clockTimeUtc = fromPrim prim__clockTimeUtc
 
 %foreign "scheme:blodwen-clock-time-process"
+         "C:clockTimeProcess"
 prim__clockTimeProcess : PrimIO OSClock
 
 clockTimeProcess : IO OSClock
 clockTimeProcess = fromPrim prim__clockTimeProcess
 
 %foreign "scheme:blodwen-clock-time-thread"
+         "C:clockTimeThread"
 prim__clockTimeThread : PrimIO OSClock
 
 clockTimeThread : IO OSClock
 clockTimeThread = fromPrim prim__clockTimeThread
 
 %foreign "scheme:blodwen-clock-time-gccpu"
+         "C:clockTimeGcCpu"
 prim__clockTimeGcCpu : PrimIO OSClock
 
 clockTimeGcCpu : IO OSClock
 clockTimeGcCpu = fromPrim prim__clockTimeGcCpu
 
 %foreign "scheme:blodwen-clock-time-gcreal"
+         "C:clockTimeGcReal"
 prim__clockTimeGcReal : PrimIO OSClock
 
 clockTimeGcReal : IO OSClock
@@ -126,6 +132,7 @@ fetchOSClock GCReal    = clockTimeGcReal
 fetchOSClock Duration  = clockTimeMonotonic
 
 %foreign "scheme:blodwen-is-time?"
+         "C:clockValid"
 prim__osClockValid : OSClock -> PrimIO Int
 
 ||| A test to determine the status of optional clocks.
@@ -133,12 +140,14 @@ osClockValid : OSClock -> IO Int
 osClockValid clk = fromPrim (prim__osClockValid clk)
 
 %foreign "scheme:blodwen-clock-second"
+         "C:clockSecond"
 prim__osClockSecond : OSClock -> PrimIO Bits64
 
 osClockSecond : OSClock -> IO Bits64
 osClockSecond clk = fromPrim (prim__osClockSecond clk)
 
 %foreign "scheme:blodwen-clock-nanosecond"
+         "C:clockNanosecond"
 prim__osClockNanosecond : OSClock -> PrimIO Bits64
 
 osClockNanosecond : OSClock -> IO Bits64

libs/base/System/Directory.idr

@@ -7,9 +7,9 @@ DirPtr : Type
 DirPtr = AnyPtr
 
 support : String -> String
-support fn = "C:" ++ fn ++ ", libidris2_support"
+support fn = "C:" ++ fn ++ ", libidris2_support, idris_directory.h"
 
-%foreign support "idris2_fileErrno"
+%foreign "C:idris2_fileErrno, libidris2_support, idris_file.h"
          "node:support:fileErrno,support_system_file"
 prim__fileErrno : PrimIO Int
 

libs/base/System/File.idr

@@ -16,10 +16,7 @@ FilePtr : Type
 FilePtr = AnyPtr
 
 support : String -> String
-support fn = "C:" ++ fn ++ ", libidris2_support"
+support fn = "C:" ++ fn ++ ", libidris2_support, idris_file.h"
-
-libc : String -> String
-libc fn = "C:" ++ fn ++ ", libc 6"
 
 %foreign support "idris2_openFile"
          "node:support:openFile,support_system_file"
@@ -97,7 +94,7 @@ prim__stdout : FilePtr
          "node:lambda:x=>({fd:2, buffer: Buffer.alloc(0), name:'<stderr>', eof: false})"
 prim__stderr : FilePtr
 
-%foreign libc "chmod"
+%foreign "C:chmod, libc 6, sys/stat.h"
          "node:support:chmod,support_system_file"
 prim__chmod : String -> Int -> PrimIO Int
 

libs/base/System/Info.idr

@@ -15,7 +15,7 @@ export
 isWindows : Bool
 isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
 
-%foreign "C:idris2_getNProcessors, libidris2_support"
+%foreign "C:idris2_getNProcessors, libidris2_support, idris_support.h"
 prim__getNProcessors : PrimIO Int
 
 export

libs/base/System/Signal.idr

@@ -0,0 +1,252 @@
+||| Signal raising and handling.
+|||
+||| NOTE that there are important differences between
+||| what can be done out-of-box in Windows and POSIX based
+||| operating systems. This module tries to honor both
+||| by putting things only available in POSIX environments
+||| into appropriately named namespaces or data types.
+module System.Signal
+
+import Data.Fuel
+import Data.List
+import Data.List.Elem
+
+%default total
+
+signalFFI : String -> String
+signalFFI fn = "C:" ++ fn ++ ", libidris2_support, idris_signal.h"
+
+--
+-- Signals
+--
+%foreign signalFFI "sighup"
+prim__sighup : Int
+
+%foreign signalFFI "sigint"
+prim__sigint : Int
+
+%foreign signalFFI "sigabrt"
+prim__sigabrt : Int
+
+%foreign signalFFI "sigquit"
+prim__sigquit : Int
+
+%foreign signalFFI "sigill"
+prim__sigill : Int
+
+%foreign signalFFI "sigsegv"
+prim__sigsegv : Int
+
+%foreign signalFFI "sigtrap"
+prim__sigtrap : Int
+
+%foreign signalFFI "sigfpe"
+prim__sigfpe : Int
+
+%foreign signalFFI "sigusr1"
+prim__sigusr1 : Int
+
+%foreign signalFFI "sigusr2"
+prim__sigusr2 : Int
+
+public export
+data PosixSignal = ||| Hangup (i.e. controlling terminal closed)
+                   SigHUP
+                 | ||| Quit
+                   SigQUIT
+                 | ||| Trap (as used by debuggers)
+                   SigTRAP
+                 | SigUser1
+                 | SigUser2
+
+export
+Eq PosixSignal where
+  SigHUP   == SigHUP   = True
+  SigQUIT  == SigQUIT  = True
+  SigTRAP  == SigTRAP  = True
+  SigUser1 == SigUser1 = True
+  SigUser2 == SigUser2 = True
+  _ == _ = False
+
+public export
+data Signal = ||| Interrupt (e.g. ctrl+c pressed)
+              SigINT
+            | ||| Abnormal termination
+              SigABRT
+            | ||| Ill-formed instruction
+              SigILL
+            | ||| Segmentation fault
+              SigSEGV
+            | ||| Floating-point error
+              SigFPE
+            | ||| Signals only available on POSIX operating systems
+              SigPosix PosixSignal
+
+export
+Eq Signal where
+  SigINT   == SigINT   = True
+  SigABRT  == SigABRT  = True
+  SigILL   == SigILL   = True
+  SigSEGV  == SigSEGV  = True
+  SigFPE   == SigFPE   = True
+  SigPosix x == SigPosix y = x == y
+  _ == _ = False
+
+signalCode : Signal -> Int
+signalCode SigINT   = prim__sigint
+signalCode SigABRT  = prim__sigabrt
+signalCode SigILL   = prim__sigill
+signalCode SigSEGV  = prim__sigsegv
+signalCode SigFPE   = prim__sigfpe
+signalCode (SigPosix SigHUP  ) = prim__sighup
+signalCode (SigPosix SigQUIT ) = prim__sigquit
+signalCode (SigPosix SigTRAP ) = prim__sigtrap
+signalCode (SigPosix SigUser1) = prim__sigusr1
+signalCode (SigPosix SigUser2) = prim__sigusr2
+
+toSignal : Int -> Maybe Signal
+toSignal (-1) = Nothing
+toSignal x    = lookup x codes
+  where
+    codes : List (Int, Signal)
+    codes = [
+              (prim__sigint , SigINT)
+            , (prim__sigabrt, SigABRT)
+            , (prim__sigill , SigILL)
+            , (prim__sigsegv, SigSEGV)
+            , (prim__sigfpe , SigFPE)
+            , (prim__sighup , SigPosix SigHUP)
+            , (prim__sigquit, SigPosix SigQUIT)
+            , (prim__sigtrap, SigPosix SigTRAP)
+            , (prim__sigusr1, SigPosix SigUser1)
+            , (prim__sigusr2, SigPosix SigUser2)
+            ]
+
+--
+-- Signal Handling
+--
+%foreign signalFFI "ignore_signal"
+prim__ignoreSignal : Int -> PrimIO Int
+
+%foreign signalFFI "default_signal"
+prim__defaultSignal : Int -> PrimIO Int
+
+%foreign signalFFI "collect_signal"
+prim__collectSignal : Int -> PrimIO Int
+
+%foreign signalFFI "handle_next_collected_signal"
+prim__handleNextCollectedSignal : PrimIO Int
+
+%foreign signalFFI "send_signal"
+prim__sendSignal : Int -> Int -> PrimIO Int
+
+%foreign signalFFI "raise_signal"
+prim__raiseSignal : Int -> PrimIO Int
+
+%foreign "C:idris2_getErrno, libidris2_support, idris_support.h"
+prim__getErrorNo : PrimIO Int
+
+||| An Error represented by a code. See
+||| relevant `errno` documentation.
+||| https://man7.org/linux/man-pages/man3/errno.3.html
+public export
+data SignalError = Error Int
+
+getError : HasIO io => io SignalError
+getError = Error <$> primIO prim__getErrorNo
+
+isError : Int -> Bool
+isError (-1) = True
+isError _    = False
+
+||| Ignore the given signal.
+||| Be careful doing this, as most signals have useful
+||| default behavior -- you might want to set the signal
+||| to its default behavior instead with `defaultSignal`.
+export
+ignoreSignal : HasIO io => Signal -> io (Either SignalError ())
+ignoreSignal sig = do
+  res <- primIO $ prim__ignoreSignal (signalCode sig)
+  case isError res of
+       False => pure $ Right ()
+       True  => Left <$> getError
+
+||| Use the default handler for the given signal.
+||| You can use this function to unset custom
+||| handling of a signal.
+export
+defaultSignal : HasIO io => Signal -> io (Either SignalError ())
+defaultSignal sig = do
+  res <- primIO $ prim__defaultSignal (signalCode sig)
+  case isError res of
+       False => pure $ Right ()
+       True  => Left <$> getError
+
+||| Collect the given signal.
+|||
+||| This replaces the existing handling of the given signal
+||| and instead results in Idris collecting occurrences of
+||| the signal until you call `handleNextCollectedSignal`.
+|||
+||| First, call `collectSignal` for any number of signals.
+||| Then, call `handleNextCollectedSignal` in each main loop
+||| of your program to retrieve (and mark as handled) the next
+||| signal that was collected, if any.
+|||
+||| Multiple signals will be collected and can then be retrieved
+||| in the order they were received by multiple calls to
+||| `handleNextCollectedSignal`.
+|||
+||| You can call `handleManyCollectedSignals` to get a List of
+||| pending signals instead of retrieving them one at a time.
+export
+collectSignal : HasIO io => Signal -> io (Either SignalError ())
+collectSignal sig = do
+  res <- primIO $ prim__collectSignal (signalCode sig)
+  case isError res of
+       False => pure $ Right ()
+       True  => Left <$> getError
+
+||| Get next collected signal under the pretense of handling it.
+|||
+||| Calling this "marks" the signal as handled so the next time
+||| this function is called you will retrieve the next unhandled
+||| signal instead of the same signal again.
+|||
+||| You get back Nothing if there are no pending signals.
+export
+handleNextCollectedSignal : HasIO io => io (Maybe Signal)
+handleNextCollectedSignal =
+  toSignal <$> primIO prim__handleNextCollectedSignal
+
+||| Get many collected signals and mark them as handled.
+|||
+||| Use `forever` as your fuel if you don't want or need to
+||| retain totality. Alternatively, pick a max number to
+||| retrieve and use `limit/1` as your fuel.
+export
+handleManyCollectedSignals : HasIO io => Fuel -> io (List Signal)
+handleManyCollectedSignals Dry = pure []
+handleManyCollectedSignals (More fuel) = do
+  Just next <- handleNextCollectedSignal
+    | Nothing => pure []
+  pure $ next :: !(handleManyCollectedSignals fuel)
+
+||| Send a signal to the current process.
+export
+raiseSignal : HasIO io => Signal -> io (Either SignalError ())
+raiseSignal sig = do
+  res <- primIO $ prim__raiseSignal (signalCode sig)
+  case isError res of
+       False => pure $ Right ()
+       True  => Left <$> getError
+
+namespace Posix
+  ||| Send a signal to a POSIX process using a PID to identify the process.
+  export
+  sendSignal : HasIO io => Signal -> (pid : Int) -> io (Either SignalError ())
+  sendSignal sig pid = do
+    res <- primIO $ prim__sendSignal pid (signalCode sig)
+    case isError res of
+         False => pure $ Right ()
+         True  => Left <$> getError

libs/base/base.ipkg

@@ -48,6 +48,7 @@ modules = Control.App,
           Data.IOArray.Prims,
           Data.IORef,
           Data.List,
+          Data.SnocList,
           Data.List.Elem,
           Data.List.Views,
           Data.List.Quantifiers,
@@ -82,10 +83,11 @@ modules = Control.App,
           Language.Reflection.TTImp,
 
           System,
-          System.Concurrency,
           System.Clock,
+          System.Concurrency,
           System.Directory,
-          System.File,
           System.FFI,
+          System.File,
           System.Info,
-          System.REPL
+          System.REPL,
+          System.Signal

libs/contrib/Control/Delayed.idr

@@ -1,4 +1,4 @@
-||| Utilities functions for contitionally delaying values.
+||| Utilities functions for conditionally delaying values.
 module Control.Delayed
 
 ||| Type-level function for a conditionally infinite type.

libs/contrib/Data/Fin/Extra.idr

@@ -180,7 +180,7 @@ natToFinToNat (S k) (LTESucc lte) = cong S (natToFinToNat k lte)
 ||| as illustated by the relations with the `last` function.
 public export
 (+) : {m, n : Nat} -> Fin m -> Fin (S n) -> Fin (m + n)
-(+) FZ y = cast (cong S $ plusCommutative n (pred m)) (weakenN (pred m) y)
+(+) FZ y = coerce (cong S $ plusCommutative n (pred m)) (weakenN (pred m) y)
 (+) (FS x) y = FS (x + y)
 
 ||| Multiplication of `Fin`s as bounded naturals.
@@ -200,7 +200,7 @@ finToNatPlusHomo : {m, n : Nat} -> (x : Fin m) -> (y : Fin (S n)) ->
                    finToNat (x + y) = finToNat x + finToNat y
 finToNatPlusHomo FZ _
   = finToNatQuotient $ transitive
-     (castEq _)
+     (coerceEq _)
      (weakenNNeutral _ _)
 finToNatPlusHomo (FS x) y = cong S (finToNatPlusHomo x y)
 
@@ -221,7 +221,7 @@ export
 plusPreservesLast : (m, n : Nat) -> Fin.last {n=m} + Fin.last {n} = Fin.last
 plusPreservesLast Z     n
   = homoPointwiseIsEqual $ transitive
-      (castEq _)
+      (coerceEq _)
       (weakenNNeutral _ _)
 plusPreservesLast (S m) n = cong FS (plusPreservesLast m n)
 
@@ -238,7 +238,7 @@ multPreservesLast (S m) n = Calc $
 export
 plusSuccRightSucc : {m, n : Nat} -> (left : Fin m) -> (right : Fin (S n)) ->
                     FS (left + right) ~~~ left + FS right
-plusSuccRightSucc FZ        right = FS $ congCast reflexive
+plusSuccRightSucc FZ        right = FS $ congCoerce reflexive
 plusSuccRightSucc (FS left) right = FS $ plusSuccRightSucc left right
 
 -- Relations to `Fin`-specific `shift` and `weaken`
@@ -247,7 +247,7 @@ export
 shiftAsPlus : {m, n : Nat} -> (k : Fin (S m)) ->
               shift n k ~~~ last {n} + k
 shiftAsPlus {n=Z}   k =
-  symmetric $ transitive (castEq _) (weakenNNeutral _ _)
+  symmetric $ transitive (coerceEq _) (weakenNNeutral _ _)
 shiftAsPlus {n=S n} k = FS (shiftAsPlus k)
 
 export
@@ -267,15 +267,15 @@ weakenNOfPlus :
   {m, n : Nat} -> (k : Fin m) -> (l : Fin (S n)) ->
   weakenN w (k + l) ~~~ weakenN w k + l
 weakenNOfPlus FZ l
-  = transitive (congWeakenN (castEq _))
+  = transitive (congWeakenN (coerceEq _))
   $ transitive (weakenNPlusHomo l)
-  $ symmetric (castEq _)
+  $ symmetric (coerceEq _)
 weakenNOfPlus (FS k) l = FS (weakenNOfPlus k l)
 -- General addition properties (continued)
 
 export
 plusZeroLeftNeutral : (k : Fin (S n)) -> FZ + k ~~~ k
-plusZeroLeftNeutral k = transitive (castEq _) (weakenNNeutral _ k)
+plusZeroLeftNeutral k = transitive (coerceEq _) (weakenNNeutral _ k)
 
 export
 congPlusLeft : {m, n, p : Nat} -> {k : Fin m} -> {l : Fin n} ->

libs/contrib/Data/String/Iterator.idr

@@ -23,6 +23,7 @@ data StringIterator : String -> Type where [external]
 -- to avoid subverting the linearity guarantees of withString.
 %foreign
   "scheme:blodwen-string-iterator-new"
+  "C:stringIteratorNew"
   "javascript:stringIterator:new"
 private
 fromString : (str : String) -> StringIterator str
@@ -37,6 +38,7 @@ withString str f = f (fromString str)
 ||| iterator `it`
 %foreign
   "scheme:blodwen-string-iterator-to-string"
+  "C:stringIteratorToString"
   "javascript:stringIterator:toString"
 export
 withIteratorString : (str : String)
@@ -61,6 +63,7 @@ data UnconsResult : String -> Type where
 -- (e.g. byte offset into an UTF-8 string).
 %foreign
   "scheme:blodwen-string-iterator-next"
+  "C:stringIteratorNext"
   "javascript:stringIterator:next"
 export
 uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str

libs/contrib/Data/Vect/Extra.idr

@@ -0,0 +1,23 @@
+||| Additional functions about vectors
+module Data.Vect.Extra
+
+import Data.Vect
+import Data.Fin
+import Data.Vect.Elem
+
+||| Version of `map` with access to the current position
+public export
+mapWithPos : (f : Fin n -> a -> b) -> Vect n a -> Vect n b
+mapWithPos f [] = []
+mapWithPos f (x :: xs) = f 0 x :: mapWithPos (f . FS) xs
+
+||| Version of `map` with runtime-irrelevant information that the
+||| argument is an element of the vector
+public export
+mapWithElem : (xs : Vect n a)
+  -> (f : (x : a) -> (0 pos : x `Elem` xs) -> b)
+  -> Vect n b
+mapWithElem []        f = []
+mapWithElem (x :: xs) f
+  = f x Here :: mapWithElem xs
+                (\x,pos => f x (There pos))

libs/contrib/Data/Vect/Properties.idr

@@ -0,0 +1,8 @@
+||| Additional properties and lemmata to do with Vect
+module Data.Vect.Properties
+
+import public Data.Vect.Properties.Tabulate
+import public Data.Vect.Properties.Index
+import public Data.Vect.Properties.Foldr
+import public Data.Vect.Properties.Map
+import public Data.Vect.Properties.Fin

libs/contrib/Data/Vect/Properties/Fin.idr

@@ -0,0 +1,44 @@
+module Data.Vect.Properties.Fin
+
+import Data.Vect
+import Data.Vect.Elem
+import Data.Vect.Extra
+import Data.Fin
+import Data.Nat
+
+||| Witnesses non-empty runtime-irrelevant vectors. Analogous to Data.List.NonEmpty
+public export
+data NonEmpty : Vect n a -> Type where
+  IsNonEmpty : NonEmpty (x :: xs)
+
+||| eta-law (extensionality) of head-tail cons
+export
+etaCons : (xs : Vect (S n) a) -> head xs :: tail xs = xs
+etaCons (x :: xs) = Refl
+
+||| Inhabitants of `Fin n` witness `NonZero n`
+export
+finNonZero : Fin n -> NonZero n
+finNonZero  FZ    = SIsNonZero
+finNonZero (FS i) = SIsNonZero
+
+||| Inhabitants of `Fin n` witness runtime-irrelevant vectors of length `n` aren't empty
+export
+finNonEmpty : (0 xs : Vect n a) -> NonZero n -> NonEmpty xs
+finNonEmpty xs SIsNonZero = replace {p = NonEmpty} (etaCons xs) IsNonEmpty
+
+||| Cast an index into a runtime-irrelevant `Vect` into the position
+||| of the corresponding element
+public export
+finToElem : (0 xs : Vect n a) -> (i : Fin n) -> (index i xs) `Elem` xs
+finToElem  {n      }       xs  i with (finNonEmpty xs $ finNonZero i)
+ finToElem {n = S n} (x :: xs)  FZ    | IsNonEmpty = Here
+ finToElem {n = S n} (x :: xs) (FS i) | IsNonEmpty = There (finToElem xs i)
+
+||| Analogus to `indexNaturality`, but morhisms can (irrelevantly) know the context
+export
+indexNaturalityWithElem : (i : Fin n) -> (xs : Vect n a) -> (f : (x : a) -> (0 pos : x `Elem` xs) -> b)
+  -> index i (mapWithElem xs f) = f (index i xs) (finToElem xs i)
+indexNaturalityWithElem  {n    } i       xs  f with (finNonEmpty xs (finNonZero i))
+ indexNaturalityWithElem {n = _}  FZ    (x :: xs) f | IsNonEmpty = Refl
+ indexNaturalityWithElem {n = _} (FS i) (x :: xs) f | IsNonEmpty = indexNaturalityWithElem i xs _

libs/contrib/Data/Vect/Properties/Foldr.idr

@@ -0,0 +1,120 @@
+|||
+|||
+||| foldr is the unique solution to the equation:
+|||
+|||   h f e [] = e
+|||   h f e (x :: xs) = x `h` (foldr f e xs)
+|||
+||| (This fact is called 'the universal property of foldr'.)
+|||
+||| Since the prelude defines foldr tail-recursively, this fact isn't immediate
+||| and we need some lemmata to prove it.
+module Data.Vect.Properties.Foldr
+
+import Data.Vect
+import Data.Vect.Elem
+import Data.Fin
+import Data.Nat
+import Data.Nat.Order
+
+import Syntax.PreorderReasoning
+import Syntax.PreorderReasoning.Generic
+
+import Decidable.Order
+
+||| A function H : forall n. Vect n A -> B preserving the structure of vectors over A
+public export
+record VectHomomorphismProperty {0 A, B : Type} (F : A -> B -> B) (E : B) (H : forall n . Vect n A -> B) where
+  constructor ShowVectHomomorphismProperty
+  nil  : H [] = E
+  cons : {0 n : Nat} -> (x : A) -> (xs : Vect n A) -> H (x :: xs) = x `F` (H xs)
+
+||| There is an extensionally unique function preserving the vector structure
+export
+nilConsInitiality :
+     (f : a -> b -> b) -> (e : b)
+  -> (h1, h2 : forall n . Vect n a -> b)
+  -> (prf1 : VectHomomorphismProperty f e h1)
+  -> (prf2 : VectHomomorphismProperty f e h2)
+  -> (xs : Vect n a) -> h1 xs = h2 xs
+nilConsInitiality f e h1 h2 prf1 prf2 [] = Calc $
+  |~ h1 []
+  ~~ e     ...(prf1.nil)
+  ~~ h2 [] ...(sym prf2.nil)
+
+nilConsInitiality f e h1 h2 prf1 prf2 (x :: xs) = Calc $
+  |~ h1 (x :: xs)
+  ~~ (x `f` (h1 xs)) ...(prf1.cons _ _)
+  ~~ (x `f` (h2 xs)) ...(cong (x `f`) $ nilConsInitiality f e h1 h2 prf1 prf2 xs)
+  ~~ h2 (x :: xs) ...(sym $ prf2.cons _ _)
+
+||| extensionality is a congruence with respect to Data.Vect.foldrImpl
+foldrImplExtensional :
+  (f : a -> b -> b) -> (e : b)
+  -> (go1, go2 : b -> b)
+  -> ((y : b) -> go1 y = go2 y)
+  -> (xs : Vect n a)
+  -> foldrImpl f e go1 xs = foldrImpl f e go2 xs
+foldrImplExtensional f e go1 go2 ext [] = ext e
+foldrImplExtensional f e go1 go2 ext (x :: xs) =
+  foldrImplExtensional f e _ _
+  (\y => ext (f x y))
+  xs
+
+||| foldrImpl f e x : (b -> -) -> - is natural
+foldrImplNaturality : (f : a -> b -> b) -> (e : b) -> (xs : Vect n a) -> (go1, go2 : b -> b)
+  -> foldrImpl f e (go1 . go2) xs = go1 (foldrImpl f e go2 xs)
+foldrImplNaturality f e    []     go1 go2 = Refl
+foldrImplNaturality f e (x :: xs) go1 go2 = foldrImplNaturality f e xs go1 (go2 . (f x))
+
+||| Our tail-recursive foldr preserves the vector structure
+export
+foldrVectHomomorphism : VectHomomorphismProperty f e (foldr f e)
+foldrVectHomomorphism = ShowVectHomomorphismProperty
+  { nil  = Refl
+  , cons = \x, xs => Calc $
+    |~ foldr f e (x :: xs)
+    ~~ foldrImpl f e (id . (f x)) xs ...(Refl)
+    ~~ foldrImpl f e ((f x) . id) xs ...(foldrImplExtensional f e _ _ (\y => Refl) xs)
+    ~~ f x (foldrImpl f e id xs)     ...(foldrImplNaturality f e xs (f x) _)
+    ~~ f x (foldr f e xs)            ...(Refl)
+  }
+
+||| foldr is the unique function preserving the vector structure
+export
+foldrUniqueness : (h : forall n . Vect n a -> b) -> VectHomomorphismProperty f e h -> (xs : Vect n a) -> h xs = foldr f e xs
+foldrUniqueness {f} h prf xs = irrelevantEq $
+  nilConsInitiality f e h (foldr f e) prf foldrVectHomomorphism xs
+
+
+||| Each summand is `LTE` the sum
+export
+sumIsGTEtoParts : {x : Nat} -> (xs : Vect n Nat) -> (x `Elem` xs) -> sum xs `GTE` x
+sumIsGTEtoParts (x :: xs) Here
+  = CalcWith $
+  |~ x
+  ~~ x + 0 ...(sym $ plusZeroRightNeutral _)
+  <~ x + (sum xs)   ...(plusLteMonotoneLeft x 0 _ LTEZero)
+  ~~ sum (x :: xs)  ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons _ _)
+
+sumIsGTEtoParts {x} (y :: xs) (There later)
+  = CalcWith $
+    |~ x
+    <~ sum xs       ...(sumIsGTEtoParts {x} xs later)
+    ~~ 0 + sum xs   ...(Refl)
+    <~ y + (sum xs) ...(plusLteMonotoneRight (sum xs) 0 y LTEZero)
+    ~~ sum (y :: xs) ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons _ _)
+
+||| `sum : Vect n Nat -> Nat` is monotone
+export
+sumMonotone : {n : Nat} -> (xs, ys : Vect n Nat)
+  -> (prf : (i : Fin n) -> index i xs `LTE` index i ys)
+  -> (sum xs `LTE` sum ys)
+sumMonotone [] [] prf = LTEZero
+sumMonotone (x :: xs) (y :: ys) prf =
+  let prf' = sumMonotone xs ys (\i => prf (FS i))
+  in CalcWith $
+  |~ sum (x :: xs)
+  ~~ x + sum xs    ...((foldrVectHomomorphism {f = plus} {e = 0}).cons x xs)
+  <~ y + sum ys    ...(plusLteMonotone  (prf 0) prf')
+  ~~ sum (y :: ys) ...(sym $ (foldrVectHomomorphism {f = plus} {e = 0}).cons y ys)

libs/contrib/Data/Vect/Properties/Index.idr

@@ -0,0 +1,61 @@
+||| Properties of Data.Vect.index
+module Data.Vect.Properties.Index
+
+import Data.Vect.Properties.Tabulate
+
+import Data.Vect
+import Data.Vect.Elem
+import Data.Fin
+
+import Syntax.PreorderReasoning
+
+||| Recall an element by its position, as we may not have the element
+||| at runtime
+public export
+recallElem : {xs : Vect n a} -> x `Elem` xs -> a
+recallElem {xs = x :: _ }  Here         = x
+recallElem {xs = _ :: xs} (There later) = recallElem later
+
+||| Recalling by a position of `x` does yield `x`
+export
+recallElemSpec : (pos : x `Elem` xs) -> recallElem pos = x
+recallElemSpec  Here         = Refl
+recallElemSpec (There later) = recallElemSpec later
+
+||| `index i : Vect n a -> a` is a natural transformation
+export
+indexNaturality : (i : Fin n) -> (f : a -> b) -> (xs : Vect n a)
+  -> index i (map f xs) = f (index i xs)
+indexNaturality  FZ    f (x :: xs) = Refl
+indexNaturality (FS x) f (_ :: xs)  = indexNaturality x f xs
+
+||| Replication tabulates the constant function
+export
+indexReplicate : (i : Fin n) -> (x : a)
+  -> index i (replicate n x) = x
+indexReplicate  FZ    x = Refl
+indexReplicate (FS i) x = indexReplicate i x
+
+||| `range` tabulates the identity function (by definition)
+export
+indexRange : (i : Fin n) -> index i (range {len = n}) === i
+indexRange i = irrelevantEq $ indexTabulate id i
+
+||| Inductive step auxiliary lemma for indexTranspose
+indexZipWith_Cons : (i : Fin n) -> (xs : Vect n a) -> (xss : Vect n (Vect m a))
+  -> index i (zipWith (::) xs xss)
+  = (index i xs)       :: (index i xss)
+indexZipWith_Cons  FZ    (x :: _ ) (xs:: _  ) = Refl
+indexZipWith_Cons (FS i) (_ :: xs) (_ :: xss) = indexZipWith_Cons i xs xss
+
+||| The `i`-th vector in a transposed matrix is the vector of `i`-th components
+export
+indexTranspose : (xss : Vect m (Vect n a)) -> (i : Fin n)
+  -> index i (transpose xss) = map (index i) xss
+indexTranspose     []      i = indexReplicate i []
+indexTranspose (xs :: xss) i = Calc $
+  |~ index i (transpose (xs :: xss))
+  ~~ index i (zipWith (::) xs (transpose xss))  ...(Refl)
+  ~~ index i xs :: index i (transpose xss)      ...(indexZipWith_Cons i xs (transpose xss))
+  ~~ index i xs :: map (index i) xss            ...(cong (index i xs ::)
+                                                         $ indexTranspose xss i)

libs/contrib/Data/Vect/Properties/Map.idr

@@ -0,0 +1,79 @@
+||| Properties of Data.Vect.map
+module Data.Vect.Properties.Map
+
+import Data.Vect.Properties.Tabulate
+import Data.Vect.Properties.Index
+import Data.Vect.Properties.Foldr
+
+import Data.Vect
+import Data.Vect.Elem
+import Data.Fin
+import Data.Vect.Extra
+
+import Syntax.PreorderReasoning
+
+||| `map` functoriality: identity preservation
+export
+mapId : (xs : Vect n a) -> map Prelude.id xs = xs
+mapId xs = vectorExtensionality _ _ \i => indexNaturality _ _ _
+
+||| `mapWtihPos f` represents post-composition the tabulated function `f`
+export
+indexMapWithPos : (f : Fin n -> a -> b) -> (xs : Vect n a) -> (i : Fin n)
+  -> index i (mapWithPos f xs) = f i (index i xs)
+indexMapWithPos f (x :: _ )  FZ    = Refl
+indexMapWithPos f (_ :: xs) (FS i) = indexMapWithPos _ _ _
+
+||| `tabulate : (Fin n ->) -> Vect n` is a natural transformation
+export
+mapTabulate : (f : a -> b) -> (g : Fin n -> a)
+  -> tabulate (f . g) = map f (tabulate g)
+mapTabulate f g = irrelevantEq $
+  vectorExtensionality _ _ \i => Calc $
+  |~ index i (tabulate (f . g))
+  ~~ f (g i)                      ...(indexTabulate _ _)
+  ~~ f (index i $ tabulate g)     ...(cong f (sym $ indexTabulate _ _))
+  ~~ index i (map f $ tabulate g) ...(sym $ indexNaturality _ _ _)
+
+||| Tabulating with the constant function is replication
+export
+tabulateConstantly : (x : a) -> Fin.tabulate {len} (const x) === replicate len  x
+tabulateConstantly x = irrelevantEq $
+  vectorExtensionality _ _ \i => Calc $
+  |~ index i (Fin.tabulate (const x))
+  ~~ x ...(indexTabulate _ _)
+  ~~ index i (replicate _ x) ...(sym $ indexReplicate _ _)
+
+||| It's enough that two functions agree on the elements of a vector for the maps to agree
+export
+mapRestrictedExtensional : (f, g : a -> b) -> (xs : Vect n a)
+  -> (prf : (i : Fin n) -> f (index i xs) = g (index i xs))
+  -> map f xs = map g xs
+mapRestrictedExtensional f g xs prf = vectorExtensionality _ _ \i => Calc $
+  |~ index i (map f xs)
+  ~~ f (index i xs)     ...(      indexNaturality _ _ _)
+  ~~ g (index i xs)     ...(prf _)
+  ~~ index i (map g xs) ...(sym $ indexNaturality _ _ _)
+
+||| function extensionality is a congruence wrt map
+export
+mapExtensional : (f, g : a -> b)
+  -> (prf : (x : a) -> f x = g x)
+  -> (xs : Vect n a)
+  -> map f xs = map g xs
+mapExtensional f g prf xs = mapRestrictedExtensional f g xs (\i => prf (index i xs))
+
+||| map-fusion property for vectors up to function extensionality
+export
+mapFusion : (f : b -> c) -> (g : a -> b) -> (xs : Vect n a)
+  -> map f (map g xs) = map (f . g) xs
+mapFusion f g    []     = Refl
+mapFusion f g (x :: xs) = cong (f $ g x ::) $ mapFusion f g xs
+
+||| function extensionality is a congruence wrt mapWithElem
+export
+mapWithElemExtensional : (xs : Vect n a) -> (f, g :  (x : a) -> (0 _ : x `Elem` xs) -> b)
+  -> ((x : a) -> (0 pos : x `Elem` xs) -> f x pos = g x pos)
+  -> mapWithElem xs f = mapWithElem xs g
+mapWithElemExtensional    []     f g prf = Refl
+mapWithElemExtensional (x :: xs) f g prf = cong2 (::) (prf x Here) (mapWithElemExtensional xs _ _ (\x,pos => prf x (There pos)))

libs/contrib/Data/Vect/Properties/Tabulate.idr

@@ -0,0 +1,37 @@
+||| Tabulation gives a bijection between functions `f : Fin n -> a`
+||| (up to extensional equality) and vectors `tabulate f : Vect n a`.
+module Data.Vect.Properties.Tabulate
+
+import Data.Vect
+import Data.Fin
+
+||| Vectors are uniquely determined by their elements
+export
+vectorExtensionality
+  : (xs, ys : Vect n a) -> (ext : (i : Fin n) -> index i xs = index i ys)
+ -> xs = ys
+vectorExtensionality    []        []     ext = Refl
+vectorExtensionality (x :: xs) (y :: ys) ext =
+  cong2 (::)
+        (ext FZ)
+        (vectorExtensionality xs ys (\i => ext (FS i)))
+
+||| Extensionally equivalent functions tabulate to the same vector
+export
+tabulateExtensional
+  : {n : Nat} -> (f, g : Fin n -> a) -> (ext : (i : Fin n) -> f i = g i)
+ -> tabulate f = tabulate g
+tabulateExtensional {n = 0  } f g ext = Refl
+tabulateExtensional {n = S n} f g ext =
+  cong2 (::) (ext FZ) (tabulateExtensional (f . FS) (g . FS) (\ i => ext $ FS i))
+
+||| Taking an index amounts to applying the tabulated function
+export
+indexTabulate : {n : Nat} -> (f : Fin n -> a) -> (i : Fin n) -> index i (tabulate f) = f i
+indexTabulate f  FZ    = Refl
+indexTabulate f (FS i) = indexTabulate (f . FS) i
+
+||| The empty vector represents the unique function `Fin 0 -> a`
+export
+emptyInitial : (v : Vect 0 a) -> v = []
+emptyInitial [] = Refl

libs/contrib/contrib.ipkg

@@ -113,7 +113,13 @@ modules = Control.ANSI,
           Data.Validated,
 
           Data.Vect.Binary,
-
+          Data.Vect.Properties,
+          Data.Vect.Properties.Tabulate,
+          Data.Vect.Properties.Index,
+          Data.Vect.Properties.Foldr,
+          Data.Vect.Properties.Map,
+          Data.Vect.Properties.Fin,
+          Data.Vect.Extra,
           Data.Vect.Sort,
 
           Data.Void,

libs/network/Network/FFI.idr

@@ -7,7 +7,7 @@ import Network.Socket.Data
 
 -- From sys/socket.h
 
-%foreign "C:close,libidris2_support"
+%foreign "C:close, libc 6"
 export
 prim__socket_close : (sockdes : SocketDescriptor) -> PrimIO Int
 
@@ -18,135 +18,135 @@ prim__socket_listen : (sockfd : SocketDescriptor) -> (backlog : Int) -> PrimIO I
 
 -- From idris_net.h
 
-%foreign "C:idrnet_socket,libidris2_support"
+%foreign "C:idrnet_socket, libidris2_support, idris_net.h"
 export
 prim__idrnet_socket : (domain, type, protocol : Int) -> PrimIO Int
 
-%foreign "C:idrnet_bind,libidris2_support"
+%foreign "C:idrnet_bind, libidris2_support, idris_net.h"
 export
 prim__idrnet_bind : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
                     (host : String) -> (port : Port) -> PrimIO Int
 
-%foreign "C:idrnet_connect,libidris2_support"
+%foreign "C:idrnet_connect, libidris2_support, idris_net.h"
 export
 prim__idrnet_connect : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
                        (host : String) -> (port : Port) -> PrimIO Int
 
-%foreign "C:idrnet_sockaddr_family,libidris2_support"
+%foreign "C:idrnet_sockaddr_family, libidris2_support, idris_net.h"
 export
 prim__idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int
 
-%foreign "C:idrnet_sockaddr_ipv4,libidris2_support"
+%foreign "C:idrnet_sockaddr_ipv4, libidris2_support, idris_net.h"
 export
 prim__idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String
 
-%foreign "C:idrnet_sockaddr_unix,libidris2_support"
+%foreign "C:idrnet_sockaddr_unix, libidris2_support, idris_net.h"
 export
 prim__idrnet_sockaddr_unix : (sockaddr : AnyPtr) -> PrimIO String
 
-%foreign "C:idrnet_sockaddr_ipv4_port,libidris2_support"
+%foreign "C:idrnet_sockaddr_ipv4_port, libidris2_support, idris_net.h"
 export
 prim__idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int
 
-%foreign "C:idrnet_sockaddr_port,libidris2_support"
+%foreign "C:idrnet_sockaddr_port, libidris2_support, idris_net.h"
 export
 prim__idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int
 
 
-%foreign "C:idrnet_create_sockaddr,libidris2_support"
+%foreign "C:idrnet_create_sockaddr, libidris2_support, idris_net.h"
 export
 prim__idrnet_create_sockaddr : PrimIO AnyPtr
 
-%foreign "C:idrnet_accept,libidris2_support"
+%foreign "C:idrnet_accept, libidris2_support, idris_net.h"
 export
 prim__idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO Int
 
-%foreign "C:idrnet_send,libidris2_support"
+%foreign "C:idrnet_send, libidris2_support, idris_net.h"
 export
 prim__idrnet_send : (sockfd : SocketDescriptor) -> (dataString : String) -> PrimIO Int
 
-%foreign "C:idrnet_send_buf,libidris2_support"
+%foreign "C:idrnet_send_buf, libidris2_support, idris_net.h"
 export
 prim__idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int
 
 
-%foreign "C:idrnet_recv,libidris2_support"
+%foreign "C:idrnet_recv, libidris2_support, idris_net.h"
 export
 prim__idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
 
-%foreign "C:idrnet_recv_buf,libidris2_support"
+%foreign "C:idrnet_recv_buf, libidris2_support, idris_net.h"
 export
 prim__idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO Int
 
-%foreign "C:idrnet_sendto,libidris2_support"
+%foreign "C:idrnet_sendto, libidris2_support, idris_net.h"
 export
 prim__idrnet_sendto : (sockfd : SocketDescriptor) -> (dataString,host : String) ->
                       (port : Port) -> (family : Int) -> PrimIO Int
 
-%foreign "C:idrnet_sendto_buf,libidris2_support"
+%foreign "C:idrnet_sendto_buf, libidris2_support, idris_net.h"
 export
 prim__idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) ->
                           (buf_len : Int) -> (host : String) -> (port : Port) ->
                           (family : Int) -> PrimIO Int
 
-%foreign "C:idrnet_recvfrom,libidris2_support"
+%foreign "C:idrnet_recvfrom, libidris2_support, idris_net.h"
 export
 prim__idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr
 
-%foreign "C:idrnet_recvfrom_buf,libidris2_support"
+%foreign "C:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
 export
 prim__idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO AnyPtr
 
-%foreign "C:idrnet_get_recv_res,libidris2_support"
+%foreign "C:idrnet_get_recv_res, libidris2_support, idris_net.h"
 export
 prim__idrnet_get_recv_res : (res_struct : AnyPtr) -> PrimIO Int
 
-%foreign "C:idrnet_get_recv_payload,libidris2_support"
+%foreign "C:idrnet_get_recv_payload, libidris2_support, idris_net.h"
 export
 prim__idrnet_get_recv_payload : (res_struct : AnyPtr) -> PrimIO String
 
-%foreign "C:idrnet_free_recv_struct,libidris2_support"
+%foreign "C:idrnet_free_recv_struct, libidris2_support, idris_net.h"
 export
 prim__idrnet_free_recv_struct : (res_struct : AnyPtr) -> PrimIO ()
 
-%foreign "C:idrnet_get_recvfrom_res,libidris2_support"
+%foreign "C:idrnet_get_recvfrom_res, libidris2_support, idris_net.h"
 export
 prim__idrnet_get_recvfrom_res : (res_struct : AnyPtr) -> PrimIO Int
 
-%foreign "C:idrnet_get_recvfrom_payload,libidris2_support"
+%foreign "C:idrnet_get_recvfrom_payload, libidris2_support, idris_net.h"
 export
 prim__idrnet_get_recvfrom_payload : (res_struct : AnyPtr) -> PrimIO String
 
-%foreign "C:idrnet_get_recvfrom_sockaddr,libidris2_support"
+%foreign "C:idrnet_get_recvfrom_sockaddr, libidris2_support, idris_net.h"
 export
 prim__idrnet_get_recvfrom_sockaddr : (res_struct : AnyPtr) -> PrimIO AnyPtr
 
-%foreign "C:idrnet_free_recvfrom_struct,libidris2_support"
+%foreign "C:idrnet_free_recvfrom_struct, libidris2_support, idris_net.h"
 export
 prim__idrnet_free_recvfrom_struct : (res_struct : AnyPtr) -> PrimIO ()
 
 
-%foreign "C:idrnet_geteagain,libidris2_support"
+%foreign "C:idrnet_geteagain, libidris2_support, idris_net.h"
 export
 prim__idrnet_geteagain : PrimIO Int
 
-%foreign "C:idrnet_errno,libidris2_support"
+%foreign "C:idrnet_errno, libidris2_support, idris_net.h"
 export
 prim__idrnet_errno : PrimIO Int
 
-%foreign "C:idrnet_malloc,libidris2_support"
+%foreign "C:idrnet_malloc, libidris2_support, idris_net.h"
 export
 prim__idrnet_malloc : (size : Int) -> PrimIO AnyPtr
 
-%foreign "C:idrnet_free,libidris2_support"
+%foreign "C:idrnet_free, libidris2_support, idris_net.h"
 export
 prim__idrnet_free : (ptr : AnyPtr) -> PrimIO ()
 
-%foreign "C:idrnet_peek,libidris2_support"
+%foreign "C:idrnet_peek, libidris2_support, idris_net.h"
 export
 prim__idrnet_peek : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> PrimIO {-Unsigned-} Int
 
-%foreign "C:idrnet_poke,libidris2_support"
+%foreign "C:idrnet_poke, libidris2_support, idris_net.h"
 export
 prim__idrnet_poke : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) ->
                     (val : Int {- should be Char? -}) -> PrimIO ()

libs/network/Network/Socket/Data.idr

@@ -48,7 +48,7 @@ BACKLOG : Int
 BACKLOG = 20
 
 -- Repeat to avoid a dependency cycle
-%foreign "C:idrnet_geteagain,libidris2_support"
+%foreign "C:idrnet_geteagain, libidris2_support, idris_net.h"
 prim__idrnet_geteagain : PrimIO Int
 
 export
@@ -61,10 +61,10 @@ EAGAIN =
 -- ---------------------------------------------------------------- [ Error Code ]
 
 -- repeat without export to avoid dependency cycles
-%foreign "C:idrnet_errno,libidris2_support"
+%foreign "C:idrnet_errno, libidris2_support, idris_net.h"
 prim__idrnet_errno : PrimIO Int
 
-%foreign "C:isNull,libidris2_support"
+%foreign "C:isNull, libidris2_support, idris_support.h"
 prim__idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int
 
 
@@ -113,16 +113,16 @@ Show SocketFamily where
 -- This is a bit of a hack to get the OS-dependent magic constants out of C and
 -- into Idris without having to faff around on the preprocessor on the Idris
 -- side.
-%foreign "C:idrnet_af_unspec,libidris2_support"
+%foreign "C:idrnet_af_unspec, libidris2_support, idris_net.h"
 prim__idrnet_af_unspec : PrimIO Int
 
-%foreign "C:idrnet_af_unix,libidris2_support"
+%foreign "C:idrnet_af_unix, libidris2_support, idris_net.h"
 prim__idrnet_af_unix : PrimIO Int
 
-%foreign "C:idrnet_af_inet,libidris2_support"
+%foreign "C:idrnet_af_inet, libidris2_support, idris_net.h"
 prim__idrnet_af_inet : PrimIO Int
 
-%foreign "C:idrnet_af_inet6,libidris2_support"
+%foreign "C:idrnet_af_inet6, libidris2_support, idris_net.h"
 prim__idrnet_af_inet6 : PrimIO Int
 
 export

libs/prelude/Prelude/Basics.idr

@@ -169,3 +169,14 @@ data List a =
   (::) a (List a)
 
 %name List xs, ys, zs
+
+||| Snoc lists.
+public export
+data SnocList a =
+  ||| Empty snoc-list
+  Lin
+
+  | ||| A non-empty snoc-list, consisting of the rest of the snoc-list and the final element.
+  (:<) (SnocList a) a
+
+%name SnocList sx, sy, sz

libs/prelude/Prelude/IO.idr

@@ -69,7 +69,7 @@ export
 onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t)
 onCollect ptr c = fromPrim (prim__onCollect ptr (\x => toPrim (c x)))
 
-%foreign "C:idris2_getString, libidris2_support"
+%foreign "C:idris2_getString, libidris2_support, idris_support.h"
          "javascript:lambda:x=>x"
 export
 prim__getString : Ptr String -> String
@@ -79,11 +79,11 @@ prim__putChar : Char -> (1 x : %World) -> IORes ()
 %foreign "C:getchar,libc 6"
 %extern prim__getChar : (1 x : %World) -> IORes Char
 
-%foreign "C:idris2_getStr,libidris2_support"
+%foreign "C:idris2_getStr, libidris2_support, idris_support.h"
          "node:support:getStr,support_system_file"
 prim__getStr : PrimIO String
 
-%foreign "C:idris2_putStr,libidris2_support"
+%foreign "C:idris2_putStr, libidris2_support, idris_support.h"
          "node:lambda:x=>process.stdout.write(x)"
 prim__putStr : String -> PrimIO ()
 
@@ -133,7 +133,7 @@ export
 threadWait : (1 threadID : ThreadID) -> IO ()
 threadWait threadID = fromPrim (prim__threadWait threadID)
 
-%foreign "C:idris2_readString, libidris2_support"
+%foreign "C:idris2_readString, libidris2_support, idris_support.h"
 export
 prim__getErrno : Int
 

libs/prelude/Prelude/Ops.idr

@@ -11,6 +11,7 @@ infixr 4 ||
 
 -- List and String operators
 infixr 7 ::, ++
+infixl 7 :<
 
 -- Functor/Applicative/Monad/Algebra operators
 infixl 1 >>=, =<<, >>, >=>, <=<, <&>

libs/prelude/Prelude/Types.idr

@@ -416,6 +416,7 @@ Traversable List where
 -- If you need to concatenate strings at compile time, use Prelude.concat.
 %foreign
   "scheme:string-concat"
+  "C:fastConcat"
   "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
 export
 fastConcat : List String -> String
@@ -543,6 +544,7 @@ pack (x :: xs) = strCons x (pack xs)
 
 %foreign
     "scheme:string-pack"
+    "C:fastPack"
     "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
 export
 fastPack : List Char -> String
@@ -569,6 +571,7 @@ unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str
 -- If you need to unpack strings at compile time, use Prelude.unpack.
 %foreign
   "scheme:string-unpack"
+  "C:fastUnpack"
   "javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
 export
 fastUnpack : String -> List Char

libs/prelude/PrimIO.idr

@@ -70,12 +70,12 @@ export %inline
 toPrim : (1 act : IO a) -> PrimIO a
 toPrim (MkIO fn) = fn
 
-%foreign "C:idris2_isNull, libidris2_support"
+%foreign "C:idris2_isNull, libidris2_support, idris_support.h"
          "javascript:lambda:x=>x===undefined||x===null?1n:0n"
 export
 prim__nullAnyPtr : AnyPtr -> Int
 
-%foreign "C:idris2_getNull,libidris2_support"
+%foreign "C:idris2_getNull, libidris2_support, idris_support.h"
 export
 prim__getNullAnyPtr : AnyPtr
 

src/Compiler/CompileExpr.idr

@@ -609,6 +609,10 @@ nfToCFType _ _ (NPrimVal _ Bits8Type) = pure CFUnsigned8
 nfToCFType _ _ (NPrimVal _ Bits16Type) = pure CFUnsigned16
 nfToCFType _ _ (NPrimVal _ Bits32Type) = pure CFUnsigned32
 nfToCFType _ _ (NPrimVal _ Bits64Type) = pure CFUnsigned64
+nfToCFType _ _ (NPrimVal _ Int8Type) = pure CFInt8
+nfToCFType _ _ (NPrimVal _ Int16Type) = pure CFInt16
+nfToCFType _ _ (NPrimVal _ Int32Type) = pure CFInt32
+nfToCFType _ _ (NPrimVal _ Int64Type) = pure CFInt64
 nfToCFType _ False (NPrimVal _ StringType) = pure CFString
 nfToCFType fc True (NPrimVal _ StringType)
     = throw (GenericMsg fc "String not allowed in a foreign struct")

src/Compiler/RefC/CC.idr

@@ -33,7 +33,7 @@ compileCObjectFile {asLibrary} sourceFile objectFile =
 
      let libraryFlag = if asLibrary then "-fpic " else ""
 
-     let runccobj = cc ++ " -c " ++ libraryFlag ++ sourceFile ++
+     let runccobj = cc ++ " -Werror -c " ++ libraryFlag ++ sourceFile ++
                        " -o " ++ objectFile ++ " " ++
                        "-I" ++ fullprefix_dir dirs "refc " ++
                        "-I" ++ fullprefix_dir dirs "include"
@@ -56,12 +56,13 @@ compileCFile {asShared} objectFile outFile =
 
      let sharedFlag = if asShared then "-shared " else ""
 
-     let runcc = cc ++ " " ++ sharedFlag ++ objectFile ++
+     let runcc = cc ++ " -Werror " ++ sharedFlag ++ objectFile ++
                        " -o " ++ outFile ++ " " ++
                        fullprefix_dir dirs "lib" </> "libidris2_support.a" ++ " " ++
                        "-lidris2_refc " ++
                        "-L" ++ fullprefix_dir dirs "refc " ++
-                       clibdirs (lib_dirs dirs)
+                       clibdirs (lib_dirs dirs) ++
+                       "-lm"
 
      log "compiler.refc.cc" 10 runcc
      0 <- coreLift $ system runcc

src/Compiler/RefC/RefC.idr

@@ -14,6 +14,7 @@ import Data.List
 import Libraries.Data.DList
 import Data.Nat
 import Data.Strings
+import Libraries.Data.SortedSet
 import Data.Vect
 
 import System
@@ -74,49 +75,15 @@ cName n = assert_total $ idris_crash ("INTERNAL ERROR: Unsupported name in C bac
 -- not really total but this way this internal error does not contaminate everything else
 
 escapeChar : Char -> String
-escapeChar '\DEL' = "127"
+escapeChar c = if isAlphaNum c || isNL c
-escapeChar '\NUL' = "0"
+                  then show c
-escapeChar '\SOH' = "1"
+                  else "(char)" ++ show (ord c)
-escapeChar '\STX' = "2"
-escapeChar '\ETX' = "3"
-escapeChar '\EOT' = "4"
-escapeChar '\ENQ' = "5"
-escapeChar '\ACK' = "6"
-escapeChar '\BEL' = "7"
-escapeChar '\BS' = "8"
-escapeChar '\HT' = "9"
-escapeChar '\LF' = "10"
-escapeChar '\VT' = "11"
-escapeChar '\FF' = "12"
-escapeChar '\CR' = "13"
-escapeChar '\SO' = "14"
-escapeChar '\SI' = "15"
-escapeChar '\DLE' = "16"
-escapeChar '\DC1' = "17"
-escapeChar '\DC2' = "18"
-escapeChar '\DC3' = "19"
-escapeChar '\DC4' = "20"
-escapeChar '\NAK' = "21"
-escapeChar '\SYN' = "22"
-escapeChar '\ETB' = "23"
-escapeChar '\CAN' = "24"
-escapeChar '\EM' = "25"
-escapeChar '\SUB' = "26"
-escapeChar '\ESC' = "27"
-escapeChar '\FS' = "28"
-escapeChar '\GS' = "29"
-escapeChar '\RS' = "30"
-escapeChar '\US' = "31"
-escapeChar c = show c
-
--- escapeChar '\\' = "'\\\\'"
--- escapeChar c = show c
 
 cStringQuoted : String -> String
 cStringQuoted cs = strCons '"' (showCString (unpack cs) "\"")
 where
     showCChar : Char -> String -> String
-    showCChar '\\' = ("bkslash" ++)
+    showCChar '\\' = ("\\\\" ++)
     showCChar c
        = if c < chr 32
             then (("\\x" ++ leftPad '0' 2 (asHex (cast c))) ++ "\"\"" ++)
@@ -131,12 +98,11 @@ where
 
 
 cConstant : Constant -> String
-cConstant (I x) = "(Value*)makeInt32("++ show x ++")" -- (constant #:type 'i32 #:val " ++ show x ++ ")"
+cConstant (I x) = "(Value*)makeInt32("++ show x ++")"
-cConstant (BI x) = "(Value*)makeInt64("++ show x ++")" --"(constant #:type 'i64 #:val " ++ show x ++ ")"
+cConstant (BI x) = "(Value*)makeInt64("++ show x ++")"
-cConstant (Db x) = "(Value*)makeDouble("++ show x ++")"--"(constant #:type 'double #:val " ++ show x ++ ")"
+cConstant (Db x) = "(Value*)makeDouble("++ show x ++")"
-cConstant (Ch x) = "(Value*)makeChar("++ escapeChar x ++")" --"(constant #:type 'char #:val " ++ escapeChar x ++  ")"
+cConstant (Ch x) = "(Value*)makeChar("++ escapeChar x ++")"
 cConstant (Str x) = "(Value*)makeString("++ cStringQuoted x ++")"
-  -- = "(constant #:type 'string #:val " ++ cStringQuoted x ++ ")"
 cConstant WorldVal = "(Value*)makeWorld()"
 cConstant IntType = "i32"
 cConstant IntegerType = "i64"
@@ -144,10 +110,10 @@ cConstant StringType = "string"
 cConstant CharType = "char"
 cConstant DoubleType = "double"
 cConstant WorldType = "f32"
-cConstant (B8 x)   = "(Value*)makeInt8("++ show x ++")" --"(constant #:type 'i64 #:val " ++ show x ++ ")"
+cConstant (B8 x)   = "(Value*)makeInt8("++ show x ++")"
-cConstant (B16 x)  = "(Value*)makeInt16("++ show x ++")" --"(constant #:type 'i64 #:val " ++ show x ++ ")"
+cConstant (B16 x)  = "(Value*)makeInt16("++ show x ++")"
-cConstant (B32 x)  = "(Value*)makeInt32("++ show x ++")" --"(constant #:type 'i64 #:val " ++ show x ++ ")"
+cConstant (B32 x)  = "(Value*)makeInt32("++ show x ++")"
-cConstant (B64 x)  = "(Value*)makeInt64("++ show x ++")" --"(constant #:type 'i64 #:val " ++ show x ++ ")"
+cConstant (B64 x)  = "(Value*)makeInt64("++ show x ++")"
 cConstant Bits8Type = "Bits8"
 cConstant Bits16Type = "Bits16"
 cConstant Bits32Type = "Bits32"
@@ -165,8 +131,8 @@ extractConstant (B8 x)  = show x
 extractConstant (B16 x)  = show x
 extractConstant (B32 x)  = show x
 extractConstant (B64 x)  = show x
-extractConstant c = "unable_to_extract constant >>" ++ cConstant c ++ "<<"
+extractConstant c = assert_total $ idris_crash ("INTERNAL ERROR: Unable to extract constant: " ++ cConstant c)
-
+-- not really total but this way this internal error does not contaminate everything else
 
 ||| Generate scheme for a plain function.
 plainOp : String -> List String -> String
@@ -212,7 +178,7 @@ cOp StrIndex      [x, i]    = "strIndex(" ++ x ++ ", " ++ i ++ ")"
 cOp StrCons       [x, y]    = "strCons(" ++ x ++ ", " ++ y ++ ")"
 cOp StrAppend     [x, y]    = "strAppend(" ++ x ++ ", " ++ y ++ ")"
 cOp StrSubstr     [x, y, z] =  "strSubstr(" ++ x ++ ", " ++ y  ++ ", " ++ z ++ ")"
-cOp BelieveMe     [_, _, x] = x
+cOp BelieveMe     [_, _, x] = "newReference(" ++ x ++ ")"
 cOp Crash         [_, msg]  = "idris2_crash(" ++ msg ++ ");"
 cOp fn args = plainOp (show fn) (toList args)
 
@@ -262,7 +228,8 @@ toPrim pn@(NS _ n)
             (n == UN "prim__onCollectAny", OnCollectAny)
             ]
            (Unknown pn)
-toPrim pn = Unknown pn -- todo: crash rather than generate garbage?
+toPrim pn = assert_total $ idris_crash ("INTERNAL ERROR: Unknown primitive: " ++ cName pn)
+-- not really total but this way this internal error does not contaminate everything else
 
 
 varName : AVar -> String
@@ -273,7 +240,7 @@ data ArgCounter : Type where
 data FunctionDefinitions : Type where
 data TemporaryVariableTracker : Type where
 data IndentLevel : Type where
-data ExternalLibs : Type where
+data HeaderFiles : Type where
 
 ------------------------------------------------------------------------
 -- Output generation: using a difference list for efficient append
@@ -371,15 +338,12 @@ freeTmpVars = do
         [] => pure ()
 
 
-addExternalLib : {auto e : Ref ExternalLibs (List String)}
+addHeader : {auto h : Ref HeaderFiles (SortedSet String)}
          -> String
          -> Core ()
-addExternalLib extLib = do
+addHeader header = do
-    libs <- get ExternalLibs
+    headerFiles <- get HeaderFiles
-    case elem extLib libs of
+    put HeaderFiles $ insert header headerFiles
-        True => pure () -- library already in list
-        False => do
-            put ExternalLibs (extLib :: libs)
 
 
 
@@ -432,14 +396,6 @@ cArgsVectANF : {0 arity : Nat} -> Vect arity AVar -> Core (Vect arity String)
 cArgsVectANF [] = pure []
 cArgsVectANF (x :: xs) = pure $  (varName x) :: !(cArgsVectANF xs)
 
-showEitherStringInt : Either String Int -> String
-showEitherStringInt (Left s) = s
-showEitherStringInt (Right i) = show i
-
-toIntEitherStringInt : Either String Int -> Int -> Int
-toIntEitherStringInt (Left s) k = k
-toIntEitherStringInt (Right i) _ = i
-
 integer_switch : List AConstAlt -> Bool
 integer_switch [] = True
 integer_switch (MkAConstAlt c _  :: _) =
@@ -489,7 +445,6 @@ mutual
                     -> Core $ ()
     copyConstructors _ [] _ _ _ = pure ()
     copyConstructors sc ((MkAConAlt n _ mTag args body) :: xs) constrFieldVar retValVar k = do
-        --(restConstructionCopy, restBody) <- copyConstructors sc xs constrFieldVar retValVar (S k)
         (tag', name') <- getNameTag mTag n
         emit EmptyFC $ constrFieldVar ++ "[" ++ show k ++ "].tag = " ++ tag' ++ ";"
         emit EmptyFC $ constrFieldVar ++ "[" ++ show k ++ "].name = " ++ name' ++ ";"
@@ -647,7 +602,6 @@ mutual
         let returnLine = "(Value*)makeClosureFromArglist(" ++ f_ptr_name  ++ ", " ++ arglist ++ ")"
         pure $ MkRS returnLine returnLine
     cStatementsFromANF (AApp fc _ closure arg) =
-        -- pure $ "apply_closure(" ++ varName closure ++ ", " ++ varName arg ++ ")"
         pure $ MkRS ("apply_closure(" ++ varName closure ++ ", " ++ varName arg ++ ")")
                     ("tailcall_apply_closure(" ++ varName closure ++ ", " ++ varName arg ++ ")")
     cStatementsFromANF (ALet fc var value body) = do
@@ -669,8 +623,6 @@ mutual
 
         fillConstructorArgs constr args 0
         pure $ MkRS ("(Value*)" ++ constr) ("(Value*)" ++ constr)
-        --fillingStatements <- fillConstructorArgs constr args 0
-        --pure $ (statement1 :: fillingStatements, "(Value*)" ++ constr ++ ";")
     cStatementsFromANF (AOp fc _ op args) = do
         argsVec <- cArgsVectANF args
         let opStatement = cOp op argsVec
@@ -708,15 +660,11 @@ mutual
                 increaseIndentation
                 newTemporaryVariableLevel
                 defaultAssignment <- cStatementsFromANF d
-                -- traverse_ (\l => emit EmptyFC (l) ) defaultBody
                 emit EmptyFC $ switchReturnVar ++ " = " ++ nonTailCall defaultAssignment ++ ";"
                 freeTmpVars
                 decreaseIndentation
                 emit EmptyFC $ "  }"
                 emit EmptyFC $ "}"
-                -- let defaultBlock = []
-                --                 ++ (map (\s => s) defaultBody)
-                --                 ++ [defaultLastLine1, defaultLastLine2]
                 emit EmptyFC $ "free(" ++ constructorField ++ ");"
                 pure $ MkRS switchReturnVar switchReturnVar
     cStatementsFromANF (AConstCase fc sc alts def) = do
@@ -748,25 +696,6 @@ mutual
 
 
 
-readCCPart : Char -> String -> (String, String)
-readCCPart b x =
-    let (cc, def) = break (== b) x
-    in (cc, drop 1 def)
-  where
-      drop : Int -> String -> String
-      drop headLength s =
-          let len = cast (length s)
-              subStrLen = len - headLength in
-          strSubstr headLength subStrLen s
-
-extractFFILocation : (lang:String) -> List String -> Maybe (String, String)
-extractFFILocation targetLang [] = Nothing
-extractFFILocation targetLang (def :: defs) =
-    let (thisLang,pos) = readCCPart ':' def in
-    case targetLang == thisLang of
-        True => Just (readCCPart ',' pos)
-        False => extractFFILocation targetLang defs
-
 addCommaToList : List String -> List String
 addCommaToList [] = []
 addCommaToList (x :: xs) = ("  " ++ x) :: map (", " ++) xs
@@ -789,24 +718,25 @@ getArgsNrList [] _ = []
 getArgsNrList (x :: xs) k = k :: getArgsNrList xs (S k)
 
 
-cTypeOfCFType : CFType -> Core $ String
+cTypeOfCFType : CFType -> String
-cTypeOfCFType CFUnit          = pure $ "void"
+cTypeOfCFType CFUnit          = "void"
-cTypeOfCFType CFInt           = pure $ "int"
+cTypeOfCFType CFInt           = "int"
-cTypeOfCFType CFUnsigned8     = pure $ "uint8_t"
+cTypeOfCFType CFUnsigned8     = "uint8_t"
-cTypeOfCFType CFUnsigned16    = pure $ "uint16_t"
+cTypeOfCFType CFUnsigned16    = "uint16_t"
-cTypeOfCFType CFUnsigned32    = pure $ "uint32_t"
+cTypeOfCFType CFUnsigned32    = "uint32_t"
-cTypeOfCFType CFUnsigned64    = pure $ "uint64_t"
+cTypeOfCFType CFUnsigned64    = "uint64_t"
-cTypeOfCFType CFString        = pure $ "char *"
+cTypeOfCFType CFString        = "char *"
-cTypeOfCFType CFDouble        = pure $ "double"
+cTypeOfCFType CFDouble        = "double"
-cTypeOfCFType CFChar          = pure $ "char"
+cTypeOfCFType CFChar          = "char"
-cTypeOfCFType CFPtr           = pure $ "void *"
+cTypeOfCFType CFPtr           = "void *"
-cTypeOfCFType CFGCPtr         = pure $ "void *"
+cTypeOfCFType CFGCPtr         = "void *"
-cTypeOfCFType CFBuffer        = pure $ "void *"
+cTypeOfCFType CFBuffer        = "void *"
-cTypeOfCFType CFWorld         = pure $ "void *"
+cTypeOfCFType CFWorld         = "void *"
-cTypeOfCFType (CFFun x y)     = pure $ "void *"
+cTypeOfCFType (CFFun x y)     = "void *"
-cTypeOfCFType (CFIORes x)     = pure $ "void *"
+cTypeOfCFType (CFIORes x)     = "void *"
-cTypeOfCFType (CFStruct x ys) = pure $ "void *"
+cTypeOfCFType (CFStruct x ys) = "void *"
-cTypeOfCFType (CFUser x ys)   = pure $ "void *"
+cTypeOfCFType (CFUser x ys)   = "void *"
+cTypeOfCFType n = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw FFI type in C backend: " ++ show n)
 
 varNamesFromList : List ty -> Nat -> List String
 varNamesFromList str k = map (("var_" ++) . show) (getArgsNrList str k)
@@ -814,7 +744,7 @@ varNamesFromList str k = map (("var_" ++) . show) (getArgsNrList str k)
 createFFIArgList : List CFType
                 -> Core $ List (String, String, CFType)
 createFFIArgList cftypeList = do
-    sList <- traverse cTypeOfCFType cftypeList
+    let sList = map cTypeOfCFType cftypeList
     let varList = varNamesFromList cftypeList 1
     pure $ zip3 sList varList cftypeList
 
@@ -823,7 +753,7 @@ emitFDef : {auto oft : Ref OutfileText Output}
         -> (funcName:Name)
         -> (arglist:List (String, String, CFType))
         -> Core ()
-emitFDef funcName [] = emit EmptyFC $ cName funcName ++ "(void)"
+emitFDef funcName [] = emit EmptyFC $ "Value *" ++ cName funcName ++ "(void)"
 emitFDef funcName ((varType, varName, varCFType) :: xs) = do
     emit EmptyFC $ "Value *" ++ cName funcName
     emit EmptyFC "("
@@ -847,10 +777,12 @@ extractValue CFPtr           varName = "((Value_Pointer*)" ++ varName ++ ")->p"
 extractValue CFGCPtr         varName = "((Value_GCPointer*)" ++ varName ++ ")->p->p"
 extractValue CFBuffer        varName = "((Value_Buffer*)" ++ varName ++ ")->buffer"
 extractValue CFWorld         varName = "(Value_World*)" ++ varName
-extractValue (CFFun x y)     varName = "Value* " ++ varName ++ "/* function pointer not implemented */"
+extractValue (CFFun x y)     varName = "(Value_Closure*)" ++ varName
 extractValue (CFIORes x)     varName = extractValue x varName
-extractValue (CFStruct x xs) varName = "Value* " ++ varName ++ "/* struct access not implemented */"
+extractValue (CFStruct x xs) varName = assert_total $ idris_crash ("INTERNAL ERROR: Struct access not implemented: " ++ varName)
-extractValue (CFUser x xs)   varName = "Value* " ++ varName
+-- not really total but this way this internal error does not contaminate everything else
+extractValue (CFUser x xs)   varName = "(Value*)" ++ varName
+extractValue n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw FFI type in C backend: " ++ show n)
 
 packCFType : (cfType:CFType) -> (varName:String) -> String
 packCFType CFUnit          varName = "NULL"
@@ -869,7 +801,8 @@ packCFType CFWorld         varName = "makeWorld(" ++ varName ++ ")"
 packCFType (CFFun x y)     varName = "makeFunction(" ++ varName ++ ")"
 packCFType (CFIORes x)     varName = packCFType x varName
 packCFType (CFStruct x xs) varName = "makeStruct(" ++ varName ++ ")"
-packCFType (CFUser x xs)   varName = "makeCustomUser(" ++ varName ++ ")"
+packCFType (CFUser x xs)   varName = varName
+packCFType n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw FFI type in C backend: " ++ show n)
 
 discardLastArgument : List ty -> List ty
 discardLastArgument [] = []
@@ -881,7 +814,7 @@ createCFunctions : {auto c : Ref Ctxt Defs}
                 -> {auto t : Ref TemporaryVariableTracker (List (List String))}
                 -> {auto oft : Ref OutfileText Output}
                 -> {auto il : Ref IndentLevel Nat}
-                -> {auto e : Ref ExternalLibs (List String)}
+                -> {auto h : Ref HeaderFiles (SortedSet String)}
                 -> Name
                 -> ANFDef
                 -> Core ()
@@ -924,13 +857,12 @@ createCFunctions n (MkACon tag arity nt) = do
   emit EmptyFC $ ( "// Constructor tag " ++ show tag ++ " arity " ++ show arity) -- Nothing to compile here
 
 
-createCFunctions n (MkAForeign ccs fargs (CFIORes ret)) = do
+createCFunctions n (MkAForeign ccs fargs ret) = do
-  case extractFFILocation "C" ccs of
+  case parseCC ["C"] ccs of
-      Nothing => case extractFFILocation "scheme" ccs of
+      Just (_, fctName :: extLibOpts) => do
-          Nothing => pure ()
+          case extLibOpts of
-          (Just (fctName, lib)) => emit EmptyFC $ "// call ffi to a scheme substitute for " ++ fctName
+              [lib, header] => addHeader header
-      (Just (fctName, lib)) => do
+              _ => pure ()
-          addExternalLib lib
           otherDefs <- get FunctionDefinitions
           let fnDef = "Value *" ++ (cName n) ++ "(" ++ showSep ", " (replicate (length fargs) "Value *") ++ ");"
           fn_arglist <- functionDefSignatureArglist n
@@ -958,67 +890,59 @@ createCFunctions n (MkAForeign ccs fargs (CFIORes ret)) = do
           increaseIndentation
           emit EmptyFC $ " // ffi call to " ++ fctName
           case ret of
-              CFUnit => do
+              CFIORes CFUnit => do
                   emit EmptyFC $ fctName
                               ++ "("
                               ++ showSep ", " (map (\(_, vn, vt) => extractValue vt vn) (discardLastArgument typeVarNameArgList))
                               ++ ");"
                   emit EmptyFC "return NULL;"
-                  decreaseIndentation
+              CFIORes ret => do
-                  emit EmptyFC "}\n"
+                  emit EmptyFC $ cTypeOfCFType ret ++ " retVal = " ++ fctName
-              _ => do
-                  emit EmptyFC $ !(cTypeOfCFType ret) ++ " retVal = " ++ fctName
                               ++ "("
                               ++ showSep ", " (map (\(_, vn, vt) => extractValue vt vn) (discardLastArgument typeVarNameArgList))
                               ++ ");"
                   emit EmptyFC $ "return (Value*)" ++ packCFType ret "retVal" ++ ";"
+              _ => do
+                  emit EmptyFC $ cTypeOfCFType ret ++ " retVal = " ++ fctName
+                              ++ "("
+                              ++ showSep ", " (map (\(_, vn, vt) => extractValue vt vn) typeVarNameArgList)
+                              ++ ");"
+                  emit EmptyFC $ "return (Value*)" ++ packCFType ret "retVal" ++ ";"
+
           decreaseIndentation
-                  emit EmptyFC "}\n"
+          emit EmptyFC "}"
-
+      _ => assert_total $ idris_crash ("INTERNAL ERROR: FFI not found for " ++ cName n)
-          -- decreaseIndentation
+          -- not really total but this way this internal error does not contaminate everything else
-          -- emit EmptyFC "}"
-
-          --put FunctionDefinitions ((fn ++ ";\n") :: (fn' ++ ";\n") :: otherDefs)
-      --ffiString n fctName lib fargs (CFIORes ret)
-
-createCFunctions n (MkAForeign ccs fargs ret) = pure () -- unable to deal with return values that are not CFIORes
-createCFunctions n (MkAError exp) = do
-    fn <- functionDefSignature n []
-    fn' <- functionDefSignatureArglist n
-    otherDefs <- get FunctionDefinitions
-    put FunctionDefinitions (fn :: fn' :: otherDefs)
-    --(statements, assignment) <- cStatementsFromANF exp
-    emit EmptyFC $ fn
-        ++ "\n{"
-        ++ "fprintf(stderr, \"Error in "  ++ (cName n) ++ "\");\n"
-        ++ "exit(-1);\n"
-        ++ "return NULL;"
-        ++ "\n}"
-    pure ()
 
+createCFunctions n (MkAError exp) = assert_total $ idris_crash ("INTERNAL ERROR: Error with expression: " ++ show exp)
+-- not really total but this way this internal error does not contaminate everything else
 
 header : {auto c : Ref Ctxt Defs}
       -> {auto f : Ref FunctionDefinitions (List String)}
       -> {auto o : Ref OutfileText Output}
       -> {auto il : Ref IndentLevel Nat}
-      -> {auto e : Ref ExternalLibs (List String)}
+      -> {auto h : Ref HeaderFiles (SortedSet String)}
       -> Core ()
 header = do
     let initLines = [ "#include <runtime.h>"
-                    , "/* automatically generated using the Idris2 C Backend */"
+                    , "/* automatically generated using the Idris2 C Backend */"]
-                    , "#include <idris_support.h> // for libidris2_support"]
+    let headerFiles = Libraries.Data.SortedSet.toList !(get HeaderFiles)
-    extLibs <- get ExternalLibs
+    let headerLines = map (\h => "#include <" ++ h ++ ">\n") headerFiles
-    let extLibLines = map (\lib => "// add header(s) for library: " ++ lib ++ "\n") extLibs
-    traverse_ (\l => log "compiler.refc" 20 $ " header for " ++ l ++ " needed") extLibs
     fns <- get FunctionDefinitions
-    update OutfileText (appendL (initLines ++ extLibLines ++ ["\n// function definitions"] ++ fns))
+    update OutfileText (appendL (initLines ++ headerLines ++ ["\n// function definitions"] ++ fns))
 
-footer : {auto il : Ref IndentLevel Nat} -> {auto f : Ref OutfileText Output} -> Core ()
+footer : {auto il : Ref IndentLevel Nat}
+      -> {auto f : Ref OutfileText Output}
+      -> {auto h : Ref HeaderFiles (SortedSet String)}
+      -> Core ()
 footer = do
     emit EmptyFC ""
     emit EmptyFC " // main function"
-    emit EmptyFC "int main()"
+    emit EmptyFC "int main(int argc, char *argv[])"
     emit EmptyFC "{"
+    if contains "idris_support.h" !(get HeaderFiles)
+       then emit EmptyFC "   idris2_setArgs(argc, argv);"
+       else pure ()
     emit EmptyFC "   Value *mainExprVal = __mainExpression_0();"
     emit EmptyFC "   trampoline(mainExprVal);"
     emit EmptyFC "   return 0; // bye bye"
@@ -1040,7 +964,7 @@ generateCSourceFile defs outn =
      _ <- newRef FunctionDefinitions []
      _ <- newRef TemporaryVariableTracker []
      _ <- newRef OutfileText DList.Nil
-     _ <- newRef ExternalLibs []
+     _ <- newRef HeaderFiles empty
      _ <- newRef IndentLevel 0
      traverse_ (uncurry createCFunctions) defs
      header -- added after the definition traversal in order to add all encountered function defintions

src/Compiler/Scheme/Chez.idr

@@ -177,6 +177,10 @@ data Structs : Type where
 cftySpec : FC -> CFType -> Core String
 cftySpec fc CFUnit = pure "void"
 cftySpec fc CFInt = pure "int"
+cftySpec fc CFInt8 = pure "integer-8"
+cftySpec fc CFInt16 = pure "integer-16"
+cftySpec fc CFInt32 = pure "integer-32"
+cftySpec fc CFInt64 = pure "integer-64"
 cftySpec fc CFUnsigned8 = pure "unsigned-8"
 cftySpec fc CFUnsigned16 = pure "unsigned-16"
 cftySpec fc CFUnsigned32 = pure "unsigned-32"
@@ -349,22 +353,11 @@ startChezPreamble = unlines
     , ""
     , "set -e # exit on any error"
     , ""
-    , "case $(uname -s) in            "
+    , "if [ \"$(uname)\" = Darwin ]; then"
-    , "    OpenBSD | FreeBSD | NetBSD)"
+    , "  DIR=$(zsh -c 'printf %s \"$0:A:h\"' \"$0\")"
-    , "        REALPATH=\"grealpath\" "
+    , "else"
-    , "        ;;                     "
+    , "  DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
-    , "                               "
-    , "    *)                         "
-    , "        REALPATH=\"realpath\"  "
-    , "        ;;                     "
-    , "esac                           "
-    , ""
-    , "if ! command -v \"$REALPATH\" >/dev/null; then             "
-    , "    echo \"$REALPATH is required for Chez code generator.\""
-    , "    exit 1                                                 "
     , "fi"
-    , ""
-    , "DIR=$(dirname \"$($REALPATH \"$0\")\")"
     , ""  -- so that the preamble ends with a newline
     ]
 
@@ -388,7 +381,7 @@ startChezWinSh chez appdir target = unlines
     , ""
     , "set -e # exit on any error"
     , ""
-    , "DIR=$(dirname \"$(realpath \"$0\")\")"
+    , "DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
     , "CHEZ=$(cygpath \"" ++ chez ++"\")"
     , "export PATH=\"$DIR/" ++ appdir ++ "\":$PATH"
     , "\"$CHEZ\" --script \"$DIR/" ++ target ++ "\" \"$@\""

src/Compiler/Scheme/ChezSep.idr

@@ -78,7 +78,7 @@ startChezWinSh chez appDirSh targetSh = unlines
     , ""
     , "set -e # exit on any error"
     , ""
-    , "DIR=$(dirname \"$(realpath \"$0\")\")"
+    , "DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
     , "CHEZ=$(cygpath \"" ++ chez ++"\")"
     , "export PATH=\"$DIR/" ++ appDirSh ++ "\":$PATH"
     , "\"$CHEZ\" --program \"$DIR/" ++ targetSh ++ "\" \"$@\""

src/Compiler/Scheme/Gambit.idr

@@ -152,6 +152,10 @@ cType fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
 cftySpec : FC -> CFType -> Core String
 cftySpec fc CFUnit = pure "void"
 cftySpec fc CFInt = pure "int"
+cftySpec fc CFInt8 = pure "char"
+cftySpec fc CFInt16 = pure "short"
+cftySpec fc CFInt32 = pure "int"
+cftySpec fc CFInt64 = pure "long"
 cftySpec fc CFUnsigned8 = pure "unsigned-char"
 cftySpec fc CFUnsigned16 = pure "unsigned-short"
 cftySpec fc CFUnsigned32 = pure "unsigned-int"

src/Compiler/Scheme/Racket.idr

@@ -119,6 +119,10 @@ data Done : Type where
 cftySpec : FC -> CFType -> Core String
 cftySpec fc CFUnit = pure "_void"
 cftySpec fc CFInt = pure "_int"
+cftySpec fc CFInt8 = pure "_int8"
+cftySpec fc CFInt16 = pure "_int16"
+cftySpec fc CFInt32 = pure "_int32"
+cftySpec fc CFInt64 = pure "_int64"
 cftySpec fc CFUnsigned8 = pure "_uint8"
 cftySpec fc CFUnsigned16 = pure "_uint16"
 cftySpec fc CFUnsigned32 = pure "_uint32"
@@ -330,22 +334,12 @@ startRacket racket appdir target = unlines
     , ""
     , "set -e # exit on any error"
     , ""
-    , "case $(uname -s) in            "
+    , "if [ \"$(uname)\" = Darwin ]; then"
-    , "    OpenBSD | FreeBSD | NetBSD)"
+    , "  DIR=$(zsh -c 'printf %s \"$0:A:h\"' \"$0\")"
-    , "        REALPATH=\"grealpath\" "
+    , "else"
-    , "        ;;                     "
+    , "  DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
-    , "                               "
-    , "    *)                         "
-    , "        REALPATH=\"realpath\"  "
-    , "        ;;                     "
-    , "esac                           "
-    , ""
-    , "if ! command -v \"$REALPATH\" >/dev/null; then               "
-    , "    echo \"$REALPATH is required for Racket code generator.\""
-    , "    exit 1                                                   "
     , "fi"
     , ""
-    , "DIR=$(dirname \"$($REALPATH \"$0\")\")"
     , "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ "\":$LD_LIBRARY_PATH"
     , racket ++ "\"$DIR/" ++ target ++ "\" \"$@\""
     ]
@@ -364,7 +358,7 @@ startRacketWinSh racket appdir target = unlines
     , ""
     , "set -e # exit on any error"
     , ""
-    , "DIR=$(dirname \"$(realpath \"$0\")\")"
+    , "DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
     , "export PATH=\"$DIR/" ++ appdir ++ "\":$PATH"
     , racket ++ "\"" ++ target ++ "\" \"$@\""
     ]

src/Core/Binary.idr

@@ -176,7 +176,7 @@ writeTTCFile : (HasNames extra, TTC extra) =>
 writeTTCFile b file_in
       = do file <- toFullNames file_in
            toBuf b "TT2"
-           toBuf b (version file)
+           toBuf @{Wasteful} b (version file)
            toBuf b (ifaceHash file)
            toBuf b (importHashes file)
            toBuf b (imported file)
@@ -203,7 +203,7 @@ readTTCFile readall file as b
       = do hdr <- fromBuf b
            chunk <- get Bin
            when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
-           ver <- fromBuf b
+           ver <- fromBuf @{Wasteful} b
            checkTTCVersion file ver ttcVersion
            ifaceHash <- fromBuf b
            importHashes <- fromBuf b

src/Core/CompileExpr.idr

@@ -153,6 +153,10 @@ public export
 data CFType : Type where
      CFUnit : CFType
      CFInt : CFType
+     CFInt8 : CFType
+     CFInt16 : CFType
+     CFInt32 : CFType
+     CFInt64 : CFType
      CFUnsigned8 : CFType
      CFUnsigned16 : CFType
      CFUnsigned32 : CFType
@@ -346,6 +350,10 @@ export
 Show CFType where
   show CFUnit = "Unit"
   show CFInt = "Int"
+  show CFInt8 = "Int_8"
+  show CFInt16 = "Int_16"
+  show CFInt32 = "Int_32"
+  show CFInt64 = "Int_64"
   show CFUnsigned8 = "Bits_8"
   show CFUnsigned16 = "Bits_16"
   show CFUnsigned32 = "Bits_32"

src/Core/Context.idr

@@ -1172,6 +1172,15 @@ clearCtxt
     resetElab : Options -> Options
     resetElab = record { elabDirectives = defaultElab }
 
+export
+getFieldNames : Context -> Namespace -> List Name
+getFieldNames ctxt recNS
+  = let nms = resolvedAs ctxt in
+    keys $ flip filterBy nms $ \ n =>
+      case isRF n of
+        Nothing => False
+        Just (ns, field) => ns == recNS
+
 -- Find similar looking names in the context
 getSimilarNames : {auto c : Ref Ctxt Defs} -> Name -> Core (List String)
 getSimilarNames nm = case userNameRoot nm of

src/Core/Context/Log.idr

@@ -2,6 +2,7 @@ module Core.Context.Log
 
 import Core.Context
 import Core.Options
+import Data.Strings
 
 import Libraries.Data.StringMap
 
@@ -9,7 +10,45 @@ import System.Clock
 
 %default covering
 
--- Log message with a term, translating back to human readable names first
+-- if this function is called, then logging must be enabled.
+%inline
+export
+logString : String -> Nat -> String -> Core ()
+logString "" n msg = coreLift $ putStrLn
+    $ "LOG " ++ show n ++ ": " ++ msg
+logString str n msg = coreLift $ putStrLn
+    $ "LOG " ++ str ++ ":" ++ show n ++ ": " ++ msg
+
+%inline
+export
+logString' : LogLevel -> String -> Core ()
+logString' lvl =
+  logString (fastAppend (intersperse "." (topics lvl)) ++ ":")
+            (verbosity lvl)
+
+export
+logging' : {auto c : Ref Ctxt Defs} ->
+           LogLevel -> Core Bool
+logging' lvl = do
+    opts <- getSession
+    pure $ verbosity lvl == 0 || (logEnabled opts && keepLog lvl (logLevel opts))
+
+export
+unverifiedLogging : {auto c : Ref Ctxt Defs} ->
+                    String -> Nat -> Core Bool
+unverifiedLogging str Z = pure True
+unverifiedLogging str n = do
+    opts <- getSession
+    pure $ logEnabled opts && keepLog (mkUnverifiedLogLevel str n) (logLevel opts)
+
+%inline
+export
+logging : {auto c : Ref Ctxt Defs} ->
+          (s : String) -> {auto 0 _ : KnownTopic s} ->
+          Nat -> Core Bool
+logging str n = unverifiedLogging str n
+
+||| Log message with a term, translating back to human readable names first.
 export
 logTerm : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
@@ -17,21 +56,16 @@ logTerm : {vars : _} ->
           {auto 0 _ : KnownTopic s} ->
           Nat -> Lazy String -> Term vars -> Core ()
 logTerm str n msg tm
-    = do opts <- getSession
+    = when !(logging str n)
-         let lvl = mkLogLevel (logEnabled opts) str n
+        $ do tm' <- toFullNames tm
-         if keepLog lvl (logEnabled opts) (logLevel opts)
+             logString str n $ msg ++ ": " ++ show tm'
-            then do tm' <- toFullNames tm
+
-                    coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
-                                          ++ ": " ++ show tm'
-            else pure ()
 export
 log' : {auto c : Ref Ctxt Defs} ->
        LogLevel -> Lazy String -> Core ()
 log' lvl msg
-    = do opts <- getSession
+    = when !(logging' lvl)
-         if keepLog lvl (logEnabled opts) (logLevel opts)
+        $ logString' lvl msg
-            then coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
-            else pure ()
 
 ||| Log a message with the given log level. Use increasingly
 ||| high log level numbers for more granular logging.
@@ -41,21 +75,19 @@ log : {auto c : Ref Ctxt Defs} ->
       {auto 0 _ : KnownTopic s} ->
       Nat -> Lazy String -> Core ()
 log str n msg
-    = do let lvl = mkLogLevel (logEnabled !getSession) str n
+    = when !(logging str n)
-         log' lvl msg
+        $ logString str n msg
 
 export
 unverifiedLogC : {auto c : Ref Ctxt Defs} ->
                  (s : String) ->
                  Nat -> Core String -> Core ()
 unverifiedLogC str n cmsg
-    = do opts <- getSession
+    = when !(unverifiedLogging str n)
-         let lvl = mkUnverifiedLogLevel (logEnabled opts) str n
+        $ do msg <- cmsg
-         if keepLog lvl (logEnabled opts) (logLevel opts)
+             logString str n msg
-            then do msg <- cmsg
-                    coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
-            else pure ()
 
+%inline
 export
 logC : {auto c : Ref Ctxt Defs} ->
        (s : String) ->
@@ -63,11 +95,16 @@ logC : {auto c : Ref Ctxt Defs} ->
        Nat -> Core String -> Core ()
 logC str = unverifiedLogC str
 
+nano : Integer
+nano = 1000000000
+
+micro : Integer
+micro = 1000000
+
 export
 logTimeOver : Integer -> Core String -> Core a -> Core a
 logTimeOver nsecs str act
     = do clock <- coreLift (clockTime Process)
-         let nano = 1000000000
          let t = seconds clock * nano + nanoseconds clock
          res <- act
          clock <- coreLift (clockTime Process)
@@ -78,7 +115,7 @@ logTimeOver nsecs str act
               do str' <- str
                  coreLift $ putStrLn $ "TIMING " ++ str' ++ ": " ++
                           show (time `div` nano) ++ "." ++
-                          addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
+                          addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
                           "s"
          pure res
   where
@@ -94,7 +131,6 @@ logTimeWhen : {auto c : Ref Ctxt Defs} ->
 logTimeWhen p str act
     = if p
          then do clock <- coreLift (clockTime Process)
-                 let nano = 1000000000
                  let t = seconds clock * nano + nanoseconds clock
                  res <- act
                  clock <- coreLift (clockTime Process)
@@ -103,7 +139,7 @@ logTimeWhen p str act
                  assert_total $ -- We're not dividing by 0
                     coreLift $ putStrLn $ "TIMING " ++ str ++ ": " ++
                              show (time `div` nano) ++ "." ++
-                             addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
+                             addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
                              "s"
                  pure res
          else act
@@ -118,7 +154,6 @@ logTimeRecord' : {auto c : Ref Ctxt Defs} ->
                  String -> Core a -> Core a
 logTimeRecord' key act
     = do clock <- coreLift (clockTime Process)
-         let nano = 1000000000
          let t = seconds clock * nano + nanoseconds clock
          res <- act
          clock <- coreLift (clockTime Process)
@@ -163,10 +198,9 @@ showTimeRecord
     showTimeLog : (String, (Bool, Integer)) -> Core ()
     showTimeLog (key, (_, time))
         = do coreLift $ putStr (key ++ ": ")
-             let nano = 1000000000
              assert_total $ -- We're not dividing by 0
                     coreLift $ putStrLn $ show (time `div` nano) ++ "." ++
-                               addZeros (unpack (show ((time `mod` nano) `div` 1000000))) ++
+                               addZeros (unpack (show ((time `mod` nano) `div` micro))) ++
                                "s"
 
 export

src/Core/Hash.idr

@@ -227,6 +227,14 @@ Hashable CFType where
       h `hashWithSalt` 15 `hashWithSalt` n `hashWithSalt` fs
     CFUser n xs =>
       h `hashWithSalt` 16 `hashWithSalt` n `hashWithSalt` xs
+    CFInt8 =>
+      h `hashWithSalt` 17
+    CFInt16 =>
+      h `hashWithSalt` 18
+    CFInt32 =>
+      h `hashWithSalt` 19
+    CFInt64 =>
+      h `hashWithSalt` 20
 
 export
 Hashable Constant where

src/Core/Name.idr

@@ -91,6 +91,12 @@ isSourceName (CaseBlock _ _) = False
 isSourceName (WithBlock _ _) = False
 isSourceName (Resolved _) = False
 
+export
+isRF : Name -> Maybe (Namespace, String)
+isRF (NS ns n) = map (mapFst (ns <.>)) (isRF n)
+isRF (RF n) = Just (emptyNS, n)
+isRF _ = Nothing
+
 export
 isUN : Name -> Maybe String
 isUN (UN str) = Just str

src/Core/Normalise.idr

@@ -1200,29 +1200,25 @@ logNF : {vars : _} ->
         {auto 0 _ : KnownTopic s} ->
         Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()
 logNF str n msg env tmnf
-    = do opts <- getSession
+    = when !(logging str n) $
-         let lvl = mkLogLevel (logEnabled opts) str n
-         when (keepLog lvl (logEnabled opts) (logLevel opts)) $
         do defs <- get Ctxt
            tm <- quote defs env tmnf
            tm' <- toFullNames tm
-               coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
+           logString str n (msg ++ ": " ++ show tm')
-                                          ++ ": " ++ show tm'
 
 -- Log message with a term, reducing holes and translating back to human
 -- readable names first
 export
 logTermNF' : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
-             LogLevel -> Lazy String -> Env Term vars -> Term vars -> Core ()
+             (s : String) ->
-logTermNF' lvl msg env tm
+             {auto 0 _ : KnownTopic s} ->
-    = do opts <- getSession
+             Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
-         when (keepLog lvl (logEnabled opts) (logLevel opts)) $
+logTermNF' str n msg env tm
-            do defs <- get Ctxt
+    = do defs <- get Ctxt
          tmnf <- normaliseHoles defs env tm
          tm' <- toFullNames tmnf
-               coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
+         logString str n (msg ++ ": " ++ show tm')
-                                          ++ ": " ++ show tm'
 
 export
 logTermNF : {vars : _} ->
@@ -1231,8 +1227,7 @@ logTermNF : {vars : _} ->
             {auto 0 _ : KnownTopic s} ->
             Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()
 logTermNF str n msg env tm
-    = do let lvl = mkLogLevel (logEnabled !getSession) str n
+    = when !(logging str n) $ logTermNF' str n msg env tm
-         logTermNF' lvl msg env tm
 
 export
 logGlue : {vars : _} ->
@@ -1241,14 +1236,11 @@ logGlue : {vars : _} ->
           {auto 0 _ : KnownTopic s} ->
           Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
 logGlue str n msg env gtm
-    = do opts <- getSession
+    = when !(logging str n) $
-         let lvl = mkLogLevel (logEnabled opts) str n
-         when (keepLog lvl (logEnabled opts) (logLevel opts)) $
         do defs <- get Ctxt
            tm <- getTerm gtm
            tm' <- toFullNames tm
-               coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
+           logString str n (msg ++ ": " ++ show tm')
-                                          ++ ": " ++ show tm'
 
 export
 logGlueNF : {vars : _} ->
@@ -1257,15 +1249,12 @@ logGlueNF : {vars : _} ->
             {auto 0 _ : KnownTopic s} ->
             Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()
 logGlueNF str n msg env gtm
-    = do opts <- getSession
+    = when !(logging str n) $
-         let lvl = mkLogLevel (logEnabled opts) str n
-         when (keepLog lvl (logEnabled opts) (logLevel opts)) $
         do defs <- get Ctxt
            tm <- getTerm gtm
            tmnf <- normaliseHoles defs env tm
            tm' <- toFullNames tmnf
-               coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
+           logString str n (msg ++ ": " ++ show tm')
-                                          ++ ": " ++ show tm'
 
 export
 logEnv : {vars : _} ->
@@ -1274,25 +1263,20 @@ logEnv : {vars : _} ->
          {auto 0 _ : KnownTopic s} ->
          Nat -> String -> Env Term vars -> Core ()
 logEnv str n msg env
-    = do opts <- getSession
+    = when !(logging str n) $
-         when (logEnabled opts &&
+        do logString str n msg
-                   keepLog lvl (logEnabled opts) (logLevel opts)) $ do
-           coreLift (putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg)
            dumpEnv env
 
   where
-    lvl : LogLevel
-    lvl = mkLogLevel True str n
 
     dumpEnv : {vs : List Name} -> Env Term vs -> Core ()
     dumpEnv [] = pure ()
     dumpEnv {vs = x :: _} (Let _ c val ty :: bs)
-        = do logTermNF' lvl (msg ++ ": let " ++ show x) bs val
+        = do logTermNF' str n (msg ++ ": let " ++ show x) bs val
-             logTermNF' lvl (msg ++ ":" ++ show c ++ " " ++
+             logTermNF' str n (msg ++ ":" ++ show c ++ " " ++ show x) bs ty
-                             show x) bs ty
              dumpEnv bs
     dumpEnv {vs = x :: _} (b :: bs)
-        = do logTermNF' lvl (msg ++ ":" ++ show (multiplicity b) ++ " " ++
+        = do logTermNF' str n (msg ++ ":" ++ show (multiplicity b) ++ " " ++
                            show (piInfo b) ++ " " ++
                            show x) bs (binderType b)
              dumpEnv bs

src/Core/Options/Log.idr

@@ -8,6 +8,8 @@ import Libraries.Data.StringTrie
 import Data.Strings
 import Data.These
 import Libraries.Text.PrettyPrint.Prettyprinter
+import Libraries.Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.PrettyPrint.Prettyprinter.Render.String
 
 %default total
 
@@ -35,128 +37,140 @@ import Libraries.Text.PrettyPrint.Prettyprinter
 -- INDIVIDUAL LOG LEVEL
 
 public export
-knownTopics : List (String,String)
+knownTopics : List (String, Maybe String)
 knownTopics = [
-    ("auto", "some documentation of this option"),
+    ("auto", Nothing),
-    ("builtin.Natural", "some documentation of this option"),
+    ("builtin.Natural", Nothing),
-    ("builtin.Natural.addTransform", "some documentation of this option"),
+    ("builtin.Natural.addTransform", Nothing),
-    ("builtin.NaturalToInteger", "some documentation of this option"),
+    ("builtin.NaturalToInteger", Nothing),
-    ("builtin.NaturalToInteger.addTransforms", "some documentation of this option"),
+    ("builtin.NaturalToInteger.addTransforms", Nothing),
-    ("builtin.IntegerToNatural", "some documentation of this option"),
+    ("builtin.IntegerToNatural", Nothing),
-    ("builtin.IntegerToNatural.addTransforms", "some documentation of this option"),
+    ("builtin.IntegerToNatural.addTransforms", Nothing),
-    ("compile.casetree", "some documentation of this option"),
+    ("compile.casetree", Nothing),
-    ("compile.casetree.clauses", "some documentation of this option"),
+    ("compile.casetree.clauses", Nothing),
-    ("compile.casetree.getpmdef", "some documentation of this option"),
+    ("compile.casetree.getpmdef", Nothing),
-    ("compile.casetree.intermediate", "some documentation of this option"),
+    ("compile.casetree.intermediate", Nothing),
-    ("compile.casetree.pick", "some documentation of this option"),
+    ("compile.casetree.pick", Nothing),
-    ("compile.casetree.partition", "some documentation of this option"),
+    ("compile.casetree.partition", Nothing),
-    ("compiler.inline.eval", "some documentation of this option"),
+    ("compiler.inline.eval", Nothing),
-    ("compiler.refc", "some documentation of this option"),
+    ("compiler.refc", Nothing),
-    ("compiler.refc.cc", "some documentation of this option"),
+    ("compiler.refc.cc", Nothing),
-    ("compiler.scheme.chez", "some documentation of this option"),
+    ("compiler.scheme.chez", Nothing),
-    ("coverage", "some documentation of this option"),
+    ("coverage", Nothing),
-    ("coverage.empty", "some documentation of this option"),
+    ("coverage.empty", Nothing),
-    ("coverage.missing", "some documentation of this option"),
+    ("coverage.missing", Nothing),
-    ("coverage.recover", "some documentation of this option"),
+    ("coverage.recover", Nothing),
-    ("declare.data", "some documentation of this option"),
+    ("declare.data", Nothing),
-    ("declare.data.constructor", "some documentation of this option"),
+    ("declare.data.constructor", Nothing),
-    ("declare.data.parameters", "some documentation of this option"),
+    ("declare.data.parameters", Nothing),
-    ("declare.def", "some documentation of this option"),
+    ("declare.def", Nothing),
-    ("declare.def.clause", "some documentation of this option"),
+    ("declare.def.clause", Nothing),
-    ("declare.def.clause.impossible", "some documentation of this option"),
+    ("declare.def.clause.impossible", Nothing),
-    ("declare.def.clause.with", "some documentation of this option"),
+    ("declare.def.clause.with", Nothing),
-    ("declare.def.impossible", "some documentation of this option"),
+    ("declare.def.impossible", Nothing),
-    ("declare.def.lhs", "some documentation of this option"),
+    ("declare.def.lhs", Nothing),
-    ("declare.def.lhs.implicits", "some documentation of this option"),
+    ("declare.def.lhs.implicits", Nothing),
-    ("declare.param", "some documentation of this option"),
+    ("declare.param", Nothing),
-    ("declare.record", "some documentation of this option"),
+    ("declare.record", Nothing),
-    ("declare.record.field", "some documentation of this option"),
+    ("declare.record.field", Nothing),
-    ("declare.record.projection", "some documentation of this option"),
+    ("declare.record.projection", Nothing),
-    ("declare.record.projection.prefix", "some documentation of this option"),
+    ("declare.record.projection.prefix", Nothing),
-    ("declare.type", "some documentation of this option"),
+    ("declare.type", Nothing),
-    ("desugar.idiom", "some documentation of this option"),
+    ("desugar.idiom", Nothing),
-    ("doc.record", "some documentation of this option"),
+    ("doc.record", Nothing),
-    ("elab", "some documentation of this option"),
+    ("elab", Nothing),
-    ("elab.ambiguous", "some documentation of this option"),
+    ("elab.ambiguous", Nothing),
-    ("elab.app.lhs", "some documentation of this option"),
+    ("elab.app.lhs", Nothing),
-    ("elab.as", "some documentation of this option"),
+    ("elab.as", Nothing),
-    ("elab.bindnames", "some documentation of this option"),
+    ("elab.bindnames", Nothing),
-    ("elab.binder", "some documentation of this option"),
+    ("elab.binder", Nothing),
-    ("elab.case", "some documentation of this option"),
+    ("elab.case", Nothing),
-    ("elab.def.local", "some documentation of this option"),
+    ("elab.def.local", Nothing),
-    ("elab.delay", "some documentation of this option"),
+    ("elab.delay", Nothing),
-    ("elab.hole", "some documentation of this option"),
+    ("elab.hole", Nothing),
-    ("elab.implicits", "some documentation of this option"),
+    ("elab.implicits", Nothing),
-    ("elab.implementation", "some documentation of this option"),
+    ("elab.implementation", Nothing),
-    ("elab.interface", "some documentation of this option"),
+    ("elab.interface", Nothing),
-    ("elab.interface.default", "some documentation of this option"),
+    ("elab.interface.default", Nothing),
-    ("elab.local", "some documentation of this option"),
+    ("elab.local", Nothing),
-    ("elab.prun", "some documentation of this option"),
+    ("elab.prun", Nothing),
-    ("elab.prune", "some documentation of this option"),
+    ("elab.prune", Nothing),
-    ("elab.record", "some documentation of this option"),
+    ("elab.record", Nothing),
-    ("elab.retry", "some documentation of this option"),
+    ("elab.retry", Nothing),
-    ("elab.rewrite", "some documentation of this option"),
+    ("elab.rewrite", Nothing),
-    ("elab.unify", "some documentation of this option"),
+    ("elab.unify", Nothing),
-    ("elab.update", "some documentation of this option"),
+    ("elab.update", Nothing),
-    ("elab.with", "some documentation of this option"),
+    ("elab.with", Nothing),
-    ("eval.casetree", "some documentation of this option"),
+    ("eval.casetree", Nothing),
-    ("eval.casetree.stuck", "some documentation of this option"),
+    ("eval.casetree.stuck", Nothing),
-    ("eval.eta", "some documentation of this option"),
+    ("eval.eta", Nothing),
-    ("eval.stuck", "some documentation of this option"),
+    ("eval.stuck", Nothing),
-    ("idemode.hole", "some documentation of this option"),
+    ("idemode.hole", Nothing),
-    ("ide-mode.highlight", "some documentation of this option"),
+    ("ide-mode.highlight", Nothing),
-    ("ide-mode.highlight.alias", "some documentation of this option"),
+    ("ide-mode.highlight.alias", Nothing),
-    ("ide-mode.send", "some documentation of this option"),
+    ("ide-mode.send", Nothing),
-    ("import", "some documentation of this option"),
+    ("import", Nothing),
-    ("import.file", "some documentation of this option"),
+    ("import.file", Nothing),
-    ("interaction.casesplit", "some documentation of this option"),
+    ("interaction.casesplit", Nothing),
-    ("interaction.generate", "some documentation of this option"),
+    ("interaction.generate", Nothing),
-    ("interaction.search", "some documentation of this option"),
+    ("interaction.search", Nothing),
-    ("metadata.names", "some documentation of this option"),
+    ("metadata.names", Nothing),
-    ("module.hash", "some documentation of this option"),
+    ("module.hash", Nothing),
-    ("quantity", "some documentation of this option"),
+    ("quantity", Nothing),
-    ("quantity.hole", "some documentation of this option"),
+    ("quantity.hole", Nothing),
-    ("quantity.hole.update", "some documentation of this option"),
+    ("quantity.hole.update", Nothing),
-    ("repl.eval", "some documentation of this option"),
+    ("repl.eval", Nothing),
-    ("specialise", "some documentation of this option"),
+    ("specialise", Nothing),
-    ("totality", "some documentation of this option"),
+    ("totality", Nothing),
-    ("totality.positivity", "some documentation of this option"),
+    ("totality.positivity", Nothing),
-    ("totality.termination", "some documentation of this option"),
+    ("totality.termination", Nothing),
-    ("totality.termination.calc", "some documentation of this option"),
+    ("totality.termination.calc", Nothing),
-    ("totality.termination.guarded", "some documentation of this option"),
+    ("totality.termination.guarded", Nothing),
-    ("totality.termination.sizechange", "some documentation of this option"),
+    ("totality.termination.sizechange", Nothing),
-    ("totality.termination.sizechange.checkCall", "some documentation of this option"),
+    ("totality.termination.sizechange.checkCall", Nothing),
-    ("totality.termination.sizechange.checkCall.inPath", "some documentation of this option"),
+    ("totality.termination.sizechange.checkCall.inPath", Nothing),
-    ("totality.termination.sizechange.checkCall.inPathNot.restart", "some documentation of this option"),
+    ("totality.termination.sizechange.checkCall.inPathNot.restart", Nothing),
-    ("totality.termination.sizechange.checkCall.inPathNot.return", "some documentation of this option"),
+    ("totality.termination.sizechange.checkCall.inPathNot.return", Nothing),
-    ("totality.termination.sizechange.inPath", "some documentation of this option"),
+    ("totality.termination.sizechange.inPath", Nothing),
-    ("totality.termination.sizechange.isTerminating", "some documentation of this option"),
+    ("totality.termination.sizechange.isTerminating", Nothing),
-    ("totality.termination.sizechange.needsChecking", "some documentation of this option"),
+    ("totality.termination.sizechange.needsChecking", Nothing),
-    ("transform.lhs", "some documentation of this option"),
+    ("transform.lhs", Nothing),
-    ("transform.rhs", "some documentation of this option"),
+    ("transform.rhs", Nothing),
-    ("ttc.read", "some documentation of this option"),
+    ("ttc.read", Nothing),
-    ("ttc.write", "some documentation of this option"),
+    ("ttc.write", Nothing),
-    ("typesearch.equiv", "some documentation of this option"),
+    ("typesearch.equiv", Nothing),
-    ("unelab.case", "some documentation of this option"),
+    ("unelab.case", Nothing),
-    ("unify", "some documentation of this option"),
+    ("unify", Nothing),
-    ("unify.application", "some documentation of this option"),
+    ("unify.application", Nothing),
-    ("unify.binder", "some documentation of this option"),
+    ("unify.binder", Nothing),
-    ("unify.constant", "some documentation of this option"),
+    ("unify.constant", Nothing),
-    ("unify.constraint", "some documentation of this option"),
+    ("unify.constraint", Nothing),
-    ("unify.delay", "some documentation of this option"),
+    ("unify.delay", Nothing),
-    ("unify.equal", "some documentation of this option"),
+    ("unify.equal", Nothing),
-    ("unify.head", "some documentation of this option"),
+    ("unify.head", Nothing),
-    ("unify.hole", "some documentation of this option"),
+    ("unify.hole", Nothing),
-    ("unify.instantiate", "some documentation of this option"),
+    ("unify.instantiate", Nothing),
-    ("unify.invertible", "some documentation of this option"),
+    ("unify.invertible", Nothing),
-    ("unify.meta", "some documentation of this option"),
+    ("unify.meta", Nothing),
-    ("unify.noeta", "some documentation of this option"),
+    ("unify.noeta", Nothing),
-    ("unify.postpone", "some documentation of this option"),
+    ("unify.postpone", Nothing),
-    ("unify.retry", "some documentation of this option"),
+    ("unify.retry", Nothing),
-    ("unify.search", "some documentation of this option"),
+    ("unify.search", Nothing),
-    ("unify.unsolved", "some documentation of this option")
+    ("unify.unsolved", Nothing)
 ]
 
+export
+helpTopics : String
+helpTopics = show $ vcat $ map helpTopic knownTopics
+
+  where
+
+  helpTopic : (String, Maybe String) -> Doc ()
+  helpTopic (str, mblurb)
+    = let title = "+" <++> pretty str
+          blurb = maybe [] ((::[]) . indent 2 . reflow) mblurb
+      in vcat (title :: blurb)
+
 public export
 KnownTopic : String -> Type
 KnownTopic s = IsJust (lookup s knownTopics)
@@ -184,16 +198,15 @@ mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n
 ||| Use this function to create user defined loglevels, for instance, during
 ||| elaborator reflection.
 export
-mkUnverifiedLogLevel : Bool -> (s : String) -> Nat -> LogLevel
+mkUnverifiedLogLevel : (s : String) -> Nat -> LogLevel
-mkUnverifiedLogLevel False _ = mkLogLevel' Nothing
+mkUnverifiedLogLevel "" = mkLogLevel' Nothing
-mkUnverifiedLogLevel _ "" = mkLogLevel' Nothing
+mkUnverifiedLogLevel ps = mkLogLevel' (Just (split (== '.') ps))
-mkUnverifiedLogLevel _ ps = mkLogLevel' (Just (split (== '.') ps))
 
 ||| Like `mkUnverifiedLogLevel` but with a compile time check that
 ||| the passed string is a known topic.
 export
-mkLogLevel : Bool -> (s : String) -> {auto 0 _ : KnownTopic s} -> Nat -> LogLevel
+mkLogLevel : (s : String) -> {auto 0 _ : KnownTopic s} -> Nat -> LogLevel
-mkLogLevel b s = mkUnverifiedLogLevel b s
+mkLogLevel s = mkUnverifiedLogLevel s
 
 ||| The unsafe constructor should only be used in places where the topic has already
 ||| been appropriately processed.
@@ -239,7 +252,7 @@ parseLogLevel str = do
                 ns = tail nns in
                 case ns of
                      [] => pure (MkLogLevel [], n)
-                     [ns] => pure (mkUnverifiedLogLevel True n, ns)
+                     [ns] => pure (mkUnverifiedLogLevel n, ns)
                      _ => Nothing
   lvl <- parsePositive n
   pure $ c (fromInteger lvl)
@@ -268,9 +281,9 @@ insertLogLevel (MkLogLevel ps n) = insert ps n
 ||| We keep a log if there is a prefix of its path associated to a larger number
 ||| in the LogLevels.
 export
-keepLog : LogLevel -> Bool -> LogLevels -> Bool
+keepLog : LogLevel -> LogLevels -> Bool
-keepLog (MkLogLevel _ Z) _ _ = True
+keepLog (MkLogLevel _ Z) _ = True
-keepLog (MkLogLevel path n) enabled levels = enabled && go path levels where
+keepLog (MkLogLevel path n) levels = go path levels where
 
   go : List String -> StringTrie Nat -> Bool
   go path (MkStringTrie current) = here || there where

src/Core/TTC.idr

@@ -758,6 +758,10 @@ TTC CFType where
   toBuf b (CFUser n a) = do tag 14; toBuf b n; toBuf b a
   toBuf b CFGCPtr = tag 15
   toBuf b CFBuffer = tag 16
+  toBuf b CFInt8 = tag 17
+  toBuf b CFInt16 = tag 18
+  toBuf b CFInt32 = tag 19
+  toBuf b CFInt64 = tag 20
 
   fromBuf b
       = case !getTag of
@@ -778,6 +782,10 @@ TTC CFType where
              14 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
              15 => pure CFGCPtr
              16 => pure CFBuffer
+             17 => pure CFInt8
+             18 => pure CFInt16
+             19 => pure CFInt32
+             20 => pure CFInt64
              _ => corrupt "CFType"
 
 export

src/Core/Termination.idr

@@ -11,6 +11,7 @@ import Core.Value
 import Control.Monad.State
 
 import Libraries.Data.NameMap
+import Libraries.Data.SortedMap
 import Data.List
 
 %default covering
@@ -438,22 +439,36 @@ initArgs (S k)
          args' <- initArgs k
          pure (Just (arg, Same) :: args')
 
+data Explored : Type where
+
+-- Cached results of exploring the size change graph, so that if we visit a
+-- node again, we don't have to re-explore the whole thing
+SizeChanges : Type
+SizeChanges = SortedMap (Name, List (Maybe Arg)) Terminating
+
 -- Traverse the size change graph. When we reach a point we've seen before,
 -- at least one of the arguments must have got smaller, otherwise it's
 -- potentially non-terminating
 checkSC : {auto a : Ref APos Arg} ->
           {auto c : Ref Ctxt Defs} ->
+          {auto e : Ref Explored SizeChanges} ->
           Defs ->
           Name -> -- function we're checking
           List (Maybe (Arg, SizeChange)) -> -- functions arguments and change
           List (Name, List (Maybe Arg)) -> -- calls we've seen so far
           Core Terminating
 checkSC defs f args path
-   = do log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f)
+   = do exp <- get Explored
+        log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f)
         let pos = (f, map (map Builtin.fst) args)
+        case lookup pos exp of
+             Just done => pure done -- already explored this bit of tree
+             Nothing =>
                 if pos `elem` path
                    then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show !(toFullNames f)
-                   toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
+                           res <- toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
+                           put Explored (insert pos res exp)
+                           pure res
                    else case !(lookupCtxtExact f (gamma defs)) of
                              Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show !(toFullNames f)
                                            pure IsTerminating
@@ -488,14 +503,14 @@ checkSC defs f args path
 
     checkCall : List (Name, List (Maybe Arg)) -> SCCall -> Core Terminating
     checkCall path sc
-        = do let inpath = fnCall sc `elem` map fst path
+        = do Just gdef <- lookupCtxtExact (fnCall sc) (gamma defs)
-             Just gdef <- lookupCtxtExact (fnCall sc) (gamma defs)
                   | Nothing => pure IsTerminating -- nothing to check
              let Unchecked = isTerminating (totality gdef)
                   | IsTerminating => pure IsTerminating
                   | _ => pure (NotTerminating (BadCall [fnCall sc]))
              log "totality.termination.sizechange.checkCall" 8 $ "CheckCall Size Change Graph: " ++ show !(toFullNames (fnCall sc))
              term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path
+             let inpath = fnCall sc `elem` map fst path
              if not inpath
                 then case term of
                        NotTerminating (RecPath _) =>
@@ -505,7 +520,9 @@ checkSC defs f args path
                           -- function was the top level thing we were checking)
                           do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show !(toFullNames (fnCall sc))
                              args' <- initArgs (length (fnArgs sc))
-                             checkSC defs (fnCall sc) args' path
+                             t <- checkSC defs (fnCall sc) args' path
+                             setTerminating emptyFC (fnCall sc) t
+                             pure t
                        t => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show !(toFullNames (fnCall sc))
                                pure t
                 else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show !(toFullNames (fnCall sc))
@@ -535,6 +552,7 @@ calcTerminating loc n
                         do let ty = type def
                            a <- newRef APos firstArg
                            args <- initArgs !(getArity defs [] ty)
+                           e <- newRef Explored empty
                            checkSC defs n args []
                      bad => pure bad
   where

src/Core/UnifyState.idr

@@ -623,64 +623,70 @@ checkNoGuards : {auto u : Ref UST UState} ->
 checkNoGuards = checkUserHoles False
 
 export
-dumpHole' : {auto u : Ref UST UState} ->
+dumpHole : {auto u : Ref UST UState} ->
            {auto c : Ref Ctxt Defs} ->
-            LogLevel -> (hole : Int) -> Core ()
+           (s : String) ->
-dumpHole' lvl hole
+           {auto 0 _ : KnownTopic s} ->
+           Nat -> (hole : Int) -> Core ()
+dumpHole str n hole
     = do ust <- get UST
          defs <- get Ctxt
          sopts <- getSession
-         when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $ do
          defs <- get Ctxt
          case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
           Nothing => pure ()
           Just gdef => case (definition gdef, type gdef) of
              (Guess tm envb constraints, ty) =>
-                         do log' lvl $ "!" ++ show !(getFullName (Resolved hole)) ++ " : " ++
+                  do logString str n $
-                                              show !(toFullNames !(normaliseHoles defs [] ty))
+                       "!" ++ show !(getFullName (Resolved hole)) ++ " : "
-                            log' lvl $ "\t  = " ++ show !(normaliseHoles defs [] tm)
+                           ++ show !(toFullNames !(normaliseHoles defs [] ty))
+                       ++ "\n\t  = "
+                           ++ show !(normaliseHoles defs [] tm)
                            ++ "\n\twhen"
                      traverse_ dumpConstraint constraints
              (Hole _ p, ty) =>
-                         log' lvl $ "?" ++ show (fullname gdef) ++ " : " ++
+                  logString str n $
-                                           show !(normaliseHoles defs [] ty)
+                    "?" ++ show (fullname gdef) ++ " : "
+                        ++ show !(normaliseHoles defs [] ty)
                         ++ if implbind p then " (ImplBind)" else ""
                         ++ if invertible gdef then " (Invertible)" else ""
              (BySearch _ _ _, ty) =>
-                         log' lvl $ "Search " ++ show hole ++ " : " ++
+                  logString str n $
+                     "Search " ++ show hole ++ " : " ++
                      show !(toFullNames !(normaliseHoles defs [] ty))
              (PMDef _ args t _ _, ty) =>
-                         log' (withVerbosity 4 lvl) $
+                  log str 4 $
                      "Solved: " ++ show hole ++ " : " ++
                      show !(normalise defs [] ty) ++
                      " = " ++ show !(normalise defs [] (Ref emptyFC Func (Resolved hole)))
              (ImpBind, ty) =>
-                         log' (withVerbosity 4 lvl) $
+                  log str 4 $
                       "Bound: " ++ show hole ++ " : " ++
                       show !(normalise defs [] ty)
              (Delayed, ty) =>
-                         log' (withVerbosity 4 lvl) $
+                  log str 4 $
                      "Delayed elaborator : " ++
                      show !(normalise defs [] ty)
              _ => pure ()
   where
     dumpConstraint : Int -> Core ()
-    dumpConstraint n
+    dumpConstraint cid
         = do ust <- get UST
              defs <- get Ctxt
-             case lookup n (constraints ust) of
+             case lookup cid (constraints ust) of
                   Nothing => pure ()
-                  Just Resolved => log' lvl "\tResolved"
+                  Just Resolved => logString str n "\tResolved"
                   Just (MkConstraint _ lazy env x y) =>
-                    do log' lvl $ "\t  " ++ show !(toFullNames !(quote defs env x))
+                    do logString str n $
+                         "\t  " ++ show !(toFullNames !(quote defs env x))
                                 ++ " =?= " ++ show !(toFullNames !(quote defs env y))
                        empty <- clearDefs defs
-                       log' (withVerbosity 5 lvl)
+                       log str 5 $
-                                $ "\t    from " ++ show !(toFullNames !(quote empty env x))
+                         "\t    from " ++ show !(toFullNames !(quote empty env x))
-                                      ++ " =?= " ++ show !(toFullNames !(quote empty env y)) ++
+                            ++ " =?= " ++ show !(toFullNames !(quote empty env y))
-                               if lazy then "\n\t(lazy allowed)" else ""
+                            ++ if lazy then "\n\t(lazy allowed)" else ""
                   Just (MkSeqConstraint _ _ xs ys) =>
-                       log' lvl $ "\t\t" ++ show xs ++ " =?= " ++ show ys
+                       logString str n $ "\t\t" ++ show xs ++ " =?= " ++ show ys
 
 export
 dumpConstraints : {auto u : Ref UST UState} ->
@@ -694,11 +700,9 @@ dumpConstraints str n all
     = do ust <- get UST
          defs <- get Ctxt
          sopts <- getSession
-         let lvl = mkLogLevel (logEnabled sopts) str n
+         when !(logging str n) $ do
-         when (keepLog lvl (logEnabled sopts) (logLevel sopts)) $
+           let hs = toList (guesses ust) ++
-            do let hs = toList (guesses ust) ++
                     toList (if all then holes ust else currentHoles ust)
-               case hs of
+           unless (isNil hs) $
-                    [] => pure ()
+             do logString str n "--- CONSTRAINTS AND HOLES ---"
-                    _ => do log' lvl "--- CONSTRAINTS AND HOLES ---"
+                traverse_ (dumpHole str n) (map fst hs)
-                            traverse_ (dumpHole' lvl) (map fst hs)

src/Idris/CommandLine.idr

@@ -46,6 +46,17 @@ export
 Show DirCommand where
   show LibDir = "--libdir"
 
+||| Help topics
+public export
+data HelpTopic
+  =
+    ||| Interactive debugging topics
+   HelpLogging
+
+recogniseHelpTopic : String -> Maybe HelpTopic
+recogniseHelpTopic "logging" = pure HelpLogging
+recogniseHelpTopic _ = Nothing
+
 ||| CLOpt - possible command line options
 public export
 data CLOpt
@@ -75,7 +86,7 @@ data CLOpt
    ||| Display Idris version
   Version |
    ||| Display help text
-  Help |
+  Help (Maybe HelpTopic) |
    ||| Suppress the banner
   NoBanner |
    ||| Run Idris 2 in quiet mode
@@ -271,7 +282,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
            optSeparator,
            MkOpt ["--version", "-v"] [] [Version]
               (Just "Display version string"),
-           MkOpt ["--help", "-h", "-?"] [] [Help]
+           MkOpt ["--help", "-h", "-?"] [Optional "topic"] (\ tp => [Help (tp >>= recogniseHelpTopic)])
               (Just "Display help text"),
 
            -- Internal debugging options

src/Idris/Desugar.idr

@@ -16,7 +16,7 @@ import Libraries.Data.StringMap
 import Libraries.Data.String.Extra
 import Libraries.Data.ANameMap
 
-import Idris.DocString
+import Idris.Doc.String
 import Idris.Syntax
 
 import Idris.Elab.Implementation
@@ -69,6 +69,12 @@ import Libraries.Data.String.Extra
 public export
 data Side = LHS | AnyExpr
 
+export
+Eq Side where
+  LHS == LHS = True
+  AnyExpr == AnyExpr = True
+  _ == _ = False
+
 export
 extendSyn : {auto s : Ref Syn SyntaxInfo} ->
             SyntaxInfo -> Core ()
@@ -190,24 +196,24 @@ mutual
       =  if lowerFirst nm || nm == "_"
            then do whenJust (isConcreteFC prefFC) \nfc
                      => addSemanticDecorations [(nfc, Bound, Just n)]
-                   pure $ ILam fc rig !(traverse (desugar side ps) p)
+                   pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
-                           (Just n) !(desugarB side ps argTy)
+                           (Just n) !(desugarB AnyExpr ps argTy)
-                                    !(desugar side (n :: ps) scope)
+                                    !(desugar AnyExpr (n :: ps) scope)
-           else pure $ ILam EmptyFC rig !(traverse (desugar side ps) p)
+           else pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p)
-                   (Just (MN "lamc" 0)) !(desugarB side ps argTy) $
+                   (Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $
                  ICase fc (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
                      [snd !(desugarClause ps True (MkPatClause fc pat scope []))]
   desugarB side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope)
-      = pure $ ILam fc rig !(traverse (desugar side ps) p)
+      = pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
-                           (Just n) !(desugarB side ps argTy)
+                           (Just n) !(desugarB AnyExpr ps argTy)
-                                    !(desugar side (n :: ps) scope)
+                                    !(desugar AnyExpr (n :: ps) scope)
   desugarB side ps (PLam fc rig p (PImplicit _) argTy scope)
-      = pure $ ILam fc rig !(traverse (desugar side ps) p)
+      = pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
-                           Nothing !(desugarB side ps argTy)
+                           Nothing !(desugarB AnyExpr ps argTy)
-                                   !(desugar side ps scope)
+                                   !(desugar AnyExpr ps scope)
   desugarB side ps (PLam fc rig p pat argTy scope)
-      = pure $ ILam EmptyFC rig !(traverse (desugar side ps) p)
+      = pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p)
-                   (Just (MN "lamc" 0)) !(desugarB side ps argTy) $
+                   (Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $
                  ICase fc (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
                      [snd !(desugarClause ps True (MkPatClause fc pat scope []))]
   desugarB side ps (PLet fc rig (PRef prefFC n) nTy nVal scope [])
@@ -321,7 +327,10 @@ mutual
   desugarB side ps (PDotted fc x)
       = pure $ IMustUnify fc UserDotted !(desugarB side ps x)
   desugarB side ps (PImplicit fc) = pure $ Implicit fc True
-  desugarB side ps (PInfer fc) = pure $ Implicit fc False
+  desugarB side ps (PInfer fc)
+    = do when (side == LHS) $
+           throw (GenericMsg fc "? is not a valid pattern")
+         pure $ Implicit fc False
   desugarB side ps (PMultiline fc indent lines)
       = addFromString fc !(expandString side ps fc !(trimMultiline fc indent lines))
   desugarB side ps (PString fc strs)
@@ -344,6 +353,8 @@ mutual
            pure val
   desugarB side ps (PList fc nilFC args)
       = expandList side ps nilFC args
+  desugarB side ps (PSnocList fc nilFC args)
+      = expandSnocList side ps nilFC (reverse args)
   desugarB side ps (PPair fc l r)
       = do l' <- desugarB side ps l
            r' <- desugarB side ps r
@@ -439,6 +450,18 @@ mutual
       = pure $ apply (IVar consFC (UN "::"))
                 [!(desugarB side ps x), !(expandList side ps nilFC xs)]
 
+  expandSnocList
+             : {auto s : Ref Syn SyntaxInfo} ->
+               {auto b : Ref Bang BangData} ->
+               {auto c : Ref Ctxt Defs} ->
+               {auto u : Ref UST UState} ->
+               {auto m : Ref MD Metadata} ->
+               Side -> List Name -> (nilFC : FC) -> List (FC, PTerm) -> Core RawImp
+  expandSnocList side ps nilFC [] = pure (IVar nilFC (UN "Lin"))
+  expandSnocList side ps nilFC ((consFC, x) :: xs)
+      = pure $ apply (IVar consFC (UN ":<"))
+                [!(expandSnocList side ps nilFC xs) , !(desugarB side ps x)]
+
   addFromString : {auto c : Ref Ctxt Defs} ->
                   FC -> RawImp -> Core RawImp
   addFromString fc tm

src/Idris/Doc/HTML.idr

@@ -12,7 +12,7 @@ import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML
 import Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree
 
-import Idris.DocString
+import Idris.Doc.String
 import Idris.Package.Types
 import Idris.Pretty
 import Idris.Version

src/Idris/Doc/String.idr

@@ -1,4 +1,4 @@
-module Idris.DocString
+module Idris.Doc.String
 
 import Core.Context
 import Core.Context.Log
@@ -233,23 +233,57 @@ getDocsForName fc n
                                    , annotate Declarations $ vcat $ map (indent 2) docs]]
              pure (vcat (params ++ constraints ++ meths ++ insts))
 
-    getExtra : Name -> GlobalDef -> Core (List (Doc IdrisDocAnn))
+    getFieldDoc : Name -> Core (Doc IdrisDocAnn)
-    getExtra n d
+    getFieldDoc nm
       = do syn <- get Syn
+           defs <- get Ctxt
+           Just def <- lookupCtxtExact nm (gamma defs)
+                -- should never happen, since we know that the DCon exists:
+                | Nothing => pure Empty
+           ty <- resugar [] =<< normaliseHoles defs [] (type def)
+           let prettyName = pretty (nameRoot nm)
+           let projDecl = hsep [ fun nm prettyName, colon, prettyTerm ty ]
+           let [(_, str)] = lookupName nm (docstrings syn)
+                  | _ => pure projDecl
+           pure $ annotate (Decl nm)
+                $ vcat [ projDecl
+                       , annotate DocStringBody $ vcat (reflowDoc str)
+                       ]
+
+    getFieldsDoc : Name -> Core (List (Doc IdrisDocAnn))
+    getFieldsDoc recName
+      = do let (Just ns, n) = displayName recName
+               | _ => pure []
+           let recNS = ns <.> mkNamespace n
+           defs <- get Ctxt
+           let fields = getFieldNames (gamma defs) recNS
+           syn <- get Syn
+           case fields of
+             [] => pure []
+             [proj] => pure [header "Projection" <++> annotate Declarations !(getFieldDoc proj)]
+             projs => pure [vcat [header "Projections"
+                                 , annotate Declarations $
+                                      vcat $ map (indent 2) $ !(traverse getFieldDoc projs)]]
+
+    getExtra : Name -> GlobalDef -> Core (List (Doc IdrisDocAnn))
+    getExtra n d = do
+      do syn <- get Syn
          let [] = lookupName n (ifaces syn)
              | [ifacedata] => pure <$> getIFaceDoc ifacedata
              | _ => pure [] -- shouldn't happen, we've resolved ambiguity by now
          case definition d of
-               PMDef _ _ _ _ _
+           PMDef _ _ _ _ _ => pure [showTotal n (totality d)]
-                   => pure [showTotal n (totality d)]
+           TCon _ _ _ _ _ _ cons _ =>
-               TCon _ _ _ _ _ _ cons _
+             do let tot = [showTotal n (totality d)]
-                   => do let tot = [showTotal n (totality d)]
                 cdocs <- traverse (getDConDoc <=< toFullNames) cons
-                         let cdoc = case cdocs of
+                cdoc <- case cdocs of
-                              [] => []
+                  [] => pure []
-                              [doc] => [header "Constructor" <++> annotate Declarations doc]
+                  [doc] => pure
-                              docs => [vcat [header "Constructors"
+                         $ (header "Constructor" <++> annotate Declarations doc)
-                                      , annotate Declarations $ vcat $ map (indent 2) docs]]
+                         :: !(getFieldsDoc n)
+                  docs => pure [vcat [header "Constructors"
+                                     , annotate Declarations $
+                                         vcat $ map (indent 2) docs]]
                 pure (tot ++ cdoc)
            _ => pure []
 
@@ -287,6 +321,7 @@ getDocsForPTerm (PPrimVal _ constant) = getDocsForPrimitive constant
 getDocsForPTerm (PType _) = pure ["Type : Type\n\tThe type of all types is Type. The type of Type is Type."]
 getDocsForPTerm (PString _ _) = pure ["String Literal\n\tDesugars to a fromString call"]
 getDocsForPTerm (PList _ _ _) = pure ["List Literal\n\tDesugars to (::) and Nil"]
+getDocsForPTerm (PSnocList _ _ _) = pure ["SnocList Literal\n\tDesugars to (:<) and Empty"]
 getDocsForPTerm (PPair _ _ _) = pure ["Pair Literal\n\tDesugars to MkPair or Pair"]
 getDocsForPTerm (PDPair _ _ _ _ _) = pure ["Dependant Pair Literal\n\tDesugars to MkDPair or DPair"]
 getDocsForPTerm (PUnit _) = pure ["Unit Literal\n\tDesugars to MkUnit or Unit"]

src/Idris/Driver.idr

@@ -247,9 +247,12 @@ quitOpts [] = pure True
 quitOpts (Version :: _)
     = do putStrLn versionMsg
          pure False
-quitOpts (Help :: _)
+quitOpts (Help Nothing :: _)
     = do putStrLn usage
          pure False
+quitOpts (Help (Just HelpLogging) :: _)
+    = do putStrLn helpTopics
+         pure False
 quitOpts (ShowPrefix :: _)
     = do putStrLn yprefix
          pure False

src/Idris/IDEMode/CaseSplit.idr

@@ -49,6 +49,7 @@ toStrUpdate (UN n, term)
     bracket : PTerm -> PTerm
     bracket tm@(PRef _ _) = tm
     bracket tm@(PList _ _ _) = tm
+    bracket tm@(PSnocList _ _ _) = tm
     bracket tm@(PPair _ _ _) = tm
     bracket tm@(PUnit _) = tm
     bracket tm@(PComprehension _ _ _) = tm

src/Idris/IDEMode/SyntaxHighlight.idr

@@ -8,7 +8,7 @@ import Core.TT
 
 import Idris.REPL
 import Idris.Syntax
-import Idris.DocString
+import Idris.Doc.String
 import Idris.IDEMode.Commands
 
 import Data.List

src/Idris/Package.idr

@@ -30,7 +30,7 @@ import Libraries.Utils.Path
 
 import Idris.CommandLine
 import Idris.Doc.HTML
-import Idris.DocString
+import Idris.Doc.String
 import Idris.ModTree
 import Idris.ProcessIdr
 import Idris.REPL

src/Idris/Parser.idr

@@ -384,7 +384,7 @@ mutual
            decorateKeywords fname xs
            pure (PRange fc (fst rstate) (snd rstate) y.val)
 
-  listExpr : FileName -> WithBounds t -> IndentInfo -> Rule PTerm
+  listExpr : FileName -> WithBounds () -> IndentInfo -> Rule PTerm
   listExpr fname s indents
       = do b <- bounds (do ret <- expr pnowith fname indents
                            decoratedSymbol fname "|"
@@ -407,6 +407,26 @@ mutual
                            nilFC = if null xs then fc else boundToFC fname b
                        in PList fc nilFC (map (\ t => (boundToFC fname t, t.val)) xs))
 
+  snocListExpr : FileName -> WithBounds () -> IndentInfo -> Rule PTerm
+  snocListExpr fname s indents
+      = {- TODO: comprehension -}
+        do mHeadTail <- optional $ do
+             hd <- many $ do x <- expr pdef fname indents
+                             b <- bounds (symbol ",")
+                             pure (x <$ b)
+             tl <- expr pdef fname indents
+             pure (hd, tl)
+           {- TODO: reverse ranges -}
+           b <- bounds (symbol "]")
+           pure $
+             let xs : List (WithBounds PTerm)
+                    = case mHeadTail of
+                        Nothing      => []
+                        Just (hd,tl) => hd ++ [ tl <$ b]
+                 fc = boundToFC fname (mergeBounds s b)
+                 nilFC = ifThenElse (null xs) fc (boundToFC fname s)
+             in PSnocList fc nilFC (map (\ t => (boundToFC fname t, t.val)) xs) --)
+
   nonEmptyTuple : FileName -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
   nonEmptyTuple fname s indents e
       = do vals <- some $ do b <- bounds (symbol ",")
@@ -492,7 +512,9 @@ mutual
            pure (PUnquote (boundToFC fname b) b.val)
     <|> do start <- bounds (symbol "(")
            bracketedExpr fname start indents
-    <|> do start <- bounds (symbol "[")
+    <|> do start <- bounds (symbol "[<")
+           snocListExpr fname start indents
+    <|> do start <- bounds (symbol "[>" <|> symbol "[")
            listExpr fname start indents
     <|> do b <- bounds (decoratedSymbol fname "!" *> simpleExpr fname indents)
            pure (PBang (virtualiseFC $ boundToFC fname b) b.val)

src/Idris/Pretty.idr

@@ -306,6 +306,8 @@ mutual
       go d (PBang _ tm) = "!" <+> go d tm
       go d (PIdiom _ tm) = enclose (pretty "[|") (pretty "|]") (go startPrec tm)
       go d (PList _ _ xs) = brackets (group $ align $ vsep $ punctuate comma (go startPrec . snd <$> xs))
+      go d (PSnocList _ _ xs) = brackets {ldelim = "[<"}
+                                   (group $ align $ vsep $ punctuate comma (go startPrec . snd <$> xs))
       go d (PPair _ l r) = group $ parens (go startPrec l <+> comma <+> line <+> go startPrec r)
       go d (PDPair _ _ l (PImplicit _) r) = group $ parens (go startPrec l <++> pretty "**" <+> line <+> go startPrec r)
       go d (PDPair _ _ l ty r) = group $ parens (go startPrec l <++> colon <++> go startPrec ty <++> pretty "**" <+> line <+> go startPrec r)

src/Idris/REPL.idr

@@ -29,7 +29,7 @@ import Core.Unify
 import Parser.Unlit
 
 import Idris.Desugar
-import Idris.DocString
+import Idris.Doc.String
 import Idris.Error
 import Idris.IDEMode.CaseSplit
 import Idris.IDEMode.Commands

src/Idris/REPL/Common.idr

@@ -9,7 +9,7 @@ import Core.TT
 import Core.Unify
 import Core.UnifyState
 
-import Idris.DocString
+import Idris.Doc.String
 import Idris.Error
 import Idris.IDEMode.Commands
 import Idris.IDEMode.Holes

src/Idris/REPL/FuzzySearch.idr

@@ -16,7 +16,7 @@ import Core.TT
 import Core.Unify
 
 import Idris.Desugar
-import Idris.DocString
+import Idris.Doc.String
 import Idris.Error
 import Idris.IDEMode.CaseSplit
 import Idris.IDEMode.Commands

src/Idris/Resugar.idr

@@ -48,6 +48,7 @@ addBracket fc tm = if needed tm then PBracketed fc tm else tm
     needed (PUnit _) = False
     needed (PComprehension _ _ _) = False
     needed (PList _ _ _) = False
+    needed (PSnocList _ _ _) = False
     needed (PPrimVal _ _) = False
     needed tm = True
 
@@ -125,11 +126,16 @@ mutual
          "==="    => pure $ PEq fc (unbracket l) (unbracket r)
          "~=~"    => pure $ PEq fc (unbracket l) (unbracket r)
          _        => Nothing
-       else if nameRoot nm == "::"
+       else case nameRoot nm of
-               then case sugarApp (unbracket r) of
+              "::" => case sugarApp (unbracket r) of
                 PList fc nilFC xs => pure $ PList fc nilFC ((opFC, unbracketApp l) :: xs)
                 _           => Nothing
-               else Nothing
+              ":<" => case sugarApp (unbracket r) of
+                        PSnocList fc nilFC xs => pure $ PSnocList fc nilFC
+                                                  -- use a snoc list here in a future version
+                                                  (xs ++ [(opFC, unbracketApp l)])
+                        _                     => Nothing
+              _    => Nothing
   sugarAppM tm =
   -- refolding natural numbers if the expression is a constant
     case extractNat 0 tm of
@@ -141,9 +147,10 @@ mutual
                "Unit"   => pure $ PUnit fc
                "MkUnit" => pure $ PUnit fc
                _           => Nothing
-             else if nameRoot nm == "Nil"
+             else case nameRoot nm of
-                     then pure $ PList fc fc []
+               "Nil" => pure $ PList fc fc []
-                     else Nothing
+               "Lin" => pure $ PSnocList fc fc []
+               _     => Nothing
         _ => Nothing
 
   ||| Put the special names (Nil, ::, Pair, Z, S, etc.) back as syntax

src/Idris/Syntax.idr

@@ -96,7 +96,8 @@ mutual
        PBang : FC -> PTerm -> PTerm
        PIdiom : FC -> PTerm -> PTerm
        PList : (full, nilFC : FC) -> List (FC, PTerm) -> PTerm
-                                        -- ^ location of the conses
+                                        -- ^   v location of the conses/snocs
+       PSnocList : (full, nilFC : FC) -> List ((FC, PTerm)) -> PTerm
        PPair : FC -> PTerm -> PTerm -> PTerm
        PDPair : (full, opFC : FC) -> PTerm -> PTerm -> PTerm -> PTerm
        PUnit : FC -> PTerm
@@ -159,6 +160,7 @@ mutual
   getPTermLoc (PBang fc _) = fc
   getPTermLoc (PIdiom fc _) = fc
   getPTermLoc (PList fc _ _) = fc
+  getPTermLoc (PSnocList fc _ _) = fc
   getPTermLoc (PPair fc _ _) = fc
   getPTermLoc (PDPair fc _ _ _ _) = fc
   getPTermLoc (PUnit fc) = fc
@@ -624,6 +626,8 @@ mutual
     showPrec d (PIdiom _ tm) = "[|" ++ showPrec d tm ++ "|]"
     showPrec d (PList _ _ xs)
         = "[" ++ showSep ", " (map (showPrec d . snd) xs) ++ "]"
+    showPrec d (PSnocList _ _ xs)
+        = "[<" ++ showSep ", " (map (showPrec d . snd) xs) ++ "]"
     showPrec d (PPair _ l r) = "(" ++ showPrec d l ++ ", " ++ showPrec d r ++ ")"
     showPrec d (PDPair _ _ l (PImplicit _) r) = "(" ++ showPrec d l ++ " ** " ++ showPrec d r ++ ")"
     showPrec d (PDPair _ _ l ty r) = "(" ++ showPrec d l ++ " : " ++ showPrec d ty ++
@@ -986,6 +990,9 @@ mapPTermM f = goPTerm where
     goPTerm (PList fc nilFC xs) =
       PList fc nilFC <$> goPairedPTerms xs
       >>= f
+    goPTerm (PSnocList fc nilFC xs) =
+      PSnocList fc nilFC <$> goPairedPTerms xs
+      >>= f
     goPTerm (PPair fc x y) =
       PPair fc <$> goPTerm x
                <*> goPTerm y

src/Libraries/Data/NameMap.idr

@@ -327,6 +327,18 @@ export
   neutral = empty
 
 
+treeFilterBy : (Key -> Bool) -> Tree n v -> NameMap v
+treeFilterBy test = loop empty where
+
+  loop : NameMap v -> Tree _ v -> NameMap v
+  loop acc (Leaf k v)
+    = let True = test k | _ => acc in
+      insert k v acc
+  loop acc (Branch2 t1 _ t2)
+    = loop (loop acc t1) t2
+  loop acc (Branch3 t1 _ t2 _ t3)
+    = loop (loop (loop acc t1) t2) t3
+
 treeFilterByM : Monad m => (Key -> m Bool) -> Tree n v -> m (NameMap v)
 treeFilterByM test = loop empty where
 
@@ -342,6 +354,11 @@ treeFilterByM test = loop empty where
          acc <- loop acc t2
          loop acc t3
 
+export
+filterBy : (Name -> Bool) -> NameMap v -> NameMap v
+filterBy test Empty = Empty
+filterBy test (M _ t) = treeFilterBy test t
+
 export
 filterByM : Monad m => (Name -> m Bool) -> NameMap v -> m (NameMap v)
 filterByM test Empty = pure Empty

src/Libraries/Data/String/Iterator.idr

@@ -22,6 +22,7 @@ data StringIterator : String -> Type where [external]
 -- to avoid subverting the linearity guarantees of withString.
 %foreign
   "scheme:blodwen-string-iterator-new"
+  "C:stringIteratorNew"
   "javascript:stringIterator:new"
 private
 fromString : (str : String) -> StringIterator str
@@ -49,6 +50,7 @@ data UnconsResult : String -> Type where
 -- (e.g. byte offset into an UTF-8 string).
 %foreign
   "scheme:blodwen-string-iterator-next"
+  "C:stringIteratorNext"
   "javascript:stringIterator:next"
 export
 uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str

src/Libraries/Text/PrettyPrint/Prettyprinter/Symbols.idr

@@ -101,8 +101,10 @@ angles : Doc ann -> Doc ann
 angles = enclose langle rangle
 
 export
-brackets : Doc ann -> Doc ann
+brackets : {default lbracket ldelim : Doc ann} ->
-brackets = enclose lbracket rbracket
+           {default rbracket rdelim : Doc ann} ->
+           Doc ann -> Doc ann
+brackets {ldelim, rdelim} = enclose ldelim rdelim
 
 export
 braces : Doc ann -> Doc ann

src/Libraries/Utils/Binary.idr

@@ -151,6 +151,27 @@ getTag {b}
 
 -- Some useful types from the prelude
 
+export
+[Wasteful] TTC Int where
+  toBuf b val
+    = do chunk <- get Bin
+         if avail chunk >= 8
+            then
+              do coreLift $ setInt (buf chunk) (loc chunk) val
+                 put Bin (appended 8 chunk)
+            else do chunk' <- extendBinary 8 chunk
+                    coreLift $ setInt (buf chunk') (loc chunk') val
+                    put Bin (appended 8 chunk')
+
+  fromBuf b
+    = do chunk <- get Bin
+         if toRead chunk >= 8
+            then
+              do val <- coreLift $ getInt (buf chunk) (loc chunk)
+                 put Bin (incLoc 8 chunk)
+                 pure val
+              else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk))))
+
 export
 TTC Int where
   toBuf b val

src/Libraries/Utils/Term.idr

@@ -5,7 +5,7 @@ import System.FFI
 %default total
 
 libterm : String -> String
-libterm s = "C:" ++ s ++ ", libidris2_support"
+libterm s = "C:" ++ s ++ ", libidris2_support, idris_term.h"
 
 %foreign libterm "idris2_setupTerm"
 prim__setupTerm : PrimIO ()

src/Parser/Lexer/Source.idr

@@ -219,7 +219,7 @@ symbols = [",", ";", "_", "`"]
 export
 groupSymbols : List String
 groupSymbols = [".(", -- for things such as Foo.Bar.(+)
-    "@{", "[|", "(", "{", "[", "`(", "`{{", "`["]
+    "@{", "[|", "(", "{", "[<", "[>", "[", "`(", "`{{", "`["]
 
 export
 groupClose : String -> String
@@ -228,6 +228,8 @@ groupClose "@{" = "}"
 groupClose "[|" = "|]"
 groupClose "(" = ")"
 groupClose "[" = "]"
+groupClose "[<" = "]"
+groupClose "[>" = "]"
 groupClose "{" = "}"
 groupClose "`(" = ")"
 groupClose "`{{" = "}}"

src/TTImp/Elab/Local.idr

@@ -33,17 +33,25 @@ localHelper {vars} nest env nestdecls_in func
     = do est <- get EST
          let f = defining est
          defs <- get Ctxt
-         let vis = case !(lookupCtxtExact (Resolved (defining est)) (gamma defs)) of
+         gdef <- lookupCtxtExact (Resolved (defining est)) (gamma defs)
-                        Just gdef => visibility gdef
+         let vis  = maybe Public visibility gdef
-                        Nothing => Public
+         let mult = maybe linear GlobalDef.multiplicity gdef
+
          -- If the parent function is public, the nested definitions need
          -- to be public too
-         let nestdecls =
+         let nestdeclsVis =
                if vis == Public
                   then map setPublic nestdecls_in
                   else nestdecls_in
 
-         let defNames = definedInBlock emptyNS nestdecls
+         -- If the parent function is erased, then the nested definitions
+         -- will be erased too
+         let nestdeclsMult =
+           if mult == erased
+              then map setErased nestdeclsVis
+              else nestdeclsVis
+
+         let defNames = definedInBlock emptyNS nestdeclsMult
          names' <- traverse (applyEnv f)
                             (nub defNames) -- binding names must be unique
                                            -- fixes bug #115
@@ -60,7 +68,7 @@ localHelper {vars} nest env nestdecls_in func
          -- everything
          let oldhints = localHints defs
 
-         let nestdecls = map (updateName nest') nestdecls
+         let nestdecls = map (updateName nest') nestdeclsMult
          log "elab.def.local" 20 $ show nestdecls
 
          traverse_ (processDecl [] nest' env') nestdecls
@@ -134,6 +142,14 @@ localHelper {vars} nest env nestdecls_in func
         = INamespace fc ps (map setPublic decls)
     setPublic d = d
 
+    setErased : ImpDecl -> ImpDecl
+    setErased (IClaim fc _ v opts ty) = IClaim fc erased v opts ty
+    setErased (IParameters fc ps decls)
+        = IParameters fc ps (map setErased decls)
+    setErased (INamespace fc ps decls)
+        = INamespace fc ps (map setErased decls)
+    setErased d = d
+
 export
 checkLocal : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->

src/TTImp/ProcessDef.idr

@@ -854,6 +854,7 @@ processDef opts nest env fc n_in cs_in
 
          -- Dynamically rebind default totality requirement to this function's totality requirement
          -- and use this requirement when processing `with` blocks
+         log "declare.def" 5 $ "Traversing clauses of " ++ show n ++ " with mult " ++ show mult
          let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
          cs <- withTotality treq $
                traverse (checkClause mult (visibility gdef) treq

src/TTImp/ProcessType.idr

@@ -19,6 +19,7 @@ import TTImp.TTImp
 import TTImp.Utils
 
 import Data.List
+import Data.Strings
 import Libraries.Data.NameMap
 
 %default covering
@@ -267,7 +268,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra
          addNameLoc nameFC n
 
          log "declare.type" 1 $ "Processing " ++ show n
-         log "declare.type" 5 $ "Checking type decl " ++ show n ++ " : " ++ show ty_raw
+         log "declare.type" 5 $ unwords ["Checking type decl:", show rig, show n, ":", show ty_raw]
          idx <- resolveName n
 
          -- Check 'n' is undefined

src/TTImp/TTImp.idr

@@ -360,7 +360,7 @@ mutual
 
   export
   Show ImpDecl where
-    show (IClaim _ _ _ opts ty) = show opts ++ " " ++ show ty
+    show (IClaim _ c _ opts ty) = show opts ++ " " ++ show c ++ " " ++ show ty
     show (IData _ _ d) = show d
     show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")"
     show (IParameters _ ps ds)
@@ -1179,9 +1179,5 @@ logRaw : {auto c : Ref Ctxt Defs} ->
          {auto 0 _ : KnownTopic s} ->
          Nat -> Lazy String -> RawImp -> Core ()
 logRaw str n msg tm
-    = do opts <- getSession
+    = when !(logging str n) $
-         let lvl = mkLogLevel (logEnabled opts) str n
+        do logString str n (msg ++ ": " ++ show tm)
-         if keepLog lvl (logEnabled opts) (logLevel opts)
-            then do coreLift $ putStrLn $ "LOG " ++ show lvl ++ ": " ++ msg
-                                          ++ ": " ++ show tm
-            else pure ()

support/c/idris_signal.c

@@ -0,0 +1,217 @@
+#include "idris_signal.h"
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <signal.h>
+
+#ifdef _WIN32
+#include <windows.h>
+HANDLE ghMutex;
+#else
+#include <pthread.h>
+static pthread_mutex_t sig_mutex = PTHREAD_MUTEX_INITIALIZER;
+#endif
+
+// ring buffer style storage for collected
+// signals.
+static int signal_buf_cap = 0;
+static int signals_in_buf = 0;
+static int signal_buf_next_read_idx = 0;
+static int *signal_buf = NULL;
+
+void _init_buf() {
+  if (signal_buf == NULL) {
+    signal_buf_cap = 10;
+    signal_buf = malloc(sizeof(int) * signal_buf_cap);
+  }
+}
+
+// returns truthy or falsey (1 or 0)
+int _lock() {
+#ifdef _WIN32
+  if (ghMutex == NULL) {
+    ghMutex = CreateMutex(
+      NULL,
+      FALSE,
+      NULL);
+  }
+
+  DWORD dwWaitResult = WaitForSingleObject(
+    ghMutex,
+    INFINITE);
+
+  switch (dwWaitResult) 
+    {
+       case WAIT_OBJECT_0: 
+         return 1;
+
+       case WAIT_ABANDONED: 
+         return 0;
+    }
+#else
+  pthread_mutex_lock(&sig_mutex);
+  return 1;
+#endif
+}
+
+void _unlock() {
+#ifdef _WIN32
+  ReleaseMutex(ghMutex);
+#else
+  pthread_mutex_unlock(&sig_mutex);
+#endif
+}
+
+void _collect_signal(int signum);
+
+void _collect_signal_core(int signum) {
+  _init_buf();
+
+  // FIXME: allow for adjusting capacity of signal buffer
+  // instead of ignoring new signals when at capacity.
+  if (signals_in_buf == signal_buf_cap) {
+    return;
+  }
+
+  int write_idx = (signal_buf_next_read_idx + signals_in_buf) % signal_buf_cap;
+  signal_buf[write_idx] = signum;
+  signals_in_buf += 1;
+
+#ifdef _WIN32
+  //re-instate signal handler
+  signal(signum, _collect_signal);
+#endif
+}
+
+void _collect_signal(int signum) {
+  if (_lock()) {
+    _collect_signal_core(signum);
+    _unlock();
+  }
+}
+
+#ifndef _WIN32
+inline struct sigaction _simple_handler(void (*handler)(int)) {
+  struct sigaction new_action;
+
+  new_action.sa_handler = handler;
+  sigemptyset (&new_action.sa_mask);
+  new_action.sa_flags = 0;
+
+  return new_action;
+}
+#endif
+
+int ignore_signal(int signum) {
+#ifdef _WIN32
+  return signal(signum, SIG_IGN) == SIG_ERR ? -1 : 0;
+#else
+  struct sigaction handler = _simple_handler(SIG_IGN);
+  return sigaction(signum, &handler, NULL);
+#endif
+}
+
+int default_signal(int signum) {
+#ifdef _WIN32
+  return signal(signum, SIG_DFL) == SIG_ERR ? -1 : 0;
+#else
+  struct sigaction handler = _simple_handler(SIG_DFL);
+  return sigaction(signum, &handler, NULL);
+#endif
+}
+
+int collect_signal(int signum) {
+#ifdef _WIN32
+  return signal(signum, _collect_signal) == SIG_ERR ? -1 : 0;
+#else
+  struct sigaction handler = _simple_handler(_collect_signal);
+  return sigaction(signum, &handler, NULL);
+#endif
+}
+
+int handle_next_collected_signal() {
+  if (_lock()) {
+    if (signals_in_buf == 0) {
+      return -1;
+    }
+    int next = signal_buf[signal_buf_next_read_idx];
+    signal_buf_next_read_idx = (signal_buf_next_read_idx + 1) % signal_buf_cap;
+    signals_in_buf -= 1;
+    _unlock();
+    return next;
+  }
+  return -1;
+}
+
+int raise_signal(int signum) {
+  return raise(signum);
+}
+
+int send_signal(int pid, int signum) {
+#ifdef _WIN32
+  return raise_signal(signum);
+#else
+  return kill(pid, signum);
+#endif
+}
+
+int sighup() {
+#ifdef _WIN32
+  return -1;
+#else
+  return SIGHUP;
+#endif
+}
+
+int sigint() {
+  return SIGINT;
+}
+
+int sigabrt() {
+  return SIGABRT;
+}
+
+int sigquit() {
+#ifdef _WIN32
+  return -1;
+#else
+  return SIGQUIT;
+#endif
+}
+
+int sigill() {
+  return SIGILL;
+}
+
+int sigsegv() {
+  return SIGSEGV;
+}
+
+int sigtrap() {
+#ifdef _WIN32
+  return -1;
+#else
+  return SIGTRAP;
+#endif
+}
+
+int sigfpe() {
+  return SIGFPE;
+}
+
+int sigusr1() {
+#ifdef _WIN32
+  return -1;
+#else
+  return SIGUSR1;
+#endif
+}
+
+int sigusr2() {
+#ifdef _WIN32
+  return -1;
+#else
+  return SIGUSR2;
+#endif
+}
+

support/c/idris_signal.h

@@ -0,0 +1,46 @@
+#ifndef __IDRIS_SIGNAL_H
+#define __IDRIS_SIGNAL_H
+
+#include <signal.h>
+
+int ignore_signal(int signum);
+int default_signal(int signum);
+
+// Add another signal that should be collected. All collected signals
+// should be handled at the earliest convenience by calling
+// get_next_pending_signal().
+int collect_signal(int signum);
+
+// when collecting signals you can get the next one that has been
+// collected but not yet handled with this function.
+// Returns -1 to indicate no pending signals.
+int handle_next_collected_signal();
+
+// Raise a signal to the current process.
+int raise_signal(int signum);
+
+// Send a signal to another process.
+// IMPORTANT: On Windows you cannot send to other processes
+// so this is implemented as `raise_signal()` which sends the signal
+// to the calling process.
+int send_signal(int pid, int signum);
+
+// available signals in a cross-platform compatible way;
+// omits SIGKILL and SIGSTOP because those signals cannot
+// be handled in a custom way.
+int sigint();
+int sigill();
+int sigsegv();
+int sigfpe();
+int sigabrt();
+
+// Following unavailable in Windows and defined as -1 in
+// this implementation so that they can be unconditionally
+// defined in Idris.
+int sighup();
+int sigquit();
+int sigtrap();
+int sigusr1();
+int sigusr2();
+
+#endif

support/c/idris_support.c

@@ -8,6 +8,9 @@
 #include <stdlib.h>
 #include <unistd.h>
 
+int _argc;
+char **_argv;
+
 #ifdef _WIN32
 extern char **_environ;
 #include "windows/win_utils.h"
@@ -80,6 +83,19 @@ int idris2_time() {
     return time(NULL); // RTS needs to have 32 bit integers at least
 }
 
+void idris2_setArgs(int argc, char *argv[]) {
+    _argc = argc;
+    _argv = argv;
+}
+
+int idris2_getArgCount() {
+    return _argc;
+}
+
+char* idris2_getArg(int n) {
+    return _argv[n];
+}
+
 char* idris2_getEnvPair(int i) {
     return *(environ + i);
 }
@@ -100,6 +116,14 @@ int idris2_unsetenv(const char *name) {
 #endif
 }
 
+int idris2_getPID() {
+#ifdef _WIN32
+    return win32_getPID();
+#else
+    return getpid();
+#endif
+}
+
 // get the number of processors configured
 long idris2_getNProcessors() {
 #ifdef _WIN32

support/c/idris_support.h

@@ -17,8 +17,13 @@ void idris2_sleep(int sec);
 void idris2_usleep(int usec);
 int idris2_time();
 
+int idris2_getArgCount();
+void idris2_setArgs(int argc, char *argv[]);
+char* idris2_getArg(int n);
 char* idris2_getEnvPair(int i);
 
+int idris2_getPID();
+
 long idris2_getNProcessors();
 
 #endif

support/c/windows/win_utils.c

@@ -2,6 +2,7 @@
 #include <stdint.h>
 #include <stdio.h>
 #include <windows.h>
+#include <process.h>
 
 // THis file exists to avoid clashes between windows.h and idris_rts.h
 //
@@ -83,6 +84,10 @@ int win32_getErrno() {
     return GetLastError();
 }
 
+int win32_getPID() {
+    return _getpid();
+}
+
 typedef BOOL (WINAPI *LPFN_GLPI)(
     PSYSTEM_LOGICAL_PROCESSOR_INFORMATION,
     PDWORD);

support/c/windows/win_utils.h

@@ -11,5 +11,6 @@ void win32_sleep(int ms);
 int win32_modenv(const char* name, const char* value, int overwrite);
 
 int win32_getErrno();
+int win32_getPID();
 long win32_getNProcessors();
 

support/chez/support.ss

@@ -186,6 +186,9 @@
 (define (blodwen-buffer-size buf)
   (bytevector-length buf))
 
+(define (blodwen-buffer-free buf)
+  (void))  ; Rely on built-in memory management
+
 (define (blodwen-buffer-setbyte buf loc val)
   (bytevector-u8-set! buf loc val))
 

support/racket/support.rkt

@@ -179,6 +179,9 @@
 (define (blodwen-buffer-size buf)
   (bytevector-length buf))
 
+(define (blodwen-buffer-free buf)
+  (void))  ; Rely on built-in memory management
+
 (define (blodwen-buffer-setbyte buf loc val)
   (bytevector-u8-set! buf loc val))
 

support/refc/cBackend.h

@@ -10,6 +10,7 @@
 #include "mathFunctions.h"
 #include "runtime.h"
 #include "stringOps.h"
+#include "clock.h"
 #include "casts.h"
 #include "conCaseHelper.h"
 #include "prim.h"

support/refc/casts.c

@@ -22,7 +22,7 @@ Value *cast_i32_to_Bits16(Value *input)
 }
 Value *cast_i32_to_Bits32(Value *input)
 {
-	return input;
+	return newReference(input);
 }
 Value *cast_i32_to_Bits64(Value *input)
 {
@@ -97,7 +97,7 @@ Value *cast_i64_to_Bits32(Value *input)
 
 Value *cast_i64_to_Bits64(Value *input)
 {
-	return input;
+	return newReference(input);
 }
 
 Value *cast_i64_to_i32(Value *input)
@@ -535,7 +535,7 @@ Value *cast_Bits32_to_Bits64(Value *input)
 }
 Value *cast_Bits32_to_i32(Value *input)
 {
-	return input;
+	return newReference(input);
 }
 Value *cast_Bits32_to_i64(Value *input)
 {
@@ -617,7 +617,7 @@ Value *cast_Bits64_to_i32(Value *input)
 }
 Value *cast_Bits64_to_i64(Value *input)
 {
-	return input;
+	return newReference(input);
 }
 Value *cast_Bits64_to_double(Value *input)
 {

support/refc/clock.c

@@ -0,0 +1,52 @@
+#include "clock.h"
+
+#define NSEC_PER_SEC 1000000000
+#define CLOCKS_PER_NSEC ((float)(CLOCKS_PER_SEC / NSEC_PER_SEC))
+
+Value *clockTimeMonotonic()
+{
+    return clockTimeUtc();
+}
+
+Value *clockTimeUtc()
+{
+    return (Value *)makeInt64(time(NULL) * NSEC_PER_SEC);
+}
+
+Value *clockTimeProcess()
+{
+    uint64_t time_ns = clock() / CLOCKS_PER_NSEC;
+    return (Value *)makeInt64(time_ns);
+}
+
+Value *clockTimeThread()
+{
+    return clockTimeProcess();
+}
+
+Value *clockTimeGcCpu()
+{
+    return NULL;
+}
+
+Value *clockTimeGcReal()
+{
+    return NULL;
+}
+
+int clockValid(Value *clock)
+{
+    return clock != NULL;
+}
+
+uint64_t clockSecond(Value *clock)
+{
+    uint64_t totalNano = ((Value_Int64 *)clock)->i64;
+    return totalNano / NSEC_PER_SEC;
+}
+
+uint64_t clockNanosecond(Value *clock)
+{
+    uint64_t totalNano = ((Value_Int64 *)clock)->i64;
+    return totalNano % NSEC_PER_SEC;
+}

support/refc/clock.h

@@ -0,0 +1,19 @@
+#ifndef __IDRIS_CLOCK_H__
+#define __IDRIS_CLOCK_H__
+
+#include <time.h>
+
+#include "cBackend.h"
+
+Value *clockTimeMonotonic();
+Value *clockTimeUtc();
+Value *clockTimeProcess();
+Value *clockTimeThread();
+Value *clockTimeGcCpu();
+Value *clockTimeGcReal();
+
+int clockValid(Value *clock);
+uint64_t clockSecond(Value *clock);
+uint64_t clockNanosecond(Value *clock);
+
+#endif

support/refc/datatypes.h

@@ -76,7 +76,7 @@ typedef struct
 typedef struct
 {
     Value_header header;
-    char c;
+    unsigned char c;
 } Value_Char;
 
 typedef struct

support/refc/mathFunctions.c

@@ -7,11 +7,6 @@ double unpackDouble(Value *d)
     return ((Value_Double *)d)->d;
 }
 
-Value *believe_me(Value *a, Value *b, Value *c)
-{
-    return c;
-}
-
 /* add */
 Value *add_i32(Value *x, Value *y)
 {