-- | Type signatures

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

module Hyper.Type.AST.TypeSig
    ( TypeSig(..), tsType, tsTerm, W_TypeSig(..)
    ) where

import           Generics.Constraints (Constraints)
import           Hyper
import           Hyper.Infer
import           Hyper.Type.AST.Scheme
import           Hyper.Unify (UnifyGen, unify)
import           Hyper.Unify.Generalize (instantiateWith)
import           Hyper.Unify.Term (UTerm(..))
import           Text.PrettyPrint ((<+>))
import qualified Text.PrettyPrint as Pretty
import           Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)

import           Hyper.Internal.Prelude

data TypeSig vars term h = TypeSig
    { TypeSig vars term h -> h :# term
_tsTerm :: h :# term
    , TypeSig vars term h -> h :# Scheme vars (TypeOf term)
_tsType :: h :# Scheme vars (TypeOf term)
    } deriving (forall x. TypeSig vars term h -> Rep (TypeSig vars term h) x)
-> (forall x. Rep (TypeSig vars term h) x -> TypeSig vars term h)
-> Generic (TypeSig vars term h)
forall x. Rep (TypeSig vars term h) x -> TypeSig vars term h
forall x. TypeSig vars term h -> Rep (TypeSig vars term h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType) x.
Rep (TypeSig vars term h) x -> TypeSig vars term h
forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType) x.
TypeSig vars term h -> Rep (TypeSig vars term h) x
$cto :: forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType) x.
Rep (TypeSig vars term h) x -> TypeSig vars term h
$cfrom :: forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType) x.
TypeSig vars term h -> Rep (TypeSig vars term h) x
Generic

makeLenses ''TypeSig
makeCommonInstances [''TypeSig]
makeHTraversableApplyAndBases ''TypeSig

instance
    Constraints (TypeSig vars term h) Pretty =>
    Pretty (TypeSig vars term h) where
    pPrintPrec :: PrettyLevel -> Rational -> TypeSig vars term h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (TypeSig h :# term
term h :# Scheme vars (TypeOf term)
typ) =
        PrettyLevel -> Rational -> (h :# term) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
1 h :# term
term Doc -> Doc -> Doc
<+> String -> Doc
Pretty.text String
":" Doc -> Doc -> Doc
<+> PrettyLevel -> Rational -> (h :# Scheme vars (TypeOf term)) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
1 h :# Scheme vars (TypeOf term)
typ
        Doc -> (Doc -> Doc) -> Doc
forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
1)

type instance InferOf (TypeSig _ t) = InferOf t

instance
    ( MonadScopeLevel m
    , HasInferredType term
    , HasInferredValue (TypeOf term)
    , HTraversable vars
    , HTraversable (InferOf term)
    , HNodesConstraint (InferOf term) (UnifyGen m)
    , HNodesConstraint vars (MonadInstantiate m)
    , UnifyGen m (TypeOf term)
    , Infer m (TypeOf term)
    , Infer m term
    ) =>
    Infer m (TypeSig vars term) where

    inferBody :: (TypeSig vars term # InferChild m h)
-> m (TypeSig vars term # h,
      InferOf (TypeSig vars term) # UVarOf m)
inferBody (TypeSig 'AHyperType (InferChild m h) :# term
x 'AHyperType (InferChild m h) :# Scheme vars (TypeOf term)
s) =
        do
            InferredChild h ('AHyperType term)
xI InferOf (GetHyperType ('AHyperType term)) # UVarOf m
xR <- InferChild m h ('AHyperType term)
-> m (InferredChild (UVarOf m) h ('AHyperType term))
forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# term
InferChild m h ('AHyperType term)
x
            InferredChild h ('AHyperType (Scheme vars (TypeOf term)))
sI InferOf (GetHyperType ('AHyperType (Scheme vars (TypeOf term))))
# UVarOf m
sR <- InferChild m h ('AHyperType (Scheme vars (TypeOf term)))
-> m (InferredChild
        (UVarOf m) h ('AHyperType (Scheme vars (TypeOf term))))
forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# Scheme vars (TypeOf term)
InferChild m h ('AHyperType (Scheme vars (TypeOf term)))
s
            (UVarOf m # TypeOf term
t, ()) <- m ()
-> (forall (n :: AHyperType -> *).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # TypeOf term)
-> m (UVarOf m # TypeOf term, ())
forall (m :: * -> *) (t :: AHyperType -> *) a.
UnifyGen m t =>
m a
-> (forall (n :: AHyperType -> *).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith (() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem (HFlip GTerm (TypeOf term) ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType (Scheme vars (TypeOf term))))
# UVarOf m
sR HFlip GTerm (TypeOf term) ('AHyperType (UVarOf m))
-> Getting
     (GTerm (UVarOf m) # TypeOf term)
     (HFlip GTerm (TypeOf term) ('AHyperType (UVarOf m)))
     (GTerm (UVarOf m) # TypeOf term)
-> GTerm (UVarOf m) # TypeOf term
forall s a. s -> Getting a s a -> a
^. Getting
  (GTerm (UVarOf m) # TypeOf term)
  (HFlip GTerm (TypeOf term) ('AHyperType (UVarOf m)))
  (GTerm (UVarOf m) # TypeOf term)
forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
       (x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
       (f1 :: (AHyperType -> *) -> AHyperType -> *)
       (x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip)
            InferOf term # UVarOf m
InferOf (GetHyperType ('AHyperType term)) # UVarOf m
xR (InferOf term # UVarOf m)
-> ((InferOf term # UVarOf m) -> m (InferOf term # UVarOf m))
-> m (InferOf term # UVarOf m)
forall a b. a -> (a -> b) -> b
& Proxy term
-> ((UVarOf m # TypeOf term)
    -> Pretext
         (->)
         (UVarOf m # TypeOf term)
         (UVarOf m # TypeOf term)
         (UVarOf m # TypeOf term))
-> (InferOf term # UVarOf m)
-> Pretext
     (->)
     (UVarOf m # TypeOf term)
     (UVarOf m # TypeOf term)
     (InferOf term # UVarOf m)
forall (t :: AHyperType -> *) (v :: AHyperType -> *).
HasInferredType t =>
Proxy t -> ALens' (InferOf t # v) (v # TypeOf t)
inferredType (Proxy term
forall k (t :: k). Proxy t
Proxy @term) (((UVarOf m # TypeOf term)
  -> Pretext
       (->)
       (UVarOf m # TypeOf term)
       (UVarOf m # TypeOf term)
       (UVarOf m # TypeOf term))
 -> (InferOf term # UVarOf m)
 -> Pretext
      (->)
      (UVarOf m # TypeOf term)
      (UVarOf m # TypeOf term)
      (InferOf term # UVarOf m))
-> ((UVarOf m # TypeOf term) -> m (UVarOf m # TypeOf term))
-> (InferOf term # UVarOf m)
-> m (InferOf term # UVarOf m)
forall (f :: * -> *) s t a b.
Functor f =>
ALens s t a b -> (a -> f b) -> s -> f t
#%%~ (UVarOf m # TypeOf term)
-> (UVarOf m # TypeOf term) -> m (UVarOf m # TypeOf term)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
unify UVarOf m # TypeOf term
t
                m (InferOf term # UVarOf m)
-> ((InferOf term # UVarOf m)
    -> (TypeSig vars term # h, InferOf term # UVarOf m))
-> m (TypeSig vars term # h, InferOf term # UVarOf m)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (('AHyperType h :# term)
-> ('AHyperType h :# Scheme vars (TypeOf term))
-> TypeSig vars term # h
forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
       (h :: AHyperType).
(h :# term)
-> (h :# Scheme vars (TypeOf term)) -> TypeSig vars term h
TypeSig h ('AHyperType term)
'AHyperType h :# term
xI h ('AHyperType (Scheme vars (TypeOf term)))
'AHyperType h :# Scheme vars (TypeOf term)
sI, )
        m (TypeSig vars term # h, InferOf term # UVarOf m)
-> (m (TypeSig vars term # h, InferOf term # UVarOf m)
    -> m (TypeSig vars term # h, InferOf term # UVarOf m))
-> m (TypeSig vars term # h, InferOf term # UVarOf m)
forall a b. a -> (a -> b) -> b
& m (TypeSig vars term # h, InferOf term # UVarOf m)
-> m (TypeSig vars term # h, InferOf term # UVarOf m)
forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel