Merge remote-tracking branch 'upstream/master'

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
 ----------------------------
 

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
-                    | False @@ s => do putStrLn "Wrong password"
-                                       disconnect s
-                  let str @@ s = readSecret s
+               do let True # s = login s password
+                    | False # s => do putStrLn "Wrong password"
+                                      disconnect 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)
-               else pure1 (False @@ MkStore str)
+               then pure1 (True # 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"

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/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

@@ -479,8 +479,8 @@ multDistributesOverMinusRight left centre right =
 
 -- power proofs
 
-multPowerPowerPlus : (base, exp, exp' : Nat) ->
-  power base (exp + exp') = (power base exp) * (power base exp')
+-- multPowerPowerPlus : (base, exp, exp' : Nat) ->
+--   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' =
@@ -488,21 +488,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 = rewrite multCommutative base 1 in multOneLeftNeutral base
-
-powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
-powerOneSuccOne Z       = Refl
-powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
-
-powerPowerMultPower : (base, exp, exp' : Nat) ->
-  power (power base exp) exp' = power base (exp * exp')
-powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
-powerPowerMultPower base exp (S exp') =
-  rewrite powerPowerMultPower base exp exp' in
-  rewrite multRightSuccPlus exp exp' in
-  rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
-          Refl
+--powerOneNeutral : (base : Nat) -> power base 1 = base
+--powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
+--
+--powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
+--powerOneSuccOne Z       = Refl
+--powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
+--
+--powerPowerMultPower : (base, exp, exp' : Nat) ->
+--  power (power base exp) exp' = power base (exp * exp')
+--powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
+--powerPowerMultPower base exp (S exp') =
+--  rewrite powerPowerMultPower base exp exp' in
+--  rewrite multRightSuccPlus exp exp' in
+--  rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
+--          Refl
 
 -- minimum / maximum proofs
 
@@ -519,7 +519,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
 
@@ -536,7 +536,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)
 
@@ -554,18 +554,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/base.ipkg

@@ -15,6 +15,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/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
-||| 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.
+infix 5 #
+
+||| A pair type for use in operations on linear resources, which return a
+||| value and an updated resource
+public export
+data LPair : Type -> Type -> Type where
+     (#) : (x : a) -> (1 _ : b) -> LPair a b
+
 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/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

@@ -49,6 +49,12 @@ Eq CG where
   Gambit == Gambit = True
   _ == _ = False
 
+export
+Show CG where
+  show Chez = "chez"
+  show Racket = "racket"
+  show Gambit = "gambit"
+
 export
 availableCGs : List (String, CG)
 availableCGs
@@ -138,13 +144,14 @@ record Options where
   extensions : List LangExt
 
 defaultDirs : Dirs
-defaultDirs = MkDirs "." Nothing "build" 
-                     ("build" </> "exec") 
+defaultDirs = MkDirs "." Nothing "build"
+                     ("build" </> "exec")
                      "/usr/local" ["."] [] []
 
 defaultPPrint : PPrinter
 defaultPPrint = MkPPOpts False True False
 
+export
 defaultSession : Session
 defaultSession = MkSessionOpts False False False Chez 0 False False
                                Nothing Nothing Nothing Nothing

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/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
-                            (LinearMisuse _ _ r _)
-                              => branchOne
-                                   (do c <- runDelays 0 $ check linear elabinfo
-                                                nest env nVal (Just (gnf env tyv))
-                                       pure (fst c, snd c, linear))
-                                   (do c <- check (rigl |*| rigc)
-                                                elabinfo -- without preciseInf
-                                                nest env nVal (Just (gnf env tyv))
-                                       pure (fst c, snd c, rigMult rigl rigc))
-                                   r
+              (\err => case linearErr err of
+                            Just r
+                              => do branchOne
+                                     (do c <- runDelays 0 $ check linear elabinfo
+                                                  nest env nVal (Just (gnf env tyv))
+                                         pure (fst c, snd c, linear))
+                                     (do c <- check (rigl |*| rigc)
+                                                  elabinfo -- without preciseInf
+                                                  nest env nVal (Just (gnf env tyv))
+                                         pure (fst c, snd c, rigMult rigl rigc))
+                                     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/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

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)
-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)
-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 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 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 "?{_: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: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 ?{_: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)
-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)
+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: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/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)
-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)
-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 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 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 "?{_: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: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 ?{_: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)
-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)
+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: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/coverage008/expected

@@ -1,6 +1,6 @@
 1/1: Building wcov (wcov.idr)
 Main> Main.tfoo is total
 Main> Main.wfoo is total
-Main> Main.wbar is not covering due to call to function Main.with block in 1372
+Main> Main.wbar is not covering due to call to function Main.with block in 1376
 Main> Main.wbar1 is total
 Main> Bye for now!

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
-              (False @@ d) => ?now_3
+              (True # d) => ?now_2
+              (False # d) => ?now_3

tests/idris2/interactive009/expected

@@ -1,7 +1,7 @@
 1/1: Building Door (Door.idr)
-Main>               (y @@ res) => ?now_4
-Main>               (True @@ d) => ?now_4
-              (False @@ d) => ?now_5
+Main>               (val # y) => ?now_4
+Main>               (True # d) => ?now_4
+              (False # d) => ?now_5
 Main>  0 m : Type -> Type
  1 d : Door Open
    x : Integer

tests/idris2/interactive009/input

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

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/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/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
->               (False @@ d) => ?now_3
+>               (True # d) => ?now_2
+>               (False # d) => ?now_3

tests/idris2/literate006/expected

@@ -1,7 +1,7 @@
 1/1: Building Door (Door.lidr)
-Main> >               (y @@ res) => ?now_4
-Main> >               (True @@ d) => ?now_4
->               (False @@ d) => ?now_5
+Main> >               (val # y) => ?now_4
+Main> >               (True # d) => ?now_4
+>               (False # d) => ?now_5
 Main>  0 m : Type -> Type
  1 d : Door Open
    x : Integer

tests/idris2/literate006/input

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

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)
-                          Just res => pure (Just res @@ chan)
+                          Nothing => pure (Nothing # 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/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)
-           else pure1 (False @@ MkStore str)
+           then pure1 (True # 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
-              | False @@ s => do app $ putStrLn "Login failed"
-                                 app $ disconnect s
+         True # s <- login s pwd
+              | False # s => do app $ putStrLn "Login failed"
+                                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
-         else False @@ MkStore secret
+         then True # 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
-                       | False @@ s => do putStrLn "Incorrect password"
-                                          disconnect s
+             do let True # s = login s password
+                       | False # s => do putStrLn "Incorrect password"
+                                         disconnect s
                 putStrLn "Door opened"
                 let s = logout s 
                 putStrLn "Door closed"

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:
-Error during reflection: failed after generating Main.{plus:6151}
+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: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