Module Generic_core.Extensible

module Extensible: Generic_core_extensible

Extensible type-indexed functions.

exception Type_pattern_match_failure of string

Raised by the f field of a Generic_core_extensible.closure when there is no case registered to deal with the type witness.

exception Type_pattern_overwrite of string

Raised by the ext field of a Generic_core_extensible.closure when trying to extend a type indexed function with a case for a pattern that is already covered.

type 'b ty_fun = {

f : 'a. 'a Ty.ty -> ('a, 'b) App.t;

}

Type-indexed function, 'b is the code for a parametric type 'a f such that 'b ty_fun is equivalent to for all 'a . 'a f

type 'b closure = {

	`f : 'a. 'a Ty.ty -> ('a, 'b) App.t;`	`(*`	`f`: applies the extensible function. Raises `Type_pattern_match_failure` when the type index doesn't match any of the patterns in the collection.	`*)`
	`ext : 'a. 'a Ty.pat -> 'b ty_fun -> unit;`	`(*`	`ext`: extends the function with a new case. We must provide a type pattern, (example: `List Any`). The `ty_fun` provided is only expected to handle types matching with the pattern. Effectful. Raises `Pattern_overwrite` when called with a type pattern that was already registered.	`*)`

}

A closure allows us to call a type-indexed function and to extend it to new type cases.

val create : string -> 'f closure

create name, creates a new closure initially empty: calling f will raise Type_pattern_match_failure. The name is used in the exception messages. Effectful.