{- |
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