
  0 | module Network.HTTP.Path
  1 | 
  2 | import Data.String
  3 | import Data.String.Extra
  4 | import Data.List1
  5 | import Data.List
  6 | import Derive.Prelude
  7 | 
  8 | %language ElabReflection
  9 | 
 10 | data PathComponent : Type where
 11 |   Root : PathComponent
 12 |   Parent : PathComponent
 13 |   Current : PathComponent
 14 |   End : PathComponent
 15 |   Named : String -> PathComponent
 16 | 
 17 | %runElab derive "PathComponent" [Eq]
 18 | 
 19 | export
 20 | record Path where
 21 |   constructor MkPath
 22 |   components : List1 PathComponent
 23 | 
 24 | zip_with_last : List a -> List (a, Maybe a)
 25 | zip_with_last list =
 26 |   let (_ :: xs) = map Just list
 27 |   | [] => []
 28 |   in zip list (snoc xs Nothing)
 29 | 
 30 | export
 31 | normalize : Path -> Path
 32 | normalize path = decompose $ trim_root path.components where
 33 |   is_current : PathComponent -> Bool
 34 |   is_current Current = True
 35 |   is_current (Named "") = True
 36 |   is_current _ = False
 37 | 
 38 |   rid_current : List PathComponent -> List PathComponent
 39 |   rid_current components = filter (not . is_current) components
 40 | 
 41 |   rid_parent : List PathComponent -> List PathComponent -> List PathComponent
 42 |   rid_parent acc [] = reverse acc
 43 |   rid_parent acc@(Parent :: as) (Parent :: xs) = rid_parent (Parent :: acc) xs
 44 |   rid_parent acc@(Root :: as) (Parent :: xs) = rid_parent acc xs
 45 |   rid_parent (a :: as) (Parent :: xs) = rid_parent as xs
 46 |   rid_parent acc (x :: xs) = rid_parent (x :: acc) xs
 47 | 
 48 |   append_current : List PathComponent -> List1 PathComponent
 49 |   append_current (Named x :: xs) = Current ::: (Named x :: xs)
 50 |   append_current [] = Current ::: []
 51 |   append_current (x :: xs) = (x ::: xs)
 52 | 
 53 |   decompose : List1 PathComponent -> Path
 54 |   decompose (x ::: xs) = MkPath $ append_current $ rid_parent [] (x :: rid_current xs)
 55 | 
 56 |   trim_root : List1 PathComponent -> List1 PathComponent
 57 |   trim_root list = case dropWhile (/= Root) $ forget list of [] => list; (x :: xs) => x ::: xs
 58 | 
 59 | concat : List a -> List1 a -> List1 a
 60 | concat [] y = y
 61 | concat (x :: xs) (y ::: ys) = x ::: (xs <+> (y :: ys))
 62 | 
 63 | export
 64 | Semigroup Path where
 65 |   a <+> b =
 66 |     let as = (normalize a).components
 67 |         ai = init as
 68 |     in normalize $ MkPath $ concat ai (normalize b).components
 69 | 
 70 | export
 71 | Show Path where
 72 |   show path = trim_leading_roots $ join "/" $ map component_to_string path.components
 73 |     where
 74 |       trim_leading_roots : String -> String
 75 |       trim_leading_roots str = assert_total $ if isPrefixOf "//" str then strTail str else str
 76 | 
 77 |       component_to_string : PathComponent -> String
 78 |       component_to_string Root = "/"
 79 |       component_to_string End = "/"
 80 |       component_to_string Parent = ".."
 81 |       component_to_string Current = "."
 82 |       component_to_string (Named x) = x
 83 | 
 84 | export
 85 | FromString Path where
 86 |   fromString "" = MkPath $ singleton Current
 87 |   fromString string =
 88 |     MkPath $ case split ('/' ==) string of
 89 |       ("" ::: xs) => Root ::: (map string_to_component xs)
 90 |       (x ::: xs) => map string_to_component $ (x ::: xs)
 91 |   where
 92 |     string_to_component : String -> PathComponent
 93 |     string_to_component "" = End
 94 |     string_to_component "." = Current
 95 |     string_to_component ".." = Parent
 96 |     string_to_component x = Named x
 97 |