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

module Hyper.Type.AST.Let
    ( Let(..), letVar, letEquals, letIn, W_Let(..), MorphWitness(..)
    ) where

import           Generics.Constraints (Constraints)
import           Hyper
import           Hyper.Class.Unify (UnifyGen, UVarOf)
import           Hyper.Infer
import           Hyper.Unify.Generalize (GTerm, generalize)
import           Text.PrettyPrint (($+$), (<+>))
import qualified Text.PrettyPrint as Pretty
import           Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)

import           Hyper.Internal.Prelude

-- | A term for let-expressions with let-generalization.
--
-- @Let v expr@s express let-expressions with @v@s as variable names and @expr@s for terms.
--
-- Apart from the data type, an 'Infer' instance is also provided.
data Let v expr h = Let
    { Let v expr h -> v
_letVar :: v
    , Let v expr h -> h :# expr
_letEquals :: h :# expr
    , Let v expr h -> h :# expr
_letIn :: h :# expr
    } deriving ((forall x. Let v expr h -> Rep (Let v expr h) x)
-> (forall x. Rep (Let v expr h) x -> Let v expr h)
-> Generic (Let v expr h)
forall x. Rep (Let v expr h) x -> Let v expr h
forall x. Let v expr h -> Rep (Let 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 (Let v expr h) x -> Let v expr h
forall v (expr :: HyperType) (h :: AHyperType) x.
Let v expr h -> Rep (Let v expr h) x
$cto :: forall v (expr :: HyperType) (h :: AHyperType) x.
Rep (Let v expr h) x -> Let v expr h
$cfrom :: forall v (expr :: HyperType) (h :: AHyperType) x.
Let v expr h -> Rep (Let v expr h) x
Generic)

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

instance
    Constraints (Let v expr h) Pretty =>
    Pretty (Let v expr h) where
    pPrintPrec :: PrettyLevel -> Rational -> Let v expr h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (Let v
v h :# expr
e h :# expr
i) =
        String -> Doc
Pretty.text String
"let" Doc -> Doc -> Doc
<+> PrettyLevel -> Rational -> v -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 v
v Doc -> Doc -> Doc
<+> String -> Doc
Pretty.text String
"="
        Doc -> Doc -> Doc
<+> PrettyLevel -> Rational -> (h :# expr) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 h :# expr
e
        Doc -> Doc -> Doc
$+$ PrettyLevel -> Rational -> (h :# expr) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 h :# expr
i
        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
0)

type instance InferOf (Let _ e) = InferOf e

instance
    ( MonadScopeLevel m
    , LocalScopeType v (GTerm (UVarOf m) # TypeOf expr) m
    , UnifyGen m (TypeOf expr)
    , HasInferredType expr
    , HNodesConstraint (InferOf expr) (UnifyGen m)
    , HTraversable (InferOf expr)
    , Infer m expr
    ) =>
    Infer m (Let v expr) where

    inferBody :: (Let v expr # InferChild m h)
-> m (Let v expr # h, InferOf (Let v expr) # UVarOf m)
inferBody (Let v
v 'AHyperType (InferChild m h) :# expr
e 'AHyperType (InferChild m h) :# expr
i) =
        do
            (h ('AHyperType expr)
eI, GTerm (UVarOf m) # TypeOf expr
eG) <-
                do
                    InferredChild h ('AHyperType expr)
eI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
eR <- 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)
e
                    (UVarOf m # TypeOf expr) -> m (GTerm (UVarOf m) # TypeOf expr)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize (InferOf expr ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
eR 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
^# 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))
                        m (GTerm (UVarOf m) # TypeOf expr)
-> ((GTerm (UVarOf m) # TypeOf expr)
    -> (h ('AHyperType expr), GTerm (UVarOf m) # TypeOf expr))
-> m (h ('AHyperType expr), GTerm (UVarOf m) # TypeOf expr)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (h ('AHyperType expr)
eI ,)
                m (h ('AHyperType expr), GTerm (UVarOf m) # TypeOf expr)
-> (m (h ('AHyperType expr), GTerm (UVarOf m) # TypeOf expr)
    -> m (h ('AHyperType expr), GTerm (UVarOf m) # TypeOf expr))
-> m (h ('AHyperType expr), GTerm (UVarOf m) # TypeOf expr)
forall a b. a -> (a -> b) -> b
& m (h ('AHyperType expr), GTerm (UVarOf m) # TypeOf expr)
-> m (h ('AHyperType expr), GTerm (UVarOf m) # TypeOf expr)
forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel
            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)
i
                m (InferredChild (UVarOf m) h ('AHyperType expr))
-> (m (InferredChild (UVarOf m) h ('AHyperType expr))
    -> m (InferredChild (UVarOf m) h ('AHyperType expr)))
-> m (InferredChild (UVarOf m) h ('AHyperType expr))
forall a b. a -> (a -> b) -> b
& v
-> (GTerm (UVarOf m) # TypeOf expr)
-> m (InferredChild (UVarOf m) h ('AHyperType expr))
-> m (InferredChild (UVarOf m) h ('AHyperType expr))
forall var scheme (m :: * -> *) a.
LocalScopeType var scheme m =>
var -> scheme -> m a -> m a
localScopeType v
v GTerm (UVarOf m) # TypeOf expr
eG
                m (InferredChild (UVarOf m) h ('AHyperType expr))
-> (InferredChild (UVarOf m) h ('AHyperType expr)
    -> (Let v expr # h, InferOf expr ('AHyperType (UVarOf m))))
-> m (Let v expr # h, InferOf expr ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(InferredChild h ('AHyperType expr)
iI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
iR) -> (v
-> ('AHyperType h :# expr)
-> ('AHyperType h :# expr)
-> Let v expr # h
forall v (expr :: HyperType) (h :: AHyperType).
v -> (h :# expr) -> (h :# expr) -> Let v expr h
Let v
v h ('AHyperType expr)
'AHyperType h :# expr
eI h ('AHyperType expr)
'AHyperType h :# expr
iI, InferOf expr ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
iR)