28 lines
613 B
Agda
28 lines
613 B
Agda
module Data.List1
|
||
|
||
import Prelude
|
||
|
||
infixr 7 _:::_
|
||
|
||
record List1 a where
|
||
constructor _:::_
|
||
head1 : a
|
||
tail1 : List a
|
||
|
||
splitBy1 : String → Char → List1 String
|
||
splitBy1 str by = case splitBy str by of
|
||
Nil => str ::: Nil
|
||
x :: xs => x ::: xs
|
||
|
||
unsnoc : ∀ a. List1 a → List a × a
|
||
unsnoc {a} (x ::: xs) = go x xs
|
||
where
|
||
go : a → List a → List a × a
|
||
go x Nil = (Nil, x)
|
||
go x (y :: ys) = let (as, a) = go y ys in (x :: as, a)
|
||
|
||
splitFileName : String → String × String
|
||
splitFileName fn = case splitBy1 fn '.' of
|
||
part ::: Nil => (part, "")
|
||
xs => mapFst (joinBy ".") $ unsnoc xs
|