{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE UndecidableInstances  #-}
{-|
Module      : ContextLattice
Description : models a Lattice for a context type, the top of the lattice is represented by One and inherits a list of all subcontexts, the bottom of the lattice is represented by Zero.
Maintainer  : hahn@geoinfo.tuwien.ac.at
Stability   : beta

models a Lattice for a context type, the top of the lattice is represented by One and inherits a list of all subcontexts, the bottom of the lattice is represented by Zero. To inherit the contextlattice to a new data type the data type has to instanciate: Enumerable c, Eq c, Ord c, Show c
-}
module ContextLattice (Context (One,Ctx,Zero), getFinerContexts
                      ,extractContext, propCommutative,propIdempotent,propAssociative) where

import           Algebra.Enumerable
import           Algebra.Lattice
import qualified Data.List          as L
import qualified Debug.Trace        as T

-- | data type to represent a lattice structure, the actual context is the type variable @c@
data Context c=
 -- | constructor represents the One element of the lattice, all contexts are included in this constructor,
 -- for this constructor the model includes all contexts
 One [Context c]
 -- | constructor for one context
 | Ctx [c]
 -- | constructor represents the bottom element of the lattice, without any context
 | Zero  deriving (Show,Eq,Ord)

-- | makes the Context c type to a MeetSemiLattice by implementing the meet function
instance (Enumerable  c,Eq c,(Enumerable (Context c)))=>
  MeetSemiLattice (Context c) where

 -- | the meet funtion implements the algebraic properties of context
 meet:: Context c-> Context c-> Context c
 meet (One _) c = c -- cummutative with One element
 meet c (One _) = c -- cummutative with One element
 meet firstContext secondContext
  | null firstIntersectWithSecondContext = Zero
  | otherwise  = Ctx (L.head firstIntersectWithSecondContext)
   where firstContextList = L.concatMap extractContext $ getFinerContexts firstContext
         secondContextList = L.concatMap extractContext $ getFinerContexts secondContext
         firstIntersectWithSecondContext = firstContextList `isPartOf` secondContextList -- commutativity property

-- | extracts a context list of contexts from the element,
-- needed for the One wrapper constructor
extractContext ::
 Context c  -- ^ Context where elements are extracted from,
 -> [[c]]   -- ^ extracted context list
extractContext (One c) = extractOneContext c
extractContext (Ctx c) = [c]
extractContext Zero = []

-- | makes a list of contexts for the One constructor
extractOneContext ::
 [Context c]  -- ^ list of context c occured by constructor c
 -> [[c]]      -- ^ extracted list
extractOneContext [] = []
extractOneContext (Ctx c:cs)= c : extractOneContext cs

-- | takes a context and returns all finer
getFinerContexts :: (Eq c, (Enumerable  c),(Enumerable (Context c))) =>
 Context c      -- ^ context that is used as start
 -> [Context c] -- ^ all finer contexts of the start context included in the lattice
getFinerContexts c = L.map Ctx $ contextListWholeLattice  `isPartOf` contextListfromStart
 where contextListfromStart = extractContext c
       contextListWholeLattice = extractContext (One universe)

-- | Checks if the first context list is included in the second, if so the context is returned,
--   so far the function is does not have any order restrictions (is commutative)
--   checks also sublists, if an element of a sublist is in both lists, the whole list is included
isPartOf ::(Eq c) =>
 [[c]]      -- ^ first list that is used to check against second one
 -> [[c]]   -- ^ second list is like a reference
 -> [[c]]   -- ^ elements that are included in both lists
isPartOf = L.intersectBy (\lista listb -> all (`elem` lista) listb)


-- * algebraic property test methods
-- | test for commutativity
--
-- >>> (Ctx [Walking]) `propCommutative` One [Ctx [Walking],Ctx [Driving],Ctx [Walking,Driving],Ctx [Uphill],Ctx [Walking,Uphill],Ctx [Driving,Uphill],Ctx [Walking,Driving,Uphill]] = (Ctx [Walking]) `meet` One [Ctx [Walking],Ctx [Driving],Ctx [Walking,Driving],Ctx [Uphill],Ctx [Walking,Uphill],Ctx [Driving,Uphill],Ctx [Walking,Driving,Uphill]] == One [Ctx [Walking],Ctx [Driving],Ctx [Walking,Driving],Ctx [Uphill],Ctx [Walking,Uphill],Ctx [Driving,Uphill],Ctx [Walking,Driving,Uphill]] `meet` (Ctx [Walking])
-- true
propCommutative ::(Eq c,Enumerable c, Enumerable (Context c)) =>
  Context c    -- ^ context one
  -> Context c -- ^ context two
  -> Bool      -- ^ true if the property is full-filled
propCommutative c1 c2 =  c1 `meet` c2 == c2 `meet` c1

-- | test for idempotency
--
-- >>> propIdempotent (Ctx [Walking]) = (Ctx [Walking]) `meet` (Ctx [Walking]) == (Ctx [Walking])
-- true
propIdempotent ::(Eq c,Enumerable c, Enumerable (Context c)) =>
  Context c-- ^ context to test
  -> Bool  -- ^ true if the property is full-filled
propIdempotent c =  c `meet` c == c

-- | test for associativity
--
-- >>> propAssociative (Ctx [Walking]) (Ctx [Driving]) (Ctx [Uphill]) =  (Ctx [Walking]) `meet` ((Ctx [Driving]) `meet` (Ctx [Uphill])) == ((Ctx [Walking]) `meet` (Ctx [Driving])) `meet` (Ctx [Uphill])
-- true
propAssociative :: (Eq c, Enumerable c, Enumerable (Context c)) =>
  Context c    -- ^ context one
  -> Context c -- ^ context two
  -> Context c -- ^ context three
  -> Bool      -- ^ true if the property is full-filled
propAssociative x y z = x `meet` (y `meet` z) == (x `meet` y) `meet` z


-- * not needed
-- | checks in which level of the lattice the actual @Context c@ is
-- One gets level 1, Zero gets level 0, and all others are 1+
level ::
 Context c -- ^ context to check level in the lattice
 -> Int    -- ^ level in the lattice
level (One _)= 1
level (Zero)=0
level (Ctx a)= L.length a