Copyright	(c) A. Tsogias DFKI Bremen 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Alexis.Tsogias@dfki.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.HasCASL2THFP_P

Description

The embedding comorphism from HasCASL to THFP_P.

Synopsis

data HasCASL2THFP_P = HasCASL2THFP_P
reqSubLogicForTHFP :: Sublogic
transTheory :: (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula])
transTypeMap :: TypeMap -> Result (TypeMap, Map Id Constant)
transTypeInfo :: TypeInfo -> Constant -> Result TypeInfo
transRawKind :: RawKind -> Result Kind
transAssumps :: Assumps -> Map Id Constant -> Result ConstMap
type IdConstantMap = Map Id Constant
genIdConstantMap :: Env -> Result IdConstantMap
transType :: IdConstantMap -> Type -> Result Type
isUnitType :: Type -> Bool
insLast :: Type -> Type -> Type
mkSymbolMap :: TypeMap -> ConstMap -> Result SymbolMap
typeInfoToSymbol :: TypeInfo -> SymbolTHF
constInfoToSymbol :: ConstInfo -> SymbolTHF
transSymbol :: Env -> Symbol -> Result (Set SymbolTHF)
transNamedSentence :: Maybe IdConstantMap -> IdSet -> Env -> Named Sentence -> Result (Named THFFormula, IdSet)
getFormulaRole :: Named Sentence -> FormulaRole
transTerm :: Env -> IdConstantMap -> IdSet -> Term -> Result (THFLogicFormula, IdSet)
redTypedTerm :: Term -> TypeQual -> Type -> Range -> Result Term
transQualOp :: Env -> IdSet -> OpBrand -> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Result (Constant, IdSet)
transApplTerm :: Env -> IdConstantMap -> IdSet -> Term -> Term -> Range -> Result (THFLogicFormula, IdSet)
myGetAppl :: Term -> Maybe (Term, Id, [Term])
transLamdaTerm :: Env -> IdConstantMap -> IdSet -> [Term] -> Partiality -> Term -> Range -> Result (THFLogicFormula, IdSet)
transQuantifiedTerm :: Env -> IdConstantMap -> IdSet -> Quantifier -> [GenVarDecl] -> Term -> Range -> Result (THFQuantifiedFormula, IdSet)
transGenVatDecl :: IdConstantMap -> GenVarDecl -> Result THFVariable
transVarDecl :: IdConstantMap -> VarDecl -> Result THFVariable
genTuple :: [Type] -> Result THFBinaryType
lfToUf :: THFLogicFormula -> THFUnitaryFormula
type IdSet = Set Id
myFmap :: (a -> b) -> Result (a, IdSet) -> Result (b, IdSet)

Documentation

data HasCASL2THFP_P Source #

The identity of the comorphism

Constructors

HasCASL2THFP_P

Instances

Instances details

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