8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias Tristl{- |

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias TristlModule : $Header$

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias TristlDescription : A formula wrapper from formulae defined in SoftFOL.Sign to data Formula defined in Common.Normalization

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias TristlCopyright : (c) Immanuel Normann, Uni Bremen 2007

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias TristlLicense : GPLv2 or higher, see LICENSE.txt

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias Tristl

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias TristlMaintainer : inormann@jacobs-university.de

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias TristlStability : provisional

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias TristlPortability : portable

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias Tristl-}

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias Tristlmodule Search.SPASS.FormulaWrapper where

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias Tristl

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias Tristl

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias Tristlimport Search.Common.Data

8a0678903b06fbd3c9acf4f4cd137482e1dcd2aaMatthias Tristlimport SoftFOL.Sign

type SpassConst = SPIdentifier

wrapTerm :: SPTerm -> Formula (Constant SpassConst) SPIdentifier

wrapTerm (SPQuantTerm q vars f) = Binder (wrapQConst q) (map wrapVar vars) (wrapTerm f)

wrapTerm (SPComplexTerm SPImplied args) = wrapTerm (SPComplexTerm SPImplies (reverse args)) -- ist das die Semantik von implied?!?

wrapTerm (SPComplexTerm f args) =

case f

of (SPCustomSymbol s) -> Var s (map wrapTerm args)

_ -> Const (wrapConst f) (map wrapTerm args)

wrapTerm (SPSimpleTerm c) =

case c

of (SPCustomSymbol s) -> Var s []

_ -> Const (wrapConst c) []

wrapConst :: SPSymbol -> Constant SpassConst

wrapConst SPEqual = Equal

wrapConst SPTrue = TrueAtom

wrapConst SPFalse = FalseAtom

wrapConst SPOr = Or

wrapConst SPAnd = And

wrapConst SPNot = Not

wrapConst SPImplies = Imp

wrapConst SPEquiv = Eqv

--wrapConst SPXor = Xor

wrapQConst :: SPQuantSym -> Constant SpassConst

wrapQConst SPForall = All

wrapQConst SPExists = Some

wrapQConst (SPCustomQuantSym q) = LogicDependent q

wrapVar :: SPTerm -> SPIdentifier

wrapVar (SPSimpleTerm (SPCustomSymbol v)) = v -- only single variable can be bound

wrapVar v = error (show v ++ " is not allowed as bound variable")