cgi.idr

module network.cgi

import system

public
Vars : Set
Vars = List (String, String)

data CGIInfo = CGISt Vars -- GET
                     Vars -- POST
                     Vars -- Cookies
                     String -- User agent
                     String -- headers
                     String -- output

get_GET : CGIInfo -> Vars
get_GET (CGISt g _ _ _ _ _) = g

get_POST : CGIInfo -> Vars
get_POST (CGISt _ p _ _ _ _) = p

get_Cookies : CGIInfo -> Vars
get_Cookies (CGISt _ _ c _ _ _) = c

get_UAgent : CGIInfo -> String
get_UAgent (CGISt _ _ _ a _ _) = a

get_Headers : CGIInfo -> String
get_Headers (CGISt _ _ _ _ h _) = h

get_Output : CGIInfo -> String
get_Output (CGISt _ _ _ _ _ o) = o

add_Headers : String -> CGIInfo -> CGIInfo
add_Headers str (CGISt g p c a h o) = CGISt g p c a (h ++ str) o

add_Output : String -> CGIInfo -> CGIInfo
add_Output str (CGISt g p c a h o) = CGISt g p c a h (o ++ str)

abstract
data CGI : Set -> Set where
    MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a

getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)
getAction (MkCGI act) = act

instance Monad CGI where {
    (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s
                                        getAction (k (fst v)) (snd v))

    return v = MkCGI (\s => return (v, s))
}

setInfo : CGIInfo -> CGI ()
setInfo i = MkCGI (\s => return ((), i))

getInfo : CGI CGIInfo
getInfo = MkCGI (\s => return (s, s))

abstract
lift : IO a -> CGI a 
lift op = MkCGI (\st => do { x <- op
                             return (x, st) } ) 

abstract
output : String -> CGI ()
output s = do i <- getInfo
              setInfo (add_Output s i)

abstract
queryVars : CGI Vars
queryVars = do i <- getInfo
               return (get_GET i)

abstract
postVars : CGI Vars
postVars = do i <- getInfo
              return (get_POST i)

abstract
cookieVars : CGI Vars
cookieVars = do i <- getInfo
                return (get_Cookies i)

abstract
queryVar : String -> CGI (Maybe String)
queryVar x = do vs <- queryVars
                return (lookup x vs)

getOutput : CGI String
getOutput = do i <- getInfo
               return (get_Output i)

getHeaders : CGI String
getHeaders = do i <- getInfo
                return (get_Headers i)

abstract
flushHeaders : CGI ()
flushHeaders = do o <- getHeaders
                  lift (putStrLn o)

abstract
flush : CGI ()
flush = do o <- getOutput
           lift (putStr o) 

getVars : List Char -> String -> List (String, String)
getVars seps query = mapMaybe readVar (split (\x => elem x seps) query) 
  where
    readVar : String -> Maybe (String, String)
    readVar xs with (split (\x => x == '=') xs)
        | [k, v] = Just (trim k, trim v)
        | _      = Nothing

getContent : Int -> IO String
getContent x = getC x "" where
    getC : Int -> String -> IO String
    getC 0 acc = return $ rev acc
    getC n acc = do x <- getChar
                    getC (n-1) (strCons x acc)

abstract
runCGI : CGI a -> IO a
runCGI prog = do 
    clen_in <- getEnv "CONTENT_LENGTH"
    let clen = prim__strToInt clen_in
    content <- getContent clen
    query   <- getEnv "QUERY_STRING"
    cookie  <- getEnv "HTTP_COOKIE"
    agent   <- getEnv "HTTP_USER_AGENT"

    let get_vars  = getVars ['&',';'] query
    let post_vars = getVars ['&'] content
    let cookies   = getVars [';'] cookie

    p <- getAction prog (CGISt get_vars post_vars cookies agent 
            "Content-type: text/html\n" 
            "")
    putStrLn (get_Headers (snd p))
    putStr (get_Output (snd p))
    return (fst p)