AST.Term.Nominal

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

Documentation

data NominalDecl typ k

A declaration of a nominal type.

Constructors

NominalDecl

Fields

• _nParams :: Tree (NomVarTypes typ) QVars
• _nScheme :: Scheme (NomVarTypes typ) typ k

Instances

KNodes (NominalDecl typ)

Defined in AST.Term.Nominal

Associated Types

type KNodesConstraint (NominalDecl typ) c :: Constraint

data KWitness (NominalDecl typ) a :: Type

Methods

kLiftConstraint :: KNodesConstraint (NominalDecl typ) c => KWitness (NominalDecl typ) n -> Proxy c -> (c n -> r) -> r

KFunctor (NominalDecl typ)

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

KFoldable (NominalDecl typ)

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

KTraversable (NominalDecl typ)

Defined in AST.Term.Nominal

Methods

sequenceK :: Applicative f => Tree (NominalDecl typ) (ContainedK f p) -> f (Tree (NominalDecl typ) p)

Constraints (NominalDecl typ k) Eq => Eq (NominalDecl typ k)

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)

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)

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)

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)

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)

Defined in AST.Term.Nominal

Methods

rnf :: NominalDecl typ k -> ()

data KWitness (NominalDecl typ) node

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

Defined in AST.Term.Nominal

type KNodesConstraint (NominalDecl typ) constraint = constraint typ

type Rep (NominalDecl typ k)

Defined in AST.Term.Nominal

type Rep (NominalDecl typ k) = D1 (MetaData "NominalDecl" "AST.Term.Nominal" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" 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)

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

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

Instances

data KWitness Pure node

Defined in AST.Knot.Pure

data KWitness Pure node where

• W_Pure_Pure :: forall (node :: Knot -> Type). KWitness Pure Pure

data KWitness Prune node

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

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

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

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

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

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

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

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

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

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

Defined in AST.Class.Nodes

data KWitness (Const a :: Knot -> Type) i

data KWitness (Flip GTerm a) n

Defined in AST.Unify.Generalize

data KWitness (Flip GTerm a) n = E_Flip_GTerm (KRecWitness a n)

data KWitness (Flip (ITerm a) e) n

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

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

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

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

Defined in AST.Term.Var

data KWitness (Var v expr) node

data KWitness (Scheme varTypes typ) node

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

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

Defined in AST.Term.Nominal

data KWitness (FromNom nomId term) node

data KWitness (ToNom nomId term) node

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

Defined in AST.Term.Nominal

data KWitness (NominalInst n v) c = E_NominalInst_k (KWitness v c)

data KWitness (Let v expr) node

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

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

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

Defined in AST.Term.NamelessScope

data KWitness (ScopeVar expr a) node

data KWitness (Product a b) n

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

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

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

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

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

An instantiation of a nominal type

Constructors

NominalInst

Fields

• _nId :: nomId
• _nArgs :: Tree varTypes (QVarInstances (GetKnot k))

Instances

KNodes v => KNodes (NominalInst n v)

Defined in AST.Term.Nominal

Associated Types

type KNodesConstraint (NominalInst n v) c :: Constraint

data KWitness (NominalInst n v) a :: Type

Methods

kLiftConstraint :: KNodesConstraint (NominalInst n v) c => KWitness (NominalInst n v) n0 -> Proxy c -> (c n0 -> r) -> r

KFunctor v => KFunctor (NominalInst n v)

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

KFoldable v => KFoldable (NominalInst n v)

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

KTraversable v => KTraversable (NominalInst n v)

Defined in AST.Term.Nominal

Methods

sequenceK :: Applicative f => Tree (NominalInst n v) (ContainedK f p) -> f (Tree (NominalInst n v) p)

(Eq nomId, ZipMatch varTypes, KTraversable varTypes, KNodesConstraint varTypes ZipMatch, KNodesConstraint varTypes OrdQVar) => ZipMatch (NominalInst nomId varTypes)

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))

Constraints (NominalInst nomId varTypes k) Eq => Eq (NominalInst nomId varTypes k)

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)

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)

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)

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)

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)

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)

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

Defined in AST.Term.Nominal

data KWitness (NominalInst n v) c = E_NominalInst_k (KWitness v c)

type KNodesConstraint (NominalInst n v) c

Defined in AST.Term.Nominal

type KNodesConstraint (NominalInst n v) c = KNodesConstraint v c

type Rep (NominalInst nomId varTypes k)

Defined in AST.Term.Nominal

type Rep (NominalInst nomId varTypes k) = D1 (MetaData "NominalInst" "AST.Term.Nominal" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" 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

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

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)

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))

inferContext :: Proxy m -> Proxy (ToNom nomId expr) -> Dict (KNodesConstraint (ToNom nomId expr) (Infer m), KNodesConstraint (InferOf (ToNom nomId expr)) (Unify m))

KNodes (ToNom nomId term)

Defined in AST.Term.Nominal

Associated Types

type KNodesConstraint (ToNom nomId term) c :: Constraint

data KWitness (ToNom nomId term) a :: Type

Methods

kLiftConstraint :: KNodesConstraint (ToNom nomId term) c => KWitness (ToNom nomId term) n -> Proxy c -> (c n -> r) -> r

Monoid nomId => KPointed (ToNom nomId term)

Defined in AST.Term.Nominal

Methods

pureK :: (forall (n :: Knot -> Type). KWitness (ToNom nomId term) n -> Tree p n) -> Tree (ToNom nomId term) p

KFunctor (ToNom nomId term)

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

Semigroup nomId => KApply (ToNom nomId term)

Defined in AST.Term.Nominal

Methods

zipK :: Tree (ToNom nomId term) p -> Tree (ToNom nomId term) q -> Tree (ToNom nomId term) (Product p q)

KFoldable (ToNom nomId term)

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

KTraversable (ToNom nomId term)

Defined in AST.Term.Nominal

Methods

sequenceK :: Applicative f => Tree (ToNom nomId term) (ContainedK f p) -> f (Tree (ToNom nomId term) p)

Constraints (ToNom nomId term k) Eq => Eq (ToNom nomId term k)

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)

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)

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)

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)

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)

Defined in AST.Term.Nominal

Methods

rnf :: ToNom nomId term k -> ()

Constraints (ToNom nomId term k) Pretty => Pretty (ToNom nomId term k)

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

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)

Defined in AST.Term.Nominal

type InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))

type KNodesConstraint (ToNom nomId term) constraint

Defined in AST.Term.Nominal

type KNodesConstraint (ToNom nomId term) constraint = constraint term

type Rep (ToNom nomId term k)

Defined in AST.Term.Nominal

type Rep (ToNom nomId term k) = D1 (MetaData "ToNom" "AST.Term.Nominal" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" 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

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)

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)

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))

inferContext :: Proxy m -> Proxy (FromNom nomId expr) -> Dict (KNodesConstraint (FromNom nomId expr) (Infer m), KNodesConstraint (InferOf (FromNom nomId expr)) (Unify m))

KNodes (FromNom nomId term)

Defined in AST.Term.Nominal

Associated Types

type KNodesConstraint (FromNom nomId term) c :: Constraint

data KWitness (FromNom nomId term) a :: Type

Methods

kLiftConstraint :: KNodesConstraint (FromNom nomId term) c => KWitness (FromNom nomId term) n -> Proxy c -> (c n -> r) -> r

Monoid nomId => KPointed (FromNom nomId term)

Defined in AST.Term.Nominal

Methods

pureK :: (forall (n :: Knot -> Type). KWitness (FromNom nomId term) n -> Tree p n) -> Tree (FromNom nomId term) p

KFunctor (FromNom nomId term)

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

Semigroup nomId => KApply (FromNom nomId term)

Defined in AST.Term.Nominal

Methods

zipK :: Tree (FromNom nomId term) p -> Tree (FromNom nomId term) q -> Tree (FromNom nomId term) (Product p q)

KFoldable (FromNom nomId term)

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

KTraversable (FromNom nomId term)

Defined in AST.Term.Nominal

Methods

sequenceK :: Applicative f => Tree (FromNom nomId term) (ContainedK f p) -> f (Tree (FromNom nomId term) p)

Eq nomId => Eq (FromNom nomId term k)

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)

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)

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)

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)

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)

Defined in AST.Term.Nominal

Methods

rnf :: FromNom nomId term k -> ()

data KWitness (FromNom nomId term) node

Defined in AST.Term.Nominal

data KWitness (FromNom nomId term) node

type InferOf (FromNom n e)

Defined in AST.Term.Nominal

type InferOf (FromNom n e) = FuncType (TypeOf e)

type KNodesConstraint (FromNom nomId term) constraint

Defined in AST.Term.Nominal

type KNodesConstraint (FromNom nomId term) constraint = ()

type Rep (FromNom nomId term k)

Defined in AST.Term.Nominal

type Rep (FromNom nomId term k) = D1 (MetaData "FromNom" "AST.Term.Nominal" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" 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

class HasNominalInst nomId typ where

Methods

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

Methods

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

data LoadedNominalDecl typ v

A nominal declaration loaded into scope in an inference monad.

Instances

(RNodes t, KNodes (NomVarTypes t)) => KNodes (LoadedNominalDecl t)

Defined in AST.Term.Nominal

Associated Types

type KNodesConstraint (LoadedNominalDecl t) c :: Constraint

data KWitness (LoadedNominalDecl t) a :: Type

Methods

kLiftConstraint :: KNodesConstraint (LoadedNominalDecl t) c => KWitness (LoadedNominalDecl t) n -> Proxy c -> (c n -> r) -> r

(Recursively KFunctor typ, KFunctor (NomVarTypes typ)) => KFunctor (LoadedNominalDecl typ)

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

(Recursively KFoldable typ, KFoldable (NomVarTypes typ)) => KFoldable (LoadedNominalDecl typ)

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

(RTraversable typ, KTraversable (NomVarTypes typ)) => KTraversable (LoadedNominalDecl typ)

Defined in AST.Term.Nominal

Methods

sequenceK :: Applicative f => Tree (LoadedNominalDecl typ) (ContainedK f p) -> f (Tree (LoadedNominalDecl typ) p)

Constraints (LoadedNominalDecl typ v) Eq => Eq (LoadedNominalDecl typ v)

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)

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)

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)

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)

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)

Defined in AST.Term.Nominal

Methods

rnf :: LoadedNominalDecl typ v -> ()

data KWitness (LoadedNominalDecl t) n

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

Defined in AST.Term.Nominal

type KNodesConstraint (LoadedNominalDecl t) c = (KNodesConstraint (NomVarTypes t) c, c t, Recursive c)

type Rep (LoadedNominalDecl typ v)

Defined in AST.Term.Nominal

type Rep (LoadedNominalDecl typ v) = D1 (MetaData "LoadedNominalDecl" "AST.Term.Nominal" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" 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))