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

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

import qualified Data.Bool as Bool
import Prelude hiding (and, not, or)

import Language.LOL.Symantic.Trans.Common
import Language.LOL.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
	
	and (Trans_Bool_Const_Known True) y   = y
	and (Trans_Bool_Const_Known False) _y = Trans_Bool_Const_Known False
	and x  (Trans_Bool_Const_Known True)  = x
	and _x (Trans_Bool_Const_Known False) = Trans_Bool_Const_Known False
	and (Trans_Bool_Const_Unknown x)
	    (Trans_Bool_Const_Unknown y)
	 =   Trans_Bool_Const_Unknown $ and x y
	
	or (Trans_Bool_Const_Known False) y = y
	or (Trans_Bool_Const_Known True) _y = Trans_Bool_Const_Known True
	or x (Trans_Bool_Const_Known False) = x
	or _x (Trans_Bool_Const_Known True) = Trans_Bool_Const_Known True
	or (Trans_Bool_Const_Unknown x)
	   (Trans_Bool_Const_Unknown y)
	 =  Trans_Bool_Const_Unknown $ or x y

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