Merge branch 'master' of github.com:idris-lang/Idris2 into javascript

.github/workflows/ci-full-bootstrap.yml

@@ -0,0 +1,38 @@
+name: Idris bootstrap
+on:
+  push:
+    branches:
+      - master
+    tags:
+      - '*'
+
+env:
+  SCHEME: scheme
+jobs:
+  build:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v2
+      - name: Install build dependencies
+        run: |
+          sudo apt-get install -y chezscheme zlib1g-dev ghc cabal-install
+          cabal update
+          echo "::add-path::$HOME/.idris2/bin"
+          echo "::add-path::$HOME/.cabal/bin"
+      - name: Get Idris2-boot
+        run: |
+          cd $HOME && git clone https://github.com/edwinb/Idris2-boot
+      - name: Install Idris 1
+        run: cabal v1-install idris
+      - name: Build Idris2-boot
+        run: cd $HOME/Idris2-boot && make && make install
+      - name: Build from bootstrap
+        run: |
+          make all IDRIS2_BOOT=$HOME/.idris2boot/bin/idris2boot
+          make install
+        shell: bash
+      - name: Build and test self-hosted
+        run: make clean && make all && make test INTERACTIVE=''
+        shell: bash
+

.github/workflows/ci-windows.yml

@@ -18,6 +18,9 @@ jobs:
   build:
     runs-on: windows-latest
     steps:
+      - name: Init
+        run: |
+          git config --global core.autocrlf false
       - name: Checkout
         uses: actions/checkout@v2
       - name: Get Chez Scheme

CHANGELOG.md

@@ -18,6 +18,15 @@ Language changes:
      invoking elaborator scripts. This means the function must always
      be fully applied, and is run under `%runElab`
 
+Library changes:
+
+* Experimental `Data.Linear.Array` added to `contrib`, support mutable linear
+  arrays with constant time read/write, convertible to immutable arrays with
+  constant time read.
+   + Anything in `Data.Linear` in `contrib`, just like the rest of `contrib`,
+     should be considered experimental with the API able to change at any time!
+     Further experiments in `Data.Linear` are welcome :).
+
 Changes since Idris 2 v0.1.0
 ----------------------------
 

README.md

@@ -6,6 +6,7 @@ Idris 2
 [![](https://github.com/idris-lang/Idris2/workflows/Ubuntu/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Ubuntu")
 [![](https://github.com/idris-lang/Idris2/workflows/Ubuntu%20Racket/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Ubuntu+Racket")
 [![](https://github.com/idris-lang/Idris2/workflows/macOS/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"macOS")
+[![](https://github.com/idris-lang/Idris2/workflows/Idris%20bootstrap/badge.svg)](https://github.com/idris-lang/Idris2/actions?query=workflow%3A"Idris+bootstrap")
 
 [Idris 2](https://idris-lang.org/) is a purely functional programming language
 with first class types.

docs/source/app/linear.rst

@@ -83,7 +83,7 @@ access the resource directly:
 .. code-block:: idris
 
     data Res : (a : Type) -> (a -> Type) -> Type where
-         (@@) : (val : a) -> (1 resource : r val) -> Res a r
+         (#) : (val : a) -> (1 resource : r val) -> Res a r
 
     login : (1 s : Store LoggedOut) -> (password : String) ->
             Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
@@ -91,7 +91,7 @@ access the resource directly:
     readSecret : (1 s : Store LoggedIn) -> 
                  Res String (const (Store LoggedIn))
 
-``Res`` is defined in ``Control.App`` since it is commonly useful.  It is a
+``Res`` is defined in the Prelude, since it is commonly useful.  It is a
 dependent pair type, which associates a value with a linear resource.
 We'll leave the other definitions abstract, for the purposes of this
 introductory example.
@@ -108,10 +108,10 @@ secret data. It uses ``let (>>=) = bindL`` to redefine
           do putStr "Password: "
              password <- getStr
              connect $ \s =>
-               do let True @@ s = login s password
+               do let True # s = login s password
-                    | False @@ s => do putStrLn "Wrong password"
+                    | False # s => do putStrLn "Wrong password"
-                                       disconnect s
+                                      disconnect s
-                  let str @@ s = readSecret s
+                  let str # s = readSecret s
                   putStrLn $ "Secret: " ++ show str
                   let s = logout s
                   disconnect s
@@ -237,10 +237,10 @@ hard coded password and internal data:
 
       login (MkStore str) pwd
           = if pwd == "Mornington Crescent"
-               then pure1 (True @@ MkStore str)
+               then pure1 (True # MkStore str)
-               else pure1 (False @@ MkStore str)
+               else pure1 (False # MkStore str)
       logout (MkStore str) = pure1 (MkStore str)
-      readSecret (MkStore str) = pure1 (str @@ MkStore str)
+      readSecret (MkStore str) = pure1 (str # MkStore str)
 
       disconnect (MkStore _)
           = putStrLn "Door destroyed"

docs/source/typedd/typedd.rst

@@ -204,6 +204,15 @@ views explicit:
            = merge (mergeSort lefts | lrec)
                    (mergeSort rights | rrec)
 
+In the problem 1 of exercise 10-1, the ``rest`` argument of the data
+constructor ``Exact`` of ``TakeN`` must be made explicit.
+
+.. code-block:: idris
+
+    data TakeN : List a -> Type where
+      Fewer : TakeN xs
+      Exact : (n_xs : List a) -> {rest : _} -> TakeN (n_xs ++ rest)
+
 In ``SnocList.idr``, in ``my_reverse``, the link between ``Snoc rec`` and ``xs ++ [x]``
 needs to be made explicit. Idris 1 would happily decide that ``xs`` and ``x`` were
 the relevant implicit arguments to ``Snoc`` but this was little more than a guess

libs/base/Control/App.idr

@@ -339,8 +339,6 @@ HasErr Void e => PrimIO e where
                     $ \_ =>
                MkAppRes (Right ())
 
-infix 5 @@
-
 export
 new1 :  t -> (1 p : State tag t e => App1 {u} e a) -> App1 {u} e a
 new1 val prog
@@ -349,10 +347,6 @@ new1 val prog
             MkApp1 res = prog @{st} in
             res
 
-public export
-data Res : (a : Type) -> (a -> Type) -> Type where
-     (@@) : (val : a) -> (1 r : t val) -> Res a t
-
 public export
 data FileEx = GenericFileEx Int -- errno
             | FileReadError

libs/base/Data/Buffer.idr

@@ -3,6 +3,13 @@ module Data.Buffer
 import System.Directory
 import System.File
 
+-- Reading and writing binary buffers. Note that this primitives are unsafe,
+-- in that they don't check that buffer locations are within bounds.
+-- We really need a safe wrapper!
+-- They are used in the Idris compiler itself for reading/writing checked
+-- files.
+
+-- This is known to the compiler, so maybe ought to be moved to Builtin
 export
 data Buffer : Type where [external]
 
@@ -199,50 +206,58 @@ copyData : (src : Buffer) -> (start, len : Int) ->
 copyData src start len dest loc
     = primIO (prim__copyData src start len dest loc)
 
--- %foreign "scheme:blodwen-readbuffer-bytes"
+%foreign "C:idris2_readBufferData,libidris2_support"
--- prim__readBufferBytes : FilePtr -> AnyPtr -> Int -> Int -> PrimIO Int
+prim__readBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
---
+%foreign "C:idris2_writeBufferData,libidris2_support"
--- export
+prim__writeBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int
--- readBufferFromFile : BinaryFile -> Buffer -> (maxbytes : Int) ->
---                      IO (Either FileError Buffer)
--- readBufferFromFile (FHandle h) (MkBuffer buf size loc) max
---     = do read <- primIO (prim__readBufferBytes h buf loc max)
---          if read >= 0
---             then pure (Right (MkBuffer buf size (loc + read)))
---             else pure (Left FileReadError)
 
-%foreign "scheme:blodwen-read-bytevec"
+export
-prim__readBufferFromFile : String -> String -> PrimIO Buffer
+readBufferData : File -> Buffer ->
+                 (loc : Int) -> -- position in buffer to start adding
+                 (maxbytes : Int) -> -- maximums size to read, which must not
+                                     -- exceed buffer length
+                 IO (Either FileError ())
+readBufferData (FHandle h) buf loc max
+    = do read <- primIO (prim__readBufferData h buf loc max)
+         if read >= 0
+            then pure (Right ())
+            else pure (Left FileReadError)
 
-%foreign "scheme:blodwen-isbytevec"
+export
-prim__isBuffer : Buffer -> Int
+writeBufferData : File -> Buffer ->
+                  (loc : Int) -> -- position in buffer to write from
+                  (maxbytes : Int) -> -- maximums size to write, which must not
+                                      -- exceed buffer length
+                  IO (Either FileError ())
+writeBufferData (FHandle h) buf loc max
+    = do written <- primIO (prim__writeBufferData h buf loc max)
+         if written >= 0
+            then pure (Right ())
+            else pure (Left FileWriteError)
+
+export
+writeBufferToFile : String -> Buffer -> Int -> IO (Either FileError ())
+writeBufferToFile fn buf max
+    = do Right f <- openFile fn WriteTruncate
+             | Left err => pure (Left err)
+         Right ok <- writeBufferData f buf 0 max
+             | Left err => pure (Left err)
+         closeFile f
+         pure (Right ok)
 
--- Create a new buffer by reading all the contents from the given file
--- Fails if no bytes can be read or buffer can't be created
 export
 createBufferFromFile : String -> IO (Either FileError Buffer)
 createBufferFromFile fn
-    = do Just cwd <- currentDir
+    = do Right f <- openFile fn Read
-              | Nothing => pure (Left FileReadError)
+             | Left err => pure (Left err)
-         buf <- primIO (prim__readBufferFromFile cwd fn)
+         Right size <- fileSize f
-         if prim__isBuffer buf /= 0
+             | Left err => pure (Left err)
-            then pure (Left FileReadError)
+         Just buf <- newBuffer size
-            else do let sz = prim__bufferSize buf
+             | Nothing => pure (Left FileReadError)
-                    pure (Right buf)
+         Right ok <- readBufferData f buf 0 size
-
+             | Left err => pure (Left err)
-%foreign "scheme:blodwen-write-bytevec"
+         closeFile f
-prim__writeBuffer : String -> String -> Buffer -> Int -> PrimIO Int
+         pure (Right buf)
-
-export
-writeBufferToFile : String -> Buffer -> (maxbytes : Int) ->
-                    IO (Either FileError ())
-writeBufferToFile fn buf max
-    = do Just cwd <- currentDir
-              | Nothing => pure (Left FileReadError)
-         res <- primIO (prim__writeBuffer cwd fn buf max)
-         if res /= 0
-            then pure (Left FileWriteError)
-            else pure (Right ())
 
 export
 resizeBuffer : Buffer -> Int -> IO (Maybe Buffer)

libs/base/Data/IOArray.idr

@@ -1,17 +1,8 @@
 module Data.IOArray
 
+import Data.IOArray.Prims
 import Data.List
 
--- Implemented externally
-data ArrayData : Type -> Type where
-
--- 'unsafe' primitive access, backend dependent
--- get and set assume that the bounds have been checked. Behavious is undefined
--- otherwise.
-%extern prim__newArray : forall a . Int -> a -> PrimIO (ArrayData a)
-%extern prim__arrayGet : forall a . ArrayData a -> Int -> PrimIO a
-%extern prim__arraySet : forall a . ArrayData a -> Int -> a -> PrimIO ()
-
 export
 record IOArray elem where
   constructor MkIOArray

libs/base/Data/IOArray/Prims.idr

@@ -0,0 +1,11 @@
+module Data.IOArray.Prims
+
+export
+data ArrayData : Type -> Type where [external]
+
+-- 'unsafe' primitive access, backend dependent
+-- get and set assume that the bounds have been checked. Behaviour is undefined
+-- otherwise.
+export %extern prim__newArray : forall a . Int -> a -> PrimIO (ArrayData a)
+export %extern prim__arrayGet : forall a . ArrayData a -> Int -> PrimIO a
+export %extern prim__arraySet : forall a . ArrayData a -> Int -> a -> PrimIO ()

libs/base/Data/List.idr

@@ -33,6 +33,41 @@ drop Z     xs      = xs
 drop (S n) []      = []
 drop (S n) (x::xs) = drop n xs
 
+||| Satisfiable if `k` is a valid index into `xs`
+|||
+||| @ k the potential index
+||| @ xs the list into which k may be an index
+public export
+data InBounds : (k : Nat) -> (xs : List a) -> Type where
+    ||| Z is a valid index into any cons cell
+    InFirst : InBounds Z (x :: xs)
+    ||| Valid indices can be extended
+    InLater : InBounds k xs -> InBounds (S k) (x :: xs)
+
+export
+Uninhabited (InBounds k []) where
+    uninhabited InFirst impossible
+    uninhabited (InLater _) impossible
+
+||| Decide whether `k` is a valid index into `xs`
+export
+inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
+inBounds k [] = No uninhabited
+inBounds Z (x :: xs) = Yes InFirst
+inBounds (S k) (x :: xs) with (inBounds k xs)
+  inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)
+  inBounds (S k) (x :: xs) | (No contra)
+      = No (\p => case p of
+                       InLater y => contra y)
+
+||| Find a particular element of a list.
+|||
+||| @ ok a proof that the index is within bounds
+export
+index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
+index Z (x :: xs) {ok = InFirst} = x
+index (S k) (x :: xs) {ok = (InLater p)} = index k xs
+
 ||| Generate a list by repeatedly applying a partial function until exhausted.
 ||| @ f the function to iterate
 ||| @ x the initial value that will be the head of the list
@@ -595,7 +630,7 @@ revOnto xs [] = Refl
 revOnto xs (v :: vs)
     = rewrite revOnto (v :: xs) vs in
         rewrite appendAssociative (reverse vs) [v] xs in
-				  rewrite revOnto [v] vs in Refl
+                                  rewrite revOnto [v] vs in Refl
 
 export
 revAppend : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)

libs/base/Data/Nat.idr

@@ -466,8 +466,8 @@ multDistributesOverMinusRight left centre right =
 
 -- power proofs
 
-multPowerPowerPlus : (base, exp, exp' : Nat) ->
+-- multPowerPowerPlus : (base, exp, exp' : Nat) ->
-  power base (exp + exp') = (power base exp) * (power base exp')
+--   power base (exp + exp') = (power base exp) * (power base exp')
 -- multPowerPowerPlus base Z       exp' =
 --     rewrite sym $ plusZeroRightNeutral (power base exp') in Refl
 -- multPowerPowerPlus base (S exp) exp' =
@@ -475,21 +475,21 @@ multPowerPowerPlus : (base, exp, exp' : Nat) ->
 --     rewrite sym $ multAssociative base (power base exp) (power base exp') in
 --       Refl
 
-powerOneNeutral : (base : Nat) -> power base 1 = base
+--powerOneNeutral : (base : Nat) -> power base 1 = base
-powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
+--powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
-
+--
-powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
+--powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
-powerOneSuccOne Z       = Refl
+--powerOneSuccOne Z       = Refl
-powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
+--powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
-
+--
-powerPowerMultPower : (base, exp, exp' : Nat) ->
+--powerPowerMultPower : (base, exp, exp' : Nat) ->
-  power (power base exp) exp' = power base (exp * exp')
+--  power (power base exp) exp' = power base (exp * exp')
-powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
+--powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
-powerPowerMultPower base exp (S exp') =
+--powerPowerMultPower base exp (S exp') =
-  rewrite powerPowerMultPower base exp exp' in
+--  rewrite powerPowerMultPower base exp exp' in
-  rewrite multRightSuccPlus exp exp' in
+--  rewrite multRightSuccPlus exp exp' in
-  rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
+--  rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
-          Refl
+--          Refl
 
 -- minimum / maximum proofs
 
@@ -506,7 +506,7 @@ maximumCommutative Z (S _) = Refl
 maximumCommutative (S _) Z = Refl
 maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl
 
-maximumIdempotent : (n : Nat) -> maximum n n = n
+-- maximumIdempotent : (n : Nat) -> maximum n n = n
 -- maximumIdempotent Z = Refl
 -- maximumIdempotent (S k) = cong $ maximumIdempotent k
 
@@ -523,7 +523,7 @@ minimumCommutative Z (S _) = Refl
 minimumCommutative (S _) Z = Refl
 minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl
 
-minimumIdempotent : (n : Nat) -> minimum n n = n
+-- minimumIdempotent : (n : Nat) -> minimum n n = n
 -- minimumIdempotent Z = Refl
 -- minimumIdempotent (S k) = cong (minimumIdempotent k)
 
@@ -541,18 +541,18 @@ maximumSuccSucc : (left, right : Nat) ->
   S (maximum left right) = maximum (S left) (S right)
 maximumSuccSucc _ _ = Refl
 
-sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
+-- sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
 -- sucMaxL Z = Refl
 -- sucMaxL (S l) = cong $ sucMaxL l
 
-sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
+-- sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
 -- sucMaxR Z = Refl
 -- sucMaxR (S l) = cong $ sucMaxR l
 
-sucMinL : (l : Nat) -> minimum (S l) l = l
+-- sucMinL : (l : Nat) -> minimum (S l) l = l
 -- sucMinL Z = Refl
 -- sucMinL (S l) = cong $ sucMinL l
 
-sucMinR : (l : Nat) -> minimum l (S l) = l
+-- sucMinR : (l : Nat) -> minimum l (S l) = l
 -- sucMinR Z = Refl
 -- sucMinR (S l) = cong $ sucMinR l

libs/base/System/File.idr

@@ -2,6 +2,7 @@ module System.File
 
 import Data.List
 import Data.Strings
+import System.Info
 
 public export
 data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend
@@ -68,12 +69,12 @@ prim__stderr : FilePtr
 prim__chmod : String -> Int -> PrimIO Int
 
 modeStr : Mode -> String
-modeStr Read              = "r"
+modeStr Read              = if isWindows then "rb" else "r"
-modeStr WriteTruncate     = "w"
+modeStr WriteTruncate     = if isWindows then "wb" else "w"
-modeStr Append            = "a"
+modeStr Append            = if isWindows then "ab" else "a"
-modeStr ReadWrite         = "r+"
+modeStr ReadWrite         = if isWindows then "rb+" else "r+"
-modeStr ReadWriteTruncate = "w+"
+modeStr ReadWriteTruncate = if isWindows then "wb+" else "w+"
-modeStr ReadAppend        = "a+"
+modeStr ReadAppend        = if isWindows then "ab+" else "a+"
 
 public export
 data FileError = GenericFileError Int -- errno

libs/base/base.ipkg

@@ -13,6 +13,7 @@ modules = Control.App,
           Data.Either,
           Data.Fin,
           Data.IOArray,
+          Data.IOArray.Prims,
           Data.IORef,
           Data.List,
           Data.List.Elem,

libs/contrib/Data/Linear/Array.idr

@@ -0,0 +1,74 @@
+module Data.Linear.Array
+
+import Data.IOArray
+
+-- Linear arrays. General idea: mutable arrays are constructed linearly,
+-- using newArray. Once everything is set up, they can be converted to
+-- read only arrays with constant time, pure, access, using toIArray.
+
+-- Immutable arrays which can be read in constant time, but not updated
+public export
+interface Array arr where
+  read : (1 _ : arr t) -> Int -> Maybe t
+  size : (1 _ : arr t) -> Int
+
+-- Mutable arrays which can be used linearly
+public export
+interface Array arr => MArray arr where
+  newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> a) -> a
+  -- Array is unchanged if the index is out of bounds
+  write : (1 _ : arr t) -> Int -> t -> arr t
+
+  mread : (1 _ : arr t) -> Int -> LPair (Maybe t) (arr t)
+  msize : (1 _ : arr t) -> LPair Int (arr t)
+
+export
+data IArray : Type -> Type where
+     MkIArray : IOArray t -> IArray t
+
+export
+data LinArray : Type -> Type where
+     MkLinArray : IOArray t -> LinArray t
+
+-- Convert a mutable array to an immutable array
+export
+toIArray : (1 _ : LinArray t) -> (IArray t -> a) -> a
+toIArray (MkLinArray arr) k = k (MkIArray arr)
+
+export
+Array LinArray where
+  read (MkLinArray a) i = unsafePerformIO (readArray a i)
+  size (MkLinArray a) = max a
+
+export
+MArray LinArray where
+  newArray size k = k (MkLinArray (unsafePerformIO (newArray size)))
+
+  write (MkLinArray a) i el
+      = unsafePerformIO (do writeArray a i el
+                            pure (MkLinArray a))
+  msize (MkLinArray a) = max a # MkLinArray a
+  mread (MkLinArray a) i
+      = unsafePerformIO (readArray a i) # MkLinArray a
+
+export
+Array IArray where
+  read (MkIArray a) i = unsafePerformIO (readArray a i)
+  size (MkIArray a) = max a
+
+export
+copyArray : MArray arr => (newsize : Int) -> (1 _ : arr t) -> (arr t, arr t)
+copyArray newsize a
+    = let size # a = msize a in
+          newArray newsize $
+            (\a' => copyContent (min (newsize - 1) (size - 1)) a a')
+  where
+    copyContent : Int -> (1 _ : arr t) -> (1 _ : arr t) -> (arr t, arr t)
+    copyContent pos a a'
+        = if pos < 0
+             then (a, a')
+             else let val # a = mread a pos
+                      1 a' = case val of
+                                  Nothing => a'
+                                  Just v => write a' pos v in
+                      copyContent (pos - 1) a a'

libs/contrib/contrib.ipkg

@@ -2,6 +2,8 @@ package contrib
 
 modules = Control.Delayed,
 
+          Data.Linear.Array,
+
           Data.List.TailRec,
           Data.List.Equalities,
           Data.List.Reverse,

libs/network/Network/Socket.idr

@@ -173,10 +173,10 @@ recvAll sock = recvRec sock [] 64
     recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String)
     recvRec sock acc n = do res <- recv sock n
                             case res of
-                              Left 0 => pure (Right $ concat $ reverse acc)
                               Left c => pure (Left c)
-                              Right (str, _) => let n' = min (n * 2) 65536 in
+                              Right (str, res) => let n' = min (n * 2) 65536 in
-                                                recvRec sock (str :: acc) n'
+                                                  if res < n then pure (Right $ concat $ reverse $ str :: acc)
+                                                  else recvRec sock (str :: acc) n'
 
 ||| Send a message.
 |||

libs/prelude/Builtin.idr

@@ -67,22 +67,36 @@ snd (x, y) = y
 -- This directive tells auto implicit search what to use to look inside pairs
 %pair Pair fst snd
 
-||| Dependent pairs aid in the construction of dependent types by providing
+infix 5 #
-||| evidence that some value resides in the type.
+
-|||
+||| A pair type for use in operations on linear resources, which return a
-||| Formally, speaking, dependent pairs represent existential quantification -
+||| value and an updated resource
-||| they consist of a witness for the existential claim and a proof that the
+public export
-||| property holds for it.
+data LPair : Type -> Type -> Type where
-|||
+     (#) : (x : a) -> (1 _ : b) -> LPair a b
-||| @ a the value to place in the type.
+
-||| @ p the dependent type that requires the value.
 namespace DPair
+  ||| Dependent pairs aid in the construction of dependent types by providing
+  ||| evidence that some value resides in the type.
+  |||
+  ||| Formally, speaking, dependent pairs represent existential quantification -
+  ||| they consist of a witness for the existential claim and a proof that the
+  ||| property holds for it.
+  |||
+  ||| @ a the value to place in the type.
+  ||| @ p the dependent type that requires the value.
   public export
   record DPair a (p : a -> Type) where
     constructor MkDPair
     fst : a
     snd : p fst
 
+  ||| A dependent variant of LPair, pairing a result value with a resource
+  ||| that depends on the result value
+  public export
+  data Res : (a : Type) -> (a -> Type) -> Type where
+       (#) : (val : a) -> (1 r : t val) -> Res a t
+
 -- The empty type
 
 ||| The empty type, also known as the trivially false proposition.

src/Compiler/CompileExpr.idr

@@ -462,6 +462,7 @@ data NArgs : Type where
      NUnit : NArgs
      NPtr : NArgs
      NGCPtr : NArgs
+     NBuffer : NArgs
      NIORes : Closure [] -> NArgs
 
 getPArgs : Defs -> Closure [] -> Core (String, Closure [])
@@ -494,6 +495,7 @@ getNArgs defs (NS _ (UN "Ptr")) [arg] = pure NPtr
 getNArgs defs (NS _ (UN "AnyPtr")) [] = pure NPtr
 getNArgs defs (NS _ (UN "GCPtr")) [arg] = pure NGCPtr
 getNArgs defs (NS _ (UN "GCAnyPtr")) [] = pure NGCPtr
+getNArgs defs (NS _ (UN "Buffer")) [] = pure NBuffer
 getNArgs defs (NS _ (UN "Unit")) [] = pure NUnit
 getNArgs defs (NS _ (UN "Struct")) [n, args]
     = do NPrimVal _ (Str n') <- evalClosure defs n
@@ -540,6 +542,7 @@ nfToCFType _ s (NTCon fc n_in _ _ args)
               NUnit => pure CFUnit
               NPtr => pure CFPtr
               NGCPtr => pure CFGCPtr
+              NBuffer => pure CFBuffer
               NIORes uarg =>
                 do narg <- evalClosure defs uarg
                    carg <- nfToCFType fc s narg

src/Compiler/Scheme/Chez.idr

@@ -109,7 +109,8 @@ mutual
   tySpec (NmCon fc (UN "Char") _ []) = pure "char"
   tySpec (NmCon fc (NS _ n) _ [_])
      = cond [(n == UN "Ptr", pure "void*"),
-             (n == UN "GCPtr", pure "void*")]
+             (n == UN "GCPtr", pure "void*"),
+             (n == UN "Buffer", pure "u8*")]
           (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
   tySpec (NmCon fc (NS _ n) _ [])
      = cond [(n == UN "Unit", pure "void"),
@@ -182,6 +183,7 @@ cftySpec fc CFDouble = pure "double"
 cftySpec fc CFChar = pure "char"
 cftySpec fc CFPtr = pure "void*"
 cftySpec fc CFGCPtr = pure "void*"
+cftySpec fc CFBuffer = pure "u8*"
 cftySpec fc (CFFun s t) = pure "void*"
 cftySpec fc (CFIORes t) = cftySpec fc t
 cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
@@ -196,6 +198,10 @@ cCall appdir fc cfn clib args (CFIORes CFGCPtr)
     = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
 cCall appdir fc cfn clib args CFGCPtr
     = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
+cCall appdir fc cfn clib args (CFIORes CFBuffer)
+    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
+cCall appdir fc cfn clib args CFBuffer
+    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
 cCall appdir fc cfn clib args ret
     = do loaded <- get Loaded
          lib <- if clib `elem` loaded

src/Compiler/Scheme/Racket.idr

@@ -122,6 +122,7 @@ cftySpec fc CFDouble = pure "_double"
 cftySpec fc CFChar = pure "_int8"
 cftySpec fc CFPtr = pure "_pointer"
 cftySpec fc CFGCPtr = pure "_pointer"
+cftySpec fc CFBuffer = pure "_bytes"
 cftySpec fc (CFIORes t) = cftySpec fc t
 cftySpec fc (CFStruct n t) = pure $ "_" ++ n ++ "-pointer"
 cftySpec fc (CFFun s t) = funTySpec [s] t
@@ -172,6 +173,10 @@ cCall appdir fc cfn clib args (CFIORes CFGCPtr)
     = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
 cCall appdir fc cfn clib args CFGCPtr
     = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
+cCall appdir fc cfn clib args (CFIORes CFBuffer)
+    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
+cCall appdir fc cfn clib args CFBuffer
+    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
 cCall appdir fc cfn libspec args ret
     = do loaded <- get Loaded
          bound <- get Done

src/Core/AutoSearch.idr

@@ -147,15 +147,15 @@ anyOne fc env top (elab :: elabs)
 exactlyOne : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
-             FC -> Env Term vars -> (topTy : ClosedTerm) ->
+             FC -> Env Term vars -> (topTy : ClosedTerm) -> (target : NF vars) ->
              List (Core (Term vars)) ->
              Core (Term vars)
-exactlyOne fc env top [elab]
+exactlyOne fc env top target [elab]
     = catch elab
          (\err => case err of
                        CantSolveGoal _ _ _ => throw err
                        _ => throw (CantSolveGoal fc [] top))
-exactlyOne {vars} fc env top all
+exactlyOne {vars} fc env top target all
     = do elabs <- successful all
          case rights elabs of
               [(res, defs, ust)] =>
@@ -164,7 +164,7 @@ exactlyOne {vars} fc env top all
                        commit
                        pure res
               [] => throw (CantSolveGoal fc [] top)
-              rs => throw (AmbiguousSearch fc env
+              rs => throw (AmbiguousSearch fc env !(quote !(get Ctxt) env target)
                              !(traverse normRes rs))
   where
     normRes : (Term vars, Defs, UState) -> Core (Term vars)
@@ -247,7 +247,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
          findPos defs prf id nty target
   where
     ambig : Error -> Bool
-    ambig (AmbiguousSearch _ _ _) = True
+    ambig (AmbiguousSearch _ _ _ _) = True
     ambig _ = False
 
     clearEnvType : {idx : Nat} -> (0 p : IsVar name idx vs) ->
@@ -307,7 +307,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe
                    then do empty <- clearDefs defs
                            xtytm <- quote empty env xty
                            ytytm <- quote empty env yty
-                           exactlyOne fc env top
+                           exactlyOne fc env top target
                             [(do xtynf <- evalClosure defs xty
                                  findPos defs p
                                      (\arg => apply fc (Ref fc Func fname)
@@ -339,7 +339,7 @@ searchLocal fc rig defaults trying depth def top env target
     = let elabs = map (\t => searchLocalWith fc rig defaults trying depth def
                                              top env t target)
                       (getAllEnv fc rig [] env) in
-          exactlyOne fc env top elabs
+          exactlyOne fc env top target elabs
 
 isPairNF : {auto c : Ref Ctxt Defs} ->
            Env Term vars -> NF vars -> Defs -> Core Bool
@@ -406,7 +406,7 @@ searchNames fc rigc defaults trying depth defining topty env ambig (n :: ns) tar
          let elabs = map (searchName fc rigc defaults trying depth defining topty env target) visns
          if ambig
             then anyOne fc env topty elabs
-            else exactlyOne fc env topty elabs
+            else exactlyOne fc env topty target elabs
   where
     visible : Context ->
               List (List String) -> Name -> Core (Maybe (Name, GlobalDef))
@@ -528,7 +528,7 @@ searchType {vars} fc rigc defaults trying depth def checkdets top env target
                       searchLocal fc rigc defaults trying' depth def top env nty
   where
     ambig : Error -> Bool
-    ambig (AmbiguousSearch _ _ _) = True
+    ambig (AmbiguousSearch _ _ _ _) = True
     ambig _ = False
 
     -- Take the earliest error message (that's when we look inside pairs,

src/Core/Binary.idr

@@ -246,10 +246,6 @@ getSaveDefs (n :: ns) acc defs
                       b <- get Bin
                       getSaveDefs ns ((fullname gdef, b) :: acc) defs
 
-freeDefBuffer : (Name, Binary) -> Core ()
-freeDefBuffer (n, b)
-    = coreLift $ freeBuffer (buf b)
-
 -- Write out the things in the context which have been defined in the
 -- current source file
 export
@@ -283,8 +279,6 @@ writeToTTC extradata fname
 
          Right ok <- coreLift $ writeToFile fname !(get Bin)
                | Left err => throw (InternalError (fname ++ ": " ++ show err))
-         traverse_ freeDefBuffer gdefs
-         freeBinary bin
          pure ()
 
 addGlobalDef : {auto c : Ref Ctxt Defs} ->
@@ -436,8 +430,7 @@ readFromTTC nestedns loc reexp fname modNS importAs
          -- Otherwise, add the data
          let ex = extraData ttc
          if ((modNS, importAs) `elem` map getNSas (allImported defs))
-            then do coreLift $ freeBuffer (buf buffer)
+            then pure (Just (ex, ifaceHash ttc, imported ttc))
-                    pure (Just (ex, ifaceHash ttc, imported ttc))
             else do
                traverse (addGlobalDef modNS as) (context ttc)
                traverse_ addUserHole (userHoles ttc)
@@ -461,7 +454,6 @@ readFromTTC nestedns loc reexp fname modNS importAs
                -- ttc
                ust <- get UST
                put UST (record { nextName = nextVar ttc } ust)
-               coreLift $ freeBuffer (buf buffer)
                pure (Just (ex, ifaceHash ttc, imported ttc))
 
 getImportHashes : String -> Ref Bin Binary ->
@@ -490,10 +482,8 @@ readIFaceHash fname
             | Left err => pure 0
          b <- newRef Bin buffer
          catch (do res <- getHash fname b
-                   coreLift $ freeBuffer (buf buffer)
                    pure res)
-               (\err => do coreLift $ freeBuffer (buf buffer)
+               (\err => pure 0)
-                           pure 0)
 
 export
 readImportHashes : (fname : String) -> -- file containing the module
@@ -503,7 +493,5 @@ readImportHashes fname
             | Left err => pure []
          b <- newRef Bin buffer
          catch (do res <- getImportHashes fname b
-                   coreLift $ freeBuffer (buf buffer)
                    pure res)
-               (\err => do coreLift $ freeBuffer (buf buffer)
+               (\err => pure [])
-                           pure [])

src/Core/CompileExpr.idr

@@ -117,6 +117,7 @@ data CFType : Type where
      CFChar : CFType
      CFPtr : CFType
      CFGCPtr : CFType
+     CFBuffer : CFType
      CFWorld : CFType
      CFFun : CFType -> CFType -> CFType
      CFIORes : CFType -> CFType
@@ -298,6 +299,7 @@ Show CFType where
   show CFChar = "Char"
   show CFPtr = "Ptr"
   show CFGCPtr = "GCPtr"
+  show CFBuffer = "Buffer"
   show CFWorld = "%World"
   show (CFFun s t) = show s ++ " -> " ++ show t
   show (CFIORes t) = "IORes " ++ show t

src/Core/Core.idr

@@ -2,6 +2,7 @@ module Core.Core
 
 import Core.Env
 import Core.TT
+
 import Data.List
 import Data.Vect
 import Parser.Source
@@ -74,7 +75,7 @@ data Error : Type where
      AmbiguousElab : {vars : _} ->
                      FC -> Env Term vars -> List (Term vars) -> Error
      AmbiguousSearch : {vars : _} ->
-                       FC -> Env Term vars -> List (Term vars) -> Error
+                       FC -> Env Term vars -> Term vars -> List (Term vars) -> Error
      AmbiguityTooDeep : FC -> Name -> List Name -> Error
      AllFailed : List (Maybe Name, Error) -> Error
      RecordTypeNeeded : {vars : _} ->
@@ -214,7 +215,7 @@ Show Error where
 
   show (AmbiguousName fc ns) = show fc ++ ":Ambiguous name " ++ show ns
   show (AmbiguousElab fc env ts) = show fc ++ ":Ambiguous elaboration " ++ show ts
-  show (AmbiguousSearch fc env ts) = show fc ++ ":Ambiguous search " ++ show ts
+  show (AmbiguousSearch fc env tgt ts) = show fc ++ ":Ambiguous search " ++ show ts
   show (AmbiguityTooDeep fc n ns)
       = show fc ++ ":Ambiguity too deep in " ++ show n ++ " " ++ show ns
   show (AllFailed ts) = "No successful elaboration: " ++ assert_total (show ts)
@@ -327,7 +328,7 @@ getErrorLoc (BorrowPartial loc _ _ _) = Just loc
 getErrorLoc (BorrowPartialType loc _ _) = Just loc
 getErrorLoc (AmbiguousName loc _) = Just loc
 getErrorLoc (AmbiguousElab loc _ _) = Just loc
-getErrorLoc (AmbiguousSearch loc _ _) = Just loc
+getErrorLoc (AmbiguousSearch loc _ _ _) = Just loc
 getErrorLoc (AmbiguityTooDeep loc _ _) = Just loc
 getErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc x
 getErrorLoc (AllFailed []) = Nothing

src/Core/LinearCheck.idr

@@ -247,7 +247,13 @@ mutual
       unusedHoleArgs _ ty = ty
 
   lcheck rig_in erase env (Bind fc nm b sc)
-      = do (b', bt, usedb) <- lcheckBinder rig erase env b
+      = do (b', bt, usedb) <- handleUnify (lcheckBinder rig erase env b)
+                                 (\err =>
+                                     case err of
+                                          LinearMisuse _ _ r _ =>
+                                             lcheckBinder rig erase env
+                                                (setMultiplicity b linear)
+                                          _ => throw err)
            -- Anything linear can't be used in the scope of a lambda, if we're
            -- checking in general context
            let env' = if rig_in == top

src/Core/Options.idr

@@ -51,6 +51,12 @@ Eq CG where
   Node == Node = True
   _ == _ = False
 
+export
+Show CG where
+  show Chez = "chez"
+  show Racket = "racket"
+  show Gambit = "gambit"
+
 export
 availableCGs : List (String, CG)
 availableCGs
@@ -148,6 +154,7 @@ defaultDirs = MkDirs "." Nothing "build"
 defaultPPrint : PPrinter
 defaultPPrint = MkPPOpts False True False
 
+export
 defaultSession : Session
 defaultSession = MkSessionOpts False False False Chez 0 False False
                                Nothing Nothing Nothing Nothing

src/Core/Primitives.idr

@@ -62,36 +62,44 @@ castInt [NPrimVal fc (Ch i)] = Just (NPrimVal fc (I (cast i)))
 castInt [NPrimVal fc (Str i)] = Just (NPrimVal fc (I (cast i)))
 castInt _ = Nothing
 
+b8max : Int
+b8max = 0x100
+
+b16max : Int
+b16max = 0x10000
+
+b32max : Int
+b32max = 0x100000000
+
+b64max : Integer
+b64max = 18446744073709551616 -- 0x10000000000000000
+
 castBits8 : Vect 1 (NF vars) -> Maybe (NF vars)
 castBits8 [NPrimVal fc (BI i)]
-    = let max = prim__shl_Int 1 8 in
+    = if i > 0 -- oops, we don't have `rem` yet!
-          if i > 0 -- oops, we don't have `rem` yet!
+          then Just (NPrimVal fc (B8 (fromInteger i `mod` b8max)))
-             then Just (NPrimVal fc (B8 (fromInteger i `mod` max)))
+          else Just (NPrimVal fc (B8 (b8max + fromInteger i `mod` b8max)))
-             else Just (NPrimVal fc (B8 (max + fromInteger i `mod` max)))
 castBits8 _ = Nothing
 
 castBits16 : Vect 1 (NF vars) -> Maybe (NF vars)
 castBits16 [NPrimVal fc (BI i)]
-    = let max = prim__shl_Int 1 16 in
+    = if i > 0 -- oops, we don't have `rem` yet!
-          if i > 0 -- oops, we don't have `rem` yet!
+          then Just (NPrimVal fc (B8 (fromInteger i `mod` b16max)))
-             then Just (NPrimVal fc (B16 (fromInteger i `mod` max)))
+          else Just (NPrimVal fc (B8 (b16max + fromInteger i `mod` b16max)))
-             else Just (NPrimVal fc (B16 (max + fromInteger i `mod` max)))
 castBits16 _ = Nothing
 
 castBits32 : Vect 1 (NF vars) -> Maybe (NF vars)
 castBits32 [NPrimVal fc (BI i)]
-    = let max = prim__shl_Int 1 32 in
+    = if i > 0 -- oops, we don't have `rem` yet!
-          if i > 0 -- oops, we don't have `rem` yet!
+          then Just (NPrimVal fc (B8 (fromInteger i `mod` b32max)))
-             then Just (NPrimVal fc (B32 (fromInteger i `mod` max)))
+          else Just (NPrimVal fc (B8 (b32max + fromInteger i `mod` b32max)))
-             else Just (NPrimVal fc (B32 (max + fromInteger i `mod` max)))
 castBits32 _ = Nothing
 
 castBits64 : Vect 1 (NF vars) -> Maybe (NF vars)
 castBits64 [NPrimVal fc (BI i)]
-    = let max = prim__shl_Integer 1 64 in
+    = if i > 0 -- oops, we don't have `rem` yet!
-          if i > 0 -- oops, we don't have `rem` yet!
+          then Just (NPrimVal fc (B64 (i `mod` b64max)))
-             then Just (NPrimVal fc (B64 (i `mod` max)))
+          else Just (NPrimVal fc (B64 (b64max + i `mod` b64max)))
-             else Just (NPrimVal fc (B64 (max + i `mod` max)))
 castBits64 _ = Nothing
 
 castDouble : Vect 1 (NF vars) -> Maybe (NF vars)
@@ -147,13 +155,14 @@ strSubstr [NPrimVal fc (I start), NPrimVal _ (I len), NPrimVal _ (Str str)]
     = Just (NPrimVal fc (Str (prim__strSubstr start len str)))
 strSubstr _ = Nothing
 
+
 add : Constant -> Constant -> Maybe Constant
 add (BI x) (BI y) = pure $ BI (x + y)
 add (I x) (I y) = pure $ I (x + y)
-add (B8 x) (B8 y) = pure $ B8 $ (x + y)
+add (B8 x) (B8 y) = pure $ B8 $ (x + y) `mod` b8max
-add (B16 x) (B16 y) = pure $ B16 $ (x + y) `mod` (prim__shl_Int 1 16)
+add (B16 x) (B16 y) = pure $ B16 $ (x + y) `mod` b16max
-add (B32 x) (B32 y) = pure $ B32 $ (x + y) `mod` (prim__shl_Int 1 32)
+add (B32 x) (B32 y) = pure $ B32 $ (x + y) `mod` b32max
-add (B64 x) (B64 y) = pure $ B64 $ (x + y) `mod` (prim__shl_Integer 1 64)
+add (B64 x) (B64 y) = pure $ B64 $ (x + y) `mod` b64max
 add (Ch x) (Ch y) = pure $ Ch (cast (cast {to=Int} x + cast y))
 add (Db x) (Db y) = pure $ Db (x + y)
 add _ _ = Nothing
@@ -167,10 +176,10 @@ sub _ _ = Nothing
 
 mul : Constant -> Constant -> Maybe Constant
 mul (BI x) (BI y) = pure $ BI (x * y)
-mul (B8 x) (B8 y) = pure $ B8 $ (x * y) `mod` (prim__shl_Int 1 8)
+mul (B8 x) (B8 y) = pure $ B8 $ (x * y) `mod` b8max
-mul (B16 x) (B16 y) = pure $ B16 $ (x * y) `mod` (prim__shl_Int 1 16)
+mul (B16 x) (B16 y) = pure $ B16 $ (x * y) `mod` b16max
-mul (B32 x) (B32 y) = pure $ B32 $ (x * y) `mod` (prim__shl_Int 1 32)
+mul (B32 x) (B32 y) = pure $ B32 $ (x * y) `mod` b32max
-mul (B64 x) (B64 y) = pure $ B64 $ (x * y) `mod` (prim__shl_Integer 1 64)
+mul (B64 x) (B64 y) = pure $ B64 $ (x * y) `mod` b64max
 mul (I x) (I y) = pure $ I (x * y)
 mul (Db x) (Db y) = pure $ Db (x * y)
 mul _ _ = Nothing
@@ -193,10 +202,10 @@ mod _ _ = Nothing
 shiftl : Constant -> Constant -> Maybe Constant
 shiftl (I x) (I y) = pure $ I (shiftL x y)
 shiftl (BI x) (BI y) = pure $ BI (prim__shl_Integer x y)
-shiftl (B8 x) (B8 y) = pure $ B8 $ (prim__shl_Int x y) `mod` (prim__shl_Int 1 8)
+shiftl (B8 x) (B8 y) = pure $ B8 $ (prim__shl_Int x y) `mod` b8max
-shiftl (B16 x) (B16 y) = pure $ B16 $ (prim__shl_Int x y) `mod` (prim__shl_Int 1 16)
+shiftl (B16 x) (B16 y) = pure $ B16 $ (prim__shl_Int x y) `mod` b16max
-shiftl (B32 x) (B32 y) = pure $ B32 $ (prim__shl_Int x y) `mod` (prim__shl_Int 1 32)
+shiftl (B32 x) (B32 y) = pure $ B32 $ (prim__shl_Int x y) `mod` b32max
-shiftl (B64 x) (B64 y) = pure $ B64 $ (prim__shl_Integer x y) `mod` (prim__shl_Integer 1 64)
+shiftl (B64 x) (B64 y) = pure $ B64 $ (prim__shl_Integer x y) `mod` b64max
 shiftl _ _ = Nothing
 
 shiftr : Constant -> Constant -> Maybe Constant

src/Core/TTC.idr

@@ -689,6 +689,7 @@ TTC CFType where
   toBuf b (CFStruct n a) = do tag 10; toBuf b n; toBuf b a
   toBuf b (CFUser n a) = do tag 11; toBuf b n; toBuf b a
   toBuf b CFGCPtr = tag 12
+  toBuf b CFBuffer = tag 13
 
   fromBuf b
       = case !getTag of
@@ -705,6 +706,7 @@ TTC CFType where
              10 => do n <- fromBuf b; a <- fromBuf b; pure (CFStruct n a)
              11 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
              12 => pure CFGCPtr
+             13 => pure CFBuffer
              _ => corrupt "CFType"
 
 export

src/Idris/CommandLine.idr

@@ -4,6 +4,8 @@ import IdrisPaths
 
 import Idris.Version
 
+import Core.Options
+
 import Data.List
 import Data.Maybe
 import Data.Strings
@@ -44,7 +46,7 @@ data CLOpt
   OutputFile String |
    ||| Execute a given function after checking the source file
   ExecFn String |
-   ||| Use a specific code generator (default chez)
+   ||| Use a specific code generator
   SetCG String |
    ||| Don't implicitly import Prelude
   NoPrelude |
@@ -113,7 +115,7 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
            MkOpt ["--no-prelude"] [] [NoPrelude]
               (Just "Don't implicitly import Prelude"),
            MkOpt ["--codegen", "--cg"] ["backend"] (\f => [SetCG f])
-              (Just "Set code generator (default chez)"),
+              (Just $ "Set code generator (default \""++ show (codegen defaultSession) ++ "\")"),
            MkOpt ["--package", "-p"] ["package"] (\f => [PkgPath f])
               (Just "Add a package as a dependency"),
 

src/Idris/Error.idr

@@ -5,6 +5,7 @@ import Core.Core
 import Core.Context
 import Core.Env
 import Core.Options
+import Core.Value
 
 import Idris.Resugar
 import Idris.Syntax
@@ -117,8 +118,10 @@ perror (AmbiguousElab fc env ts)
                    showSep "\n\t" !(traverse (pshow env) ts)
          setPPrint pp
          pure res
-perror (AmbiguousSearch fc env ts)
+perror (AmbiguousSearch fc env tgt ts)
-    = pure $ "Multiple solutions found in search. Possible correct results:\n\t" ++
+    = pure $ "Multiple solutions found in search of:\n\t"
+           ++ !(pshowNoNorm env tgt)
+           ++ "\nPossible correct results:\n\t" ++
            showSep "\n\t" !(traverse (pshowNoNorm env) ts)
 perror (AmbiguityTooDeep fc n ns)
     = pure $ "Maximum ambiguity depth exceeded in "  ++ show !(getFullName n)

src/Idris/IDEMode/REPL.idr

@@ -20,6 +20,7 @@ import Data.So
 import Idris.Desugar
 import Idris.Error
 import Idris.ModTree
+import Idris.Package
 import Idris.Parser
 import Idris.Resugar
 import Idris.REPL
@@ -148,8 +149,11 @@ process : {auto c : Ref Ctxt Defs} ->
           IDECommand -> Core IDEResult
 process (Interpret cmd)
     = replWrap $ interpret cmd
-process (LoadFile fname _)
+process (LoadFile fname_in _)
-    = replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
+    = do let fname = case !(findIpkg (Just fname_in)) of
+                          Nothing => fname_in
+                          Just f' => f'
+         replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname
 process (TypeOf n Nothing)
     = replWrap $ Idris.REPL.process (Check (PRef replFC (UN n)))
 process (TypeOf n (Just (l, c)))

src/Idris/Main.idr

@@ -131,7 +131,6 @@ stMain opts
          defs <- initDefs
          c <- newRef Ctxt defs
          s <- newRef Syn initSyntax
-         m <- newRef MD initMetadata
          addPrimitives
 
          setWorkingDir "."
@@ -157,6 +156,7 @@ stMain opts
                  when (checkVerbose opts) $ -- override Quiet if implicitly set
                      setOutput (REPL False)
                  u <- newRef UST initUState
+                 m <- newRef MD initMetadata
                  updateREPLOpts
                  session <- getSession
                  when (not $ nobanner session) $

src/Idris/Package.idr

@@ -444,15 +444,16 @@ getParseErrorLoc fname _ = replFC
 -- Just load the 'Main' module, if it exists, which will involve building
 -- it if necessary
 runRepl : {auto c : Ref Ctxt Defs} ->
+          {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           PkgDesc ->
           List CLOpt ->
           Core ()
-runRepl pkg opts
+runRepl pkg opts = do
-    = do addDeps pkg
+  u <- newRef UST initUState
-         processOptions (options pkg)
+  m <- newRef MD initMetadata
-         preOptions opts
+  repl {u} {s}
-         throw (InternalError "Not implemented")
+
 
 processPackage : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
@@ -480,7 +481,10 @@ processPackage cmd file opts
                                        | errs => coreLift (exitWith (ExitFailure 1))
                                     install pkg opts
                       Clean => clean pkg opts
-                      REPL => runRepl pkg opts
+                      REPL => do
+                        [] <- build pkg opts
+                           | errs => coreLift (exitWith (ExitFailure 1))
+                        runRepl pkg opts
 
 record POptsFilterResult where
   constructor MkPFR

src/TTImp/Elab/Binders.idr

@@ -201,17 +201,17 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty {vars}
                              (record { preciseInf = True } elabinfo)
                              nest env nVal (Just (gnf env tyv))
                   pure (fst c, snd c, rigl |*| rigc))
-              (\err => case err of
+              (\err => case linearErr err of
-                            (LinearMisuse _ _ r _)
+                            Just r
-                              => branchOne
+                              => do branchOne
-                                   (do c <- runDelays 0 $ check linear elabinfo
+                                     (do c <- runDelays 0 $ check linear elabinfo
-                                                nest env nVal (Just (gnf env tyv))
+                                                  nest env nVal (Just (gnf env tyv))
-                                       pure (fst c, snd c, linear))
+                                         pure (fst c, snd c, linear))
-                                   (do c <- check (rigl |*| rigc)
+                                     (do c <- check (rigl |*| rigc)
-                                                elabinfo -- without preciseInf
+                                                  elabinfo -- without preciseInf
-                                                nest env nVal (Just (gnf env tyv))
+                                                  nest env nVal (Just (gnf env tyv))
-                                       pure (fst c, snd c, rigMult rigl rigc))
+                                         pure (fst c, snd c, rigMult rigl rigc))
-                                   r
+                                     r
                             _ => do c <- check (rigl |*| rigc)
                                                elabinfo -- without preciseInf
                                                nest env nVal (Just (gnf env tyv))
@@ -229,3 +229,11 @@ checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty {vars}
          -- build the term directly
          pure (Bind fc n (Let rigb valv tyv) scopev,
                gnf env (Bind fc n (Let rigb valv tyv) scopet))
+  where
+    linearErr : Error -> Maybe RigCount
+    linearErr (LinearMisuse _ _ r _) = Just r
+    linearErr (InType _ _ e) = linearErr e
+    linearErr (InCon _ _ e) = linearErr e
+    linearErr (InLHS _ _ e) = linearErr e
+    linearErr (InRHS _ _ e) = linearErr e
+    linearErr _ = Nothing

src/TTImp/Elab/Case.idr

@@ -184,6 +184,12 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- (esp. in the scrutinee!) are set to 0 in the case type
          let env = updateMults (linearUsed est) env
          defs <- get Ctxt
+         let vis = case !(lookupCtxtExact (Resolved (defining est)) (gamma defs)) of
+                        Just gdef =>
+                             if visibility gdef == Public
+                                then Public
+                                else Private
+                        Nothing => Public
 
          -- if the scrutinee is ones of the arguments in 'env' we should
          -- split on that, rather than adding it as a new argument
@@ -213,7 +219,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- the alternative of fixing up the environment
          when (not (isNil fullImps)) $ findImpsIn fc [] [] casefnty
          cidx <- addDef casen (newDef fc casen (if isErased rigc then erased else top)
-                                      [] casefnty Public None)
+                                      [] casefnty vis None)
          -- don't worry about totality of the case block; it'll be handled
          -- by the totality of the parent function
          setFlag fc (Resolved cidx) (SetTotal PartialOK)

src/TTImp/Elab/Delayed.idr

@@ -179,6 +179,7 @@ recoverable (CantSolveEq _ env l r)
    = do defs <- get Ctxt
         pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
 recoverable (UndefinedName _ _) = pure False
+recoverable (LinearMisuse _ _ _ _) = pure False
 recoverable (InType _ _ err) = recoverable err
 recoverable (InCon _ _ err) = recoverable err
 recoverable (InLHS _ _ err) = recoverable err

src/TTImp/Elab/Local.idr

@@ -29,10 +29,20 @@ checkLocal : {vars : _} ->
              FC -> List ImpDecl -> (scope : RawImp) ->
              (expTy : Maybe (Glued vars)) ->
              Core (Term vars, Glued vars)
-checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
+checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
-    = do let defNames = definedInBlock [] nestdecls
+    = do est <- get EST
-         est <- get EST
          let f = defining est
+         defs <- get Ctxt
+         let vis = case !(lookupCtxtExact (Resolved (defining est)) (gamma defs)) of
+                        Just gdef => visibility gdef
+                        Nothing => Public
+         -- If the parent function is public, the nested definitions need
+         -- to be public too
+         let nestdecls =
+               if vis == Public
+                  then map setPublic nestdecls_in
+                  else nestdecls_in
+         let defNames = definedInBlock [] nestdecls
          names' <- traverse (applyEnv f)
                             (nub defNames) -- binding names must be unique
                                            -- fixes bug #115
@@ -101,6 +111,16 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
          = IData loc' vis (updateDataName nest d)
     updateName nest i = i
 
+    setPublic : ImpDecl -> ImpDecl
+    setPublic (IClaim fc c _ opts ty) = IClaim fc c Public opts ty
+    setPublic (IData fc _ d) = IData fc Public d
+    setPublic (IRecord fc c _ r) = IRecord fc c Public r
+    setPublic (IParameters fc ps decls)
+        = IParameters fc ps (map setPublic decls)
+    setPublic (INamespace fc ps decls)
+        = INamespace fc ps (map setPublic decls)
+    setPublic d = d
+
 getLocalTerm : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                FC -> Env Term vars -> Term vars -> List Name ->

src/TTImp/Interactive/GenerateDef.idr

@@ -57,7 +57,7 @@ expandClause : {auto c : Ref Ctxt Defs} ->
 expandClause loc n c
     = do log 10 $ "Trying clause " ++ show c
          c <- uniqueRHS c
-         Right clause <- checkClause linear False n [] (MkNested []) [] c
+         Right clause <- checkClause linear Private False n [] (MkNested []) [] c
             | Left _ => pure [] -- TODO: impossible clause, do something
                                 -- appropriate
          let MkClause {vars} env lhs rhs = clause

src/TTImp/ProcessDef.idr

@@ -352,10 +352,10 @@ checkClause : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
-              (mult : RigCount) -> (hashit : Bool) ->
+              (mult : RigCount) -> (vis : Visibility) -> (hashit : Bool) ->
               Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
               ImpClause -> Core (Either RawImp Clause)
-checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
+checkClause mult vis hashit n opts nest env (ImpossibleClause fc lhs)
     = do lhs_raw <- lhsInCurrentNS nest lhs
          handleUnify
            (do autoimp <- isUnboundImplicits
@@ -380,7 +380,7 @@ checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
                            if !(impossibleErrOK defs err)
                               then pure (Left lhs_raw)
                               else throw (ValidCase fc env (Right err)))
-checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
+checkClause {vars} mult vis hashit n opts nest env (PatClause fc lhs_in rhs)
     = do (_, (vars'  ** (sub', env', nest', lhstm', lhsty'))) <-
              checkLHS False mult hashit n opts nest env fc lhs_in
          let rhsMode = if isErased mult then InType else InExpr
@@ -405,7 +405,7 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
 
          pure (Right (MkClause env' lhstm' rhstm))
 -- TODO: (to decide) With is complicated. Move this into its own module?
-checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw flags cs)
+checkClause {vars} mult vis hashit n opts nest env (WithClause fc lhs_in wval_raw flags cs)
     = do (lhs, (vars'  ** (sub', env', nest', lhspat, reqty))) <-
              checkLHS False mult hashit n opts nest env fc lhs_in
          let wmode
@@ -468,7 +468,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw fl
 
          wname <- genWithName n
          widx <- addDef wname (newDef fc wname (if isErased mult then erased else top)
-                                      vars wtype Private None)
+                                      vars wtype vis None)
          let rhs_in = apply (IVar fc wname)
                         (map (IVar fc) envns ++
                          map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)
@@ -696,7 +696,8 @@ processDef opts nest env fc n_in cs_in
                        then erased
                        else linear
          nidx <- resolveName n
-         cs <- traverse (checkClause mult hashit nidx opts nest env) cs_in
+         cs <- traverse (checkClause mult (visibility gdef)
+                                     hashit nidx opts nest env) cs_in
          let pats = map toPats (rights cs)
 
          (cargs ** (tree_ct, unreachable)) <-

src/Text/Literate.idr

@@ -32,14 +32,18 @@ import Data.Strings
 %default total
 
 untilEOL : Recognise False
-untilEOL = manyUntil (is '\n') any
+untilEOL = manyUntil newline any
 
 line : String -> Lexer
-line s = exact s <+> space <+> untilEOL
+line s = exact s <+> (newline <|> space <+> untilEOL)
 
 block : String -> String -> Lexer
 block s e = surround (exact s <+> untilEOL) (exact e <+> untilEOL) any
 
+notCodeLine : Lexer
+notCodeLine = newline
+           <|> any <+> untilEOL
+
 data Token = CodeBlock String String String
            | Any String
            | CodeLine String String
@@ -55,30 +59,31 @@ rawTokens : (delims  : List (String, String))
 rawTokens delims ls =
           map (\(l,r) => (block l r, CodeBlock (trim l) (trim r))) delims
        ++ map (\m => (line m, CodeLine (trim m))) ls
-       ++ [(any, Any)]
+       ++ [(notCodeLine, Any)]
 
 ||| Merge the tokens into a single source file.
-reduce : List (TokenData Token) -> String -> String
+reduce : List (TokenData Token) -> List String -> String
-reduce [] acc = acc
+reduce [] acc = fastAppend (reverse acc)
-reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest (acc ++ blank_content)
+reduce (MkToken _ _ (Any x) :: rest) acc = reduce rest (blank_content::acc)
   where
     -- Preserve the original document's line count.
     blank_content : String
-    blank_content = if elem '\n' (unpack x)
+    blank_content = fastAppend (replicate (length (lines x)) "\n")
-      then concat $ replicate (length (lines x)) "\n"
+
-      else ""
 reduce (MkToken _ _ (CodeLine m src) :: rest) acc =
-    reduce rest (acc ++ (substr
+    if m == trim src
-                           (length m + 1) -- remove space to right of marker.
+    then reduce rest ("\n"::acc)
-                           (length src)
+    else reduce rest ((substr (length m + 1) -- remove space to right of marker.
-                           src))
+                              (length src)
+                              src
+                      )::acc)
 
 reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc with (lines src) -- Strip the deliminators surrounding the block.
   reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | [] = reduce rest acc -- 1
   reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: ys) with (snocList ys)
     reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: []) | Empty = reduce rest acc -- 2
     reduce (MkToken _ _ (CodeBlock l r src) :: rest) acc | (s :: (srcs ++ [f])) | (Snoc f srcs rec) =
-        reduce rest (acc ++ "\n" ++ unlines srcs)
+        reduce rest ("\n" :: unlines srcs :: acc)
 
 -- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.
 
@@ -159,7 +164,7 @@ extractCode : (specification : LiterateStyle)
            -> Either LiterateError String
 extractCode (MkLitStyle delims markers exts) str =
       case lex (rawTokens delims markers) str of
-        (toks, (_,_,"")) => Right $ reduce toks ""
+        (toks, (_,_,"")) => Right (reduce toks Nil)
         (_, (l,c,i))     => Left (MkLitErr l c i)
 
 ||| Synonym for `extractCode`.

src/Utils/Binary.idr

@@ -105,12 +105,6 @@ initBinaryS s
              | Nothing => throw (InternalError "Buffer creation failed")
          newRef Bin (newBinary buf s)
 
-export
-freeBinary : Ref Bin Binary -> Core ()
-freeBinary b
-    = do b <- get Bin
-         coreLift $ freeBuffer (buf b)
-
 extendBinary : Int -> Binary -> Core Binary
 extendBinary need (MkBin buf l s u)
     = do let newsize = s * 2

support/c/idris_buffer.c

@@ -16,7 +16,7 @@ void* idris2_newBuffer(int bytes) {
     }
 
     buf->size = bytes;
-    memset(buf->data, 0, bytes);
+//    memset(buf->data, 0, bytes);
 
     return (void*)buf;
 }
@@ -124,64 +124,10 @@ char* idris2_getBufferString(void* buffer, int loc, int len) {
     return rs;
 }
 
-void* idris2_readBufferFromFile(char* fn) {
+int idris2_readBufferData(FILE* h, char* buffer, int loc, int max) {
-    FILE* f = fopen(fn, "r");
+    return fread(buffer+loc, sizeof(uint8_t), (size_t)max, h);
-    if (f == NULL) { return NULL; }
-
-    int fd = fileno(f);
-    int len;
-
-    struct stat fbuf;
-    if (fstat(fd, &fbuf) == 0) {
-        len = (int)(fbuf.st_size);
-    } else {
-        return NULL;
-    }
-
-    size_t size = sizeof(Buffer) + len*sizeof(uint8_t);
-    Buffer* buf = malloc(size);
-    buf->size = len;
-
-    fread((buf->data), sizeof(uint8_t), (size_t)len, f);
-    fclose(f);
-    return buf;
 }
 
-int idris2_writeBufferToFile(char* fn, void* buffer, int max) {
+int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len) {
-    Buffer* b = buffer;
+    return fwrite(buffer+loc, sizeof(uint8_t), len, h);
-    FILE* f = fopen(fn, "w");
-    if (f == NULL) { return 0; }
-
-    fwrite((b->data), sizeof(uint8_t), max, f);
-    fclose(f);
-    return -1;
 }
-
-// To be added when the file API has moved to the C support libs
-/*
-int idris2_readBuffer(FILE* h, void* buffer, int loc, int max) {
-    Buffer* b = buffer;
-    size_t len;
-
-    if (loc >= 0 && loc < b->size) {
-        if (loc + max > b->size) {
-            max = b->size - loc;
-        }
-        len = fread((b->data)+loc, sizeof(uint8_t), (size_t)max, h);
-        return len;
-    } else {
-        return 0;
-    }
-}
-
-void idris2_writeBuffer(FILE* h, void* buffer, int loc, int len) {
-    Buffer* b = buffer;
-
-    if (loc >= 0 && loc < b->size) {
-        if (loc + len > b->size) {
-            len = b->size - loc;
-        }
-        fwrite((b->data)+loc, sizeof(uint8_t), len, h);
-    }
-}
-*/

support/c/idris_buffer.h

@@ -18,12 +18,9 @@ void idris2_setBufferString(void* buffer, int loc, char* str);
 void idris2_copyBuffer(void* from, int start, int len,
                        void* to, int loc);
 
-void* idris2_readBufferFromFile(char* fn);
+// Reading and writing the raw data, to the pointer in the buffer
-int idris2_writeBufferToFile(char* fn, void* buffer, int max);
+int idris2_readBufferData(FILE* h, char* buffer, int loc, int max);
-
+int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len);
-// To be added when the file API has moved to the C support libs
-// int idris2_readBuffer(FILE* h, void* buffer, int loc, int max);
-// void idris2_writeBuffer(FILE* h, void* buffer, int loc, int len);
 
 int idris2_getBufferByte(void* buffer, int loc);
 int idris2_getBufferInt(void* buffer, int loc);

support/c/idris_directory.c

@@ -8,8 +8,7 @@
 
 char* idris2_currentDirectory() {
    char* cwd = malloc(1024); // probably ought to deal with the unlikely event of this being too small
-   getcwd(cwd, 1024);
+   return getcwd(cwd, 1024); // Freed by RTS
-   return cwd; // freed by RTS
 }
 
 int idris2_changeDir(char* dir) {

support/chez/support.ss

@@ -160,34 +160,6 @@
 (define (blodwen-buffer-copydata buf start len dest loc)
   (bytevector-copy! buf start dest loc len))
 
-; 'dir' is only needed in Racket
-(define (blodwen-read-bytevec curdir fname)
-  (guard
-    (x (#t #f))
-    (let* [(h (open-file-input-port fname
-                                    (file-options)
-                                    (buffer-mode line) #f))
-           (vec (get-bytevector-all h))]
-      (begin (close-port h)
-             vec))))
-
-(define (blodwen-isbytevec v)
-(if (bytevector? v)
-    0
-    -1))
-
-; 'dir' is only needed in Racket
-(define (blodwen-write-bytevec curdir fname vec max)
-  (guard
-    (x (#t -1))
-    (let* [(h (open-file-output-port fname (file-options no-fail)
-                                     (buffer-mode line) #f))]
-      (begin (put-bytevector h vec 0 max)
-             (close-port h)
-             0))))
-
-
-
 ;; Threads
 
 (define blodwen-thread-data (make-thread-parameter #f))

support/racket/support.rkt

@@ -155,43 +155,6 @@
 (define (blodwen-buffer-copydata buf start len dest loc)
   (bytevector-copy! buf start dest loc len))
 
-; The 'dir' argument is an annoying hack. Racket appears to have a different
-; notion of current directory than the OS, so we pass what we think it is so
-; that racket can change to it
-(define (blodwen-read-bytevec dir fname)
-   (let ((origdir (current-directory)))
-     (begin
-          (current-directory dir)
-          (with-handlers
-            ([(lambda (x) #t) (lambda (exn) (current-directory origdir) #f)])
-            (let* [(h (open-file-input-port fname
-                                            (file-options)
-                                            (buffer-mode line) #f))
-                   (vec (get-bytevector-all h))]
-              (begin (close-port h)
-                     (current-directory origdir)
-                     vec))))))
-
-(define (blodwen-isbytevec v)
-(if (bytevector? v)
-    0
-    -1))
-
-; See blodwen-read-bytevec for what 'dir' is for
-(define (blodwen-write-bytevec dir fname vec max)
-   (let ((origdir (current-directory)))
-     (begin
-           (current-directory dir)
-           (with-handlers
-            ([(lambda (x) #t) (lambda (exn) (current-directory origdir) -1)])
-            (let* [(h (open-file-output-port fname (file-options no-fail)
-                                             (buffer-mode line) #f))]
-              (begin (put-bytevector h vec 0 max)
-                     (close-port h)
-                     (current-directory origdir)
-                     0))))))
-
-
 ;; Threads
 
 (define blodwen-thread-data (make-thread-cell #f))

tests/Main.idr

@@ -58,11 +58,12 @@ idrisTests
        "literate001", "literate002", "literate003", "literate004",
        "literate005", "literate006", "literate007", "literate008",
        "literate009", "literate010", "literate011", "literate012",
+       "literate013",
        -- Interfaces
        "interface001", "interface002", "interface003", "interface004",
        "interface005", "interface006", "interface007", "interface008",
        "interface009", "interface010", "interface011", "interface012",
-       "interface013", "interface014", "interface015",
+       "interface013", "interface014", "interface015", "interface016",
        -- Miscellaneous REPL
        "interpreter001", "interpreter002",
        -- Implicit laziness, lazy evaluation
@@ -79,7 +80,7 @@ idrisTests
        "perror001", "perror002", "perror003", "perror004", "perror005",
        "perror006",
        -- Packages and ipkg files
-       "pkg001", "pkg002", "pkg003",
+       "pkg001", "pkg002", "pkg003", "pkg004",
        -- Larger programs arising from real usage. Typically things with
        -- interesting interactions between features
        "real001", "real002",
@@ -207,7 +208,7 @@ runTest opts testPath
               ]
             Just exp => do
               putStrLn "Golden value differs from actual value."
-              code <- system "git diff --exit-code expected output"
+              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

tests/chez/chez021/expected

@@ -12,7 +12,7 @@ False
 4294967295
 18446744073709551615
 1/1: Building Bits (Bits.idr)
-Main> ["257", "200", "248", "1", "255", "200", "254"]
+Main> ["1", "200", "248", "1", "255", "200", "254"]
-Main> ["True", "True"]
+Main> ["True", "False"]
 Main> ["255", "65535", "4294967295", "18446744073709551615"]
 Main> Main> Bye for now!

tests/ideMode/ideMode001/dummy.ipkg

@@ -0,0 +1 @@
+package idemode001

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 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((: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 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:260} a)")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:261}_[]")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 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:260}_[] ?{_:261}_[])")))))) 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:269}_[] ?{_:270}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((: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 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:251}_[] ?{_:250}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:241} : (Main.Vect n[0] a[1])) -> (({arg:242} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(: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.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

tests/ideMode/ideMode003/dummy.ipkg

@@ -0,0 +1 @@
+package idemode003

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 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((: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 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:260} a)")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:269} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:261}_[]")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:270}_[]")))))) 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:260}_[] ?{_:261}_[])")))))) 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:269}_[] ?{_:270}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:271}_[] ?{_:270}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((: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 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:251}_[] ?{_:250}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:241} : (Main.Vect n[0] a[1])) -> (({arg:242} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:250} : (Main.Vect n[0] a[1])) -> (({arg:251} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(: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.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

tests/idris2/coverage010/expected

@@ -1,3 +1,3 @@
 1/1: Building casetot (casetot.idr)
 casetot.idr:12:1--13:1:main is not covering:
-	Calls non covering function Main.case block in 2087(290)
+	Calls non covering function Main.case block in 2087(287)

tests/idris2/interactive009/Door.idr

@@ -22,11 +22,6 @@ One = Use Once
 Any : (Type -> Type) -> Type -> Type
 Any = Use Many
 
-infix 2 @@
-
-data Res : (a : Type) -> (a -> Type) -> Type where
-     (@@) : (x : a) -> (1 res : r x) -> Res a r
-
 data DoorState = Closed | Open
 
 data Door : DoorState -> Type where
@@ -57,7 +52,7 @@ doorProg2
          r <- openDoor d
          let x = 42
          case r of
-              (res @@ d) => ?now_1
+              (res # d) => ?now_1
 
 doorProg3 : Any m ()
 doorProg3
@@ -65,5 +60,5 @@ doorProg3
          r <- openDoor d
          let x = 42
          case r of
-              (True @@ d) => ?now_2
+              (True # d) => ?now_2
-              (False @@ d) => ?now_3
+              (False # d) => ?now_3

tests/idris2/interactive009/expected

@@ -1,17 +1,12 @@
 1/1: Building Door (Door.idr)
-Main>               (y @@ res) => ?now_4
+Door.idr:35:19--35:69:While processing type of openDoor at Door.idr:34:1--37:1:
-Main>               (True @@ d) => ?now_4
+Undefined name Res
-              (False @@ d) => ?now_5
+Door.idr:44:15--45:10:While processing right hand side of doorProg at Door.idr:42:1--49:1:
-Main>  0 m : Type -> Type
+Undefined name openDoor
- 1 d : Door Open
+Door.idr:55:16--55:23:Unknown operator '#'
-   x : Integer
+Door.idr:63:16--63:24:Unknown operator '#'
- 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
+Main> No clause to split here
--------------------------------------
+Main> No clause to split here
-now_2 : Use Many m ()
+Main> (interactive):1:4--1:9:Undefined name now_2
-Main>  0 m : Type -> Type
+Main> (interactive):1:4--1:9:Undefined name now_3
- 1 d : Door Closed
-   x : Integer
- 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
--------------------------------------
-now_3 : Use Many m ()
 Main> Bye for now!

tests/idris2/interactive009/input

@@ -1,5 +1,5 @@
-:cs 52 15 what
+:cs 47 15 what
-:cs 60 16 res
+:cs 55 16 res
 :t now_2
 :t now_3
 :q

tests/idris2/interface016/TwoNum.idr

@@ -0,0 +1,4 @@
+f : Num a => a
+f = g where
+  g : Num a => a
+  g = 0

tests/idris2/interface016/expected

@@ -0,0 +1,8 @@
+1/1: Building TwoNum (TwoNum.idr)
+TwoNum.idr:4:7--5:1:While processing right hand side of f at TwoNum.idr:2:1--5:1:
+While processing right hand side of f,g at TwoNum.idr:4:3--5:1:
+Multiple solutions found in search of:
+	Num a
+Possible correct results:
+	conArg
+	conArg

tests/idris2/interface016/run

@@ -0,0 +1,3 @@
+$1 TwoNum.idr --check
+
+rm -rf build

tests/idris2/linear005/Linear.idr

@@ -30,9 +30,3 @@ One = Use Once
 public export
 Any : (Type -> Type) -> Type -> Type
 Any = Use Many
-
-infix 2 @@
-
-public export
-data Res : (a : Type) -> (a -> Type) -> Type where
-     (@@) : (x : a) -> (1 res : r x) -> Res a r

tests/idris2/linear005/expected

@@ -1,5 +1,7 @@
 1/2: Building Linear (Linear.idr)
 2/2: Building Door (Door.idr)
+Door.idr:12:44--12:94:While processing type of openDoor at Door.idr:12:1--13:1:
+Undefined name Res
 Door>  0 m : Type -> Type
  1 d : Door Closed
 -------------------------------------

tests/idris2/linear008/Door.idr

@@ -56,12 +56,6 @@ public export
 Any : (Type -> Type) -> Type -> Type
 Any m = Lin m Many
 
-infix 2 @@
-
-public export
-data Res : (a : Type) -> (a -> Type) -> Type where
-     (@@) : (val : a) -> (1 resource : r val) -> Res a r
-
 data DoorState = Closed | Open
 
 -- changes start here

tests/idris2/linear008/expected

@@ -1 +1,3 @@
 1/1: Building Door (Door.idr)
+Door.idr:74:25--74:77:While processing constructor Doored at Door.idr:70:1--77:1 at Door.idr:70:1--77:1:
+Undefined name Res

tests/idris2/literate006/Door.lidr

@@ -22,11 +22,6 @@
 > Any : (Type -> Type) -> Type -> Type
 > Any = Use Many
 
-> infix 2 @@
-
-> data Res : (a : Type) -> (a -> Type) -> Type where
->      (@@) : (x : a) -> (1 res : r x) -> Res a r
-
 > data DoorState = Closed | Open
 
 > data Door : DoorState -> Type where
@@ -57,7 +52,7 @@
 >          r <- openDoor d
 >          let x = 42
 >          case r of
->               (res @@ d) => ?now_1
+>               (res # d) => ?now_1
 
 > doorProg3 : Any m ()
 > doorProg3
@@ -65,5 +60,5 @@
 >          r <- openDoor d
 >          let x = 42
 >          case r of
->               (True @@ d) => ?now_2
+>               (True # d) => ?now_2
->               (False @@ d) => ?now_3
+>               (False # d) => ?now_3

tests/idris2/literate006/expected

@@ -1,17 +1,12 @@
 1/1: Building Door (Door.lidr)
-Main> >               (y @@ res) => ?now_4
+Door.lidr:35:19--35:69:While processing type of openDoor at Door.lidr:34:1--37:1:
-Main> >               (True @@ d) => ?now_4
+Undefined name Res
->               (False @@ d) => ?now_5
+Door.lidr:44:15--45:10:While processing right hand side of doorProg at Door.lidr:42:1--49:1:
-Main>  0 m : Type -> Type
+Undefined name openDoor
- 1 d : Door Open
+Door.lidr:55:16--55:23:Unknown operator '#'
-   x : Integer
+Door.lidr:63:16--63:24:Unknown operator '#'
- 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
+Main> No clause to split here
--------------------------------------
+Main> No clause to split here
-now_2 : Use Many m ()
+Main> (interactive):1:4--1:9:Undefined name now_2
-Main>  0 m : Type -> Type
+Main> (interactive):1:4--1:9:Undefined name now_3
- 1 d : Door Closed
-   x : Integer
- 0 r : Res Bool (\r => (Door (if r then Open else Closed)))
--------------------------------------
-now_3 : Use Many m ()
 Main> Bye for now!

tests/idris2/literate006/input

@@ -1,5 +1,5 @@
-:cs 52 17 what
+:cs 47 17 what
-:cs 60 18 res
+:cs 55 18 res
 :t now_2
 :t now_3
 :q

tests/idris2/literate013/Lit.lidr

@@ -0,0 +1,16 @@
+> module Lit
+>
+> %default total
+
+a > b
+
+a < b
+
+> data V a = Empty | Extend a (V a)
+
+> isCons : V a -> Bool
+> isCons Empty = False
+> isCons (Extend _ _) = True
+
+< namespace Hidden
+<   data U a = Empty | Extend a (U a)

tests/idris2/literate013/expected

@@ -0,0 +1 @@
+1/1: Building Lit (Lit.lidr)

tests/idris2/literate013/run

@@ -0,0 +1,3 @@
+$1 --no-banner --check Lit.lidr
+
+rm -rf build

tests/idris2/pkg004/Dummy.idr

@@ -0,0 +1,7 @@
+module Dummy
+
+something : String
+something = "Something something"
+
+data Proxy : Type -> Type where
+  MkProxy : Proxy a

tests/idris2/pkg004/dummy.ipkg

@@ -0,0 +1,9 @@
+package dummy
+
+authors = "Joe Bloggs"
+maintainers = "Joe Bloggs"
+license = "BSD3 but see LICENSE for more information"
+brief = "This is a dummy package."
+readme = "README.md"
+
+modules = Dummy

tests/idris2/pkg004/expected

@@ -0,0 +1,9 @@
+1/1: Building Dummy (Dummy.idr)
+Dummy> (interactive):1:4--1:13:Undefined name undefined
+Dummy> Dummy.something : String
+Dummy> "Something something"
+Dummy> Dummy.Proxy : Type -> Type
+Dummy> Proxy
+Dummy> Proxy String : Type
+Dummy> 
+Bye for now!

tests/idris2/pkg004/input

@@ -0,0 +1,6 @@
+:t undefined
+:t something
+something
+:t Proxy
+Proxy
+:t Proxy String

tests/idris2/pkg004/run

@@ -0,0 +1,3 @@
+$1 --repl dummy.ipkg < input
+
+rm -rf build

tests/idris2/real001/Channel.idr

@@ -134,11 +134,11 @@ tryRecv (MkChannel lock cond_lock cond local remote)
          case dequeue rq of
               Nothing =>
                   do lift $ mutexRelease lock
-                     pure (Nothing @@ MkChannel lock cond_lock cond local remote)
+                     pure (Nothing # MkChannel lock cond_lock cond local remote)
               Just (rq', Entry {any} val) =>
                   do lift $ writeIORef local rq'
                      lift $ mutexRelease lock
-                     pure (Just (believe_me {a=any} val) @@
+                     pure (Just (believe_me {a=any} val) #
                            MkChannel lock cond_lock cond local remote)
 
 -- blocks until the message is there
@@ -158,7 +158,7 @@ recv (MkChannel lock cond_lock cond local remote)
               Just (rq', Entry {any} val) =>
                   do lift $ writeIORef local rq'
                      lift $ mutexRelease lock
-                     pure (believe_me {a=any} val @@
+                     pure (believe_me {a=any} val #
                            MkChannel lock cond_lock cond local remote)
 
 export
@@ -180,14 +180,14 @@ timeoutRecv (MkChannel lock cond_lock cond local remote) timeout
                      lift $ mutexAcquire cond_lock
                      lift $ conditionWaitTimeout cond cond_lock timeout
                      lift $ mutexRelease cond_lock
-                     res @@ chan <- tryRecv {ty} {next} (MkChannel lock cond_lock cond local remote)
+                     res # chan <- tryRecv {ty} {next} (MkChannel lock cond_lock cond local remote)
                      case res of
-                          Nothing => pure (Nothing @@ chan)
+                          Nothing => pure (Nothing # chan)
-                          Just res => pure (Just res @@ chan)
+                          Just res => pure (Just res # chan)
               Just (rq', Entry {any} val) =>
                   do lift $ writeIORef local rq'
                      lift $ mutexRelease lock
-                     pure (Just (believe_me {a=any} val) @@
+                     pure (Just (believe_me {a=any} val) #
                            MkChannel lock cond_lock cond local remote)
 
 export

tests/idris2/real001/Linear.idr

@@ -54,13 +54,6 @@ public export
 Any : (Type -> Type) -> Type -> Type
 Any m = Lin m Many
 
-infix 2 @@
-
-public export
-data Res : (a : Type) -> (a -> Type) -> Type where
-     (@@) : (val : a) -> (1 resource : r val) -> Res a r
-
-
 {-
 data DoorState = Closed | Open
 

tests/idris2/real001/MakeChans.idr

@@ -18,12 +18,12 @@ Utils
 
 utilServer : (1 chan : Server Utils) -> Any IO ()
 utilServer chan
-    = do cmd @@ chan <- recv chan
+    = do cmd # chan <- recv chan
          case cmd of
-              Add => do (x, y) @@ chan <- recv chan
+              Add => do (x, y) # chan <- recv chan
                         chan <- send chan (x + y)
                         close chan
-              Append => do (x, y) @@ chan <- recv chan
+              Append => do (x, y) # chan <- recv chan
                            chan <- send chan (x ++ y)
                            close chan
 
@@ -35,7 +35,7 @@ MakeUtils = do cmd <- Request Bool
 
 sendUtils : (1 chan : Server MakeUtils) -> Any IO ()
 sendUtils chan
-    = do cmd @@ chan <- recv chan
+    = do cmd # chan <- recv chan
          if cmd
             then do cchan <- Channel.fork utilServer
                     chan <- send chan cchan
@@ -46,7 +46,7 @@ getUtilsChan : (1 chan : Client MakeUtils) ->
                One IO (Client Utils, Client MakeUtils)
 getUtilsChan chan
     = do chan <- send chan True
-         cchan @@ chan <- recv chan
+         cchan # chan <- recv chan
          pure (cchan, chan)
 
 closeUtilsChan : (1 chan : Client MakeUtils) ->
@@ -69,12 +69,12 @@ doThings
          uchan1 <- send uchan1 Add
          uchan2 <- send uchan2 Append
          uchan2 <- send uchan2 ("aaa", "bbb")
-         res @@ uchan2 <- recv uchan2
+         res # uchan2 <- recv uchan2
          close uchan2
          lift $ printLn res
 
          uchan1 <- send uchan1 (40, 54)
-         res @@ uchan1 <- recv uchan1
+         res # uchan1 <- recv uchan1
          close uchan1
 
          lift $ printLn res

tests/idris2/real001/TestProto.idr

@@ -18,14 +18,14 @@ testClient chan
          lift $ putStrLn "Sending value"
          chan <- send chan False
          lift $ putStrLn "Sent"
-         c @@ chan <- recv chan
+         c # chan <- recv chan
          lift $ putStrLn ("Result: " ++ c)
          close chan
 
 testServer : (1 chan : Server TestProto) -> Any IO ()
 testServer chan
     = do lift $ putStrLn "Waiting"
-         cmd @@ chan <- recv chan
+         cmd # chan <- recv chan
          lift $ putStrLn ("Received " ++ show cmd)
          lift $ sleep 1
          lift $ putStrLn "Sending answer"

tests/idris2/real001/expected

@@ -1,4 +1,21 @@
 1/3: Building Linear (Linear.idr)
 2/3: Building Channel (Channel.idr)
-3/3: Building TestProto (TestProto.idr)
+Channel.idr:128:19--130:81:While processing type of tryRecv at Channel.idr:122:1--131:1:
-3/3: Building MakeChans (MakeChans.idr)
+Undefined name Res
+Channel.idr:137:28--137:80:Unknown operator '#'
+Channel.idr:147:16--147:55:While processing type of recv at Channel.idr:145:1--148:1:
+Undefined name Res
+Channel.idr:161:28--162:70:Unknown operator '#'
+Channel.idr:171:23--173:85:While processing type of timeoutRecv at Channel.idr:164:1--174:1:
+Undefined name Res
+Channel.idr:183:22--183:33:Unknown operator '#'
+2/3: Building Channel (Channel.idr)
+Channel.idr:128:19--130:81:While processing type of tryRecv at Channel.idr:122:1--131:1:
+Undefined name Res
+Channel.idr:137:28--137:80:Unknown operator '#'
+Channel.idr:147:16--147:55:While processing type of recv at Channel.idr:145:1--148:1:
+Undefined name Res
+Channel.idr:161:28--162:70:Unknown operator '#'
+Channel.idr:171:23--173:85:While processing type of timeoutRecv at Channel.idr:164:1--174:1:
+Undefined name Res
+Channel.idr:183:22--183:33:Unknown operator '#'

tests/idris2/real002/Control/App.idr

@@ -339,12 +339,6 @@ HasErr Void e => PrimIO e where
                     $ \_ =>
                MkAppRes (Right ())
 
-infix 5 @@
-
-public export
-data Res : (a : Type) -> (a -> Type) -> Type where
-     (@@) : (val : a) -> (1 r : t val) -> Res a t
-
 public export
 data FileEx = GenericFileEx Int -- errno
             | FileReadError

tests/idris2/real002/Store.idr

@@ -23,10 +23,10 @@ Has [Console] e => StoreI e where
 
   login (MkStore str) pwd
       = if pwd == "Mornington Crescent"
-           then pure1 (True @@ MkStore str)
+           then pure1 (True # MkStore str)
-           else pure1 (False @@ MkStore str)
+           else pure1 (False # MkStore str)
   logout (MkStore str) = pure1 (MkStore str)
-  readSecret (MkStore str) = pure1 (str @@ MkStore str)
+  readSecret (MkStore str) = pure1 (str # MkStore str)
 
   disconnect (MkStore _)
       = putStrLn "Door destroyed"
@@ -38,11 +38,11 @@ storeProg
          s <- connect
          app $ putStr "Password: "
          pwd <- app $ getStr
-         True @@ s <- login s pwd
+         True # s <- login s pwd
-              | False @@ s => do app $ putStrLn "Login failed"
+              | False # s => do app $ putStrLn "Login failed"
-                                 app $ disconnect s
+                                app $ disconnect s
          app $ putStrLn "Logged in"
-         secret @@ s <- readSecret s
+         secret # s <- readSecret s
          app $ putStrLn ("Secret: " ++ secret)
          s <- logout s 
          app $ putStrLn "Logged out"

tests/idris2/real002/StoreL.idr

@@ -25,8 +25,8 @@ login : (1 s : Store LoggedOut) -> (password : String) ->
         Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
 login (MkStore secret) password
     = if password == "Mornington Crescent"
-         then True @@ MkStore secret
+         then True # MkStore secret
-         else False @@ MkStore secret
+         else False # MkStore secret
 
 logout : (1 s : Store LoggedIn) -> Store LoggedOut
 logout (MkStore secret) = MkStore secret
@@ -37,9 +37,9 @@ storeProg
         do putStr "Password: "
            password <- Console.getStr
            connect $ \s =>
-             do let True @@ s = login s password
+             do let True # s = login s password
-                       | False @@ s => do putStrLn "Incorrect password"
+                       | False # s => do putStrLn "Incorrect password"
-                                          disconnect s
+                                         disconnect s
                 putStrLn "Door opened"
                 let s = logout s 
                 putStrLn "Door closed"

tests/idris2/real002/expected

@@ -1,4 +1,14 @@
 1/3: Building Control.App (Control/App.idr)
 2/3: Building Control.App.Console (Control/App/Console.idr)
 3/3: Building Store (Store.idr)
+Store.idr:13:19--13:79:While processing constructor StoreI at Store.idr:10:1--19:1 at Store.idr:10:1--19:1:
+Undefined name Res
+Store.idr:26:24--26:42:Unknown operator '#'
+Store.idr:41:10--41:19:Unknown operator '#'
+Store.idr:52:12--53:1:While processing right hand side of main at Store.idr:52:1--53:1:
+Can't find an implementation for StoreI [Void]
 3/3: Building StoreL (StoreL.idr)
+StoreL.idr:25:9--26:1:While processing type of login at StoreL.idr:24:1--26:1:
+Undefined name Res
+StoreL.idr:28:15--29:10:Unknown operator '#'
+StoreL.idr:40:21--40:30:Unknown operator '#'

tests/idris2/reflection003/expected

@@ -5,11 +5,11 @@ LOG 0: Name: Prelude.Strings.++
 LOG 0: Type: (%pi Rig1 Explicit (Just _) String (%pi Rig1 Explicit (Just _) String String))
 LOG 0: Resolved name: Prelude.Nat
 LOG 0: Constructors: [Prelude.Z, Prelude.S]
-refprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:
+refprims.idr:43:10--45:1:While processing right hand side of dummy1 at refprims.idr:43:1--45:1:
 Error during reflection: Not really trying
-refprims.idr:40:10--42:1:While processing right hand side of dummy2 at refprims.idr:40:1--42:1:
+refprims.idr:46:10--48:1:While processing right hand side of dummy2 at refprims.idr:46:1--48:1:
 Error during reflection: Still not trying
-refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:
+refprims.idr:49:10--51:1:While processing right hand side of dummy3 at refprims.idr:49:1--51:1:
 Error during reflection: Undefined name
-refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:
+refprims.idr:52:10--54:1:While processing right hand side of dummy4 at refprims.idr:52:1--54:1:
-Error during reflection: failed after generating Main.{plus:6078}
+Error during reflection: failed after generating Main.{plus:XXXX}

tests/idris2/reflection003/refprims.idr

@@ -27,11 +27,17 @@ logBad
          logMsg 0 ("Constructors: " ++ show !(getCons n))
          fail "Still not trying"
 
+-- because the exact sequence number in a gensym depends on
+-- the library and compiler internals we need to censor it so the
+-- output won't be overly dependent on the exact versions used.
+censorDigits : String -> String
+censorDigits str = pack $ map (\c => if isDigit c then 'X' else c) (unpack str)
+
 tryGenSym : Elab a
 tryGenSym
    = do n <- genSym "plus"
         ns <- inCurrentNS n
-        fail $ "failed after generating " ++ show ns
+        fail $ "failed after generating " ++ censorDigits (show ns)
 
 dummy1 : a
 dummy1 = %runElab logPrims