{- |

Module : $Header$

Copyright : (c) Christian Maeder and Uni Bremen 2003

Licence : All rights reserved.

Maintainer : hets@tzi.de

Stability : experimental

Portability : portable

printing data types of the abstract syntax

-}

module HasCASL.PrintAs where

import HasCASL.As

import Common.Keywords

import HasCASL.HToken

import Common.Lib.Pretty

import Common.PPUtils

import qualified Common.Lib.Set as Set

import Common.PrettyPrint

import Common.GlobalAnnotations(GlobalAnnos)

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

noPrint :: Bool -> Doc -> Doc

noPrint b d = if b then empty else d

instance PrettyPrint TypePattern where

printText0 ga (TypePattern name args _) = printText0 ga name

<> fcat (map (parens . printText0 ga) args)

printText0 ga (TypePatternToken t) = printText0 ga t

printText0 ga (MixfixTypePattern ts) = fsep (map (printText0 ga) ts)

printText0 ga (BracketTypePattern k l _) = bracket k $ commaT_text ga l

printText0 ga (TypePatternArg t _) = parens $ printText0 ga t

-- | put proper brackets around a document

bracket :: BracketKind -> Doc -> Doc

bracket b t = let (o,c) = getBrackets b in ptext o <> t <> ptext c

-- | print a 'Kind' plus a preceding colon (or nothing for 'star')

printKind :: GlobalAnnos -> Kind -> Doc

printKind ga kind = case kind of

ExtClass (Intersection s _) InVar _ ->

if Set.isEmpty s then empty else erg

_ -> erg

where erg = space <> colon <+> printText0 ga kind

instance PrettyPrint Type where

printText0 ga (TypeName name _k _i) = printText0 ga name

-- <> printKind ga k

-- <> if i == 0 then empty

-- else parens (int i)

printText0 ga (TypeAppl t1 t2) = parens (printText0 ga t1)

<> parens (printText0 ga t2)

printText0 ga (TypeToken t) = printText0 ga t

printText0 ga (BracketType k l _) = bracket k $ commaT_text ga l

printText0 ga (KindedType t kind _) = (case t of

FunType _ _ _ _ -> parens

ProductType _ _ -> parens

LazyType _ _ -> parens

TypeAppl _ _ -> parens

_ -> id) (printText0 ga t)

<+> colon <+> printText0 ga kind

printText0 ga (MixfixType ts) = fsep (map (printText0 ga) ts)

printText0 ga (LazyType t _) = text quMark <+> (case t of

FunType _ _ _ _ -> parens

ProductType _ _ -> parens

KindedType _ _ _ -> parens

_ -> id) (printText0 ga t)

printText0 ga (ProductType ts _) = if null ts then parens empty

else fsep (punctuate (space <> text timesS)

(map ( \ t ->

(case t of

FunType _ _ _ _ -> parens

ProductType _ _ -> parens

_ -> id) $ printText0 ga t) ts))

printText0 ga (FunType t1 arr t2 _) = (case t1 of

FunType _ _ _ _ -> parens

_ -> id) (printText0 ga t1)

<+> printText0 ga arr

<+> printText0 ga t2

instance PrettyPrint Pred where

printText0 ga (IsIn c ts) = if null ts then printText0 ga c

else if null $ tail ts then

printText0 ga (head ts) <+>

colon <+> printText0 ga c

else printText0 ga c <+>

fsep (punctuate space

(map (printText0 ga) ts))

instance PrettyPrint t => PrettyPrint (Qual t) where

printText0 ga (ps :=> t) = (if null ps then empty

else parens $ commaT_text ga ps <+>

ptext implS <+> space) <>

printText0 ga t

-- no curried notation for bound variables

instance PrettyPrint TypeScheme where

printText0 ga (TypeScheme vs t _) = noPrint (null vs) (text forallS

<+> semiT_text ga vs

<+> text dotS <+> space)

<> printText0 ga t

instance PrettyPrint Partiality where

printText0 _ Partial = text quMark

printText0 _ Total = text exMark

instance PrettyPrint Arrow where

printText0 _ FunArr = text funS

printText0 _ PFunArr = text pFun

printText0 _ ContFunArr = text contFun

printText0 _ PContFunArr = text pContFun

instance PrettyPrint Quantifier where

printText0 _ Universal = text forallS

printText0 _ Existential = text existsS

printText0 _ Unique = text $ existsS ++ exMark

instance PrettyPrint TypeQual where

printText0 _ OfType = colon

printText0 _ AsType = text asS

printText0 _ InType = text inS

instance PrettyPrint Term where

printText0 ga (QualVar v t _) = parens $ text varS

<+> printText0 ga v

<+> colon

<+> printText0 ga t

printText0 ga (QualOp n t _) = parens $

text opS

<+> printText0 ga n

<+> colon

<+> printText0 ga t

printText0 ga (ResolvedMixTerm n ts _) = (parens $ printText0 ga n)

<+> noPrint (null ts) (parens $ commaT_text ga ts)

printText0 ga (ApplTerm t1 t2 _) = printText0 ga t1

<+> (case t2 of

QualVar _ _ _ -> id

QualOp _ _ _ -> id

TupleTerm _ _ -> id

BracketTerm Parens _ _ -> id

TermToken _ -> id

_ -> parens) (printText0 ga t2)

printText0 ga (TupleTerm ts _) = parens $ commaT_text ga ts

printText0 ga (TypedTerm term q typ _) = printText0 ga term

<+> printText0 ga q

<+> printText0 ga typ

printText0 ga (QuantifiedTerm q vs t _) = printText0 ga q

<+> semiT_text ga vs

<+> text dotS

<+> printText0 ga t

printText0 ga (LambdaTerm ps q t _) = text lamS

<+> (case ps of

[p] -> printText0 ga p

_ -> fcat $ map

(parens.printText0 ga) ps)

<+> (case q of

Partial -> text dotS

Total -> text $ dotS ++ exMark)

<+> printText0 ga t

printText0 ga (CaseTerm t es _ ) = text caseS

<+> printText0 ga t

<+> text ofS

<+> vcat (punctuate (text " | ")

(map (printEq0 ga funS) es))

printText0 ga (LetTerm es t _) = text letS

<+> vcat (punctuate semi

(map (printEq0 ga equalS) es))

<+> text inS

<+> printText0 ga t

printText0 ga (TermToken t) = printText0 ga t

printText0 ga (MixfixTerm ts) = fsep $ map (printText0 ga) ts

printText0 ga (BracketTerm k l _) = bracket k $ commaT_text ga l

instance PrettyPrint Pattern where

printText0 ga (PatternVar v) = printText0 ga v

printText0 ga (ResolvedMixPattern n args _) = parens (printText0 ga n)

<+> noPrint (null args)

(parens $ commaT_text ga args)

printText0 ga (PatternConstr n t args _) = printText0 ga n

<+> colon

<+> printText0 ga t

<+> fcat (map (parens.printText0 ga) args)

printText0 ga (PatternToken t) = printText0 ga t

printText0 ga (BracketPattern k l _) = bracket k $ commaT_text ga l

printText0 ga (TuplePattern ps _) = parens $ commaT_text ga ps

printText0 ga (MixfixPattern ps) = fsep (map (printText0 ga) ps)

printText0 ga (TypedPattern p t _) = printText0 ga p

<+> colon

<+> printText0 ga t

printText0 ga (AsPattern v p _) = printText0 ga v

<+> text asP

<+> printText0 ga p

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

printEq0 :: GlobalAnnos -> String -> ProgEq -> Doc

printEq0 ga s (ProgEq p t _) = fsep [printText0 ga p

, text s

, printText0 ga t]

instance PrettyPrint VarDecl where

printText0 ga (VarDecl v t _ _) = printText0 ga v <+> colon

<+> printText0 ga t

instance PrettyPrint GenVarDecl where

printText0 ga (GenVarDecl v) = printText0 ga v

printText0 ga (GenTypeVarDecl tv) = printText0 ga tv

instance PrettyPrint TypeArg where

printText0 ga (TypeArg v c _ _) = printText0 ga v <+> colon

<+> printText0 ga c

instance PrettyPrint Variance where

printText0 _ CoVar = text plusS

printText0 _ ContraVar = text minusS

printText0 _ InVar = empty

instance PrettyPrint Kind where

printText0 ga (ExtClass k v _) = printText0 ga k

<> printText0 ga v

printText0 ga (KindAppl k1 k2 _) =

(case k1 of

KindAppl _ _ _ -> parens

_ -> id) (printText0 ga k1)

<+> text funS

<+> printText0 ga k2

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

printList0 :: (PrettyPrint a) => GlobalAnnos -> [a] -> Doc

printList0 ga l = case l of

[] -> empty

[x] -> printText0 ga x

_ -> parens $ commaT_text ga l

instance PrettyPrint Class where

printText0 ga (Downset t) = braces $

text "_" <+> text lessS <+> printText0 ga t

printText0 ga (Intersection c _) = if Set.isEmpty c then ptext "Type"

else printList0 ga $ Set.toList c

instance PrettyPrint InstOpId where

printText0 ga (InstOpId n l _) = printText0 ga n

<> noPrint (null l)

(brackets $ semiT_text ga l)

------------------------------------------------------------------------

-- item stuff

------------------------------------------------------------------------

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

printPseudoType :: GlobalAnnos -> TypeScheme -> Doc

printPseudoType ga (TypeScheme l t _) = noPrint (null l) (text lamS

<+> (if null $ tail l then

printText0 ga $ head l

else fcat(map (parens . printText0 ga) l))

<+> text dotS <> space) <> printText0 ga t

instance PrettyPrint BasicSpec where

printText0 ga (BasicSpec l) = vcat (map (printText0 ga) l)

instance PrettyPrint ProgEq where

printText0 ga = printEq0 ga equalS

instance PrettyPrint BasicItem where

printText0 ga (SigItems s) = printText0 ga s

printText0 ga (ProgItems l _) = text programS <+> semiT_text ga l

printText0 ga (ClassItems i l _) = text classS <+> printText0 ga i

<+> semiT_text ga l

printText0 ga (GenVarItems l _) = text varS <+> semiT_text ga l

printText0 ga (FreeDatatype l _) = text freeS <+> text typeS

<+> semiT_text ga l

printText0 ga (GenItems l _) = text generatedS <+> braces (semiT_text ga l)

printText0 ga (AxiomItems vs fs _) = (if null vs then empty

else text forallS <+> semiT_text ga vs)

$$ vcat (map

(\x -> text dotS <+> printText0 ga x)

fs)

instance PrettyPrint SigItems where

printText0 ga (TypeItems i l _) = text typeS <+> printText0 ga i

<+> semiT_text ga l

printText0 ga (OpItems l _) = text opS <+> semiT_text ga l

instance PrettyPrint Instance where

printText0 _ Instance = text instanceS

printText0 _ _ = empty

instance PrettyPrint ClassItem where

printText0 ga (ClassItem d l _) = printText0 ga d $$

if null l then empty

else braces (semiT_text ga l)

instance PrettyPrint ClassDecl where

printText0 ga (ClassDecl l k _) = commaT_text ga l <> printKind ga k

printText0 ga (SubclassDecl l k s _) = commaT_text ga l

<> printKind ga k

<+> text lessS

<+> printText0 ga s

printText0 ga (ClassDefn n k c _) = printText0 ga n

<> printKind ga k

<+> text equalS

<+> printText0 ga c

printText0 ga (DownsetDefn c v t _) =

let pv = printText0 ga v in

printText0 ga c

<> text equalS

<> braces (pv <> text dotS <> pv

<> text lessS

<+> printText0 ga t)

instance PrettyPrint Vars where

printText0 ga (Var v) = printText0 ga v

printText0 ga (VarTuple vs _) = parens $ commaT_text ga vs

instance PrettyPrint TypeItem where

printText0 ga (TypeDecl l k _) = commaT_text ga l <>

printKind ga k

printText0 ga (SubtypeDecl l t _) = commaT_text ga l <+> text lessS

<+> printText0 ga t

printText0 ga (IsoDecl l _) = cat(punctuate (text " = ")

(map (printText0 ga) l))

printText0 ga (SubtypeDefn p v t f _) = printText0 ga p

<+> text equalS

<+> braces (printText0 ga v

<+> colon

<+> printText0 ga t

<+> text dotS

<+> printText0 ga f)

printText0 ga (AliasType p k t _) = (printText0 ga p <>

case k of

Nothing -> empty

Just j -> space <> colon <+>

printText0 ga j)

<+> text assignS

<+> printPseudoType ga t

printText0 ga (Datatype t) = printText0 ga t

instance PrettyPrint OpItem where

printText0 ga (OpDecl l t as _) = commaT_text ga l <+> colon

<+> (printText0 ga t

<> (if null as then empty else comma)

<> commaT_text ga as)

printText0 ga (OpDefn n ps s p t _) = (printText0 ga n

<> fcat (map (printText0 ga) ps))

<+> (colon <> if p == Partial

then text quMark else empty)

<+> printText0 ga s

<+> text equalS

<+> printText0 ga t

instance PrettyPrint BinOpAttr where

printText0 _ Assoc = text assocS

printText0 _ Comm = text commS

printText0 _ Idem = text idemS

instance PrettyPrint OpAttr where

printText0 ga (BinOpAttr a _) = printText0 ga a

printText0 ga (UnitOpAttr t _) = text unitS <+> printText0 ga t

instance PrettyPrint DatatypeDecl where

printText0 ga (DatatypeDecl p k as d _) = (printText0 ga p <>

printKind ga k)

<+> text defnS

<+> vcat(punctuate (text " | ")

(map (printText0 ga) as))

<+> case d of Nothing -> empty

Just c -> text derivingS

<+> printText0 ga c

instance PrettyPrint Alternative where

printText0 ga (Constructor n cs p _) = printText0 ga n

<+> fsep (map (printText0 ga) cs)

<+> (case p of {Partial -> text quMark;

_ -> empty})

printText0 ga (Subtype l _) = text typeS <+> commaT_text ga l

instance PrettyPrint Components where

printText0 ga (Selector n p t _ _) = printText0 ga n

<> colon <> (case p of { Partial ->text quMark;

_ -> empty }

<+> printText0 ga t)

printText0 ga (NoSelector t) = printText0 ga t

printText0 ga (NestedComponents l _) = parens $ semiT_text ga l

instance PrettyPrint OpId where

printText0 ga (OpId n ts _) = printText0 ga n

<+> noPrint (null ts)

(brackets $ commaT_text ga ts)