fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz{- |

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzModule : $Header$

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzCopyright : (c) Christian Maeder and Uni Bremen 2003

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzMaintainer : maeder@tzi.de

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzStability : experimental

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzPortability : portable

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzprinting data types of the abstract syntax

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-}

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzmodule HasCASL.PrintAs where

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.As

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.AsUtils

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.FoldTerm

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport HasCASL.Builtin

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Id

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Keywords

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.DocUtils

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.Doc

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Common.AS_Annotation

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulzimport Data.List (groupBy)

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz-- | short cut for: if b then empty else d

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulznoPrint :: Bool -> Doc -> Doc

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulznoPrint b d = if b then empty else d

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulznoNullPrint :: [a] -> Doc -> Doc

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavunoNullPrint = noPrint . null

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzsemiDs :: Pretty a => [a] -> Doc

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzsemiDs = fsep . punctuate semi . map pretty

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst Schulz

fcd50ed0f526645ca50bad2170e3b98b911b7678Ewaryst SchulzsemiAnnoted :: Pretty a => [Annoted a] -> Doc

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavusemiAnnoted = vcat . map (printSemiAnno pretty True)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuinstance Pretty Variance where

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu pretty = sidDoc . mkSimpleId . show

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuinstance Pretty a => Pretty (AnyKind a) where

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu pretty knd = case knd of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ClassKind ci -> pretty ci

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu FunKind v k1 k2 _ -> fsep [pretty v <>

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (case k1 of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu FunKind _ _ _ _ -> parens

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu _ -> id) (pretty k1)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , funArrow

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , pretty k2]

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuvarOfTypeArg :: TypeArg -> Id

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuvarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savuinstance Pretty TypePattern where

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu pretty tp = case tp of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu TypePattern name args _ -> pretty name

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu <+> fsep (map (pretty . varOfTypeArg) args)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu TypePatternToken t -> pretty t

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu MixfixTypePattern ts -> fsep $ map pretty ts

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu BracketTypePattern k l _ -> bracket k $ ppWithCommas l

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu TypePatternArg t _ -> parens $ pretty t

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- | put proper brackets around a document

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savubracket :: BracketKind -> Doc -> Doc

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savubracket b = case b of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Parens -> parens

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Squares -> brackets

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Braces -> specBraces

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu NoBrackets -> id

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- | print a 'Kind' plus a preceding colon (or nothing)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprintKind :: Kind -> Doc

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu-- | print the kind of a variable with its variance and a preceding colon

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprintVarKind :: Variance -> VarKind -> Doc

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprintVarKind e vk = case vk of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Downset t ->

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu space <> less <+> pretty t

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu VarKind k -> space <> colon <+>

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu pretty e <> pretty k

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu MissingKind -> empty

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savudata TypePrec = Outfix | Prefix | ProdInfix | FunInfix deriving (Eq, Ord)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprintTypeToken :: Token -> Doc

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavuprintTypeToken t = let

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu l = ("*", cross) : map ( \ (a, d) -> (show a, d) )

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu [ (FunArr, funArrow)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , (PFunArr, pfun)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , (ContFunArr, cfun)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu , (PContFunArr, pcfun) ]

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu in case lookup (tokStr t) l of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu Just d -> d

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu _ -> pretty t

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavutoMixType :: Type -> (TypePrec, Doc)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert SavutoMixType typ = case typ of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu ExpandedType t1 _ -> toMixType t1

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu BracketType k l _ -> (Outfix, bracket k $ sepByCommas $ map

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu (snd . toMixType) l)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu KindedType t kind _ -> (Prefix,

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu fsep [parenPrec Prefix $ toMixType t, colon, pretty kind])

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu _ -> let (topTy, tyArgs) = getTypeAppl typ in

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu case topTy of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu TypeName name@(Id ts cs _) _k _i -> let topDoc = pretty name in

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu case tyArgs of

ad306df140215d8fb88d14bbb7d685011e0f770bRobert Savu [] -> (Outfix, pretty name)

[arg] -> let dArg = toMixType arg in

case ts of

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

&& not (isPlace e3) && null cs ->

(Outfix, fsep [pretty e1, snd dArg, pretty e3])

_ -> (Prefix, fsep [topDoc, parenPrec Prefix dArg])

[arg1, arg2] -> let dArg1 = toMixType arg1

dArg2 = toMixType arg2 in

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])

_ -> (Prefix, fsep [topDoc, parenPrec Prefix dArg1,

parenPrec Prefix dArg2])

_ -> if name == productId (length tyArgs) then

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

map (parenPrec ProdInfix . toMixType) tyArgs)

else (Prefix, fsep $ topDoc :

map (parenPrec Prefix . toMixType) tyArgs)

_ | null tyArgs -> (Outfix, printType topTy)

_ -> (Prefix, fsep $ parenPrec ProdInfix (toMixType topTy)

: map (parenPrec Prefix . toMixType) tyArgs)

printType :: Type -> Doc

printType ty = case ty of

TypeName name _ _ -> pretty name

TypeAppl t1 t2 -> fcat [parens (printType t1),

parens (printType t2)]

ExpandedType t1 t2 -> fcat [printType t1, text asP, printType t2]

TypeToken t -> printTypeToken t

BracketType k l _ -> bracket k $ sepByCommas $ map (printType) l

KindedType t kind _ -> sep [printType t, colon <+> pretty kind]

MixfixType ts -> fsep $ map printType ts

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

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

idApplDoc n $ zipArgs n os ts

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 ts ps ->

ResolvedMixTerm n (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 l _) = pretty n <> noNullPrint l

(brackets $ semiDs l)

-- | print a 'TypeScheme' as a pseudo type

printPseudoType :: TypeScheme -> Doc

printPseudoType (TypeScheme l t _) = noNullPrint l (lambda

<+> (if null $ tail l then pretty $ head l

else fsep(map (parens . pretty) l))

<+> bullet <> space) <> pretty t

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 in case i of

Plain -> topSigKey classS <+> b

Instance -> sep [keyword classS <+> keyword instanceS, 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 _) = fsep [ppWithCommas l, 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