syntax-tree-0.1.0.0: Typed ASTs

Safe HaskellNone
LanguageHaskell2010

AST.Class.Infer

Synopsis

Documentation

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

InferOf e is the inference result of e.

Most commonly it is an inferred type, using

type instance InferOf MyTerm = ANode MyType

But it may also be other things, for example:

  • An inferred value (for types inside terms)
  • An inferred type together with a scope
Instances
type InferOf (App e) Source # 
Instance details

Defined in AST.Term.App

type InferOf (App e) = ANode (TypeOf e)
type InferOf (Compose Prune t) Source # 
Instance details

Defined in AST.Knot.Prune

type InferOf (Var v t) Source # 
Instance details

Defined in AST.Term.Var

type InferOf (Var v t) = ANode (TypeOf t)
type InferOf (Scheme v t) Source # 
Instance details

Defined in AST.Term.Scheme

type InferOf (Scheme v t) = Flip GTerm t
type InferOf (TypeSig v t) Source # 
Instance details

Defined in AST.Term.TypeSig

type InferOf (TypeSig v t) = InferOf t
type InferOf (FromNom n e) Source # 
Instance details

Defined in AST.Term.Nominal

type InferOf (FromNom n e) = FuncType (TypeOf e)
type InferOf (ToNom n e) Source # 
Instance details

Defined in AST.Term.Nominal

type InferOf (Let v e) Source # 
Instance details

Defined in AST.Term.Let

type InferOf (Let v e) = InferOf e
type InferOf (Lam v t) Source # 
Instance details

Defined in AST.Term.Lam

type InferOf (Lam v t) = FuncType (TypeOf t)
type InferOf (Scope t k) Source # 
Instance details

Defined in AST.Term.NamelessScope

type InferOf (Scope t k) = FuncType (TypeOf (t k))
type InferOf (ScopeVar t k) Source # 
Instance details

Defined in AST.Term.NamelessScope

type InferOf (ScopeVar t k) = ANode (TypeOf (t k))
type InferOf (Sum a b) Source # 
Instance details

Defined in AST.Class.Infer

type InferOf (Sum a b) = InferOf a
type InferOf (TypedLam v t e) Source # 
Instance details

Defined in AST.Term.TypedLam

type InferOf (TypedLam v t e) = FuncType (TypeOf e)

class (Monad m, KFunctor t) => Infer m t where Source #

Infer m t enables infer to perform type-inference for t in the Monad m.

The inferContext method represents the following constraints on t:

  • KNodesConstraint (InferOf t) (Unify m) - The child nodes of the inferrence can unify in the m Monad
  • KNodesConstraint t (Infer m) - Infer m is also available for child nodes

It replaces context for the Infer class to avoid UndecidableSuperClasses.

Instances usually don't need to implement this method as the default implementation works for them, but infinitely polymorphic trees such as Scope do need to implement the method, because the required context is infinite.

Minimal complete definition

inferBody

Methods

inferBody :: Tree t (InferChild m k) -> m (Tree t k, Tree (InferOf t) (UVarOf m)) Source #

Infer the body of an expression given the inference actions for its child nodes.

inferContext :: Proxy m -> Proxy t -> Dict (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m)) Source #

inferContext :: (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m)) => Proxy m -> Proxy t -> Dict (KNodesConstraint t (Infer m), KNodesConstraint (InferOf t) (Unify m)) Source #

Instances
(Infer m expr, HasInferredType expr, HasFuncType (TypeOf expr), Unify m (TypeOf expr)) => Infer m (App expr) Source # 
Instance details

Defined in AST.Term.App

Methods

inferBody :: Tree (App expr) (InferChild m k) -> m (Tree (App expr) k, Tree (InferOf (App expr)) (UVarOf m)) Source #

inferContext :: Proxy m -> Proxy (App expr) -> Dict (KNodesConstraint (App expr) (Infer m), KNodesConstraint (InferOf (App expr)) (Unify m)) Source #

(Unify m (TypeOf expr), HasScope m (ScopeOf expr), VarType v expr, Monad m) => Infer m (Var v expr) Source # 
Instance details

Defined in AST.Term.Var

Methods

inferBody :: Tree (Var v expr) (InferChild m k) -> m (Tree (Var v expr) k, Tree (InferOf (Var v expr)) (UVarOf m)) Source #

inferContext :: Proxy m -> Proxy (Var v expr) -> Dict (KNodesConstraint (Var v expr) (Infer m), KNodesConstraint (InferOf (Var v expr)) (Unify m)) Source #

(Monad m, HasInferredValue typ, Unify m typ, KTraversable varTypes, KNodesConstraint varTypes (MonadInstantiate m), RTraversable typ, Infer m typ) => Infer m (Scheme varTypes typ) Source # 
Instance details

Defined in AST.Term.Scheme

Methods

inferBody :: Tree (Scheme varTypes typ) (InferChild m k) -> m (Tree (Scheme varTypes typ) k, Tree (InferOf (Scheme varTypes typ)) (UVarOf m)) Source #

inferContext :: Proxy m -> Proxy (Scheme varTypes typ) -> Dict (KNodesConstraint (Scheme varTypes typ) (Infer m), KNodesConstraint (InferOf (Scheme varTypes typ)) (Unify m)) Source #

(MonadScopeLevel m, HasInferredType term, HasInferredValue (TypeOf term), KTraversable vars, KTraversable (InferOf term), KNodesConstraint (InferOf term) (Unify m), KNodesConstraint vars (MonadInstantiate m), Unify m (TypeOf term), Infer m (TypeOf term), Infer m term) => Infer m (TypeSig vars term) Source # 
Instance details

Defined in AST.Term.TypeSig

Methods

inferBody :: Tree (TypeSig vars term) (InferChild m k) -> m (Tree (TypeSig vars term) k, Tree (InferOf (TypeSig vars term)) (UVarOf m)) Source #

inferContext :: Proxy m -> Proxy (TypeSig vars term) -> Dict (KNodesConstraint (TypeSig vars term) (Infer m), KNodesConstraint (InferOf (TypeSig vars term)) (Unify m)) Source #

(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 #

(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 #

(MonadScopeLevel m, LocalScopeType v (Tree (GTerm (UVarOf m)) (TypeOf expr)) m, Unify m (TypeOf expr), HasInferredType expr, KNodesConstraint (InferOf expr) (Unify m), KTraversable (InferOf expr), Infer m expr) => Infer m (Let v expr) Source # 
Instance details

Defined in AST.Term.Let

Methods

inferBody :: Tree (Let v expr) (InferChild m k) -> m (Tree (Let v expr) k, Tree (InferOf (Let v expr)) (UVarOf m)) Source #

inferContext :: Proxy m -> Proxy (Let v expr) -> Dict (KNodesConstraint (Let v expr) (Infer m), KNodesConstraint (InferOf (Let v expr)) (Unify m)) Source #

(Infer m t, Unify m (TypeOf t), HasInferredType t, LocalScopeType v (Tree (UVarOf m) (TypeOf t)) m) => Infer m (Lam v t) Source # 
Instance details

Defined in AST.Term.Lam

Methods

inferBody :: Tree (Lam v t) (InferChild m k) -> m (Tree (Lam v t) k, Tree (InferOf (Lam v t)) (UVarOf m)) Source #

inferContext :: Proxy m -> Proxy (Lam v t) -> Dict (KNodesConstraint (Lam v t) (Infer m), KNodesConstraint (InferOf (Lam v t)) (Unify m)) Source #

(Infer m t, KPointed (InferOf t), KTraversable (InferOf t)) => Infer m (Compose Prune t) Source # 
Instance details

Defined in AST.Knot.Prune

(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

(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 #

(InferOf a ~ InferOf b, Infer m a, Infer m b) => Infer m (Sum a b) Source # 
Instance details

Defined in AST.Class.Infer

Methods

inferBody :: Tree (Sum a b) (InferChild m k) -> m (Tree (Sum a b) k, Tree (InferOf (Sum a b)) (UVarOf m)) Source #

inferContext :: Proxy m -> Proxy (Sum a b) -> Dict (KNodesConstraint (Sum a b) (Infer m), KNodesConstraint (InferOf (Sum a b)) (Unify m)) Source #

(Infer m t, Infer m e, HasInferredType e, Unify m (TypeOf e), HasChild (InferOf t) (TypeOf e), LocalScopeType v (Tree (UVarOf m) (TypeOf e)) m) => Infer m (TypedLam v t e) Source # 
Instance details

Defined in AST.Term.TypedLam

Methods

inferBody :: Tree (TypedLam v t e) (InferChild m k) -> m (Tree (TypedLam v t e) k, Tree (InferOf (TypedLam v t e)) (UVarOf m)) Source #

inferContext :: Proxy m -> Proxy (TypedLam v t e) -> Dict (KNodesConstraint (TypedLam v t e) (Infer m), KNodesConstraint (InferOf (TypedLam v t e)) (Unify m)) Source #

Recursive (Infer m) Source # 
Instance details

Defined in AST.Class.Infer

Methods

recurse :: (KNodes k, Infer m k) => Proxy (Infer m k) -> Dict (KNodesConstraint k (Infer m)) Source #

newtype InferChild m k t Source #

A Knot containing an inference action.

The caller may modify the scope before invoking the action via localScopeType or localLevel

Constructors

InferChild 

Fields

_InferChild :: forall m k t m k t. Iso (InferChild m k t) (InferChild m k t) (m (InferredChild (UVarOf m) k t)) (m (InferredChild (UVarOf m) k t)) Source #

data InferredChild v k t Source #

A Knot containing an inferred child node

Constructors

InferredChild 

Fields

  • _inRep :: !(k t)

    Inferred node.

    An inferBody implementation needs to place this value in the corresponding child node of the inferred term body

  • _inType :: !(Tree (InferOf (GetKnot t)) v)

    The inference result for the child node.

    An inferBody implementation may use it to perform unifications with it.

inType :: forall v k t v. Lens (InferredChild v k t) (InferredChild v k t) (Tree (InferOf (GetKnot t)) v) (Tree (InferOf (GetKnot t)) v) Source #

inRep :: forall v k t k. Lens (InferredChild v k t) (InferredChild v k t) (k t) (k t) Source #