diff: clean up handling of unbound type variables
Fergus Henderson
fjh at cs.mu.oz.au
Thu Jan 1 19:12:56 AEDT 1998
Clean up the handling of unbound type variables.
Fix a bug with unbound type variables in lambda expressions.
compiler/typecheck.m:
compiler/purity.m:
Move the code for checking for unbound type variables
from typecheck.m to purity.m. It needs to be done
*after* type inference has been completed, so it
can't be done in the ordinary type checking/inference
passes. Add code to purity.m to bind the
unbound type variables to `void'.
compiler/polymorphism.m:
Comment out old code to bind unbound type variables
to `void'; the old code was incomplete, and this
is now done in purity.m.
compiler/notes/compiler_design.html:
Document the above changes.
tests/valid/Mmakefile:
tests/valid/unbound_tvar_in_lambda.m:
Regression test.
cvs diff compiler/notes/compiler_design.html compiler/polymorphism.m compiler/purity.m compiler/typecheck.m tests/valid/Mmakefile tests/valid/unbound_tvar_in_lambda.m
Index: compiler/notes/compiler_design.html
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/notes/compiler_design.html,v
retrieving revision 1.11
diff -u -r1.11 compiler_design.html
--- compiler_design.html 1997/12/22 06:59:04 1.11
+++ compiler_design.html 1998/01/01 06:57:35
@@ -223,7 +223,8 @@
purity.m is responsible for purity checking, as well as
defining the <CODE>purity</CODE> type and a few public
operations on it. It also completes the handling of predicate
- overloading for cases which typecheck.m is unable to handle.
+ overloading for cases which typecheck.m is unable to handle,
+ and checks for unbound type variables.
<dt> mode analysis
Index: compiler/polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.118
diff -u -r1.118 polymorphism.m
--- polymorphism.m 1997/10/14 09:27:53 1.118
+++ polymorphism.m 1998/01/01 07:59:42
@@ -796,7 +796,7 @@
VarTypes = VarTypes0,
TypeInfoMap = TypeInfoMap0
;
- Type = term__variable(TypeVar1)
+ Type = term__variable(_TypeVar1)
->
% This occurs for code where a predicate calls a polymorphic
% predicate with an unbound type variable, for example
@@ -804,7 +804,16 @@
% :- pred p.
% :- pred q(list(T)).
% p :- q([]).
- %
+
+ % this case is now treated as an error;
+ % it should be caught by purity.m.
+ error("polymorphism__make_var: unbound type variable")
+/************
+This is what we used to do... but this didn't handle the case of type
+variables used by lambda expressions properly.
+Binding unbound type variables to `void' is now done in purity.m,
+because it is easier to do it correctly there.
+
% In this case T is unbound, so there cannot be any objects
% of type T, and so q/1 cannot possibly use the unification
% predicate for type T. We pass the type-info for the
@@ -832,6 +841,7 @@
no, ModuleInfo, TypeInfoMap0, VarSet0, VarTypes0,
Var, TypeInfoMap1, ExtraGoals, VarSet, VarTypes),
map__det_insert(TypeInfoMap1, TypeVar1, Var, TypeInfoMap)
+***************/
;
error("polymorphism__make_var: unknown type")
).
Index: compiler/purity.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
retrieving revision 1.2
diff -u -r1.2 purity.m
--- purity.m 1997/12/11 10:31:08 1.2
+++ purity.m 1998/01/01 08:08:02
@@ -6,10 +6,28 @@
%
% File : purity.m
% Authors : pets (Peter Schachte)
-% Purpose : handle `impure' and `promise_pure' declarations
+% Purpose : handle `impure' and `promise_pure' declarations;
+% finish off type checking.
%
-% The purpose of this module is to allow one to declare certain parts of
-% one's program to be impure, thereby forbidding the compiler from making
+% The main purpose of this module is check the consistency of the
+% `impure' and `promise_pure' (etc.) declarations, and to thus report
+% error messages if the program is not "purity-correct".
+%
+% This module also does two final parts of type analysis:
+% - it resolves predicate overloading
+% (perhaps it ought to also resolve function overloading,
+% converting unifications that are function calls into
+% HLDS call instructions, but currently that is still done
+% in modecheck_unify.m)
+% - it checks for unbound type variables and if there are any,
+% it reports an error (or a warning, binding them to the type `void').
+% These actions cannot be done until after type inference is complete,
+% so they need to be a separate "post-typecheck pass"; they are done
+% here in combination with the purity-analysis pass for efficiency reasons.
+%
+%
+% The aim of Mercury's purity system is to allow one to declare certain parts
+% of one's program to be impure, thereby forbidding the compiler from making
% certain optimizations to that part of the code. Since one can often
% implement a perfectly pure predicate or function in terms of impure
% predicates and functions, one is also allowed to promise to the compiler
@@ -217,27 +235,188 @@
NumErrors0, NumErrors) -->
{ module_info_preds(ModuleInfo0, Preds0) },
{ map__lookup(Preds0, PredId, PredInfo0) },
- ( { pred_info_is_imported(PredInfo0)
- ; pred_info_is_pseudo_imported(PredInfo0)} ->
+ (
+ { pred_info_is_imported(PredInfo0)
+ ; pred_info_is_pseudo_imported(PredInfo0) }
+ ->
{ ModuleInfo1 = ModuleInfo0 },
{ NumErrors1 = NumErrors0 }
;
write_pred_progress_message("% Purity-checking ", PredId,
ModuleInfo0),
- puritycheck_pred(PredId, PredInfo0, PredInfo1, ModuleInfo0,
- ErrsInThisPred),
- { map__det_update(Preds0, PredId, PredInfo1, Preds) },
+ check_type_bindings(PredId, PredInfo0, PredInfo1, ModuleInfo0,
+ UnboundTypeErrsInThisPred),
+ puritycheck_pred(PredId, PredInfo1, PredInfo2, ModuleInfo0,
+ PurityErrsInThisPred),
+ { map__det_update(Preds0, PredId, PredInfo2, Preds) },
{ module_info_get_predicate_table(ModuleInfo0, PredTable0) },
{ predicate_table_set_preds(PredTable0, Preds, PredTable) },
{ module_info_set_predicate_table(ModuleInfo0, PredTable,
ModuleInfo1) },
- { NumErrors1 is NumErrors0 + ErrsInThisPred }
+ { NumErrors1 is NumErrors0 + UnboundTypeErrsInThisPred
+ + PurityErrsInThisPred }
),
check_preds_purity_2(PredIds, ModuleInfo1, ModuleInfo,
NumErrors1, NumErrors).
% Purity-check the code for single predicate, reporting any errors.
+
+%-----------------------------------------------------------------------------%
+% Check for unbound type variables
+%
+% Check that the all of the types which have been inferred
+% for the variables in the clause do not contain any unbound type
+% variables other than those that occur in the types of head
+% variables.
+
+:- pred check_type_bindings(pred_id, pred_info, pred_info,
+ module_info, int, io__state, io__state).
+:- mode check_type_bindings(in, in, out, in, out, di, uo) is det.
+
+check_type_bindings(PredId, PredInfo0, PredInfo, ModuleInfo, NumErrors,
+ IOState0, IOState) :-
+ pred_info_clauses_info(PredInfo0, ClausesInfo0),
+ ClausesInfo0 = clauses_info(VarSet, B, VarTypesMap0, HeadVars, E),
+ map__apply_to_list(HeadVars, VarTypesMap0, HeadVarTypes),
+ term__vars_list(HeadVarTypes, HeadVarTypeParams),
+ map__to_assoc_list(VarTypesMap0, VarTypesList),
+ set__init(Set0),
+ check_type_bindings_2(VarTypesList, HeadVarTypeParams,
+ [], Errs, Set0, Set),
+ ( Errs = [] ->
+ PredInfo = PredInfo0,
+ IOState = IOState0,
+ NumErrors = 0
+ ;
+ %
+ % report the warning
+ %
+ report_unresolved_type_warning(Errs, PredId, PredInfo0,
+ ModuleInfo, VarSet, IOState0, IOState),
+ NumErrors = 0,
+
+ %
+ % bind all the type variables in `Set' to `void' ...
+ %
+ pred_info_context(PredInfo0, Context),
+ bind_type_vars_to_void(Set, Context, VarTypesMap0, VarTypesMap),
+ ClausesInfo = clauses_info(VarSet, B, VarTypesMap, HeadVars, E),
+ pred_info_set_clauses_info(PredInfo0, ClausesInfo, PredInfo)
+ ).
+
+:- pred check_type_bindings_2(assoc_list(var, (type)), list(var),
+ assoc_list(var, (type)), assoc_list(var, (type)),
+ set(tvar), set(tvar)).
+:- mode check_type_bindings_2(in, in, in, out, in, out) is det.
+
+check_type_bindings_2([], _, Errs, Errs, Set, Set).
+check_type_bindings_2([Var - Type | VarTypes], HeadTypeParams,
+ Errs0, Errs, Set0, Set) :-
+ term__vars(Type, TVars),
+ set__list_to_set(TVars, TVarsSet0),
+ set__delete_list(TVarsSet0, HeadTypeParams, TVarsSet1),
+ ( \+ set__empty(TVarsSet1) ->
+ Errs1 = [Var - Type | Errs0],
+ set__union(Set0, TVarsSet1, Set1)
+ ;
+ Errs1 = Errs0,
+ Set0 = Set1
+ ),
+ check_type_bindings_2(VarTypes, HeadTypeParams,
+ Errs1, Errs, Set1, Set).
+
+%
+% bind all the type variables in `UnboundTypeVarsSet' to the type `void' ...
+%
+:- pred bind_type_vars_to_void(set(var), term__context,
+ map(var, type), map(var, type)).
+:- mode bind_type_vars_to_void(in, in, in, out) is det.
+
+bind_type_vars_to_void(UnboundTypeVarsSet, Context,
+ VarTypesMap0, VarTypesMap) :-
+ %
+ % first create a pair of corresponding lists (UnboundTypeVars, Voids)
+ % that map the unbound type variables to void
+ %
+ set__to_sorted_list(UnboundTypeVarsSet, UnboundTypeVars),
+ list__length(UnboundTypeVars, Length),
+ Void = term__functor(term__atom("void"), [], Context),
+ list__duplicate(Length, Void, Voids),
+
+ %
+ % then apply the substitution we just created to the variable types
+ %
+ map__keys(VarTypesMap0, Vars),
+ map__values(VarTypesMap0, Types0),
+ term__substitute_corresponding_list(UnboundTypeVars, Voids,
+ Types0, Types),
+ map__from_corresponding_lists(Vars, Types, VarTypesMap).
+
+%
+% report an error: uninstantiated type parameter
+%
+:- pred report_unresolved_type_warning(assoc_list(var, (type)), pred_id,
+ pred_info, module_info, varset, io__state, io__state).
+:- mode report_unresolved_type_warning(in, in, in, in, in, di, uo) is det.
+
+report_unresolved_type_warning(Errs, PredId, PredInfo, ModuleInfo, VarSet) -->
+ globals__io_lookup_bool_option(halt_at_warn, HaltAtWarn),
+ ( { HaltAtWarn = yes } ->
+ io__set_exit_status(1)
+ ;
+ []
+ ),
+
+ { pred_info_typevarset(PredInfo, TypeVarSet) },
+ { pred_info_context(PredInfo, Context) },
+
+ prog_out__write_context(Context),
+ io__write_string("In "),
+ hlds_out__write_pred_id(ModuleInfo, PredId),
+ io__write_string(":\n"),
+
+ prog_out__write_context(Context),
+ io__write_string(" warning: unresolved polymorphism.\n"),
+ prog_out__write_context(Context),
+ ( { Errs = [_] } ->
+ io__write_string(" The variable with an unbound type was:\n")
+ ;
+ io__write_string(" The variables with unbound types were:\n")
+ ),
+ write_type_var_list(Errs, Context, VarSet, TypeVarSet),
+ prog_out__write_context(Context),
+ io__write_string(" The unbound type variable(s) will be implicitly\n"),
+ prog_out__write_context(Context),
+ io__write_string(" bound to the builtin type `void'.\n"),
+ globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
+ ( { VerboseErrors = yes } ->
+ io__write_strings([
+"\tThe body of the clause contains a call to a polymorphic predicate,\n",
+"\tbut I can't determine which version should be called,\n",
+"\tbecause the type variables listed above didn't get bound.\n",
+% "\tYou may need to use an explicit type qualifier.\n",
+% XXX improve error message
+"\t(I ought to tell you which call caused the problem, but I'm afraid\n",
+"\tyou'll have to work it out yourself. My apologies.)\n"
+ ])
+ ;
+ []
+ ).
+
+:- pred write_type_var_list(assoc_list(var, (type)), term__context,
+ varset, tvarset, io__state, io__state).
+:- mode write_type_var_list(in, in, in, in, di, uo) is det.
+
+write_type_var_list([], _, _, _) --> [].
+write_type_var_list([Var - Type | Rest], Context, VarSet, TVarSet) -->
+ prog_out__write_context(Context),
+ io__write_string(" "),
+ mercury_output_var(Var, VarSet, no),
+ io__write_string(" :: "),
+ mercury_output_term(Type, TVarSet, no),
+ io__write_string("\n"),
+ write_type_var_list(Rest, Context, VarSet, TVarSet).
%-----------------------------------------------------------------------------%
% Check purity of a single predicate
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.222
diff -u -r1.222 typecheck.m
--- typecheck.m 1997/12/09 04:01:42 1.222
+++ typecheck.m 1997/12/22 10:54:12
@@ -594,17 +594,8 @@
typecheck_check_for_ambiguity(StuffToCheck, HeadVars,
TypeCheckInfo0, TypeCheckInfo) :-
typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet),
- ( TypeAssignSet = [TypeAssign] ->
- typecheck_info_get_found_error(TypeCheckInfo0, FoundError),
- (
- StuffToCheck = whole_pred,
- FoundError = no
- ->
- check_type_bindings(TypeAssign, HeadVars,
- TypeCheckInfo0, TypeCheckInfo)
- ;
- TypeCheckInfo = TypeCheckInfo0
- )
+ ( TypeAssignSet = [_SingleTypeAssign] ->
+ TypeCheckInfo = TypeCheckInfo0
; TypeAssignSet = [TypeAssign1, TypeAssign2 | _] ->
%
% we only report an ambiguity error if
@@ -662,139 +653,6 @@
error("internal error in typechecker: no type-assignment"),
TypeCheckInfo = TypeCheckInfo0
).
-
- % Check that the all of the types which have been inferred
- % for the variables in the clause do not contain any unbound type
- % variables other than those that occur in the types of head
- % variables.
-
-:- pred check_type_bindings(type_assign, list(var),
- typecheck_info, typecheck_info).
-:- mode check_type_bindings(in, in,
- typecheck_info_di, typecheck_info_uo) is det.
-
-check_type_bindings(TypeAssign, HeadVars, TypeCheckInfo0, TypeCheckInfo) :-
- type_assign_get_type_bindings(TypeAssign, TypeBindings),
- type_assign_get_var_types(TypeAssign, VarTypesMap),
- map__apply_to_list(HeadVars, VarTypesMap, HeadVarTypes0),
- term__apply_rec_substitution_to_list(HeadVarTypes0, TypeBindings,
- HeadVarTypes),
- term__vars_list(HeadVarTypes, HeadVarTypeParams),
- map__to_assoc_list(VarTypesMap, VarTypesList),
- set__init(Set0),
- check_type_bindings_2(VarTypesList, TypeBindings, HeadVarTypeParams,
- [], Errs, Set0, _Set),
- % ... we could at this point bind all the type variables in `Set'
- % to `void' ...
- ( Errs = [] ->
- TypeCheckInfo = TypeCheckInfo0
- ;
- type_assign_get_typevarset(TypeAssign, TVarSet),
- report_unresolved_type_error(Errs, TVarSet, TypeCheckInfo0,
- TypeCheckInfo)
- ).
-
-:- pred check_type_bindings_2(assoc_list(var, (type)), tsubst, headtypes,
- assoc_list(var, (type)), assoc_list(var, (type)),
- set(tvar), set(tvar)).
-:- mode check_type_bindings_2(in, in, in, in, out, in, out) is det.
-
-check_type_bindings_2([], _, _, Errs, Errs, Set, Set).
-check_type_bindings_2([Var - Type0 | VarTypes], TypeBindings, HeadTypeParams,
- Errs0, Errs, Set0, Set) :-
- term__apply_rec_substitution(Type0, TypeBindings, Type),
- term__vars(Type, TVars),
- set__list_to_set(TVars, TVarsSet0),
- set__delete_list(TVarsSet0, HeadTypeParams, TVarsSet1),
- ( \+ set__empty(TVarsSet1) ->
- Errs1 = [Var - Type | Errs0],
- set__union(Set0, TVarsSet1, Set1)
- ;
- Errs1 = Errs0,
- Set0 = Set1
- ),
- check_type_bindings_2(VarTypes, TypeBindings, HeadTypeParams,
- Errs1, Errs, Set1, Set).
-
- % report a warning: uninstantiated type parameter
-
-:- pred report_unresolved_type_error(assoc_list(var, (type)), tvarset,
- typecheck_info, typecheck_info).
-:- mode report_unresolved_type_error(in, in, typecheck_info_di,
- typecheck_info_uo) is det.
-
-report_unresolved_type_error(Errs, TVarSet, TypeCheckInfo0, TypeCheckInfo) :-
- typecheck_info_get_io_state(TypeCheckInfo0, IOState0),
- globals__io_lookup_bool_option(infer_types, Inferring,
- IOState0, IOState1),
- ( Inferring = yes ->
- %
- % If type inferences is enabled, it can result in spurious
- % unresolved type warnings in the early passes; the warnings
- % may be spurious because the types may get resolved in later
- % passes. Unfortunately there's no way to tell which
- % is the last pass until after it is finished...
- % probably these warnings ought to be issued in a different
- % pass than type checking.
- %
- % For the moment, if type inference is enabled, you just don't
- % get these warnings.
- %
- IOState = IOState1
- ;
- report_unresolved_type_error_2(TypeCheckInfo0, Errs, TVarSet,
- IOState1, IOState)
- ),
- typecheck_info_set_io_state(TypeCheckInfo0, IOState, TypeCheckInfo).
- % Currently it is just a warning, not an error.
- % typecheck_info_set_found_error(TypeCheckInfo1, yes, TypeCheckInfo).
-
-:- pred report_unresolved_type_error_2(typecheck_info, assoc_list(var, (type)),
- tvarset, io__state, io__state).
-:- mode report_unresolved_type_error_2(typecheck_info_no_io, in, in, di, uo)
- is det.
-
-report_unresolved_type_error_2(TypeCheckInfo, Errs, TVarSet) -->
- write_typecheck_info_context(TypeCheckInfo),
- { typecheck_info_get_varset(TypeCheckInfo, VarSet) },
- { typecheck_info_get_context(TypeCheckInfo, Context) },
- io__write_string(" warning: unresolved polymorphism.\n"),
- prog_out__write_context(Context),
- ( { Errs = [_] } ->
- io__write_string(" The variable with an unbound type was:\n")
- ;
- io__write_string(" The variables with unbound types were:\n")
- ),
- write_type_var_list(Errs, Context, VarSet, TVarSet),
- prog_out__write_context(Context),
- io__write_string(" The unbound type variable(s) will be implicitly\n"),
- prog_out__write_context(Context),
- io__write_string(" bound to the builtin type `void'.\n"),
- globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
- ( { VerboseErrors = yes } ->
- io__write_string("\tThe body of the clause contains a call to a polymorphic predicate,\n"),
- io__write_string("\tbut I can't determine which version should be called,\n"),
- io__write_string("\tbecause the type variables listed above didn't get bound.\n"),
- % XXX improve error message
- io__write_string("\t(I ought to tell you which call caused the problem, but I'm afraid\n"),
- io__write_string("\tyou'll have to work it out yourself. My apologies.)\n")
- ;
- []
- ).
-
-:- pred write_type_var_list(assoc_list(var, (type)), term__context,
- varset, tvarset, io__state, io__state).
-:- mode write_type_var_list(in, in, in, in, di, uo) is det.
-
-write_type_var_list([], _, _, _) --> [].
-write_type_var_list([Var - Type | Rest], Context, VarSet, TVarSet) -->
- prog_out__write_context(Context),
- io__write_string(" "),
- mercury_output_var(Var, VarSet, no),
- io__write_string(" :: "),
- mercury_output_term(Type, TVarSet, no),
- io__write_string("\n"),
- write_type_var_list(Rest, Context, VarSet, TVarSet).
%-----------------------------------------------------------------------------%
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.4
diff -u -r1.4 Mmakefile
--- Mmakefile 1997/11/24 23:10:37 1.4
+++ Mmakefile 1998/01/01 08:09:43
@@ -77,6 +77,7 @@
type_inf_ambig_test.m \
undead_proc.m \
uniq_unify.m \
+ unbound_tvar_in_lambda.m \
unreachable_code.m \
unused_args_test2.m \
vn_float.m
Index: tests/valid/unbound_tvar_in_lambda.m
===================================================================
RCS file: unbound_tvar_in_lambda.m
diff -N unbound_tvar_in_lambda.m
--- /dev/null Thu Jan 1 19:12:00 1998
+++ unbound_tvar_in_lambda.m Thu Jan 1 19:06:53 1998
@@ -0,0 +1,40 @@
+:- module unbound_tvar_in_lambda.
+:- interface.
+:- import_module io.
+:- pred main(io__state::di, io__state::uo) is det.
+:- implementation.
+:- import_module list, int, std_util, require.
+
+%--------------------------------------------------------%
+
+:- type node(S, T)
+ ---> append(list(S), list(S), list(S)).
+
+:- type proof(N)
+ ---> node(N, proof(N))
+ ; assumed.
+
+:- type proof(S, T) == proof(node(S, T)).
+
+%--------------------------------------------------------%
+
+% Simple polymorphic examples
+
+:- pred append_w(list(S), list(S), list(S), proof(S, T)).
+:- mode append_w(in, in, out, out) is det.
+:- mode append_w(out, out, in, out) is multi.
+
+append_w([], Bs, Bs, node(append([], Bs, Bs), assumed)).
+append_w([A|As], Bs, [A|Cs], node(append([A|As], Bs, [A|Cs]), Proof)) :-
+ append_w(As, Bs, Cs, Proof).
+
+
+%--------------------------------------------------------%
+
+main -->
+ write_string("--- Start Proofs ---\n\n"),
+ { Pred = (pred(P1::out) is nondet :-
+ append_w([1,2,3,4], [5,6,7], _, P1)) },
+ io__write(Pred),
+ write_string("--- End Proofs ---\n\n").
+
--
Fergus Henderson <fjh at cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3 | -- the last words of T. S. Garp.
More information about the developers
mailing list