Merge branch 'main' into incompatible-visibilities

.gitignore

@@ -15,6 +15,7 @@ idris2docs_venv
 /docs/build
 
 /libs/**/build
+/ipkg/build
 
 /tests/**/build
 /tests/**/output*

CHANGELOG.md

@@ -110,6 +110,11 @@
 
 * Fixed a bug that caused `f` to sometimes be replaced by `fx` after matching `fx = f x`.
 
+* Refactor the idris2protocols package to depend on fewer Idris2 modules.
+  We can now export the package independently.
+  To avoid confusing tooling about which `.ipkg` to use, the
+  package file is under the newly added `ipkg` sub-directory.
+
 * Added `Libraries.Data.WithDefault` to facilitate consistent use
   of a default-if-unspecified value, currently for `private` visibility.
 

Makefile

@@ -59,12 +59,13 @@ export SCHEME
 
 .PHONY: all idris2-exec libdocs testenv testenv-clean support clean-support clean FORCE
 
-all: support ${TARGET} libs
+all: ${TARGET} libs
 
 idris2-exec: ${TARGET}
 
-${TARGET}: src/IdrisPaths.idr
+${TARGET}: support src/IdrisPaths.idr
 	${IDRIS2_BOOT} --build ${IDRIS2_APP_IPKG}
+	cp ${IDRIS2_CURDIR}/support/c/${IDRIS2_SUPPORT} ${TARGETDIR}/${NAME}_app/${IDRIS2_SUPPORT}
 
 # We use FORCE to always rebuild IdrisPath so that the git SHA1 info is always up to date
 src/IdrisPaths.idr: FORCE

idris2api.ipkg

@@ -193,6 +193,7 @@ modules =
 
     Libraries.System.File,
     Libraries.System.File.Buffer,
+    Libraries.System.File.Meta,
     Libraries.System.Directory.Tree,
 
     Libraries.Text.Bounded,
@@ -225,6 +226,7 @@ modules =
     Parser.Package,
     Parser.Source,
     Parser.Support,
+    Parser.Support.Escaping,
     Parser.Unlit,
 
     Parser.Lexer.Common,

idris2protocols.ipkg.hide → ipkg/idris2protocols.ipkg

@@ -3,33 +3,37 @@ version = 0.0.1
 
 modules
   = Protocol.Hex
-  -- , Protocol.IDE
+  , Protocol.IDE
   , Protocol.IDE.Command
   , Protocol.IDE.Decoration
   , Protocol.SExp
-  -- TODO: want to add this module, but the parser library introduces
-  -- dependencies on core idris
-  -- , Protocol.SExp.Parser
-  , Libraries.Data.Span
-  , Libraries.Text.Lexer
   , Libraries.Control.Delayed
   , Libraries.Text.Bounded
   , Libraries.Text.Lexer.Core
   , Libraries.Text.Quantity
   , Libraries.Text.Token
-  , Libraries.Text.Lexer.Tokenizer
+  , Libraries.Text.Lexer
+  , Parser.Lexer.Common
+  , Libraries.Data.Span
   , Libraries.Data.String.Extra
   , Libraries.Text.PrettyPrint.Prettyprinter.Doc
   , Libraries.Text.PrettyPrint.Prettyprinter.Symbols
+  , Libraries.Text.PrettyPrint.Prettyprinter.Util
+  , Libraries.Text.PrettyPrint.Prettyprinter.Render.String
   , Libraries.Text.PrettyPrint.Prettyprinter
+  , Libraries.Text.Lexer.Tokenizer
   , Libraries.Text.Parser.Core
   , Libraries.Text.Parser
-  , Parser.Rule.Source
-  -- , Protocol.IDE.FileContext
-  -- , Protocol.IDE.Formatting
-  -- , Protocol.IDE.Holes
-  -- , Protocol.IDE.Result
-  -- , Protocol.IDE.Highlight
+  , Parser.Support.Escaping
+  , Protocol.SExp.Parser
+  , Protocol.IDE.Decoration
+  , Protocol.IDE.Command
+  , Protocol.Hex
+  , Protocol.IDE.FileContext
+  , Protocol.IDE.Formatting
+  , Protocol.IDE.Holes
+  , Protocol.IDE.Result
+  , Protocol.IDE.Highlight
 
 --depends =
 

libs/base/System/File/Meta.idr

@@ -1,28 +1,54 @@
 ||| Functions for accessing file metadata.
 module 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_fileSize"
          "node:lambda:fp=>require('fs').fstatSync(fp.fd).size"
 prim__fileSize : FilePtr -> PrimIO Int
 
 %foreign supportC "idris2_fileSize"
 prim__fPoll : FilePtr -> PrimIO Int
 
-%foreign supportC "idris2_fileAccessTime"
-prim__fileAccessTime : FilePtr -> PrimIO Int
+%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_fileModifiedTime"
-         "node:lambda:fp=>require('fs').fstatSync(fp.fd).mtimeMs / 1000"
-prim__fileModifiedTime : FilePtr -> PrimIO Int
+%foreign supportC "idris2_filetimeModifiedTimeNsec"
+         "node:lambda:ft=>ft.mtime_nsec"
+prim__filetimeModifiedTimeNsec : FileTimePtr -> PrimIO Int
 
-%foreign supportC "idris2_fileStatusTime"
-prim__fileStatusTime : FilePtr -> 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
 
 %foreign supportC "idris2_fileIsTTY"
          "node:lambda:fp=>Number(require('tty').isatty(fp.fd))"
@@ -43,32 +69,70 @@ firstExists : HasIO io => List String -> io (Maybe String)
 firstExists [] = pure Nothing
 firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs
 
+||| 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 (FHandle f)
-    = do res <- primIO (prim__fileAccessTime f)
-         if res > 0
-            then ok res
-            else returnError
+fileAccessTime h = (fileTime h <&> (.atime.sec)) @{Compose}
 
 ||| Get the File's mtime.
 export
 fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int)
-fileModifiedTime (FHandle f)
-    = do res <- primIO (prim__fileModifiedTime f)
-         if res > 0
-            then ok res
-            else returnError
+fileModifiedTime h = (fileTime h <&> (.mtime.sec)) @{Compose}
 
 ||| Get the File's ctime.
 export
 fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int)
-fileStatusTime (FHandle f)
-    = do res <- primIO (prim__fileStatusTime f)
-         if res > 0
-            then ok res
-            else returnError
+fileStatusTime h = (fileTime h <&> (.ctime.sec)) @{Compose}
 
 ||| Get the File's size.
 export

src/Core/Binary/Prims.idr

@@ -12,6 +12,7 @@ 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 public Libraries.Data.WithDefault
@@ -457,15 +458,15 @@ TTC Nat where
 
 ||| Get a file's modified time. If it doesn't exist, return 0 (UNIX Epoch)
 export
-modTime : String -> Core Int
+modTime : String -> Core L.Timestamp
 modTime fname
   = do Right f <- coreLift $ openFile fname Read
-         | Left err => pure 0 -- Beginning of Time :)
-       Right t <- coreLift $ fileModifiedTime f
+         | Left err => pure $ MkTimestamp 0 0 -- Beginning of Time :)
+       Right t <- coreLift $ L.fileTime f
          | Left err => do coreLift $ closeFile f
-                          pure 0
+                          pure $ MkTimestamp 0 0
        coreLift $ closeFile f
-       pure t
+       pure $ t.mtime
 
 export
 hashFileWith : Maybe String -> String -> Core (Maybe String)

src/Libraries/System/File/Meta.idr

@@ -0,0 +1,110 @@
+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}
+
+