content: {-# LANGUAGE DeriveDataTypeable #-}
  {- |
  Module      :  ./Propositional/AS_BASIC_Propositional.der.hs
  Description :  Abstract syntax for propositional logic
  Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  luecke@informatik.uni-bremen.de
  Stability   :  experimental
  Portability :  portable
  
  Definition of abstract syntax for propositional logic
  -}
  
  {-
    Ref.
    http://en.wikipedia.org/wiki/Propositional_logic
  -}
  
  module Propositional.AS_BASIC_Propositional
      ( FORMULA (..)             -- datatype for Propositional Formulas
      , BASIC_ITEMS (..)         -- Items of a Basic Spec
      , BASIC_SPEC (..)          -- Basic Spec
      , SYMB_ITEMS (..)          -- List of symbols
      , SYMB (..)                -- Symbols
      , SYMB_MAP_ITEMS (..)      -- Symbol map
      , SYMB_OR_MAP (..)         -- Symbol or symbol map
      , PRED_ITEM (..)           -- Predicates
      , isPrimForm
      ) 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
  
  -- DrIFT command
  {-! global: GetRange !-}
  
  -- | predicates = propotions
  data PRED_ITEM = Pred_item [Id.Token] Id.Range
                 deriving (Show, Typeable, Data)
  
  newtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted BASIC_ITEMS]
                    deriving (Show, Typeable, Data)
  
  data BASIC_ITEMS =
      Pred_decl PRED_ITEM
      | Axiom_items [AS_Anno.Annoted FORMULA]
      -- pos: dots
      deriving (Show, Typeable, Data)
  
  -- | Datatype for propositional formulas
  data FORMULA =
      False_atom Id.Range
      -- pos: "False
    | True_atom 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: "<=>"
      deriving (Show, Eq, Ord, Typeable, Data)
  
  data SYMB_ITEMS = Symb_items [SYMB] Id.Range
                    -- pos: SYMB_KIND, commas
                    deriving (Show, Eq, Ord, Typeable, Data)
  
  newtype SYMB = Symb_id Id.Token
              -- pos: colon
              deriving (Show, Eq, Ord, Typeable, Data)
  
  data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP] Id.Range
                        -- pos: SYMB_KIND, commas
                        deriving (Show, Eq, Ord, Typeable, Data)
  
  data SYMB_OR_MAP = Symb SYMB
                   | Symb_map 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 BASIC_SPEC where
      pretty = printBasicSpec
  instance Pretty SYMB where
      pretty = printSymbol
  instance Pretty SYMB_ITEMS where
      pretty = printSymbItems
  instance Pretty SYMB_MAP_ITEMS where
      pretty = printSymbMapItems
  instance Pretty BASIC_ITEMS where
      pretty = printBasicItems
  instance Pretty SYMB_OR_MAP where
      pretty = printSymbOrMap
  instance Pretty PRED_ITEM where
      pretty = printPredItem
  
  isPrimForm :: FORMULA -> Bool
  isPrimForm f = case f of
          True_atom _ -> True
          False_atom _ -> 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
          _ -> True
    in case frm of
    False_atom _ -> text falseS
    True_atom _ -> 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
  
  sepByArbitrary :: Doc -> [Doc] -> Doc
  sepByArbitrary d = fsep . prepPunctuate (d <> space)
  
  printPredItem :: PRED_ITEM -> Doc
  printPredItem (Pred_item xs _) =
    keyword (propS ++ case xs of
       [_] -> ""
       _ -> "s") <+> ppWithCommas xs
  
  printBasicSpec :: BASIC_SPEC -> Doc
  printBasicSpec (Basic_spec xs) = vcat $ map pretty xs
  
  printBasicItems :: BASIC_ITEMS -> Doc
  printBasicItems (Axiom_items xs) = vcat $ map (addBullet . pretty) xs
  printBasicItems (Pred_decl x) = pretty x
  
  printSymbol :: SYMB -> Doc
  printSymbol (Symb_id sym) = pretty sym
  
  printSymbItems :: SYMB_ITEMS -> Doc
  printSymbItems (Symb_items xs _) = fsep $ map pretty xs
  
  printSymbOrMap :: SYMB_OR_MAP -> Doc
  printSymbOrMap (Symb sym) = pretty sym
  printSymbOrMap (Symb_map source dest _) =
    pretty source <+> mapsto <+> pretty dest
  
  printSymbMapItems :: SYMB_MAP_ITEMS -> Doc
  printSymbMapItems (Symb_map_items xs _) = fsep $ map pretty xs
  