| Copyright | (c) Pascal Schmidt C. Maeder and Uni Bremen 2002-2006 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
CASL.Sublogic
Contents
Description
Sublogic analysis for CASL
This module provides the sublogic functions (as required by Logic.hs) for CASL. The functions allow to compute the minimal sublogics needed by a given element, to check whether an item is part of a given sublogic, and to project an element into a given sublogic.
- type CASL_Sublogics = CASL_SL ()
- data CASL_SL a = CASL_SL {
- sub_features :: SubsortingFeatures
- has_part :: Bool
- cons_features :: SortGenerationFeatures
- has_eq :: Bool
- has_pred :: Bool
- which_logic :: CASL_Formulas
- has_empty_sorts :: Bool
- ext_features :: a
- data CASL_Formulas
- data SubsortingFeatures
- data SortGenerationFeatures
- = NoSortGen
- | SortGen {
- emptyMapping :: Bool
- onlyInjConstrs :: Bool
- class (Ord l, Show l) => Lattice l where
- has_sub :: CASL_SL a -> Bool
- has_cons :: CASL_SL a -> Bool
- mkTop :: a -> CASL_SL a
- top :: Lattice a => CASL_SL a
- caslTop :: Lattice a => CASL_SL a
- cFol :: Lattice a => CASL_SL a
- fol :: Lattice a => CASL_SL a
- cPrenex :: Lattice a => CASL_SL a
- sublogics_max :: Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
- comp_list :: Lattice a => [CASL_SL a] -> CASL_SL a
- bottom :: Lattice a => CASL_SL a
- mkBot :: a -> CASL_SL a
- emptyMapConsFeature :: SortGenerationFeatures
- need_sub :: Lattice a => CASL_SL a
- need_pred :: Lattice a => CASL_SL a
- need_horn :: Lattice a => CASL_SL a
- need_fol :: Lattice a => CASL_SL a
- updExtFeature :: (a -> a) -> CASL_SL a -> CASL_SL a
- sublogics_name :: (a -> String) -> CASL_SL a -> String
- parseSL :: (String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a)
- parseBool :: String -> String -> (Bool, String)
- sublogics_all :: Lattice a => [a] -> [CASL_SL a]
- sDims :: Lattice a => [[a]] -> [[CASL_SL a]]
- sl_sig_items :: Lattice a => (s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a
- sl_basic_spec :: Lattice a => (b -> CASL_SL a) -> (s -> CASL_SL a) -> (f -> CASL_SL a) -> BASIC_SPEC b s f -> CASL_SL a
- sl_opkind :: Lattice a => OpKind -> CASL_SL a
- sl_op_type :: Lattice a => OP_TYPE -> CASL_SL a
- sl_op_item :: Lattice a => (f -> CASL_SL a) -> OP_ITEM f -> CASL_SL a
- sl_pred_item :: Lattice a => (f -> CASL_SL a) -> PRED_ITEM f -> CASL_SL a
- sl_sentence :: Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
- sl_term :: Lattice a => (f -> CASL_SL a) -> TERM f -> CASL_SL a
- sl_symb_items :: Lattice a => SYMB_ITEMS -> CASL_SL a
- sl_symb_map_items :: Lattice a => SYMB_MAP_ITEMS -> CASL_SL a
- sl_sign :: Lattice a => (e -> CASL_SL a) -> Sign f e -> CASL_SL a
- sl_morphism :: Lattice a => (e -> CASL_SL a) -> Morphism f e m -> CASL_SL a
- sl_symbol :: Lattice a => Symbol -> CASL_SL a
- pr_basic_spec :: Lattice a => (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])) -> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])) -> (CASL_SL a -> f -> Maybe (FORMULA f)) -> CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f
- pr_symb_items :: Lattice a => CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS
- pr_symb_map_items :: Lattice a => CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
- pr_sign :: CASL_SL a -> Sign f e -> Sign f e
- pr_morphism :: Lattice a => CASL_SL a -> Morphism f e m -> Morphism f e m
- pr_epsilon :: m -> CASL_SL a -> Sign f e -> Morphism f e m
- pr_symbol :: Lattice a => CASL_SL a -> Symbol -> Maybe Symbol
types
type CASL_Sublogics = CASL_SL () Source #
Constructors
| CASL_SL | |
Fields
| |
Instances
data CASL_Formulas Source #
Constructors
| Atomic | atomic logic |
| Horn | positive conditional logic |
| GHorn | generalized positive conditional logic |
| Prenex | formulas in prenex normal form |
| FOL | first-order logic |
| SOL | second-order logic |
Instances
| Eq CASL_Formulas Source # | |
| Data CASL_Formulas Source # | |
| Ord CASL_Formulas Source # | |
| Show CASL_Formulas Source # | |
data SubsortingFeatures Source #
Instances
| Eq SubsortingFeatures Source # | |
| Data SubsortingFeatures Source # | |
| Ord SubsortingFeatures Source # | |
| Show SubsortingFeatures Source # | |
data SortGenerationFeatures Source #
Constructors
| NoSortGen | |
| SortGen | |
Fields
| |
Instances
class
predicates on CASL_SL
functions for SemiLatticeWithTop instance
functions for the creation of minimal sublogics
updExtFeature :: (a -> a) -> CASL_SL a -> CASL_SL a Source #
functions for Logic instance sublogic to string conversion
sublogics_name :: (a -> String) -> CASL_SL a -> String Source #
list of all sublogics
sublogics_all :: Lattice a => [a] -> [CASL_SL a] Source #
computes the sublogic of a given element
sl_sig_items :: Lattice a => (s -> CASL_SL a) -> (f -> CASL_SL a) -> SIG_ITEMS s f -> CASL_SL a Source #
sl_basic_spec :: Lattice a => (b -> CASL_SL a) -> (s -> CASL_SL a) -> (f -> CASL_SL a) -> BASIC_SPEC b s f -> CASL_SL a Source #
sl_symb_items :: Lattice a => SYMB_ITEMS -> CASL_SL a Source #
sl_symb_map_items :: Lattice a => SYMB_MAP_ITEMS -> CASL_SL a Source #
projects an element into a given sublogic
pr_basic_spec :: Lattice a => (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])) -> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])) -> (CASL_SL a -> f -> Maybe (FORMULA f)) -> CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f Source #
pr_symb_items :: Lattice a => CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS Source #
pr_symb_map_items :: Lattice a => CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS Source #