Hets - the Heterogeneous Tool Set
Copyright (c) Sonja Groening C. Maeder and Uni Bremen 2002-2006 GPLv2 or higher, see LICENSE.txt Christian.Maeder@dfki.de experimental portable None

HasCASL.Sublogic

Description

This module provides the sublogic functions (as required by Logic.hs) for HasCASL. The functions allow to compute the minimal sublogic needed by a given element, to check whether an item is part of a given sublogic, and -- not yet -- to project an element into a given sublogic.

Synopsis

# datatypes

data Sublogic Source #

HasCASL sublogics

Constructors

 Sublogic Fieldshas_sub :: Boolsubsortinghas_part :: Boolpartialityhas_eq :: Boolequalityhas_pred :: Boolpredicatestype_classes :: Classes has_polymorphism :: Bool has_type_constructors :: Bool has_products :: Bool which_logic :: Formulas

#### Instances

Instances details

data Formulas Source #

formula kinds of HasCASL sublogics

Constructors

 Atomic atomic logic Horn positive conditional logic GHorn generalized positive conditional logic FOL first-order logic HOL higher-order logic

#### Instances

Instances details
 Eq Formulas Source # Instance detailsDefined in HasCASL.Sublogic Methods(==) :: Formulas -> Formulas -> Bool(/=) :: Formulas -> Formulas -> Bool Data Formulas Source # Instance detailsDefined in HasCASL.Sublogic Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formulas -> c Formulasgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FormulastoConstr :: Formulas -> ConstrdataTypeOf :: Formulas -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Formulas)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formulas)gmapT :: (forall b. Data b => b -> b) -> Formulas -> FormulasgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formulas -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formulas -> rgmapQ :: (forall d. Data d => d -> u) -> Formulas -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> Formulas -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> Formulas -> m FormulasgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formulas -> m FormulasgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formulas -> m Formulas Ord Formulas Source # Instance detailsDefined in HasCASL.Sublogic Methodscompare :: Formulas -> Formulas -> Ordering(<) :: Formulas -> Formulas -> Bool(<=) :: Formulas -> Formulas -> Bool(>) :: Formulas -> Formulas -> Bool(>=) :: Formulas -> Formulas -> Bool Show Formulas Source # Instance detailsDefined in HasCASL.Sublogic MethodsshowsPrec :: Int -> Formulas -> ShowSshow :: Formulas -> StringshowList :: [Formulas] -> ShowS Generic Formulas Instance detailsDefined in HasCASL.ATC_HasCASL Associated Typestype Rep Formulas :: Type -> Type Methodsfrom :: Formulas -> Rep Formulas xto :: Rep Formulas x -> Formulas FromJSON Formulas Instance detailsDefined in HasCASL.ATC_HasCASL MethodsparseJSON :: Value -> Parser FormulasparseJSONList :: Value -> Parser [Formulas] ToJSON Formulas Instance detailsDefined in HasCASL.ATC_HasCASL MethodstoJSON :: Formulas -> ValuetoEncoding :: Formulas -> EncodingtoJSONList :: [Formulas] -> ValuetoEncodingList :: [Formulas] -> Encoding ShATermConvertible Formulas Instance detailsDefined in HasCASL.ATC_HasCASL MethodstoShATermAux :: ATermTable -> Formulas -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [Formulas] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, Formulas)fromShATermList' :: Int -> ATermTable -> (ATermTable, [Formulas]) type Rep Formulas Instance detailsDefined in HasCASL.ATC_HasCASL type Rep Formulas = D1 ('MetaData "Formulas" "HasCASL.Sublogic" "main" 'False) ((C1 ('MetaCons "Atomic" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Horn" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "GHorn" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FOL" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "HOL" 'PrefixI 'False) (U1 :: Type -> Type))))

data Classes Source #

Constructors

 NoClasses SimpleTypeClasses ConstructorClasses

#### Instances

Instances details
 Eq Classes Source # Instance detailsDefined in HasCASL.Sublogic Methods(==) :: Classes -> Classes -> Bool(/=) :: Classes -> Classes -> Bool Data Classes Source # Instance detailsDefined in HasCASL.Sublogic Methodsgfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Classes -> c Classesgunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ClassestoConstr :: Classes -> ConstrdataTypeOf :: Classes -> DataTypedataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Classes)dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Classes)gmapT :: (forall b. Data b => b -> b) -> Classes -> ClassesgmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Classes -> rgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Classes -> rgmapQ :: (forall d. Data d => d -> u) -> Classes -> [u]gmapQi :: Int -> (forall d. Data d => d -> u) -> Classes -> ugmapM :: Monad m => (forall d. Data d => d -> m d) -> Classes -> m ClassesgmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Classes -> m ClassesgmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Classes -> m Classes Ord Classes Source # Instance detailsDefined in HasCASL.Sublogic Methodscompare :: Classes -> Classes -> Ordering(<) :: Classes -> Classes -> Bool(<=) :: Classes -> Classes -> Bool(>) :: Classes -> Classes -> Bool(>=) :: Classes -> Classes -> Boolmax :: Classes -> Classes -> Classesmin :: Classes -> Classes -> Classes Show Classes Source # Instance detailsDefined in HasCASL.Sublogic MethodsshowsPrec :: Int -> Classes -> ShowSshow :: Classes -> StringshowList :: [Classes] -> ShowS Generic Classes Instance detailsDefined in HasCASL.ATC_HasCASL Associated Typestype Rep Classes :: Type -> Type Methodsfrom :: Classes -> Rep Classes xto :: Rep Classes x -> Classes FromJSON Classes Instance detailsDefined in HasCASL.ATC_HasCASL MethodsparseJSON :: Value -> Parser ClassesparseJSONList :: Value -> Parser [Classes] ToJSON Classes Instance detailsDefined in HasCASL.ATC_HasCASL MethodstoJSON :: Classes -> ValuetoEncoding :: Classes -> EncodingtoJSONList :: [Classes] -> ValuetoEncodingList :: [Classes] -> Encoding ShATermConvertible Classes Instance detailsDefined in HasCASL.ATC_HasCASL MethodstoShATermAux :: ATermTable -> Classes -> IO (ATermTable, Int)toShATermList' :: ATermTable -> [Classes] -> IO (ATermTable, Int)fromShATermAux :: Int -> ATermTable -> (ATermTable, Classes)fromShATermList' :: Int -> ATermTable -> (ATermTable, [Classes]) type Rep Classes Instance detailsDefined in HasCASL.ATC_HasCASL type Rep Classes = D1 ('MetaData "Classes" "HasCASL.Sublogic" "main" 'False) (C1 ('MetaCons "NoClasses" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "SimpleTypeClasses" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConstructorClasses" 'PrefixI 'False) (U1 :: Type -> Type)))

top element

# combining sublogics restrictions

make sublogic consistent w.r.t. illegal combinations

# further sublogic constants

bottom sublogic

top sublogic without subtypes

top sublogic without type classes

top sublogic without partiality

# functions for Logic instance

## sublogic to string converstion

sublogic_name :: Sublogic -> String Source #

the sublogic name as a singleton string list

## list of all sublogics

generate a list of all sublogics for HasCASL

## checks if element is in given sublogic

in_env :: Sublogic -> Env -> Bool Source #