-- | Variables.

{-# LANGUAGE UndecidableInstances, EmptyCase #-}
{-# LANGUAGE FlexibleInstances, TemplateHaskell, FlexibleContexts #-}

module Hyper.Type.AST.Var
    ( Var(..), _Var
    , VarType(..)
    , ScopeOf, HasScope(..)
    ) where

import Hyper
import Hyper.Infer
import Hyper.Unify (UnifyGen, UVarOf)
import Text.PrettyPrint.HughesPJClass (Pretty(..))

import Hyper.Internal.Prelude

type family ScopeOf (t :: HyperType) :: HyperType

class HasScope m s where
    getScope :: m (s # UVarOf m)

class VarType var expr where
    -- | Instantiate a type for a variable in a given scope
    varType ::
        UnifyGen m (TypeOf expr) =>
        Proxy expr -> var -> ScopeOf expr # UVarOf m ->
        m (UVarOf m # TypeOf expr)

-- | Parameterized by term AST and not by its type AST
-- (which currently is its only part used),
-- for future evaluation/complilation support.
newtype Var v (expr :: HyperType) (h :: AHyperType) = Var v
    deriving newtype (Eq, Ord, Binary, NFData)
    deriving stock (Show, Generic)

makePrisms ''Var
makeHTraversableApplyAndBases ''Var
makeZipMatch ''Var
makeHContext ''Var
makeHMorph ''Var

instance Pretty v => Pretty (Var v expr h) where
    pPrintPrec lvl p (Var v) = pPrintPrec lvl p v

type instance InferOf (Var _ t) = ANode (TypeOf t)

instance HasInferredType (Var v t) where
    type instance (TypeOf (Var v t)) = TypeOf t
    {-# INLINE inferredType #-}
    inferredType _ = _ANode

instance
    ( UnifyGen m (TypeOf expr)
    , HasScope m (ScopeOf expr)
    , VarType v expr
    , Monad m
    ) =>
    Infer m (Var v expr) where

    {-# INLINE inferBody #-}
    inferBody (Var x) =
        getScope >>= varType (Proxy @expr) x <&> MkANode <&> (Var x, )