5784N/A{- |

5784N/AModule : $Header$

5784N/ADescription : pretty printing data types of BASIC_SPEC

5784N/ACopyright : (c) Christian Maeder and Uni Bremen 2006

5784N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

5784N/A

5784N/AMaintainer : Christian.Maeder@dfki.de

5784N/AStability : experimental

5784N/APortability : portable

5784N/A

5784N/APretty printing data types of 'BASIC_SPEC'

5784N/A-}

5784N/A

5784N/Amodule CASL.ToDoc

5784N/A ( printBASIC_SPEC

5784N/A , printFormula

5784N/A , printTerm

5784N/A , printTheoryFormula

5784N/A , pluralS

5784N/A , isJunct

5784N/A , ListCheck(..)

5784N/A , recoverType

5784N/A , printALTERNATIVE

5784N/A , typeString

5784N/A , printVarDecl

5784N/A , printSortItem

5784N/A , printOpItem

5784N/A , printPredItem

5784N/A , printPredHead

5784N/A , printAttr

5784N/A

5784N/A ) where

5784N/A

5784N/Aimport Common.Id

5784N/Aimport Common.Keywords

5784N/Aimport Common.Doc

5784N/Aimport Common.DocUtils

5784N/Aimport Common.AS_Annotation

5784N/A

5784N/Aimport CASL.AS_Basic_CASL

5784N/Aimport CASL.Fold

5784N/A

5784N/Ainstance (Pretty b, Pretty s, Pretty f) => Pretty (BASIC_SPEC b s f) where

5784N/A pretty = printBASIC_SPEC pretty pretty pretty

5784N/A

5784N/AprintBASIC_SPEC :: (b -> Doc) -> (s -> Doc) -> (f -> Doc)

5784N/A -> BASIC_SPEC b s f -> Doc

5784N/AprintBASIC_SPEC fB fS fF (Basic_spec l) = case l of

5784N/A [] -> specBraces empty

5784N/A _ -> vcat $ map (printAnnoted ( printBASIC_ITEMS fB fS fF)) l

5784N/A

5784N/Ainstance (Pretty b, Pretty s, Pretty f) => Pretty (BASIC_ITEMS b s f) where

5784N/A pretty = printBASIC_ITEMS pretty pretty pretty

5784N/A

5784N/AtypeString :: SortsKind -> [Annoted DATATYPE_DECL] -> String

5784N/AtypeString sk l = (case sk of

5784N/A NonEmptySorts -> typeS

5784N/A PossiblyEmptySorts -> etypeS) ++ pluralS l

5784N/A

5784N/AprintBASIC_ITEMS :: (b -> Doc) -> (s -> Doc) -> (f -> Doc)

5784N/A -> BASIC_ITEMS b s f -> Doc

5784N/AprintBASIC_ITEMS fB fS fF sis = case sis of

5784N/A Sig_items s -> printSIG_ITEMS fS fF s

5784N/A Free_datatype sk l _ -> sep [keyword freeS <+> keyword (typeString sk l),

5784N/A semiAnnos printDATATYPE_DECL l]

5784N/A Sort_gen l _ -> case l of

5784N/A [Annoted (Datatype_items sk l' _) _ las ras] ->

5784N/A (if null las then id else (printAnnotationList las $+$))

5784N/A $ (if null ras then id else ($+$ printAnnotationList ras))

5784N/A $ sep [keyword generatedS <+> keyword (typeString sk l'),

5784N/A semiAnnos printDATATYPE_DECL l']

5784N/A _ -> sep [keyword generatedS, specBraces $ vcat $ map

5784N/A (printAnnoted $ printSIG_ITEMS fS fF) l]

5784N/A Var_items l _ -> topSigKey (varS ++ pluralS l) <+>

5784N/A fsep (punctuate semi $ map printVarDecl l)

5784N/A Local_var_axioms l f _ ->

5784N/A fsep [fsep $ forallDoc : punctuate semi (map printVarDecl l)

5784N/A , printAnnotedBulletFormulas fF f]

5784N/A Axiom_items f _ -> printAnnotedBulletFormulas fF f

5784N/A Ext_BASIC_ITEMS b -> fB b

5784N/A

5784N/AprintAnnotedBulletFormulas :: (f -> Doc) -> [Annoted (FORMULA f)] -> Doc

5784N/AprintAnnotedBulletFormulas fF l = vcat $ case l of

5784N/A [] -> []

5784N/A _ -> let pp = addBullet . printFormula fF in

5784N/A map (printAnnoted pp) (init l)

5784N/A ++ [printSemiAnno pp False $ last l] -- use True for HasCASL

5784N/A

5784N/Ainstance (Pretty s, Pretty f) => Pretty (SIG_ITEMS s f) where

5784N/A pretty = printSIG_ITEMS pretty pretty

5784N/A

5784N/AprintSIG_ITEMS :: (s -> Doc) -> (f -> Doc) -> SIG_ITEMS s f -> Doc

5784N/AprintSIG_ITEMS fS fF sis = case sis of

5784N/A Sort_items sk l _ -> topSigKey ((case sk of

5784N/A NonEmptySorts -> sortS

5784N/A PossiblyEmptySorts -> esortS) ++ pluralS l) <+>

5784N/A semiAnnos (printSortItem fF) l

5784N/A Op_items l _ -> topSigKey (opS ++ pluralS l) <+>

5784N/A let pp = printOpItem fF in

5784N/A if null l then empty else if case item $ last l of

5784N/A Op_decl _ _ a@(_ : _) _ -> case last a of

5784N/A Unit_op_attr {} -> False -- use True for HasCASL

5784N/A _ -> False

5784N/A Op_defn {} -> False -- use True for HasCASL

5784N/A _ -> False

5784N/A then vcat $ map (printSemiAnno pp True) l else semiAnnos pp l

5784N/A Pred_items l _ -> topSigKey (predS ++ pluralS l) <+>

5784N/A let pp = printPredItem fF in

5784N/A if null l then empty else if case item $ last l of

5784N/A Pred_defn {} -> True

5784N/A _ -> False

5784N/A then vcat $ map (printSemiAnno pp True) l else semiAnnos pp l

5784N/A Datatype_items sk l _ -> topSigKey (typeString sk l) <+>

5784N/A semiAnnos printDATATYPE_DECL l

5784N/A Ext_SIG_ITEMS s -> fS s

5784N/A

5784N/AprintDATATYPE_DECL :: DATATYPE_DECL ->Doc

5784N/AprintDATATYPE_DECL (Datatype_decl s a r) =

5784N/A let pa = printAnnoted printALTERNATIVE in case a of

5784N/A [] -> printDATATYPE_DECL (Datatype_decl s [emptyAnno $ Subsorts [s] r] r)

5784N/A h : t -> sep [idLabelDoc s, colon <> colon <> sep

5784N/A ((equals <+> pa h) :

5784N/A map ((bar <+>) . pa) t)]

5784N/A

5784N/Ainstance Pretty DATATYPE_DECL where

5784N/A pretty = printDATATYPE_DECL

5784N/A

5784N/AprintCOMPONENTS :: COMPONENTS ->Doc

5784N/AprintCOMPONENTS c = case c of

5784N/A Cons_select k l s _ -> fsep $ punctuate comma (map idLabelDoc l)

5784N/A ++ [case k of

5784N/A Total -> colon

5784N/A Partial -> colon <> quMarkD, idDoc s]

5784N/A Sort s -> idDoc s

5784N/A

5784N/Ainstance Pretty COMPONENTS where

5784N/A pretty = printCOMPONENTS

5784N/A

5784N/AprintALTERNATIVE :: ALTERNATIVE ->Doc

5784N/AprintALTERNATIVE a = case a of

5784N/A Alt_construct k n l _ -> case l of

5784N/A [] -> idLabelDoc n

5784N/A _ -> idLabelDoc n <>

5784N/A parens ( sep $ punctuate semi $ map printCOMPONENTS l)

5784N/A <> case k of

5784N/A Total -> empty

5784N/A Partial -> quMarkD

5784N/A Subsorts l _ -> fsep $ text (sortS ++ pluralS l)

5784N/A : punctuate comma (map idDoc l)

5784N/A

5784N/Ainstance Pretty ALTERNATIVE where

5784N/A pretty = printALTERNATIVE

5784N/A

5784N/AprintSortItem :: (f -> Doc) -> SORT_ITEM f -> Doc

5784N/AprintSortItem mf si = case si of

5784N/A Sort_decl sl _ -> sepByCommas $ map idLabelDoc sl

5784N/A Subsort_decl sl sup _ ->

5784N/A fsep $ punctuate comma (map idDoc sl) ++ [less, idDoc sup]

5784N/A Subsort_defn s v sup af _ -> fsep [idLabelDoc s, equals,

5784N/A specBraces $ fsep [sidDoc v, colon <+> idDoc sup,

5784N/A printAnnoted (addBullet . printFormula mf) af]]

5784N/A Iso_decl sl _ -> fsep $ punctuate (space <> equals) $ map idDoc sl

5784N/A

5784N/Ainstance Pretty f => Pretty (SORT_ITEM f) where

5784N/A pretty = printSortItem pretty

5784N/A

5784N/AprintQuant :: QUANTIFIER -> Doc

5784N/AprintQuant q = case q of

5784N/A Universal -> forallDoc

5784N/A Existential -> exists

5784N/A Unique_existential -> unique

5784N/A

5784N/AprintSortedVars :: [VAR] -> SORT -> Doc

5784N/AprintSortedVars l s =

5784N/A fsep $ punctuate comma (map sidDoc l) ++ [colon <+> idDoc s]

5784N/A

5784N/AprintVarDecl :: VAR_DECL -> Doc

5784N/AprintVarDecl (Var_decl l s _) = printSortedVars l s

5784N/A

5784N/AprintArgDecl :: ARG_DECL -> Doc

5784N/AprintArgDecl (Arg_decl l s _) = printSortedVars l s

5784N/A

5784N/AprintArgDecls :: [ARG_DECL] -> Doc

5784N/AprintArgDecls = parens . fsep . punctuate semi . map printArgDecl

5784N/A

5784N/AprintPredHead :: PRED_HEAD -> Doc

5784N/AprintPredHead (Pred_head l _) = printArgDecls l

5784N/A

5784N/AprintPredItem :: (f -> Doc) -> PRED_ITEM f -> Doc

5784N/AprintPredItem mf p = case p of

5784N/A Pred_decl l t _ -> fsep $ punctuate comma (map idLabelDoc l)

5784N/A ++ [colon <+> printPredType t]

5784N/A Pred_defn i h f _ ->

5784N/A sep[ cat [idLabelDoc i, printPredHead h]

5784N/A , equiv <+> printAnnoted (printFormula mf) f]

5784N/A

5784N/Ainstance Pretty f => Pretty (PRED_ITEM f) where

5784N/A pretty = printPredItem pretty

5784N/A

5784N/A

5784N/AprintAttr :: (f -> Doc) -> OP_ATTR f -> Doc

5784N/AprintAttr mf a = case a of

5784N/A Assoc_op_attr -> text assocS

5784N/A Comm_op_attr -> text commS

5784N/A Idem_op_attr -> text idemS

5784N/A Unit_op_attr t -> text unitS <+> printTerm mf t

5784N/A

5784N/Ainstance Pretty f => Pretty (OP_ATTR f) where

5784N/A pretty = printAttr pretty

5784N/A

5784N/AprintOpHead :: OP_HEAD -> Doc

5784N/AprintOpHead (Op_head k l r _) =

5784N/A sep $ (if null l then [] else [printArgDecls l]) ++

5784N/A [ (case k of

5784N/A Total -> colon

5784N/A Partial -> text colonQuMark) <+> idDoc r]

5784N/A

5784N/Ainstance Pretty OP_HEAD where

5784N/A pretty = printOpHead

5784N/A

5784N/AprintOpItem :: (f -> Doc) -> OP_ITEM f -> Doc

5784N/AprintOpItem mf p = case p of

5784N/A Op_decl l t a _ -> fsep $ punctuate comma (map idLabelDoc l)

5784N/A ++ [colon <> (if null a then id else (<> comma))(printOpType t)]

5784N/A ++ punctuate comma (map (printAttr mf) a)

5784N/A Op_defn i h@(Op_head _ l _ _) t _ ->

5784N/A sep [ (if null l then sep else cat) [idLabelDoc i, printOpHead h]

5784N/A , equals <+> printAnnoted (printTerm mf) t]

5784N/A

5784N/Ainstance Pretty f => Pretty (OP_ITEM f) where

5784N/A pretty = printOpItem pretty

5784N/A

5784N/Ainstance Pretty VAR_DECL where

5784N/A pretty = printVarDecl

5784N/A

5784N/AprintOpType :: OP_TYPE -> Doc

5784N/AprintOpType (Op_type p l r _) =

5784N/A case l of

5784N/A [] -> case p of

5784N/A Partial -> quMarkD <+> idDoc r

5784N/A Total -> space <> idDoc r

5784N/A _ -> space <> fsep

5784N/A (punctuate (space <> cross) (map idDoc l)

5784N/A ++ [case p of

5784N/A Partial -> pfun

5784N/A Total -> funArrow,

5784N/A idDoc r])

5784N/A

5784N/Ainstance Pretty OP_TYPE where

5784N/A pretty = printOpType

5784N/A

5784N/AprintOpSymb :: OP_SYMB -> Doc

5784N/AprintOpSymb o = case o of

5784N/A Op_name i -> idDoc i

5784N/A Qual_op_name i t _ -> fsep [text opS, idDoc i, colon <> printOpType t]

5784N/A

5784N/Ainstance Pretty OP_SYMB where

5784N/A pretty = printOpSymb

5784N/A

5784N/AprintPredType :: PRED_TYPE -> Doc

5784N/AprintPredType (Pred_type l _) = case l of

5784N/A [] -> parens empty

5784N/A _ -> fsep $ punctuate (space <> cross) $ map idDoc l

5784N/A

5784N/Ainstance Pretty PRED_TYPE where

5784N/A pretty = printPredType

5784N/A

5784N/AprintPredSymb :: PRED_SYMB -> Doc

5784N/AprintPredSymb p = case p of

5784N/A Pred_name i -> idDoc i

5784N/A Qual_pred_name i t _ ->

5784N/A parens $ fsep [text predS, idDoc i, colon <+> printPredType t]

5784N/A

5784N/Ainstance Pretty PRED_SYMB where

5784N/A pretty = printPredSymb

5784N/A

5784N/Ainstance Pretty SYMB_ITEMS where

5784N/A pretty = printSymbItems

5784N/A

5784N/AprintSymbItems :: SYMB_ITEMS -> Doc

5784N/AprintSymbItems (Symb_items k l _) =

5784N/A print_kind_text k l <+> sepByCommas (map printSymb l)

5784N/A

5784N/Ainstance Pretty SYMB where

5784N/A pretty = printSymb

5784N/A

5784N/AprintSymb :: SYMB -> Doc

5789N/AprintSymb s = case s of

5784N/A Symb_id i -> idDoc i

5784N/A Qual_id i t _ -> fsep [idDoc i, colon <> printType t]

5784N/A

5784N/Ainstance Pretty TYPE where

5784N/A pretty = printType

5784N/A

5784N/AprintType :: TYPE -> Doc

5784N/AprintType t = case t of

5784N/A O_type ot -> printOpType ot

5784N/A P_type pt -> space <> printPredType pt

5784N/A A_type s -> space <> idDoc s

5784N/A

5784N/Aprint_kind_text :: SYMB_KIND -> [a] -> Doc

5784N/Aprint_kind_text k l = case k of

5784N/A Implicit -> empty

5784N/A _ -> keyword (pluralS_symb_list k l)

5784N/A

5784N/ApluralS_symb_list :: SYMB_KIND -> [a] -> String

5784N/ApluralS_symb_list k l = (case k of

5784N/A Implicit -> error "pluralS_symb_list"

5784N/A Sorts_kind -> sortS

5784N/A OtherKinds s -> s

5784N/A Ops_kind -> opS

5784N/A Preds_kind -> predS) ++ (if isSingle l then "" else "s")

5784N/A

5784N/Ainstance Pretty SYMB_OR_MAP where

5784N/A pretty = printSymbOrMap

5784N/A

5784N/AprintSymbOrMap :: SYMB_OR_MAP -> Doc

5784N/AprintSymbOrMap som = case som of

5784N/A Symb s -> printSymb s

5784N/A Symb_map s t _ -> fsep [printSymb s, mapsto <+> printSymb t]

5784N/A

5784N/Ainstance Pretty SYMB_KIND where

5784N/A pretty = printSymbKind

5784N/A

5784N/AprintSymbKind :: SYMB_KIND -> Doc

5784N/AprintSymbKind sk = print_kind_text sk [()]

5784N/A

5784N/Ainstance Pretty SYMB_MAP_ITEMS where

5784N/A pretty = printSymbMapItems

5784N/A

5784N/AprintSymbMapItems :: SYMB_MAP_ITEMS -> Doc

5784N/AprintSymbMapItems (Symb_map_items k l _) =

5784N/A print_kind_text k l <+> sepByCommas (map printSymbOrMap l)

5784N/A

5784N/AprintRecord :: (f -> Doc) -> Record f Doc Doc

5784N/AprintRecord mf = Record

5784N/A { foldQuantification = \ _ q l r _ ->

5784N/A fsep $ printQuant q : punctuate semi (map printVarDecl l)

5784N/A ++ [addBullet r]

5784N/A , foldConjunction = \ (Conjunction ol _) l _ -> case ol of

5784N/A [] -> text trueS

5784N/A _ -> fsep $ prepPunctuate (andDoc <> space)

5784N/A $ zipWith (mkJunctDoc True) (init ol) (init l) ++

5784N/A [mkJunctDoc False (last ol) (last l)]

5784N/A , foldDisjunction = \ (Disjunction ol _) l _ -> case ol of

5784N/A [] -> text falseS

5784N/A _ -> fsep $ prepPunctuate (orDoc <> space)

5784N/A $ zipWith (mkJunctDoc True) (init ol) (init l) ++

5784N/A [mkJunctDoc False (last ol) (last l)]

5784N/A , foldImplication = \ (Implication oL oR b _) l r _ _ ->

5784N/A let nl = if isAnyImpl oL || b && isQuant oL

5784N/A then parens l else l

5784N/A nr = if isImpl b oR || not b && isQuant oR

5784N/A then parens r else r

5784N/A in if b then sep [nl, hsep [implies, nr]]

5784N/A else sep [nr, hsep [text ifS, nl]]

5784N/A , foldEquivalence = \ (Equivalence oL oR _) l r _ ->

5784N/A sep [if isQuant oL then parens l else

5784N/A mkEquivDoc oL l, hsep [equiv, mkEquivDoc oR r]]

5784N/A , foldNegation = \ (Negation o _) r _ ->

5784N/A hsep [notDoc, mkJunctDoc False o r]

5784N/A , foldTrue_atom = \ _ _ -> text trueS

5784N/A , foldFalse_atom = \ _ _ -> text falseS

5784N/A , foldPredication = \ (Predication _ ol _) p l _ -> case p of

5784N/A Pred_name i -> predIdApplDoc i $ zipConds ol l

5784N/A Qual_pred_name _ _ _ -> if null l then printPredSymb p else

5784N/A fcat [printPredSymb p, parens $ sepByCommas l]

5784N/A , foldDefinedness = \ _ r _ -> hsep [text defS, r]

5784N/A , foldExistl_equation = \ _ l r _ -> sep [l, hsep[exequal, r]]

5784N/A , foldStrong_equation = \ _ l r _ -> sep [l, hsep [equals, r]]

5784N/A , foldMembership = \ _ r t _ -> fsep [r, inDoc, idDoc t]

5784N/A , foldMixfix_formula = \ _ r -> r

5784N/A , foldSort_gen_ax = \ (Sort_gen_ax constrs b) _ _ ->

5784N/A let l = recoverType constrs

5784N/A genAx = sep [ keyword generatedS <+> keyword (typeS ++ pluralS l)

5784N/A , semiAnnos printDATATYPE_DECL l]

5784N/A in if b then text "%% free" $+$ genAx else genAx

5784N/A , foldQuantOp = \ _ o n r -> fsep

5784N/A [ forallDoc

5784N/A , printOpSymb $ Qual_op_name o n nullRange

5784N/A , addBullet r ]

5784N/A , foldQuantPred = \ _ p n r -> fsep

5784N/A [ forallDoc

5784N/A , printPredSymb $ Qual_pred_name p n nullRange

5784N/A , addBullet r ]

5784N/A , foldExtFORMULA = const mf

5784N/A , foldQual_var = \ _ v s _ ->

5784N/A parens $ fsep [text varS, sidDoc v, colon <+> idDoc s]

5784N/A , foldApplication = \ (Application _ ol _) o l _ -> case o of

5784N/A Op_name i -> idApplDoc i $ zipConds ol l

5784N/A Qual_op_name _ _ _ -> let d = parens $ printOpSymb o in

5784N/A if null l then d else fcat [d, parens $ sepByCommas l]

5784N/A , foldSorted_term = \ _ r t _ -> fsep[idApplDoc typeId [r], idDoc t]

5784N/A , foldCast = \ _ r t _ ->

5784N/A fsep[idApplDoc (mkId [placeTok, mkSimpleId asS]) [r], idDoc t]

5784N/A , foldConditional = \ (Conditional ol _ _ _) l f r _ ->

5784N/A fsep [if isCond ol then parens l else l,

5784N/A text whenS <+> f, text elseS <+> r]

5784N/A , foldMixfix_qual_pred = const printPredSymb

5784N/A , foldMixfix_term = \ (Mixfix_term ol) l -> case ol of

5784N/A [_, Mixfix_parenthesized _ _] -> fcat l

5784N/A _ -> fsep l

5784N/A , foldMixfix_token = const sidDoc

5784N/A , foldMixfix_sorted_term = \ _ s _ -> colon <+> idDoc s

5784N/A , foldMixfix_cast = \ _ s _ -> text asS <+> idDoc s

5784N/A , foldMixfix_parenthesized = \ _ l _ -> parens $ sepByCommas l

5784N/A , foldMixfix_bracketed = \ _ l _ -> brackets $ sepByCommas l

5784N/A , foldMixfix_braced = \ _ l _ -> specBraces $ sepByCommas l }

5784N/A

5784N/ArecoverType :: [Constraint] -> [Annoted DATATYPE_DECL]

5784N/ArecoverType =

5784N/A map (\ c -> let s = newSort c in emptyAnno $ Datatype_decl s

5789N/A (map (\ (o, _) -> case o of

5784N/A Qual_op_name i (Op_type fk args _ ps) r ->

5784N/A let qs = appRange ps r in emptyAnno $ case args of

5784N/A [_] | isInjName i -> Subsorts args qs

5784N/A _ -> Alt_construct fk i (map Sort args) qs

5784N/A _ -> error "CASL.recoverType") $ opSymbs c) nullRange)

5784N/A

5784N/AzipConds :: [TERM f] -> [Doc] -> [Doc]

5784N/AzipConds = zipWith (\ o d -> if isCond o then parens d else d)

5784N/A

5784N/AprintFormula :: (f -> Doc) -> FORMULA f -> Doc

5784N/AprintFormula = foldFormula . printRecord

5784N/A

5784N/Ainstance Pretty f => Pretty (FORMULA f) where

5784N/A pretty = printFormula pretty

5784N/A

5784N/AprintTerm :: (f -> Doc) -> TERM f -> Doc

5784N/AprintTerm = foldTerm . printRecord

5784N/A

5784N/Ainstance Pretty f => Pretty (TERM f) where

5784N/A pretty = printTerm pretty

5789N/A

5784N/AisQuant :: FORMULA f -> Bool

5784N/AisQuant f = case f of

5784N/A Quantification _ _ _ _ -> True

5784N/A ExtFORMULA _ -> True

5784N/A Conjunction l _ -> case l of

5784N/A [] -> False

5784N/A _ -> isQuant $ last l

5784N/A Disjunction l _ -> case l of

5784N/A [] -> False

5784N/A _ -> isQuant $ last l

5784N/A Implication a b impl _ -> isQuant $ if impl then b else a

5784N/A Equivalence _ b _ -> isQuant b

5784N/A Negation a _ -> isQuant a

5784N/A _ -> False

5784N/A

5784N/AisEquiv :: FORMULA f -> Bool

5784N/AisEquiv f = case f of

5784N/A Equivalence _ _ _ -> True

5784N/A _ -> False

5784N/A

5784N/AisAnyImpl :: FORMULA f -> Bool

5784N/AisAnyImpl f = isImpl True f || isImpl False f

isJunct :: FORMULA f -> Bool

isJunct f = case f of

Conjunction _ _ -> True

Disjunction _ _ -> True

_ -> isAnyImpl f

-- true for non-final

mkJunctDoc :: 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 :: Bool -> FORMULA f -> Bool

isImpl a f = case f of

Implication _ _ b _ -> a /= b

_ -> isEquiv f

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 a list with elements in class ListCheck for a list

-- greater than zero. It returns an empty String if the list and all

-- nested lists have only one element. If the list or an nested list

-- has more than one element a String containig one "s" is returned.

pluralS :: ListCheck a => a -> String

pluralS l = if isSingle $ innerList 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 _ _) = [()]

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 DATATYPE_DECL where

innerList (Datatype_decl _ _ _) = [()]

instance ListCheck VAR_DECL where

innerList (Var_decl l _ _) = innerList l

-- | print a formula as a sentence

printTheoryFormula :: Pretty f => Named (FORMULA f) -> Doc

printTheoryFormula f = printAnnoted

((case sentence f of

Quantification Universal _ _ _ -> id

Sort_gen_ax _ _ -> id

_ -> (bullet <+>)) . pretty) $ fromLabelledSen f