c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule : ./HasCASL/PrintAs.hs

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

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederMaintainer : Christian.Maeder@dfki.de

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederStability : experimental

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederprinting data types of the abstract syntax

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maedermodule HasCASL.PrintAs where

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport HasCASL.As

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport HasCASL.AsUtils

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport HasCASL.FoldTerm

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.Builtin

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.Id

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport Common.Keywords

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.DocUtils

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport Common.Doc

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.AS_Annotation

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport qualified Data.Set as Set

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport Data.List

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

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

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian MaedernoPrint :: Bool -> Doc -> Doc

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian MaedernoPrint b d = if b then empty else d

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder

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

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian MaedernoNullPrint = noPrint . null

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedersemiDs :: Pretty a => [a] -> Doc

04dada28736b4a237745e92063d8bdd49a362debChristian MaedersemiDs = fsep . punctuate semi . map pretty

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder

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

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedersemiAnnoted = vcat . map (printSemiAnno pretty True)

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederinstance Pretty Variance where

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder pretty = sidDoc . mkSimpleId . show

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederinstance Pretty a => Pretty (AnyKind a) where

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder pretty knd = case knd of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ClassKind ci -> pretty ci

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder FunKind v k1 k2 _ -> fsep

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder [ pretty v <> (case k1 of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder FunKind {} -> parens

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder _ -> id) (pretty k1)

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder , funArrow, pretty k2]

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedervarOfTypeArg :: TypeArg -> Id

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedervarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederinstance Pretty TypePattern where

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder pretty tp = case tp of

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

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

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder if placeCount name == length args then

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

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder case l of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder x : r -> (r, x)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder _ -> error "Pretty TypePattern"

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder else (l, printTypeToken t)) ds ts

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder [brackets $ sepByCommas $ map printTypeId cs])

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder ++ ras

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder else printTypeId name <+> fsep ds

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder TypePatternToken t -> printTypeToken t

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder MixfixTypePattern ts -> fsep $ map pretty ts

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder TypePatternArg t _ -> parens $ pretty t

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- | put proper brackets around a document

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederbracket :: BracketKind -> Doc -> Doc

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederbracket b = case b of

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Parens -> parens

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Squares -> brackets

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Braces -> specBraces

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder NoBrackets -> id

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

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

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederprintKind :: Kind -> Doc

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederprintKind k = noPrint (k == universe) $ printVarKind NonVar (VarKind k)

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

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

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederprintVarKind :: Variance -> VarKind -> Doc

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederprintVarKind e vk = case vk of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Downset t -> less <+> pretty t

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder VarKind k -> colon <+> pretty e <> pretty k

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder MissingKind -> empty

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederdata TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder deriving (Eq, Ord)

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaederprintTypeToken :: Token -> Doc

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederprintTypeToken t = let

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder [ (FunArr, funArrow)

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder , (PFunArr, pfun)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , (ContFunArr, cfun)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , (PContFunArr, pcfun) ]

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder in case lookup (tokStr t) l of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Just d -> d

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder _ -> pretty t

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederprintTypeId :: Id -> Doc

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fcat $ map printTypeToken toks

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ++ (if null cs then [] else [brackets $ sepByCommas $ map printTypeId cs])

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ++ map printTypeToken pls

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedertoMixType :: Type -> (TypePrec, Doc)

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedertoMixType typ = case typ of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder TypeName name _ _ -> (Outfix, printTypeId name)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder TypeToken tt -> (Outfix, printTypeToken tt)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder TypeAbs v t _ ->

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder (Absfix, sep [ lambda <+> pretty v, bullet <+> snd (toMixType t)])

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder BracketType k l _ ->

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder KindedType t kind _ -> (Lazyfix, sep

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder [ parenPrec Lazyfix $ toMixType t

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

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

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder TypeAppl t1 t2 -> let

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder (topTy, tyArgs) = getTypeApplAux False typ

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder , parenPrec Prefix $ toMixType t2 ])

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder in case topTy of

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case map toMixType tyArgs of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder [dArg] -> case ts of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder [e] | name == lazyTypeId ->

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

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

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

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

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder _ -> aArgs

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

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

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder if tokStr e2 == prodS then

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (ProdInfix, fsep

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder [ parenPrec ProdInfix dArg1

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder , cross, parenPrec ProdInfix dArg2])

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder else -- assume fun type

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (FunInfix, fsep

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder [ parenPrec FunInfix dArg1

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , printTypeToken e2, snd dArg2])

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder _ -> aArgs

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder dArgs -> if isProductIdWithArgs name $ length tyArgs then

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

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder map (parenPrec ProdInfix) dArgs) else aArgs

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder _ -> aArgs

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Pretty Type where

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder pretty = snd . toMixType

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaederprintTypeScheme :: PolyId -> TypeScheme -> Doc

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

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder let tdoc = pretty t in

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder if null vs || not (null tys) then tdoc else

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

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder-- no curried notation for bound variables

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederinstance Pretty TypeScheme where

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder pretty = printTypeScheme (PolyId applId [] nullRange)

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maederinstance Pretty Partiality where

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder pretty p = case p of

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder Partial -> quMarkD

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder Total -> empty

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederinstance Pretty Quantifier where

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder pretty q = case q of

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder Universal -> forallDoc

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder Existential -> exists

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder Unique -> unique

962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederinstance Pretty TypeQual where

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder pretty q = case q of

b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder OfType -> colon

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder AsType -> text asS

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder InType -> inDoc

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Inferred -> colon

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederinstance Pretty Term where

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder pretty = printTerm . rmSomeTypes

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederisSimpleTerm :: Term -> Bool

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederisSimpleTerm trm = case trm of

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder QualVar _ -> True

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder QualOp {} -> True

6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder ResolvedMixTerm {} -> True

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder ApplTerm {} -> True

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder TupleTerm _ _ -> True

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder TermToken _ -> True

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder BracketTerm {} -> True

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder _ -> False

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder

15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder-- | used only to produce CASL applications

15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaederisSimpleArgTerm :: Term -> Bool

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian MaederisSimpleArgTerm 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

_ -> ""