PrintAs.hs

{- |
Module      :  ./HasCASL/PrintAs.hs
Description :  print the abstract syntax so that it can be re-parsed
Copyright   :  (c) Christian Maeder and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

printing data types of the abstract syntax
-}

module HasCASL.PrintAs where

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.FoldTerm
import HasCASL.Builtin

import Common.Id
import Common.Keywords
import Common.DocUtils
import Common.Doc
import Common.AS_Annotation

import qualified Data.Set as Set
import Data.List

-- | short cut for: if b then empty else d
noPrint :: Bool -> Doc -> Doc
noPrint b d = if b then empty else d

noNullPrint :: [a] -> Doc -> Doc
noNullPrint = noPrint . null

semiDs :: Pretty a => [a] -> Doc
semiDs = fsep . punctuate semi . map pretty

semiAnnoted :: Pretty a => [Annoted a] -> Doc
semiAnnoted = vcat . map (printSemiAnno pretty True)

instance Pretty Variance where
    pretty = sidDoc . mkSimpleId . show

instance Pretty a => Pretty (AnyKind a) where
    pretty knd = case knd of
        ClassKind ci -> pretty ci
        FunKind v k1 k2 _ -> fsep
            [ pretty v <> (case k1 of
                FunKind {} -> parens
                _ -> id) (pretty k1)
            , funArrow, pretty k2]

varOfTypeArg :: TypeArg -> Id
varOfTypeArg (TypeArg i _ _ _ _ _ _) = i

instance Pretty TypePattern where
    pretty tp = case tp of
        TypePattern name@(Id ts cs _) args _ ->
          let ds = map (pretty . varOfTypeArg) args in
            if placeCount name == length args then
                let (ras, dts) = mapAccumL ( \ l t -> if isPlace t then
                          case l of
                            x : r -> (r, x)
                            _ -> error "Pretty TypePattern"
                          else (l, printTypeToken t)) ds ts
                in fsep $ dts ++ (if null cs then [] else
                        [brackets $ sepByCommas $ map printTypeId cs])
                       ++ ras
            else printTypeId name <+> fsep ds
        TypePatternToken t -> printTypeToken t
        MixfixTypePattern ts -> fsep $ map pretty ts
        BracketTypePattern k l _ -> bracket k $ ppWithCommas l
        TypePatternArg t _ -> parens $ pretty t

-- | put proper brackets around a document
bracket :: BracketKind -> Doc -> Doc
bracket b = case b of
    Parens -> parens
    Squares -> brackets
    Braces -> specBraces
    NoBrackets -> id

-- | print a 'Kind' plus a preceding colon (or nothing)
printKind :: Kind -> Doc
printKind k = noPrint (k == universe) $ printVarKind NonVar (VarKind k)

-- | print the kind of a variable with its variance and a preceding colon
printVarKind :: Variance -> VarKind -> Doc
printVarKind e vk = case vk of
    Downset t -> less <+> pretty t
    VarKind k -> colon <+> pretty e <> pretty k
    MissingKind -> empty

data TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix
    deriving (Eq, Ord)

parenPrec :: TypePrec -> (TypePrec, Doc) -> Doc
parenPrec p1 (p2, d) = if p2 < p1 then d else parens d

printTypeToken :: Token -> Doc
printTypeToken t = let
  l = ("*", cross) : map ( \ (a, d) -> (show a, d) )
    [ (FunArr, funArrow)
    , (PFunArr, pfun)
    , (ContFunArr, cfun)
    , (PContFunArr, pcfun) ]
  in case lookup (tokStr t) l of
       Just d -> d
       _ -> pretty t

printTypeId :: Id -> Doc
printTypeId (Id ts cs _) = let (toks, pls) = splitMixToken ts in
   fcat $ map printTypeToken toks
   ++ (if null cs then [] else [brackets $ sepByCommas $ map printTypeId cs])
   ++ map printTypeToken pls

toMixType :: Type -> (TypePrec, Doc)
toMixType typ = case typ of
    TypeName name _ _ -> (Outfix, printTypeId name)
    TypeToken tt -> (Outfix, printTypeToken tt)
    TypeAbs v t _ ->
        (Absfix, sep [ lambda <+> pretty v, bullet <+> snd (toMixType t)])
    ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type
    BracketType k l _ ->
        (Outfix, bracket k $ sepByCommas $ map (snd . toMixType) l)
    KindedType t kind _ -> (Lazyfix, sep
      [ parenPrec Lazyfix $ toMixType t
      , colon <+> printList0 (Set.toList kind)])
    MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)
    TypeAppl t1 t2 -> let
        (topTy, tyArgs) = getTypeApplAux False typ
        aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1
                             , parenPrec Prefix $ toMixType t2 ])
         in case topTy of
      TypeName name@(Id ts cs _) _k _i ->
        case map toMixType tyArgs of
          [dArg] -> case ts of
               [e] | name == lazyTypeId ->
                   (Lazyfix, pretty e <+> parenPrec Lazyfix dArg)
               [e1, e2, e3] | not (isPlace e1) && isPlace e2
                              && not (isPlace e3) && null cs ->
                   (Outfix, fsep [pretty e1, snd dArg, pretty e3])
               _ -> aArgs
          [dArg1, dArg2] -> case ts of
               [_, e2, _] | isInfix name && null cs ->
                  if tokStr e2 == prodS then
                    (ProdInfix, fsep
                     [ parenPrec ProdInfix dArg1
                     , cross, parenPrec ProdInfix dArg2])
                  else -- assume fun type
                  (FunInfix, fsep
                   [ parenPrec FunInfix dArg1
                   , printTypeToken e2, snd dArg2])
               _ -> aArgs
          dArgs -> if isProductIdWithArgs name $ length tyArgs then
              (ProdInfix, fsep $ punctuate (space <> cross) $
               map (parenPrec ProdInfix) dArgs) else aArgs
      _ -> aArgs

instance Pretty Type where
    pretty = snd . toMixType

printTypeScheme :: PolyId -> TypeScheme -> Doc
printTypeScheme (PolyId _ tys _) (TypeScheme vs t _) =
    let tdoc = pretty t in
    if null vs || not (null tys) then tdoc else
        fsep [forallDoc, semiDs vs, bullet <+> tdoc]

-- no curried notation for bound variables
instance Pretty TypeScheme where
    pretty = printTypeScheme (PolyId applId [] nullRange)

instance Pretty Partiality where
    pretty p = case p of
        Partial -> quMarkD
        Total -> empty

instance Pretty Quantifier where
    pretty q = case q of
        Universal -> forallDoc
        Existential -> exists
        Unique -> unique

instance Pretty TypeQual where
    pretty q = case q of
        OfType -> colon
        AsType -> text asS
        InType -> inDoc
        Inferred -> colon

instance Pretty Term where
    pretty = printTerm . rmSomeTypes

isSimpleTerm :: Term -> Bool
isSimpleTerm trm = case trm of
    QualVar _ -> True
    QualOp {} -> True
    ResolvedMixTerm {} -> True
    ApplTerm {} -> True
    TupleTerm _ _ -> True
    TermToken _ -> True
    BracketTerm {} -> True
    _ -> False

-- | used only to produce CASL applications
isSimpleArgTerm :: Term -> Bool
isSimpleArgTerm trm = case trm of
    QualVar vd -> not (isPatVarDecl vd)
    QualOp {} -> True
    ResolvedMixTerm n _ l _ -> placeCount n /= 0 || not (null l)
    TupleTerm _ _ -> True
    BracketTerm {} -> True
    _ -> False

hasRightQuant :: Term -> Bool
hasRightQuant t = case t of
    QuantifiedTerm {} -> True
    LambdaTerm {} -> True
    CaseTerm {} -> True
    LetTerm Let _ _ _ -> True
    ResolvedMixTerm n _ ts _ | endPlace n && placeCount n == length ts
        -> hasRightQuant (last ts)
    ApplTerm (ResolvedMixTerm n _ [] _) t2 _ | endPlace n ->
        case t2 of
          TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)
          _ -> hasRightQuant t2
    ApplTerm _ t2 _ -> hasRightQuant t2
    _ -> False

zipArgs :: Id -> [Term] -> [Doc] -> [Doc]
zipArgs n ts ds = case (ts, ds) of
    (t : r, d : s) -> let
        p = parenTermDoc t d
        e = if hasRightQuant t then parens d else p
        in if null r && null s && endPlace n then
               [if hasRightQuant t then d else p]
           else e : zipArgs n r s
    _ -> []

isPatVarDecl :: VarDecl -> Bool
isPatVarDecl (VarDecl v ty _ _) = case ty of
           TypeName t _ _ -> isSimpleId v && isPrefixOf "_v" (show t)
           _ -> False

parenTermDoc :: Term -> Doc -> Doc
parenTermDoc trm = if isSimpleTerm trm then id else parens

printTermRec :: FoldRec Doc (Doc, Doc)
printTermRec = FoldRec
    { foldQualVar = \ _ vd@(VarDecl v _ _ _) ->
         if isPatVarDecl vd then pretty v
         else parens $ keyword varS <+> pretty vd
    , foldQualOp = \ _ br n t tys k _ ->
        (if null tys || k == Infer then id else
          (<> brackets (ppWithCommas tys))) $
          parens $ fsep [pretty br, pretty n, colon, printTypeScheme n $
                         if isPred br then unPredTypeScheme t else t]
    , foldResolvedMixTerm = \ rt n@(Id toks cs ps) tys ts _ ->
          let pn = placeCount n
              ResolvedMixTerm _ _ os _ = rt
              ds = zipArgs n os ts
          in if pn == length ts || null ts then
            if null tys then idApplDoc n ds
            else let (ftoks, _) = splitMixToken toks
                     fId = Id ftoks cs ps
                     (fts, rts) = splitAt (placeCount fId) $ if null ts
                          then replicate pn $ pretty placeTok else ds
                 in fsep $ (idApplDoc fId fts <> brackets (ppWithCommas tys))
                    : rts
          else idApplDoc applId [idDoc n, parens $ sepByCommas ts]
    , foldApplTerm = \ ot t1 t2 _ ->
        case ot of
          -- comment out the following two guards for CASL applications
          ApplTerm (ResolvedMixTerm n _ [] _) (TupleTerm ts@(_ : _) _) _
              | placeCount n == length ts ->
                  idApplDoc n (zipArgs n ts $ map printTerm ts)
          ApplTerm (ResolvedMixTerm n _ [] _) o2 _ | placeCount n == 1
            -> idApplDoc n $ zipArgs n [o2] [t2]
          ApplTerm o1 o2 _
            -> idApplDoc applId $ zipArgs applId [o1, o2] [t1, t2]
          _ -> error "printTermRec.foldApplTerm"
     , foldTupleTerm = \ _ ts _ -> parens $ sepByCommas ts
     , foldTypedTerm = \ ~(TypedTerm ot _ _ _) t q typ _ -> fsep [(case ot of
           TypedTerm {} | elem q [Inferred, OfType] -> parens
           ApplTerm (ResolvedMixTerm n _ [] _) arg _ ->
             let pn = placeCount n in case arg of
               TupleTerm ts@(_ : _) _ | pn == length ts -> parens
               _ | pn == 1 || hasRightQuant ot -> parens
               _ -> id
           _ | hasRightQuant ot -> parens
           _ -> id) t, pretty q, pretty typ]
     , foldQuantifiedTerm = \ _ q vs t _ ->
           fsep [pretty q, printGenVarDecls vs, bullet <+> t]
     , foldLambdaTerm = \ ot ps q t _ ->
            let LambdaTerm ops _ _ _ = ot in
            fsep [ lambda
                 , case ops of
                      [p] -> case p of
                          TupleTerm [] _ -> empty
                          QualVar vd@(VarDecl v ty _ _) ->
                              pretty v <+> if isPatVarDecl vd then empty
                                     else printVarDeclType ty
                          _ -> head ps
                      _ -> if all ( \ p -> case p of
                                QualVar vd -> not $ isPatVarDecl vd
                                _ -> False) ops
                           then printGenVarDecls $ map
                                (\ pt -> let QualVar vd = pt in GenVarDecl vd)
                                ops
                           else fcat $ map parens ps
                 , (case q of
                     Partial -> bullet
                     Total -> bullet <> text exMark) <+> t]
     , foldCaseTerm = \ _ t es _ ->
            fsep [text caseS, t, text ofS,
                  cat $ punctuate (space <> bar <> space) $
                       map (printEq0 funArrow) es]
     , foldLetTerm = \ _ br es t _ ->
            let des = sep $ punctuate semi $ map (printEq0 equals) es
                in case br of
                Let -> fsep [sep [text letS <+> des, text inS], t]
                Where -> fsep [sep [t, text whereS], des]
                Program -> text programS <+> des
     , foldTermToken = const pretty
     , foldMixTypeTerm = \ _ q t _ -> pretty q <+> pretty t
     , foldMixfixTerm = const fsep
     , foldBracketTerm = \ _ k l _ -> bracket k $ sepByCommas l
     , foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->
           fsep [pretty v, text asP, p]
     , foldProgEq = \ _ p t _ -> (p, t) }

printTerm :: Term -> Doc
printTerm = foldTerm printTermRec

rmTypeRec :: MapRec
rmTypeRec = mapRec
    { foldQualOp = \ t _ (PolyId i _ _) _ tys k ps ->
        if elem i $ map fst bList then ResolvedMixTerm i
           (if k == Infer then [] else tys) [] ps else t
    , foldTypedTerm = \ _ nt q ty ps -> case q of
        Inferred -> nt
        _ -> case nt of
          TypedTerm tt oq oty _ | oty == ty || oq == InType ->
            if q == AsType then TypedTerm tt q ty ps else nt
          QualVar (VarDecl _ oty _ _) | oty == ty -> nt
          _ -> TypedTerm nt q ty ps }

rmSomeTypes :: Term -> Term
rmSomeTypes = foldTerm rmTypeRec

-- | put parenthesis around applications
parenTermRec :: MapRec
parenTermRec = let
     addParAppl t = case t of
           ResolvedMixTerm _ _ [] _ -> t
           QualVar _ -> t
           QualOp {} -> t
           TermToken _ -> t
           BracketTerm {} -> t
           TupleTerm _ _ -> t
           _ -> TupleTerm [t] nullRange
     in mapRec
    { foldApplTerm = \ _ t1 t2 ->
         ApplTerm (addParAppl t1) (addParAppl t2)
    , foldResolvedMixTerm = \ _ n tys ->
        ResolvedMixTerm n tys . map addParAppl
    , foldTypedTerm = \ _ ->
        TypedTerm . addParAppl
    , foldMixfixTerm = \ _ -> MixfixTerm . map addParAppl
    , foldAsPattern = \ _ v -> AsPattern v . addParAppl
    }

parenTerm :: Term -> Term
parenTerm = foldTerm parenTermRec

-- | print an equation with different symbols between pattern and term
printEq0 :: Doc -> (Doc, Doc) -> Doc
printEq0 s (p, t) = sep [p, hsep [s, t]]

printGenVarDecls :: [GenVarDecl] -> Doc
printGenVarDecls = fsep . punctuate semi . map
  ( \ l -> case l of
     [x] -> pretty x
     GenVarDecl (VarDecl _ t _ _) : _ -> sep
       [ ppWithCommas
         $ map (\ g -> let GenVarDecl (VarDecl v _ _ _) = g in v) l
       , printVarDeclType t]
     GenTypeVarDecl (TypeArg _ e c _ _ _ _) : _ -> sep
       [ ppWithCommas
         $ map (\ g -> let GenTypeVarDecl v = g in varOfTypeArg v) l
       , printVarKind e c]
     _ -> error "printGenVarDecls") . groupBy sameType

sameType :: GenVarDecl -> GenVarDecl -> Bool
sameType g1 g2 = case (g1, g2) of
    (GenVarDecl (VarDecl _ t1 Comma _), GenVarDecl (VarDecl _ t2 _ _))
      | t1 == t2 -> True
    (GenTypeVarDecl (TypeArg _ e1 c1 _ _ Comma _),
     GenTypeVarDecl (TypeArg _ e2 c2 _ _ _ _)) | e1 == e2 && c1 == c2 -> True
    _ -> False

printVarDeclType :: Type -> Doc
printVarDeclType t = case t of
       MixfixType [] -> empty
       _ -> colon <+> pretty t

instance Pretty VarDecl where
    pretty (VarDecl v t _ _) = pretty v <+> printVarDeclType t

instance Pretty GenVarDecl where
    pretty gvd = case gvd of
        GenVarDecl v -> pretty v
        GenTypeVarDecl tv -> pretty tv

instance Pretty TypeArg where
    pretty (TypeArg v e c _ _ _ _) =
        pretty v <+> printVarKind e c

-- | don't print an empty list and put parens around longer lists
printList0 :: (Pretty a) => [a] -> Doc
printList0 l = case l of
    [] -> empty
    [x] -> pretty x
    _ -> parens $ ppWithCommas l

instance Pretty BasicSpec where
    pretty (BasicSpec l) = if null l then specBraces empty else
        changeGlobalAnnos addBuiltins . vcat $ map pretty l

instance Pretty ProgEq where
    pretty (ProgEq p t ps) = printEq0 equals $ foldEq printTermRec
        $ ProgEq (rmSomeTypes p) (rmSomeTypes t) ps

instance Pretty BasicItem where
    pretty bi = case bi of
        SigItems s -> pretty s
        ProgItems l _ -> noNullPrint l $ sep [keyword programS, semiAnnoted l]
        ClassItems i l _ -> noNullPrint l $ let
            b = semiAnnos pretty l
            p = plClass l
            in case i of
            Plain -> topSigKey (classS ++ if p then "es" else "") <+> b
            Instance -> sep [keyword classS <+>
                             keyword (instanceS ++ if p then sS else ""), b]
        GenVarItems l _ -> topSigKey (varS ++ pluralS l) <+> printGenVarDecls l
        FreeDatatype l _ -> sep
            [ keyword freeS <+> keyword (typeS ++ pluralS l)
            , semiAnnos pretty l]
        GenItems l _ -> let gkw = keyword generatedS in
            (if all (isDatatype . item) l then \ i -> gkw <+> rmTopKey i
             else \ i -> sep [gkw, specBraces i])
             $ vcat $ map (printAnnoted pretty) l
        AxiomItems vs fs _ -> sep
            [ if null vs then empty else forallDoc <+> printGenVarDecls vs
           , case fs of
             [] -> empty
             _ -> let pp = addBullet . pretty in
               vcat $ map (printAnnoted pp) (init fs)
                    ++ [printSemiAnno pp True $ last fs]]
        Internal l _ -> sep
            [ keyword internalS
            , specBraces $ vcat $ map (printAnnoted pretty) l]

plClass :: [Annoted ClassItem] -> Bool
plClass l = case map item l of
    _ : _ : _ -> True
    [ClassItem (ClassDecl (_ : _ : _) _ _) _ _] -> True
    _ -> False

pluralS :: [a] -> String
pluralS l = case l of
    _ : _ : _ -> sS
    _ -> ""

isDatatype :: SigItems -> Bool
isDatatype si = case si of
    TypeItems _ l _ -> all
      ((\ t -> case t of
        Datatype _ -> True
        _ -> False) . item) l
    _ -> False

instance Pretty OpBrand where
    pretty = keyword . show

instance Pretty SigItems where
    pretty si = case si of
        TypeItems i l _ -> noNullPrint l $
          let b = semiAnnos pretty l in case i of
            Plain -> topSigKey (typeS ++ plTypes l) <+> b
            Instance ->
              sep [keyword typeS <+> keyword (instanceS ++ plTypes l), b]
        OpItems b l _ -> noNullPrint l $ topSigKey (show b ++ plOps l)
            <+> let po = prettyOpItem $ isPred b in
                if case item $ last l of
                  OpDecl _ _ a@(_ : _) _ -> case last a of
                    UnitOpAttr {} -> True
                    _ -> False
                  OpDefn {} -> True
                  _ -> False
                then vcat (map (printSemiAnno po True) l)
                else semiAnnos po l

plTypes :: [Annoted TypeItem] -> String
plTypes l = case map item l of
    _ : _ : _ -> sS
    [TypeDecl (_ : _ : _) _ _] -> sS
    [SubtypeDecl (_ : _ : _) _ _] -> sS
    [IsoDecl (_ : _ : _) _] -> sS
    _ -> ""

plOps :: [Annoted OpItem] -> String
plOps l = case map item l of
    _ : _ : _ -> sS
    [OpDecl (_ : _ : _) _ _ _] -> sS
    _ -> ""

isSimpleTypeItem :: TypeItem -> Bool
isSimpleTypeItem ti = case ti of
    TypeDecl l k _ -> k == universe && all isSimpleTypePat l
    SubtypeDecl l (TypeName i _ _) _ ->
        not (isMixfix i) && all isSimpleTypePat l
    SubtypeDefn p (Var _) t _ _ ->
        isSimpleTypePat p && isSimpleType t
    _ -> False

isSimpleTypePat :: TypePattern -> Bool
isSimpleTypePat tp = case tp of
    TypePattern i [] _ -> not $ isMixfix i
    _ -> False

isSimpleType :: Type -> Bool
isSimpleType t = case t of
    TypeName i _ _ -> not $ isMixfix i
    TypeToken _ -> True
    MixfixType [TypeToken _, BracketType Squares (_ : _) _] -> True
    _ -> False

instance Pretty ClassItem where
    pretty (ClassItem d l _) = pretty d $+$ noNullPrint l
                   (specBraces $ vcat $ map (printAnnoted pretty) l)

instance Pretty ClassDecl where
    pretty (ClassDecl l k _) = let cs = ppWithCommas l in
        if k == universe then cs else fsep [cs, less, pretty k]

instance Pretty Vars where
    pretty vd = case vd of
        Var v -> pretty v
        VarTuple vs _ -> parens $ ppWithCommas vs

instance Pretty TypeItem where
    pretty ti = case ti of
        TypeDecl l k _ -> sep [ppWithCommas l, printKind k]
        SubtypeDecl l t _ ->
            fsep [ppWithCommas l, less, pretty t]
        IsoDecl l _ -> fsep $ punctuate (space <> equals) $ map pretty l
        SubtypeDefn p v t f _ ->
            fsep [pretty p, equals,
                  specBraces $ fsep
                  [pretty v, colon <+> pretty t, bullet <+> pretty f]]
        AliasType p _ (TypeScheme l t _) _ ->
            fsep $ pretty p : map (pretty . varOfTypeArg) l
                  ++ [text assignS <+> pretty t]
        Datatype t -> pretty t

printItScheme :: [PolyId] -> Bool -> TypeScheme -> Doc
printItScheme ps b = (case ps of
    [p] -> printTypeScheme p
    _ -> pretty) . (if b then unPredTypeScheme else id)

printHead :: [[VarDecl]] -> [Doc]
printHead = map ((<> space) . parens . printGenVarDecls . map GenVarDecl)

prettyOpItem :: Bool -> OpItem -> Doc
prettyOpItem b oi = case oi of
        OpDecl l t a _ -> fsep $ punctuate comma (map pretty l)
          ++ [colon <+>
              (if null a then id else (<> comma)) (printItScheme l b t)]
          ++ punctuate comma (map pretty a)
        OpDefn n ps s t _ -> fcat $
            (if null ps then (<> space) else id) (pretty n)
            : printHead ps
            ++ (if b then [] else [colon <+> printItScheme [n] b s <> space])
            ++ [(if b then equiv else equals) <> space, pretty t]

instance Pretty PolyId where
    pretty (PolyId i@(Id ts cs ps) tys _) = if null tys then pretty i else
      let (fts, plcs) = splitMixToken ts
      in idDoc (Id fts cs ps) <> brackets (ppWithCommas tys)
         <> hcat (map pretty plcs)

instance Pretty BinOpAttr where
    pretty a = text $ case a of
        Assoc -> assocS
        Comm -> commS
        Idem -> idemS

instance Pretty OpAttr where
    pretty oa = case oa of
        BinOpAttr a _ -> pretty a
        UnitOpAttr t _ -> text unitS <+> pretty t

instance Pretty DatatypeDecl where
    pretty (DatatypeDecl p k alts d _) =
        fsep [ pretty p, printKind k, defn
              <+> cat (punctuate (space <> bar <> space)
                      $ map pretty alts)
             , case d of
                 [] -> empty
                 _ -> keyword derivingS <+> ppWithCommas d]

instance Pretty Alternative where
    pretty alt = case alt of
        Constructor n cs p _ -> pretty n <+> fsep
          (map ( \ l -> case (l, p) of
-- comment out the following line to output real CASL
            ([NoSelector (TypeToken t)], Total) | isSimpleId n -> pretty t
            _ -> parens $ semiDs l) cs) <> pretty p
        Subtype l _ -> text typeS <+> ppWithCommas l

instance Pretty Component where
    pretty sel = case sel of
        Selector n _ t _ _ -> sep [pretty n, colon <+> pretty t]
        NoSelector t -> pretty t

instance Pretty Symb where
    pretty (Symb i mt _) =
        sep $ pretty i : case mt of
            Nothing -> []
            Just (SymbType t) -> [colon <+> pretty t]

instance Pretty SymbItems where
    pretty (SymbItems k syms _ _) =
        printSK k syms <+> ppWithCommas syms

instance Pretty SymbOrMap where
    pretty (SymbOrMap s mt _) =
        sep $ pretty s : case mt of
            Nothing -> []
            Just t -> [mapsto <+> pretty t]

instance Pretty SymbMapItems where
    pretty (SymbMapItems k syms _ _) =
        printSK k syms <+> ppWithCommas syms

-- | print symbol kind
printSK :: SymbKind -> [a] -> Doc
printSK k l = case k of
      Implicit -> empty
      _ -> keyword $ drop 3 (show k) ++ case l of
        _ : _ : _ -> sS
        _ -> ""