agda-server-0.1: Html.hs

-- An interface to construct Html data
--    (later: dedicated data type)

{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternGuards #-}

module Html
    ( code'
    , showR
    ) where

import Memo
import JS

import Agda.Interaction.Response
import Agda.Interaction.Highlighting.Precise
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Common
import Agda.Utils.Pretty (Doc, render, pretty)

import System.FilePath ((<.>))
import Data.List
import Data.Monoid
import Data.Function
import qualified Data.Map as Map

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

-- | Constructs the HTML displaying the code.

code'
    :: (AreaID -> ResID -> Stmt ())
    -> AgdaCode         -- ^ The contents of the module.
    -> CompressedFile -- ^ Highlighting information.
    -> Memo Html
code' giveCode (unAgdaCode -> contents) info
    = fmap mconcat
    . mapM (\cs -> case cs of
              (mi, (pos, _)) : _ -> annotate pos (maybe mempty id mi) (map (snd . snd) cs)
              []                 -> error "__IMPOSSIBLE__"
          )
    . groupBy ((==) `on` fst)
    . map (\(pos, c) -> (Map.lookup pos infoMap, (pos, c)))
    . zip [1..]
    $ contents
  where
    infoMap = toMap (decompress info)

    getHole "?" = Just ""
    getHole ('{':'!':cs)
        | ('}':'!':cs') <- reverse cs
        = Just $ reverse cs'
    getHole _ = Nothing

    annotate :: Integer -> MetaInfo -> String -> Memo Html
    annotate pos mi s
        | Just h <- getHole s -- = stringToHtml "HOLE"
        = do
            (i2, thediv_) <- thediv'
            (i1, tar) <- textarea' 30 1
            return $
                thediv_ [] <<
                    [ tar [] << h
                    , br
                    , button' "Give" (giveCode i1 i2)
                    ]
{-
                ! [ theclass "interpreter"
                  , thetype "text"
                  , size $ show $ 3 + length h -- limit
                  , maxlength 1000
            --          , identifier $ "tarea" ++ i
                  , value h -- $ if prompt == 'R' then "" else exp
                  ]
-}
    annotate pos mi s
        = return $ anchor ! attributes << stringToHtml s
      where
        attributes
          = [name (show pos)]
          ++ maybe [] link (definitionSite mi)
          ++ (case classes of
            [] -> []
            cs -> [theclass $ unwords cs])

        classes
          =  maybe [] noteClasses (note mi)
          ++ otherAspectClasses (otherAspects mi)
          ++ maybe [] aspectClasses (aspect mi)

        aspectClasses (Name mKind op) = kindClass ++ opClass
          where
            kindClass = maybe [] ((: []) . showKind) mKind

            showKind (Constructor Inductive)   = "InductiveConstructor"
            showKind (Constructor CoInductive) = "CoinductiveConstructor"
            showKind k                         = show k

            opClass = if op then ["Operator"] else []
        aspectClasses a = [show a]

        otherAspectClasses = map show

        -- Notes are not included.
        noteClasses s = []

        link (m, pos) = [href $ modToFile m ++ "#" ++ show pos]
          where
            modToFile :: C.TopLevelModuleName -> FilePath
            modToFile m = render (pretty m) <.> "xml"


---------------------------------------------------------------
{-
instance IsString Html where
    fromString = toHtml :: String -> Html
-}
showR :: Response -> Maybe Html
showR (Resp_Status s) = Just $ ("checked: " :: String) +++ show (sChecked s)
showR (Resp_DisplayInfo x) = Just $ showD x --a ++ " :displayinfo: " ++ b
showR (Resp_RunningInfo i x) = Just $ "runninginfo: " +++ show i +++ x
showR Resp_ClearRunningInfo = Just $ toHtml "clearRunningInfo"
--showR (Resp_HighlightingInfo h) = "highlightingInfo: " ++ show h
--showR (Resp_UpdateHighlighting (a,b)) = "highlighting: " ++ show (a,b)
showR (Resp_JumpToError f i) = Just $ "jumpToError" +++ f +++ show i
showR (Resp_InteractionPoints is) = Just $ "ipoints: " +++ show is
showR (Resp_GiveAction i s) = Just $ "give: " +++ show i +++ showG s
showR (Resp_MakeCaseAction ss) = Just $ "caseaction: " +++  ss
showR (Resp_MakeCase s ss) = Just $ "case: " +++ s +++  ss
showR (Resp_SolveAll x) = Just $ "solveAll: " +++ show x
showR _ = Nothing

instance HTML Doc where
    toHtml = toHtml . render

showG :: GiveResult -> Html
showG (Give_String s) = toHtml s
showG Give_Paren = toHtml "give paren"
showG Give_NoParen = toHtml "give no paren"

showD :: DisplayInfo -> Html
showD x = case x of
   Info_CompilationOk -> toHtml "compilation ok"
   Info_Constraints s -> "constraints:" +++ s
   Info_AllGoals s -> "all goals:" +++ s
   Info_Error s -> "error:" +++ s
   Info_Intro d -> "intro:" +++ d
   Info_Auto s -> "auto:" +++ s
   Info_ModuleContents d -> "module contents:" +++ d
   Info_NormalForm d -> "normal form:" +++ d
   Info_GoalType d -> "goal type:" +++ d
   Info_CurrentGoal d -> "current goal:" +++ d
   Info_InferredType d -> "inferred type:" +++ d
   Info_Context d -> "context:" +++ d