fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance{- |

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceModule : $Header$

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceCopyright : (c) Christian Maeder and Uni Bremen 2003

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceMaintainer : maeder@tzi.de

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceStability : experimental

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancePortability : portable

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceprinting data types of the abstract syntax

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance-}

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mancemodule HasCASL.PrintAs where

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceimport HasCASL.As

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceimport HasCASL.AsUtils

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceimport HasCASL.FoldTerm

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceimport HasCASL.Builtin

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceimport Common.Id

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceimport Common.Keywords

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceimport Common.DocUtils

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceimport Common.Doc

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Manceimport Common.AS_Annotation

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceimport Data.List (groupBy)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancenoPrint :: Bool -> Doc -> Doc

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancenoNullPrint :: [a] -> Doc -> Doc

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancenoNullPrint = noPrint . null

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancesemiDs = fsep . punctuate semi . map pretty

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

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

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceinstance Pretty Variance where

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance pretty = sidDoc . mkSimpleId . show

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceinstance Pretty a => Pretty (AnyKind a) where

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance pretty knd = case knd of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance ClassKind ci -> pretty ci

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance (case k1 of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance FunKind _ _ _ _ -> parens

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , funArrow

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , pretty k2]

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancevarOfTypeArg :: TypeArg -> Id

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel MancevarOfTypeArg (TypeArg i _ _ _ _ _ _) = i

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceinstance Pretty TypePattern where

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance pretty tp = case tp of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance TypePattern name args _ -> pretty name

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance TypePatternToken t -> pretty t

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance BracketTypePattern k l _ -> bracket k $ ppWithCommas l

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mancebracket :: BracketKind -> Doc -> Doc

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mancebracket b = case b of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance Parens -> parens

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance Squares -> brackets

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance Braces -> specBraces

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance NoBrackets -> id

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance-- | print a 'Kind' plus a preceding colon (or nothing)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceprintKind :: Kind -> Doc

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

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

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceprintVarKind e vk = case vk of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance Downset t ->

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance space <> less <+> pretty t

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance VarKind k -> space <> colon <+>

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance pretty e <> pretty k

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance MissingKind -> empty

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mancedata TypePrec = Outfix | Prefix | ProdInfix | FunInfix deriving (Eq, Ord)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceprintTypeToken :: Token -> Doc

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel ManceprintTypeToken t = let

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

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance [ (FunArr, funArrow)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , (PFunArr, pfun)

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance , (ContFunArr, cfun)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance , (PContFunArr, pcfun) ]

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance in case lookup (tokStr t) l of

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance Just d -> d

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance _ -> pretty t

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel MancetoMixType :: Type -> (TypePrec, Doc)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel MancetoMixType typ = case typ of

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance ExpandedType t1 _ -> toMixType t1

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance BracketType k l _ -> (Outfix, bracket k $ sepByCommas $ map

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance (snd . toMixType) l)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance KindedType t kind _ -> (Prefix,

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

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

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance _ -> let (topTy, tyArgs) = getTypeAppl typ in

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance case topTy of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance TypeName name@(Id ts cs _) _k _i -> let topDoc = pretty name in

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance case tyArgs of

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance [] -> (Outfix, pretty name)

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Mance [arg] -> let dArg = toMixType arg in

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance case ts of

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

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

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

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance _ -> (Prefix, fsep [topDoc, parenPrec Prefix dArg])

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance [arg1, arg2] -> let dArg1 = toMixType arg1

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance dArg2 = toMixType arg2 in

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance case ts of

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

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

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance if tokStr e2 == prodS then

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance (ProdInfix, fsep [

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance parenPrec ProdInfix dArg1, cross,

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance parenPrec ProdInfix dArg2])

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance else -- assume fun type

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance (FunInfix, fsep [

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

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance _ -> (Prefix, fsep [topDoc, parenPrec Prefix dArg1,

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance parenPrec Prefix dArg2])

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance _ -> if name == productId (length tyArgs) then

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

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance map (parenPrec ProdInfix . toMixType) tyArgs)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance else (Prefix, fsep $ topDoc :

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance map (parenPrec Prefix . toMixType) tyArgs)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance _ | null tyArgs -> (Outfix, printType topTy)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance _ -> (Prefix, fsep $ parenPrec ProdInfix (toMixType topTy)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance : map (parenPrec Prefix . toMixType) tyArgs)

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel Mance

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel ManceprintType :: Type -> Doc

ce5d83770556362fe2c8b567975c2a3758888358Felix Gabriel ManceprintType ty = case ty of

c92573b85930868b709024284c0f13dbcaec9554Felix Gabriel Mance TypeName name _ _ -> pretty name

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance TypeAppl t1 t2 -> fcat [parens (printType t1),

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance parens (printType t2)]

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance ExpandedType t1 t2 -> fcat [printType t1, text asP, printType t2]

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance TypeToken t -> printTypeToken t

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance BracketType k l _ -> bracket k $ sepByCommas $ map (printType) l

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance KindedType t kind _ -> sep [printType t, colon <+> pretty kind]

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance MixfixType ts -> fsep $ map printType ts

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Manceinstance Pretty Type where

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance pretty = snd . toMixType

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance-- no curried notation for bound variables

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Manceinstance Pretty TypeScheme where

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

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance if null vs then tdoc else

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

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Manceinstance Pretty Partiality where

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance pretty p = case p of

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance Partial -> quMarkD

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance Total -> empty

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Manceinstance Pretty Quantifier where

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance pretty q = case q of

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance Universal -> forallDoc

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance Existential -> exists

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance Unique -> unique

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Manceinstance Pretty TypeQual where

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance pretty q = case q of

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance OfType -> colon

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance AsType -> text asS

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance InType -> inDoc

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance Inferred -> colon

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance

ae2e84ab0a53874417f01b792cbc6907ee6d09f6Felix Gabriel Manceinstance Pretty Term where

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance pretty = printTerm . rmSomeTypes

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceisSimpleTerm :: Term -> Bool

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceisSimpleTerm trm = case trm of

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance QualVar _ -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance QualOp _ _ _ _ -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance ResolvedMixTerm _ _ _ -> True

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance ApplTerm _ _ _ -> True

4440f5c4ab1cb6dfd445da97f87a72d87d24c25aFelix Gabriel Mance TupleTerm _ _ -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance TermToken _ -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance BracketTerm _ _ _ -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance _ -> False

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceisSimpleArgTerm :: Term -> Bool

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceisSimpleArgTerm trm = case trm of

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance QualOp _ _ _ _ -> True

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance TupleTerm _ _ -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance BracketTerm _ _ _ -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance _ -> False

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancehasRightQuant :: Term -> Bool

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancehasRightQuant t = case t of

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance QuantifiedTerm {} -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance LambdaTerm {} -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance CaseTerm {} -> True

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance LetTerm Let _ _ _ -> True

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance -> hasRightQuant (last ts)

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance case t2 of

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance _ -> hasRightQuant t2

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance ApplTerm _ t2 _ -> hasRightQuant t2

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance _ -> False

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancezipArgs :: Id -> [Term] -> [Doc] -> [Doc]

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel MancezipArgs n ts ds = case (ts, ds) of

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance p = parenTermDoc t d

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

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance [if hasRightQuant t then d else p]

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance else e : zipArgs n r s

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance _ -> []

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceisPatVarDecl :: VarDecl -> Bool

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceisPatVarDecl (VarDecl v ty _ _) = case ty of

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance _ -> False

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceparenTermDoc :: Term -> Doc -> Doc

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceparenTermDoc trm = if isSimpleTerm trm then id else parens

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceprintTermRec :: FoldRec Doc (Doc, Doc)

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel ManceprintTermRec = FoldRec

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance if isPatVarDecl vd then pretty v

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

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance parens $ fsep [pretty br, pretty n, colon, pretty $

808e2693447ecc5a311a2b9de6b81ca07f193778Felix Gabriel Mance if isPred br then unPredTypeScheme t else t]

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

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance idApplDoc n $ zipArgs n os ts

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

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

fae04f4a69922eb1ddf0f46b34fa15a5a080b693Felix Gabriel Mance case (o1, o2) of

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

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

-> idApplDoc n $ zipArgs n ts $ map printTerm ts

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

-> idApplDoc n $ zipArgs n [o2] [t2]

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

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

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

LambdaTerm {} -> parens

LetTerm {} -> parens

CaseTerm {} -> parens

QuantifiedTerm {} -> parens

_ -> id) t, pretty q, pretty typ]

, foldQuantifiedTerm = \ _ q vs t _ ->

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

, foldLambdaTerm = \ _ ps q t _ ->

fsep [ lambda

, case ps of

[p] -> p

_ -> fcat $ map parens ps

, (case q of

Partial -> bullet

Total -> bullet <> text exMark) <+> t]

, foldCaseTerm = \ _ t es _ ->

fsep [text caseS, t, text ofS,

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

map (printEq0 funArrow) es]

, foldLetTerm = \ _ br es t _ ->

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

in case br of

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

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

Program -> text programS <+> des

, foldTermToken = \ _ t -> pretty t

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

, foldMixfixTerm = \ _ ts -> fsep ts

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

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

fsep [pretty v, text asP, p]

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

}

printTerm :: Term -> Doc

printTerm = foldTerm printTermRec

rmTypeRec :: MapRec

rmTypeRec = mapRec

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

if elem i $ map fst bList then

ResolvedMixTerm i [] ps else t

, foldTypedTerm = \ _ nt q ty ps ->

case q of

Inferred -> nt

_ -> case nt of

TypedTerm _ oq oty _ | oty == ty || oq == InType -> nt

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

_ -> TypedTerm nt q ty ps

}

rmSomeTypes :: Term -> Term

rmSomeTypes = foldTerm rmTypeRec

-- | put parenthesis around applications

parenTermRec :: MapRec

parenTermRec = let

addParAppl t = case t of

ResolvedMixTerm _ [] _ -> t

QualVar _ -> t

QualOp _ _ _ _ -> t

TermToken _ -> t

BracketTerm _ _ _ -> t

TupleTerm _ _ -> t

_ -> TupleTerm [t] nullRange

in mapRec

{ foldApplTerm = \ _ t1 t2 ps ->

ApplTerm (addParAppl t1) (addParAppl t2) ps

, foldResolvedMixTerm = \ _ n ts ps ->

ResolvedMixTerm n (map addParAppl ts) ps

, foldTypedTerm = \ _ t q typ ps ->

TypedTerm (addParAppl t) q typ ps

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

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

}

parenTerm :: Term -> Term

parenTerm = foldTerm parenTermRec

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

printEq0 :: Doc -> (Doc, Doc) -> Doc

printEq0 s (p, t) = sep [p, hsep [s, t]]

printGenVarDecls :: [GenVarDecl] -> Doc

printGenVarDecls = fsep . punctuate semi . map

( \ l -> case l of

[x] -> pretty x

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

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

<> printVarDeclType t

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

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

_ -> space <> 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 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 fsep(map (parens . pretty) l))

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

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 in case i of

Plain -> topSigKey classS <+> b

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

GenVarItems l _ -> topSigKey (varS ++ case l of

_ : _ : _ -> sS

_ -> "") <+> printGenVarDecls l

FreeDatatype l _ ->

sep [keyword freeS <+> keyword (typeS ++ case l of

_ : _ : _ -> sS

_ -> ""), 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]

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 _) = 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