CASL.Sublogic

Contents

• types
• class
• predicates on CASL_SL
• functions for SemiLatticeWithTop instance
• functions for the creation of minimal sublogics
• functions for Logic instance sublogic to string conversion
  • list of all sublogics
• computes the sublogic of a given element
• projects an element into a given sublogic

Description

Synopsis

• 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
  • = Atomic
  • | Horn
  • | GHorn
  • | FOL
  • | SOL
• data SubsortingFeatures
  • = NoSub
  • | LocFilSub
  • | Sub
• data SortGenerationFeatures
  • = NoSortGen
  • | SortGen {
    • emptyMapping :: Bool
    • onlyInjConstrs :: Bool
    }
• class (Ord l, Show l) => Lattice l where
  • cjoin :: l -> l -> l
  • ctop :: l
  • bot :: l
• 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
• 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

class

predicates on CASL_SL

functions for SemiLatticeWithTop instance

functions for the creation of minimal sublogics

functions for Logic instance sublogic to string conversion

list of all sublogics

computes the sublogic of a given element

projects an element into a given sublogic