Merge branch 'master' into fix-makefiles

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:

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 

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

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)

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

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

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 _

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

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"
 

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,

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

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

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)

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))))))
+  (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)))
 
@@ -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))))
 

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)