From 5088cb621cb07b90cacfa9869f0910bcf734e452 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Wed, 13 May 2020 13:39:09 +0300 Subject: [PATCH 1/5] Idiom brackets syntax was fixed in the docs --- docs/source/tutorial/interfaces.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/source/tutorial/interfaces.rst b/docs/source/tutorial/interfaces.rst index c63248b..70e57f1 100644 --- a/docs/source/tutorial/interfaces.rst +++ b/docs/source/tutorial/interfaces.rst @@ -470,13 +470,13 @@ above (this is defined in the Idris library): _ <*> _ = Nothing Using ``<*>`` we can use this implementation as follows, where a function -application ``[ f a1 …an |]`` is translated into ``pure f <*> a1 <*> +application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*> … <*> an``: .. code-block:: idris m_add' : Maybe Int -> Maybe Int -> Maybe Int - m_add' x y = [ x + y |] + m_add' x y = [| x + y |] An error-handling interpreter ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ From 9a0608b01f77a3f60dbd04e2ea49d3583bff2316 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 13 May 2020 12:05:00 +0100 Subject: [PATCH 2/5] Add idris_crash function Because sometimes all you can do is give up (e.g. failing to allocate memory for some crucial thing). --- libs/base/System/File.idr | 2 +- libs/prelude/Builtin.idr | 4 ++++ src/Compiler/Scheme/Common.idr | 1 + src/Core/Primitives.idr | 10 +++++++++- src/Core/TT.idr | 2 ++ src/Core/TTC.idr | 2 ++ 6 files changed, 19 insertions(+), 2 deletions(-) diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index 1c71d6a..ed1cb18 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -26,7 +26,7 @@ prim_fileErrno : PrimIO Int %foreign support "idris2_readLine" prim__readLine : FilePtr -> PrimIO (Ptr String) -%foreign support "idris2_readLine" +%foreign support "idris2_readChars" prim__readChars : Int -> FilePtr -> PrimIO (Ptr String) %foreign support "idris2_writeLine" prim__writeLine : FilePtr -> String -> PrimIO Int diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr index fce06f3..bca7ffe 100644 --- a/libs/prelude/Builtin.idr +++ b/libs/prelude/Builtin.idr @@ -140,3 +140,7 @@ trans Refl Refl = Refl public export believe_me : a -> b believe_me = prim__believe_me _ _ + +export partial +idris_crash : String -> a +idris_crash = prim__crash _ diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index 45910be..82874fa 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -156,6 +156,7 @@ schOp (Cast IntType CharType) [x] = op "integer->char" [x] schOp (Cast from to) [x] = "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")" schOp BelieveMe [_,_,x] = x +schOp Crash [_,msg] = "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))" ||| Extended primitives for the scheme backend, outside the standard set of primFn public export diff --git a/src/Core/Primitives.idr b/src/Core/Primitives.idr index 15c8ee8..c757bad 100644 --- a/src/Core/Primitives.idr +++ b/src/Core/Primitives.idr @@ -287,6 +287,12 @@ believeMeTy Bind emptyFC (UN "x") (Pi top Explicit (Local emptyFC Nothing _ (Later First))) $ Local emptyFC Nothing _ (Later First) +crashTy : ClosedTerm +crashTy + = Bind emptyFC (UN "a") (Pi erased Explicit (TType emptyFC)) $ + Bind emptyFC (UN "msg") (Pi top Explicit (PrimVal emptyFC StringType)) $ + Local emptyFC Nothing _ (Later First) + castTo : Constant -> Vect 1 (NF vars) -> Maybe (NF vars) castTo IntType = castInt castTo IntegerType = castInteger @@ -385,6 +391,7 @@ opName DoubleFloor = prim "doubleFloor" opName DoubleCeiling = prim "doubleCeiling" opName (Cast x y) = prim $ "cast_" ++ show x ++ show y opName BelieveMe = prim $ "believe_me" +opName Crash = prim $ "crash" export allPrimitives : List Prim @@ -416,7 +423,8 @@ allPrimitives = MkPrim StrAppend (arithTy StringType) isTotal, MkPrim StrReverse (predTy StringType StringType) isTotal, MkPrim StrSubstr (constTy3 IntType IntType StringType StringType) isTotal, - MkPrim BelieveMe believeMeTy isTotal] ++ + MkPrim BelieveMe believeMeTy isTotal, + MkPrim Crash crashTy notCovering] ++ [MkPrim DoubleExp doubleTy isTotal, MkPrim DoubleLog doubleTy isTotal, diff --git a/src/Core/TT.idr b/src/Core/TT.idr index a189dad..7ec6134 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -147,6 +147,7 @@ data PrimFn : Nat -> Type where Cast : Constant -> Constant -> PrimFn 1 BelieveMe : PrimFn 3 + Crash : PrimFn 2 export Show (PrimFn arity) where @@ -187,6 +188,7 @@ Show (PrimFn arity) where show DoubleCeiling = "op_doubleCeiling" show (Cast x y) = "cast-" ++ show x ++ "-" ++ show y show BelieveMe = "believe_me" + show Crash = "crash" public export data PiInfo t = Implicit | Explicit | AutoImplicit | DefImplicit t diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index cd3416b..04b14ba 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -517,6 +517,7 @@ TTC (PrimFn n) where toBuf b (Cast x y) = do tag 99; toBuf b x; toBuf b y toBuf b BelieveMe = tag 100 + toBuf b Crash = tag 101 fromBuf {n} b = case n of @@ -571,6 +572,7 @@ TTC (PrimFn n) where 37 => do ty <- fromBuf b; pure (BAnd ty) 38 => do ty <- fromBuf b; pure (BOr ty) 39 => do ty <- fromBuf b; pure (BXOr ty) + 101 => pure Crash _ => corrupt "PrimFn 2" fromBuf3 : Ref Bin Binary -> From 18dff43d2b66b7b7799555c02187645bcbcf7d53 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 13 May 2020 12:18:21 +0100 Subject: [PATCH 3/5] Move Concurrency.Raw to new FFI --- libs/base/System/Concurrency/Raw.idr | 58 +++++++++++++++++++++------- support/chez/support.ss | 2 +- support/gambit/support.scm | 6 +-- support/racket/support.rkt | 2 +- 4 files changed, 48 insertions(+), 20 deletions(-) diff --git a/libs/base/System/Concurrency/Raw.idr b/libs/base/System/Concurrency/Raw.idr index 85478c3..38f4886 100644 --- a/libs/base/System/Concurrency/Raw.idr +++ b/libs/base/System/Concurrency/Raw.idr @@ -1,55 +1,83 @@ module System.Concurrency.Raw +-- At the moment this is pretty fundamentally tied to the Scheme RTS +-- Given that different back ends will have entirely different threading +-- models, it might be unavoidable, but we might want to think about possible +-- primitives that back ends should support. + +%foreign "scheme:blodwen-thisthread" +prim__threadID : PrimIO ThreadID +%foreign "scheme:blodwen-set-thread-data" +prim__setThreadData : {a : Type} -> a -> PrimIO () +%foreign "scheme:blodwen-get-thread-data" +prim__getThreadData : (a : Type) -> PrimIO a + -- Mutexes and condition variables. export threadID : IO ThreadID -threadID = schemeCall ThreadID "blodwen-thisthread" [] +threadID = primIO prim__threadID export setThreadData : {a : Type} -> a -> IO () -setThreadData val = schemeCall () "blodwen-set-thread-data" [val] +setThreadData val = primIO (prim__setThreadData val) export getThreadData : (a : Type) -> IO a -getThreadData a = schemeCall a "blodwen-get-thread-data" [] +getThreadData a = primIO (prim__getThreadData a) export -data Mutex : Type where +data Mutex : Type where [external] + +%foreign "scheme:blodwen-mutex" +prim__makeMutex : PrimIO Mutex +%foreign "scheme:blodwen-lock" +prim__mutexAcquire : Mutex -> PrimIO () +%foreign "scheme:blodwen-unlock" +prim__mutexRelease : Mutex -> PrimIO () export makeMutex : IO Mutex -makeMutex = schemeCall Mutex "blodwen-mutex" [] +makeMutex = primIO prim__makeMutex export mutexAcquire : Mutex -> IO () -mutexAcquire m = schemeCall () "blodwen-lock" [m] +mutexAcquire m = primIO (prim__mutexAcquire m) export mutexRelease : Mutex -> IO () -mutexRelease m = schemeCall () "blodwen-unlock" [m] +mutexRelease m = primIO (prim__mutexRelease m) export -data Condition : Type where +data Condition : Type where [external] + +%foreign "scheme:blodwen-condition" +prim__makeCondition : PrimIO Condition +%foreign "scheme:blodwen-condition-wait" +prim__conditionWait : Condition -> Mutex -> PrimIO () +%foreign "scheme:blodwen-condition-wait-timoue" +prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO () +%foreign "scheme:blodwen-condition-signal" +prim__conditionSignal : Condition -> PrimIO () +%foreign "scheme:blodwen-condition-broadcast" +prim__conditionBroadcast : Condition -> PrimIO () export makeCondition : IO Condition -makeCondition = schemeCall Condition "blodwen-condition" [] +makeCondition = primIO prim__makeCondition export conditionWait : Condition -> Mutex -> IO () -conditionWait c m = schemeCall () "blodwen-condition-wait" [c, m] +conditionWait c m = primIO (prim__conditionWait c m) export conditionWaitTimeout : Condition -> Mutex -> Int -> IO () -conditionWaitTimeout c m t - = schemeCall () "blodwen-condition-wait-timeout" [c, m, t] +conditionWaitTimeout c m t = primIO (prim__conditionWaitTimeout c m t) export conditionSignal : Condition -> IO () -conditionSignal c = schemeCall () "blodwen-condition-signal" [c] +conditionSignal c = primIO (prim__conditionSignal c) export conditionBroadcast : Condition -> IO () -conditionBroadcast c = schemeCall () "blodwen-condition-broadcast" [c] - +conditionBroadcast c = primIO (prim__conditionBroadcast c) diff --git a/support/chez/support.ss b/support/chez/support.ss index 244be62..7eec01b 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -80,7 +80,7 @@ (define (blodwen-thread p) (fork-thread (lambda () (p (vector 0))))) -(define (blodwen-get-thread-data) +(define (blodwen-get-thread-data ty) (blodwen-thread-data)) (define (blodwen-set-thread-data a) diff --git a/support/gambit/support.scm b/support/gambit/support.scm index 2f28148..79c4318 100644 --- a/support/gambit/support.scm +++ b/support/gambit/support.scm @@ -78,15 +78,15 @@ (define (blodwen-get-char p) (if (input-port? p) (let ((chr (read-char p))) - (if (eof-object? chr) #\null chr)) - #\null)) + (if (eof-object? chr) #\nul chr)) + #\nul)) ;; Threads (define (blodwen-thread p) (thread-start! (make-thread (lambda () (p #(0)))))) -(define (blodwen-get-thread-data) +(define (blodwen-get-thread-data ty) (let ((data (thread-specific (current-thread)))) (if (eq? data #!void) #f data))) diff --git a/support/racket/support.rkt b/support/racket/support.rkt index d7f7a99..3a38955 100644 --- a/support/racket/support.rkt +++ b/support/racket/support.rkt @@ -77,7 +77,7 @@ (define (blodwen-thread p) (thread (lambda () (p (vector 0))))) -(define (blodwen-get-thread-data) +(define (blodwen-get-thread-data ty) (thread-cell-ref blodwen-thread-data)) (define (blodwen-set-thread-data a) From 68081ed86cdc95d13bac80fe7ec78d76821583ec Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 13 May 2020 12:41:38 +0100 Subject: [PATCH 4/5] Some scheme generation fixes In racket, importing date and srfi/19 fails. Also some minor edits to gambit support code. --- src/Compiler/Scheme/Racket.idr | 3 +-- support/gambit/support.scm | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index d2acd1b..c135a9b 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -38,9 +38,8 @@ schHeader libs "(require racket/system)\n" ++ -- for system "(require rnrs/bytevectors-6)\n" ++ -- for buffers "(require rnrs/io/ports-6)\n" ++ -- for file handling - "(require srfi/19)\n" ++ -- for file handling + "(require srfi/19)\n" ++ -- for file handling and data "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C - "(require racket/date)\n" ++ -- for date libs ++ "(let ()\n" diff --git a/support/gambit/support.scm b/support/gambit/support.scm index 79c4318..a363d9e 100644 --- a/support/gambit/support.scm +++ b/support/gambit/support.scm @@ -84,7 +84,7 @@ ;; Threads (define (blodwen-thread p) - (thread-start! (make-thread (lambda () (p #(0)))))) + (thread-start! (make-thread (lambda () (p '#(0)))))) (define (blodwen-get-thread-data ty) (let ((data (thread-specific (current-thread)))) @@ -117,7 +117,7 @@ (define (blodwen-args) (define (blodwen-build-args args) (if (null? args) - #(0) ; Prelude.List + (vector 0) ; Prelude.List (vector 1 (car args) (blodwen-build-args (cdr args))))) (blodwen-build-args (cdr (command-line)))) From 5285b36a4f59338ea72c556ea8b7d357bf1f9f69 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 13 May 2020 13:12:41 +0100 Subject: [PATCH 5/5] Update CHANGELOG and CONTRIBUTORS Trying to keep both up to date - apologies if I'm missed anyone. I got the list from the git logs, but feel free to edit yourself in or out as you prefer. --- CHANGELOG.md | 6 ++++++ CONTRIBUTORS | 9 +++++++++ libs/contrib/contrib.ipkg | 28 ++++++++++++++++------------ 3 files changed, 31 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 542cc76..d5320be 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -22,6 +22,12 @@ Language extensions: evaluation, following the rules from "Scrapping Your Inefficient Engine" (ICFP 2010, Brady & Hammond) +Library additions: + +* Additional file management operations in `base` +* New modules in `contrib` for time (`System.Clock`); JSON (`Language.JSON.*`); + random numbers (`System.Random`) + Other improvements: * Various performance improvements in the typechecker: diff --git a/CONTRIBUTORS b/CONTRIBUTORS index 9015d0d..f076133 100644 --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -1,5 +1,6 @@ Thanks to the following for their help and contributions to Idris 2: +Abdelhakim Qbaich Alex Gryzlov Alex Silva Andre Kuhlenschmidt @@ -9,16 +10,20 @@ Brian Wignall Christian Rasmussen David Smith Edwin Brady +Fabián Heredia Montiel +George Pollard GhiOm Guillaume Allais Ilya Rezvov Jan de Muijnck-Hughes +Jeetu Kamil Shakirov Bryn Keller Kevin Boulain lodi LuoChen Marc Petit-Huguenin +MarcelineVQ Marshall Bowers Matthew Wilson Matus Tejiscak @@ -26,10 +31,14 @@ Michael Morgan Milan Kral Molly Miller Mounir Boudia +Nicolas Biri Niklas Larsson Ohad Kammar Peter Hajdu +Rohit Grover +Rui Barreiro Simon Chatterjee +then0rTh Theo Butler Tim Süberkrüb Timmy Jose diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg index 968e07f..d502d24 100644 --- a/libs/contrib/contrib.ipkg +++ b/libs/contrib/contrib.ipkg @@ -1,21 +1,13 @@ package contrib -modules = Syntax.WithProof, - Syntax.PreorderReasoning, +modules = Control.Delayed, + Data.List.TailRec, Data.Bool.Extra, Data.SortedMap, Data.SortedSet, Data.String.Extra, - Text.Token, - Text.Quantity, - Control.Delayed, - Text.Parser, - Text.Lexer, - Text.Parser.Core, - Text.Lexer.Core, - System.Clock, - System.Random, + Language.JSON, Language.JSON.Data, Language.JSON.Lexer, @@ -24,4 +16,16 @@ modules = Syntax.WithProof, Language.JSON.String.Lexer, Language.JSON.String.Parser, Language.JSON.String.Tokens, - Language.JSON.Tokens + Language.JSON.Tokens, + + Text.Token, + Text.Quantity, + Text.Parser, + Text.Lexer, + Text.Parser.Core, + Text.Lexer.Core, + + System.Clock, + System.Random, + Syntax.WithProof, + Syntax.PreorderReasoning