Copyright | (c) Christian Maeder and Uni Bremen 2003-2005 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
HasCASL.Le
Contents
Description
abstract syntax during static analysis
- data ClassInfo = ClassInfo {
- rawKind :: RawKind
- classKinds :: Set Kind
- type ClassMap = Map Id ClassInfo
- data GenKind
- data AltDefn = Construct (Maybe Id) [Type] Partiality [[Selector]]
- data Selector = Select (Maybe Id) Type Partiality
- type IdMap = Map Id Id
- data DataEntry = DataEntry IdMap Id GenKind [TypeArg] RawKind (Set AltDefn)
- data TypeDefn
- data TypeInfo = TypeInfo {
- typeKind :: RawKind
- otherTypeKinds :: Set Kind
- superTypes :: Set Id
- typeDefn :: TypeDefn
- type TypeMap = Map Id TypeInfo
- starTypeInfo :: TypeInfo
- mapType :: IdMap -> Type -> Type
- data Sentence
- data TypeVarDefn = TypeVarDefn Variance VarKind RawKind Int
- type LocalTypeVars = Map Id TypeVarDefn
- data VarDefn = VarDefn Type
- data ConstrInfo = ConstrInfo {
- constrId :: Id
- constrType :: TypeScheme
- data OpDefn
- = NoOpDefn OpBrand
- | ConstructData Id
- | SelectData (Set ConstrInfo) Id
- | Definition OpBrand Term
- data OpInfo = OpInfo {}
- isConstructor :: OpInfo -> Bool
- type Assumps = Map Id (Set OpInfo)
- data Env = Env {}
- initialEnv :: Env
- data Constrain
- addDiags :: [Diagnosis] -> State Env ()
- appendSentences :: [Named Sentence] -> State Env ()
- putClassMap :: ClassMap -> State Env ()
- putLocalVars :: Map Id VarDefn -> State Env ()
- fromResult :: (Env -> Result a) -> State Env (Maybe a)
- addSymbol :: Symbol -> State Env ()
- putLocalTypeVars :: LocalTypeVars -> State Env ()
- putTypeMap :: TypeMap -> State Env ()
- putAssumps :: Assumps -> State Env ()
- putBinders :: Map Id Id -> State Env ()
- getVar :: VarDecl -> Id
- checkUniqueVars :: [VarDecl] -> State Env ()
- type FunMap = Map (Id, TypeScheme) (Id, TypeScheme)
- data Morphism = Morphism {}
- mkMorphism :: Env -> Env -> Morphism
- isInclMor :: Morphism -> Bool
- data SymbolType
- data Symbol = Symbol {
- symName :: Id
- symType :: SymbolType
- type SymbolMap = Map Symbol Symbol
- type SymbolSet = Set Symbol
- idToTypeSymbol :: Id -> RawKind -> Symbol
- idToClassSymbol :: Id -> RawKind -> Symbol
- idToOpSymbol :: Id -> TypeScheme -> Symbol
- data RawSymbol
- type RawSymbolMap = Map RawSymbol RawSymbol
- idToRaw :: Id -> RawSymbol
- rawSymName :: RawSymbol -> Id
- symbTypeToKind :: SymbolType -> SymbKind
- symbolToRaw :: Symbol -> RawSymbol
- symbKindToRaw :: SymbKind -> Id -> RawSymbol
- getCompoundLists :: Env -> Set [Id]
class info
store the raw kind and all superclasses of a class identifier
Constructors
ClassInfo | |
Fields
|
type info
data type generatedness indicator
an analysed alternative with a list of (product) types
Constructors
Construct (Maybe Id) [Type] Partiality [[Selector]] |
an analysed component
Constructors
Select (Maybe Id) Type Partiality |
data entries are produced from possibly mutual recursive data types. The top-level identifiers of these types are never renamed but there renaming is stored in the identifier map. This identifier map must never be empty (even without renamings) because (the domain of) this map is used to store the other (recursively dependent) top-level identifiers.
possible definitions for type identifiers
Constructors
NoTypeDefn | |
PreDatatype | |
DatatypeDefn DataEntry | |
AliasTypeDefn Type |
for type identifiers also store the raw kind, instances and supertypes
Constructors
TypeInfo | |
Fields
|
starTypeInfo :: TypeInfo Source #
the minimal information for a sort
mapType :: IdMap -> Type -> Type Source #
rename the type according to identifier map (for comorphisms)
sentences
data types are also special sentences because of their properties
Constructors
Formula Term | |
DatatypeSen [DataEntry] | |
ProgEqSen Id TypeScheme ProgEq |
Instances
variables
data TypeVarDefn Source #
type variable are kept separately
Constructors
TypeVarDefn Variance VarKind RawKind Int |
Instances
Data TypeVarDefn Source # | |
Show TypeVarDefn Source # | |
type LocalTypeVars = Map Id TypeVarDefn Source #
mapping type variables to their definition
the type of a local variable
assumptions
data ConstrInfo Source #
name and scheme of a constructor
Constructors
ConstrInfo | |
Fields
|
Instances
Eq ConstrInfo Source # | |
Data ConstrInfo Source # | |
Ord ConstrInfo Source # | |
Show ConstrInfo Source # | |
possible definitions of functions
Constructors
NoOpDefn OpBrand | |
ConstructData Id | target type |
SelectData (Set ConstrInfo) Id | constructors of source type |
Definition OpBrand Term |
scheme, attributes and definition for function identifiers
isConstructor :: OpInfo -> Bool Source #
test for constructor
the local environment and final signature
the signature is established by the classes, types and assumptions
Constructors
Env | |
Instances
initialEnv :: Env Source #
the empty environment (fresh variables start with 1)
accessing the environment
fromResult :: (Env -> Result a) -> State Env (Maybe a) Source #
converting a result to a state computation
putLocalTypeVars :: LocalTypeVars -> State Env () Source #
store local type variables
morphisms
type FunMap = Map (Id, TypeScheme) (Id, TypeScheme) Source #
keep types and class disjoint and use a single identifier map for both
Constructors
Morphism | |
Instances
symbol stuff
data SymbolType Source #
the type or kind of an identifier
Constructors
OpAsItemType TypeScheme | |
TypeAsItemType RawKind | |
ClassAsItemType RawKind | |
SuperClassSymbol Kind | |
TypeKindInstance Kind | |
SuperTypeSymbol Id | |
TypeAliasSymbol Type | |
PredAsItemType TypeScheme |
Instances
Eq SymbolType Source # | |
Data SymbolType Source # | |
Ord SymbolType Source # | |
Show SymbolType Source # | |
symbols with their type
Constructors
Symbol | |
Fields
|
Instances
idToOpSymbol :: Id -> TypeScheme -> Symbol Source #
create an operation symbol
raw symbols where the type of a qualified raw symbol can be a type scheme and also be a kind if the symbol kind is unknown.
Instances
type RawSymbolMap = Map RawSymbol RawSymbol Source #
mapping raw symbols to raw symbols
rawSymName :: RawSymbol -> Id Source #
extract the top identifer from a raw symbol
symbTypeToKind :: SymbolType -> SymbKind Source #
convert a symbol type to a symbol kind
symbKindToRaw :: SymbKind -> Id -> RawSymbol Source #
create a raw symbol from a symbol kind and an identifier
getCompoundLists :: Env -> Set [Id] Source #