hydra.substitution module

Variable substitution in type and term expressions.

hydra.substitution.compose_type_subst(s1: TypeSubst, s2: TypeSubst) → TypeSubst

Compose two type substitutions.

hydra.substitution.compose_type_subst_list(v1: Sequence[TypeSubst]) → TypeSubst

Compose a list of type substitutions.

hydra.substitution.compose_type_subst_non_empty(s1: TypeSubst, s2: TypeSubst) → TypeSubst

Compose two non-empty type substitutions (internal helper).

hydra.substitution.id_type_subst() → TypeSubst

The identity type substitution.

hydra.substitution.singleton_type_subst(v: Name, t: Type) → TypeSubst

Create a type substitution with a single variable mapping.

hydra.substitution.subst_in_class_constraints(subst: TypeSubst, constraints: Mapping[Name, TypeVariableConstraints]) → Mapping[Name, TypeVariableConstraints]

Apply a type substitution to class constraints, propagating to free variables or discharging/retaining on concrete resolution.

hydra.substitution.subst_in_context(subst: TypeSubst, cx: Graph) → Graph

Apply a type substitution to a graph’s bound types and class constraints.

hydra.substitution.subst_in_type(subst: TypeSubst, typ0: Type) → Type

Apply a type substitution to a type.

hydra.substitution.subst_in_type_non_empty(subst: TypeSubst, typ0: Type) → Type

Apply a non-empty type substitution to a type (internal helper).

hydra.substitution.subst_in_type_scheme(subst: TypeSubst, ts: TypeScheme) → TypeScheme

Apply a type substitution to a type scheme. The scheme’s quantifier variables shadow the substitution: any name in typeSchemeVariables is removed from subst before substituting into the body and constraints. Without this, a substitution like {t0 -> Foo} applied to forall [t0]. t0 -> t0 would incorrectly replace the bound t0.

hydra.substitution.subst_types_in_term(subst: TypeSubst, term0: Term) → Term

Apply a type substitution to the type annotations within a term.

hydra.substitution.substitute_in_binding(subst: TermSubst, b: Binding) → Binding

Apply a term substitution to a binding.

hydra.substitution.substitute_in_constraint(subst: TypeSubst, c: TypeConstraint) → TypeConstraint

Apply a type substitution to a type constraint.

hydra.substitution.substitute_in_constraints(subst: TypeSubst, cs: Sequence[TypeConstraint]) → Sequence[TypeConstraint]

Apply a type substitution to a list of type constraints.

hydra.substitution.substitute_in_term(subst: TermSubst, term0: Term) → Term

Apply a term substitution to a term.