0N/A{- |

0N/AModule : $Header$

0N/ADescription : print the abstract syntax so that it can be re-parsed

0N/ACopyright : (c) Christian Maeder and Uni Bremen 2003

0N/ALicense : GPLv2 or higher, see LICENSE.txt

0N/A

0N/AMaintainer : Christian.Maeder@dfki.de

0N/AStability : experimental

0N/APortability : portable

0N/A

0N/Aprinting data types of the abstract syntax

0N/A-}

0N/A

0N/Amodule HasCASL.PrintAs where

0N/A

0N/Aimport HasCASL.As

0N/Aimport HasCASL.AsUtils

0N/Aimport HasCASL.FoldTerm

0N/Aimport HasCASL.Builtin

0N/A

0N/Aimport Common.Id

0N/Aimport Common.Keywords

0N/Aimport Common.DocUtils

0N/Aimport Common.Doc

0N/Aimport Common.AS_Annotation

0N/A

0N/Aimport qualified Data.Set as Set

0N/Aimport Data.List

0N/A

0N/A-- | short cut for: if b then empty else d

0N/AnoPrint :: Bool -> Doc -> Doc

0N/AnoPrint b d = if b then empty else d

0N/A

0N/AnoNullPrint :: [a] -> Doc -> Doc

0N/AnoNullPrint = noPrint . null

0N/A

0N/AsemiDs :: Pretty a => [a] -> Doc

0N/AsemiDs = fsep . punctuate semi . map pretty

0N/A

0N/AsemiAnnoted :: Pretty a => [Annoted a] -> Doc

0N/AsemiAnnoted = vcat . map (printSemiAnno pretty True)

0N/A

0N/Ainstance Pretty Variance where

0N/A pretty = sidDoc . mkSimpleId . show

0N/A

0N/Ainstance Pretty a => Pretty (AnyKind a) where

0N/A pretty knd = case knd of

0N/A ClassKind ci -> pretty ci

0N/A FunKind v k1 k2 _ -> fsep

0N/A [ pretty v <> (case k1 of

0N/A FunKind _ _ _ _ -> parens

0N/A _ -> id) (pretty k1)

0N/A , funArrow, pretty k2]

0N/A

0N/AvarOfTypeArg :: TypeArg -> Id

0N/AvarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

0N/A

0N/Ainstance Pretty TypePattern where

0N/A pretty tp = case tp of

0N/A TypePattern name@(Id ts cs _) args _ ->

0N/A let ds = map (pretty . varOfTypeArg) args in

0N/A if placeCount name == length args then

0N/A let (ras, dts) = mapAccumL ( \ l t -> if isPlace t then

0N/A case l of

0N/A x : r -> (r, x)

0N/A _ -> error "Pretty TypePattern"

0N/A else (l, printTypeToken t)) ds ts

0N/A in fsep $ dts ++ (if null cs then [] else

0N/A [brackets $ sepByCommas $ map printTypeId cs])

0N/A ++ ras

0N/A else printTypeId name <+> fsep ds

0N/A TypePatternToken t -> printTypeToken t

0N/A MixfixTypePattern ts -> fsep $ map pretty ts

0N/A BracketTypePattern k l _ -> bracket k $ ppWithCommas l

0N/A TypePatternArg t _ -> parens $ pretty t

0N/A

0N/A-- | put proper brackets around a document

0N/Abracket :: BracketKind -> Doc -> Doc

0N/Abracket b = case b of

0N/A Parens -> parens

0N/A Squares -> brackets

0N/A Braces -> specBraces

0N/A NoBrackets -> id

0N/A

0N/A-- | print a 'Kind' plus a preceding colon (or nothing)

0N/AprintKind :: Kind -> Doc

0N/AprintKind k = noPrint (k == universe) $ printVarKind NonVar (VarKind k)

0N/A

0N/A-- | print the kind of a variable with its variance and a preceding colon

0N/AprintVarKind :: Variance -> VarKind -> Doc

0N/AprintVarKind e vk = case vk of

0N/A Downset t -> less <+> pretty t

0N/A VarKind k -> colon <+> pretty e <> pretty k

0N/A MissingKind -> empty

0N/A

0N/Adata TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix

0N/A deriving (Eq, Ord)

0N/A

0N/AparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

0N/AparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

0N/A

0N/AprintTypeToken :: Token -> Doc

0N/AprintTypeToken t = let

0N/A l = ("*", cross) : map ( \ (a, d) -> (show a, d) )

0N/A [ (FunArr, funArrow)

0N/A , (PFunArr, pfun)

0N/A , (ContFunArr, cfun)

0N/A , (PContFunArr, pcfun) ]

0N/A in case lookup (tokStr t) l of

0N/A Just d -> d

0N/A _ -> pretty t

0N/A

0N/AprintTypeId :: Id -> Doc

0N/AprintTypeId (Id ts cs _) = let (toks, pls) = splitMixToken ts in

0N/A fcat $ map printTypeToken toks

0N/A ++ (if null cs then [] else [brackets $ sepByCommas $ map printTypeId cs])

0N/A ++ map printTypeToken pls

0N/A

0N/AtoMixType :: Type -> (TypePrec, Doc)

0N/AtoMixType typ = case typ of

0N/A TypeName name _ _ -> (Outfix, printTypeId name)

0N/A TypeToken tt -> (Outfix, printTypeToken tt)

0N/A TypeAbs v t _ ->

0N/A (Absfix, sep [ lambda <+> pretty v, bullet <+> snd (toMixType t)])

0N/A ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type

0N/A BracketType k l _ ->

0N/A (Outfix, bracket k $ sepByCommas $ map (snd . toMixType) l)

0N/A KindedType t kind _ -> (Lazyfix, sep

0N/A [ parenPrec Lazyfix $ toMixType t

0N/A , colon <+> printList0 (Set.toList kind)])

0N/A MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)

0N/A TypeAppl t1 t2 -> let

0N/A (topTy, tyArgs) = getTypeApplAux False typ

0N/A aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1

0N/A , parenPrec Prefix $ toMixType t2 ])

0N/A in case topTy of

0N/A TypeName name@(Id ts cs _) _k _i ->

0N/A case map toMixType tyArgs of

0N/A [dArg] -> case ts of

0N/A [e] | name == lazyTypeId ->

0N/A (Lazyfix, pretty e <+> parenPrec Lazyfix dArg)

0N/A [e1, e2, e3] | not (isPlace e1) && isPlace e2

0N/A && not (isPlace e3) && null cs ->

0N/A (Outfix, fsep [pretty e1, snd dArg, pretty e3])

0N/A _ -> aArgs

0N/A [dArg1, dArg2] -> case ts of

0N/A [_, e2, _] | isInfix name && null cs ->

0N/A if tokStr e2 == prodS then

0N/A (ProdInfix, fsep

0N/A [ parenPrec ProdInfix dArg1

0N/A , cross, parenPrec ProdInfix dArg2])

0N/A else -- assume fun type

0N/A (FunInfix, fsep

0N/A [ parenPrec FunInfix dArg1

0N/A , printTypeToken e2, snd dArg2])

0N/A _ -> aArgs

0N/A dArgs -> if isProductIdWithArgs name $ length tyArgs then

0N/A (ProdInfix, fsep $ punctuate (space <> cross) $

0N/A map (parenPrec ProdInfix) dArgs) else aArgs

0N/A _ -> aArgs

0N/A

0N/Ainstance Pretty Type where

0N/A pretty = snd . toMixType

0N/A

0N/AprintTypeScheme :: PolyId -> TypeScheme -> Doc

0N/AprintTypeScheme (PolyId _ tys _) (TypeScheme vs t _) =

0N/A let tdoc = pretty t in

0N/A if null vs || not (null tys) then tdoc else

0N/A fsep [forallDoc, semiDs vs, bullet <+> tdoc]

0N/A

0N/A-- no curried notation for bound variables

0N/Ainstance Pretty TypeScheme where

0N/A pretty = printTypeScheme (PolyId applId [] nullRange)

0N/A

0N/Ainstance Pretty Partiality where

0N/A pretty p = case p of

0N/A Partial -> quMarkD

0N/A Total -> empty

0N/A

0N/Ainstance Pretty Quantifier where

0N/A pretty q = case q of

0N/A Universal -> forallDoc

0N/A Existential -> exists

0N/A Unique -> unique

0N/A

0N/Ainstance Pretty TypeQual where

0N/A pretty q = case q of

0N/A OfType -> colon

0N/A AsType -> text asS

0N/A InType -> inDoc

0N/A Inferred -> colon

0N/A

0N/Ainstance Pretty Term where

0N/A pretty = printTerm . rmSomeTypes

0N/A

0N/AisSimpleTerm :: Term -> Bool

0N/AisSimpleTerm trm = case trm of

0N/A QualVar _ -> True

0N/A QualOp _ _ _ _ _ _ -> True

0N/A ResolvedMixTerm _ _ _ _ -> True

0N/A ApplTerm _ _ _ -> True

0N/A TupleTerm _ _ -> True

0N/A TermToken _ -> True

0N/A BracketTerm _ _ _ -> True

0N/A _ -> False

0N/A

0N/A-- | used only to produce CASL applications

0N/AisSimpleArgTerm :: Term -> Bool

0N/AisSimpleArgTerm trm = case trm of

0N/A QualVar vd -> not (isPatVarDecl vd)

0N/A QualOp _ _ _ _ _ _ -> True

0N/A ResolvedMixTerm n _ l _ -> placeCount n /= 0 || not (null l)

0N/A TupleTerm _ _ -> True

0N/A BracketTerm _ _ _ -> True

0N/A _ -> False

0N/A

0N/AhasRightQuant :: Term -> Bool

0N/AhasRightQuant t = case t of

0N/A QuantifiedTerm {} -> True

0N/A LambdaTerm {} -> True

0N/A CaseTerm {} -> True

0N/A LetTerm Let _ _ _ -> True

0N/A ResolvedMixTerm n _ ts _ | endPlace n && placeCount n == length ts

0N/A -> hasRightQuant (last ts)

0N/A ApplTerm (ResolvedMixTerm n _ [] _) t2 _ | endPlace n ->

0N/A case t2 of

0N/A TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)

0N/A _ -> hasRightQuant t2

0N/A ApplTerm _ t2 _ -> hasRightQuant t2

0N/A _ -> False

0N/A

0N/AzipArgs :: Id -> [Term] -> [Doc] -> [Doc]

0N/AzipArgs n ts ds = case (ts, ds) of

0N/A (t : r, d : s) -> let

0N/A p = parenTermDoc t d

0N/A e = if hasRightQuant t then parens d else p

0N/A in if null r && null s && endPlace n then

0N/A [if hasRightQuant t then d else p]

0N/A else e : zipArgs n r s

0N/A _ -> []

0N/A

0N/AisPatVarDecl :: VarDecl -> Bool

0N/AisPatVarDecl (VarDecl v ty _ _) = case ty of

0N/A TypeName t _ _ -> isSimpleId v && isPrefixOf "_v" (show t)

0N/A _ -> False

0N/A

0N/AparenTermDoc :: Term -> Doc -> Doc

0N/AparenTermDoc trm = if isSimpleTerm trm then id else parens

0N/A

0N/AprintTermRec :: FoldRec Doc (Doc, Doc)

0N/AprintTermRec = FoldRec

0N/A { foldQualVar = \ _ vd@(VarDecl v _ _ _) ->

0N/A if isPatVarDecl vd then pretty v

0N/A else parens $ keyword varS <+> pretty vd

0N/A , foldQualOp = \ _ br n t tys k _ ->

0N/A (if null tys || k == Infer then id else

0N/A (<> brackets (ppWithCommas tys))) $

0N/A parens $ fsep [pretty br, pretty n, colon, printTypeScheme n $

0N/A if isPred br then unPredTypeScheme t else t]

0N/A , foldResolvedMixTerm = \ rt n@(Id toks cs ps) tys ts _ ->

0N/A let pn = placeCount n

0N/A ResolvedMixTerm _ _ os _ = rt

0N/A ds = zipArgs n os ts

0N/A in if pn == length ts || null ts then

0N/A if null tys then idApplDoc n ds

0N/A else let (ftoks, _) = splitMixToken toks

0N/A fId = Id ftoks cs ps

0N/A (fts, rts) = splitAt (placeCount fId) $ if null ts

0N/A then replicate pn $ pretty placeTok else ds

0N/A in fsep $ (idApplDoc fId fts <> brackets (ppWithCommas tys))

0N/A : rts

0N/A else idApplDoc applId [idDoc n, parens $ sepByCommas ts]

0N/A , foldApplTerm = \ ot t1 t2 _ ->

0N/A case ot of

0N/A -- comment out the following two guards for CASL applications

0N/A ApplTerm (ResolvedMixTerm n _ [] _) (TupleTerm ts@(_ : _) _) _

0N/A | placeCount n == length ts ->

0N/A idApplDoc n (zipArgs n ts $ map printTerm ts)

0N/A ApplTerm (ResolvedMixTerm n _ [] _) o2 _ | placeCount n == 1

0N/A -> idApplDoc n $ zipArgs n [o2] [t2]

0N/A ApplTerm o1 o2 _

0N/A -> idApplDoc applId $ zipArgs applId [o1, o2] [t1, t2]

0N/A _ -> error "printTermRec.foldApplTerm"

0N/A , foldTupleTerm = \ _ ts _ -> parens $ sepByCommas ts

0N/A , foldTypedTerm = \ ~(TypedTerm ot _ _ _) t q typ _ -> fsep [(case ot of

0N/A TypedTerm {} | elem q [Inferred, OfType] -> parens

0N/A ApplTerm (ResolvedMixTerm n _ [] _) arg _ ->

0N/A let pn = placeCount n in case arg of

0N/A TupleTerm ts@(_ : _) _ | pn == length ts -> parens

0N/A _ | pn == 1 || hasRightQuant ot -> parens

0N/A _ -> id

0N/A _ | hasRightQuant ot -> parens

0N/A _ -> id) t, pretty q, pretty typ]

0N/A , foldQuantifiedTerm = \ _ q vs t _ ->

0N/A fsep [pretty q, printGenVarDecls vs, bullet <+> t]

0N/A , foldLambdaTerm = \ ot ps q t _ ->

0N/A let LambdaTerm ops _ _ _ = ot in

0N/A fsep [ lambda

0N/A , case ops of

0N/A [p] -> case p of

0N/A TupleTerm [] _ -> empty

0N/A QualVar vd@(VarDecl v ty _ _) ->

0N/A pretty v <+> if isPatVarDecl vd then empty

0N/A else printVarDeclType ty

0N/A _ -> head ps

0N/A _ -> if all ( \ p -> case p of

0N/A QualVar vd -> not $ isPatVarDecl vd

0N/A _ -> False) ops

0N/A then printGenVarDecls $ map

0N/A (\ pt -> let QualVar vd = pt in GenVarDecl vd)

0N/A ops

0N/A else fcat $ map parens ps

0N/A , (case q of

0N/A Partial -> bullet

0N/A Total -> bullet <> text exMark) <+> t]

0N/A , foldCaseTerm = \ _ t es _ ->

0N/A fsep [text caseS, t, text ofS,

0N/A cat $ punctuate (space <> bar <> space) $

0N/A map (printEq0 funArrow) es]

0N/A , foldLetTerm = \ _ br es t _ ->

0N/A let des = sep $ punctuate semi $ map (printEq0 equals) es

0N/A in case br of

0N/A Let -> fsep [sep [text letS <+> des, text inS], t]

0N/A Where -> fsep [sep [t, text whereS], des]

0N/A Program -> text programS <+> des

0N/A , foldTermToken = const pretty

0N/A , foldMixTypeTerm = \ _ q t _ -> pretty q <+> pretty t

0N/A , foldMixfixTerm = const fsep

0N/A , foldBracketTerm = \ _ k l _ -> bracket k $ sepByCommas l

0N/A , foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->

0N/A fsep [pretty v, text asP, p]

0N/A , foldProgEq = \ _ p t _ -> (p, t) }

0N/A

0N/AprintTerm :: Term -> Doc

0N/AprintTerm = foldTerm printTermRec

0N/A

0N/ArmTypeRec :: MapRec

0N/ArmTypeRec = mapRec

0N/A { foldQualOp = \ t _ (PolyId i _ _) _ tys k ps ->

0N/A if elem i $ map fst bList then ResolvedMixTerm i

0N/A (if k == Infer then [] else tys) [] ps else t

0N/A , foldTypedTerm = \ _ nt q ty ps -> case q of

0N/A Inferred -> nt

0N/A _ -> case nt of

0N/A TypedTerm tt oq oty _ | oty == ty || oq == InType ->

0N/A if q == AsType then TypedTerm tt q ty ps else nt

0N/A QualVar (VarDecl _ oty _ _) | oty == ty -> nt

0N/A _ -> TypedTerm nt q ty ps }

0N/A

0N/ArmSomeTypes :: Term -> Term

0N/ArmSomeTypes = foldTerm rmTypeRec

0N/A

0N/A-- | put parenthesis around applications

0N/AparenTermRec :: MapRec

0N/AparenTermRec = let

0N/A addParAppl t = case t of

0N/A ResolvedMixTerm _ _ [] _ -> t

0N/A QualVar _ -> t

0N/A QualOp _ _ _ _ _ _ -> t

0N/A TermToken _ -> t

0N/A BracketTerm _ _ _ -> t

0N/A TupleTerm _ _ -> t

0N/A _ -> TupleTerm [t] nullRange

0N/A in mapRec

0N/A { foldApplTerm = \ _ t1 t2 ->

0N/A ApplTerm (addParAppl t1) (addParAppl t2)

0N/A , foldResolvedMixTerm = \ _ n tys ->

0N/A ResolvedMixTerm n tys . map addParAppl

0N/A , foldTypedTerm = \ _ ->

0N/A TypedTerm . addParAppl

0N/A , foldMixfixTerm = \ _ -> MixfixTerm . map addParAppl

0N/A , foldAsPattern = \ _ v -> AsPattern v . addParAppl

0N/A }

0N/A

0N/AparenTerm :: Term -> Term

0N/AparenTerm = foldTerm parenTermRec

0N/A

0N/A-- | print an equation with different symbols between pattern and term

0N/AprintEq0 :: Doc -> (Doc, Doc) -> Doc

0N/AprintEq0 s (p, t) = sep [p, hsep [s, t]]

0N/A

0N/AprintGenVarDecls :: [GenVarDecl] -> Doc

0N/AprintGenVarDecls = fsep . punctuate semi . map

0N/A ( \ l -> case l of

0N/A [x] -> pretty x

0N/A 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 ((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 _ -> 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 (if all isSimpleType l then typeS else 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

_ -> ""