Copyright	(c) Zicheng Wang C.Maeder Uni Bremen 2002-2009
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (imports Logic.Comorphism)
Safe Haskell	None

Comorphisms.CASL2SubCFOL

Description

Coding out partiality (SubPCFOL= -> SubCFOL=) while keeping subsorting. Without unique bottoms sort generation axioms are not allowed. Then we have (SubPFOL= -> SubFOL=).

Synopsis

data FormulaTreatment
- = NoMembershipOrCast
- | FormulaDependent
- | SubsortBottoms
- | AllSortBottoms
treatFormula :: FormulaTreatment -> a -> a -> a -> a -> a
data CASL2SubCFOL = CASL2SubCFOL {
- uniqueBottom :: Bool
- formulaTreatment :: FormulaTreatment
}
defaultCASL2SubCFOL :: CASL2SubCFOL
totalizeSymbType :: SymbType -> SymbType
sortsWithBottom :: FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
defPred :: Id
defined :: TermExtension f => Set SORT -> TERM f -> Range -> FORMULA f
defVards :: TermExtension f => Set SORT -> [VAR_DECL] -> FORMULA f
defVars :: TermExtension f => Set SORT -> VAR_DECL -> [FORMULA f]
defVar :: TermExtension f => Set SORT -> SORT -> Token -> FORMULA f
totalizeOpSymb :: OP_SYMB -> OP_SYMB
addBottomAlt :: Constraint -> Constraint
argSorts :: Constraint -> Set SORT
totalizeConstraint :: Set SORT -> Constraint -> Constraint
botType :: SORT -> OpType
encodeSig :: Set SORT -> Sign f e -> Sign f e
mkNonEmptyAxiomName :: SORT -> String
mkNotDefBotAxiomName :: SORT -> String
mkTotalityAxiomName :: OP_NAME -> String
generateAxioms :: (Ord f, TermExtension f) => Bool -> Set SORT -> Sign f e -> [Named (FORMULA f)]
codeRecord :: TermExtension f => Bool -> Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeFormula :: Bool -> Set SORT -> FORMULA () -> FORMULA ()
codeTerm :: Bool -> Set SORT -> TERM () -> TERM ()
botSorts :: (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
botFormulaSorts :: FORMULA f -> Set SORT
botTermSorts :: TERM f -> Set SORT

Documentation

data FormulaTreatment Source #

determine the need for bottom constants

Constructors

NoMembershipOrCast
FormulaDependent
SubsortBottoms
AllSortBottoms

Instances

Instances details

Show FormulaTreatment Source #
Instance details Defined in Comorphisms.CASL2SubCFOL Methods showsPrec :: Int -> FormulaTreatment -> ShowS show :: FormulaTreatment -> String showList :: [FormulaTreatment] -> ShowS

treatFormula :: FormulaTreatment -> a -> a -> a -> a -> a Source #

a case selector for formula treatment

data CASL2SubCFOL Source #

The identity of the comorphism depending on parameters. NoMembershipOrCast reject membership test or cast to non-bottom sorts. . FormulaDependent creates a formula dependent signature translation. SubsortBottoms creates bottoms for all proper subsorts.

Constructors

CASL2SubCFOL
Fields uniqueBottom :: Bool removes free types formulaTreatment :: FormulaTreatment deal with membership tests and casts

Instances

Instances details

Show CASL2SubCFOL Source #
Instance details Defined in Comorphisms.CASL2SubCFOL Methods showsPrec :: Int -> CASL2SubCFOL -> ShowS show :: CASL2SubCFOL -> String showList :: [CASL2SubCFOL] -> ShowS
Language CASL2SubCFOL Source #
Instance details Defined in Comorphisms.CASL2SubCFOL Methods language_name :: CASL2SubCFOL -> String Source # description :: CASL2SubCFOL -> String Source #
Comorphism CASL2SubCFOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.CASL2SubCFOL Methods sourceLogic :: CASL2SubCFOL -> CASL Source # sourceSublogic :: CASL2SubCFOL -> CASL_Sublogics Source # sourceSublogicLossy :: CASL2SubCFOL -> CASL_Sublogics Source # minSourceTheory :: CASL2SubCFOL -> Maybe (LibName, String) Source # targetLogic :: CASL2SubCFOL -> CASL Source # mapSublogic :: CASL2SubCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics Source # map_theory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: CASL2SubCFOL -> (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: CASL2SubCFOL -> CASLMor -> Result CASLMor Source # map_sentence :: CASL2SubCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA Source # map_symbol :: CASL2SubCFOL -> CASLSign -> Symbol -> Set Symbol Source # extractModel :: CASL2SubCFOL -> CASLSign -> ProofTree -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CASL2SubCFOL -> Bool Source # has_model_expansion :: CASL2SubCFOL -> Bool Source # is_weakly_amalgamable :: CASL2SubCFOL -> Bool Source # constituents :: CASL2SubCFOL -> [String] Source # isInclusionComorphism :: CASL2SubCFOL -> Bool Source # rps :: CASL2SubCFOL -> Bool Source # eps :: CASL2SubCFOL -> Bool Source # isGTC :: CASL2SubCFOL -> Bool Source #