From c9b20911e1f0cc7e8549bb4112e4d0ba294352e5 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 12 Jun 2020 11:18:12 +0100 Subject: [PATCH 1/5] Add linear pair/dependent pair to the prelude I'm playing with some linear structures and finding these useful a lot, so good to have a consistent syntax for it. '#' is chosen because it's short, looks a bit like a cross if you look at it from the right angle (!) and so as not to clash with '@@' in preorder reasoning syntax. --- docs/source/app/linear.rst | 18 ++++++++-------- libs/base/Control/App.idr | 6 ------ libs/prelude/Builtin.idr | 32 ++++++++++++++++++++-------- tests/ideMode/ideMode001/expected | 12 +++++------ tests/ideMode/ideMode003/expected | 12 +++++------ tests/idris2/coverage008/expected | 2 +- tests/idris2/coverage010/expected | 2 +- tests/idris2/interactive009/Door.idr | 11 +++------- tests/idris2/interactive009/expected | 6 +++--- tests/idris2/interactive009/input | 4 ++-- tests/idris2/linear005/Linear.idr | 6 ------ tests/idris2/linear008/Door.idr | 6 ------ tests/idris2/literate006/Door.lidr | 11 +++------- tests/idris2/literate006/expected | 6 +++--- tests/idris2/literate006/input | 4 ++-- tests/idris2/real001/Channel.idr | 14 ++++++------ tests/idris2/real001/Linear.idr | 7 ------ tests/idris2/real001/MakeChans.idr | 14 ++++++------ tests/idris2/real001/TestProto.idr | 4 ++-- tests/idris2/real002/Control/App.idr | 6 ------ tests/idris2/real002/Store.idr | 14 ++++++------ tests/idris2/real002/StoreL.idr | 10 ++++----- tests/idris2/reflection003/expected | 2 +- 23 files changed, 91 insertions(+), 118 deletions(-) diff --git a/docs/source/app/linear.rst b/docs/source/app/linear.rst index c222155fe..93686f4c5 100644 --- a/docs/source/app/linear.rst +++ b/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" diff --git a/libs/base/Control/App.idr b/libs/base/Control/App.idr index 25aae13b9..ba6b30a9b 100644 --- a/libs/base/Control/App.idr +++ b/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 diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr index e6c464d90..7a1d82bcc 100644 --- a/libs/prelude/Builtin.idr +++ b/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. diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected index 9fb896acd..99066f17d 100644 --- a/tests/ideMode/ideMode001/expected +++ b/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) diff --git a/tests/ideMode/ideMode003/expected b/tests/ideMode/ideMode003/expected index 8aca93c6f..5a52769ba 100644 --- a/tests/ideMode/ideMode003/expected +++ b/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) diff --git a/tests/idris2/coverage008/expected b/tests/idris2/coverage008/expected index 76fe3b30a..77b301b2d 100644 --- a/tests/idris2/coverage008/expected +++ b/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! diff --git a/tests/idris2/coverage010/expected b/tests/idris2/coverage010/expected index b1bc35648..51e4daf93 100644 --- a/tests/idris2/coverage010/expected +++ b/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) diff --git a/tests/idris2/interactive009/Door.idr b/tests/idris2/interactive009/Door.idr index 67c61a71b..6ad72d9d7 100644 --- a/tests/idris2/interactive009/Door.idr +++ b/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 diff --git a/tests/idris2/interactive009/expected b/tests/idris2/interactive009/expected index a03467c9f..4191aca87 100644 --- a/tests/idris2/interactive009/expected +++ b/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 diff --git a/tests/idris2/interactive009/input b/tests/idris2/interactive009/input index 55512ee9b..4adf7e13a 100644 --- a/tests/idris2/interactive009/input +++ b/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 diff --git a/tests/idris2/linear005/Linear.idr b/tests/idris2/linear005/Linear.idr index 91614d754..e93d70f13 100644 --- a/tests/idris2/linear005/Linear.idr +++ b/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 diff --git a/tests/idris2/linear008/Door.idr b/tests/idris2/linear008/Door.idr index fded2b0f2..bac817a08 100644 --- a/tests/idris2/linear008/Door.idr +++ b/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 diff --git a/tests/idris2/literate006/Door.lidr b/tests/idris2/literate006/Door.lidr index 972fc1a71..953b41710 100644 --- a/tests/idris2/literate006/Door.lidr +++ b/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 diff --git a/tests/idris2/literate006/expected b/tests/idris2/literate006/expected index 832d268f7..ca96cd352 100644 --- a/tests/idris2/literate006/expected +++ b/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 diff --git a/tests/idris2/literate006/input b/tests/idris2/literate006/input index ab0e6f324..38632fbb1 100644 --- a/tests/idris2/literate006/input +++ b/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 diff --git a/tests/idris2/real001/Channel.idr b/tests/idris2/real001/Channel.idr index a098bdc84..d3d1d2d41 100644 --- a/tests/idris2/real001/Channel.idr +++ b/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 diff --git a/tests/idris2/real001/Linear.idr b/tests/idris2/real001/Linear.idr index 75dd16ea2..2ee4cde8e 100644 --- a/tests/idris2/real001/Linear.idr +++ b/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 diff --git a/tests/idris2/real001/MakeChans.idr b/tests/idris2/real001/MakeChans.idr index d90505c38..a6a452451 100644 --- a/tests/idris2/real001/MakeChans.idr +++ b/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 diff --git a/tests/idris2/real001/TestProto.idr b/tests/idris2/real001/TestProto.idr index cdf968c72..f361bf054 100644 --- a/tests/idris2/real001/TestProto.idr +++ b/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" diff --git a/tests/idris2/real002/Control/App.idr b/tests/idris2/real002/Control/App.idr index f420419df..87a35547f 100644 --- a/tests/idris2/real002/Control/App.idr +++ b/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 diff --git a/tests/idris2/real002/Store.idr b/tests/idris2/real002/Store.idr index 9b0c3a966..beedbb172 100644 --- a/tests/idris2/real002/Store.idr +++ b/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" diff --git a/tests/idris2/real002/StoreL.idr b/tests/idris2/real002/StoreL.idr index b362e811c..c90de49c9 100644 --- a/tests/idris2/real002/StoreL.idr +++ b/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" diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 34042f6d7..e023fc7dc 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -12,4 +12,4 @@ 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: 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:6078} +Error during reflection: failed after generating Main.{plus:6087} From b2c7029b6bb0dfbcd6bcaf604d7e86f01cc33d78 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 12 Jun 2020 13:47:15 +0100 Subject: [PATCH 2/5] Improve inference of linearity in let This involves a bit of backtracking in linearity checking, which I'd prefer to avoid, but it won't hurt in the normal case. If checking a binder fails due to linearity misuse, try again at linear multiplicity. --- src/Core/LinearCheck.idr | 8 +++++++- src/TTImp/Elab/Binders.idr | 30 +++++++++++++++++++----------- src/TTImp/Elab/Delayed.idr | 1 + 3 files changed, 27 insertions(+), 12 deletions(-) diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index 00c3cbba8..1a367aa96 100644 --- a/src/Core/LinearCheck.idr +++ b/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 diff --git a/src/TTImp/Elab/Binders.idr b/src/TTImp/Elab/Binders.idr index bfe71ecda..4a306fabb 100644 --- a/src/TTImp/Elab/Binders.idr +++ b/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 diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr index f233ab3c1..98b2ed641 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/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 From 1c576cb068c8d2a18e672f3b0ca07d3d83064077 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 12 Jun 2020 14:08:00 +0100 Subject: [PATCH 3/5] Add experimental support for linear arrays Backed by Data.IOArray. Also moved the array external primitives to a separate module Data.IOArray.Prims, since the next step is to add a linear bounded array type where the bounds checks are done at compile time, so we'll want to read and write without bounds likes. --- libs/base/Data/IOArray.idr | 11 +---- libs/base/Data/IOArray/Prims.idr | 11 +++++ libs/base/base.ipkg | 1 + libs/contrib/Data/Linear/Array.idr | 74 ++++++++++++++++++++++++++++++ libs/contrib/contrib.ipkg | 2 + 5 files changed, 89 insertions(+), 10 deletions(-) create mode 100644 libs/base/Data/IOArray/Prims.idr create mode 100644 libs/contrib/Data/Linear/Array.idr diff --git a/libs/base/Data/IOArray.idr b/libs/base/Data/IOArray.idr index 487127e1b..3d87dda01 100644 --- a/libs/base/Data/IOArray.idr +++ b/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 diff --git a/libs/base/Data/IOArray/Prims.idr b/libs/base/Data/IOArray/Prims.idr new file mode 100644 index 000000000..087da583e --- /dev/null +++ b/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 () diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index b0e955755..a2c770f89 100644 --- a/libs/base/base.ipkg +++ b/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, diff --git a/libs/contrib/Data/Linear/Array.idr b/libs/contrib/Data/Linear/Array.idr new file mode 100644 index 000000000..46706f411 --- /dev/null +++ b/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 + a' = case val of + Nothing => a' + Just v => write a' pos v in + copyContent (pos - 1) a a' diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index cb3514d51..04af84a7f 100644 --- a/libs/contrib/contrib.ipkg +++ b/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, From ec89b9789628b48704862eeb3309d75cf92d4e3b Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 12 Jun 2020 14:12:32 +0100 Subject: [PATCH 4/5] Add note to CHANGELOG --- CHANGELOG.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f16b4b50..4d1f9dac8 100644 --- a/CHANGELOG.md +++ b/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 ---------------------------- From 84adbe6dc8d23a45ac269dba406ddd339ccc5b95 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 12 Jun 2020 14:18:57 +0100 Subject: [PATCH 5/5] Be explicit about multiplicity in Array The bootstrap version can't infer it! --- libs/contrib/Data/Linear/Array.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/contrib/Data/Linear/Array.idr b/libs/contrib/Data/Linear/Array.idr index 46706f411..83930d124 100644 --- a/libs/contrib/Data/Linear/Array.idr +++ b/libs/contrib/Data/Linear/Array.idr @@ -68,7 +68,7 @@ copyArray newsize a = if pos < 0 then (a, a') else let val # a = mread a pos - a' = case val of + 1 a' = case val of Nothing => a' Just v => write a' pos v in copyContent (pos - 1) a a'