agda-server-0.1: Memo.hs

-- An interface to construct Memo actions
--    type Memo = StateT MemoState Snap
--    (later: newtype)

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Memo
    ( Memo
    , initMemo
    , loadCmd
    , giveCmd
    , newMemoId     -- for inner use
    , setMainDiv
    , getMainDiv
    , loadAgdaFile
    , writeAgdaFile
    , writeAgdaFileGive

    , ResID
    , AreaID
    , HtmlStr
    , CodePath
    , AgdaCode (unAgdaCode)
    , agdaCodeHtml

    , Html, HTML
    , toHtml
    , textarea', thediv'
    , indent
    , stringToHtml'
    , (+++), br, (<<), rows, cols
    , stringToHtml, (!), thediv, theclass, pre
    , htmlStr
    , input, thetype, size, maxlength, value, anchor, name, href
    , floatRight
    ) where

import Param

import Text.XHtml.Strict

import Snap.Core (Snap)

import AgdaInterface

import Control.Concurrent.MVar
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Trans.State
import Control.Monad.Trans.Reader
import Data.List
--import Data.Maybe
import Data.Monoid
import System.FilePath
import System.Directory

---------------------------------------------------------------

type IState = (ResID, InteractionState)

data SR = SR
    { sr_filePath :: CodePath
    , _sr_is       :: Maybe IState
    }

type MemoState = (MVar [SR], MVar Int)

newtype Memo a
    = Memo (ReaderT MemoState Snap a)
        deriving (Functor, Monad, MonadIO)

initMemo :: Int -> IO (Memo m -> Snap m)
initMemo i = do
    state <- liftM2 (,) (newMVar []) (newMVar i)
    return $ \(Memo m) -> runReaderT m state

newMemoId :: Memo String
newMemoId = Memo $ ReaderT $ \(_,v) -> do
    i <- liftIO $ takeMVar v
    liftIO $ putMVar v $! i + 1
    return $ 'm' : show i


--initState :: FilePath -> 

getState_ :: CodePath -> Memo IState
getState_ fp = Memo $ ReaderT $ \(state, _) -> do
    Just s <- liftIO $ modifyMVar state $ \xs -> return $ do
        case [x | x <- xs, sr_filePath x == fp] of
            [SR _ s@(Just _)] -> (SR fp Nothing : dele fp xs, s)
            [] -> (SR fp Nothing : xs, Just (ResID "", initState)) --Just (stringToHtml "Empty", "", initState))
    return s

saveState_ :: CodePath -> IState -> Memo ()
saveState_ fp s = Memo $ ReaderT $ \(state, _) ->
    liftIO $ modifyMVar_ state $ \xs -> do
        case [x | x <- xs, sr_filePath x == fp] of
            [SR _ Nothing] -> return $ SR fp (Just s) : dele fp xs
--            [] -> return $ SR fp (Just s) : xs


newtype ResID = ResID { unResID :: String }

instance JType ResID

instance IsExp ResID ResID where
    toExp = jconst . unResID


newtype CodePath = CodePath { unCodePath :: String }
    deriving Eq

instance JType CodePath

instance FromString CodePath where fs = CodePath

instance IsExp CodePath CodePath where
    toExp = jconst . unCodePath


setMainDiv :: CodePath -> ResID -> Memo ()
setMainDiv fp s = do
    (_, st) <- getState_ fp
    saveState_ fp (s, st)

getMainDiv :: CodePath -> Memo ResID
getMainDiv fp = do
    (s, st) <- getState_ fp
    saveState_ fp (s, st)
    return s

dele :: CodePath -> [SR] -> [SR]
dele fp = filter ((/=fp) . sr_filePath)

tcmAction :: CodePath -> Interaction -> Memo [Response]
tcmAction filepath action = do
    (md, st) <- getState_ filepath
    (rs, endstate) <- liftIO $ runStateT (tcmAction_ (unCodePath filepath) action) st
    saveState_ filepath (md, {-fromMaybe st-} endstate)
    return rs


loadCmd :: [FilePath] -> CodePath -> Memo [Response]
loadCmd includedirs filepath
    = tcmAction filepath $ Cmd_load (unCodePath filepath) includedirs

giveCmd :: CodePath -> InteractionId -> Range -> AgdaCode -> Memo [Response]
giveCmd filepath ii r c
    = tcmAction filepath $ Cmd_give ii r (unAgdaCode c)

loadAgdaFile
  :: FilePath
  -> FilePath
  -> Memo (AgdaCode, String, CodePath)
loadAgdaFile workdir inp__ = liftIO $ do
    b <- doesFileExist inp
    when (not b) $ writeFile inp $ unwords ["module", inp', "where"] ++ "\n\n\n"
    x <- readFile inp
    return (AgdaCode x, inp', CodePath inp)
  where
    inp = workdir </> inp__ <.> "agda"
    inp' = map repl inp__

    repl '/' = '.'
    repl c = c

writeAgdaFile :: CodePath -> AgdaCode -> Memo ()
writeAgdaFile filepath code
    = liftIO $ writeFile (unCodePath filepath) (unAgdaCode code)

writeAgdaFileGive :: CodePath -> String -> Memo ()
writeAgdaFileGive filepath code
    = liftIO $ do
        x <- readFile (unCodePath filepath)
        length x `seq` return ()
        writeFile (unCodePath filepath) $ repHole code x
  where
    repHole x ('?':c22) = x ++ c22
    repHole x ('{':'!':c2) = x ++ c22
      where
        (_, c22) = split "!}" c2
    repHole x (c:cs) = c: repHole x cs

split :: [Char] -> [Char] -> ([Char], [Char])
split a b = (reverse c, d) where
    (c,d) = split' a b
    split' s s' | isPrefixOf s s' = ("", drop (length s) s')
    split' s (c:cs) = (c:x, y)
      where
        (x,y) = split s cs


---------------

newtype AreaID = AreaID { unAreaID :: String }

instance JType AreaID

instance IsExp AreaID AreaID where
    toExp = jconst . unAreaID


newtype HtmlStr = HtmlStr { unHtmlStr :: String }

instance IsExp HtmlStr HtmlStr where
    toExp = jconst . unHtmlStr

instance JType HtmlStr

instance ToString HtmlStr where ts = unHtmlStr

-----

textarea' :: Int -> Int -> Memo (AreaID, [HtmlAttr] -> Html -> Html)
textarea' c r = do
    i <- newMemoId    
    return (AreaID i, \xs -> textarea ! ([identifier i, cols (show c), rows (show r) ] ++ xs))

floatRight :: HtmlAttr
floatRight = strAttr "style" "float:right"

thediv' :: Memo (ResID, [HtmlAttr] -> Html -> Html)
thediv' = do
    i <- newMemoId    
    return (ResID i, \xs -> thediv ! (identifier i : xs))

htmlStr :: Html -> HtmlStr
htmlStr = HtmlStr . showHtmlFragment

indent :: HTML a => a -> Html
indent x = thediv ! [ theclass "indent" ]  << x

lines' :: String -> [String]
lines' [] = []
lines' ('\n':cs) = []: lines' cs
lines' (c:cs) = add c $ lines' cs
  where
    add x (xs:xss) = (x:xs):xss
    add x [] = [[x]]

stringToHtml' :: String -> Html
stringToHtml' = mconcat . intersperse br . map stringToHtml . lines'


------

newtype AgdaCode = AgdaCode { unAgdaCode :: String }

instance JType AgdaCode

instance FromString AgdaCode where fs = AgdaCode

agdaCodeHtml :: AgdaCode -> Html
agdaCodeHtml = toHtml . unAgdaCode