<commit_before>{-# LANGUAGE GADTs #-}
-----------------------------------------------------------------------------
-- Copyright 2011, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  <EMAIL>
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- Encoding in HTML
--
-----------------------------------------------------------------------------
module Ideas.Service.EncoderHTML (htmlEncoder) where

import Ideas.Common.Utils
import Control.Monad
import Data.Char
import Data.List
import Data.Maybe
import Data.Ord
import Ideas.Common.Library hiding (ready)
import Ideas.Text.XML
import Ideas.Text.HTML
import Ideas.Service.RulePresenter
import Ideas.Service.Diagnose
import Ideas.Service.DomainReasoner
import Ideas.Service.Evaluator
import Ideas.Service.LinkManager
import Ideas.Service.State
import Ideas.Service.Types
import Ideas.Service.BasicServices
import Ideas.Service.StrategyInfo
import Ideas.Common.Strategy.Prefix
import Ideas.Text.OpenMath.Object
import Ideas.Text.OpenMath.FMP
import Ideas.Service.RulesInfo

htmlEncoder :: LinkManager -> DomainReasoner -> Exercise a -> TypedValue (Type a) -> HTML
htmlEncoder lm dr ex tv = 
   htmlPage "EncoderHTML" (Just (resource "ideas.css")) $ mconcat
      [ divClass "header" $ mconcat
           [ divClass  "ideas-logo" $ image $ resource "ideas.png"
           , divClass  "ounl-logo"  $ image $ resource "ounl.png"
           , spanClass "menuitem"   $ linkToIndex lm $ string "Index"
           , spanClass "menuitem"   $ linkToExercises lm $ string "Exercises"
           , spanClass "menuitem"   $ linkToServices lm $ string "Services"
           ]
      , divClass "content" $
           case runEncoderState (encodeType lm ex) () tv of
              Left err -> string err
              Right ok -> ok
      , divClass "footer" $
           string (fullVersion dr)
      ]
 where
   resource = urlForResource lm

type HTMLEncoder t = EncoderState () t HTMLBuilder

encodeType :: LinkManager -> Exercise a -> HTMLEncoder (TypedValue (Type a))
encodeType lm ex = msum
   [ encodeTyped encodeIndex
   , encodeTyped (exerciseHeader lm // ex <> htmlDiagnosis lm)
   , encodeTyped (exerciseHeader lm // ex <> encodeExampleList lm ex)
   , encodeTyped (exerciseHeader lm // ex <> htmlAllFirsts lm)
   , encodeTyped (exerciseHeader lm // ex <> htmlAllApplications lm)
   , encodeTyped (exerciseHeader lm // ex <> encodeDerivation lm ex)
   , encodeTyped (exerciseHeader lm // ex <> encodeDerivationList lm ex)
   , encoderFor $ \(val ::: tp) -> 
        case tp of 
           Iso iso t  -> encodeType lm ex // (to iso val ::: t)           
           Tag _ t    -> encodeType lm ex // (val ::: t)
           Pair t1 t2 -> encodeType lm ex // (fst val ::: t1) <>
                         encodeType lm ex // (snd val ::: t2)
           t1 :|: t2  -> case val of
                            Left x  -> encodeType lm ex // (x ::: t1)
                            Right x -> encodeType lm ex // (x ::: t2)
           List (Const Service) -> encodeServiceList lm // val
           List (Const SomeExercise) -> encodeExerciseList lm // val
           List (Const Rule) -> (exerciseHeader lm // ex) <> encodeRuleList lm ex // val
           List t ->
              ul <$> sequence [ encodeType lm ex // (x ::: t) | x <- val ]
           Const t -> encodeConst lm ex // (val ::: t)
           _ -> return $ string $ "unknown: " ++ show tp
   ]

encodeConst :: LinkManager -> Exercise a -> HTMLEncoder (TypedValue (Const a))
encodeConst lm ex = encoderFor $ \tv@(val ::: tp) ->
   case tp of 
      Service     -> encodeService // val
      Exercise    -> (exerciseHeader lm // ex) <> encodeExercise lm // val
      Strategy    -> (exerciseHeader lm // ex) <> encodeStrategy ex // val
      Rule        -> encodeRule ex // val
      State       -> (exerciseHeader lm // ex) <> (encodeState lm // val)
      Location    -> return $ text val
      Environment -> return $ text val
      Context     -> return $ string $ prettyPrinterContext ex val
      String      -> return $ string val
      _           -> return $ text tv

encodeIndex :: HTMLEncoder DomainReasoner
encodeIndex = simpleEncoder $ \dr -> mconcat
   [ h1 $ "Domain reasoner " ++ showId dr
   , htmlDescription dr
   , keyValueTable
        [ ("version", string $ fullVersion dr)
        , ("exercises", text $ length $ exercises dr)
        , ("services", text $ length $ services dr)
        ]
   , munless (null $ aliases dr) $ 
        h2 "Exercise aliases" <>
        table True (
           [ string "alias", string "exercise"] :
           [ [string (showId a), string (showId b)]
           | (a, b) <- aliases dr
           ])
   , munless (null $ scripts dr) 
        h2 "Feedback scripts" <>
        table True (
           [ string "exercise", string "script"] :
           [ [string (showId a), string file]
           | (a, file) <- scripts dr
           ])
   ]
   
encodeServiceList :: LinkManager -> HTMLEncoder [Service]
encodeServiceList lm = simpleEncoder $ \srvs ->
   h1 "Services" <>
   mconcat
      [ h2 (show i ++ ". " ++ s) <> table False (map make xs)
      | (i, s, xs) <- groupById srvs
      ]  
 where
   make s = [ linkToService lm s (string (showId s)) <>
              mwhen (serviceDeprecated s) (italic (string " (deprecated)"))
            , string (description s)
            ]

encodeExerciseList :: LinkManager -> HTMLEncoder [Some Exercise]
encodeExerciseList lm = simpleEncoder $ \exs ->
   h1 "Exercises" <>
   mconcat
      [ h2 (show i ++ ". " ++ dom) <> table False (map make xs)
      | (i, dom, xs) <- groupsWith f exs
      ]  
 where
   f :: Some Exercise -> String
   f (Some ex) = fromMaybe "" (listToMaybe (qualifiers (getId ex)))
 
   make :: Some Exercise -> [HTMLBuilder]
   make (Some ex) = 
      [ linkToExercise lm ex $ string $ showId ex
      , string $ map toLower $ show $ status ex
      , string $ description ex
      ]

groupById :: HasId a => [a] -> [(Int, String, [a])]
groupById = groupsWith (fromMaybe "" . listToMaybe . qualifiers . getId)

groupsWith :: (a -> String) -> [a] -> [(Int, String, [a])]
groupsWith = orderedGroupsWith id 

orderedGroupsWith :: Ord b => (b -> String) -> (a -> b) -> [a] -> [(Int, String, [a])]
orderedGroupsWith showf get = 
   zipWith f [1..] . groupBy eq . sortBy (comparing get)
 where
   eq x y = get x == get y
   f i xs = (i, showf (get (head xs)), xs)

encodeService :: HTMLEncoder Service
encodeService = simpleEncoder $ \srv -> mconcat
   [ h1 $ "Service " ++ showId srv
   , mwhen (serviceDeprecated srv) $ 
        para $ spanClass "warning" $ string "Warning: this service is deprecated"
   , htmlDescription srv
   , case serviceFunction srv of
        _ ::: tp ->
           let (xs, ys) = inputOutputTypes tp
               f :: Some (Type a) -> HTMLBuilder
               f (Some (t :|: Unit)) = text t <> italic (string " (optional)")
               f (Some t) = text t
           in  
              munless (null xs) (para $ 
                 bold (string "Input") <> ul (map f xs))
              <>
              munless (null ys) (para $
                 bold (string "Output") <> ul (map f ys))    
   ]

inputOutputTypes :: Type a t -> ([Some (Type a)], [Some (Type a)])
inputOutputTypes tp =
   case tp of
      Iso _ t   -> inputOutputTypes t
      t1 :-> t2 -> let (xs, ys) = inputOutputTypes t2 
                   in (productType t1 ++ xs, ys)
      Const String :|: t -> ([], productType t)
      _         -> ([], productType tp)

productType :: Type a t -> [Some (Type a)]
productType tp = 
   case tp of
      Iso _ t    -> productType t
      Pair t1 t2 -> productType t1 ++ productType t2
      Unit       -> []
      _          -> [Some tp]

encodeExercise :: LinkManager -> HTMLEncoder (Exercise a)
encodeExercise lm = simpleEncoder $ \ex -> mconcat
   [ generalInfo ex
   , h2 "Example exercises"
   , ul $ [ para $ linkToExamples lm ex $ string "list of examples"
          | not (null (examples ex))
          ] ++
          [ para $ mconcat $
               string "generate exercise: " :
               intersperse (string ", ")
                  [ linkToRandomExample lm ex d $ text d
                  | d <- [VeryEasy .. VeryDifficult]
                  ]
          | isJust (randomExercise ex)
          ] ++
          [ para $ submitStateInfo lm ex
          | not (isStatic lm)
          ]
   ]
 where
   generalInfo ex = keyValueTable
      [ ("Code",   ttText (showId ex))
      , ("Status", text $ status ex)
      , ("Strategy", linkToStrategy lm ex $ string (showId $ strategy ex))
      , ("Rules", text nrOfSoundRules)
      , ("Buggy rules", text nrOfBuggyRules)
      , ("OpenMath support", bool $ isJust $ hasTermView ex)
      , ("Restartable strategy", bool $ canBeRestarted ex)
      , ("Exercise generator", bool $ isJust $ randomExercise ex)
      , ("Examples", text $ length $ examples ex)
      ]
    where
      (nrOfBuggyRules, nrOfSoundRules) = 
         mapBoth length (partition isBuggy (ruleset ex))

exerciseHeader :: LinkManager -> HTMLEncoder (Exercise a)
exerciseHeader lm = simpleEncoder $ \ex -> mconcat
   [ exerciseMenu lm ex
   , h1 $ "Exercise " ++ showId ex
   , htmlDescription ex
   ]

keyValueTable :: [(String, HTMLBuilder)] -> HTMLBuilder
keyValueTable = 
   let f (s, a) = [bold (string s), a]
   in para . table False . map f 

exerciseMenu :: LinkManager -> Exercise a -> HTMLBuilder
exerciseMenu lm ex = divClass "menubox" $
   bold (string "Exercise") <>
   ul [ linkToExercise lm ex    $ string "information"
      , linkToStrategy lm ex    $ string "strategy"
      , linkToRules lm ex       $ string "rules"
      , linkToExamples lm ex    $ string "examples"
      , linkToDerivations lm ex $ string "derivations"
      ]

encodeStrategy :: Exercise a -> HTMLEncoder (Strategy (Context a))
encodeStrategy ex = simpleEncoder $ \s -> mconcat
   [ h2 "Strategy"
   , highlightXML True (strategyToXML s)
   , h2 "Locations"
   , let f :: HasId a => ([Int], a) -> [HTMLBuilder]
         f (loc, a) = [text loc, indent (length loc) <> string (showId a)]
         indent n = string (replicate (3*n) '.')
     in table True
           ( [string "Location", string "Label"]
           : map f (strategyLocations (strategy ex))
           )
   ]

bool :: Bool -> HTMLBuilder
bool b = string (if b then "yes" else "no")

encodeRuleList :: LinkManager -> Exercise a -> HTMLEncoder [Rule (Context a)]
encodeRuleList lm ex = simpleEncoder $ \rs ->
   let (rs1, rs2) = partition isBuggy rs
   in mconcat 
         [ h2 $ "Rules for " ++ showId ex
         , table True (header:map f rs2)
         , h2 $ "Buggy rules for " ++ showId ex
         , table True (header:map f rs1)
         ]
 where
   header = [ string "Rule name", string "Args"
            , string "Used", string "Rewrite rule"
            ]
   used = rulesInStrategy (strategy ex)
   f r  = [ linkToRule lm ex r $ ttText (showId r)
          , text $ length $ getRefs r
          , bool $ r `elem` used
          , mwhen (isRewriteRule r) $
               ruleToHTML (Some ex) r
          ]

encodeRule :: Exercise a -> HTMLEncoder (Rule (Context a))
encodeRule ex = simpleEncoder $ \r -> mconcat
   [ h1 $ "Rule " ++ showId r
   , htmlDescription r
   , let commas  = string . intercalate ", "
         idList  = commas . map showId
         refList = commas . map show . getRefIds
     in para $ keyValueTable
           [ ("Parameters", refList r)
           , ("Buggy", bool (isBuggy r))
           , ("Rewrite rule", bool (isRewriteRule r))
           , ("Siblings", idList $ ruleSiblings r)
           ]
   , mwhen (isRewriteRule r) $
        h2 "Rewrite rule" <> ruleToHTML (Some ex) r
   -- FMPS
   , let xs = getRewriteRules (transformation r)
     in munless (null xs) $ mconcat $
           h2 "Formal Mathematical Properties" :
           [ para $
              let fmp = rewriteRuleToFMP (not $ isBuggy r) rr
              in highlightXML False $ makeXML "FMP" $
                    builder $ omobj2xml $ toObject fmp
           | Some rr <- xs
           ]
   ]
   
encodeExampleList :: LinkManager -> Exercise a -> HTMLEncoder [(Difficulty, Context a)]
encodeExampleList lm ex = simpleEncoder $ \pairs -> mconcat $
   h2 "Examples" :
   [ h3 (s ++ " (" ++ show (length xs) ++ ")")
       <> (if isStatic lm then ul else mconcat) (map make xs)
   | (_, s, xs) <- orderedGroupsWith show fst pairs
   ]  
 where
   make (_, x) = para $
      munless (isStatic lm) $
         let st = emptyStateContext ex x
         in spanClass "statelink" $ linkToState lm st $ 
               element "img" ["src" .=. "external.png", "width" .=. "15"]
      <> string (prettyPrinterContext ex x) 

encodeDerivation :: LinkManager -> Exercise a -> HTMLEncoder (Derivation (Rule (Context a), Environment) (Context a))
encodeDerivation lm ex =
   return (h2 "Derivation") 
   <> htmlDerivation lm ex

encodeDerivationList :: LinkManager -> Exercise a -> HTMLEncoder ([Derivation (Rule (Context a), Environment) (Context a)])
encodeDerivationList lm ex = encoderFor $ \ds ->  
   return (h2 "Derivations") 
   <> mconcat 
      [ return (h3 $ show i ++ ".") <> htmlDerivation lm ex // d
      | (i, d) <- zip [1::Int ..] ds
      ]
      
htmlDerivation :: LinkManager -> Exercise a -> HTMLEncoder (Derivation (Rule (Context a), Environment) (Context a))
htmlDerivation lm ex = encoderFor $ \d ->
   arr derivationDiffEnv 
   >>> htmlDerivationWith (before d) forStep forTerm
 where
   before d = do
      stateLink lm (emptyStateContext ex (firstTerm d))
   forStep ((r, env1), env2) = 
      let showEnv e = munless (noBindings e) $ string $ ", " ++ show e in
      spanClass "derivation-step" $ mconcat
         [ unescaped "&#8658; "
         , string $ unqualified r
         , showEnv env1 -- local environment
         , showEnv env2 -- global environment (diff)
         ]
   forTerm a = do 
      divClass "term" $ string $ prettyPrinterContext ex a

htmlState :: LinkManager -> HTMLEncoder (State a)
htmlState lm = simpleEncoder $ \state ->
   para $ divClass "state" $
      stateLink lm state
      <> divClass "term" (string $ prettyPrinterContext (exercise state) (stateContext state))
      <> string "ready: " <> bool (ready state)

stateLink :: LinkManager -> State a -> HTMLBuilder
stateLink lm st = munless (isStatic lm) $
   spanClass "derivation-statelink" $ linkToState lm st $ 
      element "img"<commit_msg>making non-finished derivations better visible in HTML mode; slight improvement in logic proof strategy using oncetd for sort rules <commit_after>{-# LANGUAGE GADTs #-}
-----------------------------------------------------------------------------
-- Copyright 2011, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  <EMAIL>
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- Encoding in HTML
--
-----------------------------------------------------------------------------
module Ideas.Service.EncoderHTML (htmlEncoder) where

import Ideas.Common.Utils
import Control.Monad
import Data.Char
import Data.List
import Data.Maybe
import Data.Ord
import Ideas.Common.Library hiding (ready)
import Ideas.Text.XML
import Ideas.Text.HTML
import Ideas.Service.RulePresenter
import Ideas.Service.Diagnose
import Ideas.Service.DomainReasoner
import Ideas.Service.Evaluator
import Ideas.Service.LinkManager
import Ideas.Service.State
import Ideas.Service.Types
import Ideas.Service.BasicServices
import Ideas.Service.StrategyInfo
import Ideas.Common.Strategy.Prefix
import Ideas.Text.OpenMath.Object
import Ideas.Text.OpenMath.FMP
import Ideas.Service.RulesInfo

htmlEncoder :: LinkManager -> DomainReasoner -> Exercise a -> TypedValue (Type a) -> HTML
htmlEncoder lm dr ex tv = 
   htmlPage "EncoderHTML" (Just (resource "ideas.css")) $ mconcat
      [ divClass "header" $ mconcat
           [ divClass  "ideas-logo" $ image $ resource "ideas.png"
           , divClass  "ounl-logo"  $ image $ resource "ounl.png"
           , spanClass "menuitem"   $ linkToIndex lm $ string "Index"
           , spanClass "menuitem"   $ linkToExercises lm $ string "Exercises"
           , spanClass "menuitem"   $ linkToServices lm $ string "Services"
           ]
      , divClass "content" $
           case runEncoderState (encodeType lm ex) () tv of
              Left err -> string err
              Right ok -> ok
      , divClass "footer" $
           string (fullVersion dr)
      ]
 where
   resource = urlForResource lm

type HTMLEncoder t = EncoderState () t HTMLBuilder

encodeType :: LinkManager -> Exercise a -> HTMLEncoder (TypedValue (Type a))
encodeType lm ex = msum
   [ encodeTyped encodeIndex
   , encodeTyped (exerciseHeader lm // ex <> htmlDiagnosis lm)
   , encodeTyped (exerciseHeader lm // ex <> encodeExampleList lm ex)
   , encodeTyped (exerciseHeader lm // ex <> htmlAllFirsts lm)
   , encodeTyped (exerciseHeader lm // ex <> htmlAllApplications lm)
   , encodeTyped (exerciseHeader lm // ex <> encodeDerivation lm ex)
   , encodeTyped (exerciseHeader lm // ex <> encodeDerivationList lm ex)
   , encoderFor $ \(val ::: tp) -> 
        case tp of 
           Iso iso t  -> encodeType lm ex // (to iso val ::: t)           
           Tag _ t    -> encodeType lm ex // (val ::: t)
           Pair t1 t2 -> encodeType lm ex // (fst val ::: t1) <>
                         encodeType lm ex // (snd val ::: t2)
           t1 :|: t2  -> case val of
                            Left x  -> encodeType lm ex // (x ::: t1)
                            Right x -> encodeType lm ex // (x ::: t2)
           List (Const Service) -> encodeServiceList lm // val
           List (Const SomeExercise) -> encodeExerciseList lm // val
           List (Const Rule) -> (exerciseHeader lm // ex) <> encodeRuleList lm ex // val
           List t ->
              ul <$> sequence [ encodeType lm ex // (x ::: t) | x <- val ]
           Const t -> encodeConst lm ex // (val ::: t)
           _ -> return $ string $ "unknown: " ++ show tp
   ]

encodeConst :: LinkManager -> Exercise a -> HTMLEncoder (TypedValue (Const a))
encodeConst lm ex = encoderFor $ \tv@(val ::: tp) ->
   case tp of 
      Service     -> encodeService // val
      Exercise    -> (exerciseHeader lm // ex) <> encodeExercise lm // val
      Strategy    -> (exerciseHeader lm // ex) <> encodeStrategy ex // val
      Rule        -> encodeRule ex // val
      State       -> (exerciseHeader lm // ex) <> (encodeState lm // val)
      Location    -> return $ text val
      Environment -> return $ text val
      Context     -> return $ string $ prettyPrinterContext ex val
      String      -> return $ string val
      _           -> return $ text tv

encodeIndex :: HTMLEncoder DomainReasoner
encodeIndex = simpleEncoder $ \dr -> mconcat
   [ h1 $ "Domain reasoner " ++ showId dr
   , htmlDescription dr
   , keyValueTable
        [ ("version", string $ fullVersion dr)
        , ("exercises", text $ length $ exercises dr)
        , ("services", text $ length $ services dr)
        ]
   , munless (null $ aliases dr) $ 
        h2 "Exercise aliases" <>
        table True (
           [ string "alias", string "exercise"] :
           [ [string (showId a), string (showId b)]
           | (a, b) <- aliases dr
           ])
   , munless (null $ scripts dr) 
        h2 "Feedback scripts" <>
        table True (
           [ string "exercise", string "script"] :
           [ [string (showId a), string file]
           | (a, file) <- scripts dr
           ])
   ]
   
encodeServiceList :: LinkManager -> HTMLEncoder [Service]
encodeServiceList lm = simpleEncoder $ \srvs ->
   h1 "Services" <>
   mconcat
      [ h2 (show i ++ ". " ++ s) <> table False (map make xs)
      | (i, s, xs) <- groupById srvs
      ]  
 where
   make s = [ linkToService lm s (string (showId s)) <>
              mwhen (serviceDeprecated s) (italic (string " (deprecated)"))
            , string (description s)
            ]

encodeExerciseList :: LinkManager -> HTMLEncoder [Some Exercise]
encodeExerciseList lm = simpleEncoder $ \exs ->
   h1 "Exercises" <>
   mconcat
      [ h2 (show i ++ ". " ++ dom) <> table False (map make xs)
      | (i, dom, xs) <- groupsWith f exs
      ]  
 where
   f :: Some Exercise -> String
   f (Some ex) = fromMaybe "" (listToMaybe (qualifiers (getId ex)))
 
   make :: Some Exercise -> [HTMLBuilder]
   make (Some ex) = 
      [ linkToExercise lm ex $ string $ showId ex
      , string $ map toLower $ show $ status ex
      , string $ description ex
      ]

groupById :: HasId a => [a] -> [(Int, String, [a])]
groupById = groupsWith (fromMaybe "" . listToMaybe . qualifiers . getId)

groupsWith :: (a -> String) -> [a] -> [(Int, String, [a])]
groupsWith = orderedGroupsWith id 

orderedGroupsWith :: Ord b => (b -> String) -> (a -> b) -> [a] -> [(Int, String, [a])]
orderedGroupsWith showf get = 
   zipWith f [1..] . groupBy eq . sortBy (comparing get)
 where
   eq x y = get x == get y
   f i xs = (i, showf (get (head xs)), xs)

encodeService :: HTMLEncoder Service
encodeService = simpleEncoder $ \srv -> mconcat
   [ h1 $ "Service " ++ showId srv
   , mwhen (serviceDeprecated srv) $ 
        para $ spanClass "warning" $ string "Warning: this service is deprecated"
   , htmlDescription srv
   , case serviceFunction srv of
        _ ::: tp ->
           let (xs, ys) = inputOutputTypes tp
               f :: Some (Type a) -> HTMLBuilder
               f (Some (t :|: Unit)) = text t <> italic (string " (optional)")
               f (Some t) = text t
           in  
              munless (null xs) (para $ 
                 bold (string "Input") <> ul (map f xs))
              <>
              munless (null ys) (para $
                 bold (string "Output") <> ul (map f ys))    
   ]

inputOutputTypes :: Type a t -> ([Some (Type a)], [Some (Type a)])
inputOutputTypes tp =
   case tp of
      Iso _ t   -> inputOutputTypes t
      t1 :-> t2 -> let (xs, ys) = inputOutputTypes t2 
                   in (productType t1 ++ xs, ys)
      Const String :|: t -> ([], productType t)
      _         -> ([], productType tp)

productType :: Type a t -> [Some (Type a)]
productType tp = 
   case tp of
      Iso _ t    -> productType t
      Pair t1 t2 -> productType t1 ++ productType t2
      Unit       -> []
      _          -> [Some tp]

encodeExercise :: LinkManager -> HTMLEncoder (Exercise a)
encodeExercise lm = simpleEncoder $ \ex -> mconcat
   [ generalInfo ex
   , h2 "Example exercises"
   , ul $ [ para $ linkToExamples lm ex $ string "list of examples"
          | not (null (examples ex))
          ] ++
          [ para $ mconcat $
               string "generate exercise: " :
               intersperse (string ", ")
                  [ linkToRandomExample lm ex d $ text d
                  | d <- [VeryEasy .. VeryDifficult]
                  ]
          | isJust (randomExercise ex)
          ] ++
          [ para $ submitStateInfo lm ex
          | not (isStatic lm)
          ]
   ]
 where
   generalInfo ex = keyValueTable
      [ ("Code",   ttText (showId ex))
      , ("Status", text $ status ex)
      , ("Strategy", linkToStrategy lm ex $ string (showId $ strategy ex))
      , ("Rules", text nrOfSoundRules)
      , ("Buggy rules", text nrOfBuggyRules)
      , ("OpenMath support", bool $ isJust $ hasTermView ex)
      , ("Restartable strategy", bool $ canBeRestarted ex)
      , ("Exercise generator", bool $ isJust $ randomExercise ex)
      , ("Examples", text $ length $ examples ex)
      ]
    where
      (nrOfBuggyRules, nrOfSoundRules) = 
         mapBoth length (partition isBuggy (ruleset ex))

exerciseHeader :: LinkManager -> HTMLEncoder (Exercise a)
exerciseHeader lm = simpleEncoder $ \ex -> mconcat
   [ exerciseMenu lm ex
   , h1 $ "Exercise " ++ showId ex
   , htmlDescription ex
   ]

keyValueTable :: [(String, HTMLBuilder)] -> HTMLBuilder
keyValueTable = 
   let f (s, a) = [bold (string s), a]
   in para . table False . map f 

exerciseMenu :: LinkManager -> Exercise a -> HTMLBuilder
exerciseMenu lm ex = divClass "menubox" $
   bold (string "Exercise") <>
   ul [ linkToExercise lm ex    $ string "information"
      , linkToStrategy lm ex    $ string "strategy"
      , linkToRules lm ex       $ string "rules"
      , linkToExamples lm ex    $ string "examples"
      , linkToDerivations lm ex $ string "derivations"
      ]

encodeStrategy :: Exercise a -> HTMLEncoder (Strategy (Context a))
encodeStrategy ex = simpleEncoder $ \s -> mconcat
   [ h2 "Strategy"
   , highlightXML True (strategyToXML s)
   , h2 "Locations"
   , let f :: HasId a => ([Int], a) -> [HTMLBuilder]
         f (loc, a) = [text loc, indent (length loc) <> string (showId a)]
         indent n = string (replicate (3*n) '.')
     in table True
           ( [string "Location", string "Label"]
           : map f (strategyLocations (strategy ex))
           )
   ]

bool :: Bool -> HTMLBuilder
bool b = string (if b then "yes" else "no")

encodeRuleList :: LinkManager -> Exercise a -> HTMLEncoder [Rule (Context a)]
encodeRuleList lm ex = simpleEncoder $ \rs ->
   let (rs1, rs2) = partition isBuggy rs
   in mconcat 
         [ h2 $ "Rules for " ++ showId ex
         , table True (header:map f rs2)
         , h2 $ "Buggy rules for " ++ showId ex
         , table True (header:map f rs1)
         ]
 where
   header = [ string "Rule name", string "Args"
            , string "Used", string "Rewrite rule"
            ]
   used = rulesInStrategy (strategy ex)
   f r  = [ linkToRule lm ex r $ ttText (showId r)
          , text $ length $ getRefs r
          , bool $ r `elem` used
          , mwhen (isRewriteRule r) $
               ruleToHTML (Some ex) r
          ]

encodeRule :: Exercise a -> HTMLEncoder (Rule (Context a))
encodeRule ex = simpleEncoder $ \r -> mconcat
   [ h1 $ "Rule " ++ showId r
   , htmlDescription r
   , let commas  = string . intercalate ", "
         idList  = commas . map showId
         refList = commas . map show . getRefIds
     in para $ keyValueTable
           [ ("Parameters", refList r)
           , ("Buggy", bool (isBuggy r))
           , ("Rewrite rule", bool (isRewriteRule r))
           , ("Siblings", idList $ ruleSiblings r)
           ]
   , mwhen (isRewriteRule r) $
        h2 "Rewrite rule" <> ruleToHTML (Some ex) r
   -- FMPS
   , let xs = getRewriteRules (transformation r)
     in munless (null xs) $ mconcat $
           h2 "Formal Mathematical Properties" :
           [ para $
              let fmp = rewriteRuleToFMP (not $ isBuggy r) rr
              in highlightXML False $ makeXML "FMP" $
                    builder $ omobj2xml $ toObject fmp
           | Some rr <- xs
           ]
   ]
   
encodeExampleList :: LinkManager -> Exercise a -> HTMLEncoder [(Difficulty, Context a)]
encodeExampleList lm ex = simpleEncoder $ \pairs -> mconcat $
   h2 "Examples" :
   [ h3 (s ++ " (" ++ show (length xs) ++ ")")
       <> (if isStatic lm then ul else mconcat) (map make xs)
   | (_, s, xs) <- orderedGroupsWith show fst pairs
   ]  
 where
   make (_, x) = para $
      munless (isStatic lm) $
         let st = emptyStateContext ex x
         in spanClass "statelink" $ linkToState lm st $ 
               element "img" ["src" .=. "external.png", "width" .=. "15"]
      <> string (prettyPrinterContext ex x) 

encodeDerivation :: LinkManager -> Exercise a -> HTMLEncoder (Derivation (Rule (Context a), Environment) (Context a))
encodeDerivation lm ex =
   return (h2 "Derivation") 
   <> htmlDerivation lm ex

encodeDerivationList :: LinkManager -> Exercise a -> HTMLEncoder ([Derivation (Rule (Context a), Environment) (Context a)])
encodeDerivationList lm ex = encoderFor $ \ds ->  
   return (h2 "Derivations") 
   <> mconcat 
      [ return (h3 $ show i ++ ".") <> htmlDerivation lm ex // d
      | (i, d) <- zip [1::Int ..] ds
      ]
      
htmlDerivation :: LinkManager -> Exercise a -> HTMLEncoder (Derivation (Rule (Context a), Environment) (Context a))
htmlDerivation lm ex = encoderFor $ \d ->
   arr derivationDiffEnv 
   >>> htmlDerivationWith (before d) forStep forTerm
 where
   before d =
      stateLink lm (emptyStateContext ex (firstTerm d))
      <> case fmap (isReady ex) (fromContext (lastTerm d)) of
            Just True -> mempty
            _ -> spanClass "error" (string "Final term is not finished")
   forStep ((r, env1), env2) = 
      let showEnv e = munless (noBindings e) $ string $ ", " ++ show e in
      spanClass "derivation-step" $ mconcat
         [ unescaped "&#8658; "
         , string $ showId r
         , showEnv env1 -- local environment
         , showEnv env2 -- global environment (diff)
         ]
   forTerm a = do 
      divClass "term" $ string $ prettyPrinterContext ex a

htmlState :: LinkManager -> HTMLEncoder (State a)
htmlState lm = simpleEncoder $ \state ->
   para $ divClass "state" $
      stateLink lm state
      <> divClass "term" (string $ prettyPrinterContext (exercise state) (stateContext state))
      <> string "ready: " <> bool (ready state)

stateLink :: LinkManager -> State a -> HTMLBuilder
stateLink lm st = munless (isStatic lm) $
   spanClass "derivation-statelink" $ linkToState lm st $ 
      element "img"
{'fraction_non_alphanumeric': 0.1315096251266464, 'fraction_numerical': 0.004052684903748734, 'mean_word_length': 2.0893062076160667, 'pattern_counts': {'":': 0, '<': 92, '<?xml version=': 0, '>': 278, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 2}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3930348', 'n_tokens_mistral': 9182, 'n_tokens_neox': 8789, 'n_words': 2944}