-----------------------------------------------------------------------------
-- Copyright 2015, 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  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-----------------------------------------------------------------------------
--  $Id: RulePresenter.hs 7524 2015-04-08 07:31:15Z bastiaan $

module Ideas.Encoding.RulePresenter (ruleToHTML) where

import Data.List
import Data.Maybe
import Ideas.Common.Library
import Ideas.Common.Utils (Some(..))
import Ideas.Text.HTML

ruleToHTML :: Some Exercise -> Rule a -> HTMLBuilder
ruleToHTML ex r = mconcat
   [ rewriteRuleToHTML (not $ isBuggy r) ex rr
   | Some rr <- getRewriteRules (transformation r)
   ]

rewriteRuleToHTML :: Bool -> Some Exercise -> RewriteRule a -> HTMLBuilder
rewriteRuleToHTML sound ex r =
   showTerm ex lhs <> spaces 3 <>
   showLeadsTo sound <> spaces 3 <>
   showTerm ex rhs <> br
 where
   lhs :~> rhs = ruleSpecTerm r

showLeadsTo :: Bool -> HTMLBuilder
showLeadsTo sound = string (if sound then "\x21D2" else "\x21CF")

showTerm :: Some Exercise -> Term -> HTMLBuilder
showTerm (Some ex) = string . rec
 where
   rec term =
      case term of
         TVar s    -> s
         TNum i    -> show i
         TFloat a  -> show a
         TMeta n   -> showMeta ex n
         TCon s xs -> concatMap (either id recp) $
                      let txt = spaced (Left (show s) : map Right xs)
                      in fromMaybe txt (specialSymbol s xs)
         TList xs  -> "[" ++ intercalate ", " (map rec xs) ++ "]"

   recp term = parIf (isCon term) (rec term)
   spaced    = intersperse (Left " ")

   isCon (TCon _ xs) = not (null xs)
   isCon _           = False

   parIf b s = if b then "(" ++ s ++ ")" else s

specialSymbol :: Symbol -> [Term] -> Maybe [Either String Term]
-- constants
specialSymbol s []
   | sameSymbol s "logic1.true"     = con "T"
   | sameSymbol s "logic1.false"    = con "F"
   | sameSymbol s "relalg.universe" = con "V" -- universe
   | sameSymbol s "relalg.ident"    = con "I" -- identity
 where
   con x = return [Left x]
-- unary symbols
specialSymbol s [a]
   | sameSymbol s "logic1.not"         = pref "\172" -- "~"
   | sameSymbol s "arith1.unary_minus" = pref "-"
   | sameSymbol s "relalg.not"         = post "\x203E"
   | sameSymbol s "relalg.inv"         = post "~"
 where
   pref x  = return [Left x, Right a]
   post x = return [Right a, Left x]
-- binary symbols
specialSymbol s [a, b]
   | sameSymbol s "logic1.or"         = bin " \8744 " -- "||"
   | sameSymbol s "logic1.and"        = bin " \8743 " -- "&&"
   | sameSymbol s "logic1.implies"    = bin " \8594 " -- "->"
   | sameSymbol s "logic1.equivalent" = bin " \8596 " -- "<->"
   | sameSymbol s "relation1.eq"      = bin " = "
   | sameSymbol s "arith1.plus"       = bin "+"
   | sameSymbol s "arith1.minus"      = bin "-"
   | sameSymbol s "arith1.power"      = bin "^"
   | sameSymbol s "arith1.times"      = bin "\x00B7" -- "*"
   | sameSymbol s "arith1.divide"     = bin "/"
   | sameSymbol s "relalg.conj"       = bin " \x2229 " -- intersect
   | sameSymbol s "relalg.disj"       = bin " \x222A " -- union
   | sameSymbol s "relalg.comp"       = bin " ; " -- composition
   | sameSymbol s "relalg.add"        = bin " \x2020 " -- relative addition/dagger
 where
   bin x = return [Right a, Left x, Right b]

specialSymbol s1 [TCon s2 [x, a]]
   | sameSymbol s1 "calculus1.diff" && sameSymbol s2 "fns1.lambda" =
        return [Left "D(", Right x, Left ") ", Right a]
specialSymbol _ _ = Nothing

sameSymbol :: Symbol -> String -> Bool
sameSymbol = (==) . show

showMeta :: Exercise a -> Int -> String
showMeta ex n
   | listToMaybe (qualifiers ex) == Just "logic" = [ [c] | c <- ['p'..] ] !! n
   | listToMaybe (qualifiers ex) == Just "relationalgebra" = [ [c] | c <- ['r'..] ] !! n
   | otherwise = [ [c] | c <- ['a'..] ] !! n