{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
-- | Symantic for @if@.
module Language.Symantic.Compiling.If where

import Data.Monoid ((<>))
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Bool (tyBool)
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * 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 Consts_of_Iface (Proxy If) = Consts_imported_by If
type instance Consts_imported_by 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 $ \p v ->
			let p' = Precedence 2 in
			paren p p' $
			"if " <> cond p' v <>
			" then " <> ok p' v <>
			" else " <> ko p' v
instance (Sym_If r1, Sym_If r2) => Sym_If (DupI r1 r2) where
	if_  = dupI3 sym_If if_

instance Const_from Text cs => Const_from Text (Proxy If ': cs) where
	const_from s k = const_from s $ k . ConstS

instance -- If
 Proj_ConC cs (Proxy If)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Term_from is ast
 ) => Term_fromI is (Proxy If) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "if" -> if_from
		 _ -> Left $ Error_Term_unsupported
		where
		if_from =
		 -- if :: Bool -> a -> a -> a
			from_ast3 ast $ \ast_cond ast_ok ast_ko as ->
			term_from ast_cond ctx $ \ty_cond (TermLC cond) ->
			term_from ast_ok   ctx $ \ty_ok   (TermLC ok) ->
			term_from ast_ko   ctx $ \ty_ko   (TermLC ko) ->
			check_type (At Nothing tyBool) (At (Just ast_cond) ty_cond) $ \Refl ->
			check_type (At (Just ast_ok) ty_ok) (At (Just ast_ko) ty_ko) $ \Refl ->
			k as ty_ok $ TermLC $
			 \c -> if_ (cond c) (ok c) (ko c)

sym_If :: Proxy Sym_If
sym_If = Proxy

syIf :: IsString a => Syntax a -> Syntax a -> Syntax a -> Syntax a
syIf cond ok ko = Syntax "if" [cond, ok, ko]