076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : print the abstract syntax so that it can be re-parsed

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederStability : experimental

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maederprinting data types of the abstract syntax

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-}

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule HasCASL.PrintAs where

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.As

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.AsUtils

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.FoldTerm

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport HasCASL.Builtin

076b559b2ea7b2f1d303df992ae71cd6c6fe563cChristian Maederimport Common.Id

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport Common.Keywords

35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maederimport Common.DocUtils

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederimport Common.Doc

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederimport Common.AS_Annotation

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederimport Data.List (groupBy, mapAccumL)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder-- | short cut for: if b then empty else d

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaedernoPrint :: Bool -> Doc -> Doc

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaedernoPrint b d = if b then empty else d

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder

99f16a0f9ca757410960ff51a79b034503384fe2Christian MaedernoNullPrint :: [a] -> Doc -> Doc

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaedernoNullPrint = noPrint . null

99f16a0f9ca757410960ff51a79b034503384fe2Christian Maeder

6e5180855658f12f9059d9041f447bf0935de344Christian MaedersemiDs :: Pretty a => [a] -> Doc

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaedersemiDs = fsep . punctuate semi . map pretty

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder

76647324ed70f33b95a881b536d883daccf9568dChristian MaedersemiAnnoted :: Pretty a => [Annoted a] -> Doc

76647324ed70f33b95a881b536d883daccf9568dChristian MaedersemiAnnoted = vcat . map (printSemiAnno pretty True)

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

4e013227ed41ccd2e3d09dd44bedd651e1901f38Christian Maederinstance Pretty Variance where

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder pretty = sidDoc . mkSimpleId . show

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maederinstance Pretty a => Pretty (AnyKind a) where

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder pretty knd = case knd of

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder ClassKind ci -> pretty ci

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder FunKind v k1 k2 _ -> fsep [pretty v <>

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder (case k1 of

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder FunKind _ _ _ _ -> parens

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder _ -> id) (pretty k1)

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder , funArrow

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder , pretty k2]

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder

529f678f015ae5276f87da63114cdce750b366aeChristian MaedervarOfTypeArg :: TypeArg -> Id

529f678f015ae5276f87da63114cdce750b366aeChristian MaedervarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder

529f678f015ae5276f87da63114cdce750b366aeChristian Maederinstance Pretty TypePattern where

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder pretty tp = case tp of

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder TypePattern name@(Id ts cs _) args _ ->

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder let ds = map (pretty . varOfTypeArg) args in

8a1f427564a5ae2db32332512237ef645289c34dChristian Maeder if placeCount name == length args then

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder let (ras, dts) = mapAccumL ( \ l t -> if isPlace t then

b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder case l of

529f678f015ae5276f87da63114cdce750b366aeChristian Maeder x : r -> (r, x)

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder _ -> error "Pretty TypePattern"

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder else (l, printTypeToken t)) ds ts

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder in fsep $ dts ++ (if null cs then [] else

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder [brackets $ sepByCommas $ map printTypeId cs])

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder ++ ras

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder else printTypeId name <+> fsep ds

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder TypePatternToken t -> printTypeToken t

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder MixfixTypePattern ts -> fsep $ map pretty ts

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder TypePatternArg t _ -> parens $ pretty t

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder-- | put proper brackets around a document

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maederbracket :: BracketKind -> Doc -> Doc

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maederbracket b = case b of

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder Parens -> parens

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder Squares -> brackets

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder Braces -> specBraces

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder NoBrackets -> id

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder

4be371b81d055e03a5946e4ec333613f313d689bChristian Maeder-- | print a 'Kind' plus a preceding colon (or nothing)

ac510075311023bf24175f7a76b89ec2bbda0626Christian MaederprintKind :: Kind -> Doc

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)

ac9e33c3c35b2663e5cb76483228910f142d9576Christian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder-- | print the kind of a variable with its variance and a preceding colon

529f678f015ae5276f87da63114cdce750b366aeChristian MaederprintVarKind :: Variance -> VarKind -> Doc

ac510075311023bf24175f7a76b89ec2bbda0626Christian MaederprintVarKind e vk = case vk of

b7941d1840cb336e11e7a7c0916f7b763c0366f0Christian Maeder Downset t ->

568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder space <> less <+> pretty t

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maeder VarKind k -> space <> colon <+>

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder pretty e <> pretty k

81700fac589336e88451a2a8474a893a28506438Christian Maeder MissingKind -> empty

76647324ed70f33b95a881b536d883daccf9568dChristian Maeder

ac510075311023bf24175f7a76b89ec2bbda0626Christian Maederdata TypePrec = Outfix | Prefix | ProdInfix | FunInfix | Absfix

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder deriving (Eq, Ord)

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian MaederparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

5b1f1d57c75562a7af79e8256f4afa07febe921bChristian Maeder

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 _ -> (Prefix,

fsep [parenPrec Prefix $ toMixType t, colon, pretty 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

[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

[e1, e2, e3] | isPlace e1 && not (isPlace e2)

&& isPlace e3 && 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 name == productId (length tyArgs) then

(ProdInfix, fsep $ punctuate (space <> cross) $

map (parenPrec ProdInfix) dArgs)

else aArgs

_ -> aArgs

instance Pretty Type where

pretty = snd . toMixType

-- no curried notation for bound variables

instance Pretty TypeScheme where

pretty (TypeScheme vs t _) = let tdoc = pretty t in

if null vs then tdoc else

fsep [forallDoc, semiDs vs, bullet <+> tdoc]

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 && take 2 (show t) == "_v"

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

parens $ fsep [pretty br, pretty n, colon, pretty $

if isPred br then unPredTypeScheme t else t]

, foldResolvedMixTerm =

\ (ResolvedMixTerm _ _ os _) n@(Id toks cs ps) tys ts _ ->

if placeCount n == length ts || null ts then

let ds = zipArgs n os ts in

if null tys then idApplDoc n ds

else let (ftoks, _) = splitMixToken toks

fId = Id ftoks cs ps

(fts, rts) = splitAt (placeCount fId) ds

in fsep $ (idApplDoc fId fts <> brackets (ppWithCommas tys))

: rts

else idApplDoc applId [idDoc n, parens $ sepByCommas ts]

, foldApplTerm = \ (ApplTerm o1 o2 _) t1 t2 _ ->

case (o1, o2) of

-- comment out the following two guards for CASL applications

(ResolvedMixTerm n _ [] _, TupleTerm ts@(_ : _) _)

| placeCount n == length ts ->

idApplDoc n (zipArgs n ts $ map printTerm ts)

(ResolvedMixTerm n _ [] _, _) | placeCount n == 1

-> idApplDoc n $ zipArgs n [o2] [t2]

_ -> idApplDoc applId $ zipArgs applId [o1, o2] [t1, t2]

, foldTupleTerm = \ _ ts _ -> parens $ sepByCommas ts

, foldTypedTerm = \ (TypedTerm ot _ _ _) t q typ _ -> fsep [(case ot of

LambdaTerm {} -> parens

LetTerm {} -> parens

CaseTerm {} -> parens

QuantifiedTerm {} -> parens

_ -> id) t, pretty q, pretty typ]

, foldQuantifiedTerm = \ _ q vs t _ ->

fsep [pretty q, printGenVarDecls vs, bullet <+> t]

, foldLambdaTerm = \ _ ps q t _ ->

fsep [ lambda

, case ps of

[p] -> p

_ -> 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 = \ _ t -> pretty t

, foldMixTypeTerm = \ _ q t _ -> pretty q <+> pretty t

, foldMixfixTerm = \ _ ts -> fsep ts

, 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 _ (InstOpId i _ _) _ ps ->

if elem i $ map fst bList then

ResolvedMixTerm i [] [] ps else t

, foldTypedTerm = \ _ nt q ty ps ->

case q of

Inferred -> nt

_ -> case nt of

TypedTerm _ oq oty _ | oty == ty || oq == InType -> 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 ps ->

ApplTerm (addParAppl t1) (addParAppl t2) ps

, foldResolvedMixTerm = \ _ n tys ts ps ->

ResolvedMixTerm n tys (map addParAppl ts) ps

, foldTypedTerm = \ _ t q typ ps ->

TypedTerm (addParAppl t) q typ ps

, foldMixfixTerm = \ _ ts -> MixfixTerm $ map addParAppl ts

, foldAsPattern = \ _ v p ps -> AsPattern v (addParAppl p) ps

}

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 _ _) : _ ->

ppWithCommas (map ( \ (GenVarDecl (VarDecl v _ _ _)) -> v) l)

<> printVarDeclType t

GenTypeVarDecl (TypeArg _ e c _ _ _ _) : _ ->

ppWithCommas (map ( \ (GenTypeVarDecl v) -> 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

_ -> space <> 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 InstOpId where

pretty (InstOpId n@(Id ts cs ps) l _) = if null l then pretty n else

let (toks, pls) = splitMixToken ts in

fcat $ pretty (Id toks cs ps) : brackets (ppWithCommas l)

: map pretty pls

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 = printEq0 equals . foldEq printTermRec

instance Pretty BasicItem where

pretty bi = case bi of

SigItems s -> pretty s

ProgItems l _ -> sep [keyword programS, semiAnnoted l]

ClassItems i l _ -> let

b = semiAnnos pretty l

p = case map item l of

_ : _ : _ -> True

[ClassItem (ClassDecl (_ : _ : _) _ _) _ _] -> True

_ -> False

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 ++ case l of

_ : _ : _ -> sS

_ -> "") <+> printGenVarDecls l

FreeDatatype l _ ->

sep [keyword freeS <+> keyword (typeS ++ case l of

_ : _ : _ -> sS

_ -> ""), 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]

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 b = keyword $ show b

instance Pretty SigItems where

pretty si = case si of

TypeItems i l _ -> let b = semiAnnos pretty l in case i of

Plain -> topSigKey ((if all (isSimpleTypeItem . item) l

then typeS else 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 _ -> 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

prettyTypeScheme :: Bool -> TypeScheme -> Doc

prettyTypeScheme b = pretty . (if b then unPredTypeScheme else id)

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))(prettyTypeScheme b t)]

++ punctuate comma (map pretty a)

OpDefn n ps s p t _ ->

fcat $ ((if null ps then (<> space) else id) $ pretty n)

: map ((<> space) . parens . semiDs) ps

++ (if b then [] else

[colon <> pretty p <+> prettyTypeScheme b s <> space])

++ [(if b then equiv else equals) <> space, pretty t]

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 (if all isSimpleType l then typeS else typeS)

<+> ppWithCommas l

instance Pretty Component where

pretty sel = case sel of

Selector n p t _ _ -> sep [pretty n, colon <> pretty p <+> pretty t]

NoSelector t -> pretty t

instance Pretty OpId where

pretty (OpId n ts _) =

sep $ pretty n : if null ts then [] else [brackets $ ppWithCommas ts]

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

_ -> "") <> space