{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for '(->)'.
module Language.Symantic.Lib.Function where

import Prelude hiding (const, flip, id)
import qualified Data.Function as Fun
import qualified Data.MonoTraversable as MT

import Language.Symantic

-- * Class 'Sym_Function'
type instance Sym (->) = Sym_Function
class Sym_Function term where
        comp  :: term (b -> c) -> term (a -> b) -> term (a -> c); infixr 9 `comp`
        const :: term a -> term b -> term a
        flip  :: term (a -> b -> c) -> term (b -> a -> c)
        id    :: term a -> term a
        default comp  :: Sym_Function (UnT term) => Trans term => term (b -> c) -> term (a -> b) -> term (a -> c)
        default const :: Sym_Function (UnT term) => Trans term => term a -> term b -> term a
        default flip  :: Sym_Function (UnT term) => Trans term => term (a -> b -> c) -> term (b -> a -> c)
        default id    :: Sym_Function (UnT term) => Trans term => term a -> term a
        comp  = trans2 comp
        const = trans2 const
        flip  = trans1 flip
        id    = trans1 id

-- Interpreting
instance Sym_Function Eval where
        comp  = eval2 (Fun..)
        const = eval2 Fun.const
        flip  = eval1 Fun.flip
        id    = eval1 Fun.id
instance Sym_Function View where
        comp  = viewInfix "." (infixR 9)
        const = view2 "const"
        flip  = view1 "flip"
        id    = view1 "id"
instance (Sym_Function r1, Sym_Function r2) => Sym_Function (Dup r1 r2) where
        comp  = dup2 @Sym_Function comp
        const = dup2 @Sym_Function const
        flip  = dup1 @Sym_Function flip
        id    = dup1 @Sym_Function id

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

-- Typing
instance NameTyOf (->) where
        nameTyOf _c = [] `Mod` "->"
instance ClassInstancesFor (->) where
        proveConstraintFor _c (TyConst _ _ q :$ f:@_r)
         | Just HRefl <- proj_ConstKiTy @_ @(->) f
         = case () of
                 _ | Just Refl <- proj_Const @Functor     q -> Just Dict
                   | Just Refl <- proj_Const @Applicative q -> Just Dict
                   | Just Refl <- proj_Const @Monad       q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c (tq@(TyConst _ _ q) :$ f:@_a:@b)
         | Just HRefl <- proj_ConstKiTy @_ @(->) f
         = case () of
                 _ | Just Refl <- proj_Const @Monoid q
                   , Just Dict <- proveConstraint (tq`tyApp`b) -> Just Dict
                   | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
                 _ -> Nothing
        proveConstraintFor _c _q = Nothing
instance TypeInstancesFor (->)

-- Compiling
instance Gram_Term_AtomsFor src ss g (->)
instance (Source src, SymInj ss (->)) => ModuleFor src ss (->) where
        moduleFor = ["Function"] `moduleWhere`
         [ "const" := teFunction_const
         , "flip"  := teFunction_flip
         , "id"    := teFunction_id
         , "." `withInfixR` 9 := teFunction_compose
         , "$" `withInfixR` 0 := teFunction_apply
         ]

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

a0 :: Source src => LenInj vs => KindInj (K a) =>
     Type src (Proxy a ': vs) a
a0 = tyVar "a" varZ

b1 :: Source src => LenInj vs => KindInj (K b) =>
     Type src (a ': Proxy b ': vs) b
b1 = tyVar "b" $ VarS varZ

c2 :: Source src => LenInj vs => KindInj (K c) =>
     Type src (a ': b ': Proxy c ': vs) c
c2 = tyVar "c" $ VarS $ VarS varZ

-- ** 'Term's
teFunction_compose :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((b -> c) -> (a -> b) -> (a -> c)))
teFunction_compose = Term noConstraint ((b1 ~> c2) ~> (a0 ~> b1) ~> (a0 ~> c2)) $ teSym @(->) $ lam2 comp

teFunction_const :: TermDef (->) '[Proxy a, Proxy b] (() #> (a -> b -> a))
teFunction_const = Term noConstraint (a0 ~> b1 ~> a0) $ teSym @(->) $ lam2 const

teFunction_flip :: TermDef (->) '[Proxy a, Proxy b, Proxy c] (() #> ((a -> b -> c) -> (b -> a -> c)))
teFunction_flip = Term noConstraint ((a0 ~> b1 ~> c2) ~> (b1 ~> a0 ~> c2)) $ teSym @(->) $ lam1 flip

teFunction_id :: TermDef (->) '[Proxy a] (() #> (a -> a))
teFunction_id = Term noConstraint (a0 ~> a0) $ teSym @(->) $ lam1 id

teFunction_apply :: TermDef (->) '[Proxy a, Proxy b] (() #> ((a -> b) -> a -> b))
teFunction_apply = Term noConstraint ((a0 ~> b1) ~> a0 ~> b1) $ teSym @(->) apply