Merge pull request #292 from edwinb/linear-things

Some small linearity improvements, and linear arrays

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/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/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/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/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 2071(287)
+	Calls non covering function Main.case block in 2075(296)

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"