hydra.environment module

Graph to type environment conversions.

hydra.environment.definition_as_type_application_term(el: Binding) object

Convert a definition to a typed term.

hydra.environment.graph_as_let(bindings: Sequence[Binding], body: Term) Let

Convert bindings and a body to a let expression.

hydra.environment.graph_as_term(bindings: Sequence[Binding], body: Term) Term

Convert bindings and a body to a term, using let-term duality.

hydra.environment.graph_as_types(graph: Graph, els: Sequence[Binding]) object

Decode a list of type-encoding bindings into a map of named types.

hydra.environment.partition_definitions(defs: Sequence[Definition]) tuple[Sequence[TypeDefinition], Sequence[TermDefinition]]

Partition a list of definitions into type definitions and term definitions.

hydra.environment.reorder_defs(defs: Sequence[Definition]) Sequence[Definition]

Reorder definitions: types first (with hydra.core.Name first among types), then topologically sorted terms.

hydra.environment.schema_graph_to_typing_environment(g: Graph) object

Convert a schema graph to a typing environment (Either version).

hydra.environment.term_as_bindings(term: Term) Sequence[Binding]

Extract the bindings from a let term, or return an empty list for other terms.

hydra.environment.types_to_definitions(type_map: Mapping[Name, Type]) Sequence[Binding]

Encode a map of named types to a list of bindings.

hydra.environment.with_lambda_context(get_context: Callable[[T0], Graph], set_context: Callable[[Graph, T0], T1], env: T0, lam: Lambda, body: Callable[[T1], T2]) T2

Execute a computation in the context of a lambda body, extending the type context with the lambda parameter.

hydra.environment.with_let_context(get_context: Callable[[T0], Graph], set_context: Callable[[Graph, T0], T1], for_binding: Callable[[Graph, Binding], object], env: T0, letrec: Let, body: Callable[[T1], T2]) T2

Execute a computation in the context of a let body, extending the type context with the let bindings.

hydra.environment.with_type_lambda_context(get_context: Callable[[T0], Graph], set_context: Callable[[Graph, T0], T1], env: T0, tlam: TypeLambda, body: Callable[[T1], T2]) T2

Execute a computation in the context of a type lambda body, extending the type context with the type parameter.