9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder{- |

eb483f2216949400bfef8f6deb5320f071445626Christian MaederModule : $Header$

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

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

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

eb483f2216949400bfef8f6deb5320f071445626Christian MaederMaintainer : maeder@tzi.de

eb483f2216949400bfef8f6deb5320f071445626Christian MaederStability : experimental

eb483f2216949400bfef8f6deb5320f071445626Christian MaederPortability : portable

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederprinting data types of the abstract syntax

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-}

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

eb483f2216949400bfef8f6deb5320f071445626Christian Maedermodule HasCASL.PrintAs where

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport HasCASL.As

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport HasCASL.AsUtils

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport HasCASL.FoldTerm

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport HasCASL.Builtin

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Id

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Keywords

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.DocUtils

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Doc

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.AS_Annotation

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedernoPrint :: Bool -> Doc -> Doc

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedernoPrint b d = if b then empty else d

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedernoNullPrint :: [a] -> Doc -> Doc

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedernoNullPrint = noPrint . null

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedersemiDs :: Pretty a => [a] -> Doc

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedersemiDs = fsep . punctuate semi . map pretty

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedersemiAnnoted :: Pretty a => [Annoted a] -> Doc

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedersemiAnnoted = semiAnnos pretty

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Pretty Variance where

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder pretty = sidDoc . mkSimpleId . show

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Pretty a => Pretty (AnyKind a) where

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder pretty knd = case knd of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder ClassKind ci -> pretty ci

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (case k1 of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder FunKind _ _ _ _ -> parens

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> id) (pretty k1)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , funArrow

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , pretty k2]

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Pretty TypePattern where

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder pretty tp = case tp of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder TypePattern name args _ -> pretty name

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder <> fcat (map (parens . pretty) args)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder TypePatternToken t -> pretty t

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder MixfixTypePattern ts -> fsep (map (pretty) ts)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder TypePatternArg t _ -> parens $ pretty t

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | put proper brackets around a document

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederbracket :: BracketKind -> Doc -> Doc

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederbracket b = case b of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Parens -> parens

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Squares -> brackets

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Braces -> specBraces

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder NoBrackets -> id

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederprintKind :: Kind -> Doc

2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian MaederprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

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

2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian MaederprintVarKind :: Variance -> VarKind -> Doc

2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian MaederprintVarKind e vk = case vk of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Downset t ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder space <> less <+> pretty t

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder VarKind k -> space <> colon <+>

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder pretty e <> pretty k

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder MissingKind -> empty

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

eb483f2216949400bfef8f6deb5320f071445626Christian Maederdata TypePrec = Outfix | Prefix | ProdInfix | FunInfix deriving (Eq, Ord)

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

7325bbe03797fd413af504fb3fac109b2c652a7bChristian MaederparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

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

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

eb483f2216949400bfef8f6deb5320f071445626Christian MaedertoMixType :: Type -> (TypePrec, Doc)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedertoMixType typ = case typ of

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ExpandedType t1 _ -> toMixType t1

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder {- (Prefix, ExpandedType

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (parenPrec Prefix $ toMixType t1)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder $ parenPrec Prefix $ toMixType t2) -}

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder BracketType k l _ -> (Outfix, bracket k $ sepByCommas $ map

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski (snd . toMixType) l)

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski KindedType t kind _ -> (Prefix,

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski fsep [parenPrec Prefix $ toMixType t, colon, pretty kind])

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski _ -> let (topTy, tyArgs) = getTypeAppl typ in

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski case topTy of

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski TypeName name@(Id ts cs _) _k _i -> let topDoc = pretty name in

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski case tyArgs of

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski [] -> (Outfix, pretty name)

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski [arg] -> let dArg = toMixType arg in

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski case ts of

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski [e1, e2, e3] | not (isPlace e1) && isPlace e2

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski && not (isPlace e3) && null cs ->

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski (Outfix, fsep [pretty e1, snd dArg, pretty e3])

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski _ -> (Prefix, fsep [topDoc, parenPrec Prefix dArg])

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski [arg1, arg2] -> let dArg1 = toMixType arg1

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder dArg2 = toMixType arg2 in

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder case ts of

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

083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski && isPlace e3 && null cs ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder if tokStr e2 == prodS then

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (ProdInfix, fsep [

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder parenPrec ProdInfix dArg1, cross,

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder parenPrec ProdInfix dArg2])

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder else -- assume fun type

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder (FunInfix, fsep [

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder parenPrec FunInfix dArg1, pretty e2, snd dArg2])

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> (Prefix, fsep [topDoc, parenPrec Prefix dArg1,

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder parenPrec Prefix dArg2])

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> if name == productId (length tyArgs) then

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

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder map (parenPrec ProdInfix . toMixType) tyArgs)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder else (Prefix, fsep $ topDoc :

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder map (parenPrec Prefix . toMixType) tyArgs)

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder _ | null tyArgs -> (Outfix, printType topTy)

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder _ -> (Prefix, fsep $ parenPrec ProdInfix (toMixType topTy)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder : map (parenPrec Prefix . toMixType) tyArgs)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederprintType :: Type -> Doc

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederprintType ty = case ty of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder TypeName name _ _ -> pretty name

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder TypeAppl t1 t2 -> fcat [parens (printType t1),

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder parens (printType t2)]

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ExpandedType t1 t2 -> fcat [printType t1, text asP, printType t2]

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder TypeToken t -> pretty t

1509ea46b471bef1c5e70864fb1cfc0a5280266bChristian Maeder BracketType k l _ -> bracket k $ sepByCommas $ map (printType) l

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder KindedType t kind _ -> sep [printType t, colon <+> pretty kind]

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder MixfixType ts -> fsep $ map printType ts

afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Pretty Type where

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder pretty = snd . toMixType

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- no curried notation for bound variables

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Pretty TypeScheme where

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

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder if null vs then tdoc else

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder fsep [forallDoc, semiDs vs, bullet, tdoc]

afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder

afbd86903151121381e4e9d22862136817d7f0f0Christian Maederinstance Pretty Partiality where

afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder pretty p = case p of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Partial -> quMarkD

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Total -> empty

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Pretty Quantifier where

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder pretty q = case q of

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Universal -> forallDoc

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Existential -> exists

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Unique -> unique

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

eb483f2216949400bfef8f6deb5320f071445626Christian Maederinstance Pretty TypeQual where

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder pretty q = case q of

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder OfType -> colon

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder AsType -> text asS

afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder InType -> inDoc

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Inferred -> colon

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

eb483f2216949400bfef8f6deb5320f071445626Christian Maederinstance Pretty Term where

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder pretty = changeGlobalAnnos addBuiltins . printTerm . rmSomeTypes

afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder

afbd86903151121381e4e9d22862136817d7f0f0Christian MaederisSimpleTerm :: Term -> Bool

afbd86903151121381e4e9d22862136817d7f0f0Christian MaederisSimpleTerm trm = case trm of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder QualVar _ -> True

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder QualOp _ _ _ _ -> True

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ResolvedMixTerm _ _ _ -> True

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ApplTerm _ _ _ -> True

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder TupleTerm _ _ -> True

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder TermToken _ -> True

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder BracketTerm _ _ _ -> True

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder _ -> False

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederparenTermDoc :: Term -> Doc -> Doc

eb483f2216949400bfef8f6deb5320f071445626Christian MaederparenTermDoc trm = if isSimpleTerm trm then id else parens

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

eb483f2216949400bfef8f6deb5320f071445626Christian MaederprintTermRec :: FoldRec Doc (Doc, Doc)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederprintTermRec = FoldRec

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder { foldQualVar = \ _ vd@(VarDecl v ty _ _) ->

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder case ty of

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder TypeName t _ _

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder | isSimpleId v && take 2 (show t) == "_v"

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -> pretty v

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> parens $ keyword varS <+> pretty vd

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , foldQualOp = \ _ br n t _ ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder parens $ fsep [pretty br, pretty n, colon, pretty $

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder if isPred br then unPredTypeScheme t else t]

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder , foldResolvedMixTerm = \ (ResolvedMixTerm _ os _) n ts _ ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder if placeCount n == length ts || null ts then

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder idApplDoc n $ zipWith parenTermDoc os ts

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , foldApplTerm = \ (ApplTerm o1 o2 _) t1 t2 _ ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder case (o1, o2) of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (ResolvedMixTerm n [] _, TupleTerm ts _)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | placeCount n == length ts ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder idApplDoc n $ zipWith parenTermDoc ts $ map printTerm ts

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (ResolvedMixTerm n [] _, _) | placeCount n == 1 ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder idApplDoc n [parenTermDoc o2 t2]

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder _ -> idApplDoc applId [parenTermDoc o1 t1, parenTermDoc o2 t2]

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

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

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder LambdaTerm {} -> parens

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder LetTerm {} -> parens

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder CaseTerm {} -> parens

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder QuantifiedTerm {} -> parens

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> id) t, pretty q, pretty typ]

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , foldQuantifiedTerm = \ _ q vs t _ ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder fsep [pretty q, semiDs vs, bullet, t]

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , foldLambdaTerm = \ _ ps q t _ ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder fsep [ lambda

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder , case ps of

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder [p] -> p

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder _ -> fcat $ map parens ps

7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder , case q of

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Partial -> bullet

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Total -> bullet <> text exMark

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder , t]

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , foldCaseTerm = \ _ t es _ ->

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder fsep [text caseS, t, text ofS,

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder cat $ punctuate (space <> bar <> space) $

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder map (printEq0 funArrow) es]

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder , foldLetTerm = \ _ br es t _ ->

7325bbe03797fd413af504fb3fac109b2c652a7bChristian Maeder let des = sep $ punctuate semi $ map (printEq0 equals) es

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder in case br of

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

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Where -> fsep [sep [t, text whereS], des]

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder Program -> text programS <+> des

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder , foldTermToken = \ _ t -> pretty t

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder , foldMixTypeTerm = \ _ q t _ -> pretty q <+> pretty t

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder , foldMixfixTerm = \ _ ts -> fsep ts

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

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder , foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder fsep [pretty v, text asP, p]

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder , foldProgEq = \ _ p t _ -> (p, t)

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder }

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederprintTerm :: Term -> Doc

50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederprintTerm = foldTerm printTermRec

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski

50dce6b011347f92377adb8bbabaeeb80975e86dChristian MaederrmTypeRec :: MapRec

90bf4bf40789422552e566b73738ba5efae144c3Christian MaederrmTypeRec = mapRec

50dce6b011347f92377adb8bbabaeeb80975e86dChristian Maeder { -- foldQualVar = \ _ (VarDecl v _ _ ps) -> ResolvedMixTerm v [] ps

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski foldQualOp = \ t _ (InstOpId i _ _) _ ps ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder if elem i $ map fst bList then

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder ResolvedMixTerm i [] ps else t

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , foldTypedTerm = \ _ nt q ty ps ->

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder case q of

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder Inferred -> nt

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> case nt of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder TypedTerm _ oq oty _ | oty == ty || oq == InType -> nt

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder QualVar (VarDecl _ oty _ _) | oty == ty -> nt

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder _ -> TypedTerm nt q ty ps

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder }

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederrmSomeTypes :: Term -> Term

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederrmSomeTypes = foldTerm rmTypeRec

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | print an equation with different symbols between 'Pattern' and 'Term'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederprintEq0 :: Doc -> (Doc, Doc) -> Doc

printEq0 s (p, t) = fsep [p, s, t]

instance Pretty VarDecl where

pretty (VarDecl v t _ _) = pretty v <>

case t of

MixfixType [] -> empty

_ -> space <> colon <+> pretty 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 InstOpId where

pretty (InstOpId n l _) = pretty n <> noNullPrint l

(brackets $ semiDs l)

-- | print a 'TypeScheme' as a pseudo type

printPseudoType :: TypeScheme -> Doc

printPseudoType (TypeScheme l t _) = noNullPrint l (lambda

<+> (if null $ tail l then pretty $ head l

else fcat(map (parens . pretty) l))

<+> bullet <> space) <> pretty t

instance Pretty BasicSpec where

pretty (BasicSpec l) = 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 _ -> noNullPrint l $ sep [keyword programS, semiAnnoted l]

ClassItems i l _ -> let b = semiAnnoted l in noNullPrint l $ case i of

Plain -> topSigKey classS <+>b

Instance -> sep [keyword classS <+> keyword instanceS, b]

GenVarItems l _ -> noNullPrint l $ topSigKey varS <+> semiDs l

FreeDatatype l _ -> noNullPrint l $ sep

[keyword freeS <+> keyword typeS, semiAnnoted l]

GenItems l _ -> noNullPrint l $ sep [keyword generatedS,

specBraces $ semiAnnoted l]

AxiomItems vs fs _ ->

vcat $ (if null vs then [] else

[forallDoc <+> semiDs vs])

++ (map (addBullet . pretty) fs)

Internal l _ -> noNullPrint l $ sep

[keyword internalS, specBraces $ semiAnnoted l]

instance Pretty OpBrand where

pretty b = keyword $ show b

instance Pretty SigItems where

pretty si = case si of

TypeItems i l _ -> let b = semiAnnoted l in noNullPrint l $ case i of

Plain -> topSigKey typeS <+> b

Instance -> sep [keyword typeS <+> keyword instanceS, b]

OpItems b l _ -> noNullPrint l $ topSigKey (show b) <+> semiAnnoted

(if isPred b then concat $

mapAnM ((:[]) . mapOpItem) l else l)

instance Pretty ClassItem where

pretty (ClassItem d l _) =

pretty d $+$ noNullPrint l (specBraces $ semiAnnoted l)

instance Pretty ClassDecl where

pretty (ClassDecl l k _) = fsep [ppWithCommas l, 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 _ -> noNullPrint l $ ppWithCommas l <> printKind k

SubtypeDecl l t _ ->

noNullPrint l $ 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 k t _ ->

fsep $ pretty p : (case k of

Just j | j /= universe -> [colon <+> pretty j]

_ -> [])

++ [text assignS <+> printPseudoType t]

Datatype t -> pretty t

mapOpItem :: OpItem -> OpItem

mapOpItem oi = case oi of

OpDecl l t as ps -> OpDecl l (unPredTypeScheme t) as ps

OpDefn n ps s p t qs -> OpDefn n ps (unPredTypeScheme s) p t qs

instance Pretty OpItem where

pretty oi = case oi of

OpDecl l t attrs _ -> if null l then error "pretty OpDecl" else

ppWithCommas l <+> colon <+> (pretty t

<> (noNullPrint attrs $ comma <> space)

<> ppWithCommas attrs)

OpDefn n ps s p t _ ->

fsep [fcat $ pretty n : (map (parens . semiDs) ps)

, colon <> pretty p, pretty s, equals, pretty t]

instance Pretty BinOpAttr where

pretty a = text $ case a of

Assoc -> assocS

Comm -> commS

Idem -> idemS

instance Pretty OpAttr where

pretty oa = case oa of

BinOpAttr a _ -> pretty a

UnitOpAttr t _ -> text unitS <+> pretty t

instance Pretty DatatypeDecl where

pretty (DatatypeDecl p k alts d _) =

fsep [ pretty p <> printKind k, defn

<+> cat (punctuate (space <> bar <> space)

$ map pretty alts)

, case d of

[] -> empty

_ -> keyword derivingS <+> ppWithCommas d]

instance Pretty Alternative where

pretty alt = case alt of

Constructor n cs p _ ->

pretty n <+> fsep (map ( \ l -> case (l, p) of

([NoSelector (TypeToken t)], Total)

-> pretty t

_ -> parens $ semiDs l) cs)

<> pretty p

Subtype l _ -> noNullPrint l $ text typeS <+> ppWithCommas l

instance Pretty Component where

pretty sel = case sel of

Selector n p t _ _ -> pretty n

<+> colon <> pretty p

<+> pretty t

NoSelector t -> pretty t

instance Pretty OpId where

pretty (OpId n ts _) = pretty n

<+> noNullPrint ts

(brackets $ ppWithCommas ts)

instance Pretty Symb where

pretty (Symb i mt _) =

pretty i <> (case mt of

Nothing -> empty

Just (SymbType t) ->

space <> colon <+> pretty t)

instance Pretty SymbItems where

pretty (SymbItems k syms _ _) =

printSK k <> ppWithCommas syms

instance Pretty SymbOrMap where

pretty (SymbOrMap s mt _) =

pretty s <> (case mt of

Nothing -> empty

Just t ->

space <> mapsto <+> pretty t)

instance Pretty SymbMapItems where

pretty (SymbMapItems k syms _ _) =

printSK k <> ppWithCommas syms

-- | print symbol kind

printSK :: SymbKind -> Doc

printSK k =

case k of Implicit -> empty

_ -> text (drop 3 $ show k) <> space