| 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-Inferred |
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
- 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
data ClassInfo
store the raw kind and all superclasses of a class identifier
type info
data GenKind
data type generatedness indicator
data AltDefn
an analysed alternative with a list of (product) types
data DataEntry
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.
data TypeDefn
possible definitions for type identifiers
Constructors
| NoTypeDefn | |
| PreDatatype | |
| DatatypeDefn DataEntry | |
| AliasTypeDefn Type |
data TypeInfo
for type identifiers also store the raw kind, instances and supertypes
the minimal information for a sort
sentences
data Sentence
data types are also special sentences because of their properties
Constructors
| Formula Term | |
| DatatypeSen [DataEntry] | |
| ProgEqSen Id TypeScheme ProgEq |
Instances
variables
data TypeVarDefn
type variable are kept separately
Constructors
| TypeVarDefn Variance VarKind RawKind Int |
type LocalTypeVars = Map Id TypeVarDefn
mapping type variables to their definition
data VarDefn
the type of a local variable
assumptions
data ConstrInfo
name and scheme of a constructor
Constructors
| ConstrInfo | |
Fields
| |
data OpDefn
possible definitions of functions
Constructors
| NoOpDefn OpBrand | |
| ConstructData Id | target type |
| SelectData (Set ConstrInfo) Id | constructors of source type |
| Definition OpBrand Term |
data OpInfo
scheme, attributes and definition for function identifiers
isConstructor :: OpInfo -> Bool
test for constructor
the local environment and final signature
data Env
the signature is established by the classes, types and assumptions
Constructors
| Env | |
Instances
initialEnv :: Env
the empty environment (fresh variables start with 1)
data Constrain
accessing the environment
appendSentences :: [Named Sentence] -> State Env ()
add sentences
putClassMap :: ClassMap -> State Env ()
store a class map
putLocalTypeVars :: LocalTypeVars -> State Env ()
store local type variables
putTypeMap :: TypeMap -> State Env ()
store a complete type map
putAssumps :: Assumps -> State Env ()
store assumptions
checkUniqueVars :: [VarDecl] -> State Env ()
check uniqueness of variables
morphisms
type FunMap = Map (Id, TypeScheme) (Id, TypeScheme)
data Morphism
keep types and class disjoint and use a single identifier map for both
Constructors
| Morphism | |
Instances
mkMorphism :: Env -> Env -> Morphism
construct morphism for subsignatures
symbol stuff
data SymbolType
the type or kind of an identifier
data Symbol
symbols with their type
Constructors
| Symbol | |
Fields
| |
Instances
idToTypeSymbol :: Id -> RawKind -> Symbol
create a type symbol
idToClassSymbol :: Id -> RawKind -> Symbol
create a class symbol
idToOpSymbol :: Id -> TypeScheme -> Symbol
create an operation symbol
data RawSymbol
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
mapping raw symbols to raw symbols
rawSymName :: RawSymbol -> Id
extract the top identifer from a raw symbol
symbTypeToKind :: SymbolType -> SymbKind
convert a symbol type to a symbol kind
symbolToRaw :: Symbol -> RawSymbol
wrap a symbol as raw symbol (is ASymbol)
symbKindToRaw :: SymbKind -> Id -> RawSymbol
create a raw symbol from a symbol kind and an identifier
getCompoundLists :: Env -> Set [Id]