syntax-tree-0.1.0.0: Typed ASTs

Safe HaskellNone
LanguageHaskell2010

AST.Unify.Generalize

Description

Generalization of type schemes

Synopsis

Documentation

generalize :: forall m t. Unify m t => Tree (UVarOf m) t -> m (Tree (GTerm (UVarOf m)) t) Source #

Generalize a unification term pointed by the given variable to a GTerm. Unification variables that are scoped within the term become universally quantified skolems.

instantiate :: Unify m t => Tree (GTerm (UVarOf m)) t -> m (Tree (UVarOf m) t) Source #

Instantiate a generalized type with fresh unification variables for the quantified variables

data GTerm v ast Source #

An efficient representation of a type scheme arising from generalizing a unification term. Type subexpressions which are completely monomoprhic are tagged as such, to avoid redundant instantation and unification work

Constructors

GMono (v ast)

Completely monomoprhic term

GPoly (v ast)

Points to a quantified variable (instantiation will create fresh unification terms) (USkolem or UResolved)

GBody (ast # GTerm v)

Term with some polymorphic parts

Instances
Constraints (GTerm v ast) Eq => Eq (GTerm v ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Methods

(==) :: GTerm v ast -> GTerm v ast -> Bool #

(/=) :: GTerm v ast -> GTerm v ast -> Bool #

Constraints (GTerm v ast) Ord => Ord (GTerm v ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Methods

compare :: GTerm v ast -> GTerm v ast -> Ordering #

(<) :: GTerm v ast -> GTerm v ast -> Bool #

(<=) :: GTerm v ast -> GTerm v ast -> Bool #

(>) :: GTerm v ast -> GTerm v ast -> Bool #

(>=) :: GTerm v ast -> GTerm v ast -> Bool #

max :: GTerm v ast -> GTerm v ast -> GTerm v ast #

min :: GTerm v ast -> GTerm v ast -> GTerm v ast #

Constraints (GTerm v ast) Show => Show (GTerm v ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Methods

showsPrec :: Int -> GTerm v ast -> ShowS #

show :: GTerm v ast -> String #

showList :: [GTerm v ast] -> ShowS #

Generic (GTerm v ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Associated Types

type Rep (GTerm v ast) :: Type -> Type #

Methods

from :: GTerm v ast -> Rep (GTerm v ast) x #

to :: Rep (GTerm v ast) x -> GTerm v ast #

Constraints (GTerm v ast) Binary => Binary (GTerm v ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Methods

put :: GTerm v ast -> Put #

get :: Get (GTerm v ast) #

putList :: [GTerm v ast] -> Put #

Constraints (GTerm v ast) NFData => NFData (GTerm v ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Methods

rnf :: GTerm v ast -> () #

RNodes a => KNodes (Flip GTerm a) Source # 
Instance details

Defined in AST.Unify.Generalize

Associated Types

type KNodesConstraint (Flip GTerm a) c :: Constraint Source #

data KWitness (Flip GTerm a) a :: Type Source #

Methods

kLiftConstraint :: KNodesConstraint (Flip GTerm a) c => KWitness (Flip GTerm a) n -> Proxy c -> (c n -> r) -> r Source #

Recursively KFunctor ast => KFunctor (Flip GTerm ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Methods

mapK :: (forall (n :: Knot -> Type). KWitness (Flip GTerm ast) n -> Tree p n -> Tree q n) -> Tree (Flip GTerm ast) p -> Tree (Flip GTerm ast) q Source #

Recursively KFoldable ast => KFoldable (Flip GTerm ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Methods

foldMapK :: Monoid a => (forall (n :: Knot -> Type). KWitness (Flip GTerm ast) n -> Tree p n -> a) -> Tree (Flip GTerm ast) p -> a Source #

RTraversable ast => KTraversable (Flip GTerm ast) Source # 
Instance details

Defined in AST.Unify.Generalize

Methods

sequenceK :: Applicative f => Tree (Flip GTerm ast) (ContainedK f p) -> f (Tree (Flip GTerm ast) p) Source #

type Rep (GTerm v ast) Source # 
Instance details

Defined in AST.Unify.Generalize

type Rep (GTerm v ast) = D1 (MetaData "GTerm" "AST.Unify.Generalize" "syntax-tree-0.1.0.0-8tfou50n4eQ4Iq1dis9DWN" False) (C1 (MetaCons "GMono" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (v ast))) :+: (C1 (MetaCons "GPoly" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (v ast))) :+: C1 (MetaCons "GBody" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (ast # GTerm v)))))
data KWitness (Flip GTerm a) n Source # 
Instance details

Defined in AST.Unify.Generalize

type KNodesConstraint (Flip GTerm a) c Source # 
Instance details

Defined in AST.Unify.Generalize

type KNodesConstraint (Flip GTerm a) c = (c a, Recursive c)

_GMono :: forall v ast. Prism' (GTerm v ast) (v ast) Source #

_GPoly :: forall v ast. Prism' (GTerm v ast) (v ast) Source #

_GBody :: forall v ast. Prism' (GTerm v ast) ((#) ast (GTerm v)) 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
data KWitness Prune node Source # 
Instance details

Defined in AST.Knot.Prune

data KWitness Prune node where
data KWitness (ANode c) node Source # 
Instance details

Defined in AST.Combinator.ANode

data KWitness (ANode c) node where
data KWitness (F f) node Source # 
Instance details

Defined in AST.Knot.Functor

data KWitness (F f) node where
data KWitness (Ann a) node Source # 
Instance details

Defined in AST.Knot.Ann

data KWitness (Ann a) node where
data KWitness (UnifyError t) n Source # 
Instance details

Defined in AST.Unify.Error

data KWitness (UnifyError t) n where
data KWitness (FuncType typ) node Source # 
Instance details

Defined in AST.Term.FuncType

data KWitness (FuncType typ) node where
data KWitness (LoadedNominalDecl t) n Source # 
Instance details

Defined in AST.Term.Nominal

data KWitness (NominalDecl typ) node Source # 
Instance details

Defined in AST.Term.Nominal

data KWitness (App expr) node Source # 
Instance details

Defined in AST.Term.App

data KWitness (App expr) node where
data KWitness (ScopeTypes t) node Source # 
Instance details

Defined in AST.Term.NamelessScope

data KWitness (ScopeTypes t) node where
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 (ITerm a) e) n Source # 
Instance details

Defined in AST.Infer.Term

data KWitness (Flip (ITerm a) e) n where
data KWitness (Flip (BTerm a) e) n Source # 
Instance details

Defined in AST.Infer.Blame

data KWitness (Flip (BTerm a) e) n where
data KWitness (Compose a b) n Source # 
Instance details

Defined in AST.Combinator.Compose

data KWitness (Compose a b) n where
data KWitness (TermMap k expr) node Source # 
Instance details

Defined in AST.Term.Map

data KWitness (TermMap k expr) node where
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
data KWitness (TypeSig vars term) node Source # 
Instance details

Defined in AST.Term.TypeSig

data KWitness (TypeSig vars term) node where
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
data KWitness (NominalInst n v) c Source # 
Instance details

Defined in AST.Term.Nominal

data KWitness (Let v expr) node Source # 
Instance details

Defined in AST.Term.Let

data KWitness (Let v expr) node where
data KWitness (Lam v expr) node Source # 
Instance details

Defined in AST.Term.Lam

data KWitness (Lam v expr) node where
data KWitness (Scope expr a) node Source # 
Instance details

Defined in AST.Term.NamelessScope

data KWitness (Scope expr a) node where
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 (Sum a b) n Source # 
Instance details

Defined in AST.Class.Nodes

data KWitness (Sum a 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
data KWitness (RowExtend key val rest) node Source # 
Instance details

Defined in AST.Term.Row

data KWitness (RowExtend key val rest) node where
data KWitness (TypedLam var typ expr) node Source # 
Instance details

Defined in AST.Term.TypedLam

data KWitness (TypedLam var typ expr) node where

instantiateWith :: forall m t a. Unify m t => m a -> (forall n. TypeConstraintsOf n -> Tree (UTerm (UVarOf m)) n) -> Tree (GTerm (UVarOf m)) t -> m (Tree (UVarOf m) t, a) Source #

instantiateForAll :: Unify m t => (TypeConstraintsOf t -> Tree (UTerm (UVarOf m)) t) -> Tree (UVarOf m) t -> WriterT [m ()] m (Tree (UVarOf m) t) Source #

Exports for SPECIALIZE pragmas.

instantiateH :: forall m t. Unify m t => (forall n. TypeConstraintsOf n -> Tree (UTerm (UVarOf m)) n) -> Tree (GTerm (UVarOf m)) t -> WriterT [m ()] m (Tree (UVarOf m) t) Source #