Module Unification

module Unification: sig .. end
A library of types and combinators supporting continuation-passing-style unifiers

type ('a, 'b) continuation = 'a -> 'b option 
The type of continuations accepted by CPS-unifiers
val trivial_continuation : ('a, 'a) continuation
type 'a state_update = 'a * 'a 
type ('a, 'b) realizer = ('a -> 'b) -> 'b 
type ('a, 'b, 'c) cps_unifier = 'c ->
'c -> ('a, 'b) continuation -> ('a, 'b) continuation
The type of continuation-passing-style unifiers that may accept an initial solution state. ('a, 'b, 'c) cps_unifier is the type of a CPS-unifier that unifies terms of type 'c producing a solution of type 'a by extending a given initial state, which is then passed to a continuation that returns a value of type 'b option. If unification is impossible, then the unifier should return None immediately without calling the continuation.
type ('a, 'b, 'c) cps_backtracker = 'c -> 'c -> ('a, 'b) continuation -> 'a -> 'b list 
module MakeUnifier: 
functor (T : sig
type t 
type elt 
val empty : t
val is_empty : t -> bool
val equal : t -> t -> bool
val add : elt -> t -> t
val choose : t -> elt
val remove : elt -> t -> t
val find_map : (elt -> 'a option) -> t -> 'a option
end) -> sig .. end
This functor makes a mk_unifier function for a particular implementation of a container.
val backtrack : ('a, 'b, 'c) cps_unifier ->
('a, 'b, 'c) cps_backtracker
backtrack u takes a cps-style unifier u and produces a backtracking unifier that returns a list of all possible solutions returned by u such that cont solution is not None.
val transform : ('d -> 'a) ->
('d -> 'a -> 'd) ->
('a, 'b, 'c) cps_unifier -> ('d, 'b, 'c) cps_unifier