Copyright	(c) Sonja Groening, 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

HasCASL.Sublogic

Contents

datatypes
functions for SemiLatticeWithTop instance
combining sublogics restrictions
further sublogic constants
functions for Logic instance
computes the sublogic of a given element

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

HasCASL sublogics

Constructors

Sublogic
Fields has_sub :: Bool subsorting has_part :: Bool partiality has_eq :: Bool equality has_pred :: Bool predicates type_classes :: Classes has_polymorphism :: Bool has_type_constructors :: Bool has_products :: Bool which_logic :: Formulas

Instances

Eq Sublogic
Data Sublogic
Ord Sublogic
Show Sublogic
ShATermConvertible Sublogic
SublogicName Sublogic
SemiLatticeWithTop Sublogic
Typeable * Sublogic
ProjectSublogicM Sublogic SymbMapItems
ProjectSublogicM Sublogic SymbItems
ProjectSublogicM Sublogic Symbol
ProjectSublogic Sublogic BasicSpec
ProjectSublogic Sublogic Morphism
ProjectSublogic Sublogic Env
MinSublogic Sublogic SymbMapItems
MinSublogic Sublogic SymbItems
MinSublogic Sublogic BasicSpec
MinSublogic Sublogic Symbol
MinSublogic Sublogic Morphism
MinSublogic Sublogic Env
MinSublogic Sublogic Sentence
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol ()
Comorphism HasCASL2Haskell HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism Symbol RawSymbol ()