967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |

967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$

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

f11f713bebd8e1e623a0a4361065df256033de47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de

967e5f3c25249c779575864692935627004d3f9eChristian MaederStability : experimental

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederprinting data types of the abstract syntax

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-}

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maedermodule HasCASL.PrintAs where

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport HasCASL.As

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport HasCASL.AsUtils

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport HasCASL.FoldTerm

650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maederimport HasCASL.Builtin

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maederimport Common.Id

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maederimport Common.Keywords

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Common.DocUtils

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport Common.Doc

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederimport Common.AS_Annotation

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport qualified Data.Set as Set

ad187062b0009820118c1b773a232e29b879a2faChristian Maederimport Data.List

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

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

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedernoPrint :: Bool -> Doc -> Doc

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaedernoPrint b d = if b then empty else d

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaedernoNullPrint :: [a] -> Doc -> Doc

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedernoNullPrint = noPrint . null

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedersemiDs :: Pretty a => [a] -> Doc

7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedersemiDs = fsep . punctuate semi . map pretty

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

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

7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedersemiAnnoted = vcat . map (printSemiAnno pretty True)

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maederinstance Pretty Variance where

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder pretty = sidDoc . mkSimpleId . show

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

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

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder pretty knd = case knd of

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder ClassKind ci -> pretty ci

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder FunKind v k1 k2 _ -> fsep

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

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder FunKind {} -> parens

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder _ -> id) (pretty k1)

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder , funArrow, pretty k2]

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedervarOfTypeArg :: TypeArg -> Id

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaedervarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maederinstance Pretty TypePattern where

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder pretty tp = case tp of

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

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

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder if placeCount name == length args then

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

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder case l of

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder x : r -> (r, x)

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder _ -> error "Pretty TypePattern"

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder else (l, printTypeToken t)) ds ts

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

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder [brackets $ sepByCommas $ map printTypeId cs])

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder ++ ras

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder else printTypeId name <+> fsep ds

67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder TypePatternToken t -> printTypeToken t

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder MixfixTypePattern ts -> fsep $ map pretty ts

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder TypePatternArg t _ -> parens $ pretty t

d48085f765fca838c1d972d2123601997174583dChristian Maeder

d48085f765fca838c1d972d2123601997174583dChristian Maeder-- | put proper brackets around a document

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederbracket :: BracketKind -> Doc -> Doc

d48085f765fca838c1d972d2123601997174583dChristian Maederbracket b = case b of

d48085f765fca838c1d972d2123601997174583dChristian Maeder Parens -> parens

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder Squares -> brackets

d48085f765fca838c1d972d2123601997174583dChristian Maeder Braces -> specBraces

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder NoBrackets -> id

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

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

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederprintKind :: Kind -> Doc

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederprintKind k = noPrint (k == universe) $ printVarKind NonVar (VarKind k)

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

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

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederprintVarKind :: Variance -> VarKind -> Doc

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederprintVarKind e vk = case vk of

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder Downset t -> less <+> pretty t

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder VarKind k -> colon <+> pretty e <> pretty k

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder MissingKind -> empty

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

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

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder deriving (Eq, Ord)

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

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

f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederprintTypeToken :: Token -> Doc

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederprintTypeToken t = let

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

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder [ (FunArr, funArrow)

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , (PFunArr, pfun)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , (ContFunArr, cfun)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , (PContFunArr, pcfun) ]

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder in case lookup (tokStr t) l of

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder Just d -> d

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder _ -> pretty t

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederprintTypeId :: Id -> Doc

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

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder fcat $ map printTypeToken toks

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

99f1a09ee1847410faf46527f5465bd2070800c2Christian Maeder ++ map printTypeToken pls

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian MaedertoMixType :: Type -> (TypePrec, Doc)

81d182b21020b815887e9057959228546cf61b6bChristian MaedertoMixType typ = case typ of

242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder TypeName name _ _ -> (Outfix, printTypeId name)

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder TypeToken tt -> (Outfix, printTypeToken tt)

242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder TypeAbs v t _ ->

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

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder BracketType k l _ ->

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

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder KindedType t kind _ -> (Lazyfix, sep

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder [ parenPrec Lazyfix $ toMixType t

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

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

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder TypeAppl t1 t2 -> let

2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder (topTy, tyArgs) = getTypeApplAux False typ

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

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder , parenPrec Prefix $ toMixType t2 ])

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder in case topTy of

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski TypeName name@(Id ts cs _) _k _i ->

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder case map toMixType tyArgs of

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder [dArg] -> case ts of

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder [e] | name == lazyTypeId ->

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

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

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski && not (isPlace e3) && null cs ->

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

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder _ -> aArgs

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder [dArg1, dArg2] -> case ts of

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

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder if tokStr e2 == prodS then

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder (ProdInfix, fsep

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski [ parenPrec ProdInfix dArg1

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , cross, parenPrec ProdInfix dArg2])

967e5f3c25249c779575864692935627004d3f9eChristian Maeder else -- assume fun type

967e5f3c25249c779575864692935627004d3f9eChristian Maeder (FunInfix, fsep

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder [ parenPrec FunInfix dArg1

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , printTypeToken e2, snd dArg2])

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder _ -> aArgs

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder dArgs -> if isProductIdWithArgs name $ length tyArgs then

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

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder map (parenPrec ProdInfix) dArgs) else aArgs

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder _ -> aArgs

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederinstance Pretty Type where

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder pretty = snd . toMixType

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederprintTypeScheme :: PolyId -> TypeScheme -> Doc

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederprintTypeScheme (PolyId _ tys _) (TypeScheme vs t _) =

967e5f3c25249c779575864692935627004d3f9eChristian Maeder let tdoc = pretty t in

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

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

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- no curried notation for bound variables

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederinstance Pretty TypeScheme where

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

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian Maederinstance Pretty Partiality where

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder pretty p = case p of

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Partial -> quMarkD

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Total -> empty

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian Maederinstance Pretty Quantifier where

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder pretty q = case q of

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Universal -> forallDoc

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Existential -> exists

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Unique -> unique

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian Maederinstance Pretty TypeQual where

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder pretty q = case q of

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder OfType -> colon

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder AsType -> text asS

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder InType -> inDoc

2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Inferred -> colon

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian Maederinstance Pretty Term where

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder pretty = printTerm . rmSomeTypes

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian MaederisSimpleTerm :: Term -> Bool

ad187062b0009820118c1b773a232e29b879a2faChristian MaederisSimpleTerm trm = case trm of

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder QualVar _ -> True

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder QualOp {} -> True

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder ResolvedMixTerm {} -> True

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder ApplTerm {} -> True

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder TupleTerm _ _ -> True

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder TermToken _ -> True

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder BracketTerm {} -> True

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder _ -> False

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder-- | used only to produce CASL applications

ad187062b0009820118c1b773a232e29b879a2faChristian MaederisSimpleArgTerm :: Term -> Bool

ad187062b0009820118c1b773a232e29b879a2faChristian MaederisSimpleArgTerm trm = case trm of

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder QualVar vd -> not (isPatVarDecl vd)

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder QualOp {} -> True

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

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder TupleTerm _ _ -> True

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder BracketTerm {} -> True

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder _ -> False

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederhasRightQuant :: Term -> Bool

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederhasRightQuant t = case t of

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder QuantifiedTerm {} -> True

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder LambdaTerm {} -> True

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder CaseTerm {} -> True

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder LetTerm Let _ _ _ -> True

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder ResolvedMixTerm n _ ts _ | endPlace n && placeCount n == length ts

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder -> hasRightQuant (last ts)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ApplTerm (ResolvedMixTerm n _ [] _) t2 _ | endPlace n ->

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder case t2 of

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder _ -> hasRightQuant t2

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder ApplTerm _ t2 _ -> hasRightQuant t2

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder _ -> False

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder

b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederzipArgs :: Id -> [Term] -> [Doc] -> [Doc]

588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederzipArgs n ts ds = case (ts, ds) of

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder (t : r, d : s) -> let

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder 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

_ -> ""