a9de0a2f34860a24f457c777e740b7e87e6e3827Christian Maeder{- |

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederModule : $Header$

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederDescription : print the abstract syntax so that it can be re-parsed

3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : Christian.Maeder@dfki.de

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : experimental

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederprinting data types of the abstract syntax

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski-}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule HasCASL.PrintAs where

af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.As

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.AsUtils

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.FoldTerm

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport HasCASL.Builtin

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Id

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Keywords

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.DocUtils

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Doc

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.AS_Annotation

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Data.List (groupBy, mapAccumL)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

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

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedernoPrint :: Bool -> Doc -> Doc

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedernoPrint b d = if b then empty else d

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedernoNullPrint :: [a] -> Doc -> Doc

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedernoNullPrint = noPrint . null

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedersemiDs :: Pretty a => [a] -> Doc

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedersemiDs = fsep . punctuate semi . map pretty

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedersemiAnnoted :: Pretty a => [Annoted a] -> Doc

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedersemiAnnoted = vcat . map (printSemiAnno pretty True)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Pretty Variance where

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder pretty = sidDoc . mkSimpleId . show

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Pretty a => Pretty (AnyKind a) where

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder pretty knd = case knd of

63324a97283728a30932828a612c7b0b0f687624Christian Maeder ClassKind ci -> pretty ci

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

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder (case k1 of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder FunKind _ _ _ _ -> parens

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder _ -> id) (pretty k1)

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder , funArrow

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder , pretty k2]

63324a97283728a30932828a612c7b0b0f687624Christian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedervarOfTypeArg :: TypeArg -> Id

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskivarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Pretty TypePattern where

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski pretty tp = case tp of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski TypePattern name@(Id ts cs _) args _ ->

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let ds = map (pretty . varOfTypeArg) args in

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder if placeCount name == length args then

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski case l of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski x : r -> (r, x)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski _ -> error "Pretty TypePattern"

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski else (l, printTypeToken t)) ds ts

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in fsep $ dts ++ (if null cs then [] else

3a87487c048b275c56e502c4a933273788e8d0bbChristian Maeder [brackets $ sepByCommas $ map printTypeId cs])

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu ++ ras

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu else printTypeId name <+> fsep ds

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu TypePatternToken t -> printTypeToken t

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski MixfixTypePattern ts -> fsep $ map pretty ts

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski BracketTypePattern k l _ -> bracket k $ ppWithCommas l

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski TypePatternArg t _ -> parens $ pretty t

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- | put proper brackets around a document

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowskibracket :: BracketKind -> Doc -> Doc

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskibracket b = case b of

bba825b39570777866d560bfde3807731131097eKlaus Luettich Parens -> parens

bba825b39570777866d560bfde3807731131097eKlaus Luettich Squares -> brackets

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder Braces -> specBraces

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski NoBrackets -> id

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | print a 'Kind' plus a preceding colon (or nothing)

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill MossakowskiprintKind :: Kind -> Doc

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaederprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiprintVarKind :: Variance -> VarKind -> Doc

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiprintVarKind e vk = case vk of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Downset t ->

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder space <> less <+> pretty t

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu VarKind k -> space <> colon <+>

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder pretty e <> pretty k

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder MissingKind -> empty

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maederdata TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder deriving (Eq, Ord)

63324a97283728a30932828a612c7b0b0f687624Christian Maeder

a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescuparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescuparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu

b4e202184f6977662c439c82866fe93f06cebe41Christian MaederprintTypeToken :: Token -> Doc

830e14495f9cac8e154dd4813dae010166f33d09Mihai CodescuprintTypeToken t = let

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

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu [ (FunArr, funArrow)

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu , (PFunArr, pfun)

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder , (ContFunArr, cfun)

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu , (PContFunArr, pcfun) ]

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder in case lookup (tokStr t) l of

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu Just d -> d

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski _ -> pretty t

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaederprintTypeId :: Id -> Doc

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaederprintTypeId (Id ts cs _) =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let (toks, pls) = splitMixToken ts

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder in fcat $ map printTypeToken toks ++

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (if null cs then [] else

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder [brackets $ sepByCommas $ map printTypeId cs])

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder ++ map printTypeToken pls

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedertoMixType :: Type -> (TypePrec, Doc)

da955132262baab309a50fdffe228c9efe68251dCui JiantoMixType typ = case typ of

da955132262baab309a50fdffe228c9efe68251dCui Jian TypeName name _ _ -> (Outfix, printTypeId name)

bba825b39570777866d560bfde3807731131097eKlaus Luettich TypeToken tt -> (Outfix, printTypeToken tt)

da955132262baab309a50fdffe228c9efe68251dCui Jian TypeAbs v t _ -> (Absfix, sep [ lambda <+> pretty v

bba825b39570777866d560bfde3807731131097eKlaus Luettich , bullet <+> snd (toMixType t)])

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder BracketType k l _ -> (Outfix, bracket k $ sepByCommas $ map

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (snd . toMixType) l)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder KindedType t kind _ -> (Lazyfix,

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder fsep [parenPrec Lazyfix $ toMixType t, colon, pretty kind])

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

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder TypeAppl t1 t2 -> let

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (topTy, tyArgs) = getTypeApplAux False typ

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder , parenPrec Prefix $ toMixType t2 ])

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder in case topTy of

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

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case map toMixType tyArgs of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder [dArg] ->

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder case ts of

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder [e] | name == lazyTypeId ->

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

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

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder && not (isPlace e3) && null cs ->

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

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder _ -> aArgs

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder [dArg1, dArg2] ->

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder case ts of

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

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder && isPlace e3 && null cs ->

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if tokStr e2 == prodS then

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (ProdInfix, fsep [

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder parenPrec ProdInfix dArg1, cross,

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder parenPrec ProdInfix dArg2])

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder else -- assume fun type

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (FunInfix, fsep [

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder parenPrec FunInfix dArg1, printTypeToken e2, snd dArg2])

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder _ -> aArgs

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder dArgs -> if isProductIdWithArgs name $ length tyArgs then

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

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map (parenPrec ProdInfix) dArgs)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder else aArgs

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder _ -> aArgs

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederinstance Pretty Type where

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder pretty = snd . toMixType

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder-- no curried notation for bound variables

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederinstance Pretty TypeScheme where

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder pretty (TypeScheme vs t _) = let tdoc = pretty t in

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if null vs then tdoc else

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

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederinstance Pretty Partiality where

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder pretty p = case p of

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder Partial -> quMarkD

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder Total -> empty

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederinstance Pretty Quantifier where

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder pretty q = case q of

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder Universal -> forallDoc

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder Existential -> exists

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder Unique -> unique

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maederinstance Pretty TypeQual where

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder pretty q = case q of

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder OfType -> colon

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder AsType -> text asS

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder InType -> inDoc

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder Inferred -> colon

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maederinstance Pretty Term where

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder pretty = printTerm . rmSomeTypes

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian MaederisSimpleTerm :: Term -> Bool

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederisSimpleTerm trm = case trm of

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder QualVar _ -> True

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder QualOp _ _ _ _ _ -> True

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder ResolvedMixTerm _ _ _ _ -> True

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ApplTerm _ _ _ -> True

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder TupleTerm _ _ -> True

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder TermToken _ -> True

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder BracketTerm _ _ _ -> True

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder _ -> False

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- | used only to produce CASL applications

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederisSimpleArgTerm :: Term -> Bool

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederisSimpleArgTerm trm = case trm of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder QualVar vd -> not (isPatVarDecl vd)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder QualOp _ _ _ _ _ -> True

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder ResolvedMixTerm n _ l _ -> placeCount n /= 0 || not (null l)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder TupleTerm _ _ -> True

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder BracketTerm _ _ _ -> True

a129422b14eea673dc481d2553cec108e35e72efChristian Maeder _ -> False

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederhasRightQuant :: Term -> Bool

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederhasRightQuant t = case t of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder QuantifiedTerm {} -> True

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder LambdaTerm {} -> True

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder CaseTerm {} -> True

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich LetTerm Let _ _ _ -> True

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ResolvedMixTerm n _ ts _ | endPlace n && placeCount n == length ts

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich -> hasRightQuant (last ts)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ApplTerm (ResolvedMixTerm n _ [] _) t2 _ | endPlace n ->

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich case t2 of

6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> hasRightQuant t2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ApplTerm _ t2 _ -> hasRightQuant t2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> False

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichzipArgs :: Id -> [Term] -> [Doc] -> [Doc]

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichzipArgs n ts ds = case (ts, ds) of

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich (t : r, d : s) -> let

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich p = parenTermDoc t d

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich e = if hasRightQuant t then parens d else p

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich in if null r && null s && endPlace n then

da955132262baab309a50fdffe228c9efe68251dCui Jian [if hasRightQuant t then d else p]

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich else e : zipArgs n r s

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich _ -> []

da955132262baab309a50fdffe228c9efe68251dCui Jian

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederisPatVarDecl :: VarDecl -> Bool

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederisPatVarDecl (VarDecl v ty _ _) = case ty of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder TypeName t _ _ -> isSimpleId v && take 2 (show t) == "_v"

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> False

da955132262baab309a50fdffe228c9efe68251dCui Jian

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichparenTermDoc :: Term -> Doc -> Doc

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichparenTermDoc trm = if isSimpleTerm trm then id else parens

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder

3946c010d94321f14139e12061dd4261a3cc7295Christian MaederprintTermRec :: FoldRec Doc (Doc, Doc)

3946c010d94321f14139e12061dd4261a3cc7295Christian MaederprintTermRec = FoldRec

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder { foldQualVar = \ _ vd@(VarDecl v _ _ _) ->

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder if isPatVarDecl vd then pretty v

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder else parens $ keyword varS <+> pretty vd

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder , foldQualOp = \ _ br n t tys _ -> (if null tys then id else

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder (<> brackets (ppWithCommas tys))) $

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder parens $ fsep [pretty br, pretty n, colon, pretty $

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder if isPred br then unPredTypeScheme t else t]

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder , foldResolvedMixTerm =

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let pn = placeCount n in if pn == length ts || null ts then

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let ds = zipArgs n os ts in

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski if null tys then idApplDoc n ds

6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu else let (ftoks, _) = splitMixToken toks

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fId = Id ftoks cs ps

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (fts, rts) = splitAt (placeCount fId) $ if null ts

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski then replicate pn $ pretty placeTok else ds

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski : rts

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

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

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich case (o1, o2) of

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich -- comment out the following two guards for CASL applications

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

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder | placeCount n == length ts ->

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder idApplDoc n (zipArgs n ts $ map printTerm ts)

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

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

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

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

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

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu LambdaTerm {} -> parens

da955132262baab309a50fdffe228c9efe68251dCui Jian LetTerm {} -> parens

da955132262baab309a50fdffe228c9efe68251dCui Jian CaseTerm {} -> parens

da955132262baab309a50fdffe228c9efe68251dCui Jian QuantifiedTerm {} -> parens

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

da955132262baab309a50fdffe228c9efe68251dCui Jian , foldQuantifiedTerm = \ _ q vs t _ ->

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

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu , foldLambdaTerm = \ _ ps q t _ ->

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu fsep [ lambda

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder , case ps of

da955132262baab309a50fdffe228c9efe68251dCui Jian [p] -> if show p == "()" then empty else p

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder _ -> fcat $ map parens ps

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder , (case q of

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder Partial -> bullet

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Total -> bullet <> text exMark) <+> t]

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder , foldCaseTerm = \ _ t es _ ->

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder fsep [text caseS, t, text ofS,

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cat $ punctuate (space <> bar <> space) $

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map (printEq0 funArrow) es]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , foldLetTerm = \ _ br es t _ ->

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let des = sep $ punctuate semi $ map (printEq0 equals) es

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in case br of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder Let -> fsep [sep [text letS <+> des, text inS], t]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Where -> fsep [sep [t, text whereS], des]

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder Program -> text programS <+> des

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder , foldTermToken = \ _ t -> pretty t

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

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , foldMixfixTerm = \ _ ts -> fsep ts

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder , foldBracketTerm = \ _ k l _ -> bracket k $ sepByCommas l

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fsep [pretty v, text asP, p]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , foldProgEq = \ _ p t _ -> (p, t)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder }

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

f7819aa9d183836144a98c70d4fa7d65e31cb513Till MossakowskiprintTerm :: Term -> Doc

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederprintTerm = foldTerm printTermRec

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederrmTypeRec :: MapRec

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill MossakowskirmTypeRec = mapRec

bba825b39570777866d560bfde3807731131097eKlaus Luettich { foldQualOp = \ t _ i _ _ ps ->

da955132262baab309a50fdffe228c9efe68251dCui Jian if elem i $ map fst bList then

da955132262baab309a50fdffe228c9efe68251dCui Jian ResolvedMixTerm i [] [] ps else t

bba825b39570777866d560bfde3807731131097eKlaus Luettich , foldTypedTerm = \ _ nt q ty ps ->

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case q of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder Inferred -> nt

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski _ -> case nt of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder TypedTerm _ oq oty _ | oty == ty || oq == InType -> nt

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder QualVar (VarDecl _ oty _ _) | oty == ty -> nt

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder _ -> TypedTerm nt q ty ps

c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maeder }

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian MaederrmSomeTypes :: Term -> Term

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian MaederrmSomeTypes = foldTerm rmTypeRec

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder-- | put parenthesis around applications

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederparenTermRec :: MapRec

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian MaederparenTermRec = let

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder addParAppl t = case t of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder ResolvedMixTerm _ _ [] _ -> t

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder QualVar _ -> t

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder QualOp _ _ _ _ _ -> t

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder TermToken _ -> t

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder BracketTerm _ _ _ -> t

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder TupleTerm _ _ -> t

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski _ -> TupleTerm [t] nullRange

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder in mapRec

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { foldApplTerm = \ _ t1 t2 ps ->

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu ApplTerm (addParAppl t1) (addParAppl t2) ps

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu , foldResolvedMixTerm = \ _ n tys ts ps ->

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu ResolvedMixTerm n tys (map addParAppl ts) ps

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu , foldTypedTerm = \ _ t q typ ps ->

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu TypedTerm (addParAppl t) q typ ps

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

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

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu }

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai CodescuparenTerm :: Term -> Term

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai CodescuparenTerm = foldTerm parenTermRec

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu-- | print an equation with different symbols between 'Pattern' and 'Term'

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai CodescuprintEq0 :: Doc -> (Doc, Doc) -> Doc

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai CodescuprintEq0 s (p, t) = sep [p, hsep [s, t]]

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu

63324a97283728a30932828a612c7b0b0f687624Christian MaederprintGenVarDecls :: [GenVarDecl] -> Doc

a975722baf6fee1ca3e67df170c732c4abd0a945Christian MaederprintGenVarDecls = fsep . punctuate semi . map

63324a97283728a30932828a612c7b0b0f687624Christian Maeder ( \ l -> case l of

63324a97283728a30932828a612c7b0b0f687624Christian Maeder [x] -> pretty x

63324a97283728a30932828a612c7b0b0f687624Christian Maeder GenVarDecl (VarDecl _ t _ _) : _ ->

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

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder <> printVarDeclType t

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

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder ppWithCommas (map ( \ (GenTypeVarDecl v) -> varOfTypeArg v) l)

63324a97283728a30932828a612c7b0b0f687624Christian Maeder <> printVarKind e c

63324a97283728a30932828a612c7b0b0f687624Christian Maeder _ -> error "printGenVarDecls") . groupBy sameType

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

933baca0720dae81434de384b32a93b47e754d09Christian MaedersameType :: GenVarDecl -> GenVarDecl -> Bool

a98fd29a06e80e447af26d898044c23497adbc73Mihai CodescusameType g1 g2 = case (g1, g2) of

da955132262baab309a50fdffe228c9efe68251dCui Jian (GenVarDecl (VarDecl _ t1 Comma _), GenVarDecl (VarDecl _ t2 _ _))

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu | t1 == t2 -> True

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu (GenTypeVarDecl (TypeArg _ e1 c1 _ _ Comma _),

da955132262baab309a50fdffe228c9efe68251dCui Jian GenTypeVarDecl (TypeArg _ e2 c2 _ _ _ _)) | e1 == e2 && c1 == c2 -> True

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu _ -> False

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu

da955132262baab309a50fdffe228c9efe68251dCui JianprintVarDeclType :: Type -> Doc

da955132262baab309a50fdffe228c9efe68251dCui JianprintVarDeclType t = case t of

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder MixfixType [] -> empty

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder _ -> space <> colon <+> pretty t

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Pretty VarDecl where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty (VarDecl v t _ _) = pretty v <> printVarDeclType t

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Pretty GenVarDecl where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty gvd = case gvd of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder GenVarDecl v -> pretty v

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder GenTypeVarDecl tv -> pretty tv

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Pretty TypeArg where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty (TypeArg v e c _ _ _ _) =

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty v <> printVarKind e c

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder-- | don't print an empty list and put parens around longer lists

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederprintList0 :: (Pretty a) => [a] -> Doc

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederprintList0 l = case l of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [] -> empty

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [x] -> pretty x

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> parens $ ppWithCommas l

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maederinstance Pretty BasicSpec where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty (BasicSpec l) = if null l then specBraces empty else

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder changeGlobalAnnos addBuiltins . vcat $ map pretty l

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maeder

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maederinstance Pretty ProgEq where

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maeder pretty = printEq0 equals . foldEq printTermRec

a9183ce3b997bf3539e427b3cd22d70c3565446eChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Pretty BasicItem where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty bi = case bi of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder SigItems s -> pretty s

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

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ClassItems i l _ -> let

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder b = semiAnnos pretty l

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder p = case map item l of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ : _ : _ -> True

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [ClassItem (ClassDecl (_ : _ : _) _ _) _ _] -> True

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> False

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder in case i of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Plain -> topSigKey (classS ++ if p then "es" else "") <+> b

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Instance -> sep [keyword classS <+>

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder keyword (instanceS ++ if p then sS else ""), b]

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder GenVarItems l _ -> topSigKey (varS ++ case l of

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder _ : _ : _ -> sS

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> "") <+> printGenVarDecls l

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder FreeDatatype l _ ->

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

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ : _ : _ -> sS

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> ""), semiAnnos pretty l]

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder GenItems l _ -> let gkw = keyword generatedS in

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder (if all (isDatatype . item) l then \ i -> gkw <+> rmTopKey i

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder else \ i -> sep [gkw, specBraces i])

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder $ vcat $ map (printAnnoted pretty) l

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder AxiomItems vs fs _ ->

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sep [ if null vs then empty else

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder forallDoc <+> printGenVarDecls vs

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder , case fs of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder [] -> empty

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> let pp = addBullet . pretty in

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder vcat $ map (printAnnoted pp) (init fs)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ++ [printSemiAnno pp True $ last fs]]

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Internal l _ -> sep [keyword internalS,

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder specBraces $ vcat $ map (printAnnoted pretty) l]

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian MaederisDatatype :: SigItems -> Bool

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian MaederisDatatype si = case si of

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder TypeItems _ l _ -> all ((\ t -> case t of

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder Datatype _ -> True

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> False) . item) l

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder _ -> False

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Pretty OpBrand where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder pretty b = keyword $ show b

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maederinstance Pretty SigItems where

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder 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 t _ ->

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

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

++ (if b then [] else

[colon <+> 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 _ 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

_ -> "") <> space