Copyright	(c) Zicheng Wang Liam O'Reilly 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.Logic)
Safe Haskell	None

Comorphisms.CASL2PCFOL

Description

Coding out subsorting (SubPCFOL= -> PCFOL=), following Chap. III:3.1 of the CASL Reference Manual

Synopsis

data CASL2PCFOL = CASL2PCFOL
encodeSig :: Sign f e -> Sign f e
mkInjectivityName :: String -> SORT -> SORT -> String
mkEmbInjName :: SORT -> SORT -> String
mkProjInjName :: SORT -> SORT -> String
mkInjectivity :: (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f
mkInjImpl :: (TERM f -> TERM f) -> TERM f -> TERM f -> FORMULA f
injectTo :: TermExtension f => SORT -> TERM f -> TERM f
projectTo :: TermExtension f => SORT -> TERM f -> TERM f
mkEmbInjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f)
mkProjInjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f)
mkProjName :: SORT -> SORT -> String
mkXExEq :: SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f
mkProjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f)
mkTransAxiomName :: SORT -> SORT -> SORT -> String
mkTransAxiom :: TermExtension f => SORT -> SORT -> SORT -> Named (FORMULA f)
mkIdAxiomName :: SORT -> SORT -> String
mkIdAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f)
generateAxioms :: TermExtension f => Sign f e -> [Named (FORMULA f)]
f2Formula :: TermExtension f => FORMULA f -> FORMULA f
t2Term :: TermExtension f => TERM f -> TERM f

Documentation

data CASL2PCFOL Source #

The identity of the comorphism

Constructors

CASL2PCFOL

Instances

Instances details

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

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

Add injection, projection and membership symbols to a signature

mkInjectivityName :: String -> SORT -> SORT -> String Source #

Make the name for the embedding or projecton injectivity axiom

mkEmbInjName :: SORT -> SORT -> String Source #

Make the name for the embedding injectivity axiom

mkProjInjName :: SORT -> SORT -> String Source #

Make the name for the projection injectivity axiom

mkInjectivity :: (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f Source #

create a quantified injectivity implication

mkInjImpl :: (TERM f -> TERM f) -> TERM f -> TERM f -> FORMULA f Source #

create an injectivity implication over x and y

injectTo :: TermExtension f => SORT -> TERM f -> TERM f Source #

apply injection function

projectTo :: TermExtension f => SORT -> TERM f -> TERM f Source #

apply (a partial) projection function

mkEmbInjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the embedding injectivity axiom from s to s' i.e., forall x,y:s . inj(x)=e=inj(y) => x=e=y

mkProjInjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the projection injectivity axiom from s' to s i.e., forall x,y:s . pr(x)=e=pr(y) => x=e=y

mkProjName :: SORT -> SORT -> String Source #

Make the name for the projection axiom

mkXExEq :: SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f Source #

create a quantified existential equation over x of sort s

mkProjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the projection axiom from s' to s i.e., forall x:s . pr(inj(x))=e=x

mkTransAxiomName :: SORT -> SORT -> SORT -> String Source #

Make the name for the transitivity axiom from s to s' to s''

mkTransAxiom :: TermExtension f => SORT -> SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the transitivity axiom from s to s' to s'' i.e., forall x:s . inj(inj(x))=e=inj(x)

mkIdAxiomName :: SORT -> SORT -> String Source #

Make the name for the identity axiom from s to s'

mkIdAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f) Source #

Make the named sentence for the identity axiom from s to s' i.e., forall x:s . inj(inj(x))=e=x

generateAxioms :: TermExtension f => Sign f e -> [Named (FORMULA f)] Source #

f2Formula :: TermExtension f => FORMULA f -> FORMULA f Source #

t2Term :: TermExtension f => TERM f -> TERM f Source #