Logic_Haskell.hs revision f3a94a197960e548ecd6520bb768cb0d547457bb
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan MmillerModule : $Header$
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan MmillerCopyright : (c) Christian Maeder, Sonja Groening, Uni Bremen 2002-2004
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan MmillerLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan MmillerMaintainer : maeder@tzi.de
548846fe158900a483ca91f47603c6bb6fde9b47Jon BranchStability : provisional
81d426f4e03ac36896437325e6f67f74657b7dd9Chris DrakePortability : non-portable(Logic)
0f63005dc454e8131506be734dc0404f48c8578cJason LemayHere is the place where the classes 'Category', 'Syntax',
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch 'StaticAnalysis', 'Sentences', and 'Logic' are instantiated for
0f63005dc454e8131506be734dc0404f48c8578cJason Lemay Some method implementations for 'StaticAnalysis' and 'Sentences'
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch are still missing. -}
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchmodule Haskell.Logic_Haskell (Haskell(..), HaskellMorphism) where
0f63005dc454e8131506be734dc0404f48c8578cJason LemayhsDeclsTc :: TyCon
81d426f4e03ac36896437325e6f67f74657b7dd9Chris DrakehsDeclsTc = mkTyCon "Haskell.HatParser.HsDecls"
0f63005dc454e8131506be734dc0404f48c8578cJason Lemayinstance Typeable HsDecls where
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller typeOf _ = mkTyConApp hsDeclsTc []
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan MmillertyconSign :: TyCon
548846fe158900a483ca91f47603c6bb6fde9b47Jon BranchtyconSign = mkTyCon "Haskell.HatAna.Sign"
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchinstance Typeable Sign where
81d426f4e03ac36896437325e6f67f74657b7dd9Chris Drake typeOf _ = mkTyConApp tyconSign []
0f63005dc454e8131506be734dc0404f48c8578cJason LemaytyconPNT :: TyCon
0f63005dc454e8131506be734dc0404f48c8578cJason LemaytyconPNT = mkTyCon "Haskell.HatAna.PNT"
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchinstance Typeable PNT where
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch typeOf _ = mkTyConApp tyconPNT []
548846fe158900a483ca91f47603c6bb6fde9b47Jon BranchhsDeclItc :: TyCon
0f63005dc454e8131506be734dc0404f48c8578cJason LemayhsDeclItc = mkTyCon "Haskell.HatAna.TiDecl"
81d426f4e03ac36896437325e6f67f74657b7dd9Chris Drakeinstance Typeable i => Typeable (TiDecl i) where
81d426f4e03ac36896437325e6f67f74657b7dd9Chris Drake typeOf s = mkTyConApp hsDeclItc [typeOf $ (undefined :: TiDecl a -> a) s]
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchinstance PrintLaTeX HsDecls where
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch printLatex0 = printText0
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchinstance PrintLaTeX Sign where
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch printLatex0 = printText0
81d426f4e03ac36896437325e6f67f74657b7dd9Chris Drakeinstance PrintLaTeX (TiDecl PNT) where
0f63005dc454e8131506be734dc0404f48c8578cJason Lemay printLatex0 = printText0
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch-- a dummy datatype for the LogicGraph and for identifying the right
0f63005dc454e8131506be734dc0404f48c8578cJason Lemaydata Haskell = Haskell deriving (Show)
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchinstance Language Haskell where
0f63005dc454e8131506be734dc0404f48c8578cJason Lemay description _ =
0f63005dc454e8131506be734dc0404f48c8578cJason Lemay "Haskell - a purely functional programming language,\
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller \ featuring static typing, higher-order functions, polymorphism,\
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller \ type classes and monadic effects.\
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller \ See http://www.haskell.org. This version is based on Programatica,\
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch \ see http://www.cse.ogi.edu/PacSoft/projects/programatica/"
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchtype HaskellMorphism = DefaultMorphism Sign
81d426f4e03ac36896437325e6f67f74657b7dd9Chris Drakeinstance Category Haskell Sign HaskellMorphism where
81d426f4e03ac36896437325e6f67f74657b7dd9Chris Drake dom Haskell = domOfDefaultMorphism
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch cod Haskell = codOfDefaultMorphism
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch ide Haskell = ideOfDefaultMorphism
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller comp Haskell = compOfDefaultMorphism
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller legal_obj Haskell = const True
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller legal_mor Haskell = legalDefaultMorphism (legal_obj Haskell)
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller-- abstract syntax, parsing (and printing)
81d426f4e03ac36896437325e6f67f74657b7dd9Chris Draketype SYMB_ITEMS = ()
0f63005dc454e8131506be734dc0404f48c8578cJason Lemaytype SYMB_MAP_ITEMS = ()
0f63005dc454e8131506be734dc0404f48c8578cJason Lemayinstance Syntax Haskell HsDecls
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch SYMB_ITEMS SYMB_MAP_ITEMS
0f63005dc454e8131506be734dc0404f48c8578cJason Lemay parse_basic_spec Haskell = Just hatParser
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller parse_symb_items Haskell = Nothing
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch parse_symb_map_items Haskell = Nothing
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchtype Haskell_Sublogics = ()
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchtype Symbol = ()
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchtype RawSymbol = ()
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchinstance Sentences Haskell (TiDecl PNT) () Sign HaskellMorphism Symbol where
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch map_sen Haskell _m s = return s
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch print_named Haskell ga (NamedSen lab _ sen) = printText0 ga sen <>
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch if null lab then empty
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch else space <> text "{-" <+> text lab <+> text "-}"
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch provers Haskell = []
0f63005dc454e8131506be734dc0404f48c8578cJason Lemay cons_checkers Haskell = []
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branchinstance StaticAnalysis Haskell HsDecls
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch (TiDecl PNT) ()
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch SYMB_ITEMS SYMB_MAP_ITEMS
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch HaskellMorphism
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch Symbol RawSymbol where
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch basic_analysis Haskell = Just hatAna
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch empty_signature Haskell = emptySign
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller signature_union Haskell s = return . addSign s
7dcb2f62e25d05f2afeb4e79f10102350d7c2c7bBrendan Mmiller final_union Haskell = signature_union Haskell
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch inclusion Haskell = defaultInclusion (is_subsig Haskell)
8013147372959d2435f1f8b0305057cfce308168Jason Lemay is_subsig Haskell = isSubSign
8013147372959d2435f1f8b0305057cfce308168Jason Lemayinstance Logic Haskell Haskell_Sublogics
548846fe158900a483ca91f47603c6bb6fde9b47Jon Branch HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS
0f63005dc454e8131506be734dc0404f48c8578cJason Lemay HaskellMorphism
0f63005dc454e8131506be734dc0404f48c8578cJason Lemay Symbol RawSymbol ()