{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Hyper.Syntax.Let
( Let (..)
, letVar
, letEquals
, letIn
, W_Let (..)
, MorphWitness (..)
) where
import Generics.Constraints (Constraints)
import Hyper
import Hyper.Class.Unify (UVarOf, UnifyGen)
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
data Let v expr h = Let
{ forall v (expr :: HyperType) (h :: AHyperType). Let v expr h -> v
_letVar :: v
, forall v (expr :: HyperType) (h :: AHyperType).
Let v expr h -> h :# expr
_letEquals :: h :# expr
, forall v (expr :: HyperType) (h :: AHyperType).
Let v expr h -> h :# expr
_letIn :: h :# expr
}
deriving (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 GetHyperType h ('AHyperType expr)
e GetHyperType h ('AHyperType expr)
i) =
String -> Doc
Pretty.text String
"let"
Doc -> Doc -> 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
<+> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 GetHyperType h ('AHyperType expr)
e
Doc -> Doc -> Doc
$+$ forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 GetHyperType h ('AHyperType expr)
i
forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p 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 :: forall (h :: HyperType).
(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 <- forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# expr
e
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize (InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
eR forall s t a b. s -> ALens s t a b -> a
^# forall (t :: HyperType) (v :: HyperType).
HasInferredType t =>
Proxy t -> ALens' (InferOf t # v) (v # TypeOf t)
inferredType (forall {k} (t :: k). Proxy t
Proxy @expr))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (h ('AHyperType expr)
eI,)
forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel
forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# expr
i
forall a b. a -> (a -> b) -> b
& forall var scheme (m :: * -> *) a.
LocalScopeType var scheme m =>
var -> scheme -> m a -> m a
localScopeType v
v GTerm (UVarOf m) # TypeOf expr
eG
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(InferredChild h ('AHyperType expr)
iI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
iR) -> (forall v (expr :: HyperType) (h :: AHyperType).
v -> (h :# expr) -> (h :# expr) -> Let v expr h
Let v
v h ('AHyperType expr)
eI h ('AHyperType expr)
iI, InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
iR)