| 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=).
- data FormulaTreatment
- treatFormula :: FormulaTreatment -> a -> a -> a -> a -> a
- data CASL2SubCFOL = CASL2SubCFOL {}
- 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
treatFormula :: FormulaTreatment -> a -> a -> a -> a -> a
a case selector for formula treatment
data CASL2SubCFOL
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
| |
Instances
defaultCASL2SubCFOL :: CASL2SubCFOL
create unique bottoms, sorts with bottom depend on membership and casts in theory sentences.
totalizeSymbType :: SymbType -> SymbType
sortsWithBottom :: FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
totalizeOpSymb :: OP_SYMB -> OP_SYMB
addBottomAlt :: Constraint -> Constraint
argSorts :: Constraint -> Set SORT
totalizeConstraint :: Set SORT -> Constraint -> Constraint
mkNonEmptyAxiomName :: SORT -> String
Make the name for the non empty axiom from s to s' to s''
mkNotDefBotAxiomName :: SORT -> String
Make the name for the not defined bottom axiom
mkTotalityAxiomName :: OP_NAME -> String
Make the name for the totality axiom
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)
botSorts :: (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
find sorts that need a bottom in membership formulas and casts
botFormulaSorts :: FORMULA f -> Set SORT
botTermSorts :: TERM f -> Set SORT