020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett{- |

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettMaintainer : maeder@tzi.de

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettStability : experimental

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettPortability : portable

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettprinting data types of the abstract syntax

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett-}

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettmodule HasCASL.PrintAs where

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport HasCASL.As

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport HasCASL.AsUtils

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport HasCASL.FoldTerm

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblettimport HasCASL.Builtin

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.Id

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.Keywords

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettimport Common.DocUtils

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederimport Common.Doc

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederimport Common.AS_Annotation

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett-- | short cut for: if b then empty else d

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettnoPrint :: Bool -> Doc -> Doc

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettnoPrint b d = if b then empty else d

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettnoNullPrint :: [a] -> Doc -> Doc

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettnoNullPrint = noPrint . null

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettsemiDs :: Pretty a => [a] -> Doc

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettsemiDs = fsep . punctuate semi . map pretty

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettsemiAnnoted :: Pretty a => [Annoted a] -> Doc

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettsemiAnnoted = semiAnnos pretty

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettinstance Pretty Variance where

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett pretty = sidDoc . mkSimpleId . show

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettinstance Pretty a => Pretty (AnyKind a) where

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett pretty knd = case knd of

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett ClassKind ci -> pretty ci

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett FunKind v k1 k2 _ -> fsep [pretty v <>

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett (case k1 of

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett FunKind _ _ _ _ -> parens

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett _ -> id) (pretty k1)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett , funArrow

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett , pretty k2]

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblettinstance Pretty TypePattern where

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett pretty tp = case tp of

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett TypePattern name args _ -> pretty name

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett <> fcat (map (parens . pretty) args)

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett TypePatternToken t -> pretty t

ac5ec613b786cd05f495b568ab5214c31a333e67Andy Gimblett MixfixTypePattern ts -> fsep (map (pretty) ts)

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett BracketTypePattern k l _ -> bracket k $ ppWithCommas l

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett TypePatternArg t _ -> parens $ pretty t

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett-- | put proper brackets around a document

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettbracket :: BracketKind -> Doc -> Doc

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederbracket b = case b of

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett Parens -> parens

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett Squares -> brackets

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett Braces -> specBraces

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett NoBrackets -> id

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett-- | print a 'Kind' plus a preceding colon (or nothing)

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy GimblettprintKind :: Kind -> Doc

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy GimblettprintKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett-- | print the kind of a variable with its variance and a preceding colon

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettprintVarKind :: Variance -> VarKind -> Doc

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy GimblettprintVarKind e vk = case vk of

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett Downset t ->

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett space <> less <+> pretty t

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett VarKind k -> space <> colon <+>

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett pretty e <> pretty k

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett MissingKind -> empty

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettdata TypePrec = Outfix | Prefix | ProdInfix | FunInfix deriving (Eq, Ord)

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett

2f06b54890375b6cac90394b80b07bd451d728fcAndy GimblettparenPrec :: TypePrec -> (TypePrec, Doc) -> Doc

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy GimblettparenPrec p1 (p2, d) = if p2 < p1 then d else parens d

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimbletttoMixType :: Type -> (TypePrec, Doc)

toMixType typ = case typ of

ExpandedType t1 _ -> toMixType t1

{- (Prefix, ExpandedType

(parenPrec Prefix $ toMixType t1)

$ parenPrec Prefix $ toMixType t2) -}

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

(snd . toMixType) l)

KindedType t kind _ -> (Prefix,

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

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

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

case topTy of

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

case tyArgs of

[] -> (Outfix, pretty name)

[arg] -> let dArg = toMixType arg in

case ts of

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

&& not (isPlace e3) && null cs ->

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

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

[arg1, arg2] -> let dArg1 = toMixType arg1

dArg2 = toMixType arg2 in

case ts of

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

&& isPlace e3 && null cs ->

if tokStr e2 == prodS then

(ProdInfix, fsep [

parenPrec ProdInfix dArg1, cross,

parenPrec ProdInfix dArg2])

else -- assume fun type

(FunInfix, fsep [

parenPrec FunInfix dArg1, pretty e2, snd dArg2])

_ -> (Prefix, fsep [topDoc, parenPrec Prefix dArg1,

parenPrec Prefix dArg2])

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

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

map (parenPrec ProdInfix . toMixType) tyArgs)

else (Prefix, fsep $ topDoc :

map (parenPrec Prefix . toMixType) tyArgs)

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

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

: map (parenPrec Prefix . toMixType) tyArgs)

printType :: Type -> Doc

printType ty = case ty of

TypeName name _ _ -> pretty name

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

parens (printType t2)]

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

TypeToken t -> pretty t

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

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

MixfixType ts -> fsep $ map printType ts

instance Pretty Type where

pretty = snd . toMixType

-- no curried notation for bound variables

instance Pretty TypeScheme where

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

if null vs then tdoc else

fsep [forallDoc, semiDs vs, bullet, tdoc]

instance Pretty Partiality where

pretty p = case p of

Partial -> quMarkD

Total -> empty

instance Pretty Quantifier where

pretty q = case q of

Universal -> forallDoc

Existential -> exists

Unique -> unique

instance Pretty TypeQual where

pretty q = case q of

OfType -> colon

AsType -> text asS

InType -> inDoc

Inferred -> colon

instance Pretty Term where

pretty = changeGlobalAnnos addBuiltins . printTerm . rmSomeTypes

isSimpleTerm :: Term -> Bool

isSimpleTerm trm = case trm of

QualVar _ -> True

QualOp _ _ _ _ -> True

ResolvedMixTerm _ _ _ -> True

ApplTerm _ _ _ -> True

TupleTerm _ _ -> True

TermToken _ -> True

BracketTerm _ _ _ -> True

_ -> False

parenTermDoc :: Term -> Doc -> Doc

parenTermDoc trm = if isSimpleTerm trm then id else parens

printTermRec :: FoldRec Doc (Doc, Doc)

printTermRec = FoldRec

{ foldQualVar = \ _ vd -> parens $ keyword varS <+> pretty vd

, foldQualOp = \ _ br n t _ ->

parens $ fsep [pretty br, pretty n, colon, pretty $

if isPred br then unPredTypeScheme t else t]

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

if placeCount n == length ts || null ts then

idApplDoc n $ zipWith parenTermDoc os ts

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

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

case (o1, o2) of

(ResolvedMixTerm n [] _, TupleTerm ts _)

| placeCount n == length ts ->

idApplDoc n $ zipWith parenTermDoc ts $ map printTerm ts

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

idApplDoc n [parenTermDoc o2 t2]

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

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

, foldTypedTerm = \ _ t q typ _ -> fsep [t, pretty q, pretty typ]

, foldQuantifiedTerm = \ _ q vs t _ ->

fsep [pretty q, semiDs 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,

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

map (printEq0 funArrow) es]

, foldLetTerm = \ _ br es t _ ->

let des = vcat $ 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

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

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

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

printEq0 :: 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

<+> sep (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 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