a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett{- HetCATS/HasCASL/PrintAs.hs

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski $Id$

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Authors: Christian Maeder

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Year: 2002

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski printing As data types

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule HasCASL.PrintAs where

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblettimport HasCASL.As

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Keywords

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport HasCASL.HToken

fbb2d28086a1860850f661fbf4af531322bac405Christian Maederimport Common.Lib.Pretty

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.PPUtils

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Common.Lib.Set as Set

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.PrettyPrint

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.GlobalAnnotations(GlobalAnnos)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Print_AS_Annotation

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

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

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettcommas = commaT printText0

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettsemis = semiT printText0

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettinstance PrettyPrint TypePattern where

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

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

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett printText0 ga (TypePatternToken t) = printText0 ga t

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

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

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

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettbracket :: BracketKind -> Doc -> Doc

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettbracket Parens t = parens t

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettbracket Squares t = brackets t

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettbracket Braces t = braces t

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettprintKind :: GlobalAnnos -> Kind -> Doc

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachprintKind ga kind = case kind of

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett ExtClass (Intersection s _) InVar _ ->

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett if Set.isEmpty s then empty else erg

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett _ -> erg

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblett where erg = space <> colon <> printText0 ga kind

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblettinstance PrettyPrint Type where

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

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- <> printKind ga k

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- <> if i == 0 then empty

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- else parens (int i)

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

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett <> parens (printText0 ga t2)

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

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett printText0 ga (BracketType k l _) = bracket k $ commas ga l

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett printText0 ga (KindedType t kind _) = printText0 ga t

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett <> space <> colon <> printText0 ga kind

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

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett printText0 ga (LazyType t _) = text quMark <+> printText0 ga (t)

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett printText0 ga (ProductType ts _) = fsep (punctuate (space <> text timesS)

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett (map (printText0 ga) ts))

e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski printText0 ga (FunType t1 arr t2 _) = printText0 ga t1

e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski <+> printText0 ga arr

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett <+> printText0 ga t2

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance PrettyPrint Pred where

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

eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder else if null $ tail ts then

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski printText0 ga (head ts) <+>

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett colon <+> printText0 ga c

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett else printText0 ga c <+>

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski fsep (punctuate space

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski (map (printText0 ga) ts))

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance PrettyPrint t => PrettyPrint (Qual t) where

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

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett else parens $ commas ga ps <+>

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ptext implS <+> space) <>

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett printText0 ga t

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- no curried notation for bound variables

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskiinstance PrettyPrint TypeScheme where

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

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski <+> semis ga vs

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <+> text dotS <+> space)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <> printText0 ga t

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance PrettyPrint Partiality where

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett printText0 _ Partial = text quMark

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski printText0 _ Total = text exMark

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinstance PrettyPrint Arrow where

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett printText0 _ FunArr = text funS

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett printText0 _ PFunArr = text pFun

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett 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 (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

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

printList0 ga l = noPrint (null l)

(if null $ tail l then printText0 ga $ head l

else parens $ commas 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 $ semis 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 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 k _) = commas ga l <> printKind ga k

printText0 ga (SubclassDecl l k s _) = commas 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 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

<+> noPrint (null ts)

(brackets $ commas ga ts)