A | |
atomic [Dalton_aux.Kind] | atomic k tests whether the kind k is atomic, i.e.
|
B | |
bottom [Dalton_sig.GROUND.Lb] | bottom is a distinguished lower bound.
|
C | |
combine [Dalton_aux.Variance] | combine v1 v2 calculates the combination of two variances.
|
compare [Dalton.Make.Scheme] | compare sh1 sh2 test wether sh2 is more general than sh1
(i.e.
|
compare [Dalton_sig.GROUND.Label] |
A function
compare definining a total order on row labels must
be provided.
|
compare [Dalton_sig.GROUND.Ub] |
A comparison function on constant upper bounds has to be
provided.
|
compare [Dalton_sig.GROUND.Lb] |
A comparison function on constant lower bounds has to be
provided.
|
compatible [Dalton_sig.GROUND.Type] | compatible t1 t2 indicates wether the type constructors
t1 and t2 are compatible.
|
copy [Dalton.Make.SCHEME_ROOT] | copy cset' f sh creates a new scheme sh' as follows: the constraint set of sh' is cset' ,, each root of sh' is obtained by applying f on the
corresponding root of sh .
|
copy [Dalton.Make.Scheme] | copy ?subst sh returns a fresh copy of the type scheme sh.
|
cset [Dalton.Make.SCHEME_ROOT] | cset sh returns the constraint set of the scheme sh .
|
cset [Dalton.Make] |
Each invokation of
cset () returns a new fresh empty constraint
set.
|
cset_begin [Dalton_templates.Print] | |
cset_begin [Dalton_sig.PRINT] | cset_begin ppf is called before printing a constraint set on the
formatter ppf .
|
cset_end [Dalton_templates.Print] | |
cset_end [Dalton_sig.PRINT] | cset_end ppf is called at the end of the printing a constraint set
on the formatter ppf .
|
cset_item [Dalton_templates.Print] | |
cset_item [Dalton_sig.PRINT] |
Every constraint
c of a constraint set is printed on the formatter
ppf by a call of the form cset_item printer ppf c where printer
is a suitable printer for the constraint.
|
cycle [Dalton_templates.ErrorReport] | |
cycle [Dalton_sig.ERROR_REPORT] | cycle ppf variable term prints the explanation of an unification
failure due to the occur-check.
|
D | |
draw [Dalton.Make.Scheme] | draw window sh x y draws the scheme sh on the window window .
|
draw [Dalton_sig.GROUND.Ub] | |
draw [Dalton_sig.GROUND.Lb] | |
draw_curves [Dalton_templates.DrawGraphics] | |
draw_dotted_lines [Dalton_templates.DrawGraphics] | |
draw_dotted_lines [Dalton_sig.DRAW] | |
draw_ellipse [Dalton_templates.DrawGraphics] | |
draw_ellipse [Dalton_sig.DRAW] | |
draw_lines [Dalton_templates.DrawGraphics] | |
draw_lines [Dalton_sig.DRAW] | |
draw_rect [Dalton_templates.DrawGraphics] | |
draw_rect [Dalton_sig.DRAW] | |
draw_text [Dalton_templates.DrawGraphics] | |
draw_text [Dalton_sig.DRAW] | |
E | |
equal [Dalton.Make] | equal nd1 nd2 sets a constraint nd1 = nd2 .
|
equal [Dalton_templates.Print] | |
equal [Dalton_sig.PRINT] | same_skel printer ppf list prints an equality involving elements
of the list list .
|
equivalent [Dalton.Make.Scheme] | equivalent sh1 sh2 returns a boolean indicating wether the
type schemes sh1 and sh2 are equivalent.
|
F | |
fill_ellipse [Dalton_templates.DrawGraphics] | |
fill_ellipse [Dalton_sig.DRAW] | |
fill_poly [Dalton_templates.DrawGraphics] | |
fill_poly [Dalton_sig.DRAW] | |
fill_rect [Dalton_templates.DrawGraphics] | |
fill_rect [Dalton_sig.DRAW] | |
first [Dalton_templates.Print] | |
for_all2 [Dalton_sig.GROUND.Type] |
Given two compatible constructors
t1 and t2 , for_all f t1 t2
tests wether for all pair of sons x1 and x2 , f i x1 x2 is
true .
|
fprint [Dalton.Make.SCHEME_ROOT] | fprint ppf print_cset print_node sh pretty prints the scheme
sh on the formatter ppf .
|
fprint [Dalton.Make.Scheme] | fprint ppf sh pretty-prints the scheme sh on the formatter ppf .
|
fprint [Dalton_sig.GROUND.Type] | fprint ppf skip f t pretty-prints the type constructor t
on the formatter ppf .
|
fprint [Dalton_sig.GROUND.Label] | fprint ppf lbl pretty-prints the row label lbl on the
formatter ppf .
|
fprint [Dalton_sig.GROUND.Ub] | fprint ppf ub pretty-prints the constant upper bound ub on
the formatter ppf .
|
fprint [Dalton_sig.GROUND.Lb] | fprint ppf lb pretty-prints the constant lower bound lb on
the formatter ppf .
|
fprint [Dalton_aux.Variance] | fprint ppf v prints the variance v on the formatter ppf ,
using one of the three symbols "+", "-" and "=".
|
fprint [Dalton_aux.Kind] | fprint ppf k prints the kind k on the formatter ppf .
|
fprint_in_term [Dalton_sig.GROUND.Lub] | fprint_in_term ppf lb ub is used to print a pair of a
lower bound and a upper bound in a term.
|
fprint_in_term [Dalton_sig.GROUND.Ub] | fprint_in_term ppf ub is used to print the constant lower
bound ub on the formatter ppf when it appears in a term, in
place of a non-negative variable which has no predecessor.
|
fprint_in_term [Dalton_sig.GROUND.Lb] | fprint_in_term ppf lb is used to prints the constant lower
bound lb on the formatter ppf when it appears in a term, in
place of a non-negative variable which has no predecessor.
|
fprint_name [Dalton_aux.Variance] | fprint_name ppf v prints the variance v on the formatter ppf ,
using its litteral name (i.e.
|
G | |
geq [Dalton_sig.GROUND.Lub] | geq lb ub returns true if and only if lb is greater than
or equal to ub , i.e.
|
geq [Dalton_sig.GROUND.Ub] | geq lb1 lb2 tells wether lb1 is greater than or equal to
lb2 in the semi-lattice of constant upper bounds.
|
ghost [Dalton_templates.Print] | |
ghost [Dalton_sig.PRINT] |
The string to be printed in place of ghost variables (i.e.
|
H | |
has_minimal_instance [Dalton.Make.Scheme] | has_minimal_instance sh tests wether the scheme sh has a minimal
instance.
|
hash [Dalton_sig.GROUND.Type] | hash t returns a hash integer of the type constructor t which
carries hashes of its sons.
|
hash [Dalton_sig.GROUND.Label] | hash lbl returns a hash integer of the label lbl .
|
I | |
incompatible [Dalton_templates.ErrorReport] | |
incompatible [Dalton_sig.ERROR_REPORT] | cycle ppf ~term1 ~term2 prints the explanation of an unification
failure due to incompatibles type constructors.
|
incompatible_schemes [Dalton_templates.ErrorReport] | |
incompatible_schemes [Dalton_sig.ERROR_REPORT] | incompatible_schemes ppf ~scheme1 ~scheme2 ~explanation reports
that schemes scheme1 and scheme2 are not comparable, because of
an unification error.
|
inequality [Dalton_templates.ErrorReport] | |
inequality [Dalton_sig.ERROR_REPORT] | inequality ppf ~lb ~ub tells that a constraint is not satisfiable
because it implies the incorrect inequality lb < ub between constant
bounds.
|
inter [Dalton_sig.GROUND.Ub] | inter lb1 lb2 gives the intersection (according to the
semi-lattice structure) of the lower bounds lb1 and lb2 .
|
is_bottom [Dalton_sig.GROUND.Lb] | is_bottom lb must return true if and only if lb is bottom .
|
is_top [Dalton_sig.GROUND.Ub] | is_top lb must return true if and only if lb is top .
|
iter [Dalton.Make.SCHEME_ROOT] | iter f sh applies f on every root of sh (with the
variance of the root as first argument).
|
iter [Dalton_sig.GROUND.Type] | iter f t applies f on every son x of t .
|
iter2 [Dalton.Make.SCHEME_ROOT] | iter2 f sh1 sh2 applieas f on every pair of corresponding
roots of sh1 and sh2 (with the variance of the roots as first
argument).
|
iter2 [Dalton_sig.GROUND.Type] |
Given two compatible constructors
t1 and t2 , iter2 f t1 t2
applies f on every pair of corresponding sons of t1 and t2 .
|
L | |
ldestr [Dalton_templates.ErrorReport] | |
ldestr [Dalton_sig.ERROR_REPORT] | ldestr ppf ~term tells that the left-destructor has been applied
on the type term term which cannot be so.
|
ldestr [Dalton_sig.GROUND.Type] | ldestr t returns false if the type t cannot be an argument
of the left destructor.
|
ldestr_inv [Dalton_sig.GROUND.Type] |
The boolean constant
ldestr_inv tells wether there exists a
type constructor for which the left destructor propagates on
an invariant argument.
|
left_destructor [Dalton_templates.Print] | |
left_destructor [Dalton_sig.PRINT] | |
left_destructor_skel [Dalton_templates.Print] | |
left_destructor_skel [Dalton_sig.PRINT] | |
leq [Dalton_templates.Print] | |
leq [Dalton_sig.PRINT] | |
leq [Dalton_sig.GROUND.Lub] | geq lb ub returns true if and only if lb is less than
or equal to ub , i.e.
|
leq [Dalton_sig.GROUND.Lb] | leq env lb1 lb2 tells wether lb1 is less than or equal to
lb2 in the semi-lattice of constant lower bounds, i.e.:
for all alpha, lb2 < alpha implies lb1 < alpha .
|
leq [Dalton_aux.Variance] | leq v1 v2 tests whether the variance v1 is less than or equal to
the variance v2 in the usual order on variance (which is the smallest
order such that Covariant and Contravariant are less than Invariant .
|
lhs [Dalton_templates.Print] | |
lhs [Dalton_sig.PRINT] | lhs printer ppf list prints the left-hand side of an inequality,
consisting in the elements of list the list .
|
lower_bound [Dalton.Make] | lower_bound lb ns sets the weak inequality lb < ns .
|
M | |
map [Dalton_sig.GROUND.Type] | map f t returns the constructor t' obtained by replacing
every son x of t by f i x (where i is the information
of variance, kind and destructor propagation associated to the
argument x in t ).
|
map2 [Dalton_sig.GROUND.Type] |
Given two compatible constructors
t1 and t2 , map2 f t1 t2 ...
|
merge_cset [Dalton.Make] | merge_cset cs1 cs2 merges the two constraint sets cs1 and cs2 .
|
minimal [Dalton_templates.ErrorReport] | |
minimal [Dalton_sig.ERROR_REPORT] | minimal ppf ~scheme ~variablesx prints a message telling that the
type scheme scheme has no minimal instance.
|
missing_bound [Dalton_templates.ErrorReport] | |
missing_bound [Dalton_sig.ERROR_REPORT] | missing_desc ppf ~scheme ~variable ~term reports a comparison failure
due to a missing constant bound.
|
missing_constraint [Dalton_templates.ErrorReport] | |
missing_constraint [Dalton_sig.ERROR_REPORT] | missing_desc ppf ~scheme ~variable ~term reports a comparison failure
due to a missing inequality.
|
missing_desc [Dalton_templates.ErrorReport] | |
missing_desc [Dalton_sig.ERROR_REPORT] | missing_desc ppf ~scheme ~variable ~term reports a comparison failure
due to a variable instatiation.
|
N | |
normalize [Dalton_sig.GROUND.Ub] | normalize lb internally normalizes the lower bound lb.
|
normalize [Dalton_sig.GROUND.Lb] | normalize lb internally normalizes the lower bound lb.
|
P | |
parenthesize [Dalton_sig.GROUND.Type] | parenthesize pos t returns a boolean indication wether the
type constructor t must be parenthesized in context pos .
|
print_list [Dalton_templates.Print] | |
R | |
rdestr [Dalton_templates.ErrorReport] | |
rdestr [Dalton_sig.ERROR_REPORT] | rdestr ppf ~term tells that the right-destructor has been applied
on the type term term which cannot be so.
|
rdestr [Dalton_sig.GROUND.Type] | rdestr t returns false if the type t cannot be an argument
of the right destructor.
|
rdestr_inv [Dalton_sig.GROUND.Type] |
The boolean constant
ldestr_inv tells wether there exists a
type constructor for which the right destructor propagates on
an invariant argument.
|
report_comparison [Dalton.Make.Scheme] | report_comparison ppf r pretty prints an error message on the
formatter ppf describing the comparison report r .
|
report_minimal [Dalton.Make.Scheme] | report_minimal ppf r pretty prints an error message on the
formatter ppf describing the report r .
|
report_solve [Dalton.Make.Scheme] | report_solve ppf r pretty prints an error message on the
formatter ppf corresponding to the comparison report r .
|
report_unification [Dalton.Make] | report_unification ppf r pretty prints an error message on the
formatter ppf describing the unification error reported by r .
|
rhs [Dalton_templates.Print] | |
rhs [Dalton_sig.PRINT] | rhs printer ppf list prints the right-hand side of an inequality,
consisting in the elements of list the list .
|
right_destructor [Dalton_templates.Print] | |
right_destructor [Dalton_sig.PRINT] | |
right_destructor_skel [Dalton_templates.Print] | |
right_destructor_skel [Dalton_sig.PRINT] | |
row [Dalton.Make] | row cs (lbl, nd_lbl, nd') returns a fresh row node representing
the term lbl: nd_lbl, nd' in the constraint set cs .
|
rows [Dalton_aux.Kind] | rows k counts the number of Row in the kind k .
|
S | |
same_skel [Dalton.Make] | same_skel nd1 nd2 sets a constraint nd1 ~ nd2 .
|
same_skel [Dalton_templates.Print] | |
same_skel [Dalton_sig.PRINT] | same_skel printer ppf list prints a same-skeleton constraint
involving elements of the list list .
|
solve [Dalton.Make.Scheme] | solve sh solves the scheme sh .
|
strong_leq [Dalton.Make] | strong_leq nd1 nd2 sets the strong inequality ns1 < ns2 .
|
T | |
text_size [Dalton_templates.DrawGraphics] | |
text_size [Dalton_sig.DRAW] | |
to_string [Dalton_aux.Variance] | to_string v gives a string representation of the variance v .
|
top [Dalton_sig.GROUND.Ub] | top is a distinguished upper bound.
|
typ [Dalton.Make] | typ cs t returns a fresh type term described by the type constructor
t in the constraint set cs .
|
U | |
unification [Dalton_templates.ErrorReport] | |
unification [Dalton_sig.ERROR_REPORT] | unification ppf ~term1 ~term2 ~explanation reports an unification
failure of the terms term1 and term2 .
|
union [Dalton_sig.GROUND.Lb] | union lb1 lb2 gives the union (according to the semi-lattice
structure) of the lower bounds lb1 and lb2 .
|
upper_bound [Dalton.Make] | upper_bound ns ub sets the weak inequality ns < ub .
|
V | |
variable [Dalton.Make] | variable cs k returns a fresh variable term of kind k .
|
variable_in_sk [Dalton.Make] | variable_in_sk nd returns a fresh variable belonging to the same
skeleton (and the same constraint set) as the node nd .
|
W | |
weak_leq [Dalton.Make] | weak_leq ns1 ns2 sets a weak inequality ns1 < ns2 .
|