From 82bb12cf7283f6d0db9ee847440bbdc4f0e3d686 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Sun, 24 Dec 2023 19:59:13 +0300 Subject: [PATCH] [ cleanup ] Post v0.7.0 cleanup --- .github/workflows/ci-idris2-and-libs.yml | 4 +- idris2api.ipkg | 4 - libs/base/Deriving/Common.idr | 4 +- libs/prelude/Builtin.idr | 10 +- src/Core/Binary/Prims.idr | 5 +- src/Core/CompileExpr/Pretty.idr | 2 - src/Core/Name/Scoped.idr | 3 +- src/Idris/Driver.idr | 2 +- src/Idris/Pretty/Render.idr | 2 +- src/Libraries/Data/List/HasLength.idr | 40 +------- src/Libraries/Data/List/SizeOf.idr | 7 +- src/Libraries/Data/SnocList/HasLength.idr | 2 +- src/Libraries/Data/SnocList/SizeOf.idr | 2 +- src/Libraries/System/Directory/Tree.idr | 4 +- src/Libraries/System/File.idr | 27 ------ src/Libraries/System/File/Buffer.idr | 101 -------------------- src/Libraries/System/File/Meta.idr | 110 ---------------------- src/Libraries/Utils/Binary.idr | 2 +- src/Libraries/Utils/Term.idr | 29 ------ 19 files changed, 24 insertions(+), 336 deletions(-) delete mode 100644 src/Libraries/System/File.idr delete mode 100644 src/Libraries/System/File/Buffer.idr delete mode 100644 src/Libraries/System/File/Meta.idr delete mode 100644 src/Libraries/Utils/Term.idr diff --git a/.github/workflows/ci-idris2-and-libs.yml b/.github/workflows/ci-idris2-and-libs.yml index 0d8690b711..f084c7fe7c 100644 --- a/.github/workflows/ci-idris2-and-libs.yml +++ b/.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 diff --git a/idris2api.ipkg b/idris2api.ipkg index e49dd712c1..f924514f51 100644 --- a/idris2api.ipkg +++ b/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, diff --git a/libs/base/Deriving/Common.idr b/libs/base/Deriving/Common.idr index c18834b85b..eeebec0dee 100644 --- a/libs/base/Deriving/Common.idr +++ b/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 diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr index 8076d2c55f..1a839238d7 100644 --- a/libs/prelude/Builtin.idr +++ b/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 _ diff --git a/src/Core/Binary/Prims.idr b/src/Core/Binary/Prims.idr index 6a5d18448f..ddd0fccbd2 100644 --- a/src/Core/Binary/Prims.idr +++ b/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 diff --git a/src/Core/CompileExpr/Pretty.idr b/src/Core/CompileExpr/Pretty.idr index 57e89af7b3..ba7ae1fc73 100644 --- a/src/Core/CompileExpr/Pretty.idr +++ b/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 diff --git a/src/Core/Name/Scoped.idr b/src/Core/Name/Scoped.idr index 89186a941c..8d66b57fce 100644 --- a/src/Core/Name/Scoped.idr +++ b/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 diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 8ae8573eb0..8988120176 100644 --- a/src/Idris/Driver.idr +++ b/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 diff --git a/src/Idris/Pretty/Render.idr b/src/Idris/Pretty/Render.idr index c48db45276..d910246f7a 100644 --- a/src/Idris/Pretty/Render.idr +++ b/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 diff --git a/src/Libraries/Data/List/HasLength.idr b/src/Libraries/Data/List/HasLength.idr index 1512a9cb01..394b870a9c 100644 --- a/src/Libraries/Data/List/HasLength.idr +++ b/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 diff --git a/src/Libraries/Data/List/SizeOf.idr b/src/Libraries/Data/List/SizeOf.idr index 7b5978aa94..f177a294b3 100644 --- a/src/Libraries/Data/List/SizeOf.idr +++ b/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) diff --git a/src/Libraries/Data/SnocList/HasLength.idr b/src/Libraries/Data/SnocList/HasLength.idr index 142d551993..eda9f7a5e0 100644 --- a/src/Libraries/Data/SnocList/HasLength.idr +++ b/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 diff --git a/src/Libraries/Data/SnocList/SizeOf.idr b/src/Libraries/Data/SnocList/SizeOf.idr index 68817c4086..5caf966098 100644 --- a/src/Libraries/Data/SnocList/SizeOf.idr +++ b/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 --------------------------------------- diff --git a/src/Libraries/System/Directory/Tree.idr b/src/Libraries/System/Directory/Tree.idr index b808139d65..6804b0b655 100644 --- a/src/Libraries/System/Directory/Tree.idr +++ b/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) diff --git a/src/Libraries/System/File.idr b/src/Libraries/System/File.idr deleted file mode 100644 index b493bf9dc3..0000000000 --- a/src/Libraries/System/File.idr +++ /dev/null @@ -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) diff --git a/src/Libraries/System/File/Buffer.idr b/src/Libraries/System/File/Buffer.idr deleted file mode 100644 index 381dba5445..0000000000 --- a/src/Libraries/System/File/Buffer.idr +++ /dev/null @@ -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) diff --git a/src/Libraries/System/File/Meta.idr b/src/Libraries/System/File/Meta.idr deleted file mode 100644 index a1fe07cdc3..0000000000 --- a/src/Libraries/System/File/Meta.idr +++ /dev/null @@ -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} - - diff --git a/src/Libraries/Utils/Binary.idr b/src/Libraries/Utils/Binary.idr index 34303d5dc2..9bbe51d4ef 100644 --- a/src/Libraries/Utils/Binary.idr +++ b/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 diff --git a/src/Libraries/Utils/Term.idr b/src/Libraries/Utils/Term.idr deleted file mode 100644 index bb479eb1c8..0000000000 --- a/src/Libraries/Utils/Term.idr +++ /dev/null @@ -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