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

import Control.Applicative (Alternative)
import Prelude hiding (Functor(..))
import qualified Control.Applicative as Alternative

import Language.Symantic
import Language.Symantic.Lib.Functor (Sym_Functor(..), f1)
import Language.Symantic.Lib.Function (a0)

-- * Class 'Sym_Alternative'
type instance Sym Alternative = Sym_Alternative
class Sym_Functor term => Sym_Alternative term where
	empty :: Alternative f => term (f a)
	(<|>) :: Alternative f => term (f a) -> term (f a) -> term (f a)
	infixl 3 <|>
	
	default empty :: Sym_Alternative (UnT term) => Trans term => Alternative f => term (f a)
	default (<|>) :: Sym_Alternative (UnT term) => Trans term => Alternative f => term (f a) -> term (f a) -> term (f a)
	
	empty = trans empty
	(<|>) = trans2 (<|>)

-- Interpreting
instance Sym_Alternative Eval where
	empty = Eval Alternative.empty
	(<|>) = eval2 (Alternative.<|>)
instance Sym_Alternative View where
	empty = view0 "empty"
	(<|>) = viewInfix "<|>" (infixL 3)
instance (Sym_Alternative r1, Sym_Alternative r2) => Sym_Alternative (Dup r1 r2) where
	empty = dup0 @Sym_Alternative empty
	(<|>) = dup2 @Sym_Alternative (<|>)

-- Transforming
instance (Sym_Lambda term, Sym_Alternative term) => Sym_Alternative (BetaT term)

-- Typing
instance NameTyOf Alternative where
	nameTyOf _c = ["Alternative"] `Mod` "Alternative"
instance FixityOf Alternative
instance ClassInstancesFor Alternative
instance TypeInstancesFor Alternative

-- Compiling
instance Gram_Term_AtomsFor src ss g Alternative
instance (Source src, SymInj ss Alternative) => ModuleFor src ss Alternative where
	moduleFor = ["Alternative"] `moduleWhere`
	 [ "empty" := teAlternative_empty
	 , "<|>" `withInfixL` 3 := teAlternative_alt
	 ]

-- ** 'Type's
tyAlternative :: Source src => Type src vs a -> Type src vs (Alternative a)
tyAlternative a = tyConstLen @(K Alternative) @Alternative (lenVars a) `tyApp` a

-- ** 'Term's
teAlternative_empty :: TermDef Alternative '[Proxy a, Proxy f] (Alternative f #> f a)
teAlternative_empty = Term (tyAlternative f1) (f1 `tyApp` a0) $ teSym @Alternative $ empty

teAlternative_alt :: TermDef Alternative '[Proxy a, Proxy f] (Alternative f #> (f a -> f a -> f a))
teAlternative_alt = Term (tyAlternative f1) (f1 `tyApp` a0 ~> f1 `tyApp` a0 ~> f1 `tyApp` a0) $ teSym @Alternative $ lam2 (<|>)