Data.FilePath.Body

This provides a more or less reasonable representation for
bodies in a file path.

Definitions

check : (b : Bool) -> Maybe (b = True)

Totality: total
Visibility: public export

Sep : Char

  The platform dependent path separator

Totality: total
Visibility: public export

isBodyChar : Char -> Bool

  A character acceptable in the middle of a path body.
  We don't allow path separators and control characters in path bodies.

Totality: total
Visibility: public export

0 BodyChar : Char -> Type

Totality: total
Visibility: public export

0 notBodyCharTab : BodyChar '\t' -> Void

Totality: total
Visibility: export

0 notBodyCharRet : BodyChar '\r' -> Void

Totality: total
Visibility: export

0 notBodyCharNL : BodyChar '\n' -> Void

Totality: total
Visibility: export

0 notBodyCharB : BodyChar '\b' -> Void

Totality: total
Visibility: export

0 notBodyChar0 : BodyChar '\NUL' -> Void

Totality: total
Visibility: export

isEndChar : Char -> Bool

  We don't accept spaces at the end of path bodies.

Totality: total
Visibility: public export

0 EndChar : Char -> Type

Totality: total
Visibility: public export

0 notEndCharSpace : EndChar ' ' -> Void

Totality: total
Visibility: export

isSingleChar : Char -> Bool

  We don't accept path bodies consisting of a single dot.

Totality: total
Visibility: public export

0 SingleChar : Char -> Type

Totality: total
Visibility: public export

0 notSingleCharDot : SingleChar '.' -> Void

Totality: total
Visibility: export

isBodyInner : List Char -> Bool

  True if the given list of characters can appear after the initial
  character of a path body.

Totality: total
Visibility: public export

0 BodyInner : List Char -> Type

Totality: total
Visibility: public export

isBodyChars : List Char -> Bool

  True if the given list of characters represent a valid path body.

Totality: total
Visibility: public export

0 BodyChars : List Char -> Type

Totality: total
Visibility: public export

0 toInner : (xs : List Char) -> BodyChars xs -> BodyInner xs

Totality: total
Visibility: export

0 appendInnerChars : (xs : List Char) -> (ys : List Char) -> BodyInner xs -> BodyInner ys -> BodyInner (xs ++ ys)

Totality: total
Visibility: export

0 appendBodyChars : (xs : List Char) -> (ys : List Char) -> BodyChars xs -> BodyChars ys -> BodyChars (xs ++ ys)

Totality: total
Visibility: export

0 preDotBodyChars : (cs : List Char) -> BodyChars cs -> BodyChars ('.' :: cs)

Totality: total
Visibility: export

record Body : Type

  A single body in a path. This is represented as a list of characters,
  since otherwise we'd have to constantly unpack and pack this anyway.

Totality: total
Visibility: public export
Constructor: 

MkBody : (body : List Char) -> (0 _ : BodyChars body) -> Body

Projections:

.body : Body -> List Char

0 .prf : ({rec:0} : Body) -> BodyChars (body {rec:0})

Hints:

Eq Body

Interpolation Body

Ord Body

Semigroup Body

Show Body

.body : Body -> List Char

Totality: total
Visibility: public export

body : Body -> List Char

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Body) -> BodyChars (body {rec:0})

Totality: total
Visibility: public export

0 prf : ({rec:0} : Body) -> BodyChars (body {rec:0})

Totality: total
Visibility: public export

fromChars : List Char -> Maybe Body

  Tries to convert a list of character to a body

Totality: total
Visibility: public export

parse : String -> Maybe Body

  Tries to convert a string to a body

Totality: total
Visibility: public export

fromString : (s : String) -> {auto 0 _ : BodyChars (unpack s)} -> Body

Totality: total
Visibility: public export

preDot : Body -> Body

Totality: total
Visibility: export

(<.>) : Body -> Body -> Body

  Append a file ending to a path body.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

split : Body -> Maybe (Body, Body)

  Tries to split a path body into its stem an extension.

Totality: total
Visibility: export

fileStem : Body -> Maybe Body

  Tries to extract a stem from a file name.

Totality: total
Visibility: export

isHidden : Body -> Bool

  True if the file body starts with a dot.

Totality: total
Visibility: export

extension : Body -> Maybe Body

  Tries to extract an extension from a file name.

Totality: total
Visibility: export