Skip to content

Commit

Permalink
[feat] add HTTP URL stringify and testes
Browse files Browse the repository at this point in the history
  • Loading branch information
running-grass committed Jul 31, 2022
1 parent 629baa5 commit 70db076
Show file tree
Hide file tree
Showing 5 changed files with 148 additions and 43 deletions.
4 changes: 3 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@
# idris2-url
WIP……

A URL library for idris2, Based on [RFC 1738](https://www.rfc-wiki.org/wiki/RFC1738).

# Feature
- [x] General Sytax
- [ ] HTTP URL parse and stringify
- [x] HTTP URL parse and stringify
- [ ] HTTP URL utils
- [ ] FTP URL
23 changes: 22 additions & 1 deletion src/Network/URL/HTTP.idr
Original file line number Diff line number Diff line change
@@ -1,5 +1,26 @@
module Network.URL.HTTP


import public Network.URL.HTTP.Data

import Data.List
import Data.Fin

public export
insertParam : QueryParam -> HTTPURL -> HTTPURL
insertParam p@(key, value) url = { query := newQuery } url
where
params : List QueryParam
params = url.query

hasIn : Maybe (Fin (Prelude.List.length $ url.query))
hasIn = findIndex (\(k,_) => k == key) params

update : Fin (length (url .query)) -> List QueryParam -> List QueryParam
update idx ps = case inBounds (cast idx) ps of
(Yes _) => replaceAt (cast idx) p ps
_ => ps

newQuery : List QueryParam
newQuery = case hasIn of
Nothing => snoc params p
(Just idx) => update idx params
25 changes: 18 additions & 7 deletions src/Network/URL/HTTP/Data.idr
Original file line number Diff line number Diff line change
@@ -1,25 +1,36 @@
module Network.URL.HTTP.Data

-- Data
-- data HTTPURL = MkHTTPURL String String
public export
QueryParam : Type
QueryParam = (String, String)

public export
record HTTPURL where
constructor MkHTTPURL
scheme, host, port, path, query : String
scheme, host : String
port : Maybe String
path : String

query : List QueryParam

fragment : Maybe String

public export
Show HTTPURL where
show (MkHTTPURL scheme host port path query) = "MkHTTPURL \"" ++ scheme ++ "\" \""
show (MkHTTPURL scheme host port path query fragment) = "MkHTTPURL \"" ++ scheme ++ "\" \""
++ host ++ "\" \""
++ port ++ "\" \""
++ show port ++ "\" \""
++ path ++ "\" \""
++ query ++ "\""
++ show query ++ "\" \""
++ show fragment ++ "\""

public export
Eq HTTPURL where
(MkHTTPURL scheme host port path query) == (MkHTTPURL scheme1 host1 port1 path1 query1) =
(MkHTTPURL scheme host port path query fragment) == (MkHTTPURL scheme1 host1 port1 path1 query1 fragment1) =
scheme == scheme1
&& host == host1
&& port == port1
&& path == path1
&& query == query1
&& fragment == fragment1

98 changes: 75 additions & 23 deletions src/Network/URL/HTTP/Parser.idr
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ data HTTPTokenKind
= Alpha | Digit | Dot
| Colon | Plus | Minus
| NumberSign | QuestionMark
| Ampersand | EqualsSign
| Slash | Other

private
Expand All @@ -28,6 +29,8 @@ Eq HTTPTokenKind where
(==) Slash Slash = True
(==) NumberSign NumberSign = True
(==) QuestionMark QuestionMark = True
(==) Ampersand Ampersand = True
(==) EqualsSign EqualsSign = True
(==) Other Other = True
(==) _ _ = False

Expand All @@ -42,6 +45,8 @@ Show HTTPTokenKind where
show Slash = "Slash"
show NumberSign = "NumberSign"
show QuestionMark = "QuestionMark"
show Ampersand = "Ampersand"
show EqualsSign = "EqualsSign"
show Other = "Other"

private
Expand All @@ -55,6 +60,8 @@ TokenKind HTTPTokenKind where
TokType Slash = String
TokType NumberSign = String
TokType QuestionMark = String
TokType Ampersand = String
TokType EqualsSign = String
TokType Other = String

tokValue Alpha s = s
Expand All @@ -66,6 +73,8 @@ TokenKind HTTPTokenKind where
tokValue Slash s = s
tokValue NumberSign s = s
tokValue QuestionMark s = s
tokValue Ampersand s = s
tokValue EqualsSign s = s
tokValue Other s = s

private
Expand All @@ -89,6 +98,8 @@ tokenMap = toTokenMap [
(is '/', Slash),
(is '?', QuestionMark),
(is '#', NumberSign),
(is '&', Ampersand),
(is '=', EqualsSign),
(digit, Digit),
(alpha, Alpha),
(any, Other)
Expand Down Expand Up @@ -125,17 +136,35 @@ parserPath = do


private
parserQuery : Grammar state HTTPToken True String
parserQuery : Grammar state HTTPToken True (List QueryParam)
parserQuery = do
_ <- match QuestionMark
path1 <- many (match Slash
<|> match Alpha
<|> match Digit
<|> match Plus
<|> match Minus
<|> match Dot
<|> match Other)
pure $ joinBy "" path1
sepBy (match Ampersand) param

where
key : Grammar state HTTPToken False String
key = do
keys <- many (match Slash
<|> match Alpha
<|> match Digit
<|> match Plus
<|> match Minus
<|> match Dot
<|> match Other
)
pure $ joinBy "" keys

value : Grammar state HTTPToken False String
value = key

param : Grammar state HTTPToken True QueryParam
param = do
k <- optional key
_ <- match EqualsSign
v <- optional value

pure (fromMaybe "" k, fromMaybe "" v)


private
parserFragment : Grammar state HTTPToken True String
Expand All @@ -151,31 +180,37 @@ parserFragment = do
pure $ joinBy "" path1

private
url : Grammar state HTTPToken True HTTPURL
url = do
parserScheme : Grammar state HTTPToken True String
parserScheme = do
schemeHead <- match Alpha
schemeTail <- many (match Alpha <|> match Dot <|> match Plus <|> match Minus)

_ <- match Colon
c <- match Slash
c <- match Slash
pure $ schemeHead ++ joinBy "" schemeTail

private
parserHost : Grammar state HTTPToken True String
parserHost = do
_ <- match Slash
_ <- match Slash

host1 <- some (match Alpha <|> match Digit <|> match Plus <|> match Minus <|> match Dot)
pure $ joinBy "" (forget host1)

private
url : Grammar state HTTPToken True HTTPURL
url = do
scheme <- parserScheme
host <- parserHost
port1 <- optional port
path1 <- optional parserPath
query1 <- optional parserQuery
fragment1 <- optional parserFragment
eof

scheme <- pure $ schemeHead ++ joinBy "" schemeTail
host <- pure $ joinBy "" (forget host1)
port <- pure $ (fromMaybe "" port1)
path <- pure $ (fromMaybe "" path1)
query <- pure $ (fromMaybe "" query1)
fragment <- pure $ (fromMaybe "" fragment1)

pure $ MkHTTPURL scheme host port path query
path <- pure $ (fromMaybe "/" path1)
query <- pure $ (fromMaybe [] query1)

pure $ MkHTTPURL scheme host port1 path query fragment1

private
parser : List (WithBounds HTTPToken) -> Maybe HTTPURL
Expand All @@ -189,4 +224,21 @@ parse x = parser !(lexer x)

public export
stringify : HTTPURL -> String
stringify (MkHTTPURL scheme host port path query) = scheme ++ ":" ++ host
stringify (MkHTTPURL scheme host port path query fragment) = scheme
++ "://" ++ host ++ port'
++ path ++ query' ++ fragment'
where
port' : String
port' = case port of
Nothing => ""
(Just p) => ":" ++ p

query' : String
query' = case query of
[] => ""
xs => "?" ++ (joinBy "&" $ map (\(a,b) => a ++ "=" ++ b) xs)

fragment' : String
fragment' = case fragment of
Nothing => ""
(Just f) => "#" ++ f
41 changes: 30 additions & 11 deletions test/src/Test/HTTP.idr
Original file line number Diff line number Diff line change
Expand Up @@ -10,22 +10,41 @@ import Network.URL.HTTP.Parser
private
testParser : List Test
testParser = [
test "测试解析1" $ assertEq (parse "http://www.baidu.com") (Just $ MkHTTPURL "http" "www.baidu.com" "" "" "")
, test "测试解析2" $ assertEq (parse "http://127.0.0.1:8080") (Just $ MkHTTPURL "http" "127.0.0.1" "8080" "" "")
, test "测试解析3" $ assertEq (parse "http://127.0.0.1:8080/a/b.html") (Just $ MkHTTPURL "http" "127.0.0.1" "8080" "/a/b.html" "")
, test "测试解析4" $ assertEq (parse "http://127.0.0.1:8080/a/b.html?a=1&b=2") (Just $ MkHTTPURL "http" "127.0.0.1" "8080" "/a/b.html" "a=1&b=2")
test "测试解析1" $ assertEq (parse "http://www.baidu.com") (Just $ MkHTTPURL "http" "www.baidu.com" Nothing "/" [] Nothing)
, test "测试解析2" $ assertEq (parse "http://127.0.0.1:8080") (Just $ MkHTTPURL "http" "127.0.0.1" (Just "8080") "/" [] Nothing)
, test "测试解析3" $ assertEq (parse "http://127.0.0.1:8080/a/b.html") (Just $ MkHTTPURL "http" "127.0.0.1" (Just "8080") "/a/b.html" [] Nothing)
, test "测试解析4" $ assertEq (parse "http://127.0.0.1:8080/a/b.html?a=1&b=2") (Just $ MkHTTPURL "http" "127.0.0.1" (Just "8080") "/a/b.html" [("a","1"),("b","2")] Nothing)
, test "测试解析5" $ assertEq (parse "http://127.0.0.1:8080/a/b.html?a=1&b=2#hello-world") (Just $ MkHTTPURL "http" "127.0.0.1" (Just "8080") "/a/b.html" [("a","1"),("b","2")] (Just "hello-world"))
, test "测试解析6" $ assertEq (parse "http://127.0.0.1:8080/a/b.html#hello-world") (Just $ MkHTTPURL "http" "127.0.0.1" (Just "8080") "/a/b.html" [] (Just "hello-world"))
]

-- private
-- testStringify : List Test
-- testStringify = [
-- test "测试解析1" $ assertEq (stringify $ MkGeneralURL "file" "//c:/path/file") "file://c:/path/file"
-- , test "测试解析2" $ assertEq (stringify $ MkGeneralURL "mailto" "[email protected]") "mailto:[email protected]"
-- ]
private
testStringify : List Test
testStringify = [
test "测试编码1" $ assertEq (stringify $ MkHTTPURL "http" "127.0.0.1" (Just "8080") "/a/b.html" [("a","1"),("b","2")] (Just "hello-world")) "http://127.0.0.1:8080/a/b.html?a=1&b=2#hello-world"
, test "测试编码2" $ assertEq (stringify $ MkHTTPURL "http" "127.0.0.1" (Just "8080") "/a/b.html" [] (Just "hello-world")) "http://127.0.0.1:8080/a/b.html#hello-world"
]

private
mkUrlByParams : List QueryParam -> HTTPURL
mkUrlByParams qs = MkHTTPURL "https" "grass.show" Nothing "/" qs Nothing

private
testAddParams : List Test
testAddParams = [
test "向空列表插入查询参数" $ assertEq test1 $ insertParam ("a","1") test0
, test "向已有列表插入查询参数" $ assertEq test2 $ insertParam ("b","2") test1
, test "向已有列表更新查询参数" $ assertEq test1 $ insertParam ("a","1") test11
]
where
test0 = mkUrlByParams []
test1 = mkUrlByParams [("a","1")]
test11 = mkUrlByParams [("a","11")]
test2 = mkUrlByParams [("a","1"), ("b","2")]

export
tests : List Test
tests = testParser
tests = testParser ++ testStringify ++ testAddParams

private
main : IO Bool
Expand Down

0 comments on commit 70db076

Please sign in to comment.