[m-rev.] for review: functional dependencies (2/3)
Mark Brown
mark at cs.mu.OZ.AU
Wed Apr 20 17:23:35 AEST 2005
Index: compiler/modules.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modules.m,v
retrieving revision 1.326
diff -u -r1.326 modules.m
--- compiler/modules.m 12 Apr 2005 07:58:16 -0000 1.326
+++ compiler/modules.m 12 Apr 2005 08:07:52 -0000
@@ -7235,7 +7235,7 @@
item_needs_imports(pragma(_)) = yes.
item_needs_imports(pred_or_func(_, _, _, _, _, _, _, _, _, _, _, _)) = yes.
item_needs_imports(pred_or_func_mode(_, _, _, _, _, _, _)) = yes.
-item_needs_imports(Item @ typeclass(_, _, _, _, _)) =
+item_needs_imports(Item @ typeclass(_, _, _, _, _, _)) =
(
Item ^ tc_class_methods = abstract,
\+ (
@@ -7279,7 +7279,7 @@
% Since these constructors are abstractly exported,
% we won't need the local instance declarations.
%
-include_in_int_file_implementation(typeclass(_, _, _, _, _)).
+include_in_int_file_implementation(typeclass(_, _, _, _, _, _)).
include_in_int_file_implementation(pragma(foreign_import_module(_, _))).
:- pred make_abstract_defn(item::in, short_interface_kind::in, item::out)
@@ -7327,8 +7327,8 @@
).
make_abstract_defn(instance(_, _, _, _, _, _) @ Item0, int2, Item) :-
make_abstract_instance(Item0, Item).
-make_abstract_defn(typeclass(A, B, C, _, E), _,
- typeclass(A, B, C, abstract, E)).
+make_abstract_defn(typeclass(_, _, _, _, _, _) @ Item, _,
+ Item ^ tc_class_methods := abstract).
:- pred make_abstract_unify_compare(item::in, short_interface_kind::in,
item::out) is semidet.
@@ -7516,7 +7516,7 @@
reorderable(inst_defn(_, _, _, _, _) - _).
reorderable(mode_defn(_, _, _, _, _) - _).
reorderable(promise(_, _, _, _) - _).
-reorderable(typeclass(_, _, _, _, _) - _).
+reorderable(typeclass(_, _, _, _, _, _) - _).
reorderable(instance(_, _, _, _, _, _) - _).
% Given a list of items for which chunkable succeeds, we need to keep
@@ -7546,7 +7546,7 @@
chunkable(pred_or_func(_, _, _, _, _, _, _, _, _, _, _, _) - _).
chunkable(pred_or_func_mode(_, _, _, _, _, _, _) - _).
chunkable(promise(_, _, _, _) - _).
-chunkable(typeclass(_, _, _, _, _) - _).
+chunkable(typeclass(_, _, _, _, _, _) - _).
chunkable(instance(_, _, _, _, _, _) - _).
% Given a list of items for which symname_ordered succeeds, we need to keep
Index: compiler/polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.263
diff -u -r1.263 polymorphism.m
--- compiler/polymorphism.m 1 Apr 2005 14:28:59 -0000 1.263
+++ compiler/polymorphism.m 11 Apr 2005 12:32:13 -0000
@@ -1856,7 +1856,7 @@
poly_info_get_constraint_map(!.Info, ConstraintMap),
goal_info_get_goal_path(GoalInfo0, GoalPath),
list__length(ParentUnivConstraints, NumUnivConstraints),
- lookup_hlds_constraint_list(ConstraintMap, universal, GoalPath,
+ lookup_hlds_constraint_list(ConstraintMap, unproven, GoalPath,
NumUnivConstraints, ActualUnivConstraints),
term__apply_rec_substitution_to_list(ParentExistQVarTerms,
ParentToActualTypeSubst, ActualExistQVarTerms),
@@ -1871,7 +1871,7 @@
% quantified typeclass_infos in the call,
% insert them into the typeclass_info map
list__length(ParentExistConstraints, NumExistConstraints),
- lookup_hlds_constraint_list(ConstraintMap, existential,
+ lookup_hlds_constraint_list(ConstraintMap, assumed,
GoalPath, NumExistConstraints, ActualExistConstraints),
polymorphism__make_existq_typeclass_info_vars(
ActualExistConstraints, ExtraExistClassVars,
@@ -2353,14 +2353,12 @@
% Look up the definition of the subclass
module_info_classes(ModuleInfo, ClassTable),
map__lookup(ClassTable, SubClassId, SubClassDefn),
- SubClassDefn = hlds_class_defn(_, SuperClasses0,
- SubClassVars, _, _, _, _),
% Work out which superclass typeclass_info to take.
- map__from_corresponding_lists(SubClassVars, SubClassTypes,
+ map__from_corresponding_lists(SubClassDefn ^ class_vars, SubClassTypes,
SubTypeSubst),
- apply_subst_to_prog_constraint_list(SubTypeSubst, SuperClasses0,
- SuperClasses),
+ apply_subst_to_prog_constraint_list(SubTypeSubst,
+ SubClassDefn ^ class_supers, SuperClasses),
(
list__nth_member_search(SuperClasses, Constraint,
SuperClassIndex0)
Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.125
diff -u -r1.125 prog_data.m
--- compiler/prog_data.m 14 Apr 2005 06:51:00 -0000 1.125
+++ compiler/prog_data.m 17 Apr 2005 16:16:58 -0000
@@ -147,6 +147,7 @@
; typeclass(
tc_constraints :: list(prog_constraint),
+ tc_fundeps :: list(prog_fundep),
tc_class_name :: class_name,
tc_class_params :: list(tvar),
tc_class_methods :: class_interface,
@@ -824,6 +825,7 @@
% expected semantics.
% (This invariant now applies to all types, but is
% especially important here.)
+ %
:- type prog_constraint
---> constraint(
class_name,
@@ -840,6 +842,18 @@
% constraints
).
+ % A functional dependency on the variables in the head of a class
+ % declaration. This asserts that, given the complete set of
+ % instances of this class, the binding of the range variables
+ % can be uniquely determined from the binding of the domain
+ % variables.
+ %
+:- type prog_fundep
+ ---> fundep(
+ domain :: list(tvar),
+ range :: list(tvar)
+ ).
+
:- type class_name == sym_name.
:- type class_id
---> class_id(class_name, arity).
@@ -853,12 +867,14 @@
% that occurs in the body of a type class definition.
% Such declarations may either declare class methods,
% or they may declare modes of class methods.
+ %
:- type class_method
% pred_or_func(...) here represents a `pred ...' or `func ...'
% declaration in a type class body, which declares
% a predicate or function method. Such declarations
% specify the type of the predicate or function,
% and may optionally also specify the mode and determinism.
+ %
---> pred_or_func(
tvarset, % type variables
inst_varset, % inst variables
@@ -881,6 +897,7 @@
% pred_or_func_mode(...) here represents a `mode ...'
% declaration in a type class body. Such a declaration
% declares a mode for one of the type class methods.
+ %
; pred_or_func_mode(
inst_varset, % inst variables
maybe(pred_or_func), % whether the method is a pred
Index: compiler/prog_io_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_typeclass.m,v
retrieving revision 1.37
diff -u -r1.37 prog_io_typeclass.m
--- compiler/prog_io_typeclass.m 6 Apr 2005 10:05:47 -0000 1.37
+++ compiler/prog_io_typeclass.m 6 Apr 2005 10:07:33 -0000
@@ -67,7 +67,7 @@
parse_non_empty_class(ModuleName, Name, Methods, VarSet,
Result)
;
- parse_class_name(ModuleName, Arg, VarSet, Result)
+ parse_class_head(ModuleName, Arg, VarSet, Result)
).
:- pred parse_non_empty_class(module_name::in, term::in, term::in, varset::in,
@@ -78,17 +78,18 @@
parse_class_methods(ModuleName, Methods, VarSet, ParsedMethods),
(
ParsedMethods = ok(MethodList),
- parse_class_name(ModuleName, Name, VarSet, ParsedNameAndVars),
+ parse_class_head(ModuleName, Name, VarSet, ParsedNameAndVars),
(
ParsedNameAndVars = error(String, Term)
->
Result = error(String, Term)
;
- ParsedNameAndVars = ok(typeclass(Constraints,
- NameString, Vars, _, _))
+ ParsedNameAndVars = ok(Item),
+ Item = typeclass(_, _, _, _, _, _)
->
- Result = ok(typeclass(Constraints, NameString, Vars,
- concrete(MethodList), TVarSet))
+ Result = ok((Item
+ ^ tc_class_methods := concrete(MethodList))
+ ^ tc_varset := TVarSet)
;
% if the item we get back isn't a typeclass,
% something has gone wrong...
@@ -99,10 +100,10 @@
Result = error(String, Term)
).
-:- pred parse_class_name(module_name::in, term::in, varset::in,
+:- pred parse_class_head(module_name::in, term::in, varset::in,
maybe1(item)::out) is det.
-parse_class_name(ModuleName, Arg, VarSet, Result) :-
+parse_class_head(ModuleName, Arg, VarSet, Result) :-
(
Arg = term__functor(term__atom("<="), [Name, Constraints], _)
->
@@ -121,34 +122,54 @@
parse_superclass_constraints(ModuleName, Constraints,
ParsedConstraints),
(
- ParsedConstraints = ok(ConstraintList),
+ ParsedConstraints = ok(ConstraintList, FunDeps),
parse_unconstrained_class(ModuleName, Decl, TVarSet, Result0),
(
Result0 = error(_, _)
->
Result = Result0
;
- Result0 = ok(typeclass(_, Name, Vars, Interface,
- VarSet0))
+ Result0 = ok(Item),
+ Item = typeclass(_, _, _, _, _, _)
->
(
%
- % check for type variables in the constraints
+ % Check for type variables in the constraints
% which do not occur in the type class
- % parameters
+ % parameters.
%
prog_type__constraint_list_get_tvars(
ConstraintList, ConstrainedVars),
list__member(Var, ConstrainedVars),
- \+ list__member(Var, Vars)
+ \+ list__member(Var, Item ^ tc_class_params)
->
Result = error("type variable in " ++
"superclass constraint is not " ++
"a parameter of this type class",
Constraints)
;
- Result = ok(typeclass(ConstraintList, Name,
- Vars, Interface, VarSet0))
+ %
+ % Check for type variables in the fundeps
+ % which do not occur in the type class
+ % parameters.
+ %
+ list__member(FunDep, FunDeps),
+ FunDep = fundep(Domain, Range),
+ (
+ list__member(Var, Domain)
+ ;
+ list__member(Var, Range)
+ ),
+ \+ list__member(Var, Item ^ tc_class_params)
+ ->
+ Result = error("type variable in " ++
+ "functional dependency is not " ++
+ "a parameter of this type class",
+ Constraints)
+ ;
+ Result = ok((Item
+ ^ tc_constraints := ConstraintList)
+ ^ tc_fundeps := FunDeps)
)
;
% if the item we get back isn't a typeclass,
@@ -161,12 +182,46 @@
).
:- pred parse_superclass_constraints(module_name::in, term::in,
- maybe1(list(prog_constraint))::out) is det.
+ maybe2(list(prog_constraint), list(prog_fundep))::out) is det.
+
+parse_superclass_constraints(_ModuleName, ConstraintsTerm, Result) :-
+ parse_arbitrary_constraints(ConstraintsTerm, Result0),
+ (
+ Result0 = ok(ArbitraryConstraints),
+ (
+ collect_simple_and_fundep_constraints(
+ ArbitraryConstraints,
+ Constraints, FunDeps)
+ ->
+ Result = ok(Constraints, FunDeps)
+ ;
+ ErrorMessage = "constraints on class declarations" ++
+ " may only constrain type variables and" ++
+ " ground types",
+ Result = error(ErrorMessage, ConstraintsTerm)
+ )
+ ;
+ Result0 = error(String, Term),
+ Result = error(String, Term)
+ ).
-parse_superclass_constraints(ModuleName, Constraints, Result) :-
- parse_simple_class_constraints(ModuleName, Constraints,
- "constraints on class declarations may only constrain " ++
- "type variables and ground types", Result).
+:- pred collect_simple_and_fundep_constraints(list(arbitrary_constraint)::in,
+ list(prog_constraint)::out, list(prog_fundep)::out) is semidet.
+
+collect_simple_and_fundep_constraints([], [], []).
+collect_simple_and_fundep_constraints([Constraint | Constraints],
+ SimpleConstraints, FunDeps) :-
+ collect_simple_and_fundep_constraints(Constraints, SimpleConstraints0,
+ FunDeps0),
+ (
+ Constraint = simple(SimpleConstraint),
+ SimpleConstraints = [SimpleConstraint | SimpleConstraints0],
+ FunDeps = FunDeps0
+ ;
+ Constraint = fundep(FunDep),
+ FunDeps = [FunDep | FunDeps0],
+ SimpleConstraints = SimpleConstraints0
+ ).
:- pred parse_unconstrained_class(module_name::in, term::in, tvarset::in,
maybe1(item)::out) is det.
@@ -183,7 +238,7 @@
list__length(SortedTermVars) =
list__length(TermVars) `with_type` int
->
- Result = ok(typeclass([], ClassName, Vars,
+ Result = ok(typeclass([], [], ClassName, Vars,
abstract, TVarSet))
;
Result = error("expected distinct variables " ++
@@ -294,6 +349,7 @@
(
Result0 = ok(ArbitraryConstraints),
(
+ % Fail if any of the constraints aren't simple.
list.map(get_simple_constraint, ArbitraryConstraints,
Constraints)
->
@@ -315,16 +371,23 @@
parse_arbitrary_constraints(ConstraintsTerm, Result0),
(
Result0 = ok(ArbitraryConstraints),
- collect_class_and_inst_constraints(ArbitraryConstraints,
- ProgConstraints, InstVarSub),
- Result = ok(ProgConstraints, InstVarSub)
+ (
+ collect_class_and_inst_constraints(ArbitraryConstraints,
+ ProgConstraints, InstVarSub)
+ ->
+ Result = ok(ProgConstraints, InstVarSub)
+ ;
+ ErrorMessage = "functional dependencies are only" ++
+ " allowed in typeclass declarations",
+ Result = error(ErrorMessage, ConstraintsTerm)
+ )
;
Result0 = error(Msg, Term),
Result = error(Msg, Term)
).
:- pred collect_class_and_inst_constraints(list(arbitrary_constraint)::in,
- list(prog_constraint)::out, inst_var_sub::out) is det.
+ list(prog_constraint)::out, inst_var_sub::out) is semidet.
collect_class_and_inst_constraints([], [], map.init).
collect_class_and_inst_constraints([Constraint | Constraints],
@@ -354,10 +417,15 @@
% An arbitrary class constraint not matching the
% description of "simple".
- ; inst_constraint(inst_var, inst).
+ ; inst_constraint(inst_var, inst)
% A constraint on an inst variable (that is, one
% whose head is '=<'/2).
+ ; fundep(prog_fundep).
+ % A functional dependency (that is, one whose head
+ % is '->'/2 and whose arguments are comma-separated
+ % variables.
+
:- type arbitrary_constraints == list(arbitrary_constraint).
:- pred parse_arbitrary_constraints(term::in,
@@ -393,6 +461,10 @@
->
Result = ok(inst_constraint(InstVar, Inst))
;
+ parse_fundep(ConstraintTerm, Result0)
+ ->
+ Result = Result0
+ ;
parse_qualified_term(ConstraintTerm, ConstraintTerm,
"class constraint", ok(ClassName, Args0))
->
@@ -420,6 +492,28 @@
Arg1 = term__variable(InstVar0),
term__coerce_var(InstVar0, InstVar),
convert_inst(no_allow_constrained_inst_var, Arg2, Inst).
+
+:- pred parse_fundep(term::in, maybe1(arbitrary_constraint)::out) is semidet.
+
+parse_fundep(Term, Result) :-
+ Term = term__functor(term__atom("->"), [DomainTerm, RangeTerm], _),
+ (
+ parse_fundep_2(DomainTerm, Domain),
+ parse_fundep_2(RangeTerm, Range)
+ ->
+ Result = ok(fundep(fundep(Domain, Range)))
+ ;
+ ErrorMessage = "domain and range of functional dependency" ++
+ " must be comma-separated lists of variables",
+ Result = error(ErrorMessage, Term)
+ ).
+
+:- pred parse_fundep_2(term::in, list(tvar)::out) is semidet.
+
+parse_fundep_2(Term, TVars) :-
+ TypeTerm = term__coerce(Term),
+ conjunction_to_list(TypeTerm, List),
+ term__var_list_to_term_list(TVars, List).
:- pred constraint_is_not_simple(prog_constraint::in) is semidet.
Index: compiler/prog_type.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_type.m,v
retrieving revision 1.3
diff -u -r1.3 prog_type.m
--- compiler/prog_type.m 2 Apr 2005 17:10:01 -0000 1.3
+++ compiler/prog_type.m 13 Apr 2005 09:56:00 -0000
@@ -123,7 +123,7 @@
:- pred constraint_list_get_tvars(list(prog_constraint)::in, list(tvar)::out)
is det.
- % constraint_list_get_tvars(Constraint, TVars):
+ % constraint_get_tvars(Constraint, TVars):
% return the list of type variables contained in a constraint.
%
:- pred constraint_get_tvars(prog_constraint::in, list(tvar)::out) is det.
Index: compiler/recompilation.check.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation.check.m,v
retrieving revision 1.12
diff -u -r1.12 recompilation.check.m
--- compiler/recompilation.check.m 22 Mar 2005 06:40:21 -0000 1.12
+++ compiler/recompilation.check.m 23 Mar 2005 13:42:08 -0000
@@ -915,7 +915,7 @@
check_for_simple_item_ambiguity(NeedQualifier, OldTimestamp,
VersionNumbers, (mode), Name, list__length(Params), _, !Info).
check_for_ambiguities(NeedQualifier, OldTimestamp, VersionNumbers,
- typeclass(_, Name, Params, Interface, _) - _, !Info) :-
+ typeclass(_, _, Name, Params, Interface, _) - _, !Info) :-
check_for_simple_item_ambiguity(NeedQualifier, OldTimestamp,
VersionNumbers, (typeclass), Name, list__length(Params),
NeedsCheck, !Info),
Index: compiler/recompilation.usage.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation.usage.m,v
retrieving revision 1.18
diff -u -r1.18 recompilation.usage.m
--- compiler/recompilation.usage.m 1 Apr 2005 14:29:01 -0000 1.18
+++ compiler/recompilation.usage.m 10 Apr 2005 15:17:36 -0000
@@ -996,8 +996,8 @@
ModuleInfo = !.Info ^ module_info,
module_info_classes(ModuleInfo, Classes),
map__lookup(Classes, ClassId, ClassDefn),
- ClassDefn = hlds_class_defn(_, Constraints, _, ClassInterface,
- _, _, _),
+ Constraints = ClassDefn ^ class_supers,
+ ClassInterface = ClassDefn ^ class_interface,
recompilation__usage__find_items_used_by_class_constraints(
Constraints, !Info),
(
Index: compiler/recompilation.version.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation.version.m,v
retrieving revision 1.17
diff -u -r1.17 recompilation.version.m
--- compiler/recompilation.version.m 7 Apr 2005 06:32:14 -0000 1.17
+++ compiler/recompilation.version.m 7 Apr 2005 06:41:23 -0000
@@ -229,7 +229,7 @@
% Does this pragma match any of the methods
% of this class.
list__member(_ - ClassItem, !.ClassItems),
- ClassItem = typeclass(_, _, _, Interface, _) - _,
+ ClassItem = typeclass(_, _, _, _, Interface, _) - _,
Interface = concrete(Methods),
list__member(Method, Methods),
Method = pred_or_func(_, _, _, MethodPredOrFunc, SymName,
@@ -451,15 +451,12 @@
Section - (PredOrFuncModeItem - ItemContext)
| MatchingItems0]
;
- Item = typeclass(Constraints, ClassName, ClassArgs,
- ClassInterface0, ClassTVarSet),
- ClassInterface0 = concrete(Methods0)
+ Item ^ tc_class_methods = concrete(Methods0)
->
MethodsList = list__map(
split_class_method_types_and_modes, Methods0),
list__condense(MethodsList, Methods),
- TypeclassItem = typeclass(Constraints, ClassName, ClassArgs,
- concrete(Methods), ClassTVarSet),
+ TypeclassItem = Item ^ tc_class_methods := concrete(Methods),
MatchingItems = [Section - (TypeclassItem - ItemContext)
| MatchingItems0]
;
@@ -572,7 +569,7 @@
item_to_item_id_2(pragma(_), no).
item_to_item_id_2(promise(_, _, _, _), no).
item_to_item_id_2(Item, yes(item_id((typeclass), ClassName - ClassArity))) :-
- Item = typeclass(_, ClassName, ClassVars, _, _),
+ Item = typeclass(_, _, ClassName, ClassVars, _, _),
list__length(ClassVars, ClassArity).
% Instances are handled separately (unlike other items, the module
@@ -785,9 +782,11 @@
).
item_is_unchanged(Item1, Item2) = Result :-
- Item1 = typeclass(Constraints, Name, Vars, Interface1, _VarSet),
+ Item1 = typeclass(Constraints, FunDeps, Name, Vars, Interface1,
+ _VarSet),
(
- Item2 = typeclass(Constraints, Name, Vars, Interface2, _),
+ Item2 = typeclass(Constraints, FunDeps, Name, Vars, Interface2,
+ _),
class_interface_is_unchanged(Interface1, Interface2)
->
Result = yes
Index: compiler/type_ctor_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_ctor_info.m,v
retrieving revision 1.63
diff -u -r1.63 type_ctor_info.m
--- compiler/type_ctor_info.m 1 Apr 2005 14:29:02 -0000 1.63
+++ compiler/type_ctor_info.m 2 Apr 2005 10:52:31 -0000
@@ -873,8 +873,7 @@
FirstConstraint = constraint(ClassName, Args),
list__length(Args, ClassArity),
map__lookup(ClassTable, class_id(ClassName, ClassArity), ClassDefn),
- ClassDefn = hlds_class_defn(_, SuperClasses, _, _, _, _, _),
- list__length(SuperClasses, NumSuperClasses),
+ list__length(ClassDefn ^ class_supers, NumSuperClasses),
RealTypeInfoIndex = TypeInfoIndex + NumSuperClasses,
Locn = typeinfo_in_tci(Slot, RealTypeInfoIndex),
map__det_insert(LocnMap0, Tvar, Locn, LocnMap).
Index: compiler/type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.149
diff -u -r1.149 type_util.m
--- compiler/type_util.m 1 Apr 2005 14:29:03 -0000 1.149
+++ compiler/type_util.m 12 Apr 2005 02:35:10 -0000
@@ -1677,10 +1677,14 @@
%-----------------------------------------------------------------------------%
apply_rec_subst_to_constraints(Subst, !Constraints) :-
- !.Constraints = constraints(UnivCs0, ExistCs0),
- apply_rec_subst_to_constraint_list(Subst, UnivCs0, UnivCs),
- apply_rec_subst_to_constraint_list(Subst, ExistCs0, ExistCs),
- !:Constraints = constraints(UnivCs, ExistCs).
+ !.Constraints = constraints(Unproven0, Assumed0, Redundant0),
+ apply_rec_subst_to_constraint_list(Subst, Unproven0, Unproven),
+ apply_rec_subst_to_constraint_list(Subst, Assumed0, Assumed),
+ Pred = (pred(_::in, C0::in, C::out) is det :-
+ apply_rec_subst_to_constraint_list(Subst, C0, C)
+ ),
+ map.map_values(Pred, Redundant0, Redundant),
+ !:Constraints = constraints(Unproven, Assumed, Redundant).
apply_rec_subst_to_constraint_list(Subst, !Constraints) :-
list__map(apply_rec_subst_to_constraint(Subst), !Constraints).
@@ -1690,11 +1694,15 @@
term.apply_rec_substitution_to_list(Types0, Subst, Types),
!:Constraint = constraint(Ids, Name, Types).
-apply_subst_to_constraints(Subst,
- constraints(UniversalCs0, ExistentialCs0),
- constraints(UniversalCs, ExistentialCs)) :-
- apply_subst_to_constraint_list(Subst, UniversalCs0, UniversalCs),
- apply_subst_to_constraint_list(Subst, ExistentialCs0, ExistentialCs).
+apply_subst_to_constraints(Subst, !Constraints) :-
+ !.Constraints = constraints(Unproven0, Assumed0, Redundant0),
+ apply_subst_to_constraint_list(Subst, Unproven0, Unproven),
+ apply_subst_to_constraint_list(Subst, Assumed0, Assumed),
+ Pred = (pred(_::in, C0::in, C::out) is det :-
+ apply_subst_to_constraint_list(Subst, C0, C)
+ ),
+ map.map_values(Pred, Redundant0, Redundant),
+ !:Constraints = constraints(Unproven, Assumed, Redundant).
apply_subst_to_constraint_list(Subst, Constraints0, Constraints) :-
list__map(apply_subst_to_constraint(Subst), Constraints0, Constraints).
@@ -1770,13 +1778,17 @@
term__apply_variable_renaming(Type0, Renaming, Type)
), Map0, Map).
-apply_variable_renaming_to_constraints(Renaming,
- constraints(UniversalCs0, ExistentialCs0),
- constraints(UniversalCs, ExistentialCs)) :-
- apply_variable_renaming_to_constraint_list(Renaming,
- UniversalCs0, UniversalCs),
- apply_variable_renaming_to_constraint_list(Renaming,
- ExistentialCs0, ExistentialCs).
+apply_variable_renaming_to_constraints(Renaming, !Constraints) :-
+ !.Constraints = constraints(Unproven0, Assumed0, Redundant0),
+ apply_variable_renaming_to_constraint_list(Renaming, Unproven0,
+ Unproven),
+ apply_variable_renaming_to_constraint_list(Renaming, Assumed0,
+ Assumed),
+ Pred = (pred(_::in, C0::in, C::out) is det :-
+ apply_variable_renaming_to_constraint_list(Renaming, C0, C)
+ ),
+ map.map_values(Pred, Redundant0, Redundant),
+ !:Constraints = constraints(Unproven, Assumed, Redundant).
apply_variable_renaming_to_constraint_list(Renaming, !Constraints) :-
list__map(apply_variable_renaming_to_constraint(Renaming),
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.369
diff -u -r1.369 typecheck.m
--- compiler/typecheck.m 1 Apr 2005 14:29:03 -0000 1.369
+++ compiler/typecheck.m 20 Apr 2005 04:04:50 -0000
@@ -119,14 +119,14 @@
% Apply context reduction to the list of class constraints by applying
% the instance rules or superclass rules, building up proofs for
- % redundant constraints
+ % redundant constraints.
%
-:- pred typecheck__reduce_context_by_rule_application(instance_table::in,
- superclass_table::in, list(hlds_constraint)::in, tsubst::in,
- tvarset::in, tvarset::out,
+:- pred typecheck__reduce_context_by_rule_application(class_table::in,
+ instance_table::in, superclass_table::in, head_type_params::in,
+ tsubst::in, tsubst::out, tvarset::in, tvarset::out,
constraint_proof_map::in, constraint_proof_map::out,
constraint_map::in, constraint_map::out,
- list(hlds_constraint)::in, list(hlds_constraint)::out) is det.
+ hlds_constraints::in, hlds_constraints::out) is det.
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -433,28 +433,28 @@
Inferring = yes,
write_pred_progress_message("% Inferring type of ",
PredId, !.ModuleInfo, !IO),
- HeadTypeParams1 = [],
+ HeadTypeParams3 = [],
PredConstraints = constraints([], [])
;
Inferring = no,
write_pred_progress_message("% Type-checking ",
PredId, !.ModuleInfo, !IO),
term__vars_list(ArgTypes0, HeadTypeParams0),
- list__delete_elems(HeadTypeParams0, ExistQVars0,
- HeadTypeParams1),
pred_info_get_class_context(!.PredInfo,
- PredConstraints)
+ PredConstraints),
+ constraint_list_get_tvars(
+ PredConstraints ^ univ_constraints, UnivTVars),
+ list__append(UnivTVars, HeadTypeParams0,
+ HeadTypeParams1),
+ list__sort_and_remove_dups(HeadTypeParams1,
+ HeadTypeParams2),
+ list__delete_elems(HeadTypeParams2, ExistQVars0,
+ HeadTypeParams3)
),
- %
- % let the initial constraint set be the
- % dual of the constraints for this pred
- % (anything which we can assume in the caller
- % is something that we must prove in the callee,
- % and vice versa)
- %
- make_hlds_constraints(PredConstraints, [], Constraints),
- dual_constraints(Constraints, DualConstraints),
+ module_info_classes(!.ModuleInfo, ClassTable),
+ make_head_hlds_constraints(ClassTable, TypeVarSet0,
+ PredConstraints, Constraints),
(
pred_info_is_field_access_function(!.ModuleInfo,
!.PredInfo)
@@ -466,8 +466,8 @@
pred_info_get_markers(!.PredInfo, Markers),
typecheck_info_init(!.ModuleInfo, PredId,
IsFieldAccessFunction, TypeVarSet0, VarSet,
- ExplicitVarTypes0, HeadTypeParams1,
- DualConstraints, Status, Markers, Info1),
+ ExplicitVarTypes0, HeadTypeParams3, Constraints,
+ Status, Markers, Info1),
typecheck_info_get_type_assign_set(Info1, OrigTypeAssignSet),
typecheck_clause_list(HeadVars, ArgTypes0,
Clauses1, Clauses, Info1, Info2, !IO),
@@ -477,9 +477,9 @@
!IO),
typecheck_check_for_ambiguity(whole_pred, HeadVars,
Info3, Info4, !IO),
- typecheck_info_get_final_info(Info4, HeadTypeParams1,
+ typecheck_info_get_final_info(Info4, HeadTypeParams3,
ExistQVars0, ExplicitVarTypes0, TypeVarSet,
- HeadTypeParams2, InferredVarTypes0,
+ HeadTypeParams4, InferredVarTypes0,
InferredTypeConstraints0, ConstraintProofs,
ConstraintMap, TVarRenaming, ExistTypeRenaming),
map__optimize(InferredVarTypes0, InferredVarTypes),
@@ -538,7 +538,7 @@
% types must be existentially quantified
%
infer_existential_types(ArgTypeVars, ExistQVars,
- HeadTypeParams2, HeadTypeParams),
+ HeadTypeParams4, HeadTypeParams),
%
% Now save the information we inferred in the pred_info
@@ -570,7 +570,7 @@
)
;
Inferring = no,
- pred_info_set_head_type_params(HeadTypeParams2,
+ pred_info_set_head_type_params(HeadTypeParams4,
!PredInfo),
pred_info_get_origin(!.PredInfo, Origin0),
@@ -1475,8 +1475,9 @@
varset__init(TypeVarSet0),
varset__new_vars(TypeVarSet0, NumVars, TypeVars, TypeVarSet),
term__var_list_to_term_list(TypeVars, Types),
+ empty_hlds_constraints(EmptyConstraints),
typecheck_var_has_polymorphic_type_list(Vars, TypeVarSet, [],
- Types, constraints([], []), !Info, !IO)
+ Types, EmptyConstraints, !Info, !IO)
).
%-----------------------------------------------------------------------------%
@@ -1491,11 +1492,11 @@
TypeVarSet, PredVarType, ArgTypes),
% The class context is empty because higher-order predicates
% are always monomorphic. Similarly for ExistQVars.
- ClassContext = constraints([], []),
+ empty_hlds_constraints(EmptyConstraints),
ExistQVars = [],
typecheck_var_has_polymorphic_type_list([PredVar | Args], TypeVarSet,
- ExistQVars, [PredVarType | ArgTypes], ClassContext, !Info,
- !IO).
+ ExistQVars, [PredVarType | ArgTypes], EmptyConstraints,
+ !Info, !IO).
:- pred higher_order_pred_type(purity::in, int::in, lambda_eval_method::in,
tvarset::out, (type)::out, list(type)::out) is det.
@@ -1752,6 +1753,7 @@
typecheck_call_pred_id_adjust_arg_types(PredId, Args, GoalPath, AdjustArgTypes,
!Info, !IO) :-
typecheck_info_get_module_info(!.Info, ModuleInfo),
+ module_info_classes(ModuleInfo, ClassTable),
module_info_get_predicate_table(ModuleInfo, PredicateTable),
predicate_table_get_preds(PredicateTable, Preds),
map__lookup(Preds, PredId, PredInfo),
@@ -1771,11 +1773,11 @@
->
typecheck_var_has_type_list(Args, PredArgTypes, 1, !Info, !IO)
;
- make_hlds_constraints(PredClassContext, GoalPath,
- HLDSClassContext),
+ make_body_hlds_constraints(ClassTable, PredTypeVarSet,
+ GoalPath, PredClassContext, PredConstraints),
typecheck_var_has_polymorphic_type_list(Args, PredTypeVarSet,
- PredExistQVars, PredArgTypes, HLDSClassContext, !Info,
- !IO)
+ PredExistQVars, PredArgTypes, PredConstraints,
+ !Info, !IO)
).
:- pred report_pred_call_error(simple_call_id::in,
@@ -1832,10 +1834,11 @@
% suitable renamed apart.
%
typecheck_info_get_module_info(!.Info, ModuleInfo),
+ module_info_classes(ModuleInfo, ClassTable),
module_info_get_predicate_table(ModuleInfo, PredicateTable),
predicate_table_get_preds(PredicateTable, Preds),
typecheck_info_get_type_assign_set(!.Info, TypeAssignSet0),
- get_overloaded_pred_arg_types(PredIdList, Preds, GoalPath,
+ get_overloaded_pred_arg_types(PredIdList, Preds, ClassTable, GoalPath,
AdjustArgTypes, TypeAssignSet0, [], ArgsTypeAssignSet),
%
% Then unify the types of the call arguments with the
@@ -1845,24 +1848,26 @@
!IO).
:- pred get_overloaded_pred_arg_types(list(pred_id)::in, pred_table::in,
- goal_path::in, adjust_arg_types::in(adjust_arg_types),
+ class_table::in, goal_path::in, adjust_arg_types::in(adjust_arg_types),
type_assign_set::in,
args_type_assign_set::in, args_type_assign_set::out) is det.
-get_overloaded_pred_arg_types([], _Preds, _GoalPath, _AdjustArgTypes,
- _TypeAssignSet0, !ArgsTypeAssignSet).
-get_overloaded_pred_arg_types([PredId | PredIds], Preds, GoalPath,
+get_overloaded_pred_arg_types([], _Preds, _ClassTable, _GoalPath,
+ _AdjustArgTypes, _TypeAssignSet0, !ArgsTypeAssignSet).
+get_overloaded_pred_arg_types([PredId | PredIds], Preds, ClassTable, GoalPath,
AdjustArgTypes, TypeAssignSet0, !ArgsTypeAssignSet) :-
map__lookup(Preds, PredId, PredInfo),
pred_info_arg_types(PredInfo, PredTypeVarSet, PredExistQVars,
PredArgTypes0),
call(AdjustArgTypes, PredArgTypes0, PredArgTypes),
pred_info_get_class_context(PredInfo, PredClassContext),
- make_hlds_constraints(PredClassContext, GoalPath, HLDSConstraints),
+ pred_info_typevarset(PredInfo, TVarSet),
+ make_body_hlds_constraints(ClassTable, TVarSet, GoalPath,
+ PredClassContext, PredConstraints),
rename_apart(TypeAssignSet0, PredTypeVarSet, PredExistQVars,
- PredArgTypes, HLDSConstraints, !ArgsTypeAssignSet),
- get_overloaded_pred_arg_types(PredIds, Preds, GoalPath, AdjustArgTypes,
- TypeAssignSet0, !ArgsTypeAssignSet).
+ PredArgTypes, PredConstraints, !ArgsTypeAssignSet),
+ get_overloaded_pred_arg_types(PredIds, Preds, ClassTable, GoalPath,
+ AdjustArgTypes, TypeAssignSet0, !ArgsTypeAssignSet).
%-----------------------------------------------------------------------------%
@@ -1957,10 +1962,10 @@
typecheck_info::in, typecheck_info::out, io::di, io::uo) is det.
typecheck_var_has_polymorphic_type_list(Args, PredTypeVarSet, PredExistQVars,
- PredArgTypes, PredClassConstraints, !Info, !IO) :-
+ PredArgTypes, PredConstraints, !Info, !IO) :-
typecheck_info_get_type_assign_set(!.Info, TypeAssignSet0),
rename_apart(TypeAssignSet0, PredTypeVarSet, PredExistQVars,
- PredArgTypes, PredClassConstraints, [], ArgsTypeAssignSet),
+ PredArgTypes, PredConstraints, [], ArgsTypeAssignSet),
typecheck_var_has_arg_type_list(Args, 1, ArgsTypeAssignSet, !Info,
!IO).
@@ -1969,15 +1974,16 @@
args_type_assign_set::in, args_type_assign_set::out) is det.
rename_apart([], _, _, _, _, !ArgTypeAssigns).
-rename_apart([TypeAssign0 | TypeAssigns0], PredTypeVarSet, PredExistQVars0,
- PredArgTypes0, HLDSConstraints0, !ArgTypeAssigns) :-
+rename_apart([TypeAssign0 | TypeAssigns0], PredTypeVarSet, PredExistQVars,
+ PredArgTypes, PredConstraints, !ArgTypeAssigns) :-
%
% rename everything apart
%
- type_assign_rename_apart(TypeAssign0, PredTypeVarSet, PredArgTypes0,
- TypeAssign1, PredArgTypes, Subst),
- apply_substitution_to_var_list(PredExistQVars0, Subst, PredExistQVars),
- apply_subst_to_constraints(Subst, HLDSConstraints0, HLDSConstraints),
+ type_assign_rename_apart(TypeAssign0, PredTypeVarSet, PredArgTypes,
+ TypeAssign1, ParentArgTypes, Subst),
+ apply_substitution_to_var_list(PredExistQVars, Subst,
+ ParentExistQVars),
+ apply_subst_to_constraints(Subst, PredConstraints, ParentConstraints),
%
% insert the existentially quantified type variables for the called
@@ -1985,27 +1991,27 @@
% variables which the caller is not allowed to bind).
%
type_assign_get_head_type_params(TypeAssign1, HeadTypeParams0),
- list__append(PredExistQVars, HeadTypeParams0, HeadTypeParams),
+ list__append(ParentExistQVars, HeadTypeParams0, HeadTypeParams),
type_assign_set_head_type_params(HeadTypeParams,
TypeAssign1, TypeAssign),
%
% save the results and recurse
%
- NewArgTypeAssign = args(TypeAssign, PredArgTypes, HLDSConstraints),
+ NewArgTypeAssign = args(TypeAssign, ParentArgTypes, ParentConstraints),
!:ArgTypeAssigns = [NewArgTypeAssign | !.ArgTypeAssigns],
- rename_apart(TypeAssigns0, PredTypeVarSet, PredExistQVars0,
- PredArgTypes0, HLDSConstraints0, !ArgTypeAssigns).
+ rename_apart(TypeAssigns0, PredTypeVarSet, PredExistQVars,
+ PredArgTypes, PredConstraints, !ArgTypeAssigns).
:- pred type_assign_rename_apart(type_assign::in, tvarset::in, list(type)::in,
type_assign::out, list(type)::out, tsubst::out) is det.
-type_assign_rename_apart(TypeAssign0, PredTypeVarSet, PredArgTypes0,
- TypeAssign, PredArgTypes, Subst) :-
+type_assign_rename_apart(TypeAssign0, PredTypeVarSet, PredArgTypes,
+ TypeAssign, ParentArgTypes, Subst) :-
type_assign_get_typevarset(TypeAssign0, TypeVarSet0),
varset__merge_subst(TypeVarSet0, PredTypeVarSet, TypeVarSet,
Subst),
- term__apply_substitution_to_list(PredArgTypes0, Subst,
- PredArgTypes),
+ term__apply_substitution_to_list(PredArgTypes, Subst,
+ ParentArgTypes),
type_assign_set_typevarset(TypeVarSet, TypeAssign0, TypeAssign).
%-----------------------------------------------------------------------------%
@@ -2065,7 +2071,7 @@
type_assign_get_typeclass_constraints(TypeAssign0, OldConstraints),
type_assign_get_type_bindings(TypeAssign0, Bindings),
apply_rec_subst_to_constraints(Bindings, Constraints0, Constraints),
- add_constraints(OldConstraints, Constraints, NewConstraints),
+ merge_hlds_constraints(Constraints, OldConstraints, NewConstraints),
type_assign_set_typeclass_constraints(NewConstraints,
TypeAssign0, TypeAssign).
@@ -2254,8 +2260,6 @@
ArgTypeStuffs = [ArgTypeStuff | TailArgTypeStuffs]
).
-:- type headtypes == list(tvar).
-
:- pred typecheck_var_has_type_2(type_assign_set::in, prog_var::in, (type)::in,
type_assign_set::in, type_assign_set::out) is det.
@@ -2545,11 +2549,13 @@
:- type args_type_assign
---> args(
caller_arg_assign :: type_assign,
- % Type assignment,
+ % Type assignment.
callee_arg_types :: list(type),
- % types of callee args,
+ % Types of callee args,
+ % renamed apart.
callee_constraints :: hlds_constraints
- % constraints from callee
+ % Constraints from callee,
+ % renamed apart.
).
:- func get_caller_arg_assign(args_type_assign) = type_assign.
@@ -2736,9 +2742,10 @@
% The constraints are empty here because
% none are added by unification with a
% functor.
- Constraints = constraints([], []),
+ %
+ empty_hlds_constraints(EmptyConstraints),
ArgsTypeAssign = args(TypeAssign2, ArgTypes,
- Constraints),
+ EmptyConstraints),
!:TypeAssignSet = [ArgsTypeAssign | !.TypeAssignSet]
;
true
@@ -2747,10 +2754,11 @@
% The constraints are empty here because
% none are added by unification with a
% functor.
+ %
map__det_insert(VarTypes0, Y, ConsType, VarTypes),
type_assign_set_var_types(VarTypes, TypeAssign1, TypeAssign3),
- Constraints = constraints([], []),
- ArgsTypeAssign = args(TypeAssign3, ArgTypes, Constraints),
+ empty_hlds_constraints(EmptyConstraints),
+ ArgsTypeAssign = args(TypeAssign3, ArgTypes, EmptyConstraints),
!:TypeAssignSet = [ArgsTypeAssign | !.TypeAssignSet]
).
@@ -2806,30 +2814,11 @@
% be used as deconstructors rather than as constructors.
%
type_assign_get_typeclass_constraints(TypeAssign2, OldConstraints),
- add_constraints(OldConstraints, ConstraintsToAdd, ClassConstraints),
+ merge_hlds_constraints(ConstraintsToAdd, OldConstraints,
+ ClassConstraints),
type_assign_set_typeclass_constraints(ClassConstraints, TypeAssign2,
TypeAssign).
- % Compute the dual of a set of constraints: anything which
- % we can assume in the caller is something that we must prove
- % in the callee, and vice versa.
- %
-:- pred dual_constraints(hlds_constraints::in, hlds_constraints::out) is det.
-
-dual_constraints(constraints(Univs, Exists), constraints(Exists, Univs)).
-
- % Add the specified constraints to the current constraint set.
- %
-:- pred add_constraints(hlds_constraints::in, hlds_constraints::in,
- hlds_constraints::out) is det.
-
-add_constraints(Constraints0, CsToAdd, Constraints) :-
- Constraints0 = constraints(UnivCs0, ExistCs0),
- CsToAdd = constraints(UnivCsToAdd, ExistCsToAdd),
- list__append(UnivCsToAdd, UnivCs0, UnivCs),
- list__append(ExistCsToAdd, ExistCs0, ExistCs),
- Constraints = constraints(UnivCs, ExistCs).
-
:- pred apply_substitution_to_var_list(list(var(T))::in, map(var(T),
term(T))::in, list(var(T))::out) is det.
@@ -3011,12 +3000,14 @@
int::in, goal_path::in,
list(cons_type_info)::in, list(cons_type_info)::out) is det.
-make_pred_cons_info(_Info, PredId, PredTable, FuncArity, GoalPath,
+make_pred_cons_info(Info, PredId, PredTable, FuncArity, GoalPath,
!ConsInfos) :-
+ typecheck_info_get_module_info(Info, ModuleInfo),
+ module_info_classes(ModuleInfo, ClassTable),
map__lookup(PredTable, PredId, PredInfo),
PredArity = pred_info_orig_arity(PredInfo),
IsPredOrFunc = pred_info_is_pred_or_func(PredInfo),
- pred_info_get_class_context(PredInfo, ClassContext),
+ pred_info_get_class_context(PredInfo, PredClassContext),
pred_info_arg_types(PredInfo, PredTypeVarSet, PredExistQVars,
CompleteArgTypes),
pred_info_get_purity(PredInfo, Purity),
@@ -3034,11 +3025,11 @@
->
construct_higher_order_pred_type(Purity, normal,
PredTypeParams, PredType),
- make_hlds_constraints(ClassContext, GoalPath,
- HLDSContext),
+ make_body_hlds_constraints(ClassTable, PredTypeVarSet,
+ GoalPath, PredClassContext, PredConstraints),
ConsInfo = cons_type_info(PredTypeVarSet,
PredExistQVars, PredType, ArgTypes,
- HLDSContext),
+ PredConstraints),
!:ConsInfos = [ConsInfo | !.ConsInfos],
% If the predicate has an Aditi marker,
@@ -3052,7 +3043,7 @@
PredType2),
ConsInfo2 = cons_type_info(PredTypeVarSet,
PredExistQVars, PredType2,
- ArgTypes, HLDSContext),
+ ArgTypes, PredConstraints),
!:ConsInfos = [ConsInfo2 | !.ConsInfos]
;
true
@@ -3083,11 +3074,11 @@
normal, FuncArgTypeParams,
FuncReturnTypeParam, FuncType)
),
- make_hlds_constraints(ClassContext, GoalPath,
- HLDSContext),
+ make_body_hlds_constraints(ClassTable, PredTypeVarSet,
+ GoalPath, PredClassContext, PredConstraints),
ConsInfo = cons_type_info(PredTypeVarSet,
PredExistQVars, FuncType, FuncArgTypes,
- HLDSContext),
+ PredConstraints),
!:ConsInfos = [ConsInfo | !.ConsInfos]
;
error("make_pred_cons_info: split_list failed")
@@ -3118,9 +3109,9 @@
higher_order_func_type(Purity, Arity1, normal, TypeVarSet, FuncType,
ArgTypes, RetType),
ExistQVars = [],
- Constraints = constraints([], []),
+ empty_hlds_constraints(EmptyConstraints),
ConsTypeInfos = [cons_type_info(TypeVarSet, ExistQVars, RetType,
- [FuncType | ArgTypes], Constraints)].
+ [FuncType | ArgTypes], EmptyConstraints)].
% builtin_field_access_function_type(Info, GoalPath, Functor,
% Arity, ConsTypeInfos):
@@ -3158,11 +3149,14 @@
make_field_access_function_cons_type_info(Info, GoalPath, FuncName, Arity,
AccessType, FieldName, FieldDefn, ConsTypeInfo) :-
get_field_access_constructor(Info, GoalPath, FuncName, Arity,
- AccessType, FieldDefn, MaybeFunctorConsTypeInfo),
+ AccessType, FieldDefn, OrigExistTVars,
+ MaybeFunctorConsTypeInfo),
(
MaybeFunctorConsTypeInfo = ok(FunctorConsTypeInfo),
- convert_field_access_cons_type_info(AccessType, FieldName,
- FieldDefn, FunctorConsTypeInfo, ConsTypeInfo)
+ module_info_classes(Info ^ module_info, ClassTable),
+ convert_field_access_cons_type_info(ClassTable, AccessType,
+ FieldName, FieldDefn, FunctorConsTypeInfo,
+ OrigExistTVars, ConsTypeInfo)
;
MaybeFunctorConsTypeInfo = error(_),
ConsTypeInfo = MaybeFunctorConsTypeInfo
@@ -3170,10 +3164,11 @@
:- pred get_field_access_constructor(typecheck_info::in, goal_path::in,
sym_name::in, arity::in, field_access_type::in,
- hlds_ctor_field_defn::in, maybe_cons_type_info::out) is semidet.
+ hlds_ctor_field_defn::in, existq_tvars::out, maybe_cons_type_info::out)
+ is semidet.
-get_field_access_constructor(Info, GoalPath, FuncName, Arity, _AccessType,
- FieldDefn, FunctorConsTypeInfo) :-
+get_field_access_constructor(Info, GoalPath, FuncName, Arity, AccessType,
+ FieldDefn, OrigExistTVars, FunctorConsTypeInfo) :-
FieldDefn = hlds_ctor_field_defn(_, _, TypeCtor, ConsId, _),
TypeCtor = qualified(TypeModule, _) - _,
@@ -3201,7 +3196,16 @@
TypeCtor = CtorDefn ^ cons_type_ctor
), ConsDefns0, ConsDefns),
ConsDefns = [ConsDefn],
- convert_cons_defn(Info, GoalPath, ConsDefn, FunctorConsTypeInfo).
+ (
+ AccessType = get,
+ ConsAction = do_not_flip_constraints
+ ;
+ AccessType = set,
+ ConsAction = flip_constraints_for_field_set
+ ),
+ OrigExistTVars = ConsDefn ^ cons_exist_tvars,
+ convert_cons_defn(Info, GoalPath, ConsAction, ConsDefn,
+ FunctorConsTypeInfo).
:- type maybe_cons_type_info
---> ok(cons_type_info)
@@ -3211,14 +3215,17 @@
---> foreign_type_constructor(type_ctor, hlds_type_defn)
; abstract_imported_type
; invalid_field_update(ctor_field_name, hlds_ctor_field_defn,
- tvarset, list(tvar)).
+ tvarset, list(tvar))
+ ; new_on_non_existential_type(type_ctor).
-:- pred convert_field_access_cons_type_info(field_access_type::in,
- ctor_field_name::in, hlds_ctor_field_defn::in,
- cons_type_info::in, maybe_cons_type_info::out) is det.
+:- pred convert_field_access_cons_type_info(class_table::in,
+ field_access_type::in, ctor_field_name::in, hlds_ctor_field_defn::in,
+ cons_type_info::in, existq_tvars::in, maybe_cons_type_info::out)
+ is det.
-convert_field_access_cons_type_info(AccessType, FieldName, FieldDefn,
- FunctorConsTypeInfo, ConsTypeInfo) :-
+convert_field_access_cons_type_info(ClassTable, AccessType, FieldName,
+ FieldDefn, FunctorConsTypeInfo, OrigExistTVars,
+ ConsTypeInfo) :-
FunctorConsTypeInfo = cons_type_info(TVarSet0, ExistQVars0,
FunctorType, ConsArgTypes, Constraints0),
FieldDefn = hlds_ctor_field_defn(_, _, _, _, FieldNumber),
@@ -3266,13 +3273,13 @@
ArgTypes = [FunctorType, FieldType],
%
- % Remove any existential constraints - the
- % typeclass-infos supplied by the input term
+ % Remove any existential constraints (which are in
+ % the unproven field, since this is a construction).
+ % The typeclass-infos supplied by the input term
% are local to the set function, so they don't
% have to be considered here.
%
- Constraints0 = constraints(UnivConstraints, _),
- Constraints = constraints(UnivConstraints, []),
+ Constraints = Constraints0 ^ unproven := [],
ConsTypeInfo = ok(cons_type_info(TVarSet, ExistQVars,
RetType, ArgTypes, Constraints))
;
@@ -3302,7 +3309,7 @@
set__list_to_set(TVarsInField),
set__intersect(
set__list_to_set(TVarsInOtherArgs),
- set__list_to_set(ExistQVars0)
+ set__list_to_set(OrigExistTVars)
),
ExistQVarsInFieldAndOthers),
( set__empty(ExistQVarsInFieldAndOthers) ->
@@ -3330,14 +3337,15 @@
% Rename the class constraints, projecting
% the constraints onto the set of type variables
% occuring in the types of the arguments of
- % the call to `'field :='/2'.
+ % the call to `'field :='/2'. Note that we
+ % have already flipped the constraints.
%
term__vars_list([FunctorType, FieldType],
CallTVars0),
set__list_to_set(CallTVars0, CallTVars),
- project_rename_flip_constraints(CallTVars,
- TVarRenaming, Constraints0,
- Constraints),
+ project_and_rename_constraints(ClassTable,
+ TVarSet, CallTVars, TVarRenaming,
+ Constraints0, Constraints),
RetType = OutputFunctorType,
ArgTypes = [FunctorType, RenamedFieldType],
@@ -3367,37 +3375,37 @@
% These constraints are all universal constraints - the values
% of the type variables are supplied by the caller.
%
-:- pred project_rename_flip_constraints(set(tvar)::in,
- map(tvar, tvar)::in, hlds_constraints::in, hlds_constraints::out)
- is det.
-
-project_rename_flip_constraints(CallTVars, TVarRenaming, !Constraints) :-
- !.Constraints = constraints(UnivConstraints0, ExistConstraints0),
+:- pred project_and_rename_constraints(class_table::in, tvarset::in,
+ set(tvar)::in, map(tvar, tvar)::in,
+ hlds_constraints::in, hlds_constraints::out) is det.
+
+project_and_rename_constraints(ClassTable, TVarSet, CallTVars, TVarRenaming,
+ !Constraints) :-
+ !.Constraints = constraints(Unproven0, Assumed, _),
%
% XXX We currently don't allow universal constraints on types or
% data constructors (but we should). When we implement handling
- % of those, they will need to be renamed here as well.
+ % of those, they will need to be renamed here as well. (The
+ % constraints have already been flipped at this point, which is why
+ % we test the assumed constraints here.)
%
(
- UnivConstraints0 = []
+ Assumed = []
;
- UnivConstraints0 = [_ | _],
- error("project_rename_flip_constraints: universal constraints")
+ Assumed = [_ | _],
+ error("project_and_rename_constraints: universal constraints")
),
%
% Project the constraints down onto the list of tvars
% in the call.
%
- list__filter(project_constraint(CallTVars),
- ExistConstraints0, ExistConstraints1),
- list__filter_map(rename_constraint(TVarRenaming),
- ExistConstraints1, NewConstraints),
-
- % The variables which were previously existentially quantified
- % are now universally quantified.
- !:Constraints = constraints(NewConstraints, []).
+ list.filter(project_constraint(CallTVars), Unproven0, Unproven1),
+ list.filter_map(rename_constraint(TVarRenaming), Unproven1, Unproven),
+ update_redundant_constraints(ClassTable, TVarSet, Unproven,
+ multi_map.init, Redundant),
+ !:Constraints = constraints(Unproven, [], Redundant).
:- pred project_constraint(set(tvar)::in, hlds_constraint::in) is semidet.
@@ -3485,7 +3493,7 @@
:- pred typecheck_info_init(module_info::in, pred_id::in,
bool::in, tvarset::in, prog_varset::in, map(prog_var, type)::in,
- headtypes::in, hlds_constraints::in, import_status::in,
+ head_type_params::in, hlds_constraints::in, import_status::in,
pred_markers::in, typecheck_info::out) is det.
typecheck_info_init(ModuleInfo, PredId, IsFieldAccessFunction,
@@ -3665,7 +3673,7 @@
% need to be put in the constraint map now.
%
HLDSTypeConstraints = constraints(HLDSUnivConstraints,
- HLDSExistConstraints),
+ HLDSExistConstraints, _),
list__foldl(update_constraint_map, HLDSUnivConstraints,
ConstraintMap1, ConstraintMap2),
list__foldl(update_constraint_map, HLDSExistConstraints,
@@ -3832,6 +3840,8 @@
typecheck_info_get_ctor_list_2(Info, Functor, Arity, GoalPath, ConsInfoList,
ConsErrors) :-
+ empty_hlds_constraints(EmptyConstraints),
+
% Check if `Functor/Arity' has been defined as a constructor
% in some discriminated union type(s). This gives
% us a list of possible cons_type_infos.
@@ -3840,8 +3850,8 @@
Functor = cons(_, _),
map__search(Ctors, Functor, HLDS_ConsDefnList)
->
- convert_cons_defn_list(Info, GoalPath, HLDS_ConsDefnList,
- MaybeConsInfoList0)
+ convert_cons_defn_list(Info, GoalPath, do_not_flip_constraints,
+ HLDS_ConsDefnList, MaybeConsInfoList0)
;
MaybeConsInfoList0 = []
),
@@ -3870,9 +3880,8 @@
OrigFunctor = cons(OrigName, Arity),
map__search(Ctors, OrigFunctor, HLDS_ExistQConsDefnList)
->
- convert_cons_defn_list(Info, GoalPath, HLDS_ExistQConsDefnList,
- ExistQuantifiedConsInfoList),
- list__filter_map(flip_quantifiers, ExistQuantifiedConsInfoList,
+ convert_cons_defn_list(Info, GoalPath,
+ flip_constraints_for_new, HLDS_ExistQConsDefnList,
UnivQuantifiedConsInfoList),
list__append(UnivQuantifiedConsInfoList,
MaybeConsInfoList0, MaybeConsInfoList1)
@@ -3906,7 +3915,7 @@
construct_type(unqualified(BuiltInTypeName) - 0, [], ConsType),
varset__init(ConsTypeVarSet),
ConsInfo = cons_type_info(ConsTypeVarSet, [], ConsType, [],
- constraints([], [])),
+ EmptyConstraints),
ConsInfoList2 = [ConsInfo | ConsInfoList1]
;
ConsInfoList2 = ConsInfoList1
@@ -3931,10 +3940,9 @@
% Tuples can't have existentially typed arguments.
TupleExistQVars = [],
-
TupleConsInfo = cons_type_info(TupleConsTypeVarSet,
TupleExistQVars, TupleConsType,
- TupleArgTypes, constraints([], [])),
+ TupleArgTypes, EmptyConstraints),
ConsInfoList3 = [TupleConsInfo | ConsInfoList2]
;
ConsInfoList3 = ConsInfoList2
@@ -3961,27 +3969,6 @@
ConsInfoList = ConsInfoList4
).
-:- pred flip_quantifiers(maybe_cons_type_info::in, maybe_cons_type_info::out)
- is semidet.
-
-flip_quantifiers(Error @ error(_), Error).
-flip_quantifiers(ok(cons_type_info(A, ExistQVars0, C, D, Constraints0)),
- ok(cons_type_info(A, ExistQVars, C, D, Constraints))) :-
- % Fail if there are no existentially quantifier variables.
- % We do this because we want to allow the 'new foo' syntax only
- % for existentially typed functors, not for ordinary functors.
- %
- ExistQVars0 = [_ | _],
-
- % convert the existentially quantified type vars into
- % universally quantified type vars by just discarding
- % the old list of existentially quantified type vars and
- % replacing it with an empty list.
- ExistQVars = [],
-
- % convert the existential constraints into universal constraints
- dual_constraints(Constraints0, Constraints).
-
:- pred split_cons_errors(list(maybe_cons_type_info)::in,
list(cons_type_info)::out, list(cons_error)::out) is det.
@@ -4025,7 +4012,7 @@
write_constraints(Context, TypeAssign, !IO) :-
type_assign_get_typeclass_constraints(TypeAssign, Constraints),
- Constraints = constraints(UnprovenConstraints, _AssumedConstraints),
+ UnprovenConstraints = Constraints ^ unproven,
retrieve_prog_constraint_list(UnprovenConstraints,
UnprovenProgConstraints0),
@@ -4069,6 +4056,13 @@
%
% In addition, context reduction removes repeated constraints.
%
+ % During context reduction we also try to "improve" the type binding
+ % in the given type_assign (that is, binding the type variables in
+ % such a way that the satisfiability of the constraints is not
+ % changed). This is done by applying improvement rules inside the
+ % fixpoint loop. The improvement rules are those which are induced
+ % by functional dependencies attached to typeclass declarations.
+ %
% If context reduction fails on a type_assign, that type_assign is
% removed from the type_assign_set. Context reduction fails if there is
% a constraint where the type of (at least) one of the arguments to
@@ -4088,11 +4082,13 @@
perform_context_reduction(OrigTypeAssignSet, !Info, !IO) :-
checkpoint("before context reduction", !Info, !IO),
typecheck_info_get_module_info(!.Info, ModuleInfo),
+ module_info_classes(ModuleInfo, ClassTable),
module_info_superclasses(ModuleInfo, SuperClassTable),
module_info_instances(ModuleInfo, InstanceTable),
typecheck_info_get_type_assign_set(!.Info, TypeAssignSet0),
list__filter_map(
- reduce_type_assign_context(SuperClassTable, InstanceTable),
+ reduce_type_assign_context(ClassTable, SuperClassTable,
+ InstanceTable),
TypeAssignSet0, TypeAssignSet),
(
% Check that this context reduction hasn't eliminated
@@ -4103,9 +4099,12 @@
report_unsatisfiable_constraints(TypeAssignSet0, !Info, !IO),
DeleteConstraints = (pred(TA0::in, TA::out) is det :-
type_assign_get_typeclass_constraints(TA0,
- constraints(_, AssumedConstraints)),
- type_assign_set_typeclass_constraints(
- constraints([], AssumedConstraints), TA0, TA)
+ Constraints0),
+ Constraints = (Constraints0
+ ^ unproven := [])
+ ^ redundant := multi_map.init,
+ type_assign_set_typeclass_constraints(Constraints,
+ TA0, TA)
),
list__map(DeleteConstraints, OrigTypeAssignSet,
NewTypeAssignSet),
@@ -4114,78 +4113,82 @@
typecheck_info_set_type_assign_set(TypeAssignSet, !Info)
).
-:- pred reduce_type_assign_context(superclass_table::in, instance_table::in,
- type_assign::in, type_assign::out) is semidet.
+:- pred reduce_type_assign_context(class_table::in, superclass_table::in,
+ instance_table::in, type_assign::in, type_assign::out) is semidet.
-reduce_type_assign_context(SuperClassTable, InstanceTable, !TypeAssign) :-
+reduce_type_assign_context(ClassTable, SuperClassTable, InstanceTable,
+ !TypeAssign) :-
type_assign_get_head_type_params(!.TypeAssign, HeadTypeParams),
- type_assign_get_type_bindings(!.TypeAssign, Bindings),
+ type_assign_get_type_bindings(!.TypeAssign, Bindings0),
type_assign_get_typeclass_constraints(!.TypeAssign, Constraints0),
type_assign_get_typevarset(!.TypeAssign, TVarSet0),
type_assign_get_constraint_proofs(!.TypeAssign, Proofs0),
type_assign_get_constraint_map(!.TypeAssign, ConstraintMap0),
- Constraints0 = constraints(UnprovenConstraints0, AssumedConstraints),
- typecheck__reduce_context_by_rule_application(InstanceTable,
- SuperClassTable, AssumedConstraints,
- Bindings, TVarSet0, TVarSet, Proofs0, Proofs,
- ConstraintMap0, ConstraintMap,
- UnprovenConstraints0, UnprovenConstraints),
- check_satisfiability(UnprovenConstraints, HeadTypeParams),
- Constraints = constraints(UnprovenConstraints, AssumedConstraints),
+ typecheck__reduce_context_by_rule_application(ClassTable,
+ InstanceTable, SuperClassTable, HeadTypeParams,
+ Bindings0, Bindings, TVarSet0, TVarSet, Proofs0, Proofs,
+ ConstraintMap0, ConstraintMap, Constraints0, Constraints),
+ check_satisfiability(Constraints ^ unproven, HeadTypeParams),
+ type_assign_set_type_bindings(Bindings, !TypeAssign),
type_assign_set_typeclass_constraints(Constraints, !TypeAssign),
type_assign_set_typevarset(TVarSet, !TypeAssign),
type_assign_set_constraint_proofs(Proofs, !TypeAssign),
type_assign_set_constraint_map(ConstraintMap, !TypeAssign).
-typecheck__reduce_context_by_rule_application(InstanceTable, SuperClassTable,
- AssumedConstraints, Bindings, !TVarSet, !Proofs,
+typecheck__reduce_context_by_rule_application(ClassTable, InstanceTable,
+ SuperClassTable, HeadTypeParams, !Bindings, !TVarSet, !Proofs,
!ConstraintMap, !Constraints) :-
- typecheck__reduce_context_by_rule_application_2(InstanceTable,
- SuperClassTable, AssumedConstraints, Bindings, !TVarSet,
- !Proofs, !ConstraintMap, !Constraints, !.Constraints, _).
-
-:- pred typecheck__reduce_context_by_rule_application_2(instance_table::in,
- superclass_table::in, list(hlds_constraint)::in, tsubst::in,
- tvarset::in, tvarset::out,
+ typecheck__reduce_context_by_rule_application_2(ClassTable,
+ InstanceTable, SuperClassTable, HeadTypeParams, !Bindings,
+ !TVarSet, !Proofs, !ConstraintMap, !Constraints,
+ !.Constraints ^ unproven, _).
+
+:- pred typecheck__reduce_context_by_rule_application_2(class_table::in,
+ instance_table::in, superclass_table::in, head_type_params::in,
+ tsubst::in, tsubst::out, tvarset::in, tvarset::out,
constraint_proof_map::in, constraint_proof_map::out,
constraint_map::in, constraint_map::out,
- list(hlds_constraint)::in, list(hlds_constraint)::out,
+ hlds_constraints::in, hlds_constraints::out,
list(hlds_constraint)::in, list(hlds_constraint)::out) is det.
-typecheck__reduce_context_by_rule_application_2(InstanceTable,
- SuperClassTable, AssumedConstraints, Bindings,
- !TVarSet, !Proofs, !ConstraintMap, !Constraints, !Seen) :-
- InitialTVarSet = !.TVarSet,
- apply_rec_subst_to_constraint_list(Bindings, !Constraints),
- eliminate_assumed_constraints(AssumedConstraints, !ConstraintMap,
- !Constraints, Changed1),
- apply_instance_rules(InstanceTable, !TVarSet, !Proofs, !ConstraintMap,
- !Seen, !Constraints, Changed2),
- varset__vars(!.TVarSet, TVars),
- apply_class_rules(AssumedConstraints, TVars, SuperClassTable,
- InitialTVarSet, !Proofs, !ConstraintMap, !Constraints,
- Changed3),
- (
- Changed1 = no,
- Changed2 = no,
- Changed3 = no
+typecheck__reduce_context_by_rule_application_2(ClassTable, InstanceTable,
+ SuperClassTable, HeadTypeParams, !Bindings, !TVarSet, !Proofs,
+ !ConstraintMap, !Constraints, !Seen) :-
+ apply_rec_subst_to_constraints(!.Bindings, !Constraints),
+ apply_improvement_rules(ClassTable, InstanceTable, HeadTypeParams,
+ !TVarSet, !Bindings, !Constraints, AppliedImprovementRule),
+ eliminate_assumed_constraints(!ConstraintMap, !Constraints,
+ EliminatedAssumed),
+ apply_instance_rules(ClassTable, InstanceTable, !TVarSet, !Proofs,
+ !ConstraintMap, !Seen, !Constraints, AppliedInstanceRule),
+ apply_class_rules(SuperClassTable, HeadTypeParams, !.TVarSet,
+ !Proofs, !ConstraintMap, !Constraints, AppliedClassRule),
+ (
+ AppliedImprovementRule = no,
+ EliminatedAssumed = no,
+ AppliedInstanceRule = no,
+ AppliedClassRule = no
->
% We have reached fixpoint
sort_and_merge_dups(!Constraints)
;
- typecheck__reduce_context_by_rule_application_2(InstanceTable,
- SuperClassTable, AssumedConstraints, Bindings,
- !TVarSet, !Proofs, !ConstraintMap, !Constraints, !Seen)
+ typecheck__reduce_context_by_rule_application_2(ClassTable,
+ InstanceTable, SuperClassTable, HeadTypeParams,
+ !Bindings, !TVarSet, !Proofs, !ConstraintMap,
+ !Constraints, !Seen)
).
-:- pred sort_and_merge_dups(list(hlds_constraint)::in,
- list(hlds_constraint)::out) is det.
+:- pred sort_and_merge_dups(hlds_constraints::in, hlds_constraints::out)
+ is det.
sort_and_merge_dups(!Constraints) :-
- list__sort(compare_hlds_constraints, !Constraints),
- merge_adjacent_constraints(!Constraints).
+ % Should we also sort and merge the other fields?
+ Unproven0 = !.Constraints ^ unproven,
+ list__sort(compare_hlds_constraints, Unproven0, Unproven1),
+ merge_adjacent_constraints(Unproven1, Unproven),
+ !:Constraints = !.Constraints ^ unproven := Unproven.
:- pred merge_adjacent_constraints(list(hlds_constraint)::in,
list(hlds_constraint)::out) is det.
@@ -4220,15 +4223,330 @@
list__append(IdsA, IdsB, Ids0),
list__sort_and_remove_dups(Ids0, Ids).
-:- pred eliminate_assumed_constraints(list(hlds_constraint)::in,
- constraint_map::in, constraint_map::out,
- list(hlds_constraint)::in, list(hlds_constraint)::out, bool::out)
+:- pred apply_improvement_rules(class_table::in, instance_table::in,
+ head_type_params::in, tvarset::in, tvarset::out,
+ tsubst::in, tsubst::out, hlds_constraints::in, hlds_constraints::out,
+ bool::out) is det.
+
+apply_improvement_rules(ClassTable, InstanceTable, HeadTypeParams, !TVarSet,
+ !Bindings, !Constraints, Changed) :-
+ % XXX should we sort and merge the constraints here?
+ do_class_improvement(ClassTable, HeadTypeParams, !.Constraints,
+ !Bindings, Changed1),
+ % XXX do we really need to modify the varset? See the comment above
+ % find_matching_instance_rule.
+ do_instance_improvement(ClassTable, InstanceTable, HeadTypeParams,
+ !.Constraints, !TVarSet, !Bindings, Changed2),
+ apply_rec_subst_to_constraints(!.Bindings, !Constraints),
+ Changed = bool__or(Changed1, Changed2).
+
+:- pred do_class_improvement(class_table::in, head_type_params::in,
+ hlds_constraints::in, tsubst::in, tsubst::out, bool::out) is det.
+
+do_class_improvement(ClassTable, HeadTypeParams, Constraints, !Bindings,
+ Changed) :-
+ Redundant = Constraints ^ redundant,
+ Assumed = Constraints ^ assumed,
+ multi_map__keys(Redundant, ClassIds),
+ list__foldl2(
+ do_class_improvement_2(ClassTable, HeadTypeParams, Redundant,
+ Assumed),
+ ClassIds, !Bindings, no, Changed).
+
+:- pred do_class_improvement_2(class_table::in, head_type_params::in,
+ redundant_constraints::in, list(hlds_constraint)::in, class_id::in,
+ tsubst::in, tsubst::out, bool::in, bool::out) is det.
+
+do_class_improvement_2(ClassTable, HeadTypeParams, RedundantConstraints,
+ Assumed, ClassId, !Bindings, !Changed) :-
+ map__lookup(ClassTable, ClassId, ClassDefn),
+ FunDeps = ClassDefn ^ class_fundeps,
+ map__lookup(RedundantConstraints, ClassId, Constraints),
+ do_class_improvement_by_pairs(Constraints, FunDeps, HeadTypeParams,
+ !Bindings, !Changed),
+ list__filter(has_class_id(ClassId), Assumed, ThisClassAssumed),
+ do_class_improvement_by_assumed(ThisClassAssumed, Constraints, FunDeps,
+ HeadTypeParams, !Bindings, !Changed).
+
+:- pred has_class_id(class_id::in, hlds_constraint::in) is semidet.
+
+has_class_id(class_id(Name, Arity), constraint(_, Name, Args)) :-
+ list__length(Args, Arity).
+
+ % Try to find an opportunity for improvement for each (unordered)
+ % pair of constraints from the list.
+ %
+:- pred do_class_improvement_by_pairs(list(hlds_constraint)::in,
+ hlds_class_fundeps::in, head_type_params::in, tsubst::in, tsubst::out,
+ bool::in, bool::out) is det.
+
+do_class_improvement_by_pairs([], _, _, !Bindings, !Changed).
+do_class_improvement_by_pairs([Constraint | Constraints], FunDeps,
+ HeadTypeParams, !Bindings, !Changed) :-
+ do_class_improvement_by_pairs_2(Constraint, Constraints, FunDeps,
+ HeadTypeParams, !Bindings, !Changed),
+ do_class_improvement_by_pairs(Constraints, FunDeps, HeadTypeParams,
+ !Bindings, !Changed).
+
+:- pred do_class_improvement_by_pairs_2(hlds_constraint::in,
+ list(hlds_constraint)::in, hlds_class_fundeps::in,
+ head_type_params::in, tsubst::in, tsubst::out, bool::in, bool::out)
+ is det.
+
+do_class_improvement_by_pairs_2(_, [], _, _, !Bindings, !Changed).
+do_class_improvement_by_pairs_2(Constraint, [HeadConstraint | TailConstraints],
+ FunDeps, HeadTypeParams, !Bindings, !Changed) :-
+ do_class_improvement_pair(Constraint, HeadConstraint, FunDeps,
+ HeadTypeParams, !Bindings, !Changed),
+ do_class_improvement_by_pairs_2(Constraint, TailConstraints, FunDeps,
+ HeadTypeParams, !Bindings, !Changed).
+
+ % Try to find an opportunity for improvement for each pair of
+ % constraints where one comes from the assumed constraints and the
+ % other comes from the redundant constraints.
+ %
+:- pred do_class_improvement_by_assumed(list(hlds_constraint)::in,
+ list(hlds_constraint)::in, hlds_class_fundeps::in,
+ head_type_params::in, tsubst::in, tsubst::out, bool::in, bool::out)
is det.
-eliminate_assumed_constraints(_, !ConstraintMap, [], [], no).
-eliminate_assumed_constraints(AssumedCs, !ConstraintMap, [C | Cs], NewCs,
+do_class_improvement_by_assumed(Assumed, Constraints, FunDeps, HeadTypeParams,
+ !Bindings, !Changed) :-
+ list__foldl2(
+ do_class_improvement_by_assumed_2(Constraints, FunDeps,
+ HeadTypeParams),
+ Assumed, !Bindings, !Changed).
+
+:- pred do_class_improvement_by_assumed_2(list(hlds_constraint)::in,
+ hlds_class_fundeps::in, head_type_params::in, hlds_constraint::in,
+ tsubst::in, tsubst::out, bool::in, bool::out) is det.
+
+do_class_improvement_by_assumed_2([], _, _, _, !Bindings, !Changed).
+do_class_improvement_by_assumed_2([Constraint | Constraints], FunDeps,
+ HeadTypeParams, Assumed, !Bindings, !Changed) :-
+ do_class_improvement_pair(Constraint, Assumed, FunDeps, HeadTypeParams,
+ !Bindings, !Changed),
+ do_class_improvement_by_assumed_2(Constraints, FunDeps, HeadTypeParams,
+ Assumed, !Bindings, !Changed).
+
+ % Try to find an opportunity for improvement for this pair of
+ % constraints, using each fundep in turn.
+ %
+:- pred do_class_improvement_pair(hlds_constraint::in, hlds_constraint::in,
+ hlds_class_fundeps::in, head_type_params::in, tsubst::in, tsubst::out,
+ bool::in, bool::out) is det.
+
+do_class_improvement_pair(_, _, [], _, !Bindings, !Changed).
+do_class_improvement_pair(ConstraintA, ConstraintB, [FunDep | FunDeps],
+ HeadTypeParams, !Bindings, !Changed) :-
+ do_class_improvement_fundep(ConstraintA, ConstraintB, FunDep,
+ HeadTypeParams, !Bindings, !Changed),
+ do_class_improvement_pair(ConstraintA, ConstraintB, FunDeps,
+ HeadTypeParams, !Bindings, !Changed).
+
+:- pred do_class_improvement_fundep(hlds_constraint::in, hlds_constraint::in,
+ hlds_class_fundep::in, head_type_params::in, tsubst::in, tsubst::out,
+ bool::in, bool::out) is det.
+
+do_class_improvement_fundep(ConstraintA, ConstraintB, FunDep, HeadTypeParams,
+ !Bindings, !Changed) :-
+ ConstraintA = constraint(_, _, TypesA),
+ ConstraintB = constraint(_, _, TypesB),
+ FunDep = fundep(Domain, Range),
+ (
+ %
+ % We already know that the name/arity of the
+ % constraints match, since we have partitioned them
+ % already.
+ %
+ lists_match_on_elements(Domain, TypesA, TypesB),
+ \+ lists_match_on_elements(Range, TypesA, TypesB),
+
+ %
+ % The unification can fail if type parameters in the
+ % declaration would be bound by the improvement rule.
+ % This means that the declaration is not as specific
+ % as it could be, but that is not a problem for us.
+ %
+ unify_on_elements(Range, TypesA, TypesB, HeadTypeParams,
+ !Bindings)
+ ->
+ !:Changed = yes
+ ;
+ true
+ ).
+
+:- pred do_instance_improvement(class_table::in, instance_table::in,
+ head_type_params::in, hlds_constraints::in, tvarset::in, tvarset::out,
+ tsubst::in, tsubst::out, bool::out) is det.
+
+do_instance_improvement(ClassTable, InstanceTable, HeadTypeParams, Constraints,
+ !TVarSet, !Bindings, Changed) :-
+ RedundantConstraints = Constraints ^ redundant,
+ map__keys(RedundantConstraints, ClassIds),
+ list__foldl3(
+ do_instance_improvement_2(ClassTable, InstanceTable,
+ HeadTypeParams, RedundantConstraints),
+ ClassIds, !TVarSet, !Bindings, no, Changed).
+
+:- pred do_instance_improvement_2(class_table::in, instance_table::in,
+ head_type_params::in, redundant_constraints::in, class_id::in,
+ tvarset::in, tvarset::out, tsubst::in, tsubst::out,
+ bool::in, bool::out) is det.
+
+do_instance_improvement_2(ClassTable, InstanceTable, HeadTypeParams,
+ RedundantConstraints, ClassId, !TVarSet, !Bindings,
+ !Changed) :-
+ map__lookup(ClassTable, ClassId, ClassDefn),
+ FunDeps = ClassDefn ^ class_fundeps,
+ map__lookup(InstanceTable, ClassId, InstanceDefns),
+ map__lookup(RedundantConstraints, ClassId, Constraints),
+ list__foldl3(
+ do_instance_improvement_3(Constraints, FunDeps,
+ HeadTypeParams),
+ InstanceDefns, !TVarSet, !Bindings, !Changed).
+
+:- pred do_instance_improvement_3(list(hlds_constraint)::in,
+ hlds_class_fundeps::in, head_type_params::in, hlds_instance_defn::in,
+ tvarset::in, tvarset::out, tsubst::in, tsubst::out,
+ bool::in, bool::out) is det.
+
+do_instance_improvement_3(Constraints, FunDeps, HeadTypeParams, InstanceDefn,
+ !TVarSet, !Bindings, !Changed) :-
+ InstanceTVarSet = InstanceDefn ^ instance_tvarset,
+ InstanceTypes0 = InstanceDefn ^ instance_types,
+ varset__merge_subst(!.TVarSet, InstanceTVarSet, NewTVarSet,
+ RenameSubst),
+ term__apply_substitution_to_list(InstanceTypes0, RenameSubst,
+ InstanceTypes),
+ list__foldl2(
+ do_instance_improvement_4(FunDeps, InstanceTypes,
+ HeadTypeParams),
+ Constraints, !Bindings, no, Changed0),
+ (
+ Changed0 = yes,
+ !:TVarSet = NewTVarSet,
+ !:Changed = yes
+ ;
+ Changed0 = no
+ ).
+
+:- pred do_instance_improvement_4(hlds_class_fundeps::in, list(type)::in,
+ head_type_params::in, hlds_constraint::in, tsubst::in, tsubst::out,
+ bool::in, bool::out) is det.
+
+do_instance_improvement_4(FunDeps, InstanceTypes, HeadTypeParams, Constraint,
+ !Bindings, !Changed) :-
+ list__foldl2(
+ do_instance_improvement_fundep(Constraint, InstanceTypes,
+ HeadTypeParams),
+ FunDeps, !Bindings, !Changed).
+
+:- pred do_instance_improvement_fundep(hlds_constraint::in, list(type)::in,
+ head_type_params::in, hlds_class_fundep::in, tsubst::in, tsubst::out,
+ bool::in, bool::out) is det.
+
+do_instance_improvement_fundep(Constraint, InstanceTypes0, HeadTypeParams,
+ FunDep, !Bindings, !Changed) :-
+ Constraint = constraint(_, _, ConstraintTypes),
+ FunDep = fundep(Domain, Range),
+ (
+ %
+ % We already know that the name/arity of the
+ % constraints match, since we have partitioned them
+ % already.
+ %
+ subsumes_on_elements(Domain, InstanceTypes0, ConstraintTypes,
+ Subst),
+ term__apply_rec_substitution_to_list(InstanceTypes0, Subst,
+ InstanceTypes),
+ \+ lists_match_on_elements(Range, InstanceTypes,
+ ConstraintTypes),
+
+ %
+ % The unification can fail if type parameters in the
+ % declaration would be bound by the improvement rule.
+ % This means that the declaration is not as specific
+ % as it could be, but that is not a problem for us.
+ %
+ unify_on_elements(Range, InstanceTypes, ConstraintTypes,
+ HeadTypeParams, !Bindings)
+ ->
+ !:Changed = yes
+ ;
+ true
+ ).
+
+ % For each index in the set, check that the types in the corresponding
+ % positions in the lists are identical.
+ %
+:- pred lists_match_on_elements(set(int)::in, list(type)::in, list(type)::in)
+ is semidet.
+
+lists_match_on_elements(Elements, TypesA, TypesB) :-
+ RTypesA = restrict_list_elements(Elements, TypesA),
+ RTypesB = restrict_list_elements(Elements, TypesB),
+ RTypesA = RTypesB.
+
+ % For each index in the set, unify the types in the corresponding
+ % positions in the lists and add to the current bindings.
+ %
+:- pred unify_on_elements(set(int)::in, list(type)::in, list(type)::in,
+ head_type_params::in, tsubst::in, tsubst::out) is semidet.
+
+unify_on_elements(Elements, TypesA, TypesB, HeadTypeParams, !Bindings) :-
+ RTypesA = restrict_list_elements(Elements, TypesA),
+ RTypesB = restrict_list_elements(Elements, TypesB),
+ type_unify_list(RTypesA, RTypesB, HeadTypeParams, !Bindings).
+
+ % Analogous to type_list_subsumes except that it only checks those
+ % elements of the list specified by the set of indices.
+ %
+:- pred subsumes_on_elements(set(int)::in, list(type)::in, list(type)::in,
+ tsubst::out) is semidet.
+
+subsumes_on_elements(Elements, TypesA, TypesB, Subst) :-
+ RTypesA = restrict_list_elements(Elements, TypesA),
+ RTypesB = restrict_list_elements(Elements, TypesB),
+ term__vars_list(RTypesB, RTypesBVars),
+ map__init(Subst0),
+ type_unify_list(RTypesA, RTypesB, RTypesBVars, Subst0, Subst).
+
+:- func restrict_list_elements(set(int), list(T)) = list(T).
+
+restrict_list_elements(Elements, List) =
+ restrict_list_elements_2(Elements, 1, List).
+
+:- func restrict_list_elements_2(set(int), int, list(T)) = list(T).
+
+restrict_list_elements_2(_, _, []) = [].
+restrict_list_elements_2(Elements, Index, [X | Xs]) =
+ (
+ set__member(Index, Elements)
+ ->
+ [X | restrict_list_elements_2(Elements, Index + 1, Xs)]
+ ;
+ restrict_list_elements_2(Elements, Index + 1, Xs)
+ ).
+
+:- pred eliminate_assumed_constraints(constraint_map::in, constraint_map::out,
+ hlds_constraints::in, hlds_constraints::out, bool::out) is det.
+
+eliminate_assumed_constraints(!ConstraintMap, !Constraints, Changed) :-
+ !.Constraints = constraints(Unproven0, Assumed, Redundant),
+ eliminate_assumed_constraints_2(Assumed, !ConstraintMap,
+ Unproven0, Unproven, Changed),
+ !:Constraints = constraints(Unproven, Assumed, Redundant).
+
+:- pred eliminate_assumed_constraints_2(list(hlds_constraint)::in,
+ constraint_map::in, constraint_map::out,
+ list(hlds_constraint)::in, list(hlds_constraint)::out,
+ bool::out) is det.
+
+eliminate_assumed_constraints_2(_, !ConstraintMap, [], [], no).
+eliminate_assumed_constraints_2(AssumedCs, !ConstraintMap, [C | Cs], NewCs,
Changed) :-
- eliminate_assumed_constraints(AssumedCs, !ConstraintMap, Cs, NewCs0,
+ eliminate_assumed_constraints_2(AssumedCs, !ConstraintMap, Cs, NewCs0,
Changed0),
(
some [A] (
@@ -4244,16 +4562,35 @@
Changed = Changed0
).
-:- pred apply_instance_rules(instance_table::in, tvarset::in, tvarset::out,
+:- pred apply_instance_rules(class_table::in, instance_table::in,
+ tvarset::in, tvarset::out,
+ constraint_proof_map::in, constraint_proof_map::out,
+ constraint_map::in, constraint_map::out,
+ list(hlds_constraint)::in, list(hlds_constraint)::out,
+ hlds_constraints::in, hlds_constraints::out, bool::out) is det.
+
+apply_instance_rules(ClassTable, InstanceTable, !TVarSet, !Proofs,
+ !ConstraintMap, !Seen, !Constraints, Changed) :-
+ !.Constraints = constraints(Unproven0, Assumed, Redundant0),
+ apply_instance_rules_2(ClassTable, InstanceTable, !TVarSet, !Proofs,
+ !ConstraintMap, Redundant0, Redundant, !Seen,
+ Unproven0, Unproven, Changed),
+ !:Constraints = constraints(Unproven, Assumed, Redundant).
+
+:- pred apply_instance_rules_2(class_table::in, instance_table::in,
+ tvarset::in, tvarset::out,
constraint_proof_map::in, constraint_proof_map::out,
constraint_map::in, constraint_map::out,
+ redundant_constraints::in, redundant_constraints::out,
list(hlds_constraint)::in, list(hlds_constraint)::out,
list(hlds_constraint)::in, list(hlds_constraint)::out, bool::out)
is det.
-apply_instance_rules(_, !TVarSet, !Proofs, !ConstraintMap, !Seen, [], [], no).
-apply_instance_rules(InstanceTable, !TVarSet, !Proofs, !ConstraintMap, !Seen,
- [C | Cs], Constraints, Changed) :-
+apply_instance_rules_2(_, _, !TVarSet, !Proofs, !ConstraintMap, !Redundant,
+ !Seen, [], [], no).
+apply_instance_rules_2(ClassTable, InstanceTable, !TVarSet, !Proofs,
+ !ConstraintMap, !Redundant, !Seen, [C | Cs], Constraints,
+ Changed) :-
C = constraint(_, ClassName, Types),
list__length(Types, Arity),
map__lookup(InstanceTable, class_id(ClassName, Arity), Instances),
@@ -4267,6 +4604,8 @@
% This ensures we don't get into an infinite loop.
list__filter(matches_no_constraint(!.Seen), NewConstraints0,
NewConstraints),
+ update_redundant_constraints(ClassTable, !.TVarSet,
+ NewConstraints, !Redundant),
% Put the new constraints at the front of the list
!:Seen = NewConstraints ++ !.Seen,
Changed1 = yes
@@ -4276,8 +4615,9 @@
!:TVarSet = InitialTVarSet,
Changed1 = no
),
- apply_instance_rules(InstanceTable, !TVarSet, !Proofs, !ConstraintMap,
- !Seen, Cs, TailConstraints, Changed2),
+ apply_instance_rules_2(ClassTable, InstanceTable, !TVarSet, !Proofs,
+ !ConstraintMap, !Redundant, !Seen, Cs, TailConstraints,
+ Changed2),
bool__or(Changed1, Changed2, Changed),
list__append(NewConstraints, TailConstraints, Constraints).
@@ -4349,32 +4689,44 @@
% superclass relation to find a path from the inferred constraint to
% another (declared or inferred) constraint.
%
-:- pred apply_class_rules(list(hlds_constraint)::in, list(tvar)::in,
- superclass_table::in, tvarset::in,
+:- pred apply_class_rules(superclass_table::in, head_type_params::in,
+ tvarset::in, constraint_proof_map::in, constraint_proof_map::out,
+ constraint_map::in, constraint_map::out,
+ hlds_constraints::in, hlds_constraints::out, bool::out) is det.
+
+apply_class_rules(SuperClassTable, HeadTypeParams, TVarSet, !Proofs,
+ !ConstraintMap, !Constraints, Changed) :-
+ !.Constraints = constraints(Unproven0, Assumed, _),
+ apply_class_rules_2(Assumed, SuperClassTable, HeadTypeParams, TVarSet,
+ !Proofs, !ConstraintMap, Unproven0, Unproven, Changed),
+ !:Constraints = !.Constraints ^ unproven := Unproven.
+
+:- pred apply_class_rules_2(list(hlds_constraint)::in, superclass_table::in,
+ head_type_params::in, tvarset::in,
constraint_proof_map::in, constraint_proof_map::out,
constraint_map::in, constraint_map::out,
- list(hlds_constraint)::in, list(hlds_constraint)::out, bool::out)
- is det.
+ list(hlds_constraint)::in, list(hlds_constraint)::out,
+ bool::out) is det.
-apply_class_rules(_, _, _, _, !Proofs, !ConstraintMap, [], [], no).
-apply_class_rules(AssumedConstraints, HeadTypeParams, SuperClassTable, TVarSet,
- !Proofs, !ConstraintMap,
+apply_class_rules_2(_, _, _, _, !Proofs, !ConstraintMap, [], [], no).
+apply_class_rules_2(AssumedConstraints, SuperClassTable, HeadTypeParams,
+ TVarSet, !Proofs, !ConstraintMap,
[Constraint0 | Constraints0], Constraints, Changed) :-
(
Parents = [],
retrieve_prog_constraint(Constraint0, ProgConstraint0),
eliminate_constraint_by_class_rules(ProgConstraint0, _, _,
- HeadTypeParams, AssumedConstraints, SuperClassTable,
+ AssumedConstraints, SuperClassTable, HeadTypeParams,
TVarSet, Parents, !Proofs)
->
update_constraint_map(Constraint0, !ConstraintMap),
- apply_class_rules(AssumedConstraints, HeadTypeParams,
- SuperClassTable, TVarSet, !Proofs, !ConstraintMap,
+ apply_class_rules_2(AssumedConstraints, SuperClassTable,
+ HeadTypeParams, TVarSet, !Proofs, !ConstraintMap,
Constraints0, Constraints, _),
Changed = yes
;
- apply_class_rules(AssumedConstraints, HeadTypeParams,
- SuperClassTable, TVarSet, !Proofs, !ConstraintMap,
+ apply_class_rules_2(AssumedConstraints, SuperClassTable,
+ HeadTypeParams, TVarSet, !Proofs, !ConstraintMap,
Constraints0, TailConstraints, Changed),
Constraints = [Constraint0 | TailConstraints]
).
@@ -4385,19 +4737,19 @@
% (recursively) in the process of checking, and is used to ensure that
% we don't get into a cycle in the relation.
%
- % The list(tvar) argument contains all the variables from the
+ % The head_type_params argument contains all the variables from the
% original constraint that we are trying to prove. (These are the
% type variables that must not be bound as we search through the
% superclass relation).
%
:- pred eliminate_constraint_by_class_rules(prog_constraint::in,
- prog_constraint::out, tsubst::out, list(tvar)::in,
- list(hlds_constraint)::in, superclass_table::in, tvarset::in,
+ prog_constraint::out, tsubst::out, list(hlds_constraint)::in,
+ superclass_table::in, head_type_params::in, tvarset::in,
list(prog_constraint)::in,
constraint_proof_map::in, constraint_proof_map::out) is semidet.
-eliminate_constraint_by_class_rules(C, SubstC, SubClassSubst, ConstVars,
- AssumedConstraints, SuperClassTable, TVarSet,
+eliminate_constraint_by_class_rules(C, SubstC, SubClassSubst,
+ AssumedConstraints, SuperClassTable, HeadTypeParams, TVarSet,
ParentConstraints, Proofs0, Proofs) :-
% Make sure we aren't in a cycle in the
@@ -4424,7 +4776,7 @@
% an assumed constraint which unifies with any
% of the subclass constraints.
list.find_first_map(
- match_assumed_constraint(ConstVars,
+ match_assumed_constraint(HeadTypeParams,
SubClassConstraints),
AssumedConstraints, SubClass - SubClassSubst0)
->
@@ -4440,8 +4792,8 @@
is semidet :-
eliminate_constraint_by_class_rules(Constraint,
SubstConstraint, SubClassSubst0,
- ConstVars, AssumedConstraints, SuperClassTable,
- TVarSet, NewParentConstraints,
+ AssumedConstraints, SuperClassTable,
+ HeadTypeParams, TVarSet, NewParentConstraints,
Proofs0, SubProofs),
CnstrtAndProof = {SubstConstraint, SubClassSubst0,
SubProofs}
@@ -4454,19 +4806,20 @@
map__set(NewProofs, SubstC, superclass(NewSubClass), Proofs)
).
-:- pred match_assumed_constraint(list(tvar)::in, list(prog_constraint)::in,
- hlds_constraint::in, pair(prog_constraint, tsubst)::out) is semidet.
+:- pred match_assumed_constraint(head_type_params::in,
+ list(prog_constraint)::in, hlds_constraint::in,
+ pair(prog_constraint, tsubst)::out) is semidet.
-match_assumed_constraint(ConstVars, SubClassConstraints, AssumedConstraint,
- Match) :-
+match_assumed_constraint(HeadTypeParams, SubClassConstraints,
+ AssumedConstraint, Match) :-
find_first_map(
- match_assumed_constraint_2(ConstVars, AssumedConstraint),
+ match_assumed_constraint_2(HeadTypeParams, AssumedConstraint),
SubClassConstraints, Match).
-:- pred match_assumed_constraint_2(list(tvar)::in, hlds_constraint::in,
+:- pred match_assumed_constraint_2(head_type_params::in, hlds_constraint::in,
prog_constraint::in, pair(prog_constraint, tsubst)::out) is semidet.
-match_assumed_constraint_2(ConstVars, AssumedConstraint,
+match_assumed_constraint_2(HeadTypeParams, AssumedConstraint,
SubClassConstraint, Match) :-
AssumedConstraint = constraint(_, AssumedConstraintClass,
AssumedConstraintTypes),
@@ -4474,7 +4827,7 @@
SubClassConstraintTypes),
map__init(EmptySub),
type_unify_list(SubClassConstraintTypes, AssumedConstraintTypes,
- ConstVars, EmptySub, AssumedConstraintSub),
+ HeadTypeParams, EmptySub, AssumedConstraintSub),
retrieve_prog_constraint(AssumedConstraint, MatchingProgConstraint),
Match = MatchingProgConstraint - AssumedConstraintSub.
@@ -4552,19 +4905,26 @@
%-----------------------------------------------------------------------------%
+:- type cons_constraints_action
+ ---> flip_constraints_for_new
+ ; flip_constraints_for_field_set
+ ; do_not_flip_constraints.
+
:- pred convert_cons_defn_list(typecheck_info::in, goal_path::in,
- list(hlds_cons_defn)::in, list(maybe_cons_type_info)::out) is det.
+ cons_constraints_action::in, list(hlds_cons_defn)::in,
+ list(maybe_cons_type_info)::out) is det.
-convert_cons_defn_list(_Info, _GoalPath, [], []).
-convert_cons_defn_list(Info, GoalPath, [X | Xs], [Y | Ys]) :-
- convert_cons_defn(Info, GoalPath, X, Y),
- convert_cons_defn_list(Info, GoalPath, Xs, Ys).
+convert_cons_defn_list(_Info, _GoalPath, _Action, [], []).
+convert_cons_defn_list(Info, GoalPath, Action, [X | Xs], [Y | Ys]) :-
+ convert_cons_defn(Info, GoalPath, Action, X, Y),
+ convert_cons_defn_list(Info, GoalPath, Action, Xs, Ys).
:- pred convert_cons_defn(typecheck_info::in, goal_path::in,
- hlds_cons_defn::in, maybe_cons_type_info::out) is det.
+ cons_constraints_action::in, hlds_cons_defn::in,
+ maybe_cons_type_info::out) is det.
-convert_cons_defn(Info, GoalPath, HLDS_ConsDefn, ConsTypeInfo) :-
- HLDS_ConsDefn = hlds_cons_defn(ExistQVars, ExistProgConstraints, Args,
+convert_cons_defn(Info, GoalPath, Action, HLDS_ConsDefn, ConsTypeInfo) :-
+ HLDS_ConsDefn = hlds_cons_defn(ExistQVars0, ExistProgConstraints, Args,
TypeCtor, _),
assoc_list__values(Args, ArgTypes),
typecheck_info_get_types(Info, Types),
@@ -4597,6 +4957,7 @@
%
typecheck_info_get_predid(Info, PredId),
typecheck_info_get_module_info(Info, ModuleInfo),
+ module_info_classes(ModuleInfo, ClassTable),
module_info_pred_info(ModuleInfo, PredId, PredInfo),
(
Body ^ du_type_is_foreign_type = yes(_),
@@ -4615,11 +4976,33 @@
->
ConsTypeInfo = error(abstract_imported_type)
;
+ Action = flip_constraints_for_new,
+ ExistQVars0 = []
+ ->
+ % Do not allow 'new' constructors except on existential types.
+ ConsTypeInfo = error(new_on_non_existential_type(TypeCtor))
+ ;
construct_type(TypeCtor, ConsTypeParams, ConsType),
- UnivConstraints = [],
- make_hlds_constraint_list(ExistProgConstraints, existential,
- GoalPath, ExistConstraints),
- Constraints = constraints(UnivConstraints, ExistConstraints),
+ UnivProgConstraints = [],
+ (
+ Action = do_not_flip_constraints
+ ->
+ ProgConstraints = constraints(UnivProgConstraints,
+ ExistProgConstraints),
+ ExistQVars = ExistQVars0
+ ;
+ %
+ % Make the existential constraints into
+ % universal ones, and discard the existentially
+ % quantified variables (since they are now
+ % universally quantified).
+ %
+ ProgConstraints = constraints(ExistProgConstraints,
+ UnivProgConstraints),
+ ExistQVars = []
+ ),
+ make_body_hlds_constraints(ClassTable, ConsTypeVarSet,
+ GoalPath, ProgConstraints, Constraints),
ConsTypeInfo = ok(cons_type_info(ConsTypeVarSet, ExistQVars,
ConsType, ArgTypes, Constraints))
).
@@ -4636,28 +5019,13 @@
var_types :: map(prog_var, type),
type_varset :: tvarset,
% type names
- head_type_params :: headtypes,
+ head_type_params :: head_type_params,
% universally quantified type variables
type_bindings :: tsubst,
% type bindings
class_constraints :: hlds_constraints,
- % This field has the form
- % constraints(Universal, Existential).
- % The first element in this pair
- % (the "universal" constraints) holds
- % the constraints that we must prove,
- % i.e. universal constraints from
- % callees, or existential constraints
- % on the declaration of the predicate
- % we are analyzing. The second element
- % in the pair (the "existential"
- % constraints) holds the constraints
- % we can assume, i.e. existential
- % constraints from callees, or
- % universal constraints on the
- % declaration of the predicate
- % we are analyzing.
-
+ % the set of class constraints
+ % collected so far
constraint_proofs :: constraint_proof_map,
% for each constraint
% found to be redundant,
@@ -4674,7 +5042,7 @@
:- pred type_assign_get_typevarset(type_assign::in,
tvarset::out) is det.
:- pred type_assign_get_head_type_params(type_assign::in,
- headtypes::out) is det.
+ head_type_params::out) is det.
:- pred type_assign_get_type_bindings(type_assign::in,
tsubst::out) is det.
:- pred type_assign_get_typeclass_constraints(type_assign::in,
@@ -4698,7 +5066,7 @@
type_assign::in, type_assign::out) is det.
:- pred type_assign_set_typevarset(tvarset::in,
type_assign::in, type_assign::out) is det.
-:- pred type_assign_set_head_type_params(headtypes::in,
+:- pred type_assign_set_head_type_params(head_type_params::in,
type_assign::in, type_assign::out) is det.
:- pred type_assign_set_type_bindings(tsubst::in,
type_assign::in, type_assign::out) is det.
@@ -5376,6 +5744,9 @@
%-----------------------------------------------------------------------------%
+:- func varnums = bool.
+varnums = yes.
+
:- pred write_type_assign_set(type_assign_set::in, prog_varset::in,
io::di, io::uo) is det.
@@ -5412,7 +5783,7 @@
;
HeadTypeParams = [_ | _],
io__write_string("some [", !IO),
- mercury_output_vars(HeadTypeParams, TypeVarSet, no, !IO),
+ mercury_output_vars(HeadTypeParams, TypeVarSet, varnums, !IO),
io__write_string("]\n\t", !IO)
),
write_type_assign_types(Vars, VarSet, VarTypes, TypeBindings,
@@ -5442,7 +5813,7 @@
;
FoundOne = no
),
- mercury_output_var(Var, VarSet, no, !IO),
+ mercury_output_var(Var, VarSet, varnums, !IO),
io__write_string(": ", !IO),
write_type_b(Type, TypeVarSet, TypeBindings, !IO),
write_type_assign_types(Vars, VarSet, VarTypes, TypeBindings,
@@ -5456,7 +5827,7 @@
tsubst::in, tvarset::in, io::di, io::uo) is det.
write_type_assign_constraints(Constraints, TypeBindings, TypeVarSet, !IO) :-
- Constraints = constraints(ConstraintsToProve, AssumedConstraints),
+ Constraints = constraints(ConstraintsToProve, AssumedConstraints, _),
write_type_assign_constraints("&", AssumedConstraints,
TypeBindings, TypeVarSet, no, !IO),
write_type_assign_constraints("<=", ConstraintsToProve,
@@ -5477,9 +5848,8 @@
),
apply_rec_subst_to_constraint(TypeBindings, Constraint,
BoundConstraint),
- AppendVarNums = no,
retrieve_prog_constraint(BoundConstraint, ProgConstraint),
- mercury_output_constraint(TypeVarSet, AppendVarNums, ProgConstraint,
+ mercury_output_constraint(TypeVarSet, varnums, ProgConstraint,
!IO),
write_type_assign_constraints(Operator, Constraints, TypeBindings,
TypeVarSet, yes, !IO).
@@ -5499,7 +5869,7 @@
write_type_b(Type, TypeVarSet, TypeBindings, !IO) :-
term__apply_rec_substitution(Type, TypeBindings, Type2),
strip_builtin_qualifiers_from_type(Type2, Type3),
- mercury_output_term(Type3, TypeVarSet, no, !IO).
+ mercury_output_term(Type3, TypeVarSet, varnums, !IO).
:- func typestuff_to_typestr(type_stuff) = string.
@@ -6137,11 +6507,11 @@
report_cons_error(Context, ConsError, !IO) :-
(
ConsError = foreign_type_constructor(TypeName - TypeArity, _),
- TNA = describe_sym_name_and_arity(TypeName / TypeArity),
Pieces = [words("There are"),
fixed("`:- pragma foreign_type'"),
words("declarations for type"),
- fixed(TNA ++ ","),
+ sym_name_and_arity(TypeName / TypeArity),
+ suffix(","),
words("so it is treated as an abstract type"),
words("in all predicates and functions"),
words("which are not implemented"),
@@ -6183,6 +6553,14 @@
fixed("`" ++ ConsIdStr ++ "'.")],
Pieces = Pieces1 ++ Pieces2 ++ Pieces3,
write_error_pieces_not_first_line(DefnContext, 0, Pieces, !IO)
+ ;
+ ConsError = new_on_non_existential_type(TypeCtor),
+ TypeCtor = TypeName - TypeArity,
+ Pieces = [words("Invalid use of `new'"),
+ words("on a constructor of type"),
+ sym_name_and_arity(TypeName / TypeArity),
+ words("which is not existentially typed.")],
+ write_error_pieces_not_first_line(Context, 0, Pieces, !IO)
).
:- pred report_wrong_arity_constructor(sym_name::in, arity::in, list(int)::in,
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list