hydra.strip module

Annotation and type stripping and normalization.

hydra.strip.deannotate_and_detype_term(t: Term) → Term

Strip type annotations from the top levels of a term.

hydra.strip.deannotate_term(t: Term) → Term

Strip all annotations (including System F type annotations) from the top levels of a term.

hydra.strip.deannotate_type(t: Type) → Type

Strip all annotations from a term.

hydra.strip.deannotate_type_parameters(t: Type) → Type

Strip any top-level type lambdas from a type, extracting the (possibly nested) type body.

hydra.strip.deannotate_type_recursive(typ: Type) → Type

Recursively strip all annotations from a type.

hydra.strip.deannotate_type_scheme_recursive(ts: TypeScheme) → TypeScheme

Recursively strip all annotations from a type scheme.

hydra.strip.detype_term(t: Term) → Term

Strip System F type annotations from the top levels of a term, but leave application-specific annotations intact.

hydra.strip.remove_term_annotations(term: Term) → Term

Recursively remove term annotations, including within subterms.

hydra.strip.remove_type_annotations(typ: Type) → Type

Recursively remove type annotations, including within subtypes.

hydra.strip.remove_type_annotations_from_term(term: Term) → Term

Strip type annotations (TypeLambda, TypeApplication, binding type schemes) from terms while preserving lambda domain types and other annotations.

hydra.strip.remove_types_from_term(term: Term) → Term

Strip type annotations from terms while preserving other annotations.

hydra.strip.strip_type_lambdas(t: Term) → Term

Strip outer type lambda wrappers from a term, preserving type application wrappers and annotations.