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.