module Flx_unify: sig
.. end
this module provides type unification
and utilities
val unification : bool ->
Flx_types.symbol_table_t ->
(Flx_types.btypecode_t * Flx_types.btypecode_t) list ->
Flx_mtypes1.IntSet.t -> (int * Flx_types.btypecode_t) list
obtain the mgu of a set of type equations with specified
dependent variable set, throws Not_found if cannot unify
val maybe_unification : Flx_types.symbol_table_t ->
(Flx_types.btypecode_t * Flx_types.btypecode_t) list ->
(int * Flx_types.btypecode_t) list option
obtain the mgu of a set of type equations
val maybe_matches : Flx_types.symbol_table_t ->
(Flx_types.btypecode_t * Flx_types.btypecode_t) list ->
(int * Flx_types.btypecode_t) list option
obtain the mgu of a set of type equations,
for matching parameters against arguments: allows
special subtyping for lvalues
val maybe_specialisation : Flx_types.symbol_table_t ->
(Flx_types.btypecode_t * Flx_types.btypecode_t) list ->
(int * Flx_types.btypecode_t) list option
val unifies : Flx_types.symbol_table_t ->
Flx_types.btypecode_t -> Flx_types.btypecode_t -> bool
test if two types unify
val compare_sigs : Flx_types.symbol_table_t ->
Flx_types.btypecode_t ->
Flx_types.btypecode_t -> Flx_types.partial_order_result_t
compare type for structural/unificational ordering
val do_unify : Flx_mtypes2.sym_state_t ->
Flx_types.btypecode_t -> Flx_types.btypecode_t -> bool
check if the two types unify: update the
variable definitions in sym_state ??? Only
useful if type variables are global, which is
the function return type unknown variable case..
val type_eq : Flx_types.symbol_table_t ->
Flx_types.btypecode_t -> Flx_types.btypecode_t -> bool
compare for iso-equality
val type_match : Flx_types.symbol_table_t ->
Flx_types.btypecode_t -> Flx_types.btypecode_t -> bool
compare parameter with argument type,
argument may have extra lvalue in it
val lstrip : Flx_types.symbol_table_t -> Flx_types.btypecode_t -> Flx_types.btypecode_t
lstrip t
returns t all lvalue combinators elided
val unfold : Flx_types.symbol_table_t -> Flx_types.btypecode_t -> Flx_types.btypecode_t
unfold t
returns t with each fix variable
denoting t replaced with t
val fold : Flx_types.symbol_table_t -> Flx_types.btypecode_t -> Flx_types.btypecode_t
undo an unfold
minimise the representation of a type
with respect to recursion
val minimise : Flx_types.symbol_table_t -> Flx_types.btypecode_t -> Flx_types.btypecode_t
val list_subst : (int * Flx_types.btypecode_t) list ->
Flx_types.btypecode_t -> Flx_types.btypecode_t
replace variables in the term using
the mapping in a list
val mk_varmap : (string * int) list ->
Flx_types.btypecode_t list -> (int, Flx_types.btypecode_t) Hashtbl.t
make a varmap using vs and ts list
val tsubst : (string * int) list ->
Flx_types.btypecode_t list -> Flx_types.btypecode_t -> Flx_types.btypecode_t
replace variables using vs and ts list to
determine mapping
val varmap_subst : (int, Flx_types.btypecode_t) Hashtbl.t ->
Flx_types.btypecode_t -> Flx_types.btypecode_t
replace variables in the term using
the mapping in the hashtable
val var_occurs : Flx_types.btypecode_t -> bool
check for variables
val var_i_occurs : int -> Flx_types.btypecode_t -> bool
check for a particular variable
val var_list_occurs : int list -> Flx_types.btypecode_t -> bool
check for variables
val normalise_type : Flx_types.btypecode_t -> int list * Flx_types.btypecode_t
normalise returns count of the type variables
occuring in a type, and the type rewritten so the type variables
are systematically numbered from 0 - n-1
val check_recursion : Flx_types.btypecode_t -> unit
check for bad recursions
val dual : Flx_types.btypecode_t -> Flx_types.btypecode_t
construct the dual of a type