for review: change typecheck.m to handle type class inference
Fergus Henderson
fjh at cs.mu.OZ.AU
Mon Mar 30 22:18:41 AEST 1998
Hi,
DJ, can you please review this one?
Estimated hours taken: 2
compiler/typecheck.m:
Get type inference working for type classes.
tests/hard_coded/typeclasses/Mmakefile:
tests/hard_coded/typeclasses/inference_test.m:
tests/hard_coded/typeclasses/inference_test.exp:
Add a simple test case for type class inference.
cvs diff -N compiler/typecheck.m tests/hard_coded/typeclasses/Mmakefile tests/hard_coded/typeclasses/inference_test.exp tests/hard_coded/typeclasses/inference_test.m
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.232
diff -u -r1.232 typecheck.m
--- typecheck.m 1998/03/03 17:36:25 1.232
+++ typecheck.m 1998/03/30 11:37:31
@@ -488,13 +488,14 @@
typecheck_check_for_ambiguity(whole_pred, HeadVars,
TypeCheckInfo3, TypeCheckInfo4),
typecheck_info_get_final_info(TypeCheckInfo4, TypeVarSet,
- InferredVarTypes0),
+ InferredVarTypes0, InferredTypeConstraints,
+ ConstraintProofs),
map__optimize(InferredVarTypes0, InferredVarTypes),
ClausesInfo = clauses_info(VarSet, ExplicitVarTypes,
InferredVarTypes, HeadVars, Clauses),
pred_info_set_clauses_info(PredInfo0, ClausesInfo, PredInfo1),
pred_info_set_typevarset(PredInfo1, TypeVarSet, PredInfo2),
- record_class_constraint_proofs(PredInfo2, TypeCheckInfo4,
+ pred_info_set_constraint_proofs(PredInfo2, ConstraintProofs,
PredInfo3),
( Inferring = no ->
PredInfo = PredInfo3,
@@ -503,8 +504,28 @@
map__apply_to_list(HeadVars, InferredVarTypes,
ArgTypes),
pred_info_set_arg_types(PredInfo3, TypeVarSet,
- ArgTypes, PredInfo),
- ( identical_up_to_renaming(ArgTypes0, ArgTypes) ->
+ ArgTypes, PredInfo4),
+ pred_info_get_class_context(PredInfo0,
+ OldTypeConstraints),
+ pred_info_set_class_context(PredInfo4,
+ InferredTypeConstraints, PredInfo),
+ (
+ % if the argument types and the type
+ % constraints are identical up to renaming,
+ % then nothing has changed
+ % (the call to same_length is just an
+ % optimization -- catch the easy cases first)
+ list__same_length(OldTypeConstraints,
+ InferredTypeConstraints),
+ same_structure(OldTypeConstraints,
+ InferredTypeConstraints,
+ ConstrainedTypes0, ConstrainedTypes),
+ list__append(ConstrainedTypes0, ArgTypes0,
+ TypesList0),
+ list__append(ConstrainedTypes, ArgTypes,
+ TypesList),
+ identical_up_to_renaming(TypesList0, TypesList)
+ ->
Changed = no
;
Changed = yes
@@ -522,6 +543,24 @@
)
).
+:- pred same_structure(list(class_constraint)::in, list(class_constraint)::in,
+ list(type)::out, list(type)::out) is semidet.
+
+% check if two sets of type class constraints have the same structure
+% (i.e. they specify the same list of type classes with the same arities)
+% and if so, concatenate the argument types for all the type classes
+% in each set of type class constraints and return them.
+
+same_structure([], [], [], []).
+same_structure([ConstraintA | ConstraintsA], [ConstraintB | ConstraintsB],
+ TypesA, TypesB) :-
+ ConstraintA = constraint(ClassName, ArgTypesA),
+ ConstraintB = constraint(ClassName, ArgTypesB),
+ list__same_length(ArgTypesA, ArgTypesB),
+ same_structure(ConstraintsA, ConstraintsB, TypesA0, TypesB0),
+ list__append(ArgTypesA, TypesA0, TypesA),
+ list__append(ArgTypesB, TypesB0, TypesB).
+
:- pred pred_is_user_defined_equality_pred(pred_info::in, module_info::in)
is semidet.
@@ -2522,15 +2561,22 @@
%-----------------------------------------------------------------------------%
-:- pred typecheck_info_get_final_info(typecheck_info, tvarset, map(var, type)).
-:- mode typecheck_info_get_final_info(in, out, out) is det.
+:- pred typecheck_info_get_final_info(typecheck_info, tvarset, map(var, type),
+ list(class_constraint),
+ map(class_constraint, constraint_proof)).
+:- mode typecheck_info_get_final_info(in, out, out, out, out) is det.
-typecheck_info_get_final_info(TypeCheckInfo, NewTypeVarSet, NewVarTypes) :-
+typecheck_info_get_final_info(TypeCheckInfo, NewTypeVarSet, NewVarTypes,
+ NewTypeConstraints, NewConstraintProofs) :-
typecheck_info_get_type_assign_set(TypeCheckInfo, TypeAssignSet),
( TypeAssignSet = [TypeAssign | _] ->
type_assign_get_typevarset(TypeAssign, OldTypeVarSet),
type_assign_get_var_types(TypeAssign, VarTypes0),
type_assign_get_type_bindings(TypeAssign, TypeBindings),
+ type_assign_get_typeclass_constraints(TypeAssign,
+ TypeConstraints),
+ type_assign_get_constraint_proofs(TypeAssign,
+ ConstraintProofs),
map__keys(VarTypes0, Vars),
expand_types(Vars, TypeBindings, VarTypes0, VarTypes),
@@ -2578,11 +2624,26 @@
copy_type_var_names(TypeVarNames, TSubst, NewTypeVarSet1,
NewTypeVarSet),
%
- % Finally, rename the types to use the new typevarset
- % type variables.
+ % Finally, rename the types and type class constraints
+ % to use the new typevarset type variables.
%
term__apply_variable_renaming_to_list(Types, TSubst, NewTypes),
- map__from_corresponding_lists(Vars, NewTypes, NewVarTypes)
+ map__from_corresponding_lists(Vars, NewTypes, NewVarTypes),
+ list__map(rename_class_constraint(TSubst), TypeConstraints,
+ NewTypeConstraints),
+ ( map__is_empty(ConstraintProofs) ->
+ % optimize simple case
+ NewConstraintProofs = ConstraintProofs
+ ;
+ map__keys(ConstraintProofs, ProofKeysList),
+ map__values(ConstraintProofs, ProofValuesList),
+ list__map(rename_class_constraint(TSubst),
+ ProofKeysList, NewProofKeysList),
+ list__map(rename_constraint_proof(TSubst),
+ ProofValuesList, NewProofValuesList),
+ map__from_corresponding_lists(NewProofKeysList,
+ NewProofValuesList, NewConstraintProofs)
+ )
;
error("internal error in typecheck_info_get_vartypes")
).
@@ -2615,6 +2676,28 @@
),
copy_type_var_names(Rest, TypeSubst, NewTypeVarSet1, NewTypeVarSet).
+:- pred rename_class_constraint(map(tvar, tvar), class_constraint,
+ class_constraint).
+:- mode rename_class_constraint(in, in, out) is det.
+
+% apply a type variable renaming to a class constraint
+
+rename_class_constraint(TSubst, constraint(ClassName, ArgTypes0),
+ constraint(ClassName, ArgTypes)) :-
+ term__apply_variable_renaming_to_list(ArgTypes0, TSubst, ArgTypes).
+
+:- pred rename_constraint_proof(map(tvar, tvar), constraint_proof,
+ constraint_proof).
+:- mode rename_constraint_proof(in, in, out) is det.
+
+% apply a type variable renaming to a class constraint proof
+
+rename_constraint_proof(_TSubst, apply_instance(Instance, Num),
+ apply_instance(Instance, Num)).
+rename_constraint_proof(TSubst, superclass(ClassConstraint0),
+ superclass(ClassConstraint)) :-
+ rename_class_constraint(TSubst, ClassConstraint0, ClassConstraint).
+
%-----------------------------------------------------------------------------%
:- pred typecheck_info_set_type_assign_set(typecheck_info, type_assign_set,
@@ -2824,10 +2907,6 @@
:- pred typecheck_constraints(bool, typecheck_info, typecheck_info).
:- mode typecheck_constraints(in, typecheck_info_di, typecheck_info_uo) is det.
- % XXX if we're inferring, don't bother checking the constraints at this
- % XXX stage. Fix this up. Handling inference isn't actually that
- % XXX difficult: you just collect the constraint set, perform context
- % XXX reduction, and that is the class context of the pred.
typecheck_constraints(yes, TypeCheckInfo, TypeCheckInfo).
typecheck_constraints(no, TypeCheckInfo0, TypeCheckInfo) :-
% get the declared constraints
@@ -3174,27 +3253,6 @@
apply_class_rules_2(NewCs, NewConstraints, ClassTable,
NewTVarSet, Proofs1, Proofs, Constraints, Changed2),
bool__or(Changed1, Changed2, Changed).
-
-%-----------------------------------------------------------------------------%
-
-:- pred record_class_constraint_proofs(pred_info, typecheck_info,
- pred_info).
-:- mode record_class_constraint_proofs(in, typecheck_info_ui, out) is det.
-
-record_class_constraint_proofs(PredInfo0, TypeCheckInfo, PredInfo) :-
- typecheck_info_get_type_assign_set(TypeCheckInfo, TypeAssignSet),
- (
- TypeAssignSet = [TypeAssign]
- ->
- type_assign_get_constraint_proofs(TypeAssign, Proofs),
- pred_info_set_constraint_proofs(PredInfo0, Proofs,
- PredInfo)
- ;
- % If there's not exactly one type_assign, don't
- % bother recording the proofs since an error has
- % occured, and will have been noted elsewhere
- PredInfo = PredInfo0
- ).
%-----------------------------------------------------------------------------%
Index: tests/hard_coded/typeclasses/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/typeclasses/Mmakefile,v
retrieving revision 1.5
diff -u -r1.5 Mmakefile
--- Mmakefile 1998/02/04 03:23:18 1.5
+++ Mmakefile 1998/03/30 11:14:36
@@ -12,6 +12,7 @@
ho_map \
implied_instance \
implied_instance_poly \
+ inference_test \
multi_constraint_diff_tvar \
multi_constraint_same_tvar \
multi_parameter \
@@ -28,11 +29,11 @@
# find exactly how to trigger the bug. Oh well...
# we do not yet pass the following tests:
-# implied_instance
-# implied_instance_poly
# typeclass_test_5.m (this is really a WISHLIST item)
#
-#
+
+
+MCFLAGS-inference_test = --infer-all
#-----------------------------------------------------------------------------#
Index: tests/hard_coded/typeclasses/inference_test.exp
===================================================================
RCS file: inference_test.exp
diff -N inference_test.exp
--- /dev/null Mon Mar 30 22:05:00 1998
+++ inference_test.exp Mon Mar 30 21:55:41 1998
@@ -0,0 +1 @@
+yes
Index: tests/hard_coded/typeclasses/inference_test.m
===================================================================
RCS file: inference_test.m
diff -N inference_test.m
--- /dev/null Mon Mar 30 22:05:00 1998
+++ inference_test.m Mon Mar 30 21:54:59 1998
@@ -0,0 +1,31 @@
+:- module inference_test.
+:- interface.
+:- import_module io.
+
+:- pred main(state::di, state::uo) is det.
+
+:- implementation.
+:- import_module int.
+
+:- typeclass foo(T) where [
+ pred p(T::in, int::out) is det
+].
+
+:- instance foo(int) where [
+ pred(p/2) is forty_two
+].
+
+% :- pred forty_two(int, int) is det.
+:- mode forty_two(in, out) is det.
+forty_two(X, Y) :- Y is X + 42.
+
+main -->
+ ( { q(0) } ->
+ print("yes\n")
+ ;
+ print("no\n")
+ ).
+
+% :- pred q(T) <= foo(T).
+q(X) :- p(X, 42).
+
--
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