{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts, TemplateHaskell, EmptyCase #-}
module Hyper.Type.AST.Nominal
( NominalDecl(..), nParams, nScheme, W_NominalDecl(..)
, NominalInst(..), nId, nArgs
, ToNom(..), tnId, tnVal, W_ToNom(..)
, FromNom(..), _FromNom
, HasNominalInst(..)
, NomVarTypes
, MonadNominals(..)
, LoadedNominalDecl, loadNominalDecl
) where
import Control.Applicative (Alternative(..))
import Control.Lens (Prism')
import qualified Control.Lens as Lens
import Control.Monad.Trans.Writer (execWriterT)
import Generics.Constraints (Constraints)
import Hyper
import Hyper.Class.Context (HContext(..))
import Hyper.Class.Optic
import Hyper.Class.Traversable (ContainedH(..))
import Hyper.Class.ZipMatch (ZipMatch(..))
import Hyper.Infer
import Hyper.Recurse
import Hyper.Type.AST.FuncType (FuncType(..))
import Hyper.Type.AST.Map (TermMap(..), _TermMap)
import Hyper.Type.AST.Scheme
import Hyper.Unify
import Hyper.Unify.Generalize (GTerm(..), _GMono, instantiateWith, instantiateForAll)
import Hyper.Unify.New (newTerm)
import Hyper.Unify.QuantifiedVar (HasQuantifiedVar(..), OrdQVar)
import Hyper.Unify.Term (UTerm(..))
import qualified Text.PrettyPrint as P
import Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)
import Hyper.Internal.Prelude
type family NomVarTypes (t :: HyperType) :: HyperType
data NominalDecl typ h = NominalDecl
{ NominalDecl typ h -> NomVarTypes typ # QVars
_nParams :: NomVarTypes typ # QVars
, NominalDecl typ h -> Scheme (NomVarTypes typ) typ h
_nScheme :: Scheme (NomVarTypes typ) typ h
} deriving (forall x. NominalDecl typ h -> Rep (NominalDecl typ h) x)
-> (forall x. Rep (NominalDecl typ h) x -> NominalDecl typ h)
-> Generic (NominalDecl typ h)
forall x. Rep (NominalDecl typ h) x -> NominalDecl typ h
forall x. NominalDecl typ h -> Rep (NominalDecl typ h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (typ :: HyperType) (h :: AHyperType) x.
Rep (NominalDecl typ h) x -> NominalDecl typ h
forall (typ :: HyperType) (h :: AHyperType) x.
NominalDecl typ h -> Rep (NominalDecl typ h) x
$cto :: forall (typ :: HyperType) (h :: AHyperType) x.
Rep (NominalDecl typ h) x -> NominalDecl typ h
$cfrom :: forall (typ :: HyperType) (h :: AHyperType) x.
NominalDecl typ h -> Rep (NominalDecl typ h) x
Generic
data NominalInst nomId varTypes h = NominalInst
{ NominalInst nomId varTypes h -> nomId
_nId :: nomId
, NominalInst nomId varTypes h
-> varTypes # QVarInstances (GetHyperType h)
_nArgs :: varTypes # QVarInstances (GetHyperType h)
} deriving (forall x.
NominalInst nomId varTypes h
-> Rep (NominalInst nomId varTypes h) x)
-> (forall x.
Rep (NominalInst nomId varTypes h) x
-> NominalInst nomId varTypes h)
-> Generic (NominalInst nomId varTypes h)
forall x.
Rep (NominalInst nomId varTypes h) x
-> NominalInst nomId varTypes h
forall x.
NominalInst nomId varTypes h
-> Rep (NominalInst nomId varTypes h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall nomId (varTypes :: HyperType) (h :: AHyperType) x.
Rep (NominalInst nomId varTypes h) x
-> NominalInst nomId varTypes h
forall nomId (varTypes :: HyperType) (h :: AHyperType) x.
NominalInst nomId varTypes h
-> Rep (NominalInst nomId varTypes h) x
$cto :: forall nomId (varTypes :: HyperType) (h :: AHyperType) x.
Rep (NominalInst nomId varTypes h) x
-> NominalInst nomId varTypes h
$cfrom :: forall nomId (varTypes :: HyperType) (h :: AHyperType) x.
NominalInst nomId varTypes h
-> Rep (NominalInst nomId varTypes h) x
Generic
data ToNom nomId term h = ToNom
{ ToNom nomId term h -> nomId
_tnId :: nomId
, ToNom nomId term h -> h :# term
_tnVal :: h :# term
} deriving (forall x. ToNom nomId term h -> Rep (ToNom nomId term h) x)
-> (forall x. Rep (ToNom nomId term h) x -> ToNom nomId term h)
-> Generic (ToNom nomId term h)
forall x. Rep (ToNom nomId term h) x -> ToNom nomId term h
forall x. ToNom nomId term h -> Rep (ToNom nomId term h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall nomId (term :: HyperType) (h :: AHyperType) x.
Rep (ToNom nomId term h) x -> ToNom nomId term h
forall nomId (term :: HyperType) (h :: AHyperType) x.
ToNom nomId term h -> Rep (ToNom nomId term h) x
$cto :: forall nomId (term :: HyperType) (h :: AHyperType) x.
Rep (ToNom nomId term h) x -> ToNom nomId term h
$cfrom :: forall nomId (term :: HyperType) (h :: AHyperType) x.
ToNom nomId term h -> Rep (ToNom nomId term h) x
Generic
newtype FromNom nomId (term :: HyperType) (h :: AHyperType) = FromNom nomId
deriving newtype (FromNom nomId term h -> FromNom nomId term h -> Bool
(FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> Eq (FromNom nomId term h)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall nomId (term :: HyperType) (h :: AHyperType).
Eq nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
/= :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c/= :: forall nomId (term :: HyperType) (h :: AHyperType).
Eq nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
== :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c== :: forall nomId (term :: HyperType) (h :: AHyperType).
Eq nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
Eq, Eq (FromNom nomId term h)
Eq (FromNom nomId term h)
-> (FromNom nomId term h -> FromNom nomId term h -> Ordering)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h)
-> (FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h)
-> Ord (FromNom nomId term h)
FromNom nomId term h -> FromNom nomId term h -> Bool
FromNom nomId term h -> FromNom nomId term h -> Ordering
FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term 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 nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
Eq (FromNom nomId term h)
forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Ordering
forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
min :: FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
$cmin :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
max :: FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
$cmax :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
>= :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c>= :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
> :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c> :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
<= :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c<= :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
< :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c< :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
compare :: FromNom nomId term h -> FromNom nomId term h -> Ordering
$ccompare :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Ordering
$cp1Ord :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
Eq (FromNom nomId term h)
Ord, Get (FromNom nomId term h)
[FromNom nomId term h] -> Put
FromNom nomId term h -> Put
(FromNom nomId term h -> Put)
-> Get (FromNom nomId term h)
-> ([FromNom nomId term h] -> Put)
-> Binary (FromNom nomId term h)
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
Get (FromNom nomId term h)
forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
[FromNom nomId term h] -> Put
forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
FromNom nomId term h -> Put
putList :: [FromNom nomId term h] -> Put
$cputList :: forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
[FromNom nomId term h] -> Put
get :: Get (FromNom nomId term h)
$cget :: forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
Get (FromNom nomId term h)
put :: FromNom nomId term h -> Put
$cput :: forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
FromNom nomId term h -> Put
Binary, FromNom nomId term h -> ()
(FromNom nomId term h -> ()) -> NFData (FromNom nomId term h)
forall a. (a -> ()) -> NFData a
forall nomId (term :: HyperType) (h :: AHyperType).
NFData nomId =>
FromNom nomId term h -> ()
rnf :: FromNom nomId term h -> ()
$crnf :: forall nomId (term :: HyperType) (h :: AHyperType).
NFData nomId =>
FromNom nomId term h -> ()
NFData)
deriving stock (Int -> FromNom nomId term h -> ShowS
[FromNom nomId term h] -> ShowS
FromNom nomId term h -> String
(Int -> FromNom nomId term h -> ShowS)
-> (FromNom nomId term h -> String)
-> ([FromNom nomId term h] -> ShowS)
-> Show (FromNom nomId term h)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
Int -> FromNom nomId term h -> ShowS
forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
[FromNom nomId term h] -> ShowS
forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
FromNom nomId term h -> String
showList :: [FromNom nomId term h] -> ShowS
$cshowList :: forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
[FromNom nomId term h] -> ShowS
show :: FromNom nomId term h -> String
$cshow :: forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
FromNom nomId term h -> String
showsPrec :: Int -> FromNom nomId term h -> ShowS
$cshowsPrec :: forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
Int -> FromNom nomId term h -> ShowS
Show, (forall x. FromNom nomId term h -> Rep (FromNom nomId term h) x)
-> (forall x. Rep (FromNom nomId term h) x -> FromNom nomId term h)
-> Generic (FromNom nomId term h)
forall x. Rep (FromNom nomId term h) x -> FromNom nomId term h
forall x. FromNom nomId term h -> Rep (FromNom nomId term h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall nomId (term :: HyperType) (h :: AHyperType) x.
Rep (FromNom nomId term h) x -> FromNom nomId term h
forall nomId (term :: HyperType) (h :: AHyperType) x.
FromNom nomId term h -> Rep (FromNom nomId term h) x
$cto :: forall nomId (term :: HyperType) (h :: AHyperType) x.
Rep (FromNom nomId term h) x -> FromNom nomId term h
$cfrom :: forall nomId (term :: HyperType) (h :: AHyperType) x.
FromNom nomId term h -> Rep (FromNom nomId term h) x
Generic)
data LoadedNominalDecl typ v = LoadedNominalDecl
{ LoadedNominalDecl typ v
-> NomVarTypes typ # QVarInstances (GetHyperType v)
_lnParams :: NomVarTypes typ # QVarInstances (GetHyperType v)
, LoadedNominalDecl typ v
-> NomVarTypes typ # QVarInstances (GetHyperType v)
_lnForalls :: NomVarTypes typ # QVarInstances (GetHyperType v)
, LoadedNominalDecl typ v -> GTerm (GetHyperType v) # typ
_lnType :: GTerm (GetHyperType v) # typ
} deriving (forall x.
LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x)
-> (forall x.
Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v)
-> Generic (LoadedNominalDecl typ v)
forall x.
Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v
forall x.
LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (typ :: HyperType) (v :: AHyperType) x.
Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v
forall (typ :: HyperType) (v :: AHyperType) x.
LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x
$cto :: forall (typ :: HyperType) (v :: AHyperType) x.
Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v
$cfrom :: forall (typ :: HyperType) (v :: AHyperType) x.
LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x
Generic
makeLenses ''NominalDecl
makeLenses ''NominalInst
makeLenses ''ToNom
makePrisms ''FromNom
makeCommonInstances [''NominalDecl, ''NominalInst, ''ToNom, ''LoadedNominalDecl]
makeHTraversableAndBases ''NominalDecl
makeHTraversableApplyAndBases ''ToNom
makeHTraversableApplyAndBases ''FromNom
makeHMorph ''ToNom
makeZipMatch ''ToNom
makeZipMatch ''FromNom
makeHContext ''ToNom
makeHContext ''FromNom
instance HNodes v => HNodes (NominalInst n v) where
type HNodesConstraint (NominalInst n v) c = HNodesConstraint v c
type HWitnessType (NominalInst n v) = HWitnessType v
{-# INLINE hLiftConstraint #-}
hLiftConstraint :: HWitness (NominalInst n v) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness HWitnessType (NominalInst n v) n
w) = HWitness v n -> Proxy c -> (c n => r) -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint @v (HWitnessType v n -> HWitness v n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
HWitnessType (NominalInst n v) n
w)
instance HFunctor v => HFunctor (NominalInst n v) where
{-# INLINE hmap #-}
hmap :: (forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> q # n)
-> (NominalInst n v # p) -> NominalInst n v # q
hmap forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> q # n
f = (v ('AHyperType (QVarInstances p))
-> Identity (v ('AHyperType (QVarInstances q))))
-> (NominalInst n v # p) -> Identity (NominalInst n v # q)
forall nomId (varTypes :: HyperType) (h :: AHyperType)
(varTypes :: HyperType) (h :: AHyperType).
Lens
(NominalInst nomId varTypes h)
(NominalInst nomId varTypes h)
(varTypes # QVarInstances (GetHyperType h))
(varTypes # QVarInstances (GetHyperType h))
nArgs ((v ('AHyperType (QVarInstances p))
-> Identity (v ('AHyperType (QVarInstances q))))
-> (NominalInst n v # p) -> Identity (NominalInst n v # q))
-> (v ('AHyperType (QVarInstances p))
-> v ('AHyperType (QVarInstances q)))
-> (NominalInst n v # p)
-> NominalInst n v # q
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (n :: HyperType).
HWitness v n -> (QVarInstances p # n) -> QVarInstances q # n)
-> v ('AHyperType (QVarInstances p))
-> v ('AHyperType (QVarInstances q))
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (\(HWitness HWitnessType v n
w) -> (Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n)))
-> (QVarInstances p # n) -> Identity (QVarInstances q # n)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n)))
-> (QVarInstances p # n) -> Identity (QVarInstances q # n))
-> ((p ('AHyperType n) -> Identity (q # n))
-> Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n)))
-> (p ('AHyperType n) -> Identity (q # n))
-> (QVarInstances p # n)
-> Identity (QVarInstances q # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p ('AHyperType n) -> Identity (q # n))
-> Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n))
forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
Lens.mapped ((p ('AHyperType n) -> Identity (q # n))
-> (QVarInstances p # n) -> Identity (QVarInstances q # n))
-> (p ('AHyperType n) -> q # n)
-> (QVarInstances p # n)
-> QVarInstances q # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ HWitness (NominalInst n v) n -> p ('AHyperType n) -> q # n
forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> q # n
f (HWitnessType (NominalInst n v) n -> HWitness (NominalInst n v) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
HWitnessType (NominalInst n v) n
w))
instance HFoldable v => HFoldable (NominalInst n v) where
{-# INLINE hfoldMap #-}
hfoldMap :: (forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> a)
-> (NominalInst n v # p) -> a
hfoldMap forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> a
f =
(forall (n :: HyperType).
HWitness v n -> (QVarInstances p # n) -> a)
-> (v # QVarInstances p) -> a
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (\(HWitness HWitnessType v n
w) -> ((p # n) -> a) -> Map (QVar n) (p # n) -> a
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (HWitness (NominalInst n v) n -> (p # n) -> a
forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> a
f (HWitnessType (NominalInst n v) n -> HWitness (NominalInst n v) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
HWitnessType (NominalInst n v) n
w)) (Map (QVar n) (p # n) -> a)
-> ((QVarInstances p # n) -> Map (QVar n) (p # n))
-> (QVarInstances p # n)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QVarInstances p # n)
-> Getting
(Map (QVar n) (p # n)) (QVarInstances p # n) (Map (QVar n) (p # n))
-> Map (QVar n) (p # n)
forall s a. s -> Getting a s a -> a
^. Getting
(Map (QVar n) (p # n)) (QVarInstances p # n) (Map (QVar n) (p # n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances)) ((v # QVarInstances p) -> a)
-> ((NominalInst n v # p) -> v # QVarInstances p)
-> (NominalInst n v # p)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((NominalInst n v # p)
-> Getting
(v # QVarInstances p) (NominalInst n v # p) (v # QVarInstances p)
-> v # QVarInstances p
forall s a. s -> Getting a s a -> a
^. Getting
(v # QVarInstances p) (NominalInst n v # p) (v # QVarInstances p)
forall nomId (varTypes :: HyperType) (h :: AHyperType)
(varTypes :: HyperType) (h :: AHyperType).
Lens
(NominalInst nomId varTypes h)
(NominalInst nomId varTypes h)
(varTypes # QVarInstances (GetHyperType h))
(varTypes # QVarInstances (GetHyperType h))
nArgs)
instance HTraversable v => HTraversable (NominalInst n v) where
{-# INLINE hsequence #-}
hsequence :: (NominalInst n v # ContainedH f p) -> f (NominalInst n v # p)
hsequence (NominalInst n
n v # QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
v) =
(forall (n :: HyperType).
HWitness v n
-> (QVarInstances (ContainedH f p) # n) -> f (QVarInstances p # n))
-> (v # QVarInstances (ContainedH f p)) -> f (v # QVarInstances p)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse ((QVarInstances (ContainedH f p) ('AHyperType n)
-> f (QVarInstances p ('AHyperType n)))
-> HWitness v n
-> QVarInstances (ContainedH f p) ('AHyperType n)
-> f (QVarInstances p ('AHyperType n))
forall a b. a -> b -> a
const ((Map
(QVar (GetHyperType ('AHyperType n)))
(ContainedH f p ('AHyperType n))
-> f (Map
(QVar (GetHyperType ('AHyperType n))) (p ('AHyperType n))))
-> QVarInstances (ContainedH f p) ('AHyperType n)
-> f (QVarInstances p ('AHyperType n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((ContainedH f p ('AHyperType n) -> f (p ('AHyperType n)))
-> Map (QVar n) (ContainedH f p ('AHyperType n))
-> f (Map (QVar n) (p ('AHyperType n)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ContainedH f p ('AHyperType n) -> f (p ('AHyperType n))
forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH))) v # QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
v # QVarInstances (ContainedH f p)
v
f (v # QVarInstances p)
-> ((v # QVarInstances p) -> NominalInst n v # p)
-> f (NominalInst n v # p)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> n
-> (v # QVarInstances (GetHyperType ('AHyperType p)))
-> NominalInst n v # p
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst n
n
instance
( Eq nomId
, ZipMatch varTypes
, HTraversable varTypes
, HNodesConstraint varTypes ZipMatch
, HNodesConstraint varTypes OrdQVar
) =>
ZipMatch (NominalInst nomId varTypes) where
{-# INLINE zipMatch #-}
zipMatch :: (NominalInst nomId varTypes # p)
-> (NominalInst nomId varTypes # q)
-> Maybe (NominalInst nomId varTypes # (p :*: q))
zipMatch (NominalInst nomId
xId varTypes # QVarInstances (GetHyperType ('AHyperType p))
x) (NominalInst nomId
yId varTypes # QVarInstances (GetHyperType ('AHyperType q))
y)
| nomId
xId nomId -> nomId -> Bool
forall a. Eq a => a -> a -> Bool
/= nomId
yId = Maybe (NominalInst nomId varTypes # (p :*: q))
forall a. Maybe a
Nothing
| Bool
otherwise =
(varTypes # QVarInstances p)
-> (varTypes # QVarInstances q)
-> Maybe (varTypes # (QVarInstances p :*: QVarInstances q))
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
ZipMatch h =>
(h # p) -> (h # q) -> Maybe (h # (p :*: q))
zipMatch varTypes # QVarInstances p
varTypes # QVarInstances (GetHyperType ('AHyperType p))
x varTypes # QVarInstances q
varTypes # QVarInstances (GetHyperType ('AHyperType q))
y
Maybe (varTypes # (QVarInstances p :*: QVarInstances q))
-> ((varTypes # (QVarInstances p :*: QVarInstances q))
-> Maybe (varTypes # QVarInstances (p :*: q)))
-> Maybe (varTypes # QVarInstances (p :*: q))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (n :: HyperType).
HWitness varTypes n
-> ((QVarInstances p :*: QVarInstances q) # n)
-> Maybe (QVarInstances (p :*: q) # n))
-> (varTypes # (QVarInstances p :*: QVarInstances q))
-> Maybe (varTypes # QVarInstances (p :*: q))
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse
( Proxy ZipMatch
forall k (t :: k). Proxy t
Proxy @ZipMatch Proxy ZipMatch
-> (ZipMatch n =>
HWitness varTypes n
-> ((QVarInstances p :*: QVarInstances q) # n)
-> Maybe (QVarInstances (p :*: q) # n))
-> HWitness varTypes n
-> ((QVarInstances p :*: QVarInstances q) # n)
-> Maybe (QVarInstances (p :*: q) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*# Proxy OrdQVar
forall k (t :: k). Proxy t
Proxy @OrdQVar Proxy OrdQVar
-> (OrdQVar n =>
((QVarInstances p :*: QVarInstances q) # n)
-> Maybe (QVarInstances (p :*: q) # n))
-> HWitness varTypes n
-> ((QVarInstances p :*: QVarInstances q) # n)
-> Maybe (QVarInstances (p :*: q) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
\(QVarInstances Map (QVar (GetHyperType ('AHyperType n))) (p ('AHyperType n))
c0 :*: QVarInstances Map (QVar (GetHyperType ('AHyperType n))) (q ('AHyperType n))
c1) ->
(TermMap (QVar n) n # p)
-> (TermMap (QVar n) n # q)
-> Maybe (TermMap (QVar n) n # (p :*: q))
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
ZipMatch h =>
(h # p) -> (h # q) -> Maybe (h # (p :*: q))
zipMatch (Map (QVar n) ('AHyperType p :# n) -> TermMap (QVar n) n # p
forall h2 (expr2 :: HyperType) (f2 :: AHyperType).
Map h2 (f2 :# expr2) -> TermMap h2 expr2 f2
TermMap Map (QVar n) ('AHyperType p :# n)
Map (QVar (GetHyperType ('AHyperType n))) (p ('AHyperType n))
c0) (Map (QVar n) ('AHyperType q :# n) -> TermMap (QVar n) n # q
forall h2 (expr2 :: HyperType) (f2 :: AHyperType).
Map h2 (f2 :# expr2) -> TermMap h2 expr2 f2
TermMap Map (QVar n) ('AHyperType q :# n)
Map (QVar (GetHyperType ('AHyperType n))) (q ('AHyperType n))
c1)
Maybe (TermMap (QVar n) n # (p :*: q))
-> ((TermMap (QVar n) n # (p :*: q))
-> Map (QVar n) ((p :*: q) # n))
-> Maybe (Map (QVar n) ((p :*: q) # n))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ((TermMap (QVar n) n # (p :*: q))
-> Getting
(Map (QVar n) ((p :*: q) # n))
(TermMap (QVar n) n # (p :*: q))
(Map (QVar n) ((p :*: q) # n))
-> Map (QVar n) ((p :*: q) # n)
forall s a. s -> Getting a s a -> a
^. Getting
(Map (QVar n) ((p :*: q) # n))
(TermMap (QVar n) n # (p :*: q))
(Map (QVar n) ((p :*: q) # n))
forall h1 (expr1 :: HyperType) (f1 :: AHyperType) h2
(expr2 :: HyperType) (f2 :: AHyperType).
Iso
(TermMap h1 expr1 f1)
(TermMap h2 expr2 f2)
(Map h1 (f1 :# expr1))
(Map h2 (f2 :# expr2))
_TermMap)
Maybe (Map (QVar n) ((p :*: q) # n))
-> (Map (QVar n) ((p :*: q) # n) -> QVarInstances (p :*: q) # n)
-> Maybe (QVarInstances (p :*: q) # n)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Map (QVar n) ((p :*: q) # n) -> QVarInstances (p :*: q) # n
forall (h :: HyperType) (typ :: AHyperType).
Map (QVar (GetHyperType typ)) (h typ) -> QVarInstances h typ
QVarInstances
)
Maybe (varTypes # QVarInstances (p :*: q))
-> ((varTypes # QVarInstances (p :*: q))
-> NominalInst nomId varTypes # (p :*: q))
-> Maybe (NominalInst nomId varTypes # (p :*: q))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> nomId
-> (varTypes
# QVarInstances (GetHyperType ('AHyperType (p :*: q))))
-> NominalInst nomId varTypes # (p :*: q)
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
xId
instance
( HFunctor varTypes
, HContext varTypes
, HNodesConstraint varTypes OrdQVar
) => HContext (NominalInst nomId varTypes) where
hcontext :: (NominalInst nomId varTypes # p)
-> NominalInst nomId varTypes
# (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
hcontext (NominalInst nomId
n varTypes # QVarInstances (GetHyperType ('AHyperType p))
args) =
(varTypes # QVarInstances p)
-> varTypes
# (HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
:*: QVarInstances p)
forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext varTypes # QVarInstances p
varTypes # QVarInstances (GetHyperType ('AHyperType p))
args
(varTypes
# (HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
:*: QVarInstances p))
-> ((varTypes
# (HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
:*: QVarInstances p))
-> varTypes
# QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))
-> varTypes
# QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
forall a b. a -> (a -> b) -> b
& (forall (n :: HyperType).
HWitness varTypes n
-> ((HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
:*: QVarInstances p)
# n)
-> QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n)
-> (varTypes
# (HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
:*: QVarInstances p))
-> varTypes
# QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
( Proxy OrdQVar
forall k (t :: k). Proxy t
Proxy @OrdQVar Proxy OrdQVar
-> (OrdQVar n =>
((HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
:*: QVarInstances p)
# n)
-> QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n)
-> HWitness varTypes n
-> ((HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
:*: QVarInstances p)
# n)
-> QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
\(HFunc QVarInstances p ('AHyperType n)
-> Const (varTypes # QVarInstances p) ('AHyperType n)
c :*: QVarInstances p ('AHyperType n)
x) ->
QVarInstances p ('AHyperType n)
x QVarInstances p ('AHyperType n)
-> (QVarInstances p ('AHyperType n)
-> QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n)
-> QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n
forall a b. a -> (a -> b) -> b
& (Map (QVar n) (p ('AHyperType n))
-> Identity
(Map
(QVar n)
((:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity
(QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (p ('AHyperType n))
-> Identity
(Map
(QVar n)
((:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity
(QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n))
-> (Indexed
(QVar n)
(p ('AHyperType n))
(Identity
((:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n)))
-> Map (QVar n) (p ('AHyperType n))
-> Identity
(Map
(QVar n)
((:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n))))
-> Indexed
(QVar n)
(p ('AHyperType n))
(Identity
((:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n)))
-> QVarInstances p ('AHyperType n)
-> Identity
(QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Indexed
(QVar n)
(p ('AHyperType n))
(Identity
((:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n)))
-> Map (QVar n) (p ('AHyperType n))
-> Identity
(Map
(QVar n)
((:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n)))
forall i (f :: * -> *) a b.
FunctorWithIndex i f =>
IndexedSetter i (f a) (f b) a b
Lens.imapped (Indexed
(QVar n)
(p ('AHyperType n))
(Identity
((:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n)))
-> QVarInstances p ('AHyperType n)
-> Identity
(QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n))
-> (QVar n
-> p ('AHyperType n)
-> (:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n))
-> QVarInstances p ('AHyperType n)
-> QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
# n
forall i s t a b.
AnIndexedSetter i s t a b -> (i -> a -> b) -> s -> t
%@~
\QVar n
k p ('AHyperType n)
v ->
(p ('AHyperType n)
-> Const (NominalInst nomId varTypes # p) ('AHyperType n))
-> HFunc p (Const (NominalInst nomId varTypes # p)) ('AHyperType n)
forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc
( \p ('AHyperType n)
newV ->
QVarInstances p ('AHyperType n)
x
QVarInstances p ('AHyperType n)
-> (QVarInstances p ('AHyperType n)
-> QVarInstances p ('AHyperType n))
-> QVarInstances p ('AHyperType n)
forall a b. a -> (a -> b) -> b
& (Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (p ('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity (QVarInstances p ('AHyperType n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (p ('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity (QVarInstances p ('AHyperType n)))
-> ((Maybe (p ('AHyperType n))
-> Identity (Maybe (p ('AHyperType n))))
-> Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (p ('AHyperType n))))
-> (Maybe (p ('AHyperType n))
-> Identity (Maybe (p ('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity (QVarInstances p ('AHyperType n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (QVar n) (p ('AHyperType n)))
-> Lens'
(Map (QVar n) (p ('AHyperType n)))
(Maybe (IxValue (Map (QVar n) (p ('AHyperType n)))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at Index (Map (QVar n) (p ('AHyperType n)))
QVar n
k ((Maybe (p ('AHyperType n))
-> Identity (Maybe (p ('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity (QVarInstances p ('AHyperType n)))
-> p ('AHyperType n)
-> QVarInstances p ('AHyperType n)
-> QVarInstances p ('AHyperType n)
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ p ('AHyperType n)
newV
QVarInstances p ('AHyperType n)
-> (QVarInstances p ('AHyperType n)
-> Const (varTypes # QVarInstances p) ('AHyperType n))
-> Const (varTypes # QVarInstances p) ('AHyperType n)
forall a b. a -> (a -> b) -> b
& QVarInstances p ('AHyperType n)
-> Const (varTypes # QVarInstances p) ('AHyperType n)
c Const (varTypes # QVarInstances p) ('AHyperType n)
-> (Const (varTypes # QVarInstances p) ('AHyperType n)
-> varTypes # QVarInstances p)
-> varTypes # QVarInstances p
forall a b. a -> (a -> b) -> b
& Const (varTypes # QVarInstances p) ('AHyperType n)
-> varTypes # QVarInstances p
forall a k (b :: k). Const a b -> a
getConst (varTypes # QVarInstances p)
-> ((varTypes # QVarInstances p) -> NominalInst nomId varTypes # p)
-> NominalInst nomId varTypes # p
forall a b. a -> (a -> b) -> b
& nomId
-> (varTypes # QVarInstances (GetHyperType ('AHyperType p)))
-> NominalInst nomId varTypes # p
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
n
(NominalInst nomId varTypes # p)
-> ((NominalInst nomId varTypes # p)
-> Const (NominalInst nomId varTypes # p) ('AHyperType n))
-> Const (NominalInst nomId varTypes # p) ('AHyperType n)
forall a b. a -> (a -> b) -> b
& (NominalInst nomId varTypes # p)
-> Const (NominalInst nomId varTypes # p) ('AHyperType n)
forall k a (b :: k). a -> Const a b
Const
) HFunc p (Const (NominalInst nomId varTypes # p)) ('AHyperType n)
-> p ('AHyperType n)
-> (:*:)
(HFunc p (Const (NominalInst nomId varTypes # p)))
p
('AHyperType n)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p ('AHyperType n)
v
)
(varTypes
# QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))
-> ((varTypes
# QVarInstances
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))
-> NominalInst nomId varTypes
# (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))
-> NominalInst nomId varTypes
# (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
forall a b. a -> (a -> b) -> b
& nomId
-> (varTypes
# QVarInstances
(GetHyperType
('AHyperType
(HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))))
-> NominalInst nomId varTypes
# (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
n
instance Constraints (ToNom nomId term h) Pretty => Pretty (ToNom nomId term h) where
pPrintPrec :: PrettyLevel -> Rational -> ToNom nomId term h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (ToNom nomId
nomId h :# term
term) =
(nomId -> Doc
forall a. Pretty a => a -> Doc
pPrint nomId
nomId Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
"#") Doc -> Doc -> Doc
P.<+> PrettyLevel -> Rational -> (h :# term) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
11 h :# term
term
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)
class (Pretty (QVar h), Pretty (outer :# h)) => PrettyConstraints outer h
instance (Pretty (QVar h), Pretty (outer :# h)) => PrettyConstraints outer h
instance
( Pretty nomId
, HApply varTypes, HFoldable varTypes
, HNodesConstraint varTypes (PrettyConstraints h)
) =>
Pretty (NominalInst nomId varTypes h) where
pPrint :: NominalInst nomId varTypes h -> Doc
pPrint (NominalInst nomId
n varTypes # QVarInstances (GetHyperType h)
vars) =
nomId -> Doc
forall a. Pretty a => a -> Doc
pPrint nomId
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
[Doc] -> Doc
joinArgs
((forall (n :: HyperType).
HWitness varTypes n
-> (QVarInstances (GetHyperType h) # n) -> [Doc])
-> (varTypes # QVarInstances (GetHyperType h)) -> [Doc]
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (Proxy (PrettyConstraints h)
forall k (t :: k). Proxy t
Proxy @(PrettyConstraints h) Proxy (PrettyConstraints h)
-> (PrettyConstraints h n =>
(QVarInstances (GetHyperType h) # n) -> [Doc])
-> HWitness varTypes n
-> (QVarInstances (GetHyperType h) # n)
-> [Doc]
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> PrettyConstraints h n =>
(QVarInstances (GetHyperType h) # n) -> [Doc]
forall (typ :: AHyperType) (h :: HyperType).
(Pretty (QVar (GetHyperType typ)), Pretty (h typ)) =>
QVarInstances h typ -> [Doc]
mkArgs) varTypes # QVarInstances (GetHyperType h)
vars)
where
joinArgs :: [Doc] -> Doc
joinArgs [] = Doc
forall a. Monoid a => a
mempty
joinArgs [Doc]
xs = String -> Doc
P.text String
"[" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
P.sep (Doc -> [Doc] -> [Doc]
P.punctuate (String -> Doc
P.text String
",") [Doc]
xs) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
"]"
mkArgs :: QVarInstances h typ -> [Doc]
mkArgs (QVarInstances Map (QVar (GetHyperType typ)) (h typ)
m) =
Map (QVar (GetHyperType typ)) (h typ)
m Map (QVar (GetHyperType typ)) (h typ)
-> IndexedGetting
(QVar (GetHyperType typ))
(Endo [(QVar (GetHyperType typ), h typ)])
(Map (QVar (GetHyperType typ)) (h typ))
(h typ)
-> [(QVar (GetHyperType typ), h typ)]
forall s i a. s -> IndexedGetting i (Endo [(i, a)]) s a -> [(i, a)]
^@.. IndexedGetting
(QVar (GetHyperType typ))
(Endo [(QVar (GetHyperType typ), h typ)])
(Map (QVar (GetHyperType typ)) (h typ))
(h typ)
forall i (t :: * -> *) a b.
TraversableWithIndex i t =>
IndexedTraversal i (t a) (t b) a b
Lens.itraversed [(QVar (GetHyperType typ), h typ)]
-> ((QVar (GetHyperType typ), h typ) -> Doc) -> [Doc]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\(QVar (GetHyperType typ)
h, h typ
v) ->
(QVar (GetHyperType typ) -> Doc
forall a. Pretty a => a -> Doc
pPrint QVar (GetHyperType typ)
h Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
":") Doc -> Doc -> Doc
P.<+> h typ -> Doc
forall a. Pretty a => a -> Doc
pPrint h typ
v
{-# ANN module "HLint: ignore Use camelCase" #-}
data W_LoadedNominalDecl t n where
E_LoadedNominalDecl_Body :: HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_NomVarTypes :: HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n
instance (RNodes t, HNodes (NomVarTypes t)) => HNodes (LoadedNominalDecl t) where
type HNodesConstraint (LoadedNominalDecl t) c =
( HNodesConstraint (NomVarTypes t) c
, c t
, Recursive c
)
type HWitnessType (LoadedNominalDecl t) = W_LoadedNominalDecl t
{-# INLINE hLiftConstraint #-}
hLiftConstraint :: HWitness (LoadedNominalDecl t) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness (E_LoadedNominalDecl_Body w)) = HWitness (HFlip GTerm t) n -> Proxy c -> (c n => r) -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint @(HFlip GTerm _) (HWitnessType (HFlip GTerm t) n -> HWitness (HFlip GTerm t) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm t) n
HRecWitness t n
w)
hLiftConstraint (HWitness (E_LoadedNominalDecl_NomVarTypes w)) = HWitness (NomVarTypes t) n -> Proxy c -> (c n => r) -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness (NomVarTypes t) n
w
instance
(Recursively HFunctor typ, HFunctor (NomVarTypes typ)) =>
HFunctor (LoadedNominalDecl typ) where
{-# INLINE hmap #-}
hmap :: (forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n)
-> (LoadedNominalDecl typ # p) -> LoadedNominalDecl typ # q
hmap forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (LoadedNominalDecl NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mp NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf GTerm (GetHyperType ('AHyperType p)) # typ
t) =
(NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType q)))
-> (NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType q)))
-> (GTerm (GetHyperType ('AHyperType q)) # typ)
-> LoadedNominalDecl typ # q
forall (typ :: HyperType) (v :: AHyperType).
(NomVarTypes typ # QVarInstances (GetHyperType v))
-> (NomVarTypes typ # QVarInstances (GetHyperType v))
-> (GTerm (GetHyperType v) # typ)
-> LoadedNominalDecl typ v
LoadedNominalDecl ((NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap NomVarTypes typ # QVarInstances p
NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mp) ((NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap NomVarTypes typ # QVarInstances p
NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf)
(GTerm p ('AHyperType typ)
GTerm (GetHyperType ('AHyperType p)) # typ
t GTerm p ('AHyperType typ)
-> (GTerm p ('AHyperType typ) -> GTerm q # typ) -> GTerm q # typ
forall a b. a -> (a -> b) -> b
& ((HFlip GTerm typ # p) -> Identity (HFlip GTerm typ # q))
-> GTerm p ('AHyperType typ) -> Identity (GTerm q # typ)
forall (f0 :: HyperType -> HyperType) (k0 :: HyperType)
(x0 :: HyperType) (f1 :: HyperType -> HyperType) (k1 :: HyperType)
(x1 :: HyperType).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped (((HFlip GTerm typ # p) -> Identity (HFlip GTerm typ # q))
-> GTerm p ('AHyperType typ) -> Identity (GTerm q # typ))
-> ((HFlip GTerm typ # p) -> HFlip GTerm typ # q)
-> GTerm p ('AHyperType typ)
-> GTerm q # typ
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (n :: HyperType).
HWitness (HFlip GTerm typ) n -> (p # n) -> q # n)
-> (HFlip GTerm typ # p) -> HFlip GTerm typ # q
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (\(HWitness HWitnessType (HFlip GTerm typ) n
w) -> HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (HWitnessType (LoadedNominalDecl typ) n
-> HWitness (LoadedNominalDecl typ) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (HRecWitness typ n -> W_LoadedNominalDecl typ n
forall (t :: HyperType) (n :: HyperType).
HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_Body HWitnessType (HFlip GTerm typ) n
HRecWitness typ n
w))))
where
onMap :: (NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap = (forall (n :: HyperType).
HWitness (NomVarTypes typ) n
-> (QVarInstances p # n) -> QVarInstances q # n)
-> (NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (\HWitness (NomVarTypes typ) n
w -> (Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n)))
-> (QVarInstances p # n) -> Identity (QVarInstances q # n)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n)))
-> (QVarInstances p # n) -> Identity (QVarInstances q # n))
-> ((p ('AHyperType n) -> Identity (q # n))
-> Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n)))
-> (p ('AHyperType n) -> Identity (q # n))
-> (QVarInstances p # n)
-> Identity (QVarInstances q # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p ('AHyperType n) -> Identity (q # n))
-> Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n))
forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
Lens.mapped ((p ('AHyperType n) -> Identity (q # n))
-> (QVarInstances p # n) -> Identity (QVarInstances q # n))
-> (p ('AHyperType n) -> q # n)
-> (QVarInstances p # n)
-> QVarInstances q # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ HWitness (LoadedNominalDecl typ) n -> p ('AHyperType n) -> q # n
forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (HWitnessType (LoadedNominalDecl typ) n
-> HWitness (LoadedNominalDecl typ) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (HWitness (NomVarTypes typ) n -> W_LoadedNominalDecl typ n
forall (t :: HyperType) (n :: HyperType).
HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_NomVarTypes HWitness (NomVarTypes typ) n
w)))
instance
(Recursively HFoldable typ, HFoldable (NomVarTypes typ)) =>
HFoldable (LoadedNominalDecl typ) where
{-# INLINE hfoldMap #-}
hfoldMap :: (forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a)
-> (LoadedNominalDecl typ # p) -> a
hfoldMap forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (LoadedNominalDecl NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mp NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf GTerm (GetHyperType ('AHyperType p)) # typ
t) =
(NomVarTypes typ # QVarInstances p) -> a
onMap NomVarTypes typ # QVarInstances p
NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mp a -> a -> a
forall a. Semigroup a => a -> a -> a
<> (NomVarTypes typ # QVarInstances p) -> a
onMap NomVarTypes typ # QVarInstances p
NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf a -> a -> a
forall a. Semigroup a => a -> a -> a
<>
(forall (n :: HyperType).
HWitness (HFlip GTerm typ) n -> (p # n) -> a)
-> (HFlip GTerm typ # p) -> a
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (\(HWitness HWitnessType (HFlip GTerm typ) n
w) -> HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (HWitnessType (LoadedNominalDecl typ) n
-> HWitness (LoadedNominalDecl typ) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (HRecWitness typ n -> W_LoadedNominalDecl typ n
forall (t :: HyperType) (n :: HyperType).
HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_Body HWitnessType (HFlip GTerm typ) n
HRecWitness typ n
w))) (Tagged (GTerm p # typ) (Identity (GTerm p # typ))
-> Tagged (HFlip GTerm typ # p) (Identity (HFlip GTerm typ # p))
forall (f0 :: HyperType -> HyperType) (x0 :: HyperType)
(k0 :: HyperType) (f1 :: HyperType -> HyperType) (x1 :: HyperType)
(k1 :: HyperType).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip (Tagged (GTerm p # typ) (Identity (GTerm p # typ))
-> Tagged (HFlip GTerm typ # p) (Identity (HFlip GTerm typ # p)))
-> (GTerm p # typ) -> HFlip GTerm typ # p
forall t b. AReview t b -> b -> t
# GTerm p # typ
GTerm (GetHyperType ('AHyperType p)) # typ
t)
where
onMap :: (NomVarTypes typ # QVarInstances p) -> a
onMap =
(forall (n :: HyperType).
HWitness (NomVarTypes typ) n -> (QVarInstances p # n) -> a)
-> (NomVarTypes typ # QVarInstances p) -> a
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (\HWitness (NomVarTypes typ) n
w -> ((p # n) -> a) -> Map (QVar n) (p # n) -> a
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (HWitnessType (LoadedNominalDecl typ) n
-> HWitness (LoadedNominalDecl typ) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (HWitness (NomVarTypes typ) n -> W_LoadedNominalDecl typ n
forall (t :: HyperType) (n :: HyperType).
HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_NomVarTypes HWitness (NomVarTypes typ) n
w)))
(Map (QVar n) (p # n) -> a)
-> ((QVarInstances p # n) -> Map (QVar n) (p # n))
-> (QVarInstances p # n)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QVarInstances p # n)
-> Getting
(Map (QVar n) (p # n)) (QVarInstances p # n) (Map (QVar n) (p # n))
-> Map (QVar n) (p # n)
forall s a. s -> Getting a s a -> a
^. Getting
(Map (QVar n) (p # n)) (QVarInstances p # n) (Map (QVar n) (p # n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances))
instance
(RTraversable typ, HTraversable (NomVarTypes typ)) =>
HTraversable (LoadedNominalDecl typ) where
{-# INLINE hsequence #-}
hsequence :: (LoadedNominalDecl typ # ContainedH f p)
-> f (LoadedNominalDecl typ # p)
hsequence (LoadedNominalDecl NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
p NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
f GTerm (GetHyperType ('AHyperType (ContainedH f p))) # typ
t) =
NomVarTypes typ ('AHyperType (QVarInstances p))
-> NomVarTypes typ ('AHyperType (QVarInstances p))
-> GTerm p ('AHyperType typ)
-> LoadedNominalDecl typ # p
forall (typ :: HyperType) (v :: AHyperType).
(NomVarTypes typ # QVarInstances (GetHyperType v))
-> (NomVarTypes typ # QVarInstances (GetHyperType v))
-> (GTerm (GetHyperType v) # typ)
-> LoadedNominalDecl typ v
LoadedNominalDecl
(NomVarTypes typ ('AHyperType (QVarInstances p))
-> NomVarTypes typ ('AHyperType (QVarInstances p))
-> GTerm p ('AHyperType typ)
-> LoadedNominalDecl typ # p)
-> f (NomVarTypes typ ('AHyperType (QVarInstances p)))
-> f (NomVarTypes typ ('AHyperType (QVarInstances p))
-> GTerm p ('AHyperType typ) -> LoadedNominalDecl typ # p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ ('AHyperType (QVarInstances p)))
forall (h2 :: HyperType).
(NomVarTypes typ # QVarInstances (ContainedH f h2))
-> f (NomVarTypes typ # QVarInstances h2)
onMap NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
NomVarTypes typ # QVarInstances (ContainedH f p)
p
f (NomVarTypes typ ('AHyperType (QVarInstances p))
-> GTerm p ('AHyperType typ) -> LoadedNominalDecl typ # p)
-> f (NomVarTypes typ ('AHyperType (QVarInstances p)))
-> f (GTerm p ('AHyperType typ) -> LoadedNominalDecl typ # p)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ ('AHyperType (QVarInstances p)))
forall (h2 :: HyperType).
(NomVarTypes typ # QVarInstances (ContainedH f h2))
-> f (NomVarTypes typ # QVarInstances h2)
onMap NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
NomVarTypes typ # QVarInstances (ContainedH f p)
f
f (GTerm p ('AHyperType typ) -> LoadedNominalDecl typ # p)
-> f (GTerm p ('AHyperType typ)) -> f (LoadedNominalDecl typ # p)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((HFlip GTerm typ # ContainedH f p) -> f (HFlip GTerm typ # p))
-> (GTerm (ContainedH f p) # typ) -> f (GTerm p ('AHyperType typ))
forall (f0 :: HyperType -> HyperType) (k0 :: HyperType)
(x0 :: HyperType) (f1 :: HyperType -> HyperType) (k1 :: HyperType)
(x1 :: HyperType).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped (HFlip GTerm typ # ContainedH f p) -> f (HFlip GTerm typ # p)
forall (h :: HyperType) (f :: * -> *) (p :: HyperType).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence GTerm (GetHyperType ('AHyperType (ContainedH f p))) # typ
GTerm (ContainedH f p) # typ
t
where
onMap :: (NomVarTypes typ # QVarInstances (ContainedH f h2))
-> f (NomVarTypes typ # QVarInstances h2)
onMap = (forall (n :: HyperType).
HWitness (NomVarTypes typ) n
-> (QVarInstances (ContainedH f h2) # n)
-> f (QVarInstances h2 # n))
-> (NomVarTypes typ # QVarInstances (ContainedH f h2))
-> f (NomVarTypes typ # QVarInstances h2)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse ((QVarInstances (ContainedH f h2) ('AHyperType n)
-> f (QVarInstances h2 ('AHyperType n)))
-> HWitness (NomVarTypes typ) n
-> QVarInstances (ContainedH f h2) ('AHyperType n)
-> f (QVarInstances h2 ('AHyperType n))
forall a b. a -> b -> a
const (((Map (QVar n) (ContainedH f h2 ('AHyperType n))
-> f (Map (QVar n) (h2 ('AHyperType n))))
-> QVarInstances (ContainedH f h2) ('AHyperType n)
-> f (QVarInstances h2 ('AHyperType n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (ContainedH f h2 ('AHyperType n))
-> f (Map (QVar n) (h2 ('AHyperType n))))
-> QVarInstances (ContainedH f h2) ('AHyperType n)
-> f (QVarInstances h2 ('AHyperType n)))
-> ((ContainedH f h2 ('AHyperType n) -> f (h2 ('AHyperType n)))
-> Map (QVar n) (ContainedH f h2 ('AHyperType n))
-> f (Map (QVar n) (h2 ('AHyperType n))))
-> (ContainedH f h2 ('AHyperType n) -> f (h2 ('AHyperType n)))
-> QVarInstances (ContainedH f h2) ('AHyperType n)
-> f (QVarInstances h2 ('AHyperType n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ContainedH f h2 ('AHyperType n) -> f (h2 ('AHyperType n)))
-> Map (QVar n) (ContainedH f h2 ('AHyperType n))
-> f (Map (QVar n) (h2 ('AHyperType n)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) ContainedH f h2 ('AHyperType n) -> f (h2 ('AHyperType n))
forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH))
{-# INLINE loadBody #-}
loadBody ::
( UnifyGen m typ
, HNodeLens varTypes typ
, Ord (QVar typ)
) =>
varTypes # QVarInstances (UVarOf m) ->
varTypes # QVarInstances (UVarOf m) ->
typ # GTerm (UVarOf m) ->
m (GTerm (UVarOf m) # typ)
loadBody :: (varTypes # QVarInstances (UVarOf m))
-> (varTypes # QVarInstances (UVarOf m))
-> (typ # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # typ)
loadBody varTypes # QVarInstances (UVarOf m)
params varTypes # QVarInstances (UVarOf m)
foralls typ # GTerm (UVarOf m)
x =
case typ # GTerm (UVarOf m)
x (typ # GTerm (UVarOf m))
-> Getting (First (QVar typ)) (typ # GTerm (UVarOf m)) (QVar typ)
-> Maybe (QVar typ)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First (QVar typ)) (typ # GTerm (UVarOf m)) (QVar typ)
forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar Maybe (QVar typ)
-> (QVar typ -> Maybe (UVarOf m ('AHyperType typ)))
-> Maybe (UVarOf m ('AHyperType typ))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QVar typ -> Maybe (UVarOf m ('AHyperType typ))
get of
Just UVarOf m ('AHyperType typ)
r -> UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ
forall (v :: HyperType) (ast :: AHyperType). v ast -> GTerm v ast
GPoly UVarOf m ('AHyperType typ)
r (GTerm (UVarOf m) # typ)
-> ((GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ))
-> m (GTerm (UVarOf m) # typ)
forall a b. a -> (a -> b) -> b
& (GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
Maybe (UVarOf m ('AHyperType typ))
Nothing ->
case (forall (n :: HyperType).
HWitness typ n -> (GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n))
-> (typ # GTerm (UVarOf m)) -> Maybe (typ # UVarOf m)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (((GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n))
-> HWitness typ n -> (GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n)
forall a b. a -> b -> a
const ((GTerm (UVarOf m) # n)
-> Getting
(First (UVarOf m # n)) (GTerm (UVarOf m) # n) (UVarOf m # n)
-> Maybe (UVarOf m # n)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting
(First (UVarOf m # n)) (GTerm (UVarOf m) # n) (UVarOf m # n)
forall (v :: HyperType) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono)) typ # GTerm (UVarOf m)
x of
Just typ # UVarOf m
xm -> (typ # UVarOf m) -> m (UVarOf m ('AHyperType typ))
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm typ # UVarOf m
xm m (UVarOf m ('AHyperType typ))
-> (UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ)
-> m (GTerm (UVarOf m) # typ)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ
forall (v :: HyperType) (ast :: AHyperType). v ast -> GTerm v ast
GMono
Maybe (typ # UVarOf m)
Nothing -> ('AHyperType typ :# GTerm (UVarOf m)) -> GTerm (UVarOf m) # typ
forall (v :: HyperType) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody typ # GTerm (UVarOf m)
'AHyperType typ :# GTerm (UVarOf m)
x (GTerm (UVarOf m) # typ)
-> ((GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ))
-> m (GTerm (UVarOf m) # typ)
forall a b. a -> (a -> b) -> b
& (GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
where
get :: QVar typ -> Maybe (UVarOf m ('AHyperType typ))
get QVar typ
v =
varTypes # QVarInstances (UVarOf m)
params (varTypes # QVarInstances (UVarOf m))
-> Getting
(First (UVarOf m ('AHyperType typ)))
(varTypes # QVarInstances (UVarOf m))
(UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
forall s a. s -> Getting (First a) s a -> Maybe a
^? ((QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ))
-> (varTypes # QVarInstances (UVarOf m))
-> Const
(First (UVarOf m ('AHyperType typ)))
(varTypes # QVarInstances (UVarOf m))
forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ))
-> (varTypes # QVarInstances (UVarOf m))
-> Const
(First (UVarOf m ('AHyperType typ)))
(varTypes # QVarInstances (UVarOf m)))
-> ((UVarOf m ('AHyperType typ)
-> Const
(First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> (QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ))
-> Getting
(First (UVarOf m ('AHyperType typ)))
(varTypes # QVarInstances (UVarOf m))
(UVarOf m ('AHyperType typ))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (QVar typ) (UVarOf m ('AHyperType typ))
-> Const
(First (UVarOf m ('AHyperType typ)))
(Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar typ) (UVarOf m ('AHyperType typ))
-> Const
(First (UVarOf m ('AHyperType typ)))
(Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ))
-> ((UVarOf m ('AHyperType typ)
-> Const
(First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> Map (QVar typ) (UVarOf m ('AHyperType typ))
-> Const
(First (UVarOf m ('AHyperType typ)))
(Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (UVarOf m ('AHyperType typ)
-> Const
(First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> (QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
-> Traversal'
(Map (QVar typ) (UVarOf m ('AHyperType typ)))
(IxValue (Map (QVar typ) (UVarOf m ('AHyperType typ))))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
QVar typ
v Maybe (UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
varTypes # QVarInstances (UVarOf m)
foralls (varTypes # QVarInstances (UVarOf m))
-> Getting
(First (UVarOf m ('AHyperType typ)))
(varTypes # QVarInstances (UVarOf m))
(UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
forall s a. s -> Getting (First a) s a -> Maybe a
^? ((QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ))
-> (varTypes # QVarInstances (UVarOf m))
-> Const
(First (UVarOf m ('AHyperType typ)))
(varTypes # QVarInstances (UVarOf m))
forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ))
-> (varTypes # QVarInstances (UVarOf m))
-> Const
(First (UVarOf m ('AHyperType typ)))
(varTypes # QVarInstances (UVarOf m)))
-> ((UVarOf m ('AHyperType typ)
-> Const
(First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> (QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ))
-> Getting
(First (UVarOf m ('AHyperType typ)))
(varTypes # QVarInstances (UVarOf m))
(UVarOf m ('AHyperType typ))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (QVar typ) (UVarOf m ('AHyperType typ))
-> Const
(First (UVarOf m ('AHyperType typ)))
(Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar typ) (UVarOf m ('AHyperType typ))
-> Const
(First (UVarOf m ('AHyperType typ)))
(Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ))
-> ((UVarOf m ('AHyperType typ)
-> Const
(First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> Map (QVar typ) (UVarOf m ('AHyperType typ))
-> Const
(First (UVarOf m ('AHyperType typ)))
(Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (UVarOf m ('AHyperType typ)
-> Const
(First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> (QVarInstances (UVarOf m) # typ)
-> Const
(First (UVarOf m ('AHyperType typ)))
(QVarInstances (UVarOf m) # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
-> Traversal'
(Map (QVar typ) (UVarOf m ('AHyperType typ)))
(IxValue (Map (QVar typ) (UVarOf m ('AHyperType typ))))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
QVar typ
v
{-# INLINE loadNominalDecl #-}
loadNominalDecl ::
forall m typ.
( Monad m
, HTraversable (NomVarTypes typ)
, HNodesConstraint (NomVarTypes typ) (Unify m)
, HasScheme (NomVarTypes typ) m typ
) =>
Pure # NominalDecl typ ->
m (LoadedNominalDecl typ # UVarOf m)
loadNominalDecl :: (Pure # NominalDecl typ) -> m (LoadedNominalDecl typ # UVarOf m)
loadNominalDecl (Pure (NominalDecl params (Scheme foralls typ))) =
do
NomVarTypes typ # QVarInstances (UVarOf m)
paramsL <- (forall (n :: HyperType).
HWitness (NomVarTypes typ) n
-> (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> (NomVarTypes typ # QVars)
-> m (NomVarTypes typ # QVarInstances (UVarOf m))
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> HWitness (NomVarTypes typ) n
-> (QVars # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Unify m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n)
forall (m :: * -> *) (typ :: HyperType).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) NomVarTypes typ # QVars
params
NomVarTypes typ # QVarInstances (UVarOf m)
forallsL <- (forall (n :: HyperType).
HWitness (NomVarTypes typ) n
-> (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> (NomVarTypes typ # QVars)
-> m (NomVarTypes typ # QVarInstances (UVarOf m))
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> HWitness (NomVarTypes typ) n
-> (QVars # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Unify m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n)
forall (m :: * -> *) (typ :: HyperType).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) NomVarTypes typ # QVars
foralls
(forall (n :: HyperType).
HRecWitness typ n
-> (n # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # n))
-> (Pure # typ) -> m (GTerm (UVarOf m) # typ)
forall (m :: * -> *) (h :: HyperType) (w :: HyperType).
(Monad m, RTraversable h) =>
(forall (n :: HyperType). HRecWitness h n -> (n # w) -> m (w # n))
-> (Pure # h) -> m (w # h)
wrapM
(Proxy (HasScheme (NomVarTypes typ) m)
forall k (t :: k). Proxy t
Proxy @(HasScheme (NomVarTypes typ) m) Proxy (HasScheme (NomVarTypes typ) m)
-> (HasScheme (NomVarTypes typ) m n =>
(n # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # n))
-> HRecWitness typ n
-> (n # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # n)
forall (c :: HyperType -> Constraint) (h :: HyperType)
(n :: HyperType) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>>
(NomVarTypes typ # QVarInstances (UVarOf m))
-> (NomVarTypes typ # QVarInstances (UVarOf m))
-> (n # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # n)
forall (m :: * -> *) (typ :: HyperType) (varTypes :: HyperType).
(UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>
(varTypes # QVarInstances (UVarOf m))
-> (varTypes # QVarInstances (UVarOf m))
-> (typ # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # typ)
loadBody NomVarTypes typ # QVarInstances (UVarOf m)
paramsL NomVarTypes typ # QVarInstances (UVarOf m)
forallsL
) 'AHyperType Pure :# typ
Pure # typ
typ
m (GTerm (UVarOf m) # typ)
-> ((GTerm (UVarOf m) # typ) -> LoadedNominalDecl typ # UVarOf m)
-> m (LoadedNominalDecl typ # UVarOf m)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (UVarOf m))))
-> (NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (UVarOf m))))
-> (GTerm (GetHyperType ('AHyperType (UVarOf m))) # typ)
-> LoadedNominalDecl typ # UVarOf m
forall (typ :: HyperType) (v :: AHyperType).
(NomVarTypes typ # QVarInstances (GetHyperType v))
-> (NomVarTypes typ # QVarInstances (GetHyperType v))
-> (GTerm (GetHyperType v) # typ)
-> LoadedNominalDecl typ v
LoadedNominalDecl NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes typ # QVarInstances (UVarOf m)
paramsL NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes typ # QVarInstances (UVarOf m)
forallsL
class MonadNominals nomId typ m where
getNominalDecl :: nomId -> m (LoadedNominalDecl typ # UVarOf m)
class HasNominalInst nomId typ where
nominalInst :: Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)
{-# INLINE lookupParams #-}
lookupParams ::
forall m varTypes.
( Applicative m
, HTraversable varTypes
, HNodesConstraint varTypes (UnifyGen m)
) =>
varTypes # QVarInstances (UVarOf m) ->
m (varTypes # QVarInstances (UVarOf m))
lookupParams :: (varTypes # QVarInstances (UVarOf m))
-> m (varTypes # QVarInstances (UVarOf m))
lookupParams =
(forall (n :: HyperType).
HWitness varTypes n
-> (QVarInstances (UVarOf m) # n)
-> m (QVarInstances (UVarOf m) # n))
-> (varTypes # QVarInstances (UVarOf m))
-> m (varTypes # QVarInstances (UVarOf m))
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
(q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n =>
(QVarInstances (UVarOf m) # n) -> m (QVarInstances (UVarOf m) # n))
-> HWitness varTypes n
-> (QVarInstances (UVarOf m) # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> ((Map (QVar n) (UVarOf m ('AHyperType n))
-> m (Map (QVar n) (UVarOf m ('AHyperType n))))
-> (QVarInstances (UVarOf m) # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (UVarOf m ('AHyperType n))
-> m (Map (QVar n) (UVarOf m ('AHyperType n))))
-> (QVarInstances (UVarOf m) # n)
-> m (QVarInstances (UVarOf m) # n))
-> ((UVarOf m ('AHyperType n) -> m (UVarOf m ('AHyperType n)))
-> Map (QVar n) (UVarOf m ('AHyperType n))
-> m (Map (QVar n) (UVarOf m ('AHyperType n))))
-> (UVarOf m ('AHyperType n) -> m (UVarOf m ('AHyperType n)))
-> (QVarInstances (UVarOf m) # n)
-> m (QVarInstances (UVarOf m) # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UVarOf m ('AHyperType n) -> m (UVarOf m ('AHyperType n)))
-> Map (QVar n) (UVarOf m ('AHyperType n))
-> m (Map (QVar n) (UVarOf m ('AHyperType n)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) UVarOf m ('AHyperType n) -> m (UVarOf m ('AHyperType n))
forall (t :: HyperType).
UnifyGen m t =>
(UVarOf m # t) -> m (UVarOf m # t)
lookupParam)
where
lookupParam :: forall t. UnifyGen m t => UVarOf m # t -> m (UVarOf m # t)
lookupParam :: (UVarOf m # t) -> m (UVarOf m # t)
lookupParam UVarOf m # t
v =
BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> m (UTerm (UVarOf m) # t)
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v
m (UTerm (UVarOf m) # t)
-> ((UTerm (UVarOf m) # t) -> m (UVarOf m # t)) -> m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\case
UInstantiated UVarOf m # t
r -> (UVarOf m # t) -> m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
r
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l ->
Proxy t -> m (TypeConstraintsOf t)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy t
forall k (t :: k). Proxy t
Proxy @t) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> TypeConstraintsOf t)
-> m (TypeConstraintsOf t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (TypeConstraintsOf t -> TypeConstraintsOf t -> TypeConstraintsOf t
forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> m (UVarOf m # t)) -> m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BindingDict (UVarOf m) m t
-> (UTerm (UVarOf m) # t) -> m (UVarOf m # t)
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding ((UTerm (UVarOf m) # t) -> m (UVarOf m # t))
-> (TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> TypeConstraintsOf t
-> m (UVarOf m # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf t -> UTerm (UVarOf m) # t
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound
UTerm (UVarOf m) # t
_ -> String -> m (UVarOf m # t)
forall a. HasCallStack => String -> a
error String
"unexpected state at nominal's parameter"
type instance InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))
instance
( MonadScopeLevel m
, MonadNominals nomId (TypeOf expr) m
, HTraversable (NomVarTypes (TypeOf expr))
, HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m)
, UnifyGen m (TypeOf expr)
, HasInferredType expr
, Infer m expr
) =>
Infer m (ToNom nomId expr) where
{-# INLINE inferBody #-}
inferBody :: (ToNom nomId expr # InferChild m h)
-> m (ToNom nomId expr # h, InferOf (ToNom nomId expr) # UVarOf m)
inferBody (ToNom nomId
nomId 'AHyperType (InferChild m h) :# expr
val) =
do
(InferredChild h ('AHyperType expr)
valI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
valR, UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) <-
do
InferredChild (UVarOf m) h ('AHyperType expr)
v <- 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)
val
LoadedNominalDecl NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
params NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
foralls GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
gen <- nomId
-> m (LoadedNominalDecl (TypeOf expr) ('AHyperType (UVarOf m)))
forall nomId (typ :: HyperType) (m :: * -> *).
MonadNominals nomId typ m =>
nomId -> m (LoadedNominalDecl typ # UVarOf m)
getNominalDecl nomId
nomId
[m ()]
recover <-
(forall (c :: HyperType).
HWitness (NomVarTypes (TypeOf expr)) c
-> (QVarInstances (UVarOf m) # c) -> WriterT [m ()] m ())
-> (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> WriterT [m ()] m ()
forall (f :: * -> *) (h :: HyperType) (m :: HyperType).
(Applicative f, HFoldable h) =>
(forall (c :: HyperType). HWitness h c -> (m # c) -> f ())
-> (h # m) -> f ()
htraverse_
( Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m c =>
(QVarInstances (UVarOf m) # c) -> WriterT [m ()] m ())
-> HWitness (NomVarTypes (TypeOf expr)) c
-> (QVarInstances (UVarOf m) # c)
-> WriterT [m ()] m ()
forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
((UVarOf m # c) -> WriterT [m ()] m (UVarOf m # c))
-> Map (QVar c) (UVarOf m # c) -> WriterT [m ()] m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((TypeConstraintsOf c -> UTerm (UVarOf m) # c)
-> (UVarOf m # c) -> WriterT [m ()] m (UVarOf m # c)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll TypeConstraintsOf c -> UTerm (UVarOf m) # c
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem) (Map (QVar c) (UVarOf m # c) -> WriterT [m ()] m ())
-> ((QVarInstances (UVarOf m) # c) -> Map (QVar c) (UVarOf m # c))
-> (QVarInstances (UVarOf m) # c)
-> WriterT [m ()] m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QVarInstances (UVarOf m) # c)
-> Getting
(Map (QVar c) (UVarOf m # c))
(QVarInstances (UVarOf m) # c)
(Map (QVar c) (UVarOf m # c))
-> Map (QVar c) (UVarOf m # c)
forall s a. s -> Getting a s a -> a
^. Getting
(Map (QVar c) (UVarOf m # c))
(QVarInstances (UVarOf m) # c)
(Map (QVar c) (UVarOf m # c))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
(typ :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances)
) NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
foralls
WriterT [m ()] m ()
-> (WriterT [m ()] m () -> m [m ()]) -> m [m ()]
forall a b. a -> (a -> b) -> b
& WriterT [m ()] m () -> m [m ()]
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT
(UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) <- m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> (forall (n :: HyperType).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # TypeOf expr)
-> m (UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) (t :: HyperType) a.
UnifyGen m t =>
m a
-> (forall (n :: HyperType).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith ((NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) (varTypes :: HyperType).
(Applicative m, HTraversable varTypes,
HNodesConstraint varTypes (UnifyGen m)) =>
(varTypes # QVarInstances (UVarOf m))
-> m (varTypes # QVarInstances (UVarOf m))
lookupParams NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
params) forall (n :: HyperType).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
GTerm (UVarOf m) # TypeOf expr
gen
(InferredChild (UVarOf m) h ('AHyperType expr)
v, UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) (InferredChild (UVarOf m) h ('AHyperType expr),
UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m ()
-> m (InferredChild (UVarOf m) h ('AHyperType expr),
UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover
m (InferredChild (UVarOf m) h ('AHyperType expr),
UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> (m (InferredChild (UVarOf m) h ('AHyperType expr),
UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m (InferredChild (UVarOf m) h ('AHyperType expr),
UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)))
-> m (InferredChild (UVarOf m) h ('AHyperType expr),
UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall a b. a -> (a -> b) -> b
& m (InferredChild (UVarOf m) h ('AHyperType expr),
UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m (InferredChild (UVarOf m) h ('AHyperType expr),
UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel
(nomId -> ('AHyperType h :# expr) -> ToNom nomId expr # h
forall nomId (term :: HyperType) (h :: AHyperType).
nomId -> (h :# term) -> ToNom nomId term h
ToNom nomId
nomId h ('AHyperType expr)
'AHyperType h :# expr
valI, nomId
-> (NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m))))
-> NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
nomId NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT)
(ToNom nomId expr # h,
NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m)))
-> m (UVarOf m # TypeOf expr)
-> m (ToNom nomId expr # h,
NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (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 UVarOf m # TypeOf expr
typ (InferOf expr ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
valR 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))
type instance InferOf (FromNom _ e) = FuncType (TypeOf e)
instance
( Infer m expr
, HasNominalInst nomId (TypeOf expr)
, MonadNominals nomId (TypeOf expr) m
, HTraversable (NomVarTypes (TypeOf expr))
, HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m)
, UnifyGen m (TypeOf expr)
) =>
Infer m (FromNom nomId expr) where
{-# INLINE inferBody #-}
inferBody :: (FromNom nomId expr # InferChild m h)
-> m (FromNom nomId expr # h,
InferOf (FromNom nomId expr) # UVarOf m)
inferBody (FromNom nomId
nomId) =
do
LoadedNominalDecl NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
params NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
_ GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
gen <- nomId
-> m (LoadedNominalDecl (TypeOf expr) ('AHyperType (UVarOf m)))
forall nomId (typ :: HyperType) (m :: * -> *).
MonadNominals nomId typ m =>
nomId -> m (LoadedNominalDecl typ # UVarOf m)
getNominalDecl nomId
nomId
(UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) <- m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> (forall (n :: HyperType).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # TypeOf expr)
-> m (UVarOf m # TypeOf expr,
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) (t :: HyperType) a.
UnifyGen m t =>
m a
-> (forall (n :: HyperType).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith ((NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) (varTypes :: HyperType).
(Applicative m, HTraversable varTypes,
HNodesConstraint varTypes (UnifyGen m)) =>
(varTypes # QVarInstances (UVarOf m))
-> m (varTypes # QVarInstances (UVarOf m))
lookupParams NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
params) forall (n :: HyperType).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
GTerm (UVarOf m) # TypeOf expr
gen
Tagged
(NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m)))
(Identity
(NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))))
-> Tagged
(TypeOf expr # UVarOf m) (Identity (TypeOf expr # UVarOf m))
forall nomId (typ :: HyperType) (h :: HyperType).
HasNominalInst nomId typ =>
Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)
nominalInst (Tagged
(NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m)))
(Identity
(NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))))
-> Tagged
(TypeOf expr # UVarOf m) (Identity (TypeOf expr # UVarOf m)))
-> NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))
-> TypeOf expr # UVarOf m
forall t b. AReview t b -> b -> t
# nomId
-> (NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m))))
-> NominalInst
nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
nomId NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT (TypeOf expr # UVarOf m)
-> ((TypeOf expr # UVarOf m) -> m (UVarOf m # TypeOf expr))
-> m (UVarOf m # TypeOf expr)
forall a b. a -> (a -> b) -> b
& (TypeOf expr # UVarOf m) -> m (UVarOf m # TypeOf expr)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
m (UVarOf m # TypeOf expr)
-> ((UVarOf m # TypeOf expr)
-> FuncType (TypeOf expr) ('AHyperType (UVarOf m)))
-> m (FuncType (TypeOf expr) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (('AHyperType (UVarOf m) :# TypeOf expr)
-> ('AHyperType (UVarOf m) :# TypeOf expr)
-> FuncType (TypeOf expr) ('AHyperType (UVarOf m))
forall (typ :: HyperType) (h :: AHyperType).
(h :# typ) -> (h :# typ) -> FuncType typ h
`FuncType` 'AHyperType (UVarOf m) :# TypeOf expr
UVarOf m # TypeOf expr
typ)
m (FuncType (TypeOf expr) ('AHyperType (UVarOf m)))
-> (FuncType (TypeOf expr) ('AHyperType (UVarOf m))
-> (FromNom nomId expr # h,
FuncType (TypeOf expr) ('AHyperType (UVarOf m))))
-> m (FromNom nomId expr # h,
FuncType (TypeOf expr) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (nomId -> FromNom nomId expr # h
forall nomId (term :: HyperType) (h :: AHyperType).
nomId -> FromNom nomId term h
FromNom nomId
nomId, )