module Language.Haskell.FreeTheorems.PrettyTheorems (
PrettyTheoremOption (..)
, prettyTheorem
, prettyRelationVariable
, prettyUnfoldedLift
, prettyUnfoldedClass
) where
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 Eq
data PrettyControl = PrettyControl
{ options :: [PrettyTheoremOption]
, parentheses :: Parens
, inPremise :: Bool
}
defaultPrettyControl :: [PrettyTheoremOption] -> PrettyControl
defaultPrettyControl opts =
PrettyControl
{ options = opts
, parentheses = NoParens
, inPremise = False
}
withTypeInstantiations :: PrettyControl -> Bool
withTypeInstantiations = notElem OmitTypeInstantiations . options
withLanguageSubsets :: PrettyControl -> Bool
withLanguageSubsets = notElem OmitLanguageSubsets . options
noParens :: PrettyControl -> PrettyControl
noParens pc = pc { parentheses = NoParens }
useParens :: PrettyControl -> PrettyControl
useParens pc = pc { parentheses = ParensFun }
withParens :: PrettyControl -> Bool
withParens pc = parentheses pc > NoParens
setPremise :: PrettyControl -> PrettyControl
setPremise pc = pc { inPremise = not (inPremise pc) }
prettyLanguageSubset :: LanguageSubset -> Doc
prettyLanguageSubset l = case l of
BasicSubset -> text "basic"
SubsetWithFix EquationalTheorem -> text "fix" <> comma <> text "="
SubsetWithFix InequationalTheorem -> text "fix" <> comma <> text "[="
SubsetWithSeq EquationalTheorem -> text "seq" <> comma <> text "="
SubsetWithSeq InequationalTheorem -> text "seq" <> comma <> text "[="
prettyTheorem :: [PrettyTheoremOption] -> Theorem -> Doc
prettyTheorem opt = prettyFormula (defaultPrettyControl opt)
prettyFormula :: PrettyControl -> Formula -> Doc
prettyFormula pc (ForallRelations v (t1,t2) res f) =
let rv = prettyRelationVariable v
ts = prettyTypeExpression NoParens t1 <> comma
<> prettyTypeExpression NoParens t2
cs = getTypeClasses res
ds = if null cs
then empty
else parens . fsep . punctuate comma . map prettyTypeClass $ cs
in parensIf (withParens pc) $
sep
[ fsep $
[ text "forall"
, ts, text "in", text "TYPES" <> ds <> comma
, rv, text "in"
, text "REL" <> parens ts
<> if null res then char '.' else comma ]
++ prettyRestrictionList rv res
, nest 1 (prettyFormula (noParens pc) f) ]
prettyFormula pc (ForallFunctions v (t1,t2) res f) =
let ts = prettyTypeExpression NoParens t1 <> comma
<> prettyTypeExpression NoParens t2
pv = either prettyTermVariable prettyTermVariable v
cs = getTypeClasses res
ds = if null cs
then empty
else parens . fsep . punctuate comma . map prettyTypeClass $ cs
in parensIf (withParens pc) $
sep
[ fsep $
[ text "forall"
, ts, text "in", text "TYPES" <> ds <> comma
, pv, text "::"
, prettyTypeExpression NoParens
(either (\_ -> TypeFun t1 t2) (\_ -> TypeFun t2 t1) v)
<> if null res then char '.' else comma ]
++ prettyRestrictionList pv res
, nest 1 (prettyFormula (noParens pc) f) ]
prettyFormula pc (ForallPairs (v1,v2) r f) =
parensIf (withParens pc) $
sep [ fsep [ text "forall"
, parens (prettyTermVariable v1 <> comma
<+> prettyTermVariable v2)
, text "in", prettyRelation (useParens pc) False r <> char '.' ]
, nest 1 (prettyFormula (noParens pc) f) ]
prettyFormula pc (ForallVariables v t f) =
parensIf (withParens pc) $
sep [ fsep [ text "forall", prettyTermVariable v, text "::"
, prettyTypeExpression NoParens t <> char '.' ]
, nest 1 (prettyFormula (noParens pc) f) ]
prettyFormula pc (Equivalence f1 f2) =
parensIf (withParens pc) $
sep [ prettyFormula (useParens pc) f1
, text "<=>" <+> prettyFormula (useParens pc) f2]
prettyFormula pc (Implication f1 f2) =
parensIf (withParens pc) $
sep [ prettyFormula (useParens (setPremise pc)) f1
, text "==>" <+> prettyFormula (useParens pc) f2]
prettyFormula pc (Conjunction f1 f2) =
parensIf (withParens pc) $
sep [ prettyFormula (useParens pc) f1
, text "&&" <+> prettyFormula (useParens pc) f2]
prettyFormula pc (Predicate predicate) =
parensIf (withParens pc) (prettyPredicate (noParens pc) predicate)
getTypeClasses :: [Restriction] -> [TypeClass]
getTypeClasses = concatMap exTC
where exTC r = case r of
RespectsClasses tcs -> tcs
otherwise -> []
prettyRestrictionList :: Doc -> [Restriction] -> [Doc]
prettyRestrictionList v res = case res of
[] -> []
(r:[]) -> v : [ prettyRestriction r <> char '.' ]
(r1:r2:[]) -> v : (punctuate comma [prettyRestriction r1] ++ [text "and", prettyRestriction r2 <> char '.' ])
otherwise -> let dres = map prettyRestriction res
in v : (punctuate comma (init dres ++ [text "and"])
++ [last dres <> char '.' ])
prettyRestriction :: Restriction -> Doc
prettyRestriction Strict = text "strict"
prettyRestriction Continuous = text "continuous"
prettyRestriction Total = text "total"
prettyRestriction BottomReflecting = text "bottom-reflecting"
prettyRestriction LeftClosed = text "left-closed"
prettyRestriction (RespectsClasses tcs) =
when (not (null tcs)) $
fsep [ text "respects"
, parensIf (length tcs > 1) $
fsep . punctuate comma . map prettyTypeClass $ tcs ]
prettyPredicate :: PrettyControl -> Predicate -> Doc
prettyPredicate pc (IsMember x y r) =
fsep [ parens (prettyTerm (noParens pc) x <> comma
<+> prettyTerm (noParens pc) y)
, text "in", prettyRelation (useParens pc) False r ]
prettyPredicate pc (IsEqual x y) =
fsep [ prettyTerm (noParens pc) x, char '=', prettyTerm (noParens pc) y ]
prettyPredicate pc (IsLessEq x y) =
fsep [ prettyTerm (noParens pc) x, text "[=", prettyTerm (noParens pc) y ]
prettyPredicate pc (IsNotBot x) =
parensIf (withParens pc) $
fsep [ prettyTerm (noParens pc) x, text "/=", text "_|_" ]
prettyPredicate pc (IsTrue) =
text "True"
prettyTerm :: PrettyControl -> Term -> Doc
prettyTerm pc (TermVar v) = prettyTermVariable v
prettyTerm pc (TermApp t1 t2) =
parensIf (withParens pc) $ prettyTerm (noParens pc) t1 <+> prettyTerm (useParens pc) t2
prettyTerm pc (TermIns t ty) =
let d = prettyTypeExpression NoParens ty
withTypes = withTypeInstantiations pc
p = if withTypes then useParens else noParens
pt = prettyTerm (useParens pc) t
in pt <> showInstantiation withTypes d
prettyTerm pc (TermComp []) =
text "id"
prettyTerm pc (TermComp [t]) =
parensIf (withParens pc) $ prettyTerm (noParens pc) t
prettyTerm pc (TermComp (t:ts)) =
parensIf (withParens pc) $ prettyTerm (noParens pc) t <+> text "." <+>
prettyTerm (noParens pc) (TermComp ts)
showInstantiation :: Bool -> Doc -> Doc
showInstantiation False _ = empty
showInstantiation True d = char '_' <> braces d
prettyTermVariable :: TermVariable -> Doc
prettyTermVariable (TVar v) = text v
prettyRelation :: PrettyControl -> Bool -> Relation -> Doc
prettyRelation _ _ (RelVar _ rv) = prettyRelationVariable rv
prettyRelation pc _ (FunVar ri (Left t)) =
case theoremType (relationLanguageSubset ri) of
EquationalTheorem -> prettyTerm (noParens pc) t
InequationalTheorem -> prettyTerm (useParens pc) t <> text " ; [="
prettyRelation pc _ (FunVar _ (Right t)) =
text "[= ; " <> prettyTerm (useParens pc) t <> text "^{-1}"
prettyRelation _ _ (RelBasic ri) =
case theoremType (relationLanguageSubset ri) of
EquationalTheorem -> text "id"
InequationalTheorem -> text "[="
prettyRelation pc omitOrder (RelLift ri con rs) =
let pl = case relationLanguageSubset ri of
BasicSubset -> text "lift"
otherwise -> case theoremType (relationLanguageSubset ri) of
EquationalTheorem -> text "lift"
InequationalTheorem -> if omitOrder
then text "lift"
else text "[= ; lift"
in pl <> braces (prettyTypeConstructor con)
<> (parens . foldl1 (\a b -> a <> comma <> b)
. map (prettyRelation (noParens pc) False) $ rs)
prettyRelation pc _ (RelFun ri r1 r2) =
let l = if withLanguageSubsets pc
then case relationLanguageSubset ri of
SubsetWithSeq _ -> text "^" <> braces (prettyLanguageSubset
(relationLanguageSubset ri))
otherwise -> empty
else empty
in parensIf (withParens pc) $
fsep [ prettyRelation (useParens pc) False r1
, text "->" <> l
, prettyRelation (useParens pc) False r2 ]
prettyRelation pc _ (RelFunLab ri r1 r2) =
parensIf (withParens pc) $
fsep [ prettyRelation (useParens pc) False r1
, text "->^o" <> empty
, prettyRelation (useParens pc) False r2 ]
prettyRelation pc _ (RelAbs ri v _ res r) =
let tcs = getTypeClasses res
dcs = if null tcs
then empty
else parens (fcat . punctuate comma . map prettyTypeClass $ tcs)
in parensIf (withParens pc) $
fsep [ text "forall"
, prettyRelationVariable v
, text "in"
, text "REL"
<> (when (withLanguageSubsets pc) $
text "^" <> braces (prettyLanguageSubset
(relationLanguageSubset ri)))
<> dcs
<> char '.'
, prettyRelation (useParens pc) False r ]
prettyRelation pc _ (FunAbs ri v _ res r) =
let tcs = getTypeClasses res
dcs = if null tcs
then empty
else parens (fcat . punctuate comma . map prettyTypeClass $ tcs)
in parensIf (withParens pc) $
fsep [ text "forall"
, either prettyTermVariable prettyTermVariable v
, text "in"
, either (const (text "FUN")) (const (text "FUN_i")) v
<> (when (withLanguageSubsets pc) $
text "^" <> braces (prettyLanguageSubset
(relationLanguageSubset ri)))
<> dcs
<> char '.'
, prettyRelation (useParens pc) False r ]
prettyRelationVariable :: RelationVariable -> Doc
prettyRelationVariable (RVar r) = text r
prettyUnfoldedLift :: [PrettyTheoremOption] -> UnfoldedLift -> Doc
prettyUnfoldedLift opt (UnfoldedLift r dcs) =
let pc = defaultPrettyControl opt
sc = braces . fsep . punctuate comma . map (prettyUnfoldedDataCon pc)
$ simpleCons
ccs = map (braces . prettyUnfoldedDataCon pc) complexCons
dcs = if null simpleCons then ccs else sc : ccs
in vcat $
[ prettyRelation (noParens pc) True r ]
++ zipWith (\t d -> nest 2 (text t <+> d)) ("=" : repeat "u") dcs
where
(simpleCons, complexCons) = partition isSimpleCon dcs
isSimpleCon d = case d of
BotPair -> True
ConPair _ -> True
otherwise -> False
prettyUnfoldedDataCon :: PrettyControl -> UnfoldedDataCon -> Doc
prettyUnfoldedDataCon _ BotPair =
parens (fsep (punctuate comma [ text "_|_", text "_|_" ]))
prettyUnfoldedDataCon _ (ConPair d) =
let d' = prettyDataConstructor d []
in parens (fsep (punctuate comma [ d', d' ]))
prettyUnfoldedDataCon pc (ConMore d xs ys f) =
let d1 = prettyDataConstructor d xs
d2 = prettyDataConstructor d ys
in sep [ fsep [ parens . fsep . punctuate comma $ [d1, d2]
, text "|" ]
, nest 2 (prettyFormula pc f) ]
prettyDataConstructor :: DataConstructor -> [TermVariable] -> Doc
prettyDataConstructor DConEmptyList _ = brackets empty
prettyDataConstructor DConConsList [x,y] = fsep [prettyTermVariable x, text ":"
, prettyTermVariable y]
prettyDataConstructor DConConsList _ = brackets empty
prettyDataConstructor (DConTuple _) xs =
parens (fsep . punctuate comma . map prettyTermVariable $ xs)
prettyDataConstructor (DCon s) xs = fsep (text s : map prettyTermVariable xs)
prettyUnfoldedClass :: [PrettyTheoremOption] -> UnfoldedClass -> Doc
prettyUnfoldedClass opt (UnfoldedClass tcs tc v fs) =
let pc = defaultPrettyControl opt
pv = either prettyRelationVariable prettyTermVariable v
intro = [ pv, text "respects", prettyTypeClass tc ]
in if null tcs && null fs
then fsep $ intro ++ (map text . words $
"without further restrictions")
else vcat $
(fsep $
intro ++ [text "if"]
++ if null tcs
then []
else [ pv, text "respects" ]
++ (punctuate comma . map prettyTypeClass $ tcs)
++ if not (null tcs) && not (null fs)
then [ text "and" ]
else [])
: (map (nest 2 . prettyFormula pc) fs)