for review: more existential types stuff
Fergus Henderson
fjh at cs.mu.OZ.AU
Wed Jun 17 02:52:51 AEST 1998
DJ, can you please review this one too?
I'm going to commit this on the `existential_types' branch for now.
--------------------
Estimated hours taken: 20
Improve the support for existential types in the following ways:
1. Fix several bugs related to existentially typed predicates
(a bug with type inference, a bug with quantification of type_infos,
and some problems with the code generated by polymorphism.m to
construct type_infos).
2. Allow mixing of type classes and existential typed predicates/functions,
by adding support for existentially quantified type class constraints.
Existentially quantified constraints are introduced with `&' instead
of `<=', and should apply only to existentially quantified type variables.
(XXX this is not yet checked.)
3. Make a start towards allowing existentially typed data types.
The compiler now accepts quantifiers on type definitions, and
type checks them accordingly (XXX assuming all functor occurrences are
deconstructors, not constructors). But there's no special handling
for them in polymorphism.m, so it will abort and/or generate
incorrect code. Also type class constraints are not yet allowed.
There are still some bugs in the handling of inlining, specialization,
etc. for existentially typed predicates which this change does not fix.
compiler/polymorphism.m:
Lots of changes to support existentially quantified
type class constraints.
Also some changes to make the code more maintainable:
- add access predicates for the `poly_info' type,
and modify the code to use them.
- split up polymorphism__process_proc into several subroutines.
compiler/prog_data.m:
Add a new type `class_constraints', which holds two different
lists of constraints, namely the existentially quantified constraints
and the universally quantified ones.
Add a new field to the `constructor' data type (formerly just a pair)
to hold the existentially quantified type variables.
(TODO: add another field to hold the class constraints on those
type variables. I should have done that at the same time.)
compiler/prog_io.m:
Add code to parse the new constructs.
compiler/typecheck.m:
Fix a bug in the inference of which type variables are
existentially quantified. Ensure that we keep iterating
type inference if the set of existentially quantified type
variables changes.
Modify the code to support existentially quantified type class
constraints.
compiler/equiv_type.m:
compiler/make_hlds.m:
compiler/make_tags.m:
compiler/mercury_to_goedel.m:
compiler/mercury_to_mercury.m:
compiler/mode_util.m:
compiler/module_qual.m:
compiler/term_util.m:
compiler/type_util.m:
compiler/unify_proc.m:
Trivial changes to handle the new field in the `constructor' type.
compiler/check_typeclass.m:
compiler/dnf.m:
compiler/equiv_type.m:
compiler/hlds_pred.m:
compiler/lambda.m:
compiler/make_hlds.m:
compiler/mercury_to_mercury.m:
compiler/module_qual.m:
compiler/type_util.m:
Various minor changes to reflect the fact that class
constraints are now a pair of lists (for the universally
and existentially quantified constraints) rather than
a single list.
compiler/hlds_data.m:
Add a new field to hlds_cons_defn to hold the existentially
quantified type variables.
compiler/base_type_layout.m:
compiler/hlds_out.m:
compiler/make_hlds.m:
compiler/type_util.m:
compiler/typecheck.m:
Trivial changes to handle the new field in hlds_cons_defn.
compiler/goal_util.m:
compiler/polymorphism.m:
compiler/hlds_pred.m:
compiler/lambda.m:
Include type_infos for existentially quantified type variables
in the set of extra type_info variables computed by
goal_util__extra_type_info_vars.
Index: compiler/base_type_layout.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/base_type_layout.m,v
retrieving revision 1.30
diff -u -r1.30 base_type_layout.m
--- base_type_layout.m 1998/05/25 21:48:45 1.30
+++ base_type_layout.m 1998/06/06 17:31:07
@@ -1218,9 +1218,9 @@
(
map__search(ConsTable, ConsId, HldsConsList),
list__filter(lambda([X::in] is semidet, (
- X = hlds_cons_defn(_, TypeId, _))),
+ X = hlds_cons_defn(_, _, TypeId, _))),
HldsConsList,
- [hlds_cons_defn(TypeArgs0, _, _)])
+ [hlds_cons_defn(_, TypeArgs0, _, _)])
->
TypeArgs = TypeArgs0
;
Index: compiler/check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.9.2.1
diff -u -r1.9.2.1 check_typeclass.m
--- check_typeclass.m 1998/06/06 11:39:28 1.9.2.1
+++ check_typeclass.m 1998/06/08 08:48:13
@@ -161,7 +161,7 @@
arity, % Arity of the method.
list(type), % Expected types of
% arguments.
- list(class_constraint), % Constraints from
+ class_constraints, % Constraints from
% class method.
list(pair(list(mode), determinism)), % Modes and
% determinisms of the
@@ -205,9 +205,10 @@
% declaration, we don't check that constraint... the instance
% declaration itself satisfies it!
(
- ClassContext0 = [_|Tail]
+ ClassContext0 = constraints([_|OtherUnivCs], ExistCs)
->
- ClassContext = Tail
+ UnivCs = OtherUnivCs,
+ ClassContext = constraints(UnivCs, ExistCs)
;
error("check_instance_pred: no constraint on class method")
),
@@ -406,7 +407,7 @@
RenameSubst),
term__apply_substitution_to_list(InstanceTypes0, RenameSubst,
InstanceTypes),
- apply_subst_to_constraints(RenameSubst, InstanceConstraints0,
+ apply_subst_to_constraint_list(RenameSubst, InstanceConstraints0,
InstanceConstraints),
% Work out what the type variables are bound to for this
@@ -419,7 +420,9 @@
% constraints from the class method. This allows an instance
% method to have constraints on it which are part of the
% instance declaration as a whole.
- list__append(InstanceConstraints, ClassContext1, ClassContext),
+ ClassContext1 = constraints(UnivConstraints1, ExistConstraints),
+ list__append(InstanceConstraints, UnivConstraints1, UnivConstraints),
+ ClassContext = constraints(UnivConstraints, ExistConstraints),
Info1 = instance_method_info(ModuleInfo, PredName, PredArity,
ArgTypes, ClassContext, ArgModes, Errors0, ArgTypeVars,
@@ -669,7 +672,7 @@
Subst),
% Make the constraints in terms of the instance variables
- apply_subst_to_constraints(Subst, SuperClasses0, SuperClasses),
+ apply_subst_to_constraint_list(Subst, SuperClasses0, SuperClasses),
% Now handle the class variables
map__apply_to_list(ClassVars0, Subst, ClassVarTerms),
@@ -694,7 +697,7 @@
typecheck__reduce_context_by_rule_application(InstanceTable,
SuperClassTable, InstanceConstraints, TypeSubst,
InstanceVarSet1, InstanceVarSet2,
- Proofs0, Proofs1, SuperClasses,
+ Proofs0, Proofs1, SuperClasses,
[])
->
Errors = Errors0,
Index: compiler/dnf.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dnf.m,v
retrieving revision 1.30
diff -u -r1.30 dnf.m
--- dnf.m 1998/04/27 04:00:55 1.30
+++ dnf.m 1998/06/06 18:59:59
@@ -157,7 +157,7 @@
:- type dnf_info ---> dnf_info(
tvarset,
map(var, type),
- list(class_constraint),
+ class_constraints,
varset,
pred_markers,
map(tvar, type_info_locn),
Index: compiler/equiv_type.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/equiv_type.m,v
retrieving revision 1.15.2.1
diff -u -r1.15.2.1 equiv_type.m
--- equiv_type.m 1998/06/06 11:39:32 1.15.2.1
+++ equiv_type.m 1998/06/06 17:32:51
@@ -147,7 +147,7 @@
typeclass(Constraints, ClassName, Vars,
ClassInterface, VarSet),
no) :-
- equiv_type__replace_in_class_constraints(Constraints0, VarSet0,
+ equiv_type__replace_in_class_constraint_list(Constraints0, VarSet0,
EqvMap, Constraints, VarSet),
equiv_type__replace_in_class_interface(ClassInterface0,
EqvMap, ClassInterface).
@@ -159,7 +159,7 @@
instance(Constraints, ClassName, Ts,
InstanceInterface, VarSet),
no) :-
- equiv_type__replace_in_class_constraints(Constraints0, VarSet0,
+ equiv_type__replace_in_class_constraint_list(Constraints0, VarSet0,
EqvMap, Constraints, VarSet1),
equiv_type__replace_in_type_list(Ts0, VarSet1, EqvMap, Ts, VarSet, _).
@@ -184,16 +184,29 @@
%-----------------------------------------------------------------------------%
-:- pred equiv_type__replace_in_class_constraints(list(class_constraint),
- varset, eqv_map, list(class_constraint), varset).
+:- pred equiv_type__replace_in_class_constraints(class_constraints,
+ varset, eqv_map, class_constraints, varset).
:- mode equiv_type__replace_in_class_constraints(in, in, in, out, out) is det.
-equiv_type__replace_in_class_constraints([], VarSet, _, [], VarSet).
-equiv_type__replace_in_class_constraints([C0|C0s], VarSet0, EqvMap,
+equiv_type__replace_in_class_constraints(Cs0, VarSet0, EqvMap, Cs, VarSet) :-
+ Cs0 = constraints(UnivCs0, ExistCs0),
+ Cs = constraints(UnivCs, ExistCs),
+ equiv_type__replace_in_class_constraint_list(UnivCs0, VarSet0, EqvMap,
+ UnivCs, VarSet1),
+ equiv_type__replace_in_class_constraint_list(ExistCs0, VarSet1, EqvMap,
+ ExistCs, VarSet).
+
+:- pred equiv_type__replace_in_class_constraint_list(list(class_constraint),
+ varset, eqv_map, list(class_constraint), varset).
+:- mode equiv_type__replace_in_class_constraint_list(in, in, in, out, out)
+ is det.
+
+equiv_type__replace_in_class_constraint_list([], VarSet, _, [], VarSet).
+equiv_type__replace_in_class_constraint_list([C0|C0s], VarSet0, EqvMap,
[C|Cs], VarSet) :-
equiv_type__replace_in_class_constraint(C0, VarSet0, EqvMap, C,
VarSet1),
- equiv_type__replace_in_class_constraints(C0s, VarSet1, EqvMap, Cs,
+ equiv_type__replace_in_class_constraint_list(C0s, VarSet1, EqvMap, Cs,
VarSet).
:- pred equiv_type__replace_in_class_constraint(class_constraint, varset,
@@ -284,8 +297,8 @@
constructor, tvarset).
:- mode equiv_type__replace_in_ctor(in, in, in, out, out) is det.
-equiv_type__replace_in_ctor(TName - Targs0, VarSet0, EqvMap,
- TName - Targs, VarSet) :-
+equiv_type__replace_in_ctor(ctor(ExistQVars, TName, Targs0), VarSet0, EqvMap,
+ ctor(ExistQVars, TName, Targs), VarSet) :-
equiv_type__replace_in_ctor_arg_list(Targs0, VarSet0, EqvMap,
Targs, VarSet, _).
Index: compiler/goal_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/goal_util.m,v
retrieving revision 1.45
diff -u -r1.45 goal_util.m
--- goal_util.m 1998/04/27 04:00:58 1.45
+++ goal_util.m 1998/06/16 13:25:24
@@ -70,17 +70,17 @@
%
% A type-info variable may be non-local to a goal if any of
% the ordinary non-local variables for that goal are
- % polymorphically typed with a type that depends on that
- % type-info variable.
+ % polymorphically or existentially typed with a type
+ % that depends on that type-info variable.
%
% In addition, a typeclass-info may be non-local to a goal if
% any of the non-local variables for that goal are
- % polymorphically typed and are constrained by the typeclass
- % constraints for that typeclass-info variable.
+ % polymorphically or existentially typed and are constrained
+ % by the typeclass constraints for that typeclass-info variable.
%
-:- pred goal_util__extra_nonlocal_typeinfos(map(var, type_info_locn),
- map(var, type), hlds_goal, set(var)).
-:- mode goal_util__extra_nonlocal_typeinfos(in, in, in, out) is det.
+:- pred goal_util__extra_nonlocal_typeinfos(map(tvar, type_info_locn),
+ map(var, type), existq_tvars, hlds_goal, set(var)).
+:- mode goal_util__extra_nonlocal_typeinfos(in, in, in, in, out) is det.
% See whether the goal is a branched structure.
:- pred goal_util__goal_is_branched(hlds_goal_expr).
@@ -520,7 +520,7 @@
%-----------------------------------------------------------------------------%
-goal_util__extra_nonlocal_typeinfos(TypeVarMap, VarTypes,
+goal_util__extra_nonlocal_typeinfos(TypeVarMap, VarTypes, ExistQVars,
Goal0, NonLocalTypeInfos) :-
Goal0 = _ - GoalInfo0,
goal_info_get_nonlocals(GoalInfo0, NonLocals),
@@ -530,8 +530,10 @@
% Find all the type-infos and typeclass-infos that are
% non-local
solutions_set(lambda([Var::out] is nondet, (
- list__member(TheVar, NonLocalTypeVars),
- map__search(TypeVarMap, TheVar, Location),
+ ( list__member(TypeVar, NonLocalTypeVars)
+ ; list__member(TypeVar, ExistQVars)
+ ),
+ map__search(TypeVarMap, TypeVar, Location),
type_info_locn_var(Location, Var)
)), NonLocalTypeInfos).
Index: compiler/hlds_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_data.m,v
retrieving revision 1.24
diff -u -r1.24 hlds_data.m
--- hlds_data.m 1998/05/15 07:07:07 1.24
+++ hlds_data.m 1998/06/06 16:55:34
@@ -49,7 +49,9 @@
:- type hlds_cons_defn
---> hlds_cons_defn(
- % maybe add tvarset?
+ % maybe add tvarset here?
+ % you can get the tvarset from the hlds__type_defn.
+ existq_tvars,
list(type), % The types of the arguments
% of this functor (if any)
type_id, % The result type, i.e. the
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.193.2.1
diff -u -r1.193.2.1 hlds_out.m
--- hlds_out.m 1998/06/06 11:39:36 1.193.2.1
+++ hlds_out.m 1998/06/06 18:36:48
@@ -1939,7 +1939,8 @@
:- pred hlds_out__write_constructor(tvarset, constructor, io__state, io__state).
:- mode hlds_out__write_constructor(in, in, di, uo) is det.
-hlds_out__write_constructor(Tvarset, Name - Args) -->
+hlds_out__write_constructor(Tvarset, ctor(ExistQVars, Name, Args)) -->
+ mercury_output_quantifier(Tvarset, ExistQVars),
prog_out__write_sym_name(Name),
( { Args = [Arg | Rest] } ->
io__write_char('('),
Index: compiler/hlds_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_pred.m,v
retrieving revision 1.48.2.1
diff -u -r1.48.2.1 hlds_pred.m
--- hlds_pred.m 1998/06/06 11:39:37 1.48.2.1
+++ hlds_pred.m 1998/06/16 13:24:15
@@ -266,7 +266,7 @@
% call the created predicate.
:- pred hlds_pred__define_new_pred(hlds_goal, hlds_goal, list(var),
instmap, string, tvarset, map(var, type),
- list(class_constraint), map(tvar, type_info_locn),
+ class_constraints, map(tvar, type_info_locn),
map(class_constraint, var), varset, pred_markers,
module_info, module_info, pred_proc_id).
:- mode hlds_pred__define_new_pred(in, out, in, in, in, in, in,
@@ -277,14 +277,14 @@
:- pred pred_info_init(module_name, sym_name, arity, tvarset, existq_tvars,
list(type), condition, term__context, clauses_info, import_status,
- pred_markers, goal_type, pred_or_func, list(class_constraint),
+ pred_markers, goal_type, pred_or_func, class_constraints,
map(class_constraint, constraint_proof), pred_info).
:- mode pred_info_init(in, in, in, in, in, in, in, in, in, in, in, in, in,
in, in, out) is det.
:- pred pred_info_create(module_name, sym_name, tvarset, existq_tvars,
list(type), condition, term__context, import_status, pred_markers,
- pred_or_func, list(class_constraint), proc_info, proc_id, pred_info).
+ pred_or_func, class_constraints, proc_info, proc_id, pred_info).
:- mode pred_info_create(in, in, in, in, in, in, in, in, in, in, in, in,
out, out) is det.
@@ -397,11 +397,10 @@
:- pred pred_info_get_is_pred_or_func(pred_info, pred_or_func).
:- mode pred_info_get_is_pred_or_func(in, out) is det.
-:- pred pred_info_get_class_context(pred_info, list(class_constraint)).
+:- pred pred_info_get_class_context(pred_info, class_constraints).
:- mode pred_info_get_class_context(in, out) is det.
-:- pred pred_info_set_class_context(pred_info, list(class_constraint),
- pred_info).
+:- pred pred_info_set_class_context(pred_info, class_constraints, pred_info).
:- mode pred_info_set_class_context(in, in, out) is det.
:- pred pred_info_get_constraint_proofs(pred_info,
@@ -505,7 +504,7 @@
pred_markers, % various boolean flags
pred_or_func, % whether this "predicate" was really
% a predicate or a function
- list(class_constraint),
+ class_constraints,
% the class constraints on the
% predicate
map(class_constraint, constraint_proof),
@@ -802,6 +801,10 @@
goal_info_get_instmap_delta(GoalInfo, InstMapDelta),
instmap__apply_instmap_delta(InstMap0, InstMapDelta, InstMap),
+ % XXX The set of existentially quantified type variables
+ % here might not be correct.
+ ExistQVars = [],
+
% If typeinfo_liveness is set, all type_infos for the argument
% variables need to be passed in, not just the ones that are used.
module_info_globals(ModuleInfo0, Globals),
@@ -809,7 +812,7 @@
TypeInfoLiveness),
( TypeInfoLiveness = yes ->
goal_util__extra_nonlocal_typeinfos(TVarMap, VarTypes0,
- Goal0, ExtraTypeInfos0),
+ ExistQVars, Goal0, ExtraTypeInfos0),
set__delete_list(ExtraTypeInfos0, ArgVars0, ExtraTypeInfos),
set__to_sorted_list(ExtraTypeInfos, ExtraArgs),
list__append(ExtraArgs, ArgVars0, ArgVars)
@@ -845,10 +848,6 @@
Detism, Goal0, Context, TVarMap, TCVarMap, ArgsMethod,
ProcInfo0),
proc_info_set_maybe_termination_info(ProcInfo0, TermInfo, ProcInfo),
-
- % XXX The set of existentially quantified type variables
- % here might not be correct.
- ExistQVars = [],
pred_info_create(ModuleName, SymName, TVarSet, ExistQVars, ArgTypes,
true, Context, local, Markers, predicate, ClassContext,
Index: compiler/lambda.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/lambda.m,v
retrieving revision 1.42.2.1
diff -u -r1.42.2.1 lambda.m
--- lambda.m 1998/06/06 11:39:40 1.42.2.1
+++ lambda.m 1998/06/16 13:23:24
@@ -48,7 +48,7 @@
:- pred lambda__transform_lambda(pred_or_func, string, list(var), list(mode),
determinism, list(var), set(var), hlds_goal, unification,
- varset, map(var, type), list(class_constraint), tvarset,
+ varset, map(var, type), class_constraints, tvarset,
map(tvar, type_info_locn), map(class_constraint, var),
module_info, unify_rhs, unification, module_info).
:- mode lambda__transform_lambda(in, in, in, in, in, in, in, in, in, in, in,
@@ -68,7 +68,7 @@
lambda_info(
varset, % from the proc_info
map(var, type), % from the proc_info
- list(class_constraint), % from the pred_info
+ class_constraints, % from the pred_info
tvarset, % from the proc_info
map(tvar, type_info_locn),
% from the proc_info
@@ -238,7 +238,8 @@
Unification0, Functor, Unification, LambdaInfo0, LambdaInfo) :-
LambdaInfo0 = lambda_info(VarSet, VarTypes, Constraints, TVarSet,
TVarMap, TCVarMap, POF, PredName, ModuleInfo0),
- goal_util__extra_nonlocal_typeinfos(TVarMap, VarTypes,
+ ExistQVars = [],
+ goal_util__extra_nonlocal_typeinfos(TVarMap, VarTypes, ExistQVars,
LambdaGoal, ExtraTypeInfos),
lambda__transform_lambda(PredOrFunc, PredName, Vars, Modes, Det,
OrigNonLocals0, ExtraTypeInfos, LambdaGoal, Unification0,
@@ -355,9 +356,9 @@
goal_info_get_context(LambdaGoalInfo, LambdaContext),
% The TVarSet is a superset of what it really ought be,
% but that shouldn't matter.
- % Currently lambda expressions are always monomorphic
- % in Mercury, so there are no existentially quantified
- % type variables (no universally quantified tvars either).
+ % Currently we don't allow existentially typed lambda
+ % expressions (we can change this if/when we allow
+ % `in' modes for existentially typed arguments)
ExistQVars = [],
lambda__uni_modes_to_modes(UniModes1, OrigArgModes),
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.265.2.1
diff -u -r1.265.2.1 make_hlds.m
--- make_hlds.m 1998/06/06 11:39:41 1.265.2.1
+++ make_hlds.m 1998/06/06 19:01:37
@@ -1140,10 +1140,11 @@
:- mode ctors_add(in, in, in, in, in, out, di, uo) is det.
ctors_add([], _TypeId, _NeedQual, _Context, Ctors, Ctors) --> [].
-ctors_add([Name - Args | Rest], TypeId, NeedQual, Context, Ctors0, Ctors) -->
+ctors_add([Ctor | Rest], TypeId, NeedQual, Context, Ctors0, Ctors) -->
+ { Ctor = ctor(ExistQVars, Name, Args) },
{ make_cons_id(Name, Args, TypeId, QualifiedConsId) },
{ assoc_list__values(Args, Types) },
- { ConsDefn = hlds_cons_defn(Types, TypeId, Context) },
+ { ConsDefn = hlds_cons_defn(ExistQVars, Types, TypeId, Context) },
(
{ map__search(Ctors0, QualifiedConsId, QualifiedConsDefns0) }
->
@@ -1153,7 +1154,7 @@
),
(
{ list__member(OtherConsDefn, QualifiedConsDefns1) },
- { OtherConsDefn = hlds_cons_defn(_, TypeId, _) }
+ { OtherConsDefn = hlds_cons_defn(_, _, TypeId, _) }
->
% XXX we should record each error using module_info_incr_errors
io__stderr_stream(StdErr),
@@ -1207,8 +1208,7 @@
:- pred module_add_pred(module_info, varset, existq_tvars, sym_name,
list(type_and_mode), maybe(determinism), condition, purity,
- list(class_constraint),
- pred_markers, term__context, item_status,
+ class_constraints, pred_markers, term__context, item_status,
maybe(pair(pred_id, proc_id)), module_info,
io__state, io__state).
:- mode module_add_pred(in, in, in, in, in, in, in, in, in, in, in, in,
@@ -1243,7 +1243,7 @@
:- pred module_add_func(module_info, varset, existq_tvars, sym_name,
list(type_and_mode),
type_and_mode, maybe(determinism), condition, purity,
- list(class_constraint), pred_markers, term__context,
+ class_constraints, pred_markers, term__context,
item_status, maybe(pair(pred_id, proc_id)),
module_info, io__state, io__state).
:- mode module_add_func(in, in, in, in, in, in, in, in, in, in, in, in, in, out, out, di, uo) is det.
@@ -1376,7 +1376,9 @@
{ Method = pred(VarSet, ExistQVars, PredName, TypesAndModes,
MaybeDet, Cond, ClassContext, Context) },
{ term__var_list_to_term_list(Vars, VarTerms) },
- { NewClassContext = [constraint(Name, VarTerms)|ClassContext] },
+ { ClassContext = constraints(UnivCnstrs, ExistCnstrs) },
+ { NewUnivCnstrs = [constraint(Name, VarTerms) | UnivCnstrs] },
+ { NewClassContext = constraints(NewUnivCnstrs, ExistCnstrs) },
{ init_markers(Markers0) },
{ add_marker(Markers0, class_method, Markers) },
module_add_pred(Module0, VarSet, ExistQVars, PredName,
@@ -1387,7 +1389,9 @@
RetTypeAndMode, MaybeDet, Cond, ClassContext,
Context) },
{ term__var_list_to_term_list(Vars, VarTerms) },
- { NewClassContext = [constraint(Name, VarTerms)|ClassContext] },
+ { ClassContext = constraints(UnivCnstrs, ExistCnstrs) },
+ { NewUnivCnstrs = [constraint(Name, VarTerms) | UnivCnstrs] },
+ { NewClassContext = constraints(NewUnivCnstrs, ExistCnstrs) },
{ init_markers(Markers0) },
{ add_marker(Markers0, class_method, Markers) },
module_add_func(Module0, VarSet, ExistQVars, FuncName,
@@ -1503,7 +1507,7 @@
%-----------------------------------------------------------------------------%
:- pred add_new_pred(module_info, tvarset, existq_tvars, sym_name, list(type),
- condition, purity, list(class_constraint), pred_markers,
+ condition, purity, class_constraints, pred_markers,
term__context, import_status, need_qualifier, pred_or_func,
module_info, io__state, io__state).
:- mode add_new_pred(in, in, in, in, in, in, in, in, in, in, in, in, in, out,
@@ -1724,7 +1728,7 @@
init_markers(Markers),
% XXX If/when we have "comparable" or "unifiable" typeclasses,
% XXX this context might not be empty
- ClassContext = [],
+ ClassContext = constraints([], []),
ExistQVars = [],
pred_info_init(ModuleName, PredName, Arity, TVarSet, ExistQVars,
ArgTypes, Cond, Context, ClausesInfo0, Status, Markers,
@@ -1883,7 +1887,7 @@
map__init(Proofs),
% The class context is empty since this is an implicit
% definition. Inference will fill it in.
- ClassContext = [],
+ ClassContext = constraints([], []),
% We assume none of the arguments are existentially typed.
% Existential types must be declared, they won't be inferred.
ExistQVars = [],
Index: compiler/make_tags.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_tags.m,v
retrieving revision 1.27
diff -u -r1.27 make_tags.m
--- make_tags.m 1998/03/03 17:35:02 1.27
+++ make_tags.m 1998/06/06 17:35:46
@@ -108,7 +108,8 @@
:- mode assign_enum_constants(in, in, in, out) is det.
assign_enum_constants([], _, CtorTags, CtorTags).
-assign_enum_constants([Name - Args | Rest], Val, CtorTags0, CtorTags) :-
+assign_enum_constants([ctor(_ExistQVars, Name, Args) | Rest], Val,
+ CtorTags0, CtorTags) :-
create_cons_id(Name, Args, ConsId),
Tag = int_constant(Val),
map__set(CtorTags0, ConsId, Tag, CtorTags1),
@@ -144,12 +145,13 @@
:- mode assign_simple_tags(in, in, in, in, out) is det.
assign_simple_tags([], _, _, CtorTags, CtorTags).
-assign_simple_tags([Name - Args | Rest], Val, MaxTag, CtorTags0, CtorTags) :-
+assign_simple_tags([Ctor | Rest], Val, MaxTag, CtorTags0, CtorTags) :-
+ Ctor = ctor(_ExistQVars, Name, Args),
create_cons_id(Name, Args, ConsId),
% if we're about to run out of simple tags, start assigning
% complicated tags instead
( Val = MaxTag, Rest \= [] ->
- assign_complicated_tags([Name - Args | Rest], MaxTag, 0,
+ assign_complicated_tags([Ctor | Rest], MaxTag, 0,
CtorTags0, CtorTags)
;
Tag = simple_tag(Val),
@@ -163,8 +165,9 @@
:- mode assign_complicated_tags(in, in, in, in, out) is det.
assign_complicated_tags([], _, _, CtorTags, CtorTags).
-assign_complicated_tags([Name - Args | Rest], PrimaryVal, SecondaryVal,
+assign_complicated_tags([Ctor | Rest], PrimaryVal, SecondaryVal,
CtorTags0, CtorTags) :-
+ Ctor = ctor(_ExistQVars, Name, Args),
create_cons_id(Name, Args, ConsId),
Tag = complicated_tag(PrimaryVal, SecondaryVal),
map__set(CtorTags0, ConsId, Tag, CtorTags1),
@@ -177,8 +180,9 @@
:- mode assign_complicated_constant_tags(in, in, in, in, out) is det.
assign_complicated_constant_tags([], _, _, CtorTags, CtorTags).
-assign_complicated_constant_tags([Name - Args | Rest], PrimaryVal,
- SecondaryVal, CtorTags0, CtorTags) :-
+assign_complicated_constant_tags([Ctor | Rest], PrimaryVal, SecondaryVal,
+ CtorTags0, CtorTags) :-
+ Ctor = ctor(_ExistQVars, Name, Args),
create_cons_id(Name, Args, ConsId),
Tag = complicated_constant_tag(PrimaryVal, SecondaryVal),
map__set(CtorTags0, ConsId, Tag, CtorTags1),
@@ -200,7 +204,7 @@
:- mode ctors_are_all_constants(in) is semidet.
ctors_are_all_constants([]).
-ctors_are_all_constants([_Name - Args | Rest]) :-
+ctors_are_all_constants([ctor(_ExistQVars, _Name, Args) | Rest]) :-
Args = [],
ctors_are_all_constants(Rest).
@@ -212,7 +216,7 @@
split_constructors([], [], []).
split_constructors([Ctor | Ctors], Constants, Functors) :-
- Ctor = _Name - Args,
+ Ctor = ctor(_ExistQVars, _Name, Args),
( Args = [] ->
Constants = [Ctor | Constants0],
Functors = Functors0
Index: compiler/mercury_to_goedel.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_goedel.m,v
retrieving revision 1.63.2.1
diff -u -r1.63.2.1 mercury_to_goedel.m
--- mercury_to_goedel.m 1998/06/06 11:39:44 1.63.2.1
+++ mercury_to_goedel.m 1998/06/06 17:38:28
@@ -332,9 +332,10 @@
:- mode goedel_output_ctors(in, in, in, di, uo) is det.
goedel_output_ctors([], _, _) --> [].
-goedel_output_ctors([Name - Args | Ctors], Type, VarSet) -->
- { unqualify_name(Name, Name2),
- convert_functor_name(Name2, Name3) },
+goedel_output_ctors([Ctor | Ctors], Type, VarSet) -->
+ { Ctor = ctor(_ExistQVars, Name, Args) },
+ { unqualify_name(Name, Name2) },
+ { convert_functor_name(Name2, Name3) },
(
{ Args = [_ArgName - ArgType | Rest] }
->
@@ -461,7 +462,7 @@
goedel_output_func_type(VarSet, FuncName, Types, RetType, _Context) -->
{ list__map(lambda([Type::in, Arg::out] is det, (Arg = "" - Type)),
Types, Args) },
- goedel_output_ctors([FuncName - Args], RetType, VarSet).
+ goedel_output_ctors([ctor([], FuncName, Args)], RetType, VarSet).
%-----------------------------------------------------------------------------%
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.136.2.1
diff -u -r1.136.2.1 mercury_to_mercury.m
--- mercury_to_mercury.m 1998/06/06 11:39:45 1.136.2.1
+++ mercury_to_mercury.m 1998/06/06 19:01:56
@@ -32,13 +32,13 @@
:- mode convert_to_mercury(in, in, in, di, uo) is det.
:- pred mercury_output_pred_type(tvarset, existq_tvars, sym_name, list(type),
- maybe(determinism), purity, list(class_constraint),
+ maybe(determinism), purity, class_constraints,
term__context, io__state, io__state).
:- mode mercury_output_pred_type(in, in, in, in, in, in, in, in, di, uo) is det.
:- pred mercury_output_func_type(tvarset, existq_tvars, sym_name,
list(type), type,
- maybe(determinism), purity, list(class_constraint),
+ maybe(determinism), purity, class_constraints,
term__context, io__state, io__state).
:- mode mercury_output_func_type(in, in, in, in, in, in, in, in, in,
di, uo) is det.
@@ -170,6 +170,10 @@
io__state, io__state).
:- mode mercury_output_constraint(in, in, di, uo) is det.
+ % output an existential quantifier
+:- pred mercury_output_quantifier(tvarset, existq_tvars, io__state, io__state).
+:- mode mercury_output_quantifier(in, in, di, uo) is det.
+
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -369,14 +373,7 @@
),
io__write_char(')'),
- (
- { Constraints = [] }
- ;
- { Constraints = [_|_] },
- io__write_string(" <= ("),
- output_class_constraints(Constraints, VarSet),
- io__write_string(")")
- ),
+ mercury_output_class_constraint_list(Constraints, VarSet, "<="),
io__write_string(" where [\n"),
@@ -396,14 +393,7 @@
io__write_char(')'),
io__write_char(')'),
- (
- { Constraints = [] }
- ;
- { Constraints = [_|_] },
- io__write_string(" <= ("),
- output_class_constraints(Constraints, VarSet),
- io__write_string(")")
- ),
+ mercury_output_class_constraint_list(Constraints, VarSet, "<="),
io__write_string(" where [\n"),
@@ -412,21 +402,6 @@
io__write_string("\n].\n").
%-----------------------------------------------------------------------------%
-:- pred output_class_constraints(list(class_constraint), varset,
- io__state, io__state).
-:- mode output_class_constraints(in, in, di, uo) is det.
-
-output_class_constraints(Constraints, VarSet) -->
- io__write_list(Constraints, ", ", output_class_constraint(VarSet)).
-
-:- pred output_class_constraint(varset, class_constraint, io__state, io__state).
-:- mode output_class_constraint(in, in, di, uo) is det.
-
-output_class_constraint(VarSet, constraint(Name, Types)) -->
- mercury_output_sym_name(Name),
- io__write_char('('),
- io__write_list(Types, ", ", term_io__write_term(VarSet)),
- io__write_char(')').
:- pred output_class_methods(list(class_method), io__state, io__state).
:- mode output_class_methods(in, di, uo) is det.
@@ -1177,7 +1152,9 @@
:- mode mercury_output_ctors(in, in, di, uo) is det.
mercury_output_ctors([], _) --> [].
-mercury_output_ctors([Name - Args | Ctors], VarSet) -->
+mercury_output_ctors([Ctor | Ctors], VarSet) -->
+ { Ctor = ctor(ExistQVars, Name, Args) },
+
% we need to quote ';'/2 and '{}'/2
{ list__length(Args, Arity) },
(
@@ -1188,6 +1165,7 @@
;
[]
),
+ mercury_output_quantifier(VarSet, ExistQVars),
(
{ Args = [Arg | Rest] }
->
@@ -1241,7 +1219,7 @@
:- pred mercury_output_pred_decl(tvarset, existq_tvars,
sym_name, list(type_and_mode),
- maybe(determinism), purity, list(class_constraint),
+ maybe(determinism), purity, class_constraints,
term__context, string, string, string, io__state, io__state).
:- mode mercury_output_pred_decl(in, in, in, in, in, in, in, in, in, in, in,
di, uo) is det.
@@ -1272,7 +1250,7 @@
:- pred mercury_output_pred_type_2(tvarset, existq_tvars, sym_name, list(type),
- maybe(determinism), purity, list(class_constraint),
+ maybe(determinism), purity, class_constraints,
term__context, string, string, io__state, io__state).
:- mode mercury_output_pred_type_2(in, in, in, in, in, in, in, in, in, in,
di, uo) is det.
@@ -1326,7 +1304,7 @@
:- pred mercury_output_func_decl(tvarset, existq_tvars, sym_name,
list(type_and_mode), type_and_mode, maybe(determinism),
- purity, list(class_constraint), term__context, string, string,
+ purity, class_constraints, term__context, string, string,
string, io__state, io__state).
:- mode mercury_output_func_decl(in, in, in, in, in, in, in, in, in, in, in,
in, di, uo) is det.
@@ -1359,7 +1337,7 @@
":- ", ".\n").
:- pred mercury_output_func_type_2(varset, existq_tvars, sym_name, list(type),
- type, maybe(determinism), purity, list(class_constraint),
+ type, maybe(determinism), purity, class_constraints,
term__context, string, string, io__state, io__state).
:- mode mercury_output_func_type_2(in, in, in, in, in, in, in, in, in, in, in,
di, uo) is det.
@@ -1390,9 +1368,6 @@
%-----------------------------------------------------------------------------%
-:- pred mercury_output_quantifier(tvarset, list(tvar), io__state, io__state).
-:- mode mercury_output_quantifier(in, in, di, uo) is det.
-
mercury_output_quantifier(VarSet, ExistQVars) -->
( { ExistQVars = [] } ->
[]
@@ -1404,17 +1379,26 @@
%-----------------------------------------------------------------------------%
-:- pred mercury_output_class_context(list(class_constraint), varset,
+:- pred mercury_output_class_context(class_constraints, varset,
io__state, io__state).
:- mode mercury_output_class_context(in, in, di, uo) is det.
mercury_output_class_context(ClassContext, VarSet) -->
+ { ClassContext = constraints(UnivCs, ExistCs) },
+ mercury_output_class_constraint_list(ExistCs, VarSet, "&"),
+ mercury_output_class_constraint_list(UnivCs, VarSet, "<=").
+
+:- pred mercury_output_class_constraint_list(list(class_constraint), varset,
+ string, io__state, io__state).
+:- mode mercury_output_class_constraint_list(in, in, in, di, uo) is det.
+
+mercury_output_class_constraint_list(Constraints, VarSet, Operator) -->
(
- { ClassContext = [] }
+ { Constraints = [] }
;
- { ClassContext = [_|_] },
- io__write_string(" <= ("),
- io__write_list(ClassContext, ", ",
+ { Constraints = [_|_] },
+ io__write_strings([" ", Operator, " ("]),
+ io__write_list(Constraints, ", ",
mercury_output_constraint(VarSet)),
io__write_char(')')
).
Index: compiler/mode_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_util.m,v
retrieving revision 1.109
diff -u -r1.109 mode_util.m
--- mode_util.m 1998/05/25 21:48:50 1.109
+++ mode_util.m 1998/06/06 19:02:50
@@ -761,7 +761,7 @@
constructors_to_bound_insts([], _, _, []).
constructors_to_bound_insts([Ctor | Ctors], Uniq, ModuleInfo,
[BoundInst | BoundInsts]) :-
- Ctor = Name - Args,
+ Ctor = ctor(_ExistQVars, Name, Args),
ctor_arg_list_to_inst_list(Args, Uniq, Insts),
list__length(Insts, Arity),
BoundInst = functor(cons(Name, Arity), Insts),
@@ -819,12 +819,12 @@
(
ConsId = cons(ConsName, Arity),
GetCons = lambda([Ctor::in] is semidet, (
- Ctor = ConsName - CtorArgs,
+ Ctor = ctor(_, ConsName, CtorArgs),
list__length(CtorArgs, Arity)
)),
list__filter(GetCons, Constructors, [Constructor])
->
- Constructor = _ - Args,
+ Constructor = ctor(_ExistQVars, _Name, Args),
GetArgTypes = lambda([CtorArg::in, ArgType::out] is det, (
CtorArg = _ArgName - ArgType
)),
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.36.2.1
diff -u -r1.36.2.1 module_qual.m
--- module_qual.m 1998/06/06 11:39:47 1.36.2.1
+++ module_qual.m 1998/06/06 18:07:12
@@ -336,7 +336,7 @@
{ list__length(Vars, Arity) },
{ Id = Name - Arity },
{ mq_info_set_error_context(Info0, class(Id) - Context, Info1) },
- qualify_class_constraints(Constraints0, Constraints, Info1, Info2),
+ qualify_class_constraint_list(Constraints0, Constraints, Info1, Info2),
qualify_class_interface(Interface0, Interface, Info2, Info).
module_qualify_item(instance(Constraints0, Name0, Types0, Interface0, VarSet) -
@@ -349,7 +349,7 @@
{ mq_info_set_error_context(Info0, instance(Id) - Context, Info1) },
% We don't qualify the implementation yet, since that requires
% us to resolve overloading.
- qualify_class_constraints(Constraints0, Constraints, Info1, Info2),
+ qualify_class_constraint_list(Constraints0, Constraints, Info1, Info2),
qualify_class_name(Id, Name - _, Info2, Info3),
qualify_type_list(Types0, Types, Info3, Info),
{ qualify_instance_interface(Name, Interface0, Interface) }.
@@ -417,8 +417,9 @@
mq_info::in, mq_info::out, io__state::di, io__state::uo) is det.
qualify_constructors([], [], Info, Info) --> [].
-qualify_constructors([SymName - Args0 | Ctors0], [SymName - Args | Ctors],
- Info0, Info) -->
+qualify_constructors([Ctor0 | Ctors0], [Ctor | Ctors], Info0, Info) -->
+ { Ctor0 = ctor(ExistQVars, SymName, Args0) },
+ { Ctor = ctor(ExistQVars, SymName, Args) },
qualify_constructor_arg_list(Args0, Args, Info0, Info1),
qualify_constructors(Ctors0, Ctors, Info1, Info).
@@ -702,14 +703,23 @@
qualify_mode(Mode0, Mode, Info0, Info1),
qualify_pragma_vars(PragmaVars0, PragmaVars, Info1, Info).
-:- pred qualify_class_constraints(list(class_constraint)::in,
+:- pred qualify_class_constraints(class_constraints::in,
+ class_constraints::out, mq_info::in, mq_info::out, io__state::di,
+ io__state::uo) is det.
+
+qualify_class_constraints(constraints(UnivCs0, ExistCs0),
+ constraints(UnivCs, ExistCs), MQInfo0, MQInfo) -->
+ qualify_class_constraint_list(UnivCs0, UnivCs, MQInfo0, MQInfo1),
+ qualify_class_constraint_list(ExistCs0, ExistCs, MQInfo1, MQInfo).
+
+:- pred qualify_class_constraint_list(list(class_constraint)::in,
list(class_constraint)::out, mq_info::in, mq_info::out, io__state::di,
io__state::uo) is det.
-qualify_class_constraints([], [], MQInfo, MQInfo) --> [].
-qualify_class_constraints([C0|C0s], [C|Cs], MQInfo0, MQInfo) -->
+qualify_class_constraint_list([], [], MQInfo, MQInfo) --> [].
+qualify_class_constraint_list([C0|C0s], [C|Cs], MQInfo0, MQInfo) -->
qualify_class_constraint(C0, C, MQInfo0, MQInfo1),
- qualify_class_constraints(C0s, Cs, MQInfo1, MQInfo).
+ qualify_class_constraint_list(C0s, Cs, MQInfo1, MQInfo).
:- pred qualify_class_constraint(class_constraint::in, class_constraint::out,
mq_info::in, mq_info::out, io__state::di, io__state::uo) is det.
Index: compiler/polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.134.2.1
diff -u -r1.134.2.1 polymorphism.m
--- polymorphism.m 1998/06/06 11:39:48 1.134.2.1
+++ polymorphism.m 1998/06/16 15:26:16
@@ -366,8 +366,8 @@
write_proc_progress_message("% Transforming polymorphism for ",
PredId, ProcId, ModuleInfo0, IO0, IO1),
- polymorphism__process_proc(ProcInfo0, PredInfo0, ModuleInfo0,
- ProcInfo, PredInfo1, ModuleInfo1),
+ polymorphism__process_proc(ProcId, ProcInfo0, PredId, PredInfo0,
+ ModuleInfo0, ProcInfo, PredInfo1, ModuleInfo1),
pred_info_procedures(PredInfo1, ProcTable1),
map__det_update(ProcTable1, ProcId, ProcInfo, ProcTable),
@@ -445,60 +445,105 @@
%---------------------------------------------------------------------------%
-:- type poly_info --->
- poly_info(
- varset, % from the proc_info
- map(var, type), % from the proc_info
- tvarset, % from the proc_info
- map(tvar, type_info_locn),
- % specifies the location of
- % the type_info var
- % for each of the pred's type
- % parameters
- map(class_constraint, var),
- % specifies the location of
- % the typeclass_info var
- % for each of the pred's class
- % constraints
- map(class_constraint, constraint_proof),
- % specifies why each constraint
- % that was eliminated from the
- % pred was able to be eliminated
- % (this allows us to efficiently
- % construct the dictionary)
+:- pred polymorphism__process_proc(proc_id, proc_info, pred_id, pred_info,
+ module_info, proc_info, pred_info, module_info).
+:- mode polymorphism__process_proc(in, in, in, in, in, out, out, out) is det.
- % Note that the two maps above
- % are separate since the second
- % is the information calculated
- % by typecheck.m, while the
- % first is the information
- % calculated here in
- % polymorphism.m
+polymorphism__process_proc(ProcId, ProcInfo0, PredId, PredInfo0, ModuleInfo0,
+ ProcInfo, PredInfo, ModuleInfo) :-
+ proc_info_goal(ProcInfo0, Goal0),
+ init_poly_info(ModuleInfo0, PredInfo0, ProcInfo0, Info0),
+ polymorphism__setup_headvars(PredInfo0, ProcInfo0,
+ HeadVars, ArgModes, HeadTypeVars, UnconstrainedTVars,
+ ExtraTypeInfoHeadVars, Info0, Info1),
- string, % pred name
- module_info
- ).
+ (
+ ( pred_info_is_imported(PredInfo0)
+ ; pred_info_is_pseudo_imported(PredInfo0),
+ in_in_unification_proc_id(ProcId)
+ )
+ ->
+ Goal = Goal0,
+ Info = Info1
+ ;
+ %
+ % process any polymorphic calls inside the goal
+ %
+ polymorphism__process_goal(Goal0, Goal1, Info1, Info2),
-:- pred polymorphism__process_proc(proc_info, pred_info, module_info,
- proc_info, pred_info, module_info).
-:- mode polymorphism__process_proc(in, in, in, out, out, out) is det.
+ %
+ % generate code to construct the type-class-infos
+ % and type-infos for existentially quantified type vars
+ %
+ polymorphism__produce_existq_tvars(
+ PredId, PredInfo0, ProcId, ProcInfo0,
+ UnconstrainedTVars, ExtraTypeInfoHeadVars,
+ Goal1, Goal2, Info2, Info3),
+
+ pred_info_get_exist_quant_tvars(PredInfo0, ExistQVars),
+ polymorphism__fixup_quantification(Goal2, ExistQVars, Goal3, _,
+ Info3, Info4),
-polymorphism__process_proc(ProcInfo0, PredInfo0, ModuleInfo0,
- ProcInfo, PredInfo, ModuleInfo) :-
+ %
+ % if there were any existentially quantified type variables,
+ % either in this predicate or in any predicate that it calls,
+ % then we may need to recompute the instmap deltas too
+ %
+ (
+ ExistQVars = [],
+ pred_info_get_head_type_params(PredInfo0,
+ HeadTypeParams),
+ HeadTypeVars = HeadTypeParams
+ ->
+ Goal = Goal3,
+ Info = Info4
+ ;
+ poly_info_get_module_info(Info4, ModuleInfo4),
+ mode_list_get_initial_insts(ArgModes, ModuleInfo4,
+ InitialInsts),
+ assoc_list__from_corresponding_lists(HeadVars,
+ InitialInsts, InstAL),
+ instmap__from_assoc_list(InstAL, InstMap),
+ recompute_instmap_delta(no, Goal3, Goal, InstMap,
+ ModuleInfo4, ModuleInfo5),
+ poly_info_set_module_info(ModuleInfo5, Info4, Info)
+ )
+ ),
+
+ %
+ % set the new values of the fields in proc_info and pred_info
+ %
+ Info = poly_info(VarSet, VarTypes, TypeVarSet,
+ TypeInfoMap, TypeClassInfoMap,
+ _Proofs, _PredName, ModuleInfo),
+ proc_info_set_headvars(ProcInfo0, HeadVars, ProcInfo1),
+ proc_info_set_goal(ProcInfo1, Goal, ProcInfo2),
+ proc_info_set_varset(ProcInfo2, VarSet, ProcInfo3),
+ proc_info_set_vartypes(ProcInfo3, VarTypes, ProcInfo4),
+ proc_info_set_argmodes(ProcInfo4, ArgModes, ProcInfo5),
+ proc_info_set_typeinfo_varmap(ProcInfo5, TypeInfoMap, ProcInfo6),
+ proc_info_set_typeclass_info_varmap(ProcInfo6, TypeClassInfoMap,
+ ProcInfo),
+ pred_info_set_typevarset(PredInfo0, TypeVarSet, PredInfo).
+
+:- pred polymorphism__setup_headvars(pred_info, proc_info,
+ list(var), list(mode), list(tvar), list(tvar), list(var),
+ poly_info, poly_info).
+:- mode polymorphism__setup_headvars(in, in, out, out, out, out, out, in, out)
+ is det.
+
+polymorphism__setup_headvars(PredInfo, ProcInfo, HeadVars, ArgModes,
+ HeadTypeVars, UnconstrainedTVars, ExtraHeadTypeInfoVars,
+ PolyInfo0, PolyInfo) :-
%
% grab the appropriate fields from the pred_info and proc_info
%
- pred_info_arg_types(PredInfo0, ArgTypeVarSet, ExistQVars, ArgTypes),
- pred_info_typevarset(PredInfo0, TypeVarSet0),
- pred_info_get_class_context(PredInfo0, ClassContext),
- pred_info_get_constraint_proofs(PredInfo0, Proofs),
- pred_info_name(PredInfo0, PredName),
- proc_info_headvars(ProcInfo0, HeadVars0),
- proc_info_varset(ProcInfo0, VarSet0),
- proc_info_vartypes(ProcInfo0, VarTypes0),
- proc_info_goal(ProcInfo0, Goal0),
- proc_info_argmodes(ProcInfo0, ArgModes0),
+ pred_info_arg_types(PredInfo, ArgTypeVarSet, ExistQVars, ArgTypes),
+ pred_info_get_class_context(PredInfo, ClassContext),
+ proc_info_headvars(ProcInfo, HeadVars0),
+ proc_info_argmodes(ProcInfo, ArgModes0),
+
%
% Insert extra head variables to hold the address of the
@@ -507,25 +552,29 @@
% (for the type_info) and one variable for each constraint (for
% the typeclass_info).
%
- term__vars_list(ArgTypes, HeadTypeVars0),
+
% Make a fresh variable for each class constraint, returning
% a list of variables that appear in the constraints, along
% with the location of the type infos for them.
- polymorphism__make_typeclass_info_head_vars(ClassContext, ModuleInfo0,
- VarSet0, VarTypes0, ExtraHeadTypeclassInfoVars,
- TypeClassInfoMap, ConstrainedTVars,
- VarSet1, VarTypes1),
+ ClassContext = constraints(UnivConstraints, ExistConstraints),
+ list__append(UnivConstraints, ExistConstraints, AllConstraints),
- list__delete_elems(HeadTypeVars0, ConstrainedTVars,
+ polymorphism__make_typeclass_info_head_vars(AllConstraints,
+ ExtraHeadTypeClassInfoVars, PolyInfo0, PolyInfo1),
+ poly_info_get_type_info_map(PolyInfo1, TypeInfoMap1),
+
+ term__vars_list(ArgTypes, HeadTypeVars),
+ map__keys(TypeInfoMap1, ConstrainedTVars),
+ list__delete_elems(HeadTypeVars, ConstrainedTVars,
UnconstrainedTVars0),
list__remove_dups(UnconstrainedTVars0, UnconstrainedTVars),
polymorphism__make_head_vars(UnconstrainedTVars, ArgTypeVarSet,
- VarSet1, VarTypes1, ExtraHeadTypeInfoVars, VarSet2, VarTypes2),
+ ExtraHeadTypeInfoVars, PolyInfo1, PolyInfo2),
% First the type_infos, then the typeclass_infos,
% but we have to do it in reverse because we're appending...
- list__append(ExtraHeadTypeclassInfoVars, HeadVars0, HeadVars1),
+ list__append(ExtraHeadTypeClassInfoVars, HeadVars0, HeadVars1),
list__append(ExtraHeadTypeInfoVars, HeadVars1, HeadVars),
%
@@ -536,7 +585,7 @@
list__map(polymorphism__typeinfo_mode(ExistQVars),
UnconstrainedTVars, TypeInfoModes),
in_mode(In),
- list__length(ExtraHeadTypeclassInfoVars, NumExtraClassInfoVars),
+ list__length(ExtraHeadTypeClassInfoVars, NumExtraClassInfoVars),
list__duplicate(NumExtraClassInfoVars, In, TypeClassInfoModes),
list__append(TypeClassInfoModes, ArgModes0, ArgModes1),
list__append(TypeInfoModes, ArgModes1, ArgModes),
@@ -549,42 +598,147 @@
AddLocn = lambda([TVarAndVar::in, TIM0::in, TIM::out] is det,
(
TVarAndVar = TVar - TheVar,
- map__det_insert(TIM0, TVar, type_info(TheVar),
- TIM)
+ map__det_insert(TIM0, TVar, type_info(TheVar), TIM)
)),
assoc_list__from_corresponding_lists(UnconstrainedTVars,
- ExtraHeadTypeInfoVars, TVarsAndVars),
- list__foldl(AddLocn, TVarsAndVars, TypeClassInfoMap, TypeInfoMap1),
+ ExtraHeadTypeInfoVars, TVarsAndVars),
+ list__foldl(AddLocn, TVarsAndVars, TypeInfoMap1, TypeInfoMap2),
+
+ poly_info_set_type_info_map(TypeInfoMap2, PolyInfo2, PolyInfo3),
% Make a map of the locations of the typeclass_infos
- map__from_corresponding_lists(ClassContext, ExtraHeadTypeclassInfoVars,
- TypeclassInfoLocations0),
+ map__from_corresponding_lists(AllConstraints,
+ ExtraHeadTypeClassInfoVars, TypeClassInfoMap),
+
+ poly_info_set_typeclass_info_map(TypeClassInfoMap,
+ PolyInfo3, PolyInfo).
- Info0 = poly_info(VarSet2, VarTypes2, TypeVarSet0,
- TypeInfoMap1, TypeclassInfoLocations0,
- Proofs, PredName, ModuleInfo0),
+%
+% generate code to produce the values of type_infos and typeclass_infos
+% for existentially quantified type variables in the head
+%
+:- pred polymorphism__produce_existq_tvars(
+ pred_id, pred_info, proc_id, proc_info,
+ list(tvar), list(var), hlds_goal, hlds_goal,
+ poly_info, poly_info).
+:- mode polymorphism__produce_existq_tvars(in, in, in, in, in, in, in, out,
+ in, out) is det.
+
+polymorphism__produce_existq_tvars(PredId, PredInfo, ProcId, ProcInfo,
+ UnconstrainedTVars, TypeInfoHeadVars,
+ Goal0, Goal, Info0, Info) :-
+ poly_info_get_var_types(Info0, VarTypes0),
+ pred_info_arg_types(PredInfo, _ArgTypeVarSet, ExistQVars, ArgTypes),
+ pred_info_get_class_context(PredInfo, ClassContext),
+ proc_info_headvars(ProcInfo, HeadVars0),
+
+ %
+ % Figure out the bindings for any existentially quantified
+ % type variables in the head.
+ %
+ ClassContext = constraints(_UnivConstraints, ExistConstraints),
+ ( map__is_empty(VarTypes0) ->
+ % this can happen for compiler-generated procedures
+ map__init(TypeSubst)
+ ;
+ map__apply_to_list(HeadVars0, VarTypes0, ActualArgTypes),
+ type_list_subsumes(ArgTypes, ActualArgTypes, ArgTypeSubst)
+ ->
+ TypeSubst = ArgTypeSubst
+ ;
+ % this can happen for unification procedures
+ % of equivalence types
+ % error("polymorphism.m: type_list_subsumes failed")
+ map__init(TypeSubst)
+ ),
+
+ poly_info_get_type_class_info_map(Info0, TypeClassInfoMap0),
+ map__apply_to_list(ExistConstraints, TypeClassInfoMap0,
+ ExistTypeClassInfoHeadVars),
+ map__delete_list(TypeClassInfoMap0, ExistConstraints,
+ TypeClassInfoMap1),
+ poly_info_set_typeclass_info_map(TypeClassInfoMap1, Info0, Info1),
+
+ %
+ % generate code to produce values for any existentially quantified
+ % typeclass-info variables in the head
+ %
+ map__init(Subst),
+ ExistQVarsForCall = [],
+ Goal0 = _ - GoalInfo,
+ goal_info_get_context(GoalInfo, Context),
+ polymorphism__make_typeclass_info_vars(
+ ExistConstraints, Subst, TypeSubst, ExistQVarsForCall, Context,
+ hlds_class_proc(PredId, ProcId),
+ hlds_class_proc(NewPredId, NewProcId),
+ ExistTypeClassVars, ExtraTypeClassGoals,
+ _ExistConstrainedTVars, Info1, Info2),
+ % sanity check
+ ( PredId = NewPredId, ProcId = NewProcId ->
+ true
+ ;
+ error("polymorphism.m: impossible specialization")
+ ),
+ polymorphism__assign_var_list(
+ ExistTypeClassInfoHeadVars, ExistTypeClassVars,
+ ExtraTypeClassUnifyGoals),
+
%
- % process any polymorphic calls inside the goal
+ % figure out the list of universally quantified type variables
%
- polymorphism__process_goal(Goal0, Goal1, Info0, Info1),
- polymorphism__fixup_quantification(Goal1, Goal, _, Info1, Info),
- Info = poly_info(VarSet, VarTypes, TypeVarSet,
- TypeInfoMap, TypeclassInfoLocations,
- _Proofs, _PredName, ModuleInfo),
+ term__vars_list(ArgTypes, HeadTypeVars0),
+ list__remove_dups(HeadTypeVars0, HeadTypeVars),
+ list__delete_elems(HeadTypeVars, ExistQVars, UnivQTVars),
%
- % set the new values of the fields in proc_info and pred_info
- %
- proc_info_set_headvars(ProcInfo0, HeadVars, ProcInfo1),
- proc_info_set_goal(ProcInfo1, Goal, ProcInfo2),
- proc_info_set_varset(ProcInfo2, VarSet, ProcInfo3),
- proc_info_set_vartypes(ProcInfo3, VarTypes, ProcInfo4),
- proc_info_set_argmodes(ProcInfo4, ArgModes, ProcInfo5),
- proc_info_set_typeinfo_varmap(ProcInfo5, TypeInfoMap, ProcInfo6),
- proc_info_set_typeclass_info_varmap(ProcInfo6, TypeclassInfoLocations,
- ProcInfo),
- pred_info_set_typevarset(PredInfo0, TypeVarSet, PredInfo).
+ % apply the type bindings to the unconstrained type variables
+ % to give the actual types, and then generate code
+ % to initialize the type_infos for those types
+ %
+ term__var_list_to_term_list(UnconstrainedTVars,
+ UnconstrainedTVarTerms),
+ term__apply_substitution_to_list(UnconstrainedTVarTerms,
+ TypeSubst, ActualTypes),
+ polymorphism__make_type_info_vars(ActualTypes, UnivQTVars, Context,
+ TypeInfoVars, ExtraTypeInfoGoals, Info2, Info),
+ polymorphism__assign_var_list(TypeInfoHeadVars, TypeInfoVars,
+ ExtraTypeInfoUnifyGoals),
+ list__condense([[Goal0],
+ ExtraTypeClassGoals, ExtraTypeClassUnifyGoals,
+ ExtraTypeInfoGoals, ExtraTypeInfoUnifyGoals],
+ GoalList),
+ conj_list_to_goal(GoalList, GoalInfo, Goal).
+
+:- pred polymorphism__assign_var_list(list(var), list(var), list(hlds_goal)).
+:- mode polymorphism__assign_var_list(in, in, out) is det.
+
+polymorphism__assign_var_list([], [_|_], _) :-
+ error("unify_proc__assign_var_list: length mismatch").
+polymorphism__assign_var_list([_|_], [], _) :-
+ error("unify_proc__assign_var_list: length mismatch").
+polymorphism__assign_var_list([], [], []).
+polymorphism__assign_var_list([Var1 | Vars1], [Var2 | Vars2], [Goal | Goals]) :-
+
+ % Doing just this wouldn't work, because we also need to fill in
+ % the mode and determinism info:
+ % term__context_init(Context),
+ % create_atomic_unification(Var1, var(Var2), Context, explicit,
+ % [], Goal),
+
+ Ground = ground(shared, no),
+ Mode = ((free -> Ground) - (Ground -> Ground)),
+ UnifyInfo = assign(Var1, Var2),
+ UnifyC = unify_context(explicit, []),
+ goal_info_init(GoalInfo0),
+ instmap_delta_from_assoc_list([Var1 - Ground], InstMapDelta),
+ goal_info_set_instmap_delta(GoalInfo0, InstMapDelta, GoalInfo1),
+ goal_info_set_determinism(GoalInfo1, det, GoalInfo2),
+ set__list_to_set([Var1, Var2], NonLocals),
+ goal_info_set_nonlocals(GoalInfo2, NonLocals, GoalInfo),
+ Goal = unify(Var1, var(Var2), Mode, UnifyInfo, UnifyC) - GoalInfo,
+
+ polymorphism__assign_var_list(Vars1, Vars2, Goals).
:- pred polymorphism__process_goal(hlds_goal, hlds_goal,
poly_info, poly_info).
@@ -621,7 +775,8 @@
{ list__length(ArgVars0, Arity) },
{ special_pred_name_arity(SpecialPredId, PredName0,
MangledPredName, Arity) },
- =(poly_info(_, VarTypes, _, _, _, _, _, ModuleInfo)),
+ =(Info0),
+ { poly_info_get_var_types(Info0, VarTypes) },
{ special_pred_get_type(MangledPredName, ArgVars0, MainVar) },
{ map__lookup(VarTypes, MainVar, Type) },
{ Type \= term__variable(_) },
@@ -632,6 +787,7 @@
{ special_pred_list(SpecialPredIds) },
{ list__member(SpecialPredId, SpecialPredIds) }
->
+ { poly_info_get_module_info(Info0, ModuleInfo) },
{ classify_type(Type, ModuleInfo, TypeCategory) },
{ polymorphism__get_special_proc(TypeCategory, Type,
SpecialPredId, ModuleInfo, Name, PredId1, ProcId1) }
@@ -655,7 +811,10 @@
{ Unification = complicated_unify(UniMode, CanFail) },
{ Y = var(YVar) }
->
- =(poly_info(_, VarTypes, _, TypeInfoMap, _, _, _, ModuleInfo)),
+ =(Info0),
+ { poly_info_get_var_types(Info0, VarTypes) },
+ { poly_info_get_type_info_map(Info0, TypeInfoMap) },
+ { poly_info_get_module_info(Info0, ModuleInfo) },
{ map__lookup(VarTypes, XVar, Type) },
( { Type = term__variable(TypeVar) } ->
% Convert polymorphic unifications into calls to
@@ -766,7 +925,10 @@
% lambda goal and then convert the lambda expression
% into a new predicate
polymorphism__process_goal(LambdaGoal0, LambdaGoal1),
- polymorphism__fixup_quantification(LambdaGoal1,
+ % XXX currently we don't allow lambda goals to be
+ % existentially typed
+ { ExistQVars = [] },
+ polymorphism__fixup_quantification(LambdaGoal1, ExistQVars,
LambdaGoal, NonLocalTypeInfos),
polymorphism__process_lambda(PredOrFunc, Vars, Modes,
Det, ArgVars, NonLocalTypeInfos, LambdaGoal,
@@ -811,7 +973,8 @@
% so that the c_code can refer to the type_info variable
% for type T as `TypeInfo_for_T'.
%
- =(poly_info(_, _, _, _, _, _, _, ModuleInfo)),
+ =(Info0),
+ { poly_info_get_module_info(Info0, ModuleInfo) },
{ module_info_pred_info(ModuleInfo, PredId, PredInfo) },
{ pred_info_arg_types(PredInfo, PredTypeVarSet, ExistQVars,
PredArgTypes) },
@@ -913,7 +1076,9 @@
PredId, ProcId, ArgVars, ExtraVars, GoalInfo, ExtraGoals,
Info0, Info) :-
- Info0 = poly_info(A, VarTypes, TypeVarSet0, D, E, F, G, ModuleInfo),
+ poly_info_get_var_types(Info0, VarTypes),
+ poly_info_get_typevarset(Info0, TypeVarSet0),
+ poly_info_get_module_info(Info0, ModuleInfo),
module_info_pred_info(ModuleInfo, PredId0, PredInfo),
pred_info_arg_types(PredInfo, PredTypeVarSet, PredExistQVars0,
@@ -973,23 +1138,34 @@
apply_subst_to_constraints(Subst, PredClassContext0,
PredClassContext),
- Info1 = poly_info(A, VarTypes, TypeVarSet, D, E, F, G,
- ModuleInfo),
+ poly_info_set_typevarset(TypeVarSet, Info0, Info1),
% Make the typeclass_infos for the call, and return
% a list of which variables were constrained by the
% context
goal_info_get_context(GoalInfo0, Context),
+ PredClassContext = constraints(UniversalConstraints,
+ ExistentialConstraints),
polymorphism__make_typeclass_info_vars(
- PredClassContext, Subst, TypeSubst,
+ UniversalConstraints, Subst, TypeSubst,
PredExistQVars, Context,
hlds_class_proc(PredId0, ProcId0),
hlds_class_proc(PredId, ProcId),
- ExtraTypeClassVars, ExtraTypeClassGoals,
- ConstrainedVars, Info1, Info2),
+ UnivTypeClassVars, ExtraTypeClassGoals,
+ UnivConstrainedTVars, Info1, Info2),
+ polymorphism__make_typeclass_info_head_vars(
+ ExistentialConstraints, ExistTypeClassVars,
+ Info2, Info3),
+ constraint_list_get_tvars(ExistentialConstraints,
+ ExistConstrainedTVars),
+
+ list__append(UnivTypeClassVars, ExistTypeClassVars,
+ ExtraTypeClassVars),
% No need to make typeinfos for the constrained vars
- list__delete_elems(PredTypeVars1, ConstrainedVars,
+ list__delete_elems(PredTypeVars1, UnivConstrainedTVars,
+ PredTypeVars2),
+ list__delete_elems(PredTypeVars2, ExistConstrainedTVars,
PredTypeVars),
term__var_list_to_term_list(PredTypeVars, PredTypes0),
@@ -1002,7 +1178,7 @@
polymorphism__make_type_info_vars(PredTypes, PredExistQVars,
Context, ExtraTypeInfoVars, ExtraTypeInfoGoals,
- Info2, Info),
+ Info3, Info),
list__append(ExtraTypeClassVars, ArgVars0, ArgVars1),
list__append(ExtraTypeInfoVars, ArgVars1, ArgVars),
list__append(ExtraTypeClassGoals, ExtraTypeInfoGoals,
@@ -1022,8 +1198,7 @@
% any existentially quantified type vars in the callee's
% type: such typeinfo variables are produced by this call
%
- Info = poly_info(_, _, _, TypeVarMap, _, _, _, _),
-
+ poly_info_get_type_info_map(Info, TypeVarMap),
goal_info_get_instmap_delta(GoalInfo1, InstmapDelta0),
AddInstDelta = lambda([TVar::in, IMD0::in, IMD::out] is det, (
map__lookup(TypeVarMap, TVar, TypeInfoLocn),
@@ -1036,9 +1211,27 @@
goal_info_set_instmap_delta(GoalInfo1, InstmapDelta, GoalInfo)
).
-:- pred polymorphism__fixup_quantification(hlds_goal, hlds_goal,
- set(var), poly_info, poly_info).
-:- mode polymorphism__fixup_quantification(in, out, out, in, out) is det.
+%-----------------------------------------------------------------------------%
+
+% constraint_list_get_tvars(Constraints, TVars):
+% return the list of type variables contained in a list of constraints
+
+:- pred constraint_list_get_tvars(list(class_constraint), list(tvar)).
+:- mode constraint_list_get_tvars(in, out) is det.
+constraint_list_get_tvars(Constraints, TVars) :-
+ list__map(constraint_get_tvars, Constraints, TVarsList),
+ list__condense(TVarsList, TVars).
+
+:- pred constraint_get_tvars(class_constraint, list(tvar)).
+:- mode constraint_get_tvars(in, out) is det.
+constraint_get_tvars(constraint(_Name, Args), TVars) :-
+ term__vars_list(Args, TVars).
+
+%-----------------------------------------------------------------------------%
+
+:- pred polymorphism__fixup_quantification(hlds_goal, existq_tvars,
+ hlds_goal, set(var), poly_info, poly_info).
+:- mode polymorphism__fixup_quantification(in, in, out, out, in, out) is det.
%
% If the predicate we are processing is a polymorphic predicate,
@@ -1047,23 +1240,24 @@
% so that it includes the type-info variables in the non-locals set.
%
-polymorphism__fixup_quantification(Goal0, Goal, NewOutsideVars, Info0, Info) :-
- Info0 = poly_info(VarSet0, VarTypes0, TypeVarSet, TypeVarMap,
- TypeClassVarMap, Proofs, PredName, ModuleInfo),
+polymorphism__fixup_quantification(Goal0, ExistQVars, Goal, NewOutsideVars,
+ Info0, Info) :-
+ poly_info_get_type_info_map(Info0, TypeVarMap),
( map__is_empty(TypeVarMap) ->
set__init(NewOutsideVars),
Info = Info0,
Goal = Goal0
;
- goal_util__extra_nonlocal_typeinfos(TypeVarMap,
- VarTypes0, Goal0, NewOutsideVars),
+ poly_info_get_varset(Info0, VarSet0),
+ poly_info_get_var_types(Info0, VarTypes0),
+ goal_util__extra_nonlocal_typeinfos(TypeVarMap, VarTypes0,
+ ExistQVars, Goal0, NewOutsideVars),
Goal0 = _ - GoalInfo0,
goal_info_get_nonlocals(GoalInfo0, NonLocals),
set__union(NewOutsideVars, NonLocals, OutsideVars),
implicitly_quantify_goal(Goal0, VarSet0, VarTypes0,
OutsideVars, Goal, VarSet, VarTypes, _Warnings),
- Info = poly_info(VarSet, VarTypes, TypeVarSet, TypeVarMap,
- TypeClassVarMap, Proofs, PredName, ModuleInfo)
+ poly_info_set_varset_and_types(VarSet, VarTypes, Info0, Info)
).
:- pred polymorphism__process_lambda(pred_or_func, list(var),
@@ -1077,23 +1271,24 @@
NonLocalTypeInfos, LambdaGoal, Unification0, Functor,
Unification, PolyInfo0, PolyInfo) :-
PolyInfo0 = poly_info(VarSet, VarTypes, TVarSet, TVarMap,
- TCVarMap, Proofs, PredName, ModuleInfo0),
+ TCVarMap, _Proofs, PredName, ModuleInfo0),
% Calculate the constraints which apply to this lambda
- % expression.
+ % expression.
+ % XXX Note currently we only allow lambda expressions
+ % to have universally quantified constraints.
map__keys(TCVarMap, AllConstraints),
map__apply_to_list(Vars, VarTypes, LambdaVarTypes),
list__map(type_util__vars, LambdaVarTypes, LambdaTypeVarsList),
list__condense(LambdaTypeVarsList, LambdaTypeVars),
list__filter(polymorphism__constraint_contains_vars(LambdaTypeVars),
- AllConstraints, Constraints),
-
+ AllConstraints, UnivConstraints),
+ Constraints = constraints(UnivConstraints, []),
lambda__transform_lambda(PredOrFunc, PredName, Vars, Modes, Det,
OrigNonLocals, NonLocalTypeInfos, LambdaGoal, Unification0,
VarSet, VarTypes, Constraints, TVarSet, TVarMap, TCVarMap,
ModuleInfo0, Functor, Unification, ModuleInfo),
- PolyInfo = poly_info(VarSet, VarTypes, TVarSet, TVarMap,
- TCVarMap, Proofs, PredName, ModuleInfo).
+ poly_info_set_module_info(ModuleInfo, PolyInfo0, PolyInfo).
:- pred polymorphism__constraint_contains_vars(list(var), class_constraint).
:- mode polymorphism__constraint_contains_vars(in, in) is semidet.
@@ -1114,10 +1309,15 @@
% variables to hold the typeclass_info for those constraints,
% and create a list of goals to initialize those typeclass_info variables
% to the appropriate typeclass_info structures for the constraints.
+%
+% Constraints which are already in the TypeClassInfoMap are assumed to
+% have already had their typeclass_infos initialized; for them, we
+% just return the variable in the TypeClassInfoMap.
+%
% If the called predicate is a class method, and we know which instance
% it is, then instead of creating a type_info variable for the type class
-% instance, just return the pred_proc_id for that instance.
-% Otherwise return the original pred_proc_id unchanged.
+% instance, we just return the pred_proc_id for that instance.
+% Otherwise we return the original pred_proc_id unchanged.
:- pred polymorphism__make_typeclass_info_vars(list(class_constraint),
substitution, tsubst, existq_tvars, term__context,
@@ -1432,7 +1632,7 @@
;
error("polymorphism__make_typeclass_info_var")
),
- apply_rec_subst_to_constraints(SubTypeSubst,
+ apply_rec_subst_to_constraint_list(SubTypeSubst,
SuperClasses0, SuperClasses),
(
list__nth_member_search(SuperClasses,
@@ -1441,21 +1641,17 @@
SuperClassIndex0 = SuperClassIndex
;
% We shouldn't have got this far if
- % the constraints were not satifsied
+ % the constraints were not satisfied
error("polymorphism.m: constraint not in constraint list")
),
- Info2 = poly_info(VarSet2, VarTypes2, TypeVarSet2,
- TypeInfoMap2, TypeClassInfoMap2, Proofs2,
- PredName2, ModuleInfo2),
-
+ poly_info_get_varset(Info2, VarSet2),
+ poly_info_get_var_types(Info2, VarTypes2),
polymorphism__make_count_var(SuperClassIndex, VarSet2,
VarTypes2, IndexVar, IndexGoal, VarSet,
VarTypes),
-
- Info = poly_info(VarSet, VarTypes, TypeVarSet2,
- TypeInfoMap2, TypeClassInfoMap2, Proofs2,
- PredName2, ModuleInfo2),
+ poly_info_set_varset_and_types(VarSet, VarTypes,
+ Info2, Info),
% We extract the superclass typeclass_info by
% inserting a call to
@@ -1506,7 +1702,7 @@
ClassId, InstanceNum, ExistQVars,
NewVar, NewGoals, Info0, Info) :-
- Info0 = poly_info(_, _, _, _, _, _, _, ModuleInfo),
+ poly_info_get_module_info(Info0, ModuleInfo),
module_info_instances(ModuleInfo, InstanceTable),
map__lookup(InstanceTable, ClassId, InstanceList),
@@ -1521,8 +1717,8 @@
SuperClassProofs, ExistQVars, ArgSuperClassVars,
SuperClassGoals, Info0, Info1),
- Info1 = poly_info(VarSet0, VarTypes0, TVarSet, TVarMap, TCVarMap,
- Proofs, PredName, _),
+ poly_info_get_varset(Info1, VarSet0),
+ poly_info_get_var_types(Info1, VarTypes0),
% lay out the argument variables as expected in the
% typeclass_info
@@ -1607,8 +1803,7 @@
TypeClassInfoGoal = Unify - GoalInfo,
NewGoals0 = [TypeClassInfoGoal, BaseGoal],
list__append(SuperClassGoals, NewGoals0, NewGoals),
- Info = poly_info(VarSet, VarTypes, TVarSet, TVarMap,
- TCVarMap, Proofs, PredName, ModuleInfo).
+ poly_info_set_varset_and_types(VarSet, VarTypes, Info1, Info).
%---------------------------------------------------------------------------%
@@ -1622,25 +1817,20 @@
SuperClassProofs, ExistQVars, NewVars, NewGoals,
Info0, Info) :-
- Info0 = poly_info(VarSet0, VarTypes0, TVarSet, TVarMap0, TCVarMap0,
- Proofs, PredName, ModuleInfo),
+ poly_info_get_proofs(Info0, Proofs),
+ poly_info_get_varset(Info0, VarSet0),
ClassDefn = hlds_class_defn(SuperClasses, ClassVars, _, ClassVarSet, _),
-
map__from_corresponding_lists(ClassVars, InstanceTypes, TypeSubst),
varset__merge_subst(VarSet0, ClassVarSet, VarSet1, Subst),
+ poly_info_set_varset(VarSet1, Info0, Info1),
- Info1 = poly_info(VarSet1, VarTypes0, TVarSet, TVarMap0, TCVarMap0,
- SuperClassProofs, PredName, ModuleInfo),
-
+ poly_info_set_proofs(SuperClassProofs, Info1, Info2),
polymorphism__make_superclasses_from_proofs(SuperClasses, Subst,
- TypeSubst, ExistQVars, [], NewGoals, Info1, Info2,
+ TypeSubst, ExistQVars, [], NewGoals, Info2, Info3,
[], NewVars),
- Info2 = poly_info(VarSet, VarTypes, _, TVarMap, TCVarMap, _, _, _),
-
- Info = poly_info(VarSet, VarTypes, TVarSet, TVarMap, TCVarMap,
- Proofs, PredName, ModuleInfo) .
+ poly_info_set_proofs(Proofs, Info3, Info).
:- pred polymorphism__make_superclasses_from_proofs(list(class_constraint),
@@ -1712,8 +1902,7 @@
Type = term__variable(TVar),
list__member(TVar, ExistQVars)
->
- Info0 = poly_info(VarSet0, VarTypes0, C, TypeInfoMap0,
- E, F, G, H),
+ poly_info_get_type_info_map(Info0, TypeInfoMap0),
% existentially quantified tvars in the head will already
% have a type_info var allocated for them
( map__search(TypeInfoMap0, TVar, type_info(HeadVar)) ->
@@ -1721,11 +1910,10 @@
Info = Info0
;
polymorphism__new_type_info_var(Type, "type_info",
- VarSet0, VarTypes0, Var, VarSet, VarTypes),
+ Var, Info0, Info1),
map__det_insert(TypeInfoMap0, TVar, type_info(Var),
TypeInfoMap),
- Info = poly_info(VarSet, VarTypes, C, TypeInfoMap,
- E, F, G, H)
+ poly_info_set_type_info_map(TypeInfoMap, Info1, Info)
),
ExtraGoals = []
;
@@ -1758,7 +1946,7 @@
no, ExistQVars, Context, Var, ExtraGoals, Info0, Info)
;
Type = term__variable(TypeVar),
- Info0 = poly_info(_, _, _, TypeInfoMap0, _, _, _, _),
+ poly_info_get_type_info_map(Info0, TypeInfoMap0),
map__search(TypeInfoMap0, TypeVar, TypeInfoLocn)
->
% This occurs for code where a predicate calls a polymorphic
@@ -1798,15 +1986,13 @@
% This occurs for code where a predicate calls a polymorphic
% predicate with an unbound type variable.
% Cases where there is no producer at all for the type
- % variable should get caught by purity.m.
+ % variable should get caught by post_typecheck.m.
% XXX Cases where there is a producer but it occurs
% somewhere further on in the goal should be avoided by
% mode reordering, but currently mode analysis doesn't
% do that.
%
- Info0 = poly_info(_VarSet, _VarTypes, TypeVarSet, _TypeVarMap,
- _TypeClassVarMap, _Proofs, PredName,
- _ModuleInfo),
+ poly_info_get_typevarset(Info0, TypeVarSet),
varset__lookup_name(TypeVarSet, TypeVar, TypeVarName),
term__context_file(Context, FileName),
term__context_line(Context, LineNumber),
@@ -1816,6 +2002,7 @@
string__format("%s:%03d: ",
[s(FileName), i(LineNumber)], ContextMessage)
),
+ poly_info_get_pred_name(Info0, PredName),
string__append_list([
"polymorphism__make_var:\n",
ContextMessage, "In predicate `", PredName, "':\n",
@@ -1840,7 +2027,9 @@
polymorphism__make_type_info_vars(TypeArgs, ExistQVars, Context,
ArgTypeInfoVars, ArgTypeInfoGoals, Info0, Info1),
- Info1 = poly_info(VarSet1, VarTypes1, C, D, E, F, G, ModuleInfo),
+ poly_info_get_varset(Info1, VarSet1),
+ poly_info_get_var_types(Info1, VarTypes1),
+ poly_info_get_module_info(Info1, ModuleInfo),
polymorphism__init_const_base_type_info_var(Type,
TypeId, ModuleInfo, VarSet1, VarTypes1,
@@ -1850,7 +2039,7 @@
BaseVar, VarSet2, VarTypes2, [BaseGoal],
Var, VarSet, VarTypes, ExtraGoals),
- Info = poly_info(VarSet, VarTypes, C, D, E, F, G, ModuleInfo).
+ poly_info_set_varset_and_types(VarSet, VarTypes, Info1, Info).
% Create a unification for the two-cell type_info
% variable for this type if the type arity is not zero:
@@ -2200,28 +2389,38 @@
%---------------------------------------------------------------------------%
-:- pred polymorphism__make_head_vars(list(tvar), tvarset,
- varset, map(var, type),
- list(var), varset, map(var, type)).
-:- mode polymorphism__make_head_vars(in, in, in, in, out, out, out) is det.
-
-polymorphism__make_head_vars([], _, VarSet, VarTypes, [], VarSet, VarTypes).
-polymorphism__make_head_vars([TypeVar|TypeVars], TypeVarSet,
- VarSet0, VarTypes0,
- TypeInfoVars, VarSet, VarTypes) :-
- Type = term__variable(TypeVar),
- polymorphism__new_type_info_var(Type, "type_info", VarSet0, VarTypes0,
- Var, VarSet1, VarTypes1),
- ( varset__search_name(TypeVarSet, TypeVar, TypeVarName) ->
- string__append("TypeInfo_for_", TypeVarName, VarName),
- varset__name_var(VarSet1, Var, VarName, VarSet2)
+:- pred polymorphism__make_head_vars(list(tvar), tvarset, list(var),
+ poly_info, poly_info).
+:- mode polymorphism__make_head_vars(in, in, out, in, out) is det.
+
+polymorphism__make_head_vars([], _, []) --> [].
+polymorphism__make_head_vars([TypeVar|TypeVars], TypeVarSet, TypeInfoVars) -->
+ { Type = term__variable(TypeVar) },
+ polymorphism__new_type_info_var(Type, "type_info", Var),
+ ( { varset__search_name(TypeVarSet, TypeVar, TypeVarName) } ->
+ =(Info0),
+ { poly_info_get_varset(Info0, VarSet0) },
+ { string__append("TypeInfo_for_", TypeVarName, VarName) },
+ { varset__name_var(VarSet0, Var, VarName, VarSet) },
+ poly_info_set_varset(VarSet)
;
- VarSet2 = VarSet1
+ []
),
- TypeInfoVars = [Var | TypeInfoVars1],
- polymorphism__make_head_vars(TypeVars, TypeVarSet,
- VarSet2, VarTypes1,
- TypeInfoVars1, VarSet, VarTypes).
+ { TypeInfoVars = [Var | TypeInfoVars1] },
+ polymorphism__make_head_vars(TypeVars, TypeVarSet, TypeInfoVars1).
+
+
+:- pred polymorphism__new_type_info_var(type, string, var,
+ poly_info, poly_info).
+:- mode polymorphism__new_type_info_var(in, in, out, in, out) is det.
+
+polymorphism__new_type_info_var(Type, Symbol, Var, Info0, Info) :-
+ poly_info_get_varset(Info0, VarSet0),
+ poly_info_get_var_types(Info0, VarTypes0),
+ polymorphism__new_type_info_var(Type, Symbol, VarSet0, VarTypes0,
+ Var, VarSet, VarTypes),
+ poly_info_set_varset_and_types(VarSet, VarTypes, Info0, Info).
+
:- pred polymorphism__new_type_info_var(type, string, varset, map(var, type),
var, varset, map(var, type)).
@@ -2248,13 +2447,15 @@
extract_type_info(Type, TypeVar, TypeClassInfoVar, Index, Goals,
TypeInfoVar, PolyInfo0, PolyInfo) :-
- PolyInfo0 = poly_info(VarSet0, VarTypes0, C, TypeInfoLocns0,
- E, F, G, ModuleInfo),
+ poly_info_get_varset(PolyInfo0, VarSet0),
+ poly_info_get_var_types(PolyInfo0, VarTypes0),
+ poly_info_get_type_info_map(PolyInfo0, TypeInfoLocns0),
+ poly_info_get_module_info(PolyInfo0, ModuleInfo),
extract_type_info_2(Type, TypeVar, TypeClassInfoVar, Index, ModuleInfo,
Goals, TypeInfoVar, VarSet0, VarTypes0, TypeInfoLocns0,
VarSet, VarTypes, TypeInfoLocns),
- PolyInfo = poly_info(VarSet, VarTypes, C, TypeInfoLocns, E, F, G,
- ModuleInfo).
+ poly_info_set_varset_and_types(VarSet, VarTypes, PolyInfo0, PolyInfo1),
+ poly_info_set_type_info_map(TypeInfoLocns, PolyInfo1, PolyInfo).
:- pred extract_type_info_2(type, tvar, var, int, module_info, list(hlds_goal),
var, varset, map(var, type), map(tvar, type_info_locn),
@@ -2322,56 +2523,36 @@
*/
TypeInfoLocns = TypeInfoLocns0.
-%---------------------------------------------------------------------------%
-
- % Add a head var for each class constraint, and make an entry in the
- % typeinfo locations map for each constrained type var.
-:- pred polymorphism__make_typeclass_info_head_vars(list(class_constraint),
- module_info, varset, map(var, type), list(var),
- map(var, type_info_locn), list(var), varset, map(var, type)).
-:- mode polymorphism__make_typeclass_info_head_vars(in, in, in, in,
- out, out, out, out, out) is det.
-
-polymorphism__make_typeclass_info_head_vars(ClassContext, ModuleInfo, VarSet0,
- VarTypes0, ExtraHeadVars, TypeClassInfoMap, ConstrainedTVars,
- VarSet, VarTypes) :-
-
- % initialise the new accumulators
- ExtraHeadVars0 = [],
- map__init(TypeClassInfoMap0),
+%-----------------------------------------------------------------------------%
- % do the work
- polymorphism__make_typeclass_info_head_vars_2(ClassContext, ModuleInfo,
- VarSet0, VarSet,
- VarTypes0, VarTypes,
- ExtraHeadVars0, ExtraHeadVars1,
- TypeClassInfoMap0, TypeClassInfoMap),
-
- % A type var has a location in a typeclass info iff it is
- % constrained
- map__keys(TypeClassInfoMap, ConstrainedTVars),
+ % Create a head var for each class constraint, and make an entry in
+ % the typeinfo locations map for each constrained type var.
- % The ExtraHeadVars are built up in reverse
- list__reverse(ExtraHeadVars1, ExtraHeadVars).
+:- pred polymorphism__make_typeclass_info_head_vars(list(class_constraint),
+ list(var), poly_info, poly_info).
+:- mode polymorphism__make_typeclass_info_head_vars(in, out, in, out)
+ is det.
+
+polymorphism__make_typeclass_info_head_vars(Constraints, ExtraHeadVars) -->
+ { ExtraHeadVars0 = [] },
+ polymorphism__make_typeclass_info_head_vars_2(Constraints,
+ ExtraHeadVars0, ExtraHeadVars1),
+ { list__reverse(ExtraHeadVars1, ExtraHeadVars) }.
:- pred polymorphism__make_typeclass_info_head_vars_2(list(class_constraint),
- module_info, varset, varset,
- map(var, type), map(var, type),
- list(var), list(var),
- map(var, type_info_locn), map(var, type_info_locn)).
-:- mode polymorphism__make_typeclass_info_head_vars_2(in, in, in, out, in, out,
- in, out, in, out) is det.
-
-polymorphism__make_typeclass_info_head_vars_2([], _,
- VarSet, VarSet,
- VarTypes, VarTypes,
- ExtraHeadVars, ExtraHeadVars,
- TypeInfoLocations, TypeInfoLocations).
-polymorphism__make_typeclass_info_head_vars_2([C|Cs], ModuleInfo,
- VarSet0, VarSet,
- VarTypes0, VarTypes,
- ExtraHeadVars0, ExtraHeadVars,
- TypeClassInfoMap0, TypeClassInfoMap) :-
+ list(var), list(var), poly_info, poly_info).
+:- mode polymorphism__make_typeclass_info_head_vars_2(in, in, out, in, out)
+ is det.
+
+polymorphism__make_typeclass_info_head_vars_2([],
+ ExtraHeadVars, ExtraHeadVars) --> [].
+polymorphism__make_typeclass_info_head_vars_2([C|Cs],
+ ExtraHeadVars0, ExtraHeadVars, Info0, Info) :-
+
+ poly_info_get_varset(Info0, VarSet0),
+ poly_info_get_var_types(Info0, VarTypes0),
+ poly_info_get_type_info_map(Info0, TypeInfoMap0),
+ poly_info_get_module_info(Info0, ModuleInfo),
C = constraint(ClassName0, ClassTypes),
@@ -2414,7 +2595,7 @@
IsNew = lambda([TypeVar0::in] is semidet,
(
TypeVar0 = TypeVar - _Index,
- \+ map__search(TypeClassInfoMap0, TypeVar, _)
+ \+ map__search(TypeInfoMap0, TypeVar, _)
)),
list__filter(IsNew, ClassTypeVars, NewClassTypeVars),
@@ -2428,15 +2609,14 @@
map__det_insert(LocnMap0, TheTypeVar,
typeclass_info(Var, Location), LocnMap)
)),
- list__foldl(MakeEntry, NewClassTypeVars,
- TypeClassInfoMap0, TypeClassInfoMap1),
+ list__foldl(MakeEntry, NewClassTypeVars, TypeInfoMap0, TypeInfoMap1),
+
+ poly_info_set_varset_and_types(VarSet1, VarTypes1, Info0, Info1),
+ poly_info_set_type_info_map(TypeInfoMap1, Info1, Info2),
% Handle the rest of the constraints
- polymorphism__make_typeclass_info_head_vars_2(Cs, ModuleInfo,
- VarSet1, VarSet,
- VarTypes1, VarTypes,
- ExtraHeadVars1, ExtraHeadVars,
- TypeClassInfoMap1, TypeClassInfoMap).
+ polymorphism__make_typeclass_info_head_vars_2(Cs,
+ ExtraHeadVars1, ExtraHeadVars, Info2, Info).
:- pred is_pair(pair(_, _)::in) is det.
is_pair(_).
@@ -2503,7 +2683,7 @@
% introduced because it is a class method.
pred_info_get_class_context(PredInfo0, ClassContext),
(
- ClassContext = [Head|_]
+ ClassContext = constraints([Head|_], _)
->
InstanceConstraint = Head
;
@@ -2575,16 +2755,158 @@
%---------------------------------------------------------------------------%
-:- pred polymorphism__get_module_info(module_info, poly_info, poly_info).
-:- mode polymorphism__get_module_info(out, in, out) is det.
+:- type poly_info --->
+ poly_info(
+ varset, % from the proc_info
+ map(var, type), % from the proc_info
+ tvarset, % from the proc_info
+ map(tvar, type_info_locn),
+ % specifies the location of
+ % the type_info var
+ % for each of the pred's type
+ % parameters
+
+ map(class_constraint, var),
+ % specifies the location of
+ % the typeclass_info var
+ % for each of the pred's class
+ % constraints
+ map(class_constraint, constraint_proof),
+ % specifies why each constraint
+ % that was eliminated from the
+ % pred was able to be eliminated
+ % (this allows us to efficiently
+ % construct the dictionary)
+
+ % Note that the two maps above
+ % are separate since the second
+ % is the information calculated
+ % by typecheck.m, while the
+ % first is the information
+ % calculated here in
+ % polymorphism.m
+
+ string, % pred name
+ module_info
+ ).
+
+:- pred init_poly_info(module_info, pred_info, proc_info, poly_info).
+:- mode init_poly_info(in, in, in, out) is det.
+
+init_poly_info(ModuleInfo, PredInfo, ProcInfo, PolyInfo) :-
+ pred_info_typevarset(PredInfo, TypeVarSet),
+ pred_info_name(PredInfo, PredName),
+ proc_info_varset(ProcInfo, VarSet),
+ proc_info_vartypes(ProcInfo, VarTypes),
+ map__init(TypeInfoMap),
+ map__init(TypeClassInfoMap),
+ map__init(Proofs),
+ PolyInfo = poly_info(VarSet, VarTypes, TypeVarSet,
+ TypeInfoMap, TypeClassInfoMap,
+ Proofs, PredName, ModuleInfo).
+
+:- pred poly_info_get_varset(poly_info, varset).
+:- mode poly_info_get_varset(in, out) is det.
+
+poly_info_get_varset(PolyInfo, VarSet) :-
+ PolyInfo = poly_info(VarSet, _, _, _, _, _, _, _).
+
+:- pred poly_info_get_var_types(poly_info, map(var, type)).
+:- mode poly_info_get_var_types(in, out) is det.
+
+poly_info_get_var_types(PolyInfo, VarTypes) :-
+ PolyInfo = poly_info(_, VarTypes, _, _, _, _, _, _).
+
+:- pred poly_info_get_typevarset(poly_info, tvarset).
+:- mode poly_info_get_typevarset(in, out) is det.
+
+poly_info_get_typevarset(PolyInfo, TypeVarSet) :-
+ PolyInfo = poly_info(_, _, TypeVarSet, _, _, _, _, _).
+
+:- pred poly_info_get_type_info_map(poly_info, map(tvar, type_info_locn)).
+:- mode poly_info_get_type_info_map(in, out) is det.
+
+poly_info_get_type_info_map(PolyInfo, TypeInfoMap) :-
+ PolyInfo = poly_info(_, _, _, TypeInfoMap, _, _, _, _).
-polymorphism__get_module_info(ModuleInfo, PolyInfo, PolyInfo) :-
+:- pred poly_info_get_type_class_info_map(poly_info,
+ map(class_constraint, var)).
+:- mode poly_info_get_type_class_info_map(in, out) is det.
+
+poly_info_get_type_class_info_map(PolyInfo, TypeClassInfoMap) :-
+ PolyInfo = poly_info(_, _, _, _, TypeClassInfoMap, _, _, _).
+
+:- pred poly_info_get_proofs(poly_info,
+ map(class_constraint, constraint_proof)).
+:- mode poly_info_get_proofs(in, out) is det.
+
+poly_info_get_proofs(PolyInfo, Proofs) :-
+ PolyInfo = poly_info(_, _, _, _, _, Proofs, _, _).
+
+:- pred poly_info_get_pred_name(poly_info, string).
+:- mode poly_info_get_pred_name(in, out) is det.
+
+poly_info_get_pred_name(PolyInfo, PredName) :-
+ PolyInfo = poly_info(_, _, _, _, _, _, PredName, _).
+
+:- pred poly_info_get_module_info(poly_info, module_info).
+:- mode poly_info_get_module_info(in, out) is det.
+
+poly_info_get_module_info(PolyInfo, ModuleInfo) :-
PolyInfo = poly_info(_, _, _, _, _, _, _, ModuleInfo).
-:- pred polymorphism__set_module_info(module_info, poly_info, poly_info).
-:- mode polymorphism__set_module_info(in, in, out) is det.
-polymorphism__set_module_info(ModuleInfo, PolyInfo0, PolyInfo) :-
+:- pred poly_info_set_varset(varset, poly_info, poly_info).
+:- mode poly_info_set_varset(in, in, out) is det.
+
+poly_info_set_varset(VarSet, PolyInfo0, PolyInfo) :-
+ PolyInfo0 = poly_info(_, B, C, D, E, F, G, H),
+ PolyInfo = poly_info(VarSet, B, C, D, E, F, G, H).
+
+:- pred poly_info_set_varset_and_types(varset, map(var, type),
+ poly_info, poly_info).
+:- mode poly_info_set_varset_and_types(in, in, in, out) is det.
+
+poly_info_set_varset_and_types(VarSet, VarTypes, PolyInfo0, PolyInfo) :-
+ PolyInfo0 = poly_info(_, _, C, D, E, F, G, H),
+ PolyInfo = poly_info(VarSet, VarTypes, C, D, E, F, G, H).
+
+:- pred poly_info_set_typevarset(tvarset, poly_info, poly_info).
+:- mode poly_info_set_typevarset(in, in, out) is det.
+
+poly_info_set_typevarset(TypeVarSet, PolyInfo0, PolyInfo) :-
+ PolyInfo0 = poly_info(A, B, _, D, E, F, G, H),
+ PolyInfo = poly_info(A, B, TypeVarSet, D, E, F, G, H).
+
+:- pred poly_info_set_type_info_map(map(tvar, type_info_locn),
+ poly_info, poly_info).
+:- mode poly_info_set_type_info_map(in, in, out) is det.
+
+poly_info_set_type_info_map(TypeInfoMap, PolyInfo0, PolyInfo) :-
+ PolyInfo0 = poly_info(A, B, C, _, E, F, G, H),
+ PolyInfo = poly_info(A, B, C, TypeInfoMap, E, F, G, H).
+
+:- pred poly_info_set_typeclass_info_map(map(class_constraint, var),
+ poly_info, poly_info).
+:- mode poly_info_set_typeclass_info_map(in, in, out) is det.
+
+poly_info_set_typeclass_info_map(TypeClassInfoMap, PolyInfo0, PolyInfo) :-
+ PolyInfo0 = poly_info(A, B, C, D, _, F, G, H),
+ PolyInfo = poly_info(A, B, C, D, TypeClassInfoMap, F, G, H).
+
+
+:- pred poly_info_set_proofs(map(class_constraint, constraint_proof),
+ poly_info, poly_info).
+:- mode poly_info_set_proofs(in, in, out) is det.
+
+poly_info_set_proofs(Proofs, PolyInfo0, PolyInfo) :-
+ PolyInfo0 = poly_info(A, B, C, D, E, _, G, H),
+ PolyInfo = poly_info(A, B, C, D, E, Proofs, G, H).
+
+:- pred poly_info_set_module_info(module_info, poly_info, poly_info).
+:- mode poly_info_set_module_info(in, in, out) is det.
+
+poly_info_set_module_info(ModuleInfo, PolyInfo0, PolyInfo) :-
PolyInfo0 = poly_info(A, B, C, D, E, F, G, _),
PolyInfo = poly_info(A, B, C, D, E, F, G, ModuleInfo).
Index: compiler/prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.35.2.1
diff -u -r1.35.2.1 prog_data.m
--- prog_data.m 1998/06/06 11:39:50 1.35.2.1
+++ prog_data.m 1998/06/06 16:40:30
@@ -53,14 +53,14 @@
; pred(tvarset, existq_tvars, sym_name, list(type_and_mode),
maybe(determinism), condition, purity,
- list(class_constraint))
+ class_constraints)
% VarNames, ExistentiallyQuantifiedTypeVars,
% PredName, ArgTypes, Deterministicness, Cond,
% Purity, TypeClassContext
; func(tvarset, existq_tvars, sym_name, list(type_and_mode),
type_and_mode, maybe(determinism), condition, purity,
- list(class_constraint))
+ class_constraints)
% VarNames, ExistentiallyQuantifiedTypeVars,
% PredName, ArgTypes, ReturnType,
% Deterministicness, Cond,
@@ -243,6 +243,12 @@
:- type class_constraint
---> constraint(class_name, list(type)).
+:- type class_constraints
+ ---> constraints(
+ list(class_constraint), % ordinary (universally quantified)
+ list(class_constraint) % existentially quantified constraints
+ ).
+
:- type class_name == sym_name.
:- type class_interface == list(class_method).
@@ -250,7 +256,7 @@
:- type class_method
---> pred(tvarset, existq_tvars, sym_name, list(type_and_mode),
maybe(determinism), condition,
- list(class_constraint), term__context)
+ class_constraints, term__context)
% VarNames, ExistentiallyQuantifiedTypeVars,
% PredName, ArgTypes, Determinism, Cond
% ClassContext, Context
@@ -258,7 +264,7 @@
; func(tvarset, existq_tvars, sym_name, list(type_and_mode),
type_and_mode,
maybe(determinism), condition,
- list(class_constraint), term__context)
+ class_constraints, term__context)
% VarNames, ExistentiallyQuantfiedTypeVars,
% PredName, ArgTypes, ReturnType,
% Determinism, Cond
@@ -348,7 +354,8 @@
; eqv_type(sym_name, list(type_param), type)
; abstract_type(sym_name, list(type_param)).
-:- type constructor == pair(sym_name, list(constructor_arg)).
+:- type constructor
+ ---> ctor(existq_tvars, sym_name, list(constructor_arg)).
:- type constructor_arg == pair(string, type).
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.173.2.1
diff -u -r1.173.2.1 prog_io.m
--- prog_io.m 1998/06/06 11:39:51 1.173.2.1
+++ prog_io.m 1998/06/06 18:43:08
@@ -189,6 +189,7 @@
:- import_module purity.
:- import_module int, string, std_util, parser, term_io, dir, require.
+:- import_module assoc_list.
%-----------------------------------------------------------------------------%
@@ -834,7 +835,7 @@
Result = error(Msg, Term)
;
Result = error(
- "Existential quantifiers only allowed on pred or func declarations",
+"Top-level existential quantifiers only allowed on pred or func declarations",
Decl)
).
@@ -1285,7 +1286,19 @@
:- pred process_eqv_type_2(maybe_functor, term, maybe1(type_defn)).
:- mode process_eqv_type_2(in, in, out) is det.
process_eqv_type_2(error(Error, Term), _, error(Error, Term)).
-process_eqv_type_2(ok(Name, Args), Body, ok(eqv_type(Name, Args, Body))).
+process_eqv_type_2(ok(Name, Args), Body, Result) :-
+ % check that all the variables in the body occur in the head
+ (
+ (
+ term__contains_var(Body, Var2),
+ \+ term__contains_var_list(Args, Var2)
+ )
+ ->
+ Result = error("free type parameter in RHS of type definition",
+ Body)
+ ;
+ Result = ok(eqv_type(Name, Args, Body))
+ ).
%-----------------------------------------------------------------------------%
@@ -1308,16 +1321,56 @@
process_du_type_2(ModuleName, ok(Functor, Args), Body, MaybeEqualityPred,
Result) :-
% check that body is a disjunction of constructors
- ( %%% some [Constrs]
+ (
convert_constructors(ModuleName, Body, Constrs)
->
+ % check that all type variables in the body
+ % are either explicitly existentally quantified
+ % or occur in the head.
(
- MaybeEqualityPred = ok(EqualityPred),
- Result = ok(du_type(Functor, Args, Constrs,
- EqualityPred))
+ list__member(Ctor, Constrs),
+ Ctor = ctor(ExistQVars, _CtorName, CtorArgs),
+ assoc_list__values(CtorArgs, CtorArgTypes),
+ term__contains_var_list(CtorArgTypes, Var),
+ \+ list__member(Var, ExistQVars),
+ \+ term__contains_var_list(Args, Var)
+ ->
+ Result = error(
+ "free type parameter in RHS of type definition",
+ Body)
+
+ % check that all type variables in existential quantifiers
+ % do not occur in the head
;
- MaybeEqualityPred = error(Error, Term),
- Result = error(Error, Term)
+ list__member(Ctor, Constrs),
+ Ctor = ctor(ExistQVars, _CtorName, CtorArgs),
+ list__member(Var, ExistQVars),
+ assoc_list__values(CtorArgs, CtorArgTypes),
+ \+ term__contains_var_list(CtorArgTypes, Var)
+ ->
+ Result = error( "type variable has overlapping scopes (explicit type quantifier shadows argument type)", Body)
+
+ % check that all type variables in existential quantifiers
+ % occur somewhere in the body
+ ;
+ list__member(Ctor, Constrs),
+ Ctor = ctor(ExistQVars, _CtorName, CtorArgs),
+ list__member(Var, ExistQVars),
+ assoc_list__values(CtorArgs, CtorArgTypes),
+ \+ term__contains_var_list(CtorArgTypes, Var)
+ ->
+ Result = error(
+ "var occurs only in existential quantifier",
+ Body)
+ ;
+ (
+ MaybeEqualityPred = ok(EqualityPred),
+ Result = ok(du_type(Functor, Args, Constrs,
+ EqualityPred))
+ ;
+ MaybeEqualityPred = error(Error, Term),
+ Result = error(Error, Term)
+ )
)
;
Result = error("invalid RHS of type definition", Body)
@@ -1374,7 +1427,7 @@
:- pred check_for_errors_3(sym_name, list(term), term, term, maybe_functor).
:- mode check_for_errors_3(in, in, in, in, out) is det.
-check_for_errors_3(Name, Args, Body, Head, Result) :-
+check_for_errors_3(Name, Args, _Body, Head, Result) :-
% check that all the head args are variables
( %%% some [Arg]
(
@@ -1392,15 +1445,6 @@
)
->
Result = error("repeated type parameters in LHS of type defn", Head)
- % check that all the variables in the body occur in the head
- ; %%% some [Var2]
- (
- term__contains_var(Body, Var2),
- \+ term__contains_var_list(Args, Var2)
- )
- ->
- Result = error("free type parameter in RHS of type definition",
- Body)
;
Result = ok(Name, Args)
).
@@ -1427,24 +1471,33 @@
convert_constructors_2(ModuleName, Terms, Constrs).
% true if input argument is a valid constructor.
- % Note that as a special case, one level of
- % curly braces around the constructor are ignored.
- % This is to allow you to define ';'/2 constructors.
:- pred convert_constructor(module_name, term, constructor).
:- mode convert_constructor(in, in, out) is semidet.
convert_constructor(ModuleName, Term, Result) :-
(
+ % Note that as a special case, one level of
+ % curly braces around the constructor are ignored.
+ % This is to allow you to define ';'/2 constructors.
Term = term__functor(term__atom("{}"), [Term1], _Context)
->
Term2 = Term1
;
Term2 = Term
),
+ (
+ Term2 = term__functor(term__atom("some"), [Vars, Term3], _)
+ ->
+ term__vars(Vars, ExistQVars),
+ Term4 = Term3
+ ;
+ ExistQVars = [],
+ Term4 = Term2
+ ),
parse_implicitly_qualified_term(ModuleName,
- Term2, Term, "constructor definition", ok(F, As)),
+ Term4, Term, "constructor definition", ok(F, As)),
convert_constructor_arg_list(As, Args),
- Result = F - Args.
+ Result = ctor(ExistQVars, F, Args).
%-----------------------------------------------------------------------------%
@@ -1455,30 +1508,21 @@
:- mode process_pred(in, in, in, in, in, in, out) is det.
process_pred(ModuleName, VarSet, PredType0, Cond, MaybeDet, Purity, Result) :-
+ get_class_context(ModuleName, PredType0, PredType, MaybeContext),
(
- maybe_get_class_context(ModuleName, PredType0, PredType,
- MaybeContext)
- ->
- (
- MaybeContext = ok(Constraints),
- parse_implicitly_qualified_term(ModuleName,
- PredType, PredType, "`:- pred' declaration",
- R),
- process_pred_2(R, PredType, VarSet, MaybeDet, Cond,
- Purity, Constraints, Result)
- ;
- MaybeContext = error(String, Term),
- Result = error(String, Term)
- )
- ;
+ MaybeContext = ok(Constraints),
parse_implicitly_qualified_term(ModuleName,
- PredType0, PredType0, "`:- pred' declaration", R),
- process_pred_2(R, PredType0, VarSet, MaybeDet, Cond, Purity,
- [], Result)
+ PredType, PredType, "`:- pred' declaration",
+ R),
+ process_pred_2(R, PredType, VarSet, MaybeDet, Cond,
+ Purity, Constraints, Result)
+ ;
+ MaybeContext = error(String, Term),
+ Result = error(String, Term)
).
:- pred process_pred_2(maybe_functor, term, varset, maybe(determinism),
- condition, purity, list(class_constraint),
+ condition, purity, class_constraints,
maybe1(item)).
:- mode process_pred_2(in, in, in, in, in, in, in, out) is det.
@@ -1510,14 +1554,60 @@
% an appropriate error message (if a syntactically invalid class
% context was given).
-:- pred maybe_get_class_context(module_name, term, term,
- maybe1(list(class_constraint))).
-:- mode maybe_get_class_context(in, in, out, out) is semidet.
-
-maybe_get_class_context(ModuleName, PredType0, PredType, MaybeContext) :-
- PredType0 = term__functor(term__atom("<="),
- [PredType, Constraints], _),
- parse_class_constraints(ModuleName, Constraints, MaybeContext).
+:- pred get_class_context(module_name, term, term, maybe1(class_constraints)).
+:- mode get_class_context(in, in, out, out) is det.
+
+get_class_context(ModuleName, PredType0, PredType, MaybeContext) :-
+ get_universal_constraints(ModuleName, PredType0, PredType1,
+ MaybeUniversalConstraints),
+ get_existential_constraints(ModuleName, PredType1, PredType,
+ MaybeExistentialConstraints),
+ combine_quantifier_results(MaybeUniversalConstraints,
+ MaybeExistentialConstraints, MaybeContext).
+
+:- pred combine_quantifier_results(maybe1(list(class_constraint)),
+ maybe1(list(class_constraint)), maybe1(class_constraints)).
+:- mode combine_quantifier_results(in, in, out) is det.
+combine_quantifier_results(error(Msg, Term), _, error(Msg, Term)).
+combine_quantifier_results(ok(_), error(Msg, Term), error(Msg, Term)).
+combine_quantifier_results(ok(Univs), ok(Exists),
+ ok(constraints(Univs, Exists))).
+
+:- pred get_universal_constraints(module_name, term, term,
+ maybe1(list(class_constraint))).
+:- mode get_universal_constraints(in, in, out, out) is det.
+
+get_universal_constraints(ModuleName, PredType0, PredType,
+ MaybeUniversalConstraints) :-
+ (
+ PredType0 = term__functor(term__atom("<="),
+ [PredType1, UniversalConstraints], _)
+ ->
+ PredType = PredType1,
+ parse_class_constraints(ModuleName, UniversalConstraints,
+ MaybeUniversalConstraints)
+ ;
+ PredType = PredType0,
+ MaybeUniversalConstraints = ok([])
+ ).
+
+:- pred get_existential_constraints(module_name, term, term,
+ maybe1(list(class_constraint))).
+:- mode get_existential_constraints(in, in, out, out) is det.
+
+get_existential_constraints(ModuleName, PredType0, PredType,
+ MaybeExistentialConstraints) :-
+ (
+ PredType0 = term__functor(term__atom("&"),
+ [PredType1, ExistentialConstraints], _)
+ ->
+ PredType = PredType1,
+ parse_class_constraints(ModuleName, ExistentialConstraints,
+ MaybeExistentialConstraints)
+ ;
+ PredType = PredType0,
+ MaybeExistentialConstraints = ok([])
+ ).
%-----------------------------------------------------------------------------%
@@ -1554,25 +1644,18 @@
:- mode process_func(in, in, in, in, in, in, out) is det.
process_func(ModuleName, VarSet, Term0, Cond, Purity, MaybeDet, Result) :-
+ get_class_context(ModuleName, Term0, Term, MaybeContext),
(
- maybe_get_class_context(ModuleName, Term0, Term,
- MaybeContext)
- ->
- (
- MaybeContext = ok(Constraints),
- process_unconstrained_func(ModuleName, VarSet, Term,
- Cond, MaybeDet, Purity, Constraints, Result)
- ;
- MaybeContext = error(String, ErrorTerm),
- Result = error(String, ErrorTerm)
- )
+ MaybeContext = ok(Constraints),
+ process_unconstrained_func(ModuleName, VarSet, Term,
+ Cond, MaybeDet, Purity, Constraints, Result)
;
- process_unconstrained_func(ModuleName, VarSet, Term0,
- Cond, MaybeDet, Purity, [], Result)
+ MaybeContext = error(String, ErrorTerm),
+ Result = error(String, ErrorTerm)
).
:- pred process_unconstrained_func(module_name, varset, term, condition,
- maybe(determinism), purity, list(class_constraint), maybe1(item)).
+ maybe(determinism), purity, class_constraints, maybe1(item)).
:- mode process_unconstrained_func(in, in, in, in, in, in, in, out) is det.
process_unconstrained_func(ModuleName, VarSet, Term, Cond, MaybeDet,
@@ -1591,7 +1674,7 @@
:- pred process_func_2(maybe_functor, term, term, varset, maybe(determinism),
- condition, purity, list(class_constraint),
+ condition, purity, class_constraints,
maybe1(item)).
:- mode process_func_2(in, in, in, in, in, in, in, in, out) is det.
Index: compiler/term_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_util.m,v
retrieving revision 1.7
diff -u -r1.7 term_util.m
--- term_util.m 1998/03/03 17:36:16 1.7
+++ term_util.m 1998/06/06 18:27:51
@@ -255,7 +255,9 @@
type_id::in, list(type_param)::in,
weight_table::in, weight_table::out) is det.
-find_weights_for_cons(SymName - Args, TypeId, Params, Weights0, Weights) :-
+find_weights_for_cons(Ctor, TypeId, Params, Weights0, Weights) :-
+ % XXX should we do something about ExistQVars here?
+ Ctor = ctor(_ExistQVars, SymName, Args),
list__length(Args, Arity),
( Arity > 0 ->
find_and_count_nonrec_args(Args, TypeId, Params,
Index: compiler/type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.54.2.1
diff -u -r1.54.2.1 type_util.m
--- type_util.m 1998/06/06 11:39:56 1.54.2.1
+++ type_util.m 1998/06/08 08:48:53
@@ -139,7 +139,7 @@
% type_list_matches_exactly(TypesA, TypesB) succeeds iff TypesA and
% TypesB are exactly the same modulo variable renaming.
:- pred type_and_constraint_list_matches_exactly(list(type),
- list(class_constraint), list(type), list(class_constraint)).
+ class_constraints, list(type), class_constraints).
:- mode type_and_constraint_list_matches_exactly(in, in, in, in) is semidet.
% apply a type substitution (i.e. map from tvar -> type)
@@ -166,18 +166,26 @@
map(var, var), map(tvar, type_info_locn)).
:- mode apply_substitutions_to_var_map(in, in, in, out) is det.
-:- pred apply_rec_subst_to_constraints(substitution, list(class_constraint),
- list(class_constraint)).
+:- pred apply_rec_subst_to_constraints(substitution, class_constraints,
+ class_constraints).
:- mode apply_rec_subst_to_constraints(in, in, out) is det.
+:- pred apply_rec_subst_to_constraint_list(substitution, list(class_constraint),
+ list(class_constraint)).
+:- mode apply_rec_subst_to_constraint_list(in, in, out) is det.
+
:- pred apply_rec_subst_to_constraint(substitution, class_constraint,
class_constraint).
:- mode apply_rec_subst_to_constraint(in, in, out) is det.
-:- pred apply_subst_to_constraints(substitution, list(class_constraint),
- list(class_constraint)).
+:- pred apply_subst_to_constraints(substitution, class_constraints,
+ class_constraints).
:- mode apply_subst_to_constraints(in, in, out) is det.
+:- pred apply_subst_to_constraint_list(substitution, list(class_constraint),
+ list(class_constraint)).
+:- mode apply_subst_to_constraint_list(in, in, out) is det.
+
:- pred apply_subst_to_constraint(substitution, class_constraint,
class_constraint).
:- mode apply_subst_to_constraint(in, in, out) is det.
@@ -362,10 +370,10 @@
% will fail for builtin cons_ids.
map__search(Ctors, ConsId, ConsDefns),
CorrectCons = lambda([ConsDefn::in] is semidet, (
- ConsDefn = hlds_cons_defn(_, TypeId, _)
+ ConsDefn = hlds_cons_defn(_, _, TypeId, _)
)),
list__filter(CorrectCons, ConsDefns,
- [hlds_cons_defn(ArgTypes0, _, _)]),
+ [hlds_cons_defn(_, ArgTypes0, _, _)]),
ArgTypes0 \= []
->
module_info_types(ModuleInfo, Types),
@@ -392,7 +400,9 @@
% type_is_no_tag_type/3 is called.
type_is_no_tag_type(Ctors, Ctor, Type) :-
- Ctors = [Ctor - [_FieldName - Type]],
+ Ctors = [SingleCtor],
+ SingleCtor = ctor(ExistQVars, Ctor, [_FieldName - Type]),
+ ExistQVars = [],
unqualify_name(Ctor, Name),
Name \= "type_info",
Name \= "base_type_info",
@@ -423,8 +433,12 @@
:- mode substitute_type_args_2(in, in, out) is det.
substitute_type_args_2([], _, []).
-substitute_type_args_2([Name - Args0 | Ctors0], Subst,
- [Name - Args | Ctors]) :-
+substitute_type_args_2([Ctor0| Ctors0], Subst, [Ctor | Ctors]) :-
+ % Note: prog_io.m ensures that the quantified variables,
+ % if any, are distinct from the parameters, so there'
+ % no need to worry about apply the substitution to ExistQVars
+ Ctor0 = ctor(ExistQVars, Name, Args0),
+ Ctor = ctor(ExistQVars, Name, Args),
substitute_type_args_3(Args0, Subst, Args),
substitute_type_args_2(Ctors0, Subst, Ctors).
@@ -461,9 +475,14 @@
type_list_subsumes(TypesA, TypesB, Subst),
type_list_subsumes(TypesB, TypesA, _),
apply_subst_to_constraints(Subst, ConstraintsA0, ConstraintsA),
- list__sort(ConstraintsA, SortedA),
- list__sort(ConstraintsB, SortedB),
- SortedA = SortedB.
+ ConstraintsA = constraints(UnivCsA, ExistCsA),
+ ConstraintsB = constraints(UnivCsB, ExistCsB),
+ list__sort(UnivCsA, SortedUnivCsA),
+ list__sort(UnivCsB, SortedUnivCsB),
+ SortedUnivCsA = SortedUnivCsB,
+ list__sort(ExistCsA, SortedExistCsA),
+ list__sort(ExistCsB, SortedExistCsB),
+ SortedExistCsA = SortedExistCsB.
%-----------------------------------------------------------------------------%
@@ -732,6 +751,12 @@
%-----------------------------------------------------------------------------%
apply_rec_subst_to_constraints(Subst, Constraints0, Constraints) :-
+ Constraints0 = 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).
+
+apply_rec_subst_to_constraint_list(Subst, Constraints0, Constraints) :-
list__map(apply_rec_subst_to_constraint(Subst), Constraints0,
Constraints).
@@ -743,7 +768,13 @@
strip_term_contexts(Types1, Types),
Constraint = constraint(ClassName, Types).
-apply_subst_to_constraints(Subst, Constraints0, Constraints) :-
+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_constraint_list(Subst, Constraints0, Constraints) :-
list__map(apply_subst_to_constraint(Subst), Constraints0, Constraints).
apply_subst_to_constraint(Subst, Constraint0, Constraint) :-
Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.240.2.1
diff -u -r1.240.2.1 typecheck.m
--- typecheck.m 1998/06/06 11:39:57 1.240.2.1
+++ typecheck.m 1998/06/16 15:57:05
@@ -360,7 +360,7 @@
% `pred foo(T1, T2, ..., TN)' by make_hlds.m.
Inferring = yes,
HeadTypeParams1 = [],
- Constraints = [],
+ Constraints = constraints([], []),
write_pred_progress_message("% Inferring type of ",
PredId, ModuleInfo, IOState0, IOState1)
;
@@ -389,10 +389,10 @@
TypeCheckInfo4),
typecheck_check_for_ambiguity(whole_pred, HeadVars,
TypeCheckInfo4, TypeCheckInfo5),
- typecheck_info_get_final_info(TypeCheckInfo5, Constraints,
+ typecheck_info_get_final_info(TypeCheckInfo5, ExistQVars0,
TypeVarSet, HeadTypeParams2, InferredVarTypes0,
- InferredTypeConstraints, RenamedOldConstraints,
- ConstraintProofs),
+ InferredTypeConstraints, ConstraintProofs,
+ TVarRenaming),
map__optimize(InferredVarTypes0, InferredVarTypes),
ClausesInfo = clauses_info(VarSet, ExplicitVarTypes,
InferredVarTypes, HeadVars, Clauses),
@@ -400,8 +400,9 @@
pred_info_set_typevarset(PredInfo1, TypeVarSet, PredInfo2),
pred_info_set_constraint_proofs(PredInfo2, ConstraintProofs,
PredInfo3),
- map__apply_to_list(HeadVars, InferredVarTypes, ArgTypes),
( Inferring = yes ->
+ map__apply_to_list(HeadVars, InferredVarTypes,
+ ArgTypes),
%
% Now we need to infer which of the head variable
% types must be existentially quantified:
@@ -409,79 +410,82 @@
% set must have been inserted due to an existential
% type in something we called, and thus must be
% existentially quantified.
- % (In theory, we could also infer more variables as
- % being existentially typed, but we try to infer
- % universally quantified types or concrete
- % types in preference to existentially quantified
- % types.)
+ % (Note that concrete types are "more general" than
+ % existentially quantified types, so we prefer to
+ % infer a concrete type if we can rather than an
+ % existential type.)
%
term__vars_list(ArgTypes, ArgTypeVars),
set__list_to_set(ArgTypeVars, ArgTypeVarsSet),
set__list_to_set(HeadTypeParams2, HeadTypeParamsSet),
set__intersect(ArgTypeVarsSet, HeadTypeParamsSet,
ExistQVarsSet),
+ set__difference(ArgTypeVarsSet, ExistQVarsSet,
+ UnivQVarsSet),
set__to_sorted_list(ExistQVarsSet, ExistQVars),
+ set__to_sorted_list(UnivQVarsSet, UnivQVars),
%
% Then we need to insert the universally
% quantified head variable types into the
- % HeadTypeParams set, and delete the
- % existentially quantified ones.
+ % HeadTypeParams set, which will now contain
+ % all the type variables that are produced
+ % either by stuff we call or by our caller.
% This is needed so that it has the right
% value when post_typecheck.m uses it to
% check for unbound type variables.
%
- list__append(ArgTypeVars, HeadTypeParams2,
- HeadTypeParams3),
- list__delete_elems(HeadTypeParams3, ExistQVars,
- HeadTypeParams)
- ;
- ExistQVars = ExistQVars0,
- HeadTypeParams = HeadTypeParams2
- ),
- pred_info_set_head_type_params(PredInfo3, HeadTypeParams,
- PredInfo4),
- pred_info_set_arg_types(PredInfo4, TypeVarSet, ExistQVars,
- ArgTypes, PredInfo5),
- ( Inferring = no ->
- pred_info_set_class_context(PredInfo5,
- RenamedOldConstraints, PredInfo),
- Changed = no
- ;
+ list__append(UnivQVars, HeadTypeParams2,
+ HeadTypeParams),
+
+ %
+ % Now save the information we inferred in the pred_info
+ %
+ pred_info_set_head_type_params(PredInfo3,
+ HeadTypeParams, PredInfo4),
+ pred_info_set_arg_types(PredInfo4, TypeVarSet,
+ ExistQVars, ArgTypes, PredInfo5),
pred_info_get_class_context(PredInfo0,
OldTypeConstraints),
pred_info_set_class_context(PredInfo5,
InferredTypeConstraints, PredInfo),
+ %
+ % Check if anything changed
+ %
(
% If the argument types and the type
% constraints are identical up to renaming,
% then nothing has changed.
- %
- % Note that we can't compare each of the
- % parts seperately, since we need to ensure
- % that the renaming (if any) is consistent
- % over all the arguments and all the
- % constraints. So we need to append all
- % the relevant types into one big type list
- % and then compare them in a single call
- % to indentical_up_to_renaming.
-
- % The call to same_length here 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)
+ argtypes_identical_up_to_renaming(
+ ExistQVars0, ArgTypes0,
+ OldTypeConstraints,
+ ExistQVars, ArgTypes,
+ InferredTypeConstraints)
->
Changed = no
;
Changed = yes
)
+ ; % Inferring = no
+ pred_info_set_head_type_params(PredInfo3,
+ HeadTypeParams2, PredInfo4),
+
+ % leave the original argtypes etc., but rename them,
+ % so that the type variables names match up
+ % (e.g. with the type variables in the
+ % constraint_proofs)
+
+ apply_var_renaming_to_var_list(ExistQVars0,
+ TVarRenaming, ExistQVars),
+ term__apply_variable_renaming_to_list(ArgTypes0,
+ TVarRenaming, ArgTypes),
+ pred_info_set_arg_types(PredInfo4, TypeVarSet,
+ ExistQVars, ArgTypes, PredInfo5),
+ rename_class_constraints(TVarRenaming, Constraints,
+ RenamedOldConstraints),
+ pred_info_set_class_context(PredInfo5,
+ RenamedOldConstraints, PredInfo),
+
+ Changed = no
),
typecheck_info_get_found_error(TypeCheckInfo4, Error),
(
@@ -495,21 +499,62 @@
)
).
-:- pred same_structure(list(class_constraint)::in, list(class_constraint)::in,
- list(type)::out, list(type)::out) is semidet.
+% Check whether the argument types, type quantifiers, and type constraints
+% are identical up to renaming.
+%
+% Note that we can't compare each of the parts seperately, since we need to
+% ensure that the renaming (if any) is consistent over all the arguments and
+% all the constraints. So we need to append all the relevant types into one
+% big type list and then compare them in a single call to
+% identical_up_to_renaming.
+
+:- pred argtypes_identical_up_to_renaming(
+ existq_tvars, list(type), class_constraints,
+ existq_tvars, list(type), class_constraints).
+:- mode argtypes_identical_up_to_renaming(in, in, in, in, in, in) is semidet.
+
+argtypes_identical_up_to_renaming(ExistQVarsA, ArgTypesA, TypeConstraintsA,
+ ExistQVarsB, ArgTypesB, TypeConstraintsB) :-
+ same_structure(TypeConstraintsA, TypeConstraintsB,
+ ConstrainedTypesA, ConstrainedTypesB),
+ term__var_list_to_term_list(ExistQVarsA, ExistQVarTermsA),
+ term__var_list_to_term_list(ExistQVarsB, ExistQVarTermsB),
+ list__condense([ExistQVarTermsA, ArgTypesA, ConstrainedTypesA],
+ TypesListA),
+ list__condense([ExistQVarTermsB, ArgTypesB, ConstrainedTypesB],
+ TypesListB),
+ identical_up_to_renaming(TypesListA, TypesListB).
% 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.
+%
+:- pred same_structure(class_constraints::in, class_constraints::in,
+ list(type)::out, list(type)::out) is semidet.
-same_structure([], [], [], []).
-same_structure([ConstraintA | ConstraintsA], [ConstraintB | ConstraintsB],
+same_structure(ConstraintsA, ConstraintsB, TypesA, TypesB) :-
+ ConstraintsA = constraints(UnivCsA, ExistCsA),
+ ConstraintsB = constraints(UnivCsB, ExistCsB),
+ % these calls to same_length are just an optimization,
+ % to catch the simple cases quicker
+ list__same_length(UnivCsA, UnivCsB),
+ list__same_length(ExistCsA, ExistCsB),
+ same_structure_2(UnivCsA, UnivCsB, UnivTypesA, UnivTypesB),
+ same_structure_2(ExistCsA, ExistCsB, ExistTypesA, ExistTypesB),
+ list__append(ExistTypesA, UnivTypesA, TypesA),
+ list__append(ExistTypesB, UnivTypesB, TypesB).
+
+:- pred same_structure_2(list(class_constraint)::in, list(class_constraint)::in,
+ list(type)::out, list(type)::out) is semidet.
+
+same_structure_2([], [], [], []).
+same_structure_2([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),
+ same_structure_2(ConstraintsA, ConstraintsB, TypesA0, TypesB0),
list__append(ArgTypesA, TypesA0, TypesA),
list__append(ArgTypesB, TypesB0, TypesB).
@@ -585,6 +630,7 @@
% then the body
typecheck_var_has_type_list(HeadVars, ArgTypes, 0),
typecheck_goal(Body0, Body),
+ checkpoint("end of clause"),
{ Clause = clause(Modes, Body, Context) },
typecheck_info_set_context(Context),
typecheck_check_for_ambiguity(clause_only, HeadVars).
@@ -794,7 +840,7 @@
TypeVars, TypeVarSet) },
{ term__var_list_to_term_list(TypeVars, Types) },
typecheck_var_has_polymorphic_type_list(Vars, TypeVarSet, [],
- Types, [])
+ Types, constraints([], []))
).
%-----------------------------------------------------------------------------%
@@ -812,7 +858,7 @@
typecheck_info_set_called_predid(PredCallId),
% The class context is empty because higher-order predicates
% are always monomorphic. Similarly for ExistQVars.
- { ClassContext = [] },
+ { ClassContext = constraints([], []) },
{ ExistQVars = [] },
typecheck_var_has_polymorphic_type_list([PredVar|Args], TypeVarSet,
ExistQVars, [PredVarType|ArgTypes], ClassContext).
@@ -943,7 +989,7 @@
TypeCheckInfo),
(
% sanity check
- PredClassContext \= []
+ PredClassContext \= constraints([], [])
->
error("non-polymorphic pred has class context")
;
@@ -1138,7 +1184,7 @@
% types contained within renamed apart.
:- pred typecheck_var_has_polymorphic_type_list(list(var),
- tvarset, existq_tvars, list(type), list(class_constraint),
+ tvarset, existq_tvars, list(type), class_constraints,
typecheck_info, typecheck_info).
:- mode typecheck_var_has_polymorphic_type_list(in, in, in, in, in,
typecheck_info_di, typecheck_info_uo) is det.
@@ -1154,7 +1200,7 @@
TypeCheckInfo0, TypeCheckInfo).
:- pred rename_apart(type_assign_set, tvarset, existq_tvars, list(type),
- list(class_constraint),
+ class_constraints,
args_type_assign_set, args_type_assign_set).
:- mode rename_apart(in, in, in, in, in, in, out) is det.
@@ -1259,7 +1305,17 @@
type_assign_get_type_bindings(TypeAssign0, Bindings),
apply_rec_subst_to_constraints(Bindings, Constraints0, Constraints),
- list__append(Constraints, OldConstraints, NewConstraints),
+ %
+ % add the dual of the constraints for this functor
+ % to the current constraint set
+ % (anything which we can assume in the caller
+ % is something that we must prove in the callee,
+ % and vice versa)
+ %
+ Constraints = constraints(UnivCs, ExistCs),
+ ConstraintsToAdd = constraints(ExistCs, UnivCs),
+ add_constraints(OldConstraints, ConstraintsToAdd, NewConstraints),
+
type_assign_set_typeclass_constraints(TypeAssign0,
NewConstraints, TypeAssign).
@@ -1317,7 +1373,7 @@
typecheck_var_has_arg_type_2(TypeAssignSet0, VarId).
:- pred arg_type_assign_var_has_type(type_assign, list(type), var,
- list(class_constraint),
+ class_constraints,
args_type_assign_set, args_type_assign_set).
:- mode arg_type_assign_var_has_type(in, in, in, in, in, out) is det.
@@ -1788,7 +1844,7 @@
---> args(
type_assign, % Type assignment,
list(type), % types of callee args,
- list(class_constraint) % constraints from callee
+ class_constraints % constraints from callee
).
:- pred typecheck_unify_var_functor_get_ctors(type_assign_set,
@@ -1956,8 +2012,9 @@
% The constraints are empty here because
% none are added by unification with a
% functor
- TypeAssignSet = [args(TypeAssign2, ArgTypes, []) |
- TypeAssignSet0]
+ Constraints = constraints([], []),
+ TypeAssignSet = [args(TypeAssign2, ArgTypes,
+ Constraints) | TypeAssignSet0]
;
TypeAssignSet = TypeAssignSet0
)
@@ -1967,7 +2024,8 @@
% functor
map__det_insert(VarTypes0, Y, ConsType, VarTypes),
type_assign_set_var_types(TypeAssign1, VarTypes, TypeAssign3),
- TypeAssignSet = [args(TypeAssign3, ArgTypes, []) |
+ Constraints = constraints([], []),
+ TypeAssignSet = [args(TypeAssign3, ArgTypes, Constraints) |
TypeAssignSet0]
).
@@ -2007,8 +2065,7 @@
ClassConstraints2),
type_assign_get_typeclass_constraints(TypeAssign1,
OldConstraints),
- % XXX this is O(n*n) -- is it safe to swap the order here?
- list__append(OldConstraints, ClassConstraints2,
+ add_constraints(OldConstraints, ClassConstraints2,
ClassConstraints),
type_assign_set_typeclass_constraints(TypeAssign1,
ClassConstraints, TypeAssign2),
@@ -2025,6 +2082,17 @@
error("get_cons_stuff: type_assign_rename_apart failed")
).
+:- pred add_constraints(class_constraints, class_constraints,
+ class_constraints).
+:- mode add_constraints(in, in, out) is det.
+
+add_constraints(Cs0, CsToAdd, Cs) :-
+ Cs0 = constraints(UnivCs0, ExistCs0),
+ CsToAdd = constraints(UnivCsToAdd, ExistCsToAdd),
+ list__append(UnivCsToAdd, UnivCs0, UnivCs),
+ list__append(ExistCsToAdd, ExistCs0, ExistCs),
+ Cs = constraints(UnivCs, ExistCs).
+
:- pred apply_substitution_to_var_list(list(var), map(var, term), list(var)).
:- mode apply_substitution_to_var_list(in, in, out) is det.
@@ -2033,6 +2101,22 @@
term__apply_substitution_to_list(Terms0, RenameSubst, Terms),
term__term_list_to_var_list(Terms, Vars).
+:- pred apply_var_renaming_to_var_list(list(var), map(var, var), list(var)).
+:- mode apply_var_renaming_to_var_list(in, in, out) is det.
+
+apply_var_renaming_to_var_list(Vars0, RenameSubst, Vars) :-
+ list__map(apply_var_renaming_to_var(RenameSubst), Vars0, Vars).
+
+:- pred apply_var_renaming_to_var(map(var, var), var, var).
+:- mode apply_var_renaming_to_var(in, in, out) is det.
+
+apply_var_renaming_to_var(RenameSubst, Var0, Var) :-
+ ( map__search(RenameSubst, Var0, Var1) ->
+ Var = Var1
+ ;
+ Var = Var0
+ ).
+
%-----------------------------------------------------------------------------%
% typecheck_lambda_var_has_type(Var, ArgVars, ...)
@@ -2197,9 +2281,11 @@
% type vars
type, % Constructor type
list(type), % Types of the arguments
- list(class_constraint) % Constraints introduced by
- % this constructor (ie. if it
- % is actually a function).
+ class_constraints % Constraints introduced by
+ % this constructor (e.g. if
+ % it is actually a function,
+ % or if it is an existentially
+ % quantified data constructor)
).
:- pred make_pred_cons_info(typecheck_info, pred_id, pred_table, int,
@@ -2286,8 +2372,9 @@
Arity1 is Arity - 1,
higher_order_func_type(Arity1, TypeVarSet, FuncType, ArgTypes, RetType),
ExistQVars = [],
+ Constraints = constraints([], []),
ConsTypeInfos = [cons_type_info(TypeVarSet, ExistQVars, RetType,
- [FuncType | ArgTypes], [])].
+ [FuncType | ArgTypes], Constraints)].
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -2326,8 +2413,7 @@
unit, % UNUSED junk field
- list(class_constraint),
- % The declared typeclass constraints
+ unit, % UNUSED junk field
bool, % Have we already warned about
% highly ambiguous overloading?
@@ -2380,7 +2466,7 @@
%-----------------------------------------------------------------------------%
:- pred typecheck_info_init(io__state, module_info, pred_id, varset,
- varset, map(var, type), headtypes, list(class_constraint),
+ varset, map(var, type), headtypes, class_constraints,
import_status, typecheck_info).
:- mode typecheck_info_init(di, in, in, in, in, in, in, in, in,
typecheck_info_uo)
@@ -2400,7 +2486,7 @@
unify_context(explicit, []), VarSet,
[type_assign(VarTypes, TypeVarSet, HeadTypeParams,
TypeBindings, Constraints, Proofs)],
- FoundTypeError, unit, Constraints,
+ FoundTypeError, unit, unit,
WarnedAboutOverloading, Status
).
@@ -2569,16 +2655,16 @@
%-----------------------------------------------------------------------------%
-:- pred typecheck_info_get_final_info(typecheck_info, list(class_constraint),
+:- pred typecheck_info_get_final_info(typecheck_info, existq_tvars,
tvarset, existq_tvars, map(var, type),
- list(class_constraint), list(class_constraint),
- map(class_constraint, constraint_proof)).
+ class_constraints, map(class_constraint, constraint_proof),
+ map(tvar, tvar)).
:- mode typecheck_info_get_final_info(in, in, out, out, out, out, out, out)
is det.
-typecheck_info_get_final_info(TypeCheckInfo, OldConstraints, NewTypeVarSet,
+typecheck_info_get_final_info(TypeCheckInfo, OldExistQVars, NewTypeVarSet,
NewHeadTypeParams, NewVarTypes, NewTypeConstraints,
- RenamedOldConstraints, NewConstraintProofs) :-
+ NewConstraintProofs, TSubst) :-
typecheck_info_get_type_assign_set(TypeCheckInfo, TypeAssignSet),
( TypeAssignSet = [TypeAssign | _] ->
type_assign_get_head_type_params(TypeAssign, HeadTypeParams),
@@ -2606,11 +2692,14 @@
%
% First, find the set (sorted list) of type variables
- % that we need.
+ % that we need. This must include any type variables
+ % in the inferred types, plus any existentially typed
+ % variables in the declaration.
%
map__values(VarTypes, Types),
term__vars_list(Types, TypeVars0),
- list__sort_and_remove_dups(TypeVars0, TypeVars),
+ list__append(OldExistQVars, TypeVars0, TypeVars1),
+ list__sort_and_remove_dups(TypeVars1, TypeVars),
%
% Next, create a new typevarset with the same number of
% variables.
@@ -2642,17 +2731,15 @@
term__apply_variable_renaming_to_list(Types, TSubst, NewTypes),
map__from_corresponding_lists(Vars, NewTypes, NewVarTypes),
map__apply_to_list(HeadTypeParams, TSubst, NewHeadTypeParams),
- list__map(rename_class_constraint(TSubst), TypeConstraints,
+ rename_class_constraints(TSubst, TypeConstraints,
NewTypeConstraints),
- list__map(rename_class_constraint(TSubst), OldConstraints,
- RenamedOldConstraints),
( map__is_empty(ConstraintProofs) ->
% optimize simple case
NewConstraintProofs = ConstraintProofs
;
map__keys(ConstraintProofs, ProofKeysList),
map__values(ConstraintProofs, ProofValuesList),
- list__map(rename_class_constraint(TSubst),
+ rename_class_constraint_list(TSubst,
ProofKeysList, NewProofKeysList),
list__map(rename_constraint_proof(TSubst),
ProofValuesList, NewProofValuesList),
@@ -2691,6 +2778,25 @@
),
copy_type_var_names(Rest, TypeSubst, NewTypeVarSet1, NewTypeVarSet).
+:- pred rename_class_constraints(map(tvar, tvar), class_constraints,
+ class_constraints).
+:- mode rename_class_constraints(in, in, out) is det.
+
+% apply a type variable renaming to a set of universal and existential
+% class constraints
+
+rename_class_constraints(TSubst, constraints(UnivCs0, ExistCs0),
+ constraints(UnivCs, ExistCs)) :-
+ rename_class_constraint_list(TSubst, UnivCs0, UnivCs),
+ rename_class_constraint_list(TSubst, ExistCs0, ExistCs).
+
+:- pred rename_class_constraint_list(map(tvar, tvar), list(class_constraint),
+ list(class_constraint)).
+:- mode rename_class_constraint_list(in, in, out) is det.
+
+rename_class_constraint_list(TSubst, Constraints0, Constraints) :-
+ list__map(rename_class_constraint(TSubst), Constraints0, Constraints).
+
:- pred rename_class_constraint(map(tvar, tvar), class_constraint,
class_constraint).
:- mode rename_class_constraint(in, in, out) is det.
@@ -2765,25 +2871,22 @@
%-----------------------------------------------------------------------------%
-:- pred typecheck_info_get_constraints(typecheck_info, list(class_constraint)).
-:- mode typecheck_info_get_constraints(typecheck_info_ui, out) is det.
+:- pred typecheck_info_get_junk2(typecheck_info, unit).
+:- mode typecheck_info_get_junk2(typecheck_info_ui, out) is det.
-typecheck_info_get_constraints(TypeCheckInfo, Constraints) :-
+typecheck_info_get_junk2(TypeCheckInfo, Junk) :-
TypeCheckInfo =
- typecheck_info(_,_,_,_,_,_,_,_,_,_,_,Constraints,_,_).
+ typecheck_info(_,_,_,_,_,_,_,_,_,_,_,Junk,_,_).
%-----------------------------------------------------------------------------%
-:- pred typecheck_info_set_constraints(typecheck_info,
- list(class_constraint), typecheck_info).
-:- mode typecheck_info_set_constraints(typecheck_info_di, in,
+:- pred typecheck_info_set_junk2(typecheck_info, unit, typecheck_info).
+:- mode typecheck_info_set_junk2(typecheck_info_di, in,
typecheck_info_uo) is det.
-typecheck_info_set_constraints(TypeCheckInfo0, Constraints,
- TypeCheckInfo) :-
+typecheck_info_set_junk2(TypeCheckInfo0, Junk, TypeCheckInfo) :-
TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,_,M,N),
- TypeCheckInfo =
- typecheck_info(A,B,C,D,E,F,G,H,I,J,K,Constraints,M,N).
+ TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,Junk,M,N).
%-----------------------------------------------------------------------------%
@@ -2869,7 +2972,8 @@
ConsType = term__functor(term__atom(BuiltInTypeName), [],
Context),
varset__init(ConsTypeVarSet),
- ConsInfo = cons_type_info(ConsTypeVarSet, [], ConsType, [], []),
+ ConsInfo = cons_type_info(ConsTypeVarSet, [], ConsType, [],
+ constraints([], [])),
ConsInfoList1 = [ConsInfo | ConsInfoList0]
;
ConsInfoList1 = ConsInfoList0
@@ -2886,27 +2990,6 @@
ConsInfoList = ConsInfoList1
).
- % Add a set of constraints to each type_assign in the typecheck info.
-:- pred typecheck_info_add_type_assign_constraints(list(class_constraint),
- typecheck_info, typecheck_info).
-:- mode typecheck_info_add_type_assign_constraints(in, typecheck_info_di,
- typecheck_info_uo) is det.
-
-typecheck_info_add_type_assign_constraints(NewConstraints, TypecheckInfo0,
- TypecheckInfo) :-
- typecheck_info_get_type_assign_set(TypecheckInfo0, TypeAssignSet0),
- AddConstraints = lambda([TypeAssign0::in, TypeAssign::out] is det,
- (
- type_assign_get_typeclass_constraints(TypeAssign0,
- OldConstraints),
- list__append(NewConstraints, OldConstraints, Constraints),
- type_assign_set_typeclass_constraints(TypeAssign0,
- Constraints, TypeAssign)
- )),
- list__map(AddConstraints, TypeAssignSet0, TypeAssignSet),
- typecheck_info_set_type_assign_set(TypecheckInfo0, TypeAssignSet,
- TypecheckInfo).
-
%-----------------------------------------------------------------------------%
% typecheck_constraints(Inferring, TypeCheckInfo0, TypeCheckInfo)
@@ -2922,14 +3005,18 @@
typecheck_constraints(yes, TypeCheckInfo, TypeCheckInfo).
typecheck_constraints(no, TypeCheckInfo0, TypeCheckInfo) :-
- % reject any type assignment whose constraints have
- % not all been eliminated by context reduction
+ % reject any type assignment whose "constraints to prove"
+ % have not all been eliminated by context reduction
% (i.e. those which have constraints which do not match the
- % declared constraints and which are not redundant for any
- % other reason)
+ % declared constraints or the existentially quantified
+ % constraints for the called preds, and which are not
+ % redundant for any other reason)
typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
- NoConstraints = lambda([TypeAssign::in] is semidet,
- type_assign_get_typeclass_constraints(TypeAssign, [])),
+ NoConstraints = lambda([TypeAssign::in] is semidet, (
+ type_assign_get_typeclass_constraints(TypeAssign, Constraints),
+ Constraints = constraints(_AssumedConstraints,
+ ConstraintsToProve),
+ ConstraintsToProve = [])),
list__filter(NoConstraints, TypeAssignSet0, TypeAssignSet),
(
% Check that we haven't just eliminated
@@ -2961,20 +3048,23 @@
io__write_string(" unsatisfied typeclass constraint(s):\n",
IOState2, IOState3),
- WriteConstraints = lambda([TheTypeAssign::in, IO0::di, IO::uo] is det,
+ WriteConstraints = lambda([TypeAssign::in, IO0::di, IO::uo] is det,
(
type_assign_get_typeclass_constraints(
- TheTypeAssign, TheConstraints0),
- type_assign_get_typevarset(TheTypeAssign, TheVarSet),
- type_assign_get_type_bindings(TheTypeAssign, Bindings),
- apply_rec_subst_to_constraints(Bindings,
- TheConstraints0, TheConstraints1),
- list__sort_and_remove_dups(TheConstraints1,
- TheConstraints),
+ TypeAssign, Constraints),
+ Constraints = constraints(_AssumedConstraints,
+ UnprovenConstraints0),
+
+ type_assign_get_typevarset(TypeAssign, VarSet),
+ type_assign_get_type_bindings(TypeAssign, Bindings),
+ apply_rec_subst_to_constraint_list(Bindings,
+ UnprovenConstraints0, UnprovenConstraints1),
+ list__sort_and_remove_dups(UnprovenConstraints1,
+ UnprovenConstraints),
prog_out__write_context(Context, IO0, IO1),
io__write_string(" ", IO1, IO2),
- io__write_list(TheConstraints, ", ",
- mercury_output_constraint(TheVarSet), IO2, IO3),
+ io__write_list(UnprovenConstraints, ", ",
+ mercury_output_constraint(VarSet), IO2, IO3),
io__write_string(".\n", IO3, IO)
)),
@@ -3033,12 +3123,11 @@
perform_context_reduction(OrigTypeAssignSet, TypeCheckInfo0, TypeCheckInfo) :-
typecheck_info_get_module_info(TypeCheckInfo0, ModuleInfo),
- typecheck_info_get_constraints(TypeCheckInfo0, DeclaredConstraints),
module_info_superclasses(ModuleInfo, SuperClassTable),
module_info_instances(ModuleInfo, InstanceTable),
typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
list__filter_map(reduce_type_assign_context(SuperClassTable,
- InstanceTable, DeclaredConstraints),
+ InstanceTable),
TypeAssignSet0, TypeAssignSet),
(
% Check that this context reduction hasn't eliminated
@@ -3048,9 +3137,12 @@
->
report_unsatisfied_constraints(TypeAssignSet0,
TypeCheckInfo0, TypeCheckInfo1),
- DeleteConstraints = lambda([TA0::in, TA::out] is det,
- type_assign_set_typeclass_constraints(TA0, [], TA)
- ),
+ DeleteConstraints = lambda([TA0::in, TA::out] is det, (
+ type_assign_get_typeclass_constraints(TA0,
+ constraints(AssumedConstraints, _)),
+ type_assign_set_typeclass_constraints(TA0,
+ constraints(AssumedConstraints, []), TA)
+ )),
list__map(DeleteConstraints, OrigTypeAssignSet,
NewTypeAssignSet),
typecheck_info_set_type_assign_set(TypeCheckInfo1,
@@ -3061,20 +3153,24 @@
).
:- pred reduce_type_assign_context(superclass_table, instance_table,
- list(class_constraint), type_assign, type_assign).
-:- mode reduce_type_assign_context(in, in, in, in, out) is semidet.
+ type_assign, type_assign).
+:- mode reduce_type_assign_context(in, in, in, out) is semidet.
-reduce_type_assign_context(SuperClassTable, InstanceTable, DeclaredConstraints,
+reduce_type_assign_context(SuperClassTable, InstanceTable,
TypeAssign0, TypeAssign) :-
type_assign_get_typeclass_constraints(TypeAssign0, Constraints0),
type_assign_get_type_bindings(TypeAssign0, Bindings),
type_assign_get_typevarset(TypeAssign0, Tvarset0),
type_assign_get_constraint_proofs(TypeAssign0, Proofs0),
+ Constraints0 = constraints(AssumedConstraints, UnprovenConstraints0),
+
typecheck__reduce_context_by_rule_application(InstanceTable,
- SuperClassTable, DeclaredConstraints,
+ SuperClassTable, AssumedConstraints,
Bindings, Tvarset0, Tvarset, Proofs0, Proofs,
- Constraints0, Constraints),
+ UnprovenConstraints0, UnprovenConstraints),
+
+ Constraints = constraints(AssumedConstraints, UnprovenConstraints),
type_assign_set_typeclass_constraints(TypeAssign0, Constraints,
TypeAssign1),
@@ -3083,14 +3179,15 @@
typecheck__reduce_context_by_rule_application(InstanceTable, SuperClassTable,
- DeclaredConstraints, Bindings, Tvarset0, Tvarset,
+ AssumedConstraints, Bindings, Tvarset0, Tvarset,
Proofs0, Proofs, Constraints0, Constraints) :-
- apply_rec_subst_to_constraints(Bindings, Constraints0, Constraints1),
- eliminate_declared_constraints(Constraints1, DeclaredConstraints,
+ apply_rec_subst_to_constraint_list(Bindings, Constraints0,
+ Constraints1),
+ eliminate_assumed_constraints(Constraints1, AssumedConstraints,
Constraints2, Changed1),
apply_instance_rules(Constraints2, InstanceTable,
Tvarset0, Tvarset1, Proofs0, Proofs1, Constraints3, Changed2),
- apply_class_rules(Constraints3, DeclaredConstraints, SuperClassTable,
+ apply_class_rules(Constraints3, AssumedConstraints, SuperClassTable,
Tvarset0, Proofs1, Proofs2, Constraints4, Changed3),
(
Changed1 = no, Changed2 = no, Changed3 = no
@@ -3101,20 +3198,20 @@
Proofs = Proofs2
;
typecheck__reduce_context_by_rule_application(InstanceTable,
- SuperClassTable, DeclaredConstraints, Bindings,
+ SuperClassTable, AssumedConstraints, Bindings,
Tvarset1, Tvarset, Proofs2, Proofs,
Constraints4, Constraints)
).
-:- pred eliminate_declared_constraints(list(class_constraint),
+:- pred eliminate_assumed_constraints(list(class_constraint),
list(class_constraint), list(class_constraint), bool).
-:- mode eliminate_declared_constraints(in, in, out, out) is det.
+:- mode eliminate_assumed_constraints(in, in, out, out) is det.
-eliminate_declared_constraints([], _, [], no).
-eliminate_declared_constraints([C|Cs], DeclaredCs, NewCs, Changed) :-
- eliminate_declared_constraints(Cs, DeclaredCs, NewCs0, Changed0),
+eliminate_assumed_constraints([], _, [], no).
+eliminate_assumed_constraints([C|Cs], AssumedCs, NewCs, Changed) :-
+ eliminate_assumed_constraints(Cs, AssumedCs, NewCs0, Changed0),
(
- list__member(C, DeclaredCs)
+ list__member(C, AssumedCs)
->
NewCs = NewCs0,
Changed = yes
@@ -3215,9 +3312,9 @@
RenameSubst, InstanceTypes),
type_list_subsumes(InstanceTypes, Types, Subst)
->
- apply_rec_subst_to_constraints(RenameSubst, NewConstraints0,
+ apply_rec_subst_to_constraint_list(RenameSubst, NewConstraints0,
NewConstraints1),
- apply_rec_subst_to_constraints(Subst, NewConstraints1,
+ apply_rec_subst_to_constraint_list(Subst, NewConstraints1,
NewConstraints),
NewTVarSet = NewTVarSet0,
NewProof = apply_instance(hlds_instance_defn(ModuleName,
@@ -3241,19 +3338,19 @@
:- mode apply_class_rules(in, in, in, in, in, out, out, out) is det.
apply_class_rules([], _, _, _, Proofs, Proofs, [], no).
-apply_class_rules([C|Constraints0], DeclaredConstraints, SuperClassTable,
+apply_class_rules([C|Constraints0], AssumedConstraints, SuperClassTable,
TVarSet, Proofs0, Proofs, Constraints, Changed) :-
(
Parents = [],
- eliminate_constraint_by_class_rules(C, DeclaredConstraints,
+ eliminate_constraint_by_class_rules(C, AssumedConstraints,
SuperClassTable, TVarSet, Parents, Proofs0, Proofs1)
->
- apply_class_rules(Constraints0, DeclaredConstraints,
+ apply_class_rules(Constraints0, AssumedConstraints,
SuperClassTable, TVarSet, Proofs1, Proofs,
Constraints, _),
Changed = yes
;
- apply_class_rules(Constraints0, DeclaredConstraints,
+ apply_class_rules(Constraints0, AssumedConstraints,
SuperClassTable, TVarSet, Proofs0, Proofs,
Constraints1, Changed),
Constraints = [C|Constraints1]
@@ -3272,7 +3369,7 @@
:- mode eliminate_constraint_by_class_rules(in, in, in, in, in, in, out)
is semidet.
-eliminate_constraint_by_class_rules(C, DeclaredConstraints, SuperClassTable,
+eliminate_constraint_by_class_rules(C, AssumedConstraints, SuperClassTable,
TVarSet, ParentConstraints, Proofs0, Proofs) :-
% Make sure we aren't in a cycle in the
@@ -3318,7 +3415,7 @@
(
% Do the first level of search
FindSub = lambda([TheConstraint::in] is semidet,(
- list__member(TheConstraint, DeclaredConstraints)
+ list__member(TheConstraint, AssumedConstraints)
)),
list__filter(FindSub, SubClassConstraints, [Sub|_])
->
@@ -3331,7 +3428,7 @@
SubClassSearch = lambda([Constraint::in, CnstrtAndProof::out]
is semidet, (
eliminate_constraint_by_class_rules(Constraint,
- DeclaredConstraints, SuperClassTable,
+ AssumedConstraints, SuperClassTable,
TVarSet, NewParentConstraints,
Proofs0, SubProofs),
CnstrtAndProof = Constraint - SubProofs
@@ -3375,14 +3472,15 @@
:- mode convert_cons_defn(typecheck_info_ui, in, out) is det.
convert_cons_defn(TypeCheckInfo, HLDS_ConsDefn, ConsTypeInfo) :-
- HLDS_ConsDefn = hlds_cons_defn(ArgTypes, TypeId, Context),
+ HLDS_ConsDefn = hlds_cons_defn(ExistQVars, ArgTypes, TypeId, Context),
typecheck_info_get_types(TypeCheckInfo, Types),
map__lookup(Types, TypeId, TypeDefn),
hlds_data__get_type_defn_tvarset(TypeDefn, ConsTypeVarSet),
hlds_data__get_type_defn_tparams(TypeDefn, ConsTypeParams),
construct_type(TypeId, ConsTypeParams, Context, ConsType),
- ConsTypeInfo = cons_type_info(ConsTypeVarSet, [],
- ConsType, ArgTypes, []).
+ Constraints = constraints([], []), % XXX we should allow some here
+ ConsTypeInfo = cons_type_info(ConsTypeVarSet, ExistQVars,
+ ConsType, ArgTypes, Constraints).
%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
@@ -3398,7 +3496,10 @@
headtypes, % universally quantified
% type variables
tsubst, % type bindings
- list(class_constraint), % typeclass constraints
+ class_constraints, % typeclass constraints:
+ % both universal (assumed)
+ % and existential (the ones
+ % we need to prove)
map(class_constraint, % for each constraint
constraint_proof) % constraint found to be
% redundant, why is it so?
@@ -3438,8 +3539,7 @@
TypeBindings).
%-----------------------------------------------------------------------------%
-:- pred type_assign_get_typeclass_constraints(type_assign,
- list(class_constraint)).
+:- pred type_assign_get_typeclass_constraints(type_assign, class_constraints).
:- mode type_assign_get_typeclass_constraints(in, out) is det.
type_assign_get_typeclass_constraints(type_assign(_, _, _, _, Constraints, _),
@@ -3486,8 +3586,8 @@
%-----------------------------------------------------------------------------%
-:- pred type_assign_set_typeclass_constraints(type_assign,
- list(class_constraint), type_assign).
+:- pred type_assign_set_typeclass_constraints(type_assign, class_constraints,
+ type_assign).
:- mode type_assign_set_typeclass_constraints(in, in, out) is det.
type_assign_set_typeclass_constraints(type_assign(A, B, C, D, _, F),
@@ -4106,16 +4206,23 @@
write_type_assign(TypeAssign, VarSet) -->
{
+ type_assign_get_head_type_params(TypeAssign, HeadTypeParams),
type_assign_get_var_types(TypeAssign, VarTypes),
type_assign_get_typeclass_constraints(TypeAssign, Constraints),
type_assign_get_type_bindings(TypeAssign, TypeBindings),
type_assign_get_typevarset(TypeAssign, TypeVarSet),
map__keys(VarTypes, Vars)
},
+ ( { HeadTypeParams = [] } ->
+ []
+ ;
+ io__write_string("some ["),
+ mercury_output_vars(HeadTypeParams, TypeVarSet, yes),
+ io__write_string("]\n\t")
+ ),
write_type_assign_types(Vars, VarSet, VarTypes,
TypeBindings, TypeVarSet, no),
- write_type_assign_constraints(Constraints,
- TypeBindings, TypeVarSet, no),
+ write_type_assign_constraints(Constraints, TypeBindings, TypeVarSet),
io__write_string("\n").
:- pred write_type_assign_types(list(var), varset, map(var, type),
@@ -4149,22 +4256,33 @@
TypeVarSet, FoundOne)
).
-:- pred write_type_assign_constraints(list(class_constraint),
+:- pred write_type_assign_constraints(class_constraints,
+ tsubst, tvarset, io__state, io__state).
+:- mode write_type_assign_constraints(in, in, in, di, uo) is det.
+
+write_type_assign_constraints(Constraints, TypeBindings, TypeVarSet) -->
+ { Constraints = constraints(AssumedConstraints, ConstraintsToProve) },
+ write_type_assign_constraints("&", AssumedConstraints,
+ TypeBindings, TypeVarSet, no),
+ write_type_assign_constraints("<=", ConstraintsToProve,
+ TypeBindings, TypeVarSet, no).
+
+:- pred write_type_assign_constraints(string, list(class_constraint),
tsubst, tvarset, bool, io__state, io__state).
-:- mode write_type_assign_constraints(in, in, in, in, di, uo) is det.
+:- mode write_type_assign_constraints(in, in, in, in, in, di, uo) is det.
-write_type_assign_constraints([], _, _, _) --> [].
-write_type_assign_constraints([Constraint | Constraints],
+write_type_assign_constraints(_, [], _, _, _) --> [].
+write_type_assign_constraints(Operator, [Constraint | Constraints],
TypeBindings, TypeVarSet, FoundOne) -->
( { FoundOne = no } ->
- io__write_string("\n\t<= ")
+ io__write_strings(["\n\t", Operator, " "])
;
io__write_string(",\n\t ")
),
{ apply_rec_subst_to_constraint(TypeBindings, Constraint,
BoundConstraint) },
mercury_output_constraint(TypeVarSet, BoundConstraint),
- write_type_assign_constraints(Constraints,
+ write_type_assign_constraints(Operator, Constraints,
TypeBindings, TypeVarSet, yes).
% write_type_b writes out a type after applying the type bindings.
@@ -4175,7 +4293,7 @@
write_type_b(Type, TypeVarSet, TypeBindings) -->
{ term__apply_rec_substitution(Type, TypeBindings, Type2) },
{ strip_builtin_qualifiers_from_type(Type2, Type3) },
- mercury_output_term(Type3, TypeVarSet, no).
+ mercury_output_term(Type3, TypeVarSet, yes).
%-----------------------------------------------------------------------------%
Index: compiler/unify_proc.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unify_proc.m,v
retrieving revision 1.68
diff -u -r1.68 unify_proc.m
--- unify_proc.m 1998/05/25 21:49:00 1.68
+++ unify_proc.m 1998/06/09 09:21:51
@@ -594,7 +594,7 @@
unify_proc__generate_du_unify_clauses([], _H1, _H2, _Context, []) --> [].
unify_proc__generate_du_unify_clauses([Ctor | Ctors], H1, H2, Context,
[Clause | Clauses]) -->
- { Ctor = FunctorName - ArgTypes },
+ { Ctor = ctor(_ExistQVars, FunctorName, ArgTypes) },
{ list__length(ArgTypes, FunctorArity) },
{ FunctorConsId = cons(FunctorName, FunctorArity) },
unify_proc__make_fresh_vars(ArgTypes, Vars1),
@@ -651,7 +651,7 @@
unify_proc__generate_du_index_clauses([], _X, _Index, _Context, _N, []) --> [].
unify_proc__generate_du_index_clauses([Ctor | Ctors], X, Index, Context, N,
[Clause | Clauses]) -->
- { Ctor = FunctorName - ArgTypes },
+ { Ctor = ctor(_ExistQVars, FunctorName, ArgTypes) },
{ list__length(ArgTypes, FunctorArity) },
{ FunctorConsId = cons(FunctorName, FunctorArity) },
unify_proc__make_fresh_vars(ArgTypes, ArgVars),
@@ -842,7 +842,7 @@
is det.
unify_proc__generate_compare_case(Ctor, R, X, Y, Context, Case) -->
- { Ctor = FunctorName - ArgTypes },
+ { Ctor = ctor(_ExistQVars, FunctorName, ArgTypes) },
{ list__length(ArgTypes, FunctorArity) },
{ FunctorConsId = cons(FunctorName, FunctorArity) },
unify_proc__make_fresh_vars(ArgTypes, Vars1),
--
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