0 | ||| 通用 URL 处理模块
 1 | ||| 提供基本的 URL 解析和字符串化功能
 2 | module Network.URL.General
 3 |
 4 | import Data.String
 5 | import Data.String.Parser
 6 | import Network.URL.Internal.StringParser
 7 |
 8 | ||| 表示一个通用的 URL 结构
 9 | ||| @scheme URL 的协议部分
10 | ||| @specific URL 的具体内容部分
11 | public export
12 | data GeneralURL = MkGeneralURL String String
13 |
14 | ||| 实现 Show 接口，用于将 URL 转换为字符串形式
15 | public export
16 | Show GeneralURL where
17 |   show (MkGeneralURL scheme specific) = "MkGeneralURL \"" ++ scheme ++ "\" \"" ++ specific ++ "\""
18 |
19 | ||| 实现 Eq 接口，用于比较两个 URL 是否相等
20 | public export
21 | Eq GeneralURL where
22 |   (MkGeneralURL scheme specific) == (MkGeneralURL scheme1 specific1) = scheme == scheme1 && specific == specific1
23 |
24 | ||| 内部解析器，用于解析 URL 字符串
25 | private 
26 | url : Parser GeneralURL
27 | url = do
28 |   scheme <- schemeParser     -- 解析协议部分（允许字母、数字、+、-、.，首字母为字母）
29 |   token ":"            -- 解析冒号分隔符
30 |   content <- takeWhile1 (\_ => True)  -- 解析剩余的所有内容
31 |   eos                  -- 确保到达字符串末尾
32 |   pure $ MkGeneralURL scheme content
33 |
34 | ||| 将字符串解析为 URL
35 | ||| @str 要解析的字符串
36 | ||| @returns 如果解析成功则返回 Just GeneralURL，否则返回 Nothing
37 | public export
38 | parse : String -> Maybe GeneralURL
39 | parse str = case parse url str of
40 |               Right (j,_) => Just j
41 |               _ => Nothing
42 |
43 | ||| 将 URL 转换为字符串形式
44 | ||| @url 要转换的 URL
45 | ||| @returns URL 的字符串表示
46 | public export
47 | stringify : GeneralURL -> String
48 | stringify (MkGeneralURL scheme specific) = scheme ++ ":" ++ specific