hets -- a heterogenous Specification (CASL) tool setContentsIndex
CASL.Sublogic
Portability portable
Stability experimental
Maintainer hets@tzi.de
Contents
datatypes
functions for LatticeWithTop instance
functions for Logic instance
sublogic to string converstion
list of all sublogics
checks if element is in given sublogic
computes the sublogic of a given element
projects an element into a given sublogic
Description

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.

Synopsis
data CASL_Sublogics = CASL_SL {
has_sub :: Bool
has_part :: Bool
has_cons :: Bool
has_eq :: Bool
has_pred :: Bool
which_logic :: CASL_Formulas
}
data CASL_Formulas
= Atomic
| Horn
| GHorn
| FOL
top :: CASL_Sublogics
sublogics_max :: CASL_Sublogics -> CASL_Sublogics -> CASL_Sublogics
sublogics_min :: CASL_Sublogics -> CASL_Sublogics -> CASL_Sublogics
sublogics_name :: CASL_Sublogics -> [String]
sublogics_all :: [CASL_Sublogics]
in_basic_spec :: CASL_Sublogics -> BASIC_SPEC -> Bool
in_sentence :: CASL_Sublogics -> FORMULA -> Bool
in_symb_items :: CASL_Sublogics -> SYMB_ITEMS -> Bool
in_symb_items_list :: CASL_Sublogics -> SYMB_ITEMS_LIST -> Bool
in_symb_map_items :: CASL_Sublogics -> SYMB_MAP_ITEMS -> Bool
in_symb_map_items_list :: CASL_Sublogics -> SYMB_MAP_ITEMS_LIST -> Bool
in_sign :: CASL_Sublogics -> Sign -> Bool
in_morphism :: CASL_Sublogics -> Morphism -> Bool
in_symbol :: CASL_Sublogics -> Symbol -> Bool
sl_basic_spec :: BASIC_SPEC -> CASL_Sublogics
sl_sentence :: FORMULA -> CASL_Sublogics
sl_symb_items :: SYMB_ITEMS -> CASL_Sublogics
sl_symb_map_items :: SYMB_MAP_ITEMS -> CASL_Sublogics
sl_sign :: Sign -> CASL_Sublogics
sl_morphism :: Morphism -> CASL_Sublogics
sl_symbol :: Symbol -> CASL_Sublogics
pr_basic_spec :: CASL_Sublogics -> BASIC_SPEC -> BASIC_SPEC
pr_symb_items :: CASL_Sublogics -> SYMB_ITEMS -> Maybe SYMB_ITEMS
pr_symb_map_items :: CASL_Sublogics -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
pr_sign :: CASL_Sublogics -> Sign -> Sign
pr_morphism :: CASL_Sublogics -> Morphism -> Morphism
pr_epsilon :: CASL_Sublogics -> Sign -> Morphism
pr_symbol :: CASL_Sublogics -> Symbol -> Maybe Symbol
datatypes
data CASL_Sublogics
Constructors
CASL_SL
has_sub :: Bool
has_part :: Bool
has_cons :: Bool
has_eq :: Bool
has_pred :: Bool
which_logic :: CASL_Formulas
Instances
ATermConvertible CASL_Sublogics
LatticeWithTop CASL_Sublogics
Logic CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol ()
Typeable CASL_Sublogics
Show CASL_Sublogics
Ord CASL_Sublogics
Eq CASL_Sublogics
Comorphism CASL2HasCASL CASL CASL_Sublogics BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol RawSymbol () HasCASL HasCASL_Sublogics BasicSpec Term SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
data CASL_Formulas
Datatypes for CASL sublogics
Constructors
Atomic
Horn
GHorn
FOL
Instances
ATermConvertible CASL_Formulas
Show CASL_Formulas
Ord CASL_Formulas
Eq CASL_Formulas
functions for LatticeWithTop instance
top :: CASL_Sublogics
sublogics_max :: CASL_Sublogics -> CASL_Sublogics -> CASL_Sublogics
sublogics_min :: CASL_Sublogics -> CASL_Sublogics -> CASL_Sublogics
functions for Logic instance
sublogic to string converstion
sublogics_name :: CASL_Sublogics -> [String]
list of all sublogics
sublogics_all :: [CASL_Sublogics]
checks if element is in given sublogic
in_basic_spec :: CASL_Sublogics -> BASIC_SPEC -> Bool
in_sentence :: CASL_Sublogics -> FORMULA -> Bool
in_symb_items :: CASL_Sublogics -> SYMB_ITEMS -> Bool
in_symb_items_list :: CASL_Sublogics -> SYMB_ITEMS_LIST -> Bool
in_symb_map_items :: CASL_Sublogics -> SYMB_MAP_ITEMS -> Bool
in_symb_map_items_list :: CASL_Sublogics -> SYMB_MAP_ITEMS_LIST -> Bool
in_sign :: CASL_Sublogics -> Sign -> Bool
in_morphism :: CASL_Sublogics -> Morphism -> Bool
in_symbol :: CASL_Sublogics -> Symbol -> Bool
computes the sublogic of a given element
sl_basic_spec :: BASIC_SPEC -> CASL_Sublogics
sl_sentence :: FORMULA -> CASL_Sublogics
sl_symb_items :: SYMB_ITEMS -> CASL_Sublogics
sl_symb_map_items :: SYMB_MAP_ITEMS -> CASL_Sublogics
sl_sign :: Sign -> CASL_Sublogics
sl_morphism :: Morphism -> CASL_Sublogics
sl_symbol :: Symbol -> CASL_Sublogics
projects an element into a given sublogic
pr_basic_spec :: CASL_Sublogics -> BASIC_SPEC -> BASIC_SPEC
pr_symb_items :: CASL_Sublogics -> SYMB_ITEMS -> Maybe SYMB_ITEMS
pr_symb_map_items :: CASL_Sublogics -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
pr_sign :: CASL_Sublogics -> Sign -> Sign
pr_morphism :: CASL_Sublogics -> Morphism -> Morphism
pr_epsilon :: CASL_Sublogics -> Sign -> Morphism
pr_symbol :: CASL_Sublogics -> Symbol -> Maybe Symbol
Produced by Haddock version 0.6