A bit more library support

INSTALL.md

@@ -27,6 +27,14 @@ tests (if Idris 1 is available), then if all is well, install everything. The
 default installation directory is `$HOME/.idris2`. You can change this by
 setting the `PREFIX` variable in the `Makefile`.
 
+Other settings you can change in the `Makefile` are:
+
+* `OPT` which sets the optimisation level for compiling the generated C.  Leave
+  this blank for Idris 2 to build sooner, or set it to `-O2` for a faster
+  Idris 2 compiler. `-O2` takes a few minutes!
+* `CC` which sets the C compiler to use. `clang` is the default, but `gcc`
+  always works. `clang` generates code faster.
+
 ## Idris
 
 There are several sets of instructions on how to install Idris from source and

libs/base/Decidable/Equality.idr

@@ -91,6 +91,60 @@ implementation (DecEq t) => DecEq (Maybe t) where
 -- A postulate would be better, but erasure analysis may think they're needed
 -- for computation in a higher order setting.
 
+--------------------------------------------------------------------------------
+-- Tuple
+--------------------------------------------------------------------------------
+
+lemma_both_neq : (x = x' -> Void) -> (y = y' -> Void) -> ((x, y) = (x', y') -> Void)
+lemma_both_neq p_x_not_x' p_y_not_y' Refl = p_x_not_x' Refl
+
+lemma_snd_neq : (x = x) -> (y = y' -> Void) -> ((x, y) = (x, y') -> Void)
+lemma_snd_neq Refl p Refl = p Refl
+
+lemma_fst_neq_snd_eq : (x = x' -> Void) ->
+                       (y = y') ->
+                       ((x, y) = (x', y) -> Void)
+lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl
+
+export
+implementation (DecEq a, DecEq b) => DecEq (a, b) where
+  decEq (a, b) (a', b')     with (decEq a a')
+    decEq (a, b) (a, b')    | (Yes Refl) with (decEq b b')
+      decEq (a, b) (a, b)   | (Yes Refl) | (Yes Refl) = Yes Refl
+      decEq (a, b) (a, b')  | (Yes Refl) | (No p) = No (\eq => lemma_snd_neq Refl p eq)
+    decEq (a, b) (a', b')   | (No p)     with (decEq b b')
+      decEq (a, b) (a', b)  | (No p)     | (Yes Refl) =  No (\eq => lemma_fst_neq_snd_eq p Refl eq)
+      decEq (a, b) (a', b') | (No p)     | (No p') = No (\eq => lemma_both_neq p p' eq)
+
+--------------------------------------------------------------------------------
+-- List
+--------------------------------------------------------------------------------
+
+lemma_val_not_nil : (the (List _) (x :: xs) = Prelude.Nil {a = t} -> Void)
+lemma_val_not_nil Refl impossible
+
+lemma_x_eq_xs_neq : (x = y) -> (xs = ys -> Void) -> (the (List _) (x :: xs) = (y :: ys) -> Void)
+lemma_x_eq_xs_neq Refl p Refl = p Refl
+
+lemma_x_neq_xs_eq : (x = y -> Void) -> (xs = ys) -> (the (List _) (x :: xs) = (y :: ys) -> Void)
+lemma_x_neq_xs_eq p Refl Refl = p Refl
+
+lemma_x_neq_xs_neq : (x = y -> Void) -> (xs = ys -> Void) -> (the (List _) (x :: xs) = (y :: ys) -> Void)
+lemma_x_neq_xs_neq p p' Refl = p Refl
+
+implementation DecEq a => DecEq (List a) where
+  decEq [] [] = Yes Refl
+  decEq (x :: xs) [] = No lemma_val_not_nil
+  decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
+  decEq (x :: xs) (y :: ys) with (decEq x y)
+    decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
+      decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
+      decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq)
+    decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
+      decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)
+      decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)
+
+
 --------------------------------------------------------------------------------
 -- Int
 --------------------------------------------------------------------------------

libs/base/System.idr

@@ -16,6 +16,27 @@ export
 getArgs : IO (List String)
 getArgs = schemeCall (List String) "blodwen-args" []
 
+%foreign "scheme:getenv"
+prim_getEnv : String -> PrimIO String
+
+%foreign "scheme:blodwen-hasenv"
+prim_hasEnv : String -> PrimIO Int
+
+export
+getEnv : String -> IO (Maybe String)
+getEnv var
+   = do ok <- primIO $ prim_hasEnv var
+        if ok == 0
+           then pure Nothing
+           else map pure $ primIO (prim_getEnv var)
+
+%foreign "scheme:blodwen-system"
+prim_system : String -> PrimIO Int
+
+export
+system : String -> IO Int
+system cmd = primIO (prim_system cmd)
+
 export
 time : IO Integer
 time = schemeCall Integer "blodwen-time" []

libs/base/System/File.idr

@@ -16,6 +16,9 @@ data FilePtr : Type where
 %extern prim__writeLine : FilePtr -> String -> (1 x : %World) -> IORes (Either Int ())
 %extern prim__eof : FilePtr -> (1 x : %World) -> IORes Int
 
+%extern prim__fileModifiedTime : FilePtr -> (1 x : %World) ->
+                                 IORes (Either Int Integer)
+
 %extern prim__stdin : FilePtr
 %extern prim__stdout : FilePtr
 %extern prim__stderr : FilePtr
@@ -118,6 +121,12 @@ fEOF (FHandle f)
     = do res <- primIO (prim__eof f)
          pure (res /= 0)
 
+export
+fileModifiedTime : (h : File) -> IO (Either FileError Integer)
+fileModifiedTime (FHandle f)
+    = do res <- primIO (prim__fileModifiedTime f)
+         fpure res
+
 export
 readFile : String -> IO (Either FileError String)
 readFile file
@@ -138,3 +147,16 @@ readFile file
                   do Right str <- fGetLine h
                         | Left err => pure (Left err)
                      read (str :: acc) h
+
+||| Write a string to a file
+export
+writeFile : (filepath : String) -> (contents : String) ->
+            IO (Either FileError ())
+writeFile fn contents = do
+     Right h  <- openFile fn WriteTruncate
+        | Left err => pure (Left err)
+     Right () <- fPutStr h contents
+        | Left err => do closeFile h
+                         pure (Left err)
+     closeFile h
+     pure (Right ())

libs/prelude/Prelude.idr

@@ -1017,6 +1017,14 @@ isControl x
     = (x >= '\x0000' && x <= '\x001f')
        || (x >= '\x007f' && x <= '\x009f')
 
+public export
+chr : Int -> Char
+chr = prim__cast_IntChar
+
+public export
+ord : Char -> Int
+ord = prim__cast_CharInt
+
 ----------
 -- SHOW --
 ----------

src/Compiler/Scheme/Common.idr

@@ -159,7 +159,8 @@ schOp BelieveMe [_,_,x] = x
 public export
 data ExtPrim = CCall | SchemeCall
              | PutStr | GetStr | PutChar | GetChar
-             | FileOpen | FileClose | FileReadLine | FileWriteLine | FileEOF
+             | FileOpen | FileClose | FileReadLine | FileWriteLine
+             | FileEOF | FileModifiedTime
              | NewIORef | ReadIORef | WriteIORef
              | NewArray | ArrayGet | ArraySet
              | GetField | SetField
@@ -181,6 +182,7 @@ Show ExtPrim where
   show FileReadLine = "FileReadLine"
   show FileWriteLine = "FileWriteLine"
   show FileEOF = "FileEOF"
+  show FileModifiedTime = "FileModifiedTime"
   show NewIORef = "NewIORef"
   show ReadIORef = "ReadIORef"
   show WriteIORef = "WriteIORef"
@@ -211,6 +213,7 @@ toPrim pn@(NS _ n)
             (n == UN "prim__readLine", FileReadLine),
             (n == UN "prim__writeLine", FileWriteLine),
             (n == UN "prim__eof", FileEOF),
+            (n == UN "prim__fileModifiedTime", FileModifiedTime),
             (n == UN "prim__newIORef", NewIORef),
             (n == UN "prim__readIORef", ReadIORef),
             (n == UN "prim__writeIORef", WriteIORef),
@@ -368,6 +371,9 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx
                                         ++ !(schExp i vs str) ++ ")"
   schExtCommon i vs FileEOF [file, world]
       = pure $ mkWorld $ "(blodwen-eof " ++ !(schExp i vs file) ++ ")"
+  schExtCommon i vs FileModifiedTime [file, world]
+      = pure $ mkWorld $ fileOp $ "(blodwen-file-modified-time "
+                                        ++ !(schExp i vs file) ++ ")"
   schExtCommon i vs NewIORef [_, val, world]
       = pure $ mkWorld $ "(box " ++ !(schExp i vs val) ++ ")"
   schExtCommon i vs ReadIORef [_, ref, world]

src/Idris/Desugar.idr

@@ -34,14 +34,11 @@ import Control.Monad.State
 
 -- Desugaring from high level Idris syntax to TTImp involves:
 
--- Done:
 -- * Shunting infix operators into function applications according to precedence
 -- * Replacing 'do' notating with applications of (>>=)
 -- * Replacing pattern matching binds with 'case'
 -- * Changing tuples to 'Pair/MkPair'
 -- * List notation
-
--- Still TODO:
 -- * Replacing !-notation
 -- * Dependent pair notation
 -- * Idiom brackets

src/Idris/Main.idr

@@ -19,8 +19,6 @@ import Idris.ProcessIdr
 import Idris.REPL
 import Idris.SetOptions
 import Idris.Syntax
-import Idris.Socket
-import Idris.Socket.Data
 import Idris.Version
 
 import Data.Vect

src/Idris/REPLOpts.idr

@@ -1,7 +1,6 @@
 module Idris.REPLOpts
 
 import Idris.Syntax
-import Idris.Socket
 
 public export
 data OutputMode

support/chez/support.ss

@@ -161,6 +161,9 @@
         (get-char p)
         #\nul))
 
+(define (blodwen-file-modified-time p)
+    (time-second (file-modification-time p)))
+
 (define (blodwen-file-size p)
     (port-length p))
 
@@ -234,3 +237,9 @@
         (vector 0 '())
         (vector 1 '() (car args) (blodwen-build-args (cdr args)))))
     (blodwen-build-args (command-line)))
+
+(define (blodwen-hasenv var)
+  (if (eq? (getenv var) #f) 0 1))
+
+(define (blodwen-system cmd)
+  (system cmd))

support/racket/support.rkt

@@ -246,3 +246,8 @@
     (blodwen-build-args
       (cons (path->string (find-system-path 'run-file))
             (vector->list (current-command-line-arguments)))))
+
+(define (blodwen-system cmd)
+  (if (system cmd)
+      0
+      1))