mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-08-17 03:40:33 +03:00
Fix building the latest self-hosted Idris 2
* Add System.Path to the 'contrib' package * Update Data.List in the 'base' package
This commit is contained in:
parent
fa92951af0
commit
27006bc516
@ -29,6 +29,15 @@ drop Z xs = xs
|
||||
drop (S n) [] = []
|
||||
drop (S n) (x::xs) = drop n xs
|
||||
|
||||
||| Generate a list by repeatedly applying a partial function until exhausted.
|
||||
||| @ f the function to iterate
|
||||
||| @ x the initial value that will be the head of the list
|
||||
public export
|
||||
iterate : (f : a -> Maybe a) -> (x : a) -> List a
|
||||
iterate f x = x :: case f x of
|
||||
Nothing => []
|
||||
Just y => iterate f y
|
||||
|
||||
public export
|
||||
takeWhile : (p : a -> Bool) -> List a -> List a
|
||||
takeWhile p [] = []
|
||||
@ -296,6 +305,22 @@ tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
|
||||
tail [] impossible
|
||||
tail (x :: xs) = xs
|
||||
|
||||
||| Retrieve the last element of a non-empty list.
|
||||
||| @ ok proof that the list is non-empty
|
||||
public export
|
||||
last : (l : List a) -> {auto ok : NonEmpty l} -> a
|
||||
last [] impossible
|
||||
last [x] = x
|
||||
last (x::y::ys) = last (y::ys)
|
||||
|
||||
||| Return all but the last element of a non-empty list.
|
||||
||| @ ok proof the list is non-empty
|
||||
public export
|
||||
init : (l : List a) -> {auto ok : NonEmpty l} -> List a
|
||||
init [] impossible
|
||||
init [x] = []
|
||||
init (x::y::ys) = x :: init (y::ys)
|
||||
|
||||
||| Attempt to get the head of a list. If the list is empty, return `Nothing`.
|
||||
export
|
||||
head' : List a -> Maybe a
|
||||
@ -308,6 +333,22 @@ tail' : List a -> Maybe (List a)
|
||||
tail' [] = Nothing
|
||||
tail' (x::xs) = Just xs
|
||||
|
||||
||| Attempt to retrieve the last element of a non-empty list.
|
||||
|||
|
||||
||| If the list is empty, return `Nothing`.
|
||||
export
|
||||
last' : List a -> Maybe a
|
||||
last' [] = Nothing
|
||||
last' xs@(_::_) = Just (last xs)
|
||||
|
||||
||| Attempt to return all but the last element of a non-empty list.
|
||||
|||
|
||||
||| If the list is empty, return `Nothing`.
|
||||
export
|
||||
init' : List a -> Maybe (List a)
|
||||
init' [] = Nothing
|
||||
init' xs@(_::_) = Just (init xs)
|
||||
|
||||
||| Convert any Foldable structure to a list.
|
||||
export
|
||||
toList : Foldable t => t a -> List a
|
||||
@ -359,6 +400,37 @@ mapMaybe f (x::xs) =
|
||||
Nothing => mapMaybe f xs
|
||||
Just j => j :: mapMaybe f xs
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Special folds
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
||| Foldl a non-empty list without seeding the accumulator.
|
||||
||| @ ok proof that the list is non-empty
|
||||
public export
|
||||
foldl1 : (a -> a -> a) -> (l : List a) -> {auto ok : NonEmpty l} -> a
|
||||
foldl1 f [] impossible
|
||||
foldl1 f (x::xs) = foldl f x xs
|
||||
|
||||
||| Foldr a non-empty list without seeding the accumulator.
|
||||
||| @ ok proof that the list is non-empty
|
||||
public export
|
||||
foldr1 : (a -> a -> a) -> (l : List a) -> {auto ok : NonEmpty l} -> a
|
||||
foldr1 f [] impossible
|
||||
foldr1 f [x] = x
|
||||
foldr1 f (x::y::ys) = f x (foldr1 f (y::ys))
|
||||
|
||||
||| Foldl without seeding the accumulator. If the list is empty, return `Nothing`.
|
||||
public export
|
||||
foldl1' : (a -> a -> a) -> List a -> Maybe a
|
||||
foldl1' f [] = Nothing
|
||||
foldl1' f xs@(_::_) = Just (foldl1 f xs)
|
||||
|
||||
||| Foldr without seeding the accumulator. If the list is empty, return `Nothing`.
|
||||
public export
|
||||
foldr1' : (a -> a -> a) -> List a -> Maybe a
|
||||
foldr1' f [] = Nothing
|
||||
foldr1' f xs@(_::_) = Just (foldr1 f xs)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Sorting
|
||||
--------------------------------------------------------------------------------
|
||||
|
438
libs/contrib/System/Path.idr
Normal file
438
libs/contrib/System/Path.idr
Normal file
@ -0,0 +1,438 @@
|
||||
module System.Path
|
||||
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import Data.Strings
|
||||
import Data.String.Extra
|
||||
import System.Info
|
||||
import Text.Token
|
||||
import Text.Lexer
|
||||
import Text.Parser
|
||||
import Text.Quantity
|
||||
|
||||
private
|
||||
isWindows : Bool
|
||||
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]
|
||||
|
||||
||| The character that separates directories in the path.
|
||||
export
|
||||
dirSeparator : Char
|
||||
dirSeparator = if isWindows then '\\' else '/'
|
||||
|
||||
||| The character that separates multiple paths.
|
||||
export
|
||||
pathSeparator : Char
|
||||
pathSeparator = if isWindows then ';' else ':'
|
||||
|
||||
||| Windows' path prefixes.
|
||||
|||
|
||||
||| @ UNC Windows' Uniform Naming Convention, e.g., a network sharing
|
||||
||| directory: `\\host\c$\Windows\System32`
|
||||
||| @ Disk the drive, e.g., "C:". The disk character is in upper case
|
||||
public export
|
||||
data Volumn = UNC String String
|
||||
| Disk Char
|
||||
|
||||
||| A single body of path.
|
||||
|||
|
||||
||| @ CurDir "."
|
||||
||| @ ParentDir ".."
|
||||
||| @ Normal common directory or file
|
||||
public export
|
||||
data Body = CurDir
|
||||
| ParentDir
|
||||
| Normal String
|
||||
|
||||
||| A cross-platform file system path.
|
||||
|||
|
||||
||| The function `parse` is the most common way to construct a Path
|
||||
||| from String, and the function `show` converts in reverse.
|
||||
|||
|
||||
||| Trailing separator is only used for display and is ignored while
|
||||
||| comparing paths.
|
||||
|||
|
||||
||| @ volumn Windows' path prefix (only on Windows)
|
||||
||| @ hasRoot whether the path contains a root
|
||||
||| @ body path bodies
|
||||
||| @ hasTrailSep whether the path terminates with a separator
|
||||
public export
|
||||
record Path where
|
||||
constructor MkPath
|
||||
volumn : Maybe Volumn
|
||||
hasRoot : Bool
|
||||
body : List Body
|
||||
hasTrailSep : Bool
|
||||
|
||||
export
|
||||
Eq Volumn where
|
||||
(==) (UNC l1 l2) (UNC r1 r2) = l1 == r1 && r1 == r2
|
||||
(==) (Disk l) (Disk r) = l == r
|
||||
(==) _ _ = False
|
||||
|
||||
export
|
||||
Eq Body where
|
||||
(==) CurDir CurDir = True
|
||||
(==) ParentDir ParentDir = True
|
||||
(==) (Normal l) (Normal r) = l == r
|
||||
(==) _ _ = False
|
||||
|
||||
export
|
||||
Eq Path where
|
||||
(==) (MkPath l1 l2 l3 _) (MkPath r1 r2 r3 _) = l1 == r1
|
||||
&& l2 == r2
|
||||
&& l3 == r3
|
||||
|
||||
||| An empty path that represents "".
|
||||
public export
|
||||
emptyPath : Path
|
||||
emptyPath = MkPath Nothing False [] False
|
||||
|
||||
||| Returns true if the path is absolute.
|
||||
|||
|
||||
||| - On Unix, a path is absolute if it starts with the root,
|
||||
||| so isAbsolute and hasRoot are equivalent.
|
||||
|||
|
||||
||| - On Windows, a path is absolute if it has a volumn and starts
|
||||
||| with the root. e.g., `c:\\windows` is absolute, while `c:temp`
|
||||
||| and `\temp` are not. In addition, a path with UNC volumn is absolute.
|
||||
export
|
||||
isAbsolute : Path -> Bool
|
||||
isAbsolute p = if isWindows
|
||||
then case p.volumn of
|
||||
Just (UNC _ _) => True
|
||||
Just (Disk _) => p.hasRoot
|
||||
Nothing => False
|
||||
else p.hasRoot
|
||||
|
||||
||| Returns true if the path is relative, i.e., not absolute.
|
||||
export
|
||||
isRelative : Path -> Bool
|
||||
isRelative = not . isAbsolute
|
||||
|
||||
||| Appends the right path to the left one.
|
||||
|||
|
||||
||| If the path on the right is absolute, it replaces the left path.
|
||||
|||
|
||||
||| On Windows:
|
||||
|||
|
||||
||| - If the right path has a root but no volumn (e.g., `\windows`), it
|
||||
||| replaces everything except for the volumn (if any) of left.
|
||||
||| - If the right path has a volumn but no root, it replaces left.
|
||||
|||
|
||||
||| ```idris example
|
||||
||| pure $ !(parse "/usr") `append` !(parse "local/etc")
|
||||
||| ```
|
||||
export
|
||||
append : (left : Path) -> (right : Path) -> Path
|
||||
append l r = if isAbsolute r || isJust r.volumn
|
||||
then r
|
||||
else if hasRoot r
|
||||
then record { volumn = l.volumn } r
|
||||
else record { body = l.body ++ r.body,
|
||||
hasTrailSep = r.hasTrailSep } l
|
||||
|
||||
||| Returns the path without its final component, if there is one.
|
||||
|||
|
||||
||| Returns Nothing if the path terminates in a root or volumn.
|
||||
export
|
||||
parent : Path -> Maybe Path
|
||||
parent p = case p.body of
|
||||
[] => Nothing
|
||||
(x::xs) => Just $ record { body = init (x::xs),
|
||||
hasTrailSep = False } p
|
||||
|
||||
||| Returns a list of all parents of the path, longest first,
|
||||
||| self excluded.
|
||||
|||
|
||||
||| For example, the parent of the path, and the parent of the
|
||||
||| parent of the path, and so on. The list terminates in a
|
||||
||| root or volumn (if any).
|
||||
export
|
||||
parents : Path -> List Path
|
||||
parents p = drop 1 $ iterate parent p
|
||||
|
||||
||| Determines whether base is either one of the parents of full or
|
||||
||| is identical to full.
|
||||
|||
|
||||
||| Trailing separator is ignored.
|
||||
export
|
||||
startWith : (base : Path) -> (full : Path) -> Bool
|
||||
startWith base full = base `elem` (iterate parent full)
|
||||
|
||||
||| Returns a path that, when appended onto base, yields full.
|
||||
|||
|
||||
||| If base is not a prefix of full (i.e., startWith returns false),
|
||||
||| returns Nothing.
|
||||
stripPrefix : (base : Path) -> (full : Path) -> Maybe Path
|
||||
stripPrefix base full
|
||||
= do let MkPath vol1 root1 body1 _ = base
|
||||
let MkPath vol2 root2 body2 trialSep = full
|
||||
if vol1 == vol2 && root1 == root2 then Just () else Nothing
|
||||
body <- stripBody body1 body2
|
||||
pure $ MkPath Nothing False body trialSep
|
||||
where
|
||||
stripBody : (base : List Body) -> (full : List Body) -> Maybe (List Body)
|
||||
stripBody [] ys = Just ys
|
||||
stripBody xs [] = Nothing
|
||||
stripBody (x::xs) (y::ys) = if x == y then stripBody xs ys else Nothing
|
||||
|
||||
||| Returns the final body of the path, if there is one.
|
||||
|||
|
||||
||| If the path is a normal file, this is the file name. If it's the
|
||||
||| path of a directory, this is the directory name.
|
||||
|||
|
||||
||| Returns Nothing if the final body is ".." or "."
|
||||
export
|
||||
fileName : Path -> Maybe String
|
||||
fileName p = case last' p.body of
|
||||
Just (Normal s) => Just s
|
||||
_ => Nothing
|
||||
|
||||
private
|
||||
splitFileName : String -> (String, String)
|
||||
splitFileName name
|
||||
= case break (== '.') $ reverse $ unpack name of
|
||||
(_, []) => (name, "")
|
||||
(_, ['.']) => (name, "")
|
||||
(revExt, (dot :: revStem))
|
||||
=> ((pack $ reverse revStem), (pack $ reverse revExt))
|
||||
|
||||
|
||||
||| Extracts the stem (non-extension) portion of the file name of path.
|
||||
|||
|
||||
||| The stem is:
|
||||
|||
|
||||
||| - Nothing, if there is no file name;
|
||||
||| - The entire file name if there is no embedded ".";
|
||||
||| - The entire file name if the file name begins with "." and has
|
||||
||| no other "."s within;
|
||||
||| - Otherwise, the portion of the file name before the final "."
|
||||
export
|
||||
fileStem : Path -> Maybe String
|
||||
fileStem p = pure $ fst $ splitFileName !(fileName p)
|
||||
|
||||
||| Extracts the extension of the file name of path.
|
||||
|||
|
||||
||| The extension is:
|
||||
|||
|
||||
||| - Nothing, if there is no file name;
|
||||
||| - Nothing, if there is no embedded ".";
|
||||
||| - Nothing, if the file name begins with "." and has no other "."s within;
|
||||
||| - Otherwise, the portion of the file name after the final "."
|
||||
export
|
||||
extension : Path -> Maybe String
|
||||
extension p = pure $ snd $ splitFileName !(fileName p)
|
||||
|
||||
||| Updates the file name of the path.
|
||||
|||
|
||||
||| If no file name, this is equivalent to appending the name;
|
||||
||| Otherwise it is equivalent to appending the name to the parent.
|
||||
export
|
||||
setFileName : (name : String) -> Path -> Path
|
||||
setFileName name p = record { body $= updateLastBody name } p
|
||||
where
|
||||
updateLastBody : String -> List Body -> List Body
|
||||
updateLastBody s [] = [Normal s]
|
||||
updateLastBody s [Normal _] = [Normal s]
|
||||
updateLastBody s [x] = x :: [Normal s]
|
||||
updateLastBody s (x::xs) = x :: (updateLastBody s xs)
|
||||
|
||||
||| Updates the extension of the path.
|
||||
|||
|
||||
||| Returns Nothing if no file name.
|
||||
|||
|
||||
||| If extension is Nothing, the extension is added; otherwise it is replaced.
|
||||
export
|
||||
setExtension : (ext : String) -> Path -> Maybe Path
|
||||
setExtension ext p = do name <- fileName p
|
||||
let (stem, _) = splitFileName name
|
||||
pure $ setFileName (stem ++ "." ++ ext) p
|
||||
|
||||
public export
|
||||
Semigroup Path where
|
||||
(<+>) = append
|
||||
|
||||
public export
|
||||
Monoid Path where
|
||||
neutral = emptyPath
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Show
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
export
|
||||
Show Body where
|
||||
show CurDir = "."
|
||||
show ParentDir = ".."
|
||||
show (Normal s) = s
|
||||
|
||||
export
|
||||
Show Volumn where
|
||||
show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
|
||||
show (Disk disk) = singleton disk ++ ":"
|
||||
|
||||
||| Display the path in the format on the platform.
|
||||
export
|
||||
Show Path where
|
||||
show p = let sep = singleton dirSeparator
|
||||
volStr = fromMaybe "" (map show p.volumn)
|
||||
rootStr = if p.hasRoot then sep else ""
|
||||
bodyStr = join sep $ map show p.body
|
||||
trailStr = if p.hasTrailSep then sep else "" in
|
||||
volStr ++ rootStr ++ bodyStr ++ trailStr
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Parser
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
private
|
||||
data PathTokenKind = PTText | PTPunct Char
|
||||
|
||||
private
|
||||
Eq PathTokenKind where
|
||||
(==) PTText PTText = True
|
||||
(==) (PTPunct c1) (PTPunct c2) = c1 == c2
|
||||
(==) _ _ = False
|
||||
|
||||
private
|
||||
PathToken : Type
|
||||
PathToken = Token PathTokenKind
|
||||
|
||||
private
|
||||
TokenKind PathTokenKind where
|
||||
TokType PTText = String
|
||||
TokType (PTPunct _) = ()
|
||||
|
||||
tokValue PTText x = x
|
||||
tokValue (PTPunct _) _ = ()
|
||||
|
||||
private
|
||||
pathTokenMap : TokenMap PathToken
|
||||
pathTokenMap = toTokenMap $
|
||||
[ (is '/', PTPunct '/')
|
||||
, (is '\\', PTPunct '\\')
|
||||
, (is ':', PTPunct ':')
|
||||
, (is '?', PTPunct '?')
|
||||
, (some $ non $ oneOf "/\\:?", PTText)
|
||||
]
|
||||
|
||||
private
|
||||
lexPath : String -> Either String (List PathToken)
|
||||
lexPath str
|
||||
= case lex pathTokenMap str of
|
||||
(tokens, _, _, "") => Right (map TokenData.tok tokens)
|
||||
(tokens, l, c, rest) => Left ("Unrecognized tokens "
|
||||
++ show rest
|
||||
++ " at col "
|
||||
++ show c)
|
||||
|
||||
-- match both '/' and '\\' regardless of the platform.
|
||||
private
|
||||
bodySeparator : Grammar PathToken True ()
|
||||
bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/')
|
||||
|
||||
-- Example: \\?\
|
||||
-- Windows can automatically translate '/' to '\\'. The verbatim prefix,
|
||||
-- i.e., `\\?\`, disables the translation.
|
||||
-- Here, we simply parse and then ignore it.
|
||||
private
|
||||
verbatim : Grammar PathToken True ()
|
||||
verbatim = do count (exactly 2) $ match $ PTPunct '\\'
|
||||
match $ PTPunct '?'
|
||||
match $ PTPunct '\\'
|
||||
pure ()
|
||||
|
||||
-- Example: \\server\share
|
||||
private
|
||||
unc : Grammar PathToken True Volumn
|
||||
unc = do count (exactly 2) $ match $ PTPunct '\\'
|
||||
server <- match PTText
|
||||
bodySeparator
|
||||
share <- match PTText
|
||||
pure $ UNC server share
|
||||
|
||||
-- Example: \\?\server\share
|
||||
private
|
||||
verbatimUnc : Grammar PathToken True Volumn
|
||||
verbatimUnc = do verbatim
|
||||
server <- match PTText
|
||||
bodySeparator
|
||||
share <- match PTText
|
||||
pure $ UNC server share
|
||||
|
||||
-- Example: C:
|
||||
private
|
||||
disk : Grammar PathToken True Volumn
|
||||
disk = do text <- match PTText
|
||||
disk <- case unpack text of
|
||||
(disk :: xs) => pure disk
|
||||
[] => fail "Expect Disk"
|
||||
match $ PTPunct ':'
|
||||
pure $ Disk (toUpper disk)
|
||||
|
||||
-- Example: \\?\C:
|
||||
private
|
||||
verbatimDisk : Grammar PathToken True Volumn
|
||||
verbatimDisk = do verbatim
|
||||
d <- disk
|
||||
pure d
|
||||
|
||||
private
|
||||
parseVolumn : Grammar PathToken True Volumn
|
||||
parseVolumn = verbatimUnc
|
||||
<|> verbatimDisk
|
||||
<|> unc
|
||||
<|> disk
|
||||
|
||||
private
|
||||
parseBody : Grammar PathToken True Body
|
||||
parseBody = do text <- match PTText
|
||||
the (Grammar _ False _) $
|
||||
case text of
|
||||
" " => fail "Empty body"
|
||||
".." => pure ParentDir
|
||||
"." => pure CurDir
|
||||
s => pure (Normal s)
|
||||
|
||||
private
|
||||
parsePath : Grammar PathToken False Path
|
||||
parsePath = do vol <- optional parseVolumn
|
||||
root <- optional bodySeparator
|
||||
body <- sepBy bodySeparator parseBody
|
||||
trailSep <- optional bodySeparator
|
||||
pure $ MkPath vol (isJust root) body (isJust trailSep)
|
||||
|
||||
||| Attempt to parse a String into Path.
|
||||
|||
|
||||
||| Returns a error message if the parser fails.
|
||||
|||
|
||||
||| The parser is relaxed to accept invalid inputs. Relaxing rules:
|
||||
|||
|
||||
||| - Both slash('/') and backslash('\\') are parsed as directory separator,
|
||||
||| regardless of the platform;
|
||||
||| - Invalid characters in path body in allowed, e.g., glob like "/root/*";
|
||||
||| - Ignoring the verbatim prefix(`\\?\`) that disables the forward
|
||||
||| slash (Windows only).
|
||||
|||
|
||||
||| ```idris example
|
||||
||| parse "C:\\Windows/System32"
|
||||
||| ```
|
||||
||| ```idris example
|
||||
||| parse "/usr/local/etc/*"
|
||||
||| ```
|
||||
export
|
||||
parse : String -> Either String Path
|
||||
parse str = case parse parsePath !(lexPath str) of
|
||||
Right (p, []) => Right p
|
||||
Right (p, ts) => Left ("Unrecognised tokens remaining : "
|
||||
++ show (map text ts))
|
||||
Left (Error msg ts) => Left (msg ++ " : " ++ show (map text ts))
|
||||
|
||||
||| Attempt to parse the parts of a path and appends together.
|
||||
|||
|
||||
||| ```idris example
|
||||
||| parseParts ["/usr", "local/etc"]
|
||||
||| ```
|
||||
export
|
||||
parseParts : (parts : List String) -> Either String Path
|
||||
parseParts parts = map concat (traverse parse parts)
|
@ -26,6 +26,7 @@ modules = Control.Delayed,
|
||||
Text.Lexer.Core,
|
||||
|
||||
System.Clock,
|
||||
System.Path,
|
||||
System.Random,
|
||||
Syntax.WithProof,
|
||||
Syntax.PreorderReasoning
|
||||
|
Loading…
Reference in New Issue
Block a user