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
master
mercury/compiler/resolve_unify_functor.m
Zoltan Somogyi ee9c7d3a84 Speed up bound vs ground inst checks. 
The code that checks whether a bound inst wrapped around
a list of bound_functors matched the ground inst did several things
in a suboptimal fashion.

- It looked up the definition of the type constructor of the relevant type
  (the type of the variable the inst is for) more than once. (This was
  not easily visible because the lookups were in different predicates.)
  This diff factors these out, not for the immesurably small speedup,
  but to make possible the fixes for the next two issues.

- To simplify the "is there a bound_functor for each constructor in the type"
  check, it sorted the constructors of the type by name and arity. (Lists of
  bound_functors are always sorted by name and arity.) Given that most
  modules contain more than one bound inst for any given type constructor,
  any sorting after the first was unnecessarily repeated work. This diff
  therefore extends the representation of du types, which until now has
  include only a list of the data constructors in the type definition
  in definition order, with a list of those exact same data constructors
  in name/arity order.

- Even if a list of bound_functors lists all the constructors of a type,
  the bound inst containing them is not equivalent to ground if the inst
  of some argument of some bound_inst is not equivalent to ground.
  This means that we need to know the actual argument of each constructor.
  The du type definition lists argument types that refer to the type
  constructor's type parameters; we need the instances of these argument types
  that apply to type of the variable at hand, which usually binds concrete
  types to those type parameters.

  We used to apply the type-parameter-to-actual-type substitution to
  each argument of each data constructor in the type before we compared
  the resulting filled-in data constructor descriptions against the list of
  bound_functors. However, in cases where the comparison fails, the
  substitution applications to arguments beyond the point of failure
  are all wasted work. This diff therefore applies the substitution
  only when its result is about to be needed.

This diff leads to a speedup of about 3.5% on tools/speedtest,
and about 38% (yes, more than a third) when compiling options.m.

compiler/hlds_data.m:
    Add the new field to the representation of du types.

    Add a utility predicate that helps construct that field, since it is
    now needed by two modules (add_type.m and equiv_type_hlds.m).

    Delete two functions that were used only by det_check_switch.m,
    which this diff moves to that module (in modified form).

compiler/inst_match.m:
    Implement the first and third changes listed above, and take advantage
    of the second.

    The old call to all_du_ctor_arg_types, which this diff replaces,
    effectively lied about the list of constructors it returned,
    by simply not returning any constructors containing existentially
    quantified  types, on the grounds that they "were not handled yet".
    We now fail explicitly when we find any such constructors.

    Perform the check for one-to-one match between bound_functors and
    constructors with less argument passing.

compiler/det_check_switch.m:
    Move the code deleted from hlds_data.m here, and simplify it,
    taking advantage of the new field in du types.

compiler/Mercury.options:
    Specify --optimize-constructor-last-call for det_check_switch.m
    to optimize the updated moved code.

compiler/add_foreign_enum.m:
compiler/add_special_pred.m:
compiler/add_type.m:
compiler/check_typeclass.m:
compiler/code_info.m:
compiler/dead_proc_elim.m:
compiler/direct_arg_in_out.m:
compiler/du_type_layout.m:
compiler/equiv_type_hlds.m:
compiler/hlds_out_type_table.m:
compiler/inst_check.m:
compiler/intermod.m:
compiler/intermod_decide.m:
compiler/lookup_switch_util.m:
compiler/ml_type_gen.m:
compiler/ml_unify_gen_test.m:
compiler/ml_unify_gen_util.m:
compiler/mlds.m:
compiler/post_term_analysis.m:
compiler/recompilation.usage.m:
compiler/resolve_unify_functor.m:
compiler/simplify_goal_ite.m:
compiler/table_gen.m:
compiler/tag_switch_util.m:
compiler/term_norm.m:
compiler/type_ctor_info.m:
compiler/type_util.m:
compiler/typecheck_coerce.m:
compiler/unify_proc.m:
compiler/unused_imports.m:
compiler/xml_documentation.m:
    Conform to the changes above. This mostly means handling
    the new field in du types (usually by ignoring it).
2025-11-19 22:09:04 +11:00

755 lines
32 KiB
Mathematica
Raw Permalink Blame History

%---------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 2015-2025 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.
%---------------------------------------------------------------------------%
%
% This module does two tasks that are logically part of type analysis
% but must be done after type inference is complete:
%
% - it resolves function overloading; and
% - it expands field access functions.
%
% Most other similar tasks are done in post_typecheck.m or purity.m.
%
%---------------------------------------------------------------------------%
:- module check_hlds.resolve_unify_functor.
:- interface.
:- import_module hlds.
:- import_module hlds.hlds_goal.
:- import_module hlds.hlds_module.
:- import_module hlds.hlds_pred.
:- import_module parse_tree.
:- import_module parse_tree.error_spec.
:- import_module parse_tree.prog_data.
:- import_module parse_tree.var_table.
:- import_module list.
%---------------------------------------------------------------------------%
:- type is_plain_unify
---> is_not_plain_unify
; is_plain_unify
; is_unknown_ref(error_spec).
% Work out whether a var-functor unification is actually a function call.
% If so, replace the unification goal with a call.
%
:- pred resolve_unify_functor(module_info::in, prog_var::in, cons_id::in,
list(prog_var)::in, unify_mode::in, unification::in, unify_context::in,
hlds_goal_info::in, hlds_goal::out, is_plain_unify::out,
list(error_spec)::out,
var_table::in, var_table::out, pred_info::in, pred_info::out) is det.
%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%
:- implementation.
:- import_module hlds.hlds_class.
:- import_module hlds.hlds_cons.
:- import_module hlds.hlds_data.
:- import_module hlds.make_goal.
:- import_module hlds.pred_table.
:- import_module hlds.type_util.
:- import_module mdbcomp.
:- import_module mdbcomp.goal_path.
:- import_module mdbcomp.prim_data.
:- import_module mdbcomp.sym_name.
:- import_module parse_tree.prog_type.
:- import_module parse_tree.prog_type_scan.
:- import_module parse_tree.prog_type_subst.
:- import_module parse_tree.prog_type_test.
:- import_module parse_tree.prog_type_unify.
:- import_module parse_tree.prog_util.
:- import_module parse_tree.set_of_var.
:- import_module int.
:- import_module map.
:- import_module maybe.
:- import_module one_or_more.
:- import_module require.
:- import_module term_io.
:- import_module varset.
%---------------------------------------------------------------------------%
resolve_unify_functor(ModuleInfo, X0, ConsId0, ArgVars0, Mode0,
Unification0, UnifyContext, GoalInfo0, Goal, IsPlainUnify, Specs,
!VarTable, !PredInfo) :-
( if ConsId0 = du_data_ctor(DuCtor0) then
lookup_var_type(!.VarTable, X0, TypeOfX),
list.length(ArgVars0, Arity),
DuCtor0 = du_ctor(SymName0, Arity0, _TypeCtor),
( if
% Is the function symbol apply/N or ''/N, representing
% a higher-order function call? Or the impure/semipure equivalents
% impure_apply/N and semipure_apply/N?
% (XXX FIXME We should use nicer syntax for impure apply/N.)
SymName0 = unqualified(ApplyName),
(
ApplyName = "",
Purity = purity_pure,
Syntax = hos_var
;
ApplyName = "apply",
Purity = purity_pure,
Syntax = hos_call_or_apply
;
ApplyName = "impure_apply",
Purity = purity_impure,
Syntax = hos_call_or_apply
;
ApplyName = "semipure_apply",
Purity = purity_semipure,
Syntax = hos_call_or_apply
),
Arity >= 1,
ArgVars0 = [FuncVar | FuncArgVars]
then
% Convert the higher-order function call (apply/N) into
% a higher-order predicate call.
% This means replacing e.g. `X = apply(F, A, B, C)'
% with `call(F, A, B, C, X)'.
ArgVars = FuncArgVars ++ [X0],
Modes = [],
Detism = detism_erroneous,
user_arity_pred_form_arity(pf_function,
user_arity(Arity), PredFormArity),
GenericCall = higher_order(FuncVar, Purity, pf_function,
PredFormArity, Syntax),
HOCall = generic_call(GenericCall, ArgVars, Modes,
arg_reg_types_unset, Detism),
Goal = hlds_goal(HOCall, GoalInfo0),
IsPlainUnify = is_not_plain_unify,
Specs = []
else if
% Is the function symbol a user-defined function, rather than
% a functor which represents a data constructor?
% Find the set of candidate predicates which have the
% specified name and arity (and module, if module-qualified)
pred_info_get_markers(!.PredInfo, Markers),
IsFullyQualified = calls_are_fully_qualified(Markers),
module_info_get_predicate_table(ModuleInfo, PredTable),
UserArity = user_arity(Arity),
% This search will usually fail, so do it first.
predicate_table_lookup_func_sym_arity(PredTable, IsFullyQualified,
SymName0, UserArity, PredIds),
PredIds = [_ | _],
% We don't do this for compiler-generated predicates;
% they are assumed to have been generated with all functions
% already expanded. If we did this check for compiler-generated
% predicates, it would cause the wrong behaviour in the case
% where there is a user-defined function whose type is
% exactly the same as the type of a constructor.
% (Normally that would cause a type ambiguity error, but
% compiler-generated predicates are not type-checked.)
not is_unify_index_or_compare_pred(!.PredInfo),
% We don't do this for the clause introduced by the compiler for
% a field access function -- that needs to be expanded into
% unifications below.
not pred_info_is_field_access_function(ModuleInfo, !.PredInfo,
_, _, _),
% Check if any of the candidate functions have argument/return
% types which subsume the actual argument/return types of this
% function call, and which have universal constraints
% consistent with what we expect.
pred_info_get_typevarset(!.PredInfo, TVarSet),
pred_info_get_exist_quant_tvars(!.PredInfo, ExistQTVars),
pred_info_get_external_type_params(!.PredInfo, ExternalTypeParams),
lookup_var_types(!.VarTable, ArgVars0, ArgTypes0),
ArgTypes = ArgTypes0 ++ [TypeOfX],
pred_info_get_constraint_map(!.PredInfo, ConstraintMap),
GoalId = goal_info_get_goal_id(GoalInfo0),
ConstraintSearch =
search_hlds_constraint_list(ConstraintMap, unproven, GoalId),
Context = goal_info_get_context(GoalInfo0),
find_matching_pred_id(ModuleInfo, pf_function, SymName0, PredIds,
TVarSet, ExistQTVars, ArgTypes, ExternalTypeParams,
yes(ConstraintSearch), Context, PredId, QualifiedFuncName,
SpecsPrime)
then
% Convert function calls in unifications into plain calls:
% replace `X = f(A, B, C)' with `f(A, B, C, X)'.
ProcId = invalid_proc_id,
ArgVars = ArgVars0 ++ [X0],
FuncCallUnifyContext = call_unify_context(X0,
rhs_functor(ConsId0, is_not_exist_constr, ArgVars0),
UnifyContext),
FuncCall = plain_call(PredId, ProcId, ArgVars, not_builtin,
yes(FuncCallUnifyContext), QualifiedFuncName),
Goal = hlds_goal(FuncCall, GoalInfo0),
IsPlainUnify = is_not_plain_unify,
Specs = SpecsPrime
else if
% Is the function symbol a higher-order predicate or function
% constant?
type_is_higher_order_details(TypeOfX, _Purity, PredOrFunc,
HOArgTypes),
% We don't do this for the clause introduced by the compiler
% for a field access function -- that needs to be expanded
% into unifications below.
not pred_info_is_field_access_function(ModuleInfo, !.PredInfo,
_, _, _),
% Find the pred_id of the constant.
lookup_var_types(!.VarTable, ArgVars0, ArgTypes0),
AllArgTypes = ArgTypes0 ++ HOArgTypes,
pred_info_get_typevarset(!.PredInfo, TVarSet),
pred_info_get_exist_quant_tvars(!.PredInfo, ExistQVars),
pred_info_get_external_type_params(!.PredInfo, ExternalTypeParams),
pred_info_get_markers(!.PredInfo, Markers),
Context = goal_info_get_context(GoalInfo0),
get_pred_id_by_types(calls_are_fully_qualified(Markers), SymName0,
PredOrFunc, TVarSet, ExistQVars, AllArgTypes,
ExternalTypeParams, ModuleInfo, Context, PredId, SpecsPrime)
then
module_info_pred_info(ModuleInfo, PredId, PredInfo),
ProcIds = pred_info_all_procids(PredInfo),
(
ProcIds = [ProcId0],
MaybeProcId = yes(ProcId0)
;
ProcIds = [_, _ | _],
% We don't know which mode to pick. Defer it
% until mode checking.
MaybeProcId = yes(invalid_proc_id)
;
ProcIds = [],
MaybeProcId = no
),
(
MaybeProcId = yes(ProcId),
ShroudedPredProcId = shroud_pred_proc_id(proc(PredId, ProcId)),
ConsId = closure_cons(ShroudedPredProcId),
GoalExpr = unify(X0,
rhs_functor(ConsId, is_not_exist_constr, ArgVars0),
Mode0, Unification0, UnifyContext),
Goal = hlds_goal(GoalExpr, GoalInfo0),
IsPlainUnify = is_not_plain_unify
;
MaybeProcId = no,
Goal = true_goal,
SNA = sym_name_arity(SymName0, Arity),
Pieces = [words("Error: the predicate or function")] ++
color_as_subject([qual_sym_name_arity(SNA)]) ++
color_as_incorrect([words("is undefined.")]) ++
[nl],
Spec = spec($pred, severity_error, phase_type_check,
Context, Pieces),
IsPlainUnify = is_unknown_ref(Spec)
),
Specs = SpecsPrime
else if
% Is it a call to an automatically generated field access function.
% This test must come after the tests for function calls and
% higher-order terms above. We do it that way because it is easier
% to check that the types match for functions calls and
% higher-order terms.
is_field_access_function_name(ModuleInfo, SymName0, Arity,
AccessType, FieldName, _OoMFieldDefns),
Arity = Arity0,
% We don't do this for compiler-generated predicates --
% they will never contain calls to field access functions.
not is_unify_index_or_compare_pred(!.PredInfo),
% If there is a constructor for which the argument types match,
% this unification couldn't be a call to a field access function,
% otherwise there would have been an error reported for unresolved
% overloading.
pred_info_get_typevarset(!.PredInfo, TVarSet),
lookup_var_types(!.VarTable, ArgVars0, ArgTypes0),
not find_matching_constructor(ModuleInfo, TVarSet, DuCtor0,
TypeOfX, ArgTypes0)
then
finish_field_access_function(ModuleInfo, AccessType, FieldName,
UnifyContext, X0, ArgVars0, GoalInfo0, Goal,
!VarTable, !PredInfo),
IsPlainUnify = is_not_plain_unify,
Specs = []
else
% Module qualify ordinary construction/deconstruction unifications.
( if Arity = Arity0 then
( if TypeOfX = tuple_type(_, _) then
ConsId = tuple_cons(Arity)
else if TypeOfX = builtin_type(builtin_type_char) then
(
SymName0 = unqualified(Name0),
( if encode_escaped_char(Char, Name0) then
ConsId = char_const(Char)
else
unexpected($pred, "encode_escaped_char")
)
;
SymName0 = qualified(_, _),
unexpected($pred, "qualified char const")
)
else
Name = unqualify_name(SymName0),
type_to_ctor_det(TypeOfX, TypeCtorOfX),
TypeCtorOfX = type_ctor(TypeCtorSymName, _),
(
TypeCtorSymName = qualified(TypeCtorModule, _),
SymName = qualified(TypeCtorModule, Name),
DuCtor =
du_ctor(SymName, Arity, TypeCtorOfX),
ConsId = du_data_ctor(DuCtor)
;
TypeCtorSymName = unqualified(_),
unexpected($pred, "unqualified type_ctor")
)
)
else
ConsId = ConsId0
),
resolve_unify_functor_std(X0, ConsId, ArgVars0, Mode0,
Unification0, UnifyContext, GoalInfo0, Goal, IsPlainUnify,
Specs)
)
else
resolve_unify_functor_std(X0, ConsId0, ArgVars0, Mode0,
Unification0, UnifyContext, GoalInfo0, Goal, IsPlainUnify, Specs)
).
:- pred resolve_unify_functor_std(prog_var::in, cons_id::in,
list(prog_var)::in, unify_mode::in, unification::in, unify_context::in,
hlds_goal_info::in, hlds_goal::out, is_plain_unify::out,
list(error_spec)::out) is det.
resolve_unify_functor_std(X0, ConsId, ArgVars0, Mode0,
Unification0, UnifyContext, GoalInfo0, Goal, IsPlainUnify, Specs) :-
RHS = rhs_functor(ConsId, is_not_exist_constr, ArgVars0),
GoalExpr = unify(X0, RHS, Mode0, Unification0, UnifyContext),
Goal = hlds_goal(GoalExpr, GoalInfo0),
IsPlainUnify = is_plain_unify,
Specs = [].
%---------------------------------------------------------------------------%
% Succeed if there is a constructor which matches the given cons_id,
% type and argument types.
%
:- pred find_matching_constructor(module_info::in, tvarset::in,
du_ctor::in, mer_type::in, list(mer_type)::in) is semidet.
find_matching_constructor(ModuleInfo, TVarSet, DuCtor, Type, ArgTypes) :-
type_to_ctor(Type, TypeCtor),
module_info_get_cons_table(ModuleInfo, ConsTable),
search_cons_table_of_type_ctor(ConsTable, TypeCtor, DuCtor, ConsDefn),
% Overloading resolution ignores the class constraints.
ConsDefn = hlds_cons_defn(_, _, _, _, MaybeExistConstraints, ConsArgs, _),
module_info_get_type_table(ModuleInfo, TypeTable),
search_type_ctor_defn(TypeTable, TypeCtor, TypeDefn),
hlds_data.get_type_defn_tvarset(TypeDefn, TypeTVarSet),
hlds_data.get_type_defn_kind_map(TypeDefn, TypeKindMap),
(
MaybeExistConstraints = no_exist_constraints,
ConsExistQVars = []
;
MaybeExistConstraints = exist_constraints(
cons_exist_constraints(ConsExistQVars, _, _, _))
),
ConsArgTypes = list.map(func(C) = C ^ arg_type, ConsArgs),
% XXX is this correct?
ExistQVars = [],
ExternalTypeParams = [],
arg_type_list_subsumes(TVarSet, ExistQVars, ArgTypes, ExternalTypeParams,
TypeTVarSet, TypeKindMap, ConsExistQVars, ConsArgTypes).
%---------------------------------------------------------------------------%
% Convert a field access function call into the equivalent unifications
% so that later passes do not have to handle them as a special case.
% The error messages from mode analysis and determinism analysis
% shouldn't be too much worse than if the goals were special cases.
%
:- pred finish_field_access_function(module_info::in, field_access_type::in,
sym_name::in, unify_context::in, prog_var::in, list(prog_var)::in,
hlds_goal_info::in, hlds_goal::out,
var_table::in, var_table::out, pred_info::in, pred_info::out) is det.
finish_field_access_function(ModuleInfo, AccessType, FieldName, UnifyContext,
Var, Args, GoalInfo, Goal, !VarTable, !PredInfo) :-
(
AccessType = get,
field_extraction_function_args(Args, TermVar),
translate_get_function(ModuleInfo, FieldName, UnifyContext,
Var, TermVar, GoalInfo, GoalExpr, !VarTable, !PredInfo)
;
AccessType = set,
field_update_function_args(Args, TermInputVar, FieldVar),
translate_set_function(ModuleInfo, FieldName, UnifyContext,
FieldVar, TermInputVar, Var, GoalInfo, GoalExpr,
!VarTable, !PredInfo)
),
Goal = hlds_goal(GoalExpr, GoalInfo).
:- pred translate_get_function(module_info::in, sym_name::in,
unify_context::in, prog_var::in, prog_var::in,
hlds_goal_info::in, hlds_goal_expr::out,
var_table::in, var_table::out, pred_info::in, pred_info::out) is det.
translate_get_function(ModuleInfo, FieldName, UnifyContext,
FieldVar, TermInputVar, OldGoalInfo, GoalExpr, !VarTable, !PredInfo) :-
lookup_var_type(!.VarTable, TermInputVar, TermType),
get_constructor_containing_field(ModuleInfo, TermType, FieldName,
DuCtor, FieldNumber),
GoalId = goal_info_get_goal_id(OldGoalInfo),
get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, GoalId, DuCtor,
TermType, ArgTypes0, ExistQVars, !PredInfo),
% If the type of the field we are extracting contains existentially
% quantified type variables then we need to rename any other occurrences
% of those type variables in the arguments of the constructor so that
% they match those in the type of the field. (We don't need to do this
% for field updates because if any existentially quantified type variables
% occur in field to set and other fields then the field update
% should have been disallowed by typecheck.m because the result
% can't be well-typed).
(
ExistQVars = [_ | _],
lookup_var_type(!.VarTable, FieldVar, FieldType),
list.det_index1(ArgTypes0, FieldNumber, FieldArgType),
type_subsumes_det(FieldArgType, FieldType, FieldSubst),
apply_rec_subst_to_types(FieldSubst, ArgTypes0, ArgTypes)
;
ExistQVars = [],
ArgTypes = ArgTypes0
),
split_list_at_index(FieldNumber, ArgTypes, TypesBeforeField,
_, TypesAfterField),
make_new_vars(ModuleInfo, TypesBeforeField, VarsBeforeField, !VarTable),
make_new_vars(ModuleInfo, TypesAfterField, VarsAfterField, !VarTable),
ArgVars = VarsBeforeField ++ [FieldVar | VarsAfterField],
RestrictNonLocals = goal_info_get_nonlocals(OldGoalInfo),
ConsId = du_data_ctor(DuCtor),
create_pure_atomic_unification_with_nonlocals(TermInputVar,
rhs_functor(ConsId, is_not_exist_constr, ArgVars),
OldGoalInfo, RestrictNonLocals, [FieldVar, TermInputVar],
UnifyContext, FunctorGoal),
FunctorGoal = hlds_goal(GoalExpr, _).
:- pred translate_set_function(module_info::in,
sym_name::in, unify_context::in, prog_var::in, prog_var::in, prog_var::in,
hlds_goal_info::in, hlds_goal_expr::out,
var_table::in, var_table::out, pred_info::in, pred_info::out) is det.
translate_set_function(ModuleInfo, FieldName, UnifyContext,
FieldVar, TermInputVar, TermOutputVar, OldGoalInfo, Goal,
!VarTable, !PredInfo) :-
lookup_var_type(!.VarTable, TermInputVar, TermType),
get_constructor_containing_field(ModuleInfo, TermType, FieldName,
DuCtor0, FieldNumber),
GoalId = goal_info_get_goal_id(OldGoalInfo),
get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, GoalId,
DuCtor0, TermType, ArgTypes, ExistQVars, !PredInfo),
split_list_at_index(FieldNumber, ArgTypes,
TypesBeforeField, TermFieldType, TypesAfterField),
make_new_vars(ModuleInfo, TypesBeforeField, VarsBeforeField, !VarTable),
make_new_var(ModuleInfo, TermFieldType, SingletonFieldVar, !VarTable),
make_new_vars(ModuleInfo, TypesAfterField, VarsAfterField, !VarTable),
% Build a goal to deconstruct the input.
DeconstructArgs = VarsBeforeField ++ [SingletonFieldVar | VarsAfterField],
OldNonLocals = goal_info_get_nonlocals(OldGoalInfo),
NonLocalArgs = VarsBeforeField ++ VarsAfterField,
set_of_var.insert_list(NonLocalArgs, OldNonLocals,
DeconstructRestrictNonLocals),
ConsId0 = du_data_ctor(DuCtor0),
create_pure_atomic_unification_with_nonlocals(TermInputVar,
rhs_functor(ConsId0, is_not_exist_constr, DeconstructArgs),
OldGoalInfo, DeconstructRestrictNonLocals,
[TermInputVar | DeconstructArgs], UnifyContext, DeconstructGoal),
% Build a goal to construct the output.
ConstructArgs = VarsBeforeField ++ [FieldVar | VarsAfterField],
set_of_var.insert_list(NonLocalArgs, OldNonLocals,
ConstructRestrictNonLocals),
% If the cons_id is existentially quantified, add a `new' prefix
% so that polymorphism.m adds the appropriate type_infos.
(
ExistQVars = [],
ConsId = ConsId0
;
ExistQVars = [_ | _],
DuCtor0 = du_ctor(ConsSymName0, ConsArity, TypeCtor),
add_new_prefix(ConsSymName0, ConsSymName),
DuCtor = du_ctor(ConsSymName, ConsArity, TypeCtor),
ConsId = du_data_ctor(DuCtor)
),
create_pure_atomic_unification_with_nonlocals(TermOutputVar,
rhs_functor(ConsId, is_not_exist_constr, ConstructArgs), OldGoalInfo,
ConstructRestrictNonLocals, [TermOutputVar | ConstructArgs],
UnifyContext, ConstructGoal),
ConjExpr = conj(plain_conj, [DeconstructGoal, ConstructGoal]),
Conj = hlds_goal(ConjExpr, OldGoalInfo),
% Make mode analysis treat the translated access function
% as an atomic goal.
Goal = scope(barrier(removable), Conj).
:- pred get_cons_id_arg_types_adding_existq_tvars(module_info::in,
goal_id::in, du_ctor::in, mer_type::in, list(mer_type)::out,
list(tvar)::out, pred_info::in, pred_info::out) is det.
get_cons_id_arg_types_adding_existq_tvars(ModuleInfo, GoalId, DuCtor,
TermType, ActualArgTypes, ActualExistQVars, !PredInfo) :-
% Split the list of argument types at the named field.
type_to_ctor_det(TermType, TypeCtor),
get_cons_defn_det(ModuleInfo, TypeCtor, DuCtor, ConsDefn),
ConsDefn = hlds_cons_defn(_, _, TypeParams, _, MaybeExistConstraints,
ConsArgs, _),
ConsArgTypes = list.map(func(C) = C ^ arg_type, ConsArgs),
(
MaybeExistConstraints = no_exist_constraints,
ActualArgTypes0 = ConsArgTypes,
ActualExistQVars = []
;
MaybeExistConstraints = exist_constraints(ExistConstraints),
ExistConstraints = cons_exist_constraints(ConsExistQVars,
ConsConstraints, _UnconstrainedExistQVars, _ConstrainedExistQVars),
% Rename apart the existentially quantified type variables.
list.length(ConsExistQVars, NumExistQVars),
pred_info_get_typevarset(!.PredInfo, TVarSet0),
varset.new_vars(NumExistQVars, ParentExistQVars, TVarSet0, TVarSet),
pred_info_set_typevarset(TVarSet, !PredInfo),
map.from_corresponding_lists(ConsExistQVars, ParentExistQVars,
ConsToParentRenaming),
apply_renaming_to_types(ConsToParentRenaming,
ConsArgTypes, ParentArgTypes),
apply_renaming_to_prog_constraints(ConsToParentRenaming,
ConsConstraints, ParentConstraints),
% Constrained existentially quantified tvars will have already been
% created during typechecking, so we need to ensure that the new ones
% we allocate here are bound to those created earlier, so that
% the varmaps remain meaningful.
pred_info_get_constraint_map(!.PredInfo, ConstraintMap),
list.length(ConsConstraints, NumConstraints),
lookup_hlds_constraint_list(ConstraintMap, assumed, GoalId,
NumConstraints, ActualConstraints),
constraint_list_subsumes_det(ParentConstraints, ActualConstraints,
ExistTSubst),
apply_rec_subst_to_types(ExistTSubst, ParentArgTypes,
ActualArgTypes0),
% The kinds will be ignored when the types are converted back to tvars.
map.init(KindMap),
apply_rec_subst_to_tvars(KindMap, ExistTSubst, ParentExistQVars,
ActualExistQVarTypes),
( if
type_list_to_var_list(ActualExistQVarTypes, ActualExistQVars0)
then
ActualExistQVars = ActualExistQVars0
else
unexpected($pred, "existq_tvar bound to non-var")
)
),
type_to_ctor_and_args_det(TermType, _, TypeArgs),
map.from_corresponding_lists(TypeParams, TypeArgs, UnivTSubst),
apply_subst_to_types(UnivTSubst, ActualArgTypes0, ActualArgTypes).
:- pred constraint_list_subsumes_det(list(prog_constraint)::in,
list(prog_constraint)::in, tsubst::out) is det.
constraint_list_subsumes_det(ConstraintsA, ConstraintsB, Subst) :-
constraint_list_get_tvars(ConstraintsB, TVarsB),
map.init(Subst0),
( if
unify_constraint_list(ConstraintsA, ConstraintsB, TVarsB,
Subst0, Subst1)
then
Subst = Subst1
else
unexpected($pred, "failed")
).
:- pred unify_constraint_list(list(prog_constraint)::in,
list(prog_constraint)::in, list(tvar)::in, tsubst::in, tsubst::out)
is semidet.
unify_constraint_list([], [], _, !Subst).
unify_constraint_list([A | As], [B | Bs], TVars, !Subst) :-
A = constraint(_ClassNameA, ArgTypesA),
B = constraint(_ClassNameB, ArgTypesB),
type_unify_list(ArgTypesA, ArgTypesB, TVars, !Subst),
unify_constraint_list(As, Bs, TVars, !Subst).
:- pred split_list_at_index(int::in, list(T)::in, list(T)::out, T::out,
list(T)::out) is det.
split_list_at_index(Index, List, Before, At, After) :-
( if
list.split_list(Index - 1, List, BeforePrime, AtAndAfter),
AtAndAfter = [AtPrime | AfterPrime]
then
Before = BeforePrime,
At = AtPrime,
After = AfterPrime
else
unexpected($pred, "split_list_at_index")
).
%---------------------------------------------------------------------------%
% Work out which constructor of the type has an argument with the
% given field name.
%
:- pred get_constructor_containing_field(module_info::in, mer_type::in,
sym_name::in, du_ctor::out, int::out) is det.
get_constructor_containing_field(ModuleInfo, TermType, FieldSymName,
DuCtor, FieldNumber) :-
type_to_ctor_det(TermType, TermTypeCtor),
module_info_get_type_table(ModuleInfo, TypeTable),
lookup_type_ctor_defn(TypeTable, TermTypeCtor, TermTypeDefn),
hlds_data.get_type_defn_body(TermTypeDefn, TermTypeBody),
(
TermTypeBody = hlds_du_type(type_body_du(Ctors, _, _, _, _, _)),
FieldName = unqualify_name(FieldSymName),
get_constructor_containing_field_loop(TermTypeCtor,
one_or_more_to_list(Ctors), FieldName, DuCtor, FieldNumber)
;
( TermTypeBody = hlds_eqv_type(_)
; TermTypeBody = hlds_foreign_type(_)
; TermTypeBody = hlds_solver_type(_)
; TermTypeBody = hlds_abstract_type(_)
),
unexpected($pred, "not du type")
).
:- pred get_constructor_containing_field_loop(type_ctor::in,
list(constructor)::in, string::in, du_ctor::out, int::out) is det.
get_constructor_containing_field_loop(_, [], _, _, _) :-
unexpected($pred, "can't find field").
get_constructor_containing_field_loop(TypeCtor, [Ctor | Ctors],
UnqualFieldName, DuCtor, FieldNumber) :-
Ctor = ctor(_, _, SymName, CtorArgs, Arity, _Ctxt),
( if
search_for_named_field(CtorArgs, UnqualFieldName, 1, FieldNumberPrime)
then
DuCtor = du_ctor(SymName, Arity, TypeCtor),
FieldNumber = FieldNumberPrime
else
get_constructor_containing_field_loop(TypeCtor, Ctors,
UnqualFieldName, DuCtor, FieldNumber)
).
:- pred search_for_named_field(list(constructor_arg)::in,
string::in, int::in, int::out) is semidet.
search_for_named_field([CtorArg | CtorArgs], UnqualFieldName,
CurFieldNumber, NamedFieldNumber) :-
( if
CtorArg ^ arg_field_name = yes(ctor_field_name(ArgFieldName, _)),
UnqualFieldName = unqualify_name(ArgFieldName)
then
NamedFieldNumber = CurFieldNumber
else
search_for_named_field(CtorArgs, UnqualFieldName,
CurFieldNumber + 1, NamedFieldNumber)
).
%---------------------------------------------------------------------------%
:- pred create_pure_atomic_unification_with_nonlocals(prog_var::in,
unify_rhs::in, hlds_goal_info::in, set_of_progvar::in, list(prog_var)::in,
unify_context::in, hlds_goal::out) is det.
create_pure_atomic_unification_with_nonlocals(Var, RHS, OldGoalInfo,
RestrictNonLocals, VarsList, UnifyContext, Goal) :-
Context = goal_info_get_context(OldGoalInfo),
GoalId = goal_info_get_goal_id(OldGoalInfo),
UnifyContext = unify_context(UnifyMainContext, UnifySubContext),
create_pure_atomic_complicated_unification(Var, RHS,
Context, UnifyMainContext, UnifySubContext, Goal0),
Goal0 = hlds_goal(GoalExpr0, GoalInfo0),
% Compute the nonlocals of the goal.
set_of_var.list_to_set(VarsList, NonLocals1),
set_of_var.intersect(RestrictNonLocals, NonLocals1, NonLocals),
goal_info_set_nonlocals(NonLocals, GoalInfo0, GoalInfo1),
% Use the goal id from the original goal, so that the constraint_ids
% will be as expected. (See the XXX comment near the definition of
% constraint_id in hlds_data.m for more info.)
goal_info_set_goal_id(GoalId, GoalInfo1, GoalInfo),
Goal = hlds_goal(GoalExpr0, GoalInfo).
:- pred make_new_vars(module_info::in, list(mer_type)::in, list(prog_var)::out,
var_table::in, var_table::out) is det.
make_new_vars(ModuleInfo, Types, Vars, !VarTable) :-
list.map_foldl(make_new_var(ModuleInfo), Types, Vars, !VarTable).
:- pred make_new_var(module_info::in, mer_type::in, prog_var::out,
var_table::in, var_table::out) is det.
make_new_var(ModuleInfo, Type, Var, !VarTable) :-
IsDummy = is_type_a_dummy(ModuleInfo, Type),
Entry = vte("", Type, IsDummy),
add_var_entry(Entry, Var, !VarTable).
%---------------------------------------------------------------------------%
% field_extraction_function_args(Args, InputTermArg).
% Work out which arguments of a field access correspond to the
% field being extracted/set, and which are the container arguments.
%
:- pred field_extraction_function_args(list(prog_var)::in, prog_var::out)
is det.
field_extraction_function_args(Args, TermInputArg) :-
( if Args = [TermInputArg0] then
TermInputArg = TermInputArg0
else
unexpected($pred, "num_args != 1")
).
% field_update_function_args(Args, InputTermArg, FieldArg).
%
:- pred field_update_function_args(list(prog_var)::in, prog_var::out,
prog_var::out) is det.
field_update_function_args(Args, TermInputArg, FieldArg) :-
( if Args = [TermInputArg0, FieldArg0] then
FieldArg = FieldArg0,
TermInputArg = TermInputArg0
else
unexpected($pred, "num_args != 2")
).
%---------------------------------------------------------------------------%
:- end_module check_hlds.resolve_unify_functor.
%---------------------------------------------------------------------------%
Reference in New Issue View Git Blame Copy Permalink