{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving #-}

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

-- Copyright 2018, 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