From b0e07d99db8a3cc7f5d7139417b301f24b854d2a Mon Sep 17 00:00:00 2001
From: Leo Liu <467195537@qq.com>
Date: Fri, 5 Aug 2022 13:26:42 +0800
Subject: [PATCH] [refactor] use Data.String.Parser instead of Text.Parser

---
 src/Network/URL/General.idr | 85 ++++++++-----------------------------
 test/src/Test/General.idr   |  8 ++--
 2 files changed, 21 insertions(+), 72 deletions(-)

diff --git a/src/Network/URL/General.idr b/src/Network/URL/General.idr
index ceb8e96..989ccee 100644
--- a/src/Network/URL/General.idr
+++ b/src/Network/URL/General.idr
@@ -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
@@ -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
diff --git a/test/src/Test/General.idr b/test/src/Test/General.idr
index d29af2e..de84c09 100644
--- a/test/src/Test/General.idr
+++ b/test/src/Test/General.idr
@@ -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:467195537@qq.com")  (Just $ MkGeneralURL "mailto" "467195537@qq.com")
+    test "General测试解析1" $ assertEq  (parse "file://c:/path/file")  (Just $ MkGeneralURL "file" "//c:/path/file")
+    , test "General测试解析2" $ assertEq  (parse "mailto:467195537@qq.com")  (Just $ MkGeneralURL "mailto" "467195537@qq.com")
 ]
 
 private
 testStringify : List Test
 testStringify = [
-    test "测试解析1" $ assertEq  (stringify $ MkGeneralURL "file" "//c:/path/file") "file://c:/path/file"
-    , test "测试解析2" $ assertEq  (stringify $ MkGeneralURL "mailto" "467195537@qq.com") "mailto:467195537@qq.com"
+    test "General测试序列化1" $ assertEq  (stringify $ MkGeneralURL "file" "//c:/path/file") "file://c:/path/file"
+    , test "General测试序列化2" $ assertEq  (stringify $ MkGeneralURL "mailto" "467195537@qq.com") "mailto:467195537@qq.com"
 ]
 
 export