{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./QBF/AS_BASIC_QBF.der.hs
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
