Copyright	(c) Christian Maeder, Uni Bremen 2002-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (multiple parameter class, functional dependency)
Safe Haskell	None

Haskell.HatAna

Description

This module supplies a signature type and a type checking function for the Haskell logic.

Documentation

type Scope = Rel (SN HsName) (Ent (SN String))

data Sign

Constructors

Sign
Fields instances :: [Instance PNT] types :: Map (HsIdentI PNT) (Kind, TypeInfo PNT) values :: Map (HsIdentI PNT) (Scheme PNT) scope :: Scope fixities :: Map (HsIdentI (SN String)) HsFixity

Instances

Eq Sign
Ord Sign
Show Sign
ShATermConvertible Sign
Pretty Sign
Typeable * Sign
Comorphism HasCASL2Haskell HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism Symbol RawSymbol ()
Comorphism Haskell2IsabelleHOL Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Comorphism Haskell2IsabelleHOLCF Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Logic Haskell Haskell_Sublogics HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS Sign HaskellMorphism Symbol RawSymbol ()
StaticAnalysis Haskell HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS Sign HaskellMorphism Symbol RawSymbol
Sentences Haskell (TiDecl PNT) Sign HaskellMorphism Symbol

diffSign :: Sign -> Sign -> Sign

addSign :: Sign -> Sign -> Sign

isSubSign :: Sign -> Sign -> Bool

printSign :: Sign -> Doc

extendSign :: Sign -> [Instance PNT] -> [TAssump PNT] -> [Assump PNT] -> Scope -> [(HsIdentI (SN String), HsFixity)] -> Sign

emptySign :: Sign

hatAna :: (HsDecls, Sign, GlobalAnnos) -> Result (HsDecls, ExtSign Sign (), [Named (TiDecl PNT)])

preludeSign :: Sign

hatAna2 :: (HsDecls, Sign, GlobalAnnos) -> Result (HsDecls, Sign, [Named (TiDecl PNT)])

formSrcLoc :: SrcLoc -> Pos

getHsDecl :: (Rec a b, GetBaseStruct b (DI i e p ds t [t] t)) => a -> DI i e p ds t [t] t

preludeConflicts :: [HsDecl] -> ([HsDecl], [Diagnosis])

preludeEntity :: (Printable i, Show t, DefinedNames i t) => DI i e p ds t [t] t -> Bool

preludeMatch :: Printable i => HsMatchI i e p ds -> Bool

preludeConstr :: Printable i => HsConDeclI i t [t] -> Bool

genPrefixes :: [String]

prefixed :: String -> Bool

preludeValues :: Set String

preludeConstrs :: Set String

preludeTypes :: Set String

data PNT :: *

Instances

Eq PNT
Ord PNT
Read PNT
Show PNT
ShATermConvertible PNT
HasSrcLoc PNT
HasSpecialNames PNT
IsSpecialName PNT
Printable PNT
PrintableOp PNT
HasOrig PNT
TypeVar PNT
TypeId PNT
TypeCon PNT
Fresh PNT
ValueId PNT
IsaName PNT
Typeable * PNT
HasIdTy PId PNT
HasBaseName PNT HsName
TypedId PId PNT
QualNames PNT ModuleName PNT
Comorphism HasCASL2Haskell HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism Symbol RawSymbol ()
Comorphism Haskell2IsabelleHOL Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Comorphism Haskell2IsabelleHOLCF Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Logic Haskell Haskell_Sublogics HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS Sign HaskellMorphism Symbol RawSymbol ()
StaticAnalysis Haskell HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS Sign HaskellMorphism Symbol RawSymbol
Sentences Haskell (TiDecl PNT) Sign HaskellMorphism Symbol
Eq (TiDecl PNT)
Ord (TiDecl PNT)
GetRange (TiDecl PNT)
Pretty (TiDecl PNT)
ToJson (TiDecl PNT)
ToXml (TiDecl PNT)

data TiDecl i :: * -> *

Instances

Comorphism HasCASL2Haskell HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism Symbol RawSymbol ()
Comorphism Haskell2IsabelleHOL Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Comorphism Haskell2IsabelleHOLCF Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism () () () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Logic Haskell Haskell_Sublogics HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS Sign HaskellMorphism Symbol RawSymbol ()
StaticAnalysis Haskell HsDecls (TiDecl PNT) SYMB_ITEMS SYMB_MAP_ITEMS Sign HaskellMorphism Symbol RawSymbol
TypeVar i => Types i (TiDecl i)
DefinedNames i (TiDecl i)
MapDefinedNames i (TiDecl i)
HasAbstr i (TiDecl i)
Eq i => FreeNames i (TiDecl i)
(TypeVar i, ValueId i) => DeclInfo i (TiDecl i)
ClassMethods i (TiDecl i)
ValueId i => AddName i (TiDecl i)
Sentences Haskell (TiDecl PNT) Sign HaskellMorphism Symbol
Eq i => HasLocalDef i (TiExp i) (TiDecl i)
Eq (TiDecl PNT)
Ord (TiDecl PNT)
Show i => Show (TiDecl i)
ShATermConvertible i => ShATermConvertible (TiDecl i)
HasSrcLoc (TiDecl i)
(TypeId i, ValueId i, PrintableOp i) => Printable (TiDecl i)
GetRange (TiDecl PNT)
Pretty (TiDecl PNT)
ToJson (TiDecl PNT)
ToXml (TiDecl PNT)
HasBaseStruct (TiDecl i) (DBase i)
GetBaseStruct (TiDecl i) (DBase i)
Rec (TiDecl i) (DStruct i)
MapExp (TiExp i) (TiDecl i)
HasDefs (TiDecls i) (TiDecl i)
HasDef (TiDecls i) (TiDecl i)
TypeVar i => EnvFrom (TiDecl i) (DeclsUseType i)
HasPropStruct (TiDecl i) (PD i (OTiAssertion i) (TiPredicate i))
Typeable (* -> *) TiDecl