gdris

A toy gopher client written in Idris2

git clone https://git.8pit.net/gdris.git

 1module Parser
 2
 3import Gopher
 4import Data.String.Parser
 5
 6many1 : Monad m => ParseT m a -> ParseT m (List a)
 7many1 p = do
 8	x  <- p
 9	xs <- (many p)
10	pure $ (x :: xs)
11
12parseUnAscii : ParseT IO Char
13parseUnAscii = satisfy isUnAscii <?> "any character except: Tab, CR-LF, NUL"
14
15parseType : ParseT IO ItemType
16parseType = do
17	res <- parseUnAscii
18	case (unmarshalType res) of
19		Just a  => pure $ a
20		Nothing => fail $ "unknown item type: " ++ show res
21
22parseDesc : ParseT IO String
23parseDesc = do
24	res <- many parseUnAscii
25	pure $ pack res
26
27parseSelector : ParseT IO Selector
28parseSelector = parseDesc
29
30parseHost' : ParseT IO String
31parseHost' = do
32	r1 <- many $ satisfy isHostPart
33	r2 <- (string ".")
34	pure $ ((pack r1) ++ r2)
35parseHost : ParseT IO String
36parseHost = do
37	name <- many parseHost'
38	tld  <- many $ satisfy isHostPart
39	pure $ (concat name) ++ (pack tld)
40
41parsePort : ParseT IO Nat
42parsePort = natural
43
44parseTab : ParseT IO Char
45parseTab = satisfy (\x => x == '\t') <?> "tab character"
46
47parseDelim : ParseT IO String
48parseDelim = string "\r\n"
49
50parseItem : ParseT IO Item
51parseItem = do
52	type <- parseType
53	desc <- parseDesc
54	ignore $ parseTab
55	select <- parseSelector
56	ignore $ parseTab
57	host <- parseHost
58	ignore $ parseTab
59	port <- parsePort
60	ignore $ parseDelim
61	pure $ MkItem type desc select (MkPair host port)
62
63parseItems : ParseT IO (List Item)
64parseItems = many1 parseItem
65
66public export
67parseAll : String -> IO (Either String (List Item))
68parseAll input = do
69	r <- parseT parseItems input
70	pure $ case r of
71		Left err => Left err
72		Right (items, n) => if n /= (cast $ length input)
73			then Left $ "not all data consumed, remaining: "
74				++ (show $ (cast (length input)) - n)
75			else Right items