c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance{- |

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $Header$

5d801400993c9671010d244646936d8fd435638cChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : maeder@tzi.de

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceStability : experimental

5d801400993c9671010d244646936d8fd435638cChristian MaederPortability : portable

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Manceprinting data types of the abstract syntax

aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Mance-}

5d801400993c9671010d244646936d8fd435638cChristian Maeder

5d801400993c9671010d244646936d8fd435638cChristian Maedermodule HasCASL.PrintAs where

5d801400993c9671010d244646936d8fd435638cChristian Maeder

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.As

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.AsUtils

097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Manceimport HasCASL.FoldTerm

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.Builtin

852bd6145634dc2832b61c44678fe539bc1682d5Christian Maederimport Common.Id

dc8c83e9922e4746c192916565f3522418534f3aFelix Gabriel Manceimport Common.Keywords

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.DocUtils

feab1106bbee4f2ea2fd48bca7106dd041e4211dFelix Gabriel Manceimport Common.Doc

18ff56829e5e99383ee6106584d55bcbd8ed45e7Felix Gabriel Manceimport Common.AS_Annotation

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceimport Data.List (groupBy)

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance-- | short cut for: if b then empty else d

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancenoPrint :: Bool -> Doc -> Doc

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancenoPrint b d = if b then empty else d

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel MancenoNullPrint :: [a] -> Doc -> Doc

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel MancenoNullPrint = noPrint . null

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancesemiDs :: Pretty a => [a] -> Doc

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancesemiDs = fsep . punctuate semi . map pretty

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancesemiAnnoted :: Pretty a => [Annoted a] -> Doc

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancesemiAnnoted = vcat . map (printSemiAnno pretty True)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceinstance Pretty Variance where

0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Mance pretty = sidDoc . mkSimpleId . show

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

852bd6145634dc2832b61c44678fe539bc1682d5Christian Maederinstance Pretty a => Pretty (AnyKind a) where

968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder pretty knd = case knd of

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ClassKind ci -> pretty ci

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance FunKind v k1 k2 _ -> fsep [pretty v <>

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance (case k1 of

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance FunKind _ _ _ _ -> parens

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance _ -> id) (pretty k1)

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , funArrow

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , pretty k2]

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancevarOfTypeArg :: TypeArg -> Id

fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian MaedervarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder

fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maederinstance Pretty TypePattern where

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance pretty tp = case tp of

3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel Mance TypePattern name args _ -> pretty name

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance <+> fsep (map (pretty . varOfTypeArg) args)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance TypePatternToken t -> pretty t

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance MixfixTypePattern ts -> fsep $ map pretty ts

852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder BracketTypePattern k l _ -> bracket k $ ppWithCommas l

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance TypePatternArg t _ -> parens $ pretty t

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | put proper brackets around a document

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancebracket :: BracketKind -> Doc -> Doc

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancebracket b = case b of

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Parens -> parens

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Squares -> brackets

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Braces -> specBraces

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance NoBrackets -> id

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

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

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel ManceprintKind :: Kind -> Doc

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- | print the kind of a variable with its variance and a preceding colon

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceprintVarKind :: Variance -> VarKind -> Doc

852bd6145634dc2832b61c44678fe539bc1682d5Christian MaederprintVarKind e vk = case vk of

852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder Downset t ->

852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder space <> less <+> pretty t

ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder VarKind k -> space <> colon <+>

ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder pretty e <> pretty k

ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder MissingKind -> empty

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance

3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel Mancedata TypePrec = Outfix | Prefix | ProdInfix | FunInfix | Absfix

52991d9b46a98ad6a9020421a3244950b0f8a522Felix Gabriel Mance deriving (Eq, Ord)

52991d9b46a98ad6a9020421a3244950b0f8a522Felix Gabriel Mance

3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel ManceparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel ManceparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel ManceprintTypeToken :: Token -> Doc

75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel ManceprintTypeToken t = let

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance l = ("*", cross) : map ( \ (a, d) -> (show a, d) )

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance [ (FunArr, funArrow)

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , (PFunArr, pfun)

1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel Mance , (ContFunArr, cfun)

4c684d7a2343be7350eba088f8be42888f86a495Felix Gabriel Mance , (PContFunArr, pcfun) ]

1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel Mance in case lookup (tokStr t) l of

5a3ae0a9224276de25e709ef8788c1b9716cd206Christian Maeder Just d -> d

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance _ -> pretty t

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance

668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel MancetoMixType :: Type -> (TypePrec, Doc)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancetoMixType typ = case typ of

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance TypeName name _ _ -> (Outfix, pretty name)

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance TypeToken tt -> (Outfix, printTypeToken tt)

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance TypeAbs v t _ -> (Absfix, sep [ lambda <+> pretty v

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance , bullet <+> snd (toMixType t)])

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance BracketType k l _ -> (Outfix, bracket k $ sepByCommas $ map

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance (snd . toMixType) l)

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance KindedType t kind _ -> (Prefix,

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance fsep [parenPrec Prefix $ toMixType t, colon, pretty kind])

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance TypeAppl t1 t2 -> let

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance (topTy, tyArgs) = getTypeApplAux False typ

9cb6af1a7632f12b60f592ce5eb2ac51e6bd33bbFelix Gabriel Mance aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance , parenPrec Prefix $ toMixType t2 ])

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance in case topTy of

968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder TypeName name@(Id ts cs _) _k _i ->

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance case map toMixType tyArgs of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance [dArg] ->

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance case ts of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance [e1, e2, e3] | not (isPlace e1) && isPlace e2

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance && not (isPlace e3) && null cs ->

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance (Outfix, fsep [pretty e1, snd dArg, pretty e3])

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance _ -> aArgs

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance [dArg1, dArg2] ->

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance case ts of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance [e1, e2, e3] | isPlace e1 && not (isPlace e2)

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance && isPlace e3 && null cs ->

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance if tokStr e2 == prodS then

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance (ProdInfix, fsep [

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance parenPrec ProdInfix dArg1, cross,

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance parenPrec ProdInfix dArg2])

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance else -- assume fun type

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance (FunInfix, fsep [

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance parenPrec FunInfix dArg1, printTypeToken e2, snd dArg2])

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance _ -> aArgs

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance dArgs -> if name == productId (length tyArgs) then

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance (ProdInfix, fsep $ punctuate (space <> cross) $

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance map (parenPrec ProdInfix) dArgs)

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance else aArgs

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance _ -> aArgs

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceinstance Pretty Type where

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance pretty = snd . toMixType

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- no curried notation for bound variables

968930c7674ae3b63d308bf4fa651400aa263054Christian Maederinstance Pretty TypeScheme where

a921ae1da1302f673204e7b63cdce01439a9bd5eFelix Gabriel Mance pretty (TypeScheme vs t _) = let tdoc = pretty t in

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance if null vs then tdoc else

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance fsep [forallDoc, semiDs vs, bullet <+> tdoc]

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceinstance Pretty Partiality where

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance pretty p = case p of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Partial -> quMarkD

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Total -> empty

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceinstance Pretty Quantifier where

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance pretty q = case q of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Universal -> forallDoc

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Existential -> exists

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Unique -> unique

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Manceinstance Pretty TypeQual where

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance pretty q = case q of

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance OfType -> colon

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance AsType -> text asS

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance InType -> inDoc

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Inferred -> colon

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceinstance Pretty Term where

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance pretty = printTerm . rmSomeTypes

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceisSimpleTerm :: Term -> Bool

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceisSimpleTerm trm = case trm of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance QualVar _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance QualOp _ _ _ _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance ResolvedMixTerm _ _ _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance ApplTerm _ _ _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance TupleTerm _ _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance TermToken _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance BracketTerm _ _ _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance _ -> False

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- | used only to produce CASL applications

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceisSimpleArgTerm :: Term -> Bool

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceisSimpleArgTerm trm = case trm of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance QualVar vd -> not (isPatVarDecl vd)

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance QualOp _ _ _ _ -> True

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance ResolvedMixTerm n l _ -> placeCount n /= 0 || not (null l)

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance TupleTerm _ _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance BracketTerm _ _ _ -> True

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance _ -> False

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel MancehasRightQuant :: Term -> Bool

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancehasRightQuant t = case t of

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance QuantifiedTerm {} -> True

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance LambdaTerm {} -> True

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance CaseTerm {} -> True

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance LetTerm Let _ _ _ -> True

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance ResolvedMixTerm n ts _ | endPlace n && placeCount n == length ts

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance -> hasRightQuant (last ts)

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance ApplTerm (ResolvedMixTerm n [] _) t2 _ | endPlace n ->

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance case t2 of

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance _ -> hasRightQuant t2

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance ApplTerm _ t2 _ -> hasRightQuant t2

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> False

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel MancezipArgs :: Id -> [Term] -> [Doc] -> [Doc]

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel MancezipArgs n ts ds = case (ts, ds) of

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance (t : r, d : s) -> let

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance p = parenTermDoc t d

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance e = if hasRightQuant t then parens d else p

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance in if null r && null s && endPlace n then

44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maeder [if hasRightQuant t then d else p]

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance else e : zipArgs n r s

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance _ -> []

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel ManceisPatVarDecl :: VarDecl -> Bool

44985cbd4eb61dbc348617ebdd44a774e51dac07Christian MaederisPatVarDecl (VarDecl v ty _ _) = case ty of

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance TypeName t _ _ -> isSimpleId v && take 2 (show t) == "_v"

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance _ -> False

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel ManceparenTermDoc :: Term -> Doc -> Doc

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel ManceparenTermDoc trm = if isSimpleTerm trm then id else parens

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel ManceprintTermRec :: FoldRec Doc (Doc, Doc)

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel ManceprintTermRec = FoldRec

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance { foldQualVar = \ _ vd@(VarDecl v _ _ _) ->

511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance if isPatVarDecl vd then pretty v

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance else parens $ keyword varS <+> pretty vd

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance , foldQualOp = \ _ br n t _ ->

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance parens $ fsep [pretty br, pretty n, colon, pretty $

83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance if isPred br then unPredTypeScheme t else t]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , foldResolvedMixTerm = \ (ResolvedMixTerm _ os _) n ts _ ->

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance if placeCount n == length ts || null ts then

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance idApplDoc n $ zipArgs n os ts

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else idApplDoc applId [idDoc n, parens $ sepByCommas ts]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , foldApplTerm = \ (ApplTerm o1 o2 _) t1 t2 _ ->

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance case (o1, o2) of

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- comment out the following two guards for CASL applications

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (ResolvedMixTerm n [] _, TupleTerm ts _) | placeCount n == length ts

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -> idApplDoc n $ zipArgs n ts $ map printTerm ts

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (ResolvedMixTerm n [] _, _) | placeCount n == 1

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -> idApplDoc n $ zipArgs n [o2] [t2]

968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder _ -> idApplDoc applId $ zipArgs applId [o1, o2] [t1, t2]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , foldTupleTerm = \ _ ts _ -> parens $ sepByCommas ts

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , foldTypedTerm = \ (TypedTerm ot _ _ _) t q typ _ -> fsep [(case ot of

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance LambdaTerm {} -> parens

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance LetTerm {} -> parens

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance CaseTerm {} -> parens

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance QuantifiedTerm {} -> parens

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> id) t, pretty q, pretty typ]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , foldQuantifiedTerm = \ _ q vs t _ ->

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance fsep [pretty q, printGenVarDecls vs, bullet <+> t]

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , foldLambdaTerm = \ _ ps q t _ ->

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance fsep [ lambda

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , case ps of

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance [p] -> p

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> fcat $ map parens ps

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , (case q of

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance Partial -> bullet

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance Total -> bullet <> text exMark) <+> t]

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , foldCaseTerm = \ _ t es _ ->

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance fsep [text caseS, t, text ofS,

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance cat $ punctuate (space <> bar <> space) $

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance map (printEq0 funArrow) es]

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , foldLetTerm = \ _ br es t _ ->

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance let des = sep $ punctuate semi $ map (printEq0 equals) es

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance in case br of

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance Let -> fsep [sep [text letS <+> des, text inS], t]

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance Where -> fsep [sep [t, text whereS], des]

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Program -> text programS <+> des

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , foldTermToken = \ _ t -> pretty t

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , foldMixTypeTerm = \ _ q t _ -> pretty q <+> pretty t

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , foldMixfixTerm = \ _ ts -> fsep ts

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , foldBracketTerm = \ _ k l _ -> bracket k $ sepByCommas l

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance fsep [pretty v, text asP, p]

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , foldProgEq = \ _ p t _ -> (p, t)

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance }

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel ManceprintTerm :: Term -> Doc

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel ManceprintTerm = foldTerm printTermRec

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel MancermTypeRec :: MapRec

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel MancermTypeRec = mapRec

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance { foldQualOp = \ t _ (InstOpId i _ _) _ ps ->

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance if elem i $ map fst bList then

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance ResolvedMixTerm i [] ps else t

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance , foldTypedTerm = \ _ nt q ty ps ->

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance case q of

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance Inferred -> nt

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance _ -> case nt of

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance TypedTerm _ oq oty _ | oty == ty || oq == InType -> nt

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance QualVar (VarDecl _ oty _ _) | oty == ty -> nt

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance _ -> TypedTerm nt q ty ps

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance }

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel MancermSomeTypes :: Term -> Term

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel MancermSomeTypes = foldTerm rmTypeRec

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance-- | put parenthesis around applications

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel ManceparenTermRec :: MapRec

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel ManceparenTermRec = let

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance addParAppl t = case t of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance ResolvedMixTerm _ [] _ -> t

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance QualVar _ -> t

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance QualOp _ _ _ _ -> t

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance TermToken _ -> t

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance BracketTerm _ _ _ -> t

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder TupleTerm _ _ -> t

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance _ -> TupleTerm [t] nullRange

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance in mapRec

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder { foldApplTerm = \ _ t1 t2 ps ->

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder ApplTerm (addParAppl t1) (addParAppl t2) ps

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder , foldResolvedMixTerm = \ _ n ts ps ->

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder ResolvedMixTerm n (map addParAppl ts) ps

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder , foldTypedTerm = \ _ t q typ ps ->

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder TypedTerm (addParAppl t) q typ ps

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder , foldMixfixTerm = \ _ ts -> MixfixTerm $ map addParAppl ts

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder , foldAsPattern = \ _ v p ps -> AsPattern v (addParAppl p) ps

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder }

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederparenTerm :: Term -> Term

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederparenTerm = foldTerm parenTermRec

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintEq0 :: Doc -> (Doc, Doc) -> Doc

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintEq0 s (p, t) = sep [p, hsep [s, t]]

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintGenVarDecls :: [GenVarDecl] -> Doc

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintGenVarDecls = fsep . punctuate semi . map

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder ( \ l -> case l of

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder [x] -> pretty x

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder GenVarDecl (VarDecl _ t _ _) : _ ->

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder <> printVarDeclType t

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

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder <> printVarKind e c

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder _ -> error "printGenVarDecls") . groupBy sameType

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaedersameType :: GenVarDecl -> GenVarDecl -> Bool

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaedersameType g1 g2 = case (g1, g2) of

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder (GenVarDecl (VarDecl _ t1 Comma _), GenVarDecl (VarDecl _ t2 _ _))

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder | t1 == t2 -> True

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder (GenTypeVarDecl (TypeArg _ e1 c1 _ _ Comma _),

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder GenTypeVarDecl (TypeArg _ e2 c2 _ _ _ _)) | e1 == e2 && c1 == c2 -> True

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder _ -> False

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintVarDeclType :: Type -> Doc

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintVarDeclType t = case t of

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder MixfixType [] -> empty

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maederinstance Pretty VarDecl where

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

cbb0a924599bcaea230e7dcd2892cc91c49319aeChristian Maederinstance Pretty GenVarDecl where

cbb0a924599bcaea230e7dcd2892cc91c49319aeChristian Maeder pretty gvd = case gvd of

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder GenVarDecl v -> pretty v

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder GenTypeVarDecl tv -> pretty tv

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maederinstance Pretty TypeArg where

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder pretty (TypeArg v e c _ _ _ _) =

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder pretty v <> printVarKind e c

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

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

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintList0 l = case l of

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder [] -> empty

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder [x] -> pretty x

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder _ -> parens $ ppWithCommas l

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maederinstance Pretty InstOpId where

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder (brackets $ semiDs l)

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintPseudoType :: TypeScheme -> Doc

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprintPseudoType (TypeScheme l t _) = noNullPrint l (lambda

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder else fsep(map (parens . pretty) l))

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maederinstance Pretty BasicSpec where

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

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder changeGlobalAnnos addBuiltins . vcat $ map pretty l

b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Manceinstance Pretty ProgEq where

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance pretty = printEq0 equals . foldEq printTermRec

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Manceinstance Pretty BasicItem where

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance pretty bi = case bi of

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance SigItems s -> pretty s

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance ProgItems l _ -> sep [keyword programS, semiAnnoted l]

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance ClassItems i l _ -> let b = semiAnnos pretty l in case i of

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance Plain -> topSigKey classS <+> b

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

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance GenVarItems l _ -> topSigKey (varS ++ case l of

c704da29ad5d9d00c07e75f9109442d178dd990bFelix Gabriel Mance _ : _ : _ -> sS

a4a1b0cfce938fc38d5924b8fb6a7e140602ec5cFelix Gabriel Mance _ -> "") <+> printGenVarDecls l

cbb0a924599bcaea230e7dcd2892cc91c49319aeChristian Maeder FreeDatatype l _ ->

52991d9b46a98ad6a9020421a3244950b0f8a522Felix Gabriel Mance sep [keyword freeS <+> keyword (typeS ++ case l of

52991d9b46a98ad6a9020421a3244950b0f8a522Felix Gabriel Mance _ : _ : _ -> sS

52991d9b46a98ad6a9020421a3244950b0f8a522Felix Gabriel Mance _ -> ""), semiAnnos pretty l]

a4a1b0cfce938fc38d5924b8fb6a7e140602ec5cFelix Gabriel Mance GenItems l _ -> let gkw = keyword generatedS in

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance (if all (isDatatype . item) l then \ i -> gkw <+> rmTopKey i

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance else \ i -> sep [gkw, specBraces i])

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance $ vcat $ map (printAnnoted pretty) l

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance AxiomItems vs fs _ ->

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance sep [ if null vs then empty else

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance forallDoc <+> printGenVarDecls vs

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance , case fs of

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance [] -> empty

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance _ -> let pp = addBullet . pretty in

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance vcat $ map (printAnnoted pp) (init fs)

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance ++ [printSemiAnno pp True $ last fs]]

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Internal l _ -> sep [keyword internalS,

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance specBraces $ vcat $ map (printAnnoted pretty) l]

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance

c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceisDatatype :: SigItems -> Bool

962c83276bc80dd04f4a83e47eb81524d5294a4fChristian MaederisDatatype si = case si of

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance TypeItems _ l _ -> all ((\ t -> case t of

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance Datatype _ -> True

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance _ -> False) . item) l

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance _ -> False

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceinstance Pretty OpBrand where

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance pretty b = keyword $ show b

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Manceinstance Pretty SigItems where

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance pretty si = case si of

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance TypeItems i l _ -> let b = semiAnnos pretty l in case i of

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance Plain -> topSigKey ((if all (isSimpleTypeItem . item) l

e99c3c1f572d0442872bba58f187ca520ef5d040Felix Gabriel Mance then typeS else typeS) ++ plTypes l) <+> b

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance Instance ->

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance sep [keyword typeS <+> keyword (instanceS ++ plTypes l), b]

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance OpItems b l _ -> noNullPrint l $ topSigKey (show b ++ plOps l)

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance <+> let po = (prettyOpItem $ isPred b) in

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance if case item $ last l of

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance OpDecl _ _ a@(_ : _) _ -> case last a of

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance UnitOpAttr {} -> True

968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder _ -> False

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance OpDefn {} -> True

1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder _ -> False

c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance then vcat (map (printSemiAnno po True) l)

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance else semiAnnos po l

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance

8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceplTypes :: [Annoted TypeItem] -> String

962c83276bc80dd04f4a83e47eb81524d5294a4fChristian MaederplTypes l = case map item l of

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance _ : _ : _ -> sS

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance [TypeDecl (_ : _ : _) _ _] -> sS

ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance [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 _) = 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 _ -> 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 p t _ ->

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

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

++ (if b then [] else

[colon <> pretty p <+> prettyTypeScheme b s <> space])

++ [(if b then equiv else equals) <> space, pretty t]

instance Pretty BinOpAttr where

pretty a = text $ case a of

Assoc -> assocS

Comm -> commS

Idem -> idemS

instance Pretty OpAttr where

pretty oa = case oa of

BinOpAttr a _ -> pretty a

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

instance Pretty DatatypeDecl where

pretty (DatatypeDecl p k alts d _) =

fsep [ pretty p <> printKind k, defn

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

$ map pretty alts)

, case d of

[] -> empty

_ -> keyword derivingS <+> ppWithCommas d]

instance Pretty Alternative where

pretty alt = case alt of

Constructor n cs p _ -> pretty n <+> fsep

(map ( \ l -> case (l, p) of

-- comment out the following line to output real CASL

([NoSelector (TypeToken t)], Total) | isSimpleId n -> pretty t

_ -> parens $ semiDs l) cs) <> pretty p

Subtype l _ -> text (if all isSimpleType l then typeS else typeS)

<+> ppWithCommas l

instance Pretty Component where

pretty sel = case sel of

Selector n p t _ _ -> sep [pretty n, colon <> pretty p <+> pretty t]

NoSelector t -> pretty t

instance Pretty OpId where

pretty (OpId n ts _) =

sep $ pretty n : if null ts then [] else [brackets $ ppWithCommas ts]

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