{- |

Module : ./HasCASL/PrintSubst.hs

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