0 | ||| This provides a more or less reasonable representation for
  1 | ||| bodies in a file path.
  2 | module Data.FilePath.Body
  3 |
  4 | import Data.List
  5 | import Data.List1
  6 | import System.Info
  7 |
  8 | %default total
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          Utils
 12 | --------------------------------------------------------------------------------
 13 |
 14 | public export
 15 | check : (b : Bool) -> Maybe (b === True)
 16 | check False = Nothing
 17 | check True  = Just Refl
 18 |
 19 | 0 unAnd : {x,y : Bool} -> (x && y) === True -> (x === True, y === True)
 20 | unAnd {x = True}  {y = True}  _ = (Refl,Refl)
 21 | unAnd {x = True}  {y = False} _ impossible
 22 | unAnd {x = False} {y = _}     _ impossible
 23 |
 24 | 0 unAnd1 : {x,y : Bool} -> (x && y) === True -> x === True
 25 | unAnd1 = fst . unAnd
 26 |
 27 | 0 unAnd2 : {x,y : Bool} -> (x && y) === True -> y === True
 28 | unAnd2 = snd . unAnd
 29 |
 30 | 0 and : {x,y : Bool} -> x === True -> y === True -> (x && y) === True
 31 | and {x = True}  {y = True}  _ _ = Refl
 32 | and {x = True}  {y = False} _ _ impossible
 33 | and {x = False} {y = _}     _ _ impossible
 34 |
 35 | --------------------------------------------------------------------------------
 36 | --          Constants
 37 | --------------------------------------------------------------------------------
 38 |
 39 | ||| The platform dependent path separator
 40 | public export %inline
 41 | Sep : Char
 42 | Sep = '/'
 43 |
 44 | --------------------------------------------------------------------------------
 45 | --          BodyChar
 46 | --------------------------------------------------------------------------------
 47 |
 48 | ||| A character acceptable in the middle of a path body.
 49 | ||| We don't allow path separators and control characters in path bodies.
 50 | public export
 51 | isBodyChar : Char -> Bool
 52 | isBodyChar '/'  = False
 53 | isBodyChar '\\' = False
 54 | isBodyChar c    = not (isControl c)
 55 |
 56 | public export
 57 | 0 BodyChar : Char -> Type
 58 | BodyChar c = isBodyChar c === True
 59 |
 60 | export
 61 | 0 notBodyCharTab : BodyChar '\t' -> Void
 62 | notBodyCharTab prf impossible
 63 |
 64 | export
 65 | 0 notBodyCharRet : BodyChar '\r' -> Void
 66 | notBodyCharRet prf impossible
 67 |
 68 | export
 69 | 0 notBodyCharNL : BodyChar '\n' -> Void
 70 | notBodyCharNL prf impossible
 71 |
 72 | export
 73 | 0 notBodyCharB : BodyChar '\b' -> Void
 74 | notBodyCharB prf impossible
 75 |
 76 | export
 77 | 0 notBodyChar0 : BodyChar '\0' -> Void
 78 | notBodyChar0 prf impossible
 79 |
 80 | --------------------------------------------------------------------------------
 81 | --          EndChar
 82 | --------------------------------------------------------------------------------
 83 |
 84 | ||| We don't accept spaces at the end of path bodies.
 85 | public export
 86 | isEndChar : Char -> Bool
 87 | isEndChar c = isBodyChar c && c /= ' '
 88 |
 89 | public export
 90 | 0 EndChar : Char -> Type
 91 | EndChar c = isEndChar c === True
 92 |
 93 | export
 94 | Uninhabited (EndChar ' ') where
 95 |   uninhabited prf impossible
 96 |
 97 | export
 98 | 0 notEndCharSpace : EndChar ' ' -> Void
 99 | notEndCharSpace prf impossible
100 |
101 | --------------------------------------------------------------------------------
102 | --          SingleChar
103 | --------------------------------------------------------------------------------
104 |
105 | ||| We don't accept path bodies consisting of a single dot.
106 | public export
107 | isSingleChar : Char -> Bool
108 | isSingleChar c = isEndChar c && c /= '.'
109 |
110 | public export
111 | 0 SingleChar : Char -> Type
112 | SingleChar c = isSingleChar c === True
113 |
114 | export
115 | 0 notSingleCharDot : SingleChar '.' -> Void
116 | notSingleCharDot prf impossible
117 |
118 | --------------------------------------------------------------------------------
119 | --          BodyInner
120 | --------------------------------------------------------------------------------
121 |
122 | ||| True if the given list of characters can appear after the initial
123 | ||| character of a path body.
124 | public export
125 | isBodyInner : List Char -> Bool
126 | isBodyInner []        = False
127 | isBodyInner (x :: []) = isEndChar x
128 | isBodyInner (x :: xs) = isBodyChar x && isBodyInner xs
129 |
130 | public export
131 | 0 BodyInner : List Char -> Type
132 | BodyInner xs = isBodyInner xs === True
133 |
134 | ||| True if the given list of characters represent a valid path body.
135 | public export
136 | isBodyChars : List Char -> Bool
137 | isBodyChars []        = False
138 | isBodyChars (x :: []) = isSingleChar x
139 | isBodyChars (x :: xs) = isEndChar x && isBodyInner xs
140 |
141 | public export
142 | 0 BodyChars : List Char -> Type
143 | BodyChars xs = isBodyChars xs === True
144 |
145 | 0 notBodyCharsEmpty : BodyChars [] -> Void
146 | notBodyCharsEmpty refl impossible
147 |
148 | 0 notBodyCharsDot : BodyChars ['.'] -> Void
149 | notBodyCharsDot refl impossible
150 |
151 | --------------------------------------------------------------------------------
152 | --          Concatenation Proofs
153 | --------------------------------------------------------------------------------
154 |
155 | export
156 | 0 toInner : (xs : List Char) -> BodyChars xs -> BodyInner xs
157 | toInner (x :: [])      prf = unAnd1 prf
158 | toInner (x :: y :: ys) prf =
159 |   let (p1,p2) = unAnd prf in and (unAnd1 p1) p2
160 | toInner []             prf impossible
161 |
162 | export
163 | 0 appendInnerChars :
164 |      (xs,ys : List Char)
165 |   -> BodyInner xs
166 |   -> BodyInner ys
167 |   -> BodyInner (xs ++ ys)
168 | appendInnerChars (h :: [])      (y :: ys) prf1 prf2 =
169 |   and (unAnd1 prf1) prf2
170 | appendInnerChars (h :: t@(x :: xs)) ys prf1 prf2 =
171 |   and (unAnd1 prf1) (appendInnerChars t ys (unAnd2 prf1) prf2)
172 | appendInnerChars [] _ _ _ impossible
173 | appendInnerChars _  [] _ _ impossible
174 |
175 | export
176 | 0 appendBodyChars :
177 |      (xs,ys : List Char)
178 |   -> BodyChars xs
179 |   -> BodyChars ys
180 |   -> BodyChars (xs ++ ys)
181 | appendBodyChars (h :: [])      (y :: ys) prf1 prf2 =
182 |   and (unAnd1 prf1) (toInner (y :: ys) prf2)
183 | appendBodyChars (h :: x :: xs) ys prf1 prf2 =
184 |   and (unAnd1 prf1) (appendInnerChars _ _ (unAnd2 prf1) $ toInner _ prf2)
185 | appendBodyChars [] _ _ _ impossible
186 | appendBodyChars _  [] _ _ impossible
187 |
188 | export
189 | 0 preDotBodyChars : (cs : List Char) -> BodyChars cs -> BodyChars ('.' :: cs)
190 | preDotBodyChars (h :: t) prf = toInner _ prf
191 | preDotBodyChars [] prf impossible
192 |
193 | --------------------------------------------------------------------------------
194 | --          Body
195 | --------------------------------------------------------------------------------
196 |
197 | ||| A single body in a path. This is represented as a list of characters,
198 | ||| since otherwise we'd have to constantly unpack and pack this anyway.
199 | public export
200 | record Body where
201 |   constructor MkBody
202 |   body  : List Char
203 |   0 prf : BodyChars body
204 |
205 | public export %inline
206 | Eq Body where
207 |   MkBody x _ == MkBody y _ = x == y
208 |
209 | public export %inline
210 | Ord Body where
211 |   compare (MkBody x _) (MkBody y _) = compare x y
212 |
213 | export
214 | Show Body where
215 |   showPrec p (MkBody b _) = showCon p "MkBody" $ showArg b ++ " _"
216 |
217 | public export %inline
218 | Interpolation Body where
219 |   interpolate (MkBody b _) = pack b
220 |
221 | export %inline
222 | Semigroup Body where
223 |   MkBody x px <+> MkBody y py = MkBody (x ++ y) (appendBodyChars _ _px py)
224 |
225 |
226 | ||| Tries to convert a list of character to a body
227 | public export
228 | fromChars : List Char -> Maybe Body
229 | fromChars cs = case check (isBodyChars cs) of
230 |   Just prf => Just $ MkBody cs prf
231 |   Nothing  => Nothing
232 |
233 | ||| Tries to convert a string to a body
234 | public export %inline
235 | parse : String -> Maybe Body
236 | parse = fromChars . unpack
237 |
238 | public export
239 | fromString : (s : String) -> {auto 0 p : BodyChars (unpack s)} -> Body
240 | fromString s = MkBody (unpack s) p
241 |
242 | export
243 | preDot : Body -> Body
244 | preDot (MkBody cs p) = MkBody ('.' :: cs) (preDotBodyChars _ p)
245 |
246 | export infixr 7 <.>
247 |
248 | ||| Append a file ending to a path body.
249 | export
250 | (<.>) : Body -> Body -> Body
251 | x <.> y = x <+> preDot y
252 |
253 | ||| Tries to split a path body into its stem an extension.
254 | export
255 | split : Body -> Maybe (Body,Body)
256 | split (MkBody b _) =
257 |   let ss := split ('.' ==) b
258 |    in [| MkPair
259 |            (fromChars $ join $ intersperse ['.'] (init ss))
260 |            (fromChars $ last ss) |]
261 |
262 | ||| Tries to extract a stem from a file name.
263 | export %inline
264 | fileStem : Body -> Maybe Body
265 | fileStem = map fst . split
266 |
267 | ||| True if the file body starts with a dot.
268 | export
269 | isHidden : Body -> Bool
270 | isHidden (MkBody ('.' :: _) _) = True
271 | isHidden _                     = False
272 |
273 | ||| Tries to extract an extension from a file name.
274 | export %inline
275 | extension : Body -> Maybe Body
276 | extension = map snd . split
277 |
278 | --------------------------------------------------------------------------------
279 | --          Tests
280 | --------------------------------------------------------------------------------
281 |
282 | -- Performance test: This typechecks *much* faster than the original
283 | -- implementation
284 | test : Body
285 | test =
286 |   fromString $
287 |        "sdfljlsjdfsdfjl_kklsdfkj2320398wejjkwe0r9u23__02394oweijwjf"
288 |     ++ "sdfljlsjdfsdfjl_kklsdfkj2320398wejjkwe0r9u23__02394oweijwjf"
289 |     ++ "sdfljlsjdfsdfjl_kklsdfkj2320398wejjkwe0r9u23__02394oweijwjf"
290 |     ++ "sdfljlsjdfsdfjl_kklsdfkj2320398wejjkwe0r9u23__02394oweijwjf"
291 |