{-# LANGUAGE UndecidableInstances, ExistentialQuantification,
            MultiParamTypeClasses, FlexibleInstances, RankNTypes #-}
-----------------------------------------------------------------------------
-- | License      :  GPL
-- 
--   Maintainer   :  helium@cs.uu.nl
--   Stability    :  provisional
--   Portability  :  non-portable (requires extensions)
--
-- A data type to represent constraints in general, and a type class for
-- constraints that are solvable.
--
-----------------------------------------------------------------------------

module Top.Constraint where

import Top.Types (Substitutable(..))

type Constraints m = [Constraint m]
data Constraint  m = 
   forall c . (Show c, Substitutable c) => Constraint c (c -> m ()) (c -> m Bool)

-- |A constraint is solvable if it knows how it can be solved in a certain
-- state (a monadic operation), if it can check afterwards whether the final
-- state satisfies it, and when it can be shown.
class (Show c, Substitutable c, Monad m) => Solvable c m where 
   solveConstraint :: c -> m ()
   checkCondition  :: c -> m Bool
   
   -- default definition
   checkCondition _ = return True

instance Show (Constraint m) where 
   show (Constraint c _ _) = show c

instance Substitutable (Constraint m) where
   ftv (Constraint c _ _)     = ftv c
   sub |-> (Constraint c f g) = Constraint (sub |-> c) f g

instance Monad m => Solvable (Constraint m) m where
   solveConstraint (Constraint c f _) = f c
   checkCondition  (Constraint c _ g) = g c

-- |Lifting a constraint to the Constraint data type. Every instance of
-- the Solvable type class can be lifted.
liftConstraint :: Solvable c m => c -> Constraint m
liftConstraint c = Constraint c solveConstraint checkCondition

liftConstraints :: Solvable c m => [c] -> Constraints m
liftConstraints = map liftConstraint

mapConstraint :: (forall a . m1 a -> m2 a) -> Constraint m1 -> Constraint m2
mapConstraint t (Constraint c f g) = Constraint c (t . f) (t . g)

newtype Operation m = Op_ String

operation :: Monad m => String -> m () -> Constraint m
operation s m = Constraint (Op_ s) (const m) (const (return True))

instance Show (Operation m) where
   show (Op_ s) = "<" ++ s ++ ">"

instance Substitutable (Operation m) where
   ftv _    = []
   _ |-> op = op

-- |If both constraints of type 'a' and 'b' can be solved in a Monad 'm', then
-- 'Either a b' constraints can also be solved in this monad.
instance (Solvable a m, Solvable b m) => Solvable (Either a b) m where
   solveConstraint = either solveConstraint solveConstraint
   checkCondition  = either checkCondition  checkCondition

-- |The data type ConstraintSum is similar to the (standard) Either data type.    
-- However, its Show instance is slightly different as the name of the constructor
-- is not shown.
data ConstraintSum f g info 
   = SumLeft  (f info) 
   | SumRight (g info)

instance (Show (f info), Show (g info)) => Show (ConstraintSum f g info) where
   show = constraintSum show show

instance (Functor f, Functor g) => Functor (ConstraintSum f g) where
   fmap f = constraintSum (SumLeft . fmap f) (SumRight . fmap f)

instance (Substitutable (f info), Substitutable (g info)) => Substitutable (ConstraintSum f g info) where
   (|->) sub = constraintSum (SumLeft . (sub |->)) (SumRight . (sub |->))
   ftv       = constraintSum ftv ftv

instance (Solvable (f info) m, Solvable (g info) m) => Solvable (ConstraintSum f g info) m where
   solveConstraint = constraintSum solveConstraint solveConstraint
   checkCondition  = constraintSum checkCondition  checkCondition

-- |Similar to the 'either' function.
constraintSum :: (f info -> c) -> (g info -> c) -> ConstraintSum f g info -> c
constraintSum f _ (SumLeft a)  = f a
constraintSum _ f (SumRight b) = f b