0N/A{-|

0N/AModule : $Header$

0N/ACopyright : (c) Christian Maeder, Sonja Groening, Uni Bremen 2002-2004

0N/ALicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

0N/A

0N/AMaintainer : maeder@tzi.de

0N/AStability : provisional

0N/APortability : non-portable(Logic)

0N/A

0N/A Here is the place where the class Logic is instantiated for Haskell.

0N/A Also the instances for Syntax an Category.

0N/A

0N/A todo:

0N/A - writing real functions

0N/A

0N/A-}

0N/A

0N/Amodule Haskell.Logic_Haskell (Haskell(..)) where

0N/A

0N/Aimport Data.Dynamic

0N/A

0N/Aimport Common.Result (Result (..))

0N/Aimport Common.PrettyPrint

0N/A

0N/Aimport Haskell.ATC_Haskell -- generated ATerm conversions

0N/Aimport Haskell.PrintModuleInfo

0N/Aimport Haskell.HatParser (HsDecls,

0N/A hatParser)

0N/Aimport Haskell.HatAna

0N/Aimport Haskell.Hatchet.MultiModuleBasics (ModuleInfo,

0N/A emptyModuleInfo,

0N/A joinModuleInfo)

0N/Aimport Haskell.Hatchet.AnnotatedHsSyn (AHsDecl)

0N/Aimport Haskell.Hatchet.HsSyn (HsDecl)

0N/A

0N/Aimport Logic.Logic

0N/A

0N/AmoduleInfoTc, hsDeclTc, aHsDeclTc :: TyCon

0N/AmoduleInfoTc = mkTyCon "Haskell.Hatchet.MultiModuleBasics.ModuleInfo"

0N/AhsDeclTc = mkTyCon "Haskell.Hatchet.HsSyn.HsDecl"

0N/AaHsDeclTc = mkTyCon "Haskell.Hatchet.AnnotatedHsSyn.AHsDecl"

0N/A

0N/Ainstance Typeable ModuleInfo where

0N/A typeOf _ = mkTyConApp moduleInfoTc []

0N/Ainstance Typeable HsDecl where

0N/A typeOf _ = mkTyConApp hsDeclTc []

0N/Ainstance Typeable AHsDecl where

0N/A typeOf _ = mkTyConApp aHsDeclTc []

0N/A

0N/Ainstance PrintLaTeX ModuleInfo where

0N/A printLatex0 = printText0

0N/Ainstance PrintLaTeX HsDecls where

0N/A printLatex0 = printText0

0N/Ainstance PrintLaTeX AHsDecl where

0N/A printLatex0 = printText0

0N/A

0N/A-- a dummy datatype for the LogicGraph and for identifying the right

0N/A-- instances

0N/A

0N/Adata Haskell = Haskell deriving (Show)

0N/Ainstance Language Haskell -- default definition is okay

0N/A

0N/Atype Sign = ModuleInfo

0N/Atype Morphism = ()

0N/A

0N/Ainstance Category Haskell Sign Morphism where

0N/A dom Haskell _ = empty_signature Haskell

0N/A

0N/A-- abstract syntax, parsing (and printing)

0N/A

0N/Atype SYMB_ITEMS = ()

0N/Atype SYMB_MAP_ITEMS = ()

0N/A

0N/Ainstance Syntax Haskell HsDecls

0N/A SYMB_ITEMS SYMB_MAP_ITEMS

0N/A where

0N/A parse_basic_spec Haskell = Just hatParser

0N/A parse_symb_items Haskell = Nothing

0N/A parse_symb_map_items Haskell = Nothing

0N/A

0N/Atype Haskell_Sublogics = ()

0N/A

0N/Atype Sentence = AHsDecl

0N/Ainstance Ord AHsDecl where

0N/A compare _x _y = error "Haskell.Logic_Haskell: compare for AHsDecl"

0N/A

0N/Atype Symbol = ()

0N/Atype RawSymbol = ()

0N/A

0N/Ainstance Sentences Haskell Sentence () Sign Morphism Symbol where

0N/A map_sen Haskell _m s = return s

0N/A provers Haskell = []

0N/A cons_checkers Haskell = []

0N/A

0N/A

0N/Ainstance StaticAnalysis Haskell HsDecls

0N/A Sentence ()

0N/A SYMB_ITEMS SYMB_MAP_ITEMS

0N/A Sign

0N/A Morphism

0N/A Symbol RawSymbol

0N/A

0N/A

0N/A where

0N/A empty_signature Haskell

0N/A = emptyModuleInfo

0N/A signature_union Haskell sig1 sig2 = return (joinModuleInfo sig1 sig2)

0N/A inclusion Haskell _ _ = return ()

0N/A basic_analysis Haskell = Just(basicAnalysis)

0N/A where basicAnalysis (basicSpec, sig, _) =

0N/A let (modInfo, sens) = hatAna basicSpec sig

0N/A in Result [] $ Just (basicSpec, diffModInfo modInfo sig,

0N/A modInfo, sens)

0N/A

0N/Ainstance Logic Haskell Haskell_Sublogics

0N/A HsDecls Sentence SYMB_ITEMS SYMB_MAP_ITEMS

0N/A Sign

0N/A Morphism

0N/A Symbol RawSymbol ()

0N/A where data_logic Haskell = Nothing

0N/A