{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Hyper.Syntax.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.Writer (WriterT (..), 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.Syntax.FuncType (FuncType (..))
import Hyper.Syntax.Map (TermMap (..), _TermMap)
import Hyper.Syntax.Scheme
import Hyper.Unify
import Hyper.Unify.Generalize (GTerm (..), instantiate, instantiateForAll, instantiateWith, _GMono)
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
{ forall (typ :: HyperType) (h :: AHyperType).
NominalDecl typ h -> NomVarTypes typ # QVars
_nParams :: NomVarTypes typ # QVars
, forall (typ :: HyperType) (h :: AHyperType).
NominalDecl typ h -> Scheme (NomVarTypes typ) typ h
_nScheme :: Scheme (NomVarTypes typ) typ h
}
deriving (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
{ forall nomId (varTypes :: HyperType) (h :: AHyperType).
NominalInst nomId varTypes h -> nomId
_nId :: nomId
, forall nomId (varTypes :: HyperType) (h :: AHyperType).
NominalInst nomId varTypes h
-> varTypes # QVarInstances (GetHyperType h)
_nArgs :: varTypes # QVarInstances (GetHyperType h)
}
deriving (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
{ forall nomId (term :: HyperType) (h :: AHyperType).
ToNom nomId term h -> nomId
_tnId :: nomId
, forall nomId (term :: HyperType) (h :: AHyperType).
ToNom nomId term h -> h :# term
_tnVal :: h :# term
}
deriving (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
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, 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
Ord, Get (FromNom nomId term h)
[FromNom nomId term h] -> Put
FromNom nomId term h -> Put
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 -> ()
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
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 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
{ forall (typ :: HyperType) (v :: AHyperType).
LoadedNominalDecl typ v
-> NomVarTypes typ # QVarInstances (GetHyperType v)
lnParams :: NomVarTypes typ # QVarInstances (GetHyperType v)
, forall (typ :: HyperType) (v :: AHyperType).
LoadedNominalDecl typ v
-> NomVarTypes typ # QVarInstances (GetHyperType v)
lnForalls :: NomVarTypes typ # QVarInstances (GetHyperType v)
, forall (typ :: HyperType) (v :: AHyperType).
LoadedNominalDecl typ v -> GTerm (GetHyperType v) # typ
lnType :: GTerm (GetHyperType v) # typ
}
deriving (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 :: forall (c :: HyperType -> Constraint) (n :: HyperType) r.
HNodesConstraint (NominalInst n v) c =>
HWitness (NominalInst n v) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness HWitnessType (NominalInst n v) n
w) = 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 (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (NominalInst n v) n
w)
instance HFunctor v => HFunctor (NominalInst n v) where
{-# INLINE hmap #-}
hmap :: forall (p :: HyperType) (q :: HyperType).
(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 = 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 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ 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) -> forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
Lens.mapped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> q # n
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
w))
instance HFoldable v => HFoldable (NominalInst n v) where
{-# INLINE hfoldMap #-}
hfoldMap :: forall a (p :: HyperType).
Monoid a =>
(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 (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) -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> a
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
w)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. 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 :: forall (f :: * -> *) (p :: HyperType).
Applicative f =>
(NominalInst n v # ContainedH f p) -> f (NominalInst n v # p)
hsequence (NominalInst n
n v # QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
v) =
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 (forall a b. a -> b -> a
const (forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH))) v # QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
v
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> 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 :: forall (p :: HyperType) (q :: HyperType).
(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 forall a. Eq a => a -> a -> Bool
/= nomId
yId = forall a. Maybe a
Nothing
| Bool
otherwise =
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
ZipMatch h =>
(h # p) -> (h # q) -> Maybe (h # (p :*: q))
zipMatch varTypes # QVarInstances (GetHyperType ('AHyperType p))
x varTypes # QVarInstances (GetHyperType ('AHyperType q))
y
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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
( forall {k} (t :: k). Proxy t
Proxy @ZipMatch 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
#*#
forall {k} (t :: k). Proxy t
Proxy @OrdQVar 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) ->
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
ZipMatch h =>
(h # p) -> (h # q) -> Maybe (h # (p :*: q))
zipMatch (forall h (expr :: HyperType) (f :: AHyperType).
Map h (f :# expr) -> TermMap h expr f
TermMap Map (QVar (GetHyperType ('AHyperType n))) (p ('AHyperType n))
c0) (forall h (expr :: HyperType) (f :: AHyperType).
Map h (f :# expr) -> TermMap h expr f
TermMap Map (QVar (GetHyperType ('AHyperType n))) (q ('AHyperType n))
c1)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (h :: HyperType) (typ :: AHyperType).
Map (QVar (GetHyperType typ)) (h typ) -> QVarInstances h typ
QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. 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)
)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> 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 :: forall (p :: HyperType).
(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) =
forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext varTypes # QVarInstances (GetHyperType ('AHyperType p))
args
forall a b. a -> (a -> b) -> b
& forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
( forall {k} (t :: k). Proxy t
Proxy @OrdQVar 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
forall a b. a -> (a -> b) -> b
& forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (f :: * -> *) a b.
FunctorWithIndex i f =>
IndexedSetter i (f a) (f b) a b
Lens.imapped
forall i s t a b.
AnIndexedSetter i s t a b -> (i -> a -> b) -> s -> t
%@~ \QVar n
k p ('AHyperType n)
v ->
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
forall a b. a -> (a -> b) -> b
& forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at QVar n
k forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ p ('AHyperType n)
newV
forall a b. a -> (a -> b) -> b
& QVarInstances p ('AHyperType n)
-> Const (varTypes # QVarInstances p) ('AHyperType n)
c
forall a b. a -> (a -> b) -> b
& forall {k} a (b :: k). Const a b -> a
getConst
forall a b. a -> (a -> b) -> b
& forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
n
forall a b. a -> (a -> b) -> b
& forall {k} a (b :: k). a -> Const a b
Const
)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p ('AHyperType n)
v
)
forall a b. a -> (a -> b) -> b
& 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 GetHyperType h ('AHyperType term)
term) =
(forall a. Pretty a => a -> Doc
pPrint nomId
nomId forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
"#") Doc -> Doc -> Doc
P.<+> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
11 GetHyperType h ('AHyperType term)
term
forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p 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) =
forall a. Pretty a => a -> Doc
pPrint nomId
n
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
joinArgs
(forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (forall {k} (t :: k). Proxy t
Proxy @(PrettyConstraints h) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall {h :: HyperType} {typ :: AHyperType}.
(Pretty (h typ), Pretty (QVar (GetHyperType typ))) =>
QVarInstances h typ -> [Doc]
mkArgs) varTypes # QVarInstances (GetHyperType h)
vars)
where
joinArgs :: [Doc] -> Doc
joinArgs [] = forall a. Monoid a => a
mempty
joinArgs [Doc]
xs = String -> Doc
P.text String
"[" forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
P.sep (Doc -> [Doc] -> [Doc]
P.punctuate (String -> Doc
P.text String
",") [Doc]
xs) 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 forall s i a. s -> IndexedGetting i (Endo [(i, a)]) s a -> [(i, a)]
^@.. forall i (t :: * -> *) a b.
TraversableWithIndex i t =>
IndexedTraversal i (t a) (t b) a b
Lens.itraversed
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(QVar (GetHyperType typ)
h, h typ
v) ->
(forall a. Pretty a => a -> Doc
pPrint QVar (GetHyperType typ)
h forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
":") Doc -> Doc -> Doc
P.<+> 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 :: forall (c :: HyperType -> Constraint) (n :: HyperType) r.
HNodesConstraint (LoadedNominalDecl t) c =>
HWitness (LoadedNominalDecl t) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness (E_LoadedNominalDecl_Body HRecWitness t n
w)) = 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 _) (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HRecWitness t n
w)
hLiftConstraint (HWitness (E_LoadedNominalDecl_NomVarTypes HWitness (NomVarTypes t) n
w)) = 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 (p :: HyperType) (q :: HyperType).
(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) =
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 (GetHyperType ('AHyperType p))
mp)
((NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf)
(GTerm (GetHyperType ('AHyperType p)) # typ
t forall a b. a -> (a -> b) -> b
& 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 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ 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) -> forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (forall (t :: HyperType) (n :: HyperType).
HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_Body HWitnessType (HFlip GTerm typ) n
w))))
where
onMap :: (NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap = 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 -> forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
Lens.mapped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (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 a (p :: HyperType).
Monoid a =>
(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 (GetHyperType ('AHyperType p))
mp
forall a. Semigroup a => a -> a -> a
<> (NomVarTypes typ # QVarInstances p) -> a
onMap NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf
forall a. Semigroup a => a -> a -> 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) -> forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (forall (t :: HyperType) (n :: HyperType).
HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_Body HWitnessType (HFlip GTerm typ) n
w))) (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 forall t b. AReview t b -> b -> t
# GTerm (GetHyperType ('AHyperType p)) # typ
t)
where
onMap :: (NomVarTypes typ # QVarInstances p) -> a
onMap =
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 ->
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (forall (t :: HyperType) (n :: HyperType).
HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_NomVarTypes HWitness (NomVarTypes typ) n
w)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances)
)
instance
(RTraversable typ, HTraversable (NomVarTypes typ)) =>
HTraversable (LoadedNominalDecl typ)
where
{-# INLINE hsequence #-}
hsequence :: forall (f :: * -> *) (p :: HyperType).
Applicative f =>
(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) =
forall (typ :: HyperType) (v :: AHyperType).
(NomVarTypes typ # QVarInstances (GetHyperType v))
-> (NomVarTypes typ # QVarInstances (GetHyperType v))
-> (GTerm (GetHyperType v) # typ)
-> LoadedNominalDecl typ v
LoadedNominalDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {p :: HyperType}.
(NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ # QVarInstances p)
onMap NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
p
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {p :: HyperType}.
(NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ # QVarInstances p)
onMap NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
f
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 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
t
where
onMap :: (NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ # QVarInstances p)
onMap = 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 (forall a b. a -> b -> a
const ((forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) 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 :: 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 varTypes # QVarInstances (UVarOf m)
params varTypes # QVarInstances (UVarOf m)
foralls typ # GTerm (UVarOf m)
x =
case typ # GTerm (UVarOf m)
x forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar 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 -> forall (v :: HyperType) (ast :: AHyperType). v ast -> GTerm v ast
GPoly UVarOf m ('AHyperType typ)
r forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
Maybe (UVarOf m ('AHyperType typ))
Nothing ->
case 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 (forall a b. a -> b -> a
const (forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (v :: HyperType) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono)) typ # GTerm (UVarOf m)
x of
Just typ # UVarOf m
xm -> forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm typ # UVarOf m
xm forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: HyperType) (ast :: AHyperType). v ast -> GTerm v ast
GMono
Maybe (typ # UVarOf m)
Nothing -> forall (v :: HyperType) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody typ # GTerm (UVarOf m)
x forall a b. a -> (a -> b) -> b
& 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 forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix QVar typ
v
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> varTypes # QVarInstances (UVarOf m)
foralls forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix QVar typ
v
{-# INLINE loadNominalDecl #-}
loadNominalDecl ::
forall m typ.
( HTraversable (NomVarTypes typ)
, HNodesConstraint (NomVarTypes typ) (Unify m)
, HasScheme (NomVarTypes typ) m typ
) =>
Pure # NominalDecl typ ->
m (LoadedNominalDecl typ # UVarOf m)
loadNominalDecl :: forall (m :: * -> *) (typ :: HyperType).
(HTraversable (NomVarTypes typ),
HNodesConstraint (NomVarTypes typ) (Unify m),
HasScheme (NomVarTypes typ) m typ) =>
(Pure # NominalDecl typ) -> m (LoadedNominalDecl typ # UVarOf m)
loadNominalDecl (Pure (NominalDecl NomVarTypes typ # QVars
params (Scheme NomVarTypes typ # QVars
foralls 'AHyperType Pure :# typ
typ))) =
do
NomVarTypes typ # QVarInstances (UVarOf m)
paramsL <- 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 (forall {k} (t :: k). Proxy t
Proxy @(Unify m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> 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 (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 (forall {k} (t :: k). Proxy t
Proxy @(Unify m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (m :: * -> *) (typ :: HyperType).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) NomVarTypes typ # QVars
foralls
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
( forall {k} (t :: k). Proxy t
Proxy @(HasScheme (NomVarTypes typ) m) forall (c :: HyperType -> Constraint) (h :: HyperType)
(n :: HyperType) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>>
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
typ
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> 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 (UVarOf m)
paramsL 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)
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 :: forall (h :: HyperType).
(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
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 <- forall nomId (typ :: HyperType) (m :: * -> *).
MonadNominals nomId typ m =>
nomId -> m (LoadedNominalDecl typ # UVarOf m)
getNominalDecl nomId
nomId
[m ()]
recoverForAlls <-
forall (f :: * -> *) (h :: HyperType) (m :: HyperType).
(Applicative f, HFoldable h) =>
(forall (c :: HyperType). HWitness h c -> (m # c) -> f ())
-> (h # m) -> f ()
htraverse_
( forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances)
)
NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
foralls
forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT
(NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT, [m ()]
recoverParams) <-
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
( forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
(forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) (forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound)
)
NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
params
forall a b. a -> (a -> b) -> b
& forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
UVarOf m # TypeOf expr
typ <- forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(GTerm (UVarOf m) # t) -> m (UVarOf m # t)
instantiate GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
gen forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([m ()]
recoverParams forall a. Semigroup a => a -> a -> a
<> [m ()]
recoverForAlls)
InferredChild h ('AHyperType expr)
valI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
valR <- forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# expr
val forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel
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 (GetHyperType ('AHyperType expr)) # UVarOf m
valR 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. Applicative f => a -> f a
pure (forall nomId (term :: HyperType) (h :: AHyperType).
nomId -> (h :# term) -> ToNom nomId term h
ToNom nomId
nomId h ('AHyperType expr)
valI, forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
nomId NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT)
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 :: forall (h :: HyperType).
(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) <- forall nomId (typ :: HyperType) (m :: * -> *).
MonadNominals nomId typ m =>
nomId -> m (LoadedNominalDecl typ # UVarOf m)
getNominalDecl nomId
nomId
let lookupParams :: m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
lookupParams = 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 (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
(n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
(typ2 :: AHyperType).
Iso
(QVarInstances h1 typ1)
(QVarInstances h2 typ2)
(Map (QVar (GetHyperType typ1)) (h1 typ1))
(Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(UVarOf m # t) -> m (UVarOf m # t)
lookupParam) NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
params
(UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) <- 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 m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
lookupParams forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
gen
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm (forall nomId (typ :: HyperType) (h :: HyperType).
HasNominalInst nomId typ =>
Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)
nominalInst forall t b. AReview t b -> b -> t
# forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
nomId NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall nomId (term :: HyperType) (h :: AHyperType).
nomId -> FromNom nomId term h
FromNom nomId
nomId,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (typ :: HyperType) (h :: AHyperType).
(h :# typ) -> (h :# typ) -> FuncType typ h
`FuncType` UVarOf m # TypeOf expr
typ)
lookupParam :: forall m t. UnifyGen m t => UVarOf m # t -> m (UVarOf m # t)
lookupParam :: forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(UVarOf m # t) -> m (UVarOf m # t)
lookupParam UVarOf m # t
v =
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
UInstantiated UVarOf m # t
r -> forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
r
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l ->
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @t) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf (GetHyperType ('AHyperType t))
l) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound
UTerm (UVarOf m) # t
_ -> forall a. HasCallStack => String -> a
error String
"unexpected state at nominal's parameter"