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

module Hyper.Type.AST.App
    ( App(..), appFunc, appArg, W_App(..), MorphWitness(..)
    ) where

import Hyper
import Hyper.Class.Optic (HSubset(..), HSubset')
import Hyper.Infer
import Hyper.Type.AST.FuncType
import Hyper.Unify (UnifyGen, unify)
import Hyper.Unify.New (newTerm, newUnbound)
import Text.PrettyPrint ((<+>))
import Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)

import Hyper.Internal.Prelude

-- | A term for function applications.
--
-- @App expr@s express function applications of @expr@s.
--
-- Apart from the data type, an 'Infer' instance is also provided.
data App expr h = App
    { App expr h -> h :# expr
_appFunc :: h :# expr
    , App expr h -> h :# expr
_appArg :: h :# expr
    } deriving (forall x. App expr h -> Rep (App expr h) x)
-> (forall x. Rep (App expr h) x -> App expr h)
-> Generic (App expr h)
forall x. Rep (App expr h) x -> App expr h
forall x. App expr h -> Rep (App expr h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (expr :: HyperType) (h :: AHyperType) x.
Rep (App expr h) x -> App expr h
forall (expr :: HyperType) (h :: AHyperType) x.
App expr h -> Rep (App expr h) x
$cto :: forall (expr :: HyperType) (h :: AHyperType) x.
Rep (App expr h) x -> App expr h
$cfrom :: forall (expr :: HyperType) (h :: AHyperType) x.
App expr h -> Rep (App expr h) x
Generic

makeLenses ''App
makeZipMatch ''App
makeHContext ''App
makeHMorph ''App
makeHTraversableApplyAndBases ''App
makeCommonInstances [''App]

instance RNodes e => RNodes (App e)
instance (c (App e), Recursively c e) => Recursively c (App e)
instance RTraversable e => RTraversable (App e)

instance Pretty (h :# expr) => Pretty (App expr h) where
    pPrintPrec :: PrettyLevel -> Rational -> App expr h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (App h :# expr
f h :# expr
x) =
        PrettyLevel -> Rational -> (h :# expr) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
10 h :# expr
f Doc -> Doc -> Doc
<+>
        PrettyLevel -> Rational -> (h :# expr) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
11 h :# expr
x
        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
10)

type instance InferOf (App e) = ANode (TypeOf e)

instance
    ( Infer m expr
    , HasInferredType expr
    , HSubset' (TypeOf expr) (FuncType (TypeOf expr))
    , UnifyGen m (TypeOf expr)
    ) =>
    Infer m (App expr) where

    {-# INLINE inferBody #-}
    inferBody :: (App expr # InferChild m h)
-> m (App expr # h, InferOf (App expr) # UVarOf m)
inferBody (App 'AHyperType (InferChild m h) :# expr
func 'AHyperType (InferChild m h) :# expr
arg) =
        do
            InferredChild h ('AHyperType expr)
argI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
argR <- InferChild m h ('AHyperType expr)
-> m (InferredChild (UVarOf m) h ('AHyperType expr))
forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# expr
InferChild m h ('AHyperType expr)
arg
            InferredChild h ('AHyperType expr)
funcI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
funcR <- InferChild m h ('AHyperType expr)
-> m (InferredChild (UVarOf m) h ('AHyperType expr))
forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# expr
InferChild m h ('AHyperType expr)
func
            UVarOf m # TypeOf expr
funcRes <- m (UVarOf m # TypeOf expr)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
m (UVarOf m # t)
newUnbound
            (('AHyperType h :# expr) -> ('AHyperType h :# expr) -> App expr # h
forall (expr :: HyperType) (h :: AHyperType).
(h :# expr) -> (h :# expr) -> App expr h
App h ('AHyperType expr)
'AHyperType h :# expr
funcI h ('AHyperType expr)
'AHyperType h :# expr
argI, ('AHyperType (UVarOf m) :# TypeOf expr)
-> ANode (TypeOf expr) ('AHyperType (UVarOf m))
forall (c :: HyperType) (h :: AHyperType). (h :# c) -> ANode c h
MkANode 'AHyperType (UVarOf m) :# TypeOf expr
UVarOf m # TypeOf expr
funcRes) (App expr # h, ANode (TypeOf expr) ('AHyperType (UVarOf m)))
-> m (UVarOf m # TypeOf expr)
-> m (App expr # h, ANode (TypeOf expr) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$
                ((TypeOf expr # UVarOf m) -> m (UVarOf m # TypeOf expr)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm (Tagged
  (FuncType (TypeOf expr) # UVarOf m)
  (Identity (FuncType (TypeOf expr) # UVarOf m))
-> Tagged
     (TypeOf expr # UVarOf m) (Identity (TypeOf expr # UVarOf m))
forall (s :: HyperType) (t :: HyperType) (a :: HyperType)
       (b :: HyperType) (h :: HyperType).
HSubset s t a b =>
Prism (s # h) (t # h) (a # h) (b # h)
hSubset (Tagged
   (FuncType (TypeOf expr) # UVarOf m)
   (Identity (FuncType (TypeOf expr) # UVarOf m))
 -> Tagged
      (TypeOf expr # UVarOf m) (Identity (TypeOf expr # UVarOf m)))
-> (FuncType (TypeOf expr) # UVarOf m) -> TypeOf expr # UVarOf m
forall t b. AReview t b -> b -> t
# ('AHyperType (UVarOf m) :# TypeOf expr)
-> ('AHyperType (UVarOf m) :# TypeOf expr)
-> FuncType (TypeOf expr) # UVarOf m
forall (typ :: HyperType) (h :: AHyperType).
(h :# typ) -> (h :# typ) -> FuncType typ h
FuncType (InferOf expr ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
argR InferOf expr ('AHyperType (UVarOf m))
-> ALens
     (InferOf expr ('AHyperType (UVarOf m)))
     (InferOf expr ('AHyperType (UVarOf m)))
     (UVarOf m # TypeOf expr)
     (UVarOf m # TypeOf expr)
-> UVarOf m # TypeOf expr
forall s t a b. s -> ALens s t a b -> a
^# ALens
  (InferOf expr ('AHyperType (UVarOf m)))
  (InferOf expr ('AHyperType (UVarOf m)))
  (UVarOf m # TypeOf expr)
  (UVarOf m # TypeOf expr)
l) 'AHyperType (UVarOf m) :# TypeOf expr
UVarOf m # TypeOf expr
funcRes) m (UVarOf m # TypeOf expr)
-> ((UVarOf m # TypeOf expr) -> m (UVarOf m # TypeOf expr))
-> m (UVarOf m # TypeOf expr)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (UVarOf m # TypeOf expr)
-> (UVarOf m # TypeOf expr) -> m (UVarOf m # TypeOf expr)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
unify (InferOf expr ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
funcR InferOf expr ('AHyperType (UVarOf m))
-> ALens
     (InferOf expr ('AHyperType (UVarOf m)))
     (InferOf expr ('AHyperType (UVarOf m)))
     (UVarOf m # TypeOf expr)
     (UVarOf m # TypeOf expr)
-> UVarOf m # TypeOf expr
forall s t a b. s -> ALens s t a b -> a
^# ALens
  (InferOf expr ('AHyperType (UVarOf m)))
  (InferOf expr ('AHyperType (UVarOf m)))
  (UVarOf m # TypeOf expr)
  (UVarOf m # TypeOf expr)
l))
        where
            l :: ALens
  (InferOf expr ('AHyperType (UVarOf m)))
  (InferOf expr ('AHyperType (UVarOf m)))
  (UVarOf m # TypeOf expr)
  (UVarOf m # TypeOf expr)
l = Proxy expr
-> ALens
     (InferOf expr ('AHyperType (UVarOf m)))
     (InferOf expr ('AHyperType (UVarOf m)))
     (UVarOf m # TypeOf expr)
     (UVarOf m # TypeOf expr)
forall (t :: HyperType) (v :: HyperType).
HasInferredType t =>
Proxy t -> ALens' (InferOf t # v) (v # TypeOf t)
inferredType (Proxy expr
forall k (t :: k). Proxy t
Proxy @expr)