{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Bool'.
module Language.Symantic.Lib.Bool where

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

import Language.Symantic
import Language.Symantic.Lib.Function ()

-- * Class 'Sym_Bool'
type instance Sym Bool = Sym_Bool
class Sym_Bool term where
        bool ::      Bool -> term Bool
        not  :: term Bool -> term Bool
        (&&) :: term Bool -> term Bool -> term Bool; infixr 3 &&
        (||) :: term Bool -> term Bool -> term Bool; infixr 2 ||
        xor  :: term Bool -> term Bool -> term Bool; infixr 2 `xor`
        xor x y = (x || y) && not (x && y)

        default bool :: Sym_Bool (UnT term) => Trans term =>      Bool -> term Bool
        default not  :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool
        default (&&) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool
        default (||) :: Sym_Bool (UnT term) => Trans term => term Bool -> term Bool -> term Bool

        bool = trans . bool
        not  = trans1 not
        (&&) = trans2 (&&)
        (||) = trans2 (||)

-- Interpreting
instance Sym_Bool Eval where
        bool = Eval
        not  = liftM Bool.not
        (&&) = liftM2 (Bool.&&)
        (||) = liftM2 (Bool.||)
instance Sym_Bool View where
        bool o = View $ \_p _v -> Text.pack (show o)
        not    = view1 "not"
        (&&)   = viewInfix "&&"    (infixR 3)
        (||)   = viewInfix "||"    (infixR 2)
        xor    = viewInfix "`xor`" (infixR 2)
instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (Dup r1 r2) where
        bool b = bool b `Dup` bool b
        not    = dup1 @Sym_Bool not
        (&&)   = dup2 @Sym_Bool (&&)
        (||)   = dup2 @Sym_Bool (||)
        xor    = dup2 @Sym_Bool xor

-- Transforming
instance (Sym_Lambda term, Sym_Bool term) => Sym_Bool (BetaT term) where
        xor = trans2 xor

-- Typing
instance NameTyOf Bool where
        nameTyOf _c = ["Bool"] `Mod` "Bool"
instance ClassInstancesFor Bool where
        proveConstraintFor _ (TyConst _ _ q :@ b)
         | Just HRefl <- proj_ConstKiTy @_ @Bool b
         = case () of
                 _ | Just Refl <- proj_Const @Bounded q -> Just Dict
                   | Just Refl <- proj_Const @Enum    q -> Just Dict
                   | Just Refl <- proj_Const @Eq      q -> Just Dict
                   | Just Refl <- proj_Const @Ord     q -> Just Dict
                   | Just Refl <- proj_Const @Show    q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Bool

-- Compiling
instance Gram_Term_AtomsFor src ss g Bool
instance (Source src, SymInj ss Bool) => ModuleFor src ss Bool where
        moduleFor = ["Bool"] `moduleWhere`
         [ "False" := teBool False
         , "True"  := teBool True
         , "not"   := teBool_not
         , "and" `withInfixR` 3 := teBool_and
         , "or"  `withInfixR` 2 := teBool_or
         , "xor" `withInfixR` 2 := teBool_xor
         ]

-- ** 'Type's
tyBool :: Source src => LenInj vs => Type src vs Bool
tyBool = tyConst @(K Bool) @Bool

-- ** 'Term's
teBool :: Source src => SymInj ss Bool => Bool -> Term src ss ts '[] (() #> Bool)
teBool b = Term noConstraint tyBool $ teSym @Bool $ bool b

teBool_not :: TermDef Bool '[] (() #> (Bool -> Bool))
teBool_not = Term noConstraint (tyBool ~> tyBool) $ teSym @Bool $ lam1 not

teBool_and, teBool_or, teBool_xor :: TermDef Bool '[] (() #> (Bool -> Bool -> Bool))
teBool_and = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (&&)
teBool_or  = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 (||)
teBool_xor = Term noConstraint (tyBool ~> tyBool ~> tyBool) $ teSym @Bool $ lam2 xor