{- |
Module      :  $Header$
Description :  pretty printing substitutions
Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  ewaryst.schulz@dfki.de
Stability   :  experimental
Portability :  portable

pretty printing substitutions
-}

module HasCASL.PrintSubst where


import HasCASL.Subst

import HasCASL.As
import HasCASL.Le
import HasCASL.PrintAs ()
import HasCASL.SimplifyTerm

import Common.Doc
import Common.DocUtils

import qualified Data.Map as Map

class PrettyInEnv a where
    prettyInEnv :: Env -> a -> Doc

{- instance Pretty a => PrettyInEnv a where
prettyInEnv _ x  = pretty x -}


instance Pretty SubstConst where
    pretty (SConst i _) = pretty i

instance Pretty a => Pretty (SRule a) where
    pretty (Blocked x) = mapsto <+> pretty x <+> parens (text "BLOCKED")
    pretty (Ready x) = mapsto <+> pretty x

instance Pretty Subst where
    pretty (Subst (a, b, _)) =
        text "Subs"
                 <> vcat [ text "titution"
                         , prettyRuleMap "Terms" a, prettyRuleMap "Types" b]

prettyRuleMap :: (Pretty key, Pretty val)
                 => String -> Map.Map key (SRule val) -> Doc
prettyRuleMap t m | Map.null m = empty
                  | otherwise =
                      vcat $ (if null t then [] else
                                  [ text t <+> colon
                                  , text $ map (const '-') [0 .. length t + 1]])
                               ++ map prettyRule (Map.toList m)

prettyRule :: (Pretty key, Pretty val) => (key, SRule val) -> Doc
prettyRule (k, v) = pretty k <+> pretty v


instance PrettyInEnv Term where
    prettyInEnv e t = pretty $ simplifyTerm e t

instance PrettyInEnv Type where
    prettyInEnv = const pretty

instance PrettyInEnv a => PrettyInEnv (SRule a) where
    prettyInEnv e (Blocked x) = mapsto <+> prettyInEnv e x <+> parens (text "BLOCKED")
    prettyInEnv e (Ready x) = mapsto <+> prettyInEnv e x

instance PrettyInEnv Subst where
    prettyInEnv e (Subst (a, b, _)) =
        text "Subs"
                 <> vcat [ text "titution"
                         , prettyInEnvRuleMap e "Terms" a
                         , prettyInEnvRuleMap e "Types" b]

prettyInEnvRuleMap :: (Pretty key, PrettyInEnv val)
                 => Env -> String -> Map.Map key (SRule val) -> Doc
prettyInEnvRuleMap e t m
    | Map.null m = empty
    | otherwise =
        vcat
        $ (if null t then [] else
               [ text t <+> colon
               , text $ map (const '-') [0 .. length t + 1]])
            ++ map (prettyInEnvRule e) (Map.toList m)

prettyInEnvRule :: (Pretty key, PrettyInEnv val) => Env -> (key, SRule val) -> Doc
prettyInEnvRule e (k, v) = pretty k <+> prettyInEnv e v


prettyTermMapping :: Env -> [(Term, Term)] -> Doc
prettyTermMapping e l = vcat $ map f l where
    f (t1, t2) = prettyInEnv e t1 <+> text "=" <+> prettyInEnv e t2
