{- |

Module : $Header$

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

, appendS

, isJunct

, ListCheck (..)

, recoverType

, printALTERNATIVE

, typeString

, printVarDecl

, printVarDecls

, printSortItem

, printOpItem

, printPredItem

, printPredHead

, printAttr

) 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, Pretty f) => Pretty (BASIC_SPEC b s f) where

pretty = printBASIC_SPEC pretty pretty pretty

printBASIC_SPEC :: (b -> Doc) -> (s -> Doc) -> (f -> Doc)

-> BASIC_SPEC b s f -> Doc

printBASIC_SPEC fB fS fF (Basic_spec l) = case l of

[] -> specBraces empty

_ -> vcat $ map (printAnnoted (printBASIC_ITEMS fB fS fF)) l

instance (Pretty b, Pretty s, Pretty f) => Pretty (BASIC_ITEMS b s f) where

pretty = printBASIC_ITEMS pretty pretty pretty

typeString :: SortsKind -> [Annoted DATATYPE_DECL] -> String

typeString sk l = (case sk of

NonEmptySorts -> typeS

PossiblyEmptySorts -> etypeS) ++ appendS l

printBASIC_ITEMS :: (b -> Doc) -> (s -> Doc) -> (f -> Doc)

-> BASIC_ITEMS b s f -> Doc

printBASIC_ITEMS fB fS fF sis = case sis of

Sig_items s -> printSIG_ITEMS fS fF 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 fF) l]

Var_items l _ -> topSigKey (varS ++ pluralS l) <+> printVarDecls l

Local_var_axioms l f _ ->

fsep [fsep $ forallDoc : printVarDeclL l

, printAnnotedBulletFormulas fF f]

Axiom_items f _ -> printAnnotedBulletFormulas fF f

Ext_BASIC_ITEMS b -> fB b

printAnnotedBulletFormulas :: (f -> Doc) -> [Annoted (FORMULA f)] -> Doc

printAnnotedBulletFormulas fF l = vcat $ case l of

[] -> []

_ -> let pp = addBullet . printFormula fF in

map (printAnnoted pp) (init l)

++ [printSemiAnno pp False $ last l] -- use True for HasCASL

instance (Pretty s, Pretty f) => Pretty (SIG_ITEMS s f) where

pretty = printSIG_ITEMS pretty pretty

printSIG_ITEMS :: (s -> Doc) -> (f -> Doc) -> SIG_ITEMS s f -> Doc

printSIG_ITEMS fS fF sis = case sis of

Sort_items sk l _ -> topSigKey ((case sk of

NonEmptySorts -> sortS

PossiblyEmptySorts -> esortS) ++ pluralS l) <+>

semiAnnos (printSortItem fF) l

Op_items l _ -> topSigKey (opS ++ pluralS l) <+>

let pp = printOpItem fF 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 fF 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 :: (f -> Doc) -> SORT_ITEM f -> Doc

printSortItem mf 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 mf) af]]

Iso_decl sl _ -> fsep $ punctuate (space <> equals) $ map idDoc sl

instance Pretty f => Pretty (SORT_ITEM f) where

pretty = printSortItem pretty

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

printPredHead :: PRED_HEAD -> Doc

printPredHead (Pred_head l _) = printArgDecls l

printPredItem :: (f -> Doc) -> PRED_ITEM f -> Doc

printPredItem mf 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 mf) f]

instance Pretty f => Pretty (PRED_ITEM f) where

pretty = printPredItem pretty

printAttr :: (f -> Doc) -> OP_ATTR f -> Doc

printAttr mf 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 mf t

instance Pretty f => Pretty (OP_ATTR f) where

pretty = printAttr pretty

printOpHead :: OP_HEAD -> Doc

printOpHead (Op_head k l mr _) =

sep $ (if null l then [] else [printArgDecls 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 :: (f -> Doc) -> OP_ITEM f -> Doc

printOpItem mf 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 mf) a)

Op_defn i h@(Op_head _ l _ _) t _ ->

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

, equals <+> printAnnoted (printTerm mf) t]

instance Pretty f => Pretty (OP_ITEM f) where

pretty = printOpItem pretty

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) ++ (if isSingle l then "" else "s")

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]

printRecord :: (f -> Doc) -> Record f Doc Doc

printRecord mf = Record

{ foldQuantification = \ _ q l r _ ->

fsep $ printQuant q : printVarDeclL l

++ [addBullet r]

, foldConjunction = \ o l _ -> case o of

Conjunction ol@(_ : _) _ -> fsep $ prepPunctuate (andDoc <> space)

$ zipWith (mkJunctDoc True) (init ol) (init l) ++

[mkJunctDoc False (last ol) (last l)]

_ -> text trueS

, foldDisjunction = \ o l _ -> case o of

Disjunction ol@(_ : _) _ -> fsep $ prepPunctuate (orDoc <> space)

$ zipWith (mkJunctDoc True) (init ol) (init l) ++

[mkJunctDoc False (last ol) (last l)]

_ -> text falseS

, foldImplication = \ o l r _ _ ->

let Implication oL oR b _ = o

nl = if isAnyImpl oL || b && isQuant oL

then parens l else l

nr = if isImpl b oR || not b && isQuant oR

then parens r else r

in if b then printInfix True sep nl implies nr

else printInfix True sep nr (text ifS) nl

, foldEquivalence = \ o l r _ -> case o of

Equivalence oL oR _ -> printInfix True sep

(if isQuant oL then parens l else mkEquivDoc oL l)

equiv $ mkEquivDoc oR r

_ -> error "CASL.ToDoc.printRecord.foldEquivalence"

, foldNegation = \ orig r _ -> case orig of

Negation o _ -> hsep [notDoc, mkJunctDoc False o r]

_ -> error "CASL.ToDoc.printRecord.foldNegation"

, foldTrue_atom = \ _ _ -> text trueS

, foldFalse_atom = \ _ _ -> text 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]

, foldExistl_equation = \ _ l r _ -> printInfix True sep l exequal r

, foldStrong_equation = \ _ l r _ -> printInfix True sep l 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

, printOpSymb $ Qual_op_name o n nullRange

, addBullet r ]

, foldQuantPred = \ _ p n r -> fsep

[ forallDoc

, printPredSymb $ Qual_pred_name p n nullRange

, addBullet r ]

, foldExtFORMULA = const mf

, 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 mf }

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 :: (f -> Doc) -> FORMULA f -> Doc

printFormula = foldFormula . printRecord

instance Pretty f => Pretty (FORMULA f) where

pretty = printFormula pretty

printTerm :: (f -> Doc) -> TERM f -> Doc

printTerm = foldTerm . printRecord

instance Pretty f => Pretty (TERM f) where

pretty = printTerm pretty

isQuant :: FORMULA f -> Bool

isQuant f = case f of

Quantification _ _ _ _ -> True

ExtFORMULA _ -> True

Conjunction l _ -> case l of

[] -> False

_ -> isQuant $ last l

Disjunction l _ -> case l of

[] -> False

_ -> isQuant $ last l

Implication a b impl _ -> isQuant $ if impl then b else a

Equivalence _ b _ -> isQuant b

Negation a _ -> isQuant a

_ -> False

isEquiv :: FORMULA f -> Bool

isEquiv f = case f of

Equivalence _ _ _ -> True

_ -> False

isAnyImpl :: FORMULA f -> Bool

isAnyImpl 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 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 :: Pretty f => Named (FORMULA f) -> Doc

printTheoryFormula f = printAnnoted

((case sentence f of

Quantification Universal _ _ _ -> id

Sort_gen_ax _ _ -> id

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