-- | 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 (Var v expr h -> Var v expr h -> Bool
(Var v expr h -> Var v expr h -> Bool)
-> (Var v expr h -> Var v expr h -> Bool) -> Eq (Var v expr h)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v (expr :: HyperType) (h :: AHyperType).
Eq v =>
Var v expr h -> Var v expr h -> Bool
/= :: Var v expr h -> Var v expr h -> Bool
$c/= :: forall v (expr :: HyperType) (h :: AHyperType).
Eq v =>
Var v expr h -> Var v expr h -> Bool
== :: Var v expr h -> Var v expr h -> Bool
$c== :: forall v (expr :: HyperType) (h :: AHyperType).
Eq v =>
Var v expr h -> Var v expr h -> Bool
Eq, Eq (Var v expr h)
Eq (Var v expr h)
-> (Var v expr h -> Var v expr h -> Ordering)
-> (Var v expr h -> Var v expr h -> Bool)
-> (Var v expr h -> Var v expr h -> Bool)
-> (Var v expr h -> Var v expr h -> Bool)
-> (Var v expr h -> Var v expr h -> Bool)
-> (Var v expr h -> Var v expr h -> Var v expr h)
-> (Var v expr h -> Var v expr h -> Var v expr h)
-> Ord (Var v expr h)
Var v expr h -> Var v expr h -> Bool
Var v expr h -> Var v expr h -> Ordering
Var v expr h -> Var v expr h -> Var v expr h
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Eq (Var v expr h)
forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Bool
forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Ordering
forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Var v expr h
min :: Var v expr h -> Var v expr h -> Var v expr h
$cmin :: forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Var v expr h
max :: Var v expr h -> Var v expr h -> Var v expr h
$cmax :: forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Var v expr h
>= :: Var v expr h -> Var v expr h -> Bool
$c>= :: forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Bool
> :: Var v expr h -> Var v expr h -> Bool
$c> :: forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Bool
<= :: Var v expr h -> Var v expr h -> Bool
$c<= :: forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Bool
< :: Var v expr h -> Var v expr h -> Bool
$c< :: forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Bool
compare :: Var v expr h -> Var v expr h -> Ordering
$ccompare :: forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Var v expr h -> Var v expr h -> Ordering
$cp1Ord :: forall v (expr :: HyperType) (h :: AHyperType).
Ord v =>
Eq (Var v expr h)
Ord, Get (Var v expr h)
[Var v expr h] -> Put
Var v expr h -> Put
(Var v expr h -> Put)
-> Get (Var v expr h)
-> ([Var v expr h] -> Put)
-> Binary (Var v expr h)
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
forall v (expr :: HyperType) (h :: AHyperType).
Binary v =>
Get (Var v expr h)
forall v (expr :: HyperType) (h :: AHyperType).
Binary v =>
[Var v expr h] -> Put
forall v (expr :: HyperType) (h :: AHyperType).
Binary v =>
Var v expr h -> Put
putList :: [Var v expr h] -> Put
$cputList :: forall v (expr :: HyperType) (h :: AHyperType).
Binary v =>
[Var v expr h] -> Put
get :: Get (Var v expr h)
$cget :: forall v (expr :: HyperType) (h :: AHyperType).
Binary v =>
Get (Var v expr h)
put :: Var v expr h -> Put
$cput :: forall v (expr :: HyperType) (h :: AHyperType).
Binary v =>
Var v expr h -> Put
Binary, Var v expr h -> ()
(Var v expr h -> ()) -> NFData (Var v expr h)
forall a. (a -> ()) -> NFData a
forall v (expr :: HyperType) (h :: AHyperType).
NFData v =>
Var v expr h -> ()
rnf :: Var v expr h -> ()
$crnf :: forall v (expr :: HyperType) (h :: AHyperType).
NFData v =>
Var v expr h -> ()
NFData)
    deriving stock (Int -> Var v expr h -> ShowS
[Var v expr h] -> ShowS
Var v expr h -> String
(Int -> Var v expr h -> ShowS)
-> (Var v expr h -> String)
-> ([Var v expr h] -> ShowS)
-> Show (Var v expr h)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall v (expr :: HyperType) (h :: AHyperType).
Show v =>
Int -> Var v expr h -> ShowS
forall v (expr :: HyperType) (h :: AHyperType).
Show v =>
[Var v expr h] -> ShowS
forall v (expr :: HyperType) (h :: AHyperType).
Show v =>
Var v expr h -> String
showList :: [Var v expr h] -> ShowS
$cshowList :: forall v (expr :: HyperType) (h :: AHyperType).
Show v =>
[Var v expr h] -> ShowS
show :: Var v expr h -> String
$cshow :: forall v (expr :: HyperType) (h :: AHyperType).
Show v =>
Var v expr h -> String
showsPrec :: Int -> Var v expr h -> ShowS
$cshowsPrec :: forall v (expr :: HyperType) (h :: AHyperType).
Show v =>
Int -> Var v expr h -> ShowS
Show, (forall x. Var v expr h -> Rep (Var v expr h) x)
-> (forall x. Rep (Var v expr h) x -> Var v expr h)
-> Generic (Var v expr h)
forall x. Rep (Var v expr h) x -> Var v expr h
forall x. Var v expr h -> Rep (Var v expr h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v (expr :: HyperType) (h :: AHyperType) x.
Rep (Var v expr h) x -> Var v expr h
forall v (expr :: HyperType) (h :: AHyperType) x.
Var v expr h -> Rep (Var v expr h) x
$cto :: forall v (expr :: HyperType) (h :: AHyperType) x.
Rep (Var v expr h) x -> Var v expr h
$cfrom :: forall v (expr :: HyperType) (h :: AHyperType) x.
Var v expr h -> Rep (Var v expr h) x
Generic)

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

instance Pretty v => Pretty (Var v expr h) where
    pPrintPrec :: PrettyLevel -> Rational -> Var v expr h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (Var v
v) = PrettyLevel -> Rational -> v -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
p v
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 :: Proxy (Var v t)
-> ALens' (InferOf (Var v t) # v) (v # TypeOf (Var v t))
inferredType Proxy (Var v t)
_ = ALens' (InferOf (Var v t) # v) (v # TypeOf (Var v t))
forall (c0 :: HyperType) (k0 :: HyperType) (c1 :: HyperType)
       (k1 :: HyperType).
Iso (ANode c0 # k0) (ANode c1 # k1) (k0 # c0) (k1 # c1)
_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 v expr # InferChild m h)
-> m (Var v expr # h, InferOf (Var v expr) # UVarOf m)
inferBody (Var v
x) =
        m (ScopeOf expr ('AHyperType (UVarOf m)))
forall (m :: * -> *) (s :: HyperType).
HasScope m s =>
m (s # UVarOf m)
getScope m (ScopeOf expr ('AHyperType (UVarOf m)))
-> (ScopeOf expr ('AHyperType (UVarOf m))
    -> m (UVarOf m # TypeOf expr))
-> m (UVarOf m # TypeOf expr)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proxy expr
-> v
-> ScopeOf expr ('AHyperType (UVarOf m))
-> m (UVarOf m # TypeOf expr)
forall var (expr :: HyperType) (m :: * -> *).
(VarType var expr, UnifyGen m (TypeOf expr)) =>
Proxy expr
-> var -> (ScopeOf expr # UVarOf m) -> m (UVarOf m # TypeOf expr)
varType (Proxy expr
forall k (t :: k). Proxy t
Proxy @expr) v
x m (UVarOf m # TypeOf expr)
-> ((UVarOf m # TypeOf expr)
    -> ANode (TypeOf expr) ('AHyperType (UVarOf m)))
-> m (ANode (TypeOf expr) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (UVarOf m # TypeOf expr)
-> ANode (TypeOf expr) ('AHyperType (UVarOf m))
forall (c :: HyperType) (h :: AHyperType). (h :# c) -> ANode c h
MkANode m (ANode (TypeOf expr) ('AHyperType (UVarOf m)))
-> (ANode (TypeOf expr) ('AHyperType (UVarOf m))
    -> (Var v expr # h, ANode (TypeOf expr) ('AHyperType (UVarOf m))))
-> m (Var v expr # h, ANode (TypeOf expr) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (v -> Var v expr # h
forall v (expr :: HyperType) (h :: AHyperType). v -> Var v expr h
Var v
x, )