Merge

.github/workflows/ci-api.yml

@@ -11,6 +11,9 @@ on:
 
 env:
   SCHEME: scheme
+  IDRIS2_TESTS_CG: chez
+  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
+
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -26,4 +29,4 @@ jobs:
         shell: bash
       - name: Test API
         run: cd tests/idris2/api001 && ./run idris2
-        shell: bash
+        shell: bash

.github/workflows/ci-macos.yml

@@ -10,6 +10,9 @@ on:
       - master
 env:
   SCHEME: chez
+  IDRIS2_TESTS_CG: chez
+  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
+
 jobs:
   build:
     runs-on: macos-latest
@@ -26,4 +29,4 @@ jobs:
         shell: bash
       - name: Build and test self-hosted
         run: make clean && make all && make test INTERACTIVE=''
-        shell: bash
+        shell: bash

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

@@ -9,6 +9,10 @@ on:
     branches:
       - master
 
+env:
+  IDRIS2_TESTS_CG: racket
+  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
+
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -17,9 +21,8 @@ jobs:
         uses: actions/checkout@v2
       - name: Install build dependencies
         run: |
-          sudo apt-get update 
+          sudo apt-get update
           sudo apt-get install -y racket
       - name: Build from bootstrap
         run: make bootstrap-racket
         shell: bash
-

.github/workflows/ci-ubuntu.yml

@@ -11,6 +11,9 @@ on:
 
 env:
   SCHEME: scheme
+  IDRIS2_TESTS_CG: chez
+  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
+
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -27,4 +30,3 @@ jobs:
       - name: Build and test self-hosted
         run: make clean && make all && make test INTERACTIVE=''
         shell: bash
-

.github/workflows/ci-windows.yml

@@ -12,7 +12,9 @@ env:
   MSYSTEM: MINGW64
   MSYS2_PATH_TYPE: inherit
   SCHEME: scheme
+  IDRIS2_TESTS_CG: chez
   CC: gcc
+  ACTIONS_ALLOW_UNSECURE_COMMANDS: true
 
 jobs:
   build:
@@ -24,7 +26,7 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v2
       - name: Get Chez Scheme
-        run: | 
+        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))"
@@ -43,4 +45,4 @@ jobs:
         run: |
           scheme --version
       - name: Bootstrap and install
-        run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make bootstrap && make install"
+        run: c:\msys64\usr\bin\bash -l -c "cd $env:PWD && make bootstrap && make install"

CHANGELOG.md

@@ -29,6 +29,8 @@ Compiler changes:
 
 * Added primitives to the parsing library used in the compiler to get more precise
   boundaries to the AST nodes `FC`.
+* New experimental ``refc`` code generator, which generates C with reference
+  counting.
 
 REPL/IDE mode changes:
 

Makefile

@@ -87,9 +87,11 @@ test:
 
 support:
 	@${MAKE} -C support/c
+	@${MAKE} -C support/refc
 
 support-clean:
 	@${MAKE} -C support/c clean
+	@${MAKE} -C support/refc clean
 
 clean-libs:
 	${MAKE} -C libs/prelude clean
@@ -129,6 +131,7 @@ install-support:
 	install support/gambit/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/gambit
 	install support/js/* ${PREFIX}/idris2-${IDRIS2_VERSION}/support/js
 	@${MAKE} -C support/c install
+	@${MAKE} -C support/refc install
 
 install-libs:
 	${MAKE} -C libs/prelude install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}

Release/mkdist.sh

@@ -17,7 +17,7 @@ git checkout tags/v$1
 rm -rf .git
 rm -rf .github
 rm .git*
-rm .travis*
+rm -f .travis*
 rm -rf Release
 find . -type f -name '.gitignore' -exec rm -f {} \;
 

docs/source/backends/index.rst

@@ -61,4 +61,5 @@ or via the `IDRIS2_CG` environment variable.
    racket
    gambit
    javascript
+   refc
    custom

docs/source/backends/refc.rst

@@ -0,0 +1,35 @@
+*************************
+C with Reference Counting
+*************************
+
+There is an experimental code generator which compiles to an executable via C,
+using a reference counting garbage collector. This is intended as a lightweight
+(i.e. minimal dependencies) code generator that can be ported to multiple
+platforms, especially those with memory constraints.
+    
+Performance is not as good as the Scheme based code generators, partly because
+the reference counting has not yet had any optimisation, and partly because of
+the limitations of C. However, the main goal is portability: the generated
+code should run on any platform that supports a C compiler.
+
+This code generator can be accessed via the REPL command:
+
+::
+
+    Main> :set cg refc
+
+Alternatively, you can set it via the ``IDRIS2_CG`` environment variable:
+
+::
+
+    $ export IDRIS2_CG=refc
+
+The C compiler it invokes is determined by either the ``IDRIS2_CC`` or ``CC``
+environment variables. If neither is set, it uses ``cc``.
+
+This code generator does not yet support `:exec`, just `:c`.
+
+Also note that, if you link with any dynamic libraries for interfacing with
+C, you will need to arrange for them to be accessible via ``LD_LIBRARY_PATH``
+when running the executable. The default Idris 2 support libraries are
+statically linked.

docs/source/faq/faq.rst

@@ -32,7 +32,7 @@ is a very convenient way to bootstrap.
 Can Idris 2 generate Javascript? What about plug-in code generators?
 ====================================================================
 
-Yes! A `JavaScript code generator <https://idris2.readthedocs.io/en/latest/backends/javascript.html/>`_
+Yes! A `JavaScript code generator <https://idris2.readthedocs.io/en/latest/backends/javascript.html>`_
 is built in, and can target either the browser or NodeJS.
 
 Like Idris 1, Idris 2 

docs/source/tutorial/starting.rst

@@ -89,6 +89,8 @@ which you can run:
     $ idris2 hello.idr -o hello
     $ ./build/exec/hello
     Hello world
+    
+(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:

idris2api.ipkg

@@ -21,6 +21,8 @@ modules =
     Compiler.ES.RemoveUnused,
     Compiler.ES.TailRec,
 
+    Compiler.RefC.RefC,
+
     Compiler.Scheme.Chez,
     Compiler.Scheme.Racket,
     Compiler.Scheme.Gambit,

libs/base/Data/List.idr

@@ -254,6 +254,10 @@ public export
 splitOn : Eq a => a -> List a -> List1 (List a)
 splitOn a = split (== a)
 
+public export
+replaceWhen : (a -> Bool) -> a -> List a -> List a
+replaceWhen p b l = map (\c => if p c then b else c) l
+
 ||| Replaces all occurences of the first argument with the second argument in a list.
 |||
 ||| ```idris example
@@ -262,7 +266,7 @@ splitOn a = split (== a)
 |||
 public export
 replaceOn : Eq a => a -> a -> List a -> List a
-replaceOn a b l = map (\c => if c == a then b else c) l
+replaceOn a = replaceWhen (== a)
 
 public export
 reverseOnto : List a -> List a -> List a

libs/base/Decidable/Equality.idr

@@ -84,12 +84,6 @@ DecEq t => DecEq (Maybe t) where
 -- Either
 --------------------------------------------------------------------------------
 
-Uninhabited (Left x = Right y) where
-  uninhabited Refl impossible
-
-Uninhabited (Right x = Left y) where
-  uninhabited Refl impossible
-
 export
 (DecEq t, DecEq s) => DecEq (Either t s) where
   decEq (Left x) (Left y) with (decEq x y)

libs/base/System/File.idr

@@ -160,6 +160,21 @@ export
 closeFile : HasIO io => File -> io ()
 closeFile (FHandle f) = primIO (prim__close f)
 
+||| Check if a file exists for reading.
+export
+exists : HasIO io => String -> io Bool
+exists f
+    = do Right ok <- openFile f Read
+             | Left err => pure False
+         closeFile ok
+         pure True
+
+||| Pick the first existing file
+export
+firstExists : HasIO io => List String -> io (Maybe String)
+firstExists [] = pure Nothing
+firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
+
 export
 fileError : HasIO io => File -> io Bool
 fileError (FHandle f)

libs/contrib/Data/Container.idr

@@ -0,0 +1,359 @@
+------------------------------------------------------------------------
+-- This module is based on the following papers:
+
+-- Categories of Containers
+-- Abbott, Altenkirch, Ghani
+
+-- Derivatives of Containers
+-- Abbott, Altenkirch, Ghani, McBride
+------------------------------------------------------------------------
+
+module Data.Container
+
+import Data.Either
+import Decidable.Equality
+
+%default total
+
+------------------------------------------------------------------------
+-- Container and their morphisms
+-- * Extension is a functor from Container to Type
+
+-- Objects of the category of containers
+namespace Container
+
+  public export
+  record Container where
+    constructor MkContainer
+    Shape : Type
+    Position : Shape -> Type
+
+  public export
+  record Extension (c : Container) (x : Type) where
+    constructor MkExtension
+    shape    : Shape c
+    payloads : Position c shape -> x
+
+  ||| The image of a container by @Extension@ is a functor
+  public export
+  Functor (Extension c) where map f (MkExtension s p) = MkExtension s (f . p)
+
+-- Morphisms of the category of containers
+namespace Morphism
+
+  public export
+  record Morphism (c, d : Container) where
+    constructor MkMorphism
+    shapeMorphism : Shape c -> Shape d
+    positionMorphism : {s : Shape c} -> Position d (shapeMorphism s) -> Position c s
+
+  public export
+  Extension : Morphism c d -> Extension c x -> Extension d x
+  Extension phi (MkExtension s p)
+    = MkExtension (shapeMorphism phi s) (p . positionMorphism phi)
+
+------------------------------------------------------------------------
+-- Combinators to build containers
+
+namespace Combinators
+
+  -- Constant
+  public export
+  Const : Type -> Container
+  Const k = MkContainer k (const Void)
+
+  export
+  toConst : k -> Extension (Const k) x
+  toConst v = MkExtension v absurd
+
+  export
+  fromConst : Extension (Const k) x -> k
+  fromConst (MkExtension v _) = v
+
+  -- Identity
+  public export
+  Identity : Container
+  Identity = MkContainer () (\ () => ())
+
+  export
+  toIdentity : x -> Extension Identity x
+  toIdentity v = MkExtension () (const v)
+
+  export
+  fromIdentity : Extension Identity x -> x
+  fromIdentity (MkExtension () chld) = chld ()
+
+  -- Composition
+  public export
+  Compose : (d, c : Container) -> Container
+  Compose d c = MkContainer
+    (Extension d (Shape c))
+    (\ (MkExtension shp chld) => (p : Position d shp ** Position c (chld p)))
+
+  export
+  toCompose : (Extension d . Extension c) x -> Extension (Compose d c) x
+  toCompose (MkExtension shp1 chld)
+    = MkExtension (MkExtension shp1 (shape . chld)) (\ (p ** q) => payloads (chld p) q)
+
+  export
+  fromCompose : Extension (Compose d c) x -> (Extension d . Extension c) x
+  fromCompose (MkExtension (MkExtension shp1 shp2) chld)
+    = MkExtension shp1 (\ p => MkExtension (shp2 p) (\ q => chld (p ** q)))
+
+  -- Direct sum
+  public export
+  Sum : (c, d : Container) -> Container
+  Sum c d = MkContainer (Either (Shape c) (Shape d)) (either (Position c) (Position d))
+
+  export
+  toSum : Either (Extension c x) (Extension d x) -> Extension (Sum c d) x
+  toSum (Left (MkExtension shp chld)) = MkExtension (Left shp) chld
+  toSum (Right (MkExtension shp chld)) = MkExtension (Right shp) chld
+
+  export
+  fromSum : Extension (Sum c d) x -> Either (Extension c x) (Extension d x)
+  fromSum (MkExtension (Left shp) chld) = Left (MkExtension shp chld)
+  fromSum (MkExtension (Right shp) chld) = Right (MkExtension shp chld)
+
+  -- Pairing
+  public export
+  Pair : (c, d : Container) -> Container
+  Pair c d = MkContainer (Shape c, Shape d) (\ (p, q) => Either (Position c p) (Position d q))
+
+  export
+  toPair : (Extension c x, Extension d x) -> Extension (Pair c d) x
+  toPair (MkExtension shp1 chld1, MkExtension shp2 chld2)
+    = MkExtension (shp1, shp2) (either chld1 chld2)
+
+  export
+  fromPair : Extension (Pair c d) x -> (Extension c x, Extension d x)
+  fromPair (MkExtension (shp1, shp2) chld)
+    = (MkExtension shp1 (chld . Left), MkExtension shp2 (chld . Right))
+
+  -- Branching over a Type
+  public export
+  Exponential : Type -> Container -> Container
+  Exponential k c = MkContainer (k -> Shape c) (\ p => (v : k ** Position c (p v)))
+
+  export
+  toExponential : (k -> Extension c x) -> Extension (Exponential k c) x
+  toExponential f = MkExtension (shape . f) (\ (v ** p) => payloads (f v) p)
+
+  export
+  fromExponential : Extension (Exponential k c) x -> (k -> Extension c x)
+  fromExponential (MkExtension  shp chld) k = MkExtension (shp k) (\ p => chld (k ** p))
+
+------------------------------------------------------------------------
+-- Taking various fixpoints of containers
+
+namespace Initial
+
+  public export
+  data W : Container -> Type where
+    MkW : Extension c (W c) -> W c
+
+  export
+  map : Morphism c d -> W c -> W d
+  map f (MkW (MkExtension shp chld)) = MkW $ Extension f (MkExtension shp (\ p => map f (chld p)))
+  --  Container.map inlined because of -------------------^
+  --  termination checking
+
+  export
+  foldr : (Extension c x -> x) -> W c -> x
+  foldr alg (MkW (MkExtension shp chld)) = alg (MkExtension shp (\ p => foldr alg (chld p)))
+
+  export
+  para : (Extension c (x, W c) -> x) -> W c -> x
+  para alg (MkW (MkExtension shp chld)) = alg (MkExtension shp (\ p => let w = chld p in (para alg w, w)))
+
+namespace Monad
+
+  ||| @Free@ is a wrapper around @W@ to make it inference friendly.
+  ||| Without this wrapper, neither @pure@ nor @bind@ are able to infer their @c@ argument.
+  public export
+  record Free (c : Container) (x : Type) where
+    constructor MkFree
+    runFree : W (Sum c (Const x))
+
+  export
+  pure : x -> Free c x
+  pure x = MkFree $ MkW (toSum (Right (toConst x)))
+
+  export
+  (>>=) : Free c x -> (x -> Free c y) -> Free c y
+  (>>=) (MkFree mx) k = foldr (alg . fromSum {c} {d = Const x}) mx where
+
+    alg : Either (Extension c (Free c y)) (Extension (Const x) (Free c y)) -> Free c y
+    alg  = either (MkFree . MkW . toSum {c} {d = Const y} . Left . map (runFree {c}))
+                  (k . fromConst {k = x})
+
+  export
+  join : Free c (Free c x) -> Free c x
+  join = (>>= id)
+
+namespace Final
+
+  public export
+  data M : Container -> Type where
+    MkM : Extension c (Inf (M c)) -> M c
+
+  export
+  unfoldr : (s -> Extension c s) -> s -> M c
+  unfoldr next seed =
+    let (MkExtension shp chld) = next seed in
+    MkM (MkExtension shp (\ p => unfoldr next (chld p)))
+
+namespace Comonad
+
+  ||| @Cofree@ is a wrapper around @M@ to make it inference friendly.
+  ||| Without this wrapper, neither @extract@ nor @extend@ are able to infer their @c@ argument.
+  public export
+  record Cofree (c : Container) (x : Type) where
+    constructor MkCofree
+    runCofree : M (Pair (Const x) c)
+
+  export
+  extract : Cofree c x -> x
+  extract (MkCofree (MkM m)) = fst (shape m)
+
+  export
+  extend : (Cofree c a -> b) -> Cofree c a -> Cofree c b
+  extend alg = MkCofree . unfoldr next . runCofree where
+
+    next : M (Pair (Const a) c) -> Extension (Pair (Const b) c) (M (Pair (Const a) c))
+    next m@(MkM layer) =
+      let (_, (MkExtension shp chld)) = fromPair {c = Const a} layer in
+      let b = toConst (alg (MkCofree m)) in
+      toPair (b, MkExtension shp (\ p => chld p))
+-- Eta-expanded to force Inf ------^
+
+  export
+  duplicate : Cofree c a -> Cofree c (Cofree c a)
+  duplicate = extend id
+
+------------------------------------------------------------------------
+-- Derivative
+
+namespace Derivative
+
+  public export
+  Derivative : Container -> Container
+  Derivative c = MkContainer
+    (s : Shape c ** Position c s)
+    (\ (s ** p) => (p' : Position c s ** Not (p === p')))
+
+  export
+  hole : (v : Extension (Derivative c) x) -> Position c (fst (shape v))
+  hole (MkExtension (shp ** p) _) = p
+
+  export
+  unplug : (v : Extension c x) -> Position c (shape v) -> (Extension (Derivative c) x, x)
+  unplug (MkExtension shp chld) p = (MkExtension (shp ** p) (chld . fst), chld p)
+
+  export
+  plug : (v : Extension (Derivative c) x) -> DecEq (Position c (fst (shape v))) => x -> Extension c x
+  plug (MkExtension (shp ** p) chld) x = MkExtension shp $ \ p' => case decEq p p' of
+    Yes eq => x
+    No neq => chld (p' ** neq)
+
+  export
+  toConst : Extension (Const Void) x -> Extension (Derivative (Const k)) x
+  toConst v = absurd (fromConst v)
+
+  export
+  fromConst : Extension (Derivative (Const k)) x -> Extension (Const Void) x
+  fromConst v = absurd (hole {c = Const _} v)
+
+  export
+  toIdentity : Extension (Derivative Identity) x
+  toIdentity = MkExtension (() ** ()) (\ (() ** eq) => absurd (eq Refl))
+
+  export
+  toSum : Extension (Sum (Derivative c) (Derivative d)) x ->
+          Extension (Derivative (Sum c d)) x
+  toSum v = case fromSum {c = Derivative c} {d = Derivative d} v of
+    Left (MkExtension (shp ** p) chld) => MkExtension (Left shp ** p) chld
+    Right (MkExtension (shp ** p) chld) => MkExtension (Right shp ** p) chld
+
+  export
+  fromSum : Extension (Derivative (Sum c d)) x ->
+            Extension (Sum (Derivative c) (Derivative d)) x
+  fromSum (MkExtension (shp ** p) chld) = toSum {c = Derivative c} {d = Derivative d} $ case shp of
+    Left shp => Left (MkExtension (shp ** p) chld)
+    Right shp => Right (MkExtension (shp ** p) chld)
+
+  export
+  toPair : Extension (Sum (Pair (Derivative c) d) (Pair c (Derivative d))) x ->
+           Extension (Derivative (Pair c d)) x
+  toPair v = case fromSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)} v of
+    Left p => let (MkExtension (shp1 ** p1) chld1, MkExtension shp2 chld2) = fromPair {c = Derivative c} p in
+              MkExtension ((shp1, shp2) ** Left p1) $ \ (p' ** neq) => case p' of
+                  Left p1' => chld1 (p1' ** (neq . cong Left))
+                  Right p2' => chld2 p2'
+    Right p => let (MkExtension shp1 chld1, MkExtension (shp2 ** p2) chld2) = fromPair {c} {d = Derivative d} p in
+               MkExtension ((shp1, shp2) ** Right p2) $ \ (p' ** neq) => case p' of
+                  Left p1' => chld1 p1'
+                  Right p2' => chld2 (p2' ** (neq . cong Right))
+
+  export
+  fromPair : Extension (Derivative (Pair c d)) x ->
+             Extension (Sum (Pair (Derivative c) d) (Pair c (Derivative d))) x
+  fromPair (MkExtension ((shp1, shp2) ** p) chld) = case p of
+    Left p1 => toSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)}
+                     (Left (MkExtension ((shp1 ** p1), shp2) $ either
+                         (\ p1' => chld (Left (DPair.fst p1') ** DPair.snd p1' . leftInjective))
+                         (\ p2 => chld (Right p2 ** absurd))))
+    Right p2 => toSum {c = Pair (Derivative c) d} {d = Pair c (Derivative d)}
+                     (Right (MkExtension (shp1, (shp2 ** p2)) $ either
+                         (\ p1 => chld (Left p1 ** absurd))
+                         (\ p2' => chld (Right (DPair.fst p2') ** DPair.snd p2' . rightInjective))))
+
+
+  export
+  fromCompose : Extension (Derivative (Compose c d)) x ->
+                Extension (Pair (Derivative d) (Compose (Derivative c) d)) x
+  fromCompose (MkExtension (MkExtension shp1 shp2 ** (p1 ** p2)) chld)
+    = toPair (left, right) where
+
+      left : Extension (Derivative d) x
+      left = MkExtension (shp2 p1 ** p2)
+           $ \ (p2' ** neqp2) => chld ((p1 ** p2') ** neqp2 . mkDPairInjectiveSnd)
+
+      right : Extension (Compose (Derivative c) d) x
+      right = toCompose
+            $ MkExtension (shp1 ** p1)
+            $ \ (p1' ** neqp1) => MkExtension (shp2 p1')
+                                 $ \ p2' => chld ((p1' ** p2') ** (neqp1 . cong fst))
+
+  export
+  toCompose : ((s : _) -> DecEq (Position c s)) -> ((s : _) -> DecEq (Position d s)) ->
+              Extension (Pair (Derivative d) (Compose (Derivative c) d)) x ->
+              Extension (Derivative (Compose c d)) x
+  toCompose dec1 dec2 v with (fromPair {c = Derivative d} {d = Compose (Derivative c) d} v)
+    toCompose dec1 dec2 v | (MkExtension (shp2 ** p2) chld2, w) with (fromCompose w)
+      toCompose dec1 dec2 v
+        | (MkExtension (shp2 ** p2) chld2, w)
+        | (MkExtension (shp1 ** p1) chld1)
+        = MkExtension (MkExtension shp1 (\ p1' => shp2' p1' (decEq @{dec1 shp1} p1 p1')) **
+                      (p1 ** (p2' (decEq @{dec1 shp1} p1 p1))))
+        $ \ ((p1' ** p2'') ** neq) => chld2' p1' p2'' neq
+
+         where
+          shp2' : (p1' : Position c shp1) -> Dec (p1 === p1') -> Shape d
+          shp2' p1' (Yes eq) = shp2
+          shp2' p1' (No neq) = shape (chld1 (p1' ** neq))
+
+          p2' : (eq : Dec (p1 === p1)) -> Position d (shp2' p1 eq)
+          p2' (Yes Refl) = p2
+          p2' (No neq)   = absurd (neq Refl)
+
+          chld2' : (p1' : Position c shp1) ->
+                   (p2'' : Position d (shp2' p1' (decEq @{dec1 shp1} p1 p1'))) ->
+                   (neq : Not (MkDPair p1 (p2' (decEq @{dec1 shp1} p1 p1)) = MkDPair p1' p2'')) -> x
+          chld2' p1' p2'' neq with (decEq @{dec1 shp1} p1 p1')
+            chld2' p1' p2'' neq | No neq1 = payloads (chld1 (p1' ** neq1)) p2''
+            chld2' _ p2'' neq | Yes Refl with (decEq @{dec1 shp1} p1 p1)
+              chld2' _ p2'' neq | Yes Refl | No argh = absurd (argh Refl)
+              chld2' _ p2'' neq | Yes Refl | Yes Refl with (decEq @{dec2 shp2} p2 p2'')
+                chld2' _ p2'' neq | Yes Refl | Yes Refl | No neq2 = chld2 (p2'' ** neq2)
+                chld2' _ _ neq | Yes Refl | Yes Refl | Yes Refl = absurd (neq Refl)

libs/contrib/Data/InductionRecursion/DybjerSetzer.idr

@@ -0,0 +1,65 @@
+||| There are different flavours of induction-recursion. This is the one
+||| introduced in Dybjer and Setzer's paper:
+||| Indexed induction-recursion
+
+module Data.InductionRecursion.DybjerSetzer
+
+%default total
+
+public export
+data Code : (input : sort -> Type) -> (output : Type) -> Type where
+  Yield  : output -> Code input output
+  Store  : (payload : Type) -> (payload -> Code input output) -> Code input output
+  Branch : (label : Type) -> (toSort : label -> sort) ->
+           (((l : label) -> input (toSort l)) -> Code input output) ->
+           Code input output
+
+public export
+DecodeType
+  : Code input output -> (x : sort -> Type) ->
+    (f : {s : sort} -> x s -> input s) ->
+    Type
+DecodeType (Yield _) x f = ()
+DecodeType (Store payload k) x f = (v : payload ** DecodeType (k v) x f)
+DecodeType (Branch label toSort k) x f
+  = (r : ((l : label) -> x (toSort l)) ** DecodeType (k (\ l => f (r l))) x f)
+
+public export
+DecodeOutput
+  : (c : Code input output) -> (x : Lazy (sort -> Type)) ->
+    (f : {s : sort} -> x s -> input s) ->
+    DecodeType c x f -> output
+DecodeOutput (Yield o) x f _ = o
+DecodeOutput (Store p k) x f (v ** d) = DecodeOutput (k v) x f d
+DecodeOutput (Branch l s k) x f (r ** d) = DecodeOutput (k (\ l => f (r l))) x f d
+
+mutual
+
+  public export
+  data Mu : (f : (s : sort) -> Code input (input s)) -> (s : sort) -> Type where
+    MkMu : {f : (s : sort) -> Code input (input s)} -> {s : sort} ->
+           DecodeType (f s) (Mu f) Decode -> Mu {input} f s
+
+  public export
+  Decode : {f : (s : sort) -> Code input (input s)} ->
+           {s : sort} -> Mu {input} f s -> input s
+  Decode (MkMu d) = DecodeOutput (f s) (Mu f) (\ d => assert_total (Decode d)) d
+
+public export
+bind : Code i o -> (o -> Code i o') -> Code i o'
+bind (Yield v) f = f v
+bind (Store p k) f = Store p (\ v => bind (k v) f)
+bind (Branch l s k) f = Branch l s (\ r => bind (k r) f)
+
+public export
+Functor (Code i) where
+  map f v = bind v (Yield . f)
+
+public export
+Applicative (Code i) where
+  pure = Yield
+  cf <*> co = bind cf (\ f => map (f $) co)
+
+public export
+Monad (Code i) where
+  (>>=) = bind

libs/contrib/Data/Late.idr

@@ -0,0 +1,81 @@
+module Data.Late
+
+%default total
+
+------------------------------------------------------------------------
+-- Type
+
+public export
+data Late : Type -> Type where
+  Now : a -> Late a
+  Later : Inf (Late a) -> Late a
+
+------------------------------------------------------------------------
+-- Creating late values
+
+||| Never return
+never : Late a
+never = Later never
+
+||| Run a small state machine until it reaches a final state and yields a value.
+public export
+unfold : (seed -> Either seed value) -> seed -> Late value
+unfold f s = case f s of
+  Left s' => Later (unfold f s')
+  Right v => Now v
+
+||| It's easier to define map and (<*>) in terms of bind so let's start
+||| by defining it.
+public export
+bind : Late a -> (a -> Late b) -> Late b
+bind (Now v) f = f v
+bind (Later d) f = Later (bind d f)
+
+------------------------------------------------------------------------
+-- Inspecting late values
+
+||| Check whether we already have a value.
+public export
+isNow : Late a -> Maybe a
+isNow (Now v) = Just v
+isNow (Later d) = Nothing
+
+||| Wait for one tick, hoping to get a value.
+public export
+wait : Late a -> Late a
+wait (Later d) = d
+wait d = d
+
+||| Wait for a set number of ticks.
+public export
+engine : Nat -> Late a -> Late a
+engine Z = id
+engine (S n) = engine n . wait
+
+||| Wait for a set number of ticks, hoping to get a value.
+public export
+petrol : Nat -> Late a -> Maybe a
+petrol n = isNow . engine n
+
+||| Accelerate makes things happen twice as fast.
+public export
+accelerate : Late a -> Late a
+accelerate (Later (Later d)) = Later (accelerate d)
+accelerate (Later (Now v)) = Now v
+accelerate d = d
+
+------------------------------------------------------------------------
+-- Instances
+
+public export
+Functor Late where
+  map f d = bind d (Now . f)
+
+public export
+Applicative Late where
+  pure = Now
+  df <*> dx = bind df (\ f => map (f $) dx)
+
+public export
+Monad Late where
+  (>>=) = bind

libs/contrib/Data/Recursion/Free.idr

@@ -0,0 +1,285 @@
+||| Module partially based on McBride's paper:
+||| Turing-Completeness Totally Free
+|||
+||| It gives us a type to describe computation using general recursion
+||| and functions to run these computations for a while or to completion
+||| if we are able to prove them total.
+|||
+||| The content of the Erased section is new. Instead of producing the
+||| domain/evaluation pair by computing a Dybjer-Setzer code we build a
+||| specialised structure that allows us to make the domain proof runtime
+||| irrelevant.
+
+module Data.Recursion.Free
+
+import Data.Late
+import Data.InductionRecursion.DybjerSetzer
+
+%default total
+
+------------------------------------------------------------------------
+-- Type
+
+||| Syntax for a program using general recursion
+public export
+data General : (a : Type) -> (b : a -> Type) -> (x : Type) -> Type where
+  ||| We can return a value without performing any recursive call.
+  Tell : x -> General a b x
+  ||| Or we can pick an input and ask an oracle to give us a return value
+  ||| for it. The second argument is a continuation explaining what we want
+  ||| to do with the returned value.
+  Ask  : (i : a) -> (b i -> General a b x) -> General a b x
+
+||| Type of functions using general recursion
+public export
+PiG : (a : Type) -> (b : a -> Type) -> Type
+PiG a b = (i : a) -> General a b (b i)
+
+||| Recursor for General
+public export
+fold : (x -> y) -> ((i : a) -> (b i -> y) -> y) -> General a b x -> y
+fold pure ask (Tell x) = pure x
+fold pure ask (Ask i k) = ask i (\ o => fold pure ask (k o))
+
+------------------------------------------------------------------------
+-- Basic functions
+
+||| Perform a recursive call and return the value provided by the oracle.
+public export
+call : PiG a b
+call i = Ask i Tell
+
+||| Monadic bind (defined outside of the interface to be able to use it for
+||| map and (<*>)).
+public export
+bind : General a b x -> (x -> General a b y) -> General a b y
+bind m f = fold f Ask m
+
+||| Given a monadic oracle we can give a monad morphism interpreting a
+||| function using general recursion as a monadic process.
+public export
+monadMorphism : Monad m => (t : (i : a) -> m (b i)) -> General a b x -> m x
+monadMorphism t = fold pure (\ i => (t i >>=))
+
+------------------------------------------------------------------------
+-- Instances
+
+public export
+Functor (General a b) where
+  map f = fold (Tell . f) Ask
+
+public export
+Applicative (General a b) where
+  pure = Tell
+  gf <*> gv = bind gf (\ f => map (f $) gv)
+
+public export
+Monad (General a b) where
+  (>>=) = bind
+
+------------------------------------------------------------------------
+-- Fuel-based (partial) evaluation
+
+||| Check whehther we are ready to return a value
+public export
+already : General a b x -> Maybe x
+already = monadMorphism (\ i => Nothing)
+
+||| Use a function using general recursion to expand all of the oracle calls.
+public export
+expand : PiG a b -> General a b x -> General a b x
+expand f = monadMorphism f
+
+||| Recursively call expand a set number of times.
+public export
+engine : PiG a b -> Nat -> General a b x -> General a b x
+engine f Z     = id
+engine f (S n) = engine f n . expand f
+
+||| Check whether recursively calling expand a set number of times is enough
+||| to produce a value.
+public export
+petrol : PiG a b -> Nat -> (i : a) -> Maybe (b i)
+petrol f n i = already $ engine f n $ f i
+
+------------------------------------------------------------------------
+-- Late-based evaluation
+
+||| Rely on an oracle using general recursion to convert a function using
+||| general recursion into a process returning a value in the (distant) future.
+public export
+late : PiG a b -> General a b x -> Late x
+late f = monadMorphism (\ i => Later (assert_total $ late f (f i)))
+
+||| Interpret a function using general recursion as a process returning
+||| a value in the (distant) future.
+public export
+lazy : PiG a b -> (i : a) -> Late (b i)
+lazy f i = late f (f i)
+
+------------------------------------------------------------------------
+-- Domain as a Dybjer-Setzer code and total evaluation function
+
+namespace DybjerSetzer
+
+  ||| Compute, as a Dybjer-Setzer code for an inductive-recursive type, the domain
+  ||| of a function defined by general recursion.
+  public export
+  Domain : PiG a b -> (i : a) -> Code b (b i)
+  Domain f i = monadMorphism ask (f i) where
+
+    ask : (i : a) -> Code b (b i)
+    ask i = Branch () (const i) $ \ t => Yield (t ())
+
+  ||| If a given input is in the domain of the function then we may evaluate
+  ||| it fully on that input and obtain a pure return value.
+  public export
+  evaluate : (f : PiG a b) -> (i : a) -> Mu (Domain f) i -> b i
+  evaluate f i inDom = Decode inDom
+
+  ||| If every input value is in the domain then the function is total.
+  public export
+  totally : (f : PiG a b) -> ((i : a) -> Mu (Domain f) i) ->
+            (i : a) -> b i
+  totally f allInDomain i = evaluate f i (allInDomain i)
+
+------------------------------------------------------------------------
+-- Runtime irrelevant domain and total evaluation function
+
+namespace Erased
+
+  ------------------------------------------------------------------------
+  -- Domain and evaluation functions
+
+  ||| What it means to describe a terminating computation
+  ||| @ f is the function used to answer questions put to the oracle
+  ||| @ d is the description of the computation
+  public export
+  data Layer : (f : PiG a b) -> (d : General a b (b i)) -> Type
+
+  ||| The domain of a function (i.e. the set of inputs for which it terminates)
+  ||| as a predicate on inputs
+  ||| @ f is the function whose domain is being described
+  ||| @ i is the input that is purported to be in the domain
+  Domain : (f : PiG a b) -> (i : a) -> Type
+
+  ||| Fully evaluate a computation known to be terminating.
+  ||| Because of the careful design of the inductive family Layer, we can make
+  ||| the proof runtime irrelevant.
+  evaluateLayer : (f : PiG a b) -> (d : General a b (b i)) -> (0 _ : Layer f d) -> b i
+
+  ||| Fully evaluate a function call for an input known to be in its domain.
+  evaluate : (f : PiG a b) -> (i : a) -> (0 _ : Domain f i) -> b i
+
+  -- In a classic Dybjer-Setzer situation this is computed by induction over the
+  -- index of type `General a b (b i)` and the fixpoint called `Domain` is the
+  -- one thing defined as an inductive type.
+  -- Here we have to flip the script because Idris will only trust inductive data
+  -- as a legitimate source of termination metric for a recursive function. This
+  -- makes our definition of `evaluateLayer` obviously terminating.
+  data Layer : PiG a b -> General a b (b i) -> Type where
+    ||| A computation returning a value is trivially terminating
+    MkTell : {0 a : Type} -> {0 b : a -> Type} -> {0 f : PiG a b} -> {0 i : a} ->
+             (o : b i) -> Layer f (Tell o)
+
+    ||| Performing a call to the oracle is termnating if the input is in its
+    ||| domain and if the rest of the computation is also finite.
+    MkAsk  : {0 a : Type} -> {0 b : a -> Type} -> {0 f : PiG a b} -> {0 i : a} ->
+             (j : a) -> (jprf : Domain f j) ->
+             (k : b j -> General a b (b i)) -> Layer f (k (evaluate f j jprf)) ->
+             Layer f (Ask j k)
+
+  -- Domain is simply defined as the top layer leading to a terminating
+  -- computation with the function used as its own oracle.
+  Domain f i = Layer f (f i)
+
+  ||| A view that gives us a pattern-matching friendly presentation of the
+  ||| @ d computation known to be terminating
+  ||| @ l proof that it is
+  ||| This may seem like a useless definition but the function `view`
+  ||| demonstrates a very important use case: even if the proof is runtime
+  ||| irrelevant, we can manufacture a satisfying view of it.
+  data View : {d : General a b (b i)} -> (l : Layer f d) -> Type where
+    TView : {0 b : a -> Type} -> {0 f : PiG a b} -> (o : b i) -> View (MkTell {b} {f} o)
+    AView : {0 f : PiG a b} ->
+            (j : a) -> (0 jprf : Domain f j) ->
+            (k : b j -> General a b (b i)) -> (0 kprf : Layer f (k (evaluate f j jprf))) ->
+            View (MkAsk j jprf k kprf)
+
+  ||| Function computing the view by pattern-matching on the computation and
+  ||| inverting the proof. Note that the proof is runtime irrelevant even though
+  ||| the resulting view is not: this is possible because the relevant constructor
+  ||| is uniquely determined by the shape of `d`.
+  public export
+  view : (d : General a b (b i)) -> (0 l : Layer f d) -> View l
+  view (Tell o)  (MkTell o)            = TView o
+  view (Ask j k) (MkAsk j jprf k kprf) = AView j jprf k kprf
+
+  -- Just like `Domain` is defined in terms of `Layer`, the evaluation of a
+  -- function call for an input in its domain can be reduced to the evaluation
+  -- of a layer.
+  evaluate f i l = evaluateLayer f (f i) l
+
+  -- The view defined earlier allows us to pattern on the runtime irrelevant
+  -- proof that the layer describes a terminating computation and therefore
+  -- define `evaluateLayer` in a way that is purely structural.
+  -- This becomes obvious if one spells out the (forced) pattern corresponding
+  -- to `d` in each branch of the case.
+  evaluateLayer f d l = case view d l of
+    TView o => o
+    AView j jprf k kprf => evaluateLayer f (k (evaluate f j jprf)) kprf
+
+  ||| If a function's domain is total then it is a pure function.
+  public export
+  totally : (f : PiG a b) -> (0 _ : (i : a) -> Domain f i) ->
+            (i : a) -> b i
+  totally f dom i = evaluate f i (dom i)
+
+  ------------------------------------------------------------------------
+  -- Proofs
+
+  ||| Domain is a singleton type
+  export
+  irrelevantDomain : (f : PiG a b) -> (i : a) -> (p, q : Domain f i) -> p === q
+
+  ||| Layer is a singleton type
+  irrelevantLayer
+    : (f : PiG a b) -> (d : General a b (b i)) -> (l, m : Layer f d) -> l === m
+
+  irrelevantDomain f i p q = irrelevantLayer f (f i) p q
+
+  irrelevantLayer f (Tell o)
+    (MkTell o) (MkTell o) = Refl
+  irrelevantLayer f (Ask j k)
+    (MkAsk j jprf1 k kprf1) (MkAsk j jprf2 k kprf2)
+    with (irrelevantDomain f j jprf1 jprf2)
+      irrelevantLayer f (Ask j k)
+        (MkAsk j jprf k kprf1) (MkAsk j jprf k kprf2)
+        | Refl = cong (MkAsk j jprf k)
+               $ irrelevantLayer f (k (evaluate f j jprf)) kprf1 kprf2
+
+  ||| The result of `evaluateLayer` does not depend on the specific proof that
+  ||| `i` is in the domain of the layer of computation at hand.
+  export
+  evaluateLayerIrrelevance
+    : (f : PiG a b) -> (d : General a b (b i)) -> (0 p, q : Layer f d) ->
+      evaluateLayer f d p === evaluateLayer f d q
+  evaluateLayerIrrelevance f d p q
+    = rewrite irrelevantLayer f d p q in Refl
+
+  ||| The result of `evaluate` does not depend on the specific proof that `i`
+  ||| is in the domain of the function at hand.
+  export
+  evaluateIrrelevance
+    : (f : PiG a b) -> (i : a) -> (0 p, q : Domain f i) ->
+      evaluate f i p === evaluate f i q
+  evaluateIrrelevance f i p q
+    = evaluateLayerIrrelevance f (f i) p q
+
+  ||| The result computed by a total function is independent from the proof
+  ||| that it is total.
+  export
+  totallyIrrelevance
+    : (f : PiG a b) -> (0 p, q : (i : a) -> Domain f i) ->
+      (i : a) -> totally f p i === totally f q i
+  totallyIrrelevance f p q i = evaluateIrrelevance f i (p i) (q i)

libs/contrib/Data/String/Parser.idr

@@ -1,11 +1,13 @@
 ||| A simple parser combinator library for strings. Inspired by attoparsec zepto.
 module Data.String.Parser
-import Control.Monad.Identity
+import public Control.Monad.Identity
 import Control.Monad.Trans
 
 import Data.Strings
 import Data.Fin
 import Data.List
+import Data.List1
+import Data.Vect
 
 %default total
 
@@ -121,6 +123,17 @@ export
 optional : Functor m => ParseT m a -> ParseT m (Maybe a)
 optional = optionMap Nothing Just
 
+||| Succeeds if and only if the argument parser fails.
+|||
+||| In Parsec, this combinator is called `notFollowedBy`.
+export
+requireFailure : Functor m => ParseT m a -> ParseT m ()
+requireFailure (P runParser) = P $ \s => reverseResult s <$> runParser s
+where
+  reverseResult : State -> Result a -> Result ()
+  reverseResult s (Fail _ _) = OK () s
+  reverseResult s (OK _ _)   = Fail (pos s) "Purposefully changed OK to Fail"
+
 ||| Fail with some error message
 export
 fail : Applicative m => String -> ParseT m a
@@ -138,12 +151,12 @@ satisfy f = P $ \s => pure $ if s.pos < s.maxPos
 
 ||| Succeeds if the string `str` follows.
 export
-string : Applicative m => String -> ParseT m ()
+string : Applicative m => String -> ParseT m String
 string str = P $ \s => pure $ let len = strLength str in
                               if s.pos+len <= s.maxPos
                                   then let head = strSubstr s.pos len s.input in
                                        if head == str
-                                         then OK () (S s.input (s.pos + len) s.maxPos)
+                                         then OK str (S s.input (s.pos + len) s.maxPos)
                                          else Fail s.pos ("string " ++ show str)
                                   else Fail s.pos ("string " ++ show str)
 
@@ -156,13 +169,25 @@ eos = P $ \s => pure $ if s.pos == s.maxPos
 
 ||| Succeeds if the next char is `c`
 export
-char : Applicative m => Char -> ParseT m ()
-char c = skip $ satisfy (== c)
+char : Applicative m => Char -> ParseT m Char
+char c = satisfy (== c) <?> "char " ++ show c
 
 ||| Parses a space character
 export
 space : Applicative m => ParseT m Char
-space = satisfy isSpace
+space = satisfy isSpace <?> "space"
+
+||| Parses a letter or digit (a character between \'0\' and \'9\').
+||| Returns the parsed character.
+export
+alphaNum : Applicative m => ParseT m Char
+alphaNum = satisfy isAlphaNum <?> "letter or digit"
+
+||| Parses a letter (an upper case or lower case character). Returns the
+||| parsed character.
+export
+letter : Applicative m => ParseT m Char
+letter = satisfy isAlpha <?> "letter"
 
 mutual
     ||| Succeeds if `p` succeeds, will continue to match `p` until it fails
@@ -209,11 +234,23 @@ covering
 takeWhile : Monad m => (Char -> Bool) -> ParseT m String
 takeWhile f = pack <$> many (satisfy f)
 
-||| Parses one or more space characters
+||| Similar to `takeWhile` but fails if the resulting string is empty.
+export
+covering
+takeWhile1 : Monad m => (Char -> Bool) -> ParseT m String
+takeWhile1 f = pack <$> some (satisfy f)
+
+||| Parses zero or more space characters
 export
 covering
 spaces : Monad m => ParseT m ()
-spaces = skip (many space) <?> "white space"
+spaces = skip (many space)
+
+||| Parses one or more space characters
+export
+covering
+spaces1 : Monad m => ParseT m ()
+spaces1 = skip (some space) <?> "whitespaces"
 
 ||| Discards brackets around a matching parser
 export
@@ -253,11 +290,11 @@ digit = do x <- satisfy isDigit
              , ('9', 9)
              ]
 
-fromDigits : Num a => ((Fin 10) -> a) -> List (Fin 10) -> a
+fromDigits : Num a => (Fin 10 -> a) -> List (Fin 10) -> a
 fromDigits f xs = foldl addDigit 0 xs
 where
-  addDigit : a -> (Fin 10) -> a
-  addDigit num d = 10*num + (f d)
+  addDigit : a -> Fin 10 -> a
+  addDigit num d = 10*num + f d
 
 intFromDigits : List (Fin 10) -> Integer
 intFromDigits = fromDigits finToInteger
@@ -278,3 +315,47 @@ integer : Monad m => ParseT m Integer
 integer = do minus <- succeeds (char '-')
              x <- some digit
              pure $ if minus then (intFromDigits x)*(-1) else intFromDigits x
+
+
+||| Parse repeated instances of at least one `p`, separated by `s`,
+||| returning a list of successes.
+|||
+||| @ p the parser for items
+||| @ s the parser for separators
+export
+covering
+sepBy1 : Monad m => (p : ParseT m a)
+                 -> (s : ParseT m b)
+                 -> ParseT m (List1 a)
+sepBy1 p s = [| p ::: many (s *> p) |]
+
+||| Parse zero or more `p`s, separated by `s`s, returning a list of
+||| successes.
+|||
+||| @ p the parser for items
+||| @ s the parser for separators
+export
+covering
+sepBy : Monad m => (p : ParseT m a)
+                -> (s : ParseT m b)
+                -> ParseT m (List a)
+sepBy p s = optionMap [] forget (p `sepBy1` s)
+
+||| Parses /one/ or more occurrences of `p` separated by `comma`.
+export
+covering
+commaSep1 : Monad m => ParseT m a -> ParseT m (List1 a)
+commaSep1 p = p `sepBy1` (char ',')
+
+||| Parses /zero/ or more occurrences of `p` separated by `comma`.
+export
+covering
+commaSep : Monad m => ParseT m a -> ParseT m (List a)
+commaSep p = p `sepBy` (char ',')
+
+||| Run the specified parser precisely `n` times, returning a vector
+||| of successes.
+export
+ntimes : Monad m => (n : Nat) -> ParseT m a -> ParseT m (Vect n a)
+ntimes    Z  p = pure Vect.Nil
+ntimes (S n) p = [| p :: (ntimes n p) |]

libs/contrib/Syntax/PreorderReasoning/Generic.idr

@@ -8,22 +8,22 @@ infix  1  ...
 
 public export
 data Step : (leq : a -> a -> Type) -> a -> a -> Type where
-  (...) : {leq : a -> a -> Type} ->  (y : a) -> x `leq` y -> Step leq x y
+  (...) : (y : a) -> x `leq` y -> Step leq x y
 
 public export
-data FastDerivation : {leq : a -> a -> Type} -> (x : a) -> (y : a) -> Type where
-  (|~) : (x : a) -> FastDerivation x x
-  (<~) : {leq : a -> a -> Type} -> {x,y : a} 
-         -> FastDerivation {leq = leq} x y -> {z : a} -> (step : Step leq y z) 
-         -> FastDerivation {leq = leq} x z
+data FastDerivation : (leq : a -> a -> Type) -> (x : a) -> (y : a) -> Type where
+  (|~) : (x : a) -> FastDerivation leq x x
+  (<~) : {x, y : a}
+         -> FastDerivation leq x y -> {z : a} -> (step : Step leq y z)
+         -> FastDerivation leq x z
 
-public export  
-CalcWith : Preorder dom leq => {x,y : dom} -> FastDerivation {leq = leq} x y -> x `leq` y
+public export
+CalcWith : Preorder dom leq => {x,y : dom} -> FastDerivation leq x y -> x `leq` y
 CalcWith (|~ x) = reflexive x
 CalcWith ((<~) der (z ... step)) = transitive {po = leq} _ _ _ (CalcWith der) step
 
 public export
-(~~) : {x,y : dom} 
-         -> FastDerivation {leq = leq} x y -> {z : dom} -> (step : Step Equal y z)
-         -> FastDerivation {leq = leq} x z
+(~~) : {x,y : dom}
+         -> FastDerivation leq x y -> {z : dom} -> (step : Step Equal y z)
+         -> FastDerivation leq x z
 (~~) der (z ... Refl) = der

libs/contrib/Test/Golden.idr

@@ -0,0 +1,322 @@
+||| Core features required to perform Golden file testing.
+|||
+||| We provide the core functionality to run a *single* golden file test, or
+||| a whole test tree.
+||| This allows the developer freedom to use as is or design the rest of the
+||| test harness to their liking.
+|||
+||| This was originally used as part of Idris2's own test suite and
+||| the core functionality is useful for the many and not the few.
+||| Please see Idris2 test harness for example usage.
+|||
+||| # Test Structure
+|||
+||| This harness works from the assumption that each individual golden test
+||| comprises of a directory with the following structure:
+|||
+||| + `run` a *shell* script that runs the test. We expect it to:
+|||   * Use `$1` as the variable standing for the idris executable to be tested
+|||   * May use `${IDRIS2_TESTS_CG}` to pick a codegen that ought to work
+|||   * Clean up after itself (e.g. by running `rm -rf build/`)
+|||
+||| + `expected` a file containting the expected output of `run`
+|||
+||| During testing, the test harness will generate an artefact named `output` and
+||| display both outputs if there is a failure.
+||| During an interactive session the following command is used to compare them as
+||| they are:
+|||
+||| ```sh
+|||  git diff --no-index --exit-code --word-diff=color expected output
+||| ```
+|||
+||| If `git` fails then the runner will simply present the expected and 'given'
+||| files side-by-side.
+|||
+||| Of note, it is helpful if `output` was added to a local `.gitignore` instance
+||| to ensure that it is not mistakenly versioned.
+|||
+||| # Options
+|||
+||| The test harness has several options that may be set:
+|||
+||| + `idris2`       The path of the executable we are testing.
+||| + `onlyNames`    The list of tests to run relative to the generated executable.
+||| + `interactive`  Whether to offer to update the expected file or not.
+||| + `timing`       Whether to display time taken for each test.
+|||
+||| We provide an options parser (`options`) that will take the command line arguments
+||| and constructs this for you.
+|||
+||| # Usage
+|||
+||| When compiled to an executable the expected usage is:
+|||
+|||```sh
+|||runtests <path to executable under test> [--timing] [--interactive] [--only [NAMES]]
+|||```
+|||
+||| assuming that the test runner is compiled to an executable named `runtests`.
+
+module Test.Golden
+
+import Data.Maybe
+import Data.List
+import Data.List1
+import Data.Strings
+
+import System
+import System.Clock
+import System.Directory
+import System.File
+import System.Info
+import System.Path
+
+-- [ Options ]
+
+||| Options for the test driver.
+public export
+record Options where
+  constructor MkOptions
+  ||| Name of the idris2 executable
+  exeUnderTest : String
+  ||| Which codegen should we use?
+  codegen      : Maybe String
+  ||| Should we only run some specific cases?
+  onlyNames    : List String
+  ||| Should we run the test suite interactively?
+  interactive  : Bool
+  ||| Should we time and display the tests
+  timing       : Bool
+
+export
+usage : String -> String
+usage exe = unwords ["Usage:", exe, "runtests <path> [--timing] [--interactive] [--cg CODEGEN] [--only [NAMES]]"]
+
+||| Process the command line options.
+export
+options : List String -> Maybe Options
+options args = case args of
+    (_ :: exeUnderTest :: rest) => go rest (MkOptions exeUnderTest Nothing [] False False)
+    _ => Nothing
+
+  where
+
+    go : List String -> Options -> Maybe Options
+    go rest opts = case rest of
+      []                      => pure opts
+      ("--timing" :: xs)      => go xs (record { timing = True} opts)
+      ("--interactive" :: xs) => go xs (record { interactive = True } opts)
+      ("--cg" :: cg :: xs)    => go xs (record { codegen = Just cg } opts)
+      ("--only" :: xs)        => pure $ record { onlyNames = xs } opts
+      _ => Nothing
+
+-- [ Core ]
+
+export
+fail : String -> IO ()
+fail err
+    = do putStrLn err
+         exitWith (ExitFailure 1)
+
+
+||| Normalise strings between different OS.
+|||
+||| on Windows, we just ignore backslashes and slashes when comparing,
+||| similarity up to that is good enough. Leave errors that depend
+||| on the confusion of slashes and backslashes to unix machines.
+normalize : String -> String
+normalize str =
+    if isWindows
+      then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
+      else str
+
+||| Run the specified Golden test with the supplied options.
+|||
+||| See the module documentation for more information.
+|||
+||| @currdir absolute or relative path to root test directory.
+||| @testpath the directory that contains the test.
+export
+runTest : Options -> (currdir, testPath : String) -> IO Bool
+runTest opts currdir testPath
+    = do changeDir testPath
+         isSuccess <- runTest'
+         changeDir currdir
+         pure isSuccess
+    where
+        getAnswer : IO Bool
+        getAnswer = do
+          str <- getLine
+          case str of
+            "y" => pure True
+            "n" => pure False
+            _   => do putStrLn "Invalid Answer."
+                      getAnswer
+
+        printExpectedVsOutput : String -> String -> IO ()
+        printExpectedVsOutput exp out = do
+          putStrLn "Expected:"
+          putStrLn exp
+          putStrLn "Given:"
+          putStrLn out
+
+        mayOverwrite : Maybe String -> String -> IO ()
+        mayOverwrite mexp out = do
+          the (IO ()) $ case mexp of
+            Nothing => putStr $ unlines
+              [ "Golden value missing. I computed the following result:"
+              , out
+              , "Accept new golden value? [yn]"
+              ]
+            Just exp => do
+              putStrLn "Golden value differs from actual value."
+              code <- system "git diff --no-index --exit-code --word-diff=color expected output"
+              when (code < 0) $ printExpectedVsOutput exp out
+              putStrLn "Accept actual value as new golden value? [yn]"
+          b <- getAnswer
+          when b $ do Right _ <- writeFile "expected" out
+                          | Left err => print err
+                      pure ()
+
+        printTiming : Bool -> Clock type -> String -> IO ()
+        printTiming True  clock msg = putStrLn (unwords [msg, show clock])
+        printTiming False _     msg = putStrLn msg
+
+        runTest' : IO Bool
+        runTest'
+            = do putStr $ testPath ++ ": "
+                 start <- clockTime Thread
+                 let cg = case codegen opts of
+                            Nothing => ""
+                            Just cg => "env IDRIS2_TESTS_CG=" ++ cg ++ " "
+                 system $ cg ++ "sh ./run " ++ exeUnderTest opts ++ " | tr -d '\\r' > output"
+                 end <- clockTime Thread
+                 Right out <- readFile "output"
+                     | Left err => do print err
+                                      pure False
+                 Right exp <- readFile "expected"
+                     | Left FileNotFound => do
+                         if interactive opts
+                           then mayOverwrite Nothing out
+                           else print FileNotFound
+                         pure False
+                     | Left err => do print err
+                                      pure False
+                 let result = normalize out == normalize exp
+                 let time = timeDifference end start
+                 if result
+                    then printTiming (timing opts) time "success"
+                    else do
+                      printTiming (timing opts) time "FAILURE"
+                      if interactive opts
+                         then mayOverwrite (Just exp) out
+                         else printExpectedVsOutput exp out
+
+                 pure result
+
+||| Find the first occurrence of an executable on `PATH`.
+export
+pathLookup : List String -> IO (Maybe String)
+pathLookup names = do
+  path <- getEnv "PATH"
+  let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
+  let candidates = [p ++ "/" ++ x | p <- pathList,
+                                    x <- names]
+  firstExists candidates
+
+
+||| Some test may involve Idris' backends and have requirements.
+||| We define here the ones supported by Idris
+public export
+data Requirement = Chez | Node | Racket
+
+export
+Show Requirement where
+  show Chez = "Chez"
+  show Node = "node"
+  show Racket = "racket"
+
+export
+checkRequirement : Requirement -> IO (Maybe String)
+checkRequirement req
+  = do let (envvar, paths) = requirement req
+       Just exec <- getEnv envvar | Nothing => pathLookup paths
+       pure (Just exec)
+
+  where
+    requirement : Requirement -> (String, List String)
+    requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "scheme", "scheme.exe"])
+    requirement Node = ("NODE", ["node"])
+    requirement Racket = ("RACKET", ["racket"])
+
+export
+findCG : IO (Maybe String)
+findCG
+  = do Nothing <- getEnv "IDRIS2_TESTS_CG" | p => pure p
+       Nothing <- checkRequirement Chez    | p => pure (Just "chez")
+       Nothing <- checkRequirement Node    | p => pure (Just "node")
+       Nothing <- checkRequirement Racket  | p => pure (Just "racket")
+       pure Nothing
+
+||| A test pool is characterised by
+|||  + a list of requirement
+|||  + and a list of directory paths
+public export
+record TestPool where
+  constructor MkTestPool
+  constraints : List Requirement
+  testCases : List String
+
+||| Only keep the tests that have been asked for
+export
+filterTests : Options -> List String -> List String
+filterTests opts = case onlyNames opts of
+  [] => id
+  xs => filter (\ name => any (`isInfixOf` name) xs)
+
+||| A runner for a test pool
+export
+poolRunner : Options -> (currdir : String) -> TestPool -> IO (List Bool)
+poolRunner opts currdir pool
+  = do -- check that we indeed want to run some of these tests
+       let tests = filterTests opts (testCases pool)
+       let (_ :: _) = tests
+             | [] => pure []
+       -- if so make sure the constraints are satisfied
+       cs <- for (constraints pool) $ \ req => do
+          mfp <- checkRequirement req
+          putStrLn $ case mfp of
+            Nothing => show req ++ " not found"
+            Just fp => "Found " ++ show req ++ " at " ++ fp
+          pure mfp
+       let Just _ = the (Maybe (List String)) (sequence cs)
+             | Nothing => pure []
+       -- if so run them all!
+       traverse (runTest opts currdir) tests
+
+
+||| A runner for a whole test suite
+export
+runner : List TestPool -> IO ()
+runner tests
+    = do args <- getArgs
+         let (Just opts) = options args
+              | _ => do print args
+                        putStrLn (usage "runtests")
+         -- if no CG has been set, find a sensible default based on what is available
+         opts <- case codegen opts of
+                   Nothing => pure $ record { codegen = !findCG } opts
+                   Just _ => pure opts
+         -- grab the current directory
+         Just pwd <- currentDir
+            | Nothing => putStrLn "FATAL: Could not get current working directory"
+         -- run the tests
+         res <- concat <$> traverse (poolRunner opts pwd) tests
+         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res)
+                       ++ " tests successful")
+         if (any not res)
+            then exitWith (ExitFailure 1)
+            else exitWith ExitSuccess
+
+-- [ EOF ]

libs/contrib/contrib.ipkg

@@ -14,7 +14,17 @@ modules = Control.ANSI,
 
           Data.Bool.Algebra,
           Data.Bool.Decidable,
-          
+
+          Data.Container,
+
+          Data.Fin.Extra,
+
+          Data.Fun.Extra,
+
+          Data.InductionRecursion.DybjerSetzer,
+
+          Data.Late,
+
           Data.Linear.Array,
 
           Data.List.Algebra,
@@ -25,10 +35,6 @@ modules = Control.ANSI,
           Data.List.Views.Extra,
           Data.List.Palindrome,
 
-          Data.Fin.Extra,
-
-          Data.Fun.Extra,
-
           Data.Logic.Propositional,
 
           Data.Morphisms.Algebra,
@@ -44,6 +50,8 @@ modules = Control.ANSI,
           Data.Nat.Order.Properties,
           Data.Nat.Properties,
 
+          Data.Recursion.Free,
+
           Data.SortedMap,
           Data.SortedSet,
           Data.Stream.Extra,
@@ -74,6 +82,8 @@ modules = Control.ANSI,
           Language.JSON.String.Tokens,
           Language.JSON.Tokens,
 
+          Test.Golden,
+
           Text.Token,
           Text.Quantity,
           Text.Parser,

libs/prelude/Builtin.idr

@@ -165,6 +165,16 @@ public export
 trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
 trans Refl Refl = Refl
 
+||| Injectivity of MkDPair (first components)
+export
+mkDPairInjectiveFst : MkDPair a pa === MkDPair b qb -> a === b
+mkDPairInjectiveFst Refl = Refl
+
+||| Injectivity of MkDPair (snd components)
+export
+mkDPairInjectiveSnd : MkDPair a pa === MkDPair a qa -> pa === qa
+mkDPairInjectiveSnd Refl = Refl
+
 ||| Subvert the type checker.  This function is abstract, so it will not reduce
 ||| in the type checker.  Use it with care - it can result in segfaults or
 ||| worse!

libs/prelude/Prelude/Types.idr

@@ -24,6 +24,13 @@ data Nat =
 
 %name Nat k, j, i
 
+-- This is used in the compiler as an efficient substitute for integerToNat.
+prim__integerToNat : Integer -> Nat
+prim__integerToNat i
+  = if intToBool (prim__lte_Integer 0 i)
+      then believe_me i
+      else Z
+
 public export
 integerToNat : Integer -> Nat
 integerToNat x
@@ -194,6 +201,9 @@ data Dec : Type -> Type where
   ||| @ contra a demonstration that prop would be a contradiction
   No  : (contra : prop -> Void) -> Dec prop
 
+export Uninhabited (Yes p === No q) where uninhabited eq impossible
+export Uninhabited (No p === Yes q) where uninhabited eq impossible
+
 ------------
 -- EITHER --
 ------------
@@ -207,6 +217,9 @@ data Either : (a : Type) -> (b : Type) -> Type where
   ||| The other possibility, conventionally used to represent success.
   Right : forall a, b. (1 x : b) -> Either a b
 
+export Uninhabited (Left p === Right q) where uninhabited eq impossible
+export Uninhabited (Right p === Left q) where uninhabited eq impossible
+
 ||| Simply-typed eliminator for Either.
 ||| @ f the action to take on Left
 ||| @ g the action to take on Right

src/Compiler/ANF.idr

@@ -72,7 +72,7 @@ mutual
     show (AApp fc c arg)
         = show c ++ " @ (" ++ show arg ++ ")"
     show (ALet fc x val sc)
-        = "%let v" ++ show x ++ " = " ++ show val ++ " in " ++ show sc
+        = "%let v" ++ show x ++ " = (" ++ show val ++ ") in (" ++ show sc ++ ")"
     show (ACon fc n t args)
         = "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")"
     show (AOp fc op args)
@@ -81,10 +81,10 @@ mutual
         = "%extprim " ++ show p ++ "(" ++ showSep ", " (map show args) ++ ")"
     show (AConCase fc sc alts def)
         = "%case " ++ show sc ++ " of { "
-             ++ showSep "| " (map show alts) ++ " " ++ show def
+             ++ showSep "| " (map show alts) ++ " " ++ show def ++ " }"
     show (AConstCase fc sc alts def)
         = "%case " ++ show sc ++ " of { "
-             ++ showSep "| " (map show alts) ++ " " ++ show def
+             ++ showSep "| " (map show alts) ++ " " ++ show def ++ " }"
     show (APrimVal _ x) = show x
     show (AErased _) = "___"
     show (ACrash _ x) = "%CRASH(" ++ show x ++ ")"

src/Compiler/Common.idr

@@ -180,8 +180,7 @@ natHackNames
     = [UN "prim__add_Integer",
        UN "prim__sub_Integer",
        UN "prim__mul_Integer",
-       NS preludeNS (UN "natToInteger"),
-       NS preludeNS (UN "integerToNat")]
+       NS typesNS (UN "prim__integerToNat")]
 
 -- Hmm, these dump functions are all very similar aren't they...
 dumpCases : Defs -> String -> List Name ->

src/Compiler/CompileExpr.idr

@@ -174,7 +174,7 @@ natHack = magic
     , MagicCRef typesNS "natToInteger" 1
          (\ _, _, [k] => k)
     , MagicCRef typesNS "integerToNat" 1
-         (\ _, _, [k] => k)
+         (\ fc, fc', [k] => CApp fc (CRef fc' (NS typesNS (UN "prim__integerToNat"))) [k])
     , MagicCRef typesNS "plus" 2
          (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN "prim__add_Integer")) [m, n])
     , MagicCRef typesNS "mult" 2

src/Compiler/ES/ES.idr

@@ -109,7 +109,7 @@ keywordSafe "var" = "var_"
 keywordSafe s = s
 
 jsName : Name -> String
-jsName (NS ns n) = showNSWithSep "_" ns ++ "_" ++ jsName n
+jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n
 jsName (UN n) = keywordSafe $ jsIdent n
 jsName (MN n i) = jsIdent n ++ "_" ++ show i
 jsName (PV n d) = "pat__" ++ jsName n
@@ -258,6 +258,7 @@ jsOp DoubleATan [x] = pure $ "Math.atan(" ++ x ++ ")"
 jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")"
 jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")"
 jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")"
+
 jsOp (Cast IntType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
 jsOp (Cast IntegerType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
 jsOp (Cast CharType IntType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
@@ -270,6 +271,16 @@ jsOp (Cast IntegerType IntType) [x] = boundedInt 63 x
 jsOp (Cast IntType IntegerType) [x] = pure x
 jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")"
 
+jsOp (Cast Bits8Type IntType) [x] = pure x
+jsOp (Cast Bits16Type IntType) [x] = pure x
+jsOp (Cast Bits32Type IntType) [x] = pure x
+jsOp (Cast Bits64Type IntType) [x] = pure x
+
+jsOp (Cast Bits8Type IntegerType) [x] = pure x
+jsOp (Cast Bits16Type IntegerType) [x] = pure x
+jsOp (Cast Bits32Type IntegerType) [x] = pure x
+jsOp (Cast Bits64Type IntegerType) [x] = pure x
+
 jsOp (Cast IntType Bits8Type) [x] = boundedUInt 8 x
 jsOp (Cast IntType Bits16Type) [x] = boundedUInt 16 x
 jsOp (Cast IntType Bits32Type) [x] = boundedUInt 32 x
@@ -297,7 +308,7 @@ jsOp (Cast Bits64Type Bits16Type) [x] = boundedUInt 16 x
 jsOp (Cast Bits64Type Bits32Type) [x] = boundedUInt 32 x
 
 jsOp (Cast ty StringType) [x] = pure $ "(''+" ++ x ++ ")"
-jsOp (Cast ty ty2) [x] = jsCrashExp $ "invalid cast: + " ++ show ty ++ " + ' -> ' + " ++ show ty2
+jsOp (Cast ty ty2) [x] = jsCrashExp $ jsString $ "invalid cast: + " ++ show ty ++ " + ' -> ' + " ++ show ty2
 jsOp BelieveMe [_,_,x] = pure x
 jsOp (Crash) [_, msg] = jsCrashExp msg
 
@@ -366,6 +377,8 @@ jsPrim (NS _ (UN "prim__os")) [] =
     let oscalc = "(o => o === 'linux'?'unix':o==='win32'?'windows':o)"
     sysos <- addConstToPreamble "sysos" (oscalc ++ "(" ++ os ++ ".platform())")
     pure sysos
+jsPrim (NS _ (UN "void")) [_, _] = jsCrashExp $ jsString $ "Error: Executed 'void'"  -- DEPRECATED. TODO: remove when bootstrap has been updated
+jsPrim (NS _ (UN "prim__void")) [_, _] = jsCrashExp $ jsString $ "Error: Executed 'void'"
 jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x)
 
 tag2es : Either Int String -> String

src/Compiler/ES/Imperative.idr

@@ -217,9 +217,9 @@ compileToImperative c tm =
     cdata <- getCompileData Cases tm
     let ndefs = namedDefs cdata
     let ctm = forget (mainExpr cdata)
-    s <- newRef Imps (MkImpSt 0)
+    newRef Imps (MkImpSt 0)
     lst_defs <- traverse getImp (defsUsedByNamedCExp ctm ndefs)
     let defs = concat lst_defs
-    let defs_optim = tailRecOptim defs
+    defs_optim <- tailRecOptim defs
     (s, main) <- impExp False ctm
     pure $ (defs_optim, s <+> EvalExpStatement main)

src/Compiler/ES/ImperativeAst.idr

@@ -15,7 +15,7 @@ mutual
                      | IEPrimFnExt Name (List ImperativeExp)
                      | IEConstructorHead ImperativeExp
                      | IEConstructorTag (Either Int String)
-                     | IEConstructorArg Int ImperativeExp
+                     | IEConstructorArg Int ImperativeExp -- constructor arg index starts at 1
                      | IEConstructor (Either Int String) (List ImperativeExp)
                      | IEDelay ImperativeExp
                      | IEForce ImperativeExp
@@ -81,64 +81,104 @@ mutual
 
 mutual
   public export
-  replaceNamesExp : List (Name, ImperativeExp) -> ImperativeExp -> ImperativeExp
-  replaceNamesExp reps (IEVar n) =
-    case lookup n reps of
-      Nothing => IEVar n
-      Just e => e
-  replaceNamesExp reps (IELambda args body) =
-    IELambda args $ replaceNamesExpS reps body
-  replaceNamesExp reps (IEApp f args) =
-    IEApp (replaceNamesExp reps f) (replaceNamesExp reps <$> args)
-  replaceNamesExp reps (IEConstant c) =
-    IEConstant c
-  replaceNamesExp reps (IEPrimFn f args) =
-    IEPrimFn f (replaceNamesExp reps <$> args)
-  replaceNamesExp reps (IEPrimFnExt f args) =
-    IEPrimFnExt f (replaceNamesExp reps <$> args)
-  replaceNamesExp reps (IEConstructorHead e) =
-    IEConstructorHead $ replaceNamesExp reps e
-  replaceNamesExp reps (IEConstructorTag i) =
-    IEConstructorTag i
-  replaceNamesExp reps (IEConstructorArg i e) =
-    IEConstructorArg i (replaceNamesExp reps e)
-  replaceNamesExp reps (IEConstructor t args) =
-    IEConstructor t (replaceNamesExp reps <$> args)
-  replaceNamesExp reps (IEDelay e) =
-    IEDelay $ replaceNamesExp reps e
-  replaceNamesExp reps (IEForce e) =
-    IEForce $ replaceNamesExp reps e
-  replaceNamesExp reps IENull =
-    IENull
+  replaceExp : (ImperativeExp -> Maybe ImperativeExp) -> ImperativeExp -> ImperativeExp
+  replaceExp rep x@(IEVar n) =
+    case rep x of
+      Just z => z
+      Nothing => x
+  replaceExp rep x@(IELambda args body) =
+    case rep x of
+      Just z => z
+      Nothing => IELambda args $ replaceExpS rep body
+  replaceExp rep x@(IEApp f args) =
+    case rep x of
+      Just z => z
+      Nothing => IEApp (replaceExp rep f) (replaceExp rep <$> args)
+  replaceExp rep x@(IEConstant c) =
+    case rep x of
+      Just z => z
+      Nothing => x
+  replaceExp rep x@(IEPrimFn f args) =
+    case rep x of
+      Just z => z
+      Nothing => IEPrimFn f (replaceExp rep <$> args)
+  replaceExp rep x@(IEPrimFnExt f args) =
+    case rep x of
+      Just z => z
+      Nothing => IEPrimFnExt f (replaceExp rep <$> args)
+  replaceExp rep x@(IEConstructorHead e) =
+    case rep x of
+      Just z => z
+      Nothing => IEConstructorHead $ replaceExp rep e
+  replaceExp rep x@(IEConstructorTag i) =
+    case rep x of
+      Just z => z
+      Nothing => x
+  replaceExp rep x@(IEConstructorArg i e) =
+    case rep x of
+      Just z => z
+      Nothing => IEConstructorArg i (replaceExp rep e)
+  replaceExp rep x@(IEConstructor t args) =
+    case rep x of
+      Just z => z
+      Nothing => IEConstructor t (replaceExp rep <$> args)
+  replaceExp rep x@(IEDelay e) =
+    case rep x of
+      Just z => z
+      Nothing => IEDelay $ replaceExp rep e
+  replaceExp rep x@(IEForce e) =
+    case rep x of
+      Just z => z
+      Nothing => IEForce $ replaceExp rep e
+  replaceExp rep x@IENull =
+    case rep x of
+      Just z => z
+      Nothing => x
 
   public export
-  replaceNamesExpS : List (Name, ImperativeExp) -> ImperativeStatement -> ImperativeStatement
-  replaceNamesExpS reps DoNothing =
+  replaceExpS : (ImperativeExp -> Maybe ImperativeExp) -> ImperativeStatement -> ImperativeStatement
+  replaceExpS rep DoNothing =
     DoNothing
-  replaceNamesExpS reps (SeqStatement x y) =
-    SeqStatement (replaceNamesExpS reps x) (replaceNamesExpS reps y)
-  replaceNamesExpS reps (FunDecl fc n args body) =
-    FunDecl fc n args $ replaceNamesExpS reps body
-  replaceNamesExpS reps decl@(ForeignDecl fc n path args ret) =
+  replaceExpS rep (SeqStatement x y) =
+    SeqStatement (replaceExpS rep x) (replaceExpS rep y)
+  replaceExpS rep (FunDecl fc n args body) =
+    FunDecl fc n args $ replaceExpS rep body
+  replaceExpS reps decl@(ForeignDecl fc n path args ret) =
     decl
-  replaceNamesExpS reps (ReturnStatement e) =
-    ReturnStatement $ replaceNamesExp reps e
-  replaceNamesExpS reps (SwitchStatement s alts def) =
-    let s_    = replaceNamesExp reps s
-        alts_ = (\(e,b) => (replaceNamesExp reps e, replaceNamesExpS reps b)) <$> alts
-        def_  = replaceNamesExpS reps <$> def
+  replaceExpS rep (ReturnStatement e) =
+    ReturnStatement $ replaceExp rep e
+  replaceExpS rep (SwitchStatement s alts def) =
+    let s_    = replaceExp rep s
+        alts_ = (\(e,b) => (replaceExp rep e, replaceExpS rep b)) <$> alts
+        def_  = replaceExpS rep <$> def
     in SwitchStatement s_ alts_ def_
-  replaceNamesExpS reps (LetDecl n v) =
-    LetDecl n $ replaceNamesExp reps <$> v
-  replaceNamesExpS reps (ConstDecl n v) =
-    ConstDecl n $ replaceNamesExp reps v
-  replaceNamesExpS reps (MutateStatement n v) =
-    MutateStatement n $ replaceNamesExp reps v
-  replaceNamesExpS reps (ErrorStatement s) =
+  replaceExpS rep (LetDecl n v) =
+    LetDecl n $ replaceExp rep <$> v
+  replaceExpS rep (ConstDecl n v) =
+    ConstDecl n $ replaceExp rep v
+  replaceExpS rep (MutateStatement n v) =
+    MutateStatement n $ replaceExp rep v
+  replaceExpS rep (ErrorStatement s) =
     ErrorStatement s
-  replaceNamesExpS reps (EvalExpStatement x) =
-    EvalExpStatement $ replaceNamesExp reps x
-  replaceNamesExpS reps (CommentStatement x) =
+  replaceExpS rep (EvalExpStatement x) =
+    EvalExpStatement $ replaceExp rep x
+  replaceExpS rep (CommentStatement x) =
     CommentStatement x
-  replaceNamesExpS reps (ForEverLoop x) =
-    ForEverLoop $ replaceNamesExpS reps x
+  replaceExpS rep (ForEverLoop x) =
+    ForEverLoop $ replaceExpS rep x
+
+
+rep : List (Name, ImperativeExp) -> ImperativeExp -> Maybe ImperativeExp
+rep reps (IEVar n) =
+  lookup n reps
+rep _ _ = Nothing
+
+public export
+replaceNamesExpS : List (Name, ImperativeExp) -> ImperativeStatement -> ImperativeStatement
+replaceNamesExpS reps x =
+  replaceExpS (rep reps) x
+
+public export
+replaceNamesExp : List (Name, ImperativeExp) -> ImperativeExp -> ImperativeExp
+replaceNamesExp reps x =
+  replaceExp (rep reps) x

src/Compiler/ES/TailRec.idr

@@ -1,26 +1,52 @@
 module Compiler.ES.TailRec
 
+import Data.Maybe
+import Data.List
+import Data.Strings
+import Data.SortedSet
+import Data.SortedMap
+import Core.Name
+import Core.Context
 import Compiler.ES.ImperativeAst
 
-hasTailCall : Name -> ImperativeStatement -> Bool
-hasTailCall n (SeqStatement x y) =
-    hasTailCall n y
-hasTailCall n (ReturnStatement x) =
+import Debug.Trace
+
+data TailRecS : Type where
+
+record TailSt where
+  constructor MkTailSt
+  nextName : Int
+
+genName : {auto c : Ref TailRecS TailSt} -> Core Name
+genName =
+  do
+    s <- get TailRecS
+    let i = nextName s
+    put TailRecS (record { nextName = i + 1 } s)
+    pure $ MN "imp_gen_tailoptim" i
+
+allTailCalls : ImperativeStatement -> SortedSet Name
+allTailCalls (SeqStatement x y) =
+    allTailCalls y
+allTailCalls (ReturnStatement x) =
     case x of
-        IEApp (IEVar cn) _ => n == cn
-        _ => False
-hasTailCall n (SwitchStatement e alts d) =
-    (any (\(_, w)=>hasTailCall n w) alts) || (maybe False (hasTailCall n) d)
-hasTailCall n (ForEverLoop x) =
-    hasTailCall n x
-hasTailCall n o = False
+        IEApp (IEVar n) _ => insert n empty
+        _ => empty
+allTailCalls (SwitchStatement e alts d) =
+    maybe empty allTailCalls d `union` concat (map allTailCalls (map snd alts))
+allTailCalls (ForEverLoop x) =
+    allTailCalls x
+allTailCalls o = empty
 
 
 argsName : Name
-argsName = MN "tailRecOptimArgs" 0
+argsName = MN "imp_gen_tailoptim_Args" 0
 
 stepFnName : Name
-stepFnName = MN "tailRecOptimStep" 0
+stepFnName = MN "imp_gen_tailoptim_step" 0
+
+fusionArgsName : Name
+fusionArgsName = MN "imp_gen_tailoptim_fusion_args" 0
 
 createNewArgs : List ImperativeExp -> ImperativeExp
 createNewArgs values =
@@ -40,8 +66,6 @@ replaceTailCall n (ReturnStatement x) =
             if n == cn then ReturnStatement $ createNewArgs arg_vals
                 else defRet
         _ => defRet
-
-
 replaceTailCall n (SwitchStatement e alts d) =
     SwitchStatement e (map (\(x,y) => (x, replaceTailCall n y)) alts) (map (replaceTailCall n) d)
 replaceTailCall n (ForEverLoop x) =
@@ -60,11 +84,169 @@ makeTailOptimToBody n argNames body =
         loop = ForEverLoop $ SwitchStatement (IEConstructorHead $ IEVar argsName) [(IEConstructorTag $ Left 0, loopRec)] (Just loopReturn)
     in stepFn <+> createArgInit argNames <+> loop
 
+record CallGraph where
+    constructor MkCallGraph
+    calls, callers : SortedMap Name (SortedSet Name)
+
+showCallGraph : CallGraph -> String
+showCallGraph x =
+    let calls = unlines $ map
+                    (\(x,y) => show x ++ ": " ++ show (SortedSet.toList y))
+                    (SortedMap.toList x.calls)
+        callers = unlines $ map
+                    (\(x,y) => show x ++ ": " ++ show (SortedSet.toList y))
+                    (SortedMap.toList x.callers)
+    in calls ++ "\n----\n" ++ callers
+
+
+tailCallGraph : ImperativeStatement -> CallGraph
+tailCallGraph (SeqStatement x y) =
+    let xg = tailCallGraph x
+        yg = tailCallGraph y
+    in MkCallGraph
+        (mergeWith union xg.calls yg.calls)
+        (mergeWith union xg.callers yg.callers)
+tailCallGraph (FunDecl fc n args body) =
+    let calls = allTailCalls body
+    in MkCallGraph (insert n calls empty) (SortedMap.fromList $ map (\x => (x, SortedSet.insert n empty)) (SortedSet.toList calls))
+tailCallGraph _ = MkCallGraph empty empty
+
+kosarajuL : SortedSet Name -> List Name -> CallGraph -> (SortedSet Name, List Name)
+kosarajuL visited [] graph =
+    (visited, [])
+kosarajuL visited (x::xs) graph =
+    if contains x visited then kosarajuL visited xs graph
+        else let outNeighbours = maybe [] SortedSet.toList $ lookup x (graph.calls)
+                 (visited_, l_) = kosarajuL (insert x visited) (toList outNeighbours) graph
+                 (visited__, l__) = kosarajuL visited_ xs graph
+             in (visited__, l__ ++ (x :: l_))
+
+
+
+kosarajuAssign : CallGraph -> Name -> Name -> SortedMap Name Name -> SortedMap Name Name
+kosarajuAssign graph u root s =
+    case lookup u s of
+        Just _ => s
+        Nothing => let inNeighbours = maybe [] SortedSet.toList $ lookup u (graph.callers)
+                   in foldl (\acc, elem => kosarajuAssign graph elem root acc) (insert u root s) inNeighbours
+
+kosaraju: CallGraph -> SortedMap Name Name
+kosaraju graph =
+    let l = snd $ kosarajuL empty (keys $ graph.calls) graph
+    in foldl (\acc, elem => kosarajuAssign graph elem elem acc) empty l
+
+groupBy : (a -> a -> Bool) -> List a -> List (List a)
+groupBy _ [] = []
+groupBy p' (x'::xs') =
+    let (ys',zs') = go p' x' xs'
+    in (x' :: ys') :: zs'
+    where
+        go : (a -> a -> Bool) -> a -> List a -> (List a, List (List a))
+        go p z (x::xs) =
+            let (ys,zs) = go p x xs
+            in case p z x of
+                True => (x :: ys, zs)
+                False => ([], (x :: ys) :: zs)
+        go _ _ [] = ([], [])
+
+recursiveTailCallGroups : CallGraph -> List (List Name)
+recursiveTailCallGroups graph =
+    let roots = kosaraju graph
+        groups = map (map fst) $
+                 groupBy (\x,y => Builtin.snd x == Builtin.snd y) $
+                 sortBy (\x,y=> compare (snd x) (snd y)) $
+                 toList roots
+    in [x | x<-groups, hasTailCalls x]
+    where
+        hasTailCalls : List Name -> Bool
+        hasTailCalls [] =
+            False
+        hasTailCalls [x] =
+            case lookup x (graph.calls) of
+                Nothing =>
+                    False
+                Just s =>
+                    case SortedSet.toList s of
+                        [n] => n == x
+                        _   => False
+        hasTailCalls _ =
+            True
+
+
+extractFunctions : SortedSet Name -> ImperativeStatement ->
+                     (ImperativeStatement, SortedMap Name (FC, List Name, ImperativeStatement))
+extractFunctions toExtract (SeqStatement x y) =
+    let (xs, xf) = extractFunctions toExtract x
+        (ys, yf) = extractFunctions toExtract y
+    in (xs <+> ys, mergeLeft xf yf)
+extractFunctions toExtract f@(FunDecl fc n args body) =
+    if contains n toExtract then (neutral, insert n (fc, args, body) empty)
+        else (f, empty)
+extractFunctions toExtract x =
+    (x, empty)
+
+getDef : SortedMap Name (FC, List Name, ImperativeStatement) -> Name -> Core (FC, List Name, ImperativeStatement)
+getDef defs n =
+    case lookup n defs of
+        Nothing => throw $ (InternalError $ "Can't find function definition in tailRecOptim")
+        Just x => pure x
+
+
+makeFusionBranch : Name -> List (Name, Nat) ->  (Nat, FC, List Name, ImperativeStatement) ->
+                         (ImperativeExp, ImperativeStatement)
+makeFusionBranch fusionName functionsIdx (i, _, args, body) =
+    let newArgExp = map (\i => IEConstructorArg (cast i) (IEVar fusionArgsName))  [1..(length args)]
+        bodyRepArgs = replaceNamesExpS (zip args newArgExp) body
+    in (IEConstructorTag $ Left $ cast i, replaceExpS rep bodyRepArgs)
+    where
+        rep : ImperativeExp -> Maybe ImperativeExp
+        rep (IEApp (IEVar n) arg_vals) =
+            case lookup n functionsIdx of
+                Nothing => Nothing
+                Just i => Just $ IEApp
+                            (IEVar fusionName)
+                            [IEConstructor (Left $ cast i) arg_vals]
+        rep _ = Nothing
+
+changeBodyToUseFusion : Name -> (Nat, Name, FC, List Name, ImperativeStatement) -> ImperativeStatement
+changeBodyToUseFusion fusionName (i, n, (fc, args, _)) =
+    FunDecl fc n args (ReturnStatement $ IEApp (IEVar fusionName) [IEConstructor (Left $ cast i) (map IEVar args)])
+
+tailRecOptimGroup : {auto c : Ref TailRecS TailSt} ->
+                      SortedMap Name (FC, List Name, ImperativeStatement) ->
+                        List Name -> Core ImperativeStatement
+tailRecOptimGroup defs [] = pure neutral
+tailRecOptimGroup defs [n] =
+    do
+        (fc, args , body) <- getDef defs n
+        pure $ FunDecl fc n args (makeTailOptimToBody n args body)
+tailRecOptimGroup defs names =
+    do
+        fusionName <- genName
+        d <- traverse (getDef defs) names
+        let ids = [0..(length names `minus` 1)]
+        let alts = map (makeFusionBranch fusionName (zip names ids)) (zip ids d)
+        let fusionBody = SwitchStatement
+                           (IEConstructorHead $ IEVar fusionArgsName)
+                           alts
+                           Nothing
+        let fusionArgs = [fusionArgsName]
+        let fusion = FunDecl EmptyFC fusionName fusionArgs (makeTailOptimToBody fusionName fusionArgs fusionBody)
+        let newFunctions = Prelude.concat $ map
+                            (changeBodyToUseFusion fusionName)
+                            (ids `List.zip` (names `List.zip` d))
+        pure $ fusion <+> newFunctions
+
+
+
 export
-tailRecOptim :  ImperativeStatement -> ImperativeStatement
-tailRecOptim (SeqStatement x y) = SeqStatement (tailRecOptim x) (tailRecOptim y)
-tailRecOptim (FunDecl fc n args body) =
-    let new_body = if hasTailCall n body then makeTailOptimToBody n args body
-                        else body
-    in FunDecl fc n args new_body
-tailRecOptim x = x
+tailRecOptim :  ImperativeStatement -> Core ImperativeStatement
+tailRecOptim x =
+    do
+        newRef TailRecS (MkTailSt 0)
+        let graph = tailCallGraph x
+        let groups =  recursiveTailCallGroups graph
+        let functionsToOptimize = foldl SortedSet.union empty $ map SortedSet.fromList groups
+        let (unchanged, defs) = extractFunctions functionsToOptimize x
+        optimized <- traverse (tailRecOptimGroup defs) groups
+        pure $ unchanged <+> (concat optimized)

src/Compiler/Scheme/Common.idr

@@ -31,7 +31,7 @@ schString s = concatMap okchar (unpack s)
 
 export
 schName : Name -> String
-schName (NS ns n) = showNSWithSep "-" ns ++ "-" ++ schName n
+schName (NS ns n) = schString (showNSWithSep "-" ns) ++ "-" ++ schName n
 schName (UN n) = schString n
 schName (MN n i) = schString n ++ "-" ++ show i
 schName (PV n d) = "pat--" ++ schName n
@@ -236,7 +236,8 @@ toPrim pn@(NS _ n)
             (n == UN "prim__arraySet", ArraySet),
             (n == UN "prim__getField", GetField),
             (n == UN "prim__setField", SetField),
-            (n == UN "void", VoidElim),
+            (n == UN "void", VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated
+            (n == UN "prim__void", VoidElim),
             (n == UN "prim__os", SysOS),
             (n == UN "prim__codegen", SysCodegen),
             (n == UN "prim__onCollect", OnCollect),

src/Core/CaseBuilder.idr

@@ -605,8 +605,10 @@ groupCons fc fn pvars cs
          = if a == length pargs
               then addConG n t pargs pats pid rhs acc
               else throw (CaseCompile cfc fn (NotFullyApplied n))
-    addGroup (PTyCon _ n a pargs) pprf pats pid rhs acc
-         = addConG n 0 pargs pats pid rhs acc
+    addGroup (PTyCon cfc n a pargs) pprf pats pid rhs acc
+         = if a == length pargs
+           then addConG n 0 pargs pats pid rhs acc
+           else throw (CaseCompile cfc fn (NotFullyApplied n))
     addGroup (PArrow _ _ s t) pprf pats pid rhs acc
          = addConG (UN "->") 0 [s, t] pats pid rhs acc
     -- Go inside the delay; we'll flag the case as needing to force its

src/Core/Context.idr

@@ -336,8 +336,11 @@ record Context where
     -- access in a program - in all other cases, we'll assume everything is
     -- visible
     visibleNS : List Namespace
-    allPublic : Bool -- treat everything as public. This is only intended
+    allPublic : Bool -- treat everything as public. This is intended
                      -- for checking partially evaluated definitions
+                     -- or for use outside of the main compilation
+                     -- process (e.g. when implementing interactive
+                     -- features such as case splitting).
     inlineOnly : Bool -- only return things with the 'alwaysReduce' flag
     hidden : NameMap () -- Never return these
 
@@ -757,6 +760,15 @@ HasNames (Env Term vars) where
   resolved gam (b :: bs)
       = pure $ !(traverse (resolved gam) b) :: !(resolved gam bs)
 
+export
+HasNames Clause where
+  full gam (MkClause env lhs rhs)
+     = pure $ MkClause !(full gam env) !(full gam lhs) !(full gam rhs)
+
+  resolved gam (MkClause env lhs rhs)
+    = [| MkClause (resolved gam env) (resolved gam lhs) (resolved gam rhs) |]
+
+
 export
 HasNames Def where
   full gam (PMDef r args ct rt pats)

src/Core/Core.idr

@@ -438,6 +438,10 @@ export %inline
 (<$>) : (a -> b) -> Core a -> Core b
 (<$>) f (MkCore a) = MkCore (map (map f) a)
 
+export %inline
+ignore : Core a -> Core ()
+ignore = map (\ _ => ())
+
 -- Monad (specialised)
 export %inline
 (>>=) : Core a -> (a -> Core b) -> Core b

src/Core/Coverage.idr

@@ -2,6 +2,7 @@ module Core.Coverage
 
 import Core.CaseTree
 import Core.Context
+import Core.Context.Log
 import Core.Env
 import Core.Normalise
 import Core.TT
@@ -11,6 +12,8 @@ import Data.Bool.Extra
 import Data.List
 import Data.NameMap
 
+import Text.PrettyPrint.Prettyprinter
+
 %default covering
 
 -- Return whether any of the name matches conflict
@@ -119,8 +122,11 @@ isEmpty : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           Defs -> Env Term vars -> NF vars -> Core Bool
 isEmpty defs env (NTCon fc n t a args)
-     = case !(lookupDefExact n (gamma defs)) of
-            Just (TCon _ _ _ _ flags _ cons _)
+  = do Just nty <- lookupDefExact n (gamma defs)
+         | _ => pure False
+       log "coverage.empty" 10 $ "Checking type: " ++ show nty
+       case nty of
+            TCon _ _ _ _ flags _ cons _
                  => if not (external flags)
                        then allM (conflict defs env (NTCon fc n t a args)) cons
                        else pure False
@@ -482,7 +488,15 @@ export
 checkMatched : {auto c : Ref Ctxt Defs} ->
                List Clause -> ClosedTerm -> Core (Maybe ClosedTerm)
 checkMatched cs ulhs
-    = tryClauses cs !(eraseApps ulhs)
+    = do logTerm "coverage" 5 "Checking coverage for" ulhs
+         logC "coverage" 10 $ pure $ "(raw term: " ++ show !(toFullNames ulhs) ++ ")"
+         ulhs <- eraseApps ulhs
+         logTerm "coverage" 5 "Erased to" ulhs
+         logC "coverage" 5 $ do
+            cs <- traverse toFullNames cs
+            pure $ "Against clauses:\n" ++
+                   (show $ indent {ann = ()} 2 $ vcat $ map (pretty . show) cs)
+         tryClauses cs ulhs
   where
     tryClauses : List Clause -> ClosedTerm -> Core (Maybe ClosedTerm)
     tryClauses [] ulhs

src/Core/FC.idr

@@ -79,6 +79,17 @@ export
 toplevelFC : FC
 toplevelFC = MkFC "(toplevel)" (0, 0) (0, 0)
 
+------------------------------------------------------------------------
+-- Basic operations
+export
+mergeFC : FC -> FC -> Maybe FC
+mergeFC (MkFC fname1 start1 end1) (MkFC fname2 start2 end2) = 
+  if fname1 == fname2
+  then Just $ MkFC fname1 (min start1 start2) (max end1 end2)
+  else Nothing
+mergeFC _ _ = Nothing
+
+
 %name FC fc
 
 ------------------------------------------------------------------------

src/Core/Options.idr

@@ -53,6 +53,7 @@ data CG = Chez
         | Gambit
         | Node
         | Javascript
+        | RefC
         | Other String
 
 export
@@ -62,6 +63,7 @@ Eq CG where
   Gambit == Gambit = True
   Node == Node = True
   Javascript == Javascript = True
+  RefC == RefC = True
   Other s == Other t = s == t
   _ == _ = False
 
@@ -72,6 +74,7 @@ Show CG where
   show Gambit = "gambit"
   show Node = "node"
   show Javascript = "javascript"
+  show RefC = "refc"
   show (Other s) = s
 
 public export
@@ -164,6 +167,7 @@ availableCGs o
        ("racket", Racket),
        ("node", Node),
        ("javascript", Javascript),
+       ("refc", RefC),
        ("gambit", Gambit)] ++ additionalCGs o
 
 export

src/Core/TTC.idr

@@ -751,6 +751,7 @@ TTC CG where
   toBuf b (Other s) = do tag 4; toBuf b s
   toBuf b Node = tag 5
   toBuf b Javascript = tag 6
+  toBuf b RefC = tag 7
 
   fromBuf b
       = case !getTag of
@@ -761,6 +762,7 @@ TTC CG where
                      pure (Other s)
              5 => pure Node
              6 => pure Javascript
+             7 => pure RefC
              _ => corrupt "CG"
 
 export

src/Core/Termination.idr

@@ -25,8 +25,10 @@ totRefs defs (n :: ns)
               | Nothing => pure rest
          case isTerminating (totality d) of
               IsTerminating => pure rest
-              Unchecked => pure rest
-              bad => case rest of
+              Unchecked => do
+                log "totality" 20 $ "Totality unchecked for " ++ show !(toFullNames n)
+                pure rest
+              _ => case rest of
                           NotTerminating (BadCall ns)
                              => toFullNames $ NotTerminating (BadCall (n :: ns))
                           _ => toFullNames $ NotTerminating (BadCall [n])
@@ -43,7 +45,7 @@ export
 checkIfGuarded : {auto c : Ref Ctxt Defs} ->
                  FC -> Name -> Core ()
 checkIfGuarded fc n
-    = do log "totality.termination.guarded" 6 $ "Check if Guarded: " ++ show n
+    = do log "totality.termination.guarded" 6 $ "Check if Guarded: " ++ show !(toFullNames n)
          defs <- get Ctxt
          Just (PMDef _ _ _ _ pats) <- lookupDefExact n (gamma defs)
               | _ => pure ()
@@ -363,7 +365,7 @@ mutual
       = do Just gdef <- lookupCtxtExact fn_in (gamma defs)
                 | Nothing => throw (UndefinedName fc fn_in)
            let fn = fullname gdef
-           log "totality.termination.sizechange" 10 $ "Looking under " ++ show fn
+           log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn)
            aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller"))
            cond [(fn == NS builtinNS (UN "assert_total"), pure []),
               (caseFn fn,
@@ -410,7 +412,7 @@ export
 calculateSizeChange : {auto c : Ref Ctxt Defs} ->
                       FC -> Name -> Core (List SCCall)
 calculateSizeChange loc n
-    = do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show n
+    = do log "totality.termination.sizechange" 5 $ "Calculating Size Change: " ++ show !(toFullNames n)
          defs <- get Ctxt
          Just def <- lookupCtxtExact n (gamma defs)
               | Nothing => throw (UndefinedName loc n)
@@ -447,15 +449,15 @@ checkSC : {auto a : Ref APos Arg} ->
           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 f
+   = do log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f)
         let pos = (f, map (map Builtin.fst) args)
         if pos `elem` path
-           then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show f
+           then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show !(toFullNames f)
                    toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
            else case !(lookupCtxtExact f (gamma defs)) of
-                     Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show f
+                     Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show !(toFullNames f)
                                    pure IsTerminating
-                     Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show f
+                     Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show !(toFullNames f)
                                     continue (sizeChange def) (pos :: path)
   where
     -- Look for something descending in the list of size changes
@@ -492,7 +494,7 @@ checkSC defs f args path
              let Unchecked = isTerminating (totality gdef)
                   | IsTerminating => pure IsTerminating
                   | _ => pure (NotTerminating (BadCall [fnCall sc]))
-             log "totality.termination.sizechange.checkCall" 8 $ "CheckCall Size Change Graph: " ++ show (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
              if not inpath
                 then case term of
@@ -501,12 +503,12 @@ checkSC defs f args path
                           -- was mutually recursive, so start again with new
                           -- arguments (that is, where we'd start if the
                           -- function was the top level thing we were checking)
-                          do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show (fnCall sc)
+                          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 => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show (fnCall sc)
+                       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 (fnCall sc)
+                else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show !(toFullNames (fnCall sc))
                         pure term
 
     getWorst : Terminating -> List Terminating -> Terminating
@@ -524,7 +526,7 @@ calcTerminating : {auto c : Ref Ctxt Defs} ->
                   FC -> Name -> Core Terminating
 calcTerminating loc n
     = do defs <- get Ctxt
-         log "totality.termination.calc" 7 $ "Calculating termination: " ++ show n
+         log "totality.termination.calc" 7 $ "Calculating termination: " ++ show !(toFullNames n)
          case !(lookupCtxtExact n (gamma defs)) of
               Nothing => throw (UndefinedName loc n)
               Just def =>
@@ -558,7 +560,7 @@ checkTerminating : {auto c : Ref Ctxt Defs} ->
                    FC -> Name -> Core Terminating
 checkTerminating loc n
     = do tot <- getTotality loc n
-         log "totality.termination" 6 $ "Checking termination: " ++ show n
+         log "totality.termination" 6 $ "Checking termination: " ++ show !(toFullNames n)
          case isTerminating tot of
               Unchecked =>
                  do tot' <- calcTerminating loc n
@@ -651,7 +653,7 @@ calcPositive : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> Core (Terminating, List Name)
 calcPositive loc n
     = do defs <- get Ctxt
-         log "totality.positivity" 6 $ "Calculating positivity: " ++ show n
+         log "totality.positivity" 6 $ "Calculating positivity: " ++ show !(toFullNames n)
          case !(lookupDefTyExact n (gamma defs)) of
               Just (TCon _ _ _ _ _ tns dcons _, ty) =>
                   case !(totRefsIn defs ty) of
@@ -670,7 +672,7 @@ checkPositive : {auto c : Ref Ctxt Defs} ->
 checkPositive loc n_in
     = do n <- toResolvedNames n_in
          tot <- getTotality loc n
-         log "totality.positivity" 6 $ "Checking positivity: " ++ show n
+         log "totality.positivity" 6 $ "Checking positivity: " ++ show !(toFullNames n)
          case isTerminating tot of
               Unchecked =>
                   do (tot', cons) <- calcPositive loc n
@@ -679,6 +681,7 @@ checkPositive loc n_in
                      pure tot'
               t => pure t
 
+
 -- Check and record totality of the given name; positivity if it's a data
 -- type, termination if it's a function
 export
@@ -690,7 +693,7 @@ checkTotal loc n_in
              | Nothing => throw (UndefinedName loc n_in)
          let n = Resolved nidx
          tot <- getTotality loc n
-         log "totality" 5 $ "Checking totality: " ++ show n
+         log "totality" 5 $ "Checking totality: " ++ show !(toFullNames n)
          defs <- get Ctxt
          case isTerminating tot of
               Unchecked =>

src/Idris/DocString.idr

@@ -188,5 +188,5 @@ getContents ns
              pure (visibility def /= Private)
 
     inNS : Name -> Bool
-    inNS (NS xns (UN _)) = xns == ns
+    inNS (NS xns (UN _)) = ns `isParentOf` xns
     inNS _ = False

src/Idris/IDEMode/REPL.idr

@@ -84,6 +84,7 @@ initIDESocketFile h p = do
                   pure (Left ("Failed to listen on socket with error: " ++ show res))
                else
                  do putStrLn (show p)
+                    fflush stdout
                     res <- accept sock
                     case res of
                       Left err =>

src/Idris/Parser.idr

@@ -1399,13 +1399,14 @@ topDecl fname indents
 -- collectDefs : List PDecl -> List PDecl
 collectDefs [] = []
 collectDefs (PDef annot cs :: ds)
-    = let (cs', rest) = spanBy isClause ds in
-          PDef annot (cs ++ concat cs') :: assert_total (collectDefs rest)
-  where
-    isClause : PDecl -> Maybe (List PClause)
-    isClause (PDef annot cs)
-        = Just cs
-    isClause _ = Nothing
+    = let (csWithFC, rest) = spanBy isPDef ds
+          cs' = cs ++ concat (map snd csWithFC)
+          annot' = foldr 
+                   (\fc1, fc2 => fromMaybe EmptyFC (mergeFC fc1 fc2))
+                   annot 
+                   (map fst csWithFC)
+      in
+          PDef annot' cs' :: assert_total (collectDefs rest)
 collectDefs (PNamespace annot ns nds :: ds)
     = PNamespace annot ns (collectDefs nds) :: collectDefs ds
 collectDefs (PMutual annot nds :: ds)

src/Idris/REPL.idr

@@ -6,6 +6,7 @@ import Compiler.Scheme.Gambit
 import Compiler.ES.Node
 import Compiler.ES.Javascript
 import Compiler.Common
+import Compiler.RefC.RefC
 
 import Core.AutoSearch
 import Core.CaseTree
@@ -189,6 +190,7 @@ findCG
               Gambit => pure codegenGambit
               Node => pure codegenNode
               Javascript => pure codegenJavascript
+              RefC => pure codegenRefC
               Other s => case !(getCodegen s) of
                             Just cg => pure cg
                             Nothing => do coreLift $ putStrLn ("No such code generator: " ++ s)
@@ -704,7 +706,7 @@ process Edit
               Nothing => pure NoFileLoaded
               Just f =>
                 do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts)
-                   coreLift $ system (editor opts ++ " " ++ f ++ line)
+                   coreLift $ system (editor opts ++ " \"" ++ f ++ "\"" ++ line)
                    loadMainFile f
 process (Compile ctm outfile)
     = compileExp ctm outfile

src/Idris/Syntax.idr

@@ -337,6 +337,12 @@ mutual
   getPDeclLoc (PRunElabDecl fc _) = fc
   getPDeclLoc (PDirective fc _) = fc
 
+  export
+  isPDef : PDecl -> Maybe (FC, List PClause)
+  isPDef (PDef annot cs) = Just (annot, cs)
+  isPDef _ = Nothing
+
+
 definedInData : PDataDecl -> List Name
 definedInData (MkPData _ n _ _ cons) = n :: map getName cons
   where

src/Parser/Rule/Common.idr

@@ -16,20 +16,20 @@ EmptyRule token ty = Grammar token False ty
 export
 location : {token : _} -> EmptyRule token (Int, Int)
 location
-    = do tok <- bounds peek
-         pure (tok.startLine, tok.startCol)
+    = do tok <- removeIrrelevance <$> bounds peek
+         pure $ start tok
 
 export
 endLocation : {token : _} -> EmptyRule token (Int, Int)
 endLocation
-    = do tok <- bounds peek
-         pure (tok.endLine, tok.endCol)
+    = do tok <- removeIrrelevance <$> bounds peek
+         pure $ end tok
 
 export
 position : {token : _} -> EmptyRule token ((Int, Int), (Int, Int))
 position
-    = do tok <- bounds peek
-         pure ((tok.startLine, tok.startCol), (tok.endLine, tok.endCol))
+    = do tok <- removeIrrelevance <$> bounds peek
+         pure (start tok, end tok)
 
 
 export

src/TTImp/Interactive/CaseSplit.idr

@@ -334,13 +334,21 @@ mkCase {c} {u} fn orig lhs_raw
          defs <- get Ctxt
          ust <- get UST
          catch
-           (do -- Use 'Rig0' since it might be a type level function, or it might
+           (do 
+               -- Fixes Issue #74. The problem is that if the function is defined in a sub module,
+               -- then the current namespace (accessed by calling getNS) differs from the function
+               -- namespace, therefore it is not considered visible by TTImp.Elab.App.checkVisibleNS
+               setAllPublic True 
+               
+               -- Use 'Rig0' since it might be a type level function, or it might
                -- be an erased name in a case block (which will be bound elsewhere
                -- once split and turned into a pattern)
                (lhs, _) <- elabTerm {c} {m} {u}
                                     fn (InLHS erased) [] (MkNested [])
                                     [] (IBindHere (getFC lhs_raw) PATTERN lhs_raw)
                                     Nothing
+               -- Revert all public back to false
+               setAllPublic False 
                put Ctxt defs -- reset the context, we don't want any updates
                put UST ust
                lhs' <- unelabNoSugar [] lhs

src/TTImp/ProcessDecls.idr

@@ -72,14 +72,22 @@ checkTotalityOK n
     = do defs <- get Ctxt
          Just gdef <- lookupCtxtExact n (gamma defs)
               | Nothing => pure Nothing
+         let fc = location gdef
+
+         -- #524: need to check positivity even if we're not in a total context
+         -- because a definition coming later may need to know it is positive
+         case definition gdef of
+           (TCon _ _ _ _ _ _ _ _) => ignore $ checkPositive fc n
+           _ => pure ()
+
+         -- Once that is done, we build up errors if necessary
          let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
          let tot = totality gdef
-         let fc = location gdef
          log "totality" 3 $ show n ++ " must be: " ++ show treq
          case treq of
-              PartialOK => pure Nothing
-              CoveringOnly => checkCovering fc (isCovering tot)
-              Total => checkTotality fc
+            PartialOK => pure Nothing
+            CoveringOnly => checkCovering fc (isCovering tot)
+            Total => checkTotality fc
   where
     checkCovering : FC -> Covering -> Core (Maybe Error)
     checkCovering fc IsCovering = pure Nothing

src/TTImp/ProcessDef.idr

@@ -107,48 +107,58 @@ recoverable : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
               Defs -> NF vars -> NF vars -> Core Bool
 -- Unlike the above, any mismatch will do
+
+-- TYPE CONSTRUCTORS
 recoverable defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
     = if xn /= yn
          then pure False
          else pure $ not !(anyM (mismatch defs) (zip xargs yargs))
+-- Type constructor vs. primitive type
+recoverable defs (NTCon _ _ _ _ _) (NPrimVal _ _) = pure False
+recoverable defs (NPrimVal _ _) (NTCon _ _ _ _ _) = pure False
+recoverable defs (NTCon _ _ _ _ _) _ = pure True
+
+-- DATA CONSTRUCTORS
 recoverable defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
     = if xt /= yt
          then pure False
          else pure $ not !(anyM (mismatch defs) (zip xargs yargs))
+recoverable defs (NDCon _ _ _ _ _) _ = pure True
+
+-- FUNCTION CALLS
 recoverable defs (NApp _ (NRef _ f) fargs) (NApp _ (NRef _ g) gargs)
     = pure True -- both functions; recoverable
-recoverable defs (NTCon _ _ _ _ _) _ = pure True
-recoverable defs (NDCon _ _ _ _ _) _ = pure True
+
+-- PRIMITIVES
 recoverable defs (NPrimVal _ x) (NPrimVal _ y) = pure (x == y)
-recoverable defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure False
+
+-- OTHERWISE: no
 recoverable defs x y = pure False
 
 export
 recoverableErr : {auto c : Ref Ctxt Defs} ->
                  Defs -> Error -> Core Bool
-recoverableErr defs err@(CantConvert fc env l r)
-    = do logC "declare.def.impossible" 8 (show <$> normaliseErr err)
-         recoverable defs !(nf defs env l)
-                          !(nf defs env r)
-recoverableErr defs err@(CantSolveEq fc env l r)
-    = do logC "declare.def.impossible" 8 (show <$> normaliseErr err)
-         recoverable defs !(nf defs env l)
-                          !(nf defs env r)
-recoverableErr defs err@(BadDotPattern _ _ ErasedArg _ _)
-    = do logC "declare.def.impossible" 8 (show <$> normaliseErr err)
-         pure True
-recoverableErr defs err@(CyclicMeta _ _ _ _)
-    = do logC "declare.def.impossible" 8 (show <$> normaliseErr err)
-         pure True
-recoverableErr defs err@(AllFailed errs)
-    = do logC "declare.def.impossible" 8 (show <$> normaliseErr err)
-         anyM (recoverableErr defs) (map snd errs)
-recoverableErr defs err@(WhenUnifying _ _ _ _ err')
-    = do logC "declare.def.impossible" 8 (show <$> normaliseErr err)
-         recoverableErr defs err'
-recoverableErr defs err
-    = do logC "declare.def.impossible" 8 (show <$> normaliseErr err)
-         pure False
+recoverableErr defs (CantConvert fc env l r)
+  = do l <- nf defs env l
+       r <- nf defs env r
+       log "coverage.recover" 10 $ unlines
+         [ "Recovering from CantConvert?"
+         , "Checking:"
+         , "  " ++ show l
+         , "  " ++ show r
+         ]
+       recoverable defs l r
+
+recoverableErr defs (CantSolveEq fc env l r)
+    = recoverable defs !(nf defs env l)
+                       !(nf defs env r)
+recoverableErr defs (BadDotPattern _ _ ErasedArg _ _) = pure True
+recoverableErr defs (CyclicMeta _ _ _ _) = pure True
+recoverableErr defs (AllFailed errs)
+    = anyM (recoverableErr defs) (map snd errs)
+recoverableErr defs (WhenUnifying _ _ _ _ err)
+    = recoverableErr defs err
+recoverableErr defs _ = pure False
 
 -- Given a type checked LHS and its type, return the environment in which we
 -- should check the RHS, the LHS and its type in that environment,
@@ -815,29 +825,24 @@ processDef opts nest env fc n_in cs_in
                    autoimp <- isUnboundImplicits
                    setUnboundImplicits True
                    (_, lhstm) <- bindNames False itm
-                   log "declare.def.impossible" 5 $ "Pre elab: " ++ show lhstm
                    setUnboundImplicits autoimp
                    (lhstm, _) <- elabTerm n (InLHS mult) [] (MkNested []) []
                                     (IBindHere fc PATTERN lhstm) Nothing
-                   logC "declare.def.impossible" 5 $ ("Post elab: " ++) . show <$> toFullNames lhstm
                    defs <- get Ctxt
                    lhs <- normaliseHoles defs [] lhstm
-                   logC "declare.def.impossible" 5 $ ("Normalised: " ++) . show <$> toFullNames lhs
                    if !(hasEmptyPat defs [] lhs)
-                      then do put Ctxt ctxt
-                              log "declare.def.impossible" 3 "Impossible due to incompatible patterns"
+                      then do log "declare.def.impossible" 5 "No empty pat"
+                              put Ctxt ctxt
                               pure Nothing
-                      else do empty <- clearDefs ctxt
+                      else do log "declare.def.impossible" 5 "Some empty pat"
+                              empty <- clearDefs ctxt
                               rtm <- closeEnv empty !(nf empty [] lhs)
                               put Ctxt ctxt
-                              log "declare.def.impossible" 3 "Possible case: compatible patterns"
                               pure (Just rtm))
                (\err => do defs <- get Ctxt
                            if not !(recoverableErr defs err)
-                              then do log "declare.def.impossible" 3 "Impossible due to unrecoverable error"
-                                      pure Nothing
-                              else do log "declare.def.impossible" 3 "Possible case: recoverable error"
-                                      pure (Just tm))
+                              then pure Nothing
+                              else pure (Just tm))
       where
         closeEnv : Defs -> NF [] -> Core ClosedTerm
         closeEnv defs (NBind _ x (PVar _ _ _ _) sc)

src/Text/Bounded.idr

@@ -46,6 +46,10 @@ export
 irrelevantBounds : ty -> WithBounds ty
 irrelevantBounds x = MkBounded x True (-1) (-1) (-1) (-1)
 
+export
+removeIrrelevance : WithBounds ty -> WithBounds ty
+removeIrrelevance (MkBounded val ir sl sc el ec) = MkBounded val True sl sc el ec
+
 export
 mergeBounds : WithBounds ty -> WithBounds ty' -> WithBounds ty'
 mergeBounds (MkBounded _ True _ _ _ _) (MkBounded val True _ _ _ _) = irrelevantBounds val

src/Text/Literate.idr

@@ -64,11 +64,11 @@ rawTokens delims ls =
 ||| Merge the tokens into a single source file.
 reduce : List (WithBounds Token) -> List String -> String
 reduce [] acc = fastAppend (reverse acc)
-reduce (MkBounded (Any x) _ _ _ _ _ :: rest) acc = reduce rest (blank_content::acc)
-  where
-    -- Preserve the original document's line count.
-    blank_content : String
-    blank_content = fastAppend (replicate (length (lines x)) "\n")
+reduce (MkBounded (Any x) _ _ _ _ _ :: rest) acc = 
+  -- newline will always be tokenized as a single token
+  if x == "\n"
+  then reduce rest ("\n"::acc)
+  else reduce rest acc
 
 reduce (MkBounded (CodeLine m src) _ _ _ _ _ :: rest) acc =
     if m == trim src
@@ -83,7 +83,8 @@ reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc with (lines src) --
   reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: ys) with (snocList ys)
     reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
     reduce (MkBounded (CodeBlock l r src) _ _ _ _ _ :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
-        reduce rest ("\n" :: unlines srcs :: acc)
+        -- the "\n" counts for the open deliminator; the closing deliminator should always be followed by a (Any "\n"), so we don't add a newline
+        reduce rest (unlines srcs :: "\n" :: acc)
 
 -- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.
 

src/Text/Parser/Core.idr

@@ -240,7 +240,7 @@ mutual
   doParse com (NextIs err f) [] = Failure com False "End of input" []
   doParse com (NextIs err f) (x :: xs)
         = if f x
-             then Res com x (x :: xs)
+             then Res com (removeIrrelevance x) (x :: xs)
              else Failure com False err (x :: xs)
   doParse com (Alt {c1} {c2} x y) xs
       = case doParse False x xs of

support/refc/Makefile

@@ -0,0 +1,49 @@
+include ../../config.mk
+
+TARGET = libidris2_refc
+
+LIBTARGET = $(TARGET).a
+
+CFLAGS += -O2
+
+SRCS = $(wildcard *.c)
+ifeq ($(OS), windows)
+	LDFLAGS += -lws2_32
+ifeq ($(OLD_WIN), 1)
+	CFLAGS += -D_OLD_WIN
+endif
+endif
+OBJS = $(SRCS:.c=.o)
+DEPS = $(OBJS:.o=.d)
+
+
+all: build
+
+.PHONY: build
+
+build: $(LIBTARGET)
+
+$(LIBTARGET): $(OBJS)
+	$(AR) rc $@ $^
+	$(RANLIB) $@
+
+-include $(DEPS)
+
+%.d: %.c
+	@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@
+
+
+.PHONY: clean
+
+clean:
+	$(RM) $(OBJS) $(LIBTARGET)
+
+cleandep: clean
+	$(RM) $(DEPS)
+
+
+.PHONY: install
+
+install: build
+	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/refc
+	install $(LIBTARGET) *.h ${PREFIX}/idris2-${IDRIS2_VERSION}/refc

support/refc/cBackend.h

@@ -0,0 +1,17 @@
+#ifndef __C_BACKEND_H__
+#define __C_BACKEND_H__
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <pthread.h>
+
+#include "datatypes.h"
+#include "memoryManagement.h"
+#include "mathFunctions.h"
+#include "runtime.h"
+#include "stringOps.h"
+#include "casts.h"
+#include "conCaseHelper.h"
+#include "prim.h"
+
+#endif

support/refc/casts.c

@@ -0,0 +1,644 @@
+#include "casts.h"
+#include <inttypes.h>
+
+Value *cast_i32_to_Bits8(Value *input)
+{
+	Value_Int8 *retVal = (Value_Int8 *)newValue();
+	retVal->header.tag = INT8_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->i8 = (int8_t)from->i32;
+
+	return (Value *)retVal;
+}
+
+Value *cast_i32_to_Bits16(Value *input)
+{
+	Value_Int16 *retVal = (Value_Int16 *)newValue();
+	retVal->header.tag = INT16_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->i16 = (int16_t)from->i32;
+
+	return (Value *)retVal;
+}
+Value *cast_i32_to_Bits32(Value *input)
+{
+	return input;
+}
+Value *cast_i32_to_Bits64(Value *input)
+{
+	return cast_i32_to_i64(input);
+}
+
+Value *cast_i32_to_i64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->i64 = (int64_t)from->i32;
+
+	return (Value *)retVal;
+}
+
+Value *cast_i32_to_double(Value *input)
+{
+	Value_Double *retVal = (Value_Double *)newValue();
+	retVal->header.tag = DOUBLE_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->d = (double)from->i32;
+
+	return (Value *)retVal;
+}
+
+Value *cast_i32_to_char(Value *input)
+{
+	Value_Char *retVal = (Value_Char *)newValue();
+	retVal->header.tag = CHAR_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->c = (char)from->i32;
+
+	return (Value *)retVal;
+}
+
+Value *cast_i32_to_string(Value *input)
+{
+	Value_String *retVal = (Value_String *)newValue();
+	retVal->header.tag = STRING_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	int l = snprintf(NULL, 0, "%i", from->i32);
+	retVal->str = malloc((l + 1) * sizeof(char));
+	memset(retVal->str, 0, l + 1);
+	sprintf(retVal->str, "%i", from->i32);
+
+	return (Value *)retVal;
+}
+
+Value *cast_i64_to_Bits8(Value *input)
+{
+	Value_Int8 *retVal = (Value_Int8 *)newValue();
+	retVal->header.tag = INT8_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->i8 = (int8_t)from->i64;
+
+	return (Value *)retVal;
+}
+Value *cast_i64_to_Bits16(Value *input)
+{
+	Value_Int16 *retVal = (Value_Int16 *)newValue();
+	retVal->header.tag = INT16_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->i16 = (int16_t)from->i64;
+
+	return (Value *)retVal;
+}
+Value *cast_i64_to_Bits32(Value *input)
+{
+	return cast_i64_to_i32(input);
+}
+
+Value *cast_i64_to_Bits64(Value *input)
+{
+	return input;
+}
+
+Value *cast_i64_to_i32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->i32 = (int32_t)from->i64;
+
+	return (Value *)retVal;
+}
+
+Value *cast_i64_to_double(Value *input)
+{
+	Value_Double *retVal = (Value_Double *)newValue();
+	retVal->header.tag = DOUBLE_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->d = (double)from->i64;
+
+	return (Value *)retVal;
+}
+
+Value *cast_i64_to_char(Value *input)
+{
+	Value_Char *retVal = (Value_Char *)newValue();
+	retVal->header.tag = CHAR_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->c = (char)from->i64;
+
+	return (Value *)retVal;
+}
+
+Value *cast_i64_to_string(Value *input)
+{
+	Value_String *retVal = (Value_String *)newValue();
+	retVal->header.tag = STRING_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	int l = snprintf(NULL, 0, "%" PRIu64 "", from->i64);
+	retVal->str = malloc((l + 1) * sizeof(char));
+	memset(retVal->str, 0, l + 1);
+	sprintf(retVal->str, "%" PRIu64 "", from->i64);
+
+	return (Value *)retVal;
+}
+
+Value *cast_double_to_Bits8(Value *input)
+{
+	Value_Int8 *retVal = (Value_Int8 *)newValue();
+	retVal->header.tag = INT8_TAG;
+	Value_Double *from = (Value_Double *)input;
+	retVal->i8 = (int8_t)from->d;
+
+	return (Value *)retVal;
+}
+Value *cast_double_to_Bits16(Value *input)
+{
+	Value_Int16 *retVal = (Value_Int16 *)newValue();
+	retVal->header.tag = INT16_TAG;
+	Value_Double *from = (Value_Double *)input;
+	retVal->i16 = (int16_t)from->d;
+
+	return (Value *)retVal;
+}
+Value *cast_double_to_Bits32(Value *input)
+{
+	return cast_double_to_i32(input);
+}
+Value *cast_double_to_Bits64(Value *input)
+{
+	return cast_double_to_i64(input);
+}
+Value *cast_double_to_i32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Double *from = (Value_Double *)input;
+	retVal->i32 = (int32_t)from->d;
+
+	return (Value *)retVal;
+}
+
+Value *cast_double_to_i64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Double *from = (Value_Double *)input;
+	retVal->i64 = (int64_t)from->d;
+
+	return (Value *)retVal;
+}
+
+Value *cast_double_to_char(Value *input)
+{
+	Value_Char *retVal = (Value_Char *)newValue();
+	retVal->header.tag = CHAR_TAG;
+	Value_Double *from = (Value_Double *)input;
+	retVal->c = (char)from->d;
+
+	return (Value *)retVal;
+}
+
+Value *cast_double_to_string(Value *input)
+{
+	Value_String *retVal = (Value_String *)newValue();
+	retVal->header.tag = STRING_TAG;
+	Value_Double *from = (Value_Double *)input;
+	int l = snprintf(NULL, 0, "%f", from->d);
+	retVal->str = malloc((l + 1) * sizeof(char));
+	memset(retVal->str, 0, l + 1);
+	sprintf(retVal->str, "%f", from->d);
+
+	return (Value *)retVal;
+}
+
+Value *cast_char_to_Bits8(Value *input)
+{
+	Value_Int8 *retVal = (Value_Int8 *)newValue();
+	retVal->header.tag = INT8_TAG;
+	Value_Char *from = (Value_Char *)input;
+	retVal->i8 = (int8_t)from->c;
+
+	return (Value *)retVal;
+}
+Value *cast_char_to_Bits16(Value *input)
+{
+	Value_Int16 *retVal = (Value_Int16 *)newValue();
+	retVal->header.tag = INT16_TAG;
+	Value_Char *from = (Value_Char *)input;
+	retVal->i16 = (int16_t)from->c;
+
+	return (Value *)retVal;
+}
+Value *cast_char_to_Bits32(Value *input)
+{
+	return cast_char_to_i32(input);
+}
+Value *cast_char_to_Bits64(Value *input)
+{
+	return cast_char_to_i64(input);
+}
+Value *cast_char_to_i32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Char *from = (Value_Char *)input;
+	retVal->i32 = (int32_t)from->c;
+
+	return (Value *)retVal;
+}
+
+Value *cast_char_to_i64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Char *from = (Value_Char *)input;
+	retVal->i64 = (int64_t)from->c;
+
+	return (Value *)retVal;
+}
+
+Value *cast_char_to_double(Value *input)
+{
+	Value_Double *retVal = (Value_Double *)newValue();
+	retVal->header.tag = DOUBLE_TAG;
+	Value_Char *from = (Value_Char *)input;
+	retVal->d = (double)from->c;
+
+	return (Value *)retVal;
+}
+
+Value *cast_char_to_string(Value *input)
+{
+	Value_String *retVal = (Value_String *)newValue();
+	retVal->header.tag = STRING_TAG;
+	Value_Char *from = (Value_Char *)input;
+	retVal->str = malloc(2 * sizeof(char));
+	memset(retVal->str, 0, 2);
+	retVal->str[0] = from->c;
+
+	return (Value *)retVal;
+}
+
+Value *cast_string_to_Bits8(Value *input)
+{
+	Value_Int8 *retVal = (Value_Int8 *)newValue();
+	retVal->header.tag = INT8_TAG;
+	Value_String *from = (Value_String *)input;
+	retVal->i8 = (uint8_t)atoi(from->str);
+
+	return (Value *)retVal;
+}
+Value *cast_string_to_Bits16(Value *input)
+{
+	Value_Int16 *retVal = (Value_Int16 *)newValue();
+	retVal->header.tag = INT16_TAG;
+	Value_String *from = (Value_String *)input;
+	retVal->i16 = (uint16_t)atoi(from->str);
+
+	return (Value *)retVal;
+}
+Value *cast_string_to_Bits32(Value *input)
+{
+	return cast_string_to_i32(input);
+}
+Value *cast_string_to_Bits64(Value *input)
+{
+	return cast_string_to_i64(input);
+}
+Value *cast_string_to_i32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_String *from = (Value_String *)input;
+	retVal->i32 = atoi(from->str);
+
+	return (Value *)retVal;
+}
+
+Value *cast_string_to_i64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_String *from = (Value_String *)input;
+	retVal->i64 = atoi(from->str);
+
+	return (Value *)retVal;
+}
+
+Value *cast_string_to_double(Value *input)
+{
+	Value_Double *retVal = (Value_Double *)newValue();
+	retVal->header.tag = DOUBLE_TAG;
+	Value_String *from = (Value_String *)input;
+	retVal->d = atof(from->str);
+
+	return (Value *)retVal;
+}
+
+Value *cast_string_to_char(Value *input)
+{
+	Value_Char *retVal = (Value_Char *)newValue();
+	retVal->header.tag = CHAR_TAG;
+	Value_String *from = (Value_String *)input;
+	retVal->c = from->str[0];
+
+	return (Value *)retVal;
+}
+
+// Bits cast
+// autogenerated using Ruby
+
+/*  conversions from Bits8  */
+Value *cast_Bits8_to_Bits16(Value *input)
+{
+	Value_Int16 *retVal = (Value_Int16 *)newValue();
+	retVal->header.tag = INT16_TAG;
+	Value_Int8 *from = (Value_Int8 *)input;
+	retVal->i16 = (int16_t)from->i8;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits8_to_Bits32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Int8 *from = (Value_Int8 *)input;
+	retVal->i32 = (int32_t)from->i8;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits8_to_Bits64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Int8 *from = (Value_Int8 *)input;
+	retVal->i64 = (int64_t)from->i8;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits8_to_i32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Int8 *from = (Value_Int8 *)input;
+	retVal->i32 = (int32_t)from->i8;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits8_to_i64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Int8 *from = (Value_Int8 *)input;
+	retVal->i64 = (int64_t)from->i8;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits8_to_double(Value *input)
+{
+	Value_Double *retVal = (Value_Double *)newValue();
+	retVal->header.tag = DOUBLE_TAG;
+	Value_Int8 *from = (Value_Int8 *)input;
+	retVal->d = (double)from->i8;
+
+	return (Value *)retVal;
+}
+
+Value *cast_Bits8_to_char(Value *input)
+{
+	Value_Char *retVal = (Value_Char *)newValue();
+	retVal->header.tag = CHAR_TAG;
+	Value_Int8 *from = (Value_Int8 *)input;
+	retVal->c = (char)from->i8;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits8_to_string(Value *input)
+{
+	Value_String *retVal = (Value_String *)newValue();
+	retVal->header.tag = STRING_TAG;
+	Value_Int8 *from = (Value_Int8 *)input;
+	int l = snprintf(NULL, 0, "%" PRIu8 "", from->i8);
+	retVal->str = malloc((l + 1) * sizeof(char));
+	memset(retVal->str, 0, l + 1);
+	sprintf(retVal->str, "%" PRIu8 "", from->i8);
+
+	return (Value *)retVal;
+}
+
+/*  conversions from Bits16  */
+Value *cast_Bits16_to_Bits8(Value *input)
+{
+	Value_Int8 *retVal = (Value_Int8 *)newValue();
+	retVal->header.tag = INT8_TAG;
+	Value_Int16 *from = (Value_Int16 *)input;
+	retVal->i8 = (int8_t)from->i16;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits16_to_Bits32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Int16 *from = (Value_Int16 *)input;
+	retVal->i32 = (int32_t)from->i16;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits16_to_Bits64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Int16 *from = (Value_Int16 *)input;
+	retVal->i64 = (int64_t)from->i16;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits16_to_i32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Int16 *from = (Value_Int16 *)input;
+	retVal->i32 = (int32_t)from->i16;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits16_to_i64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Int16 *from = (Value_Int16 *)input;
+	retVal->i64 = (int64_t)from->i16;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits16_to_double(Value *input)
+{
+	Value_Double *retVal = (Value_Double *)newValue();
+	retVal->header.tag = DOUBLE_TAG;
+	Value_Int16 *from = (Value_Int16 *)input;
+	retVal->d = (double)from->i16;
+
+	return (Value *)retVal;
+}
+
+Value *cast_Bits16_to_char(Value *input)
+{
+	Value_Char *retVal = (Value_Char *)newValue();
+	retVal->header.tag = CHAR_TAG;
+	Value_Int16 *from = (Value_Int16 *)input;
+	retVal->c = (char)from->i16;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits16_to_string(Value *input)
+{
+	Value_String *retVal = (Value_String *)newValue();
+	retVal->header.tag = STRING_TAG;
+	Value_Int16 *from = (Value_Int16 *)input;
+	int l = snprintf(NULL, 0, "%" PRIu16 "", from->i16);
+	retVal->str = malloc((l + 1) * sizeof(char));
+	memset(retVal->str, 0, l + 1);
+	sprintf(retVal->str, "%" PRIu16 "", from->i16);
+
+	return (Value *)retVal;
+}
+
+/*  conversions from Bits32  */
+Value *cast_Bits32_to_Bits8(Value *input)
+{
+	Value_Int8 *retVal = (Value_Int8 *)newValue();
+	retVal->header.tag = INT8_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->i8 = (int8_t)from->i32;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits32_to_Bits16(Value *input)
+{
+	Value_Int16 *retVal = (Value_Int16 *)newValue();
+	retVal->header.tag = INT16_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->i16 = (int16_t)from->i32;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits32_to_Bits64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->i64 = (int64_t)from->i32;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits32_to_i32(Value *input)
+{
+	return input;
+}
+Value *cast_Bits32_to_i64(Value *input)
+{
+	Value_Int64 *retVal = (Value_Int64 *)newValue();
+	retVal->header.tag = INT64_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->i64 = (int64_t)from->i32;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits32_to_double(Value *input)
+{
+	Value_Double *retVal = (Value_Double *)newValue();
+	retVal->header.tag = DOUBLE_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->d = (double)from->i32;
+
+	return (Value *)retVal;
+}
+
+Value *cast_Bits32_to_char(Value *input)
+{
+	Value_Char *retVal = (Value_Char *)newValue();
+	retVal->header.tag = CHAR_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	retVal->c = (char)from->i32;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits32_to_string(Value *input)
+{
+	Value_String *retVal = (Value_String *)newValue();
+	retVal->header.tag = STRING_TAG;
+	Value_Int32 *from = (Value_Int32 *)input;
+	int l = snprintf(NULL, 0, "%" PRIu32 "", (uint32_t)from->i32);
+	retVal->str = malloc((l + 1) * sizeof(char));
+	memset(retVal->str, 0, l + 1);
+	sprintf(retVal->str, "%" PRIu32 "", (uint32_t)from->i32);
+
+	return (Value *)retVal;
+}
+
+/*  conversions from Bits64  */
+Value *cast_Bits64_to_Bits8(Value *input)
+{
+	Value_Int8 *retVal = (Value_Int8 *)newValue();
+	retVal->header.tag = INT8_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->i8 = (int8_t)from->i64;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits64_to_Bits16(Value *input)
+{
+	Value_Int16 *retVal = (Value_Int16 *)newValue();
+	retVal->header.tag = INT16_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->i16 = (int16_t)from->i64;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits64_to_Bits32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->i32 = (int32_t)from->i64;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits64_to_i32(Value *input)
+{
+	Value_Int32 *retVal = (Value_Int32 *)newValue();
+	retVal->header.tag = INT32_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->i32 = (int32_t)from->i64;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits64_to_i64(Value *input)
+{
+	return input;
+}
+Value *cast_Bits64_to_double(Value *input)
+{
+	Value_Double *retVal = (Value_Double *)newValue();
+	retVal->header.tag = DOUBLE_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->d = (double)from->i64;
+
+	return (Value *)retVal;
+}
+
+Value *cast_Bits64_to_char(Value *input)
+{
+	Value_Char *retVal = (Value_Char *)newValue();
+	retVal->header.tag = CHAR_TAG;
+	Value_Int64 *from = (Value_Int64 *)input;
+	retVal->c = (char)from->i64;
+
+	return (Value *)retVal;
+}
+Value *cast_Bits64_to_string(Value *input)
+{
+	return cast_i64_to_string(input);
+}

support/refc/casts.h

@@ -0,0 +1,85 @@
+#ifndef __CASTS_H__
+#define __CASTS_H__
+
+#include "cBackend.h"
+#include <stdio.h>
+
+Value *cast_i32_to_Bits8(Value *);
+Value *cast_i32_to_Bits16(Value *);
+Value *cast_i32_to_Bits32(Value *);
+Value *cast_i32_to_Bits64(Value *);
+Value *cast_i32_to_i64(Value *);
+Value *cast_i32_to_double(Value *);
+Value *cast_i32_to_char(Value *);
+Value *cast_i32_to_string(Value *);
+
+Value *cast_i64_to_Bits8(Value *);
+Value *cast_i64_to_Bits16(Value *);
+Value *cast_i64_to_Bits32(Value *);
+Value *cast_i64_to_Bits64(Value *);
+Value *cast_i64_to_i32(Value *);
+Value *cast_i64_to_double(Value *);
+Value *cast_i64_to_char(Value *);
+Value *cast_i64_to_string(Value *);
+
+Value *cast_double_to_Bits8(Value *);
+Value *cast_double_to_Bits16(Value *);
+Value *cast_double_to_Bits32(Value *);
+Value *cast_double_to_Bits64(Value *);
+Value *cast_double_to_i32(Value *);
+Value *cast_double_to_i64(Value *);
+Value *cast_double_to_char(Value *);
+Value *cast_double_to_string(Value *);
+
+Value *cast_char_to_Bits8(Value *);
+Value *cast_char_to_Bits16(Value *);
+Value *cast_char_to_Bits32(Value *);
+Value *cast_char_to_Bits64(Value *);
+Value *cast_char_to_i32(Value *);
+Value *cast_char_to_i64(Value *);
+Value *cast_char_to_double(Value *);
+Value *cast_char_to_string(Value *);
+
+Value *cast_string_to_Bits8(Value *);
+Value *cast_string_to_Bits16(Value *);
+Value *cast_string_to_Bits32(Value *);
+Value *cast_string_to_Bits64(Value *);
+Value *cast_string_to_i32(Value *);
+Value *cast_string_to_i64(Value *);
+Value *cast_string_to_double(Value *);
+Value *cast_string_to_char(Value *);
+
+Value *cast_Bits8_to_Bits16(Value *input);
+Value *cast_Bits8_to_Bits32(Value *input);
+Value *cast_Bits8_to_Bits64(Value *input);
+Value *cast_Bits8_to_i32(Value *input);
+Value *cast_Bits8_to_i64(Value *input);
+Value *cast_Bits8_to_double(Value *input);
+Value *cast_Bits8_to_char(Value *input);
+Value *cast_Bits8_to_string(Value *input);
+Value *cast_Bits16_to_Bits8(Value *input);
+Value *cast_Bits16_to_Bits32(Value *input);
+Value *cast_Bits16_to_Bits64(Value *input);
+Value *cast_Bits16_to_i32(Value *input);
+Value *cast_Bits16_to_i64(Value *input);
+Value *cast_Bits16_to_double(Value *input);
+Value *cast_Bits16_to_char(Value *input);
+Value *cast_Bits16_to_string(Value *input);
+Value *cast_Bits32_to_Bits8(Value *input);
+Value *cast_Bits32_to_Bits16(Value *input);
+Value *cast_Bits32_to_Bits64(Value *input);
+Value *cast_Bits32_to_i32(Value *input);
+Value *cast_Bits32_to_i64(Value *input);
+Value *cast_Bits32_to_double(Value *input);
+Value *cast_Bits32_to_char(Value *input);
+Value *cast_Bits32_to_string(Value *input);
+Value *cast_Bits64_to_Bits8(Value *input);
+Value *cast_Bits64_to_Bits16(Value *input);
+Value *cast_Bits64_to_Bits32(Value *input);
+Value *cast_Bits64_to_i32(Value *input);
+Value *cast_Bits64_to_i64(Value *input);
+Value *cast_Bits64_to_double(Value *input);
+Value *cast_Bits64_to_char(Value *input);
+Value *cast_Bits64_to_string(Value *input);
+
+#endif

support/refc/conCaseHelper.c

@@ -0,0 +1,75 @@
+#include "conCaseHelper.h"
+
+AConAlt *newConstructorField(int nr)
+{
+    AConAlt *retVal = (AConAlt *)malloc(nr * sizeof(AConAlt));
+    for (int i = 0; i < nr; i++)
+    {
+        retVal[i].tag = -1;
+    }
+    return retVal;
+}
+
+void freeConstructorField(AConAlt *cf)
+{
+    free(cf);
+}
+
+void constructorFieldFNextEntry(AConAlt *field, char *name, int tag)
+{
+    AConAlt *nextEntry = field;
+    while (nextEntry->tag == -1)
+    {
+        nextEntry++;
+    }
+    nextEntry->name = name;
+    nextEntry->tag = tag;
+}
+
+int compareConstructors(Value *sc, AConAlt *field, int nr)
+{
+    Value_Constructor *constr = (Value_Constructor *)sc;
+    for (int i = 0; i < nr; i++)
+    {
+        if (field->name) //decide my name
+        {
+            if (!strcmp(field->name, constr->name))
+            {
+                return i;
+            }
+        }
+        else // decide by tag
+        {
+            if (field->tag == constr->tag)
+            {
+                return i;
+            }
+        }
+        field++;
+    }
+    return -1;
+}
+
+int multiStringCompare(Value *sc, int nrDecicionOptions, char **options)
+{
+    for (int i = 0; i < nrDecicionOptions; i++)
+    {
+        if (!strcmp(((Value_String *)sc)->str, options[i]))
+        {
+            return i;
+        }
+    }
+    return -1;
+}
+
+int multiDoubleCompare(Value *sc, int nrDecicionOptions, double *options)
+{
+    for (int i = 0; i < nrDecicionOptions; i++)
+    {
+        if (((Value_Double *)sc)->d == options[i])
+        {
+            return i;
+        }
+    }
+    return -1;
+}

support/refc/conCaseHelper.h

@@ -0,0 +1,20 @@
+#ifndef __CON_CASE_HELPER_H__
+#define __CON_CASE_HELPER_H__
+
+#include "cBackend.h"
+
+typedef struct
+{
+    char *name;
+    int tag;
+} AConAlt;
+
+AConAlt *newConstructorField(int);
+int compareConstructors(Value *, AConAlt *, int);
+void constructorFieldFNextEntry(AConAlt *, char *, int);
+void freeConstructorField(AConAlt *);
+
+int multiStringCompare(Value *, int, char **);
+int multiDoubleCompare(Value *, int, double *);
+
+#endif

support/refc/datatypes.h

@@ -0,0 +1,172 @@
+#ifndef __DATATYPES_H__
+#define __DATATYPES_H__
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <pthread.h>
+#include <stdint.h>
+
+#define NO_TAG 0
+#define INT8_TAG 1
+#define INT16_TAG 2
+#define INT32_TAG 3
+#define INT64_TAG 4
+#define DOUBLE_TAG 5
+#define CHAR_TAG 6
+#define STRING_TAG 7
+
+#define CLOSURE_TAG 10
+#define ARGLIST_TAG 11
+#define CONSTRUCTOR_TAG 12
+
+#define IOREF_TAG 20
+#define ARRAY_TAG 21
+#define POINTER_TAG 22
+#define GC_POINTER_TAG 23
+#define BUFFER_TAG 24
+
+#define MUTEX_TAG 30
+#define CONDITION_TAG 31
+
+#define COMPLETE_CLOSURE_TAG 98 // for trampoline tail recursion handling
+#define WORLD_TAG 99
+
+typedef struct
+{
+    int refCounter;
+    int tag;
+} Value_header;
+
+typedef struct
+{
+    Value_header header;
+    char payload[25];
+} Value;
+
+typedef struct
+{
+    Value_header header;
+    uint8_t i8;
+} Value_Int8;
+
+typedef struct
+{
+    Value_header header;
+    uint16_t i16;
+} Value_Int16;
+
+typedef struct
+{
+    Value_header header;
+    int32_t i32;
+} Value_Int32;
+
+typedef struct
+{
+    Value_header header;
+    int64_t i64;
+} Value_Int64;
+
+typedef struct
+{
+    Value_header header;
+    double d;
+} Value_Double;
+
+typedef struct
+{
+    Value_header header;
+    char c;
+} Value_Char;
+
+typedef struct
+{
+    Value_header header;
+    char *str;
+} Value_String;
+
+typedef struct
+{
+    Value_header header;
+    int32_t total;
+    int32_t tag;
+    char *name;
+    Value **args;
+} Value_Constructor;
+
+typedef struct
+{
+    Value_header header;
+    int32_t total;
+    int32_t filled;
+    Value **args;
+} Value_Arglist;
+
+typedef Value *(*fun_ptr_t)(Value_Arglist *);
+
+typedef struct
+{
+    Value_header header;
+    fun_ptr_t f;
+    Value_Arglist *arglist;
+} Value_Closure;
+
+typedef struct
+{
+    Value_header header;
+    int32_t index;
+} Value_IORef;
+
+typedef struct
+{
+    Value_header header;
+    void *p;
+} Value_Pointer;
+
+typedef struct
+{
+    Value_header header;
+    Value_Pointer *p;
+    Value_Closure *onCollectFct;
+} Value_GCPointer;
+
+typedef struct
+{
+    Value_header header;
+    int capacity;
+    Value **arr;
+} Value_Array;
+
+typedef struct
+{
+    Value_header header;
+    size_t len;
+    char *buffer;
+} Value_Buffer;
+
+typedef struct
+{
+    Value_header header;
+    pthread_mutex_t *mutex;
+} Value_Mutex;
+
+typedef struct
+{
+    Value_header header;
+    pthread_cond_t *cond;
+} Value_Condition;
+
+typedef struct
+{
+    Value **refs;
+    int filled;
+    int total;
+} IORef_Storage;
+
+typedef struct
+{
+    Value_header header;
+    IORef_Storage *listIORefs;
+} Value_World;
+
+#endif

support/refc/mathFunctions.c

@@ -0,0 +1,370 @@
+#include "mathFunctions.h"
+#include "runtime.h"
+#include "memoryManagement.h"
+
+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)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 + ((Value_Int32 *)y)->i32);
+}
+Value *add_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 + ((Value_Int64 *)y)->i64);
+}
+Value *add_double(Value *x, Value *y)
+{
+    return (Value *)makeDouble(((Value_Double *)x)->d + ((Value_Double *)y)->d);
+}
+
+/* sub */
+Value *sub_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 - ((Value_Int32 *)y)->i32);
+}
+Value *sub_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 - ((Value_Int64 *)y)->i64);
+}
+Value *sub_double(Value *x, Value *y)
+{
+    return (Value *)makeDouble(((Value_Double *)x)->d - ((Value_Double *)y)->d);
+}
+
+/* mul */
+Value *mul_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 * ((Value_Int32 *)y)->i32);
+}
+Value *mul_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 * ((Value_Int64 *)y)->i64);
+}
+Value *mul_double(Value *x, Value *y)
+{
+    return (Value *)makeDouble(((Value_Double *)x)->d * ((Value_Double *)y)->d);
+}
+
+/* div */
+Value *div_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 / ((Value_Int32 *)y)->i32);
+}
+Value *div_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 / ((Value_Int64 *)y)->i64);
+}
+Value *div_double(Value *x, Value *y)
+{
+    return (Value *)makeDouble(((Value_Double *)x)->d / ((Value_Double *)y)->d);
+}
+
+/* mod */
+Value *mod_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 % ((Value_Int32 *)y)->i32);
+}
+Value *mod_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 % ((Value_Int64 *)y)->i64);
+}
+
+/* shiftl */
+Value *shiftl_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 << ((Value_Int32 *)y)->i32);
+}
+Value *shiftl_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 << ((Value_Int64 *)y)->i64);
+}
+
+/* shiftr */
+Value *shiftr_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 >> ((Value_Int32 *)y)->i32);
+}
+Value *shiftr_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 >> ((Value_Int64 *)y)->i64);
+}
+
+/* and */
+Value *and_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 & ((Value_Int32 *)y)->i32);
+}
+Value *and_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 & ((Value_Int64 *)y)->i64);
+}
+
+/* or */
+Value *or_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 | ((Value_Int32 *)y)->i32);
+}
+Value *or_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 | ((Value_Int64 *)y)->i64);
+}
+
+/* xor */
+Value *xor_i32(Value *x, Value *y)
+{
+    return (Value *)makeInt32(((Value_Int32 *)x)->i32 ^ ((Value_Int32 *)y)->i32);
+}
+Value *xor_i64(Value *x, Value *y)
+{
+    return (Value *)makeInt64(((Value_Int64 *)x)->i64 ^ ((Value_Int64 *)y)->i64);
+}
+
+/* lt */
+Value *lt_i32(Value *x, Value *y)
+{
+    if (((Value_Int32 *)x)->i32 < ((Value_Int32 *)y)->i32)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *lt_i64(Value *x, Value *y)
+{
+    if (((Value_Int64 *)x)->i64 < ((Value_Int64 *)y)->i64)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *lt_double(Value *x, Value *y)
+{
+    if (((Value_Double *)x)->d < ((Value_Double *)y)->d)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *lt_char(Value *x, Value *y)
+{
+    if (((Value_Char *)x)->c < ((Value_Char *)y)->c)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+
+/* gt */
+Value *gt_i32(Value *x, Value *y)
+{
+    if (((Value_Int32 *)x)->i32 > ((Value_Int32 *)y)->i32)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *gt_i64(Value *x, Value *y)
+{
+    if (((Value_Int64 *)x)->i64 > ((Value_Int64 *)y)->i64)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *gt_double(Value *x, Value *y)
+{
+    if (((Value_Double *)x)->d > ((Value_Double *)y)->d)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *gt_char(Value *x, Value *y)
+{
+    if (((Value_Char *)x)->c > ((Value_Char *)y)->c)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+
+/* eq */
+Value *eq_i32(Value *x, Value *y)
+{
+    if (((Value_Int32 *)x)->i32 == ((Value_Int32 *)y)->i32)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *eq_i64(Value *x, Value *y)
+{
+    if (((Value_Int64 *)x)->i64 == ((Value_Int64 *)y)->i64)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *eq_double(Value *x, Value *y)
+{
+    if (((Value_Double *)x)->d == ((Value_Double *)y)->d)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *eq_char(Value *x, Value *y)
+{
+    if (((Value_Char *)x)->c == ((Value_Char *)y)->c)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *eq_string(Value *x, Value *y)
+{
+    if (!strcmp(((Value_String *)x)->str, ((Value_String *)y)->str))
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+
+/* lte */
+Value *lte_i32(Value *x, Value *y)
+{
+    if (((Value_Int32 *)x)->i32 <= ((Value_Int32 *)y)->i32)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *lte_i64(Value *x, Value *y)
+{
+    if (((Value_Int64 *)x)->i64 <= ((Value_Int64 *)y)->i64)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *lte_double(Value *x, Value *y)
+{
+    if (((Value_Double *)x)->d <= ((Value_Double *)y)->d)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *lte_char(Value *x, Value *y)
+{
+    if (((Value_Char *)x)->c <= ((Value_Char *)y)->c)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+
+/* gte */
+Value *gte_i32(Value *x, Value *y)
+{
+    if (((Value_Int32 *)x)->i32 >= ((Value_Int32 *)y)->i32)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *gte_i64(Value *x, Value *y)
+{
+    if (((Value_Int64 *)x)->i64 >= ((Value_Int64 *)y)->i64)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *gte_double(Value *x, Value *y)
+{
+    if (((Value_Double *)x)->d >= ((Value_Double *)y)->d)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}
+Value *gte_char(Value *x, Value *y)
+{
+    if (((Value_Char *)x)->c >= ((Value_Char *)y)->c)
+    {
+        return (Value *)makeInt32(1);
+    }
+    else
+    {
+        return (Value *)makeInt32(0);
+    }
+}

support/refc/mathFunctions.h

@@ -0,0 +1,84 @@
+#ifndef __MATH_FUNCTIONS_H__
+#define __MATH_FUNCTIONS_H__
+#include "cBackend.h"
+#include <math.h>
+
+double unpackDouble(Value *d);
+Value *believe_me(Value *, Value *, Value *);
+
+/* add */
+Value *add_i32(Value *x, Value *y);
+Value *add_i64(Value *x, Value *y);
+Value *add_double(Value *x, Value *y);
+
+/* sub */
+Value *sub_i32(Value *x, Value *y);
+Value *sub_i64(Value *x, Value *y);
+Value *sub_double(Value *x, Value *y);
+
+/* mul */
+Value *mul_i32(Value *x, Value *y);
+Value *mul_i64(Value *x, Value *y);
+Value *mul_double(Value *x, Value *y);
+
+/* div */
+Value *div_i32(Value *x, Value *y);
+Value *div_i64(Value *x, Value *y);
+Value *div_double(Value *x, Value *y);
+
+/* mod */
+Value *mod_i32(Value *x, Value *y);
+Value *mod_i64(Value *x, Value *y);
+
+/* shiftl */
+Value *shiftl_i32(Value *x, Value *y);
+Value *shiftl_i64(Value *x, Value *y);
+
+/* shiftr */
+Value *shiftr_i32(Value *x, Value *y);
+Value *shiftr_i64(Value *x, Value *y);
+
+/* and */
+Value *and_i32(Value *x, Value *y);
+Value *and_i64(Value *x, Value *y);
+
+/* or */
+Value *or_i32(Value *x, Value *y);
+Value *or_i64(Value *x, Value *y);
+
+/* xor */
+Value *xor_i32(Value *x, Value *y);
+Value *xor_i64(Value *x, Value *y);
+
+/* lt */
+Value *lt_i32(Value *x, Value *y);
+Value *lt_i64(Value *x, Value *y);
+Value *lt_double(Value *x, Value *y);
+Value *lt_char(Value *x, Value *y);
+
+/* gt */
+Value *gt_i32(Value *x, Value *y);
+Value *gt_i64(Value *x, Value *y);
+Value *gt_double(Value *x, Value *y);
+Value *gt_char(Value *x, Value *y);
+
+/* eq */
+Value *eq_i32(Value *x, Value *y);
+Value *eq_i64(Value *x, Value *y);
+Value *eq_double(Value *x, Value *y);
+Value *eq_char(Value *x, Value *y);
+Value *eq_string(Value *x, Value *y);
+
+/* lte */
+Value *lte_i32(Value *x, Value *y);
+Value *lte_i64(Value *x, Value *y);
+Value *lte_double(Value *x, Value *y);
+Value *lte_char(Value *x, Value *y);
+
+/* gte */
+Value *gte_i32(Value *x, Value *y);
+Value *gte_i64(Value *x, Value *y);
+Value *gte_double(Value *x, Value *y);
+Value *gte_char(Value *x, Value *y);
+
+#endif

support/refc/memoryManagement.c

@@ -0,0 +1,268 @@
+#include "runtime.h"
+
+Value *newValue()
+{
+    Value *retVal = (Value *)malloc(sizeof(Value));
+    retVal->header.refCounter = 1;
+    retVal->header.tag = NO_TAG;
+    return retVal;
+}
+
+Value_Arglist *newArglist(int missing, int total)
+{
+    Value_Arglist *retVal = (Value_Arglist *)newValue();
+    retVal->header.tag = ARGLIST_TAG;
+    retVal->total = total;
+    retVal->filled = total - missing;
+    retVal->args = (Value **)malloc(sizeof(Value *) * total);
+    memset(retVal->args, 0, sizeof(Value *) * total);
+    return retVal;
+}
+
+Value_Constructor *newConstructor(int total, int tag, const char *name)
+{
+    Value_Constructor *retVal = (Value_Constructor *)newValue();
+    retVal->header.tag = CONSTRUCTOR_TAG;
+    retVal->total = total;
+    retVal->tag = tag;
+    int nameLength = strlen(name);
+    retVal->name = malloc(nameLength + 1);
+    memset(retVal->name, 0, nameLength + 1);
+    memcpy(retVal->name, name, nameLength);
+    retVal->args = (Value **)malloc(sizeof(Value *) * total);
+    return retVal;
+}
+
+Value_Closure *makeClosureFromArglist(fun_ptr_t f, Value_Arglist *arglist)
+{
+    Value_Closure *retVal = (Value_Closure *)newValue();
+    retVal->header.tag = CLOSURE_TAG;
+    retVal->arglist = arglist; // (Value_Arglist *)newReference((Value*)arglist);
+    retVal->f = f;
+    if (retVal->arglist->filled >= retVal->arglist->total)
+    {
+        retVal->header.tag = COMPLETE_CLOSURE_TAG;
+    }
+    return retVal;
+}
+
+Value_Double *makeDouble(double d)
+{
+    Value_Double *retVal = (Value_Double *)newValue();
+    retVal->header.tag = DOUBLE_TAG;
+    retVal->d = d;
+    return retVal;
+}
+
+Value_Char *makeChar(char c)
+{
+    Value_Char *retVal = (Value_Char *)newValue();
+    retVal->header.tag = CHAR_TAG;
+    retVal->c = c;
+    return retVal;
+}
+
+Value_Int8 *makeInt8(int8_t i)
+{
+    Value_Int8 *retVal = (Value_Int8 *)newValue();
+    retVal->header.tag = INT8_TAG;
+    retVal->i8 = i;
+    return retVal;
+}
+
+Value_Int16 *makeInt16(int16_t i)
+{
+    Value_Int16 *retVal = (Value_Int16 *)newValue();
+    retVal->header.tag = INT16_TAG;
+    retVal->i16 = i;
+    return retVal;
+}
+
+Value_Int32 *makeInt32(int32_t i)
+{
+    Value_Int32 *retVal = (Value_Int32 *)newValue();
+    retVal->header.tag = INT32_TAG;
+    retVal->i32 = i;
+    return retVal;
+}
+
+Value_Int64 *makeInt64(int64_t i)
+{
+    Value_Int64 *retVal = (Value_Int64 *)newValue();
+    retVal->header.tag = INT64_TAG;
+    retVal->i64 = i;
+    return retVal;
+}
+
+Value_String *makeEmptyString(size_t l)
+{
+    Value_String *retVal = (Value_String *)newValue();
+    retVal->header.tag = STRING_TAG;
+    retVal->str = malloc(l);
+    memset(retVal->str, 0, l);
+    return retVal;
+}
+
+Value_String *makeString(char *s)
+{
+    Value_String *retVal = (Value_String *)newValue();
+    int l = strlen(s);
+    retVal->header.tag = STRING_TAG;
+    retVal->str = malloc(l + 1);
+    memset(retVal->str, 0, l + 1);
+    memcpy(retVal->str, s, l);
+    return retVal;
+}
+
+Value_Pointer *makePointer(void *ptr_Raw)
+{
+    Value_Pointer *p = (Value_Pointer *)newValue();
+    p->header.tag = POINTER_TAG;
+    p->p = ptr_Raw;
+    return p;
+}
+
+Value_Array *makeArray(int length)
+{
+    Value_Array *a = (Value_Array *)newValue();
+    a->header.tag = ARRAY_TAG;
+    a->capacity = length;
+    a->arr = (Value **)malloc(sizeof(Value *) * length);
+    memset(a->arr, 0, sizeof(Value *) * length);
+    return a;
+}
+
+Value_World *makeWorld()
+{
+    Value_World *retVal = (Value_World *)newValue();
+    retVal->header.tag = WORLD_TAG;
+    retVal->listIORefs = NULL;
+    return retVal;
+}
+
+Value *newReference(Value *source)
+{
+    // note that we explicitly allow NULL as source (for erased arguments)
+    if (source)
+    {
+        source->header.refCounter++;
+    }
+    return source;
+}
+
+void removeReference(Value *elem)
+{
+    if (!elem)
+    {
+        return;
+    }
+    // remove reference counter
+    elem->header.refCounter--;
+    if (elem->header.refCounter == 0)
+    // recursively remove all references to all children
+    {
+        switch (elem->header.tag)
+        {
+        case INT32_TAG:
+            /* nothing to delete, added for sake of completeness */
+            break;
+        case INT64_TAG:
+            /* nothing to delete, added for sake of completeness */
+            break;
+        case DOUBLE_TAG:
+            /* nothing to delete, added for sake of completeness */
+            break;
+        case CHAR_TAG:
+            /* nothing to delete, added for sake of completeness */
+            break;
+        case STRING_TAG:
+            free(((Value_String *)elem)->str);
+            break;
+
+        case CLOSURE_TAG:
+        {
+            Value_Closure *cl = (Value_Closure *)elem;
+            Value_Arglist *al = cl->arglist;
+            removeReference((Value *)al);
+            break;
+        }
+        case COMPLETE_CLOSURE_TAG:
+        {
+            Value_Closure *cl = (Value_Closure *)elem;
+            Value_Arglist *al = cl->arglist;
+            removeReference((Value *)al);
+            break;
+        }
+        case ARGLIST_TAG:
+        {
+            Value_Arglist *al = (Value_Arglist *)elem;
+            for (int i = 0; i < al->filled; i++)
+            {
+                removeReference(al->args[i]);
+            }
+            free(al->args);
+            break;
+        }
+        case CONSTRUCTOR_TAG:
+        {
+            Value_Constructor *constr = (Value_Constructor *)elem;
+            for (int i = 0; i < constr->total; i++)
+            {
+                removeReference(constr->args[i]);
+            }
+            if (constr->name)
+            {
+                free(constr->name);
+            }
+            free(constr->args);
+            break;
+        }
+        case IOREF_TAG:
+            /* nothing to delete, added for sake of completeness */
+            break;
+
+        case ARRAY_TAG:
+        {
+            Value_Array *a = (Value_Array *)elem;
+            for (int i = 0; i < a->capacity; i++)
+            {
+                removeReference(a->arr[i]);
+            }
+            free(a->arr);
+            break;
+        }
+        case POINTER_TAG:
+            /* nothing to delete, added for sake of completeness */
+            break;
+
+        case GC_POINTER_TAG:
+        {
+            /* maybe here we need to invoke onCollectAny */
+            Value_GCPointer *vPtr = (Value_GCPointer *)elem;
+            Value *closure1 = apply_closure((Value *)vPtr->onCollectFct, (Value *)vPtr->p);
+            apply_closure(closure1, NULL);
+            removeReference(closure1);
+            removeReference((Value *)vPtr->onCollectFct);
+            removeReference((Value *)vPtr->p);
+            break;
+        }
+        case WORLD_TAG:
+        {
+            Value_World *w = (Value_World *)elem;
+            if (w->listIORefs)
+            {
+                for (int i = 0; i < w->listIORefs->filled; i++)
+                {
+                    removeReference(w->listIORefs->refs[i]);
+                }
+                free(w->listIORefs->refs);
+                free(w->listIORefs);
+            }
+        }
+        default:
+            break;
+        }
+        // finally, free element
+        free(elem);
+    }
+}

support/refc/memoryManagement.h

@@ -0,0 +1,28 @@
+#ifndef __MEMORY_MANAGEMENT_H__
+#define __MEMORY_MANAGEMENT_H__
+#include "cBackend.h"
+
+Value *newValue(void);
+Value *newReference(Value *source);
+void removeReference(Value *source);
+
+Value_Arglist *newArglist(int missing, int total);
+Value_Constructor *newConstructor(int total, int tag, const char *name);
+
+// copies arglist, no pointer bending
+Value_Closure *makeClosureFromArglist(fun_ptr_t f, Value_Arglist *);
+
+Value_Double *makeDouble(double d);
+Value_Char *makeChar(char d);
+Value_Int8 *makeInt8(int8_t i);
+Value_Int16 *makeInt16(int16_t i);
+Value_Int32 *makeInt32(int32_t i);
+Value_Int64 *makeInt64(int64_t i);
+Value_String *makeEmptyString(size_t l);
+Value_String *makeString(char *);
+
+Value_Pointer *makePointer(void *);
+Value_Array *makeArray(int length);
+Value_World *makeWorld(void);
+
+#endif

support/refc/prim.c

@@ -0,0 +1,323 @@
+#include <unistd.h>
+#include "prim.h"
+
+Value *Prelude_IO_prim__getChar(Value *world)
+{
+    char c = getchar();
+    return (Value *)makeChar(c);
+}
+
+// This is NOT THREAD SAFE in the current implementation
+
+IORef_Storage *newIORef_Storage(int capacity)
+{
+    IORef_Storage *retVal = (IORef_Storage *)malloc(sizeof(IORef_Storage));
+    retVal->filled = 0;
+    retVal->total = capacity;
+    retVal->refs = (Value **)malloc(sizeof(Value *) * retVal->total);
+    return retVal;
+}
+
+void doubleIORef_Storage(IORef_Storage *ior)
+{
+    Value **values = (Value **)malloc(sizeof(Value *) * ior->total * 2);
+    ior->total *= 2;
+    for (int i = 0; i < ior->filled; i++)
+    {
+        values[i] = ior->refs[i];
+    }
+    free(ior->refs);
+    ior->refs = values;
+}
+
+Value *newIORef(Value *erased, Value *input_value, Value *_world)
+{
+    // if no ioRef Storag exist, start with one
+    Value_World *world = (Value_World *)_world;
+    if (!world->listIORefs)
+    {
+        world->listIORefs = newIORef_Storage(128);
+    }
+    // expand size of needed
+    if (world->listIORefs->filled >= world->listIORefs->total)
+    {
+        doubleIORef_Storage(world->listIORefs);
+    }
+
+    // store value
+    Value_IORef *ioRef = (Value_IORef *)newValue();
+    ioRef->header.tag = IOREF_TAG;
+    ioRef->index = world->listIORefs->filled;
+    world->listIORefs->refs[world->listIORefs->filled] = newReference(input_value);
+    world->listIORefs->filled++;
+
+    return (Value *)ioRef;
+}
+
+Value *readIORef(Value *erased, Value *_index, Value *_world)
+{
+    Value_World *world = (Value_World *)_world;
+    Value_IORef *index = (Value_IORef *)_index;
+    return newReference(world->listIORefs->refs[index->index]);
+}
+
+Value *writeIORef(Value *erased, Value *_index, Value *new_value, Value *_world)
+{
+    Value_World *world = (Value_World *)_world;
+    Value_IORef *index = (Value_IORef *)_index;
+    removeReference(world->listIORefs->refs[index->index]);
+    world->listIORefs->refs[index->index] = newReference(new_value);
+    return newReference(_index);
+}
+
+// -----------------------------------
+//       System operations
+// -----------------------------------
+
+Value *sysOS(void)
+{
+#ifdef _WIN32
+    return (Value *)makeString("windows");
+#elif _WIN64
+    return (Value *)makeString("windows");
+#elif __APPLE__ || __MACH__
+    return (Value *)makeString("Mac OSX");
+#elif __linux__
+    return (Value *)makeString("Linux");
+#elif __FreeBSD__
+    return (Value *)makeString("FreeBSD");
+#elif __OpenBSD__
+    return (Value *)makeString("OpenBSD");
+#elif __NetBSD__
+    return (Value *)makeString("NetBSD");
+#elif __DragonFly__
+    return (Value *)makeString("DragonFly");
+#elif __unix || __unix__
+    return (Value *)makeString("Unix");
+#else
+    return (Value *)makeString("Other");
+#endif
+}
+
+Value* idris2_crash(Value* msg) {
+    Value_String* str = (Value_String*)msg;
+    printf("ERROR: %s\n", str->str);
+    exit(-1);
+}
+
+
+//
+//
+//
+// // -----------------------------------
+// //         Array operations
+// // -----------------------------------
+
+Value *newArray(Value *erased, Value *_length, Value *v, Value *_word)
+{
+    int length = extractInt(_length);
+    Value_Array *a = makeArray(length);
+
+    for (int i = 0; i < length; i++)
+    {
+        a->arr[i] = newReference(v);
+    }
+
+    return (Value *)a;
+}
+
+Value *arrayGet(Value *erased, Value *_array, Value *_index, Value *_word)
+{
+    Value_Array *a = (Value_Array *)_array;
+    return newReference(a->arr[((Value_Int32 *)_index)->i32]);
+}
+
+Value *arraySet(Value *erased, Value *_array, Value *_index, Value *v, Value *_word)
+{
+    Value_Array *a = (Value_Array *)_array;
+    removeReference(a->arr[((Value_Int32 *)_index)->i32]);
+    a->arr[((Value_Int32 *)_index)->i32] = newReference(v);
+    return NULL;
+}
+
+//
+// -----------------------------------
+//      Pointer operations
+// -----------------------------------
+
+Value *PrimIO_prim__nullAnyPtr(Value *ptr)
+{
+    void *p;
+    switch (ptr->header.tag)
+    {
+    case STRING_TAG:
+        p = ((Value_String *)ptr)->str;
+        break;
+    case POINTER_TAG:
+        p = ((Value_Pointer *)ptr)->p;
+        break;
+    default:
+        p = NULL;
+    }
+    if (p)
+    {
+        return (Value *)makeInt32(0);
+    }
+    else
+    {
+        return (Value *)makeInt32(1);
+    }
+}
+
+Value *onCollect(Value *_erased, Value *_anyPtr, Value *_freeingFunction, Value *_world)
+{
+    printf("onCollect called\n");
+    Value_GCPointer *retVal = (Value_GCPointer *)newValue();
+    retVal->header.tag = GC_POINTER_TAG;
+    retVal->p = (Value_Pointer *)newReference(_anyPtr);
+    retVal->onCollectFct = (Value_Closure *)newReference(_freeingFunction);
+    return (Value *)retVal;
+}
+
+Value *onCollectAny(Value *_erased, Value *_anyPtr, Value *_freeingFunction, Value *_world)
+{
+    printf("onCollectAny called\n");
+    Value_GCPointer *retVal = (Value_GCPointer *)newValue();
+    retVal->header.tag = GC_POINTER_TAG;
+    retVal->p = (Value_Pointer *)_anyPtr;
+    retVal->onCollectFct = (Value_Closure *)_freeingFunction;
+    return (Value *)retVal;
+}
+
+Value *voidElim(Value *erased1, Value *erased2)
+{
+    return NULL;
+}
+
+// Threads
+
+// %foreign "scheme:blodwen-mutex"
+// prim__makeMutex : PrimIO Mutex
+// using pthread_mutex_init(pthread_mutex_t *mutex, const pthread_mutexattr_t *attr)
+Value *System_Concurrency_Raw_prim__makeMutex(Value *_world)
+{
+    Value_Mutex *mut = (Value_Mutex *)newValue();
+    mut->header.tag = MUTEX_TAG;
+    mut->mutex = (pthread_mutex_t *)malloc(sizeof(pthread_mutex_t));
+    if (pthread_mutex_init(mut->mutex, NULL))
+    {
+        fprintf(stderr, "Error init Mutex\n");
+        exit(-1);
+    }
+    return (Value *)mut;
+}
+
+// %foreign "scheme:blodwen-lock"
+// prim__mutexAcquire : Mutex -> PrimIO ()
+// using pthread_mutex_lock(pthread_mutex_t *mutex)
+Value *System_Concurrency_Raw_prim__mutexAcquire(Value *_mutex, Value *_world)
+{
+    if (pthread_mutex_lock(((Value_Mutex *)_mutex)->mutex))
+    {
+        fprintf(stderr, "Error locking mutex\n");
+        exit(-1);
+    }
+    return NULL;
+}
+
+// %foreign "scheme:blodwen-unlock"
+// prim__mutexRelease : Mutex -> PrimIO ()
+//using int pthread_mutex_unlock(pthread_mutex_t *mutex)
+Value *System_Concurrency_Raw_prim__mutexRelease(Value *_mutex, Value *_world)
+{
+    if (pthread_mutex_unlock(((Value_Mutex *)_mutex)->mutex))
+    {
+        fprintf(stderr, "Error locking mutex\n");
+        exit(-1);
+    }
+    return NULL;
+}
+
+// %foreign "scheme:blodwen-condition"
+// prim__makeCondition : PrimIO Condition
+// using int pthread_cond_init(pthread_cond_t *cond, const pthread_condattr_t *attr)
+// with standard initialisation
+Value *System_Concurrency_Raw_prim__makeCondition(Value *_world)
+{
+    // typedef struct{
+    //     Value_header header;
+    //     pthread_cond_t *cond;
+    // }Value_Condition;
+
+    Value_Condition *c = (Value_Condition *)newValue();
+    c->header.tag = CONDITION_TAG;
+    c->cond = (pthread_cond_t *)malloc(sizeof(pthread_cond_t));
+    if (pthread_cond_init(c->cond, NULL))
+    {
+        fprintf(stderr, "error init condition\n");
+        exit(-1);
+    }
+    return (Value *)c;
+}
+
+// %foreign "scheme:blodwen-condition-wait"
+// prim__conditionWait : Condition -> Mutex -> PrimIO ()
+// using int pthread_cond_wait(pthread_cond_t *, pthread_mutex_t *mutex)
+Value *System_Concurrency_Raw_prim__conditionWait(Value *_condition, Value *_mutex, Value *_world)
+{
+    Value_Condition *cond = (Value_Condition *)_condition;
+    Value_Mutex *mutex = (Value_Mutex *)_mutex;
+    if (pthread_cond_wait(cond->cond, mutex->mutex))
+    {
+        fprintf(stderr, "Error Conditional Wait\n");
+        exit(-1);
+    }
+    return NULL;
+}
+
+// %foreign "scheme:blodwen-condition-wait-timeout"
+// prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO ()
+// using int pthread_cond_timedwait(pthread_cond_t *cond, pthread_mutex_t *mutex, const struct timespec *abstime)
+Value *System_Concurrency_Raw_prim__conditionWaitTimeout(Value *_condition, Value *_mutex, Value *_timeout, Value *_world)
+{
+    Value_Condition *cond = (Value_Condition *)_condition;
+    Value_Mutex *mutex = (Value_Mutex *)_mutex;
+    Value_Int32 *timeout = (Value_Int32 *)_timeout;
+    struct timespec t;
+    t.tv_sec = timeout->i32 / 1000000;
+    t.tv_nsec = timeout->i32 % 1000000;
+    if (pthread_cond_timedwait(cond->cond, mutex->mutex, &t))
+    {
+        fprintf(stderr, "Error in pthread_cond_timedwait\n");
+        exit(-1);
+    }
+    return NULL;
+}
+
+// %foreign "scheme:blodwen-condition-signal"
+// prim__conditionSignal : Condition -> PrimIO ()
+// using int pthread_cond_signal(pthread_cond_t *cond)
+Value *System_Concurrency_Raw_prim__conditionSignal(Value *_condition, Value *_world)
+{
+    Value_Condition *cond = (Value_Condition *)_condition;
+    if (pthread_cond_signal(cond->cond))
+    {
+        fprintf(stderr, "Error in pthread_cond_signal\n");
+        exit(-1);
+    }
+    return NULL;
+}
+
+// %foreign "scheme:blodwen-condition-broadcast"
+// prim__conditionBroadcast : Condition -> PrimIO ()
+// using int pthread_cond_broadcast(pthread_cond_t *cond)
+Value *System_Concurrency_Raw_prim__conditionBroadcast(Value *_condition, Value *_mutex)
+{
+    Value_Condition *cond = (Value_Condition *)_condition;
+    if (pthread_cond_broadcast(cond->cond))
+    {
+        fprintf(stderr, "Error in pthread_cond_broadcast\n");
+        exit(-1);
+    }
+    return NULL;
+}

support/refc/prim.h

@@ -0,0 +1,52 @@
+#ifndef __PRIM_H__
+#define __PRIM_H__
+
+#include "cBackend.h"
+
+
+
+// Value * Prelude_IO_prim__putStr(Value *, Value *);
+Value *Prelude_IO_prim__getChar(Value *);
+
+// IORef
+
+Value *newIORef(Value *, Value *, Value *);
+Value *readIORef(Value *, Value *, Value *);
+Value *writeIORef(Value *, Value *, Value *, Value *);
+
+// Sys
+
+Value *sysOS(void);
+Value* idris2_crash(Value* msg);
+
+// Array
+
+Value *newArray(Value *, Value *, Value *, Value *);
+Value *arrayGet(Value *, Value *, Value *, Value *);
+Value *arraySet(Value *, Value *, Value *, Value *, Value *);
+
+// Pointer
+Value *PrimIO_prim__nullAnyPtr(Value *);
+
+Value *onCollect(Value *, Value *, Value *, Value *);
+Value *onCollectAny(Value *, Value *, Value *, Value *);
+
+Value *voidElim(Value *, Value *);
+
+// Threads
+Value *System_Concurrency_Raw_prim__mutexRelease(Value *, Value *);
+
+Value *System_Concurrency_Raw_prim__mutexAcquire(Value *, Value *);
+
+Value *System_Concurrency_Raw_prim__makeMutex(Value *);
+
+Value *System_Concurrency_Raw_prim__makeCondition(Value *);
+
+Value *System_Concurrency_Raw_prim__conditionWait(Value *, Value *, Value *);
+
+Value *System_Concurrency_Raw_prim__conditionWaitTimeout(Value *, Value *, Value *, Value *);
+
+Value *System_Concurrency_Raw_prim__conditionSignal(Value *, Value *);
+
+Value *System_Concurrency_Raw_prim__conditionBroadcast(Value *, Value *);
+#endif

support/refc/runtime.c

@@ -0,0 +1,114 @@
+#include "runtime.h"
+
+void push_Arglist(Value_Arglist *arglist, Value *arg)
+{
+  if (arglist->filled >= arglist->total)
+  {
+    fprintf(stderr, "unable to add more arguments to arglist\n");
+    exit(1);
+  }
+
+  arglist->args[arglist->filled] = newReference(arg);
+  arglist->filled++;
+}
+
+Value *apply_closure(Value *_clos, Value *arg)
+{
+  // create a new arg list
+  Value_Arglist *oldArgs = ((Value_Closure *)_clos)->arglist;
+  Value_Arglist *newArgs = newArglist(0, oldArgs->total);
+  newArgs->filled = oldArgs->filled + 1;
+  // add argument to new arglist
+  for (int i = 0; i < oldArgs->filled; i++)
+  {
+    newArgs->args[i] = newReference(oldArgs->args[i]);
+  }
+  newArgs->args[oldArgs->filled] = newReference(arg);
+
+  Value_Closure *clos = (Value_Closure *)_clos;
+
+  // check if enough arguments exist
+  if (newArgs->filled >= newArgs->total)
+  {
+    fun_ptr_t f = clos->f;
+    while (1)
+    {
+      Value *retVal = f(newArgs);
+      removeReference((Value *)newArgs);
+      if (!retVal || retVal->header.tag != COMPLETE_CLOSURE_TAG)
+      {
+        return retVal;
+      }
+      f = ((Value_Closure *)retVal)->f;
+      newArgs = ((Value_Closure *)retVal)->arglist;
+      newArgs = (Value_Arglist *)newReference((Value *)newArgs);
+      removeReference(retVal);
+    }
+  }
+
+  return (Value *)makeClosureFromArglist(clos->f, newArgs);
+}
+
+Value *tailcall_apply_closure(Value *_clos, Value *arg)
+{
+  // create a new arg list
+  Value_Arglist *oldArgs = ((Value_Closure *)_clos)->arglist;
+  Value_Arglist *newArgs = newArglist(0, oldArgs->total);
+  newArgs->filled = oldArgs->filled + 1;
+  // add argument to new arglist
+  for (int i = 0; i < oldArgs->filled; i++)
+  {
+    newArgs->args[i] = newReference(oldArgs->args[i]);
+  }
+  newArgs->args[oldArgs->filled] = newReference(arg);
+
+  Value_Closure *clos = (Value_Closure *)_clos;
+
+  // check if enough arguments exist
+  if (newArgs->filled >= newArgs->total)
+    return (Value *)makeClosureFromArglist(clos->f, newArgs);
+
+  return (Value *)makeClosureFromArglist(clos->f, newArgs);
+}
+
+int extractInt(Value *v)
+{
+  if (v->header.tag == INT64_TAG)
+  {
+    return (int)((Value_Int64 *)v)->i64;
+  }
+
+  if (v->header.tag == INT32_TAG)
+  {
+    return ((Value_Int32 *)v)->i32;
+  }
+
+  if (v->header.tag == DOUBLE_TAG)
+  {
+    return (int)((Value_Double *)v)->d;
+  }
+
+  return -1;
+}
+
+Value *trampoline(Value *closure)
+{
+  fun_ptr_t f = ((Value_Closure *)closure)->f;
+  Value_Arglist *_arglist = ((Value_Closure *)closure)->arglist;
+  Value_Arglist *arglist = (Value_Arglist *)newReference((Value *)_arglist);
+  removeReference(closure);
+  while (1)
+  {
+    Value *retVal = f(arglist);
+    removeReference((Value *)arglist);
+    if (!retVal || retVal->header.tag != COMPLETE_CLOSURE_TAG)
+    {
+      return retVal;
+    }
+    f = ((Value_Closure *)retVal)->f;
+    arglist = ((Value_Closure *)retVal)->arglist;
+    arglist = (Value_Arglist *)newReference((Value *)arglist);
+    removeReference(retVal);
+  }
+  return NULL;
+}

support/refc/runtime.h

@@ -0,0 +1,12 @@
+#ifndef __RUNTIME_H__
+#define __RUNTIME_H__
+
+#include "cBackend.h"
+
+Value *apply_closure(Value *, Value *arg);
+void push_Arglist(Value_Arglist *arglist, Value *arg);
+
+int extractInt(Value *);
+Value *trampoline(Value *closure);
+Value *tailcall_apply_closure(Value *_clos, Value *arg);
+#endif

support/refc/stringOps.c

@@ -0,0 +1,91 @@
+#include "stringOps.h"
+
+Value *stringLength(Value *s)
+{
+    int length = strlen(((Value_String *)s)->str);
+    return (Value *)makeInt32(length);
+}
+
+Value *head(Value *str)
+{
+    Value_Char *c = (Value_Char *)newValue();
+    c->header.tag = CHAR_TAG;
+    c->c = ((Value_String *)str)->str[0];
+    return (Value *)c;
+}
+
+Value *tail(Value *str)
+{
+    Value_Char *c = (Value_Char *)newValue();
+    c->header.tag = CHAR_TAG;
+    Value_String *s = (Value_String *)str;
+    int l = strlen(s->str);
+    c->c = s->str[l - 1];
+    return (Value *)c;
+}
+
+Value *reverse(Value *str)
+{
+    Value_String *retVal = (Value_String *)newValue();
+    retVal->header.tag = STRING_TAG;
+    Value_String *input = (Value_String *)str;
+    int l = strlen(input->str);
+    retVal->str = malloc(l + 1);
+    memset(retVal->str, 0, l + 1);
+    char *p = retVal->str;
+    char *q = input->str + (l - 1);
+    for (int i = 1; i < l; i++)
+    {
+        *p++ = *q--;
+    }
+    return (Value *)retVal;
+}
+
+Value *strIndex(Value *str, Value *i)
+{
+    Value_Char *c;
+    switch (i->header.tag)
+    {
+    case INT64_TAG:
+        c = makeChar(((Value_String *)str)->str[((Value_Int64 *)i)->i64]);
+        return (Value *)c;
+    default:
+        c = makeChar(((Value_String *)str)->str[((Value_Int32 *)i)->i32]);
+        return (Value *)c;
+    }
+}
+
+Value *strCons(Value *c, Value *str)
+{
+    int l = strlen(((Value_String *)str)->str);
+    Value_String *retVal = makeEmptyString(l + 2);
+    retVal->str[0] = ((Value_Char *)c)->c;
+    memcpy(retVal->str + 1, ((Value_String *)str)->str, l);
+    return (Value *)retVal;
+}
+
+Value *strAppend(Value *a, Value *b)
+{
+    int la = strlen(((Value_String *)a)->str);
+    int lb = strlen(((Value_String *)b)->str);
+    Value_String *retVal = makeEmptyString(la + lb + 1);
+    memcpy(retVal->str, ((Value_String *)a)->str, la);
+    memcpy(retVal->str + la, ((Value_String *)b)->str, lb);
+    return (Value *)retVal;
+}
+
+Value *strSubstr(Value *s, Value *start, Value *len)
+{
+    Value_String *retVal;
+    switch (len->header.tag)
+    {
+    case INT64_TAG:
+        retVal = makeEmptyString(((Value_Int64 *)len)->i64 + 1);
+        memcpy(retVal->str, ((Value_String *)s)->str, ((Value_Int64 *)len)->i64);
+        return (Value *)retVal;
+    default:
+        retVal = makeEmptyString(((Value_Int32 *)len)->i32 + 1);
+        memcpy(retVal->str, ((Value_String *)s)->str, ((Value_Int32 *)len)->i32);
+        return (Value *)retVal;
+    }
+}

support/refc/stringOps.h

@@ -0,0 +1,15 @@
+#ifndef __STRING_OPS_H__
+#define __STRING_OPS_H__
+
+#include "cBackend.h"
+
+Value *stringLength(Value *);
+Value *head(Value *str);
+Value *tail(Value *str);
+Value *reverse(Value *str);
+Value *strIndex(Value *str, Value *i);
+Value *strCons(Value *c, Value *str);
+Value *strAppend(Value *a, Value *b);
+Value *strSubstr(Value *s, Value *start, Value *len);
+
+#endif

tests/Lib.idr

@@ -0,0 +1,322 @@
+||| Core features required to perform Golden file testing.
+|||
+||| We provide the core functionality to run a *single* golden file test, or
+||| a whole test tree.
+||| This allows the developer freedom to use as is or design the rest of the
+||| test harness to their liking.
+|||
+||| This was originally used as part of Idris2's own test suite and
+||| the core functionality is useful for the many and not the few.
+||| Please see Idris2 test harness for example usage.
+|||
+||| # Test Structure
+|||
+||| This harness works from the assumption that each individual golden test
+||| comprises of a directory with the following structure:
+|||
+||| + `run` a *shell* script that runs the test. We expect it to:
+|||   * Use `$1` as the variable standing for the idris executable to be tested
+|||   * May use `${IDRIS2_TESTS_CG}` to pick a codegen that ought to work
+|||   * Clean up after itself (e.g. by running `rm -rf build/`)
+|||
+||| + `expected` a file containting the expected output of `run`
+|||
+||| During testing, the test harness will generate an artefact named `output` and
+||| display both outputs if there is a failure.
+||| During an interactive session the following command is used to compare them as
+||| they are:
+|||
+||| ```sh
+|||  git diff --no-index --exit-code --word-diff=color expected output
+||| ```
+|||
+||| If `git` fails then the runner will simply present the expected and 'given'
+||| files side-by-side.
+|||
+||| Of note, it is helpful if `output` was added to a local `.gitignore` instance
+||| to ensure that it is not mistakenly versioned.
+|||
+||| # Options
+|||
+||| The test harness has several options that may be set:
+|||
+||| + `idris2`       The path of the executable we are testing.
+||| + `onlyNames`    The list of tests to run relative to the generated executable.
+||| + `interactive`  Whether to offer to update the expected file or not.
+||| + `timing`       Whether to display time taken for each test.
+|||
+||| We provide an options parser (`options`) that will take the command line arguments
+||| and constructs this for you.
+|||
+||| # Usage
+|||
+||| When compiled to an executable the expected usage is:
+|||
+|||```sh
+|||runtests <path to executable under test> [--timing] [--interactive] [--only [NAMES]]
+|||```
+|||
+||| assuming that the test runner is compiled to an executable named `runtests`.
+
+module Lib
+
+import Data.Maybe
+import Data.List
+import Data.List1
+import Data.Strings
+
+import System
+import System.Clock
+import System.Directory
+import System.File
+import System.Info
+import System.Path
+
+-- [ Options ]
+
+||| Options for the test driver.
+public export
+record Options where
+  constructor MkOptions
+  ||| Name of the idris2 executable
+  exeUnderTest : String
+  ||| Which codegen should we use?
+  codegen      : Maybe String
+  ||| Should we only run some specific cases?
+  onlyNames    : List String
+  ||| Should we run the test suite interactively?
+  interactive  : Bool
+  ||| Should we time and display the tests
+  timing       : Bool
+
+export
+usage : String -> String
+usage exe = unwords ["Usage:", exe, "runtests <path> [--timing] [--interactive] [--cg CODEGEN] [--only [NAMES]]"]
+
+||| Process the command line options.
+export
+options : List String -> Maybe Options
+options args = case args of
+    (_ :: exeUnderTest :: rest) => go rest (MkOptions exeUnderTest Nothing [] False False)
+    _ => Nothing
+
+  where
+
+    go : List String -> Options -> Maybe Options
+    go rest opts = case rest of
+      []                      => pure opts
+      ("--timing" :: xs)      => go xs (record { timing = True} opts)
+      ("--interactive" :: xs) => go xs (record { interactive = True } opts)
+      ("--cg" :: cg :: xs)    => go xs (record { codegen = Just cg } opts)
+      ("--only" :: xs)        => pure $ record { onlyNames = xs } opts
+      _ => Nothing
+
+-- [ Core ]
+
+export
+fail : String -> IO ()
+fail err
+    = do putStrLn err
+         exitWith (ExitFailure 1)
+
+
+||| Normalise strings between different OS.
+|||
+||| on Windows, we just ignore backslashes and slashes when comparing,
+||| similarity up to that is good enough. Leave errors that depend
+||| on the confusion of slashes and backslashes to unix machines.
+normalize : String -> String
+normalize str =
+    if isWindows
+      then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
+      else str
+
+||| Run the specified Golden test with the supplied options.
+|||
+||| See the module documentation for more information.
+|||
+||| @currdir absolute or relative path to root test directory.
+||| @testpath the directory that contains the test.
+export
+runTest : Options -> (currdir, testPath : String) -> IO Bool
+runTest opts currdir testPath
+    = do changeDir testPath
+         isSuccess <- runTest'
+         changeDir currdir
+         pure isSuccess
+    where
+        getAnswer : IO Bool
+        getAnswer = do
+          str <- getLine
+          case str of
+            "y" => pure True
+            "n" => pure False
+            _   => do putStrLn "Invalid Answer."
+                      getAnswer
+
+        printExpectedVsOutput : String -> String -> IO ()
+        printExpectedVsOutput exp out = do
+          putStrLn "Expected:"
+          putStrLn exp
+          putStrLn "Given:"
+          putStrLn out
+
+        mayOverwrite : Maybe String -> String -> IO ()
+        mayOverwrite mexp out = do
+          the (IO ()) $ case mexp of
+            Nothing => putStr $ unlines
+              [ "Golden value missing. I computed the following result:"
+              , out
+              , "Accept new golden value? [yn]"
+              ]
+            Just exp => do
+              putStrLn "Golden value differs from actual value."
+              code <- system "git diff --no-index --exit-code --word-diff=color expected output"
+              when (code < 0) $ printExpectedVsOutput exp out
+              putStrLn "Accept actual value as new golden value? [yn]"
+          b <- getAnswer
+          when b $ do Right _ <- writeFile "expected" out
+                          | Left err => print err
+                      pure ()
+
+        printTiming : Bool -> Clock type -> String -> IO ()
+        printTiming True  clock msg = putStrLn (unwords [msg, show clock])
+        printTiming False _     msg = putStrLn msg
+
+        runTest' : IO Bool
+        runTest'
+            = do putStr $ testPath ++ ": "
+                 start <- clockTime Thread
+                 let cg = case codegen opts of
+                            Nothing => ""
+                            Just cg => "env IDRIS2_TESTS_CG=" ++ cg ++ " "
+                 system $ cg ++ "sh ./run " ++ exeUnderTest opts ++ " | tr -d '\\r' > output"
+                 end <- clockTime Thread
+                 Right out <- readFile "output"
+                     | Left err => do print err
+                                      pure False
+                 Right exp <- readFile "expected"
+                     | Left FileNotFound => do
+                         if interactive opts
+                           then mayOverwrite Nothing out
+                           else print FileNotFound
+                         pure False
+                     | Left err => do print err
+                                      pure False
+                 let result = normalize out == normalize exp
+                 let time = timeDifference end start
+                 if result
+                    then printTiming (timing opts) time "success"
+                    else do
+                      printTiming (timing opts) time "FAILURE"
+                      if interactive opts
+                         then mayOverwrite (Just exp) out
+                         else printExpectedVsOutput exp out
+
+                 pure result
+
+||| Find the first occurrence of an executable on `PATH`.
+export
+pathLookup : List String -> IO (Maybe String)
+pathLookup names = do
+  path <- getEnv "PATH"
+  let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
+  let candidates = [p ++ "/" ++ x | p <- pathList,
+                                    x <- names]
+  firstExists candidates
+
+
+||| Some test may involve Idris' backends and have requirements.
+||| We define here the ones supported by Idris
+public export
+data Requirement = Chez | Node | Racket
+
+export
+Show Requirement where
+  show Chez = "Chez"
+  show Node = "node"
+  show Racket = "racket"
+
+export
+checkRequirement : Requirement -> IO (Maybe String)
+checkRequirement req
+  = do let (envvar, paths) = requirement req
+       Just exec <- getEnv envvar | Nothing => pathLookup paths
+       pure (Just exec)
+
+  where
+    requirement : Requirement -> (String, List String)
+    requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "scheme", "scheme.exe"])
+    requirement Node = ("NODE", ["node"])
+    requirement Racket = ("RACKET", ["racket"])
+
+export
+findCG : IO (Maybe String)
+findCG
+  = do Nothing <- getEnv "IDRIS2_TESTS_CG" | p => pure p
+       Nothing <- checkRequirement Chez    | p => pure (Just "chez")
+       Nothing <- checkRequirement Node    | p => pure (Just "node")
+       Nothing <- checkRequirement Racket  | p => pure (Just "racket")
+       pure Nothing
+
+||| A test pool is characterised by
+|||  + a list of requirement
+|||  + and a list of directory paths
+public export
+record TestPool where
+  constructor MkTestPool
+  constraints : List Requirement
+  testCases : List String
+
+||| Only keep the tests that have been asked for
+export
+filterTests : Options -> List String -> List String
+filterTests opts = case onlyNames opts of
+  [] => id
+  xs => filter (\ name => any (`isInfixOf` name) xs)
+
+||| A runner for a test pool
+export
+poolRunner : Options -> (currdir : String) -> TestPool -> IO (List Bool)
+poolRunner opts currdir pool
+  = do -- check that we indeed want to run some of these tests
+       let tests = filterTests opts (testCases pool)
+       let (_ :: _) = tests
+             | [] => pure []
+       -- if so make sure the constraints are satisfied
+       cs <- for (constraints pool) $ \ req => do
+          mfp <- checkRequirement req
+          putStrLn $ case mfp of
+            Nothing => show req ++ " not found"
+            Just fp => "Found " ++ show req ++ " at " ++ fp
+          pure mfp
+       let Just _ = the (Maybe (List String)) (sequence cs)
+             | Nothing => pure []
+       -- if so run them all!
+       traverse (runTest opts currdir) tests
+
+
+||| A runner for a whole test suite
+export
+runner : List TestPool -> IO ()
+runner tests
+    = do args <- getArgs
+         let (Just opts) = options args
+              | _ => do print args
+                        putStrLn (usage "runtests")
+         -- if no CG has been set, find a sensible default based on what is available
+         opts <- case codegen opts of
+                   Nothing => pure $ record { codegen = !findCG } opts
+                   Just _ => pure opts
+         -- grab the current directory
+         Just pwd <- currentDir
+            | Nothing => putStrLn "FATAL: Could not get current working directory"
+         -- run the tests
+         res <- concat <$> traverse (poolRunner opts pwd) tests
+         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res)
+                       ++ " tests successful")
+         if (any not res)
+            then exitWith (ExitFailure 1)
+            else exitWith ExitSuccess
+
+-- [ EOF ]

tests/Main.idr

@@ -11,14 +11,16 @@ import System.File
 import System.Info
 import System.Path
 
+import Lib
+
 %default covering
 
 ------------------------------------------------------------------------
 -- Test cases
 
-ttimpTests : List String
-ttimpTests
-    = ["basic001", "basic002", "basic003", "basic004", "basic005",
+ttimpTests : TestPool
+ttimpTests = MkTestPool []
+      ["basic001", "basic002", "basic003", "basic004", "basic005",
        "basic006",
        "coverage001", "coverage002",
        "dot001",
@@ -30,9 +32,9 @@ ttimpTests
        "qtt001", "qtt003",
        "total001", "total002", "total003"]
 
-idrisTests : List String
-idrisTests
-    = -- Fundamental language features
+idrisTests : TestPool
+idrisTests = MkTestPool []
+      -- Fundamental language features
       ["basic001", "basic002", "basic003", "basic004", "basic005",
        "basic006", "basic007", "basic008", "basic009", "basic010",
        "basic011", "basic012", "basic013", "basic014", "basic015",
@@ -42,19 +44,19 @@ idrisTests
        "basic031", "basic032", "basic033", "basic034", "basic035",
        "basic036", "basic037", "basic038", "basic039", "basic040",
        "basic041", "basic042", "basic043", "basic044", "basic045",
-       "basic046", "basic047", "basic048",
+       "basic046", "basic047", "basic048", "basic049",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",
-       "coverage009", "coverage010",
+       "coverage009", "coverage010", "coverage011",
        -- Documentation strings
        "docs001", "docs002",
        -- Evaluator
-       "evaluator001", "evaluator002", "evaluator003",
+       "evaluator001", "evaluator002", "evaluator003", "evaluator004",
        -- Error messages
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",
-       "error011", "error012", "error013",
+       "error011", "error012", "error013", "error014",
        -- Modules and imports
        "import001", "import002", "import003", "import004", "import005",
        -- Interactive editing support
@@ -82,14 +84,14 @@ idrisTests
        "literate001", "literate002", "literate003", "literate004",
        "literate005", "literate006", "literate007", "literate008",
        "literate009", "literate010", "literate011", "literate012",
-       "literate013", "literate014",
+       "literate013", "literate014", "literate015", "literate016",
        -- Namespace blocks
        "namespace001",
        -- Parameters blocks
        "params001",
        -- Performance: things which have been slow in the past, or which
        -- pose interesting challenges for the elaborator
-       "perf001", "perf002", "perf003", "perf004", "perf005",
+       "perf001", "perf002", "perf003", "perf004", "perf005", "perf006",
        -- Parse errors
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006",
@@ -121,15 +123,15 @@ idrisTests
        -- with-disambiguation
        "with003"]
 
-typeddTests : List String
-typeddTests
-   = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
+typeddTests : TestPool
+typeddTests = MkTestPool []
+     ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
       "chapter06", "chapter07", "chapter08", "chapter09", "chapter10",
       "chapter11", "chapter12", "chapter13", "chapter14"]
 
-chezTests : List String
-chezTests
-   = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
+chezTests : TestPool
+chezTests = MkTestPool [Chez]
+     ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
       "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
       "chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
       "chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
@@ -138,9 +140,9 @@ chezTests
       "perf001",
       "reg001"]
 
-nodeTests : List String
-nodeTests
-  = [ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009"
+nodeTests : TestPool
+nodeTests = MkTestPool [Node]
+    [ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009"
     , "node011", "node012", "node015", "node017", "node018", "node019" -- node014
     , "node021", "node022" --, "node020"
     , "reg001"
@@ -149,209 +151,29 @@ nodeTests
     , "idiom001"
     ]
 
-ideModeTests : List String
-ideModeTests
-  =  [ "ideMode001", "ideMode002", "ideMode003", "ideMode004" ]
+ideModeTests : TestPool
+ideModeTests = MkTestPool []
+  [ "ideMode001", "ideMode002", "ideMode003", "ideMode004" ]
 
-preludeTests : List String
-preludeTests
-  =  [ "reg001" ]
+preludeTests : TestPool
+preludeTests = MkTestPool []
+  [ "reg001" ]
 
-------------------------------------------------------------------------
--- Options
-
-||| Options for the test driver.
-record Options where
-  constructor MkOptions
-  ||| Name of the idris2 executable
-  idris2      : String
-  ||| Should we only run some specific cases?
-  onlyNames   : List String
-  ||| Should we run the test suite interactively?
-  interactive : Bool
-
-usage : String
-usage = "Usage: runtests <idris2 path> [--interactive] [--only [NAMES]]"
-
-options : List String -> Maybe Options
-options args = case args of
-    (_ :: idris2 :: rest) => go rest (MkOptions idris2 [] False)
-    _ => Nothing
-
-  where
-
-    go : List String -> Options -> Maybe Options
-    go rest opts = case rest of
-      []                      => pure opts
-      ("--interactive" :: xs) => go xs (record { interactive = True } opts)
-      ("--only" :: xs)        => pure $ record { onlyNames = xs } opts
-      _ => Nothing
-
-------------------------------------------------------------------------
--- Actual test runner
-
-fail : String -> IO ()
-fail err
-    = do putStrLn err
-         exitWith (ExitFailure 1)
-
--- on Windows, we just ignore backslashes and slashes when comparing,
--- similarity up to that is good enough. Leave errors that depend
--- on the confusion of slashes and backslashes to unix machines.
-normalize : String -> String
-normalize str =
-    if isWindows
-      then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
-      else str
-
-runTest : Options -> String -> IO Bool
-runTest opts testPath
-    = do changeDir testPath
-         isSuccess <- runTest'
-         changeDir "../.."
-         pure isSuccess
-    where
-        getAnswer : IO Bool
-        getAnswer = do
-          str <- getLine
-          case str of
-            "y" => pure True
-            "n" => pure False
-            _   => do putStrLn "Invalid Answer."
-                      getAnswer
-
-        printExpectedVsOutput : String -> String -> IO ()
-        printExpectedVsOutput exp out = do
-          putStrLn "Expected:"
-          printLn exp
-          putStrLn "Given:"
-          printLn out
-
-        mayOverwrite : Maybe String -> String -> IO ()
-        mayOverwrite mexp out = do
-          the (IO ()) $ case mexp of
-            Nothing => putStr $ unlines
-              [ "Golden value missing. I computed the following result:"
-              , out
-              , "Accept new golden value? [yn]"
-              ]
-            Just exp => do
-              putStrLn "Golden value differs from actual value."
-              code <- system "git diff --no-index --exit-code --word-diff=color expected output"
-              when (code < 0) $ printExpectedVsOutput exp out
-              putStrLn "Accept actual value as new golden value? [yn]"
-          b <- getAnswer
-          when b $ do Right _ <- writeFile "expected" out
-                          | Left err => print err
-                      pure ()
-        runTest' : IO Bool
-        runTest'
-            = do putStr $ testPath ++ ": "
-                 system $ "sh ./run " ++ idris2 opts ++ " | tr -d '\\r' > output"
-                 Right out <- readFile "output"
-                     | Left err => do print err
-                                      pure False
-                 Right exp <- readFile "expected"
-                     | Left FileNotFound => do
-                         if interactive opts
-                           then mayOverwrite Nothing out
-                           else print FileNotFound
-                         pure False
-                     | Left err => do print err
-                                      pure False
-                 let result = normalize out == normalize exp
-                 if result
-                    then putStrLn "success"
-                    else do
-                      putStrLn "FAILURE"
-                      if interactive opts
-                         then mayOverwrite (Just exp) out
-                         else printExpectedVsOutput exp out
-
-                 pure result
-
-exists : String -> IO Bool
-exists f
-    = do Right ok <- openFile f Read
-             | Left err => pure False
-         closeFile ok
-         pure True
-
-firstExists : List String -> IO (Maybe String)
-firstExists [] = pure Nothing
-firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
-
-pathLookup : List String -> IO (Maybe String)
-pathLookup names = do
-  path <- getEnv "PATH"
-  let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
-  let candidates = [p ++ "/" ++ x | p <- pathList,
-                                    x <- names]
-  firstExists candidates
-
-findChez : IO (Maybe String)
-findChez
-    = do Just chez <- getEnv "CHEZ" | Nothing => pathLookup ["chez", "chezscheme9.5", "scheme", "scheme.exe"]
-         pure $ Just chez
-
-findNode : IO (Maybe String)
-findNode
-    = do Just chez <- getEnv "NODE" | Nothing => pathLookup ["node"]
-         pure $ Just chez
-
-runChezTests : Options -> List String -> IO (List Bool)
-runChezTests opts tests
-    = do chexec <- findChez
-         maybe (do putStrLn "Chez Scheme not found"
-                   pure [])
-               (\c => do putStrLn $ "Found Chez Scheme at " ++ c
-                         traverse (runTest opts) tests)
-               chexec
-
-runNodeTests : Options -> List String -> IO (List Bool)
-runNodeTests opts tests
-    = do nodeexec <- findNode
-         maybe (do putStrLn "node not found"
-                   pure [])
-               (\c => do putStrLn $ "Found node at " ++ c
-                         traverse (runTest opts) tests)
-               nodeexec
-
-
-filterTests : Options -> List String -> List String
-filterTests opts = case onlyNames opts of
-  [] => id
-  xs => filter (\ name => any (`isInfixOf` name) xs)
+templateTests : TestPool
+templateTests = MkTestPool []
+  [ "simple-test", "ttimp", "with-ipkg" ]
 
 main : IO ()
-main
-    = do args <- getArgs
-         let (Just opts) = options args
-              | _ => do print args
-                        putStrLn usage
-         let filteredNonCGTests =
-              filterTests opts $ concat $
-                 [ testPaths "ttimp" ttimpTests
-                 , testPaths "idris2" idrisTests
-                 , testPaths "typedd-book" typeddTests
-                 , testPaths "ideMode" ideModeTests
-                 , testPaths "prelude" preludeTests
-                 ]
-         let filteredChezTests = filterTests opts (testPaths "chez" chezTests)
-         let filteredNodeTests = filterTests opts (testPaths "node" nodeTests)
-         nonCGTestRes <- traverse (runTest opts) filteredNonCGTests
-         chezTestRes <- if length filteredChezTests > 0
-              then runChezTests opts filteredChezTests
-              else pure []
-         nodeTestRes <- if length filteredNodeTests > 0
-              then runNodeTests opts filteredNodeTests
-              else pure []
-         let res = nonCGTestRes ++ chezTestRes ++ nodeTestRes
-         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res)
-                       ++ " tests successful")
-         if (any not res)
-            then exitWith (ExitFailure 1)
-            else exitWith ExitSuccess
-    where
-         testPaths : String -> List String -> List String
-         testPaths dir tests = map (\test => dir ++ "/" ++ test) tests
+main = runner
+  [ testPaths "ttimp" ttimpTests
+  , testPaths "idris2" idrisTests
+  , testPaths "typedd-book" typeddTests
+  , testPaths "ideMode" ideModeTests
+  , testPaths "prelude" preludeTests
+  , testPaths "chez" chezTests
+  , testPaths "node" nodeTests
+  , testPaths "templates" templateTests
+  ] where
+
+    testPaths : String -> TestPool -> TestPool
+    testPaths dir = record { testCases $= map ((dir ++ "/") ++) }

tests/README.md

@@ -11,3 +11,5 @@ Examples:
 - `make test only=chez` will run all Chez Scheme tests.
 - `make test only=ttimp/basic` will run all basic tests for `TTImp`.
 - `make test only=idris2/basic001` will run a specific test.
+
+Templates for common test instances can be found in the `templates` folder.

tests/chez/chez027/StringParser.idr

@@ -4,6 +4,7 @@ import Control.Monad.Identity
 import Control.Monad.Trans
 
 import Data.Maybe
+import Data.Vect
 import Data.String.Parser
 
 %default partial
@@ -44,7 +45,7 @@ main = do
     res <- parseT (string "hi") "hiyaaaaaa"
     case res of
         Left err => putStrLn "NOOOOOOO!"
-        Right ((), i) => printLn i
+        Right (_, i) => printLn i
     bad <- parseT (satisfy isDigit) "a"
     showRes bad
     bad2 <- parseT (string "good" <?> "Not good") "bad bad bad"
@@ -62,4 +63,12 @@ main = do
     showRes res
     res <- parseT maybeParser "def"
     showRes res
-    pure ()
+    res <- parseT (commaSep alphaNum) "a,1,b,2"
+    showRes res
+    res <- parseT (ntimes 4 letter) "abcd"
+    showRes res
+    res <- parseT (requireFailure letter) "1"
+    showRes res
+    res <- parseT (requireFailure letter) "a" -- Should error
+    showRes res
+    pure ()

tests/chez/chez027/expected

@@ -9,5 +9,9 @@ Parse failed at position 0: Not good
 ""
 True
 False
+['a', '1', 'b', '2']
+['a', 'b', 'c', 'd']
+()
+Parse failed at position 0: Purposefully changed OK to Fail
 1/1: Building StringParser (StringParser.idr)
 Main> Main> Bye for now!

tests/chez/chez029/BitCasts.idr

@@ -1,6 +1,6 @@
 -- Tests to check that casting between integer types works as expected
 -- 
--- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
+-- The tests in `idris2/basic043`, `chez/chez029` and `node/node022` are the
 -- same and should all have the same output.
 
 --
@@ -93,3 +93,19 @@ negativeNumberCast = [
     show $ cast {to = Bits32} (-19),
     show $ cast {to = Bits64} (-19)
 ]
+
+--
+-- Run via code generator
+--
+
+main : IO ()
+main = do
+    printLn bits8WideningNoEffect
+    printLn bits16WideningNoEffect
+    printLn bits32WideningNoEffect
+    printLn narrowFromInteger
+    printLn narrowFromInt
+    printLn narrowFromBits64
+    printLn narrowFromBits32
+    printLn narrowFromBits16
+    printLn negativeNumberCast

tests/chez/chez029/expected

@@ -1,11 +1,11 @@
+["123", "123", "123", "123", "123"]
+["1234", "1234", "1234", "1234"]
+["1234567", "1234567", "1234567"]
+["134", "134", "134", "134"]
+["134", "134", "134", "134"]
+["134", "134", "134"]
+["134", "134"]
+["134"]
+["237", "65517", "4294967277", "18446744073709551597"]
 1/1: Building BitCasts (BitCasts.idr)
-Main> ["123", "123", "123", "123", "123"]
-Main> ["1234", "1234", "1234", "1234"]
-Main> ["1234567", "1234567", "1234567"]
-Main> ["134", "134", "134", "134"]
-Main> ["134", "134", "134", "134"]
-Main> ["134", "134", "134"]
-Main> ["134", "134"]
-Main> ["134"]
-Main> ["237", "65517", "4294967277", "18446744073709551597"]
-Main> Bye for now!
+Main> Main> Bye for now!

tests/chez/chez029/input

@@ -1,10 +1,2 @@
-bits8WideningNoEffect
-bits16WideningNoEffect
-bits32WideningNoEffect
-narrowFromInteger
-narrowFromInt
-narrowFromBits64
-narrowFromBits32
-narrowFromBits16
-negativeNumberCast
+:exec main
 :q

tests/chez/chez031/expected

@@ -1,33 +1,29 @@
 Error: The given specifier was not accepted by any backend. Available backends:
-  chez, racket, node, javascript, gambit
+  chez, racket, node, javascript, refc, gambit
 Some backends have additional specifier rules, refer to their documentation.
 
-Specifiers.idr:29:1--34:5
+Specifiers.idr:29:1--30:35
  29 | %foreign "scheme,racket:+"
  30 | plusRacketFail : Int -> Int -> Int
- 31 | 
- 32 | -- We don't actually do any printing this is just to use the specifiers so the
- 33 | -- failures are exposed.
- 34 | main : IO ()
 
 Error: The given specifier was not accepted by any backend. Available backends:
-  chez, racket, node, javascript, gambit
+  chez, racket, node, javascript, refc, gambit
 Some backends have additional specifier rules, refer to their documentation.
 
-Specifiers.idr:29:1--34:5
+Specifiers.idr:29:1--30:35
 
 Main> Loaded file Specifiers.idr
 Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
-  chez, racket, node, javascript, gambit
+  chez, racket, node, javascript, refc, gambit
 Some backends have additional specifier rules, refer to their documentation.
 
-Specifiers.idr:29:1--34:5
+Specifiers.idr:29:1--30:35
 
 Specifiers> [exec] Specifiers> Error: The given specifier was not accepted by any backend. Available backends:
-  chez, racket, node, javascript, gambit
+  chez, racket, node, javascript, refc, gambit
 Some backends have additional specifier rules, refer to their documentation.
 
-Specifiers.idr:29:1--34:5
+Specifiers.idr:29:1--30:35
 
 [exec] Specifiers> 
 Bye for now!

tests/ideMode/ideMode001/expected

@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:295} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:296}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:295}_[] ?{_:296}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:372} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:373}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:372}_[] ?{_:373}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:374}_[] ?{_:373}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:363}_[] ?{_:362}_[])")))))) 1)
+0001ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:353} : (Main.Vect n[0] a[1])) -> ({arg:354} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

tests/ideMode/ideMode003/expected

@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:295} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:296}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:295}_[] ?{_:296}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:372} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:373}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:372}_[] ?{_:373}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:374}_[] ?{_:373}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:363}_[] ?{_:362}_[])")))))) 1)
+0001ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:353} : (Main.Vect n[0] a[1])) -> ({arg:354} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

tests/idris2/basic043/BitCasts.idr

@@ -1,6 +1,6 @@
 -- Tests to check that casting between integer types works as expected
 -- 
--- This tests in `idris2/basic043`, `chez/chez028` and `node/node022` are the
+-- The tests in `idris2/basic043`, `chez/chez029` and `node/node022` are the
 -- same and should all have the same output.
 
 --

tests/idris2/basic044/expected

@@ -98,7 +98,7 @@ Term> Bye for now!
 LOG declare.type:1: Processing Vec.Vec
 LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1])
 LOG declare.type:1: Processing Vec.Nil
-LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] ?Vec.{t:N}_[{arg:N}[0]] Data.Fin.Uninhabited implementation at Data/Fin.idr:19:1--24:7)
+LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] ?Vec.{t:N}_[{arg:N}[0]] Data.Fin.Uninhabited implementation at Data/Fin.idr:19:1--22:32)
 LOG declare.type:1: Processing Vec.::
 LOG declare.def:2: Case tree for Vec.::: case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
  { Data.Fin.FZ {e:N} => [0] {arg:N}[3]

tests/idris2/basic048/Module'.idr

@@ -0,0 +1,7 @@
+module Module'
+
+function' : Int -> Int
+function' x = x + 1
+
+main : IO ()
+main = printLn . show $ function' 4

tests/idris2/basic048/expected

@@ -1,15 +1,7 @@
-1/1: Building Fld (Fld.idr)
-Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
-    Main.R2.MkR
-    Main.R1.MkR Type
-
-Fld.idr:72:26--72:29
-    |
- 72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
-    |                          ^^^
-
-Main> Main.myDog : OrdinaryDog
-Main> Main.mySuperDog : SuperDog
-Main> Main.other : Other String
-Main> 1 hole: Main.r2_shouldNotTypecheck1
-Main> Bye for now!
+1/1: Building Module' (Module'.idr)
+Module'> 2
+Module'> Bye for now!
+"5"
+Module'> Loaded file Module'.idr
+Module'> 
+Bye for now!

tests/idris2/basic048/input

@@ -1,5 +1,2 @@
-:t myDog
-:t mySuperDog
-:t other
-:m
+function' 1
 :q

tests/idris2/basic048/input-ed

@@ -0,0 +1 @@
+:e

tests/idris2/basic048/run

@@ -1,3 +1,5 @@
-$1 --no-color --console-width 0 --no-banner Fld.idr < input
+$1 --no-banner --no-color --console-width 0 "Module'.idr" < input
+$1 --exec main --cg ${IDRIS2_TESTS_CG} "Module'.idr"
+EDITOR=true $1 --no-banner --no-color --console-width 0 "Module'.idr" < input-ed
 
 rm -rf build

tests/idris2/basic049/expected

@@ -0,0 +1,15 @@
+1/1: Building Fld (Fld.idr)
+Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
+    Main.R2.MkR
+    Main.R1.MkR Type
+
+Fld.idr:72:26--72:29
+    |
+ 72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
+    |                          ^^^
+
+Main> Main.myDog : OrdinaryDog
+Main> Main.mySuperDog : SuperDog
+Main> Main.other : Other String
+Main> 1 hole: Main.r2_shouldNotTypecheck1
+Main> Bye for now!

tests/idris2/basic049/input

@@ -0,0 +1,5 @@
+:t myDog
+:t mySuperDog
+:t other
+:m
+:q

tests/idris2/basic049/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner Fld.idr < input
+
+rm -rf build

tests/idris2/coverage010/expected

@@ -1,8 +1,9 @@
 1/1: Building casetot (casetot.idr)
 Error: main is not covering.
 
-casetot.idr:12:1--13:5
+casetot.idr:12:1--12:13
+    |
  12 | main : IO ()
- 13 | main = do
+    | ^^^^^^^^^^^^
 
 Calls non covering function Main.case block in case block in main

tests/idris2/coverage011/Sing.idr

@@ -0,0 +1,13 @@
+module Sing
+
+%default total
+
+data Fing : Type -> Type where
+  StringFing : String -> Fing String
+  BoolFing : Bool -> Fing Bool
+
+stringFing : Fing String -> String
+stringFing (StringFing s) = s
+
+boolFing : Fing Bool -> Bool
+boolFing (BoolFing b) = b

tests/idris2/coverage011/expected

@@ -0,0 +1 @@
+1/1: Building Sing (Sing.idr)

tests/idris2/coverage011/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --check Sing.idr
+
+rm -rf build

tests/idris2/error004/expected

@@ -16,8 +16,8 @@ Error2.idr:13:38--13:45
     |                                      ^^^^^^^
 
 Possible correct results:
-    Show implementation at Error2.idr:11:1--15:6
-    Show implementation at Error2.idr:7:1--11:5
+    Show implementation at Error2.idr:11:1--13:45
+    Show implementation at Error2.idr:7:1--9:45
 Error: While processing right hand side of wrong. Multiple solutions found in search of:
     Show (Vect 1 Integer)
 
@@ -27,5 +27,5 @@ Error2.idr:16:9--16:34
     |         ^^^^^^^^^^^^^^^^^^^^^^^^^
 
 Possible correct results:
-    Show implementation at Error2.idr:11:1--15:6
-    Show implementation at Error2.idr:7:1--11:5
+    Show implementation at Error2.idr:11:1--13:45
+    Show implementation at Error2.idr:7:1--9:45

tests/idris2/error013/expected

@@ -1,21 +1,22 @@
 1/1: Building Issue361 (Issue361.idr)
-Error: main is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361.idr:5:1--7:5 -> Main.== -> Main./= -> Main.==
+Error: main is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361.idr:5:1--5:11 -> Main.== -> Main./= -> Main.==
 
-Issue361.idr:7:1--8:5
+Issue361.idr:7:1--7:13
+   |
  7 | main : IO ()
- 8 | main = printLn $ T == T
+   | ^^^^^^^^^^^^
 
 Error: /= is not total, possibly not terminating due to recursive path Main./= -> Main.== -> Main./= -> Main.==
 
-Issue361.idr:5:1--7:5
+Issue361.idr:5:1--5:11
+   |
  5 | Eq S where
- 6 | 
- 7 | main : IO ()
+   | ^^^^^^^^^^
 
 Error: == is not total, possibly not terminating due to call to Main./=
 
-Issue361.idr:5:1--7:5
+Issue361.idr:5:1--5:11
+   |
  5 | Eq S where
- 6 | 
- 7 | main : IO ()
+   | ^^^^^^^^^^