hets/Propositional/Sublogic.hs

	Sublogic.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Propositional/Sublogic.hs
Description :  Sublogics 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 :  non-portable (imports Logic.Logic)

Sublogics for Propositional Logic
-}

{-
  Ref.

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

  Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
  What is a Logic?.
  In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
  2005.
-}

module Propositional.Sublogic
    (
     sl_basic_spec                  -- determine sublogic for basic spec
    , PropFormulae (..)             -- types of propositional formulae
    , PropSL (..)                   -- sublogics for propositional logic
    , sublogics_max                 -- join of sublogics
    , top                           -- Propositional
    , bottom                        -- Horn
    , sublogics_all                 -- all sublogics
    , sublogics_name                -- name of sublogics
    , sl_sig                        -- sublogic for a signature
    , sl_form                       -- sublogic for a formula
    , sl_sym                        -- sublogic for symbols
    , sl_symit                      -- sublogic for symbol items
    , sl_mor                        -- sublogic for morphisms
    , sl_symmap                     -- sublogic for symbol map items
    , prSymbolM                     -- projection of symbols
    , prSig                         -- projections of signatures
    , prMor                         -- projections of morphisms
    , prSymMapM                     -- projections of symbol maps
    , prSymM                        -- projections of SYMB_ITEMS
    , prFormulaM                    -- projections of formulae
    , prBasicSpec                   -- projections of basic specs
    , isProp
    , isHC
    )
    where

import Data.Data

import qualified Propositional.Tools as Tools
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC

import qualified Propositional.Sign as Sign
import qualified Propositional.Symbol as Symbol
import qualified Propositional.Morphism as Morphism

import qualified Common.Lib.State as State
import qualified Common.AS_Annotation as AS_Anno

{- -----------------------------------------------------------------------------
datatypes                                                                 --
----------------------------------------------------------------------------- -}

-- | types of propositional formulae
data PropFormulae = PlainFormula      -- Formula without structural constraints
                  | HornClause        -- Horn Clause Formulae
                  deriving (Show, Eq, Ord, Typeable, Data)

-- | sublogics for propositional logic
data PropSL = PropSL
    {
      format :: PropFormulae     -- Structural restrictions
    } deriving (Show, Eq, Ord, Typeable, Data)

isProp :: PropSL -> Bool
isProp sl = format sl == PlainFormula

isHC :: PropSL -> Bool
isHC sl = format sl == HornClause

-- | comparison of sublogics
compareLE :: PropSL -> PropSL -> Bool
compareLE p1 p2 =
    let f1 = format p1
        f2 = format p2
    in
      case (f1, f2) of
        (_, PlainFormula) -> True
        (HornClause, HornClause) -> True
        (_, HornClause) -> False

{- ----------------------------------------------------------------------------
Special elements in the Lattice of logics                                --
---------------------------------------------------------------------------- -}

top :: PropSL
top = PropSL PlainFormula

bottom :: PropSL
bottom = PropSL HornClause

need_PF :: PropSL
need_PF = bottom { format = PlainFormula }

{- -----------------------------------------------------------------------------
join and max                                                              --
----------------------------------------------------------------------------- -}

sublogics_join :: (PropFormulae -> PropFormulae -> PropFormulae)
                  -> PropSL -> PropSL -> PropSL
sublogics_join pfF a b = PropSL
                         {
                           format = pfF (format a) (format b)
                         }

joinType :: PropFormulae -> PropFormulae -> PropFormulae
joinType HornClause HornClause = HornClause
joinType _ _ = PlainFormula

sublogics_max :: PropSL -> PropSL -> PropSL
sublogics_max = sublogics_join joinType

{- -----------------------------------------------------------------------------
Helpers                                                                   --
----------------------------------------------------------------------------- -}

-- compute sublogics from a list of sublogics
--
comp_list :: [PropSL] -> PropSL
comp_list = foldl sublogics_max bottom

{- ----------------------------------------------------------------------------
Functions to compute minimal sublogic for a given element, these work    --
by recursing into all subelements                                        --
---------------------------------------------------------------------------- -}

-- | determines the sublogic for symbol map items
sl_symmap :: PropSL -> AS_BASIC.SYMB_MAP_ITEMS -> PropSL
sl_symmap ps _ = ps

-- | determines the sublogic for a morphism
sl_mor :: PropSL -> Morphism.Morphism -> PropSL
sl_mor ps _ = ps

-- | determines the sublogic for a Signature
sl_sig :: PropSL -> Sign.Sign -> PropSL
sl_sig ps _ = ps

-- | determines the sublogic for Symbol items
sl_symit :: PropSL -> AS_BASIC.SYMB_ITEMS -> PropSL
sl_symit ps _ = ps

-- | determines the sublogic for symbols
sl_sym :: PropSL -> Symbol.Symbol -> PropSL
sl_sym ps _ = ps

-- | determines sublogic for formula
sl_form :: PropSL -> AS_BASIC.FORMULA -> PropSL
sl_form ps f = sl_fl_form ps $ Tools.flatten f

-- | determines sublogic for flattened formula
sl_fl_form :: PropSL -> [AS_BASIC.FORMULA] -> PropSL
sl_fl_form ps f = foldl sublogics_max ps
  $ map (\ x -> State.evalState (ana_form ps x) 0) f

-- analysis of single "clauses"
ana_form :: PropSL -> AS_BASIC.FORMULA -> State.State Int PropSL
ana_form ps f =
    case f of
      AS_BASIC.Conjunction l _ ->
          do
            st <- State.get
            return $ sublogics_max need_PF $ comp_list $ map
              (\ x -> State.evalState (ana_form ps x) (st + 1)) l
      AS_BASIC.Implication l m _ ->
          do
             st <- State.get
             let analyze = sublogics_max need_PF $ sublogics_max
                   ((\ x -> State.evalState (ana_form ps x) (st + 1)) l)
                   ((\ x -> State.evalState (ana_form ps x) (st + 1)) m)
             return $
                    if st < 1 && format ps == HornClause && checkHornPos l m
                    then ps else analyze
      AS_BASIC.Equivalence l m _ ->
           do
             st <- State.get
             return $ sublogics_max need_PF $ sublogics_max
               ((\ x -> State.evalState (ana_form ps x) (st + 1)) l)
               ((\ x -> State.evalState (ana_form ps x) (st + 1)) m)
      AS_BASIC.Negation l _ ->
          if isLiteral l
          then return ps
          else
              do
                st <- State.get
                return $ (\ x -> State.evalState (ana_form ps x) (st + 1)) l
      AS_BASIC.Disjunction l _ ->
                    let lprime = concatMap Tools.flattenDis l in
                    if all isLiteral lprime
                    then return $
                          if moreThanNLit lprime 1
                          then sublogics_max need_PF ps else ps
                    else
                        do
                          st <- State.get
                          return $ sublogics_max need_PF $ comp_list $ map
                            (\ x -> State.evalState (ana_form ps x) (st + 1))
                                      lprime
      AS_BASIC.True_atom _ -> return ps
      AS_BASIC.False_atom _ -> return ps
      AS_BASIC.Predication _ -> return ps

moreThanNLit :: [AS_BASIC.FORMULA] -> Int -> Bool
moreThanNLit form n = foldl (\ y x -> if x then y + 1 else y) 0
  (map isPosLiteral form) > n

-- determines wheter a Formula is a literal
isLiteral :: AS_BASIC.FORMULA -> Bool
isLiteral (AS_BASIC.Predication _) = True
isLiteral (AS_BASIC.Negation (AS_BASIC.Predication _) _ ) = True
isLiteral (AS_BASIC.Negation _ _) = False
isLiteral (AS_BASIC.Conjunction _ _) = False
isLiteral (AS_BASIC.Implication {}) = False
isLiteral (AS_BASIC.Equivalence {}) = False
isLiteral (AS_BASIC.Disjunction _ _) = False
isLiteral (AS_BASIC.True_atom _ ) = True
isLiteral (AS_BASIC.False_atom _) = True

-- determines wheter a Formula is a positive literal
isPosLiteral :: AS_BASIC.FORMULA -> Bool
isPosLiteral (AS_BASIC.Predication _) = True
isPosLiteral (AS_BASIC.Negation _ _) = False
isPosLiteral (AS_BASIC.Conjunction _ _) = False
isPosLiteral (AS_BASIC.Implication {}) = False
isPosLiteral (AS_BASIC.Equivalence {}) = False
isPosLiteral (AS_BASIC.Disjunction _ _) = False
isPosLiteral (AS_BASIC.True_atom _ ) = True
isPosLiteral (AS_BASIC.False_atom _) = True

-- | determines subloig for basic items
sl_basic_items :: PropSL -> AS_BASIC.BASIC_ITEMS -> PropSL
sl_basic_items ps bi =
    case bi of
      AS_BASIC.Pred_decl _ -> ps
      AS_BASIC.Axiom_items xs -> comp_list $ map (sl_form ps . AS_Anno.item) xs

-- | determines sublogic for basic spec
sl_basic_spec :: PropSL -> AS_BASIC.BASIC_SPEC -> PropSL
sl_basic_spec ps (AS_BASIC.Basic_spec spec) =
    comp_list $ map (sl_basic_items ps . AS_Anno.item) spec

-- | all sublogics
sublogics_all :: [PropSL]
sublogics_all =
    [PropSL
     {
       format = HornClause
     }
    , PropSL
     {
       format = PlainFormula
     }
    ]

{- -----------------------------------------------------------------------------
Conversion functions to String                                            --
----------------------------------------------------------------------------- -}

sublogics_name :: PropSL -> String
sublogics_name f = case format f of
      HornClause -> "HornClause"
      PlainFormula -> "Prop"

{- -----------------------------------------------------------------------------
Projections to sublogics                                                  --
----------------------------------------------------------------------------- -}

prSymbolM :: PropSL -> Symbol.Symbol -> Maybe Symbol.Symbol
prSymbolM _ = Just

prSig :: PropSL -> Sign.Sign -> Sign.Sign
prSig _ sig = sig

prMor :: PropSL -> Morphism.Morphism -> Morphism.Morphism
prMor _ mor = mor

prSymMapM :: PropSL
          -> AS_BASIC.SYMB_MAP_ITEMS
          -> Maybe AS_BASIC.SYMB_MAP_ITEMS
prSymMapM _ = Just

prSymM :: PropSL -> AS_BASIC.SYMB_ITEMS -> Maybe AS_BASIC.SYMB_ITEMS
prSymM _ = Just

-- keep an element if its computed sublogic is in the given sublogic
--

prFormulaM :: PropSL -> AS_BASIC.FORMULA -> Maybe AS_BASIC.FORMULA
prFormulaM sl form
           | compareLE (sl_form bottom form) sl = Just form
           | otherwise = Nothing

prPredItem :: PropSL -> AS_BASIC.PRED_ITEM -> AS_BASIC.PRED_ITEM
prPredItem _ prI = prI

prBASIC_items :: PropSL -> AS_BASIC.BASIC_ITEMS -> AS_BASIC.BASIC_ITEMS
prBASIC_items pSL bI =
    case bI of
      AS_BASIC.Pred_decl pI -> AS_BASIC.Pred_decl $ prPredItem pSL pI
      AS_BASIC.Axiom_items aIS -> AS_BASIC.Axiom_items $ concatMap mapH aIS
    where
      mapH :: AS_Anno.Annoted AS_BASIC.FORMULA
           -> [AS_Anno.Annoted AS_BASIC.FORMULA]
      mapH annoForm = let formP = prFormulaM pSL $ AS_Anno.item annoForm in
                      case formP of
                        Nothing -> []
                        Just f -> [ AS_Anno.Annoted
                                   {
                                     AS_Anno.item = f
                                   , AS_Anno.opt_pos = AS_Anno.opt_pos annoForm
                                   , AS_Anno.l_annos = AS_Anno.l_annos annoForm
                                   , AS_Anno.r_annos = AS_Anno.r_annos annoForm
                                   }
                                   ]

prBasicSpec :: PropSL -> AS_BASIC.BASIC_SPEC -> AS_BASIC.BASIC_SPEC
prBasicSpec pSL (AS_BASIC.Basic_spec bS) =
    AS_BASIC.Basic_spec $ map mapH bS
    where
      mapH :: AS_Anno.Annoted AS_BASIC.BASIC_ITEMS
           -> AS_Anno.Annoted AS_BASIC.BASIC_ITEMS
      mapH aBI = AS_Anno.Annoted
                 {
                   AS_Anno.item = prBASIC_items pSL $ AS_Anno.item aBI
                 , AS_Anno.opt_pos = AS_Anno.opt_pos aBI
                 , AS_Anno.l_annos = AS_Anno.l_annos aBI
                 , AS_Anno.r_annos = AS_Anno.r_annos aBI
                 }

checkHornPos :: AS_BASIC.FORMULA -> AS_BASIC.FORMULA -> Bool
checkHornPos fc fl =
    case fc of
      AS_BASIC.Conjunction _ _ -> all isPosLiteral $ Tools.flatten fc
      _ -> False
    &&
    isPosLiteral fl