edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-08-16 19:30:32 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #390 from ska80/fix-idris2sh-build

Browse Source 
Fix building the latest self-hosted Idris 2
This commit is contained in:
Edwin Brady 2020-05-22 11:07:12 +01:00 committed by GitHub
commit e2ef9e05eb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 512 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -5,7 +5,7 @@
*.dSYM
/idris2
/idris2boot
/runtests
/dist/idris2.c

72
libs/base/Data/List.idr
View File

@ -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
View 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)

1
libs/contrib/contrib.ipkg
View File

@ -26,6 +26,7 @@ modules = Control.Delayed,
Text.Lexer.Core,
System.Clock,
System.Path,
System.Random,
Syntax.WithProof,
Syntax.PreorderReasoning