-- This file is part of the 'term-rewriting' library. It is licensed
-- under an MIT license. See the accompanying 'LICENSE' file for details.
--
-- Authors: Martin Avanzini

{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Data.Rewriting.Substitution.Pretty (
    prettySubst
) where

import Data.Rewriting.Substitution.Type
import Data.Rewriting.Term (prettyTerm)
import qualified Data.Map as M

import Text.PrettyPrint.ANSI.Leijen

prettyGSubst :: (v -> Doc) -> (f -> Doc) -> (v' -> Doc) -> GSubst v f v' -> Doc
prettyGSubst :: forall v f v'.
(v -> Doc) -> (f -> Doc) -> (v' -> Doc) -> GSubst v f v' -> Doc
prettyGSubst v -> Doc
var f -> Doc
fun v' -> Doc
var' GSubst v f v'
subst =
    Doc -> Doc -> Doc -> [Doc] -> Doc
encloseSep Doc
lbrace Doc
rbrace Doc
comma [v -> Term f v' -> Doc
ppBinding v
v Term f v'
t | (v
v,Term f v'
t) <- Map v (Term f v') -> [(v, Term f v')]
forall k a. Map k a -> [(k, a)]
M.toList (Map v (Term f v') -> [(v, Term f v')])
-> Map v (Term f v') -> [(v, Term f v')]
forall a b. (a -> b) -> a -> b
$ GSubst v f v' -> Map v (Term f v')
forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap GSubst v f v'
subst]
    where ppBinding :: v -> Term f v' -> Doc
ppBinding v
v Term f v'
t = v -> Doc
var v
v Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"/" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (f -> Doc) -> (v' -> Doc) -> Term f v' -> Doc
forall f v. (f -> Doc) -> (v -> Doc) -> Term f v -> Doc
prettyTerm f -> Doc
fun v' -> Doc
var' Term f v'
t

prettySubst :: (f -> Doc) -> (v -> Doc) -> Subst f v -> Doc
prettySubst :: forall f v. (f -> Doc) -> (v -> Doc) -> Subst f v -> Doc
prettySubst f -> Doc
fun v -> Doc
var = (v -> Doc) -> (f -> Doc) -> (v -> Doc) -> GSubst v f v -> Doc
forall v f v'.
(v -> Doc) -> (f -> Doc) -> (v' -> Doc) -> GSubst v f v' -> Doc
prettyGSubst v -> Doc
var f -> Doc
fun v -> Doc
var

instance (Pretty v, Pretty f, Pretty v') => Pretty (GSubst v f v') where
    pretty :: GSubst v f v' -> Doc
pretty = (v -> Doc) -> (f -> Doc) -> (v' -> Doc) -> GSubst v f v' -> Doc
forall v f v'.
(v -> Doc) -> (f -> Doc) -> (v' -> Doc) -> GSubst v f v' -> Doc
prettyGSubst v -> Doc
forall a. Pretty a => a -> Doc
pretty f -> Doc
forall a. Pretty a => a -> Doc
pretty v' -> Doc
forall a. Pretty a => a -> Doc
pretty