{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}

module Lattices.UnitIntervalStructures.Godel(
    UIGodel(UIGodel),
    BoundedLattice(..),
    mkGodelUnitInterval,
    fromGodelUnitInterval
) where

import Lattices.ResiduatedLattice
import Lattices.UnitInterval

newtype UIGodel = UIGodel UnitInterval 
    deriving (UIGodel -> UIGodel -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UIGodel -> UIGodel -> Bool
$c/= :: UIGodel -> UIGodel -> Bool
== :: UIGodel -> UIGodel -> Bool
$c== :: UIGodel -> UIGodel -> Bool
Eq, Eq UIGodel
UIGodel -> UIGodel -> Bool
UIGodel -> UIGodel -> Ordering
UIGodel -> UIGodel -> UIGodel
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: UIGodel -> UIGodel -> UIGodel
$cmin :: UIGodel -> UIGodel -> UIGodel
max :: UIGodel -> UIGodel -> UIGodel
$cmax :: UIGodel -> UIGodel -> UIGodel
>= :: UIGodel -> UIGodel -> Bool
$c>= :: UIGodel -> UIGodel -> Bool
> :: UIGodel -> UIGodel -> Bool
$c> :: UIGodel -> UIGodel -> Bool
<= :: UIGodel -> UIGodel -> Bool
$c<= :: UIGodel -> UIGodel -> Bool
< :: UIGodel -> UIGodel -> Bool
$c< :: UIGodel -> UIGodel -> Bool
compare :: UIGodel -> UIGodel -> Ordering
$ccompare :: UIGodel -> UIGodel -> Ordering
Ord, Integer -> UIGodel
UIGodel -> UIGodel
UIGodel -> UIGodel -> UIGodel
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> UIGodel
$cfromInteger :: Integer -> UIGodel
signum :: UIGodel -> UIGodel
$csignum :: UIGodel -> UIGodel
abs :: UIGodel -> UIGodel
$cabs :: UIGodel -> UIGodel
negate :: UIGodel -> UIGodel
$cnegate :: UIGodel -> UIGodel
* :: UIGodel -> UIGodel -> UIGodel
$c* :: UIGodel -> UIGodel -> UIGodel
- :: UIGodel -> UIGodel -> UIGodel
$c- :: UIGodel -> UIGodel -> UIGodel
+ :: UIGodel -> UIGodel -> UIGodel
$c+ :: UIGodel -> UIGodel -> UIGodel
Num, Num UIGodel
Ord UIGodel
UIGodel -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: UIGodel -> Rational
$ctoRational :: UIGodel -> Rational
Real, Fractional UIGodel
Real UIGodel
forall b. Integral b => UIGodel -> b
forall b. Integral b => UIGodel -> (b, UIGodel)
forall a.
Real a
-> Fractional a
-> (forall b. Integral b => a -> (b, a))
-> (forall b. Integral b => a -> b)
-> (forall b. Integral b => a -> b)
-> (forall b. Integral b => a -> b)
-> (forall b. Integral b => a -> b)
-> RealFrac a
floor :: forall b. Integral b => UIGodel -> b
$cfloor :: forall b. Integral b => UIGodel -> b
ceiling :: forall b. Integral b => UIGodel -> b
$cceiling :: forall b. Integral b => UIGodel -> b
round :: forall b. Integral b => UIGodel -> b
$cround :: forall b. Integral b => UIGodel -> b
truncate :: forall b. Integral b => UIGodel -> b
$ctruncate :: forall b. Integral b => UIGodel -> b
properFraction :: forall b. Integral b => UIGodel -> (b, UIGodel)
$cproperFraction :: forall b. Integral b => UIGodel -> (b, UIGodel)
RealFrac, Num UIGodel
Rational -> UIGodel
UIGodel -> UIGodel
UIGodel -> UIGodel -> UIGodel
forall a.
Num a
-> (a -> a -> a) -> (a -> a) -> (Rational -> a) -> Fractional a
fromRational :: Rational -> UIGodel
$cfromRational :: Rational -> UIGodel
recip :: UIGodel -> UIGodel
$crecip :: UIGodel -> UIGodel
/ :: UIGodel -> UIGodel -> UIGodel
$c/ :: UIGodel -> UIGodel -> UIGodel
Fractional)

instance BoundedLattice UIGodel where
    (/\) :: UIGodel -> UIGodel -> UIGodel
    /\ :: UIGodel -> UIGodel -> UIGodel
(/\) (UIGodel UnitInterval
x) (UIGodel UnitInterval
y) = UnitInterval -> UIGodel
UIGodel (UnitInterval
x forall l. BoundedLattice l => l -> l -> l
/\ UnitInterval
y)
    \/ :: UIGodel -> UIGodel -> UIGodel
(\/) (UIGodel UnitInterval
x) (UIGodel UnitInterval
y) = UnitInterval -> UIGodel
UIGodel (UnitInterval
x forall l. BoundedLattice l => l -> l -> l
\/ UnitInterval
y)
    bot :: UIGodel
bot = UnitInterval -> UIGodel
UIGodel forall l. BoundedLattice l => l
bot
    top :: UIGodel
top = UnitInterval -> UIGodel
UIGodel forall l. BoundedLattice l => l
top
    mkLattice :: Double -> UIGodel
mkLattice = Double -> UIGodel
mkGodelUnitInterval

-- | Gödel structure of truth values

instance ResiduatedLattice UIGodel where
    tnorm :: UIGodel -> UIGodel -> UIGodel
tnorm UIGodel
x UIGodel
y = UIGodel
x forall l. BoundedLattice l => l -> l -> l
/\ UIGodel
y
    --> :: UIGodel -> UIGodel -> UIGodel
(-->)  = UIGodel -> UIGodel -> UIGodel
godelResiduum

instance Show UIGodel where
    show :: UIGodel -> String
show (UIGodel UnitInterval
x) = forall a. Show a => a -> String
show UnitInterval
x

mkGodelUnitInterval :: Double -> UIGodel
mkGodelUnitInterval :: Double -> UIGodel
mkGodelUnitInterval Double
x = UnitInterval -> UIGodel
UIGodel forall a b. (a -> b) -> a -> b
$ Double -> UnitInterval
mkUnitInterval Double
x

fromGodelUnitInterval :: UIGodel -> Double
fromGodelUnitInterval :: UIGodel -> Double
fromGodelUnitInterval (UIGodel (UnitInterval Double
x)) = Double
x

godelResiduum :: UIGodel -> UIGodel -> UIGodel
godelResiduum :: UIGodel -> UIGodel -> UIGodel
godelResiduum UIGodel
x UIGodel
y
    | UIGodel
x forall a. Ord a => a -> a -> Bool
<= UIGodel
y = forall l. BoundedLattice l => l
top
    | Bool
otherwise = UIGodel
y