{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving #-}
-----------------------------------------------------------------------------

-- Copyright 2019, Ideas project team. This file is distributed under the

-- terms of the Apache License 2.0. For more information, see the files

-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.

-----------------------------------------------------------------------------

-- |

-- Maintainer  :  bastiaan.heeren@ou.nl

-- Stability   :  provisional

-- Portability :  portable (depends on ghc)

--

-- This module defines views on data-types, as described in "Canonical Forms

-- in Interactive Exercise Assistants"

--

-----------------------------------------------------------------------------


module Ideas.Common.View
   ( Control.Arrow.Arrow(..), Control.Arrow.ArrowChoice(..)
   , Control.Arrow.ArrowZero(..), Control.Arrow.ArrowPlus(..)
   , (>>>), (<<<)
     -- * @IsMatch@ type class

   , IsMatcher(..), matchM, belongsTo, viewEquivalent, viewEquivalentWith
   , Matcher, makeMatcher
     -- * @IsView@ type class

   , IsView(..), simplify, simplifyWith, simplifyWithM
   , canonical, canonicalWith, canonicalWithM, isCanonical, isCanonicalWith
     -- * Views

   , View, identity, makeView, matcherView
     -- * Isomorphisms

   , Isomorphism, from, to, inverse
     -- * Lifting with views

   , LiftView(..)
     -- * Some combinators

   , swapView, listView, traverseView, ($<)
     -- * Packaging a view

   , ViewPackage(..)
     -- * Properties on views

   , propIdempotence, propSoundness, propNormalForm
   ) where

import Control.Arrow
import Data.Maybe
import Ideas.Common.Classes
import Ideas.Common.Id
import Test.QuickCheck
import qualified Control.Category as C
import qualified Data.Traversable as T

----------------------------------------------------------------------------------

-- @IsMatch@ type class


class IsMatcher f where
   match   :: f a b -> a -> Maybe b
   matcher :: f a b -> Matcher a b
   -- default definitions

   match   = runKleisli . unM . matcher
   matcher = makeMatcher . match

-- |generalized monadic variant of @match@

matchM :: (Monad m, IsMatcher f) => f a b -> a -> m b
matchM v = maybe (fail "no match") return . match v

belongsTo :: IsMatcher f => a -> f a b -> Bool
belongsTo a view = isJust (match view a)

viewEquivalent :: (IsMatcher f, Eq b) => f a b -> a -> a -> Bool
viewEquivalent = viewEquivalentWith (==)

viewEquivalentWith :: IsMatcher f => (b -> b -> Bool) -> f a b -> a -> a -> Bool
viewEquivalentWith eq view x y =
   case (match view x, match view y) of
      (Just a, Just b) -> a `eq` b
      _                -> False

newtype Matcher a b = M { unM :: Kleisli Maybe a b }
   deriving (C.Category, Arrow, ArrowZero, ArrowPlus, ArrowChoice)

instance IsMatcher Matcher where
   matcher = id

makeMatcher :: (a -> Maybe b) -> Matcher a b
makeMatcher = M . Kleisli

----------------------------------------------------------------------------------

-- @IsView@ type class


-- |Minimal complete definition: @toView@ or both @match@ and @build@.

class IsMatcher f => IsView f where
   build  :: f a b -> b -> a
   toView :: f a b -> View a b
   -- default definitions

   build  f = build (toView f)
   toView f = makeView (match f) (build f)

canonical :: IsView f => f a b -> a -> Maybe a
canonical = canonicalWith id

canonicalWith :: IsView f => (b -> b) -> f a b -> a -> Maybe a
canonicalWith f = canonicalWithM (return . f)

canonicalWithM :: IsView f => (b -> Maybe b) -> f a b -> a -> Maybe a
canonicalWithM f view a =
   match view a >>= fmap (build view) . f

isCanonical :: (IsView f, Eq a) => f a b -> a -> Bool
isCanonical = isCanonicalWith (==)

isCanonicalWith :: IsView f => (a -> a -> Bool) -> f a b -> a -> Bool
isCanonicalWith eq v a = maybe False (eq a) (canonical v a)

simplify :: IsView f => f a b -> a -> a
simplify = simplifyWith id

simplifyWith :: IsView f => (b -> b) -> f a b -> a -> a
simplifyWith f = simplifyWithM (Just . f)

simplifyWithM :: IsView f => (b -> Maybe b) -> f a b -> a -> a
simplifyWithM f view a = fromMaybe a (canonicalWithM f view a)

----------------------------------------------------------------------------------

-- Views


data View a b where
   Prim     :: Matcher a b -> (b -> a) -> View a b
   (:@)     :: Id -> View a b -> View a b
   (:>>>:)  :: View a b -> View b c -> View a c
   (:***:)  :: View a c -> View b d -> View (a, b) (c, d)
   (:+++:)  :: View a c -> View b d -> View (Either a b) (Either c d)
   Traverse :: T.Traversable f => View a b -> View (f a) (f b)

instance C.Category View where
   id    = makeView return id
   v . w = w :>>>: v

instance Arrow View where
   arr     = (!->)
   first   = (*** identity)
   second  = (identity ***)
   (***)   = (:***:)
   f &&& g = copy >>> (f *** g)

instance BiArrow View where
   (<->) f = makeView (return . f)

instance ArrowChoice View where
   left    = (+++ identity)
   right   = (identity +++)
   (+++)   = (:+++:)
   f ||| g = (f +++ g) >>> merge

instance IsMatcher View where
   matcher view =
      case view of
         Prim m _   -> m
         _ :@ v     -> matcher v
         v :>>>: w  -> matcher v >>> matcher w
         v :***: w  -> matcher v *** matcher w
         v :+++: w  -> matcher v +++ matcher w
         Traverse v -> makeMatcher $ T.mapM (match v)

instance IsView View where
   build view =
      case view of
         Prim _ f   -> f
         _ :@ v     -> build v
         v :>>>: w  -> build v <<< build w
         v :***: w  -> build v *** build w
         v :+++: w  -> biMap (build v) (build w)
         Traverse v -> fmap (build v)

   toView = id

instance HasId (View a b) where
   getId (n :@ _) = n
   getId _        = mempty
   changeId f (n :@ a) = f n :@ a
   changeId f a        = f mempty :@ a

instance Identify (View a b) where
   n @> v | a == mempty = v
          | otherwise   = a :@ v
    where
      a = newId n

makeView :: (a -> Maybe b) -> (b -> a) -> View a b
makeView = matcherView . makeMatcher

matcherView :: Matcher a b -> (b -> a) -> View a b
matcherView = Prim

identity :: C.Category f => f a a
identity = C.id

----------------------------------------------------------------------------------

-- Isomorphisms (embedding-projection pairs)


-- to ep . from ep == id

data Isomorphism a b = EP { pid :: Id, from :: a -> b, to :: b -> a }

instance C.Category Isomorphism where
   id    = id <-> id
   f . g = (from f . from g) <-> (to g . to f)

instance Arrow Isomorphism where
   arr     = (!->)
   first   = (*** identity)
   second  = (identity ***)
   p *** q = from p *** from q <-> to p *** to q
   f &&& g = copy >>> (f *** g)

instance BiArrow Isomorphism where
   (<->) = EP mempty

instance ArrowChoice Isomorphism where
   left    = (+++ identity)
   right   = (identity +++)
   p +++ q = from p +++ from q <-> to p +++ to q
   f ||| g = (f +++ g) >>> merge

instance IsMatcher Isomorphism where
   match p = Just . from p

instance IsView Isomorphism where
   toView p = getId p @> makeView (match p) (to p)

instance HasId (Isomorphism a b) where
   getId = pid
   changeId f p = p { pid = f (pid p) }

instance Identify (Isomorphism a b) where
   (@>) = changeId . const . newId

inverse :: Isomorphism a b -> Isomorphism b a
inverse f = to f <-> from f

----------------------------------------------------------------------------------

-- Type class for lifting with Views


class LiftView f where
   liftView   :: View a b -> f b -> f a
   liftViewIn :: View a (b, c) -> f b -> f a
   -- default definition

   liftView v = liftViewIn (v &&& identity)

----------------------------------------------------------------------------------

-- Some combinators


swapView :: Isomorphism (a, b) (b, a)
swapView = "views.swap" @> swap

-- | Specialized version of traverseView

listView :: View a b -> View [a] [b]
listView = traverseView

-- or is liftView a better name?

traverseView :: T.Traversable f => View a b -> View (f a) (f b)
traverseView = Traverse

($<) :: T.Traversable f => View a (f b) -> View b c -> View a (f c)
a $< b = a >>> traverseView b

swap :: BiArrow arr => arr (a, b) (b, a)
swap = f <-> f
 where
   f :: (a, b) -> (b, a)
   f (a, b) = (b, a)

copy :: BiArrow arr => arr a (a, a)
copy = (\a -> (a, a)) <-> fst

merge :: BiArrow arr => arr (Either a a) a
merge = either id id <-> Left

----------------------------------------------------------------------------------

-- Packaging a view for documentation purposes


data ViewPackage where
   ViewPackage ::
      (Show a, Show b, Eq a) => (String -> Maybe a) -> View a b -> ViewPackage

instance HasId ViewPackage where
   getId      (ViewPackage _ a) = getId a
   changeId f (ViewPackage p a) = ViewPackage p (changeId f a)

----------------------------------------------------------------------------------

-- Properties on views


propIdempotence :: (Show a, Eq a) => Gen a -> View a b -> Property
propIdempotence g v = forAll g $ \a ->
   let b = simplify v a
   in b == simplify v b

propSoundness :: Show a => (a -> a -> Bool) -> Gen a -> View a c -> Property
propSoundness semEq g v = forAll g $ \a ->
   let b = simplify v a
   in semEq a b

propNormalForm :: (Show a, Eq a) => Gen a -> View a b -> Property
propNormalForm g v = forAll g $ \a -> a == simplify v a