-- | Beta-reduction of 'Term's.
module Language.Symantic.Compiling.Beta where

import Control.Arrow (left)
import qualified Data.Kind as K

import Language.Symantic.Grammar
import Language.Symantic.Typing
import Language.Symantic.Compiling.Term

-- | Term application: apply second given 'TermT' to the first,
-- applying embedded 'TeSym's, or return an error.
betaTerm ::
 forall src ss es vs fun arg.
 Inj_Source (TypeVT src) src =>
 Constable (->) =>
 Term src ss es vs (fun::K.Type) ->
 Term src ss es vs (arg::K.Type) ->
 Either (Error_Beta src) (TermT src ss es vs)
betaTerm (Term qf tf (TeSym te_fun)) (Term qa ta (TeSym te_arg)) =
	case tf of
	 TyApp _ (TyApp _ a2b a2b_a) a2b_b
	  | Just HRefl <- proj_ConstKiTy @(K (->)) @(->) a2b ->
		case a2b_a `eqType` ta of
		 Nothing -> Left $ Error_Beta_Type_mismatch (TypeVT a2b_a) (TypeVT ta)
		 Just Refl ->
			Right $
			case (proveConstraint qf, proveConstraint qa) of
			 -- NOTE: remove provable Constraints to keep those smaller.
			 (Just Dict, Just Dict) -> TermT $ Term (noConstraintLen (lenVars a2b_b)) a2b_b $
				TeSym $ \c -> te_fun c `app` te_arg c
			 (Just Dict, Nothing) -> TermT $ Term qa a2b_b $
				TeSym $ \c -> te_fun c `app` te_arg c
			 (Nothing, Just Dict) -> TermT $ Term qf a2b_b $
				TeSym $ \c -> te_fun c `app` te_arg c
			 (Nothing, Nothing) -> TermT $ Term (qf # qa) a2b_b $
				TeSym $ \c -> te_fun c `app` te_arg c
	 _ -> Left $ Error_Beta_Term_not_a_function $ TypeVT (qf #> tf)

-- | Collapse given 'BinTree' of 'TermVT's to compute a resulting 'TermVT', if possible.
betaTerms ::
 Inj_Source (TypeVT src) src =>
 Constable (->) =>
 BinTree (TermVT src ss es) ->
 Either (Error_Beta src) (TermVT src ss es)
betaTerms t =
	collapseBT (\acc ele -> do
		TermVT (Term qf tf te_fun) <- acc
		TermVT (Term qa ta te_arg) <- ele
		let (tf', ta') = appendVars tf ta
		let (qf', qa') = appendVars qf qa
		case unTyFun tf' of
		 Nothing -> Left $ Error_Beta_Term_not_a_function $ TypeVT tf'
		 Just (af, _rf) -> do
			mgu <-
				(Error_Beta_Unify `left`) $
				case (unQualsTy af, unQualsTy ta') of
				 (TypeK af', TypeK ta'') -> unifyType mempty af' ta''
			let qf'' = subst mgu qf'
			let qa'' = subst mgu qa'
			let tf'' = subst mgu tf'
			let ta'' = subst mgu ta'
			TermT (Term qr tr te_res) <- betaTerm (Term qf'' tf'' te_fun) (Term qa'' ta'' te_arg)
			normalizeVarsTy (qr #> tr) $ \(TyApp _ (TyApp _ _c qr') tr') ->
				Right $ TermVT $ Term qr' tr' te_res
	 ) (Right <$> t)

-- * Type 'Error_Beta'
data Error_Beta src
 =   Error_Beta_Term_not_a_function (TypeVT src)
 |   Error_Beta_Type_mismatch (TypeVT src) (TypeVT src)
 |   Error_Beta_Unify (Error_Unify src)
     -- ^ Cannot unify the expected 'Type' of the argument of the function,
     -- with the 'Type' of the argument.
 deriving (Eq, Show)

instance Inj_Error (Error_Beta src) (Error_Beta src) where
	inj_Error = id
instance Inj_Error (Error_Unify src) (Error_Beta src) where
	inj_Error = Error_Beta_Unify