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

class info
type info
sentences
variables
assumptions
the local environment and final signature
accessing the environment
morphisms
symbol stuff

Description

abstract syntax during static analysis

Synopsis

data ClassInfo = ClassInfo {
- rawKind :: RawKind
- classKinds :: Set Kind
}
type ClassMap = Map Id ClassInfo
data GenKind
- = Free
- | Generated
- | Loose
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
- = NoTypeDefn
- | PreDatatype
- | DatatypeDefn DataEntry
- | AliasTypeDefn Type
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
- = Formula Term
- | DatatypeSen [DataEntry]
- | ProgEqSen Id TypeScheme ProgEq
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 {
- opType :: TypeScheme
- opAttrs :: Set OpAttr
- opDefn :: OpDefn
}
isConstructor :: OpInfo -> Bool
type Assumps = Map Id (Set OpInfo)
data Env = Env {
- classMap :: ClassMap
- typeMap :: TypeMap
- localTypeVars :: LocalTypeVars
- assumps :: Assumps
- binders :: Map Id Id
- localVars :: Map Id VarDefn
- sentences :: [Named Sentence]
- declSymbs :: Set Symbol
- envDiags :: [Diagnosis]
- preIds :: (PrecMap, Set Id)
- globAnnos :: GlobalAnnos
- counter :: Int
}
initialEnv :: Env
data Constrain
- = Kinding Type Kind
- | Subtyping Type Type
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 {
- msource :: Env
- mtarget :: Env
- typeIdMap :: IdMap
- classIdMap :: IdMap
- funMap :: FunMap
}
mkMorphism :: Env -> Env -> Morphism
isInclMor :: Morphism -> Bool
data SymbolType
- = OpAsItemType TypeScheme
- | TypeAsItemType RawKind
- | ClassAsItemType RawKind
- | SuperClassSymbol Kind
- | TypeKindInstance Kind
- | SuperTypeSymbol Id
- | TypeAliasSymbol Type
- | PredAsItemType TypeScheme
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
- = AnID Id
- | AKindedId SymbKind Id
- | ASymbol Symbol
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 Source #

store the raw kind and all superclasses of a class identifier

Constructors

ClassInfo
Fields rawKind :: RawKind classKinds :: Set Kind

Instances

Instances details

Eq ClassInfo Source #
Instance details Defined in HasCASL.Le Methods (==) :: ClassInfo -> ClassInfo -> Bool (/=) :: ClassInfo -> ClassInfo -> Bool
Data ClassInfo Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ClassInfo -> c ClassInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ClassInfo toConstr :: ClassInfo -> Constr dataTypeOf :: ClassInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ClassInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ClassInfo) gmapT :: (forall b. Data b => b -> b) -> ClassInfo -> ClassInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ClassInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ClassInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ClassInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ClassInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ClassInfo -> m ClassInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassInfo -> m ClassInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ClassInfo -> m ClassInfo
Ord ClassInfo Source #
Instance details Defined in HasCASL.Le Methods compare :: ClassInfo -> ClassInfo -> Ordering (<) :: ClassInfo -> ClassInfo -> Bool (<=) :: ClassInfo -> ClassInfo -> Bool (>) :: ClassInfo -> ClassInfo -> Bool (>=) :: ClassInfo -> ClassInfo -> Bool max :: ClassInfo -> ClassInfo -> ClassInfo min :: ClassInfo -> ClassInfo -> ClassInfo
Show ClassInfo Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> ClassInfo -> ShowS show :: ClassInfo -> String showList :: [ClassInfo] -> ShowS
Generic ClassInfo
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep ClassInfo :: Type -> Type Methods from :: ClassInfo -> Rep ClassInfo x to :: Rep ClassInfo x -> ClassInfo
FromJSON ClassInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser ClassInfo parseJSONList :: Value -> Parser [ClassInfo]
ToJSON ClassInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: ClassInfo -> Value toEncoding :: ClassInfo -> Encoding toJSONList :: [ClassInfo] -> Value toEncodingList :: [ClassInfo] -> Encoding
ShATermConvertible ClassInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> ClassInfo -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ClassInfo] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ClassInfo) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ClassInfo])
Pretty ClassInfo Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: ClassInfo -> Doc Source # pretties :: [ClassInfo] -> Doc Source #
type Rep ClassInfo
Instance details Defined in HasCASL.ATC_HasCASL type Rep ClassInfo = D1 ('MetaData "ClassInfo" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "ClassInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "rawKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawKind) :*: S1 ('MetaSel ('Just "classKinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Kind))))

type ClassMap = Map Id ClassInfo Source #

mapping class identifiers to their definition

type info

data GenKind Source #

data type generatedness indicator

Constructors

Free
Generated
Loose

Instances

Instances details

Eq GenKind Source #
Instance details Defined in HasCASL.Le Methods (==) :: GenKind -> GenKind -> Bool (/=) :: GenKind -> GenKind -> Bool
Data GenKind Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> GenKind -> c GenKind gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c GenKind toConstr :: GenKind -> Constr dataTypeOf :: GenKind -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c GenKind) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c GenKind) gmapT :: (forall b. Data b => b -> b) -> GenKind -> GenKind gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> GenKind -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> GenKind -> r gmapQ :: (forall d. Data d => d -> u) -> GenKind -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> GenKind -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> GenKind -> m GenKind gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> GenKind -> m GenKind gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> GenKind -> m GenKind
Ord GenKind Source #
Instance details Defined in HasCASL.Le Methods compare :: GenKind -> GenKind -> Ordering (<) :: GenKind -> GenKind -> Bool (<=) :: GenKind -> GenKind -> Bool (>) :: GenKind -> GenKind -> Bool (>=) :: GenKind -> GenKind -> Bool max :: GenKind -> GenKind -> GenKind min :: GenKind -> GenKind -> GenKind
Show GenKind Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> GenKind -> ShowS show :: GenKind -> String showList :: [GenKind] -> ShowS
Generic GenKind
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep GenKind :: Type -> Type Methods from :: GenKind -> Rep GenKind x to :: Rep GenKind x -> GenKind
FromJSON GenKind
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser GenKind parseJSONList :: Value -> Parser [GenKind]
ToJSON GenKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: GenKind -> Value toEncoding :: GenKind -> Encoding toJSONList :: [GenKind] -> Value toEncodingList :: [GenKind] -> Encoding
ShATermConvertible GenKind
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> GenKind -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [GenKind] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, GenKind) fromShATermList' :: Int -> ATermTable -> (ATermTable, [GenKind])
type Rep GenKind
Instance details Defined in HasCASL.ATC_HasCASL type Rep GenKind = D1 ('MetaData "GenKind" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "Free" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Generated" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Loose" 'PrefixI 'False) (U1 :: Type -> Type)))

data AltDefn Source #

an analysed alternative with a list of (product) types

Constructors

Construct (Maybe Id) [Type] Partiality [[Selector]]

Instances

Instances details

Eq AltDefn Source #
Instance details Defined in HasCASL.Le Methods (==) :: AltDefn -> AltDefn -> Bool (/=) :: AltDefn -> AltDefn -> Bool
Data AltDefn Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AltDefn -> c AltDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c AltDefn toConstr :: AltDefn -> Constr dataTypeOf :: AltDefn -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c AltDefn) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c AltDefn) gmapT :: (forall b. Data b => b -> b) -> AltDefn -> AltDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AltDefn -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AltDefn -> r gmapQ :: (forall d. Data d => d -> u) -> AltDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> AltDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AltDefn -> m AltDefn
Ord AltDefn Source #
Instance details Defined in HasCASL.Le Methods compare :: AltDefn -> AltDefn -> Ordering (<) :: AltDefn -> AltDefn -> Bool (<=) :: AltDefn -> AltDefn -> Bool (>) :: AltDefn -> AltDefn -> Bool (>=) :: AltDefn -> AltDefn -> Bool max :: AltDefn -> AltDefn -> AltDefn min :: AltDefn -> AltDefn -> AltDefn
Show AltDefn Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> AltDefn -> ShowS show :: AltDefn -> String showList :: [AltDefn] -> ShowS
Generic AltDefn
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep AltDefn :: Type -> Type Methods from :: AltDefn -> Rep AltDefn x to :: Rep AltDefn x -> AltDefn
FromJSON AltDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser AltDefn parseJSONList :: Value -> Parser [AltDefn]
ToJSON AltDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: AltDefn -> Value toEncoding :: AltDefn -> Encoding toJSONList :: [AltDefn] -> Value toEncodingList :: [AltDefn] -> Encoding
ShATermConvertible AltDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> AltDefn -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [AltDefn] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, AltDefn) fromShATermList' :: Int -> ATermTable -> (ATermTable, [AltDefn])
type Rep AltDefn
Instance details Defined in HasCASL.ATC_HasCASL type Rep AltDefn = D1 ('MetaData "AltDefn" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "Construct" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Id)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type])) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Partiality) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [[Selector]]))))

data Selector Source #

an analysed component

Constructors

Select (Maybe Id) Type Partiality

Instances

Instances details

Eq Selector Source #
Instance details Defined in HasCASL.Le Methods (==) :: Selector -> Selector -> Bool (/=) :: Selector -> Selector -> Bool
Data Selector Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Selector -> c Selector gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Selector toConstr :: Selector -> Constr dataTypeOf :: Selector -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Selector) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Selector) gmapT :: (forall b. Data b => b -> b) -> Selector -> Selector gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Selector -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Selector -> r gmapQ :: (forall d. Data d => d -> u) -> Selector -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Selector -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Selector -> m Selector gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Selector -> m Selector gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Selector -> m Selector
Ord Selector Source #
Instance details Defined in HasCASL.Le Methods compare :: Selector -> Selector -> Ordering (<) :: Selector -> Selector -> Bool (<=) :: Selector -> Selector -> Bool (>) :: Selector -> Selector -> Bool (>=) :: Selector -> Selector -> Bool max :: Selector -> Selector -> Selector min :: Selector -> Selector -> Selector
Show Selector Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> Selector -> ShowS show :: Selector -> String showList :: [Selector] -> ShowS
Generic Selector
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Selector :: Type -> Type Methods from :: Selector -> Rep Selector x to :: Rep Selector x -> Selector
FromJSON Selector
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Selector parseJSONList :: Value -> Parser [Selector]
ToJSON Selector
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Selector -> Value toEncoding :: Selector -> Encoding toJSONList :: [Selector] -> Value toEncodingList :: [Selector] -> Encoding
ShATermConvertible Selector
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Selector -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Selector] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Selector) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Selector])
Pretty Selector Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: Selector -> Doc Source # pretties :: [Selector] -> Doc Source #
type Rep Selector
Instance details Defined in HasCASL.ATC_HasCASL type Rep Selector = D1 ('MetaData "Selector" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "Select" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Id)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Partiality))))

type IdMap = Map Id Id Source #

a mapping of type (and disjoint class) identifiers

data DataEntry Source #

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.

Constructors

DataEntry IdMap Id GenKind [TypeArg] RawKind (Set AltDefn)

Instances

Instances details

Eq DataEntry Source #
Instance details Defined in HasCASL.Le Methods (==) :: DataEntry -> DataEntry -> Bool (/=) :: DataEntry -> DataEntry -> Bool
Data DataEntry Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DataEntry -> c DataEntry gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DataEntry toConstr :: DataEntry -> Constr dataTypeOf :: DataEntry -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DataEntry) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DataEntry) gmapT :: (forall b. Data b => b -> b) -> DataEntry -> DataEntry gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DataEntry -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DataEntry -> r gmapQ :: (forall d. Data d => d -> u) -> DataEntry -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> DataEntry -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DataEntry -> m DataEntry
Ord DataEntry Source #
Instance details Defined in HasCASL.Le Methods compare :: DataEntry -> DataEntry -> Ordering (<) :: DataEntry -> DataEntry -> Bool (<=) :: DataEntry -> DataEntry -> Bool (>) :: DataEntry -> DataEntry -> Bool (>=) :: DataEntry -> DataEntry -> Bool max :: DataEntry -> DataEntry -> DataEntry min :: DataEntry -> DataEntry -> DataEntry
Show DataEntry Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> DataEntry -> ShowS show :: DataEntry -> String showList :: [DataEntry] -> ShowS
Generic DataEntry
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep DataEntry :: Type -> Type Methods from :: DataEntry -> Rep DataEntry x to :: Rep DataEntry x -> DataEntry
FromJSON DataEntry
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser DataEntry parseJSONList :: Value -> Parser [DataEntry]
ToJSON DataEntry
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: DataEntry -> Value toEncoding :: DataEntry -> Encoding toJSONList :: [DataEntry] -> Value toEncodingList :: [DataEntry] -> Encoding
ShATermConvertible DataEntry
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> DataEntry -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [DataEntry] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, DataEntry) fromShATermList' :: Int -> ATermTable -> (ATermTable, [DataEntry])
Pretty DataEntry Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: DataEntry -> Doc Source # pretties :: [DataEntry] -> Doc Source #
type Rep DataEntry
Instance details Defined in HasCASL.ATC_HasCASL type Rep DataEntry = D1 ('MetaData "DataEntry" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "DataEntry" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IdMap) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GenKind))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TypeArg]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set AltDefn))))))

data TypeDefn Source #

possible definitions for type identifiers

Constructors

NoTypeDefn
PreDatatype
DatatypeDefn DataEntry
AliasTypeDefn Type

Instances

Instances details

Eq TypeDefn Source #
Instance details Defined in HasCASL.Le Methods (==) :: TypeDefn -> TypeDefn -> Bool (/=) :: TypeDefn -> TypeDefn -> Bool
Data TypeDefn Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeDefn -> c TypeDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeDefn toConstr :: TypeDefn -> Constr dataTypeOf :: TypeDefn -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeDefn) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeDefn) gmapT :: (forall b. Data b => b -> b) -> TypeDefn -> TypeDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeDefn -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeDefn -> r gmapQ :: (forall d. Data d => d -> u) -> TypeDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeDefn -> m TypeDefn
Ord TypeDefn Source #
Instance details Defined in HasCASL.Le Methods compare :: TypeDefn -> TypeDefn -> Ordering (<) :: TypeDefn -> TypeDefn -> Bool (<=) :: TypeDefn -> TypeDefn -> Bool (>) :: TypeDefn -> TypeDefn -> Bool (>=) :: TypeDefn -> TypeDefn -> Bool max :: TypeDefn -> TypeDefn -> TypeDefn min :: TypeDefn -> TypeDefn -> TypeDefn
Show TypeDefn Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> TypeDefn -> ShowS show :: TypeDefn -> String showList :: [TypeDefn] -> ShowS
Generic TypeDefn
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep TypeDefn :: Type -> Type Methods from :: TypeDefn -> Rep TypeDefn x to :: Rep TypeDefn x -> TypeDefn
FromJSON TypeDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser TypeDefn parseJSONList :: Value -> Parser [TypeDefn]
ToJSON TypeDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: TypeDefn -> Value toEncoding :: TypeDefn -> Encoding toJSONList :: [TypeDefn] -> Value toEncodingList :: [TypeDefn] -> Encoding
ShATermConvertible TypeDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> TypeDefn -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TypeDefn] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeDefn) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TypeDefn])
Pretty TypeDefn Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: TypeDefn -> Doc Source # pretties :: [TypeDefn] -> Doc Source #
type Rep TypeDefn
Instance details Defined in HasCASL.ATC_HasCASL type Rep TypeDefn = D1 ('MetaData "TypeDefn" "HasCASL.Le" "main" 'False) ((C1 ('MetaCons "NoTypeDefn" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PreDatatype" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DatatypeDefn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DataEntry)) :+: C1 ('MetaCons "AliasTypeDefn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type))))

data TypeInfo Source #

for type identifiers also store the raw kind, instances and supertypes

Constructors

TypeInfo
Fields typeKind :: RawKind otherTypeKinds :: Set Kind superTypes :: Set Id typeDefn :: TypeDefn

Instances

Instances details

Eq TypeInfo Source #
Instance details Defined in HasCASL.Le Methods (==) :: TypeInfo -> TypeInfo -> Bool (/=) :: TypeInfo -> TypeInfo -> Bool
Data TypeInfo Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeInfo -> c TypeInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeInfo toConstr :: TypeInfo -> Constr dataTypeOf :: TypeInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeInfo) gmapT :: (forall b. Data b => b -> b) -> TypeInfo -> TypeInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeInfo -> r gmapQ :: (forall d. Data d => d -> u) -> TypeInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeInfo -> m TypeInfo
Ord TypeInfo Source #
Instance details Defined in HasCASL.Le Methods compare :: TypeInfo -> TypeInfo -> Ordering (<) :: TypeInfo -> TypeInfo -> Bool (<=) :: TypeInfo -> TypeInfo -> Bool (>) :: TypeInfo -> TypeInfo -> Bool (>=) :: TypeInfo -> TypeInfo -> Bool max :: TypeInfo -> TypeInfo -> TypeInfo min :: TypeInfo -> TypeInfo -> TypeInfo
Show TypeInfo Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> TypeInfo -> ShowS show :: TypeInfo -> String showList :: [TypeInfo] -> ShowS
Generic TypeInfo
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep TypeInfo :: Type -> Type Methods from :: TypeInfo -> Rep TypeInfo x to :: Rep TypeInfo x -> TypeInfo
FromJSON TypeInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser TypeInfo parseJSONList :: Value -> Parser [TypeInfo]
ToJSON TypeInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: TypeInfo -> Value toEncoding :: TypeInfo -> Encoding toJSONList :: [TypeInfo] -> Value toEncodingList :: [TypeInfo] -> Encoding
ShATermConvertible TypeInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> TypeInfo -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TypeInfo] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeInfo) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TypeInfo])
Pretty TypeInfo Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: TypeInfo -> Doc Source # pretties :: [TypeInfo] -> Doc Source #
type Rep TypeInfo
Instance details Defined in HasCASL.ATC_HasCASL type Rep TypeInfo = D1 ('MetaData "TypeInfo" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "TypeInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "typeKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawKind) :: S1 ('MetaSel ('Just "otherTypeKinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Kind))) :: (S1 ('MetaSel ('Just "superTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Id)) :*: S1 ('MetaSel ('Just "typeDefn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeDefn))))

type TypeMap = Map Id TypeInfo Source #

mapping type identifiers to their definition

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 Sentence Source #

data types are also special sentences because of their properties

Constructors

Formula Term
DatatypeSen [DataEntry]
ProgEqSen Id TypeScheme ProgEq

Instances

Instances details

Eq Sentence Source #
Instance details Defined in HasCASL.Le Methods (==) :: Sentence -> Sentence -> Bool (/=) :: Sentence -> Sentence -> Bool
Data Sentence Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sentence -> c Sentence gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sentence toConstr :: Sentence -> Constr dataTypeOf :: Sentence -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sentence) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sentence) gmapT :: (forall b. Data b => b -> b) -> Sentence -> Sentence gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sentence -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sentence -> r gmapQ :: (forall d. Data d => d -> u) -> Sentence -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sentence -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sentence -> m Sentence
Ord Sentence Source #
Instance details Defined in HasCASL.Le Methods compare :: Sentence -> Sentence -> Ordering (<) :: Sentence -> Sentence -> Bool (<=) :: Sentence -> Sentence -> Bool (>) :: Sentence -> Sentence -> Bool (>=) :: Sentence -> Sentence -> Bool max :: Sentence -> Sentence -> Sentence min :: Sentence -> Sentence -> Sentence
Show Sentence Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> Sentence -> ShowS show :: Sentence -> String showList :: [Sentence] -> ShowS
Generic Sentence
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Sentence :: Type -> Type Methods from :: Sentence -> Rep Sentence x to :: Rep Sentence x -> Sentence
GetRange Sentence Source #
Instance details Defined in HasCASL.Le Methods getRange :: Sentence -> Range Source # rangeSpan :: Sentence -> [Pos] Source #
FromJSON Sentence
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Sentence parseJSONList :: Value -> Parser [Sentence]
ToJSON Sentence
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Sentence -> Value toEncoding :: Sentence -> Encoding toJSONList :: [Sentence] -> Value toEncodingList :: [Sentence] -> Encoding
ShATermConvertible Sentence
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Sentence -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sentence] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sentence) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sentence])
Pretty Sentence Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: Sentence -> Doc Source # pretties :: [Sentence] -> Doc Source #
MinSublogic Sublogic Sentence Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: Sentence -> Sublogic Source #
Sentences HasCASL Sentence Env Morphism Symbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: HasCASL -> Env -> Sentence -> Sentence Source # negation :: HasCASL -> Sentence -> Maybe Sentence Source # print_sign :: HasCASL -> Env -> Doc Source # print_named :: HasCASL -> Named Sentence -> Doc Source # sym_of :: HasCASL -> Env -> [Set Symbol] Source # mostSymsOf :: HasCASL -> Env -> [Symbol] Source # symmap_of :: HasCASL -> Morphism -> EndoMap Symbol Source # sym_name :: HasCASL -> Symbol -> Id Source # sym_label :: HasCASL -> Symbol -> Maybe String Source # fullSymName :: HasCASL -> Symbol -> String Source # symKind :: HasCASL -> Symbol -> String Source # symsOfSen :: HasCASL -> Env -> Sentence -> [Symbol] Source # pair_symbols :: HasCASL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source # addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
type Rep Sentence
Instance details Defined in HasCASL.ATC_HasCASL type Rep Sentence = D1 ('MetaData "Sentence" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "Formula" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: (C1 ('MetaCons "DatatypeSen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DataEntry])) :+: C1 ('MetaCons "ProgEqSen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProgEq)))))

variables

data TypeVarDefn Source #

type variable are kept separately

Constructors

TypeVarDefn Variance VarKind RawKind Int

Instances

Instances details

Data TypeVarDefn Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypeVarDefn -> c TypeVarDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TypeVarDefn toConstr :: TypeVarDefn -> Constr dataTypeOf :: TypeVarDefn -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TypeVarDefn) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TypeVarDefn) gmapT :: (forall b. Data b => b -> b) -> TypeVarDefn -> TypeVarDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypeVarDefn -> r gmapQ :: (forall d. Data d => d -> u) -> TypeVarDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TypeVarDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypeVarDefn -> m TypeVarDefn
Show TypeVarDefn Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> TypeVarDefn -> ShowS show :: TypeVarDefn -> String showList :: [TypeVarDefn] -> ShowS
Generic TypeVarDefn
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep TypeVarDefn :: Type -> Type Methods from :: TypeVarDefn -> Rep TypeVarDefn x to :: Rep TypeVarDefn x -> TypeVarDefn
FromJSON TypeVarDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser TypeVarDefn parseJSONList :: Value -> Parser [TypeVarDefn]
ToJSON TypeVarDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: TypeVarDefn -> Value toEncoding :: TypeVarDefn -> Encoding toJSONList :: [TypeVarDefn] -> Value toEncodingList :: [TypeVarDefn] -> Encoding
ShATermConvertible TypeVarDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> TypeVarDefn -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TypeVarDefn] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TypeVarDefn) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TypeVarDefn])
Pretty TypeVarDefn Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: TypeVarDefn -> Doc Source # pretties :: [TypeVarDefn] -> Doc Source #
type Rep TypeVarDefn
Instance details Defined in HasCASL.ATC_HasCASL type Rep TypeVarDefn = D1 ('MetaData "TypeVarDefn" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "TypeVarDefn" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Variance) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VarKind)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawKind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))

type LocalTypeVars = Map Id TypeVarDefn Source #

mapping type variables to their definition

data VarDefn Source #

the type of a local variable

Constructors

VarDefn Type

Instances

Instances details

Data VarDefn Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarDefn -> c VarDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarDefn toConstr :: VarDefn -> Constr dataTypeOf :: VarDefn -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VarDefn) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarDefn) gmapT :: (forall b. Data b => b -> b) -> VarDefn -> VarDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarDefn -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarDefn -> r gmapQ :: (forall d. Data d => d -> u) -> VarDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> VarDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarDefn -> m VarDefn
Show VarDefn Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> VarDefn -> ShowS show :: VarDefn -> String showList :: [VarDefn] -> ShowS
Generic VarDefn
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep VarDefn :: Type -> Type Methods from :: VarDefn -> Rep VarDefn x to :: Rep VarDefn x -> VarDefn
FromJSON VarDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser VarDefn parseJSONList :: Value -> Parser [VarDefn]
ToJSON VarDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: VarDefn -> Value toEncoding :: VarDefn -> Encoding toJSONList :: [VarDefn] -> Value toEncodingList :: [VarDefn] -> Encoding
ShATermConvertible VarDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> VarDefn -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [VarDefn] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, VarDefn) fromShATermList' :: Int -> ATermTable -> (ATermTable, [VarDefn])
Pretty VarDefn Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: VarDefn -> Doc Source # pretties :: [VarDefn] -> Doc Source #
type Rep VarDefn
Instance details Defined in HasCASL.ATC_HasCASL type Rep VarDefn = D1 ('MetaData "VarDefn" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "VarDefn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))

assumptions

data ConstrInfo Source #

name and scheme of a constructor

Constructors

ConstrInfo
Fields constrId :: Id constrType :: TypeScheme

Instances

Instances details

Eq ConstrInfo Source #
Instance details Defined in HasCASL.Le Methods (==) :: ConstrInfo -> ConstrInfo -> Bool (/=) :: ConstrInfo -> ConstrInfo -> Bool
Data ConstrInfo Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ConstrInfo -> c ConstrInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ConstrInfo toConstr :: ConstrInfo -> Constr dataTypeOf :: ConstrInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ConstrInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ConstrInfo) gmapT :: (forall b. Data b => b -> b) -> ConstrInfo -> ConstrInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ConstrInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ConstrInfo -> r gmapQ :: (forall d. Data d => d -> u) -> ConstrInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ConstrInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ConstrInfo -> m ConstrInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstrInfo -> m ConstrInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ConstrInfo -> m ConstrInfo
Ord ConstrInfo Source #
Instance details Defined in HasCASL.Le Methods compare :: ConstrInfo -> ConstrInfo -> Ordering (<) :: ConstrInfo -> ConstrInfo -> Bool (<=) :: ConstrInfo -> ConstrInfo -> Bool (>) :: ConstrInfo -> ConstrInfo -> Bool (>=) :: ConstrInfo -> ConstrInfo -> Bool max :: ConstrInfo -> ConstrInfo -> ConstrInfo min :: ConstrInfo -> ConstrInfo -> ConstrInfo
Show ConstrInfo Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> ConstrInfo -> ShowS show :: ConstrInfo -> String showList :: [ConstrInfo] -> ShowS
Generic ConstrInfo
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep ConstrInfo :: Type -> Type Methods from :: ConstrInfo -> Rep ConstrInfo x to :: Rep ConstrInfo x -> ConstrInfo
FromJSON ConstrInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser ConstrInfo parseJSONList :: Value -> Parser [ConstrInfo]
ToJSON ConstrInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: ConstrInfo -> Value toEncoding :: ConstrInfo -> Encoding toJSONList :: [ConstrInfo] -> Value toEncodingList :: [ConstrInfo] -> Encoding
ShATermConvertible ConstrInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> ConstrInfo -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ConstrInfo] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ConstrInfo) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ConstrInfo])
Pretty ConstrInfo Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: ConstrInfo -> Doc Source # pretties :: [ConstrInfo] -> Doc Source #
type Rep ConstrInfo
Instance details Defined in HasCASL.ATC_HasCASL type Rep ConstrInfo = D1 ('MetaData "ConstrInfo" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "ConstrInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "constrId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: S1 ('MetaSel ('Just "constrType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme)))

data OpDefn Source #

possible definitions of functions

Constructors

NoOpDefn OpBrand
ConstructData Id	target type
SelectData (Set ConstrInfo) Id	constructors of source type
Definition OpBrand Term

Instances

Instances details

Eq OpDefn Source #
Instance details Defined in HasCASL.Le Methods (==) :: OpDefn -> OpDefn -> Bool (/=) :: OpDefn -> OpDefn -> Bool
Data OpDefn Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpDefn -> c OpDefn gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpDefn toConstr :: OpDefn -> Constr dataTypeOf :: OpDefn -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpDefn) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpDefn) gmapT :: (forall b. Data b => b -> b) -> OpDefn -> OpDefn gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpDefn -> r gmapQ :: (forall d. Data d => d -> u) -> OpDefn -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpDefn -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpDefn -> m OpDefn
Ord OpDefn Source #
Instance details Defined in HasCASL.Le Methods compare :: OpDefn -> OpDefn -> Ordering (<) :: OpDefn -> OpDefn -> Bool (<=) :: OpDefn -> OpDefn -> Bool (>) :: OpDefn -> OpDefn -> Bool (>=) :: OpDefn -> OpDefn -> Bool max :: OpDefn -> OpDefn -> OpDefn min :: OpDefn -> OpDefn -> OpDefn
Show OpDefn Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> OpDefn -> ShowS show :: OpDefn -> String showList :: [OpDefn] -> ShowS
Generic OpDefn
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep OpDefn :: Type -> Type Methods from :: OpDefn -> Rep OpDefn x to :: Rep OpDefn x -> OpDefn
FromJSON OpDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser OpDefn parseJSONList :: Value -> Parser [OpDefn]
ToJSON OpDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: OpDefn -> Value toEncoding :: OpDefn -> Encoding toJSONList :: [OpDefn] -> Value toEncodingList :: [OpDefn] -> Encoding
ShATermConvertible OpDefn
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> OpDefn -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OpDefn] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OpDefn) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OpDefn])
Pretty OpDefn Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: OpDefn -> Doc Source # pretties :: [OpDefn] -> Doc Source #
type Rep OpDefn
Instance details Defined in HasCASL.ATC_HasCASL type Rep OpDefn = D1 ('MetaData "OpDefn" "HasCASL.Le" "main" 'False) ((C1 ('MetaCons "NoOpDefn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpBrand)) :+: C1 ('MetaCons "ConstructData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id))) :+: (C1 ('MetaCons "SelectData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set ConstrInfo)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id)) :+: C1 ('MetaCons "Definition" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpBrand) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))))

data OpInfo Source #

scheme, attributes and definition for function identifiers

Constructors

OpInfo
Fields opType :: TypeScheme opAttrs :: Set OpAttr opDefn :: OpDefn

Instances

Instances details

Eq OpInfo Source #
Instance details Defined in HasCASL.Le Methods (==) :: OpInfo -> OpInfo -> Bool (/=) :: OpInfo -> OpInfo -> Bool
Data OpInfo Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpInfo -> c OpInfo gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpInfo toConstr :: OpInfo -> Constr dataTypeOf :: OpInfo -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpInfo) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpInfo) gmapT :: (forall b. Data b => b -> b) -> OpInfo -> OpInfo gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpInfo -> r gmapQ :: (forall d. Data d => d -> u) -> OpInfo -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpInfo -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpInfo -> m OpInfo
Ord OpInfo Source #
Instance details Defined in HasCASL.Le Methods compare :: OpInfo -> OpInfo -> Ordering (<) :: OpInfo -> OpInfo -> Bool (<=) :: OpInfo -> OpInfo -> Bool (>) :: OpInfo -> OpInfo -> Bool (>=) :: OpInfo -> OpInfo -> Bool max :: OpInfo -> OpInfo -> OpInfo min :: OpInfo -> OpInfo -> OpInfo
Show OpInfo Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> OpInfo -> ShowS show :: OpInfo -> String showList :: [OpInfo] -> ShowS
Generic OpInfo
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep OpInfo :: Type -> Type Methods from :: OpInfo -> Rep OpInfo x to :: Rep OpInfo x -> OpInfo
FromJSON OpInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser OpInfo parseJSONList :: Value -> Parser [OpInfo]
ToJSON OpInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: OpInfo -> Value toEncoding :: OpInfo -> Encoding toJSONList :: [OpInfo] -> Value toEncodingList :: [OpInfo] -> Encoding
ShATermConvertible OpInfo
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> OpInfo -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OpInfo] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OpInfo) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OpInfo])
Pretty OpInfo Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: OpInfo -> Doc Source # pretties :: [OpInfo] -> Doc Source #
type Rep OpInfo
Instance details Defined in HasCASL.ATC_HasCASL type Rep OpInfo = D1 ('MetaData "OpInfo" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "OpInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "opType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme) :: (S1 ('MetaSel ('Just "opAttrs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OpAttr)) :: S1 ('MetaSel ('Just "opDefn") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 OpDefn))))

isConstructor :: OpInfo -> Bool Source #

test for constructor

type Assumps = Map Id (Set OpInfo) Source #

mapping operation identifiers to their definition

the local environment and final signature

data Env Source #

the signature is established by the classes, types and assumptions

Constructors

Env
Fields classMap :: ClassMap typeMap :: TypeMap localTypeVars :: LocalTypeVars assumps :: Assumps binders :: Map Id Id localVars :: Map Id VarDefn sentences :: [Named Sentence] declSymbs :: Set Symbol envDiags :: [Diagnosis] preIds :: (PrecMap, Set Id) globAnnos :: GlobalAnnos counter :: Int

Instances

Instances details

Eq Env Source #
Instance details Defined in HasCASL.Le Methods (==) :: Env -> Env -> Bool (/=) :: Env -> Env -> Bool
Data Env Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Env -> c Env gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Env toConstr :: Env -> Constr dataTypeOf :: Env -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Env) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Env) gmapT :: (forall b. Data b => b -> b) -> Env -> Env gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Env -> r gmapQ :: (forall d. Data d => d -> u) -> Env -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Env -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Env -> m Env gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Env -> m Env gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Env -> m Env
Ord Env Source #
Instance details Defined in HasCASL.Le Methods compare :: Env -> Env -> Ordering (<) :: Env -> Env -> Bool (<=) :: Env -> Env -> Bool (>) :: Env -> Env -> Bool (>=) :: Env -> Env -> Bool max :: Env -> Env -> Env min :: Env -> Env -> Env
Show Env Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> Env -> ShowS show :: Env -> String showList :: [Env] -> ShowS
Generic Env
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Env :: Type -> Type Methods from :: Env -> Rep Env x to :: Rep Env x -> Env
FromJSON Env
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Env parseJSONList :: Value -> Parser [Env]
ToJSON Env
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Env -> Value toEncoding :: Env -> Encoding toJSONList :: [Env] -> Value toEncodingList :: [Env] -> Encoding
ShATermConvertible Env
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Env -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Env] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Env) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Env])
Pretty Env Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: Env -> Doc Source # pretties :: [Env] -> Doc Source #
ProjectSublogic Sublogic Env Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogic :: Sublogic -> Env -> Env Source #
MinSublogic Sublogic Env Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: Env -> Sublogic Source #
Category Env Morphism Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods ide :: Env -> Morphism Source # composeMorphisms :: Morphism -> Morphism -> Result Morphism Source # dom :: Morphism -> Env Source # cod :: Morphism -> Env Source # inverse :: Morphism -> Result Morphism Source # isInclusion :: Morphism -> Bool Source # legal_mor :: Morphism -> Result () Source #
Sentences HasCASL Sentence Env Morphism Symbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: HasCASL -> Env -> Sentence -> Sentence Source # negation :: HasCASL -> Sentence -> Maybe Sentence Source # print_sign :: HasCASL -> Env -> Doc Source # print_named :: HasCASL -> Named Sentence -> Doc Source # sym_of :: HasCASL -> Env -> [Set Symbol] Source # mostSymsOf :: HasCASL -> Env -> [Symbol] Source # symmap_of :: HasCASL -> Morphism -> EndoMap Symbol Source # sym_name :: HasCASL -> Symbol -> Id Source # sym_label :: HasCASL -> Symbol -> Maybe String Source # fullSymName :: HasCASL -> Symbol -> String Source # symKind :: HasCASL -> Symbol -> String Source # symsOfSen :: HasCASL -> Env -> Sentence -> [Symbol] Source # pair_symbols :: HasCASL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source # addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
type Rep Env
Instance details Defined in HasCASL.ATC_HasCASL type Rep Env = D1 ('MetaData "Env" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "Env" 'PrefixI 'True) (((S1 ('MetaSel ('Just "classMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ClassMap) :: (S1 ('MetaSel ('Just "typeMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeMap) :: S1 ('MetaSel ('Just "localTypeVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 LocalTypeVars))) :: (S1 ('MetaSel ('Just "assumps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assumps) :: (S1 ('MetaSel ('Just "binders") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Id Id)) :: S1 ('MetaSel ('Just "localVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Id VarDefn))))) :: ((S1 ('MetaSel ('Just "sentences") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Named Sentence]) :: (S1 ('MetaSel ('Just "declSymbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Symbol)) :: S1 ('MetaSel ('Just "envDiags") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Diagnosis]))) :: (S1 ('MetaSel ('Just "preIds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (PrecMap, Set Id)) :: (S1 ('MetaSel ('Just "globAnnos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GlobalAnnos) :*: S1 ('MetaSel ('Just "counter") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))))

initialEnv :: Env Source #

the empty environment (fresh variables start with 1)

data Constrain Source #

Constructors

Kinding Type Kind
Subtyping Type Type

Instances

Instances details

Eq Constrain Source #
Instance details Defined in HasCASL.Le Methods (==) :: Constrain -> Constrain -> Bool (/=) :: Constrain -> Constrain -> Bool
Data Constrain Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Constrain -> c Constrain gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Constrain toConstr :: Constrain -> Constr dataTypeOf :: Constrain -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Constrain) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constrain) gmapT :: (forall b. Data b => b -> b) -> Constrain -> Constrain gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Constrain -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Constrain -> r gmapQ :: (forall d. Data d => d -> u) -> Constrain -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Constrain -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Constrain -> m Constrain gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Constrain -> m Constrain gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Constrain -> m Constrain
Ord Constrain Source #
Instance details Defined in HasCASL.Le Methods compare :: Constrain -> Constrain -> Ordering (<) :: Constrain -> Constrain -> Bool (<=) :: Constrain -> Constrain -> Bool (>) :: Constrain -> Constrain -> Bool (>=) :: Constrain -> Constrain -> Bool max :: Constrain -> Constrain -> Constrain min :: Constrain -> Constrain -> Constrain
Show Constrain Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> Constrain -> ShowS show :: Constrain -> String showList :: [Constrain] -> ShowS
Generic Constrain
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Constrain :: Type -> Type Methods from :: Constrain -> Rep Constrain x to :: Rep Constrain x -> Constrain
GetRange Constrain Source #
Instance details Defined in HasCASL.Constrain Methods getRange :: Constrain -> Range Source # rangeSpan :: Constrain -> [Pos] Source #
FromJSON Constrain
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Constrain parseJSONList :: Value -> Parser [Constrain]
ToJSON Constrain
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Constrain -> Value toEncoding :: Constrain -> Encoding toJSONList :: [Constrain] -> Value toEncodingList :: [Constrain] -> Encoding
ShATermConvertible Constrain
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Constrain -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Constrain] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Constrain) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Constrain])
Pretty Constrain Source #
Instance details Defined in HasCASL.Constrain Methods pretty :: Constrain -> Doc Source # pretties :: [Constrain] -> Doc Source #
type Rep Constrain
Instance details Defined in HasCASL.ATC_HasCASL type Rep Constrain = D1 ('MetaData "Constrain" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "Kinding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :+: C1 ('MetaCons "Subtyping" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))

accessing the environment

addDiags :: [Diagnosis] -> State Env () Source #

add diagnostic messages

appendSentences :: [Named Sentence] -> State Env () Source #

add sentences

putClassMap :: ClassMap -> State Env () Source #

store a class map

putLocalVars :: Map Id VarDefn -> State Env () Source #

store local assumptions

fromResult :: (Env -> Result a) -> State Env (Maybe a) Source #

converting a result to a state computation

addSymbol :: Symbol -> State Env () Source #

add the symbol to the state

putLocalTypeVars :: LocalTypeVars -> State Env () Source #

store local type variables

putTypeMap :: TypeMap -> State Env () Source #

store a complete type map

putAssumps :: Assumps -> State Env () Source #

store assumptions

putBinders :: Map Id Id -> State Env () Source #

store assumptions

getVar :: VarDecl -> Id Source #

get the variable

checkUniqueVars :: [VarDecl] -> State Env () Source #

check uniqueness of variables

morphisms

type FunMap = Map (Id, TypeScheme) (Id, TypeScheme) Source #

data Morphism Source #

keep types and class disjoint and use a single identifier map for both

Constructors

Morphism
Fields msource :: Env mtarget :: Env typeIdMap :: IdMap classIdMap :: IdMap funMap :: FunMap

Instances

Instances details

Eq Morphism Source #
Instance details Defined in HasCASL.Le Methods (==) :: Morphism -> Morphism -> Bool (/=) :: Morphism -> Morphism -> Bool
Data Morphism Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Morphism -> c Morphism gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Morphism toConstr :: Morphism -> Constr dataTypeOf :: Morphism -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Morphism) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism) gmapT :: (forall b. Data b => b -> b) -> Morphism -> Morphism gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r gmapQ :: (forall d. Data d => d -> u) -> Morphism -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Morphism -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism
Ord Morphism Source #
Instance details Defined in HasCASL.Le Methods compare :: Morphism -> Morphism -> Ordering (<) :: Morphism -> Morphism -> Bool (<=) :: Morphism -> Morphism -> Bool (>) :: Morphism -> Morphism -> Bool (>=) :: Morphism -> Morphism -> Bool max :: Morphism -> Morphism -> Morphism min :: Morphism -> Morphism -> Morphism
Show Morphism Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> Morphism -> ShowS show :: Morphism -> String showList :: [Morphism] -> ShowS
Generic Morphism
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Morphism :: Type -> Type Methods from :: Morphism -> Rep Morphism x to :: Rep Morphism x -> Morphism
FromJSON Morphism
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Morphism parseJSONList :: Value -> Parser [Morphism]
ToJSON Morphism
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Morphism -> Value toEncoding :: Morphism -> Encoding toJSONList :: [Morphism] -> Value toEncodingList :: [Morphism] -> Encoding
ShATermConvertible Morphism
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Morphism -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Morphism] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Morphism) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Morphism])
Pretty Morphism Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: Morphism -> Doc Source # pretties :: [Morphism] -> Doc Source #
ProjectSublogic Sublogic Morphism Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogic :: Sublogic -> Morphism -> Morphism Source #
MinSublogic Sublogic Morphism Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: Morphism -> Sublogic Source #
Category Env Morphism Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods ide :: Env -> Morphism Source # composeMorphisms :: Morphism -> Morphism -> Result Morphism Source # dom :: Morphism -> Env Source # cod :: Morphism -> Env Source # inverse :: Morphism -> Result Morphism Source # isInclusion :: Morphism -> Bool Source # legal_mor :: Morphism -> Result () Source #
Sentences HasCASL Sentence Env Morphism Symbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: HasCASL -> Env -> Sentence -> Sentence Source # negation :: HasCASL -> Sentence -> Maybe Sentence Source # print_sign :: HasCASL -> Env -> Doc Source # print_named :: HasCASL -> Named Sentence -> Doc Source # sym_of :: HasCASL -> Env -> [Set Symbol] Source # mostSymsOf :: HasCASL -> Env -> [Symbol] Source # symmap_of :: HasCASL -> Morphism -> EndoMap Symbol Source # sym_name :: HasCASL -> Symbol -> Id Source # sym_label :: HasCASL -> Symbol -> Maybe String Source # fullSymName :: HasCASL -> Symbol -> String Source # symKind :: HasCASL -> Symbol -> String Source # symsOfSen :: HasCASL -> Env -> Sentence -> [Symbol] Source # pair_symbols :: HasCASL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source # addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
type Rep Morphism
Instance details Defined in HasCASL.ATC_HasCASL type Rep Morphism = D1 ('MetaData "Morphism" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "Morphism" 'PrefixI 'True) ((S1 ('MetaSel ('Just "msource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Env) :: S1 ('MetaSel ('Just "mtarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Env)) :: (S1 ('MetaSel ('Just "typeIdMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IdMap) :: (S1 ('MetaSel ('Just "classIdMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IdMap) :: S1 ('MetaSel ('Just "funMap") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FunMap)))))

mkMorphism :: Env -> Env -> Morphism Source #

construct morphism for subsignatures

isInclMor :: Morphism -> Bool Source #

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

Instances details

Eq SymbolType Source #
Instance details Defined in HasCASL.Le Methods (==) :: SymbolType -> SymbolType -> Bool (/=) :: SymbolType -> SymbolType -> Bool
Data SymbolType Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SymbolType -> c SymbolType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SymbolType toConstr :: SymbolType -> Constr dataTypeOf :: SymbolType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SymbolType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SymbolType) gmapT :: (forall b. Data b => b -> b) -> SymbolType -> SymbolType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SymbolType -> r gmapQ :: (forall d. Data d => d -> u) -> SymbolType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> SymbolType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SymbolType -> m SymbolType
Ord SymbolType Source #
Instance details Defined in HasCASL.Le Methods compare :: SymbolType -> SymbolType -> Ordering (<) :: SymbolType -> SymbolType -> Bool (<=) :: SymbolType -> SymbolType -> Bool (>) :: SymbolType -> SymbolType -> Bool (>=) :: SymbolType -> SymbolType -> Bool max :: SymbolType -> SymbolType -> SymbolType min :: SymbolType -> SymbolType -> SymbolType
Show SymbolType Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> SymbolType -> ShowS show :: SymbolType -> String showList :: [SymbolType] -> ShowS
Generic SymbolType
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep SymbolType :: Type -> Type Methods from :: SymbolType -> Rep SymbolType x to :: Rep SymbolType x -> SymbolType
FromJSON SymbolType
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser SymbolType parseJSONList :: Value -> Parser [SymbolType]
ToJSON SymbolType
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: SymbolType -> Value toEncoding :: SymbolType -> Encoding toJSONList :: [SymbolType] -> Value toEncodingList :: [SymbolType] -> Encoding
ShATermConvertible SymbolType
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> SymbolType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SymbolType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SymbolType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SymbolType])
type Rep SymbolType
Instance details Defined in HasCASL.ATC_HasCASL type Rep SymbolType = D1 ('MetaData "SymbolType" "HasCASL.Le" "main" 'False) (((C1 ('MetaCons "OpAsItemType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme)) :+: C1 ('MetaCons "TypeAsItemType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawKind))) :+: (C1 ('MetaCons "ClassAsItemType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 RawKind)) :+: C1 ('MetaCons "SuperClassSymbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)))) :+: ((C1 ('MetaCons "TypeKindInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :+: C1 ('MetaCons "SuperTypeSymbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id))) :+: (C1 ('MetaCons "TypeAliasSymbol" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "PredAsItemType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TypeScheme)))))

data Symbol Source #

symbols with their type

Constructors

Symbol
Fields symName :: Id symType :: SymbolType

Instances

Instances details

Eq Symbol Source #
Instance details Defined in HasCASL.Le Methods (==) :: Symbol -> Symbol -> Bool (/=) :: Symbol -> Symbol -> Bool
Data Symbol Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Symbol -> c Symbol gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Symbol toConstr :: Symbol -> Constr dataTypeOf :: Symbol -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Symbol) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol) gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Symbol -> m Symbol
Ord Symbol Source #
Instance details Defined in HasCASL.Le Methods compare :: Symbol -> Symbol -> Ordering (<) :: Symbol -> Symbol -> Bool (<=) :: Symbol -> Symbol -> Bool (>) :: Symbol -> Symbol -> Bool (>=) :: Symbol -> Symbol -> Bool max :: Symbol -> Symbol -> Symbol min :: Symbol -> Symbol -> Symbol
Show Symbol Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> Symbol -> ShowS show :: Symbol -> String showList :: [Symbol] -> ShowS
Generic Symbol
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep Symbol :: Type -> Type Methods from :: Symbol -> Rep Symbol x to :: Rep Symbol x -> Symbol
GetRange Symbol Source #
Instance details Defined in HasCASL.Symbol Methods getRange :: Symbol -> Range Source # rangeSpan :: Symbol -> [Pos] Source #
FromJSON Symbol
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser Symbol parseJSONList :: Value -> Parser [Symbol]
ToJSON Symbol
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: Symbol -> Value toEncoding :: Symbol -> Encoding toJSONList :: [Symbol] -> Value toEncodingList :: [Symbol] -> Encoding
ShATermConvertible Symbol
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> Symbol -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Symbol] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Symbol) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Symbol])
Pretty Symbol Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: Symbol -> Doc Source # pretties :: [Symbol] -> Doc Source #
ProjectSublogicM Sublogic Symbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods projectSublogicM :: Sublogic -> Symbol -> Maybe Symbol Source #
MinSublogic Sublogic Symbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods minSublogic :: Symbol -> Sublogic Source #
Sentences HasCASL Sentence Env Morphism Symbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence Source # simplify_sen :: HasCASL -> Env -> Sentence -> Sentence Source # negation :: HasCASL -> Sentence -> Maybe Sentence Source # print_sign :: HasCASL -> Env -> Doc Source # print_named :: HasCASL -> Named Sentence -> Doc Source # sym_of :: HasCASL -> Env -> [Set Symbol] Source # mostSymsOf :: HasCASL -> Env -> [Symbol] Source # symmap_of :: HasCASL -> Morphism -> EndoMap Symbol Source # sym_name :: HasCASL -> Symbol -> Id Source # sym_label :: HasCASL -> Symbol -> Maybe String Source # fullSymName :: HasCASL -> Symbol -> String Source # symKind :: HasCASL -> Symbol -> String Source # symsOfSen :: HasCASL -> Env -> Sentence -> [Symbol] Source # pair_symbols :: HasCASL -> Symbol -> Symbol -> Result Symbol Source #
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parsersAndPrinters :: HasCASL -> Map String (PrefixMap -> AParser st BasicSpec, BasicSpec -> Doc) Source # parse_basic_spec :: HasCASL -> Maybe (PrefixMap -> AParser st BasicSpec) Source # parseSingleSymbItem :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems) Source # parse_symb_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems) Source # parse_symb_map_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbMapItems) Source # toItem :: HasCASL -> BasicSpec -> Item Source # symb_items_name :: HasCASL -> SymbItems -> [String] Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: HasCASL -> NameMap Symbol -> Sentence -> Result TCorOMElement Source # export_theoryToOmdoc :: HasCASL -> SigMap Symbol -> Env -> [Named Sentence] -> Result [TCElement] Source # omdocToSym :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: HasCASL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source # addOMadtToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [[OmdADT]] -> Result (Env, [Named Sentence]) Source # addOmdocToTheory :: HasCASL -> SigMapI Symbol -> (Env, [Named Sentence]) -> [TCElement] -> Result (Env, [Named Sentence]) Source # sublogicOfTheo :: HasCASL -> (Env, [Sentence]) -> Sublogic Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2PairsInIsaHOL Methods sourceLogic :: PCoClTyConsHOL2PairsInIsaHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2PairsInIsaHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2PairsInIsaHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2PairsInIsaHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # constituents :: PCoClTyConsHOL2PairsInIsaHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # rps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # eps :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source # isGTC :: PCoClTyConsHOL2PairsInIsaHOL -> Bool Source #
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.PCoClTyConsHOL2IsabelleHOL Methods sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL Source # sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: PCoClTyConsHOL2IsabelleHOL -> Sublogic Source # minSourceTheory :: PCoClTyConsHOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle Source # mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: PCoClTyConsHOL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: PCoClTyConsHOL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: PCoClTyConsHOL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: PCoClTyConsHOL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # constituents :: PCoClTyConsHOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # rps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # eps :: PCoClTyConsHOL2IsabelleHOL -> Bool Source # isGTC :: PCoClTyConsHOL2IsabelleHOL -> Bool Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source #
Instance details Defined in Comorphisms.HasCASL2THFP_P Methods sourceLogic :: HasCASL2THFP_P -> HasCASL Source # sourceSublogic :: HasCASL2THFP_P -> Sublogic Source # sourceSublogicLossy :: HasCASL2THFP_P -> Sublogic Source # minSourceTheory :: HasCASL2THFP_P -> Maybe (LibName, String) Source # targetLogic :: HasCASL2THFP_P -> THF Source # mapSublogic :: HasCASL2THFP_P -> Sublogic -> Maybe THFSl Source # map_theory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # mapMarkedTheory :: HasCASL2THFP_P -> (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula]) Source # map_morphism :: HasCASL2THFP_P -> Morphism -> Result MorphismTHF Source # map_sentence :: HasCASL2THFP_P -> Env -> Sentence -> Result THFFormula Source # map_symbol :: HasCASL2THFP_P -> Env -> Symbol -> Set SymbolTHF Source # extractModel :: HasCASL2THFP_P -> Env -> ProofTree -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2THFP_P -> Bool Source # has_model_expansion :: HasCASL2THFP_P -> Bool Source # is_weakly_amalgamable :: HasCASL2THFP_P -> Bool Source # constituents :: HasCASL2THFP_P -> [String] Source # isInclusionComorphism :: HasCASL2THFP_P -> Bool Source # rps :: HasCASL2THFP_P -> Bool Source # eps :: HasCASL2THFP_P -> Bool Source # isGTC :: HasCASL2THFP_P -> Bool Source #
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2PCoClTyConsHOL Methods sourceLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2PCoClTyConsHOL -> Sublogic Source # minSourceTheory :: HasCASL2PCoClTyConsHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL Source # mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2PCoClTyConsHOL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2PCoClTyConsHOL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2PCoClTyConsHOL -> Bool Source # has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool Source # constituents :: HasCASL2PCoClTyConsHOL -> [String] Source # isInclusionComorphism :: HasCASL2PCoClTyConsHOL -> Bool Source # rps :: HasCASL2PCoClTyConsHOL -> Bool Source # eps :: HasCASL2PCoClTyConsHOL -> Bool Source # isGTC :: HasCASL2PCoClTyConsHOL -> Bool Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.HasCASL2HasCASL Methods sourceLogic :: HasCASL2HasCASL -> HasCASL Source # sourceSublogic :: HasCASL2HasCASL -> Sublogic Source # sourceSublogicLossy :: HasCASL2HasCASL -> Sublogic Source # minSourceTheory :: HasCASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2HasCASL -> HasCASL Source # mapSublogic :: HasCASL2HasCASL -> Sublogic -> Maybe Sublogic Source # map_theory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2HasCASL -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source # map_morphism :: HasCASL2HasCASL -> Morphism -> Result Morphism Source # map_sentence :: HasCASL2HasCASL -> Env -> Sentence -> Result Sentence Source # map_symbol :: HasCASL2HasCASL -> Env -> Symbol -> Set Symbol Source # extractModel :: HasCASL2HasCASL -> Env -> () -> Result (Env, [Named Sentence]) Source # is_model_transportable :: HasCASL2HasCASL -> Bool Source # has_model_expansion :: HasCASL2HasCASL -> Bool Source # is_weakly_amalgamable :: HasCASL2HasCASL -> Bool Source # constituents :: HasCASL2HasCASL -> [String] Source # isInclusionComorphism :: HasCASL2HasCASL -> Bool Source # rps :: HasCASL2HasCASL -> Bool Source # eps :: HasCASL2HasCASL -> Bool Source # isGTC :: HasCASL2HasCASL -> Bool Source #
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.CASL2HasCASL Methods sourceLogic :: CASL2HasCASL -> CASL Source # sourceSublogic :: CASL2HasCASL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2HasCASL -> CASL_Sublogics Source # minSourceTheory :: CASL2HasCASL -> Maybe (LibName, String) Source # targetLogic :: CASL2HasCASL -> HasCASL Source # mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic Source # map_theory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: CASL2HasCASL -> (CASLSign, [Named CASLFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism Source # map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CASL2HasCASL -> CASLSign -> Symbol0 -> Set Symbol Source # extractModel :: CASL2HasCASL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2HasCASL -> Bool Source # has_model_expansion :: CASL2HasCASL -> Bool Source # is_weakly_amalgamable :: CASL2HasCASL -> Bool Source # constituents :: CASL2HasCASL -> [String] Source # isInclusionComorphism :: CASL2HasCASL -> Bool Source # rps :: CASL2HasCASL -> Bool Source # eps :: CASL2HasCASL -> Bool Source # isGTC :: CASL2HasCASL -> Bool Source #
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.ExtModal2HasCASL Methods sourceLogic :: ExtModal2HasCASL -> ExtModal Source # sourceSublogic :: ExtModal2HasCASL -> ExtModalSL Source # sourceSublogicLossy :: ExtModal2HasCASL -> ExtModalSL Source # minSourceTheory :: ExtModal2HasCASL -> Maybe (LibName, String) Source # targetLogic :: ExtModal2HasCASL -> HasCASL Source # mapSublogic :: ExtModal2HasCASL -> ExtModalSL -> Maybe Sublogic Source # map_theory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: ExtModal2HasCASL -> (ExtModalSign, [Named ExtModalFORMULA]) -> Result (Env, [Named Sentence]) Source # map_morphism :: ExtModal2HasCASL -> ExtModalMorph -> Result Morphism Source # map_sentence :: ExtModal2HasCASL -> ExtModalSign -> ExtModalFORMULA -> Result Sentence Source # map_symbol :: ExtModal2HasCASL -> ExtModalSign -> Symbol0 -> Set Symbol Source # extractModel :: ExtModal2HasCASL -> ExtModalSign -> () -> Result (ExtModalSign, [Named ExtModalFORMULA]) Source # is_model_transportable :: ExtModal2HasCASL -> Bool Source # has_model_expansion :: ExtModal2HasCASL -> Bool Source # is_weakly_amalgamable :: ExtModal2HasCASL -> Bool Source # constituents :: ExtModal2HasCASL -> [String] Source # isInclusionComorphism :: ExtModal2HasCASL -> Bool Source # rps :: ExtModal2HasCASL -> Bool Source # eps :: ExtModal2HasCASL -> Bool Source # isGTC :: ExtModal2HasCASL -> Bool Source #
type Rep Symbol
Instance details Defined in HasCASL.ATC_HasCASL type Rep Symbol = D1 ('MetaData "Symbol" "HasCASL.Le" "main" 'False) (C1 ('MetaCons "Symbol" 'PrefixI 'True) (S1 ('MetaSel ('Just "symName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: S1 ('MetaSel ('Just "symType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SymbolType)))

type SymbolMap = Map Symbol Symbol Source #

mapping symbols to symbols

type SymbolSet = Set Symbol Source #

a set of symbols

idToTypeSymbol :: Id -> RawKind -> Symbol Source #

create a type symbol

idToClassSymbol :: Id -> RawKind -> Symbol Source #

create a class symbol

idToOpSymbol :: Id -> TypeScheme -> Symbol Source #

create an operation symbol

data RawSymbol Source #

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.

Constructors

AnID Id
AKindedId SymbKind Id
ASymbol Symbol

Instances

Instances details

Eq RawSymbol Source #
Instance details Defined in HasCASL.Le Methods (==) :: RawSymbol -> RawSymbol -> Bool (/=) :: RawSymbol -> RawSymbol -> Bool
Data RawSymbol Source #
Instance details Defined in HasCASL.Le Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RawSymbol -> c RawSymbol gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RawSymbol toConstr :: RawSymbol -> Constr dataTypeOf :: RawSymbol -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RawSymbol) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol) gmapT :: (forall b. Data b => b -> b) -> RawSymbol -> RawSymbol gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r gmapQ :: (forall d. Data d => d -> u) -> RawSymbol -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> RawSymbol -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
Ord RawSymbol Source #
Instance details Defined in HasCASL.Le Methods compare :: RawSymbol -> RawSymbol -> Ordering (<) :: RawSymbol -> RawSymbol -> Bool (<=) :: RawSymbol -> RawSymbol -> Bool (>) :: RawSymbol -> RawSymbol -> Bool (>=) :: RawSymbol -> RawSymbol -> Bool max :: RawSymbol -> RawSymbol -> RawSymbol min :: RawSymbol -> RawSymbol -> RawSymbol
Show RawSymbol Source #
Instance details Defined in HasCASL.Le Methods showsPrec :: Int -> RawSymbol -> ShowS show :: RawSymbol -> String showList :: [RawSymbol] -> ShowS
Generic RawSymbol
Instance details Defined in HasCASL.ATC_HasCASL Associated Types type Rep RawSymbol :: Type -> Type Methods from :: RawSymbol -> Rep RawSymbol x to :: Rep RawSymbol x -> RawSymbol
GetRange RawSymbol Source #
Instance details Defined in HasCASL.RawSym Methods getRange :: RawSymbol -> Range Source # rangeSpan :: RawSymbol -> [Pos] Source #
FromJSON RawSymbol
Instance details Defined in HasCASL.ATC_HasCASL Methods parseJSON :: Value -> Parser RawSymbol parseJSONList :: Value -> Parser [RawSymbol]
ToJSON RawSymbol
Instance details Defined in HasCASL.ATC_HasCASL Methods toJSON :: RawSymbol -> Value toEncoding :: RawSymbol -> Encoding toJSONList :: [RawSymbol] -> Value toEncodingList :: [RawSymbol] -> Encoding
ShATermConvertible RawSymbol
Instance details Defined in HasCASL.ATC_HasCASL Methods toShATermAux :: ATermTable -> RawSymbol -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [RawSymbol] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, RawSymbol) fromShATermList' :: Int -> ATermTable -> (ATermTable, [RawSymbol])
Pretty RawSymbol Source #
Instance details Defined in HasCASL.PrintLe Methods pretty :: RawSymbol -> Doc Source # pretties :: [RawSymbol] -> Doc Source #
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods basic_analysis :: HasCASL -> Maybe ((BasicSpec, Env, GlobalAnnos) -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])) Source # sen_analysis :: HasCASL -> Maybe ((BasicSpec, Env, Sentence) -> Result Sentence) Source # extBasicAnalysis :: HasCASL -> IRI -> LibName -> BasicSpec -> Env -> GlobalAnnos -> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]) Source # stat_symb_map_items :: HasCASL -> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol] Source # convertTheory :: HasCASL -> Maybe ((Env, [Named Sentence]) -> BasicSpec) Source # ensures_amalgamability :: HasCASL -> ([CASLAmalgOpt], Gr Env (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: HasCASL -> Morphism -> [Named Sentence] -> Result (Env, [Named Sentence]) Source # signature_colimit :: HasCASL -> Gr Env (Int, Morphism) -> Result (Env, Map Int Morphism) Source # qualify :: HasCASL -> SIMPLE_ID -> LibName -> Morphism -> Env -> Result (Morphism, [Named Sentence]) Source # symbol_to_raw :: HasCASL -> Symbol -> RawSymbol Source # id_to_raw :: HasCASL -> Id -> RawSymbol Source # matches :: HasCASL -> Symbol -> RawSymbol -> Bool Source # empty_signature :: HasCASL -> Env Source # add_symb_to_sign :: HasCASL -> Env -> Symbol -> Result Env Source # signature_union :: HasCASL -> Env -> Env -> Result Env Source # signatureDiff :: HasCASL -> Env -> Env -> Result Env Source # intersection :: HasCASL -> Env -> Env -> Result Env Source # final_union :: HasCASL -> Env -> Env -> Result Env Source # morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: HasCASL -> Env -> Env -> Bool Source # subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism Source # generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism Source # induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism Source # induced_from_to_morphism :: HasCASL -> EndoMap RawSymbol -> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism Source # is_transportable :: HasCASL -> Morphism -> Bool Source # is_injective :: HasCASL -> Morphism -> Bool Source # theory_to_taxonomy :: HasCASL -> TaxoGraphKind -> MMiSSOntology -> Env -> [Named Sentence] -> Result MMiSSOntology Source # corresp2th :: HasCASL -> String -> Bool -> Env -> Env -> [SymbItems] -> [SymbItems] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Env, [Named Sentence], Env, Env, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: HasCASL -> Env -> Env -> [SymbItems] -> [SymbItems] -> Result (Env, Env, Env, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: HasCASL -> [IRI] -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence]) Source #
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in HasCASL.Logic_HasCASL Methods parse_basic_sen :: HasCASL -> Maybe (BasicSpec -> AParser st Sentence) Source # stability :: HasCASL -> Stability Source # data_logic :: HasCASL -> Maybe AnyLogic Source # top_sublogic :: HasCASL -> Sublogic Source # all_sublogics :: HasCASL -> [Sublogic] Source # bottomSublogic :: HasCASL -> Maybe Sublogic Source # sublogicDimensions :: HasCASL -> [[Sublogic]] Source # parseSublogic :: HasCASL -> String -> Maybe Sublogic Source # proj_sublogic_epsilon :: HasCASL -> Sublogic -> Env -> Morphism Source # provers :: HasCASL -> [Prover Env Sentence Morphism Sublogic ()] Source # default_prover :: HasCASL -> String Source # cons_checkers :: HasCASL -> [ConsChecker Env Sentence Sublogic Morphism ()] Source # conservativityCheck :: HasCASL -> [ConservativityChecker Env Sentence Morphism] Source # empty_proof_tree :: HasCASL -> () Source # syntaxTable :: HasCASL -> Env -> Maybe SyntaxTable Source # omdoc_metatheory :: HasCASL -> Maybe OMCD Source # export_symToOmdoc :: HasCASL -> NameMap Symbol -> Symbol -> String -> Result