PrintAs.hs revision e05956d1da3c97e4d808926f97c6841c4a561991
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke{- HetCATS/HasCASL/PrintAs.hs
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder $Id$
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Authors: Christian Maeder
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu Year: 2002
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printing As data types
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-}
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkemodule PrintAs where
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport As
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Keywords
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport HToken
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Pretty
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport PrettyPrint
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkecommas l = hcat $ punctuate comma (map printText0 l)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkesemis l = hcat $ punctuate semi (map printText0 l)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance PrettyPrint TypePattern where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(TypePattern name args _) = printText0(name)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <> hcat (map (parens.printText0) args)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(TypePatternToken t) = printText0(t)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(MixfixTypePattern ts) = hsep (map printText0 ts)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(BracketTypePattern k l _) = bracket k $ commas l
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(TypePatternArgs l) = semis l
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederbracket Parens t = parens t
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederbracket Squares t = Pretty.brackets t
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederbracket Braces t = braces t
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederinstance PrettyPrint Type where
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(TypeConstrAppl name kind args _) = printText0 name
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> colon
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> printText0 kind
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> parens (commas args)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(TypeToken t) = printText0(t)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(BracketType k l _) = bracket k $ commas l
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(KindedType t kind _) = printText0(t)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> colon
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> printText0(kind)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(MixfixType ts) = hsep (map printText0 ts)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(TupleType args _) = parens $ commas args
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(LazyType t _) = text quMark <+> printText0(t)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(ProductType ts _) = hsep (punctuate (text " *")
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (map printText0 ts))
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(FunType t1 arr t2 _) = printText0 t1
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> printText0 arr
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> printText0 t2
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- no curried notation for bound variables
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance PrettyPrint TypeScheme where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(SimpleTypeScheme t) = printText0 t
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(TypeScheme vs t _) = text forallS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> semis vs
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> text dotS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> printText0 t
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance PrettyPrint PartialKind where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 Partial = text quMark
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 Total = text exMark
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederinstance PrettyPrint Arrow where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 FunArr = text funS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 PFunArr = text pFun
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 ContFunArr = text contFun
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0 PContFunArr = text pContFun
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance PrettyPrint Quantifier where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 Universal = text forallS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 Existential = text existsS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 Unique = text $ existsS ++ exMark
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance PrettyPrint TypeQual where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 OfType = colon
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0 AsType = text asS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 InType = text inS
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederinstance PrettyPrint Formula where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 (TermFormula t) = printText0 t
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- other cases missing
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maederinstance PrettyPrint Term where
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(CondTerm t1 f t2 _) = printText0 t1
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> text whenS
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> printText0 f
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> text elseS
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> printText0 t2
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(QualVar v t _) = parens $ text varS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> printText0 v
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> colon
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> printText0 t
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(QualOp n t _) = parens $
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke text opS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> printText0 n
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> colon
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> printText0 t
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(ApplTerm t1 t2 _) = printText0 t1
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> parens (printText0 t2)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(TupleTerm ts _) = parens $ commas ts
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder printText0(TypedTerm term q typ _) = printText0 term
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> printText0 q
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> printText0 typ
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(QuantifiedTerm q vs t _) = printText0 q
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> semis vs
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> text dotS
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder <+> printText0 t
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0(LambdaTerm ps q t _) = text lamS
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <+> (if length ps == 1 then
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke printText0 $ head ps
else hcat $ map
(parens.printText0) ps)
<+> (case q of
Partial -> text dotS
Total -> text $ dotS ++ exMark)
<+> printText0 t
printText0(CaseTerm t es _ ) = text caseS
<+> printText0 t
<+> text ofS
<+> vcat (punctuate (text " | ")
(map (printEq0 funS) es))
printText0(LetTerm es t _) = text letS
<+> vcat (punctuate semi
(map (printEq0 equalS) es))
<+> text inS
<+> printText0 t
printText0(TermToken t) = printText0 t
printText0(MixfixTerm ts) = hsep (map printText0 ts)
printText0(BracketTerm k l _) = bracket k $ commas l
instance PrettyPrint Pattern where
printText0(PatternVars vs _) = semis vs
printText0(PatternConstr n t args _) = printText0 n
<+> colon
<+> printText0 t
<+> hcat (map (parens.printText0) args)
printText0(PatternToken t) = printText0 t
printText0(BracketPattern k l _) = bracket k $ commas l
printText0(TuplePattern ps _) = parens $ commas ps
printText0(MixfixPattern ps) = hsep (map printText0 ps)
printText0(TypedPattern p t _) = printText0 p
<+> colon
<+> printText0 t
printText0(AsPattern v p _) = printText0 v
<+> text asP
<+> printText0 p
printEq0 s (ProgEq p t _) = printText0 p
<+> text s
<+> printText0 t
instance PrettyPrint VarDecl where
printText0(VarDecl v t k _) = case k of Comma -> printText0 v <> comma
_ -> printText0 v <+> colon
<+> printText0 t
instance PrettyPrint TypeVarDecl where
printText0(TypeVarDecl v c k _) = case k of
Comma -> printText0 v <> comma
_ -> printText0 v <+>
case c of
Downset t ->
text lessS <+> printText0 t
_ -> colon <+> printText0 c
instance PrettyPrint GenVarDecl where
printText0(GenVarDecl v) = printText0 v
printText0(GenTypeVarDecl tv) = printText0 tv
instance PrettyPrint TypeArg where
printText0(TypeArg v e k _) = case k of Comma -> printText0 v <> comma
_ -> printText0 v <+> colon
<+> printText0 e
instance PrettyPrint Variance where
printText0 CoVar = text plusS
printText0 ContraVar = text minusS
printText0 InVar = empty
instance PrettyPrint ExtClass where
printText0(ExtClass c v _) = printText0 c <> printText0 v
instance PrettyPrint ProdClass where
printText0(ProdClass l _) = hcat $ punctuate (text timesS)
(map printText0 l)
instance PrettyPrint Kind where
printText0(Kind l c _) = (hcat $ punctuate (text funS)
(map printText0 l))
<> text funS
<> printText0 c
instance PrettyPrint Class where
printText0(Universe _) = text typeS
printText0(ClassName n) = printText0 n
printText0(Downset t) = braces $ text lessS <+> printText0 t
printText0(Intersection c _) = parens $ commas c
instance PrettyPrint Types where
printText0(Types l _) = Pretty.brackets $ commas l
instance PrettyPrint InstOpName where
printText0 (InstOpName n l) = printText0 n <> hcat(map printText0 l)