acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- |

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederModule : ./HasCASL/PrintAs.hs

3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederDescription : print the abstract syntax so that it can be re-parsed

73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederMaintainer : Christian.Maeder@dfki.de

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederStability : experimental

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederPortability : portable

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskiprinting data types of the abstract syntax

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-}

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedermodule HasCASL.PrintAs where

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport HasCASL.As

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport HasCASL.AsUtils

85ebda7270c6883b503d3bde4757033c09c25644Christian Maederimport HasCASL.FoldTerm

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport HasCASL.Builtin

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.Id

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.Keywords

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.DocUtils

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzimport Common.Doc

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.AS_Annotation

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Set as Set

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Data.List

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedernoPrint :: Bool -> Doc -> Doc

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian MaedernoPrint b d = if b then empty else d

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedernoNullPrint :: [a] -> Doc -> Doc

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian MaedernoNullPrint = noPrint . null

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian MaedersemiDs :: Pretty a => [a] -> Doc

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian MaedersemiDs = fsep . punctuate semi . map pretty

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedersemiAnnoted :: Pretty a => [Annoted a] -> Doc

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian MaedersemiAnnoted = vcat . map (printSemiAnno pretty True)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty Variance where

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder pretty = sidDoc . mkSimpleId . show

60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty a => Pretty (AnyKind a) where

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder pretty knd = case knd of

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder ClassKind ci -> pretty ci

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski FunKind v k1 k2 _ -> fsep

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski [ pretty v <> (case k1 of

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski FunKind {} -> parens

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski _ -> id) (pretty k1)

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski , funArrow, pretty k2]

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski

6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskivarOfTypeArg :: TypeArg -> Id

6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskivarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty TypePattern where

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder pretty tp = case tp of

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

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder if placeCount name == length args then

6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski let (ras, dts) = mapAccumL ( \ l t -> if isPlace t then

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder case l of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder x : r -> (r, x)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> error "Pretty TypePattern"

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

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

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder ++ ras

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder else printTypeId name <+> fsep ds

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder TypePatternToken t -> printTypeToken t

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder MixfixTypePattern ts -> fsep $ map pretty ts

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder TypePatternArg t _ -> parens $ pretty t

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder-- | put proper brackets around a document

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederbracket :: BracketKind -> Doc -> Doc

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederbracket b = case b of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Parens -> parens

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Squares -> brackets

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Braces -> specBraces

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder NoBrackets -> id

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintKind :: Kind -> Doc

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederprintKind k = noPrint (k == universe) $ printVarKind NonVar (VarKind k)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintVarKind :: Variance -> VarKind -> Doc

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till MossakowskiprintVarKind e vk = case vk of

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski Downset t -> less <+> pretty t

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski VarKind k -> colon <+> pretty e <> pretty k

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski MissingKind -> empty

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskidata TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski deriving (Eq, Ord)

0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski

b20cc520e698253354303b7bf3bc17f84240b213Klaus LuettichparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

da955132262baab309a50fdffe228c9efe68251dCui JianparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintTypeToken :: Token -> Doc

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintTypeToken t = let

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [ (FunArr, funArrow)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , (PFunArr, pfun)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , (ContFunArr, cfun)

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder , (PContFunArr, pcfun) ]

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in case lookup (tokStr t) l of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Just d -> d

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> pretty t

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintTypeId :: Id -> Doc

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintTypeId (Id ts cs _) = let (toks, pls) = splitMixToken ts in

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder fcat $ map printTypeToken toks

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz ++ (if null cs then [] else [brackets $ sepByCommas $ map printTypeId cs])

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz ++ map printTypeToken pls

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst SchulztoMixType :: Type -> (TypePrec, Doc)

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst SchulztoMixType typ = case typ of

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz TypeName name _ _ -> (Outfix, printTypeId name)

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz TypeToken tt -> (Outfix, printTypeToken tt)

831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz TypeAbs v t _ ->

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz (Absfix, sep [ lambda <+> pretty v, bullet <+> snd (toMixType t)])

10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder BracketType k l _ ->

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Outfix, bracket k $ sepByCommas $ map (snd . toMixType) l)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder KindedType t kind _ -> (Lazyfix, sep

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [ parenPrec Lazyfix $ toMixType t

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , colon <+> printList0 (Set.toList kind)])

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder TypeAppl t1 t2 -> let

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (topTy, tyArgs) = getTypeApplAux False typ

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , parenPrec Prefix $ toMixType t2 ])

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in case topTy of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder TypeName name@(Id ts cs _) _k _i ->

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder case map toMixType tyArgs of

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder [dArg] -> case ts of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [e] | name == lazyTypeId ->

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Lazyfix, pretty e <+> parenPrec Lazyfix dArg)

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

07baaf27fc0029203075ed916999006dcc619ef0Christian Maeder && not (isPlace e3) && null cs ->

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> aArgs

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [dArg1, dArg2] -> case ts of

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [_, e2, _] | isInfix name && null cs ->

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder if tokStr e2 == prodS then

3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder (ProdInfix, fsep

07baaf27fc0029203075ed916999006dcc619ef0Christian Maeder [ parenPrec ProdInfix dArg1

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , cross, parenPrec ProdInfix dArg2])

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder else -- assume fun type

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (FunInfix, fsep

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [ parenPrec FunInfix dArg1

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , printTypeToken e2, snd dArg2])

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder _ -> aArgs

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder dArgs -> if isProductIdWithArgs name $ length tyArgs then

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

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder map (parenPrec ProdInfix) dArgs) else aArgs

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder _ -> aArgs

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Pretty Type where

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder pretty = snd . toMixType

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederprintTypeScheme :: PolyId -> TypeScheme -> Doc

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederprintTypeScheme (PolyId _ tys _) (TypeScheme vs t _) =

acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder let tdoc = pretty t in

999f839e42d594e4ae288208fec398626837c41cTill Mossakowski if null vs || not (null tys) then tdoc else

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

999f839e42d594e4ae288208fec398626837c41cTill Mossakowski

999f839e42d594e4ae288208fec398626837c41cTill Mossakowski-- no curried notation for bound variables

999f839e42d594e4ae288208fec398626837c41cTill Mossakowskiinstance Pretty TypeScheme where

999f839e42d594e4ae288208fec398626837c41cTill Mossakowski pretty = printTypeScheme (PolyId applId [] nullRange)

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder

9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maederinstance Pretty Partiality where

ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski pretty p = case p of

ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski 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

_ -> ""