PrintAs.hs revision 9e0472be46104307b974fe5079bf5cc9e94a1a96
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- |
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederDescription : print the abstract syntax so that it can be re-parsed
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : Christian.Maeder@dfki.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederprinting data types of the abstract syntax
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder-}
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedermodule HasCASL.PrintAs where
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport HasCASL.As
ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport HasCASL.AsUtils
ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport HasCASL.FoldTerm
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport HasCASL.Builtin
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Common.Id
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Common.Keywords
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.DocUtils
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport Common.Doc
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.AS_Annotation
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Data.List (groupBy, mapAccumL)
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- | short cut for: if b then empty else d
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian MaedernoPrint :: Bool -> Doc -> Doc
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian MaedernoPrint b d = if b then empty else d
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaedernoNullPrint :: [a] -> Doc -> Doc
975642b989852fc24119c59cf40bc1af653608ffChristian MaedernoNullPrint = noPrint . null
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian MaedersemiDs :: Pretty a => [a] -> Doc
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedersemiDs = fsep . punctuate semi . map pretty
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedersemiAnnoted :: Pretty a => [Annoted a] -> Doc
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedersemiAnnoted = vcat . map (printSemiAnno pretty True)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederinstance Pretty Variance where
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder pretty = sidDoc . mkSimpleId . show
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederinstance Pretty a => Pretty (AnyKind a) where
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder pretty knd = case knd of
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder ClassKind ci -> pretty ci
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder FunKind v k1 k2 _ -> fsep
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder [ pretty v <> (case k1 of
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder FunKind _ _ _ _ -> parens
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder _ -> id) (pretty k1)
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder , funArrow, pretty k2]
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedervarOfTypeArg :: TypeArg -> Id
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedervarOfTypeArg (TypeArg i _ _ _ _ _ _) = i
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederinstance Pretty TypePattern where
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder pretty tp = case tp of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder TypePattern name@(Id ts cs _) args _ ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let ds = map (pretty . varOfTypeArg) args in
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder if placeCount name == length args then
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let (ras, dts) = mapAccumL ( \ l t -> if isPlace t then
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder case l of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder x : r -> (r, x)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> error "Pretty TypePattern"
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder else (l, printTypeToken t)) ds ts
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in fsep $ dts ++ (if null cs then [] else
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder [brackets $ sepByCommas $ map printTypeId cs])
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder ++ ras
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder else printTypeId name <+> fsep ds
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder TypePatternToken t -> printTypeToken t
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder MixfixTypePattern ts -> fsep $ map pretty ts
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder TypePatternArg t _ -> parens $ pretty t
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder-- | put proper brackets around a document
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederbracket :: BracketKind -> Doc -> Doc
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maederbracket b = case b of
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian Maeder Parens -> parens
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder Squares -> brackets
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Braces -> specBraces
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder NoBrackets -> id
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- | print a 'Kind' plus a preceding colon (or nothing)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederprintKind :: Kind -> Doc
d48085f765fca838c1d972d2123601997174583dChristian MaederprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | print the kind of a variable with its variance and a preceding colon
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederprintVarKind :: Variance -> VarKind -> Doc
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederprintVarKind e vk = case vk of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Downset t -> less <+> pretty t
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder VarKind k -> colon <+> pretty e <> pretty k
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder MissingKind -> empty
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederdata TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder deriving (Eq, Ord)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederparenPrec p1 (p2, d) = if p2 < p1 then d else parens d
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederprintTypeToken :: Token -> Doc
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprintTypeToken t = let
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder l = ("*", cross) : map ( \ (a, d) -> (show a, d) )
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder [ (FunArr, funArrow)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , (PFunArr, pfun)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder , (ContFunArr, cfun)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder , (PContFunArr, pcfun) ]
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder in case lookup (tokStr t) l of
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Just d -> d
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> pretty t
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederprintTypeId :: Id -> Doc
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederprintTypeId (Id ts cs _) = let (toks, pls) = splitMixToken ts in
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder fcat $ map printTypeToken toks
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder ++ (if null cs then [] else [brackets $ sepByCommas $ map printTypeId cs])
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ++ map printTypeToken pls
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedertoMixType :: Type -> (TypePrec, Doc)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedertoMixType typ = case typ of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TypeName name _ _ -> (Outfix, printTypeId name)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TypeToken tt -> (Outfix, printTypeToken tt)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TypeAbs v t _ ->
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (Absfix, sep [ lambda <+> pretty v, bullet <+> snd (toMixType t)])
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder BracketType k l _ ->
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder (Outfix, bracket k $ sepByCommas $ map (snd . toMixType) l)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder KindedType t kind _ ->
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (Lazyfix, fsep [parenPrec Lazyfix $ toMixType t, colon, pretty kind])
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TypeAppl t1 t2 -> let
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (topTy, tyArgs) = getTypeApplAux False typ
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder , parenPrec Prefix $ toMixType t2 ])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder in case topTy of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TypeName name@(Id ts cs _) _k _i ->
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder case map toMixType tyArgs of
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder [dArg] -> case ts of
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder [e] | name == lazyTypeId ->
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (Lazyfix, pretty e <+> parenPrec Lazyfix dArg)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder [e1, e2, e3] | not (isPlace e1) && isPlace e2
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder && not (isPlace e3) && null cs ->
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (Outfix, fsep [pretty e1, snd dArg, pretty e3])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> aArgs
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder [dArg1, dArg2] -> case ts of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder [_, e2, _] | isInfix name && null cs ->
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder if tokStr e2 == prodS then
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder (ProdInfix, fsep
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder [ parenPrec ProdInfix dArg1
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder , cross, parenPrec ProdInfix dArg2])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder else -- assume fun type
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (FunInfix, fsep
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder [ parenPrec FunInfix dArg1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder , printTypeToken e2, snd dArg2])
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> aArgs
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder dArgs -> if isProductIdWithArgs name $ length tyArgs then
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (ProdInfix, fsep $ punctuate (space <> cross) $
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map (parenPrec ProdInfix) dArgs) else aArgs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> aArgs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederinstance Pretty Type where
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder pretty = snd . toMixType
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- no curried notation for bound variables
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederinstance Pretty TypeScheme where
3f7009c892b16d172314abbba83d663fa0d87a65Christian Maeder pretty (TypeScheme vs t _) = let tdoc = pretty t in
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder if null vs then tdoc else
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder fsep [forallDoc, semiDs vs, bullet <+> tdoc]
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederinstance Pretty Partiality where
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder pretty p = case p of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Partial -> quMarkD
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Total -> empty
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederinstance Pretty Quantifier where
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder pretty q = case q of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Universal -> forallDoc
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Existential -> exists
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Unique -> unique
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maederinstance Pretty TypeQual where
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder pretty q = case q of
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder OfType -> colon
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder AsType -> text asS
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder InType -> inDoc
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Inferred -> colon
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederinstance Pretty Term where
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder pretty = printTerm . rmSomeTypes
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederisSimpleTerm :: Term -> Bool
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederisSimpleTerm trm = case trm of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QualVar _ -> True
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder QualOp _ _ _ _ _ -> True
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ResolvedMixTerm _ _ _ _ -> True
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder ApplTerm _ _ _ -> True
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder TupleTerm _ _ -> True
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder TermToken _ -> True
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder BracketTerm _ _ _ -> True
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder _ -> False
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- | used only to produce CASL applications
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederisSimpleArgTerm :: Term -> Bool
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederisSimpleArgTerm trm = case trm of
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder QualVar vd -> not (isPatVarDecl vd)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder QualOp _ _ _ _ _ -> True
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder ResolvedMixTerm n _ l _ -> placeCount n /= 0 || not (null l)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TupleTerm _ _ -> True
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder BracketTerm _ _ _ -> True
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> False
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederhasRightQuant :: Term -> Bool
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian MaederhasRightQuant t = case t of
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder QuantifiedTerm {} -> True
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski LambdaTerm {} -> True
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder CaseTerm {} -> True
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder LetTerm Let _ _ _ -> True
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder ResolvedMixTerm n _ ts _ | endPlace n && placeCount n == length ts
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -> hasRightQuant (last ts)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ApplTerm (ResolvedMixTerm n _ [] _) t2 _ | endPlace n ->
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder case t2 of
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> hasRightQuant t2
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder ApplTerm _ t2 _ -> hasRightQuant t2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> False
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder
f8a03685d9184046e88e1d76aabdab4f714db440Christian MaederzipArgs :: Id -> [Term] -> [Doc] -> [Doc]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederzipArgs n ts ds = case (ts, ds) of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (t : r, d : s) -> let
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder p = parenTermDoc t d
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder e = if hasRightQuant t then parens d else p
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in if null r && null s && endPlace n then
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder [if hasRightQuant t then d else p]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder else e : zipArgs n r s
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> []
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian MaederisPatVarDecl :: VarDecl -> Bool
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederisPatVarDecl (VarDecl v ty _ _) = case ty of
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder TypeName t _ _ -> isSimpleId v && take 2 (show t) == "_v"
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> False
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian MaederparenTermDoc :: Term -> Doc -> Doc
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederparenTermDoc trm = if isSimpleTerm trm then id else parens
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederprintTermRec :: FoldRec Doc (Doc, Doc)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederprintTermRec = FoldRec
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder { foldQualVar = \ _ vd@(VarDecl v _ _ _) ->
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder if isPatVarDecl vd then pretty v
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder else parens $ keyword varS <+> pretty vd
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder , foldQualOp = \ _ br n t tys _ -> (if null tys then id else
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder (<> brackets (ppWithCommas tys))) $
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder parens $ fsep [pretty br, pretty n, colon, pretty $
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder if isPred br then unPredTypeScheme t else t]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldResolvedMixTerm =
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder \ (ResolvedMixTerm _ _ os _) n@(Id toks cs ps) tys ts _ ->
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder let pn = placeCount n in if pn == length ts || null ts then
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let ds = zipArgs n os ts in
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder if null tys then idApplDoc n ds
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder else let (ftoks, _) = splitMixToken toks
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder fId = Id ftoks cs ps
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (fts, rts) = splitAt (placeCount fId) $ if null ts
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder then replicate pn $ pretty placeTok else ds
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder in fsep $ (idApplDoc fId fts <> brackets (ppWithCommas tys))
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder : rts
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder else idApplDoc applId [idDoc n, parens $ sepByCommas ts]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldApplTerm = \ (ApplTerm o1 o2 _) t1 t2 _ ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder case (o1, o2) of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -- comment out the following two guards for CASL applications
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (ResolvedMixTerm n _ [] _, TupleTerm ts@(_ : _) _)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder | placeCount n == length ts ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder idApplDoc n (zipArgs n ts $ map printTerm ts)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (ResolvedMixTerm n _ [] _, _) | placeCount n == 1
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -> idApplDoc n $ zipArgs n [o2] [t2]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> idApplDoc applId $ zipArgs applId [o1, o2] [t1, t2]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldTupleTerm = \ _ ts _ -> parens $ sepByCommas ts
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldTypedTerm = \ (TypedTerm ot _ _ _) t q typ _ -> fsep [(case ot of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder LambdaTerm {} -> parens
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder LetTerm {} -> parens
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder CaseTerm {} -> parens
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder QuantifiedTerm {} -> parens
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder ApplTerm (ResolvedMixTerm n _ [] _) arg _ ->
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder let pn = placeCount n in case arg of
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder TupleTerm ts@(_ : _) _ | pn == length ts -> parens
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder _ | pn == 1 -> parens
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder _ -> id
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder _ -> id) t, pretty q, pretty typ]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldQuantifiedTerm = \ _ q vs t _ ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder fsep [pretty q, printGenVarDecls vs, bullet <+> t]
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , foldLambdaTerm = \ _ ps q t _ ->
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder fsep [ lambda
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , case ps of
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder [p] -> if show p == "()" then empty else p
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder _ -> fcat $ map parens ps
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , (case q of
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Partial -> bullet
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Total -> bullet <> text exMark) <+> t]
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , foldCaseTerm = \ _ t es _ ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder fsep [text caseS, t, text ofS,
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder cat $ punctuate (space <> bar <> space) $
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder map (printEq0 funArrow) es]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldLetTerm = \ _ br es t _ ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let des = sep $ punctuate semi $ map (printEq0 equals) es
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder in case br of
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Let -> fsep [sep [text letS <+> des, text inS], t]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Where -> fsep [sep [t, text whereS], des]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Program -> text programS <+> des
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldTermToken = \ _ t -> pretty t
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldMixTypeTerm = \ _ q t _ -> pretty q <+> pretty t
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldMixfixTerm = \ _ ts -> fsep ts
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldBracketTerm = \ _ k l _ -> bracket k $ sepByCommas l
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder fsep [pretty v, text asP, p]
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder , foldProgEq = \ _ p t _ -> (p, t) }
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprintTerm :: Term -> Doc
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederprintTerm = foldTerm printTermRec
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederrmTypeRec :: MapRec
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederrmTypeRec = mapRec
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder { foldQualOp = \ t _ (PolyId i _ _) _ _ ps ->
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder if elem i $ map fst bList then
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder ResolvedMixTerm i [] [] ps else t
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder , foldTypedTerm = \ _ nt q ty ps ->
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case q of
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Inferred -> nt
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> case nt of
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder TypedTerm _ oq oty _ | oty == ty || oq == InType -> nt
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder QualVar (VarDecl _ oty _ _) | oty == ty -> nt
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder _ -> TypedTerm nt q ty ps }
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederrmSomeTypes :: Term -> Term
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederrmSomeTypes = foldTerm rmTypeRec
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- | put parenthesis around applications
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederparenTermRec :: MapRec
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederparenTermRec = let
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder addParAppl t = case t of
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder ResolvedMixTerm _ _ [] _ -> t
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder QualVar _ -> t
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder QualOp _ _ _ _ _ -> t
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TermToken _ -> t
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder BracketTerm _ _ _ -> t
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder TupleTerm _ _ -> t
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> TupleTerm [t] nullRange
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder in mapRec
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder { foldApplTerm = \ _ t1 t2 ps ->
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ApplTerm (addParAppl t1) (addParAppl t2) ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder , foldResolvedMixTerm = \ _ n tys ts ps ->
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder ResolvedMixTerm n tys (map addParAppl ts) ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder , foldTypedTerm = \ _ t q typ ps ->
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder TypedTerm (addParAppl t) q typ ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder , foldMixfixTerm = \ _ ts -> MixfixTerm $ map addParAppl ts
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , foldAsPattern = \ _ v p ps -> AsPattern v (addParAppl p) ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder }
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederparenTerm :: Term -> Term
975642b989852fc24119c59cf40bc1af653608ffChristian MaederparenTerm = foldTerm parenTermRec
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- | print an equation with different symbols between 'Pattern' and 'Term'
975642b989852fc24119c59cf40bc1af653608ffChristian MaederprintEq0 :: 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 ( \ (GenVarDecl (VarDecl v _ _ _)) -> v) l)
, printVarDeclType t]
GenTypeVarDecl (TypeArg _ e c _ _ _ _) : _ -> sep
[ ppWithCommas (map ( \ (GenTypeVarDecl v) -> 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 = printEq0 equals . foldEq printTermRec
instance Pretty BasicItem where
pretty bi = case bi of
SigItems s -> pretty s
ProgItems l _ -> sep [keyword programS, semiAnnoted l]
ClassItems i 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 b = keyword $ show b
instance Pretty SigItems where
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 _ -> 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
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 PolyId where
pretty (PolyId i@(Id ts cs ps) tys _) = if null tys then pretty i else
let (fts, plcs) = splitMixToken ts
in idDoc (Id fts cs ps) <> brackets (ppWithCommas tys)
<> hcat (map pretty plcs)
instance Pretty BinOpAttr where
pretty a = text $ case a of
Assoc -> assocS
Comm -> commS
Idem -> idemS
instance Pretty OpAttr where
pretty oa = case oa of
BinOpAttr a _ -> pretty a
UnitOpAttr t _ -> text unitS <+> pretty t
instance Pretty DatatypeDecl where
pretty (DatatypeDecl p k alts d _) =
fsep [ pretty p, printKind k, defn
<+> cat (punctuate (space <> bar <> space)
$ map pretty alts)
, case d of
[] -> empty
_ -> keyword derivingS <+> ppWithCommas d]
instance Pretty Alternative where
pretty alt = case alt of
Constructor n cs p _ -> pretty n <+> fsep
(map ( \ l -> case (l, p) of
-- comment out the following line to output real CASL
([NoSelector (TypeToken t)], Total) | isSimpleId n -> pretty t
_ -> parens $ semiDs l) cs) <> pretty p
Subtype l _ -> text (if all isSimpleType l then typeS else typeS)
<+> ppWithCommas l
instance Pretty Component where
pretty sel = case sel of
Selector n _ t _ _ -> sep [pretty n, colon <+> pretty t]
NoSelector t -> pretty t
instance Pretty Symb where
pretty (Symb i mt _) =
sep $ pretty i : case mt of
Nothing -> []
Just (SymbType t) -> [colon <+> pretty t]
instance Pretty SymbItems where
pretty (SymbItems k syms _ _) =
printSK k syms <> ppWithCommas syms
instance Pretty SymbOrMap where
pretty (SymbOrMap s mt _) =
sep $ pretty s : case mt of
Nothing -> []
Just t -> [mapsto <+> pretty t]
instance Pretty SymbMapItems where
pretty (SymbMapItems k syms _ _) =
printSK k syms <> ppWithCommas syms
-- | print symbol kind
printSK :: SymbKind -> [a] -> Doc
printSK k l = case k of
Implicit -> empty
_ -> keyword (drop 3 (show k) ++ case l of
_ : _ : _ -> sS
_ -> "") <> space