Copyright	(c) Jonathan von Schroeder DFKI Bremen 2013
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.THFP_P2HasCASL

Description

The embedding comorphism from THFP to HasCASL.

Documentation

data THFP_P2HasCASL Source #

Constructors

THFP_P2HasCASL

Instances

Instances details

Show THFP_P2HasCASL Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods showsPrec :: Int -> THFP_P2HasCASL -> ShowS show :: THFP_P2HasCASL -> String showList :: [THFP_P2HasCASL] -> ShowS
Language THFP_P2HasCASL Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods language_name :: THFP_P2HasCASL -> String Source # description :: THFP_P2HasCASL -> String Source #
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Source #
Instance details Defined in Comorphisms.THFP_P2HasCASL Methods sourceLogic :: THFP_P2HasCASL -> THF Source # sourceSublogic :: THFP_P2HasCASL -> THFSl Source # sourceSublogicLossy :: THFP_P2HasCASL -> THFSl Source # minSourceTheory :: THFP_P2HasCASL -> Maybe (LibName, String) Source # targetLogic :: THFP_P2HasCASL -> HasCASL Source # mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic Source # map_theory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # mapMarkedTheory :: THFP_P2HasCASL -> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source # map_morphism :: THFP_P2HasCASL -> MorphismTHF -> Result Morphism Source # map_sentence :: THFP_P2HasCASL -> SignTHF -> THFFormula -> Result Sentence Source # map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol Source # extractModel :: THFP_P2HasCASL -> SignTHF -> () -> Result (SignTHF, [Named THFFormula]) Source # is_model_transportable :: THFP_P2HasCASL -> Bool Source # has_model_expansion :: THFP_P2HasCASL -> Bool Source # is_weakly_amalgamable :: THFP_P2HasCASL -> Bool Source # constituents :: THFP_P2HasCASL -> [String] Source # isInclusionComorphism :: THFP_P2HasCASL -> Bool Source # rps :: THFP_P2HasCASL -> Bool Source # eps :: THFP_P2HasCASL -> Bool Source # isGTC :: THFP_P2HasCASL -> Bool Source #

reqSubLogicForTHFP :: Sublogic Source #

transTheory :: (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence]) Source #

transNamedFormula :: SignTHF -> Named THFFormula -> Result (Named Sentence) Source #

transFormula :: SignTHF -> THFFormula -> Result Term Source #

transBinaryFormula :: SignTHF -> THFBinaryFormula -> Result Term Source #

transUnitaryFormula :: SignTHF -> THFUnitaryFormula -> Result Term Source #

variable2Term :: THFVariable -> Result Term Source #

variable2VarDecl :: THFVariable -> GenVarDecl Source #

transSymbol :: SymbolTHF -> Result (Set Symbol) Source #

tailType :: Type -> (Type, Maybe Type) Source #

toHCType :: Type -> Type Source #