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
data PrettyTheoremOption
= OmitTypeInstantiations
| OmitLanguageSubsets
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
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) }
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
"[="
prettyTheorem :: [PrettyTheoremOption] -> Theorem -> Doc
prettyTheorem :: [PrettyTheoremOption] -> Theorem -> Doc
prettyTheorem [PrettyTheoremOption]
opt = PrettyControl -> Theorem -> Doc
prettyFormula ([PrettyTheoremOption] -> PrettyControl
defaultPrettyControl [PrettyTheoremOption]
opt)
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)
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 -> []
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
'.' ])
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 ]
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"
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)
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
prettyTermVariable :: TermVariable -> Doc
prettyTermVariable :: TermVariable -> Doc
prettyTermVariable (TVar String
v) = String -> Doc
text String
v
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)
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 ]
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 ]
prettyRelationVariable :: RelationVariable -> Doc
prettyRelationVariable :: RelationVariable -> Doc
prettyRelationVariable (RVar String
r) = String -> Doc
text String
r
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
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) ]
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)
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)