mercurylang/mercury
1
0
Fork 0
mirror of https://github.com/Mercury-Language/mercury.git synced 2026-04-15 01:13:30 +00:00
Code Issues Projects Releases Wiki Activity
Files
ad942553b7b56ad4a0cc50647fdc81672935aca7
mercury/compiler/inst_match.m
Zoltan Somogyi ad942553b7 Fix too-long lines.
2026-02-04 04:16:37 +11:00

1885 lines
78 KiB
Mathematica
Raw Blame History

%---------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 1995-1998, 2000-2012 The University of Melbourne.
% Copyright (C) 2014-2018, 2021, 2023-2026 The Mercury team.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%---------------------------------------------------------------------------%
%
% File: inst_match.m.
% Author: fjh.
%
% This module defines some utility routines for comparing insts that are used
% by the mode analysis pass, and by the rest of the compiler.
%
% We do allow `bound' and `ground' to match `any', based on the assumption
% that `bound' and `ground' are represented in the same way as `any', i.e.
% that we use the type system rather than the mode system to distinguish
% between different representations.
%
%---------------------------------------------------------------------------%
:- module check_hlds.inst_match.
:- interface.
:- import_module hlds.
:- import_module hlds.hlds_module.
:- import_module parse_tree.
:- import_module parse_tree.prog_data.
%---------------------------------------------------------------------------%
% inst_matches_initial(ModuleInfo, Type, InstA, InstB):
%
% Succeed iff `InstA' specifies at least as much information as `InstB',
% and in those parts where they specify the same information, `InstA'
% is at least as instantiated as `InstB'. Thus, the call
% inst_matches_initial(MI, T, not_reached, ground) succeeds, since
% not_reached contains more information than ground - but not vice versa.
% Similarly, inst_matches_initial(MI, T, bound(a), bound(a;b)) should
% succeed, but inst_matches_initial(MI, T, bound(a;b), bound(a)) should
% not.
%
:- pred inst_matches_initial(module_info::in, mer_type::in,
mer_inst::in, mer_inst::in) is semidet.
% This version of inst_matches_initial builds up a substitution map
% (inst_var_sub). For each inst_var which occurs in InstA there will be
% a substitution to the corresponding inst in InstB.
%
:- pred inst_matches_initial_sub(mer_type::in, mer_inst::in, mer_inst::in,
module_info::in, module_info::out, inst_var_sub::in, inst_var_sub::out)
is semidet.
% This version of inst_matches_initial does not allow implied modes.
% This makes it almost the same as inst_matches_final. The only difference
% is in the way it handles constrained_inst_vars.
%
:- pred inst_matches_initial_no_implied_modes(module_info::in, mer_type::in,
mer_inst::in, mer_inst::in) is semidet.
% A version of the above that also computes the inst_var_sub.
%
:- pred inst_matches_initial_no_implied_modes_sub(mer_type::in,
mer_inst::in, mer_inst::in, module_info::in, module_info::out,
inst_var_sub::in, inst_var_sub::out) is semidet.
% inst_is_at_least_as_instantiated(InstA, InstB, Type, ModuleInfo)
% succeeds iff InstA is at least as instantiated as InstB. This defines
% a partial order which is the same as inst_matches_initial except that
% uniqueness comparisons are reversed and we don't allow
% inst_is_at_least_as_instantiated(any, any).
%
% XXX It is not actually clear what "this predicate" refers to
% in the next two paragraphs :-(
%
% The difference between inst_matches_initial and inst_matches_final is
% that inst_matches_initial requires only something which is at least as
% instantiated, whereas this predicate wants something which is an exact
% match (or not reachable).
%
% Note that this predicate is not symmetric, because of the existence of
% `not_reached' insts: not_reached matches_final with anything, but not
% everything matches_final with not_reached - in fact only not_reached
% matches_final with not_reached. It is also asymmetric with respect to
% unique insts.
%
% It might be a good idea to fold inst_matches_initial and
% inst_matches_final into a single predicate inst_matches(When, ...) where
% When is either `initial' or `final'.
%
:- pred inst_is_at_least_as_instantiated(module_info::in, mer_type::in,
mer_inst::in, mer_inst::in) is semidet.
%---------------------------------------------------------------------------%
% inst_matches_final(ModuleInfo, Type, InstA, InstB):
%
% Succeed iff InstA is compatible with InstB, i.e. iff InstA will satisfy
% the final inst requirement InstB. This is true if the information
% specified by InstA is at least as great as that specified by InstB,
% and where the information is the same and both insts specify a binding,
% the binding must be identical.
%
:- pred inst_matches_final(module_info::in, mer_type::in,
mer_inst::in, mer_inst::in) is semidet.
% Normally ground matches bound(...) only if the latter is complete for the
% type. However, the mode checker would reject some compiler-generated
% predicates in the absence of mode checking. We work around the problem by
% allowing ground to match incomplete bound insts when checking the final
% insts of those generated predicates.
%
:- type ground_matches_bound
---> ground_matches_bound_if_complete
; ground_matches_bound_always.
:- pred inst_matches_final_gmb(module_info::in, ground_matches_bound::in,
mer_type::in, mer_inst::in, mer_inst::in) is semidet.
%---------------------------------------------------------------------------%
% inst_matches_binding(ModuleInfo, Type, InstA, InstB):
%
% Succeed iff the binding of InstA is definitely exactly the same as
% that of InstB. This is the same as inst_matches_final except that it
% ignores uniqueness, and that `any' does not match itself. It is used
% to check whether variables get bound in negated contexts.
%
:- pred inst_matches_binding(module_info::in, mer_type::in,
mer_inst::in, mer_inst::in) is semidet.
% inst_matches_binding_allow_any_any is the same as
% inst_matches_binding except that it also allows `any' to match `any'.
%
:- pred inst_matches_binding_allow_any_any(module_info::in, mer_type::in,
mer_inst::in, mer_inst::in) is semidet.
%---------------------------------------------------------------------------%
% inst_contains_nondefault_func_mode(ModuleInfo, Type, Inst) succeeds
% iff the inst contains a higher-order function inst that does not match
% the default function mode `(in, ..., in) = out is det'.
% E.g. this predicate fails for "func(in) = uo" because that matches the
% default func mode "func(in) = out", even though it isn't the same as
% the default func mode.
%
:- pred inst_contains_nondefault_func_mode(module_info::in, mer_type::in,
mer_inst::in) is semidet.
%---------------------------------------------------------------------------%
% Succeed iff the second argument is not a function ho_inst_info
% whose mode does not match the default func mode.
%
:- pred ho_inst_info_matches_ground(module_info::in, mer_type::in,
ho_inst_info::in) is semidet.
% Succeed iff the second argument is not a function pred_inst_info
% whose mode does not match the default func mode.
%
:- pred pred_inst_matches_ground(module_info::in, mer_type::in,
pred_inst_info::in) is semidet.
% pred_inst_matches(ModuleInfo, Type, PredInstA, PredInstB)
%
% Succeeds if PredInstA specifies a pred that can be used wherever and
% whenever PredInstB could be used. This is true if they both have the
% same PredOrFunc indicator and the same determinism, and if the arguments
% match using pred_inst_argmodes_match.
%
:- pred pred_inst_matches(module_info::in, mer_type::in,
pred_inst_info::in, pred_inst_info::in) is semidet.
%---------------------------------------------------------------------------%
% unique_matches_initial(A, B) succeeds if A >= B in the ordering
% clobbered < mostly_clobbered < shared < mostly_unique < unique.
%
:- pred unique_matches_initial(uniqueness::in, uniqueness::in) is semidet.
% unique_matches_final(A, B) succeeds if A >= B in the ordering
% clobbered < mostly_clobbered < shared < mostly_unique < unique.
%
:- pred unique_matches_final(uniqueness::in, uniqueness::in) is semidet.
%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%
:- implementation.
:- import_module check_hlds.inst_abstract_unify.
:- import_module check_hlds.inst_merge.
:- import_module hlds.hlds_data.
:- import_module hlds.inst_lookup.
:- import_module hlds.inst_test.
:- import_module hlds.inst_util.
:- import_module hlds.mode_util.
:- import_module mdbcomp.
:- import_module mdbcomp.prim_data.
:- import_module mdbcomp.sym_name.
:- import_module parse_tree.prog_mode.
:- import_module parse_tree.prog_type.
:- import_module parse_tree.prog_type_subst.
:- import_module bool.
:- import_module int.
:- import_module list.
:- import_module map.
:- import_module one_or_more.
:- import_module require.
:- import_module set.
:- import_module set_tree234.
:- import_module term.
%---------------------------------------------------------------------------%
inst_matches_initial(ModuleInfo, Type, InstA, InstB) :-
inst_matches_initial_1(Type, InstA, InstB,
ModuleInfo, _, no_state, _).
inst_matches_initial_sub(Type, InstA, InstB, !ModuleInfo, !Sub) :-
inst_matches_initial_1(Type, InstA, InstB, !ModuleInfo,
inst_var_sub_state(!.Sub), MaybeState),
MaybeState = inst_var_sub_state(!:Sub).
inst_matches_initial_no_implied_modes(ModuleInfo, Type, InstA, InstB) :-
Info0 = init_inst_match_info(ModuleInfo, no_state, uc_match,
any_does_match_any, ground_matches_bound_if_complete),
inst_matches_final_mt(cs_forward, Type, InstA, InstB, Info0, _).
inst_matches_initial_no_implied_modes_sub(Type, InstA, InstB,
!ModuleInfo, !Sub) :-
Info0 = init_inst_match_info(!.ModuleInfo, inst_var_sub_state(!.Sub),
uc_match, any_does_match_any, ground_matches_bound_if_complete),
inst_matches_final_mt(cs_forward, Type, InstA, InstB, Info0, Info),
!:ModuleInfo = Info ^ imi_module_info,
inst_var_sub_state(!:Sub) = Info ^ imi_maybe_state.
inst_is_at_least_as_instantiated(ModuleInfo, Type, InstA, InstB) :-
Info0 = init_inst_match_info(ModuleInfo, no_state, uc_instantiated,
any_does_not_match_any, ground_matches_bound_if_complete),
inst_matches_initial_mt(cs_none, Type, InstA, InstB, Info0, _).
%---------------------%
:- pred inst_matches_initial_1(mer_type, mer_inst, mer_inst,
module_info, module_info, maybe_inst_match_state, maybe_inst_match_state).
:- mode inst_matches_initial_1(in, in, in, in, out,
in(no_state), out(no_state)) is semidet.
:- mode inst_matches_initial_1(in, in, in, in, out,
in(inst_var_sub_state), out(inst_var_sub_state)) is semidet.
inst_matches_initial_1(Type, InstA, InstB, !ModuleInfo, !MaybeState) :-
Info0 = init_inst_match_info(!.ModuleInfo, !.MaybeState, uc_match,
any_does_match_any, ground_matches_bound_if_complete),
inst_matches_initial_mt(cs_forward, Type, InstA, InstB, Info0, Info),
!:ModuleInfo = Info ^ imi_module_info,
!:MaybeState = Info ^ imi_maybe_state.
:- pred inst_matches_initial_mt(calculate_sub, mer_type,
mer_inst, mer_inst, inst_match_info, inst_match_info).
:- mode inst_matches_initial_mt(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_matches_initial_mt(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_matches_initial_mt(CalcSub, Type, InstA, InstB, !Info) :-
ThisExpansion = inst_match_inputs(InstA, InstB, Type),
Expansions0 = !.Info ^ imi_expansions,
( if expansion_insert_new(ThisExpansion, Expansions0, Expansions) then
!Info ^ imi_expansions := Expansions,
inst_expand(!.Info ^ imi_module_info, InstA, ExpandedInstA),
inst_expand(!.Info ^ imi_module_info, InstB, ExpandedInstB),
maybe_handle_inst_var_subs(CalcSub, Type, ExpandedInstA, ExpandedInstB,
InstVarSubResult, !Info),
require_complete_switch [InstVarSubResult]
(
InstVarSubResult = ivsr_recurse(RecurseInstA, RecurseInstB),
inst_matches_initial_mt(cs_forward, Type,
RecurseInstA, RecurseInstB, !Info)
;
InstVarSubResult = ivsr_continue(ContCalcSub,
ContinueInstA, ContinueInstB),
inst_matches_initial_mt_2(ContCalcSub, Type,
ContinueInstA, ContinueInstB, !Info)
)
else
true
).
:- pred inst_matches_initial_mt_2(calculate_sub, mer_type,
mer_inst, mer_inst, inst_match_info, inst_match_info).
:- mode inst_matches_initial_mt_2(in, in,
in(mer_inst_expanded), in(mer_inst_expanded),
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_matches_initial_mt_2(in, in,
in(mer_inst_expanded), in(mer_inst_expanded),
in(imi_ivs), out(imi_ivs)) is semidet.
inst_matches_initial_mt_2(CalcSub, Type, InstA, InstB, !Info) :-
% To avoid infinite regress, we assume that inst_matches_initial is true
% for any pairs of insts which occur in `Expansions'.
%
% XXX Maybe we could use the inst result field of bound/3 insts
% in some places.
require_complete_switch [InstA]
(
InstA = free,
InstB = free
;
InstA = any(UniqA, HOInstInfoA),
require_complete_switch [InstB]
(
InstB = free
;
InstB = ground(_, _),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqA,
HOInstInfoA, NextInstA),
inst_matches_initial_mt(CalcSub, Type, NextInstA, InstB, !Info)
;
InstB = bound(_, _, _),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqA,
HOInstInfoA, NextInstA),
inst_matches_initial_mt(CalcSub, Type, NextInstA, InstB, !Info)
;
InstB = any(UniqB, HOInstInfoB),
!.Info ^ imi_any_matches_any = any_does_match_any,
compare_uniqueness(!.Info ^ imi_uniqueness_comparison,
UniqA, UniqB),
ho_inst_info_matches_initial(CalcSub, Type,
HOInstInfoA, HOInstInfoB, !Info)
;
( InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
; InstB = not_reached
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = bound(UniqA, InstResultsA, BoundFunctorsA),
require_complete_switch [InstB]
(
InstB = free
;
InstB = ground(UniqB, none_or_default_func),
compare_uniqueness(!.Info ^ imi_uniqueness_comparison,
UniqA, UniqB),
inst_results_bound_functor_list_is_ground_mt(
!.Info ^ imi_module_info, Type, InstResultsA, BoundFunctorsA),
compare_bound_functor_list_uniq(!.Info ^ imi_module_info,
!.Info ^ imi_uniqueness_comparison, BoundFunctorsA, UniqB),
inst_contains_nondefault_func_mode_1(CalcSub, Type, InstA, no,
!Info)
;
InstB = bound(UniqB, _InstResultsB, BoundFunctorsB),
( if
same_addr_insts(InstA, InstB),
InstResultsA = inst_test_results_fgtc
then
true
else
compare_uniqueness(!.Info ^ imi_uniqueness_comparison,
UniqA, UniqB),
bound_functor_list_matches_initial_mt(CalcSub, Type,
BoundFunctorsA, BoundFunctorsB, !Info)
)
;
InstB = any(UniqB, none_or_default_func),
compare_uniqueness(!.Info ^ imi_uniqueness_comparison,
UniqA, UniqB),
compare_bound_functor_list_uniq(!.Info ^ imi_module_info,
!.Info ^ imi_uniqueness_comparison, BoundFunctorsA, UniqB),
inst_contains_nondefault_func_mode_1(CalcSub, Type, InstA, no,
!Info)
;
( InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
; InstB = not_reached
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = ground(UniqA, HOInstInfoA),
require_complete_switch [InstB]
(
InstB = free
;
InstB = ground(UniqB, HOInstInfoB),
compare_uniqueness(!.Info ^ imi_uniqueness_comparison,
UniqA, UniqB),
ho_inst_info_matches_initial(CalcSub, Type,
HOInstInfoA, HOInstInfoB, !Info)
;
InstB = bound(UniqB, _InstResultsB, BoundFunctorsB),
ModuleInfo = !.Info ^ imi_module_info,
compare_uniqueness(!.Info ^ imi_uniqueness_comparison,
UniqA, UniqB),
set.init(CompletenessExpansions0),
bound_functor_list_is_complete_for_type(ModuleInfo, Type,
CompletenessExpansions0, BoundFunctorsB),
ground_matches_initial_bound_functor_list(CalcSub, UniqA, Type,
BoundFunctorsB, !Info)
;
InstB = any(UniqB, HOInstInfoB),
compare_uniqueness(!.Info ^ imi_uniqueness_comparison,
UniqA, UniqB),
ho_inst_info_matches_initial(CalcSub, Type,
HOInstInfoA, HOInstInfoB, !Info)
;
( InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
; InstB = not_reached
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = not_reached
;
( InstA = constrained_inst_vars(_, _)
; InstA = inst_var(_)
),
% Our callers should have expanded out these insts, but some of them
% do not do that. In particular, inst_is_at_least_as_instantiated
% calls inst_matches_initial_mt with cs_none.
% XXX If and when this is fixed, and all callers expand out these
% insts, update the expected insts of InstA/InstB to reflect this.
unexpected($pred, "unexpected InstA")
).
%---------------------%
% This predicate assumes that the check of
% `bound_functor_list_is_complete_for_type' is done by the caller.
%
:- pred ground_matches_initial_bound_functor_list(calculate_sub,
uniqueness, mer_type, list(bound_functor),
inst_match_info, inst_match_info).
:- mode ground_matches_initial_bound_functor_list(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode ground_matches_initial_bound_functor_list(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
ground_matches_initial_bound_functor_list(_, _, _, [], !Info).
ground_matches_initial_bound_functor_list(CalcSub, Uniq, Type,
[BoundFunctor | BoundFunctors], !Info) :-
get_cons_id_arg_types_for_bound_functor(!.Info ^ imi_module_info, Type,
BoundFunctor, ArgTypes),
BoundFunctor = bound_functor(_ConsId, ArgInsts),
ground_matches_initial_inst_list(CalcSub, Uniq, ArgTypes, ArgInsts, !Info),
ground_matches_initial_bound_functor_list(CalcSub, Uniq, Type,
BoundFunctors, !Info).
:- pred ground_matches_initial_inst_list(calculate_sub, uniqueness,
list(mer_type), list(mer_inst), inst_match_info, inst_match_info).
:- mode ground_matches_initial_inst_list(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode ground_matches_initial_inst_list(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
ground_matches_initial_inst_list(_, _, [], [], !Info).
ground_matches_initial_inst_list(CalcSub, Uniq,
[Type | Types], [Inst | Insts], !Info) :-
Ground = ground(Uniq, none_or_default_func),
inst_matches_initial_mt(CalcSub, Type, Ground, Inst, !Info),
ground_matches_initial_inst_list(CalcSub, Uniq, Types, Insts, !Info).
%---------------------%
% This predicate checks if two ho_inst_infos match_initial.
% It does not check uniqueness.
%
:- pred ho_inst_info_matches_initial(calculate_sub, mer_type,
ho_inst_info, ho_inst_info, inst_match_info, inst_match_info).
:- mode ho_inst_info_matches_initial(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode ho_inst_info_matches_initial(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
ho_inst_info_matches_initial(CalcSub, Type, HOInstInfoA, HOInstInfoB, !Info) :-
(
HOInstInfoB = none_or_default_func,
ho_inst_info_matches_ground_1(CalcSub, Type, HOInstInfoA, !Info)
;
HOInstInfoB = higher_order(PredInstB),
(
HOInstInfoA = none_or_default_func,
PredInstB = pred_inst_info(pf_function, ArgModes, _, _Det),
Arity = list.length(ArgModes),
PredInstA = pred_inst_info_default_func_mode(Arity)
;
HOInstInfoA = higher_order(PredInstA)
),
pred_inst_matches_1(CalcSub, Type, PredInstA, PredInstB, !Info)
).
%---------------------%
:- pred compare_bound_functor_list_uniq(module_info::in,
uniqueness_comparison::in,
list(bound_functor)::in, uniqueness::in) is semidet.
compare_bound_functor_list_uniq(ModuleInfo, uc_match, BoundFunctors, Uniq) :-
bound_functor_list_matches_uniq(ModuleInfo, Uniq, BoundFunctors).
compare_bound_functor_list_uniq(ModuleInfo, uc_instantiated,
BoundFunctors, Uniq) :-
uniq_matches_bound_functor_list(ModuleInfo, Uniq, BoundFunctors).
:- pred bound_functor_list_matches_uniq(module_info::in, uniqueness::in,
list(bound_functor)::in) is semidet.
bound_functor_list_matches_uniq(ModuleInfo, Uniq, BoundFunctors) :-
( if Uniq = unique then
bound_functor_list_is_unique(ModuleInfo, BoundFunctors)
else if Uniq = mostly_unique then
bound_functor_list_is_mostly_unique(ModuleInfo, BoundFunctors)
else
true
).
:- pred uniq_matches_bound_functor_list(module_info::in, uniqueness::in,
list(bound_functor)::in) is semidet.
uniq_matches_bound_functor_list(ModuleInfo, Uniq, BoundFunctors) :-
( if Uniq = shared then
bound_functor_list_is_not_partly_unique(ModuleInfo, BoundFunctors)
else if Uniq = mostly_unique then
bound_functor_list_is_not_fully_unique(ModuleInfo, BoundFunctors)
else
true
).
%---------------------%
% Here we check that the functors in the first list are a subset of the
% functors in the second list. (If a bound(...) inst only specifies the
% insts for some of the constructors of its type, then it implicitly means
% that all other constructors must have all their arguments `not_reached'.)
% The code here makes use of the fact that the bound_functor lists
% are sorted.
%
:- pred bound_functor_list_matches_initial_mt(calculate_sub, mer_type,
list(bound_functor), list(bound_functor),
inst_match_info, inst_match_info).
:- mode bound_functor_list_matches_initial_mt(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode bound_functor_list_matches_initial_mt(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
bound_functor_list_matches_initial_mt(_, _, [], _, !Info).
bound_functor_list_matches_initial_mt(CalcSub, Type,
[BoundFunctorX | BoundFunctorXs], [BoundFunctorY | BoundFunctorYs],
!Info) :-
BoundFunctorX = bound_functor(ConsIdX, ArgInstsX),
BoundFunctorY = bound_functor(ConsIdY, ArgInstsY),
( if equivalent_cons_ids(ConsIdX, ConsIdY) then
get_cons_id_arg_types_for_bound_functor(!.Info ^ imi_module_info, Type,
BoundFunctorX, Types),
inst_list_matches_initial_mt(CalcSub, Types, ArgInstsX, ArgInstsY,
!Info),
bound_functor_list_matches_initial_mt(CalcSub, Type,
BoundFunctorXs, BoundFunctorYs, !Info)
else
first_unqual_cons_id_is_greater(ConsIdX, ConsIdY),
% ConsIdY does not occur in [BoundFunctorX | BoundFunctorXs].
% Hence [BoundFunctorX | BoundFunctorXs] implicitly specifies
% `not_reached' for the args of ConsIdY, and hence automatically
% matches_initial Y.
% We just need to check that [BoundFunctorX | BoundFunctorXs]
% matches_initial BoundFunctorsYs.
bound_functor_list_matches_initial_mt(CalcSub, Type,
[BoundFunctorX | BoundFunctorXs], BoundFunctorYs, !Info)
).
:- pred inst_list_matches_initial_mt(calculate_sub, list(mer_type),
list(mer_inst), list(mer_inst), inst_match_info, inst_match_info).
:- mode inst_list_matches_initial_mt(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_list_matches_initial_mt(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_list_matches_initial_mt(_, [], [], [], !Info).
inst_list_matches_initial_mt(CalcSub, [Type | Types],
[InstX | InstXs], [InstY | InstYs], !Info) :-
inst_matches_initial_mt(CalcSub, Type, InstX, InstY, !Info),
inst_list_matches_initial_mt(CalcSub, Types, InstXs, InstYs, !Info).
%---------------------------------------------------------------------------%
inst_matches_final(ModuleInfo, Type, InstA, InstB) :-
Info0 = init_inst_match_info(ModuleInfo, no_state,
uc_match, any_does_match_any, ground_matches_bound_if_complete),
inst_matches_final_mt(cs_none, Type, InstA, InstB, Info0, _).
inst_matches_final_gmb(ModuleInfo, GroundMatchesBound, Type, InstA, InstB) :-
Info0 = init_inst_match_info(ModuleInfo, no_state,
uc_match, any_does_match_any, GroundMatchesBound),
inst_matches_final_mt(cs_none, Type, InstA, InstB, Info0, _).
%---------------------%
:- pred inst_matches_final_mt(calculate_sub, mer_type, mer_inst, mer_inst,
inst_match_info, inst_match_info).
:- mode inst_matches_final_mt(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_matches_final_mt(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_matches_final_mt(CalcSub, Type, InstA, InstB, !Info) :-
( if InstA = InstB then
true
else
ThisExpansion = inst_match_inputs(InstA, InstB, Type),
Expansions0 = !.Info ^ imi_expansions,
( if expansion_insert_new(ThisExpansion, Expansions0, Expansions) then
!Info ^ imi_expansions := Expansions,
inst_expand(!.Info ^ imi_module_info, InstA, ExpandedInstA),
inst_expand(!.Info ^ imi_module_info, InstB, ExpandedInstB),
maybe_handle_inst_var_subs(CalcSub, Type,
ExpandedInstA, ExpandedInstB, InstVarSubResult, !Info),
require_complete_switch [InstVarSubResult]
(
InstVarSubResult = ivsr_recurse(RecurseInstA, RecurseInstB),
inst_matches_final_mt(cs_forward, Type,
RecurseInstA, RecurseInstB, !Info)
;
InstVarSubResult = ivsr_continue(ContCalcSub,
ContinueInstA, ContinueInstB),
inst_matches_final_mt_2(ContCalcSub, Type,
ContinueInstA, ContinueInstB, !Info)
)
else
true
)
).
:- pred inst_matches_final_mt_2(calculate_sub, mer_type,
mer_inst, mer_inst, inst_match_info, inst_match_info).
:- mode inst_matches_final_mt_2(in, in,
in(mer_inst_expanded), in(mer_inst_expanded),
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_matches_final_mt_2(in, in,
in(mer_inst_expanded), in(mer_inst_expanded),
in(imi_ivs), out(imi_ivs)) is semidet.
inst_matches_final_mt_2(CalcSub, Type, InstA, InstB, !Info) :-
% NOTE Both InstA and InstB may be constrained_inst_vars/2.
require_complete_switch [InstA]
(
InstA = free,
require_complete_switch [InstB]
(
InstB = free
;
InstB = any(Uniq, _),
% We do not yet allow `free' to match `any',
% unless the `any' is `clobbered_any' or `mostly_clobbered_any'.
% Among other things, changing this would break compare_inst
% in modecheck_call.m.
( Uniq = clobbered ; Uniq = mostly_clobbered )
;
( InstB = ground(_, _)
; InstB = bound(_, _, _)
; InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
; InstB = not_reached
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = ground(UniqA, HOInstInfoA),
require_complete_switch [InstB]
(
InstB = ground(UniqB, HOInstInfoB),
ho_inst_info_matches_final(CalcSub, Type,
HOInstInfoA, HOInstInfoB, !Info),
unique_matches_final(UniqA, UniqB)
;
InstB = bound(UniqB, InstResultsB, BoundFunctorsB),
ho_inst_info_matches_ground_1(CalcSub, Type, HOInstInfoA, !Info),
unique_matches_final(UniqA, UniqB),
ModuleInfo = !.Info ^ imi_module_info,
inst_results_bound_functor_list_is_ground_mt(ModuleInfo, Type,
InstResultsB, BoundFunctorsB),
uniq_matches_bound_functor_list(ModuleInfo, UniqA, BoundFunctorsB),
inst_contains_nondefault_func_mode_1(CalcSub, Type, InstB, no,
!Info),
(
% This check can succeed only if the type is known.
set.init(CompletenessExpansions0),
bound_functor_list_is_complete_for_type(ModuleInfo, Type,
CompletenessExpansions0, BoundFunctorsB)
;
% XXX the check for bound_functor_list_is_complete_for_type
% makes the mode checker too conservative in the absence
% of alias tracking. Bypass the check if instructed.
GroundMatchesBound = !.Info ^ imi_ground_matches_bound,
GroundMatchesBound = ground_matches_bound_always
)
;
InstB = any(UniqB, HOInstInfoB),
ho_inst_info_matches_final(CalcSub, Type,
HOInstInfoA, HOInstInfoB, !Info),
unique_matches_final(UniqA, UniqB)
;
( InstB = free
; InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
; InstB = not_reached
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = bound(UniqA, InstResultsA, BoundFunctorsA),
require_complete_switch [InstB]
(
InstB = ground(UniqB, none_or_default_func),
unique_matches_final(UniqA, UniqB),
inst_results_bound_functor_list_is_ground_mt(
!.Info ^ imi_module_info, Type, InstResultsA, BoundFunctorsA),
bound_functor_list_matches_uniq(!.Info ^ imi_module_info, UniqB,
BoundFunctorsA),
inst_contains_nondefault_func_mode_1(CalcSub, Type, InstA, no,
!Info)
;
InstB = bound(UniqB, _InstResultsB, BoundFunctorsB),
unique_matches_final(UniqA, UniqB),
bound_functor_list_matches_final(CalcSub, Type,
BoundFunctorsA, BoundFunctorsB, !Info)
;
InstB = any(UniqB, none_or_default_func),
unique_matches_final(UniqA, UniqB),
bound_functor_list_matches_uniq(!.Info ^ imi_module_info, UniqB,
BoundFunctorsA),
% We do not yet allow `free' to match `any'.
% Among other things, changing this would break compare_inst
% in modecheck_call.m.
inst_results_bound_functor_list_is_ground_or_any(
!.Info ^ imi_module_info, InstResultsA, BoundFunctorsA),
inst_contains_nondefault_func_mode_1(CalcSub, Type, InstA, no,
!Info)
;
( InstB = free
; InstB = not_reached
; InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = any(UniqA, HOInstInfoA),
require_complete_switch [InstB]
(
InstB = ground(_, _),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqA,
HOInstInfoA, NextInstA),
inst_matches_final_mt(CalcSub, Type, NextInstA, InstB, !Info)
;
InstB = bound(_, _, _),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqA,
HOInstInfoA, NextInstA),
inst_matches_final_mt(CalcSub, Type, NextInstA, InstB, !Info)
;
InstB = any(UniqB, HOInstInfoB),
ho_inst_info_matches_final(CalcSub, Type,
HOInstInfoA, HOInstInfoB, !Info),
unique_matches_final(UniqA, UniqB)
;
( InstB = free
; InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
; InstB = not_reached
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = constrained_inst_vars(InstVarsA, SubInstA),
( if InstB = constrained_inst_vars(InstVarsB, SubInstB) then
% Constrained_inst_vars match_final only if InstVarsA contains
% all the variables in InstVarsB.
set.subset(InstVarsB, InstVarsA),
inst_matches_final_mt(CalcSub, Type, SubInstA, SubInstB, !Info)
else
inst_matches_final_mt(CalcSub, Type, SubInstA, InstB, !Info)
)
;
InstA = not_reached
;
InstA = inst_var(_),
% XXX This case used to be simply missing, so I (zs) have no idea
% whether failing here is the right thing to do; I only know that
% that is what this code has always done implicitly. This code here
% only makes the failure explicit.
fail
).
%---------------------%
:- pred ho_inst_info_matches_final(calculate_sub, mer_type,
ho_inst_info, ho_inst_info, inst_match_info, inst_match_info).
:- mode ho_inst_info_matches_final(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode ho_inst_info_matches_final(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
ho_inst_info_matches_final(CalcSub, Type, HOInstInfoA, HOInstInfoB, !Info) :-
(
HOInstInfoB = none_or_default_func,
ho_inst_info_matches_ground_1(CalcSub, Type, HOInstInfoA, !Info)
;
HOInstInfoB = higher_order(PredInstB),
(
HOInstInfoA = none_or_default_func,
PredInstB = pred_inst_info(pf_function, ArgModes, _, _Det),
list.length(ArgModes, Arity),
PredInstA = pred_inst_info_default_func_mode(Arity),
pred_inst_matches_1(CalcSub, Type, PredInstA, PredInstB, !Info)
;
HOInstInfoA = higher_order(PredInstA),
pred_inst_matches_1(CalcSub, Type, PredInstA, PredInstB, !Info)
)
).
%---------------------%
% Here we check that the functors in the first list are a subset of the
% functors in the second list. (If a bound(...) inst only specifies
% the insts for some of the constructors of its type, then it implicitly
% means that all other constructors must have all their arguments
% `not_reached'.) The code here makes use of the fact that the
% bound_functor
% lists are sorted.
%
:- pred bound_functor_list_matches_final(calculate_sub, mer_type,
list(bound_functor), list(bound_functor),
inst_match_info, inst_match_info).
:- mode bound_functor_list_matches_final(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode bound_functor_list_matches_final(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
bound_functor_list_matches_final(_, _, [], _, !Info).
bound_functor_list_matches_final(CalcSub, Type,
[BoundFunctorX | BoundFunctorXs], [BoundFunctorY | BoundFunctorYs],
!Info) :-
BoundFunctorX = bound_functor(ConsIdX, ArgInstsX),
BoundFunctorY = bound_functor(ConsIdY, ArgInstsY),
( if equivalent_cons_ids(ConsIdX, ConsIdY) then
get_cons_id_arg_types_for_bound_functor(!.Info ^ imi_module_info, Type,
BoundFunctorX, ArgTypes),
inst_list_matches_final(CalcSub, ArgTypes,
ArgInstsX, ArgInstsY, !Info),
bound_functor_list_matches_final(CalcSub, Type,
BoundFunctorXs, BoundFunctorYs, !Info)
else
first_unqual_cons_id_is_greater(ConsIdX, ConsIdY),
% ConsIdY does not occur in [X | Xs].
% Hence [X | Xs] implicitly specifies `not_reached' for the args
% of ConsIdY, and hence automatically matches_final Y. We just
% need to check that [X | Xs] matches_final Ys.
bound_functor_list_matches_final(CalcSub, Type,
[BoundFunctorX | BoundFunctorXs], BoundFunctorYs, !Info)
).
:- pred inst_list_matches_final(calculate_sub, list(mer_type),
list(mer_inst), list(mer_inst), inst_match_info, inst_match_info).
:- mode inst_list_matches_final(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_list_matches_final(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_list_matches_final(_, [], [], [], !Info).
inst_list_matches_final(CalcSub, [ArgType | ArgTypes],
[ArgInstA | ArgInstsA], [ArgInstB | ArgInstsB], !Info) :-
inst_matches_final_mt(CalcSub, ArgType, ArgInstA, ArgInstB, !Info),
inst_list_matches_final(CalcSub, ArgTypes, ArgInstsA, ArgInstsB, !Info).
%---------------------------------------------------------------------------%
inst_matches_binding(ModuleInfo, Type, InstA, InstB) :-
Info0 = init_inst_match_info(ModuleInfo, no_state,
uc_match, any_does_not_match_any, ground_matches_bound_if_complete),
inst_matches_binding_mt(cs_none, Type, InstA, InstB, Info0, _).
inst_matches_binding_allow_any_any(ModuleInfo, Type, InstA, InstB) :-
Info0 = init_inst_match_info(ModuleInfo, no_state,
uc_match, any_does_match_any, ground_matches_bound_if_complete),
inst_matches_binding_mt(cs_none, Type, InstA, InstB, Info0, _).
%---------------------%
:- pred inst_matches_binding_mt(calculate_sub, mer_type,
mer_inst, mer_inst, inst_match_info, inst_match_info).
:- mode inst_matches_binding_mt(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_matches_binding_mt(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_matches_binding_mt(CalcSub, Type, InstA, InstB, !Info) :-
ThisExpansion = inst_match_inputs(InstA, InstB, Type),
Expansions0 = !.Info ^ imi_expansions,
( if expansion_insert_new(ThisExpansion, Expansions0, Expansions) then
!Info ^ imi_expansions := Expansions,
inst_expand_and_remove_constrained_inst_vars(!.Info ^ imi_module_info,
InstA, ExpandedInstA),
inst_expand_and_remove_constrained_inst_vars(!.Info ^ imi_module_info,
InstB, ExpandedInstB),
inst_matches_binding_2(CalcSub, Type,
ExpandedInstA, ExpandedInstB, !Info)
else
true
).
:- pred inst_matches_binding_2(calculate_sub, mer_type, mer_inst, mer_inst,
inst_match_info, inst_match_info).
:- mode inst_matches_binding_2(in, in,
in(mer_inst_expanded), in(mer_inst_expanded),
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_matches_binding_2(in, in,
in(mer_inst_expanded), in(mer_inst_expanded),
in(imi_ivs), out(imi_ivs)) is semidet.
inst_matches_binding_2(CalcSub, Type, InstA, InstB, !Info) :-
require_complete_switch [InstA]
(
InstA = free,
InstB = free
;
InstA = ground(_UniqA, HOInstInfoA),
require_complete_switch [InstB]
(
InstB = ground(_UniqB, HOInstInfoB),
ho_inst_info_matches_binding(!.Info ^ imi_module_info,
Type, HOInstInfoA, HOInstInfoB)
;
InstB = bound(_UniqB, InstResultsB, BoundFunctorsB),
inst_results_bound_functor_list_is_ground_mt(
!.Info ^ imi_module_info, Type, InstResultsB, BoundFunctorsB),
inst_contains_nondefault_func_mode_1(CalcSub, Type, InstB, no,
!Info),
set.init(CompletenessExpansions0),
bound_functor_list_is_complete_for_type(!.Info ^ imi_module_info,
Type, CompletenessExpansions0, BoundFunctorsB)
;
InstB = any(UniqB, HOInstInfoB),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqB,
HOInstInfoB, NextInstB),
inst_matches_binding_mt(CalcSub, Type, InstA, NextInstB, !Info)
;
( InstB = free
; InstB = not_reached
; InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = bound(_UniqA, InstResultsA, BoundFunctorsA),
require_complete_switch [InstB]
(
InstB = any(UniqB, HOInstInfoB),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqB,
HOInstInfoB, NextInstB),
inst_matches_binding_mt(CalcSub, Type, InstA, NextInstB, !Info)
;
InstB = bound(_UniqB, _InstResultB, BoundFunctorsB),
bound_functor_list_matches_binding(CalcSub, Type,
BoundFunctorsA, BoundFunctorsB, !Info)
;
InstB = ground(_UniqB, none_or_default_func),
inst_results_bound_functor_list_is_ground_mt(
!.Info ^ imi_module_info, Type, InstResultsA, BoundFunctorsA),
inst_contains_nondefault_func_mode_1(CalcSub, Type, InstA, no,
!Info)
;
( InstB = free
; InstB = not_reached
; InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = any(UniqA, HOInstInfoA),
(
InstB = ground(_, _),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqA,
HOInstInfoA, NextInstA),
inst_matches_binding_mt(CalcSub, Type, NextInstA, InstB, !Info)
;
InstB = bound(_, _, _),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqA,
HOInstInfoA, NextInstA),
inst_matches_binding_mt(CalcSub, Type, NextInstA, InstB, !Info)
;
InstB = any(UniqB, HOInstInfoB),
% Note that `any' is *not* considered to match `any' unless
% Info ^ any_matches_any = yes or the type is not a solver type
% (and does not contain any solver types).
AnyMatchesAny = !.Info ^ imi_any_matches_any,
(
AnyMatchesAny = any_does_match_any,
ho_inst_info_matches_final(CalcSub, Type,
HOInstInfoA, HOInstInfoB, !Info)
;
AnyMatchesAny = any_does_not_match_any,
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqA,
HOInstInfoA, NextInstA),
maybe_any_to_bound(!.Info ^ imi_module_info, Type, UniqB,
HOInstInfoB, NextInstB),
inst_matches_binding_mt(CalcSub, Type,
NextInstA, NextInstB, !Info)
)
;
( InstB = free
; InstB = not_reached
; InstB = constrained_inst_vars(_, _)
; InstB = inst_var(_)
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
)
;
InstA = not_reached
;
( InstA = constrained_inst_vars(_, _)
; InstA = inst_var(_)
),
% XXX The failures in these cases used to be implicit.
% For some of these cases, failure may be the wrong thing to do.
fail
).
%---------------------%
:- pred ho_inst_info_matches_binding(module_info::in, mer_type::in,
ho_inst_info::in, ho_inst_info::in) is semidet.
ho_inst_info_matches_binding(ModuleInfo, Type, HOInstInfoA, HOInstInfoB) :-
(
HOInstInfoB = none_or_default_func,
ho_inst_info_matches_ground(ModuleInfo, Type, HOInstInfoA)
;
HOInstInfoB = higher_order(PredInstB),
(
HOInstInfoA = none_or_default_func,
PredInstB = pred_inst_info(pf_function, ArgModes, _, _Det),
Arity = list.length(ArgModes),
PredInstA = pred_inst_info_default_func_mode(Arity)
;
HOInstInfoA = higher_order(PredInstA)
),
pred_inst_matches(ModuleInfo, Type, PredInstA, PredInstB)
).
%---------------------%
% Here we check that the functors in the first list are a subset of the
% functors in the second list. (If a bound(...) inst only specifies
% the insts for some of the constructors of its type, then it implicitly
% means that all other constructors must have all their arguments
% `not_reached'.) The code here makes use of the fact that the
% bound_functor
% lists are sorted.
%
:- pred bound_functor_list_matches_binding(calculate_sub, mer_type,
list(bound_functor), list(bound_functor),
inst_match_info, inst_match_info).
:- mode bound_functor_list_matches_binding(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode bound_functor_list_matches_binding(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
bound_functor_list_matches_binding(_, _, [], _, !Info).
bound_functor_list_matches_binding(CalcSub, Type,
[BoundFunctorX | BoundFunctorXs], [BoundFunctorY | BoundFunctorYs],
!Info) :-
BoundFunctorX = bound_functor(ConsIdX, ArgInstsX),
BoundFunctorY = bound_functor(ConsIdY, ArgInstsY),
( if equivalent_cons_ids(ConsIdX, ConsIdY) then
get_cons_id_arg_types_for_bound_functor(!.Info ^ imi_module_info, Type,
BoundFunctorX, ArgTypes),
inst_list_matches_binding(CalcSub, ArgTypes,
ArgInstsX, ArgInstsY, !Info),
bound_functor_list_matches_binding(CalcSub, Type,
BoundFunctorXs, BoundFunctorYs, !Info)
else
first_unqual_cons_id_is_greater(ConsIdX, ConsIdY),
% ConsIdX does not occur in [X | Xs].
% Hence [X | Xs] implicitly specifies `not_reached' for the args
% of ConsIdY, and hence automatically matches_binding Y. We just
% need to check that [X | Xs] matches_binding Ys.
bound_functor_list_matches_binding(CalcSub, Type,
[BoundFunctorX | BoundFunctorXs], BoundFunctorYs, !Info)
).
:- pred inst_list_matches_binding(calculate_sub, list(mer_type),
list(mer_inst), list(mer_inst), inst_match_info, inst_match_info).
:- mode inst_list_matches_binding(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_list_matches_binding(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_list_matches_binding(_, [], [], [], !Info).
inst_list_matches_binding(CalcSub, [ArgType | ArgTypes],
[ArgInstA | ArgInstsA], [ArgInstB | ArgInstsB], !Info) :-
inst_matches_binding_mt(CalcSub, ArgType, ArgInstA, ArgInstB, !Info),
inst_list_matches_binding(CalcSub, ArgTypes, ArgInstsA, ArgInstsB, !Info).
%---------------------------------------------------------------------------%
inst_contains_nondefault_func_mode(ModuleInfo, Type, Inst) :-
Info = init_inst_match_info(ModuleInfo, no_state, uc_match,
any_does_match_any, ground_matches_bound_if_complete),
inst_contains_nondefault_func_mode_1(cs_none, Type, Inst, yes, Info, _).
:- pred inst_contains_nondefault_func_mode_1(calculate_sub, mer_type,
mer_inst, bool, inst_match_info, inst_match_info).
:- mode inst_contains_nondefault_func_mode_1(in, in, in, out,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_contains_nondefault_func_mode_1(in, in, in, out,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_contains_nondefault_func_mode_1(CalcSub, Type, Inst,
ContainsNonstd, !Info) :-
inst_contains_nondefault_func_mode_2(CalcSub, Type, Inst, set.init,
ContainsNonstd, !Info).
%---------------------%
:- pred inst_contains_nondefault_func_mode_2(calculate_sub, mer_type,
mer_inst, set(inst_name), bool, inst_match_info, inst_match_info).
:- mode inst_contains_nondefault_func_mode_2(in, in, in, in, out,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_contains_nondefault_func_mode_2(in, in, in, in, out,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_contains_nondefault_func_mode_2(CalcSub, Type, Inst, !.Expansions,
ContainsNonstd, !Info) :-
(
( Inst = free
; Inst = not_reached
),
ContainsNonstd = no
;
Inst = ground(_, HOInstInfo),
( if
ho_inst_info_matches_ground_1(CalcSub, Type, HOInstInfo, !Info)
then
ContainsNonstd = no
else
ContainsNonstd = yes
)
;
Inst = bound(_, InstResults, BoundFunctors),
(
InstResults = inst_test_results_fgtc,
ContainsNonstd = no
;
( InstResults = inst_test_results(_, _, _, _, _, _)
; InstResults = inst_test_no_results
),
bound_functor_list_contains_nondefault_func_mode(CalcSub, Type,
BoundFunctors, !.Expansions, ContainsNonstd, !Info)
)
;
Inst = any(_, _),
% XXX This code preserves the old behavior of the predicate that
% preceded this function, but it is arguably incorrect, since
% any/2 insts, like ground/2 insts, contain a ho_inst_info.
ContainsNonstd = no
;
Inst = constrained_inst_vars(_, SubInst),
inst_contains_nondefault_func_mode_2(CalcSub, Type, SubInst,
!.Expansions, ContainsNonstd, !Info)
;
Inst = inst_var(_),
unexpected($pred, "uninstantiated inst parameter")
;
Inst = defined_inst(InstName),
( if set.insert_new(InstName, !Expansions) then
inst_lookup(!.Info ^ imi_module_info, InstName, SubInst),
inst_contains_nondefault_func_mode_2(CalcSub, Type, SubInst,
!.Expansions, ContainsNonstd, !Info)
else
ContainsNonstd = no
)
).
%---------------------%
:- pred bound_functor_list_contains_nondefault_func_mode(calculate_sub,
mer_type, list(bound_functor), set(inst_name), bool,
inst_match_info, inst_match_info).
:- mode bound_functor_list_contains_nondefault_func_mode(in, in, in, in, out,
in(imi_ns), out(imi_ns)) is semidet.
:- mode bound_functor_list_contains_nondefault_func_mode(in, in, in, in, out,
in(imi_ivs), out(imi_ivs)) is semidet.
bound_functor_list_contains_nondefault_func_mode(_, _, [], _Expansions,
no, !Info).
bound_functor_list_contains_nondefault_func_mode(CalcSub, Type,
[BoundFunctor | BoundFunctors], Expansions, ContainsNonstd, !Info) :-
BoundFunctor = bound_functor(_ConsId, ArgInsts),
get_cons_id_arg_types_for_bound_functor(!.Info ^ imi_module_info, Type,
BoundFunctor, ArgTypes),
inst_list_contains_nondefault_func_mode(CalcSub, ArgTypes, ArgInsts,
Expansions, HeadContainsNonstd, !Info),
(
HeadContainsNonstd = yes,
ContainsNonstd = yes
;
HeadContainsNonstd = no,
bound_functor_list_contains_nondefault_func_mode(CalcSub, Type,
BoundFunctors, Expansions, ContainsNonstd, !Info)
).
:- pred inst_list_contains_nondefault_func_mode(calculate_sub,
list(mer_type), list(mer_inst), set(inst_name), bool,
inst_match_info, inst_match_info).
:- mode inst_list_contains_nondefault_func_mode(in, in, in, in, out,
in(imi_ns), out(imi_ns)) is semidet.
:- mode inst_list_contains_nondefault_func_mode(in, in, in, in, out,
in(imi_ivs), out(imi_ivs)) is semidet.
inst_list_contains_nondefault_func_mode(_, [], [], _Expansions, no, !Info).
inst_list_contains_nondefault_func_mode(_, [], [_ | _], _, _, !Info) :-
unexpected($pred, "list length mismatch").
inst_list_contains_nondefault_func_mode(_, [_ | _], [], _, _, !Info) :-
unexpected($pred, "list length mismatch").
inst_list_contains_nondefault_func_mode(CalcSub,
[Type | Types], [Inst | Insts], Expansions, ContainsNonstd, !Info) :-
inst_contains_nondefault_func_mode_2(CalcSub, Type, Inst,
Expansions, HeadContainsNonstd, !Info),
(
HeadContainsNonstd = yes,
ContainsNonstd = yes
;
HeadContainsNonstd = no,
inst_list_contains_nondefault_func_mode(CalcSub, Types, Insts,
Expansions, ContainsNonstd, !Info)
).
%---------------------------------------------------------------------------%
ho_inst_info_matches_ground(ModuleInfo, Type, HOInstInfo) :-
Info = init_inst_match_info(ModuleInfo, no_state, uc_match,
any_does_match_any, ground_matches_bound_if_complete),
ho_inst_info_matches_ground_1(cs_none, Type, HOInstInfo, Info, _).
:- pred ho_inst_info_matches_ground_1(calculate_sub, mer_type, ho_inst_info,
inst_match_info, inst_match_info).
:- mode ho_inst_info_matches_ground_1(in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode ho_inst_info_matches_ground_1(in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
ho_inst_info_matches_ground_1(CalcSub, Type, HOInstInfo, !Info) :-
(
HOInstInfo = higher_order(PredInst),
pred_inst_matches_ground_1(CalcSub, Type, PredInst, !Info)
;
HOInstInfo = none_or_default_func
).
%---------------------%
pred_inst_matches_ground(ModuleInfo, Type, PredInst) :-
Info = init_inst_match_info(ModuleInfo, no_state, uc_match,
any_does_match_any, ground_matches_bound_if_complete),
pred_inst_matches_ground_1(cs_none, Type, PredInst, Info, _).
:- pred pred_inst_matches_ground_1(calculate_sub, mer_type, pred_inst_info,
inst_match_info, inst_match_info).
:- mode pred_inst_matches_ground_1(in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode pred_inst_matches_ground_1(in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
pred_inst_matches_ground_1(CalcSub, Type, PredInst, !Info) :-
% NOTE CalcSub is set to cs_none by pred_inst_matches_ground above,
% but NOT by ho_inst_info_matches_ground_1.
PredInst = pred_inst_info(PredOrFunc, ArgModes, _, _),
(
PredOrFunc = pf_predicate
;
PredOrFunc = pf_function,
Arity = list.length(ArgModes),
DefaultFunc = pred_inst_info_default_func_mode(Arity),
pred_inst_matches_1(CalcSub, Type, PredInst, DefaultFunc, !Info)
).
%---------------------%
pred_inst_matches(ModuleInfo, Type, PredInstA, PredInstB) :-
Info0 = init_inst_match_info(ModuleInfo, no_state,
uc_match, any_does_match_any, ground_matches_bound_if_complete),
pred_inst_matches_1(cs_none, Type, PredInstA, PredInstB, Info0, _).
% pred_inst_matches_1(Type, PredInstA, PredInstB, !Info)
%
% Same as pred_inst_matches/4, except that it updates the inst_var_sub
% in the inst_match_info, and that any inst pairs in !.Info ^ expansions
% are assumed to match_final each other. (This avoids infinite loops
% when calling inst_matches_final on higher-order recursive insts.)
%
:- pred pred_inst_matches_1(calculate_sub, mer_type,
pred_inst_info, pred_inst_info, inst_match_info, inst_match_info).
:- mode pred_inst_matches_1(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode pred_inst_matches_1(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
pred_inst_matches_1(CalcSub, Type, PredInstA, PredInstB, !Info) :-
% In the float_regs.m pass a variable may take on pred insts which differ
% only in the arg reg lists in different branches. They should be allowed
% to match here.
%
% NOTE CalcSub is set to cs_none by pred_inst_matches above,
% but NOT by ho_inst_info_matches_{initial,final}.
PredInstA = pred_inst_info(PredOrFunc, ModesA, _MaybeArgRegsA, Det),
PredInstB = pred_inst_info(PredOrFunc, ModesB, _MaybeArgRegsB, Det),
get_higher_order_arg_types(Type, list.length(ModesA), Types),
pred_inst_argmodes_matches(CalcSub, Types, ModesA, ModesB, !Info).
% pred_inst_argmodes_matches(Types, ModesA, ModesB, !Info):
%
% Succeeds if the initial insts of ModesB specify at least as much
% information as, and the same binding as, the initial insts of ModesA;
% and the final insts of ModesA specify at least as much information as,
% and the same binding as, the final insts of ModesB. Any inst pairs
% in Inst0 ^ expansions are assumed to match_final each other.
%
% (In other words, as far as subtyping goes it is contravariant in
% the initial insts, and covariant in the final insts;
% as far as binding goes, it is invariant for both.)
%
:- pred pred_inst_argmodes_matches(calculate_sub, list(mer_type),
list(mer_mode), list(mer_mode), inst_match_info, inst_match_info).
:- mode pred_inst_argmodes_matches(in, in, in, in,
in(imi_ns), out(imi_ns)) is semidet.
:- mode pred_inst_argmodes_matches(in, in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
pred_inst_argmodes_matches(_, [], [], [], !Info).
pred_inst_argmodes_matches(CalcSub, [Type | Types],
[ModeA | ModeAs], [ModeB | ModeBs], !Info) :-
ModuleInfo = !.Info ^ imi_module_info,
mode_get_insts(ModuleInfo, ModeA, InitialA, FinalA0),
mode_get_insts(ModuleInfo, ModeB, InitialB, FinalB),
InitialCalcSub = swap_calculate_sub(CalcSub),
inst_matches_final_mt(InitialCalcSub, Type, InitialB, InitialA, !Info),
% Apply the substitution computed so far (it may be necessary for InitialA
% as well).
maybe_apply_substitution(!.Info, FinalA0, FinalA),
inst_matches_final_mt(CalcSub, Type, FinalA, FinalB, !Info),
pred_inst_argmodes_matches(CalcSub, Types, ModeAs, ModeBs, !Info).
:- pred maybe_apply_substitution(inst_match_info, mer_inst, mer_inst).
:- mode maybe_apply_substitution(in(imi_ns), in, out) is det.
:- mode maybe_apply_substitution(in(imi_ivs), in, out) is det.
maybe_apply_substitution(Info, Inst0, Inst) :-
(
Info ^ imi_maybe_state = no_state,
Inst = Inst0
;
Info ^ imi_maybe_state = inst_var_sub_state(Subst),
inst_apply_substitution(Subst, Inst0, Inst)
).
%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%
:- type inst_match_inputs
---> inst_match_inputs(
mer_inst,
mer_inst,
mer_type
).
:- type expansions == set_tree234(inst_match_inputs).
:- func expansion_init = expansions.
:- pragma inline(func(expansion_init/0)).
expansion_init = set_tree234.init.
:- pred expansion_insert_new(inst_match_inputs::in,
expansions::in, expansions::out) is semidet.
:- pragma inline(pred(expansion_insert_new/3)).
expansion_insert_new(E, S0, S) :-
set_tree234.insert_new(E, S0, S).
%---------------------------------------------------------------------------%
:- type inst_match_info
---> inst_match_info(
imi_module_info :: module_info,
imi_expansions :: expansions,
imi_maybe_state :: maybe_inst_match_state,
imi_uniqueness_comparison :: uniqueness_comparison,
imi_any_matches_any :: any_matches_any,
imi_ground_matches_bound :: ground_matches_bound
).
:- inst imi_ns for inst_match_info/0
---> inst_match_info(ground, ground, no_state,
ground, ground, ground).
:- inst imi_ivs for inst_match_info/0
---> inst_match_info(ground, ground, inst_var_sub_state,
ground, ground, ground).
% The uniqueness_comparison type is used by the predicate
% compare_uniqueness to determine what order should be used for
% comparing two uniqueness annotations.
:- type uniqueness_comparison
---> uc_match
% We are doing a "matches" comparison, e.g. at a predicate call
% or the end of a procedure body.
; uc_instantiated.
% We are comparing two insts for how "instantiated" they are.
% The uniqueness order here should be the reverse of the order
% used for matching.
:- type maybe_inst_match_state
---> no_state
; inst_var_sub_state(inst_var_sub).
% The inst_var_sub records what inst should be substituted for each
% inst_var that occurs in the called procedure's argument modes.
:- inst no_state for maybe_inst_match_state/0
---> no_state.
:- inst inst_var_sub_state for maybe_inst_match_state/0
---> inst_var_sub_state(ground).
% The calculate_sub type determines how the inst var substitution
% should be calculated.
:- type calculate_sub
---> cs_forward
% Calculate in the (normal) forward direction
% (used by inst_matches_initial).
; cs_reverse
% Calculate in the reverse direction. Used by the call
% to inst_matches_final from pred_inst_argmodes_match
% to ensure contravariance of the initial argument
% insts of higher order pred insts.
; cs_none.
% Do not calculate inst var substitution.
:- type calculate_sub_dir =< calculate_sub
---> cs_forward
; cs_reverse.
:- type any_matches_any
---> any_does_not_match_any
; any_does_match_any.
:- func init_inst_match_info(module_info, maybe_inst_match_state,
uniqueness_comparison, any_matches_any, ground_matches_bound) =
inst_match_info.
:- mode init_inst_match_info(in, in(no_state), in, in, in) =
out(imi_ns) is det.
:- mode init_inst_match_info(in, in(inst_var_sub_state), in, in, in) =
out(imi_ivs) is det.
init_inst_match_info(ModuleInfo, MaybeState, UniqCmp,
AnyMatchesAny, GroundMatchesBound) =
inst_match_info(ModuleInfo, expansion_init, MaybeState, UniqCmp,
AnyMatchesAny, GroundMatchesBound).
%---------------------------------------------------------------------------%
:- func swap_calculate_sub(calculate_sub) = calculate_sub.
swap_calculate_sub(cs_forward) = cs_reverse.
swap_calculate_sub(cs_reverse) = cs_forward.
swap_calculate_sub(cs_none) = cs_none.
%---------------------------------------------------------------------------%
:- type inst_var_subs_result
---> ivsr_recurse(mer_inst, mer_inst) % CalcSub = cs_forward.
; ivsr_continue(calculate_sub, mer_inst, mer_inst).
:- inst inst_var_subs_result for inst_var_subs_result/0
---> ivsr_recurse(ground, ground)
; ivsr_continue(ground, mer_inst_expanded, mer_inst_expanded).
% We construct ivsr_continue in two places: one place each in
% maybe_handle_inst_var_subs and do_handle_inst_var_subs.
% The latter guarantees that the two mer_insts will both be
% mer_inst_expanded_nc, but the former only guarantees
% mer_inst_expanded, and that only because that is the inst
% of its input.
%
% Since both callers of maybe_handle_inst_var_subs have to be
% prepared to handle constrained_inst_vars insts being returned
% in ivsr_continue, we can guarantee only the looser inst.
:- pred maybe_handle_inst_var_subs(calculate_sub, mer_type,
mer_inst, mer_inst, inst_var_subs_result,
inst_match_info, inst_match_info).
:- mode maybe_handle_inst_var_subs(in, in,
in(mer_inst_expanded), in(mer_inst_expanded), out(inst_var_subs_result),
in(imi_ns), out(imi_ns)) is semidet.
:- mode maybe_handle_inst_var_subs(in, in,
in(mer_inst_expanded), in(mer_inst_expanded), out(inst_var_subs_result),
in(imi_ivs), out(imi_ivs)) is semidet.
maybe_handle_inst_var_subs(CalcSub, Type, InstA, InstB, Result, !Info) :-
(
CalcSub = cs_forward,
CalcSubDir = coerce(CalcSub),
do_handle_inst_var_subs(CalcSubDir, Type, InstA, InstB, Result, !Info)
;
CalcSub = cs_reverse,
CalcSubDir = coerce(CalcSub),
do_handle_inst_var_subs(CalcSubDir, Type, InstB, InstA, Result, !Info)
;
CalcSub = cs_none,
Result = ivsr_continue(cs_none, InstA, InstB)
).
:- pred do_handle_inst_var_subs(calculate_sub_dir, mer_type,
mer_inst, mer_inst, inst_var_subs_result,
inst_match_info, inst_match_info).
:- mode do_handle_inst_var_subs(in, in,
in(mer_inst_expanded), in(mer_inst_expanded), out(inst_var_subs_result),
in(imi_ns), out(imi_ns)) is semidet.
:- mode do_handle_inst_var_subs(in, in,
in(mer_inst_expanded), in(mer_inst_expanded), out(inst_var_subs_result),
in(imi_ivs), out(imi_ivs)) is semidet.
do_handle_inst_var_subs(CalcSubDir, Type, InstA, InstB, Result, !Info) :-
require_complete_switch [InstB]
(
InstB = constrained_inst_vars(InstVarsB, SubInstB),
% Add the substitution InstVarsB => InstA `glb` SubInstB
% (see get_subst_inst in dmo's thesis, page 78).
%
% We pass `Live = is_dead' because we want
% abstractly_unify(unique, unique) = unique, not shared.
ModuleInfo0 = !.Info ^ imi_module_info,
abstractly_unify_inst(Type, is_dead, fake_unify, InstA, SubInstB,
UnifyInst, _Det, ModuleInfo0, ModuleInfo),
!Info ^ imi_module_info := ModuleInfo,
update_inst_var_sub(InstVarsB, UnifyInst, Type, !Info),
% Check that InstA matches InstB after applying the substitution
% to InstB.
( if UnifyInst = constrained_inst_vars(InstVarsB, UnifySubInst) then
% Avoid infinite regress.
swap_insts_back(CalcSubDir, InstA, UnifySubInst, Inst1, Inst2)
else
swap_insts_back(CalcSubDir, InstA, UnifyInst, Inst1, Inst2)
),
Result = ivsr_recurse(Inst1, Inst2)
;
( InstB = free
; InstB = ground(_, _)
; InstB = any(_, _)
; InstB = bound(_, _, _)
; InstB = not_reached
; InstB = inst_var(_)
),
require_complete_switch [InstA]
(
InstA = constrained_inst_vars(_InstVarsA, SubInstA),
% XXX The code for InstB being constrained_inst_vars unifies
% SubInstB with InstA, and records the resulting UnifyInst against
% InstVarsB. However, if it is InstA that is bound to
% constrained_inst_vars/2, then here we *throw away* this wrapper;
% we do not unify SubInstA with InstB, and therefore we cannot
% record its results against _InstVarsA. This strikes me (zs)
% as strange.
%
% NOTE: our *caller* *may* end up unifying SubInstA with InstB,
% but it has no access to _InstVarsA, since we throw it away here.
%
% In a post to m-rev on 2024 Jul 5, wangp replied to the above
% comment with:
%
% All I can tell you is that code follows the get_subst_inst
% function in David Overton's thesis (page 78, figure 4.2).
% The InstA = constrained_inst_vars(_, _) branch is the
% second case of get_subst_inst, which ignores Ω.
swap_insts_back(CalcSubDir, SubInstA, InstB, Inst1, Inst2),
Result = ivsr_recurse(Inst1, Inst2)
;
( InstA = free
; InstA = ground(_, _)
; InstA = any(_, _)
; InstA = bound(_, _, _)
; InstA = not_reached
; InstA = inst_var(_)
),
swap_insts_back(CalcSubDir, InstA, InstB, Inst1, Inst2),
Result = ivsr_continue(cs_forward, Inst1, Inst2)
)
).
:- pred swap_insts_back(calculate_sub_dir, mer_inst, mer_inst,
mer_inst, mer_inst).
% This mode is not yet needed, but it should be needed later
% to express the inst of the ivsr_continue term constructed above.
% Note that this will kind of ivsr_continue will have to be separated
% from the ivsr_continue constructed by maybe_handle_inst_var_subs.
% :- mode swap_insts_back(in,
% in(mer_inst_expanded_nc), in(mer_inst_expanded_nc),
% out(mer_inst_expanded_nc), out(mer_inst_expanded_nc)) is det.
:- mode swap_insts_back(in, in(mer_inst_expanded), in(mer_inst_expanded),
out(mer_inst_expanded), out(mer_inst_expanded)) is det.
:- mode swap_insts_back(in, in, in, out, out) is det.
swap_insts_back(CalcSubDir, InstA, InstB, Inst1, Inst2) :-
(
CalcSubDir = cs_forward,
% handle_inst_var_subs did not swap InstA and InstB; no swap-back.
Inst1 = InstA,
Inst2 = InstB
;
CalcSubDir = cs_reverse,
% handle_inst_var_subs *did* swap InstA and InstB; swap them back.
Inst1 = InstB,
Inst2 = InstA
).
%---------------------------------------------------------------------------%
% Update the inst_var_sub that is computed by inst_matches_initial.
%
:- pred update_inst_var_sub(set(inst_var), mer_inst, mer_type,
inst_match_info, inst_match_info).
:- mode update_inst_var_sub(in, in, in, in(imi_ns), out(imi_ns)) is det.
:- mode update_inst_var_sub(in, in, in, in(imi_ivs), out(imi_ivs)) is semidet.
:- pragma inline(pred(update_inst_var_sub/5)).
update_inst_var_sub(InstVars, InstA, Type, !Info) :-
(
!.Info ^ imi_maybe_state = no_state
;
!.Info ^ imi_maybe_state = inst_var_sub_state(_),
update_inst_var_sub_vars(InstA, Type,
set.to_sorted_list(InstVars), !Info)
).
:- pred update_inst_var_sub_vars(mer_inst, mer_type, list(inst_var),
inst_match_info, inst_match_info).
:- mode update_inst_var_sub_vars(in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
update_inst_var_sub_vars(_, _, [], !Info).
update_inst_var_sub_vars(InstA, Type, [InstVar | InstVars], !Info) :-
update_inst_var_sub_2(InstA, Type, InstVar, !Info),
update_inst_var_sub_vars(InstA, Type, InstVars, !Info).
:- pred update_inst_var_sub_2(mer_inst, mer_type, inst_var,
inst_match_info, inst_match_info).
:- mode update_inst_var_sub_2(in, in, in,
in(imi_ivs), out(imi_ivs)) is semidet.
update_inst_var_sub_2(InstA, Type, InstVar, !Info) :-
!.Info ^ imi_maybe_state = inst_var_sub_state(InstVarSub0),
( if map.search(InstVarSub0, InstVar, InstB) then
% If InstVar already has an inst associated with it, merge
% the old and new insts. Fail if this merge is not possible.
ModuleInfo0 = !.Info ^ imi_module_info,
inst_merge(Type, InstA, InstB, InstAB, ModuleInfo0, ModuleInfo),
!Info ^ imi_module_info := ModuleInfo,
map.det_update(InstVar, InstAB, InstVarSub0, InstVarSub),
!Info ^ imi_maybe_state := inst_var_sub_state(InstVarSub)
else
map.det_insert(InstVar, InstA, InstVarSub0, InstVarSub),
!Info ^ imi_maybe_state := inst_var_sub_state(InstVarSub)
).
%---------------------------------------------------------------------------%
% A list(bound_functor) is complete for a given type iff
%
% - it includes each functor of that type, and
% - each argument of each functor is also complete for its type.
%
:- pred bound_functor_list_is_complete_for_type(module_info::in,
mer_type::in, set(inst_name)::in, list(bound_functor)::in) is semidet.
bound_functor_list_is_complete_for_type(ModuleInfo, Type, Expansions,
BoundFunctors) :-
type_to_ctor_and_args(Type, TypeCtor, TypeCtorArgTypes),
module_info_get_type_table(ModuleInfo, TypeTable),
search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
hlds_data.get_type_defn_body(TypeDefn, TypeDefnBody),
TypeDefnBody = hlds_du_type(TypeBodyDu),
get_type_defn_tparams(TypeDefn, TypeParams),
% TypeSubst replaces the type parameter variables in TypeCtorArgTypes
% with the cotrresponding actual types from Type.
map.from_corresponding_lists(TypeParams, TypeCtorArgTypes, TypeSubst),
TypeBodyDu = type_body_du(_, SortedOoMCtors, _, _, _, _),
SortedCtors = one_or_more_to_list(SortedOoMCtors),
bound_functor_list_is_complete_for_type_loop(ModuleInfo, TypeSubst,
Expansions, BoundFunctors, SortedCtors).
% Both the list of bound_functors and the list of constructors must be
% sorted first on the names and then on the arities of the cons_ids.
%
% Apply TypeSubst to each constructor's arguments only when processing
% that constructor. This way, we don't expend any resources
% on applying TypeSubst to a constructor if the call to
% bound_functor_list_is_complete_for_type_loop fails before it gets
% to that constructor.
%
% Likewise, even when we process a given constructor, we apply
% TypeSubst to each argument only when we know that the checking
% of all the previous arguments of that constructor has been successful.
%
:- pred bound_functor_list_is_complete_for_type_loop(module_info::in,
map(type_param, mer_type)::in, set(inst_name)::in,
list(bound_functor)::in, list(constructor)::in) is semidet.
bound_functor_list_is_complete_for_type_loop(_, _, _, [], []).
bound_functor_list_is_complete_for_type_loop(ModuleInfo, TypeSubst, Expansions,
[BoundFunctor | BoundFunctors], [Ctor | Ctors]) :-
BoundFunctor = bound_functor(InstConsId, ArgInsts),
InstConsId = du_data_ctor(InstDuCtor),
InstDuCtor = du_ctor(InstSymName, InstArity, _InstTypeCtor),
Ctor = ctor(_, MaybeExist, CtorSymName, CtorArgs, CtorArity, _),
unqualify_name(CtorSymName) = unqualify_name(InstSymName),
CtorArity = InstArity,
list.map(inst_is_complete_for_arg_type(ModuleInfo, TypeSubst, Expansions),
CtorArgs, ArgInsts),
MaybeExist = no_exist_constraints,
bound_functor_list_is_complete_for_type_loop(ModuleInfo, TypeSubst,
Expansions, BoundFunctors, Ctors).
:- pred inst_is_complete_for_arg_type(module_info::in,
map(type_param, mer_type)::in, set(inst_name)::in,
constructor_arg::in, mer_inst::in) is semidet.
inst_is_complete_for_arg_type(ModuleInfo, TypeSubst, Expansions,
CtorArg, Inst) :-
apply_subst_to_type(TypeSubst, CtorArg ^ arg_type, ExpandedArgType),
inst_is_complete_for_type(ModuleInfo, Expansions, ExpandedArgType, Inst).
:- pred inst_is_complete_for_type(module_info::in, set(inst_name)::in,
mer_type::in, mer_inst::in) is semidet.
inst_is_complete_for_type(ModuleInfo, Expansions, Type, Inst) :-
require_complete_switch [Inst]
(
Inst = defined_inst(Name),
( if set.member(Name, Expansions) then
true
else
inst_lookup(ModuleInfo, Name, ExpandedInst),
inst_is_complete_for_type(ModuleInfo, set.insert(Expansions, Name),
Type, ExpandedInst)
)
;
Inst = bound(_, _, BoundFunctors),
bound_functor_list_is_complete_for_type(ModuleInfo, Type,
Expansions, BoundFunctors)
;
% XXX This switch was originally an if-then-else chain, with explicit
% tests for defined_inst and bound, and the final else case being
% simply "Inst \= not_reached". However, several of the Inst values
% for which this succeeds look extremely dodgy. For example, I (zs)
% am pretty much certain that constrained_inst_vars should recurse
% on its sub-inst instead of succeeding.
%
% On the other hand, it is possible that some or all of the Inst values
% for which we do the wrong thing here will never be given to us
% by our callers.
( Inst = free
; Inst = any(_, _)
; Inst = ground(_, _)
; Inst = inst_var(_)
; Inst = constrained_inst_vars(_, _)
)
;
Inst = not_reached,
fail
).
%---------------------------------------------------------------------------%
% Check that the first cons_id is lexically greater than the second,
% after all module qualifiers have been removed.
%
:- pred first_unqual_cons_id_is_greater(cons_id::in, cons_id::in) is semidet.
first_unqual_cons_id_is_greater(ConsIdA, ConsIdB) :-
( if
ConsIdA = du_data_ctor(du_ctor(QNameA, ArityA, _)),
ConsIdB = du_data_ctor(du_ctor(QNameB, ArityB, _))
then
( QNameA = unqualified(NameA)
; QNameA = qualified(_, NameA)
),
( QNameB = unqualified(NameB)
; QNameB = qualified(_, NameB)
),
compare(O, NameA, NameB),
(
O = (>)
;
O = (=),
ArityA > ArityB
)
else
compare((>), ConsIdA, ConsIdB)
).
%---------------------------------------------------------------------------%
% Determine what kind of uniqueness comparison we are doing and then do it.
% If we are doing a "match" then call unique_matches_initial to do the
% comparison. If we are comparing "instantiatedness" then the uniqueness
% comparison is the reverse of when we are doing a match so call
% unique_matches_initial with the arguments reversed.
%
:- pred compare_uniqueness(uniqueness_comparison::in,
uniqueness::in, uniqueness::in) is semidet.
compare_uniqueness(uc_match, InstA, InstB) :-
unique_matches_initial(InstA, InstB).
compare_uniqueness(uc_instantiated, InstA, InstB) :-
unique_matches_initial(InstB, InstA).
unique_matches_initial(unique, _).
unique_matches_initial(mostly_unique, mostly_unique).
unique_matches_initial(mostly_unique, shared).
unique_matches_initial(mostly_unique, mostly_clobbered).
unique_matches_initial(mostly_unique, clobbered).
unique_matches_initial(shared, shared).
unique_matches_initial(shared, mostly_clobbered).
unique_matches_initial(shared, clobbered).
unique_matches_initial(mostly_clobbered, mostly_clobbered).
unique_matches_initial(mostly_clobbered, clobbered).
unique_matches_initial(clobbered, clobbered).
unique_matches_final(A, B) :-
unique_matches_initial(A, B).
%---------------------------------------------------------------------------%
:- pred same_addr_insts(mer_inst::in, mer_inst::in) is semidet.
:- pragma foreign_proc("C",
same_addr_insts(InstA::in, InstB::in),
[will_not_call_mercury, promise_pure, thread_safe],
"
SUCCESS_INDICATOR = ((void *) InstA == (void *) InstB);
").
same_addr_insts(_, _) :-
semidet_fail.
%---------------------------------------------------------------------------%
:- end_module check_hlds.inst_match.
%---------------------------------------------------------------------------%
Reference in New Issue View Git Blame Copy Permalink