gistfile1.fs

module type INFERING = functor(T:Typing.TYPING) ->
sig
    val unify: (T.t * T.t) list -> (T.t * T.t) list
    exception Occurs
end

module INFERING:INFERING = functor(T:Typing.TYPING) ->
struct
    exception Occurs
    open Util

    let sub x y rs = List.map (fun (a,b) -> ((T.substitute x y a), (T.substitute x y b)) ) rs

    let unify constr = 
        let not_occurs a b f = if not (T.occurs (T.id_of a) b) then f () else raise Occurs
        in let rec uni = function
        | [] -> []
        | (a, b)::rest when a = b -> uni rest
        | (a, b)::rest when (T.isvar a) ->  not_occurs a b (fun () ->  uni (sub (T.id_of a) b rest) @ [(a, b)] )
        | (a, b)::rest when (not (T.isvar a)) && T.isvar b -> uni ((b, a)::rest)
        | ((x,y) as z)::rest -> uni (T.merge_constraints z @ rest )
        in uni constr |> uni
end