From 2f34f85e2f222c188e6032aa0d104952bee31ecb Mon Sep 17 00:00:00 2001 From: Frederik Vigen Date: Sat, 6 Jun 2020 20:51:19 +0200 Subject: [PATCH 01/14] Added fix to recvAll that doesn't use signal (Left 0) but the size of the buffer --- libs/network/Network/Socket.idr | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr index 485bee096..e7ebf26e0 100644 --- a/libs/network/Network/Socket.idr +++ b/libs/network/Network/Socket.idr @@ -173,10 +173,10 @@ recvAll sock = recvRec sock [] 64 recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String) recvRec sock acc n = do res <- recv sock n case res of - Left 0 => pure (Right $ concat $ reverse acc) Left c => pure (Left c) - Right (str, _) => let n' = min (n * 2) 65536 in - recvRec sock (str :: acc) n' + Right (str, res) => let n' = min (n * 2) 65536 in + if res < n then pure (Right $ concat $ reverse $ str :: acc) + else recvRec sock (str :: acc) n' ||| Send a message. ||| From 2db3a61160d387de96b82ef10ca6816505c67103 Mon Sep 17 00:00:00 2001 From: Nikita Vilunov Date: Mon, 8 Jun 2020 01:31:16 +0300 Subject: [PATCH 02/14] implement "--repl" --- src/Idris/Main.idr | 2 +- src/Idris/Package.idr | 16 ++++++++++------ 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index 934348488..e14f3dd85 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -131,7 +131,6 @@ stMain opts defs <- initDefs c <- newRef Ctxt defs s <- newRef Syn initSyntax - m <- newRef MD initMetadata addPrimitives setWorkingDir "." @@ -157,6 +156,7 @@ stMain opts when (checkVerbose opts) $ -- override Quiet if implicitly set setOutput (REPL False) u <- newRef UST initUState + m <- newRef MD initMetadata updateREPLOpts session <- getSession when (not $ nobanner session) $ diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 16fcddfd7..4e641258a 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -444,15 +444,16 @@ getParseErrorLoc fname _ = replFC -- Just load the 'Main' module, if it exists, which will involve building -- it if necessary runRepl : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> PkgDesc -> List CLOpt -> Core () -runRepl pkg opts - = do addDeps pkg - processOptions (options pkg) - preOptions opts - throw (InternalError "Not implemented") +runRepl pkg opts = do + u <- newRef UST initUState + m <- newRef MD initMetadata + repl {u} {s} + processPackage : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> @@ -480,7 +481,10 @@ processPackage cmd file opts | errs => coreLift (exitWith (ExitFailure 1)) install pkg opts Clean => clean pkg opts - REPL => runRepl pkg opts + REPL => do + [] <- build pkg opts + | errs => coreLift (exitWith (ExitFailure 1)) + runRepl pkg opts record POptsFilterResult where constructor MkPFR From 560d472502b06df73a74925d0de11c566a704847 Mon Sep 17 00:00:00 2001 From: Nikita Vilunov Date: Mon, 8 Jun 2020 19:21:22 +0300 Subject: [PATCH 03/14] add a test for --repl --- tests/Main.idr | 2 +- tests/idris2/pkg004/Dummy.idr | 7 +++++++ tests/idris2/pkg004/dummy.ipkg | 9 +++++++++ tests/idris2/pkg004/expected | 9 +++++++++ tests/idris2/pkg004/input | 6 ++++++ tests/idris2/pkg004/run | 3 +++ 6 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 tests/idris2/pkg004/Dummy.idr create mode 100644 tests/idris2/pkg004/dummy.ipkg create mode 100644 tests/idris2/pkg004/expected create mode 100644 tests/idris2/pkg004/input create mode 100755 tests/idris2/pkg004/run diff --git a/tests/Main.idr b/tests/Main.idr index 43a38b45c..3f16191c4 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -79,7 +79,7 @@ idrisTests "perror001", "perror002", "perror003", "perror004", "perror005", "perror006", -- Packages and ipkg files - "pkg001", "pkg002", "pkg003", + "pkg001", "pkg002", "pkg003", "pkg004", -- Larger programs arising from real usage. Typically things with -- interesting interactions between features "real001", "real002", diff --git a/tests/idris2/pkg004/Dummy.idr b/tests/idris2/pkg004/Dummy.idr new file mode 100644 index 000000000..8a3d144df --- /dev/null +++ b/tests/idris2/pkg004/Dummy.idr @@ -0,0 +1,7 @@ +module Dummy + +something : String +something = "Something something" + +data Proxy : Type -> Type where + MkProxy : Proxy a diff --git a/tests/idris2/pkg004/dummy.ipkg b/tests/idris2/pkg004/dummy.ipkg new file mode 100644 index 000000000..fe45e2c77 --- /dev/null +++ b/tests/idris2/pkg004/dummy.ipkg @@ -0,0 +1,9 @@ +package dummy + +authors = "Joe Bloggs" +maintainers = "Joe Bloggs" +license = "BSD3 but see LICENSE for more information" +brief = "This is a dummy package." +readme = "README.md" + +modules = Dummy diff --git a/tests/idris2/pkg004/expected b/tests/idris2/pkg004/expected new file mode 100644 index 000000000..26f5df61b --- /dev/null +++ b/tests/idris2/pkg004/expected @@ -0,0 +1,9 @@ +1/1: Building Dummy (Dummy.idr) +Dummy> (interactive):1:4--1:13:Undefined name undefined +Dummy> Dummy.something : String +Dummy> "Something something" +Dummy> Dummy.Proxy : Type -> Type +Dummy> Proxy +Dummy> Proxy String : Type +Dummy> +Bye for now! diff --git a/tests/idris2/pkg004/input b/tests/idris2/pkg004/input new file mode 100644 index 000000000..0a032ad80 --- /dev/null +++ b/tests/idris2/pkg004/input @@ -0,0 +1,6 @@ +:t undefined +:t something +something +:t Proxy +Proxy +:t Proxy String diff --git a/tests/idris2/pkg004/run b/tests/idris2/pkg004/run new file mode 100755 index 000000000..3e75fd7db --- /dev/null +++ b/tests/idris2/pkg004/run @@ -0,0 +1,3 @@ +$1 --repl dummy.ipkg < input + +rm -rf build From 90997e9a22f26253f5bbb667025f13eb4df42f44 Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Fri, 12 Jun 2020 15:11:51 +0600 Subject: [PATCH 04/14] Remove hardcoded default GC from command line options --- src/Core/Options.idr | 11 +++++++++-- src/Core/TTC.idr | 8 ++++---- src/Idris/CommandLine.idr | 6 ++++-- 3 files changed, 17 insertions(+), 8 deletions(-) diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 8812c61d3..4c503461f 100644 --- a/src/Core/Options.idr +++ b/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 diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index efbd2a0a5..2e6557466 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -731,14 +731,14 @@ TTC CDef where export TTC CG where toBuf b Chez = tag 0 - toBuf b Racket = tag 2 - toBuf b Gambit = tag 3 + toBuf b Racket = tag 1 + toBuf b Gambit = tag 2 fromBuf b = case !getTag of 0 => pure Chez - 2 => pure Racket - 3 => pure Gambit + 1 => pure Racket + 2 => pure Gambit _ => corrupt "CG" export diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 52943bfe8..9c60cc1bd 100644 --- a/src/Idris/CommandLine.idr +++ b/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"), From 01c79f17d27ad7f98828e8f315b0f08cc16fe8be Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Fri, 12 Jun 2020 15:31:48 +0600 Subject: [PATCH 05/14] Change the TTC version --- src/Core/Binary.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 4aef17d22..f465188a9 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -30,7 +30,7 @@ import Data.Buffer -- TTC files can only be compatible if the version number is the same export ttcVersion : Int -ttcVersion = 33 +ttcVersion = 34 export checkTTCVersion : String -> Int -> Int -> Core () From 4d7e6eef6e41f4cc571edc44b38009e4c4568d7b Mon Sep 17 00:00:00 2001 From: Kamil Shakirov Date: Fri, 12 Jun 2020 15:36:38 +0600 Subject: [PATCH 06/14] Revert TTC changes --- src/Core/Binary.idr | 2 +- src/Core/TTC.idr | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index f465188a9..4aef17d22 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -30,7 +30,7 @@ import Data.Buffer -- TTC files can only be compatible if the version number is the same export ttcVersion : Int -ttcVersion = 34 +ttcVersion = 33 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 2e6557466..efbd2a0a5 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -731,14 +731,14 @@ TTC CDef where export TTC CG where toBuf b Chez = tag 0 - toBuf b Racket = tag 1 - toBuf b Gambit = tag 2 + toBuf b Racket = tag 2 + toBuf b Gambit = tag 3 fromBuf b = case !getTag of 0 => pure Chez - 1 => pure Racket - 2 => pure Gambit + 2 => pure Racket + 3 => pure Gambit _ => corrupt "CG" export From c9b20911e1f0cc7e8549bb4112e4d0ba294352e5 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 12 Jun 2020 11:18:12 +0100 Subject: [PATCH 07/14] 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 4b7fbb037133ddeaf187c1ba95dc891b406c6950 Mon Sep 17 00:00:00 2001 From: Niklas Larsson Date: Fri, 12 Jun 2020 12:46:19 +0200 Subject: [PATCH 08/14] Fix overly nitpicky reflection test See #287 --- tests/idris2/reflection003/expected | 10 +++++----- tests/idris2/reflection003/refprims.idr | 8 +++++++- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 34042f6d7..0004f2e74 100644 --- a/tests/idris2/reflection003/expected +++ b/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:6078} +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} diff --git a/tests/idris2/reflection003/refprims.idr b/tests/idris2/reflection003/refprims.idr index 952258575..9fedc07b9 100644 --- a/tests/idris2/reflection003/refprims.idr +++ b/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 From f7cf2dfb06a1db7469749420111c9a0a9dff50d1 Mon Sep 17 00:00:00 2001 From: Jan de Muijnck-Hughes Date: Fri, 12 Jun 2020 09:50:06 +0100 Subject: [PATCH 09/14] Ported safe indexing of Lists from Idris1 prelude. --- libs/base/Data/List.idr | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index a892dd379..3b187dda0 100644 --- a/libs/base/Data/List.idr +++ b/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) From da81146388e2bf59790b879ec4dac5c39a728910 Mon Sep 17 00:00:00 2001 From: Jan de Muijnck-Hughes Date: Fri, 12 Jun 2020 10:39:57 +0100 Subject: [PATCH 10/14] Remove unsolved holes from `base`. Having unsolved holes in a 'core' library unneccessarily pollutes the list of holes shown to the user. Thus, having unfilled holes in a 'core' library is not right. These constructs can be re-added once the holes have been filled in. --- libs/base/Data/Nat.idr | 46 +++++++++++++++++++++--------------------- 1 file changed, 23 insertions(+), 23 deletions(-) diff --git a/libs/base/Data/Nat.idr b/libs/base/Data/Nat.idr index a8854de6a..c62c0165f 100644 --- a/libs/base/Data/Nat.idr +++ b/libs/base/Data/Nat.idr @@ -466,8 +466,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' = @@ -475,21 +475,21 @@ multPowerPowerPlus : (base, exp, exp' : Nat) -> -- rewrite sym $ multAssociative base (power base exp) (power base exp') in -- Refl -powerOneNeutral : (base : Nat) -> power base 1 = base -powerOneNeutral base = 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 @@ -506,7 +506,7 @@ maximumCommutative Z (S _) = Refl maximumCommutative (S _) Z = Refl maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl -maximumIdempotent : (n : Nat) -> maximum n n = n +-- maximumIdempotent : (n : Nat) -> maximum n n = n -- maximumIdempotent Z = Refl -- maximumIdempotent (S k) = cong $ maximumIdempotent k @@ -523,7 +523,7 @@ minimumCommutative Z (S _) = Refl minimumCommutative (S _) Z = Refl minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl -minimumIdempotent : (n : Nat) -> minimum n n = n +-- minimumIdempotent : (n : Nat) -> minimum n n = n -- minimumIdempotent Z = Refl -- minimumIdempotent (S k) = cong (minimumIdempotent k) @@ -541,18 +541,18 @@ maximumSuccSucc : (left, right : Nat) -> S (maximum left right) = maximum (S left) (S right) maximumSuccSucc _ _ = Refl -sucMaxL : (l : Nat) -> maximum (S l) l = (S l) +-- sucMaxL : (l : Nat) -> maximum (S l) l = (S l) -- sucMaxL Z = Refl -- sucMaxL (S l) = cong $ sucMaxL l -sucMaxR : (l : Nat) -> maximum l (S l) = (S l) +-- sucMaxR : (l : Nat) -> maximum l (S l) = (S l) -- sucMaxR Z = Refl -- sucMaxR (S l) = cong $ sucMaxR l -sucMinL : (l : Nat) -> minimum (S l) l = l +-- sucMinL : (l : Nat) -> minimum (S l) l = l -- sucMinL Z = Refl -- sucMinL (S l) = cong $ sucMinL l -sucMinR : (l : Nat) -> minimum l (S l) = l +-- sucMinR : (l : Nat) -> minimum l (S l) = l -- sucMinR Z = Refl -- sucMinR (S l) = cong $ sucMinR l From b2c7029b6bb0dfbcd6bcaf604d7e86f01cc33d78 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Fri, 12 Jun 2020 13:47:15 +0100 Subject: [PATCH 11/14] 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 12/14] 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 13/14] 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 14/14] 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'