{-# LANGUAGE GADTs #-}
module Ideas.Encoding.EncoderXML
( XMLEncoder
, xmlEncoder, encodeState
) where
import Data.Char
import Data.List
import Data.Maybe
import Data.Monoid
import Ideas.Common.Library hiding (exerciseId)
import Ideas.Encoding.Encoder
import Ideas.Encoding.OpenMathSupport
import Ideas.Encoding.Request hiding (XML)
import Ideas.Encoding.RulesInfo (rulesInfoXML)
import Ideas.Encoding.StrategyInfo
import Ideas.Service.Diagnose
import Ideas.Service.FeedbackScript.Syntax
import Ideas.Service.State
import Ideas.Service.Types
import Ideas.Text.OpenMath.Object
import Ideas.Text.XML
import Ideas.Utils.Prelude (munless)
import qualified Ideas.Service.FeedbackText as FeedbackText
import qualified Ideas.Service.ProblemDecomposition as PD
type XMLEncoder a = EncoderX a XMLBuilder
xmlEncoder :: TypedEncoder a XMLBuilder
xmlEncoder =
(encodeDiagnosis, tDiagnosis) <?>
(encodeDecompositionReply, PD.tReply) <?>
(encodeDerivation, tDerivation (tPair tRule tEnvironment) tContext) <?>
(encodeDerivationText, tDerivation tString tContext) <?>
(encodeDifficulty, tDifficulty) <?>
(encodeMessage, FeedbackText.tMessage) <?>
\(val ::: tp) ->
case tp of
Tag "RuleShortInfo" t ->
case equal t (Const Rule) of
Just f -> ruleShortInfo (f val)
Nothing -> fail "rule short info"
Tag "RulesInfo" _ -> do
ex <- getExercise
useOM <- useOpenMath <$> getRequest
return (rulesInfoXML ex (buildExpression useOM ex))
Tag "elem" t ->
tag "elem" (xmlEncoder (val ::: t))
List (Const Rule) ->
encodeAsList [ ruleShortInfo r | r <- val ]
List t ->
encodeAsList [ xmlEncoder (a ::: t) | a <- val ]
Tag _ t -> xmlEncoder (val ::: t)
Iso iso t -> xmlEncoder (to iso val ::: t)
Pair t1 t2 -> xmlEncoder (fst val ::: t1) <>
xmlEncoder (snd val ::: t2)
t1 :|: t2 -> case val of
Left a -> xmlEncoder (a ::: t1)
Right b -> xmlEncoder (b ::: t2)
Unit -> mempty
Const t -> xmlEncoderConst (val ::: t)
_ -> fail $ show tp
xmlEncoderConst :: TypedValue (Const a) -> XMLEncoder a
xmlEncoderConst tv@(val ::: tp) =
case tp of
SomeExercise -> case val of
Some a -> exerciseInfo a
Strategy -> builder (strategyToXML val)
Rule -> "ruleid" .=. show val
Constraint -> "constraint" .=. show val
State -> encodeState val
Context -> encodeContext val
Location -> encodeLocation val
Environment -> encodeEnvironment val
Term -> builderXML (toOMOBJ val)
Text -> encodeText val
Bool -> string (showBool val)
XML -> builder val
_ -> text tv
encodeState :: State a -> XMLEncoder a
encodeState st = element "state"
[ if withoutPrefix st
then mempty
else element "prefix" [string (show (statePrefix st))]
, encodeContext (stateContext st)
]
encodeContext :: Context a -> XMLEncoder a
encodeContext ctx = do
ex <- getExercise
useOM <- useOpenMath <$> getRequest
maybe (error "encodeContext") (buildExpression useOM ex) (fromContext ctx)
<>
let values = bindings (withLoc ctx)
loc = fromLocation (location ctx)
withLoc
| null loc = id
| otherwise = insertRef (makeRef "location") loc
in munless (null values) $ element "context"
[ element "item"
[ "name" .=. showId tb
, case getTermValue tb of
term | useOM ->
builder (omobj2xml (toOMOBJ term))
_ -> "value" .=. showValue tb
]
| tb <- values
]
buildExpression :: BuildXML b => Bool -> Exercise a -> a -> b
buildExpression useOM ex
| useOM = either msg builderXML . toOpenMath ex
| otherwise = tag "expr" . string . prettyPrinter ex
where
msg s = error ("Error encoding term in OpenMath: " ++ s)
encodeLocation :: Location -> XMLEncoder a
encodeLocation loc = "location" .=. show loc
encodeEnvironment :: HasEnvironment env => env -> XMLEncoder a
encodeEnvironment env = mconcat [ encodeTypedBinding b | b <- bindings env ]
encodeTypedBinding :: Binding -> XMLEncoder a
encodeTypedBinding tb = do
useOM <- useOpenMath <$> getRequest
tag "argument" $
("description" .=. showId tb) <>
case getTermValue tb of
term | useOM -> builder $
omobj2xml $ toOMOBJ term
_ -> string (showValue tb)
encodeDerivation :: Derivation (Rule (Context a), Environment) (Context a) -> XMLEncoder a
encodeDerivation d =
let xs = [ (s, a) | (_, s, a) <- triples d ]
in xmlEncoder (xs ::: tList (tPair (tPair tRule tEnvironment) tContext))
encodeDerivationText :: Derivation String (Context a) -> XMLEncoder a
encodeDerivationText d = encodeAsList
[ ("ruletext" .=. s) <> encodeContext a
| (_, s, a) <- triples d
]
ruleShortInfo :: Rule (Context a) -> XMLEncoder a
ruleShortInfo r = mconcat
[ "name" .=. showId r
, "buggy" .=. showBool (isBuggy r)
, "arguments" .=. show (length (getRefs r))
, "rewriterule" .=. showBool (isRewriteRule r)
]
encodeDifficulty :: Difficulty -> XMLEncoder a
encodeDifficulty d =
"difficulty" .=. show d
encodeText :: Text -> XMLEncoder a
encodeText txt = do
ex <- getExercise
useOM <- useOpenMath <$> getRequest
mconcat (intersperse (string " ") [ encodeItem ex useOM item | item <- textItems txt ])
where
encodeItem ex useOM item =
case item of
TextTerm a -> fromMaybe (text item) $ do
v <- hasTermView ex
b <- match v a
return (buildExpression useOM ex b)
_ -> text item
encodeMessage :: FeedbackText.Message -> XMLEncoder a
encodeMessage msg =
element "message"
[ case FeedbackText.accept msg of
Just b -> "accept" .=. showBool b
Nothing -> mempty
, encodeText (FeedbackText.text msg)
]
encodeDiagnosis :: Diagnosis a -> XMLEncoder a
encodeDiagnosis diagnosis =
case diagnosis of
SyntaxError s -> element "syntaxerror" [string s]
Buggy env r -> element "buggy"
[encodeEnvironment env, "ruleid" .=. showId r]
NotEquivalent s ->
if null s then emptyTag "notequiv"
else element "notequiv" [ "reason" .=. s ]
Similar b st -> element "similar"
["ready" .=. showBool b, encodeState st]
WrongRule b st mr -> element "wrongrule" $
[ "ready" .=. showBool b, encodeState st ] ++
maybe [] (\r -> ["ruleid" .=. showId r]) mr
Expected b st r -> element "expected"
["ready" .=. showBool b, encodeState st, "ruleid" .=. showId r]
Detour b st env r -> element "detour"
[ "ready" .=. showBool b, encodeState st
, encodeEnvironment env, "ruleid" .=. showId r
]
Correct b st -> element "correct"
["ready" .=. showBool b, encodeState st]
Unknown b st -> element "unknown"
["ready" .=. showBool b, encodeState st]
encodeDecompositionReply :: PD.Reply a -> XMLEncoder a
encodeDecompositionReply reply =
case reply of
PD.Ok loc st ->
element "correct" [encLoc loc, encodeState st]
PD.Incorrect eq loc st env ->
element "incorrect"
[ "equivalent" .=. showBool eq
, encLoc loc
, encodeState st
, encodeEnvironment env
]
where
encLoc = tag "location" . text
exerciseInfo :: Exercise b -> XMLEncoder a
exerciseInfo ex = mconcat
[ "exerciseid" .=. showId ex
, "description" .=. description ex
, "status" .=. show (status ex)
]
encodeAsList :: [XMLEncoder a] -> XMLEncoder a
encodeAsList = element "list" . map (tag "elem")
showBool :: Bool -> String
showBool = map toLower . show