| 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.
- 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
transTheory :: (Env, [Named Sentence]) -> Result (SignTHF, [Named THFFormula])
transTypeInfo :: TypeInfo -> Constant -> Result TypeInfo
transRawKind :: RawKind -> Result Kind
type IdConstantMap = Map Id Constant
transType :: IdConstantMap -> Type -> Result Type
isUnitType :: Type -> Bool
mkSymbolMap :: TypeMap -> ConstMap -> Result SymbolMap
transNamedSentence :: Maybe IdConstantMap -> IdSet -> Env -> Named Sentence -> Result (Named THFFormula, IdSet)
transTerm :: Env -> IdConstantMap -> IdSet -> Term -> Result (THFLogicFormula, IdSet)
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])
decompose an ApplTerm into an application of an operation and a
list of arguments
transLamdaTerm :: Env -> IdConstantMap -> IdSet -> [Term] -> Partiality -> Term -> Range -> Result (THFLogicFormula, IdSet)
transQuantifiedTerm :: Env -> IdConstantMap -> IdSet -> Quantifier -> [GenVarDecl] -> Term -> Range -> Result (THFQuantifiedFormula, IdSet)
transVarDecl :: IdConstantMap -> VarDecl -> Result THFVariable
genTuple :: [Type] -> Result THFBinaryType