{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-- | Transformer propagating boolean constants.
module Language.Symantic.Trans.Bool.Const where

import qualified Data.Bool as Bool
import Prelude hiding ((&&), not, (||))

import Language.Symantic.Trans.Common
import Language.Symantic.Expr.Bool

-- * Type 'Trans_Bool_Const'

-- | Annotation.
data Trans_Bool_Const repr h where
	Trans_Bool_Const_Unknown :: repr h -> Trans_Bool_Const repr h
	Trans_Bool_Const_Known   :: Bool   -> Trans_Bool_Const repr Bool

instance
 Sym_Bool repr =>
 Trans Trans_Bool_Const repr where
	trans_lift = Trans_Bool_Const_Unknown
	trans_apply (Trans_Bool_Const_Unknown x) = x
	trans_apply (Trans_Bool_Const_Known   x) = bool x

instance
 Sym_Bool repr =>
 Sym_Bool (Trans_Bool_Const repr) where
	bool = Trans_Bool_Const_Known
	
	not (Trans_Bool_Const_Unknown e) = Trans_Bool_Const_Unknown $ not e
	not (Trans_Bool_Const_Known   x) = Trans_Bool_Const_Known $ Bool.not x
	
	(&&) (Trans_Bool_Const_Known True) y   = y
	(&&) (Trans_Bool_Const_Known False) _y = Trans_Bool_Const_Known False
	(&&) x  (Trans_Bool_Const_Known True)  = x
	(&&) _x (Trans_Bool_Const_Known False) = Trans_Bool_Const_Known False
	(&&) (Trans_Bool_Const_Unknown x)
	     (Trans_Bool_Const_Unknown y)
	 =   Trans_Bool_Const_Unknown $ (&&) x y
	
	(||) (Trans_Bool_Const_Known False) y = y
	(||) (Trans_Bool_Const_Known True) _y = Trans_Bool_Const_Known True
	(||) x (Trans_Bool_Const_Known False) = x
	(||) _x (Trans_Bool_Const_Known True) = Trans_Bool_Const_Known True
	(||) (Trans_Bool_Const_Unknown x)
	     (Trans_Bool_Const_Unknown y)
	 =  Trans_Bool_Const_Unknown $ (||) x y

-- | Transformer.
trans_bool_const
 :: Sym_Bool repr
 => (Trans_Bool_Const repr) h -> repr h
trans_bool_const = trans_apply