Skip to content

Commit

Permalink
[refactor] use Data.String.Parser instead of Text.Parser
Browse files Browse the repository at this point in the history
  • Loading branch information
running-grass committed Aug 5, 2022
1 parent 70db076 commit b0e07d9
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 72 deletions.
85 changes: 17 additions & 68 deletions src/Network/URL/General.idr
Original file line number Diff line number Diff line change
@@ -1,59 +1,7 @@
module Network.URL.General

import Text.Lexer
import Text.Parser

import Data.List1
import Data.String

private
data GeneralTokenKind
= Colon | Any

private
Eq GeneralTokenKind where
(==) Colon Colon = True
(==) Any Any = True
(==) _ _ = False

private
Show GeneralTokenKind where
show Colon = "Colon"
show Any = "Any"

private
TokenKind GeneralTokenKind where
TokType Colon = String
TokType Any = String

tokValue Colon _ = ":"
tokValue Any s = s

private
GeneralToken : Type
GeneralToken = Token GeneralTokenKind

private
Show GeneralToken where
show (Tok kind text) = "Tok kind: " ++ show kind ++ " text: " ++ text


-- Lexer


private
tokenMap : TokenMap GeneralToken
tokenMap = toTokenMap [
(is ':', Colon),
(some $ isNot ':', Any)
]

private
lexer : String -> Maybe (List (WithBounds GeneralToken))
lexer str =
case lex tokenMap str of
(tokens, _, _, "") => Just tokens
_ => Nothing
import Data.String.Parser

-- Data
public export
Expand All @@ -67,26 +15,27 @@ public export
Eq GeneralURL where
(MkGeneralURL scheme specific) == (MkGeneralURL scheme1 specific1) = scheme == scheme1 && specific == specific1

-- parser

private
url : Grammar state GeneralToken True GeneralURL
url = do
scheme <- match Any
_ <- match Colon
specific <- many (match Any <|> match Colon)
eof
pure $ MkGeneralURL scheme $ joinBy "" specific
letters : Parser String
letters = do
chars <- some $ letter
pure . joinBy "" . map Data.String.singleton $ chars

private
parser : List (WithBounds GeneralToken) -> Maybe GeneralURL
parser toks = case parse url toks of
Right (j, []) => Just j
_ => Nothing
private
url : Parser GeneralURL
url = do
scheme <- letters
token ":"
content <- takeWhile1 (\_ => True)
eos
pure $ MkGeneralURL scheme content

-- export function
public export
parse : String -> Maybe GeneralURL
parse x = parser !(lexer x)
parse str = case parse url str of
Right (j,_) => Just j
_ => Nothing

public export
stringify : GeneralURL -> String
Expand Down
8 changes: 4 additions & 4 deletions test/src/Test/General.idr
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,15 @@ import Network.URL.General
private
testParser : List Test
testParser = [
test "测试解析1" $ assertEq (parse "file://c:/path/file") (Just $ MkGeneralURL "file" "//c:/path/file")
, test "测试解析2" $ assertEq (parse "mailto:[email protected]") (Just $ MkGeneralURL "mailto" "[email protected]")
test "General测试解析1" $ assertEq (parse "file://c:/path/file") (Just $ MkGeneralURL "file" "//c:/path/file")
, test "General测试解析2" $ assertEq (parse "mailto:[email protected]") (Just $ MkGeneralURL "mailto" "[email protected]")
]

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]"
test "General测试序列化1" $ assertEq (stringify $ MkGeneralURL "file" "//c:/path/file") "file://c:/path/file"
, test "General测试序列化2" $ assertEq (stringify $ MkGeneralURL "mailto" "[email protected]") "mailto:[email protected]"
]

export
Expand Down

0 comments on commit b0e07d9

Please sign in to comment.