{- |
Module : ./CASL/ToDoc.hs
Description : pretty printing data types of BASIC_SPEC
Copyright : (c) Christian Maeder and Uni Bremen 2006
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : experimental
Portability : portable
Pretty printing data types of 'BASIC_SPEC'
-}
module CASL.ToDoc
( printBASIC_SPEC
, printFormula
, printTerm
, printTheoryFormula
, pluralS_symb_list
, pluralS
, appendS
, isJunct
, printInfix
, ListCheck (..)
, recoverType
, printALTERNATIVE
, typeString
, printVarDecl
, printVarDeclL
, printVarDecls
, printOptArgDecls
, printSortItem
, printOpItem
, printPredItem
, printPredHead
, printRecord
, printAttr
, printAnnotedBulletFormulas
, FormExtension (..)
, isQuant
) where
import Common.Id
import Common.Keywords
import Common.Doc
import Common.DocUtils
import Common.AS_Annotation
import CASL.AS_Basic_CASL
import CASL.Fold
instance (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_SPEC b s f)
where pretty = printBASIC_SPEC pretty pretty
printBASIC_SPEC :: FormExtension f => (b -> Doc) -> (s -> Doc)
-> BASIC_SPEC b s f -> Doc
printBASIC_SPEC fB fS (Basic_spec l) = case l of
[] -> specBraces empty
_ -> vcat $ map (printAnnoted (printBASIC_ITEMS fB fS)) l
instance (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_ITEMS b s f)
where pretty = printBASIC_ITEMS pretty pretty
typeString :: SortsKind -> [Annoted DATATYPE_DECL] -> String
typeString sk l = (case sk of
NonEmptySorts -> typeS
PossiblyEmptySorts -> etypeS) ++ appendS l
printBASIC_ITEMS :: FormExtension f => (b -> Doc) -> (s -> Doc)
-> BASIC_ITEMS b s f -> Doc
printBASIC_ITEMS fB fS sis = case sis of
Sig_items s -> printSIG_ITEMS fS s
Free_datatype sk l _ -> sep [keyword freeS <+> keyword (typeString sk l),
semiAnnos printDATATYPE_DECL l]
Sort_gen l _ -> case l of
[Annoted (Datatype_items sk l' _) _ las ras] ->
(if null las then id else (printAnnotationList las $+$))
$ (if null ras then id else ($+$ printAnnotationList ras))
$ sep [keyword generatedS <+> keyword (typeString sk l'),
semiAnnos printDATATYPE_DECL l']
_ -> sep [keyword generatedS, specBraces $ vcat $ map
(printAnnoted $ printSIG_ITEMS fS) l]
Var_items l _ -> topSigKey (varS ++ pluralS l) <+> printVarDecls l
Local_var_axioms l f _ ->
fsep [fsep $ forallDoc : printVarDeclL l
, printAnnotedBulletFormulas f]
Axiom_items f _ -> printAnnotedBulletFormulas f
Ext_BASIC_ITEMS b -> fB b
printAnnotedBulletFormulas :: FormExtension f => [Annoted (FORMULA f)] -> Doc
printAnnotedBulletFormulas l = vcat $ case l of
[] -> []
_ -> let pp = addBullet . printFormula in
map (printAnnoted pp) (init l)
++ [printSemiAnno pp False $ last l] -- use True for HasCASL
instance (Pretty s, FormExtension f) => Pretty (SIG_ITEMS s f) where
pretty = printSIG_ITEMS pretty
printSIG_ITEMS :: FormExtension f => (s -> Doc) -> SIG_ITEMS s f -> Doc
printSIG_ITEMS fS sis = case sis of
Sort_items sk l _ -> topSigKey ((case sk of
NonEmptySorts -> sortS
PossiblyEmptySorts -> esortS) ++ pluralS l) <+>
semiAnnos printSortItem l
Op_items l _ -> topSigKey (opS ++ pluralS l) <+>
let pp = printOpItem in
if null l then empty else if case item $ last l of
Op_decl _ _ a@(_ : _) _ -> case last a of
Unit_op_attr {} -> False -- use True for HasCASL
_ -> False
Op_defn {} -> False -- use True for HasCASL
_ -> False
then vcat $ map (printSemiAnno pp True) l else semiAnnos pp l
Pred_items l _ -> topSigKey (predS ++ pluralS l) <+>
let pp = printPredItem in
if null l then empty else if case item $ last l of
Pred_defn {} -> True
_ -> False
then vcat $ map (printSemiAnno pp True) l else semiAnnos pp l
Datatype_items sk l _ -> topSigKey (typeString sk l) <+>
semiAnnos printDATATYPE_DECL l
Ext_SIG_ITEMS s -> fS s
printDATATYPE_DECL :: DATATYPE_DECL -> Doc
printDATATYPE_DECL (Datatype_decl s a r) =
let pa = printAnnoted printALTERNATIVE in case a of
[] -> printDATATYPE_DECL (Datatype_decl s [emptyAnno $ Subsorts [s] r] r)
h : t -> sep [idLabelDoc s, colon <> colon <> sep
((equals <+> pa h) :
map ((bar <+>) . pa) t)]
instance Pretty DATATYPE_DECL where
pretty = printDATATYPE_DECL
printCOMPONENTS :: COMPONENTS -> Doc
printCOMPONENTS c = case c of
Cons_select k l s _ -> fsep $ punctuate comma (map idLabelDoc l)
++ [case k of
Total -> colon
Partial -> colon <> quMarkD, idDoc s]
Sort s -> idDoc s
instance Pretty COMPONENTS where
pretty = printCOMPONENTS
printALTERNATIVE :: ALTERNATIVE -> Doc
printALTERNATIVE a = case a of
Alt_construct k n l _ -> case l of
[] -> idLabelDoc n
_ -> idLabelDoc n <>
parens ( sep $ punctuate semi $ map printCOMPONENTS l)
<> case k of
Total -> empty
Partial -> quMarkD
Subsorts l _ -> fsep $ text (sortS ++ pluralS l)
: punctuate comma (map idDoc l)
instance Pretty ALTERNATIVE where
pretty = printALTERNATIVE
printSortItem :: FormExtension f => SORT_ITEM f -> Doc
printSortItem si = case si of
Sort_decl sl _ -> sepByCommas $ map idLabelDoc sl
Subsort_decl sl sup _ ->
fsep $ punctuate comma (map idDoc sl) ++ [less, idDoc sup]
Subsort_defn s v sup af _ -> fsep [idLabelDoc s, equals,
specBraces $ fsep [sidDoc v, colon <+> idDoc sup,
printAnnoted (addBullet . printFormula) af]]
Iso_decl sl _ -> fsep $ punctuate (space <> equals) $ map idDoc sl
instance FormExtension f => Pretty (SORT_ITEM f) where
pretty = printSortItem
printQuant :: QUANTIFIER -> Doc
printQuant q = case q of
Universal -> forallDoc
Existential -> exists
Unique_existential -> unique
printSortedVars :: [VAR] -> SORT -> Doc
printSortedVars l s =
fsep $ punctuate comma (map sidDoc l) ++ [colon <+> idDoc s]
printVarDeclL :: [VAR_DECL] -> [Doc]
printVarDeclL = punctuate semi . map printVarDecl
printVarDecls :: [VAR_DECL] -> Doc
printVarDecls = fsep . printVarDeclL
printVarDecl :: VAR_DECL -> Doc
printVarDecl (Var_decl l s _) = printSortedVars l s
printArgDecls :: [VAR_DECL] -> Doc
printArgDecls = parens . printVarDecls
printOptArgDecls :: [VAR_DECL] -> Doc
printOptArgDecls vs = if null vs then empty else printArgDecls vs
printPredHead :: PRED_HEAD -> Doc
printPredHead (Pred_head l _) = printArgDecls l
printPredItem :: FormExtension f => PRED_ITEM f -> Doc
printPredItem p = case p of
Pred_decl l t _ -> fsep $ punctuate comma (map idLabelDoc l)
++ [colon <+> printPredType t]
Pred_defn i h f _ ->
sep [ cat [idLabelDoc i, printPredHead h]
, equiv <+> printAnnoted printFormula f]
instance FormExtension f => Pretty (PRED_ITEM f) where
pretty = printPredItem
printAttr :: FormExtension f => OP_ATTR f -> Doc
printAttr a = case a of
Assoc_op_attr -> text assocS
Comm_op_attr -> text commS
Idem_op_attr -> text idemS
Unit_op_attr t -> text unitS <+> printTerm t
instance FormExtension f => Pretty (OP_ATTR f) where
pretty = printAttr
printOpHead :: OP_HEAD -> Doc
printOpHead (Op_head k l mr _) =
sep $ printOptArgDecls l : case mr of
Nothing -> []
Just r -> [(case k of
Total -> colon
Partial -> text colonQuMark) <+> idDoc r]
instance Pretty OP_HEAD where
pretty = printOpHead
printOpItem :: FormExtension f => OP_ITEM f -> Doc
printOpItem p = case p of
Op_decl l t a _ -> fsep $ punctuate comma (map idLabelDoc l)
++ [colon <> (if null a then id else (<> comma)) (printOpType t)]
++ punctuate comma (map printAttr a)
Op_defn i h@(Op_head _ l _ _) t _ ->
sep [ (if null l then sep else cat) [idLabelDoc i, printOpHead h]
, equals <+> printAnnoted printTerm t]
instance FormExtension f => Pretty (OP_ITEM f) where
pretty = printOpItem
instance Pretty VAR_DECL where
pretty = printVarDecl
printOpType :: OP_TYPE -> Doc
printOpType (Op_type p l r _) =
case l of
[] -> case p of
Partial -> quMarkD <+> idDoc r
Total -> space <> idDoc r
_ -> space <> fsep
(punctuate (space <> cross) (map idDoc l)
++ [case p of
Partial -> pfun
Total -> funArrow,
idDoc r])
instance Pretty OP_TYPE where
pretty = printOpType
printOpSymb :: OP_SYMB -> Doc
printOpSymb o = case o of
Op_name i -> idDoc i
Qual_op_name i t _ -> fsep [text opS, idDoc i, colon <> printOpType t]
instance Pretty OP_SYMB where
pretty = printOpSymb
printPredType :: PRED_TYPE -> Doc
printPredType (Pred_type l _) = case l of
[] -> parens empty
_ -> fsep $ punctuate (space <> cross) $ map idDoc l
instance Pretty PRED_TYPE where
pretty = printPredType
printPredSymb :: PRED_SYMB -> Doc
printPredSymb p = case p of
Pred_name i -> idDoc i
Qual_pred_name i t _ ->
parens $ fsep [text predS, idDoc i, colon <+> printPredType t]
instance Pretty PRED_SYMB where
pretty = printPredSymb
instance Pretty SYMB_ITEMS where
pretty = printSymbItems
printSymbItems :: SYMB_ITEMS -> Doc
printSymbItems (Symb_items k l _) =
print_kind_text k l <+> sepByCommas (map printSymb l)
instance Pretty SYMB where
pretty = printSymb
printSymb :: SYMB -> Doc
printSymb s = case s of
Symb_id i -> idDoc i
Qual_id i t _ -> fsep [idDoc i, colon <> printType t]
instance Pretty TYPE where
pretty = printType
printType :: TYPE -> Doc
printType t = case t of
O_type ot -> printOpType ot
P_type pt -> space <> printPredType pt
A_type s -> space <> idDoc s
print_kind_text :: SYMB_KIND -> [a] -> Doc
print_kind_text k l = case k of
Implicit -> empty
_ -> keyword (pluralS_symb_list k l)
pluralS_symb_list :: SYMB_KIND -> [a] -> String
pluralS_symb_list k l = (case k of
Implicit -> error "pluralS_symb_list"
Sorts_kind -> sortS
Ops_kind -> opS
Preds_kind -> predS) ++ appendS l
instance Pretty SYMB_OR_MAP where
pretty = printSymbOrMap
printSymbOrMap :: SYMB_OR_MAP -> Doc
printSymbOrMap som = case som of
Symb s -> printSymb s
Symb_map s t _ -> fsep [printSymb s, mapsto <+> printSymb t]
instance Pretty SYMB_KIND where
pretty = printSymbKind
printSymbKind :: SYMB_KIND -> Doc
printSymbKind sk = print_kind_text sk [()]
instance Pretty SYMB_MAP_ITEMS where
pretty = printSymbMapItems
printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
printSymbMapItems (Symb_map_items k l _) =
print_kind_text k l <+> sepByCommas (map printSymbOrMap l)
-- possibly use "printInfix False vcat"
printInfix :: Bool -- ^ attach separator to right argument?
-> ([Doc] -> Doc) -- ^ combinator for two docs
-> Doc -> Doc -> Doc -- ^ left, separator and right arguments
-> Doc
printInfix b join l s r =
join $ if b then [l, s <+> r] else [l <+> s, r]
class (GetRange f, Pretty f) => FormExtension f where
isQuantifierLike :: f -> Bool
isQuantifierLike _ = False
prefixExt :: f -> Doc -> Doc
prefixExt _ = (bullet <+>)
instance FormExtension ()
printRecord :: FormExtension f => Record f Doc Doc
printRecord = Record
{ foldQuantification = \ _ q l r _ ->
fsep $ printQuant q : printVarDeclL l
++ [addBullet r]
, foldJunction = \ o j l _ ->
let (n, p) = case j of
Con -> (trueS, andDoc)
Dis -> (falseS, orDoc)
in case o of
Junction _ ol@(_ : _) _ -> fsep $ prepPunctuate (p <> space)
$ zipWith (mkJunctDoc True) (init ol) (init l) ++
[mkJunctDoc False (last ol) (last l)]
_ -> text n
, foldRelation = \ o l c r _ ->
let Relation oL _ oR _ = o
b = c == Implication
nl = if isAnyImpl oL || b && isQuant oL
then parens l else l
nr = if isImpl c oR || not b && isQuant oR
then parens r else r
in case c of
Implication -> printInfix True sep nl implies nr
RevImpl -> printInfix True sep nr (text ifS) nl
Equivalence -> printInfix True sep
(if isQuant oL then parens l else mkEquivDoc oL l)
equiv $ mkEquivDoc oR r
, foldNegation = \ orig r _ -> case orig of
Negation o _ -> hsep [notDoc, mkJunctDoc False o r]
_ -> error "CASL.ToDoc.printRecord.foldNegation"
, foldAtom = \ _ b _ -> text $ if b then trueS else falseS
, foldPredication = \ o p l _ -> case (p, o) of
(Pred_name i, Predication _ ol _) -> predIdApplDoc i $ zipConds ol l
_ -> if null l then printPredSymb p else
fcat [printPredSymb p, parens $ sepByCommas l]
, foldDefinedness = \ _ r _ -> hsep [text defS, r]
, foldEquation = \ _ l e r _ -> printInfix True sep l (case e of
Existl -> exequal
Strong -> equals) r
, foldMembership = \ _ r t _ -> fsep [r, inDoc, idDoc t]
, foldMixfix_formula = \ _ r -> r
, foldSort_gen_ax = \ o _ _ ->
let Sort_gen_ax constrs b = o
l = recoverType constrs
genAx = sep [ keyword generatedS <+> keyword (typeS ++ appendS l)
, semiAnnos printDATATYPE_DECL l]
in if b then text "%% free" $+$ genAx else genAx
, foldQuantOp = \ _ o n r -> fsep
[ forallDoc
, parens . printOpSymb $ mkQualOp o n
, addBullet r ]
, foldQuantPred = \ _ p n r -> fsep
[ forallDoc
, printPredSymb $ mkQualPred p n
, addBullet r ]
, foldExtFORMULA = const pretty
, foldQual_var = \ _ v s _ ->
parens $ fsep [text varS, sidDoc v, colon <+> idDoc s]
, foldApplication = \ orig o l _ -> case (o, orig) of
(Op_name i, Application _ ol _) -> idApplDoc i $ zipConds ol l
_ -> let d = parens $ printOpSymb o in
if null l then d else fcat [d, parens $ sepByCommas l]
, foldSorted_term = \ _ r t _ -> fsep [idApplDoc typeId [r], idDoc t]
, foldCast = \ _ r t _ ->
fsep [idApplDoc (mkId [placeTok, mkSimpleId asS]) [r], idDoc t]
, foldConditional = \ o l f r _ -> case o of
Conditional ol _ _ _ -> fsep [if isCond ol then parens l else l,
text whenS <+> f, text elseS <+> r]
_ -> error "CASL.ToDoc.printRecord.foldConditional"
, foldMixfix_qual_pred = const printPredSymb
, foldMixfix_term = \ o l -> case o of
Mixfix_term [_, Mixfix_parenthesized _ _] -> fcat l
_ -> fsep l
, foldMixfix_token = const sidDoc
, foldMixfix_sorted_term = \ _ s _ -> colon <+> idDoc s
, foldMixfix_cast = \ _ s _ -> text asS <+> idDoc s
, foldMixfix_parenthesized = \ _ l _ -> parens $ sepByCommas l
, foldMixfix_bracketed = \ _ l _ -> brackets $ sepByCommas l
, foldMixfix_braced = \ _ l _ -> specBraces $ sepByCommas l
, foldExtTERM = const pretty }
recoverType :: [Constraint] -> [Annoted DATATYPE_DECL]
recoverType =
map (\ c -> let s = newSort c in emptyAnno $ Datatype_decl s
(map (\ (o, _) -> case o of
Qual_op_name i (Op_type fk args _ ps) r ->
let qs = appRange ps r in emptyAnno $ case args of
[_] | isInjName i -> Subsorts args qs
_ -> Alt_construct fk i (map Sort args) qs
_ -> error "CASL.recoverType") $ opSymbs c) nullRange)
zipConds :: [TERM f] -> [Doc] -> [Doc]
zipConds = zipWith (\ o d -> if isCond o then parens d else d)
printFormula :: FormExtension f => FORMULA f -> Doc
printFormula = foldFormula printRecord
instance FormExtension f => Pretty (FORMULA f) where
pretty = printFormula
printTerm :: FormExtension f => TERM f -> Doc
printTerm = foldTerm printRecord
instance FormExtension f => Pretty (TERM f) where
pretty = printTerm
isQuant :: FormExtension f => FORMULA f -> Bool
isQuant f = case f of
Quantification {} -> True
ExtFORMULA ef -> isQuantifierLike ef
Junction _ l _ -> case l of
[] -> False
_ -> isQuant $ last l
Relation a c b _ -> isQuant $ if c == RevImpl then a else b
Negation a _ -> isQuant a
_ -> False
isEquiv :: FORMULA f -> Bool
isEquiv f = case f of
Relation _ c _ _ -> c == Equivalence
_ -> False
isAnyImpl :: FORMULA f -> Bool
isAnyImpl f = isImpl Implication f || isImpl RevImpl f
isJunct :: FORMULA f -> Bool
isJunct f = case f of
Junction {} -> True
_ -> isAnyImpl f
-- true for non-final
mkJunctDoc :: FormExtension f => Bool -> FORMULA f -> Doc -> Doc
mkJunctDoc b f = if isJunct f || b && isQuant f then parens else id
mkEquivDoc :: FORMULA f -> Doc -> Doc
mkEquivDoc f = if isEquiv f then parens else id
isImpl :: Relation -> FORMULA f -> Bool
isImpl a f = case f of
Relation _ c _ _ -> c == Equivalence || a /= c
_ -> False
isCond :: TERM f -> Bool
isCond t = case t of
Conditional {} -> True
_ -> False
-- | a helper class for calculating the pluralS of e.g. ops
class ListCheck a where
innerList :: a -> [()]
instance ListCheck Token where
innerList _ = [()]
instance ListCheck Id where
innerList _ = [()]
instance ListCheck a => ListCheck [a] where
innerList = concatMap innerList
-- | an instance of ListCheck for Annoted stuff
instance ListCheck a => ListCheck (Annoted a) where
innerList = innerList . item
{- | pluralS checks nested lists via the class ListCheck to decide
if a plural s should be appended. -}
pluralS :: ListCheck a => a -> String
pluralS = appendS . innerList
appendS :: [a] -> String
appendS l = if isSingle l then "" else "s"
-- instances of ListCheck for various data types of AS_Basic_CASL
instance ListCheck (SORT_ITEM f) where
innerList (Sort_decl l _) = innerList l
innerList (Subsort_decl l _ _) = innerList l
innerList (Subsort_defn {}) = [()]
innerList (Iso_decl l _) = innerList $ drop 1 l
-- assume last sort is known
instance ListCheck (OP_ITEM f) where
innerList (Op_decl l _ _ _) = innerList l
innerList (Op_defn {}) = [()]
instance ListCheck (PRED_ITEM f) where
innerList (Pred_decl l _ _) = innerList l
innerList (Pred_defn {}) = [()]
instance ListCheck VAR_DECL where
innerList (Var_decl l _ _) = innerList l
-- | print a formula as a sentence
printTheoryFormula :: FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula f = printAnnoted
((case sentence f of
Quantification Universal _ _ _ -> id
Sort_gen_ax _ _ -> id
ExtFORMULA e -> prefixExt e
_ -> (bullet <+>)) . pretty) $ fromLabelledSen f