Safe Haskell	None
Language	Haskell2010

AST.Term.NamelessScope

Description

A Knot based implementation of "locally-nameless" terms, inspired by the bound library and the technique from Bird & Paterson's "de Bruijn notation as a nested datatype"

Synopsis

newtype Scope expr a k = Scope (k # expr (Maybe a))
_Scope :: forall expr a k expr a k. Iso (Scope expr a k) (Scope expr a k) ((#) k (expr (Maybe a))) ((#) k (expr (Maybe a)))
data family KWitness k :: (Knot -> Type) -> Type
newtype ScopeVar (expr :: * -> Knot -> *) a (k :: Knot) = ScopeVar a
_ScopeVar :: forall expr a k expr a k. Iso (ScopeVar expr a k) (ScopeVar expr a k) a a
data EmptyScope
class DeBruijnIndex a where
- deBruijnIndex :: Prism' Int a
newtype ScopeTypes t v = ScopeTypes (Seq (v # t))
_ScopeTypes :: forall t v t v. Iso (ScopeTypes t v) (ScopeTypes t v) (Seq ((#) v t)) (Seq ((#) v t))
class HasScopeTypes v t env where
- scopeTypes :: Lens' env (Tree (ScopeTypes t) v)

Documentation

newtype Scope expr a k Source #

Constructors

Scope (k # expr (Maybe a))

Instances

(Infer1 m t, HasInferOf1 t, InferOf1IndexConstraint t ~ DeBruijnIndex, DeBruijnIndex k, Unify m (TypeOf (t k)), MonadReader env m, HasScopeTypes (UVarOf m) (TypeOf (t k)) env, HasInferredType (t k)) => Infer m (Scope t k) Source #
Instance details Defined in AST.Term.NamelessScope Methods inferBody :: Tree (Scope t k) (InferChild m k0) -> m (Tree (Scope t k) k0, Tree (InferOf (Scope t k)) (UVarOf m)) Source # inferContext :: Proxy m -> Proxy (Scope t k) -> Dict (KNodesConstraint (Scope t k) (Infer m), KNodesConstraint (InferOf (Scope t k)) (Unify m)) Source #
HasTypeOf1 t => HasInferOf1 (Scope t) Source #
Instance details Defined in AST.Term.NamelessScope Associated Types type InferOf1 (Scope t) :: Knot -> Type Source # type InferOf1IndexConstraint (Scope t) :: Type -> Constraint Source # Methods hasInferOf1 :: Proxy (Scope t k) -> Dict (InferOf (Scope t k) ~ InferOf1 (Scope t)) Source #
KNodes (Scope expr a) Source #
Instance details Defined in AST.Term.NamelessScope Associated Types type KNodesConstraint (Scope expr a) c :: Constraint Source # data KWitness (Scope expr a) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (Scope expr a) c => KWitness (Scope expr a) n -> Proxy c -> (c n -> r) -> r Source #
KPointed (Scope expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods pureK :: (forall (n :: Knot -> Type). KWitness (Scope expr a) n -> Tree p n) -> Tree (Scope expr a) p Source #
KFunctor (Scope expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods mapK :: (forall (n :: Knot -> Type). KWitness (Scope expr a) n -> Tree p n -> Tree q n) -> Tree (Scope expr a) p -> Tree (Scope expr a) q Source #
KApply (Scope expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods zipK :: Tree (Scope expr a) p -> Tree (Scope expr a) q -> Tree (Scope expr a) (Product p q) Source #
KFoldable (Scope expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods foldMapK :: Monoid a0 => (forall (n :: Knot -> Type). KWitness (Scope expr a) n -> Tree p n -> a0) -> Tree (Scope expr a) p -> a0 Source #
KTraversable (Scope expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods sequenceK :: Applicative f => Tree (Scope expr a) (ContainedK f p) -> f (Tree (Scope expr a) p) Source #
ZipMatch (Scope expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods zipMatch :: Tree (Scope expr a) p -> Tree (Scope expr a) q -> Maybe (Tree (Scope expr a) (Product p q)) Source #
type InferOf1 (Scope t) Source #
Instance details Defined in AST.Term.NamelessScope type InferOf1 (Scope t) = FuncType (TypeOf1 t)
type InferOf1IndexConstraint (Scope t) Source #
Instance details Defined in AST.Term.NamelessScope type InferOf1IndexConstraint (Scope t) = DeBruijnIndex
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))
type InferOf (Scope t k) Source #
Instance details Defined in AST.Term.NamelessScope type InferOf (Scope t k) = FuncType (TypeOf (t k))
type KNodesConstraint (Scope expr a) constraint Source #
Instance details Defined in AST.Term.NamelessScope type KNodesConstraint (Scope expr a) constraint = constraint (expr (Maybe a))

_Scope :: forall expr a k expr a k. Iso (Scope expr a k) (Scope expr a k) ((#) k (expr (Maybe a))) ((#) k (expr (Maybe a))) 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

newtype ScopeVar (expr :: * -> Knot -> *) a (k :: Knot) Source #

Constructors

ScopeVar a

Instances

(MonadReader env m, HasScopeTypes (UVarOf m) (TypeOf (t k)) env, DeBruijnIndex k, Unify m (TypeOf (t k))) => Infer m (ScopeVar t k) Source #
Instance details Defined in AST.Term.NamelessScope Methods inferBody :: Tree (ScopeVar t k) (InferChild m k0) -> m (Tree (ScopeVar t k) k0, Tree (InferOf (ScopeVar t k)) (UVarOf m)) Source # inferContext :: Proxy m -> Proxy (ScopeVar t k) -> Dict (KNodesConstraint (ScopeVar t k) (Infer m), KNodesConstraint (InferOf (ScopeVar t k)) (Unify m)) Source #
KNodes (ScopeVar expr a) Source #
Instance details Defined in AST.Term.NamelessScope Associated Types type KNodesConstraint (ScopeVar expr a) c :: Constraint Source # data KWitness (ScopeVar expr a) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (ScopeVar expr a) c => KWitness (ScopeVar expr a) n -> Proxy c -> (c n -> r) -> r Source #
Monoid a => KPointed (ScopeVar expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods pureK :: (forall (n :: Knot -> Type). KWitness (ScopeVar expr a) n -> Tree p n) -> Tree (ScopeVar expr a) p Source #
KFunctor (ScopeVar expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods mapK :: (forall (n :: Knot -> Type). KWitness (ScopeVar expr a) n -> Tree p n -> Tree q n) -> Tree (ScopeVar expr a) p -> Tree (ScopeVar expr a) q Source #
Semigroup a => KApply (ScopeVar expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods zipK :: Tree (ScopeVar expr a) p -> Tree (ScopeVar expr a) q -> Tree (ScopeVar expr a) (Product p q) Source #
KFoldable (ScopeVar expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods foldMapK :: Monoid a0 => (forall (n :: Knot -> Type). KWitness (ScopeVar expr a) n -> Tree p n -> a0) -> Tree (ScopeVar expr a) p -> a0 Source #
KTraversable (ScopeVar expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods sequenceK :: Applicative f => Tree (ScopeVar expr a) (ContainedK f p) -> f (Tree (ScopeVar expr a) p) Source #
Eq a => ZipMatch (ScopeVar expr a) Source #
Instance details Defined in AST.Term.NamelessScope Methods zipMatch :: Tree (ScopeVar expr a) p -> Tree (ScopeVar expr a) q -> Maybe (Tree (ScopeVar expr a) (Product p q)) Source #
data KWitness (ScopeVar expr a) node Source #
Instance details Defined in AST.Term.NamelessScope data KWitness (ScopeVar expr a) node
type InferOf (ScopeVar t k) Source #
Instance details Defined in AST.Term.NamelessScope type InferOf (ScopeVar t k) = ANode (TypeOf (t k))
type KNodesConstraint (ScopeVar expr a) constraint Source #
Instance details Defined in AST.Term.NamelessScope type KNodesConstraint (ScopeVar expr a) constraint = ()

_ScopeVar :: forall expr a k expr a k. Iso (ScopeVar expr a k) (ScopeVar expr a k) a a Source #

data EmptyScope Source #

Instances

DeBruijnIndex EmptyScope Source #
Instance details Defined in AST.Term.NamelessScope Methods deBruijnIndex :: Prism' Int EmptyScope Source #
InvDeBruijnIndex EmptyScope Source #
Instance details Defined in AST.Term.NamelessScope.InvDeBruijn Methods deBruijnIndexMax :: Proxy EmptyScope -> Int Source #

class DeBruijnIndex a where Source #

Methods

deBruijnIndex :: Prism' Int a Source #

Instances

DeBruijnIndex EmptyScope Source #
Instance details Defined in AST.Term.NamelessScope Methods deBruijnIndex :: Prism' Int EmptyScope Source #
DeBruijnIndex a => DeBruijnIndex (Maybe a) Source #
Instance details Defined in AST.Term.NamelessScope Methods deBruijnIndex :: Prism' Int (Maybe a) Source #

newtype ScopeTypes t v Source #

Constructors

ScopeTypes (Seq (v # t))

Instances

HasScopeTypes v t (Tree (ScopeTypes t) v) Source #
Instance details Defined in AST.Term.NamelessScope Methods scopeTypes :: Lens' (Tree (ScopeTypes t) v) (Tree (ScopeTypes t) v) Source #
KNodes (ScopeTypes t) Source #
Instance details Defined in AST.Term.NamelessScope Associated Types type KNodesConstraint (ScopeTypes t) c :: Constraint Source # data KWitness (ScopeTypes t) a :: Type Source # Methods kLiftConstraint :: KNodesConstraint (ScopeTypes t) c => KWitness (ScopeTypes t) n -> Proxy c -> (c n -> r) -> r Source #
KPointed (ScopeTypes t) Source #
Instance details Defined in AST.Term.NamelessScope Methods pureK :: (forall (n :: Knot -> Type). KWitness (ScopeTypes t) n -> Tree p n) -> Tree (ScopeTypes t) p Source #
KFunctor (ScopeTypes t) Source #
Instance details Defined in AST.Term.NamelessScope Methods mapK :: (forall (n :: Knot -> Type). KWitness (ScopeTypes t) n -> Tree p n -> Tree q n) -> Tree (ScopeTypes t) p -> Tree (ScopeTypes t) q Source #
KApply (ScopeTypes t) Source #
Instance details Defined in AST.Term.NamelessScope Methods zipK :: Tree (ScopeTypes t) p -> Tree (ScopeTypes t) q -> Tree (ScopeTypes t) (Product p q) Source #
KFoldable (ScopeTypes t) Source #
Instance details Defined in AST.Term.NamelessScope Methods foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness (ScopeTypes t) n -> Tree p n -> a) -> Tree (ScopeTypes t) p -> a Source #
KTraversable (ScopeTypes t) Source #
Instance details Defined in AST.Term.NamelessScope Methods sequenceK :: Applicative f => Tree (ScopeTypes t) (ContainedK f p) -> f (Tree (ScopeTypes t) p) Source #
Semigroup (ScopeTypes t v) Source #
Instance details Defined in AST.Term.NamelessScope Methods (<>) :: ScopeTypes t v -> ScopeTypes t v -> ScopeTypes t v # sconcat :: NonEmpty (ScopeTypes t v) -> ScopeTypes t v # stimes :: Integral b => b -> ScopeTypes t v -> ScopeTypes t v #
Monoid (ScopeTypes t v) Source #
Instance details Defined in AST.Term.NamelessScope Methods mempty :: ScopeTypes t v # mappend :: ScopeTypes t v -> ScopeTypes t v -> ScopeTypes t v # mconcat :: [ScopeTypes t v] -> ScopeTypes t v #
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
type KNodesConstraint (ScopeTypes t) constraint Source #
Instance details Defined in AST.Term.NamelessScope type KNodesConstraint (ScopeTypes t) constraint = constraint t

_ScopeTypes :: forall t v t v. Iso (ScopeTypes t v) (ScopeTypes t v) (Seq ((#) v t)) (Seq ((#) v t)) Source #

class HasScopeTypes v t env where Source #

Methods

scopeTypes :: Lens' env (Tree (ScopeTypes t) v) Source #

Instances

HasScopeTypes v t (Tree (ScopeTypes t) v) Source #
Instance details Defined in AST.Term.NamelessScope Methods scopeTypes :: Lens' (Tree (ScopeTypes t) v) (Tree (ScopeTypes t) v) Source #