-----------------------------------------------------------------------------
-- Copyright 2014, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- Utilities for the logic domain
--
-----------------------------------------------------------------------------
--  $Id: Utils.hs 6548 2014-05-16 10:34:18Z bastiaan $

module Domain.Logic.Utils
   ( propositionalId, makeSimpleRule
     -- groups of rules
   , groupAbsorption, groupAssociativity, groupCommutativity, groupDeMorgan
   , groupDistribution, groupIdempotency
     -- other utility functions
   , makeInvRule, makeInvRuleWithUse
   , collect, andView, orView, eqView
   , (===), (==>), (<=>)
   ) where

import Domain.Logic.Formula
import Ideas.Common.Library

propositionalId :: Id
propositionalId = newId "logic.propositional"

makeSimpleRule :: String -> (a -> Maybe a) -> Rule a
makeSimpleRule s = makeRule (propositionalId # s)

-----------------------------------------------------------------------------
-- Groups of rules

groupAbsorption, groupAssociativity, groupCommutativity, groupDeMorgan,
   groupDistribution, groupIdempotency :: Id
groupAbsorption    = makeGroup "Absorption"
groupAssociativity = makeGroup "Associativity"
groupCommutativity = makeGroup "Commutativity"
groupDeMorgan      = makeGroup "DeMorgan"
groupDistribution  = makeGroup "Distribution"
groupIdempotency   = makeGroup "Idempotency"

makeGroup :: String -> Id
makeGroup s = describe "Group of logic rules" (propositionalId # s)

-----------------------------------------------------------------------------
-- Inverse of a rule

makeInvRule :: IsId n => (a -> a -> Bool) -> n -> Rule a -> Rule a
makeInvRule sim name r =
   addRecognizerBool eq $ setBuggy (isBuggy r) $ makeRule name (const Nothing)
 where
   eq a b = any (sim a) (applyAll r b)

makeInvRuleWithUse :: (IsTerm a, IsTerm b, IsId n, Show a)
                => (Context a -> Context a -> Bool) -> n -> Rule b -> Rule (Context a)
makeInvRuleWithUse sim name r =
   addRecognizerBool eq $ setBuggy (isBuggy r) $ makeRule name (const Nothing)
 where
   eq a b = any (sim a) (applyAll (somewhere (use r)) b)

collect :: View a (a, a) -> Isomorphism a [a]
collect v = f <-> g
 where
   f x = maybe [x] (\(y, z) -> f y ++ f z) (match v x)
   g   = foldr1 (curry (build v))

andView, orView, eqView :: View (Logic a) (Logic a, Logic a)
andView = makeView isAnd (uncurry (<&&>))
orView  = makeView isOr  (uncurry (<||>))
eqView  = makeView isEq  (uncurry equivalent)
 where
   isEq (p :<->: q) = Just (p, q)
   isEq _           = Nothing

infix 6 ===, ==>, <=>

(===), (==>), (<=>) :: Eq a => Logic a -> Logic a -> Bool
(===)   = eqLogic
p ==> q = tautology (p :->: q)
p <=> q = tautology (p :<->: q)