Safe Haskell	None
Language	Haskell2010

AST.Term.Nominal

Description

Nominal (named) types declaration, instantiation, construction, and access.

Synopsis

data NominalDecl typ k = NominalDecl {
- _nParams :: Tree (NomVarTypes typ) QVars
- _nScheme :: Scheme (NomVarTypes typ) typ k
}
nParams :: forall typ k. Lens' (NominalDecl typ k) (Tree (NomVarTypes typ) QVars)
nScheme :: forall typ k k. Lens (NominalDecl typ k) (NominalDecl typ k) (Scheme (NomVarTypes typ) typ k) (Scheme (NomVarTypes typ) typ k)
data family KWitness k :: (Knot -> Type) -> Type
data NominalInst nomId varTypes k = NominalInst {
- _nId :: nomId
- _nArgs :: Tree varTypes (QVarInstances (GetKnot k))
}
nId :: forall nomId varTypes k nomId. Lens (NominalInst nomId varTypes k) (NominalInst nomId varTypes k) nomId nomId
nArgs :: forall nomId varTypes k varTypes k. Lens (NominalInst nomId varTypes k) (NominalInst nomId varTypes k) (Tree varTypes (QVarInstances (GetKnot k))) (Tree varTypes (QVarInstances (GetKnot k)))
data ToNom nomId term k = ToNom {
- _tnId :: nomId
- _tnVal :: k # term
}
tnId :: forall nomId term k nomId. Lens (ToNom nomId term k) (ToNom nomId term k) nomId nomId
tnVal :: forall nomId term k term k. Lens (ToNom nomId term k) (ToNom nomId term k) ((#) k term) ((#) k term)
newtype FromNom nomId (term :: Knot -> *) (k :: Knot) = FromNom nomId
_FromNom :: forall nomId term k nomId term k. Iso (FromNom nomId term k) (FromNom nomId term k) nomId nomId
class HasNominalInst nomId typ where
- nominalInst :: Prism' (Tree typ k) (Tree (NominalInst nomId (NomVarTypes typ)) k)
type family NomVarTypes (t :: Knot -> Type) :: Knot -> Type
class MonadNominals nomId typ m where
- getNominalDecl :: nomId -> m (Tree (LoadedNominalDecl typ) (UVarOf m))
data LoadedNominalDecl typ v
loadNominalDecl :: forall m typ. (Monad m, KTraversable (NomVarTypes typ), KNodesConstraint (NomVarTypes typ) (Unify m), HasScheme (NomVarTypes typ) m typ) => Tree Pure (NominalDecl typ) -> m (Tree (LoadedNominalDecl typ) (UVarOf m))

Documentation

data NominalDecl typ k Source #

A declaration of a nominal type.

Constructors

NominalDecl
Fields _nParams :: Tree (NomVarTypes typ) QVars _nScheme :: Scheme (NomVarTypes typ) typ k

Instances

KNodes (NominalDecl typ) Source #
Instance details Defined in AST.Term.Nominal Associated Types type KNodesConstraint (NominalDecl typ) c :: Constraint Source # data KWitness (NominalDecl typ) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (NominalDecl typ) c => KWitness (NominalDecl typ) n -> Proxy c -> (c n -> r) -> r Source #
KFunctor (NominalDecl typ) Source #
Instance details Defined in AST.Term.Nominal Methods mapK :: (forall (n :: Knot -> Type). KWitness (NominalDecl typ) n -> Tree p n -> Tree q n) -> Tree (NominalDecl typ) p -> Tree (NominalDecl typ) q Source #
KFoldable (NominalDecl typ) Source #
Instance details Defined in AST.Term.Nominal Methods foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness (NominalDecl typ) n -> Tree p n -> a) -> Tree (NominalDecl typ) p -> a Source #
KTraversable (NominalDecl typ) Source #
Instance details Defined in AST.Term.Nominal Methods sequenceK :: Applicative f => Tree (NominalDecl typ) (ContainedK f p) -> f (Tree (NominalDecl typ) p) Source #
Constraints (NominalDecl typ k) Eq => Eq (NominalDecl typ k) Source #
Instance details Defined in AST.Term.Nominal Methods (==) :: NominalDecl typ k -> NominalDecl typ k -> Bool # (/=) :: NominalDecl typ k -> NominalDecl typ k -> Bool #
Constraints (NominalDecl typ k) Ord => Ord (NominalDecl typ k) Source #
Instance details Defined in AST.Term.Nominal Methods compare :: NominalDecl typ k -> NominalDecl typ k -> Ordering # (<) :: NominalDecl typ k -> NominalDecl typ k -> Bool # (<=) :: NominalDecl typ k -> NominalDecl typ k -> Bool # (>) :: NominalDecl typ k -> NominalDecl typ k -> Bool # (>=) :: NominalDecl typ k -> NominalDecl typ k -> Bool # max :: NominalDecl typ k -> NominalDecl typ k -> NominalDecl typ k # min :: NominalDecl typ k -> NominalDecl typ k -> NominalDecl typ k #
Constraints (NominalDecl typ k) Show => Show (NominalDecl typ k) Source #
Instance details Defined in AST.Term.Nominal Methods showsPrec :: Int -> NominalDecl typ k -> ShowS # show :: NominalDecl typ k -> String # showList :: [NominalDecl typ k] -> ShowS #
Generic (NominalDecl typ k) Source #
Instance details Defined in AST.Term.Nominal Associated Types type Rep (NominalDecl typ k) :: Type -> Type # Methods from :: NominalDecl typ k -> Rep (NominalDecl typ k) x # to :: Rep (NominalDecl typ k) x -> NominalDecl typ k #
Constraints (NominalDecl typ k) Binary => Binary (NominalDecl typ k) Source #
Instance details Defined in AST.Term.Nominal Methods put :: NominalDecl typ k -> Put # get :: Get (NominalDecl typ k) # putList :: [NominalDecl typ k] -> Put #
Constraints (NominalDecl typ k) NFData => NFData (NominalDecl typ k) Source #
Instance details Defined in AST.Term.Nominal Methods rnf :: NominalDecl typ k -> () #
data KWitness (NominalDecl typ) node Source #
Instance details Defined in AST.Term.Nominal data KWitness (NominalDecl typ) node = E_NominalDecl_Scheme_NomVarTypes_typ_typ (KWitness (Scheme (NomVarTypes typ) typ) node)
type KNodesConstraint (NominalDecl typ) constraint Source #
Instance details Defined in AST.Term.Nominal type KNodesConstraint (NominalDecl typ) constraint = constraint typ
type Rep (NominalDecl typ k) Source #
Instance details Defined in AST.Term.Nominal type Rep (NominalDecl typ k) = D1 (MetaData "NominalDecl" "AST.Term.Nominal" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" False) (C1 (MetaCons "NominalDecl" PrefixI True) (S1 (MetaSel (Just "_nParams") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Tree (NomVarTypes typ) QVars)) :*: S1 (MetaSel (Just "_nScheme") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Scheme (NomVarTypes typ) typ k))))

nParams :: forall typ k. Lens' (NominalDecl typ k) (Tree (NomVarTypes typ) QVars) Source #

nScheme :: forall typ k k. Lens (NominalDecl typ k) (NominalDecl typ k) (Scheme (NomVarTypes typ) typ k) (Scheme (NomVarTypes typ) typ k) Source #

data family KWitness k :: (Knot -> Type) -> Type Source #

KWitness k n is a witness that n is a node of k

Instances

data KWitness Pure node Source #
Instance details Defined in AST.Knot.Pure data KWitness Pure node where W_Pure_Pure :: forall (node :: Knot -> Type). KWitness Pure Pure
data KWitness Prune node Source #
Instance details Defined in AST.Knot.Prune data KWitness Prune node where W_Prune_Prune :: forall (node :: Knot -> Type). KWitness Prune Prune
data KWitness (ANode c) node Source #
Instance details Defined in AST.Combinator.ANode data KWitness (ANode c) node where W_ANode_c :: forall (c :: Knot -> Type) (node :: Knot -> Type). KWitness (ANode c) c
data KWitness (F f) node Source #
Instance details Defined in AST.Knot.Functor data KWitness (F f) node where W_F_F_f :: forall (f :: Type -> Type) (node :: Knot -> Type). KWitness (F f) (F f)
data KWitness (Ann a) node Source #
Instance details Defined in AST.Knot.Ann data KWitness (Ann a) node where W_Ann_Ann_a :: forall a (node :: Knot -> Type). KWitness (Ann a) (Ann a)
data KWitness (UnifyError t) n Source #
Instance details Defined in AST.Unify.Error data KWitness (UnifyError t) n where W_UnifyError_t :: forall (t :: Knot -> Type) (n :: Knot -> Type). KWitness (UnifyError t) t E_UnifyError_t :: forall (t :: Knot -> Type) (n :: Knot -> Type). KWitness t n -> KWitness (UnifyError t) n
data KWitness (FuncType typ) node Source #
Instance details Defined in AST.Term.FuncType data KWitness (FuncType typ) node where W_FuncType_typ :: forall (typ :: Knot -> Type) (node :: Knot -> Type). KWitness (FuncType typ) typ
data KWitness (LoadedNominalDecl t) n Source #
Instance details Defined in AST.Term.Nominal data KWitness (LoadedNominalDecl t) n = E_LoadedNominalDecl_Body (KRecWitness t n) \| E_LoadedNominalDecl_NomVarTypes (KWitness (NomVarTypes t) n)
data KWitness (NominalDecl typ) node Source #
Instance details Defined in AST.Term.Nominal data KWitness (NominalDecl typ) node = E_NominalDecl_Scheme_NomVarTypes_typ_typ (KWitness (Scheme (NomVarTypes typ) typ) node)
data KWitness (App expr) node Source #
Instance details Defined in AST.Term.App data KWitness (App expr) node where W_App_expr :: forall (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (App expr) expr
data KWitness (ScopeTypes t) node Source #
Instance details Defined in AST.Term.NamelessScope data KWitness (ScopeTypes t) node where W_ScopeTypes_t :: forall (t :: Knot -> Type) (node :: Knot -> Type). KWitness (ScopeTypes t) t
data KWitness (Const a :: Knot -> Type) i Source #
Instance details Defined in AST.Class.Nodes data KWitness (Const a :: Knot -> Type) i
data KWitness (Flip GTerm a) n Source #
Instance details Defined in AST.Unify.Generalize data KWitness (Flip GTerm a) n = E_Flip_GTerm (KRecWitness a n)
data KWitness (Flip (ITerm a) e) n Source #
Instance details Defined in AST.Infer.Term data KWitness (Flip (ITerm a) e) n where E_Flip_ITerm_InferOf_e :: forall a (e :: Knot -> Type) (n :: Knot -> Type). KWitness (InferOf e) n -> KWitness (Flip (ITerm a) e) n E_Flip_ITerm_e :: forall a (e :: Knot -> Type) (n :: Knot -> Type) (f :: Knot -> Type). KWitness e f -> KWitness (Flip (ITerm a) f) n -> KWitness (Flip (ITerm a) e) n
data KWitness (Flip (BTerm a) e) n Source #
Instance details Defined in AST.Infer.Blame data KWitness (Flip (BTerm a) e) n where E_Flip_BTerm_InferOf_e :: forall a (e :: Knot -> Type) (n :: Knot -> Type). KWitness (InferOf e) n -> KWitness (Flip (BTerm a) e) n E_Flip_BTerm_e :: forall a (e :: Knot -> Type) (n :: Knot -> Type) (f :: Knot -> Type). KWitness e f -> KWitness (Flip (BTerm a) f) n -> KWitness (Flip (BTerm a) e) n
data KWitness (Compose a b) n Source #
Instance details Defined in AST.Combinator.Compose data KWitness (Compose a b) n where KWitness_Compose :: forall (a :: Knot -> Type) (b :: Knot -> Type) (n :: Knot -> Type) (a0 :: Knot -> Type) (b0 :: Knot -> Type). KWitness a a0 -> KWitness b b0 -> KWitness (Compose a b) (Compose a0 b0)
data KWitness (TermMap k expr) node Source #
Instance details Defined in AST.Term.Map data KWitness (TermMap k expr) node where W_TermMap_expr :: forall k (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (TermMap k expr) expr
data KWitness (Var v expr) node Source #
Instance details Defined in AST.Term.Var data KWitness (Var v expr) node
data KWitness (Scheme varTypes typ) node Source #
Instance details Defined in AST.Term.Scheme data KWitness (Scheme varTypes typ) node where W_Scheme_typ :: forall (varTypes :: Knot -> Type) (typ :: Knot -> Type) (node :: Knot -> Type). KWitness (Scheme varTypes typ) typ
data KWitness (TypeSig vars term) node Source #
Instance details Defined in AST.Term.TypeSig data KWitness (TypeSig vars term) node where W_TypeSig_term :: forall (vars :: Knot -> Type) (term :: Knot -> Type) (node :: Knot -> Type). KWitness (TypeSig vars term) term W_TypeSig_Scheme_vars_TypeOf_term :: forall (vars :: Knot -> Type) (term :: Knot -> Type) (node :: Knot -> Type). KWitness (TypeSig vars term) (Scheme vars (TypeOf term))
data KWitness (FromNom nomId term) node Source #
Instance details Defined in AST.Term.Nominal data KWitness (FromNom nomId term) node
data KWitness (ToNom nomId term) node Source #
Instance details Defined in AST.Term.Nominal data KWitness (ToNom nomId term) node where W_ToNom_term :: forall nomId (term :: Knot -> Type) (node :: Knot -> Type). KWitness (ToNom nomId term) term
data KWitness (NominalInst n v) c Source #
Instance details Defined in AST.Term.Nominal data KWitness (NominalInst n v) c = E_NominalInst_k (KWitness v c)
data KWitness (Let v expr) node Source #
Instance details Defined in AST.Term.Let data KWitness (Let v expr) node where W_Let_expr :: forall v (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (Let v expr) expr
data KWitness (Lam v expr) node Source #
Instance details Defined in AST.Term.Lam data KWitness (Lam v expr) node where W_Lam_expr :: forall v (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (Lam v expr) expr
data KWitness (Scope expr a) node Source #
Instance details Defined in AST.Term.NamelessScope data KWitness (Scope expr a) node where W_Scope_expr_Maybe_a :: forall (expr :: Type -> Knot -> Type) a (node :: Knot -> Type). KWitness (Scope expr a) (expr (Maybe a))
data KWitness (ScopeVar expr a) node Source #
Instance details Defined in AST.Term.NamelessScope data KWitness (ScopeVar expr a) node
data KWitness (Product a b) n Source #
Instance details Defined in AST.Class.Nodes data KWitness (Product a b) n = E_Product_a (KWitness a n) \| E_Product_b (KWitness b n)
data KWitness (Sum a b) n Source #
Instance details Defined in AST.Class.Nodes data KWitness (Sum a b) n = E_Sum_a (KWitness a n) \| E_Sum_b (KWitness b n)
data KWitness (FlatRowExtends key val rest) node Source #
Instance details Defined in AST.Term.Row data KWitness (FlatRowExtends key val rest) node where W_FlatRowExtends_val :: forall key (val :: Knot -> Type) (rest :: Knot -> Type) (node :: Knot -> Type). KWitness (FlatRowExtends key val rest) val W_FlatRowExtends_rest :: forall key (val :: Knot -> Type) (rest :: Knot -> Type) (node :: Knot -> Type). KWitness (FlatRowExtends key val rest) rest
data KWitness (RowExtend key val rest) node Source #
Instance details Defined in AST.Term.Row data KWitness (RowExtend key val rest) node where W_RowExtend_val :: forall key (val :: Knot -> Type) (rest :: Knot -> Type) (node :: Knot -> Type). KWitness (RowExtend key val rest) val W_RowExtend_rest :: forall key (val :: Knot -> Type) (rest :: Knot -> Type) (node :: Knot -> Type). KWitness (RowExtend key val rest) rest
data KWitness (TypedLam var typ expr) node Source #
Instance details Defined in AST.Term.TypedLam data KWitness (TypedLam var typ expr) node where W_TypedLam_typ :: forall var (typ :: Knot -> Type) (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (TypedLam var typ expr) typ W_TypedLam_expr :: forall var (typ :: Knot -> Type) (expr :: Knot -> Type) (node :: Knot -> Type). KWitness (TypedLam var typ expr) expr

data NominalInst nomId varTypes k Source #

An instantiation of a nominal type

Constructors

NominalInst
Fields _nId :: nomId _nArgs :: Tree varTypes (QVarInstances (GetKnot k))

Instances

KNodes v => KNodes (NominalInst n v) Source #
Instance details Defined in AST.Term.Nominal Associated Types type KNodesConstraint (NominalInst n v) c :: Constraint Source # data KWitness (NominalInst n v) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (NominalInst n v) c => KWitness (NominalInst n v) n0 -> Proxy c -> (c n0 -> r) -> r Source #
KFunctor v => KFunctor (NominalInst n v) Source #
Instance details Defined in AST.Term.Nominal Methods mapK :: (forall (n0 :: Knot -> Type). KWitness (NominalInst n v) n0 -> Tree p n0 -> Tree q n0) -> Tree (NominalInst n v) p -> Tree (NominalInst n v) q Source #
KFoldable v => KFoldable (NominalInst n v) Source #
Instance details Defined in AST.Term.Nominal Methods foldMapK :: Monoid a => (forall (n0 :: Knot -> Type). KWitness (NominalInst n v) n0 -> Tree p n0 -> a) -> Tree (NominalInst n v) p -> a Source #
KTraversable v => KTraversable (NominalInst n v) Source #
Instance details Defined in AST.Term.Nominal Methods sequenceK :: Applicative f => Tree (NominalInst n v) (ContainedK f p) -> f (Tree (NominalInst n v) p) Source #
(Eq nomId, ZipMatch varTypes, KTraversable varTypes, KNodesConstraint varTypes ZipMatch, KNodesConstraint varTypes OrdQVar) => ZipMatch (NominalInst nomId varTypes) Source #
Instance details Defined in AST.Term.Nominal Methods zipMatch :: Tree (NominalInst nomId varTypes) p -> Tree (NominalInst nomId varTypes) q -> Maybe (Tree (NominalInst nomId varTypes) (Product p q)) Source #
Constraints (NominalInst nomId varTypes k) Eq => Eq (NominalInst nomId varTypes k) Source #
Instance details Defined in AST.Term.Nominal Methods (==) :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> Bool # (/=) :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> Bool #
Constraints (NominalInst nomId varTypes k) Ord => Ord (NominalInst nomId varTypes k) Source #
Instance details Defined in AST.Term.Nominal Methods compare :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> Ordering # (<) :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> Bool # (<=) :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> Bool # (>) :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> Bool # (>=) :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> Bool # max :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> NominalInst nomId varTypes k # min :: NominalInst nomId varTypes k -> NominalInst nomId varTypes k -> NominalInst nomId varTypes k #
Constraints (NominalInst nomId varTypes k) Show => Show (NominalInst nomId varTypes k) Source #
Instance details Defined in AST.Term.Nominal Methods showsPrec :: Int -> NominalInst nomId varTypes k -> ShowS # show :: NominalInst nomId varTypes k -> String # showList :: [NominalInst nomId varTypes k] -> ShowS #
Generic (NominalInst nomId varTypes k) Source #
Instance details Defined in AST.Term.Nominal Associated Types type Rep (NominalInst nomId varTypes k) :: Type -> Type # Methods from :: NominalInst nomId varTypes k -> Rep (NominalInst nomId varTypes k) x # to :: Rep (NominalInst nomId varTypes k) x -> NominalInst nomId varTypes k #
Constraints (NominalInst nomId varTypes k) Binary => Binary (NominalInst nomId varTypes k) Source #
Instance details Defined in AST.Term.Nominal Methods put :: NominalInst nomId varTypes k -> Put # get :: Get (NominalInst nomId varTypes k) # putList :: [NominalInst nomId varTypes k] -> Put #
Constraints (NominalInst nomId varTypes k) NFData => NFData (NominalInst nomId varTypes k) Source #
Instance details Defined in AST.Term.Nominal Methods rnf :: NominalInst nomId varTypes k -> () #
(Pretty nomId, KApply varTypes, KFoldable varTypes, KNodesConstraint varTypes (PrettyConstraints k)) => Pretty (NominalInst nomId varTypes k) Source #
Instance details Defined in AST.Term.Nominal Methods pPrintPrec :: PrettyLevel -> Rational -> NominalInst nomId varTypes k -> Doc # pPrint :: NominalInst nomId varTypes k -> Doc # pPrintList :: PrettyLevel -> [NominalInst nomId varTypes k] -> Doc #
data KWitness (NominalInst n v) c Source #
Instance details Defined in AST.Term.Nominal data KWitness (NominalInst n v) c = E_NominalInst_k (KWitness v c)
type KNodesConstraint (NominalInst n v) c Source #
Instance details Defined in AST.Term.Nominal type KNodesConstraint (NominalInst n v) c = KNodesConstraint v c
type Rep (NominalInst nomId varTypes k) Source #
Instance details Defined in AST.Term.Nominal type Rep (NominalInst nomId varTypes k) = D1 (MetaData "NominalInst" "AST.Term.Nominal" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" False) (C1 (MetaCons "NominalInst" PrefixI True) (S1 (MetaSel (Just "_nId") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 nomId) :*: S1 (MetaSel (Just "_nArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Tree varTypes (QVarInstances (GetKnot k))))))

nId :: forall nomId varTypes k nomId. Lens (NominalInst nomId varTypes k) (NominalInst nomId varTypes k) nomId nomId Source #

nArgs :: forall nomId varTypes k varTypes k. Lens (NominalInst nomId varTypes k) (NominalInst nomId varTypes k) (Tree varTypes (QVarInstances (GetKnot k))) (Tree varTypes (QVarInstances (GetKnot k))) Source #

data ToNom nomId term k Source #

Nominal data constructor.

Wrap content with a data constructor (analogues to a data constructor of a Haskell `newtype`'s).

Introduces the nominal's foralled type variables into the value's scope.

Constructors

ToNom
Fields _tnId :: nomId _tnVal :: k # term

Instances

(MonadScopeLevel m, MonadNominals nomId (TypeOf expr) m, KTraversable (NomVarTypes (TypeOf expr)), KNodesConstraint (NomVarTypes (TypeOf expr)) (Unify m), Unify m (TypeOf expr), HasInferredType expr, Infer m expr) => Infer m (ToNom nomId expr) Source #
Instance details Defined in AST.Term.Nominal Methods inferBody :: Tree (ToNom nomId expr) (InferChild m k) -> m (Tree (ToNom nomId expr) k, Tree (InferOf (ToNom nomId expr)) (UVarOf m)) Source # inferContext :: Proxy m -> Proxy (ToNom nomId expr) -> Dict (KNodesConstraint (ToNom nomId expr) (Infer m), KNodesConstraint (InferOf (ToNom nomId expr)) (Unify m)) Source #
KNodes (ToNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Associated Types type KNodesConstraint (ToNom nomId term) c :: Constraint Source # data KWitness (ToNom nomId term) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (ToNom nomId term) c => KWitness (ToNom nomId term) n -> Proxy c -> (c n -> r) -> r Source #
Monoid nomId => KPointed (ToNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods pureK :: (forall (n :: Knot -> Type). KWitness (ToNom nomId term) n -> Tree p n) -> Tree (ToNom nomId term) p Source #
KFunctor (ToNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods mapK :: (forall (n :: Knot -> Type). KWitness (ToNom nomId term) n -> Tree p n -> Tree q n) -> Tree (ToNom nomId term) p -> Tree (ToNom nomId term) q Source #
Semigroup nomId => KApply (ToNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods zipK :: Tree (ToNom nomId term) p -> Tree (ToNom nomId term) q -> Tree (ToNom nomId term) (Product p q) Source #
KFoldable (ToNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness (ToNom nomId term) n -> Tree p n -> a) -> Tree (ToNom nomId term) p -> a Source #
KTraversable (ToNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods sequenceK :: Applicative f => Tree (ToNom nomId term) (ContainedK f p) -> f (Tree (ToNom nomId term) p) Source #
Constraints (ToNom nomId term k) Eq => Eq (ToNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods (==) :: ToNom nomId term k -> ToNom nomId term k -> Bool # (/=) :: ToNom nomId term k -> ToNom nomId term k -> Bool #
Constraints (ToNom nomId term k) Ord => Ord (ToNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods compare :: ToNom nomId term k -> ToNom nomId term k -> Ordering # (<) :: ToNom nomId term k -> ToNom nomId term k -> Bool # (<=) :: ToNom nomId term k -> ToNom nomId term k -> Bool # (>) :: ToNom nomId term k -> ToNom nomId term k -> Bool # (>=) :: ToNom nomId term k -> ToNom nomId term k -> Bool # max :: ToNom nomId term k -> ToNom nomId term k -> ToNom nomId term k # min :: ToNom nomId term k -> ToNom nomId term k -> ToNom nomId term k #
Constraints (ToNom nomId term k) Show => Show (ToNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods showsPrec :: Int -> ToNom nomId term k -> ShowS # show :: ToNom nomId term k -> String # showList :: [ToNom nomId term k] -> ShowS #
Generic (ToNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Associated Types type Rep (ToNom nomId term k) :: Type -> Type # Methods from :: ToNom nomId term k -> Rep (ToNom nomId term k) x # to :: Rep (ToNom nomId term k) x -> ToNom nomId term k #
Constraints (ToNom nomId term k) Binary => Binary (ToNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods put :: ToNom nomId term k -> Put # get :: Get (ToNom nomId term k) # putList :: [ToNom nomId term k] -> Put #
Constraints (ToNom nomId term k) NFData => NFData (ToNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods rnf :: ToNom nomId term k -> () #
Constraints (ToNom nomId term k) Pretty => Pretty (ToNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods pPrintPrec :: PrettyLevel -> Rational -> ToNom nomId term k -> Doc # pPrint :: ToNom nomId term k -> Doc # pPrintList :: PrettyLevel -> [ToNom nomId term k] -> Doc #
data KWitness (ToNom nomId term) node Source #
Instance details Defined in AST.Term.Nominal data KWitness (ToNom nomId term) node where W_ToNom_term :: forall nomId (term :: Knot -> Type) (node :: Knot -> Type). KWitness (ToNom nomId term) term
type InferOf (ToNom n e) Source #
Instance details Defined in AST.Term.Nominal type InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))
type KNodesConstraint (ToNom nomId term) constraint Source #
Instance details Defined in AST.Term.Nominal type KNodesConstraint (ToNom nomId term) constraint = constraint term
type Rep (ToNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal type Rep (ToNom nomId term k) = D1 (MetaData "ToNom" "AST.Term.Nominal" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" False) (C1 (MetaCons "ToNom" PrefixI True) (S1 (MetaSel (Just "_tnId") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 nomId) :*: S1 (MetaSel (Just "_tnVal") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (k # term))))

tnId :: forall nomId term k nomId. Lens (ToNom nomId term k) (ToNom nomId term k) nomId nomId Source #

tnVal :: forall nomId term k term k. Lens (ToNom nomId term k) (ToNom nomId term k) ((#) k term) ((#) k term) Source #

newtype FromNom nomId (term :: Knot -> *) (k :: Knot) Source #

Access the data in a nominally typed value.

Analogues to a getter of a Haskell `newtype`.

Constructors

FromNom nomId

Instances

(Infer m expr, HasNominalInst nomId (TypeOf expr), MonadNominals nomId (TypeOf expr) m, KTraversable (NomVarTypes (TypeOf expr)), KNodesConstraint (NomVarTypes (TypeOf expr)) (Unify m), Unify m (TypeOf expr)) => Infer m (FromNom nomId expr) Source #
Instance details Defined in AST.Term.Nominal Methods inferBody :: Tree (FromNom nomId expr) (InferChild m k) -> m (Tree (FromNom nomId expr) k, Tree (InferOf (FromNom nomId expr)) (UVarOf m)) Source # inferContext :: Proxy m -> Proxy (FromNom nomId expr) -> Dict (KNodesConstraint (FromNom nomId expr) (Infer m), KNodesConstraint (InferOf (FromNom nomId expr)) (Unify m)) Source #
KNodes (FromNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Associated Types type KNodesConstraint (FromNom nomId term) c :: Constraint Source # data KWitness (FromNom nomId term) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (FromNom nomId term) c => KWitness (FromNom nomId term) n -> Proxy c -> (c n -> r) -> r Source #
Monoid nomId => KPointed (FromNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods pureK :: (forall (n :: Knot -> Type). KWitness (FromNom nomId term) n -> Tree p n) -> Tree (FromNom nomId term) p Source #
KFunctor (FromNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods mapK :: (forall (n :: Knot -> Type). KWitness (FromNom nomId term) n -> Tree p n -> Tree q n) -> Tree (FromNom nomId term) p -> Tree (FromNom nomId term) q Source #
Semigroup nomId => KApply (FromNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods zipK :: Tree (FromNom nomId term) p -> Tree (FromNom nomId term) q -> Tree (FromNom nomId term) (Product p q) Source #
KFoldable (FromNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness (FromNom nomId term) n -> Tree p n -> a) -> Tree (FromNom nomId term) p -> a Source #
KTraversable (FromNom nomId term) Source #
Instance details Defined in AST.Term.Nominal Methods sequenceK :: Applicative f => Tree (FromNom nomId term) (ContainedK f p) -> f (Tree (FromNom nomId term) p) Source #
Eq nomId => Eq (FromNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods (==) :: FromNom nomId term k -> FromNom nomId term k -> Bool # (/=) :: FromNom nomId term k -> FromNom nomId term k -> Bool #
Ord nomId => Ord (FromNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods compare :: FromNom nomId term k -> FromNom nomId term k -> Ordering # (<) :: FromNom nomId term k -> FromNom nomId term k -> Bool # (<=) :: FromNom nomId term k -> FromNom nomId term k -> Bool # (>) :: FromNom nomId term k -> FromNom nomId term k -> Bool # (>=) :: FromNom nomId term k -> FromNom nomId term k -> Bool # max :: FromNom nomId term k -> FromNom nomId term k -> FromNom nomId term k # min :: FromNom nomId term k -> FromNom nomId term k -> FromNom nomId term k #
Show nomId => Show (FromNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods showsPrec :: Int -> FromNom nomId term k -> ShowS # show :: FromNom nomId term k -> String # showList :: [FromNom nomId term k] -> ShowS #
Generic (FromNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Associated Types type Rep (FromNom nomId term k) :: Type -> Type # Methods from :: FromNom nomId term k -> Rep (FromNom nomId term k) x # to :: Rep (FromNom nomId term k) x -> FromNom nomId term k #
Binary nomId => Binary (FromNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods put :: FromNom nomId term k -> Put # get :: Get (FromNom nomId term k) # putList :: [FromNom nomId term k] -> Put #
NFData nomId => NFData (FromNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal Methods rnf :: FromNom nomId term k -> () #
data KWitness (FromNom nomId term) node Source #
Instance details Defined in AST.Term.Nominal data KWitness (FromNom nomId term) node
type InferOf (FromNom n e) Source #
Instance details Defined in AST.Term.Nominal type InferOf (FromNom n e) = FuncType (TypeOf e)
type KNodesConstraint (FromNom nomId term) constraint Source #
Instance details Defined in AST.Term.Nominal type KNodesConstraint (FromNom nomId term) constraint = ()
type Rep (FromNom nomId term k) Source #
Instance details Defined in AST.Term.Nominal type Rep (FromNom nomId term k) = D1 (MetaData "FromNom" "AST.Term.Nominal" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" True) (C1 (MetaCons "FromNom" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 nomId)))

_FromNom :: forall nomId term k nomId term k. Iso (FromNom nomId term k) (FromNom nomId term k) nomId nomId Source #

class HasNominalInst nomId typ where Source #

Methods

nominalInst :: Prism' (Tree typ k) (Tree (NominalInst nomId (NomVarTypes typ)) k) Source #

type family NomVarTypes (t :: Knot -> Type) :: Knot -> Type Source #

class MonadNominals nomId typ m where Source #

Methods

getNominalDecl :: nomId -> m (Tree (LoadedNominalDecl typ) (UVarOf m)) Source #

data LoadedNominalDecl typ v Source #

A nominal declaration loaded into scope in an inference monad.

Instances

(RNodes t, KNodes (NomVarTypes t)) => KNodes (LoadedNominalDecl t) Source #
Instance details Defined in AST.Term.Nominal Associated Types type KNodesConstraint (LoadedNominalDecl t) c :: Constraint Source # data KWitness (LoadedNominalDecl t) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (LoadedNominalDecl t) c => KWitness (LoadedNominalDecl t) n -> Proxy c -> (c n -> r) -> r Source #
(Recursively KFunctor typ, KFunctor (NomVarTypes typ)) => KFunctor (LoadedNominalDecl typ) Source #
Instance details Defined in AST.Term.Nominal Methods mapK :: (forall (n :: Knot -> Type). KWitness (LoadedNominalDecl typ) n -> Tree p n -> Tree q n) -> Tree (LoadedNominalDecl typ) p -> Tree (LoadedNominalDecl typ) q Source #
(Recursively KFoldable typ, KFoldable (NomVarTypes typ)) => KFoldable (LoadedNominalDecl typ) Source #
Instance details Defined in AST.Term.Nominal Methods foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness (LoadedNominalDecl typ) n -> Tree p n -> a) -> Tree (LoadedNominalDecl typ) p -> a Source #
(RTraversable typ, KTraversable (NomVarTypes typ)) => KTraversable (LoadedNominalDecl typ) Source #
Instance details Defined in AST.Term.Nominal Methods sequenceK :: Applicative f => Tree (LoadedNominalDecl typ) (ContainedK f p) -> f (Tree (LoadedNominalDecl typ) p) Source #
Constraints (LoadedNominalDecl typ v) Eq => Eq (LoadedNominalDecl typ v) Source #
Instance details Defined in AST.Term.Nominal Methods (==) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # (/=) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool #
Constraints (LoadedNominalDecl typ v) Ord => Ord (LoadedNominalDecl typ v) Source #
Instance details Defined in AST.Term.Nominal Methods compare :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Ordering # (<) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # (<=) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # (>) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # (>=) :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> Bool # max :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> LoadedNominalDecl typ v # min :: LoadedNominalDecl typ v -> LoadedNominalDecl typ v -> LoadedNominalDecl typ v #
Constraints (LoadedNominalDecl typ v) Show => Show (LoadedNominalDecl typ v) Source #
Instance details Defined in AST.Term.Nominal Methods showsPrec :: Int -> LoadedNominalDecl typ v -> ShowS # show :: LoadedNominalDecl typ v -> String # showList :: [LoadedNominalDecl typ v] -> ShowS #
Generic (LoadedNominalDecl typ v) Source #
Instance details Defined in AST.Term.Nominal Associated Types type Rep (LoadedNominalDecl typ v) :: Type -> Type # Methods from :: LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x # to :: Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v #
Constraints (LoadedNominalDecl typ v) Binary => Binary (LoadedNominalDecl typ v) Source #
Instance details Defined in AST.Term.Nominal Methods put :: LoadedNominalDecl typ v -> Put # get :: Get (LoadedNominalDecl typ v) # putList :: [LoadedNominalDecl typ v] -> Put #
Constraints (LoadedNominalDecl typ v) NFData => NFData (LoadedNominalDecl typ v) Source #
Instance details Defined in AST.Term.Nominal Methods rnf :: LoadedNominalDecl typ v -> () #
data KWitness (LoadedNominalDecl t) n Source #
Instance details Defined in AST.Term.Nominal data KWitness (LoadedNominalDecl t) n = E_LoadedNominalDecl_Body (KRecWitness t n) \| E_LoadedNominalDecl_NomVarTypes (KWitness (NomVarTypes t) n)
type KNodesConstraint (LoadedNominalDecl t) c Source #
Instance details Defined in AST.Term.Nominal type KNodesConstraint (LoadedNominalDecl t) c = (KNodesConstraint (NomVarTypes t) c, c t, Recursive c)
type Rep (LoadedNominalDecl typ v) Source #
Instance details Defined in AST.Term.Nominal type Rep (LoadedNominalDecl typ v) = D1 (MetaData "LoadedNominalDecl" "AST.Term.Nominal" "syntax-tree-0.1.0.1-5Y9WhklreXaDnL6Q9tTtln" False) (C1 (MetaCons "LoadedNominalDecl" PrefixI True) (S1 (MetaSel (Just "_lnParams") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Tree (NomVarTypes typ) (QVarInstances (GetKnot v)))) :: (S1 (MetaSel (Just "_lnForalls") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Tree (NomVarTypes typ) (QVarInstances (GetKnot v)))) :: S1 (MetaSel (Just "_lnType") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Tree (GTerm (GetKnot v)) typ)))))

loadNominalDecl :: forall m typ. (Monad m, KTraversable (NomVarTypes typ), KNodesConstraint (NomVarTypes typ) (Unify m), HasScheme (NomVarTypes typ) m typ) => Tree Pure (NominalDecl typ) -> m (Tree (LoadedNominalDecl typ) (UVarOf m)) Source #