Var.hs

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

-- | Variables.
module Hyper.Syntax.Var
    ( Var (..)
    , _Var
    , VarType (..)
    , ScopeOf
    , HasScope (..)
    ) where

import Hyper
import Hyper.Infer
import Hyper.Unify (UVarOf, UnifyGen)
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 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 <&> (Var x,) . MkANode