{- |
Description: Definition and operations on the ternary logic with /null/.
License: GNU LGPLv3
Maintainer: paul.bittner@uni-ulm.de

Definition and operations on the ternary logic with /null/.
In the paper, we call formulas of this logic /nullable propositional formulas/.
Reuses 'PropositionalFormula's.
-}
module NullPropositions where

import Logic
import Propositions
import Defunctor ( Defunctor(demap) )
import Data.Maybe (catMaybes, fromJust, isNothing)

-- | Data type for the ternary logic by Sobocinski.
--  The 'Nothing' case represents /null/ as used in our paper.
type NullableFormula a = Maybe (PropositionalFormula a)

-- | Returns @true@ iff the given formula is the value /null/.
isnull :: NullableFormula a -> Bool
isnull :: NullableFormula a -> Bool
isnull = NullableFormula a -> Bool
forall a. Maybe a -> Bool
isNothing

-- | Returns @false@ iff the given formula is the value /null/.
notnull :: NullableFormula a -> Bool
notnull :: NullableFormula a -> Bool
notnull = Bool -> Bool
not(Bool -> Bool)
-> (NullableFormula a -> Bool) -> NullableFormula a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.NullableFormula a -> Bool
forall a. NullableFormula a -> Bool
isnull

-- | Converts the given nullable formula to a propositional formula, assuming that the given formula is not /null/.
-- Crashes otherwise.
assure :: NullableFormula a -> PropositionalFormula a
assure :: NullableFormula a -> PropositionalFormula a
assure = NullableFormula a -> PropositionalFormula a
forall a. HasCallStack => Maybe a -> a
fromJust

-- | Simplifies the given formula. Uses 'Propositions.simplify'.
nullable_simplify :: NullableFormula a -> NullableFormula a
nullable_simplify :: NullableFormula a -> NullableFormula a
nullable_simplify = (PropositionalFormula a -> PropositionalFormula a)
-> NullableFormula a -> NullableFormula a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
Propositions.simplify

-- | Pretty Printing for nullable objects such as the nullable propositional logic.
prettyPrint :: (Show a) => Maybe a -> String
prettyPrint :: Maybe a -> String
prettyPrint Nothing = "null" -- null, none, nothing, empty, unknown
prettyPrint (Just p :: a
p) = a -> String
forall a. Show a => a -> String
show a
p

-- | Any 'Logic' can be lifted to a logic on 'Maybe'.
-- This adds a new value 'Nothing' to the values of the given logic.
-- In particular, 'NullableFormula' is thus a 'Logic'.
instance Logic a => Logic (Maybe a) where
    ltrue :: Maybe a
ltrue = a -> Maybe a
forall a. a -> Maybe a
Just a
forall l. Logic l => l
ltrue
    lfalse :: Maybe a
lfalse = a -> Maybe a
forall a. a -> Maybe a
Just a
forall l. Logic l => l
lfalse
    lvalues :: [Maybe a]
lvalues = Maybe a
forall a. Maybe a
NothingMaybe a -> [Maybe a] -> [Maybe a]
forall a. a -> [a] -> [a]
:(a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> [a] -> [Maybe a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
forall l. Logic l => [l]
lvalues)
    
    lnot :: Maybe a -> Maybe a
lnot = (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall l. Logic l => l -> l
lnot
    land :: [Maybe a] -> Maybe a
land l :: [Maybe a]
l = case [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
catMaybes [Maybe a]
l of
        [] -> Maybe a
forall a. Maybe a
Nothing
        [p :: a
p] -> a -> Maybe a
forall a. a -> Maybe a
Just a
p
        justs :: [a]
justs -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a] -> a
forall l. Logic l => [l] -> l
land [a]
justs

    leval :: (Maybe a -> Maybe a) -> Maybe a -> Maybe a
leval config :: Maybe a -> Maybe a
config m :: Maybe a
m = Maybe a
m Maybe a -> (a -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> (a -> a) -> a -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> a) -> a -> a
forall l. Logic l => (l -> l) -> l -> l
leval ((Maybe a -> Maybe a) -> a -> a
forall (f :: * -> *) a b. Defunctor f => (f a -> f b) -> a -> b
demap Maybe a -> Maybe a
config)