[refactor] use Data.String.Parser instead of Text.Parser for HTTPURL

src/Network/URL/General.idr

@@ -2,7 +2,7 @@ module Network.URL.General
 
 import Data.String
 import Data.String.Parser
-
+import Network.URL.Internal.StringParser
 -- Data
 public export
 data GeneralURL  = MkGeneralURL String String
@@ -15,11 +15,7 @@ public export
 Eq GeneralURL where
   (MkGeneralURL scheme specific) == (MkGeneralURL scheme1 specific1) = scheme == scheme1 && specific == specific1
 
-private
-letters : Parser String
-letters  = do
-  chars <- some $ letter
-  pure . joinBy "" . map Data.String.singleton $ chars
+
 
 private 
 url : Parser GeneralURL

src/Network/URL/HTTP.idr

@@ -5,6 +5,7 @@ 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

src/Network/URL/HTTP/Data.idr

@@ -8,7 +8,7 @@ public export
 record HTTPURL where
     constructor MkHTTPURL
     scheme, host : String
-    port : Maybe String
+    port : Maybe Int
     path : String
 
     query : List QueryParam

src/Network/URL/HTTP/Parser.idr

@@ -3,225 +3,97 @@ module Network.URL.HTTP.Parser
 import Text.Lexer
 import Text.Parser
 
+
 import Data.List1
+import Data.List
 import Data.String
 import Data.Maybe
 
 import Network.URL.HTTP.Data
-
-
-private
-data HTTPTokenKind
-  = Alpha | Digit | Dot 
-    | Colon | Plus | Minus 
-    | NumberSign | QuestionMark
-    | Ampersand | EqualsSign
-    | Slash | Other
-
-private
-Eq HTTPTokenKind where
-  (==) Alpha Alpha = True
-  (==) Digit Digit = True
-  (==) Dot Dot = True
-  (==) Colon Colon = True
-  (==) Plus Plus = True
-  (==) Minus Minus = True
-  (==) Slash Slash = True
-  (==) NumberSign NumberSign = True
-  (==) QuestionMark QuestionMark = True
-  (==) Ampersand Ampersand = True
-  (==) EqualsSign EqualsSign = True
-  (==) Other Other = True
-  (==) _ _ = False
-
-private
-Show HTTPTokenKind where
-  show Alpha = "Alpha"
-  show Digit = "Digit"
-  show Dot = "Dot"
-  show Colon = "Colon"
-  show Plus = "Plus"
-  show Minus = "Minus"
-  show Slash = "Slash"
-  show NumberSign = "NumberSign"
-  show QuestionMark = "QuestionMark"
-  show Ampersand = "Ampersand"
-  show EqualsSign = "EqualsSign"
-  show Other = "Other"
+import Network.URL.Internal.StringParser
+import Network.URL.Internal.Predicate
+import Data.String.Parser
 
 private
-TokenKind HTTPTokenKind where
-  TokType Alpha = String
-  TokType Digit = String
-  TokType Dot = String
-  TokType Colon = String
-  TokType Plus = String
-  TokType Minus = String
-  TokType Slash = String
-  TokType NumberSign = String
-  TokType QuestionMark = String
-  TokType Ampersand = String
-  TokType EqualsSign = String
-  TokType Other = String
-
-  tokValue Alpha s = s
-  tokValue Digit s = s
-  tokValue Dot s = s
-  tokValue Colon s = s
-  tokValue Plus s = s
-  tokValue Minus s = s
-  tokValue Slash s = s
-  tokValue NumberSign s = s
-  tokValue QuestionMark s = s
-  tokValue Ampersand s = s
-  tokValue EqualsSign s = s
-  tokValue Other s = s
+validaId : Char -> Bool
+validaId = anyPass [isAlphaNum, (== '+'), (== '-'), (== '.')]
 
-private
-HTTPToken : Type
-HTTPToken = Token HTTPTokenKind
-
-private
-Show HTTPToken where
-    show (Tok kind text) = "(" ++ show kind ++ " " ++ text ++ ")"
-
-
--- Lexer
+private 
+parserScheme : Parser String
+parserScheme = do
+  schemeHead <- letter
+  schemeTail <- takeWhile validaId
+  token ":"
+  pure $ singleton schemeHead ++ schemeTail
 
 private
-tokenMap : TokenMap HTTPToken
-tokenMap = toTokenMap [
-  (is '.',  Dot),
-  (is ':',  Colon),
-  (is '+',  Plus),
-  (is '-',  Minus),
-  (is '/',  Slash),
-  (is '?',  QuestionMark),
-  (is '#',  NumberSign),
-  (is '&',  Ampersand),
-  (is '=',  EqualsSign),
-  (digit,  Digit),
-  (alpha,  Alpha),
-  (any, Other)
-]
+parserHost : Parser String
+parserHost = do
+  token "//"
+  takeWhile1 validaId
 
 private
-lexer : String -> Maybe (List (WithBounds HTTPToken))
-lexer str = 
-  case lex tokenMap str of
-    (tokens, _, _, "") => Just tokens
-    _ => Nothing
-
--- parser
+parserPort : Parser Int
+parserPort = do
+  token ":"
+  int
 
 private
-port : Grammar state HTTPToken True String
-port = do
-  _ <- match Colon
-  p <- some $ match Digit
-  pure $ joinBy "" $ forget p
+parserPathItem : Parser String
+parserPathItem = do
+  token "/"
+  s <- takeWhile $ allPass [(/= '/'), (/= '?'), (/= '#')]
+  pure $ "/" ++ s
 
 private
-parserPath : Grammar state HTTPToken True String
+parserPath : Parser String
 parserPath = do
-  _ <- match Slash
-  path1 <- many (match Slash 
-              <|> match Alpha 
-              <|> match Digit 
-              <|> match Plus 
-              <|> match Minus 
-              <|> match Dot 
-              <|> match Other)
-  pure $ "/" ++  joinBy "" path1
+  s <- some parserPathItem
+  pure $ joinBy "" s
 
+private
+parserQueryItem : Parser QueryParam
+parserQueryItem = do
+  s <- sepBy1 (takeWhile $ allPass [(/= '#'), (/= '&'), (/= '=')]) (token "=")
+  case s of
+    (k ::: Nil) => pure (k, "")
+    (k ::: vs) => pure (k, joinBy "" vs)
+
 
 private
-parserQuery : Grammar state HTTPToken True (List QueryParam)
+parserQuery : Parser (List QueryParam)
 parserQuery = do
-  _ <- match QuestionMark
-  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)
-
+  token "?"
+  l <- sepBy1 parserQueryItem $ token "&"
+  pure $ forget l
 
-private
-parserFragment : Grammar state HTTPToken True String
-parserFragment = do
-  _ <- match NumberSign
-  path1 <- many (match Slash 
-              <|> match Alpha 
-              <|> match Digit 
-              <|> match Plus 
-              <|> match Minus 
-              <|> match Dot 
-              <|> match Other)
-  pure $ joinBy "" path1
 
-private
-parserScheme : Grammar state HTTPToken True String
-parserScheme = do
-  schemeHead <- match Alpha 
-  schemeTail <- many (match Alpha <|> match Dot <|> match Plus <|> match Minus)
-  _ <- match Colon
-  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)
+parserFragment : Parser String
+parserFragment = do
+  token "#"
+  takeWhile (\t => True)
 
-private
-url : Grammar state HTTPToken True HTTPURL
+private 
+url : Parser HTTPURL
 url = do
   scheme <- parserScheme
-  host <- parserHost
-  port1 <- optional port
-  path1 <- optional parserPath
-  query1 <- optional parserQuery
-  fragment1 <- optional parserFragment
-  eof
-
-  path <- pure $ (fromMaybe "/" path1)
-  query <- pure $ (fromMaybe [] query1)
-
-  pure $ MkHTTPURL scheme host port1 path query fragment1
-
-private
-parser : List (WithBounds HTTPToken) -> Maybe HTTPURL
-parser toks = case parse url toks of
-                      Right (j, []) => Just j
-                      _ => Nothing
-
+  content <- parserHost
+  port <- optional parserPort
+  path <- option "/" parserPath
+  query <- option [] parserQuery
+  fragment <- optional parserFragment
+  eos
+  pure $ MkHTTPURL scheme content port path query fragment
+
+-- export function
 public export
 parse : String -> Maybe HTTPURL
-parse x = parser !(lexer x)
-
+parse str = case parse url str of
+              Right (j,_) => Just j
+              _ => Nothing
+
 public export
 stringify : HTTPURL -> String
 stringify (MkHTTPURL scheme host port path query fragment) = scheme 
@@ -231,7 +103,7 @@ stringify (MkHTTPURL scheme host port path query fragment) = scheme
     port' : String
     port' = case port of
       Nothing => ""
-      (Just p) => ":" ++ p
+      (Just p) => ":" ++ show p
 
     query' : String
     query' = case query of

src/Network/URL/Internal/Predicate.idr

@@ -0,0 +1,24 @@
+module Network.URL.Internal.Predicate
+
+%default total
+
+--  针对类型a的谓词
+public export
+Predicate : Type -> Type 
+Predicate a = a -> Bool
+
+-- 特别的，如果没有谓词，算是不通过
+-- 任意一个通过，算是整体通过
+public export
+anyPass : List (Predicate a) -> a -> Bool
+anyPass [] _ = False
+anyPass [p] x = p x
+anyPass (p :: ps) x = p x || anyPass ps x
+
+-- 特别的，如果没有谓词，算是不通过
+-- 全部通过，才算是整体通过
+public export
+allPass : List (Predicate a) -> a -> Bool
+allPass [] _ = False
+allPass [p] x = p x
+allPass (p :: ps) x = p x && allPass ps x

src/Network/URL/Internal/StringParser.idr

@@ -0,0 +1,23 @@
+module Network.URL.Internal.StringParser
+
+import Data.String.Parser
+import Data.String
+import Data.Fin
+
+export
+letters : Parser String
+letters = do
+  chars <- some $ letter
+  pure . joinBy "" . map Data.String.singleton $ chars
+
+export
+digits : Parser String
+digits = do 
+  ds <- some $ digit
+  pure . joinBy "" . map show $ ds
+
+export
+int : Parser Int
+int = do
+  ds <- digits
+  pure $ cast ds

test/src/Test/General.idr

@@ -5,6 +5,7 @@ import Tester.Runner
 
 import Network.URL.General
 
+
 -- 测试斜体
 private
 testParser : List Test