-- | Pretty printer for theorems.
--   It provides functions to transform theorems into documents.
--
--   See the module \"Text.PrettyPrint\" for more details about the used
--   document type.

module Language.Haskell.FreeTheorems.PrettyTheorems (
    PrettyTheoremOption (..)
  , prettyTheorem
  , prettyRelationVariable
  , prettyUnfoldedLift
  , prettyUnfoldedClass
) where

import Prelude hiding ((<>))

import Data.List (partition, find)
import Data.Maybe (mapMaybe)
import Text.PrettyPrint

import Language.Haskell.FreeTheorems.Syntax
import Language.Haskell.FreeTheorems.LanguageSubsets
import Language.Haskell.FreeTheorems.Theorems
import Language.Haskell.FreeTheorems.PrettyBase
import Language.Haskell.FreeTheorems.PrettyTypes



------- Options ---------------------------------------------------------------


-- | Possible options for pretty-printing theorems.

data PrettyTheoremOption
  = OmitTypeInstantiations      
        -- ^ Omits all instantiations of types. This option makes theorems 
        --   usually better readable.
  
  | OmitLanguageSubsets
        -- ^ Omit mentioning language subsets explicitly for certain relations.

  deriving PrettyTheoremOption -> PrettyTheoremOption -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrettyTheoremOption -> PrettyTheoremOption -> Bool
$c/= :: PrettyTheoremOption -> PrettyTheoremOption -> Bool
== :: PrettyTheoremOption -> PrettyTheoremOption -> Bool
$c== :: PrettyTheoremOption -> PrettyTheoremOption -> Bool
Eq



------- Pretty control data ---------------------------------------------------


data PrettyControl = PrettyControl
  { PrettyControl -> [PrettyTheoremOption]
options     :: [PrettyTheoremOption]
  , PrettyControl -> Parens
parentheses :: Parens
  , PrettyControl -> Bool
inPremise   :: Bool
  }


defaultPrettyControl :: [PrettyTheoremOption] -> PrettyControl
defaultPrettyControl :: [PrettyTheoremOption] -> PrettyControl
defaultPrettyControl [PrettyTheoremOption]
opts = 
  PrettyControl
    { options :: [PrettyTheoremOption]
options = [PrettyTheoremOption]
opts
    , parentheses :: Parens
parentheses = Parens
NoParens
    , inPremise :: Bool
inPremise = Bool
False
    }


withTypeInstantiations :: PrettyControl -> Bool
withTypeInstantiations :: PrettyControl -> Bool
withTypeInstantiations = forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem PrettyTheoremOption
OmitTypeInstantiations forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrettyControl -> [PrettyTheoremOption]
options


withLanguageSubsets :: PrettyControl -> Bool
withLanguageSubsets :: PrettyControl -> Bool
withLanguageSubsets = forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem PrettyTheoremOption
OmitLanguageSubsets forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrettyControl -> [PrettyTheoremOption]
options


noParens :: PrettyControl -> PrettyControl
noParens :: PrettyControl -> PrettyControl
noParens PrettyControl
pc = PrettyControl
pc { parentheses :: Parens
parentheses = Parens
NoParens }


useParens :: PrettyControl -> PrettyControl
useParens :: PrettyControl -> PrettyControl
useParens PrettyControl
pc = PrettyControl
pc { parentheses :: Parens
parentheses = Parens
ParensFun }


withParens :: PrettyControl -> Bool
withParens :: PrettyControl -> Bool
withParens PrettyControl
pc = PrettyControl -> Parens
parentheses PrettyControl
pc forall a. Ord a => a -> a -> Bool
> Parens
NoParens


setPremise :: PrettyControl -> PrettyControl
setPremise :: PrettyControl -> PrettyControl
setPremise PrettyControl
pc = PrettyControl
pc { inPremise :: Bool
inPremise = Bool -> Bool
not (PrettyControl -> Bool
inPremise PrettyControl
pc) }





------- Language subsets ------------------------------------------------------


-- | Pretty-prints a language subset.

prettyLanguageSubset :: LanguageSubset -> Doc
prettyLanguageSubset :: LanguageSubset -> Doc
prettyLanguageSubset LanguageSubset
l = case LanguageSubset
l of
  LanguageSubset
BasicSubset                       -> String -> Doc
text String
"basic"
  SubsetWithFix TheoremType
EquationalTheorem   -> String -> Doc
text String
"fix" Doc -> Doc -> Doc
<> Doc
comma Doc -> Doc -> Doc
<> String -> Doc
text String
"="
  SubsetWithFix TheoremType
InequationalTheorem -> String -> Doc
text String
"fix" Doc -> Doc -> Doc
<> Doc
comma Doc -> Doc -> Doc
<> String -> Doc
text String
"[="
  SubsetWithSeq TheoremType
EquationalTheorem   -> String -> Doc
text String
"seq" Doc -> Doc -> Doc
<> Doc
comma Doc -> Doc -> Doc
<> String -> Doc
text String
"="
  SubsetWithSeq TheoremType
InequationalTheorem -> String -> Doc
text String
"seq" Doc -> Doc -> Doc
<> Doc
comma Doc -> Doc -> Doc
<> String -> Doc
text String
"[="





------- Formulas --------------------------------------------------------------


-- | Pretty-prints a theorem.

prettyTheorem :: [PrettyTheoremOption] -> Theorem -> Doc
prettyTheorem :: [PrettyTheoremOption] -> Theorem -> Doc
prettyTheorem [PrettyTheoremOption]
opt = PrettyControl -> Theorem -> Doc
prettyFormula ([PrettyTheoremOption] -> PrettyControl
defaultPrettyControl [PrettyTheoremOption]
opt)



-- | Pretty-prints a formula.

prettyFormula :: PrettyControl -> Formula -> Doc
prettyFormula :: PrettyControl -> Theorem -> Doc
prettyFormula PrettyControl
pc (ForallRelations RelationVariable
v (TypeExpression
t1,TypeExpression
t2) [Restriction]
res Theorem
f) =
  let rv :: Doc
rv = RelationVariable -> Doc
prettyRelationVariable RelationVariable
v
      ts :: Doc
ts = Parens -> TypeExpression -> Doc
prettyTypeExpression Parens
NoParens TypeExpression
t1 Doc -> Doc -> Doc
<> Doc
comma 
           Doc -> Doc -> Doc
<> Parens -> TypeExpression -> Doc
prettyTypeExpression Parens
NoParens TypeExpression
t2
      cs :: [TypeClass]
cs = [Restriction] -> [TypeClass]
getTypeClasses [Restriction]
res
      ds :: Doc
ds = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
cs
             then Doc
empty
             else Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map TypeClass -> Doc
prettyTypeClass forall a b. (a -> b) -> a -> b
$ [TypeClass]
cs
   in Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$ 
        [Doc] -> Doc
sep 
          [ [Doc] -> Doc
fsep forall a b. (a -> b) -> a -> b
$
              [ String -> Doc
text String
"forall"
              , Doc
ts, String -> Doc
text String
"in", String -> Doc
text String
"TYPES" Doc -> Doc -> Doc
<> Doc
ds Doc -> Doc -> Doc
<> Doc
comma
              , Doc
rv, String -> Doc
text String
"in"
              , String -> Doc
text String
"REL" Doc -> Doc -> Doc
<> Doc -> Doc
parens Doc
ts
                 Doc -> Doc -> Doc
<> if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Restriction]
res then Char -> Doc
char Char
'.' else Doc
comma ]
              forall a. [a] -> [a] -> [a]
++ Doc -> [Restriction] -> [Doc]
prettyRestrictionList Doc
rv [Restriction]
res
          , Int -> Doc -> Doc
nest Int
1 (PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Theorem
f) ]

prettyFormula PrettyControl
pc (ForallFunctions Either TermVariable TermVariable
v (TypeExpression
t1,TypeExpression
t2) [Restriction]
res Theorem
f) =
  let ts :: Doc
ts = Parens -> TypeExpression -> Doc
prettyTypeExpression Parens
NoParens TypeExpression
t1 Doc -> Doc -> Doc
<> Doc
comma 
           Doc -> Doc -> Doc
<> Parens -> TypeExpression -> Doc
prettyTypeExpression Parens
NoParens TypeExpression
t2
      pv :: Doc
pv = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TermVariable -> Doc
prettyTermVariable TermVariable -> Doc
prettyTermVariable Either TermVariable TermVariable
v
      cs :: [TypeClass]
cs = [Restriction] -> [TypeClass]
getTypeClasses [Restriction]
res
      ds :: Doc
ds = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
cs
             then Doc
empty
             else Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map TypeClass -> Doc
prettyTypeClass forall a b. (a -> b) -> a -> b
$ [TypeClass]
cs
   in Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$ 
        [Doc] -> Doc
sep 
          [ [Doc] -> Doc
fsep forall a b. (a -> b) -> a -> b
$
              [ String -> Doc
text String
"forall"
              , Doc
ts, String -> Doc
text String
"in", String -> Doc
text String
"TYPES" Doc -> Doc -> Doc
<> Doc
ds Doc -> Doc -> Doc
<> Doc
comma 
              , Doc
pv, String -> Doc
text String
"::"
              , Parens -> TypeExpression -> Doc
prettyTypeExpression Parens
NoParens 
                (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\TermVariable
_ -> TypeExpression -> TypeExpression -> TypeExpression
TypeFun TypeExpression
t1 TypeExpression
t2) (\TermVariable
_ -> TypeExpression -> TypeExpression -> TypeExpression
TypeFun TypeExpression
t2 TypeExpression
t1) Either TermVariable TermVariable
v)
                 Doc -> Doc -> Doc
<> if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Restriction]
res then Char -> Doc
char Char
'.' else Doc
comma ]
              forall a. [a] -> [a] -> [a]
++ Doc -> [Restriction] -> [Doc]
prettyRestrictionList Doc
pv [Restriction]
res
          , Int -> Doc -> Doc
nest Int
1 (PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Theorem
f) ]

prettyFormula PrettyControl
pc (ForallPairs (TermVariable
v1,TermVariable
v2) Relation
r Theorem
f) =
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
sep [ [Doc] -> Doc
fsep [ String -> Doc
text String
"forall"
               , Doc -> Doc
parens (TermVariable -> Doc
prettyTermVariable TermVariable
v1 Doc -> Doc -> Doc
<> Doc
comma 
                         Doc -> Doc -> Doc
<+> TermVariable -> Doc
prettyTermVariable TermVariable
v2)
               , String -> Doc
text String
"in", PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Bool
False Relation
r Doc -> Doc -> Doc
<> Char -> Doc
char Char
'.' ]
        , Int -> Doc -> Doc
nest Int
1 (PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Theorem
f) ]

prettyFormula PrettyControl
pc (ForallVariables TermVariable
v TypeExpression
t Theorem
f) =
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
sep [ [Doc] -> Doc
fsep [ String -> Doc
text String
"forall", TermVariable -> Doc
prettyTermVariable TermVariable
v, String -> Doc
text String
"::"
               , Parens -> TypeExpression -> Doc
prettyTypeExpression Parens
NoParens TypeExpression
t Doc -> Doc -> Doc
<> Char -> Doc
char Char
'.' ]
        , Int -> Doc -> Doc
nest Int
1 (PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Theorem
f) ]

prettyFormula PrettyControl
pc (Equivalence Theorem
f1 Theorem
f2) =
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
sep [ PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Theorem
f1
        , String -> Doc
text String
"<=>" Doc -> Doc -> Doc
<+> PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Theorem
f2]

prettyFormula PrettyControl
pc (Implication Theorem
f1 Theorem
f2) =
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
sep [ PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
useParens (PrettyControl -> PrettyControl
setPremise PrettyControl
pc)) Theorem
f1
        , String -> Doc
text String
"==>" Doc -> Doc -> Doc
<+> PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Theorem
f2]

prettyFormula PrettyControl
pc (Conjunction Theorem
f1 Theorem
f2) =
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
sep [ PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Theorem
f1
        , String -> Doc
text String
"&&" Doc -> Doc -> Doc
<+> PrettyControl -> Theorem -> Doc
prettyFormula (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Theorem
f2]

prettyFormula PrettyControl
pc (Predicate Predicate
predicate) = 
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) (PrettyControl -> Predicate -> Doc
prettyPredicate (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Predicate
predicate)



-- | Returns the type classes of a restriction list.

getTypeClasses :: [Restriction] -> [TypeClass]
getTypeClasses :: [Restriction] -> [TypeClass]
getTypeClasses = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Restriction -> [TypeClass]
exTC
  where exTC :: Restriction -> [TypeClass]
exTC Restriction
r = case Restriction
r of
          RespectsClasses [TypeClass]
tcs -> [TypeClass]
tcs
          Restriction
otherwise           -> []



-- | Pretty-prints a list of restrictions.

prettyRestrictionList :: Doc -> [Restriction] -> [Doc]
prettyRestrictionList :: Doc -> [Restriction] -> [Doc]
prettyRestrictionList Doc
v [Restriction]
res = case [Restriction]
res of
  []         -> []
  (Restriction
r:[])     -> Doc
v forall a. a -> [a] -> [a]
: [ Restriction -> Doc
prettyRestriction Restriction
r Doc -> Doc -> Doc
<> Char -> Doc
char Char
'.' ]
  (Restriction
r1:Restriction
r2:[]) -> Doc
v forall a. a -> [a] -> [a]
: (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Restriction -> Doc
prettyRestriction Restriction
r1] forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"and", Restriction -> Doc
prettyRestriction Restriction
r2 Doc -> Doc -> Doc
<> Char -> Doc
char Char
'.' ])
  [Restriction]
otherwise  -> let dres :: [Doc]
dres = forall a b. (a -> b) -> [a] -> [b]
map Restriction -> Doc
prettyRestriction [Restriction]
res
                 in Doc
v forall a. a -> [a] -> [a]
: (Doc -> [Doc] -> [Doc]
punctuate Doc
comma (forall a. [a] -> [a]
init [Doc]
dres forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"and"]) 
                        forall a. [a] -> [a] -> [a]
++ [forall a. [a] -> a
last [Doc]
dres Doc -> Doc -> Doc
<> Char -> Doc
char Char
'.' ])



-- | Pretty-prints a restriction.

prettyRestriction :: Restriction -> Doc
prettyRestriction :: Restriction -> Doc
prettyRestriction Restriction
Strict           = String -> Doc
text String
"strict"
prettyRestriction Restriction
Continuous       = String -> Doc
text String
"continuous"
prettyRestriction Restriction
Total            = String -> Doc
text String
"total"
prettyRestriction Restriction
BottomReflecting = String -> Doc
text String
"bottom-reflecting"
prettyRestriction Restriction
LeftClosed       = String -> Doc
text String
"left-closed"
prettyRestriction (RespectsClasses [TypeClass]
tcs) =
  Bool -> Doc -> Doc
when (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
tcs)) forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
fsep [ String -> Doc
text String
"respects"
         , Bool -> Doc -> Doc
parensIf (forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeClass]
tcs forall a. Ord a => a -> a -> Bool
> Int
1) forall a b. (a -> b) -> a -> b
$
             [Doc] -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map TypeClass -> Doc
prettyTypeClass forall a b. (a -> b) -> a -> b
$ [TypeClass]
tcs ]



-- | Pretty-prints a predicate.

prettyPredicate :: PrettyControl -> Predicate -> Doc
prettyPredicate :: PrettyControl -> Predicate -> Doc
prettyPredicate PrettyControl
pc (IsMember Term
x Term
y Relation
r) =
  [Doc] -> Doc
fsep [ Doc -> Doc
parens (PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
x Doc -> Doc -> Doc
<> Doc
comma 
                 Doc -> Doc -> Doc
<+> PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
y)
       , String -> Doc
text String
"in", PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Bool
False Relation
r ]

prettyPredicate PrettyControl
pc (IsEqual Term
x Term
y) = 
  [Doc] -> Doc
fsep [ PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
x, Char -> Doc
char Char
'=', PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
y ]

prettyPredicate PrettyControl
pc (IsLessEq Term
x Term
y) = 
  [Doc] -> Doc
fsep [ PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
x, String -> Doc
text String
"[=", PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
y ]

prettyPredicate PrettyControl
pc (IsNotBot Term
x) = 
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
    [Doc] -> Doc
fsep [ PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
x, String -> Doc
text String
"/=", String -> Doc
text String
"_|_" ]

prettyPredicate PrettyControl
pc (Predicate
IsTrue) = 
  String -> Doc
text String
"True"



-- | Pretty-prints a term.

prettyTerm :: PrettyControl -> Term -> Doc
prettyTerm :: PrettyControl -> Term -> Doc
prettyTerm PrettyControl
pc (TermVar TermVariable
v) = TermVariable -> Doc
prettyTermVariable TermVariable
v

prettyTerm PrettyControl
pc (TermApp Term
t1 Term
t2) = 
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$ PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
t1 Doc -> Doc -> Doc
<+> PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Term
t2

prettyTerm PrettyControl
pc (TermIns Term
t TypeExpression
ty) =
  let d :: Doc
d = Parens -> TypeExpression -> Doc
prettyTypeExpression Parens
NoParens TypeExpression
ty
      withTypes :: Bool
withTypes = PrettyControl -> Bool
withTypeInstantiations PrettyControl
pc
      p :: PrettyControl -> PrettyControl
p = if Bool
withTypes then PrettyControl -> PrettyControl
useParens else PrettyControl -> PrettyControl
noParens
      pt :: Doc
pt = PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Term
t 
   in Doc
pt Doc -> Doc -> Doc
<> Bool -> Doc -> Doc
showInstantiation Bool
withTypes Doc
d

prettyTerm PrettyControl
pc (TermComp []) = 
  String -> Doc
text String
"id"

prettyTerm PrettyControl
pc (TermComp [Term
t]) = 
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$ PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
t

prettyTerm PrettyControl
pc (TermComp (Term
t:[Term]
ts)) = 
  Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$ PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
t Doc -> Doc -> Doc
<+> String -> Doc
text String
"." Doc -> Doc -> Doc
<+>
                             PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) ([Term] -> Term
TermComp [Term]
ts)



-- | Shows an instantiation (by a type).

showInstantiation :: Bool -> Doc -> Doc
showInstantiation :: Bool -> Doc -> Doc
showInstantiation Bool
False Doc
_ = Doc
empty
showInstantiation Bool
True  Doc
d = Char -> Doc
char Char
'_' Doc -> Doc -> Doc
<> Doc -> Doc
braces Doc
d


-- | Pretty-prints a term variable.

prettyTermVariable :: TermVariable -> Doc
prettyTermVariable :: TermVariable -> Doc
prettyTermVariable (TVar String
v) = String -> Doc
text String
v



------- Relations -------------------------------------------------------------


-- | Pretty-prints a relation.

prettyRelation :: PrettyControl -> Bool -> Relation -> Doc
prettyRelation :: PrettyControl -> Bool -> Relation -> Doc
prettyRelation PrettyControl
_ Bool
_ (RelVar RelationInfo
_ RelationVariable
rv) = RelationVariable -> Doc
prettyRelationVariable RelationVariable
rv

prettyRelation PrettyControl
pc Bool
_ (FunVar RelationInfo
ri (Left Term
t)) = 
  case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of 
    TheoremType
EquationalTheorem   -> PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Term
t
    TheoremType
InequationalTheorem -> PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Term
t Doc -> Doc -> Doc
<> String -> Doc
text String
" ; [="

prettyRelation PrettyControl
pc Bool
_ (FunVar RelationInfo
_ (Right Term
t)) = 
  String -> Doc
text String
"[= ; " Doc -> Doc -> Doc
<> PrettyControl -> Term -> Doc
prettyTerm (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Term
t Doc -> Doc -> Doc
<> String -> Doc
text String
"^{-1}"

prettyRelation PrettyControl
_ Bool
_ (RelBasic RelationInfo
ri) = 
  case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
    TheoremType
EquationalTheorem   -> String -> Doc
text String
"id"
    TheoremType
InequationalTheorem -> String -> Doc
text String
"[="

prettyRelation PrettyControl
pc Bool
omitOrder (RelLift RelationInfo
ri TypeConstructor
con [Relation]
rs) =
  let pl :: Doc
pl = case RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri of
             LanguageSubset
BasicSubset -> String -> Doc
text String
"lift"
             LanguageSubset
otherwise   -> case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
                              TheoremType
EquationalTheorem   -> String -> Doc
text String
"lift"
                              TheoremType
InequationalTheorem -> if Bool
omitOrder
                                                       then String -> Doc
text String
"lift"
                                                       else String -> Doc
text String
"[= ; lift"
   in Doc
pl Doc -> Doc -> Doc
<> Doc -> Doc
braces (TypeConstructor -> Doc
prettyTypeConstructor TypeConstructor
con)
         Doc -> Doc -> Doc
<> (Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (\Doc
a Doc
b -> Doc
a Doc -> Doc -> Doc
<> Doc
comma Doc -> Doc -> Doc
<> Doc
b)  
                    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Bool
False) forall a b. (a -> b) -> a -> b
$ [Relation]
rs)
--         <> (parens . fsep . punctuate comma 
--                           . map (prettyRelation (noParens pc) False) $ rs)


prettyRelation PrettyControl
pc Bool
_ (RelFun RelationInfo
ri Relation
r1 Relation
r2) = 
  let l :: Doc
l = if PrettyControl -> Bool
withLanguageSubsets PrettyControl
pc
            then case RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri of
                   SubsetWithSeq TheoremType
_ -> String -> Doc
text String
"^" Doc -> Doc -> Doc
<> Doc -> Doc
braces (LanguageSubset -> Doc
prettyLanguageSubset 
                                                  (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri))
                   LanguageSubset
otherwise       -> Doc
empty
            else Doc
empty
   in Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
        [Doc] -> Doc
fsep [ PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Bool
False Relation
r1
             , String -> Doc
text String
"->" Doc -> Doc -> Doc
<> Doc
l
             , PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Bool
False Relation
r2 ]

-- second function relation only used in the equational setting with Seq
prettyRelation PrettyControl
pc Bool
_ (RelFunLab RelationInfo
ri Relation
r1 Relation
r2) = 
   Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
      [Doc] -> Doc
fsep [ PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Bool
False Relation
r1
           , String -> Doc
text String
"->^o" Doc -> Doc -> Doc
<> Doc
empty
           , PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Bool
False Relation
r2 ]

prettyRelation PrettyControl
pc Bool
_ (RelAbs RelationInfo
ri RelationVariable
v (TypeExpression, TypeExpression)
_ [Restriction]
res Relation
r) = 
  let tcs :: [TypeClass]
tcs = [Restriction] -> [TypeClass]
getTypeClasses [Restriction]
res
      dcs :: Doc
dcs = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
tcs
              then Doc
empty
              else Doc -> Doc
parens ([Doc] -> Doc
fcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map TypeClass -> Doc
prettyTypeClass forall a b. (a -> b) -> a -> b
$ [TypeClass]
tcs)
   in Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
        [Doc] -> Doc
fsep [ String -> Doc
text String
"forall"
             , RelationVariable -> Doc
prettyRelationVariable RelationVariable
v
             , String -> Doc
text String
"in"
             , String -> Doc
text String
"REL" 
                Doc -> Doc -> Doc
<> (Bool -> Doc -> Doc
when (PrettyControl -> Bool
withLanguageSubsets PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
                     String -> Doc
text String
"^" Doc -> Doc -> Doc
<> Doc -> Doc
braces (LanguageSubset -> Doc
prettyLanguageSubset 
                                          (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri)))
                Doc -> Doc -> Doc
<> Doc
dcs
                Doc -> Doc -> Doc
<> Char -> Doc
char Char
'.'
             , PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Bool
False Relation
r ]

prettyRelation PrettyControl
pc Bool
_ (FunAbs RelationInfo
ri Either TermVariable TermVariable
v (TypeExpression, TypeExpression)
_ [Restriction]
res Relation
r) =
  let tcs :: [TypeClass]
tcs = [Restriction] -> [TypeClass]
getTypeClasses [Restriction]
res
      dcs :: Doc
dcs = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
tcs
              then Doc
empty
              else Doc -> Doc
parens ([Doc] -> Doc
fcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map TypeClass -> Doc
prettyTypeClass forall a b. (a -> b) -> a -> b
$ [TypeClass]
tcs)
   in Bool -> Doc -> Doc
parensIf (PrettyControl -> Bool
withParens PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
        [Doc] -> Doc
fsep [ String -> Doc
text String
"forall"
             , forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either TermVariable -> Doc
prettyTermVariable TermVariable -> Doc
prettyTermVariable Either TermVariable TermVariable
v
             , String -> Doc
text String
"in"
             , forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const (String -> Doc
text String
"FUN")) (forall a b. a -> b -> a
const (String -> Doc
text String
"FUN_i")) Either TermVariable TermVariable
v
                Doc -> Doc -> Doc
<> (Bool -> Doc -> Doc
when (PrettyControl -> Bool
withLanguageSubsets PrettyControl
pc) forall a b. (a -> b) -> a -> b
$
                     String -> Doc
text String
"^" Doc -> Doc -> Doc
<> Doc -> Doc
braces (LanguageSubset -> Doc
prettyLanguageSubset 
                                          (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri)))
                Doc -> Doc -> Doc
<> Doc
dcs
                Doc -> Doc -> Doc
<> Char -> Doc
char Char
'.'
             , PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
useParens PrettyControl
pc) Bool
False Relation
r ]





-- | Pretty-prints a relation variable.

prettyRelationVariable :: RelationVariable -> Doc
prettyRelationVariable :: RelationVariable -> Doc
prettyRelationVariable (RVar String
r) = String -> Doc
text String
r





------- Unfolded formulas -----------------------------------------------------


-- | Pretty-prints an unfolded lift relation.

prettyUnfoldedLift :: [PrettyTheoremOption] -> UnfoldedLift -> Doc
prettyUnfoldedLift :: [PrettyTheoremOption] -> UnfoldedLift -> Doc
prettyUnfoldedLift [PrettyTheoremOption]
opt (UnfoldedLift Relation
r [UnfoldedDataCon]
dcs) =
  let pc :: PrettyControl
pc = [PrettyTheoremOption] -> PrettyControl
defaultPrettyControl [PrettyTheoremOption]
opt
      sc :: Doc
sc = Doc -> Doc
braces forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (PrettyControl -> UnfoldedDataCon -> Doc
prettyUnfoldedDataCon PrettyControl
pc) 
           forall a b. (a -> b) -> a -> b
$ [UnfoldedDataCon]
simpleCons
      ccs :: [Doc]
ccs = forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
braces forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrettyControl -> UnfoldedDataCon -> Doc
prettyUnfoldedDataCon PrettyControl
pc) [UnfoldedDataCon]
complexCons
      dcs :: [Doc]
dcs = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UnfoldedDataCon]
simpleCons then [Doc]
ccs else Doc
sc forall a. a -> [a] -> [a]
: [Doc]
ccs
   in [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$
        [ PrettyControl -> Bool -> Relation -> Doc
prettyRelation (PrettyControl -> PrettyControl
noParens PrettyControl
pc) Bool
True Relation
r ]
        forall a. [a] -> [a] -> [a]
++ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\String
t Doc
d -> Int -> Doc -> Doc
nest Int
2 (String -> Doc
text String
t Doc -> Doc -> Doc
<+> Doc
d)) (String
"=" forall a. a -> [a] -> [a]
: forall a. a -> [a]
repeat String
"u") [Doc]
dcs
  where
    ([UnfoldedDataCon]
simpleCons, [UnfoldedDataCon]
complexCons) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition UnfoldedDataCon -> Bool
isSimpleCon [UnfoldedDataCon]
dcs

    isSimpleCon :: UnfoldedDataCon -> Bool
isSimpleCon UnfoldedDataCon
d = case UnfoldedDataCon
d of
      UnfoldedDataCon
BotPair   -> Bool
True
      ConPair DataConstructor
_ -> Bool
True
      UnfoldedDataCon
otherwise -> Bool
False



-- | Pretty-prints an unfolded data constructor declaration.

prettyUnfoldedDataCon :: PrettyControl -> UnfoldedDataCon -> Doc
prettyUnfoldedDataCon :: PrettyControl -> UnfoldedDataCon -> Doc
prettyUnfoldedDataCon PrettyControl
_ UnfoldedDataCon
BotPair = 
  Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [ String -> Doc
text String
"_|_", String -> Doc
text String
"_|_" ]))

prettyUnfoldedDataCon PrettyControl
_ (ConPair DataConstructor
d) =
  let d' :: Doc
d' = DataConstructor -> [TermVariable] -> Doc
prettyDataConstructor DataConstructor
d []
   in Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma [ Doc
d', Doc
d' ]))

prettyUnfoldedDataCon PrettyControl
pc (ConMore DataConstructor
d [TermVariable]
xs [TermVariable]
ys Theorem
f) = 
  let d1 :: Doc
d1 = DataConstructor -> [TermVariable] -> Doc
prettyDataConstructor DataConstructor
d [TermVariable]
xs
      d2 :: Doc
d2 = DataConstructor -> [TermVariable] -> Doc
prettyDataConstructor DataConstructor
d [TermVariable]
ys
   in [Doc] -> Doc
sep [ [Doc] -> Doc
fsep [ Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall a b. (a -> b) -> a -> b
$ [Doc
d1, Doc
d2] 
                 , String -> Doc
text String
"|" ]
          , Int -> Doc -> Doc
nest Int
2 (PrettyControl -> Theorem -> Doc
prettyFormula PrettyControl
pc Theorem
f) ]



-- | Pretty-prints a data constructor.

prettyDataConstructor :: DataConstructor -> [TermVariable] -> Doc
prettyDataConstructor :: DataConstructor -> [TermVariable] -> Doc
prettyDataConstructor DataConstructor
DConEmptyList [TermVariable]
_    = Doc -> Doc
brackets Doc
empty
prettyDataConstructor DataConstructor
DConConsList [TermVariable
x,TermVariable
y] = [Doc] -> Doc
fsep [TermVariable -> Doc
prettyTermVariable TermVariable
x, String -> Doc
text String
":"
                                                , TermVariable -> Doc
prettyTermVariable TermVariable
y]
prettyDataConstructor DataConstructor
DConConsList [TermVariable]
_     = Doc -> Doc
brackets Doc
empty
prettyDataConstructor (DConTuple Int
_) [TermVariable]
xs = 
  Doc -> Doc
parens ([Doc] -> Doc
fsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map TermVariable -> Doc
prettyTermVariable forall a b. (a -> b) -> a -> b
$ [TermVariable]
xs)
prettyDataConstructor (DCon String
s) [TermVariable]
xs = [Doc] -> Doc
fsep (String -> Doc
text String
s forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map TermVariable -> Doc
prettyTermVariable [TermVariable]
xs)



-- | Pretty-prints an unfolded type class.

prettyUnfoldedClass :: [PrettyTheoremOption] -> UnfoldedClass -> Doc
prettyUnfoldedClass :: [PrettyTheoremOption] -> UnfoldedClass -> Doc
prettyUnfoldedClass [PrettyTheoremOption]
opt (UnfoldedClass [TypeClass]
tcs TypeClass
tc Either RelationVariable TermVariable
v [Theorem]
fs) =
  let pc :: PrettyControl
pc = [PrettyTheoremOption] -> PrettyControl
defaultPrettyControl [PrettyTheoremOption]
opt
      pv :: Doc
pv = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either RelationVariable -> Doc
prettyRelationVariable TermVariable -> Doc
prettyTermVariable Either RelationVariable TermVariable
v 
      intro :: [Doc]
intro = [ Doc
pv, String -> Doc
text String
"respects", TypeClass -> Doc
prettyTypeClass TypeClass
tc ] 
   in if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
tcs Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Theorem]
fs
        then [Doc] -> Doc
fsep forall a b. (a -> b) -> a -> b
$ [Doc]
intro forall a. [a] -> [a] -> [a]
++ (forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words forall a b. (a -> b) -> a -> b
$
                      String
"without further restrictions")
        else [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$
               ([Doc] -> Doc
fsep forall a b. (a -> b) -> a -> b
$
                  [Doc]
intro forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"if"]
                  forall a. [a] -> [a] -> [a]
++ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
tcs
                       then []
                       else [ Doc
pv, String -> Doc
text String
"respects" ]
                            forall a. [a] -> [a] -> [a]
++ (Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map TypeClass -> Doc
prettyTypeClass forall a b. (a -> b) -> a -> b
$ [TypeClass]
tcs)
                  forall a. [a] -> [a] -> [a]
++ if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
tcs) Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Theorem]
fs)
                       then [ String -> Doc
text String
"and" ]
                       else [])
               forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrettyControl -> Theorem -> Doc
prettyFormula PrettyControl
pc) [Theorem]
fs)