Logic_Maude.hs revision 6858f9c9c8b077b2b574a9f30753cf5fec8124d6
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuModule : $Header$
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiDescription : Instance of class Logic for Maude
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiCopyright : (c) Martin Kuehl, Uni Bremen 2008
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiMaintainer : mkhl@informatik.uni-bremen.de
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskiStability : experimental
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian MaederPortability : non-portable (imports Logic.Logic)
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian MaederInstance of class Logic for Maude.
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Also instances of Syntax and Category.
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maeder ... sometime in the future, that is.
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport qualified Maude.Sign as Sign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Maude.Morphism as Morphism
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport qualified Maude.Symbol as Symbol
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport qualified Maude.Sentence as Sentence
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- | Lid for Maude
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata Maude = Maude
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski deriving (Show, Eq)
da955132262baab309a50fdffe228c9efe68251dCui Jian-- | Instance of Language for Maude
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Language Maude where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski description _ = unlines
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski [ "Maude - A High-Performance Rewriting Logic Framework"
da955132262baab309a50fdffe228c9efe68251dCui Jian , "This logic is rewriting logic, a logic of concurrent change that"
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski , " can naturally deal with state and with concurrent computations."
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski , "For an overview of Maude see <http://maude.cs.uiuc.edu/overview.html>."
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski , "For an information on rewriting logic see <http://maude.cs.uiuc.edu/rwl.html>."
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski , "For anything else about the Maude project see <http://maude.cs.uiuc.edu/>." ]
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- | Instance of Category for Maude
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Category Sign.Sign Morphism.Morphism where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- isInclusion = \_ -> False -- TODO: implement Category.isInclusion.
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- legal_obj = Sign.isLegal -- seems to be obsolete
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- | Instance of Sentences for Maude
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Sentences Maude Sentence.Sentence Sign.Sign Morphism.Morphism Symbol.Symbol where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- -- sentences -- --
da955132262baab309a50fdffe228c9efe68251dCui Jian -- Uncommenting this signals a type error I don't understand...
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- is_of_sign Maude = flip Sign.includesSentence
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- -- | simplification of sentences (leave out qualifications)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- simplify_sen :: lid -> sign -> sentence -> sentence
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- simplify_sen _ _ = id -- default implementation
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- simplify_sen Maude _ = id
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- -- | parsing of sentences
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- parse_sentence :: lid -> Maybe (AParser st sentence)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- parse_sentence _ = Nothing
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- parse_sentence Maude = Nothing
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- -- | print a sentence with comments
da955132262baab309a50fdffe228c9efe68251dCui Jian -- print_named :: lid -> Named sentence -> Doc
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- -- symbols -- --
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski sym_name Maude = Symbol.toId