gdris

A toy gopher client written in Idris2

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

  1module Gdris
  2
  3import Gopher
  4import Client
  5import Parser
  6import Menu
  7
  8import System
  9import System.File
 10
 11import Data.Fin
 12import Data.Vect
 13import Data.Strings
 14
 15import Network.Socket.Data
 16
 17-- Valid REPL input commands.
 18data Command = Goto Integer | Menu | Exit | Unknown
 19
 20-- REPL execution context.
 21record Context where
 22    constructor MkCtx
 23    menu   : (List Item)
 24
 25-- String used to prompt for input.
 26prompt : String
 27prompt = "> "
 28
 29newCtx : Context -> (List Item) -> Context
 30newCtx _ items = MkCtx items
 31
 32-- XXX: If this returns a Maybe Monad the totality checker doesn't terminate
 33lineToCmd : String -> Command
 34lineToCmd input = case words input of
 35    ["goto", x] => Goto $ cast x
 36    ["menu"]    => Menu
 37    ["exit"]    => Exit
 38    _ => Unknown
 39
 40readCommand : String -> IO Command
 41readCommand prompt
 42   = do eof <- fEOF stdin
 43        if eof
 44          then pure Exit
 45          else do putStr prompt
 46                  fflush stdout
 47                  x <- getLine
 48                  pure $ lineToCmd x
 49
 50getItem : Context -> Integer -> Maybe Item
 51getItem ctx n = let idx = integerToFin n (length ctx.menu) in
 52    case idx of
 53        Just f  => Just $ index f (fromList ctx.menu)
 54        Nothing => Nothing
 55
 56execTrans : Context -> Item -> IO (Context, String)
 57execTrans ctx (MkItem Document _ s addr) = do
 58    out <- makeReq addr s
 59    pure $ MkPair ctx $ case out of
 60        Right out => out
 61        Left err  => "makeReq failed: " ++ show err
 62execTrans ctx (MkItem Directory _ s addr) = do
 63    out <- makeReq addr s
 64    case out of
 65        Right o => do i <- parseAll o
 66                      pure $ case i of
 67                         Right it => MkPair (newCtx ctx it) (showMenu it)
 68                         Left err => MkPair ctx $ show err
 69        Left err => pure $ MkPair ctx $ "makeReq failed: " ++ show err
 70execTrans ctx _ = do
 71    pure $ MkPair ctx "item type not implemented yet"
 72
 73execGoto : Context -> Integer -> IO (Context, String)
 74execGoto ctx n =
 75    case item of
 76        Just i  => do execTrans ctx i
 77        Nothing => do pure $ (MkPair ctx "unknown menu item")
 78    where
 79        item : Maybe Item
 80        item = getItem ctx n
 81
 82runREPL : Context -> IO ()
 83runREPL ctx = do
 84    cmd <- readCommand prompt
 85    case cmd of
 86        Goto x  => do p <- execGoto ctx x
 87                      putStrLn $ snd p
 88                      runREPL $ fst p
 89        Menu    => do putStrLn $ showMenu ctx.menu
 90                      runREPL ctx
 91        Unknown => do putStrLn "unknown command"
 92                      runREPL ctx
 93        Exit => pure ()
 94
 95    pure ()
 96
 97runClient : Address -> IO ()
 98runClient addr = do
 99    Right out <- makeReq addr ""
100        | Left err => do putStrLn $ "makeReq failed: " ++ show err
101                         exitFailure
102    Right items <- parseAll out
103        | Left err => do putStrLn $ "Parsing failed: " ++ show err
104                         exitFailure
105
106    ctx <- pure $ MkCtx items
107    putStrLn $ showMenu ctx.menu
108
109    runREPL ctx
110
111main : IO ()
112main = do
113    [prog, host, port] <- getArgs
114        | _ => do putStrLn "USAGE: gdris HOST PORT"
115                  exitFailure
116
117    runClient (MkPair host (stringToNatOrZ port))