{-# LANGUAGE GADTs, PatternSignatures #-}
{-# OPTIONS_GHC -Wall #-}
 
-------------------------------------------------------------------------------

{- |
Module      :  Language.Type.Constraint
Description :  Type equation constraints for type representation.
Copyright   :  (c) Paulo Silva
License     :  LGPL
  
Maintainer  :  paufil@di.uminho.pt
Stability   :  experimental
Portability :  portable
 
-}

-------------------------------------------------------------------------------
  
module Language.Type.Constraint  (
  Constraint(..),
  constraint2Rule,
  typeRewrite
 ) where

import Control.Monad
import Control.MonadOr
import Language.Type.Equality
import Language.Type.Rewrite
import Language.Type.Syntax

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

data Constraint where 
  (:=:) :: Type a -> Type b -> Constraint

instance Show Constraint where
  show (t1 :=: t2) = show t1 ++ " = " ++ show t2
  
instance Eq Constraint where
  (a :=: b) == (a' :=: b') = beq a a' && beq b b'

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

constraint2Rule :: Constraint -> Rule
constraint2Rule (t1 :=: t2) t1' = 
  if beq t1 t1' then return $ View t2 else mzero

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

typeRewrite :: MonadOr m => [Constraint] -> Type t -> m TypeBox
typeRewrite constr t = do
  let rules::[Rule] = map constraint2Rule constr
  return . view2Box =<< everywhere (try (seqRules rules)) t

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