[ cleanup ] Post v0.7.0 cleanup

.github/workflows/ci-idris2-and-libs.yml

@@ -44,7 +44,7 @@ env:
   # codebase, but an admirable longterm goal is to support building the
   # current version of the compiler with a previous version that is older
   # than its immediate predecessor.
-  IDRIS2_MINIMUM_COMPAT_VERSION: 0.6.0
+  IDRIS2_MINIMUM_COMPAT_VERSION: 0.7.0
 
 jobs:
 
@@ -105,7 +105,7 @@ jobs:
       - name : Build previous version
         if: steps.previous-version-cache.outputs.cache-hit != 'true'
         run: |
-          wget "https://www.idris-lang.org/idris2-src/idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz"
+          wget "https://github.com/idris-lang/Idris2/archive/refs/tags/v$IDRIS2_MINIMUM_COMPAT_VERSION.tar.gz" -O "idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz"
           tar zxvf "idris2-$IDRIS2_MINIMUM_COMPAT_VERSION.tgz"
           cd "Idris2-$IDRIS2_MINIMUM_COMPAT_VERSION"
           make bootstrap

idris2api.ipkg

@@ -206,9 +206,6 @@ modules =
     Libraries.Data.Version,
     Libraries.Data.WithDefault,
 
-    Libraries.System.File,
-    Libraries.System.File.Buffer,
-    Libraries.System.File.Meta,
     Libraries.System.Directory.Tree,
 
     Libraries.Text.Bounded,
@@ -236,7 +233,6 @@ modules =
     Libraries.Utils.Scheme,
     Libraries.Utils.Shunting,
     Libraries.Utils.String,
-    Libraries.Utils.Term,
 
     Parser.Package,
     Parser.Source,

libs/base/Deriving/Common.idr

@@ -18,7 +18,7 @@ data IsFreeOf : (x : Name) -> (ty : TTImp) -> Type where
   TrustMeFO : IsFreeOf a x
 
 ||| We may need to manufacture proofs and so we provide the `assert` escape hatch.
-export -- %unsafe -- uncomment as soon as 0.7.0 is released
+export %unsafe
 assert_IsFreeOf : IsFreeOf x ty
 assert_IsFreeOf = TrustMeFO
 
@@ -165,7 +165,7 @@ data HasImplementation : (intf : a -> Type) -> TTImp -> Type where
   TrustMeHI : HasImplementation intf t
 
 ||| We may need to manufacture proofs and so we provide the `assert` escape hatch.
-export -- %unsafe -- uncomment as soon as 0.7.0 is released
+export %unsafe
 assert_hasImplementation : HasImplementation intf t
 assert_hasImplementation = TrustMeHI
 

libs/prelude/Builtin.idr

@@ -16,7 +16,7 @@ module Builtin
 ||| Note: assert_total can reduce at compile time, if required for unification,
 ||| which might mean that it's no longer guarded a subexpression. Therefore,
 ||| it is best to use it around the smallest possible subexpression.
-%inline -- %unsafe
+%inline %unsafe
 public export
 assert_total : (1 _ : a) -> a
 assert_total x = x
@@ -34,7 +34,7 @@ assert_total x = x
 |||
 ||| @ x the larger value (typically a pattern argument)
 ||| @ y the smaller value (typically an argument to a recursive call)
-%inline -- %unsafe
+%inline %unsafe
 public export
 assert_smaller : (0 x : a) -> (1 y : b) -> b
 assert_smaller x y = y
@@ -189,19 +189,19 @@ mkDPairInjectiveSnd Refl = Refl
 ||| Subvert the type checker.  This function is abstract, so it will not reduce
 ||| in the type checker.  Use it with care - it can result in segfaults or
 ||| worse!
-public export %inline -- %unsafe
+public export %inline %unsafe
 believe_me : a -> b -- TODO: make linear
 believe_me v = prim__believe_me _ _ v
 
 ||| Assert to the usage checker that the given function uses its argument linearly.
-public export -- %unsafe
+public export %unsafe
 assert_linear : (1 f : a -> b) -> (1 val : a) -> b
 assert_linear = believe_me id
   where
     id : (1 f : a -> b) -> a -> b
     id f = f
 
-export partial -- %unsafe
+export partial %unsafe
 idris_crash : String -> a
 idris_crash = prim__crash _
 

src/Core/Binary/Prims.idr

@@ -12,7 +12,6 @@ import Data.String
 import Data.Vect
 
 import Libraries.Data.PosMap
-import public Libraries.System.File.Meta as L -- Remove after release 0.7.0
 import public Libraries.Utils.Binary
 import public Libraries.Utils.String
 import Libraries.Data.WithDefault
@@ -458,11 +457,11 @@ TTC Nat where
 
 ||| Get a file's modified time. If it doesn't exist, return 0 (UNIX Epoch)
 export
-modTime : String -> Core L.Timestamp
+modTime : String -> Core Timestamp
 modTime fname
   = do Right f <- coreLift $ openFile fname Read
          | Left err => pure $ MkTimestamp 0 0 -- Beginning of Time :)
-       Right t <- coreLift $ L.fileTime f
+       Right t <- coreLift $ fileTime f
          | Left err => do coreLift $ closeFile f
                           pure $ MkTimestamp 0 0
        coreLift $ closeFile f

src/Core/CompileExpr/Pretty.idr

@@ -17,8 +17,6 @@ import Libraries.Data.String.Extra
 %hide Vect.catMaybes
 %hide Vect.(++)
 
-%hide HasLength.cast
-
 %hide SizeOf.map
 
 %hide Core.Name.prettyOp

src/Core/Name/Scoped.idr

@@ -2,7 +2,8 @@ module Core.Name.Scoped
 
 import Core.Name
 
-import public Libraries.Data.List.HasLength
+import public Data.List.HasLength
+
 import public Libraries.Data.List.SizeOf
 
 %default total

src/Idris/Driver.idr

@@ -31,7 +31,7 @@ import System.Directory
 import System.File.Meta
 import System.File.Virtual
 import Libraries.Utils.Path
-import Libraries.Utils.Term
+import System.Term
 
 import Yaffle.Main
 

src/Idris/Pretty/Render.idr

@@ -7,9 +7,9 @@ import Idris.REPL.Opts
 
 import Libraries.Text.PrettyPrint.Prettyprinter
 import public Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
-import Libraries.Utils.Term
 
 import System
+import System.Term
 
 %default total
 

src/Libraries/Data/List/HasLength.idr

@@ -2,47 +2,9 @@ module Libraries.Data.List.HasLength
 
 import Data.Nat
 
--- TODO: delete in favor of base lib's List.HasLength once next version 0.7.0 is released.
+import Data.List.HasLength
-public export
-data HasLength : Nat -> List a -> Type where
-  Z : HasLength Z []
-  S : HasLength n as -> HasLength (S n) (a :: as)
-
--- TODO: Use List.HasLength.sucR from the base lib instead once next version 0.7.0 is released.
-export
-sucR : HasLength n xs -> HasLength (S n) (xs ++ [x])
-sucR Z     = S Z
-sucR (S n) = S (sucR n)
-
--- TODO: Use List.HasLength.hasLengthAppend from the base lib instead once next version 0.7.0 is released.
-export
-hlAppend : HasLength m xs -> HasLength n ys -> HasLength (m + n) (xs ++ ys)
-hlAppend Z ys = ys
-hlAppend (S xs) ys = S (hlAppend xs ys)
-
--- TODO: Use List.HasLength.hasLength from the base lib instead once next version 0.7.0 is released.
-export
-mkHasLength : (xs : List a) -> HasLength (length xs) xs
-mkHasLength [] = Z
-mkHasLength (_ :: xs) = S (mkHasLength xs)
-
--- TODO: Use List.HasLength.take from the base lib instead once next vresion 0.7.0 is released.
-export
-take : (n : Nat) -> (xs : Stream a) -> HasLength n (take n xs)
-take Z _ = Z
-take (S n) (x :: xs) = S (take n xs)
 
 export
 cast : {ys : _} -> (0 _ : List.length xs = List.length ys) -> HasLength m xs -> HasLength m ys
 cast {ys = []}      eq Z = Z
 cast {ys = y :: ys} eq (S p) = S (cast (injective eq) p)
-
--- TODO: Delete once version 0.7.0 is released.
-hlReverseOnto : HasLength m acc -> HasLength n xs -> HasLength (m + n) (reverseOnto acc xs)
-hlReverseOnto p Z = rewrite plusZeroRightNeutral m in p
-hlReverseOnto {n = S n} p (S q) = rewrite sym (plusSuccRightSucc m n) in hlReverseOnto (S p) q
-
--- TODO: Use List.HasLength.hasLengthReverse from the base lib instead once next version 0.7.0 is released.
-export
-hlReverse : HasLength m acc -> HasLength m (reverse acc)
-hlReverse = hlReverseOnto Z

src/Libraries/Data/List/SizeOf.idr

@@ -1,6 +1,7 @@
 module Libraries.Data.List.SizeOf
 
 import Data.List
+import Data.List.HasLength
 import Libraries.Data.List.HasLength
 
 %default total
@@ -30,15 +31,15 @@ sucR (MkSizeOf n p) = MkSizeOf (S n) (sucR p)
 
 export
 (+) : SizeOf xs -> SizeOf ys -> SizeOf (xs ++ ys)
-MkSizeOf m p + MkSizeOf n q = MkSizeOf (m + n) (hlAppend p q)
+MkSizeOf m p + MkSizeOf n q = MkSizeOf (m + n) (hasLengthAppend p q)
 
 export
 mkSizeOf : (xs : List a) -> SizeOf xs
-mkSizeOf xs = MkSizeOf (length xs) (mkHasLength xs)
+mkSizeOf xs = MkSizeOf (length xs) (hasLength xs)
 
 export
 reverse : SizeOf xs -> SizeOf (reverse xs)
-reverse (MkSizeOf n p) = MkSizeOf n (hlReverse p)
+reverse (MkSizeOf n p) = MkSizeOf n (hasLengthReverse p)
 
 export
 map : SizeOf xs -> SizeOf (map f xs)

src/Libraries/Data/SnocList/HasLength.idr

@@ -4,7 +4,7 @@ import Data.Nat
 
 ---------------------------------------
 -- horrible hack
-import Libraries.Data.List.HasLength as L
+import Data.List.HasLength as L
 
 public export
 LHasLength : Nat -> List a -> Type

src/Libraries/Data/SnocList/SizeOf.idr

@@ -2,7 +2,7 @@ module Libraries.Data.SnocList.SizeOf
 
 import Data.List
 import Data.SnocList
-import Libraries.Data.List.HasLength
+import Data.List.HasLength
 import Libraries.Data.SnocList.HasLength
 
 ---------------------------------------

src/Libraries/System/Directory/Tree.idr

@@ -7,8 +7,6 @@ import Data.Nat
 import System.Directory
 import Libraries.Utils.Path
 
-import Libraries.System.File as LibFile
-
 %default total
 
 ------------------------------------------------------------------------------
@@ -203,7 +201,7 @@ copyDir src target = runEitherT $ do
   where
     copyFile' : (srcDir : Path) -> (targetDir : Path) -> (fileName : String) -> EitherT FileError io ()
     copyFile' srcDir targetDir fileName = MkEitherT $ do
-      Right ok <- LibFile.copyFile (show $ srcDir /> fileName) (show $ targetDir /> fileName)
+      Right ok <- copyFile (show $ srcDir /> fileName) (show $ targetDir /> fileName)
       | Left (err, size) => pure (Left err)
       pure (Right ok)
 

src/Libraries/System/File.idr

@@ -1,27 +0,0 @@
-module Libraries.System.File
-
-import Data.Buffer
-
-import public System.File.Error
-import public System.File.Handle
-import public System.File.Meta
-import public System.File.Mode
-import public System.File.Permissions
-import public System.File.Process
-import public System.File.ReadWrite
-import public System.File.Types
-import public System.File.Virtual
-
-import public Libraries.System.File.Buffer
-
-||| Copy the file at the specified source to the given destination.
-||| Returns the number of bytes that have been written upon a write error.
-|||
-||| @ src  the file to copy
-||| @ dest the place to copy the file to
-export
-copyFile : HasIO io => (src : String) -> (dest : String) -> io (Either (FileError, Int) ())
-copyFile src dest
-    = do Right buf <- createBufferFromFile src
-             | Left err => pure (Left (err, 0))
-         writeBufferToFile dest buf !(rawSize buf)

src/Libraries/System/File/Buffer.idr

@@ -1,101 +0,0 @@
-module Libraries.System.File.Buffer
-
-import public System.File.Error
-import System.File.Handle
-import System.File.Meta
-import System.File.Mode
-import System.File.ReadWrite
-import System.File.Support
-import public System.File.Types
-
-import Data.Buffer
-
-%default total
-
-support : String -> String
-support fn = "C:\{fn}, libidris2_support, idris_file.h"
--- ^ Only needed until version following 0.5.1 is released at which point
---   any code in compiler src can be refactored to use renamed @supportC@
---   function.
-
-%foreign Buffer.support "idris2_readBufferData"
-         "node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)"
-prim__readBufferData : FilePtr -> Buffer -> (offset : Int) -> (maxbytes : Int) -> PrimIO Int
-
-%foreign Buffer.support "idris2_writeBufferData"
-         "node:lambda:(f,b,l,m) => require('fs').writeSync(f.fd,b,l,m)"
-prim__writeBufferData : FilePtr -> Buffer -> (offset : Int) -> (size : Int) -> PrimIO Int
-
-||| Read the data from the file into the given buffer.
-|||
-||| @ fh       the file handle to read from
-||| @ buf      the buffer to read the data into
-||| @ offset   the position in buffer to start adding
-||| @ maxbytes the maximum size to read; must not exceed buffer length
-export
-readBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
-                 (offset : Int) ->
-                 (maxbytes : Int) ->
-                 io (Either FileError ())
-readBufferData (FHandle h) buf offset max
-    = do read <- primIO (prim__readBufferData h buf offset max)
-         if read >= 0
-            then pure (Right ())
-            else pure (Left FileReadError)
-
-||| Write the data from the buffer to the given `File`. Returns the number
-||| of bytes that have been written upon a write error. Otherwise, it can
-||| be assumed that `size` number of bytes have been written.
-||| (If you do not have a `File` and just want to write to a file at a known
-||| path, you probably want to use `writeBufferToFile`.)
-|||
-||| @ fh       the file handle to write to
-||| @ buf      the buffer from which to get the data to write
-||| @ offset   the position in buffer to write from
-||| @ size     the number of bytes to write; must not exceed buffer length
-export
-writeBufferData : HasIO io => (fh : File) -> (buf : Buffer) ->
-                  (offset : Int) ->
-                  (size : Int) ->
-                  io (Either (FileError, Int) ())
-writeBufferData (FHandle h) buf offset size
-    = do written <- primIO (prim__writeBufferData h buf offset size)
-         if written == size
-            then pure (Right ())
-            else pure (Left (FileWriteError, written))
-
-||| Attempt to write the data from the buffer to the file at the specified file
-||| name. Returns the number of bytes that have been written upon a write error.
-||| Otherwise, it can be assumed that `size` number of bytes have been written.
-|||
-||| @ fn   the file name to write to
-||| @ buf  the buffer from which to get the data to write
-||| @ size the number of bytes to write; must not exceed buffer length
-export
-writeBufferToFile : HasIO io => (fn : String) -> (buf : Buffer) -> (size : Int) ->
-                                io (Either (FileError, Int) ())
-writeBufferToFile fn buf size
-    = do Right f <- openFile fn WriteTruncate
-             | Left err => pure (Left (err, 0))
-         Right ok <- writeBufferData f buf 0 size
-             | Left err => pure (Left err)
-         closeFile f
-         pure (Right ok)
-
-||| Create a new buffer by opening a file and reading its contents into a new
-||| buffer whose size matches the file size.
-|||
-||| @ fn the name of the file to read
-export
-createBufferFromFile : HasIO io => (fn : String) -> io (Either FileError Buffer)
-createBufferFromFile fn
-    = do Right f <- openFile fn Read
-             | Left err => pure (Left err)
-         Right size <- fileSize f
-             | Left err => pure (Left err)
-         Just buf <- newBuffer size
-             | Nothing => pure (Left FileReadError)
-         Right ok <- readBufferData f buf 0 size
-             | Left err => pure (Left err)
-         closeFile f
-         pure (Right buf)

src/Libraries/System/File/Meta.idr

@@ -1,110 +0,0 @@
-module Libraries.System.File.Meta
-
-import Data.String
-
-import System.FFI
-
-import System.File.Handle
-import System.File.Support
-import public System.File.Types
-
-%default total
-
-||| Pointer to a structure holding File's time attributes
-FileTimePtr : Type
-FileTimePtr = AnyPtr
-
-%foreign supportC "idris2_fileTime"
-         "node:support:filetime,support_system_file"
-prim__fileTime : FilePtr -> PrimIO FileTimePtr
-
-%foreign supportC "idris2_filetimeAccessTimeSec"
-         "node:lambda:ft=>ft.atime_sec"
-prim__filetimeAccessTimeSec : FileTimePtr -> PrimIO Int
-
-%foreign supportC "idris2_filetimeAccessTimeNsec"
-         "node:lambda:ft=>ft.atime_nsec"
-prim__filetimeAccessTimeNsec : FileTimePtr -> PrimIO Int
-
-%foreign supportC "idris2_filetimeModifiedTimeSec"
-         "node:lambda:ft=>ft.mtime_sec"
-prim__filetimeModifiedTimeSec : FileTimePtr -> PrimIO Int
-
-%foreign supportC "idris2_filetimeModifiedTimeNsec"
-         "node:lambda:ft=>ft.mtime_nsec"
-prim__filetimeModifiedTimeNsec : FileTimePtr -> PrimIO Int
-
-%foreign supportC "idris2_filetimeStatusTimeSec"
-         "node:lambda:ft=>ft.ctime_sec"
-prim__filetimeStatusTimeSec : FileTimePtr -> PrimIO Int
-
-%foreign supportC "idris2_filetimeStatusTimeNsec"
-         "node:lambda:ft=>ft.ctime_nsec"
-prim__filetimeStatusTimeNsec : FileTimePtr -> PrimIO Int
-
-||| Record that holds timestamps with nanosecond precision
-public export
-record Timestamp where
-  constructor MkTimestamp
-  sec  : Int
-  nsec : Int
-
-export
-Eq Timestamp where
-  t == t' = (t.sec == t'.sec) && (t.nsec == t'.nsec)
-
-export
-Ord Timestamp where
-  t < t' = (t.sec < t'.sec) || (t.sec == t'.sec && t.nsec < t'.nsec)
-
-export
-Show Timestamp where
-  show t = "\{show t.sec}.\{padLeft 9 '0' $ show t.nsec}"
-
-||| Record that holds file's time attributes
-public export
-record FileTime where
-  constructor MkFileTime
-  atime : Timestamp
-  mtime : Timestamp
-  ctime : Timestamp
-
-||| Get File's time attributes
-export
-fileTime : HasIO io => (h : File) -> io (Either FileError FileTime)
-fileTime (FHandle f)
-    = do res <- primIO (prim__fileTime f)
-         ft <- parseFileTime res
-         free res
-         if ft.atime.sec > 0
-            then ok ft
-            else returnError
-    where
-      parseFileTime : FileTimePtr -> io FileTime
-      parseFileTime ft = pure $ MkFileTime { atime = MkTimestamp { sec  = !(primIO (prim__filetimeAccessTimeSec ft))
-                                                                 , nsec = !(primIO (prim__filetimeAccessTimeNsec ft))
-                                                                 }
-                                           , mtime = MkTimestamp { sec  = !(primIO (prim__filetimeModifiedTimeSec ft))
-                                                                 , nsec = !(primIO (prim__filetimeModifiedTimeNsec ft))
-                                                                 }
-                                           , ctime = MkTimestamp { sec  = !(primIO (prim__filetimeStatusTimeSec ft))
-                                                                 , nsec = !(primIO (prim__filetimeStatusTimeNsec ft))
-                                                                 }
-                                           }
-
-||| Get the File's atime.
-export
-fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int)
-fileAccessTime h = (fileTime h <&> (.atime.sec)) @{Compose}
-
-||| Get the File's mtime.
-export
-fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int)
-fileModifiedTime h = (fileTime h <&> (.mtime.sec)) @{Compose}
-
-||| Get the File's ctime.
-export
-fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int)
-fileStatusTime h = (fileTime h <&> (.ctime.sec)) @{Compose}
-
-

src/Libraries/Utils/Binary.idr

@@ -3,7 +3,7 @@ module Libraries.Utils.Binary
 import Data.Buffer
 import Data.List
 
-import Libraries.System.File
+import System.File
 
 -- Serialising data as binary. Provides an interface TTC which allows
 -- reading and writing to chunks of memory, "Binary", which can be written

src/Libraries/Utils/Term.idr

@@ -1,29 +0,0 @@
-module Libraries.Utils.Term
-
-%default total
-
--- TODO: remove this file and use System.Term after 0.7.0 is released
-
-libterm : String -> String
-libterm s = "C:" ++ s ++ ", libidris2_support, idris_term.h"
-
-%foreign libterm "idris2_setupTerm"
-prim__setupTerm : PrimIO ()
-
-%foreign libterm "idris2_getTermCols"
-prim__getTermCols : PrimIO Int
-
-%foreign libterm "idris2_getTermLines"
-prim__getTermLines : PrimIO Int
-
-export
-setupTerm : IO ()
-setupTerm = primIO prim__setupTerm
-
-export
-getTermCols : IO Int
-getTermCols = primIO prim__getTermCols
-
-export
-getTermLines : IO Int
-getTermLines = primIO prim__getTermLines