{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
-- | Symantic for @if@.
module Language.Symantic.Lib.If where

import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.Text as Text

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda

-- * Class 'Sym_If'
class Sym_If term where
	if_ :: term Bool -> term a -> term a -> term a
	default if_ :: Trans t term => t term Bool -> t term a -> t term a -> t term a
	if_ = trans_map3 if_

-- * Type 'If'
data If
type instance Sym_of_Iface (Proxy If) = Sym_If
type instance TyConsts_of_Iface (Proxy If) = TyConsts_imported_by (Proxy If)
type instance TyConsts_imported_by (Proxy If) = '[ Proxy Bool ]

instance Sym_If HostI where
	if_ (HostI b) ok ko = if b then ok else ko
instance Sym_If TextI where
	if_ (TextI cond) (TextI ok) (TextI ko) =
		TextI $ \po v ->
			infix_paren po op $
			Text.concat
			 [ "if ", cond (op, L) v
			 , " then ", ok (op, L) v
			 , " else ", ko (op, L) v ]
		where op = infixN 2
instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
	if_  = dupI3 @Sym_If if_

instance
 ( Read_TyNameR TyName cs rs
 ) => Read_TyNameR TyName cs (Proxy If ': rs) where
	read_TyNameR _rs = read_TyNameR (Proxy @rs)
instance Show_TyConst cs => Show_TyConst (Proxy If ': cs) where
	show_TyConst TyConstZ{} = "If"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC cs (Proxy If)
data instance TokenT meta (ts::[*]) (Proxy If)
 = Token_Term_If_if (EToken meta ts) (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy If))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy If))

instance -- CompileI
 ( Inj_TyConst cs Bool
 , Inj_TyConst cs (->)
 , Compile cs is
 ) => CompileI cs is (Proxy If) where
	compileI tok ctx k =
		case tok of
		 Token_Term_If_if tok_cond tok_ok ->
			-- if :: Bool -> a -> a -> a
			compileO tok_cond ctx $ \ty_cond (TermO cond) ->
			compileO tok_ok   ctx $ \ty_ok   (TermO ok) ->
			check_TyEq
			 (At Nothing (ty @Bool))
			 (At (Just tok_cond) ty_cond) $ \Refl ->
			k (ty_ok ~> ty_ok) $ TermO $
			 \c -> lam $ if_ (cond c) (ok c)
instance -- TokenizeT
 -- Inj_Token meta ts If =>
 TokenizeT meta ts (Proxy If)
instance Gram_Term_AtomsT meta ts (Proxy If) g -- TODO