{-  Copyright 2010 Dominique Devriese

    This file is part of the grammar-combinators library.

    The grammar-combinators library is free software: you can
    redistribute it and/or modify it under the terms of the GNU
    Lesser General Public License as published by the Free
    Software Foundation, either version 3 of the License, or (at
    your option) any later version.

    Foobar is distributed in the hope that it will be useful, but
    WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU Lesser General Public License for more details.

    You should have received a copy of the GNU Lesser General
    Public License along with Foobar. If not, see
    <http://www.gnu.org/licenses/>.
-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Text.GrammarCombinators.Base.Domain (
    DomainMap(supIx, subIx),
    DomainEmbedding(supPF), 
    SubVal(MkSubVal, unSubVal),
    IxMapId, IxMapBase, IxMapSeq, ApplyIxMap, 
    MemoFam(toMemo, fromMemo), Memo, memoFamily,
    FoldFam(foldFam),
    EqFam(overrideIdx, eqIdx), overrideIdxK, 
    ShowFam(showIdx),
    Domain,
    memoFamilyK, toMemoK, fromMemoK,
    LiftFam(liftIdxE, liftIdxP),
    LeftIx, RightIx,
    MergeDomain (LeftIdx, RightIdx),
    EitherFunctor (LeftR, RightR),
    unLeftR, unRightR
  ) where

import Generics.MultiRec.Base
import Generics.MultiRec.HFunctor

import Language.Haskell.TH.Syntax (Exp, Pat)

data IxMapId
data IxMapBase (m :: * -> *)
data IxMapSeq (l1 :: *) (l2 :: * -> *)
type family ApplyIxMap (m :: *) ix
type instance ApplyIxMap (IxMapBase m) ix = m ix
type instance ApplyIxMap (IxMapSeq l1 l2) ix = ApplyIxMap l1 (l2 ix)
type instance ApplyIxMap IxMapId ix = ix

class MemoFam (phi :: * -> *) where
  data Memo phi :: (* -> *) -> *
  fromMemo :: Memo phi v -> (forall ix. phi ix -> v ix)
  toMemo :: (forall ix. phi ix -> v ix) -> Memo phi v

memoFamily :: (MemoFam phi) =>
              (forall ix. phi ix -> v ix) -> (forall ix. phi ix -> v ix)  
memoFamily f = fromMemo (toMemo f)

memoFamilyK :: (MemoFam phi) =>
               (forall ix. phi ix -> v) -> (forall ix. phi ix -> v)
memoFamilyK f = fromMemoK (toMemoK f) 
toMemoK :: (MemoFam phi) =>
           (forall ix. phi ix -> v) -> Memo phi (K0 v)
toMemoK f = toMemo (K0 . f)
fromMemoK :: (MemoFam phi) =>
             Memo phi (K0 v) -> phi ix -> v
fromMemoK m = unK0 . fromMemo m

-- | A domain 'phi' that is an instance of the 'FoldFam' type class supports 
-- folding over all non-terminals in the domain using the 'foldFam' function.
class FoldFam phi where
  -- | Fold a given function over all non-terminals in the domain 'phi'.
  foldFam :: (forall ix. phi ix -> b -> b) -> b -> b

-- | A domain 'phi' that is an instance of the 'ShowFam' type class supports 
-- conversion of non-terminal proof terms to Strings using the 'showIdx' function.
class ShowFam phi where
  -- | Convert a given non-terminal proof term to a String representation.
  showIdx :: forall ix. phi ix -> String

-- | A domain 'phi' that is an instance of the 'EqFam' type class supports 
-- overriding a function over the full domain at a single non-terminal using 
-- the |overrideIdx| function.
class EqFam phi where
  -- | Test equality of two given non-terminal proof terms.
  eqIdx :: forall ix1 ix2. phi ix1 -> phi ix2 -> Bool
  eqIdx idx1 = overrideIdxK (const False) idx1 True 
  -- | Override a function over the full domain at a single non-terminal.
  overrideIdx :: (forall ix'. phi ix' -> r ix') -> phi oix ->
                 r oix -> phi ix -> r ix

-- | Similar to the 'overrideIdx' function, but limited to functions whose result type is 
-- the same for all non-terminals.
overrideIdxK :: (EqFam phi) => (forall ix'. phi ix' -> v) -> phi oix -> v -> phi ix -> v
overrideIdxK f idx v = unK0 . overrideIdx (K0 . f) idx (K0 v)

-- | A decent Domain 'phi' should instantiate the 'FoldFam', 'ShowFam', 'EqFam' and 'MemoFam'. Avoid
-- using this type class in constraints, use more specific type classes whenever possible.
-- 
-- Note: instances for this type class are not automatically derived, and you have to manually instantiate 
-- it with an empty implementation block.
class (FoldFam phi,
       ShowFam phi,
       EqFam phi,
       MemoFam phi) => Domain phi

class DomainMap phi phi' supIxT where
  supIx :: phi' ix -> phi (supIxT ix)
  subIx :: phi (supIxT ix) -> phi' ix
  
class (DomainMap phi phi' supIxT) =>
      DomainEmbedding phi phi' supIxT where
  supPF :: (HFunctor phi (PF phi)) =>
           phi' ix -> phi (supIxT ix) ->
           PF phi' (SubVal supIxT r) ix -> PF phi r (supIxT ix)

-- | A generic wrapper type that restricts a semantic value family over a bigger domain
-- to a smaller domain.
data SubVal (supIxT :: * -> *) v ix = MkSubVal {
       unSubVal :: v (supIxT ix)
       } deriving (Show)

class LiftFam phi where
  liftIdxE :: phi ix -> Exp
  liftIdxP :: phi ix -> Pat

data LeftIx ix
data RightIx ix

data MergeDomain phiL phiR ix where
  LeftIdx :: phiL ix -> MergeDomain phiL phiR (LeftIx ix)
  RightIdx :: phiR ix -> MergeDomain phiL phiR (RightIx ix)

instance (MemoFam phiL, MemoFam phiR) => 
         MemoFam (MergeDomain phiL phiR) where
           data Memo (MergeDomain phiL phiR) v = MemoMD (Memo phiL (SubVal LeftIx v)) (Memo phiR (SubVal RightIx v))
           fromMemo (MemoMD ml mr) (LeftIdx idx) = unSubVal $ fromMemo ml idx
           fromMemo (MemoMD ml mr) (RightIdx idx) = unSubVal $ fromMemo mr idx
           toMemo f = MemoMD (toMemo (MkSubVal . f . LeftIdx)) (toMemo (MkSubVal . f . RightIdx))

instance (ShowFam phiL, ShowFam phiR) => 
         ShowFam (MergeDomain phiL phiR) where
           showIdx (LeftIdx idx) = concat ["LeftIdx (", (showIdx idx), ")"]
           showIdx (RightIdx idx) = concat ["RightIdx (", (showIdx idx), ")"]

instance (FoldFam phiL, FoldFam phiR) => 
         FoldFam (MergeDomain phiL phiR) where
           foldFam f n = foldFam (f . LeftIdx) $ foldFam (f . RightIdx) n

instance (EqFam phiL, EqFam phiR) => 
         EqFam (MergeDomain phiL phiR) where
           overrideIdx f (LeftIdx idx) v (LeftIdx idx') = unSubVal $ overrideIdx (MkSubVal . f . LeftIdx) idx (MkSubVal v) idx'
           overrideIdx f (RightIdx idx) v (RightIdx idx') = unSubVal $ overrideIdx (MkSubVal . f . RightIdx) idx (MkSubVal v) idx'
           overrideIdx f _ _ idx = f idx

instance (Domain phiL, Domain phiR) => Domain (MergeDomain phiL phiR) 

data EitherFunctor rL rR ix where
  LeftR :: rL ix -> EitherFunctor rL rR (LeftIx ix)
  RightR :: rR ix -> EitherFunctor rL rR (RightIx ix)

instance (Show (rL ix)) => Show (EitherFunctor rL rR (LeftIx ix)) where
  show (LeftR v) = show v

instance (Show (rR ix)) => Show (EitherFunctor rL rR (RightIx ix)) where
  show (RightR v) = show v

unLeftR :: EitherFunctor rL rR (LeftIx ix) -> rL ix
unLeftR (LeftR v) = v

unRightR :: EitherFunctor rL rR (RightIx ix) -> rR ix
unRightR (RightR v) = v

type instance PF (MergeDomain phiL phiR) = PF phiL :+: PF phiR