Copyright	(c) Mingyi Liu, Till Mossakowski, Uni Bremen 2004-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

CASL.CCC.TermFormula

Description

Auxiliary functions on terms and formulas

Synopsis

Documentation

unsortedTerm :: TERM f -> TERM f

the sorted term is always ignored

isExQuanti :: FORMULA f -> Bool

check whether it exist a (unique)existent quantification

isMembership :: FORMULA f -> Bool

check whether it contains a membership formula

containDef :: FORMULA f -> Bool

check whether it contains a definedness formula

containNeg :: FORMULA f -> Bool

check whether it contains a negation

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

isVar :: TERM t -> Bool

check whether it is a Variable

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

extract all variables of a term

arguOfTerm :: TERM f -> [TERM f]

extract all arguments of a term

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

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

patternsOfAxiom :: FORMULA f -> [TERM f]

get the patterns of a axiom

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

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

split the axiom into condition and rest axiom

conditionAxiom :: FORMULA f -> FORMULA f

get the premise of a formula, without implication return true

restAxiom :: FORMULA f -> FORMULA f

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

resultAxiom :: FORMULA f -> FORMULA f

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

resultTerm :: FORMULA f -> TERM f

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]))

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

mkSortedTerm :: SORT -> TERM f -> SORT -> TERM f

minSortTerm :: TermExtension f => TERM f -> TERM f

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

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]))

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

extract defined subsorts

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

create the obligations for subsorts

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

extract the leading symbol from a formula

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

extract the leading symbol with the range from a formula

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

extract the leading term or predication from a formula

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

extract the leading symbol from a term or a formula

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

replaces variables by terms in a term or formula

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

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

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

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

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

check whether two terms are the terms of same application symbol

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