Hets - the Heterogeneous Tool Set

Copyright(c) Zicheng Wang C.Maeder Uni Bremen 2002-2009
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Comorphism)
Safe HaskellNone

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

Documentation

data FormulaTreatment Source #

determine the need for bottom constants

Instances

Show FormulaTreatment Source # 

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

Instances

Show CASL2SubCFOL Source # 

Methods

showsPrec :: Int -> CASL2SubCFOL -> ShowS

show :: CASL2SubCFOL -> String

showList :: [CASL2SubCFOL] -> ShowS

Language CASL2SubCFOL 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 # 

defaultCASL2SubCFOL :: CASL2SubCFOL Source #

create unique bottoms, sorts with bottom depend on membership and casts in theory sentences.

defined :: TermExtension f => Set SORT -> TERM f -> Range -> FORMULA f Source #

encodeSig :: Set SORT -> Sign f e -> Sign f e Source #

Add projections to the signature

mkNonEmptyAxiomName :: SORT -> String Source #

Make the name for the non empty axiom from s to s' to s''

mkNotDefBotAxiomName :: SORT -> String Source #

Make the name for the not defined bottom axiom

mkTotalityAxiomName :: OP_NAME -> String Source #

Make the name for the totality axiom

generateAxioms :: (Ord f, TermExtension f) => Bool -> Set SORT -> Sign f e -> [Named (FORMULA f)] Source #

codeRecord :: TermExtension f => Bool -> Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f) Source #

codeFormula :: Bool -> Set SORT -> FORMULA () -> FORMULA () Source #

codeTerm :: Bool -> Set SORT -> TERM () -> TERM () Source #

botSorts :: (f -> Set SORT) -> Record f (Set SORT) (Set SORT) Source #

find sorts that need a bottom in membership formulas and casts