020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder{- HetCATS/HasCASL/PrintAs.hs

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski $Id$

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett Authors: Christian Maeder

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Year: 2002

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett printing As data types

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett-}

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettmodule HasCASL.PrintAs where

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport HasCASL.As

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.Keywords

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport HasCASL.HToken

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.Lib.Pretty

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.PrettyPrint

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.GlobalAnnotations(GlobalAnnos)

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblettimport Common.GlobalAnnotationsFunctions(emptyGlobalAnnos)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Common.Print_AS_Annotation

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett

9f93b2a8b552789cd939d599504d39732672dc84Christian MaedernoPrint :: Bool -> Doc -> Doc

9f93b2a8b552789cd939d599504d39732672dc84Christian MaedernoPrint b d = if b then empty else d

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett

04ceed96d1528b939f2e592d0656290d81d1c045Andy GimblettshowPretty :: PrettyPrint a => a -> ShowS

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettshowPretty = showString . render . printText0 emptyGlobalAnnos

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett where _just_avoid_unused_import_warning = smallSpace_latex

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettcommas, semis :: PrettyPrint a => GlobalAnnos -> [a] -> Doc

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettcommas ga l = fcat $ punctuate comma (map (printText0 ga) l)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettsemis ga l = sep $ punctuate semi (map (printText0 ga) l)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettinstance PrettyPrint TypePattern where

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett printText0 ga (TypePattern name args _) = printText0 ga name

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett <> fcat (map (parens . printText0 ga) args)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett printText0 ga (TypePatternToken t) = printText0 ga t

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett printText0 ga (MixfixTypePattern ts) = fsep (map (printText0 ga) ts)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett printText0 ga (BracketTypePattern k l _) = bracket k $ commas ga l

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblett printText0 ga (TypePatternArgs l) = semis ga l

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettbracket :: BracketKind -> Doc -> Doc

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettbracket Parens t = parens t

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettbracket Squares t = brackets t

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettbracket Braces t = braces t

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettprintKind :: GlobalAnnos -> Kind -> Doc

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettprintKind ga kind = case kind of

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett PlainClass (Intersection [] _) -> empty

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett _ -> space <> colon <> printText0 ga kind

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblettinstance PrettyPrint Type where

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett printText0 ga (TypeName name i) = printText0 ga name

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett <> if i == 0 then empty

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett else parens (int i)

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

ac5ec613b786cd05f495b568ab5214c31a333e67Andy Gimblett <> parens (printText0 ga t2)

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett printText0 ga (TypeToken t) = printText0 ga t

fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder printText0 ga (BracketType k l _) = bracket k $ commas ga l

fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder printText0 ga (KindedType t kind _) = printText0 ga t

fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder <> space <> colon <> printText0 ga kind

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

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian Maeder printText0 ga (LazyType t _) = text quMark <+> printText0 ga (t)

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian Maeder printText0 ga (ProductType ts _) = fsep (punctuate (space <> text timesS)

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder (map (printText0 ga) ts))

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder printText0 ga (FunType t1 arr t2 _) = printText0 ga t1

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder <+> printText0 ga arr

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder <+> printText0 ga t2

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian Maeder

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian Maeder

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maederinstance PrettyPrint Pred where

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder printText0 ga (IsIn c ts) = if null ts then printText0 ga c

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder else if null $ tail ts then

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder printText0 ga (head ts) <+>

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder colon <+> printText0 ga c

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder else printText0 ga c <+>

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder fsep (punctuate space

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder (map (printText0 ga) ts))

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maederinstance PrettyPrint t => PrettyPrint (Qual t) where

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

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder else parens $ commas ga ps <+>

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder ptext implS <+> space) <>

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder printText0 ga t

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder-- no curried notation for bound variables

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maederinstance PrettyPrint TypeScheme where

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder printText0 ga (TypeScheme vss t _) = hcat (map (\ (TypeArgs vs _) ->

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder text forallS

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder <+> semis ga vs

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder <+> text dotS <+> space)

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder vss)

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder <> printText0 ga t

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maederinstance PrettyPrint Partiality where

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder 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 LogOp where

printText0 _ NotOp = text notS

printText0 _ AndOp = text lAnd

printText0 _ OrOp = text lOr

printText0 _ ImplOp = text implS

printText0 _ EquivOp = text equivS

instance PrettyPrint EqOp where

printText0 _ EqualOp = text equalS

printText0 _ ExEqualOp = text exEqual

instance PrettyPrint Formula where

printText0 ga (TermFormula t) = printText0 ga t

printText0 ga (ConnectFormula o fs _) = parens $

fsep (punctuate (space <> printText0 ga o) (map (printText0 ga) fs))

printText0 ga (EqFormula o t1 t2 _) = printText0 ga t1

<+> printText0 ga o

<+> printText0 ga t2

printText0 ga (DefFormula t _) = text defS <+> printText0 ga t

printText0 ga (QuantifiedFormula q vs f _) =

printText0 ga q <+> semis ga vs <+> text dotS <+> printText0 ga f

printText0 ga (PolyFormula ts f _) =

text forallS <+> semis ga ts <+> text dotS <+> printText0 ga f

instance PrettyPrint Term where

printText0 ga (CondTerm t1 f t2 _) = printText0 ga t1

<+> text whenS

<+> printText0 ga f

<+> text elseS

<+> printText0 ga t2

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 (ApplTerm t1 t2 _) = printText0 ga t1

<+> parens (printText0 ga t2)

printText0 ga (TupleTerm ts _) = parens $ commas 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

<+> semis ga vs

<+> text dotS

<+> printText0 ga t

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

<+> (if length ps == 1 then

printText0 ga $ head ps

else 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 $ commas ga l

instance PrettyPrint Pattern where

printText0 ga (PatternVars vs _) = semis ga vs

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

case l of

[TuplePattern _ _] -> printText0 ga $ head l

_ -> bracket k $ commas ga l

printText0 ga (TuplePattern ps _) = parens $ commas 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

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 (PlainClass c) = printText0 ga c

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

PlainClass _ -> id

_ -> parens) (printText0 ga k)

<> printText0 ga v

printText0 ga (ProdClass l _) = fcat $ punctuate (space <> text timesS)

(map (\ k ->

(case k of KindAppl _ _ _ -> parens

ProdClass _ _ -> parens

_ -> id)

(printText0 ga k)) l)

printText0 ga (KindAppl k1 k2 _) =

(case k1 of

KindAppl _ _ _ -> parens

_ -> id) (printText0 ga k1)

<+> text funS

<> printText0 ga k2

instance PrettyPrint Class where

printText0 ga (Downset t) = braces $

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

printText0 ga (Intersection c _) = if null c then ptext "Type"

else if null $ tail c then printText0 ga $ head c

else parens $ commas ga c

instance PrettyPrint Types where

printText0 ga (Types l _) = brackets $ commas ga l

instance PrettyPrint InstOpId where

printText0 ga (InstOpId n l) = printText0 ga n

<> fcat(map (printText0 ga) l)

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

-- item stuff

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

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 TypeArgs where

printText0 ga (TypeArgs l _) = semis ga l

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 <+> semis ga l

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

<+> semis ga l

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

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

<+> semis ga l

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

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

else text forallS <+> semis 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

<+> semis ga l

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

printText0 ga (PredItems l _) = text predS <+> semis 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 (semis ga l)

instance PrettyPrint ClassDecl where

printText0 ga (ClassDecl l _) = commas ga l

printText0 ga (SubclassDecl l s _) = commas ga l <> text lessS

<> printText0 ga s

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

<> 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 TypeItem where

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

printKind ga k

printText0 ga (SubtypeDecl l t _) = commas 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 <>

printText ga j)

<+> text assignS

<+> printPseudoType ga t

printText0 ga (Datatype t) = printText0 ga t

instance PrettyPrint OpItem where

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

<+> (printText0 ga t

<> (if null as then empty else comma)

<> commas 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 PredItem where

printText0 ga (PredDecl l t _) = commas ga l <+> colon <+> printText0 ga t

printText0 ga (PredDefn n ps f _) = (printText0 ga n

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

<+> text equivS

<+> printText0 ga f

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

<> fcat (map (printText0 ga) cs)

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

_ -> empty})

printText0 ga (Subtype l _) = text typeS <+> commas 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 $ semis ga l

instance PrettyPrint OpId where

printText0 ga (OpId n ts) = printText0 ga n

<+> fcat(map (brackets .

printText0 ga) ts)