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

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

 Eq Formulas Source # Methods(==) :: Formulas -> Formulas -> Bool(/=) :: Formulas -> Formulas -> Bool Data Formulas Source # 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 :: (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 # Methodscompare :: Formulas -> Formulas -> Ordering(<) :: Formulas -> Formulas -> Bool(<=) :: Formulas -> Formulas -> Bool(>) :: Formulas -> Formulas -> Bool(>=) :: Formulas -> Formulas -> Bool Show Formulas Source # MethodsshowsPrec :: Int -> Formulas -> ShowSshow :: Formulas -> StringshowList :: [Formulas] -> ShowS

data Classes Source #

Constructors

 NoClasses SimpleTypeClasses ConstructorClasses

Instances

 Eq Classes Source # Methods(==) :: Classes -> Classes -> Bool(/=) :: Classes -> Classes -> Bool Data Classes Source # 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 :: (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 # 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 # MethodsshowsPrec :: Int -> Classes -> ShowSshow :: Classes -> StringshowList :: [Classes] -> ShowS

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 #