## unify-typoids.pkg
# Compiled by:
# src/lib/compiler/front/typer/typer.sublib# The center of the typechecker is
#
# src/lib/compiler/front/typer/main/type-package-language-g.pkg#
# -- see it for a higher-level overview.
#
# We get called from
#
# src/lib/compiler/front/typer/modules/api-match-g.pkg# src/lib/compiler/front/typer/types/type-core-language-declaration-g.pkg#
# The Hindley-Milner type inference algorithm on which the
# typechecker is based uses Prolog-style logical unification
# to propagate type information to syntax nodes lacking
# explicit programmer-supplied type declarations. (Which is,
# typically, the overwhelming majority of them.)
#
# A light overview of Hindley-Milner type inference may be found here:
# http://en.wikipedia.org/wiki/Type_inference
#
# A more detailed treatment may be found in the
# Types and Programming Languages
# text by Benjamin C Pierce, chapter 22.
#
# In this file we implement the required unification operation.
#
# For unification, our primary analog of a logic variable is
# a type variable set to META_TYPEVAR;
# this represents a totally unconstrained type about which
# we as yet know nothing at all.
#
# Various other type variable values also admit specialization
# during unification to reflect additional knowledge gained.
# For example INCOMPLETE_RECORD_TYPEVAR; values represent
# incompletely specified records ("..." used), which can be
# updated to reflect the complete record definition if we find it.
#
# Unification thus mostly consists of propagating type knowledge
# by setting such type variables to something more specific, perhaps
# a compound type containing more META_TYPEVAR
# type variables to be set in their turn.
#
# The entrypoint into this file is unify_typoids(). It has a
# Void result type since all its work is done via side-effects,
# setting type variables embedded in its type arguments to
# less general (and thus more informative) values.
stipulate
package tdt = type_declaration_types; # type_declaration_types is from src/lib/compiler/front/typer-stuff/types/type-declaration-types.pkgherein
api Unify_Typoids {
# If unification fails we raise
# the exception UNIFY_TYPOIDS with
# a Unify_Fail value to detail
# the exact reason for failure:
#
Unify_Fail
= CIRCULARITY # Cycle in type graph -- type variable loop.
| NEED_EQUALITY_TYPE # Equality type required.
| TYPE_MISMATCH (tdt::Type, tdt::Type) # Type constructor mismatch.
| TYPOID_MISMATCH (tdt::Typoid, tdt::Typoid) # Type mismatch.
| LITERAL_TYPE_MISMATCH tdt::Typevar # Type of literal could not be resolved.
| USER_TYPEVAR_MISMATCH tdt::Typevar # USER_TYPEVAR match
| OVERLOADED_TYPEVAR_MISMATCH # OVERLOADED_TYPEVAR, equality mismatch
| RECORD_FIELD_LABELS_MISMATCH # Record labels did not match.
;
exception UNIFY_TYPOIDS Unify_Fail;
fail_message: Unify_Fail -> String;
unify_typoids:( String, # Name1
String, # Name2
tdt::Typoid, # Type1
tdt::Typoid, # Type2
List(String), # Callstack -- debug support.
Ref (Null_Or( List (Void -> Void ))) # Undo support ("undo_log") Passing undo_log rather than maybe_note_ref_in_undo_log is a value-restriction workaround: undo_log is not polymorphic.
)
-> Void;
debugging: Ref( Bool );
};
end;
stipulate
package em = error_message; # error_message is from src/lib/compiler/front/basics/errormsg/error-message.pkg package pp = standard_prettyprinter; # standard_prettyprinter is from src/lib/prettyprint/big/src/standard-prettyprinter.pkg package pty = prettyprint_type; # prettyprint_type is from src/lib/compiler/front/typer/print/prettyprint-type.pkg package rol = resolve_overloaded_literals; # resolve_overloaded_literals is from src/lib/compiler/front/typer/types/resolve-overloaded-literals.pkg package sy = symbol; # symbol is from src/lib/compiler/front/basics/map/symbol.pkg package syx = symbolmapstack; # symbolmapstack is from src/lib/compiler/front/typer-stuff/symbolmapstack/symbolmapstack.pkg package tdt = type_declaration_types; # type_declaration_types is from src/lib/compiler/front/typer-stuff/types/type-declaration-types.pkg package tj = type_junk; # type_junk is from src/lib/compiler/front/typer-stuff/types/type-junk.pkg package td = typer_debugging; # typer_debugging is from src/lib/compiler/front/typer/main/typer-debugging.pkg package ut = unparse_type; # unparse_type is from src/lib/compiler/front/typer/print/unparse-type.pkgherein
package unify_typoids
: (weak) Unify_Typoids # Unify_Typoids is from src/lib/compiler/front/typer/types/unify-typoids.pkg {
# Type unification.
# debugging = typer_control::unify_typoids_debugging; # REF FALSE
debugging = log::debugging;
stipulate
# Debugging
say = control_print::say;
/* */ fun if_debugging_say (msg: String)
=
if *debugging
say msg;
say "\n";
fi;
/* */ fun bug msg
=
em::impossible("unify_typoids: " + msg);
unparse_typoid
=
ut::unparse_typoid syx::empty;
/* */ fun debug_unparse_typoid (msg, type)
=
td::debug_print debugging (msg, unparse_typoid, type);
/* */ fun debug_unparse_typevar_ref typevar_ref
=
if *debugging # Without this 'if' (and the matching one in type_core_language_declaration_g), compiling the compiler takes 5X as long! :-)
td::with_internals
(\\ () = if_debugging_say (ut::typevar_ref_printname typevar_ref));
fi;
prettyprint_type
=
pty::prettyprint_typoid syx::empty;
/* */ fun debug_pptype (msg, type)
=
td::debug_print debugging (msg, prettyprint_type, type);
herein
Unify_Fail
= CIRCULARITY # Cycle in type graph -- type variable loop.
| NEED_EQUALITY_TYPE # Equality type required.
| TYPE_MISMATCH (tdt::Type, tdt::Type) # Type constructor mismatch.
| TYPOID_MISMATCH (tdt::Typoid, tdt::Typoid) # Type mismatch.
| LITERAL_TYPE_MISMATCH tdt::Typevar # Type of literal could not be resolved.
| USER_TYPEVAR_MISMATCH tdt::Typevar # USER_TYPEVAR match.
| OVERLOADED_TYPEVAR_MISMATCH # OVERLOADED_TYPEVAR, equality mismatch.
| RECORD_FIELD_LABELS_MISMATCH # Record labels did not match.
;
/* */ fun fail_message failure
=
case failure
#
CIRCULARITY => "circularity";
NEED_EQUALITY_TYPE => "equality type required";
TYPE_MISMATCH _ => "type mismatch";
TYPOID_MISMATCH _ => "typoid mismatch";
LITERAL_TYPE_MISMATCH _ => "literal";
USER_TYPEVAR_MISMATCH _ => "USER_TYPEVAR match";
OVERLOADED_TYPEVAR_MISMATCH => "OVERLOADED_TYPEVAR, equality mismatch";
RECORD_FIELD_LABELS_MISMATCH => "record labels";
esac;
exception UNIFY_TYPOIDS Unify_Fail;
########################################################
# Miscellaneous functions:
fun literal_is_equality_kind (lk: tdt::Literal_Kind)
=
TRUE;
# case lk
# (tdt::INT | tdt::UNT | tdt::CHAR | tdt::STRING) => TRUE;
# tdt::FLOAT => FALSE; # FloatAsEqualityType: Changed tdt::FLOAT to be TRUE here in the hope of changing float back to an equality type (2013-12-29 CrT)
# esac;
# Return the equality_property of 'type' for use in determining
# when a TYPCON_TYPE is an equality type.
#
# Note: Calling this function on ERRONEOUS_TYPE produces an impossible
# because an ERRONEOUS_TYPE should never occur in a TYPCON_TYPE
# and hence an equality_property of one of them should never be needed.
#
# Calling this function on a tdt::NAMED_TYPE also produces an impossible because
# the current equality_property scheme is insufficiently expressive to describe
# the possibilities. (Ex: first argument must be an eq type but not
# necessarily the second) Because of this, it is currently necessary to
# expand a tdt::NAMED_TYPE before computing its equality type.
#
fun equality_property_of_type (tdt::SUM_TYPE { is_eqtype, ... } )
=>
case *is_eqtype
#
# tdt::e::EQ_ABSTRACT => tdt::e::NO;
other => other;
esac;
equality_property_of_type (tdt::RECORD_TYPE _ ) => tdt::e::YES;
equality_property_of_type (tdt::NAMED_TYPE _ ) => bug "equality_property_of_type: tdt::NAMED_TYPE";
equality_property_of_type (tdt::ERRONEOUS_TYPE) => bug "equality_property_of_type: ERRONEOUS_TYPE";
equality_property_of_type _ => bug "equality_property_of_type: unexpected type";
end;
# fieldwise (just1, just2, combine, fields1, fields2):
#
# This function merges two sorted lists of (label, type) pairs
# (sorted by label) into a single sorted list of (label, type) pairs.
#
# Our core cases are:
#
# o If (l1, t1) occurs in fields1 but l1 doesn't occur in fields2 then
# (l1, just1 t1) occurs in the output. Similarly with just2.
#
# o If (l, t1) occurs in fields1 and (l, t2) in fields2, then
# (l, combine t1 t2) occurs in the output.
#
fun fieldwise (_, just2, _, [], fields2) => map (\\ (n, t) = (n, just2 t)) fields2;
fieldwise (just1, _, _, fields1, []) => map (\\ (n, t) = (n, just1 t)) fields1;
fieldwise (just1, just2, combine, ((n1, t1) ! r1), ((n2, t2) ! r2))
=>
if (sy::eq (n1, n2))
#
(n1, combine (t1, t2)) ! (fieldwise (just1, just2, combine, r1, r2));
else
if (tj::label_is_greater_than (n2, n1))
#
(n1, just1 t1) ! (fieldwise (just1, just2, combine, r1, ((n2, t2) ! r2)));
else
(n2, just2 t2) ! (fieldwise (just1, just2, combine, ((n1, t1) ! r1), r2));
fi;
fi;
end;
fun sort_vars ( typevar_ref1 as { id => id1, ref_typevar => REF typevar1 },
typevar_ref2 as { id => id2, ref_typevar => REF typevar2 }
)
=
case (typevar1, typevar2)
#
(tdt::LITERAL_TYPEVAR _, _) => (typevar_ref1, typevar_ref2);
(_, tdt::LITERAL_TYPEVAR _) => (typevar_ref2, typevar_ref1);
(tdt::USER_TYPEVAR _, _) => (typevar_ref1, typevar_ref2);
(_, tdt::USER_TYPEVAR _) => (typevar_ref2, typevar_ref1);
(tdt::OVERLOADED_TYPEVAR _, _) => (typevar_ref1, typevar_ref2);
(_, tdt::OVERLOADED_TYPEVAR _) => (typevar_ref2, typevar_ref1);
(tdt::INCOMPLETE_RECORD_TYPEVAR _, _) => (typevar_ref1, typevar_ref2);
(_, tdt::INCOMPLETE_RECORD_TYPEVAR _) => (typevar_ref2, typevar_ref1);
_ => (typevar_ref1, typevar_ref2); # Both tdt::META_TYPEVAR
esac;
#
fun maybe_note_ref_in_undo_log
(
undo_log: Ref (Null_Or(List(Void -> Void))), # When non-NULL, *undo_log accumulates a list of thunks which will undo everything done by do_declaration() call.
ref: Ref(X) # If we're maintaining the undo_log, add an entry to undo uncoming assignment to ref.
)
=
case *undo_log
#
THE log => { oldval = *ref;
#
undo_log := THE ((\\ () = ref := oldval) ! log);
};
NULL => ();
esac;
# Here is the externally visible entrypoint.
# It is mostly just a wrapper for unify_typoids'.
#
# NB: The only side-effects here consist of setting
fun unify_typoids # typevar_ref cells in the type1 and type2 args.
( name1, name2, # Debugging only.
type1, type2,
callstack, # How we got here -- debugging aid only.
undo_log: Ref (Null_Or( List (Void -> Void ))) # Undo support. Passing undo_log rather than maybe_note_ref_in_undo_log is a value-restriction workaround: the former is polymorphic, the latter is not.
)
=
unify_typoids' (name1, name2, type1, type2, callstack)
where
fun unify_typoids' (name1, name2, type1, type2, callstack)
=
{ type1 = tj::drop_resolved_typevars type1; # Reduce tdt::TYPEVAR_REF (REF (tdt::RESOLVED_TYPEVAR type)) to just 'type'.
type2 = tj::drop_resolved_typevars type2; # " ".
if (not *debugging)
#
unify_typoids'' (type1, type2, callstack);
else
# verbose = case (type1, type2)
# #
# (tdt::TYPEVAR_REF _, tdt::TYPEVAR_REF _) => FALSE;
# _ => TRUE;
# esac;
verbose = case callstack
#
"unify_typoids''/TYPOID-TYPOID" ! _ => FALSE; # Suppress display of routine recursive calls to self, to improve signal-to-noise ratio.
_ => TRUE;
esac;
if verbose
if_debugging_say "\n\n============= unify_typoids/TOP ===============";
if_debugging_say "vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv\n";
if_debugging_say ("\nCalled by: " + (string::join " " (reverse callstack)) + "\n");
if_debugging_say "\nunparsed unify_typoids args:\n";
debug_unparse_typoid(name1 + ": ", type1);
debug_unparse_typoid(name2 + ": ", type2);
if_debugging_say "\nprettyprinted unify_typoids args:\n";
debug_pptype(">>unify_typoids: type1: ", type1);
debug_pptype(">>unify_typoids: type2: ", type2);
if_debugging_say "\n";
fi;
unify_typoids'' (type1, type2, callstack);
if verbose
if_debugging_say "\nunify_typoids/bottom unparse of updated type args:\n";
debug_unparse_typoid(name1 + ": ", type1);
debug_unparse_typoid(name2 + ": ", type2);
if_debugging_say "\nunify_typoids/bottom prettyprint of updated type args:\n";
debug_pptype(">>unify_typoids: type1: ", type1);
debug_pptype(">>unify_typoids: type2: ", type2);
if_debugging_say "\n^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^";
if_debugging_say "============= unify_typoids/BOTTOM ===============\n";
fi;
fi;
}
where
# We are about to do
#
# given_typevar_ref := tdt::RESOLVED_TYPEVAR given_typoid;
#
# or something very similar, and before doing
# so we want to propagate any relevant type
# information from the current value of *given_typevar_ref
# into 'given_typoid' by macro-expanding typescheme bodies
# with their type-args to produce plain typoids.
#
# We also want to incorporate into 'given_type'
# our given_fn_nesting and 'given_eq' values,
# by setting
# given_typevar_ref.fn_nesting to minimum of current and given value;
# given_typevar_ref.eq to 'or' of current value and 'given_eq'.
#
# Raise CIRCULARITY if there is a type variable loop.
#
# The only side-effects here are assignments to
# TYPEVAR_REF.ref_typevar refcells in given_typoid.
#
fun expand_typeschemes_and_set_fn_nesting_and_eq_flags
( given_typoid: tdt::Typoid,
given_typevar_ref: tdt::Typevar_Ref,
given_fn_nesting: Int, # Count of enclosing fun/fn lexical scopes.
given_eq: Bool # TRUE if type variable must resolve to an equality type.
)
: Void
=
expand' given_eq given_typoid
where
if_debugging_say "\n\nexpand_typeschemes_and_set_fn_nesting_and_eq_flags: variable ";
debug_unparse_typevar_ref given_typevar_ref;
debug_unparse_typoid (" ==> tdt::RESOLVED_TYPEVAR ", given_typoid);
#
fun expand' this_eq (tdt::TYPEVAR_REF (tv as { id, ref_typevar as REF typevar } ))
=>
case typevar
#
tdt::USER_TYPEVAR { fn_nesting, eq, name }
=>
# Check if eq is compatible and propagate fn_nesting:
#
if (this_eq and not eq) raise exception UNIFY_TYPOIDS NEED_EQUALITY_TYPE;
elif (given_fn_nesting < fn_nesting) maybe_note_ref_in_undo_log (undo_log, ref_typevar);
ref_typevar := tdt::USER_TYPEVAR { fn_nesting => given_fn_nesting, eq, name };
fi;
tdt::META_TYPEVAR { eq, fn_nesting }
=>
# Check for circularity,
# propagate eq and fn_nesting
#
if (tj::same_typevar_ref (given_typevar_ref, tv))
#
raise exception UNIFY_TYPOIDS CIRCULARITY;
else
maybe_note_ref_in_undo_log (undo_log, ref_typevar);
ref_typevar := tdt::META_TYPEVAR
{
fn_nesting => int::min (given_fn_nesting, fn_nesting),
eq => this_eq or eq
};
fi;
tdt::INCOMPLETE_RECORD_TYPEVAR { known_fields, eq, fn_nesting }
=>
# Check for circularity,
# propagate eq and fn_nesting
#
if (tj::same_typevar_ref (given_typevar_ref, tv))
#
raise exception UNIFY_TYPOIDS CIRCULARITY;
else
apply (\\ (field_label: tdt::Label, # Do field types recursively.
field_typoid: tdt::Typoid
)
=
expand_typeschemes_and_set_fn_nesting_and_eq_flags (field_typoid, given_typevar_ref, given_fn_nesting, eq)
)
known_fields;
maybe_note_ref_in_undo_log (undo_log, ref_typevar);
ref_typevar := tdt::INCOMPLETE_RECORD_TYPEVAR
{
fn_nesting => int::min (given_fn_nesting, fn_nesting),
eq => this_eq or eq,
known_fields
};
fi;
tdt::RESOLVED_TYPEVAR type
=>
expand' this_eq type;
tdt::LITERAL_TYPEVAR { kind, ... }
=>
# Check if eq is compatible
#
if (this_eq and not (literal_is_equality_kind kind))
raise exception UNIFY_TYPOIDS NEED_EQUALITY_TYPE;
fi;
tdt::OVERLOADED_TYPEVAR eq'
=>
if (tj::same_typevar_ref (given_typevar_ref, tv)) raise exception UNIFY_TYPOIDS CIRCULARITY;
elif (this_eq and not eq') maybe_note_ref_in_undo_log (undo_log, ref_typevar);
ref_typevar := tdt::OVERLOADED_TYPEVAR this_eq;
fi;
tdt::TYPEVAR_MARK _
=>
bug "unify: expand_typeschemes_and_set_fn_nesting_and_eq_flags: tdt::TYPEVAR_MARK";
esac;
expand' this_eq (type as tdt::TYPCON_TYPOID (tdt::NAMED_TYPE { typescheme, ... }, args))
=>
expand' this_eq (tj::head_reduce_typoid type); # tj::head_reduce_typoid() will call apply_typescheme() which will nondestructively plug 'args' into tdt::NAMED_TYPE.typescheme and return the resulting plain typoid.
expand' this_eq (tdt::TYPCON_TYPOID (type, args))
=>
case (equality_property_of_type type)
#
tdt::e::CHUNK => apply (expand' FALSE ) args;
tdt::e::YES => apply (expand' this_eq) args;
_ => if this_eq raise exception UNIFY_TYPOIDS NEED_EQUALITY_TYPE;
else apply (expand' FALSE) args;
fi;
esac;
expand' _ tdt::WILDCARD_TYPOID
=>
();
# BUG? why don't these cases blow up
# (in equality_property_of_type)
# when expand' is applied to arguments that
# are unreduced applications of tdt::NAMED_TYPE?
# XXX QUERO FIXME
# (Is this answered by the previous comment that
# a tdt::NAMED_TYPE must always be expanded
# before calling equality_property_of_type?)
expand' _ (tdt::TYPESCHEME_TYPOID _) => bug "expand_typeschemes_and_set_fn_nesting_and_eq_flags 1";
expand' _ (tdt::TYPESCHEME_ARG _) => bug "expand_typeschemes_and_set_fn_nesting_and_eq_flags 2";
expand' a b => {
printf "\nexpand' 3: given_eq=%B this_eq=%B *log::debugging=%B" given_eq a *log::debugging;
td::debug_print (REF TRUE) (" this_typoid ", unparse_typoid, b);
td::debug_print (REF TRUE) (" given_typoid ", unparse_typoid, given_typoid);
bug "expand_typeschemes_and_set_fn_nesting_and_eq_flags 3";
};
end;
end;
# Reorder two typevars in descending order according to the ordering
# tdt::LITERAL_TYPEVAR > tdt::USER_TYPEVAR > tdt::OVERLOADED_TYPEVAR > tdt::INCOMPLETE_RECORD_TYPEVAR > tdt::META_TYPEVAR
#
# The real work is unifying type variables.
# Here we handle interactions at the next
# level up, the various settings in which
# type variables are embedded:
fun unify_typoids'' (type1, type2, callstack): Void
=
case ( tj::head_reduce_typoid type1, # Mainly expands tdt::NAMED_TYPE.typescheme entries into plain typoids.
tj::head_reduce_typoid type2 # " ".
)
#
( tdt::TYPEVAR_REF var1,
tdt::TYPEVAR_REF var2
)
=>
unify_typevars (var1, var2); # This is where most of the work gets done.
(tdt::TYPEVAR_REF (var1 as { id, ref_typevar }), etype2)
=>
resolve_typevar (var1, type2, etype2); # E.g. if var1 is tdt::META_TYPEVAR it becomes tdt::RESOLVED_TYPEVAR(type).
(etype1, tdt::TYPEVAR_REF (var2 as { id, ref_typevar }))
=>
resolve_typevar (var2, type1, etype1); # " ".
( t1 as tdt::TYPCON_TYPOID (type1, args1),
t2 as tdt::TYPCON_TYPOID (type2, args2)
)
=>
if (tj::types_are_equal (type1, type2) )
if_debugging_say "--------- unify_typoids''/CONSTRUCTOR recursive calls TOP\n";
if_debugging_say "\nunify_typoids''/TYPCON+TYPCON unparse of typoid args:\n";
debug_unparse_typoid("t1: ", t1);
debug_unparse_typoid("t2: ", t2);
if_debugging_say "\nunify_typoids''/TYPCON+TYPCON prettyprint of typoid args:\n";
debug_pptype("t1: ", t1);
debug_pptype("t2: ", t2);
paired_lists::apply unify (args1, args2)
where
fun unify (type1, type2)
=
unify_typoids'
( "1", "2",
type1, type2,
"unify_typoids''/TYPOID-TYPOID" ! callstack
);
end;
if_debugging_say "--------- unify_typoids''/CONSTRUCTOR recursive calls BOTTOM\n";
else
raise exception UNIFY_TYPOIDS (TYPE_MISMATCH (type1, type2));
fi;
# If one of the types is tdt::WILDCARD_TYPOID, propagate it down into the
# other type to eliminate typevars that might otherwise cause
# generalize_type to complain.
#
(tdt::WILDCARD_TYPOID, tdt::TYPCON_TYPOID(_, args2))
=>
{
if_debugging_say "--------- unify_typoids''/WILD+CONSTRUCTOR recursive calls TOP\n";
apply (\\ x = unify_typoids' ("1", "2", x, tdt::WILDCARD_TYPOID, "unify_typoids''/WILDCARD1" ! callstack))
args2;
if_debugging_say "--------- unify_typoids''/WILD+CONSTRUCTOR recursive calls BOTTOM\n";
};
(tdt::TYPCON_TYPOID(_, args1), tdt::WILDCARD_TYPOID)
=>
{
if_debugging_say "--------- unify_typoids''/CONSTRUCTOR+WILD recursive calls TOP\n";
apply (\\ x = unify_typoids' ("1", "2", x, tdt::WILDCARD_TYPOID, "unify_typoids''/WILDCARD2" ! callstack))
args1;
if_debugging_say "--------- unify_typoids''/CONSTRUCTOR+WILD recursive calls BOTTOM\n";
};
(tdt::WILDCARD_TYPOID, _) => ();
(_, tdt::WILDCARD_TYPOID) => ();
other => raise exception UNIFY_TYPOIDS (TYPOID_MISMATCH other);
esac
also
fun unify_typevars (var1, var2)
=
{ if_debugging_say ">>unify_typevars";
if (not (tj::same_typevar_ref (var1, var2)))
#
unify_typevars' (sort_vars (var1, var2));
fi;
}
where
# Here is the beating heart of the unification logic.
# The essential tranforms are:
#
# tdt::LITERAL_TYPEVAR can resolve with a compatible
# tdt::LITERAL_TYPEVAR or a monotype of its tdt::LITERAL_TYPEVAR ilk.
#
# tdt::USER_TYPEVAR cannot be changed,
# but its fn_nesting can be reduced.
#
# tdt::INCOMPLETE_RECORD_TYPEVAR can merge with another tdt::INCOMPLETE_RECORD_TYPEVAR or resolve with a tdt::META_TYPEVAR.
#
# tdt::META_TYPEVAR can resolve with (i.e., become) anything.
#
# Note that our (typevar_ref1, typevar_ref2) arguments are run
# through sort_vars() before we are called. This reduces the
# number of cases we must consider.
# For example, we can have (tdt::USER_TYPEVAR, tdt::META_TYPEVAR)
# but we can never have (tdt::META_TYPEVAR, tdt::USER_TYPEVAR).
#
fun unify_typevars'
(
typevar_ref1 as { id => id1, ref_typevar => ref_tv1 as REF type1 },
typevar_ref2 as { id => id2, ref_typevar => ref_tv2 as REF type2 }
)
=
# ASSERT: ref_tv1 != ref_tv2
case type1
#
tdt::META_TYPEVAR
{
fn_nesting => fn_nesting1,
eq => eq1
}
=>
case type2
#
tdt::META_TYPEVAR { fn_nesting=>fn_nesting2, eq=>eq2 } # META/META unification. We'll point second to first, and update first with merged fn_nesting and eq info.
=>
{ fn_nesting = int::min (fn_nesting1, fn_nesting2);
eq = eq1 or eq2;
#
maybe_note_ref_in_undo_log (undo_log, ref_tv1);
maybe_note_ref_in_undo_log (undo_log, ref_tv2);
#
ref_tv1 := tdt::META_TYPEVAR { fn_nesting, eq }; # Update first with merged fn_nesting and eq info.
ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1 ); # Point second to first.
};
_ => bug "unify_typevars 3"; # Cannot happen, because typevars are sorted.
esac;
tdt::USER_TYPEVAR { fn_nesting=>fn_nesting1, eq=>eq1, name }
=>
case type2
#
tdt::META_TYPEVAR { eq=>eq2, fn_nesting=>fn_nesting2 } # USER/META unification. We'll point META to USER if fn_nesting and eq info permit.
=>
if (eq1 or (not eq2))
if (fn_nesting2 < fn_nesting1)
maybe_note_ref_in_undo_log (undo_log, ref_tv1);
ref_tv1 := tdt::USER_TYPEVAR { fn_nesting=>fn_nesting2, eq=>eq1, name };
fi;
maybe_note_ref_in_undo_log (undo_log, ref_tv2);
ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1);
else
raise exception UNIFY_TYPOIDS (USER_TYPEVAR_MISMATCH type1);
fi;
_ => {
raise exception UNIFY_TYPOIDS (USER_TYPEVAR_MISMATCH type1); # This case can only be USER-USER, because typevars are sorted,
};
esac;
tdt::INCOMPLETE_RECORD_TYPEVAR { known_fields => known_fields1, fn_nesting => fn_nesting1, eq => eq1 }
=>
case type2
#
tdt::META_TYPEVAR { eq=>eq2, fn_nesting=>fn_nesting2 } # INC/META unification. We'll point second to first, and update first with merged fn_nesting and eq info.
=>
{ fn_nesting = int::min (fn_nesting1, fn_nesting2);
eq = eq1 or eq2;
apply (\\ (l, t) = expand_typeschemes_and_set_fn_nesting_and_eq_flags (t, typevar_ref2, fn_nesting, eq))
known_fields1;
maybe_note_ref_in_undo_log (undo_log, ref_tv1);
maybe_note_ref_in_undo_log (undo_log, ref_tv2);
ref_tv1 := tdt::INCOMPLETE_RECORD_TYPEVAR { known_fields=>known_fields1, fn_nesting, eq };
ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1);
};
tdt::INCOMPLETE_RECORD_TYPEVAR { known_fields=>known_fields2, eq=>eq2, fn_nesting=>fn_nesting2 } # INC/INC unification. We'll point second to first, and update first with merged fieldlist etc.
=>
{ fn_nesting = int::min (fn_nesting1, fn_nesting2);
eq = eq1 or eq2;
apply (\\ (l, t) = expand_typeschemes_and_set_fn_nesting_and_eq_flags (t, typevar_ref1, fn_nesting, eq)) known_fields2;
apply (\\ (l, t) = expand_typeschemes_and_set_fn_nesting_and_eq_flags (t, typevar_ref2, fn_nesting, eq)) known_fields1;
maybe_note_ref_in_undo_log (undo_log, ref_tv1);
maybe_note_ref_in_undo_log (undo_log, ref_tv2);
ref_tv1 := tdt::INCOMPLETE_RECORD_TYPEVAR
{ fn_nesting,
eq,
known_fields => (merge_fields (TRUE, TRUE, known_fields1, known_fields2))
};
ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1);
};
_ => bug "unify_typevars 2"; # Cannot happen, because of typevar sorting.
esac;
tdt::LITERAL_TYPEVAR { kind, source_code_region }
=>
case type2
#
tdt::LITERAL_TYPEVAR { kind=>kind', ... } # LIT/LIT unification. We'll point second to first if kinds match.
=>
if (kind == kind') # Literal_Kind = INT | UNT | FLOAT | CHAR | STRING;
#
maybe_note_ref_in_undo_log (undo_log, ref_tv2);
ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1);
else
raise exception UNIFY_TYPOIDS (LITERAL_TYPE_MISMATCH type1);
fi;
(tdt::META_TYPEVAR { eq=>e2, ... } | tdt::OVERLOADED_TYPEVAR e2) # LIT/META unification. We'll point second to first if equality constraints allow.
=>
if (not e2 or literal_is_equality_kind kind) # Check eq compatibility
#
maybe_note_ref_in_undo_log (undo_log, ref_tv2);
ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1);
else
raise exception UNIFY_TYPOIDS (LITERAL_TYPE_MISMATCH type1);
fi;
_ => raise exception UNIFY_TYPOIDS (LITERAL_TYPE_MISMATCH type1);
esac;
tdt::OVERLOADED_TYPEVAR eq1
=>
case type2
#
tdt::OVERLOADED_TYPEVAR eq2 # OVER/OVER unification. Point one to other, respecting equality constraints.
=>
if (eq1 or not eq2) maybe_note_ref_in_undo_log (undo_log, ref_tv2); ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1);
else maybe_note_ref_in_undo_log (undo_log, ref_tv1); ref_tv1 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref2);
fi;
tdt::META_TYPEVAR { eq=>eq2, fn_nesting=>fn_nesting2 } # OVER/META unification.
=>
if (eq1 or (not eq2))
maybe_note_ref_in_undo_log (undo_log, ref_tv2); ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1);
else maybe_note_ref_in_undo_log (undo_log, ref_tv1); ref_tv1 := tdt::OVERLOADED_TYPEVAR eq2;
maybe_note_ref_in_undo_log (undo_log, ref_tv2); ref_tv2 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref1);
fi;
tdt::INCOMPLETE_RECORD_TYPEVAR { known_fields=>known_fields2, eq=>eq2, fn_nesting=>fn_nesting2 } # OVER/INC unification. We'll point first to second, eq constraints permitting.
=> # Added this case 2014-01-25 because we now have overloaded operations on records (like + on Xyz and Complex).
if (eq2 or not eq1)
#
maybe_note_ref_in_undo_log (undo_log, ref_tv1);
ref_tv1 := tdt::RESOLVED_TYPEVAR (tdt::TYPEVAR_REF typevar_ref2);
else
raise exception UNIFY_TYPOIDS OVERLOADED_TYPEVAR_MISMATCH;
fi;
_ => {
ds = *log::debugging;
is = *log::internals;
log::debugging := TRUE; log::internals := TRUE;
fun typevar_to_string tv
=
case tv
tdt::USER_TYPEVAR _ => "USER_TYPEVAR";
tdt::META_TYPEVAR _ => "META_TYPEVAR";
tdt::INCOMPLETE_RECORD_TYPEVAR _ => "INCOMPLETE_RECORD_TYPEVAR";
tdt::RESOLVED_TYPEVAR _ => "RESOLVED_TYPEVAR";
tdt::OVERLOADED_TYPEVAR _ => "OVERLOADED_TYPEVAR";
tdt::LITERAL_TYPEVAR _ => "LITERAL_TYPEVAR";
tdt::TYPEVAR_MARK _ => "TYPEVAR_MARK";
esac;
ts1= typevar_to_string type1;
ts2= typevar_to_string type2;
pp::with_standard_prettyprinter
#
(em::default_plaint_sink()) []
#
(\\ pp: pp::Prettyprinter
=
{ pp.lit (sprintf "*** Houston, we have a problem. (%s/%s)" ts1 ts2); pp.newline();
pp.lit "Unparsing typevar_ref1:"; pp.newline();
ut::unparse_typevar_ref syx::empty pp typevar_ref1; pp.newline();
pp.lit "Unparsing typevar_ref2:"; pp.newline();
ut::unparse_typevar_ref syx::empty pp typevar_ref2; pp.newline();
pp.lit "Prettyprinting typevar_ref1:"; pp.newline();
pty::prettyprint_typevar_ref syx::empty pp typevar_ref1; pp.newline();
pp.lit "Prettyprinting typevar_ref2:"; pp.newline();
pty::prettyprint_typevar_ref syx::empty pp typevar_ref2; pp.newline();
}
);
log::debugging := ds; log::internals := is;
raise exception UNIFY_TYPOIDS OVERLOADED_TYPEVAR_MISMATCH;
};
esac;
_ => bug "unify_typevars 4";
esac; # fun unify_typevars
end # where
also
fun resolve_typevar
( var as { id, ref_typevar as REF (tdt::META_TYPEVAR { fn_nesting, eq } ) },
type,
ety
)
=>
{ case ety tdt::WILDCARD_TYPOID => ();
_ => expand_typeschemes_and_set_fn_nesting_and_eq_flags (ety, var, fn_nesting, eq);
esac;
maybe_note_ref_in_undo_log (undo_log, ref_typevar);
ref_typevar := tdt::RESOLVED_TYPEVAR type;
};
resolve_typevar (var as { id, ref_typevar as REF (tdt::INCOMPLETE_RECORD_TYPEVAR { known_fields, fn_nesting, eq } ) }, type, ety)
=>
case ety
#
tdt::TYPCON_TYPOID (tdt::RECORD_TYPE field_names, field_typoids)
=>
{ record_fields = paired_lists::zip (field_names, field_typoids);
#
apply (\\ field_typoid = expand_typeschemes_and_set_fn_nesting_and_eq_flags (field_typoid, var, fn_nesting, eq))
field_typoids;
merge_fields (FALSE, TRUE, known_fields, record_fields);
maybe_note_ref_in_undo_log (undo_log, ref_typevar);
ref_typevar := tdt::RESOLVED_TYPEVAR type;
};
tdt::WILDCARD_TYPOID # propagate tdt::WILDCARD_TYPOID to the fields
=>
apply (\\ (lab, type) = unify_typoids' ("1", "2", tdt::WILDCARD_TYPOID, type, ["resolve_typevar"]))
known_fields;
_ => raise exception UNIFY_TYPOIDS (TYPOID_MISMATCH (tdt::TYPEVAR_REF (var), ety));
esac;
resolve_typevar (var as { id, ref_typevar as REF (i as tdt::OVERLOADED_TYPEVAR eq) }, type, ety)
=>
{ expand_typeschemes_and_set_fn_nesting_and_eq_flags (ety, var, tdt::infinity, eq);
#
maybe_note_ref_in_undo_log (undo_log, ref_typevar);
ref_typevar := tdt::RESOLVED_TYPEVAR type;
};
resolve_typevar (var as { id, ref_typevar as REF (i as tdt::LITERAL_TYPEVAR { kind, ... } ) }, type, ety)
=>
case ety
#
tdt::WILDCARD_TYPOID => ();
_ => if (rol::is_literal_typoid (kind, ety))
#
maybe_note_ref_in_undo_log (undo_log, ref_typevar);
ref_typevar := tdt::RESOLVED_TYPEVAR type;
else
raise exception UNIFY_TYPOIDS (LITERAL_TYPE_MISMATCH i); # Should return the type for error msg. XXX SUCKO FIXME
fi;
esac;
resolve_typevar ({ id, ref_typevar as REF (i as tdt::USER_TYPEVAR _) }, _, ety)
=>
case ety
#
tdt::WILDCARD_TYPOID => ();
_ => {
raise exception UNIFY_TYPOIDS (USER_TYPEVAR_MISMATCH i); # Should return the type for error msg. XXX SUCKO FIXME.
};
esac;
resolve_typevar ({ id, ref_typevar as REF (tdt::RESOLVED_TYPEVAR _) }, _, _) => bug "resolve_typevar: tdt::RESOLVED_TYPEVAR";
resolve_typevar ({ id, ref_typevar as REF (tdt::TYPEVAR_MARK _) }, _, _) => bug "resolve_typevar: tdt::TYPEVAR_MARK";
end
# merge_fields (extra1, extra2, fields1, fields2):
#
# This function merges the 2 sorted field lists. Fields occurring
# in both lists have their types unified. If a field occurs in only
# one list, say fields { i } then if extra { i } is TRUE, a unify_typoids
# error is raised.
also
fun merge_fields (extra1, extra2, fields1, fields2)
=
{ fun extra allowed t
=
if allowed t;
else raise exception UNIFY_TYPOIDS RECORD_FIELD_LABELS_MISMATCH;
fi;
fieldwise ( extra extra1,
extra extra2,
(\\ (t1, t2) = { unify_typoids' ("1", "2", t1, t2, ["unify_typoids::merge_fields"]); t1; }),
fields1,
fields2
);
};
end;
end;
end; # stipulate
}; # package unify_typoids
end;