{- |
Description: Type class for reasoning on 'Logic's.
License: GNU LGPLv3
Maintainer: paul.bittner@uni-ulm.de

Type class for reasoning on 'Logic's.
-}
module Logic where

{- |
Type class to reason on logics.
We use this type class to reason on propositional logic and the ternary logic by Sobocinski we use for feature trace recording.
-}
class Logic l where
    -- | The atomic value representing /true/ in this logic.
    ltrue :: l
    -- | The atomic value representing /false/ in this logic.
    lfalse :: l
    -- | A list of all atomic values of this logic. Default implementation comprises 'ltrue' and 'lfalse'.
    lvalues :: [l]
    lvalues = [l
forall l. Logic l => l
lfalse, l
forall l. Logic l => l
ltrue]

    -- | Negation of a logical formula.
    lnot :: l -> l
    -- lnot q = limplies q lfalse
    -- | Conjunction of a list of logical formulas.
    land :: [l] -> l
    -- land = lnot.lor.map lnot
    -- | Disjunction of a list of logical formulas.
    lor :: [l] -> l
    -- lor p q = limplies (limplies p q) q
    lor = l -> l
forall l. Logic l => l -> l
lnot(l -> l) -> ([l] -> l) -> [l] -> l
forall b c a. (b -> c) -> (a -> b) -> a -> c
.[l] -> l
forall l. Logic l => [l] -> l
land([l] -> l) -> ([l] -> [l]) -> [l] -> l
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(l -> l) -> [l] -> [l]
forall a b. (a -> b) -> [a] -> [b]
map l -> l
forall l. Logic l => l -> l
lnot
    -- | Implication between two logical formulas.
    -- The first argument @p@ is one the left side of the implication and the second argument 'q' is on the right (i.e., @p => q@).
    limplies :: l -> l -> l
    limplies p :: l
p q :: l
q = [l] -> l
forall l. Logic l => [l] -> l
lor [l -> l
forall l. Logic l => l -> l
lnot l
p, l
q]
    -- | Equivalence between two logical formulas.
    lequals :: l -> l -> l
    lequals p :: l
p q :: l
q = [l] -> l
forall l. Logic l => [l] -> l
land [l -> l -> l
forall l. Logic l => l -> l -> l
limplies l
p l
q, l -> l -> l
forall l. Logic l => l -> l -> l
limplies l
q l
p]

    {- |
    Evaluates a logical formula.
    Arguments are
    
    (1) a function assigning variables to values
    (2) a formula to evaluate
    This function should return an element of 'lvalues'.
    -}
    leval :: (l -> l) -> l -> l