Logic_Haskell.hs revision d946c1bfdd7d58aa7c023efe864d5999eb44a61b
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederCopyright : (c) Christian Maeder, Sonja Groening, Uni Bremen 2002-2004
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederMaintainer : maeder@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable(Logic)
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederHere is the place where the classes 'Category', 'Syntax',
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder 'StaticAnalysis', 'Sentences', and 'Logic' are instantiated for
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder Some method implementations for 'StaticAnalysis' and 'Sentences'
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian Maeder are still missing. -}
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (Haskell(..),
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich HaskellMorphism,
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich SYMB_MAP_ITEMS,
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich Haskell_Sublogics,
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder RawSymbol) where
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederinstance PrintLaTeX HsDecls where
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder printLatex0 = printText0
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance PrintLaTeX Sign where
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder printLatex0 = printText0
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance PrintLaTeX (TiDecl PNT) where
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder printLatex0 = printText0
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder-- a dummy datatype for the LogicGraph and for identifying the right
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata Haskell = Haskell deriving (Show)
74eed04be26f549d2f7ca35c370e1c03879b28b1Christian Maederinstance Language Haskell where
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder description _ =
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder "Haskell - a purely functional programming language,\
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder \ featuring static typing, higher-order functions, polymorphism,\
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder \ type classes and monadic effects.\
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder \ See http://www.haskell.org. This version is based on Programatica,\
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder \ see http://www.cse.ogi.edu/PacSoft/projects/programatica/"
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maedertype HaskellMorphism = DefaultMorphism Sign
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederinstance Category Haskell Sign HaskellMorphism where
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder dom Haskell = domOfDefaultMorphism
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder cod Haskell = codOfDefaultMorphism
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder ide Haskell = ideOfDefaultMorphism
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder comp Haskell = compOfDefaultMorphism
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder legal_obj Haskell = const True
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder legal_mor Haskell = legalDefaultMorphism (legal_obj Haskell)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder-- abstract syntax, parsing (and printing)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maedertype SYMB_ITEMS = ()
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maedertype SYMB_MAP_ITEMS = ()
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maederinstance Syntax Haskell HsDecls
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder parse_basic_spec Haskell = Just hatParser
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder parse_symb_items Haskell = Nothing
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder parse_symb_map_items Haskell = Nothing
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maedertype Haskell_Sublogics = ()
d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maedertype Symbol = ()
8cacad2a09782249243b80985f28e9387019fe40Christian Maedertype RawSymbol = ()
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maederinstance Sentences Haskell (TiDecl PNT) () Sign HaskellMorphism Symbol where
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder map_sen Haskell _m s = return s
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder print_named Haskell ga NamedSen{senName = lab, sentence = sen} =
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich printText0 ga sen <>
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder if null lab then empty
797ccd67cb8ae127be097cd43448801b673e3b69Christian Maeder else space <> text "{-" <+> text lab <+> text "-}"
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder provers Haskell = []
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder cons_checkers Haskell = []
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maederinstance StaticAnalysis Haskell HsDecls
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder (TiDecl PNT) ()
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder HaskellMorphism
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder Symbol RawSymbol where
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder basic_analysis Haskell = Just hatAna
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder empty_signature Haskell = emptySign
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder signature_union Haskell s = return . addSign s
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder final_union Haskell = signature_union Haskell
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder inclusion Haskell = defaultInclusion (is_subsig Haskell)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder is_subsig Haskell = isSubSign
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederinstance Logic Haskell Haskell_Sublogics
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder HaskellMorphism
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Symbol RawSymbol ()