{-# LANGUAGE GADTs, TypeOperators, FlexibleContexts, Rank2Types #-}
{-# OPTIONS_GHC -Wall #-}

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

{- |
Module      :  Galculator.Engine.GcToLaw
Description :  
Copyright   :  (c) Paulo Silva
License     :  LGPL

Maintainer  :  paufil@di.uminho.pt
Stability   :  experimental
Portability :  portable

-}

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

module Galculator.Engine.GcToLaw (
  --gc2Rules,
  rType2Law,
  gcProperties,
  gcPropertyFunc,
  gcShunting,
  gcDistributivityUpper,
  gcDistributivityLower,
  gcMonotonicityUpper,
  gcMonotonicityLower,
  gcPreservingBottom,
  gcPreservingTop,
  gcCancellationUpper,
  gcCancellationLower
 )  where

import Control.GalcError
import Control.Monad.Error
import Control.Monad.Fresh 
import Data.Existential
--import Galculator.Engine.LawToRule
--import Galculator.Rule
import Language.Law.Syntax
import Language.R.Syntax
import Language.Type.Syntax

-------------------------------------------------------------------------------
{-
gc2Rules :: Type (GC b a) -> R (GC b a) -> [Rule]
gc2Rules t gc = map getRule pp  ++
                map getRuleInv pp
  where pp = gcProperties t gc
-}
-------------------------------------------------------------------------------

rType2Law :: (MonadFresh [String] String m, MonadError GalcError m)
          => RType -> (forall a . Type a -> R a -> m Law) -> m Law
rType2Law (Exists t g) f = f t g

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

gcProperties :: Type (GC b a) -> R (GC b a) -> [Law]
gcProperties t gc = map (\f -> f t gc) gcPropertyFunc

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

gcPropertyFunc :: [Type (GC b a) -> R (GC b a) -> Law]
gcPropertyFunc = [] {- [
  gcShunting,
  --gcDistributivityUpper, 
  --gcDistributivityLower,
  gcMonotonicityUpper,
  gcMonotonicityLower, 
  gcPreservingTop,
  gcPreservingBottom, 
  gcCancellationUpper,
  gcCancellationLower
 ]-}

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

gcShunting :: (MonadFresh [String] String m, MonadError GalcError m)
           => Type a -> R a -> m Law
gcShunting (GC b a) g = do
  ladj <- lowerAdjoint g
  uadj <- upperAdjoint g
  lord <- lowerOrder g
  uord <- upperOrder g
  return $ 
        EQUIV (Meta "Shunting" (Just GCSHUNT))
        (Rel a b)
        (COMP b (CONV ladj) (ORD lord))
        (COMP a (ORD uord) uadj)
gcShunting _ _ = throwError ImpossibleError

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

gcDistributivityUpper :: (MonadFresh [String] String m, MonadError GalcError m)
                      => Type a -> R a -> m Law
gcDistributivityUpper (GC b a) g = do
  uadj <- upperAdjoint g
  lord <- lowerOrder g
  uord <- upperOrder g
  return $
        EQUIV (Meta ("Distributivity (Upper adjoint)") (Just GCDISTR) )
        (Rel a (Prod b b))
        (COMP b uadj (FUN (OMeet lord)))
        (COMP (Prod a a) (FUN (OMeet uord)) (PROD uadj uadj))
gcDistributivityUpper _ _ = error "gcDistributivityUpper"

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

gcDistributivityLower :: (MonadFresh [String] String m, MonadError GalcError m)
                      => Type a -> R a -> m Law
gcDistributivityLower (GC b a) g = do
  ladj <- lowerAdjoint g
  lord <- lowerOrder g
  uord <- upperOrder g
  return $
        EQUIV (Meta ("Distributivity (Lower adjoint)") (Just GCDISTR) )
        (Rel b (Prod a a))
        (COMP a ladj (FUN (OJoin uord)))
        (COMP (Prod b b) (FUN (OJoin lord)) (PROD ladj ladj))
gcDistributivityLower _ _ = error "gcDistributivityLower"

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

gcMonotonicityUpper :: (MonadFresh [String] String m, MonadError GalcError m)
                    => Type a -> R a -> m Law
gcMonotonicityUpper (GC b a) g = do
  uadj <- upperAdjoint g
  lord <- lowerOrder g
  uord <- upperOrder g
  return $
       IMPL (Meta "Monotonicity (upper adjoint)" (Just GCMONOT))
       (Rel a b)
       (COMP b uadj (ORD lord))
       (COMP a (ORD uord) uadj)
gcMonotonicityUpper _ _ = error "gcMonotonicityUpper"

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

gcMonotonicityLower :: (MonadFresh [String] String m, MonadError GalcError m)
                    => Type a -> R a -> m Law
gcMonotonicityLower (GC b a) g = do
  ladj <- lowerAdjoint g
  lord <- lowerOrder g
  uord <- upperOrder g
  return $ 
       IMPL (Meta "Monotonicity (lower adjoint)" (Just GCMONOT))
       (Rel b a)
       (COMP a ladj (ORD uord))
       (COMP b (ORD lord) ladj)
gcMonotonicityLower _ _ = error "gcMonotonicityLower"

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

gcPreservingTop :: (MonadFresh [String] String m, MonadError GalcError m)
                => Type a -> R a -> m Law
gcPreservingTop (GC b a) g = do
  uadj <- upperAdjointF g
  lord <- lowerOrder g
  uord <- upperOrder g
  return $
        EQUIV (Meta "Top preserving" (Just GCTOP))
        a
        (APPLY b uadj (OMax lord))
        (OMax uord)
gcPreservingTop _ _ = error "gcPreservingTop"

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

gcPreservingBottom :: (MonadFresh [String] String m, MonadError GalcError m)
                   => Type a -> R a -> m Law
gcPreservingBottom (GC b a) g = do
  ladj <- lowerAdjointF g
  lord <- lowerOrder g
  uord <- upperOrder g
  return $
        EQUIV (Meta "Bottom preserving" (Just GCBOT))
        b
        (APPLY a ladj (OMin uord))
        (OMin lord)
gcPreservingBottom _ _ = error "gcPreservingBottom"

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

gcCancellationUpper :: (MonadFresh [String] String m, MonadError GalcError m)
                    => Type a -> R a -> m Law
gcCancellationUpper (GC b a) g = do
  ladj <- lowerAdjoint g
  uadj <- upperAdjoint g
  uord <- upperOrder g
  return $
       IMPL (Meta "Cancellation (upper adjoint)" (Just GCCANC))
       (Rel a a)
       (ORD uord)
       (COMP a (ORD uord) (COMP b uadj ladj))
gcCancellationUpper _ _ = error "gcCancellationUpper"

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

gcCancellationLower :: (MonadFresh [String] String m, MonadError GalcError m)
                    => Type a -> R a -> m Law
gcCancellationLower (GC b a) g = do
  ladj <- lowerAdjoint g
  uadj <- upperAdjoint g
  lord <- lowerOrder g
  return $
       IMPL (Meta "Cancellation (lowerAdjoint)" (Just GCCANC))
       (Rel b b)
       (COMP b (COMP a ladj uadj) (ORD lord))
       (ORD lord)
gcCancellationLower _ _ = error "gcCancellationLower"

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

upperAdjoint :: MonadError GalcError m => R (GC b a) -> m (R (a :<->: b))
upperAdjoint (GDef _ _ g _ _) = return $ FUN g
upperAdjoint GId = return ID
upperAdjoint (GComp t g1 g2) = do
  g1' <- upperAdjoint g1
  g2' <- upperAdjoint g2
  return $ COMP t g2' g1'
upperAdjoint (GConv g) = lowerAdjoint g
upperAdjoint _ = throwError ImpossibleError

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

lowerAdjoint :: MonadError GalcError m => R (GC b a) -> m (R (b :<->: a))
lowerAdjoint (GDef _ f _ _ _) = return $ FUN f
lowerAdjoint GId = return ID
lowerAdjoint (GComp t g1 g2) = do
  g1' <- lowerAdjoint g1 
  g2' <- lowerAdjoint g2
  return $ COMP t g1' g2'
lowerAdjoint (GConv g) = upperAdjoint g
lowerAdjoint _ = throwError ImpossibleError

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

upperAdjointF :: MonadError GalcError m => R (GC b a) -> m (R (a :<-: b))
upperAdjointF (GDef _ _ g _ _) = return g
upperAdjointF GId = return FId 
upperAdjointF (GComp t g1 g2) = do
  g1' <- upperAdjointF g1
  g2' <- upperAdjointF g2
  return $ FComp t g2' g1'
upperAdjointF (GConv g) = lowerAdjointF g
upperAdjointF _ = throwError ImpossibleError

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

lowerAdjointF :: MonadError GalcError m => R (GC b a) -> m (R (b :<-: a))
lowerAdjointF (GDef _ f _ _ _) = return f
lowerAdjointF GId = return FId
lowerAdjointF (GComp t g1 g2) = do
  g1' <- lowerAdjointF g1
  g2' <- lowerAdjointF g2
  return $ FComp t g1' g2'
lowerAdjointF (GConv g) = upperAdjointF g
lowerAdjointF _ = throwError ImpossibleError

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

lowerOrder :: (MonadFresh [String] String m, MonadError GalcError m) 
           => R (GC b a) -> m (R (PO b))
lowerOrder (GDef _ _ _ o _) = return o
lowerOrder GId = do
  o <- getFresh 
  return $ Var ('o':o)
lowerOrder (GComp _ g1 _) = lowerOrder g1
lowerOrder (GConv g) = do
  g' <- upperOrder g
  return $ OConv g'
lowerOrder _ = error "lowerOrder"

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

upperOrder :: (MonadFresh [String] String m, MonadError GalcError m) 
           => R (GC b a) -> m (R (PO a))
upperOrder (GDef _ _ _ _ o) = return o
upperOrder GId = do
  o <- getFresh
  return $ Var ('o':o)
upperOrder (GComp _ _ g2) = upperOrder g2
upperOrder (GConv g) = do
  g' <- lowerOrder g
  return $ OConv g'
upperOrder _ = error "upperOrder"

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