Index of values


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.