Hets - the Heterogeneous Tool Set

Copyright(c) Mingyi Liu Till Mossakowski Uni Bremen 2004-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CASL.CCC.TermFormula

Description

Auxiliary functions on terms and formulas

Synopsis

Documentation

unsortedTerm :: TERM f -> TERM f Source #

the sorted term is always ignored

isExQuanti :: FORMULA f -> Bool Source #

check whether it exist a (unique)existent quantification

isMembership :: FORMULA f -> Bool Source #

check whether it contains a membership formula

containDef :: FORMULA f -> Bool Source #

check whether it contains a definedness formula

containNeg :: FORMULA f -> Bool Source #

check whether it contains a negation

domainDef :: FORMULA f -> Maybe (TERM f, FORMULA f) Source #

isVar :: TERM t -> Bool Source #

check whether it is a Variable

varOfTerm :: Ord f => TERM f -> [TERM f] Source #

extract all variables of a term

arguOfTerm :: TERM f -> [TERM f] Source #

extract all arguments of a term

nullId :: ((Id, Int), [TERM f]) Source #

topIdOfTerm :: TERM f -> ((Id, Int), [TERM f]) Source #

patternsOfAxiom :: FORMULA f -> [TERM f] Source #

get the patterns of a axiom

topIdOfAxiom :: FORMULA f -> ((Id, Int), [TERM f]) Source #

splitAxiom :: FORMULA f -> ([FORMULA f], FORMULA f) Source #

split the axiom into condition and rest axiom

conditionAxiom :: FORMULA f -> FORMULA f Source #

get the premise of a formula, without implication return true

restAxiom :: FORMULA f -> FORMULA f Source #

get the conclusion of a formula, without implication return the formula

resultAxiom :: FORMULA f -> FORMULA f Source #

get right hand side of an equivalence, without equivalence return true

resultTerm :: FORMULA f -> TERM f Source #

get right hand side of an equation, without equation return dummy term

getSubstForm :: (FormExtension f, TermExtension f, Ord f) => Sign f e -> FORMULA f -> FORMULA f -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])) Source #

mkCast :: SORT -> TERM f -> SORT -> (TERM f, [FORMULA f]) Source #

mkSTerm :: TermExtension f => Sign f e -> SORT -> TERM f -> (TERM f, [FORMULA f]) Source #

getSubst :: (FormExtension f, TermExtension f, Ord f) => Sign f e -> ([TERM f], Set VAR) -> ([TERM f], Set VAR) -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])) Source #

isSubsortDef :: FORMULA f -> Maybe (SORT, VAR_DECL, FORMULA f) Source #

extract defined subsorts

infoSubsorts :: Set SORT -> [(SORT, VAR_DECL, FORMULA f)] -> [FORMULA f] Source #

create the obligations for subsorts

leadingSym :: GetRange f => FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB) Source #

extract the leading symbol from a formula

leadingSymPos :: GetRange f => FORMULA f -> (Maybe (Either (TERM f) (FORMULA f)), Range) Source #

extract the leading symbol with the range from a formula

leadingTermPredication :: GetRange f => FORMULA f -> Maybe (Either (TERM f) (FORMULA f)) Source #

extract the leading term or predication from a formula

extractLeadingSymb :: Either (TERM f) (FORMULA f) -> Either OP_SYMB PRED_SYMB Source #

extract the leading symbol from a term or a formula

substRec :: Eq f => [(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f) Source #

replaces variables by terms in a term or formula

substitute :: Eq f => [(TERM f, TERM f)] -> TERM f -> TERM f Source #

substiF :: Eq f => [(TERM f, TERM f)] -> FORMULA f -> FORMULA f Source #

sameOpTypes :: Sign f e -> OP_TYPE -> OP_TYPE -> Bool Source #

sameOpSymbs :: Sign f e -> OP_SYMB -> OP_SYMB -> Bool Source #

sameOpsApp :: Sign f e -> TERM f -> TERM f -> Bool Source #

check whether two terms are the terms of same application symbol

eqPattern :: Sign f e -> TERM f -> TERM f -> Bool Source #