7895bc4f90d3ea250877c02a897f5dcca4590a89Christian MaederDescription : pretty printing data types of BASIC_SPEC
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederStability : experimental
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiPretty printing data types of 'BASIC_SPEC'
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maeder ( printBASIC_SPEC
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maeder , printFormula
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian Maeder , printTheoryFormula
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder , pluralS_symb_list
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder , ListCheck (..)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu , recoverType
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu , printALTERNATIVE
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maeder , printVarDecl
3b5d1e9f95905d6595b3bb01b54499a37a3d82acChristian Maeder , printVarDeclL
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder , printVarDecls
434c11a96bc623ebd5b60781efabef319bb15b0eChristian Maeder , printOptArgDecls
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maeder , printSortItem
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maeder , printOpItem
7d6fdc539541f38639e20b45bba29e39bd201c3fChristian Maeder , printPredItem
0d72630889db51ffe7a0336cbb7fde5dbe415e9dEwaryst Schulz , printPredHead
7447e9fcbe38c1d04effa0df67f49240bd9963d6Liam O'Reilly , printRecord
3b5d1e9f95905d6595b3bb01b54499a37a3d82acChristian Maeder , printAnnotedBulletFormulas
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder , FormExtension (..)
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_SPEC b s f)
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder where pretty = printBASIC_SPEC pretty pretty
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintBASIC_SPEC :: FormExtension f => (b -> Doc) -> (s -> Doc)
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maeder -> BASIC_SPEC b s f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintBASIC_SPEC fB fS (Basic_spec l) = case l of
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang [] -> specBraces empty
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder _ -> vcat $ map (printAnnoted (printBASIC_ITEMS fB fS)) l
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance (Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_ITEMS b s f)
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder where pretty = printBASIC_ITEMS pretty pretty
c7f5076658d72ea340d7fd8a648908f961af682dChristian MaedertypeString :: SortsKind -> [Annoted DATATYPE_DECL] -> String
c7f5076658d72ea340d7fd8a648908f961af682dChristian MaedertypeString sk l = (case sk of
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder NonEmptySorts -> typeS
9ba43c9323dc1a4bb1e684d87370b43468ab9096Christian Maeder PossiblyEmptySorts -> etypeS) ++ appendS l
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintBASIC_ITEMS :: FormExtension f => (b -> Doc) -> (s -> Doc)
1aee531e3fe5a94300ddc7933c1983a38a76316eChristian Maeder -> BASIC_ITEMS b s f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintBASIC_ITEMS fB fS sis = case sis of
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder Sig_items s -> printSIG_ITEMS fS s
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder Free_datatype sk l _ -> sep [keyword freeS <+> keyword (typeString sk l),
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder semiAnnos printDATATYPE_DECL l]
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang Sort_gen l _ -> case l of
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder [Annoted (Datatype_items sk l' _) _ las ras] ->
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder (if null las then id else (printAnnotationList las $+$))
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder $ (if null ras then id else ($+$ printAnnotationList ras))
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder $ sep [keyword generatedS <+> keyword (typeString sk l'),
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder semiAnnos printDATATYPE_DECL l']
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder _ -> sep [keyword generatedS, specBraces $ vcat $ map
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder (printAnnoted $ printSIG_ITEMS fS) l]
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder Var_items l _ -> topSigKey (varS ++ pluralS l) <+> printVarDecls l
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder Local_var_axioms l f _ ->
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder fsep [fsep $ forallDoc : printVarDeclL l
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder , printAnnotedBulletFormulas f]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder Axiom_items f _ -> printAnnotedBulletFormulas f
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang Ext_BASIC_ITEMS b -> fB b
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintAnnotedBulletFormulas :: FormExtension f => [Annoted (FORMULA f)] -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintAnnotedBulletFormulas l = vcat $ case l of
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder _ -> let pp = addBullet . printFormula in
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder map (printAnnoted pp) (init l)
a571b691ac0da91a895c33f250509622004dcf03Christian Maeder ++ [printSemiAnno pp False $ last l] -- use True for HasCASL
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance (Pretty s, FormExtension f) => Pretty (SIG_ITEMS s f) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder pretty = printSIG_ITEMS pretty
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintSIG_ITEMS :: FormExtension f => (s -> Doc) -> SIG_ITEMS s f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintSIG_ITEMS fS sis = case sis of
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder Sort_items sk l _ -> topSigKey ((case sk of
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder NonEmptySorts -> sortS
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder PossiblyEmptySorts -> esortS) ++ pluralS l) <+>
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder semiAnnos printSortItem l
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder Op_items l _ -> topSigKey (opS ++ pluralS l) <+>
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder let pp = printOpItem in
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder if null l then empty else if case item $ last l of
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder Op_decl _ _ a@(_ : _) _ -> case last a of
a571b691ac0da91a895c33f250509622004dcf03Christian Maeder Unit_op_attr {} -> False -- use True for HasCASL
a571b691ac0da91a895c33f250509622004dcf03Christian Maeder Op_defn {} -> False -- use True for HasCASL
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder then vcat $ map (printSemiAnno pp True) l else semiAnnos pp l
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder Pred_items l _ -> topSigKey (predS ++ pluralS l) <+>
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder let pp = printPredItem in
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder if null l then empty else if case item $ last l of
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder Pred_defn {} -> True
842a6d146e8d1023c9cc54e9064ae93be2daf831Christian Maeder then vcat $ map (printSemiAnno pp True) l else semiAnnos pp l
c7f5076658d72ea340d7fd8a648908f961af682dChristian Maeder Datatype_items sk l _ -> topSigKey (typeString sk l) <+>
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang semiAnnos printDATATYPE_DECL l
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder Ext_SIG_ITEMS s -> fS s
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian MaederprintDATATYPE_DECL :: DATATYPE_DECL -> Doc
fef03b64e3b1d7d3a8e098f62ef2e7687a433f09Christian MaederprintDATATYPE_DECL (Datatype_decl s a r) =
9aef2f9a1f6d7557bc31bf4f9db235f7f0d5170dChristian Maeder let pa = printAnnoted printALTERNATIVE in case a of
fef03b64e3b1d7d3a8e098f62ef2e7687a433f09Christian Maeder [] -> printDATATYPE_DECL (Datatype_decl s [emptyAnno $ Subsorts [s] r] r)
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder h : t -> sep [idLabelDoc s, colon <> colon <> sep
ade1f65c2bb98fbf45f8ef16bed4fa50802225a4Christian Maeder ((equals <+> pa h) :
9aef2f9a1f6d7557bc31bf4f9db235f7f0d5170dChristian Maeder map ((bar <+>) . pa) t)]
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wanginstance Pretty DATATYPE_DECL where
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang pretty = printDATATYPE_DECL
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian MaederprintCOMPONENTS :: COMPONENTS -> Doc
57d9ffd4f0d821632c5dd116a5301c3305599b19Christian MaederprintCOMPONENTS c = case c of
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian Maeder Cons_select k l s _ -> fsep $ punctuate comma (map idLabelDoc l)
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang ++ [case k of
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang Total -> colon
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder Partial -> colon <> quMarkD, idDoc s]
57d9ffd4f0d821632c5dd116a5301c3305599b19Christian Maeder Sort s -> idDoc s
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maederinstance Pretty COMPONENTS where
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang pretty = printCOMPONENTS
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian MaederprintALTERNATIVE :: ALTERNATIVE -> Doc
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian MaederprintALTERNATIVE a = case a of
8519df804b37f95a2394a6cd5662da02efa3400bChristian Maeder Alt_construct k n l _ -> case l of
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian Maeder [] -> idLabelDoc n
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian Maeder _ -> idLabelDoc n <>
8519df804b37f95a2394a6cd5662da02efa3400bChristian Maeder parens ( sep $ punctuate semi $ map printCOMPONENTS l)
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang Total -> empty
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder Partial -> quMarkD
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder Subsorts l _ -> fsep $ text (sortS ++ pluralS l)
8519df804b37f95a2394a6cd5662da02efa3400bChristian Maeder : punctuate comma (map idDoc l)
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wanginstance Pretty ALTERNATIVE where
264b794970b6f2bd437f14233f367f1067565728Jian Chun Wang pretty = printALTERNATIVE
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintSortItem :: FormExtension f => SORT_ITEM f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintSortItem si = case si of
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian Maeder Sort_decl sl _ -> sepByCommas $ map idLabelDoc sl
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder Subsort_decl sl sup _ ->
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder fsep $ punctuate comma (map idDoc sl) ++ [less, idDoc sup]
66939c546b3eaf25eb34d1dc36c0c82943f85552Christian Maeder Subsort_defn s v sup af _ -> fsep [idLabelDoc s, equals,
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder specBraces $ fsep [sidDoc v, colon <+> idDoc sup,
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder printAnnoted (addBullet . printFormula) af]]
184449040f3b741bbb6a2e881415b30d624e2c63Christian Maeder Iso_decl sl _ -> fsep $ punctuate (space <> equals) $ map idDoc sl
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension f => Pretty (SORT_ITEM f) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder pretty = printSortItem
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintQuant :: QUANTIFIER -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintQuant q = case q of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Universal -> forallDoc
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Existential -> exists
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Unique_existential -> unique
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederprintSortedVars :: [VAR] -> SORT -> Doc
479da8506f391abe070ced2fb93c9759a280fa68Christian MaederprintSortedVars l s =
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder fsep $ punctuate comma (map sidDoc l) ++ [colon <+> idDoc s]
941254a2daaf605bda18be25358f4e1322e94ec9Christian MaederprintVarDeclL :: [VAR_DECL] -> [Doc]
941254a2daaf605bda18be25358f4e1322e94ec9Christian MaederprintVarDeclL = punctuate semi . map printVarDecl
941254a2daaf605bda18be25358f4e1322e94ec9Christian MaederprintVarDecls :: [VAR_DECL] -> Doc
941254a2daaf605bda18be25358f4e1322e94ec9Christian MaederprintVarDecls = fsep . printVarDeclL
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintVarDecl :: VAR_DECL -> Doc
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederprintVarDecl (Var_decl l s _) = printSortedVars l s
6c4ee04931dded62728f3a9954b2799beed536e9Christian MaederprintArgDecls :: [VAR_DECL] -> Doc
6c4ee04931dded62728f3a9954b2799beed536e9Christian MaederprintArgDecls = parens . printVarDecls
434c11a96bc623ebd5b60781efabef319bb15b0eChristian MaederprintOptArgDecls :: [VAR_DECL] -> Doc
434c11a96bc623ebd5b60781efabef319bb15b0eChristian MaederprintOptArgDecls vs = if null vs then empty else printArgDecls vs
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederprintPredHead :: PRED_HEAD -> Doc
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederprintPredHead (Pred_head l _) = printArgDecls l
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintPredItem :: FormExtension f => PRED_ITEM f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintPredItem p = case p of
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder Pred_decl l t _ -> fsep $ punctuate comma (map idLabelDoc l)
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder ++ [colon <+> printPredType t]
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder Pred_defn i h f _ ->
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder sep [ cat [idLabelDoc i, printPredHead h]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder , equiv <+> printAnnoted printFormula f]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension f => Pretty (PRED_ITEM f) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder pretty = printPredItem
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintAttr :: FormExtension f => OP_ATTR f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintAttr a = case a of
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder Assoc_op_attr -> text assocS
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder Comm_op_attr -> text commS
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder Idem_op_attr -> text idemS
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder Unit_op_attr t -> text unitS <+> printTerm t
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension f => Pretty (OP_ATTR f) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder pretty = printAttr
0015e1756b734b34d4b550318c078f9a0c585611Christian MaederprintOpHead :: OP_HEAD -> Doc
51b1633dc0785a542da974fae21fa7d6622c934eChristian MaederprintOpHead (Op_head k l mr _) =
434c11a96bc623ebd5b60781efabef319bb15b0eChristian Maeder sep $ printOptArgDecls l : case mr of
51b1633dc0785a542da974fae21fa7d6622c934eChristian Maeder Nothing -> []
51b1633dc0785a542da974fae21fa7d6622c934eChristian Maeder Just r -> [(case k of
0015e1756b734b34d4b550318c078f9a0c585611Christian Maeder Total -> colon
4bfb376555741367711b45323007f7375958530eChristian Maeder Partial -> text colonQuMark) <+> idDoc r]
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maederinstance Pretty OP_HEAD where
03a6bbff551286168d0b15dc53476c2ede4e60d0Christian Maeder pretty = printOpHead
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintOpItem :: FormExtension f => OP_ITEM f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintOpItem p = case p of
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder Op_decl l t a _ -> fsep $ punctuate comma (map idLabelDoc l)
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder ++ [colon <> (if null a then id else (<> comma)) (printOpType t)]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder ++ punctuate comma (map printAttr a)
c4a8059d0469a85bb58c28ac66729ac19d743d3cChristian Maeder Op_defn i h@(Op_head _ l _ _) t _ ->
4bfb376555741367711b45323007f7375958530eChristian Maeder sep [ (if null l then sep else cat) [idLabelDoc i, printOpHead h]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder , equals <+> printAnnoted printTerm t]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension f => Pretty (OP_ITEM f) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder pretty = printOpItem
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance Pretty VAR_DECL where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printVarDecl
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintOpType :: OP_TYPE -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintOpType (Op_type p l r _) =
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder [] -> case p of
37354e3ed68875fb527338105a610df481f98cb0Christian Maeder Partial -> quMarkD <+> idDoc r
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Total -> space <> idDoc r
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder _ -> space <> fsep
50ed946595d60c06f773e73bb22b21f5cf1199caChristian Maeder (punctuate (space <> cross) (map idDoc l)
50ed946595d60c06f773e73bb22b21f5cf1199caChristian Maeder ++ [case p of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Partial -> pfun
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Total -> funArrow,
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance Pretty OP_TYPE where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printOpType
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintOpSymb :: OP_SYMB -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintOpSymb o = case o of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Op_name i -> idDoc i
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian Maeder Qual_op_name i t _ -> fsep [text opS, idDoc i, colon <> printOpType t]
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance Pretty OP_SYMB where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printOpSymb
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintPredType :: PRED_TYPE -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintPredType (Pred_type l _) = case l of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder [] -> parens empty
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder _ -> fsep $ punctuate (space <> cross) $ map idDoc l
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance Pretty PRED_TYPE where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printPredType
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintPredSymb :: PRED_SYMB -> Doc
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederprintPredSymb p = case p of
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Pred_name i -> idDoc i
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder Qual_pred_name i t _ ->
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder parens $ fsep [text predS, idDoc i, colon <+> printPredType t]
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maederinstance Pretty PRED_SYMB where
d06598e0c310f65ab552ca55626c2f7694ffd5e3Christian Maeder pretty = printPredSymb
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty SYMB_ITEMS where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty = printSymbItems
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintSymbItems :: SYMB_ITEMS -> Doc
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian MaederprintSymbItems (Symb_items k l _) =
9031d53c51b21d50ff4af9e8a365f0252401539fChristian Maeder print_kind_text k l <+> sepByCommas (map printSymb l)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty SYMB where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty = printSymb
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintSymb :: SYMB -> Doc
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintSymb s = case s of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Symb_id i -> idDoc i
224e5f347275f5e9ada6cd976f195de2e77e41cbChristian Maeder Qual_id i t _ -> fsep [idDoc i, colon <> printType t]
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty TYPE where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty = printType
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintType :: TYPE -> Doc
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintType t = case t of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang O_type ot -> printOpType ot
224e5f347275f5e9ada6cd976f195de2e77e41cbChristian Maeder P_type pt -> space <> printPredType pt
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder A_type s -> space <> idDoc s
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangprint_kind_text :: SYMB_KIND -> [a] -> Doc
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangprint_kind_text k l = case k of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Implicit -> empty
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder _ -> keyword (pluralS_symb_list k l)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangpluralS_symb_list :: SYMB_KIND -> [a] -> String
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangpluralS_symb_list k l = (case k of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Implicit -> error "pluralS_symb_list"
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Sorts_kind -> sortS
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder Ops_kind -> opS
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder Preds_kind -> predS) ++ appendS l
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty SYMB_OR_MAP where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty = printSymbOrMap
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintSymbOrMap :: SYMB_OR_MAP -> Doc
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintSymbOrMap som = case som of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang Symb s -> printSymb s
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian Maeder Symb_map s t _ -> fsep [printSymb s, mapsto <+> printSymb t]
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty SYMB_KIND where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty = printSymbKind
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintSymbKind :: SYMB_KIND -> Doc
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintSymbKind sk = print_kind_text sk [()]
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty SYMB_MAP_ITEMS where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty = printSymbMapItems
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangprintSymbMapItems :: SYMB_MAP_ITEMS -> Doc
8c4c53f1d84490c7eac208905e92964c6508c1d6Christian MaederprintSymbMapItems (Symb_map_items k l _) =
9031d53c51b21d50ff4af9e8a365f0252401539fChristian Maeder print_kind_text k l <+> sepByCommas (map printSymbOrMap l)
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder-- possibly use "printInfix False vcat"
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian MaederprintInfix :: Bool -- ^ attach separator to right argument?
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder -> ([Doc] -> Doc) -- ^ combinator for two docs
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder -> Doc -> Doc -> Doc -- ^ left, separator and right arguments
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian MaederprintInfix b join l s r =
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder join $ if b then [l, s <+> r] else [l <+> s, r]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederclass (GetRange f, Pretty f) => FormExtension f where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder isQuantifierLike :: f -> Bool
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder isQuantifierLike _ = False
8c6b80162937eae0fe868c3b52bda6b50a153478Christian Maeder prefixExt :: f -> Doc -> Doc
8c6b80162937eae0fe868c3b52bda6b50a153478Christian Maeder prefixExt _ = (bullet <+>)
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension ()
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintRecord :: FormExtension f => Record f Doc Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintRecord = Record
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder { foldQuantification = \ _ q l r _ ->
941254a2daaf605bda18be25358f4e1322e94ec9Christian Maeder fsep $ printQuant q : printVarDeclL l
84855a862ab77950c0c5059b1bba98cce0fb8ac3Christian Maeder ++ [addBullet r]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , foldJunction = \ o j l _ ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let (n, p) = case j of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Con -> (trueS, andDoc)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Dis -> (falseS, orDoc)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Junction _ ol@(_ : _) _ -> fsep $ prepPunctuate (p <> space)
aaae8c00d7868d09d8bf52acd7d93ac39eaff5b5Christian Maeder $ zipWith (mkJunctDoc True) (init ol) (init l) ++
aaae8c00d7868d09d8bf52acd7d93ac39eaff5b5Christian Maeder [mkJunctDoc False (last ol) (last l)]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , foldRelation = \ o l c r _ ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let Relation oL _ oR _ = o
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder b = c == Implication
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder nl = if isAnyImpl oL || b && isQuant oL
aaae8c00d7868d09d8bf52acd7d93ac39eaff5b5Christian Maeder then parens l else l
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder nr = if isImpl c oR || not b && isQuant oR
aaae8c00d7868d09d8bf52acd7d93ac39eaff5b5Christian Maeder then parens r else r
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Implication -> printInfix True sep nl implies nr
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder RevImpl -> printInfix True sep nr (text ifS) nl
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Equivalence -> printInfix True sep
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (if isQuant oL then parens l else mkEquivDoc oL l)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder equiv $ mkEquivDoc oR r
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder , foldNegation = \ orig r _ -> case orig of
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder Negation o _ -> hsep [notDoc, mkJunctDoc False o r]
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder _ -> error "CASL.ToDoc.printRecord.foldNegation"
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , foldAtom = \ _ b _ -> text $ if b then trueS else falseS
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder , foldPredication = \ o p l _ -> case (p, o) of
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder (Pred_name i, Predication _ ol _) -> predIdApplDoc i $ zipConds ol l
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder _ -> if null l then printPredSymb p else
9031d53c51b21d50ff4af9e8a365f0252401539fChristian Maeder fcat [printPredSymb p, parens $ sepByCommas l]
c26ff5708c4a855bf9503b3001bcc19e5fd6286fChristian Maeder , foldDefinedness = \ _ r _ -> hsep [text defS, r]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , foldEquation = \ _ l e r _ -> printInfix True sep l (case e of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Existl -> exequal
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Strong -> equals) r
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , foldMembership = \ _ r t _ -> fsep [r, inDoc, idDoc t]
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , foldMixfix_formula = \ _ r -> r
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder , foldSort_gen_ax = \ o _ _ ->
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder let Sort_gen_ax constrs b = o
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder l = recoverType constrs
9ba43c9323dc1a4bb1e684d87370b43468ab9096Christian Maeder genAx = sep [ keyword generatedS <+> keyword (typeS ++ appendS l)
f91429a7a295a517eda0dc70f590e44e3b71fa79Christian Maeder , semiAnnos printDATATYPE_DECL l]
9c06522a04b3f7bc904091ca1abaa2f956113c94Christian Maeder in if b then text "%% free" $+$ genAx else genAx
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldQuantOp = \ _ o n r -> fsep
fed28ca105e1d669eef1781b1fb45d29cabd9e06Christian Maeder , parens . printOpSymb $ mkQualOp o n
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , addBullet r ]
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldQuantPred = \ _ p n r -> fsep
fed28ca105e1d669eef1781b1fb45d29cabd9e06Christian Maeder , printPredSymb $ mkQualPred p n
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , addBullet r ]
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder , foldExtFORMULA = const pretty
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , foldQual_var = \ _ v s _ ->
4674b607529c8eab497240da6da1ef9ae786611cChristian Maeder parens $ fsep [text varS, sidDoc v, colon <+> idDoc s]
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder , foldApplication = \ orig o l _ -> case (o, orig) of
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder (Op_name i, Application _ ol _) -> idApplDoc i $ zipConds ol l
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder _ -> let d = parens $ printOpSymb o in
9031d53c51b21d50ff4af9e8a365f0252401539fChristian Maeder if null l then d else fcat [d, parens $ sepByCommas l]
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder , foldSorted_term = \ _ r t _ -> fsep [idApplDoc typeId [r], idDoc t]
479da8506f391abe070ced2fb93c9759a280fa68Christian Maeder , foldCast = \ _ r t _ ->
b65890a7645b96eb0d5c334c81ba9dca86d556bfChristian Maeder fsep [idApplDoc (mkId [placeTok, mkSimpleId asS]) [r], idDoc t]
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder , foldConditional = \ o l f r _ -> case o of
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder Conditional ol _ _ _ -> fsep [if isCond ol then parens l else l,
19c2d25601388b3d93c0784b944eddc81f8746b7Christian Maeder text whenS <+> f, text elseS <+> r]
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder _ -> error "CASL.ToDoc.printRecord.foldConditional"
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldMixfix_qual_pred = const printPredSymb
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder , foldMixfix_term = \ o l -> case o of
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder Mixfix_term [_, Mixfix_parenthesized _ _] -> fcat l
e92e93922166c81167de83cc7400403c5d9bb26cChristian Maeder , foldMixfix_token = const sidDoc
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , foldMixfix_sorted_term = \ _ s _ -> colon <+> idDoc s
f799084b320209cdd71a29e74fff1be054c1d342Christian Maeder , foldMixfix_cast = \ _ s _ -> text asS <+> idDoc s
9031d53c51b21d50ff4af9e8a365f0252401539fChristian Maeder , foldMixfix_parenthesized = \ _ l _ -> parens $ sepByCommas l
9031d53c51b21d50ff4af9e8a365f0252401539fChristian Maeder , foldMixfix_bracketed = \ _ l _ -> brackets $ sepByCommas l
6e538f8086fb560f0b88d49581f0006d6323bdc0Christian Maeder , foldMixfix_braced = \ _ l _ -> specBraces $ sepByCommas l
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder , foldExtTERM = const pretty }
f91429a7a295a517eda0dc70f590e44e3b71fa79Christian MaederrecoverType :: [Constraint] -> [Annoted DATATYPE_DECL]
fef03b64e3b1d7d3a8e098f62ef2e7687a433f09Christian Maeder map (\ c -> let s = newSort c in emptyAnno $ Datatype_decl s
d8f14f4b0bc8d94b61a10c1d268ac33c8e43cca0Christian Maeder (map (\ (o, _) -> case o of
4b960c5e777824979d5126bbde17f21d969a795bChristian Maeder Qual_op_name i (Op_type fk args _ ps) r ->
f91429a7a295a517eda0dc70f590e44e3b71fa79Christian Maeder let qs = appRange ps r in emptyAnno $ case args of
f91429a7a295a517eda0dc70f590e44e3b71fa79Christian Maeder [_] | isInjName i -> Subsorts args qs
f91429a7a295a517eda0dc70f590e44e3b71fa79Christian Maeder _ -> Alt_construct fk i (map Sort args) qs
fef03b64e3b1d7d3a8e098f62ef2e7687a433f09Christian Maeder _ -> error "CASL.recoverType") $ opSymbs c) nullRange)
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian MaederzipConds :: [TERM f] -> [Doc] -> [Doc]
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian MaederzipConds = zipWith (\ o d -> if isCond o then parens d else d)
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintFormula :: FormExtension f => FORMULA f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintFormula = foldFormula printRecord
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension f => Pretty (FORMULA f) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder pretty = printFormula
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintTerm :: FormExtension f => TERM f -> Doc
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintTerm = foldTerm printRecord
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maederinstance FormExtension f => Pretty (TERM f) where
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder pretty = printTerm
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederisQuant :: FormExtension f => FORMULA f -> Bool
2344f16936f5b31c9530d0cafb3838e9df3f3644Christian MaederisQuant f = case f of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Quantification {} -> True
ccd28c25c1aee73a195053e677eca17e20917d84Christian Maeder ExtFORMULA ef -> isQuantifierLike ef
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Junction _ l _ -> case l of
aaae8c00d7868d09d8bf52acd7d93ac39eaff5b5Christian Maeder _ -> isQuant $ last l
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Relation a c b _ -> isQuant $ if c == RevImpl then a else b
aaae8c00d7868d09d8bf52acd7d93ac39eaff5b5Christian Maeder Negation a _ -> isQuant a
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian MaederisEquiv :: FORMULA f -> Bool
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederisEquiv f = case f of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Relation _ c _ _ -> c == Equivalence
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian MaederisAnyImpl :: FORMULA f -> Bool
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederisAnyImpl f = isImpl Implication f || isImpl RevImpl f
8adae8b1eb0dd8562f0d1541b9ecb2fd80bda7e7Christian MaederisJunct :: FORMULA f -> Bool
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederisJunct f = case f of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Junction {} -> True
abcb1baa565c878598d732d0aa7724f474c9265cChristian Maeder _ -> isAnyImpl f
aaae8c00d7868d09d8bf52acd7d93ac39eaff5b5Christian Maeder-- true for non-final
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaedermkJunctDoc :: FormExtension f => Bool -> FORMULA f -> Doc -> Doc
aaae8c00d7868d09d8bf52acd7d93ac39eaff5b5Christian MaedermkJunctDoc b f = if isJunct f || b && isQuant f then parens else id
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaedermkEquivDoc :: FORMULA f -> Doc -> Doc
690e4ab8f298d9cff3803316cda70ad9b98e9c43Christian MaedermkEquivDoc f = if isEquiv f then parens else id
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederisImpl :: Relation -> FORMULA f -> Bool
abcb1baa565c878598d732d0aa7724f474c9265cChristian MaederisImpl a f = case f of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Relation _ c _ _ -> c == Equivalence || a /= c
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederisCond :: TERM f -> Bool
f799084b320209cdd71a29e74fff1be054c1d342Christian MaederisCond t = case t of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Conditional {} -> True
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder-- | a helper class for calculating the pluralS of e.g. ops
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederclass ListCheck a where
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder innerList :: a -> [()]
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederinstance ListCheck Token where
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder innerList _ = [()]
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederinstance ListCheck Id where
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder innerList _ = [()]
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederinstance ListCheck a => ListCheck [a] where
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder innerList = concatMap innerList
1c53d99313dcdd6e1ba0022689aa97de1b064a67Christian Maeder-- | an instance of ListCheck for Annoted stuff
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederinstance ListCheck a => ListCheck (Annoted a) where
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maeder innerList = innerList . item
25d255de248ab96a6c750309192b7217061e186dChristian Maeder{- | pluralS checks nested lists via the class ListCheck to decide
25d255de248ab96a6c750309192b7217061e186dChristian Maederif a plural s should be appended. -}
47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian MaederpluralS :: ListCheck a => a -> String
9ba43c9323dc1a4bb1e684d87370b43468ab9096Christian MaederpluralS = appendS . innerList
9ba43c9323dc1a4bb1e684d87370b43468ab9096Christian MaederappendS :: [a] -> String
9ba43c9323dc1a4bb1e684d87370b43468ab9096Christian MaederappendS l = if isSingle l then "" else "s"
9c06522a04b3f7bc904091ca1abaa2f956113c94Christian Maeder-- instances of ListCheck for various data types of AS_Basic_CASL
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wanginstance ListCheck (SORT_ITEM f) where
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang innerList (Sort_decl l _) = innerList l
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang innerList (Subsort_decl l _ _) = innerList l
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder innerList (Subsort_defn {}) = [()]
25d255de248ab96a6c750309192b7217061e186dChristian Maeder innerList (Iso_decl l _) = innerList $ drop 1 l
25d255de248ab96a6c750309192b7217061e186dChristian Maeder -- assume last sort is known
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wanginstance ListCheck (OP_ITEM f) where
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang innerList (Op_decl l _ _ _) = innerList l
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder innerList (Op_defn {}) = [()]
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wanginstance ListCheck (PRED_ITEM f) where
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang innerList (Pred_decl l _ _) = innerList l
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder innerList (Pred_defn {}) = [()]
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wanginstance ListCheck VAR_DECL where
5be2fb5bcfaa6abbb6043d679a1d536b4878b789Jian Chun Wang innerList (Var_decl l _ _) = innerList l
9c06522a04b3f7bc904091ca1abaa2f956113c94Christian Maeder-- | print a formula as a sentence
ccd28c25c1aee73a195053e677eca17e20917d84Christian MaederprintTheoryFormula :: FormExtension f => Named (FORMULA f) -> Doc
9c06522a04b3f7bc904091ca1abaa2f956113c94Christian MaederprintTheoryFormula f = printAnnoted
9c06522a04b3f7bc904091ca1abaa2f956113c94Christian Maeder ((case sentence f of
9c06522a04b3f7bc904091ca1abaa2f956113c94Christian Maeder Quantification Universal _ _ _ -> id
9c06522a04b3f7bc904091ca1abaa2f956113c94Christian Maeder Sort_gen_ax _ _ -> id
8c6b80162937eae0fe868c3b52bda6b50a153478Christian Maeder ExtFORMULA e -> prefixExt e
9c06522a04b3f7bc904091ca1abaa2f956113c94Christian Maeder _ -> (bullet <+>)) . pretty) $ fromLabelledSen f