{-# LANGUAGE DeriveDataTypeable #-}

{- |

Module : $Header$

Description : Abstract syntax for propositional logic extended with QBFs

Copyright : (c) Jonathan von Schroeder, DFKI GmbH 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : <jonathan.von_schroeder@dfki.de>

Stability : experimental

Portability : portable

Definition of abstract syntax for propositional logic extended with QBFs

Ref.

<http://en.wikipedia.org/wiki/Propositional_logic>

<http://www.voronkov.com/lics.cgi>

-}

module QBF.AS_BASIC_QBF

( FORMULA (..) -- datatype for Propositional Formulas

, BASICITEMS (..) -- Items of a Basic Spec

, BASICSPEC (..) -- Basic Spec

, SYMBITEMS (..) -- List of symbols

, SYMB (..) -- Symbols

, SYMBMAPITEMS (..) -- Symbol map

, SYMBORMAP (..) -- Symbol or symbol map

, PREDITEM (..) -- Predicates

, isPrimForm

, ID (..)

) where

import Common.Id as Id

import Common.Doc

import Common.DocUtils

import Common.Keywords

import Common.AS_Annotation as AS_Anno

import Data.Data

import Data.Maybe (isJust)

import qualified Data.List as List

-- DrIFT command

{-! global: GetRange !-}

-- | predicates = propositions

data PREDITEM = PredItem [Id.Token] Id.Range

deriving (Show, Typeable, Data)

newtype BASICSPEC = BasicSpec [AS_Anno.Annoted BASICITEMS]

deriving (Show, Typeable, Data)

data BASICITEMS =

PredDecl PREDITEM

| AxiomItems [AS_Anno.Annoted FORMULA]

-- pos: dots

deriving (Show, Typeable, Data)

-- | Datatype for QBF formulas

data FORMULA =

FalseAtom Id.Range

-- pos: "False

| TrueAtom Id.Range

-- pos: "True"

| Predication Id.Token

-- pos: Propositional Identifiers

| Negation FORMULA Id.Range

-- pos: not

| Conjunction [FORMULA] Id.Range

-- pos: "/\"s

| Disjunction [FORMULA] Id.Range

-- pos: "\/"s

| Implication FORMULA FORMULA Id.Range

-- pos: "=>"

| Equivalence FORMULA FORMULA Id.Range

-- pos: "<=>"

| ForAll [Id.Token] FORMULA Id.Range

| Exists [Id.Token] FORMULA Id.Range

deriving (Show, Ord, Typeable, Data)

data ID = ID Id.Token (Maybe Id.Token) deriving (Typeable, Data)

instance Eq ID where

ID t1 (Just t2) == ID t3 (Just t4) =

((t1 == t3) && (t2 == t4))

|| ((t2 == t3) && (t1 == t4))

ID t1 Nothing == ID t2 t3 = (t1 == t2) || (Just t1 == t3)

ID _ (Just _) == ID _ Nothing = False

{- two QBFs are equivalent if bound variables

can be renamed such that the QBFs are equal -}

qbfMakeEqual :: Maybe [ID] -> FORMULA -> [Id.Token]

-> FORMULA -> [Id.Token] -> Maybe [ID]

qbfMakeEqual (Just ids) f ts f1 ts1 = if length ts /= length ts1 then

Nothing

else case (f, f1) of

(Predication t, Predication t1)

| t == t1 -> Just ids

| t `elem` ts && t1 `elem` ts1 -> let tt1 = ID t (Just t1) in

if tt1 `elem` ids then

Just ids

else

if ID t Nothing `notElem` ids && ID t1 Nothing `notElem` ids then

Just (tt1 : ids)

else

Nothing

| otherwise -> Nothing

(Negation f_ _, Negation f1_ _) -> qbfMakeEqual (Just ids) f_ ts f1_ ts1

(Conjunction (f_ : fs) _, Conjunction (f1_ : fs1) _) ->

if length fs /= length fs1 then Nothing else

case r of

Nothing -> Nothing

_ -> qbfMakeEqual r

(Conjunction fs nullRange) ts

(Conjunction fs1 nullRange) ts1

where

r = qbfMakeEqual (Just ids) f_ ts f1_ ts1

(Disjunction fs r, Disjunction fs1 r1) -> qbfMakeEqual (Just ids)

(Conjunction fs r) ts (Conjunction fs1 r1) ts1

(Implication f_ f1_ _, Implication f2 f3 _) -> case r of

Nothing -> Nothing

_ -> qbfMakeEqual r f1_ ts f3 ts1

where

r = qbfMakeEqual (Just ids) f_ ts f2 ts1

(Equivalence f_ f1_ r1, Equivalence f2 f3 _) -> qbfMakeEqual (Just ids)

(Implication f_ f1_ r1) ts

(Implication f2 f3 r1) ts1

(ForAll ts_ f_ _, ForAll ts1_ f1_ _) -> case r of

Nothing -> Nothing

(Just ids_) -> Just (ids ++ filter (\ (ID x my) ->

let Just y = my in

(x `elem` ts_ && y `notElem` ts1_) ||

(x `elem` ts1_ && y `notElem` ts_)) d)

where

d = ids_ List.\\ ids

where

r = qbfMakeEqual (Just ids) f_ (ts ++ ts_) f1_ (ts1 ++ ts1_)

(Exists ts_ f_ r, Exists ts1_ f1_ r1) -> qbfMakeEqual (Just ids)

(Exists ts_ f_ r) ts

(Exists ts1_ f1_ r1) ts1

(_1, _2) -> Nothing

qbfMakeEqual Nothing _ _ _ _ = Nothing

-- ranges are always equal (see Common/Id.hs) - thus they can be ignored

instance Eq FORMULA where

FalseAtom _ == FalseAtom _ = True

TrueAtom _ == TrueAtom _ = True

Predication t == Predication t1 = t == t1

Negation f _ == Negation f1 _ = f == f1

Conjunction xs _ == Conjunction xs1 _ = xs == xs1

Disjunction xs _ == Disjunction xs1 _ = xs == xs1

Implication f f1 _ == Implication f2 f3 _ = (f == f2) && (f1 == f3)

Equivalence f f1 _ == Equivalence f2 f3 _ = (f == f2) && (f1 == f3)

ForAll ts f _ == ForAll ts1 f1 _ = isJust (qbfMakeEqual (Just []) f ts f1 ts1)

Exists ts f _ == Exists ts1 f1 _ = isJust (qbfMakeEqual (Just []) f ts f1 ts1)

_ == _ = False

data SYMBITEMS = SymbItems [SYMB] Id.Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq, Ord, Typeable, Data)

newtype SYMB = SymbId Id.Token

-- pos: colon

deriving (Show, Eq, Ord, Typeable, Data)

data SYMBMAPITEMS = SymbMapItems [SYMBORMAP] Id.Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq, Ord, Typeable, Data)

data SYMBORMAP = Symb SYMB

| SymbMap SYMB SYMB Id.Range

-- pos: "|->"

deriving (Show, Eq, Ord, Typeable, Data)

-- All about pretty printing we chose the easy way here :)

instance Pretty FORMULA where

pretty = printFormula

instance Pretty BASICSPEC where

pretty = printBasicSpec

instance Pretty SYMB where

pretty = printSymbol

instance Pretty SYMBITEMS where

pretty = printSymbItems

instance Pretty SYMBMAPITEMS where

pretty = printSymbMapItems

instance Pretty BASICITEMS where

pretty = printBasicItems

instance Pretty SYMBORMAP where

pretty = printSymbOrMap

instance Pretty PREDITEM where

pretty = printPredItem

isPrimForm :: FORMULA -> Bool

isPrimForm f = case f of

TrueAtom _ -> True

FalseAtom _ -> True

Predication _ -> True

Negation _ _ -> True

_ -> False

-- Pretty printing for formulas

printFormula :: FORMULA -> Doc

printFormula frm =

let ppf p f = (if p f then id else parens) $ printFormula f

isJunctForm f = case f of

Implication {} -> False

Equivalence {} -> False

ForAll {} -> False

Exists {} -> False

_ -> True

in case frm of

FalseAtom _ -> text falseS

TrueAtom _ -> text trueS

Predication x -> pretty x

Negation f _ -> notDoc <+> ppf isPrimForm f

Conjunction xs _ -> sepByArbitrary andDoc $ map (ppf isPrimForm) xs

Disjunction xs _ -> sepByArbitrary orDoc $ map (ppf isPrimForm) xs

Implication x y _ -> ppf isJunctForm x <+> implies <+> ppf isJunctForm y

Equivalence x y _ -> ppf isJunctForm x <+> equiv <+> ppf isJunctForm y

ForAll xs y _ -> forallDoc <+> sepByArbitrary comma (map pretty xs)

<+> space

<+> ppf isJunctForm y

Exists xs y _ -> exists <+> sepByArbitrary comma (map pretty xs)

<+> space

<+> ppf isJunctForm y

sepByArbitrary :: Doc -> [Doc] -> Doc

sepByArbitrary d = fsep . prepPunctuate (d <> space)

printPredItem :: PREDITEM -> Doc

printPredItem (PredItem xs _) = fsep $ map pretty xs

printBasicSpec :: BASICSPEC -> Doc

printBasicSpec (BasicSpec xs) = vcat $ map pretty xs

printBasicItems :: BASICITEMS -> Doc

printBasicItems (AxiomItems xs) = vcat $ map pretty xs

printBasicItems (PredDecl x) = pretty x

printSymbol :: SYMB -> Doc

printSymbol (SymbId sym) = pretty sym

printSymbItems :: SYMBITEMS -> Doc

printSymbItems (SymbItems xs _) = fsep $ map pretty xs

printSymbOrMap :: SYMBORMAP -> Doc

printSymbOrMap (Symb sym) = pretty sym

printSymbOrMap (SymbMap source dest _) =

pretty source <+> mapsto <+> pretty dest

printSymbMapItems :: SYMBMAPITEMS -> Doc

printSymbMapItems (SymbMapItems xs _) = fsep $ map pretty xs