mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-20 00:15:27 +00:00
04dec8c205
Besides defining most of the types representing the smaller parts of
parse trees (parts smaller than items), prog_data.m also has many utility
predicates that operate on values of these types. Carve the three substantial
clusters of predicates out of prog_data.m, and move them into their own
modules, which are each imported by fewer modules than prog_data.m itself.
compiler/vartypes.m:
New module containing the vartypes type and the predicates that operate
on it. The new module has *much* better cohesion than the old prog_data.m.
The vartypes type does not appear in any parse tree; it is used only
in the HLDS. So make vartypes.m part of the hlds.m package, not
parse_tree.m.
Move three predicates that perform renamings and substitutions on vartypes
here from prog_type_subst.m, since the latter is part of the parse_tree.m
package, and thus doesn't have access to hlds.vartypes. Make private
the service predicate that these three moved predicates used to rely on,
since it has no other callers.
compiler/prog_detism.m:
New module containing utility predicates that operate on determinisms
and determinism components.
compiler/prog_rename.m:
New module containing utility predicates that rename variables in
various data structures.
compiler/prog_data.m:
Remove the stuff now in the three new modules.
compiler/prog_type_subst.m:
Remove the three predicates now in vartypes.m.
compiler/mercury_to_mercury.m:
Delete an unneded predicate, which was the only part of this module
that referred to vartypes.
compiler/prog_type.m:
compiler/builtin_lib_types.m:
compiler/type_util.m:
Move some utility predicates that refer to vartypes from prog_type.m
and builtin_lib_types.m (both part of parse_tree.m) to type_util.m
(part of check_hlds.m).
compiler/parse_tree.m:
compiler/hlds.m:
compiler/notes/compiler_design.html:
Mention the new modules.
compiler/accumulator.m:
compiler/add_class.m:
compiler/add_clause.m:
compiler/add_foreign_proc.m:
compiler/add_heap_ops.m:
compiler/add_pragma_type_spec.m:
compiler/add_pred.m:
compiler/add_trail_ops.m:
compiler/arg_info.m:
compiler/bytecode_gen.m:
compiler/call_gen.m:
compiler/clause_to_proc.m:
compiler/closure_analysis.m:
compiler/code_info.m:
compiler/code_loc_dep.m:
compiler/common.m:
compiler/complexity.m:
compiler/const_prop.m:
compiler/constraint.m:
compiler/continuation_info.m:
compiler/coverage_profiling.m:
compiler/cse_detection.m:
compiler/ctgc.datastruct.m:
compiler/ctgc.util.m:
compiler/deep_profiling.m:
compiler/deforest.m:
compiler/delay_construct.m:
compiler/delay_partial_inst.m:
compiler/dep_par_conj.m:
compiler/det_analysis.m:
compiler/det_report.m:
compiler/det_util.m:
compiler/disj_gen.m:
compiler/equiv_type_hlds.m:
compiler/erl_call_gen.m:
compiler/erl_code_gen.m:
compiler/erl_code_util.m:
compiler/exception_analysis.m:
compiler/float_regs.m:
compiler/follow_code.m:
compiler/follow_vars.m:
compiler/format_call.m:
compiler/goal_expr_to_goal.m:
compiler/goal_path.m:
compiler/goal_store.m:
compiler/goal_util.m:
compiler/headvar_names.m:
compiler/hhf.m:
compiler/higher_order.m:
compiler/hlds_clauses.m:
compiler/hlds_goal.m:
compiler/hlds_llds.m:
compiler/hlds_out_goal.m:
compiler/hlds_out_module.m:
compiler/hlds_out_pred.m:
compiler/hlds_pred.m:
compiler/hlds_rtti.m:
compiler/inlining.m:
compiler/inst_util.m:
compiler/instmap.m:
compiler/intermod.m:
compiler/interval.m:
compiler/lambda.m:
compiler/lco.m:
compiler/live_vars.m:
compiler/liveness.m:
compiler/lookup_switch.m:
compiler/make_goal.m:
compiler/mark_tail_calls.m:
compiler/ml_accurate_gc.m:
compiler/ml_code_gen.m:
compiler/ml_code_util.m:
compiler/ml_disj_gen.m:
compiler/ml_gen_info.m:
compiler/ml_lookup_switch.m:
compiler/ml_proc_gen.m:
compiler/ml_unify_gen.m:
compiler/mode_constraints.m:
compiler/mode_info.m:
compiler/mode_util.m:
compiler/modecheck_call.m:
compiler/modecheck_conj.m:
compiler/modecheck_goal.m:
compiler/modecheck_unify.m:
compiler/modecheck_util.m:
compiler/modes.m:
compiler/par_loop_control.m:
compiler/pd_info.m:
compiler/pd_util.m:
compiler/polymorphism.m:
compiler/post_typecheck.m:
compiler/prog_rep.m:
compiler/prop_mode_constraints.m:
compiler/purity.m:
compiler/qual_info.m:
compiler/quantification.m:
compiler/rbmm.points_to_graph.m:
compiler/rbmm.points_to_info.m:
compiler/rbmm.region_liveness_info.m:
compiler/rbmm.region_transformation.m:
compiler/saved_vars.m:
compiler/set_of_var.m:
compiler/simplify_goal_call.m:
compiler/simplify_goal_conj.m:
compiler/simplify_goal_disj.m:
compiler/simplify_goal_ite.m:
compiler/simplify_goal_scope.m:
compiler/simplify_goal_switch.m:
compiler/simplify_goal_unify.m:
compiler/simplify_info.m:
compiler/simplify_proc.m:
compiler/size_prof.m:
compiler/ssdebug.m:
compiler/stack_alloc.m:
compiler/stack_layout.m:
compiler/stack_opt.m:
compiler/stm_expand.m:
compiler/store_alloc.m:
compiler/structure_reuse.analysis.m:
compiler/structure_reuse.direct.choose_reuse.m:
compiler/structure_reuse.direct.detect_garbage.m:
compiler/structure_reuse.indirect.m:
compiler/structure_reuse.lbu.m:
compiler/structure_reuse.lfu.m:
compiler/structure_sharing.analysis.m:
compiler/structure_sharing.domain.m:
compiler/switch_detection.m:
compiler/table_gen.m:
compiler/tabling_analysis.m:
compiler/term_constr_build.m:
compiler/term_constr_initial.m:
compiler/term_constr_util.m:
compiler/term_pass1.m:
compiler/term_traversal.m:
compiler/term_util.m:
compiler/trace_gen.m:
compiler/trailing_analysis.m:
compiler/try_expand.m:
compiler/tupling.m:
compiler/type_assign.m:
compiler/type_constraints.m:
compiler/typecheck.m:
compiler/typecheck_errors.m:
compiler/unify_gen.m:
compiler/unify_proc.m:
compiler/unique_modes.m:
compiler/unneeded_code.m:
compiler/untupling.m:
compiler/unused_args.m:
compiler/var_locn.m:
Conform to the above changes, mostly by importing some of the
three new modules as well as, or instead of, prog_data.m.
312 lines
13 KiB
Mathematica
312 lines
13 KiB
Mathematica
%---------------------------------------------------------------------------%
|
|
% vim: ft=mercury ts=4 sw=4 et
|
|
%---------------------------------------------------------------------------%
|
|
% Copyright (C) 1996-2012 The University of Melbourne.
|
|
% 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 contains types and predicates for working with determinism
|
|
% information.
|
|
%
|
|
%---------------------------------------------------------------------------%
|
|
|
|
:- module parse_tree.prog_detism.
|
|
:- interface.
|
|
|
|
:- import_module parse_tree.prog_data.
|
|
|
|
:- import_module maybe.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
% The following predicates implement the tables for computing the
|
|
% determinism of compound goals from the determinism of their components.
|
|
|
|
:- pred det_conjunction_detism(determinism::in, determinism::in,
|
|
determinism::out) is det.
|
|
|
|
:- pred det_par_conjunction_detism(determinism::in, determinism::in,
|
|
determinism::out) is det.
|
|
|
|
:- pred det_switch_detism(determinism::in, determinism::in, determinism::out)
|
|
is det.
|
|
|
|
:- pred det_negation_det(determinism::in, maybe(determinism)::out) is det.
|
|
|
|
% The following predicates do abstract interpretation to count
|
|
% the number of solutions and the possible number of failures.
|
|
%
|
|
% If the num_solns is at_most_many_cc, this means that the goal might have
|
|
% many logical solutions if there were no pruning, but that the goal occurs
|
|
% in a single-solution context, so only the first solution will be
|
|
% returned.
|
|
%
|
|
% The reason why we don't throw an exception in det_switch_maxsoln and
|
|
% det_disjunction_maxsoln is given in the documentation of the test case
|
|
% invalid/magicbox.m.
|
|
|
|
:- pred det_conjunction_maxsoln(soln_count::in, soln_count::in,
|
|
soln_count::out) is det.
|
|
|
|
:- pred det_conjunction_canfail(can_fail::in, can_fail::in, can_fail::out)
|
|
is det.
|
|
|
|
:- pred det_disjunction_maxsoln(soln_count::in, soln_count::in,
|
|
soln_count::out) is det.
|
|
|
|
:- pred det_disjunction_canfail(can_fail::in, can_fail::in, can_fail::out)
|
|
is det.
|
|
|
|
:- pred det_switch_maxsoln(soln_count::in, soln_count::in, soln_count::out)
|
|
is det.
|
|
|
|
:- pred det_switch_canfail(can_fail::in, can_fail::in, can_fail::out) is det.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
:- type det_comparison
|
|
---> first_detism_tighter_than
|
|
% The first determinism promises strictly more than the second.
|
|
|
|
; first_detism_same_as
|
|
% The first determinism promises exactly as much as the second.
|
|
|
|
; first_detism_looser_than
|
|
% The first determinism promises strictly less than the second.
|
|
|
|
; first_detism_incomparable.
|
|
% The first determinism promises more than the second in one aspect
|
|
% (can_fail or soln_count), but promises less in the other aspect.
|
|
|
|
:- pred compare_determinisms(determinism::in, determinism::in,
|
|
det_comparison::out) is det.
|
|
|
|
:- type det_component_comparison
|
|
---> first_tighter_than
|
|
; first_same_as
|
|
; first_looser_than.
|
|
|
|
:- pred compare_canfails(can_fail::in, can_fail::in,
|
|
det_component_comparison::out) is det.
|
|
|
|
:- pred compare_solncounts(soln_count::in, soln_count::in,
|
|
det_component_comparison::out) is det.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
:- implementation.
|
|
|
|
:- import_module require.
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
det_conjunction_detism(DetismA, DetismB, Detism) :-
|
|
% When figuring out the determinism of a conjunction, if the second goal
|
|
% is unreachable, then then the determinism of the conjunction is just
|
|
% the determinism of the first goal.
|
|
|
|
determinism_components(DetismA, CanFailA, MaxSolnA),
|
|
(
|
|
MaxSolnA = at_most_zero,
|
|
Detism = DetismA
|
|
;
|
|
( MaxSolnA = at_most_one
|
|
; MaxSolnA = at_most_many
|
|
; MaxSolnA = at_most_many_cc
|
|
),
|
|
determinism_components(DetismB, CanFailB, MaxSolnB),
|
|
det_conjunction_canfail(CanFailA, CanFailB, CanFail),
|
|
det_conjunction_maxsoln(MaxSolnA, MaxSolnB, MaxSoln),
|
|
determinism_components(Detism, CanFail, MaxSoln)
|
|
).
|
|
|
|
det_par_conjunction_detism(DetismA, DetismB, Detism) :-
|
|
% Figuring out the determinism of a parallel conjunction is much easier
|
|
% than for a sequential conjunction, since you simply ignore the case
|
|
% where the second goal is unreachable. Just do a normal solution count.
|
|
|
|
determinism_components(DetismA, CanFailA, MaxSolnA),
|
|
determinism_components(DetismB, CanFailB, MaxSolnB),
|
|
det_conjunction_canfail(CanFailA, CanFailB, CanFail),
|
|
det_conjunction_maxsoln(MaxSolnA, MaxSolnB, MaxSoln),
|
|
determinism_components(Detism, CanFail, MaxSoln).
|
|
|
|
det_switch_detism(DetismA, DetismB, Detism) :-
|
|
determinism_components(DetismA, CanFailA, MaxSolnA),
|
|
determinism_components(DetismB, CanFailB, MaxSolnB),
|
|
det_switch_canfail(CanFailA, CanFailB, CanFail),
|
|
det_switch_maxsoln(MaxSolnA, MaxSolnB, MaxSoln),
|
|
determinism_components(Detism, CanFail, MaxSoln).
|
|
|
|
det_negation_det(detism_det, yes(detism_failure)).
|
|
det_negation_det(detism_semi, yes(detism_semi)).
|
|
det_negation_det(detism_multi, no).
|
|
det_negation_det(detism_non, no).
|
|
det_negation_det(detism_cc_multi, no).
|
|
det_negation_det(detism_cc_non, no).
|
|
det_negation_det(detism_erroneous, yes(detism_erroneous)).
|
|
det_negation_det(detism_failure, yes(detism_det)).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
det_conjunction_maxsoln(at_most_zero, at_most_zero, at_most_zero).
|
|
det_conjunction_maxsoln(at_most_zero, at_most_one, at_most_zero).
|
|
det_conjunction_maxsoln(at_most_zero, at_most_many_cc, at_most_zero).
|
|
det_conjunction_maxsoln(at_most_zero, at_most_many, at_most_zero).
|
|
|
|
det_conjunction_maxsoln(at_most_one, at_most_zero, at_most_zero).
|
|
det_conjunction_maxsoln(at_most_one, at_most_one, at_most_one).
|
|
det_conjunction_maxsoln(at_most_one, at_most_many_cc, at_most_many_cc).
|
|
det_conjunction_maxsoln(at_most_one, at_most_many, at_most_many).
|
|
|
|
det_conjunction_maxsoln(at_most_many_cc, at_most_zero, at_most_zero).
|
|
det_conjunction_maxsoln(at_most_many_cc, at_most_one, at_most_many_cc).
|
|
det_conjunction_maxsoln(at_most_many_cc, at_most_many_cc, at_most_many_cc).
|
|
det_conjunction_maxsoln(at_most_many_cc, at_most_many, _) :-
|
|
% If the first conjunct could be cc pruned, the second conj ought to have
|
|
% been cc pruned too.
|
|
unexpected($module, $pred, "many_cc, many").
|
|
|
|
det_conjunction_maxsoln(at_most_many, at_most_zero, at_most_zero).
|
|
det_conjunction_maxsoln(at_most_many, at_most_one, at_most_many).
|
|
det_conjunction_maxsoln(at_most_many, at_most_many_cc, at_most_many).
|
|
det_conjunction_maxsoln(at_most_many, at_most_many, at_most_many).
|
|
|
|
det_conjunction_canfail(can_fail, can_fail, can_fail).
|
|
det_conjunction_canfail(can_fail, cannot_fail, can_fail).
|
|
det_conjunction_canfail(cannot_fail, can_fail, can_fail).
|
|
det_conjunction_canfail(cannot_fail, cannot_fail, cannot_fail).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
det_disjunction_maxsoln(at_most_zero, at_most_zero, at_most_zero).
|
|
det_disjunction_maxsoln(at_most_zero, at_most_one, at_most_one).
|
|
det_disjunction_maxsoln(at_most_zero, at_most_many_cc, at_most_many_cc).
|
|
det_disjunction_maxsoln(at_most_zero, at_most_many, at_most_many).
|
|
|
|
det_disjunction_maxsoln(at_most_one, at_most_zero, at_most_one).
|
|
det_disjunction_maxsoln(at_most_one, at_most_one, at_most_many).
|
|
det_disjunction_maxsoln(at_most_one, at_most_many_cc, at_most_many_cc).
|
|
det_disjunction_maxsoln(at_most_one, at_most_many, at_most_many).
|
|
|
|
det_disjunction_maxsoln(at_most_many_cc, at_most_zero, at_most_many_cc).
|
|
det_disjunction_maxsoln(at_most_many_cc, at_most_one, at_most_many_cc).
|
|
det_disjunction_maxsoln(at_most_many_cc, at_most_many_cc, at_most_many_cc).
|
|
det_disjunction_maxsoln(at_most_many_cc, at_most_many, at_most_many_cc).
|
|
|
|
det_disjunction_maxsoln(at_most_many, at_most_zero, at_most_many).
|
|
det_disjunction_maxsoln(at_most_many, at_most_one, at_most_many).
|
|
det_disjunction_maxsoln(at_most_many, at_most_many_cc, at_most_many_cc).
|
|
det_disjunction_maxsoln(at_most_many, at_most_many, at_most_many).
|
|
|
|
det_disjunction_canfail(can_fail, can_fail, can_fail).
|
|
det_disjunction_canfail(can_fail, cannot_fail, cannot_fail).
|
|
det_disjunction_canfail(cannot_fail, can_fail, cannot_fail).
|
|
det_disjunction_canfail(cannot_fail, cannot_fail, cannot_fail).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
det_switch_maxsoln(at_most_zero, at_most_zero, at_most_zero).
|
|
det_switch_maxsoln(at_most_zero, at_most_one, at_most_one).
|
|
det_switch_maxsoln(at_most_zero, at_most_many_cc, at_most_many_cc).
|
|
det_switch_maxsoln(at_most_zero, at_most_many, at_most_many).
|
|
|
|
det_switch_maxsoln(at_most_one, at_most_zero, at_most_one).
|
|
det_switch_maxsoln(at_most_one, at_most_one, at_most_one).
|
|
det_switch_maxsoln(at_most_one, at_most_many_cc, at_most_many_cc).
|
|
det_switch_maxsoln(at_most_one, at_most_many, at_most_many).
|
|
|
|
det_switch_maxsoln(at_most_many_cc, at_most_zero, at_most_many_cc).
|
|
det_switch_maxsoln(at_most_many_cc, at_most_one, at_most_many_cc).
|
|
det_switch_maxsoln(at_most_many_cc, at_most_many_cc, at_most_many_cc).
|
|
det_switch_maxsoln(at_most_many_cc, at_most_many, at_most_many_cc).
|
|
|
|
det_switch_maxsoln(at_most_many, at_most_zero, at_most_many).
|
|
det_switch_maxsoln(at_most_many, at_most_one, at_most_many).
|
|
det_switch_maxsoln(at_most_many, at_most_many_cc, at_most_many_cc).
|
|
det_switch_maxsoln(at_most_many, at_most_many, at_most_many).
|
|
|
|
det_switch_canfail(can_fail, can_fail, can_fail).
|
|
det_switch_canfail(can_fail, cannot_fail, can_fail).
|
|
det_switch_canfail(cannot_fail, can_fail, can_fail).
|
|
det_switch_canfail(cannot_fail, cannot_fail, cannot_fail).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
|
|
compare_determinisms(DetismA, DetismB, CmpDetism) :-
|
|
determinism_components(DetismA, CanFailA, SolnsA),
|
|
determinism_components(DetismB, CanFailB, SolnsB),
|
|
compare_canfails(CanFailA, CanFailB, CmpCanFail),
|
|
compare_solncounts(SolnsA, SolnsB, CmpSolns),
|
|
|
|
% We can get e.g. tighter canfail and looser solncount
|
|
% e.g. for a predicate declared multidet and inferred semidet.
|
|
% Therefore the ordering of the following two tests is important:
|
|
% we want errors to take precedence over warnings.
|
|
|
|
(
|
|
CmpCanFail = first_tighter_than,
|
|
(
|
|
( CmpSolns = first_tighter_than
|
|
; CmpSolns = first_same_as
|
|
),
|
|
CmpDetism = first_detism_tighter_than
|
|
;
|
|
CmpSolns = first_looser_than,
|
|
CmpDetism = first_detism_incomparable
|
|
)
|
|
;
|
|
CmpCanFail = first_same_as,
|
|
(
|
|
CmpSolns = first_tighter_than,
|
|
CmpDetism = first_detism_tighter_than
|
|
;
|
|
CmpSolns = first_same_as,
|
|
CmpDetism = first_detism_same_as
|
|
;
|
|
CmpSolns = first_looser_than,
|
|
CmpDetism = first_detism_looser_than
|
|
)
|
|
;
|
|
CmpCanFail = first_looser_than,
|
|
(
|
|
CmpSolns = first_tighter_than,
|
|
CmpDetism = first_detism_incomparable
|
|
;
|
|
( CmpSolns = first_same_as
|
|
; CmpSolns = first_looser_than
|
|
),
|
|
CmpDetism = first_detism_looser_than
|
|
)
|
|
).
|
|
|
|
compare_canfails(cannot_fail, cannot_fail, first_same_as).
|
|
compare_canfails(cannot_fail, can_fail, first_tighter_than).
|
|
compare_canfails(can_fail, cannot_fail, first_looser_than).
|
|
compare_canfails(can_fail, can_fail, first_same_as).
|
|
|
|
compare_solncounts(at_most_zero, at_most_zero, first_same_as).
|
|
compare_solncounts(at_most_zero, at_most_one, first_tighter_than).
|
|
compare_solncounts(at_most_zero, at_most_many_cc, first_tighter_than).
|
|
compare_solncounts(at_most_zero, at_most_many, first_tighter_than).
|
|
|
|
compare_solncounts(at_most_one, at_most_zero, first_looser_than).
|
|
compare_solncounts(at_most_one, at_most_one, first_same_as).
|
|
compare_solncounts(at_most_one, at_most_many_cc, first_tighter_than).
|
|
compare_solncounts(at_most_one, at_most_many, first_tighter_than).
|
|
|
|
compare_solncounts(at_most_many_cc, at_most_zero, first_looser_than).
|
|
compare_solncounts(at_most_many_cc, at_most_one, first_looser_than).
|
|
compare_solncounts(at_most_many_cc, at_most_many_cc, first_same_as).
|
|
compare_solncounts(at_most_many_cc, at_most_many, first_tighter_than).
|
|
|
|
compare_solncounts(at_most_many, at_most_zero, first_looser_than).
|
|
compare_solncounts(at_most_many, at_most_one, first_looser_than).
|
|
compare_solncounts(at_most_many, at_most_many_cc, first_looser_than).
|
|
compare_solncounts(at_most_many, at_most_many, first_same_as).
|
|
|
|
%---------------------------------------------------------------------------%
|
|
:- end_module parse_tree.prog_detism.
|
|
%---------------------------------------------------------------------------%
|