{-# LANGUAGE MagicHash, GADTs, KindSignatures, ScopedTypeVariables
           , Rank2Types #-}
{-# OPTIONS_GHC -Wall #-}
----------------------------------------------------------------------
-- |
-- Module      :  Data.Bot.Part
-- Copyright   :  (c) Conal Elliott 2008
-- License     :  BSD3
-- 
-- Maintainer  :  conal@conal.net
-- Stability   :  experimental
-- 
-- 
----------------------------------------------------------------------

module Data.Bot.Part where

import Control.Arrow hiding (pure)
import Control.Applicative
import Data.Maybe (fromMaybe)
import GHC.Base (unsafeCoerce#) -- used in partMatch and coerceV

-- | Part of a structure of nested pairs
data Part :: * -> * -> * where
  IdP     :: Part a a
  FirstP  :: Part c a -> Part (c,b) a
  SecondP :: Part c b -> Part (a,c) b

-- | Equality on parts
partEq :: Part i a -> Part i b -> Bool
IdP       `partEq` IdP       = True
FirstP  p `partEq` FirstP  q = p `partEq` q
SecondP p `partEq` SecondP q = p `partEq` q
_         `partEq` _         = False
 
-- | Leibniz equality
type Leibniz a a' = forall phi. phi a -> phi a'

--newtype Leibniz a a' = Leibniz (forall phi. phi a -> phi a')

-- | Try to match parts.  If successful, yield a proof of Leibniz
-- equality, i.e., a coercion.
partMatch :: Part c a -> Part c a' -> Maybe (Leibniz a a')
a `partMatch` a' 
  | a `partEq` a' = Just unsafeCoerce#
  | otherwise     = Nothing


-- | Extract part of a value.  Use staged to avoid interpretive overhead.
extract :: Part c a -> (c -> a)
extract IdP         = id
extract (FirstP  p) = extract p . fst
extract (SecondP p) = extract p . snd

-- | Change a part of a value.  Use staged to avoid interpretive overhead.
change :: Part c a -> ((a -> a) -> (c -> c))
change IdP         = id
change (FirstP  p) = first  . change p
change (SecondP p) = second . change p

-- I really only wanted constant @a@ values for 'change', but I like how the
-- definition mirrors @comp@'s in this slightly more general setting.
-- Also, 'extract' and 'change' relate 'Part' to composable references.

-- | Substitute for part of a value.  Use staged to avoid interpretive overhead.
subst :: Part c a -> (a -> (c -> c))
subst p = change p . const

-- About the staging comments:
-- 
-- Because of the way I've defined 'extract', 'change', and 'subst',
-- the "syntactic" analysis of parts is done once rather than at each
-- substitution.  The extra parentheses in the type signature serve as
-- a reminder.  Will haddock remove the extra parens?


-- | Compose parts.  Specification:
-- 
-- @extract (comp p q) == extract q . extract p@
-- @change  (comp p q) == change  p . change  q@
comp :: Part c b -> (Part b a -> Part c a)
comp IdP         = id
comp (FirstP  p) = FirstP  . comp p
comp (SecondP p) = SecondP . comp p

-- comp IdP         q = q
-- comp (FirstP  p) q = FirstP  (comp p q)
-- comp (SecondP p) q = SecondP (comp p q)

--    extract (comp (FirstP p) q) 
-- == extract q . extract (FirstP p)
-- == extract q . extract p . fst
-- == extract (FirstP (comp p q))

-- change p ::(b -> b) -> (c -> c)
-- change q ::(a -> a) -> (b -> b)
-- change p . change q :: (a -> a) -> (c -> c)

--    change (comp (FirstP p) q)
-- == change (FirstP p) . change q
-- == first . change p . change q
-- == first . change (comp p q)
-- == change (FirstP (comp p q))


---- experiments

-- \ ((a,b),c) -> a*b + b*c
t1 :: ((Int,Int),Int) -> Int
t1 = liftA2 (+)
       (liftA2 (*) (fst>>>fst) (fst>>>snd))
       (liftA2 (*) (fst>>>snd) snd)



-- Bot with top-level data
data DBot i o = DBot o (Bot i o)

-- Bot without top-level data
data Bot :: * -> * -> * where
  PureB :: Bot i o
  AppB  :: DBot i (a -> b) -> DBot i a -> Bot i b
  PartB :: Part i o -> Bot i o

instance Functor (DBot i) where
  fmap f = (pure f <*> )

instance Applicative (DBot i) where
  pure o = DBot o PureB
  fd@(DBot f _) <*> xd@(DBot x _) = DBot (f x) (fd `AppB` xd)

-- TODO: factor  the Applicative pattern from Bot & DBot.  Parameterize
-- by @Part i@.  The the general version has just one type argument.


-- | An 'Applicative'-style tree of values.
data AppV :: * -> * where
  PureV :: a -> AppV a
  AppV  :: a -> AppV (b -> a) -> AppV b -> AppV a

-- Extract the top-level value from a tree.
vVal :: AppV a -> a
vVal (PureV    a) = a
vVal (AppV a _ _) = a

appV :: AppV (b -> a) -> AppV b -> AppV a
fv `appV` bv = AppV ((vVal fv) (vVal bv)) fv bv

instance Functor AppV where
  fmap f = (pure f <*> )

instance Applicative AppV where
  pure  = PureV
  (<*>) = appV

data AppF :: (* -> *) -> * -> * where
  PureF :: a -> AppF h a
  AppF  :: AppF h (b -> a) -> AppF h b -> AppF h a
  InF   :: h a -> AppF h a

instance Functor (AppF h) where
  fmap f = (pure f <*> )

instance Applicative (AppF h) where
  pure  = PureF
  (<*>) = AppF


-- | Adaptive bot.
type Adapt i = AppF (Part i)

-- | Evaluate a Adapt at an input, yielding a caching structure that
-- matches the Adapt's shape.
eval :: Adapt i o -> i -> AppV o
eval (PureF a)        = const (PureV a)
eval (AppF fbot bbot) = liftA2 appV (eval fbot) (eval bbot)
eval (InF p)          = PureV . extract p

-- A possible means of substituting in an @a@ value.  A 'Nothing' means
-- that the substitution wouldn't make any change.
type MbSubst a b = Maybe (a -> AppV b -> AppV b)

-- | Make an update function for a bot.  To eliminate interpretive
-- overhead, apply 'update' in stages: first provide a bot.  Then each
-- part in turn.
update :: Adapt i o -> (Part i a -> MbSubst a o)

update (PureF _) = const Nothing

update (InF p) = \ q -> 
  case q `partMatch` p of
    Just coerce -> Just (\ a _ -> coerce (PureV a))
    Nothing     -> Nothing

update (fun `AppF` arg) = \ q ->
  case (msubf q, msuba q) of
    (Nothing,Nothing) -> Nothing
    (repf,repb)       -> Just $ \ a (AppV _ vf vb) ->
      upd fun repf a vf `appV` upd arg repb a vb
 where
   msubf = update fun
   msuba = update arg

-- Apply a 'MbSubst' to a value and an 'AppV' that matches the given
-- 'AppF'.  Warning: this matching requirement is not statically checked,
-- and Very Bad Things can happen if it's violated.  See 'coerceV'.
upd :: AppF f b -> MbSubst a b -> a -> AppV b' -> AppV b
upd appf rep a v' = fromMaybe ((const.const) v) rep a v
 where
   v = coerceV appf v'

-- The 'eval' and 'update' functions maintain an invariant that
-- corresponding 'AppF' and 'AppV' have the same intermediate @b@ type.
-- This coercion function exploits that invariant.
-- 
-- TODO: look for a statically checked alternative.
coerceV :: AppF f b -> AppV b' -> AppV b
coerceV = const unsafeCoerce#