module Scheme: functor (Root : SCHEME_ROOT) -> sig end
The functor scheme allows to build an implementation of functions
dealing which each considered form schemes.
val copy : ?subst:Dalton.Make.subst -> Root.t -> Root.t
copy ?subst sh returns a fresh copy of the type scheme sh.
No particular assumption is made about the type scheme sh, but,
for efficiency, it is more than a good idea to solve it previously.
val fprint : Format.formatter -> Root.t -> unit
fprint ppf sh pretty-prints the scheme sh on the formatter ppf.
The scheme sh is assumed to be solved.
val draw : Draw.window -> Root.t -> int -> int -> int * int
draw window sh x y draws the scheme sh on the window window.
The bottom left corner of the drawing has coordinates x and y
and the function returns the coordinates of the upper right
corner.
type solve_report
A solve report records an explanation of why the resolution
of a scheme fails.
val report_solve : Format.formatter -> solve_report -> unit
report_solve ppf r pretty prints an error message on the
formatter ppf corresponding to the comparison report r.
val solve : Root.t -> solve_report option
solve sh solves the scheme sh. If this function
returns None then the scheme sh has some instances.
Moreover, it is stored in a "solved" form which is preserved
as long as no term or constraint is added to its constraint
set.
type comparison_report
A comparison report records an explanation of the failure of
the comparison of two schemes.
val report_comparison : Format.formatter -> comparison_report -> unit
report_comparison ppf r pretty prints an error message on the
formatter ppf describing the comparison report r.
val compare : Root.t -> Root.t -> comparison_report option
compare sh1 sh2 test wether sh2 is more general than sh1
(i.e. sh2 is a correct implementation of sh1). It returns
None if sh2 is effectively so. Otherwise, it returns Some r
when r is a report "explaining" why sh2 is not more general
than sh1. The current implementation assumes that sh1 and sh2
are solved.
val equivalent : Root.t -> Root.t -> bool
equivalent sh1 sh2 returns a boolean indicating wether the
type schemes sh1 and sh2 are equivalent. The current implementation
assumes that sh1 and sh2 are in solved form.
type minimal_report
A comparison report records an explanation of why a scheme
has no minimal instance.
val report_minimal : Format.formatter -> minimal_report -> unit
report_minimal ppf r pretty prints an error message on the
formatter ppf describing the report r.
val has_minimal_instance : Root.t -> minimal_report option
has_minimal_instance sh tests wether the scheme sh has a minimal
instance. If so, the function returns None. Otherwise, it
returns Some r where r is a value of type minimal_report
"explaining" why sh has no minimal instance. The current
implementation assumes that sh is in solved form.