[ 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.
-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)
+import Data.List.HasLength
 
 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)