[m-rev.] Constraint-based typechecking
Ralph Becket
rafe at csse.unimelb.edu.au
Wed Feb 18 12:56:21 AEDT 2009
Good work!
Andrew Wesley Ebert, Tuesday, 17 February 2009:
> Estimated hours taken: 300
> Branches: main
>
> Created a constraint-based typechecker. The typechecker works by generating
> a collection of constraints on the types of variables in each clause of the
> program, then solving these constraints using propagation. Information on the
> types of local variables (clauses_info^clauses_vartypes) and the IDs of
> predicate calls (hlds_goal_expr^call_pred_id) is passed back into the HLDS.
>
> In the event that the program being compiled is not type-correct, the
> typechecker will generate an error message describing the error. If the
> constraints on a variable cannot fully determine a type, the typechecker will
> report each possible type the variable could take. If the constraints on the
> type of a variable are unatisfiable, the compiler will report each minimal
> unsatisfiable subset of the constraints, pointing out the likely location(s)
> of the error.
>
> The constraint-based typechecker can handle ambiguous predicate calls and
> functor unifications much more efficiently than the old typechecker. However,
> it cannot handle anything related to existentially qualified variables,
> typeclass constraints and typeclass methods. The detail and clarity of error
> reporting is also rather poor.
>
> These changes have not yet been comprehensively debugged, although it
> should work in most cases, given the exceptions detailed above.
>
> To use the constraint-based typechecker instead of the original typechecker,
> enable the option --type-check-constraints when compiling your program.
>
> compiler/type_constraints.m:
> Built from scratch.
>
> compiler/mercury_compile.m:
> Imported the constraint-based typechecker.
> Enabled constraint-based typechecking if the --type-check-constraints
> option is set.
>
> compiler/options.m:
> Added the --type-check-constraints option.
>
> library/list.m:
> Added a list.filter_map_foldl predicate.
> Added a list.zip_single predicate.
I don't think zip_single is useful enough to add to the standard
library: it only appears once in your code.
>
> library/set.m:
> Added a predicate version of set.filter_map.
>
> library/maybe.m:
> Added a predicate maybe.remove_maybe to semideterministically strip the
> "yes" off of a maybe expression.
I don't think remove_maybe/2 is useful enough to add to the standard
library: it only appears once in your code.
> Index: NEWS
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/NEWS,v
> retrieving revision 1.502
> diff -u -r1.502 NEWS
> --- NEWS 30 Jan 2009 03:51:43 -0000 1.502
> +++ NEWS 17 Feb 2009 04:09:08 -0000
> @@ -85,10 +85,18 @@
> * Processes no longer terminate until all threads have finished. Previously
> a process would terminate as soon as the original thread finished.
>
> +* The following predicate has been added to the set module:
> + set.filter_map/3
> +
> +* The following predicate has been added to the maybe module:
> + maybe.remove_maybe/2
> +
> * The following predicate has been added to the array module:
> array.foldl2/6
>
> * The following predicates have been added to the list module:
> + list.filter_map_foldl/5
> + list.zip_single/3
> list.map_corresponding/4
> list.map2_foldl3/10
> list.map_corresponding_foldl/6
> Index: compiler/check_hlds.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/check_hlds.m,v
> retrieving revision 1.20
> diff -u -r1.20 check_hlds.m
> --- compiler/check_hlds.m 3 Apr 2008 05:26:42 -0000 1.20
> +++ compiler/check_hlds.m 6 Feb 2009 02:36:06 -0000
> @@ -1,7 +1,7 @@
> %-----------------------------------------------------------------------------%
> % vim: ft=mercury ts=4 sw=4 et
> %-----------------------------------------------------------------------------%
> -% Copyright (C) 2002-2006 The University of Melbourne.
> +% Copyright (C) 2002-2006, 2009 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.
> %-----------------------------------------------------------------------------%
> @@ -18,6 +18,7 @@
> :- include_module check_typeclass.
> :- include_module post_typecheck.
> :- include_module purity.
> + :- include_module type_constraints.
> :- include_module type_util.
> :- include_module typecheck.
> :- include_module typecheck_errors.
> Index: compiler/mercury_compile.m
> ===================================================================
> RCS file:
> /home/mercury/mercury1/repository/mercury/compiler/mercury_compile.m,v
> retrieving revision 1.487
> diff -u -r1.487 mercury_compile.m
> --- compiler/mercury_compile.m 30 Jan 2009 03:51:44 -0000 1.487
> +++ compiler/mercury_compile.m 11 Feb 2009 00:44:07 -0000
> @@ -54,6 +54,7 @@
> :- import_module parse_tree.equiv_type.
> :- import_module hlds.make_hlds.
> :- import_module check_hlds.typecheck.
> +:- import_module check_hlds.type_constraints.
> :- import_module check_hlds.purity.
> :- import_module check_hlds.implementation_defined_literals.
> :- import_module check_hlds.polymorphism.
> @@ -2149,6 +2150,8 @@
> globals.lookup_bool_option(Globals, use_opt_files, UseOptFiles),
> globals.lookup_bool_option(Globals, make_optimization_interface,
> MakeOptInt),
> + globals.lookup_bool_option(Globals, type_check_constraints,
> + TypeCheckConstraints),
> (
> ( IntermodOpt = yes
> ; IntermodAnalysis = yes
> @@ -2185,7 +2188,15 @@
> % Next typecheck the clauses.
> maybe_write_string(Verbose, "% Type-checking...\n", !IO),
> maybe_write_string(Verbose, "% Type-checking clauses...\n", !IO),
> - typecheck_module(!HLDS, TypeCheckSpecs,
> ExceededTypeCheckIterationLimit),
> + (
> + TypeCheckConstraints = yes,
> + typecheck_constraints(!HLDS, TypeCheckSpecs),
> + ExceededTypeCheckIterationLimit = no
> + ;
> + TypeCheckConstraints = no,
> + typecheck_module(!HLDS, TypeCheckSpecs,
> + ExceededTypeCheckIterationLimit)
> + ),
> write_error_specs(TypeCheckSpecs, Globals, 0, _NumTypeWarnings,
> 0, NumTypeErrors, !IO),
> maybe_report_stats(Stats, !IO),
> Index: compiler/options.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/compiler/options.m,v
> retrieving revision 1.642
> diff -u -r1.642 options.m
> --- compiler/options.m 20 Jan 2009 06:24:03 -0000 1.642
> +++ compiler/options.m 11 Feb 2009 00:41:04 -0000
> @@ -515,6 +515,8 @@
>
> ; allow_multi_arm_switches
>
> + ; type_check_constraints
> +
> % Code generation options
> ; low_level_debug
> ; table_debug
> @@ -1296,7 +1298,8 @@
> size_region_disj_snapshot - int(3),
> size_region_commit_entry - int(1),
> solver_type_auto_init - bool(no),
> - allow_multi_arm_switches - bool(yes)
> + allow_multi_arm_switches - bool(yes),
> + type_check_constraints - bool(no)
> ]).
> option_defaults_2(code_gen_option, [
> % Code Generation Options
> @@ -2133,8 +2136,9 @@
> long_option("size-region-semi-disj-protect",
> size_region_semi_disj_protect).
> long_option("size-region-disj-snapshot", size_region_disj_snapshot).
> long_option("size-region-commit-entry", size_region_commit_entry).
> -long_option("solver-type-auto-init", solver_type_auto_init).
> -long_option("allow-multi-arm-switches", allow_multi_arm_switches).
> +long_option("solver-type-auto-init", solver_type_auto_init).
> +long_option("allow-multi-arm-switches", allow_multi_arm_switches).
> +long_option("type-check-constraints", type_check_constraints).
>
> % code generation options
> long_option("low-level-debug", low_level_debug).
> @@ -4368,6 +4372,11 @@
> % "(This option is not for general use.)",
> % Allow the compiler to generate switches in which one arm handles
> % more than one cons_id.
> +
> + % This is a developer only option.
> +% "--type-check-constraints",
> +% "(This option is not for general use.)",
> +% Use the constraint based type checker instead of the old one.
> ]).
>
> :- pred options_help_code_generation(io::di, io::uo) is det.
> Index: compiler/type_constraints.m
> ===================================================================
> RCS file: compiler/type_constraints.m
> diff -N compiler/type_constraints.m
> --- /dev/null 1 Jan 1970 00:00:00 -0000
> +++ compiler/type_constraints.m 17 Feb 2009 03:05:48 -0000
> @@ -0,0 +1,2407 @@
> +%-----------------------------------------------------------------------------%
> +% vim: ft=mercury ts=4 sw=4 et wm=4 tw=0
> +%-----------------------------------------------------------------------------%
> +%
> +%
> +% File: type_constraints.m
> +% Main author: aebert
> +%
> +% Constructs a set of constraints from a Mercury program,
> +% then solves these constraints in order to determine the
> +% types of all local variables in the program.
> +%
> +%-----------------------------------------------------------------------------%
> +
> +:- module check_hlds.type_constraints.
> +:- interface.
> +
> +:- import_module hlds.
> +:- import_module hlds.hlds_module.
> +:- import_module parse_tree.
> +:- import_module parse_tree.error_util.
> +
> +:- import_module list.
> +
> +:- pred typecheck_constraints(module_info::in, module_info::out,
> + list(error_spec)::out) is det.
> +
> +%-----------------------------------------------------------------------------%
> +
> +:- implementation.
> +
> +:- import_module check_hlds.goal_path.
> +:- import_module hlds.goal_util.
> +:- import_module hlds.hlds_clauses.
> +:- import_module hlds.hlds_data.
> +:- import_module hlds.hlds_goal.
> +:- import_module hlds.hlds_pred.
> +:- import_module hlds.pred_table.
> +:- import_module hlds.special_pred.
> +:- import_module libs.compiler_util.
> +:- import_module mdbcomp.
> +:- import_module mdbcomp.prim_data.
> +:- import_module mdbcomp.program_representation.
> +:- import_module parse_tree.mercury_to_mercury.
> +:- import_module parse_tree.prog_data.
> +:- import_module parse_tree.prog_event.
> +:- import_module parse_tree.prog_type.
> +:- import_module parse_tree.prog_type_subst.
> +
> +:- import_module assoc_list.
> +:- import_module bimap.
> +:- import_module bool.
> +:- import_module counter.
> +:- import_module int.
> +:- import_module io.
> +:- import_module map.
> +:- import_module maybe.
> +:- import_module pair.
> +:- import_module require.
> +:- import_module set.
> +:- import_module std_util.
> +:- import_module string.
> +:- import_module svbimap.
> +:- import_module svmap.
> +:- import_module svset.
> +:- import_module svvarset.
> +:- import_module term.
> +:- import_module varset.
> +
> +%-----------------------------------------------------------------------------%
> +%-----------------------------------------------------------------------------%
> +
> + % A type constraint can be a conjunction of simple type constraints,
> or a
> + % disjunction of conjunctions of simple type constraints. The second
> field
> + % of the disjunction case indicates whether the disjunction has been
> + % reduced by propagation to a single relevant constraint.
Here and below, the convention is to attach comments below the individual
data constructors rather than mention them in the header. You should
give some idea of why the singleton condition is important. You should
also use a field name or define a self explanatory type instead of using
maybe. For example:
:- type type_constraint
---> tconstr_conj(
conj_type_constraint
)
; tconstr_disj(
list(conj_type_constraint),
reduced_to_conj
% This field indicates whether propagation has
% eliminated all but one disjunct. This is
% needed because...
).
:- type reduced_to_conj
---> not_reduced_to_conj
; reduced_to_conj(conj_type_constraint).
> + %
> +:- type type_constraint
> + ---> tconstr_conj(
> + conj_type_constraint
> + )
> + ; tconstr_disj(
> + list(conj_type_constraint),
> + maybe(conj_type_constraint)
> + ).
> +
> + % A conjunction of simple type constraints, corresponding to all the
> + % constraints generated by one interpretation of a simple goal
> + % Simple constraints generated by the goal
> + % Whether the constraint has been found to be unsatisfiable
> + % The context in which the goal appeared
> + % The path to the goal, if the goal might need to be modified with
> + % information generated by the typechecker
> + % The ID of the predicate being called by the goal, if it is a
> + % predicate call goal.
As above. Also, end your sentences with full stops.
> + %
> +:- type conj_type_constraint
> + ---> ctconstr(
> + tconstr_simples :: list(simple_type_constraint),
> + tconstr_activity :: tconstr_activity,
> + tconstr_context :: prog_context,
> + tconstr_goal_path :: maybe(goal_path),
> + tconstr_pred_id :: maybe(pred_id)
> + ).
> +
> + % Whether or not a constraint is still relevant to the typechecker.
> + % Irrelevant constraints are kept in order to report accurate error
> + % messages.
> + %
> +:- type tconstr_activity
> + ---> tconstr_active
> + ; tconstr_unsatisfiable.
> +
> + % All simple type constraints constrain the possible types of type
> + % variables.
> + % This makes it easier to handle implicit unifications of type
> variables,
> + % e.g. in the case of cons(T, list(T), list(T))
> + % Unification of type variables (T1 = T2) is handled by
> + % stconstr(T1, type_variable(T2), ...)
> + % Functor unification
> + % (T1 = foo(T2, T3), where foo is a constructor of type a) is handled by
> + % stconstr( T1, defined_type(a, [type_variable(T2), type_variable(T3)]))
Can you reformat this comment to make it clearer?
> + %
> +:- type simple_type_constraint
> + ---> stconstr(
> + tvar,
> + mer_type
> + ).
stconstr is a rather opaque name. How about tvar_is_type?
> +
> +:- type type_constraint_set == set(type_constraint_id).
> +
> +:- type type_constraint_map == map(type_constraint_id, type_constraint).
> +
> + % A map from program variables to all constraints involving those
> variables
> + %
> +:- type var_constraint_map == map(tvar, list(type_constraint_id)).
Full stops! (Add throughout.)
> +
> + % A map from program variables to the type variables they correspond to
> + %
> +:- type prog_var_map == bimap(prog_var, tvar).
> +
> +:- type simple_prog_var_map == map(prog_var, tvar).
Why a bimap and a map type?
> +
> + % A map from type variables to their possible types
> + %
> +:- type type_domain_map == map(tvar, type_domain).
> +
> + % A set of types. tdomain_any represents the set of all types, for
> unbound
The convention is to put two spaces after a full stop.
> + % type variables. tdomain_singleton tells the compiler when a variable
> + % type has become known and can be propagated.
> + %
> +:- type type_domain
> + ---> tdomain(set(mer_type))
> + ; tdomain_singleton(mer_type)
> + ; tdomain_any.
> +
> + % All the information the typechecker finds for any given predicate
> + % map(prog_var, type_var)
> + % map(type_constraint_id, constraint)
> + % map(type_var, [type_constraint_id])
> + % Set of relevant type variables
> + % Set of relevant program variables
This comment is hard to understand. As mentioned above, you need to
attach field-specific comments to the fields themselves.
> + %
> +:- type type_constraint_info
> + ---> tconstr_info(
> + tconstr_var_map :: prog_var_map,
> + tconstr_constraint_counter :: type_constraint_counter,
> + tconstr_constraint_map :: type_constraint_map,
> + tconstr_var_constraints :: var_constraint_map,
> + tconstr_tvarset :: tvarset,
> + tconstr_error_spec :: error_specs
> + ).
> +
> + % Maps from IDs of program elements to their definitions,
> + % extracted from the HLDS
> + %
> +:- type tconstr_environment
> + ---> tconstr_environment(
> + event_env :: event_env,
> + class_env :: class_env,
> + func_env :: func_env,
> + pred_env :: pred_env
> + % type_env :: type_env,
> + ).
> +
> +:- type event_env == event_spec_map. % map(string, event_spec)
> +:- type class_env == class_table. % map(class_id, hlds_class_defn)
> +% :- type type_env == type_table. % map(type_ctor, hlds_type_defn)
> +:- type func_env == cons_table. % map(cons_id, list(hlds_cons_defn))
Why reproduce the types in comments? That's actually a maintenance
problem: should we ever change those types, we'll have to search for
comments like these as well. Best not to have comments like these at all.
> +:- type pred_env == predicate_table.
> +:- type type_constraint_id == int.
> +:- type type_constraint_counter == counter.
> +
> +:- type error_specs == list(error_spec).
> +
> +%-----------------------------------------------------------------------------%
> +%-----------------------------------------------------------------------------%
> +
> + % This is the predicate called by the compiler to perform the typecheck
> + % pass.
> + %
> +typecheck_constraints(!HLDS, ErrorSpec) :-
> + % hlds_module.module_info_get_type_table(!.HLDS, TypeEnv),
> + hlds_module.module_info_get_event_set(!.HLDS, event_set(_, EventEnv)),
> + hlds_module.module_info_get_class_table(!.HLDS, ClassEnv),
> + hlds_module.module_info_get_cons_table(!.HLDS, FuncEnv),
> + hlds_module.module_info_get_predicate_table(!.HLDS, PredEnv),
> + hlds_module.module_info_predids(PredIDs, !HLDS),
> +
> + list.foldl3(typecheck_one_predicate_if_needed, PredIDs,
> + tconstr_environment(EventEnv, ClassEnv, FuncEnv, PredEnv), _, !HLDS,
> + [], ErrorSpec).
> +
> +:- pred typecheck_one_predicate_if_needed(pred_id::in,
> tconstr_environment::in,
> + tconstr_environment::out, module_info::in, module_info::out,
> + error_specs::in, error_specs::out) is det.
> +typecheck_one_predicate_if_needed(PredID, !Environment, !HLDS, !Errors) :-
> + predicate_table_get_preds(!.Environment^pred_env, Preds),
> + map.lookup(Preds, PredID, PredInfo),
> + (
> + % Compiler-generated predicates are created already type-correct,
> + % so there's no need to typecheck them. The same is true for
> builtins.
> + % But, compiler-generated unify predicates are not guaranteed to be
It's not great style to start a sentence with "but".
> + % type-correct if they call a user-defined equality or comparison
> + % predicate or if it is a special pred for an existentially typed
> + % data type.
s/existentially typed data type/existentially quantified type/
> + (
> + is_unify_or_compare_pred(PredInfo),
> + \+ special_pred_needs_typecheck(PredInfo, !.HLDS)
> + ;
> + pred_info_is_builtin(PredInfo)
> + )
> + ->
> + pred_info_get_clauses_info(PredInfo, ClausesInfo0),
> + clauses_info_get_clauses_rep(ClausesInfo0, ClausesRep0),
> + IsEmpty = clause_list_is_empty(ClausesRep0),
> + (
> + IsEmpty = yes,
> + pred_info_mark_as_external(PredInfo, PredInfo1),
> + map.det_update(Preds, PredID, PredInfo1, Preds1),
> + predicate_table_set_preds(Preds1, !.Environment^pred_env,
> + PredEnv1),
> + module_info_set_predicate_table(PredEnv1, !HLDS),
> + !:Environment = !.Environment^pred_env := PredEnv1
> + ;
> + IsEmpty = no
> + )
> + ;
> + typecheck_one_predicate(PredID, !Environment, !HLDS, !Errors)
> + ).
> +
> +
> +:- pred typecheck_one_predicate(pred_id::in, tconstr_environment::in,
> + tconstr_environment::out, module_info::in, module_info::out,
> + error_specs::in, error_specs::out) is det.
> +typecheck_one_predicate(PredID, !Environment, !HLDS, !Errors) :-
Add a blank line between the pred declaration and the clause.
> + % Find the clause list in the predicate definition
> + predicate_table_get_preds(!.Environment^pred_env, Preds),
> + map.lookup(Preds, PredID, PredInfo),
> + pred_info_get_typevarset(PredInfo, TVarSet),
> + pred_info_get_context(PredInfo, Context),
> + pred_info_get_clauses_info(PredInfo, ClausesInfo),
> + clauses_info_get_varset(ClausesInfo, ProgVarSet),
> + clauses_info_clauses_only(ClausesInfo, Clauses0),
> +
> + trace [compile_time(flag("print_type_constraints")), io(!IO)] (
> + LineNumber = string.int_to_string(term.context_line(Context)),
> + FileName = term.context_file(Context),
> + PredNumber = int_to_string(pred_id_to_int(PredID)),
> + io.write_string("=== Predicate " ++ PredNumber ++ " [" ++
> + FileName ++ ": " ++ LineNumber ++ "] ===\n", !IO)
> + ),
> +
> + % Create a set of constraints on the types of the head variables
> + clauses_info_get_headvar_list(ClausesInfo, HeadVars),
> + pred_info_get_arg_types(PredInfo, HeadTypes),
> + prog_type.type_vars_list(HeadTypes, HeadTVars),
> + foldl_corresponding(variable_assignment_constraint(Context), HeadVars,
> + HeadTypes, tconstr_info(bimap.init, counter.init(0), map.init,
> + map.init, TVarSet, []), TCInfo),
> +
> + % Typecheck each clause of the predicate
> + list.map3(typecheck_one_clause(!.HLDS, !.Environment, ProgVarSet,
> + HeadTVars, TCInfo), Clauses0, Clauses, VartypesMaps, ErrorSpecs),
> +
> + % Update the predicate table in the environment and HLDS with the
> + % type info found in the typechecking process
> + clauses_info_set_clauses(Clauses, ClausesInfo, ClausesInfo1),
> + (
> + VartypesMaps = [VartypesHead | VartypesTail],
> + list.foldl(map.merge, VartypesTail, VartypesHead, Vartypes0)
> + ;
> + VartypesMaps = [],
> + Vartypes0 = map.init
> + ),
> + list.foldl(add_unused_prog_var(TCInfo), HeadVars, Vartypes0, Vartypes),
> + clauses_info_set_vartypes(Vartypes, ClausesInfo1, ClausesInfo2),
> + pred_info_set_clauses_info(ClausesInfo2, PredInfo, PredInfo1),
> + pred_info_set_typevarset(TCInfo^tconstr_tvarset, PredInfo1, PredInfo2),
> + map.det_update(Preds, PredID, PredInfo2, Preds1),
> + predicate_table_set_preds(Preds1, !.Environment^pred_env, PredEnv1),
> + module_info_set_predicate_table(PredEnv1, !HLDS),
> + !:Environment = !.Environment^pred_env := PredEnv1,
> + list.append(list.condense(ErrorSpecs), !Errors).
> +
> +
> +:- pred typecheck_one_clause(module_info::in, tconstr_environment::in,
> + prog_varset::in, list(tvar)::in, type_constraint_info::in, clause::in,
> + clause::out, vartypes::out, error_specs::out) is det.
> +
> +typecheck_one_clause(HLDS, Environment, ProgVarSet, HeadTVars, !.TCInfo,
> + !.Clause @ clause(_, !.Goal, _, Context), !:Clause, Vartypes,
> + Errors) :-
> + % Create a set of constraints from the goal
> + fill_goal_path_slots_in_goal(!.Goal, map.init, HLDS, !:Goal),
> + goal_to_constraint(Environment, !.Goal, !TCInfo),
> + trace [compile_time(flag("print_type_constraints")), io(!IO)] (
> + print_pred_constraint(!.TCInfo, ProgVarSet, !IO)
> + ),
> +
> + % Solve the constraint
> + find_type_constraint_solutions(Context, ProgVarSet, DomainMap0,
> !TCInfo),
> + list.foldl2_corresponding(unify_equal_tvars(!.TCInfo, set.init),
> + HeadTVars, HeadTVars, map.init, ReplacementMap, DomainMap0,
> DomainMap),
> +
> + % Print the solution
> + trace [compile_time(flag("print_type_constraints")), io(!IO)] (
> + print_constraint_solution(!.TCInfo, ProgVarSet, DomainMap, !IO)
> + ),
> +
> + % Update the HLDS with the results of the solving and report any
> + % ambiguity errors found in this process.
> + update_goal(Environment^pred_env, !.TCInfo^tconstr_constraint_map,
> !Goal,
> + PredErrors),
> + create_vartypes_map(Context, ProgVarSet, !.TCInfo^tconstr_tvarset,
> + !.TCInfo^tconstr_var_map, DomainMap, ReplacementMap, Vartypes,
> + VarTypeErrors),
> + !:Clause = !.Clause^clause_body := !.Goal,
> + list.append(PredErrors, VarTypeErrors, NewErrors),
> + list.foldl(add_message_to_spec, NewErrors, !TCInfo),
> + Errors = !.TCInfo^tconstr_error_spec.
> +
> +%-----------------------------------------------------------------------------%
> +% General typechecking utility predicates
> +
> + % A compiler-generated predicate only needs type checking if
> + % (a) it is a user-defined equality pred, or
You shouldn't preceed 'or' with a comma unless it's at the end of a
list.
> + % (b) it is the unification or comparison predicate for an existially
> + % quantified type.
> + %
> + % In case (b), we need to typecheck it to fill in the head_type_params
> + % field in the pred_info.
> + %
> +:- pred special_pred_needs_typecheck(pred_info::in, module_info::in)
> + is semidet.
> +
> +special_pred_needs_typecheck(PredInfo, ModuleInfo) :-
> + % Check if the predicate is a compiler-generated special
> + % predicate, and if so, for which type.
> + pred_info_get_origin(PredInfo, Origin),
> + Origin = origin_special_pred(SpecialPredId - TypeCtor),
> +
> + % Check that the special pred isn't one of the builtin types which don't
> + % have a hlds_type_defn.
> + \+ list.member(TypeCtor, builtin_type_ctors_with_no_hlds_type_defn),
> +
> + % Check whether that type is a type for which there is a user-defined
> + % equality predicate, or which is existentially typed.
> + module_info_get_type_table(ModuleInfo, TypeTable),
> + map.lookup(TypeTable, TypeCtor, TypeDefn),
> + hlds_data.get_type_defn_body(TypeDefn, Body),
> + special_pred_for_type_needs_typecheck(ModuleInfo, SpecialPredId, Body).
> +
> + % Updates the goal with the pred_ids of all predicates called in the
> goal.
> + % If there is an ambiguous predicate call, chooses one predicate to
> + % be the "correct" one and returns an error message describing the
> problem
> + %
> +:- pred update_goal(pred_env::in, type_constraint_map::in, hlds_goal::in,
> + hlds_goal::out, list(error_msg)::out) is det.
> +
> +update_goal(PredEnv, ConstraintMap, !Goal, Errors) :-
> + Disjunctions = map.values(ConstraintMap),
> + list.filter_map(has_one_disjunct, Disjunctions, Conjunctions),
> + list.filter_map(pred_constraint_info, Conjunctions, PredDataA),
> + list.filter_map(has_multiple_disjuncts, Disjunctions, AmbigDisjuncts),
> + list.filter_map(diagnose_ambig_pred_error(PredEnv), AmbigDisjuncts,
> + Errors),
> +
> + list.map(list.filter_map(pred_constraint_info), AmbigDisjuncts,
> + AmbigPredData),
> + PredDataB = list.filter_map(list.head, AmbigPredData),
> + list.append(PredDataA, PredDataB, PredData),
Use PredData = PredDataA ++ PredDataB instead.
> + list.foldl(apply_pred_data_to_goal, PredData, !Goal).
> +
> +
> +:- pred apply_pred_data_to_goal(pair(goal_path, pred_id)::in,
> + hlds_goal::in, hlds_goal::out) is det.
> +
> +apply_pred_data_to_goal((GoalPath0 - PredID), !Goal) :-
> + program_representation.goal_path_consable(GoalPath0, GoalPath),
> + (
> +
> goal_util.maybe_transform_goal_at_goal_path(set_goal_pred_id(PredID),
> + GoalPath, !.Goal, yes(Goal1))
> + ->
> + !:Goal = Goal1
> + ;
> + true
> + ).
> +
> +:- pred set_goal_pred_id(pred_id::in, hlds_goal::in, maybe(hlds_goal)::out)
> + is det.
> +
> +set_goal_pred_id(PredID, hlds_goal(Expression0, Info), MaybeGoal) :-
> + ( Expression0 = plain_call(_, _, _, _, _, _) ->
> + trace [compile_time(flag("print_type_constraints")), io(!IO)] (
> + Context = goal_info_get_context(Info),
> + LineNumber = string.int_to_string(term.context_line(Context)),
> + FileName = term.context_file(Context),
> + PredName = sym_name_to_string(Expression0^call_sym_name),
> + io.print(" Predicate " ++ PredName ++ " (" ++ FileName ++ ":
> " ++
> + LineNumber ++ ") has ID " ++
> + int_to_string(pred_id_to_int(PredID)) ++ "\n", !IO)
> + ),
> + NewCall = Expression0^call_pred_id := PredID,
> + MaybeGoal = yes(hlds_goal(NewCall, Info))
> + ;
> + MaybeGoal = no
> + ).
> +
> + % The following predicates extract the disjuncts from
> + % type constraints
> + %
> +:- pred has_one_disjunct(type_constraint::in, conj_type_constraint::out)
> + is semidet.
> +
> +has_one_disjunct(tconstr_disj(Cs, no), C) :-
> + list.filter(still_active, Cs, [C]).
> +has_one_disjunct(tconstr_disj(_, yes(C)), C).
> +has_one_disjunct(tconstr_conj(C), C).
> +
> +:- pred get_first_disjunct(type_constraint::in, conj_type_constraint::out)
> + is semidet.
> +
> +get_first_disjunct(tconstr_disj(Cs, no), C) :-
> + list.filter(still_active, Cs, [C|_]).
> +get_first_disjunct(tconstr_disj(_, yes(C)), C).
> +get_first_disjunct(tconstr_conj(C), C).
> +
> +:- pred has_multiple_disjuncts(type_constraint::in,
> + list(conj_type_constraint)::out) is semidet.
> +
> +has_multiple_disjuncts(tconstr_disj(Cs0, _), Cs) :-
> + list.filter(still_active, Cs0, Cs),
> + Cs = [_,_|_].
Write Cs = [_, _ | _] instead.
> +
> + % Creates the vartypes map, which is inserted into the relevant
> + % pred_info and used by the rest of the compiler
> +:- pred create_vartypes_map(prog_context::in, prog_varset::in, tvarset::in,
> + prog_var_map::in, type_domain_map::in, simple_prog_var_map::in,
> + vartypes::out, list(error_msg)::out) is det.
Add a blank line.
> +create_vartypes_map(Context, ProgVarSet, TVarSet, VarMap, DomainMap,
> + ReplacementMap, Vartypes, Errors) :-
> + bimap.ordinates(VarMap, ProgVars),
> + list.map2(find_variable_type(Context, ProgVarSet, TVarSet, VarMap,
> + DomainMap, ReplacementMap), ProgVars, Types, MaybeErrors),
> + list.filter_map(maybe.remove_maybe, MaybeErrors, Errors),
> + map.det_insert_from_corresponding_lists(map.init, ProgVars, Types,
> + Vartypes).
> +
> + % If a variable has a domain consisting of one type, gives it that type.
> + % Otherwise, assigns it to the type variable assigned to it by
s/assigns/assign/
I think you have the sense of this sentence the wrong way around: you
assign a value to a variable, not the other way around.
> + % constraint generation, after type variable replacement.
do you mean something like "after solving the constraints for the type
variable"?
> + %
> +:- pred find_variable_type(prog_context::in, prog_varset::in, tvarset::in,
> + prog_var_map::in, type_domain_map::in, simple_prog_var_map::in,
> + prog_var::in, mer_type::out, maybe(error_msg)::out) is det.
> +
> +find_variable_type(Context, ProgVarSet, TVarSet, VarMap, DomainMap,
> + ReplacementMap, Var, Type, Error) :-
> + bimap.lookup(VarMap, Var, TVar),
> + ( map.search(ReplacementMap, Var, ReplacementType) ->
> + DefaultType = tvar_to_type(ReplacementType)
> + ;
> + DefaultType = tvar_to_type(TVar)
> + ),
> + ( map.search(DomainMap, TVar, Domain) ->
> + (
> + Domain = tdomain_any,
> + Type = DefaultType,
> + Error = no
> + ;
> + Domain = tdomain_singleton(Type),
> + Error = no
> + ;
> + Domain = tdomain(Types),
> + ( set.singleton_set(Types, Type0) ->
> + Type = Type0,
> + Error = no
> + ; set.empty(Types) ->
> + Type = DefaultType,
> + Error = no % This error is handled elsewhere
> + ;
> + Type = DefaultType,
> + VarName = mercury_var_to_string(ProgVarSet, no, Var),
> + list.map(type_to_string(TVarSet), set.to_sorted_list(Types),
> + TypeStrings),
> + TypesString = string.join_list(" or ", TypeStrings),
> + Error = yes(simple_msg(Context, [always([words("Error:"),
> + words("ambiguous overloading causes type ambiguity."),
> + nl, words("Possible type assignments include:"), nl,
> + fixed(VarName), suffix(": "), words(TypesString)])]))
> + )
> + )
> + ;
> + Type = DefaultType,
> + Error = no
> + ).
> +
> +%-----------------------------------------------------------------------------%
> +%-----------------------------------------------------------------------------%
> +% Constraint solving
> +
> + % Tries to solve a constraint on the types of variables in a predicate.
> + % If a definite solution cannot be found, use labeling to guess the
> value
> + % of the variable with the smallest domain, then propagate this to
> + % all constraints. If exactly one guess provides a correct solution,
> + % return that solution. Otherwise, generate an error message explaining
> + % the problem
> + %
> +:- pred find_type_constraint_solutions(prog_context::in, prog_varset::in,
> + type_domain_map::out, type_constraint_info::in,
> + type_constraint_info::out) is det.
> +
> +find_type_constraint_solutions(Context, ProgVarSet, DomainMap,
> + !.TCInfo @ tconstr_info(_, _, !.ConstraintMap, VarConstraints,
> + TVarSet, _), !:TCInfo) :-
> + solve_constraint_labeling(TVarSet, VarConstraints, !.ConstraintMap,
> + map.init, map.init, Solutions, !:ConstraintMap, Success),
> + (
> + Solutions = []
> + ->
> + % This shouldn't happen
> + unexpected(this_file,
> + "Cannot find any possible solutions for the type constraints")
> + ;
> + % Unsatisfiability error (no solutions). If labeling was required
> + % and no labeling assignment produced a solution, pick an arbitrary
> + % labeling to report (this should be rare in real programs)
> + Success = no,
> + Solutions = [Solution|_]
> + ->
> + map.to_assoc_list(Solution, SolutionAssocList),
> + list.filter_map(has_empty_domain, SolutionAssocList, ErrorTVars),
> + list.map(diagnose_unsatisfiability_error(!.TCInfo, Context,
> + ProgVarSet), ErrorTVars, ErrorMessages),
> + list.foldl(add_message_to_spec, ErrorMessages, !TCInfo),
> + list.foldl(map.union(type_domain_union), Solutions, map.init,
> + DomainMap)
> + ;
> + % Type correct (one solution)
> + Solutions = [SingleSolution]
> + ->
> + DomainMap = SingleSolution
> + ;
> + % Ambiguity error (many solutions)
> + list.foldl(map.union(type_domain_union), Solutions, map.init,
> + DomainMap),
> + trace [compile_time(flag("type_error_diagnosis")), io(!IO)] (
> + io.write_string("\nAmbiguity error: possible variable
> types\n", !IO)
I don't understand this diagnostic message.
> + )
> + ),
> + !:TCInfo = !.TCInfo^tconstr_constraint_map := !.ConstraintMap.
> +
> +:- pred solve_constraint_labeling(tvarset::in, var_constraint_map::in,
> + type_constraint_map::in, type_domain_map::in, type_domain_map::in,
> + list(type_domain_map)::out, type_constraint_map::out, bool::out)
> + is det.
> +
> +solve_constraint_labeling(TVarSet, VarConstraints, ConstraintMap0,
> + DomainMap0, Guesses, DomainMaps, ConstraintMap, Success) :-
> + trace [compile_time(flag("type_constraint_prop")), io(!IO)] (
> + map.to_assoc_list(Guesses, GuessesAssocList),
> + list.foldl(print_guess(TVarSet), GuessesAssocList, !IO)
> + ),
> + map.union(type_domain_intersect, Guesses, DomainMap0, GuessMap),
> + solve_constraint(TVarSet, VarConstraints, ConstraintMap0,
> ConstraintMap1,
> + GuessMap, DomainMap1),
> + ( constraint_has_no_solutions(DomainMap1) ->
> + DomainMaps = [DomainMap1],
> + ConstraintMap = ConstraintMap1,
> + Success = no
> + ; constraint_has_multiple_solutions(DomainMap1, Var, Domains) ->
> + % If there are multiple solutions, pick the variable with the
> smallest
> + % domain. Try to solve the constraints for each valuation of the
> + % variable, then return any valuations which succeed. If none
> succeed,
> + % return all valuations and report a failure.
> + list.map(map.set(Guesses, Var), Domains, NewGuesses),
> + list.map3(solve_constraint_labeling(TVarSet, VarConstraints,
> + ConstraintMap1, DomainMap1), NewGuesses, DomainMapLists,
> + ConstraintMaps, _),
> + list.condense(DomainMapLists, DomainMaps0),
> + list.filter(constraint_has_no_solutions, DomainMaps0, FailSolutions,
> + SuccessSolutions),
> + list.foldl(map.union(merge_type_constraints), ConstraintMaps,
> + ConstraintMap0, ConstraintMap),
> + (
> + SuccessSolutions = [],
> + DomainMaps = FailSolutions,
> + Success = no
> + ;
> + SuccessSolutions = [_|_],
> + DomainMaps = SuccessSolutions,
> + Success = yes
> + )
> + ;
> + DomainMaps = [DomainMap1],
> + ConstraintMap = ConstraintMap1,
> + Success = yes
> + ).
> +
> + % Restricts the domain of each variable in the constraint based on all
> + % information in the constraint. If the domain map is unchanged in
> one pass
> + % (i.e., a fixed point), or the constraint is found to be unsatisfiable,
> + % the domain map is returned. Otherwise, solve_constraint is called
> + % again with the new domain information.
> + %
> +:- pred solve_constraint(tvarset::in, var_constraint_map::in,
> + type_constraint_map::in, type_constraint_map::out,
> + type_domain_map::in, type_domain_map::out) is det.
> +
> +solve_constraint(TVarSet, VarConstraints, ConstraintMap0, ConstraintMap,
> + DomainMap0, DomainMap) :-
> + ConstraintIDs = map.keys(ConstraintMap0),
> + list.foldl2(propagate(TVarSet, VarConstraints), ConstraintIDs,
> + ConstraintMap0, ConstraintMap1, DomainMap0, DomainMap1),
> + (
> + % Failure
> + constraint_has_no_solutions(DomainMap1)
> + ->
> + DomainMap = DomainMap1,
> + ConstraintMap = ConstraintMap1
> + ;
> + % Fixed-point reached (success)
> + DomainMap1 = DomainMap0,
> + ConstraintMap1 = ConstraintMap0
> + ->
> + DomainMap = DomainMap1,
> + ConstraintMap = ConstraintMap1
> + ;
> + % Need to iterate again
> + solve_constraint(TVarSet, VarConstraints, ConstraintMap1,
> + ConstraintMap, DomainMap1, DomainMap)
> + ).
> +
> + % Given the information from a single constraint, updates the domains of
> + % each variable in the constraint. If any variable is reduced to a
> + % singleton domain, propagates this information to all other constraints
> + % involving that variable.
> + %
> +:- pred propagate(tvarset::in, var_constraint_map::in,
> type_constraint_id::in,
> + type_constraint_map::in, type_constraint_map::out, type_domain_map::in,
> + type_domain_map::out) is det.
> +
> +propagate(TVarSet, VarConstraints, ConstraintID, !ConstraintMap,
> !DomainMap) :-
> + % Update the domain of each variable in the constraint
> + map.lookup(!.ConstraintMap, ConstraintID, Constraint0),
> + find_domain(Constraint0, Constraint, !.DomainMap, NewDomainMap),
> + % Print the changes to the domain map
> + trace [compile_time(flag("type_constraint_prop")), io(!IO)] (
> + io.format("Constraint %d:\n", [i(ConstraintID)], !IO),
> + map.to_sorted_assoc_list(NewDomainMap, NewDomainAssocList),
> + list.foldl(print_domain_map_change(TVarSet, !.DomainMap),
> + NewDomainAssocList, !IO),
> + print_constraint_change(TVarSet, Constraint0, Constraint, !IO)
> + ),
> + !:DomainMap = NewDomainMap,
> + svmap.det_update(ConstraintID, Constraint, !ConstraintMap),
> + % If any variable domains have been reduced to singleton domains
> + % by this constraint, update the status of those variables and
> + % propagate to other constriants involving them.
> + tvars_in_constraint(Constraint, TVars),
> + list.filter(has_singleton_domain(!.DomainMap), TVars, SingletonVars),
> + list.foldl(update_singleton_domain, SingletonVars, !DomainMap),
> + list.filter_map(map.search(VarConstraints), SingletonVars,
> + PropConstraints0),
> + PropConstraints = list.remove_dups(list.condense(PropConstraints0)),
> + list.foldl2(propagate(TVarSet, VarConstraints), PropConstraints,
> + !ConstraintMap, !DomainMap).
> +
> + % Given a variable and a list of constraints on that variable,
> enumerates
> + % the possible types of that variable. Also, marks as unsatisfiable any
> + % constraints that are unsatisfiable, given the current variable
> domains.
> + %
> +:- pred create_domain(type_domain_map::in, conj_type_constraint::in,
> + conj_type_constraint::out, type_domain_map::out) is det.
> +
> +create_domain(!.DomainMap, !Constraint, !:DomainMap) :-
> + conj_find_domain(!Constraint, !DomainMap).
> +
> + % Finds the domain of a type variable, given its existing domain and a
> + % set of constraints on its type. Will mark as unsatisfiable any
> constraints
> + % that are unsatisfiable.
> + %
> +:- pred find_domain(type_constraint::in, type_constraint::out,
> + type_domain_map::in, type_domain_map::out) is det.
> +
> + % A conjunction of constraints requires each constraint to be met
> + %
> +find_domain(tconstr_conj(Constraints), tconstr_conj(NewConstraints),
> + !DomainMap) :-
> + conj_find_domain(Constraints, NewConstraints, !DomainMap).
> +
> +find_domain(tconstr_disj(C, yes(Constraints)),
> + tconstr_disj(C, yes(NewConstraints)), !DomainMap) :-
> + conj_find_domain(Constraints, NewConstraints, !DomainMap).
> +
> + % A disjunction of constraints means the domain is restricted to
> + % the union of all type assignments in the each active disjunct.
> + %
> +find_domain(tconstr_disj(!.Constraints, no),
> + tconstr_disj(!:Constraints, SingleConstraint), !DomainMap) :-
> + % Generates a distinct domain map for each disjunct unifies each
> + % domain in the domain map to get an overall domain for the disjunct,
> + % then takes the intersect of this with the existing domain map.
> + list.filter(still_active, !Constraints, InactiveConstraints),
> + list.map2(create_domain(!.DomainMap), !Constraints, Domains),
> + (
> + Domains = [],
> + DisjDomain = map.init
> + ;
> + Domains = [HeadDomain | TailDomains],
> + list.foldl(map.intersect(type_domain_union), TailDomains,
> HeadDomain,
> + DisjDomain)
> + ),
> + map.union(type_domain_intersect, DisjDomain, !DomainMap),
> + % If there is only one active disjunct remaining, turn the constraint
> + % into a conjunction constraint
> + list.filter(still_active, !.Constraints, Active),
> + ( Active = [SingleConstraint0] ->
> + SingleConstraint = yes(SingleConstraint0)
> + ;
> + SingleConstraint = no
> + ),
> + list.append(InactiveConstraints, !Constraints).
> +
> + % Finds the domain of a conjunction of constraints. If the
> conjunction is
> + % unsatisfiable, marks it as unsatisfiable. If the domain of any type
> + % variable in the conjunct is reduced, propagate this information
> back to
> + % conj_find_domain.
> + %
> +:- pred conj_find_domain(conj_type_constraint::in,
> conj_type_constraint::out,
> + type_domain_map::in, type_domain_map::out) is det.
> +
> +conj_find_domain(Conj @ ctconstr(_, tconstr_unsatisfiable, _, _, _),
> + Conj, !DomainMap).
> +
> +conj_find_domain(!.Conj @ ctconstr(Constraints, tconstr_active, Context,
> + GoalPath, PredID), !:Conj, DomainMap0, DomainMap) :-
> + list.foldl(simple_find_domain, Constraints, DomainMap0, DomainMap1),
> + ( constraint_is_satisfiable(DomainMap1, Constraints) ->
> + map.to_assoc_list(DomainMap1, AssocDomain1),
> + ( list.all_true(domain_map_unchanged(DomainMap0), AssocDomain1) ->
> + DomainMap = DomainMap1
> + ;
> + conj_find_domain(!Conj, DomainMap1, DomainMap)
> + )
> + ;
> + DomainMap = DomainMap1,
> + !:Conj = ctconstr(Constraints, tconstr_unsatisfiable, Context,
> + GoalPath, PredID)
> + ).
> +
> + % Finds the domain of a type variable based on the information
> provided by
> + % a simple type constraint, and the existing domain of the variable.
> + %
> +:- pred simple_find_domain(simple_type_constraint::in, type_domain_map::in,
> + type_domain_map::out) is det.
> +
> +simple_find_domain(stconstr(TVar, Type), !DomainMap) :-
> + (
> + % If two type variables are unified, the domain of each is
> restricted
> + % to the insersection of each domain.
s/each domain/the domains/
> + Type = type_variable(TVar2, _),
> + ( map.search(!.DomainMap, TVar2, Domain20) ->
> + Domain2 = Domain20
> + ;
> + Domain2 = tdomain_any,
> + svmap.det_insert(TVar2, Domain2, !DomainMap)
> + ),
> + ( map.search(!.DomainMap, TVar, Domain) ->
> + type_domain_intersect(Domain, Domain2, NewDomain),
> + svmap.det_update(TVar, NewDomain, !DomainMap),
> + svmap.det_update(TVar2, NewDomain, !DomainMap)
> + ;
> + svmap.det_insert(TVar, Domain2, !DomainMap)
> + )
> + ;
> + % If the type is a compound type (e.g., maybe(T)), try to determine
> + % the types of its arguments
> + Type = defined_type(Name, Args, Kind),
> + list.map(find_type_of_tvar(!.DomainMap), Args, ArgTypes),
> + restrict_domain(TVar, defined_type(Name, ArgTypes, Kind),
> !DomainMap)
> + ;
> + Type = builtin_type(_),
> + restrict_domain(TVar, Type, !DomainMap)
> + ;
> + Type = tuple_type(Args, Kind),
> + list.map(find_type_of_tvar(!.DomainMap), Args, ArgTypes),
> + restrict_domain(TVar, tuple_type(ArgTypes, Kind), !DomainMap)
> + ;
> + Type = higher_order_type(Args, Return, Purity, Lambda),
> + list.map(find_type_of_tvar(!.DomainMap), Args, ArgTypes),
> + map_maybe(find_type_of_tvar(!.DomainMap), Return, ReturnType),
> + restrict_domain(TVar, higher_order_type(ArgTypes, ReturnType,
> + Purity, Lambda), !DomainMap)
> + ;
> + Type = apply_n_type(Return, Args, Kind),
> + list.map(find_type_of_tvar(!.DomainMap), Args, ArgTypes),
> + restrict_domain(TVar, apply_n_type(Return, ArgTypes, Kind),
> + !DomainMap)
> + ;
> + Type = kinded_type(Type0, _),
> + simple_find_domain(stconstr(TVar, Type0), !DomainMap)
> + ).
> +
> + % Finds each variable which is unified to the target variable. Replaces
> + % these variables with the replacement variable in the prog_var<->tvar
> + % map. Recursively calls on each of these variables. In this way,
> replaces
> + % assignments of program variables to equivalent type variables with
> + % assignments of program variables to the same type variable.
> + %
> +:- pred unify_equal_tvars(type_constraint_info::in, set(tvar)::in,
> + tvar::in, tvar::in, simple_prog_var_map::in, simple_prog_var_map::out,
> + type_domain_map::in, type_domain_map::out) is det.
> +
> +unify_equal_tvars(TCInfo @ tconstr_info(VarMap, _, ConstraintMap,
> + VarConstraints, _, _), Replaced, Replacement, Target,
> + !ReplacementMap, !DomainMap) :-
> + map.det_insert(map.init, Target, Replacement, Renaming),
> + (
> + map.search(!.DomainMap, Target, tdomain_any),
> + map.search(VarConstraints, Target, ConstraintIDs)
> + ->
> + % Find all variables unified with the target variable
> + map.apply_to_list(ConstraintIDs, ConstraintMap, Constraints),
> + list.filter_map(to_simple_constraints, Constraints,
> + SimpleConstraints0),
> + list.condense(SimpleConstraints0, SimpleConstraints),
> + list.filter_map(find_unified_var(Target), SimpleConstraints,
> + UnifiedVars0),
> + list.filter(set.contains(Replaced), UnifiedVars0, _, UnifiedVars),
> + % Update the unified variables, and unify with anything unified with
> + % those variables
> + list.foldl(update_replacement_map(VarMap, Replacement), UnifiedVars,
> + !ReplacementMap),
> + svset.insert_list(UnifiedVars, Replaced, Replaced1),
> + list.foldl2(unify_equal_tvars(TCInfo, Replaced1, Replacement),
> + UnifiedVars, !ReplacementMap, !DomainMap)
> + ;
> + map.search(!.DomainMap, Target, tdomain_singleton(Type0))
> + ->
> + apply_variable_renaming_to_type(Renaming, Type0, Type),
> + svmap.det_update(Target, tdomain_singleton(Type), !DomainMap)
> + ;
> + map.search(!.DomainMap, Target, tdomain(Types0))
> + ->
> + set.map(apply_variable_renaming_to_type(Renaming), Types0, Types),
> + svmap.det_update(Target, tdomain(Types), !DomainMap)
> + ;
> + % This case should never be reached, but is included in case there
> + % are no constraints on the type of a variable
> + true
> + ).
It would be better to throw an exception here instead. It will make
finding bugs involving this situation much easier to identify.
> +
> +/*
> +:- pred get_tvar_domain(type_domain_map::in, tvar::in, list(mer_type)::out)
> + is semidet.
> +get_tvar_domain(DomainMap, TVar, Types) :-
> + map.search(DomainMap, TVar, Domain),
> + (
> + Domain = tdomain(Types0),
> + set.to_sorted_list(Types0, Types)
> + ;
> + Domain = tdomain_singleton(SingletonType),
> + Types = [SingletonType]
> + ).
> +*/
> +
> +%-----------------------------------------------------------------------------%
> +% Constraint solving utility predicates
> +
> + % Returns the type variable that is unified with Target in the
> constraint.
> + % Fails if no such variable exists.
> + %
> +:- pred find_unified_var(tvar::in, simple_type_constraint::in,
> + tvar::out) is semidet.
> +
> +find_unified_var(Target, stconstr(LHS, type_variable(RHS, _)), Unified) :-
> + (
> + LHS = Target,
> + RHS = Unified0
> + ->
> + Unified = Unified0
> + ;
> + LHS = Unified0,
> + RHS = Target
> + ->
> + Unified = Unified0
> + ;
> + fail
> + ).
> +
Did you mean to include this commented out predicate?
> +/* I'm stupid, this is the same as apply_variable_renaming_to_type
> + % Replaces all occurrences of Target with Replacement in
> + % the type on the RHS of the constraint, then returns that
> + % as ResultType. Fails if the type on the RHS is a variable
> + % or builtin type.
> + %
> +:- pred replace_in_compound_type(tvar::in, tvar::in, mer_type::in,
> + mer_type::out) is semidet.
> +
> +replace_in_compound_type(Replacement, Target, Type,
> + ResultType) :-
> + TargetType = tvar_to_type(Target),
> + ReplacementType = tvar_to_type(Replacement),
> + (
> + Type = defined_type(Name, Args0, Kind),
> + list.replace_all(Args0, TargetType, ReplacementType, Args),
> + ResultType = defined_type(Name, Args, Kind)
> + ;
> + Type = tuple_type(Args0, Kind),
> + list.replace_all(Args0, TargetType, ReplacementType, Args),
> + ResultType = tuple_type(Args, Kind)
> + ;
> + Type = higher_order_type(Args0, MaybeReturn0, Purity, Lambda),
> + list.replace_all(Args0, TargetType, ReplacementType, Args),
> + ( MaybeReturn0 = yes(TargetType) ->
> + MaybeReturn = yes(ReplacementType)
> + ;
> + MaybeReturn = MaybeReturn0
> + ),
> + ResultType = higher_order_type(Args, MaybeReturn, Purity, Lambda),
> + ;
> + Type = apply_n_type(Tvar, Args0, Kind),
> + list.replace_all(Args0, TargetType, ReplacementType, Args),
> + ResultType = apply_n_type(TVar, Args, Kind)
> + ;
> + Type = kinded_type(Arg0, Kind),
> + ( Arg0 = TargetType ->
> + Arg = ReplacementType
> + ;
> + Arg = Arg0
> + ),
> + ResultType = kinded_type(Arg, Kind)
> + ).
> +*/
> +
> +:- pred to_simple_constraints(type_constraint::in,
> + list(simple_type_constraint)::out) is semidet.
> +
> +to_simple_constraints(tconstr_conj(Conj), Conj^tconstr_simples).
> +to_simple_constraints(tconstr_disj(_, yes(Conj)), Conj^tconstr_simples).
> +
> +:- pred update_replacement_map(prog_var_map::in, tvar::in, tvar::in,
> + simple_prog_var_map::in, simple_prog_var_map::out) is det.
> +
> +update_replacement_map(VarMap, Replacement, OldVar, !ReplacementMap) :-
> + ( bimap.reverse_search(VarMap, ProgVar, OldVar) ->
> + svmap.set(ProgVar, Replacement, !ReplacementMap)
> + ;
> + true
> + ).
> +
> +:- pred find_type_domain(type_domain_map::in, tvar::in, type_domain::out)
> + is det.
> +
> +find_type_domain(DomainMap, TVar, Domain) :-
> + ( map.search(DomainMap, TVar, Domain0) ->
> + Domain = Domain0
> + ;
> + Domain = tdomain_any
> + ).
> +
> + % If the input type is a type variable, and the type of that type
> variable
> + % is known, return the known type. Otherwise, return the type variable.
> + %
> +:- pred find_type_of_tvar(type_domain_map::in, mer_type::in, mer_type::out)
> + is det.
> +
> +find_type_of_tvar(DomainMap, !Type) :-
> + (
> + !.Type = type_variable(TVar, _),
> + map.search(DomainMap, TVar, tdomain_singleton(KnownType))
> + ->
> + !:Type = KnownType
> + ;
> + true
> + ).
> +
> + % Restrict the domain of the given type variable to the given type.
> If the
> + % variable is not currently in the domain map, insert it. If the
> variable
> + % is restricted to a singleton domain, note this.
> + %
> +:- pred restrict_domain(tvar::in, mer_type::in, type_domain_map::in,
> + type_domain_map::out) is det.
> +
> +restrict_domain(TVar, Type, !DomainMap) :-
> + ( map.search(!.DomainMap, TVar, CurrDomain0) ->
> + CurrDomain = CurrDomain0
> + ;
> + CurrDomain = tdomain_any
> + ),
> + type_domain_intersect(CurrDomain, tdomain(set.make_singleton_set(Type)),
> + NewDomain),
> + svmap.set(TVar, NewDomain, !DomainMap).
> +
> +:- pred type_domain_intersect(type_domain::in, type_domain::in,
> + type_domain::out) is det.
> +
> +type_domain_intersect(tdomain_any, D, D).
> +
> +type_domain_intersect(SD @ tdomain_singleton(_), tdomain_any, SD).
> +
> +type_domain_intersect(tdomain_singleton(Type1), tdomain_singleton(Type2),
> + Intersect) :-
> + ( unify_types(Type1, Type2, Type) ->
> + Intersect = tdomain_singleton(Type)
> + ;
> + Intersect = tdomain(set.init)
> + ).
Add a blank line.
> +type_domain_intersect(tdomain_singleton(Type), tdomain(Types),
> + Intersect) :-
> + set.filter_map(unify_types(Type), Types, UnifiedTypes),
> + ( set.singleton_set(UnifiedTypes, SingletonType) ->
> + Intersect = tdomain_singleton(SingletonType)
> + ;
> + Intersect = tdomain(UnifiedTypes)
> + ).
> +
> +type_domain_intersect(D @ tdomain(_), tdomain_any, D).
> +
> +type_domain_intersect(D @ tdomain(_), SD @ tdomain_singleton(_),
> Intersect) :-
> + type_domain_intersect(SD, D, Intersect).
> +
> +type_domain_intersect(tdomain(Set1), tdomain(Set2), tdomain(Intersect)) :-
> + set.to_sorted_list(Set1, List1),
> + set.to_sorted_list(Set2, List2),
> + td_list_intersect(List2, List1, List_Intersect),
> + set.sorted_list_to_set(List_Intersect, Intersect).
> +
> + % Very similar to set.intersect, but will unify equal functors with
> + % different type variable parameters - e.g.,m
> + % yes(type_variable(V_1)) = yes(type_variable(V_2))
> + %
> +:- pred td_list_intersect(list(mer_type)::in, list(mer_type)::in,
> + list(mer_type)::out) is det.
> +
> +td_list_intersect([], _, []).
> +td_list_intersect([_|_], [], []).
> +td_list_intersect([A|As], [B|Bs], Cs) :-
> + ( unify_types(A, B, Type) ->
> + td_list_intersect(As, Bs, Cs0),
> + Cs = [Type|Cs0]
> + ;
> + compare(R, A, B),
> + (
> + R = (<),
> + td_list_intersect(As, [B|Bs], Cs)
> + ;
> + R = (=),
> + td_list_intersect(As, Bs, Cs0),
> + Cs = [A|Cs0]
> + ;
> + R = (>),
> + td_list_intersect([A|As], Bs, Cs)
> + )
> + ).
> +
> + % Takes two types as input, and returns the most definite type that
> + % can be created from the two. When two type variables are merged,
> + % the first argument takes priority.
What do you mean by "most definite type"? Usually type unification
proceeds by finding the mgu (Most General Unifier).
> + %
> +:- pred unify_types(mer_type::in, mer_type::in, mer_type::out) is semidet.
> +
> +unify_types(A, B, Type) :-
> + % If two compound types are unified, unify each of their
> + % arguments: e.g., yes(type_variable(V_1)) = yes(type_variable(V_2)),
> + % and unify any type variable with anything.
> + % Fail if types cannot be unified.
> + ( B = type_variable(_, _) ->
> + Type = A
> + ; A = type_variable(_, _) ->
> + Type = B
> + ;
> + (
> + A = defined_type(Name, ArgsA, Kind),
> + B = defined_type(Name, ArgsB, Kind),
> + list.map_corresponding(unify_types, ArgsA, ArgsB, Args),
> + Type = defined_type(Name, Args, Kind)
> + ;
> + A = builtin_type(T),
> + B = builtin_type(T),
> + Type = A
> + ;
> + A = tuple_type(ArgsA, Kind),
> + B = tuple_type(ArgsB, Kind),
> + list.map_corresponding(unify_types, ArgsA, ArgsB, Args),
> + Type = tuple_type(Args, Kind)
> + ;
> + A = higher_order_type(ArgsA, ResultA, Purity, Lambda),
> + B = higher_order_type(ArgsB, ResultB, Purity, Lambda),
> + list.map_corresponding(unify_types, ArgsA, ArgsB, Args),
> + (
> + ResultA = yes(ResultA1),
> + ResultB = yes(ResultB1),
> + unify_types(ResultA1, ResultB1, Result1),
> + Result = yes(Result1)
> + ;
> + ResultA = no,
> + ResultB = no,
> + Result = no
> + ),
> + Type = higher_order_type(Args, Result, Purity, Lambda)
> + ;
> + A = apply_n_type(TVarA, ArgsA, Kind),
> + B = apply_n_type(_, ArgsB, Kind),
> + list.map_corresponding(unify_types, ArgsA, ArgsB, Args),
> + Type = apply_n_type(TVarA, Args, Kind)
> + ;
> + A = kinded_type(TypeA, Kind),
> + B = kinded_type(TypeB, Kind),
> + unify_types(TypeA, TypeB, Type)
> + )
> + ).
> +
> + % Like set.union, but treads tdomain_any as the universal domain
> + %
> +:- pred type_domain_union(type_domain::in, type_domain::in,
> + type_domain::out) is det.
> +
> +type_domain_union(tdomain_any, _, tdomain_any).
> +
> +type_domain_union(tdomain_singleton(_), tdomain_any, tdomain_any).
> +
> +type_domain_union(tdomain_singleton(Type1), tdomain_singleton(Type2),
> Union) :-
> + ( Type1 = Type2 ->
> + Union = tdomain_singleton(Type1)
> + ;
> + Union = tdomain(set.from_list([Type1, Type2]))
> + ).
> +
> +type_domain_union(SD @ tdomain_singleton(Type), tdomain(Types), Union) :-
> + ( set.empty(Types) ->
> + Union = SD
> + ;
> + Union = tdomain(set.insert(Types, Type))
> + ).
> +
> +type_domain_union(tdomain(_), tdomain_any, tdomain_any).
> +
> +type_domain_union(D @ tdomain(_), SD @ tdomain_singleton(_), Union) :-
> + type_domain_union(SD, D, Union).
> +
> +type_domain_union(tdomain(Set1), tdomain(Set2), tdomain(Union)) :-
> + set.union(Set2, Set1, Union).
> +
> +:- pred still_active(conj_type_constraint::in) is semidet.
> +
> +still_active(ctconstr(_, tconstr_active, _, _, _)).
> +
> + % Makes a conjunction of constraints unsatisfiable the conjunction is
> + % unsatisfiable, i.e. the domain of any type variable in any of
> + % the conjuncts is empty
> + %
> +:- pred constraint_is_satisfiable(type_domain_map::in,
> + list(simple_type_constraint)::in) is semidet.
> +
> +constraint_is_satisfiable(DomainMap, SimpleConstraints) :-
> + list.map(tvars_in_simple_constraint, SimpleConstraints, TVars0),
> + list.condense(TVars0, TVars),
> + list.filter_map(map.search(DomainMap), TVars, Domains),
> + list.all_true(non_empty_domain, Domains).
> +
> +:- pred non_empty_domain(type_domain::in) is semidet.
> +
> +non_empty_domain(tdomain_any).
> +non_empty_domain(tdomain_singleton(_)).
> +non_empty_domain(tdomain(D)) :-
> + set.non_empty(D).
> +
> + % Checks whether the given variable domain is compatible with the
> + % domain map
> + %
> +:- pred domain_map_unchanged(type_domain_map::in, pair(tvar,
> type_domain)::in)
> + is semidet.
> +
> +domain_map_unchanged(DomainMap, (TVar - Domain)) :-
> + map.search(DomainMap, TVar, Domain0),
> + equal_domain(Domain0, Domain).
> +
> +:- pred equal_domain(type_domain::in, type_domain::in) is semidet.
> +
> +equal_domain(tdomain_any, tdomain_any).
> +equal_domain(tdomain_singleton(A), tdomain_singleton(B)) :-
> + unify_types(A, B, _).
> +equal_domain(tdomain(A), tdomain(B)) :-
> + (
> + set.count(A, C),
> + set.count(B, C)
Why not write set.count(A) = set.count(B) instead?
> + ->
> + list.map_corresponding(unify_types, set.to_sorted_list(A),
> + set.to_sorted_list(B), _)
> + ;
> + fail
> + ).
> +
> +:- pred has_empty_domain(pair(tvar, type_domain)::in, tvar::out) is semidet.
> +
> +has_empty_domain((TVar - tdomain(Domain)), TVar) :-
> + set.empty(Domain).
> +
> + % Checks if a variable which was not previously known to have a
> singleton
> + % domain has a singleton domain
> + %
> +:- pred has_singleton_domain(type_domain_map::in, tvar::in) is semidet.
> +
> +has_singleton_domain(DomainMap, TVar) :-
> + map.search(DomainMap, TVar, tdomain(Domain)),
> + set.singleton_set(Domain, _).
It's more efficient to write set.count(Domain) = 1 here since
set.singleton_set/2 will allocate some memory.
> +
> +:- pred is_singleton_domain(type_domain::in, mer_type::out) is semidet.
> +
> +is_singleton_domain(tdomain_singleton(Type), Type).
> +is_singleton_domain(tdomain(Domain), Type) :-
> + set.singleton_set(Domain, Type).
> +
> +:- pred update_singleton_domain(tvar::in, type_domain_map::in,
> + type_domain_map::out) is det.
> +
> +update_singleton_domain(TVar, !DomainMap) :-
> + (
> + map.search(!.DomainMap, TVar, tdomain(Domain)),
> + set.singleton_set(Domain, Type)
> + ->
> + svmap.set(TVar, tdomain_singleton(Type), !DomainMap)
> + ;
> + true
> + ).
> +
> + % Returns all type variables present in a type constraint
> + %
> +:- pred tvars_in_constraint(type_constraint::in, list(tvar)::out) is det.
> +
> +tvars_in_constraint(tconstr_conj(ctconstr(Constraints, _, _, _, _)),
> TVars) :-
> + list.map(tvars_in_simple_constraint, Constraints, TVarLists),
> + list.condense(TVarLists, TVars).
> +tvars_in_constraint(tconstr_disj(Disjuncts0, _), TVars) :-
> + list.map(get_constraints_from_conj, Disjuncts0, Disjuncts),
> + list.condense(Disjuncts, Constraints),
> + list.map(tvars_in_simple_constraint, Constraints, TVarLists),
> + list.condense(TVarLists, TVars).
> +
> +:- pred tvars_in_simple_constraint(simple_type_constraint::in,
> + list(tvar)::out) is det.
> +
> +tvars_in_simple_constraint(stconstr(TVar, Type), [TVar|TVars]) :-
> + prog_type.type_vars(Type, TVars).
> +
> +:- pred constraint_has_no_solutions(type_domain_map::in) is semidet.
> +
> +constraint_has_no_solutions(DomainMap) :-
> + list.member(tdomain(set.init), map.values(DomainMap)).
> +
> +:- pred constraint_has_one_solution(type_domain_map::in) is semidet.
> +
> +constraint_has_one_solution(DomainMap) :-
> + list.map(is_singleton_domain, map.values(DomainMap), _).
> +
> +:- pred constraint_has_multiple_solutions(type_domain_map::in, tvar::out,
> + list(type_domain)::out) is semidet.
> +
> +constraint_has_multiple_solutions(DomainMap, Var, Domains) :-
> + map.to_assoc_list(DomainMap, DomainMap1),
> + list.filter(has_ambiguous_domain, DomainMap1, AmbigDomains0),
> + list.sort(domain_size_compare, AmbigDomains0, [(Var - Domain0)|_]),
> + Domain0 = tdomain(Domain1),
> + Domains = set.to_sorted_list(set.map(to_singleton_type_domain,
> Domain1)).
> +
> +:- pred has_ambiguous_domain(pair(tvar, type_domain)::in) is semidet.
> +
> +has_ambiguous_domain((_ - tdomain(Dom))) :-
> + set.count(Dom, Size),
> + Size > 1.
> +
> + % Compares the domain size of two domains. The variables corresponding
> + % to the domains are ignored. Should only be used to compare
> + % domains that are not singleton or undefined.
> + %
> +:- pred domain_size_compare(pair(tvar, type_domain)::in,
> + pair(tvar, type_domain)::in, comparison_result::out) is det.
> +
> +domain_size_compare((_ - A), (_ - B), Result) :-
> + (
> + A = tdomain(D1),
> + B = tdomain(D2)
> + ->
> + list.length(set.to_sorted_list(D1), L1),
> + list.length(set.to_sorted_list(D2), L2),
> + compare(Result, L1, L2)
> + ;
> + Result = (=)
> + ).
> +
> +:- func to_singleton_type_domain(mer_type) = type_domain.
> +
> +to_singleton_type_domain(Type) = tdomain_singleton(Type).
> +
> + % If the program variable is not in the vartypes map, assigns it to
> + % a fresh type variable and inserts it into the map.
> + %
> +:- pred add_unused_prog_var(type_constraint_info::in, prog_var::in,
> + vartypes::in, vartypes::out) is det.
> +
> +add_unused_prog_var(TCInfo, Var, !Vartypes) :-
> + ( map.contains(!.Vartypes, Var) ->
> + true
> + ;
> + bimap.lookup(TCInfo^tconstr_var_map, Var, TVar),
> + svmap.det_insert(Var, tvar_to_type(TVar), !Vartypes)
> + ).
> +
> +:- pred get_constraints_from_conj(conj_type_constraint::in,
> + list(simple_type_constraint)::out) is det.
> +
> +get_constraints_from_conj(Conj, Conj^tconstr_simples).
> +
> + % Merges two type constraints, which should be equal except possibly
> + % for the activity of their disjuncts, into one type constraint. The
> + % disjuncts of the result constraint are active if the respective
> + % disjuncts of either input constraint are active.
> + %
> +:- pred merge_type_constraints(type_constraint::in, type_constraint::in,
> + type_constraint::out) is det.
> +
> +merge_type_constraints(A, B, Result) :-
> + (
> + A = tconstr_conj(ConjA),
> + ConjsA = [ConjA]
> + ;
> + A = tconstr_disj(ConjsA, _)
> + ),
> + (
> + B = tconstr_conj(ConjB),
> + ConjsB = [ConjB]
> + ;
> + B = tconstr_disj(ConjsB, _)
> + ),
> + list.map_corresponding(merge_type_constraints2, ConjsA, ConjsB, Conjs),
> + ( Conjs = [SingletonConj] ->
> + Result = tconstr_conj(SingletonConj)
> + ; list.filter(still_active, Conjs, [SingletonConj]) ->
> + Result = tconstr_disj(Conjs, yes(SingletonConj))
> + ;
> + Result = tconstr_disj(Conjs, no)
> + ).
> +
> +:- pred merge_type_constraints2(conj_type_constraint::in,
> + conj_type_constraint::in, conj_type_constraint::out) is det.
> +
> +merge_type_constraints2(A, B, Result) :-
> + (
> + A^tconstr_activity = tconstr_unsatisfiable,
> + B^tconstr_activity = tconstr_unsatisfiable
> + ->
> + Result = A
> + ;
> + Result = A^tconstr_activity := tconstr_active
> + ).
> +
> +%-----------------------------------------------------------------------------%
> +% Error diagnosis
> +%
> + % If the list of type constraints contains more than one predicate call
> + % constraint, return an error message describing the ambiguity and one
> + % of the predicate call constraints (chosen arbitrarily). Otherwise,
> fail.
> + %
> +:- pred diagnose_ambig_pred_error(pred_env::in,
> list(conj_type_constraint)::in,
> + error_msg::out) is semidet.
> +
> +diagnose_ambig_pred_error(PredEnv, Conjunctions, Error) :-
> + Conjunctions = [_,_|_],
> + conj_constraint_get_context(head(Conjunctions), Context),
> + list.filter_map(pred_constraint_info, Conjunctions, AmbigPredData),
> + list.map(ambig_pred_error_message(PredEnv), AmbigPredData, Errors),
> + Errors = [_|_],
> + Error = simple_msg(Context, [always([words("Ambiguous predicate"),
> + words("call. Possible predicates include:"),
> + nl_indent_delta(2)]) | Errors]).
> +
> +:- pred ambig_pred_error_message(pred_env::in, pair(goal_path, pred_id)::in,
> + error_msg_component::out) is det.
> +
> +ambig_pred_error_message(PredEnv, (_ - ID), Error) :-
> + predicate_table_get_preds(PredEnv, Preds),
> + map.lookup(Preds, ID, PredInfo),
> + Name = pred_info_name(PredInfo),
> + Arity = pred_info_orig_arity(PredInfo),
> + pred_info_get_context(PredInfo, Context),
> + LineNumber = term.context_line(Context),
> + FileName = term.context_file(Context),
> + Error = always([fixed(Name), suffix("/"), suffix(int_to_string(Arity)),
> + prefix("("), words(FileName), suffix(": "), int_fixed(LineNumber),
> + suffix(")")]).
> +
> +:- pred pred_constraint_info(conj_type_constraint::in,
> + pair(goal_path, pred_id)::out) is semidet.
> +
> +pred_constraint_info(ctconstr(_, _, _, yes(Path), yes(ID)), (Path - ID)).
> +
> + % Creates an error message describing why a variable is unsatisfiable.
> + % This is done by finding all minimal unsatisfiable subsets of the
> + % constraints on the type of the variable, then finding the constraints
> + % that are present in all of these subsets.
> + %
> +:- pred diagnose_unsatisfiability_error(type_constraint_info::in,
> + prog_context::in, prog_varset::in, tvar::in,
> + error_msg::out) is det.
> +
> +diagnose_unsatisfiability_error(TCInfo @ tconstr_info(VarMap, _,
> ConstraintMap,
> + VarConstraints, TVarSet, _), Context, ProgVarSet, TypeVar, Error) :-
> + map.lookup(VarConstraints, TypeVar, ConstraintIDs),
> + svset.insert_list(ConstraintIDs, set.init, ConstraintSet),
> + min_unsat_constraints(TCInfo, set.init, ConstraintSet, [], MinUnsats),
> + list.map(error_from_one_min_set(ConstraintMap), MinUnsats,
> MinUnsatPieces),
> + list.zip_single([suffix(") or"), nl, prefix("(")], MinUnsatPieces,
> + ErrorLocations0),
> + list.condense(ErrorLocations0, ErrorLocations),
> + ( bimap.reverse_search(VarMap, ProgVar, TypeVar) ->
> + VarName = mercury_var_to_string(ProgVarSet, no, ProgVar),
> + VarKind = "program"
> + ;
> + VarName = mercury_var_to_string(TVarSet, yes, TypeVar),
> + VarKind = "type"
> + ),
> + Error = simple_msg(Context,
> + [always([words("Conflicting type assignments for the"),
> + fixed(VarKind), words("variable"), words(VarName), nl,
> + words("The problem is most likely due to one of the following"),
> + words("sets of goals"), nl, prefix("(")] ++ ErrorLocations ++
> + [suffix(")"), nl])]).
> +
> +:- pred error_from_one_min_set(type_constraint_map::in,
> + set(type_constraint_id)::in, list(format_component)::out) is det.
> +
> +error_from_one_min_set(ConstraintMap, MinUnsatSet, ErrorLocations) :-
> + set.to_sorted_list(MinUnsatSet, MinUnsatList),
> + map.apply_to_list(MinUnsatList, ConstraintMap, Constraints),
> + list.filter_map(get_first_disjunct, Constraints, ConjConstraints),
> + list.map(conj_constraint_get_context, ConjConstraints, Contexts),
> + list.map(context_to_string, Contexts, ContextStrings),
> + ErrorLocations = list_to_pieces(ContextStrings).
> +
> + % Uses the min_unsat1 algorithm to find all minimal unsatisfiable
> subsets
> + % of the constraints on the types of variables.
Can you supply a reference to that algorithm (e.g., a URL)?
> + %
> +:- pred min_unsat_constraints(type_constraint_info::in,
> + type_constraint_set::in, type_constraint_set::in,
> + list(type_constraint_set)::in, list(type_constraint_set)::out) is det.
> +
> +min_unsat_constraints(tconstr_info(VarMap, _, ConstraintMap0,
> + VarConstraints0, TVarSet, _), D, P, !MinUnsats) :-
> + set.union(P, D, Union),
> + trace [compile_time(flag("type_error_diagnosis")), io(!IO)] (
> + list.map(string.int_to_string, set.to_sorted_list(Union), IDs),
> + io.print("\n Constraints " ++ string.join_list(", ", IDs) ++
> "\n",
> + !IO)
> + ),
> + % Remove all constraints which are not part of the subset currently
> + % being examined.
> + list.foldl(map.det_transform_value(list.filter(set.contains(Union))),
> + map.keys(VarConstraints0), VarConstraints0, VarConstraints),
> + map.select(ConstraintMap0, Union, ConstraintMap),
> + Constraint = tconstr_info(VarMap, counter.init(0), ConstraintMap,
> + VarConstraints, TVarSet, []),
> +
> + solve_constraint_labeling(TVarSet, VarConstraints, ConstraintMap,
> + map.init, map.init, _, _, Success),
> + (
> + Success = no,
> + set.fold3(next_min_unsat(Constraint), P, D, NewD, P, _,
> + !MinUnsats),
> + ( list.all_false(set.superset(NewD), !.MinUnsats) ->
> + !:MinUnsats = [NewD|!.MinUnsats]
> + ;
> + true
> + )
> + ;
> + Success = yes
> + ).
> +
> +:- pred next_min_unsat(type_constraint_info::in, type_constraint_id::in,
> + type_constraint_set::in, type_constraint_set::out,
> + type_constraint_set::in, type_constraint_set::out,
> + list(type_constraint_set)::in, list(type_constraint_set)::out) is det.
> +
> +next_min_unsat(Constraint, C, !D, !P, !MinUnsats) :-
> + svset.delete(C, !P),
> + min_unsat_constraints(Constraint, !.D, !.P, !MinUnsats),
> + svset.insert(C, !D).
> +
> +:- pred add_message_to_spec(error_msg::in, type_constraint_info::in,
> + type_constraint_info::out) is det.
> +
> +add_message_to_spec(ErrMsg, !TCInfo) :-
> + Spec = error_spec(severity_error, phase_type_check, [ErrMsg]),
> + !:TCInfo = !.TCInfo^tconstr_error_spec :=
> + [Spec | !.TCInfo^tconstr_error_spec ].
> +
> +:- pred context_to_string(prog_context::in, string::out) is det.
> +
> +context_to_string(Context, String) :-
> + LineNumber = string.int_to_string(term.context_line(Context)),
> + FileName = term.context_file(Context),
> + String = "[" ++ FileName ++ ": " ++ LineNumber ++ "]".
> +
> +:- pred conj_constraint_get_context(conj_type_constraint::in,
> + prog_context::out) is det.
> +
> +conj_constraint_get_context(Constraint, Constraint^tconstr_context).
> +
> +%-----------------------------------------------------------------------------%
> +%-----------------------------------------------------------------------------%
> +% Constraint generation
> +
> + % Turns a goal expression to a constraint on the types of variable
> + % appearing within that goal, then updates all relevant maps with the
> + % information in the new constraint
> + %
> +:- pred goal_to_constraint(tconstr_environment::in, hlds_goal::in,
> + type_constraint_info::in, type_constraint_info::out) is det.
> +
> + % Transforms a unification constraint into an assignment of types to the
> + % variables being unified
> + %
> +goal_to_constraint(Environment @ tconstr_environment(_, _, FuncEnv,
> PredEnv),
> + hlds_goal(unify(L, RHS, _, _, _), Info), !TCInfo) :-
> + Context = goal_info_get_context(Info),
> + get_var_type(L, LTVar, !TCInfo),
> + (
> + RHS = rhs_var(R),
> + get_var_type(R, RTVar, !TCInfo),
> + Constraints = [ctconstr([stconstr(LTVar, tvar_to_type(RTVar))],
> + tconstr_active, Context, no, no)],
> + RelevantTVars = [LTVar, RTVar]
> + ;
> + RHS = rhs_functor(Cons_ID, _, Args),
> + (
> + builtin_atomic_type(Cons_ID, Name)
> + ->
> + TypeCtor = type_ctor(unqualified(Name), 0),
> + construct_type(TypeCtor, [], ConsType),
> + Constraints = [ctconstr([stconstr(LTVar, ConsType)],
> + tconstr_active, Context, no, no)],
> + RelevantTVars = [LTVar]
> +
> + ;
> + Cons_ID = cons(Name, Arity),
> + Arity = list.length(Args)
> + ->
> + list.map_foldl(get_var_type, Args, ArgTypeVars, !TCInfo),
> + % If it is a type constructor, create a disjunction
> + % constraint with each possible type of the constructor
> + (
> + map.search(FuncEnv, Cons_ID, Cons_Defns)
> + ->
> + list.map_foldl(functor_unif_constraint(LTVar, ArgTypeVars,
> + Info), Cons_Defns, TypeConstraints, !TCInfo)
> + ;
> + TypeConstraints = []
> + ),
> + % If it is a predicate constructor, create a disjunction
> + % constraint for each predicate it could refer to.
> + (
> + predicate_table_search_sym(PredEnv,
> + may_be_partially_qualified, Name, PredIDs)
> + ->
> + predicate_table_get_preds(PredEnv, Preds),
> + list.filter_map_foldl(ho_pred_unif_constraint(Preds, Info,
> + LTVar, ArgTypeVars), PredIDs, PredConstraints, !TCInfo)
> + ;
> + PredConstraints = []
> + ),
> + Constraints = TypeConstraints ++ PredConstraints,
> + RelevantTVars = [LTVar|ArgTypeVars]
> + ;
> + ErrMsg = simple_msg(Context, [always([words("The given type"),
> + words("is not supported by constraint-based type"),
> + words("checking.")])]),
> + add_message_to_spec(ErrMsg, !TCInfo),
> + RelevantTVars = [],
> + Constraints = []
What about this commented out section below?
> + /*
> + Cons_ID = pred_const(_,_),
> + error("This constructor ID is not supported yet")
> + ;
> + Cons_ID = type_ctor_info_const(_,_,_),
> + error("This constructor ID is not supported yet")
> + ;
> + Cons_ID = base_typeclass_info_const(_,_,_,_),
> + error("This constructor ID is not supported yet")
> + ;
> + Cons_ID = type_info_cell_constructor(_),
> + error("This constructor ID is not supported yet")
> + ;
> + Cons_ID = typeclass_info_cell_constructor,
> + error("This constructor ID is not supported yet")
> + ;
> + Cons_ID = tabling_info_const(_),
> + error("This constructor ID is not supported yet")
> + ;
> + Cons_ID = deep_profiling_proc_layout(_),
> + error("This constructor ID is not supported yet")
> + ;
> + Cons_ID = table_io_decl(_),
> + error("This constructor ID is not supported yet")
> + */
> + )
> + ;
> + RHS = rhs_lambda_goal(Purity, _, PredOrFunc, EvalMethod, _, Args, _,
> + _, Goal),
> + list.map_foldl(get_var_type, Args, ArgTVars, !TCInfo),
> + ArgTypes = list.map(tvar_to_type, ArgTVars),
> + construct_higher_order_type(Purity, PredOrFunc, EvalMethod,
> ArgTypes,
> + LambdaType),
> + Constraints = [ctconstr([stconstr(LTVar, LambdaType)],
> + tconstr_active, Context, no, no)],
> + RelevantTVars = [LTVar|ArgTVars],
> + goal_to_constraint(Environment, Goal, !TCInfo)
> + ),
> + add_type_constraint(Constraints, RelevantTVars, !TCInfo).
> +
> + % Transforms a predicate call to variable assignments of the
> variables used
> + % in the predicate call
> + %
> +goal_to_constraint(tconstr_environment(_, _, _, PredEnv),
> + hlds_goal(plain_call(_, _, Args, _, _, Name), Info), !TCInfo) :-
> + % "may_be_partially_qualified" might be replaced by "is_fully_qualified"
> + % (I don't know what either of them mean)
The "I don't know..." comment should be prefixed with XXX as a red flag
to other developers.
> + ( predicate_table_search_pred_sym(PredEnv, may_be_partially_qualified,
> + Name, PredIDs0) ->
> + PredIDs1 = PredIDs0
> + ;
> + PredIDs1 = []
> + ),
> + predicate_table_get_preds(PredEnv, Preds),
> + list.filter(pred_has_arity(Preds, list.length(Args)), PredIDs1,
> + PredIDs),
> + list.map_foldl(get_var_type, Args, ArgTVars, !TCInfo),
> + list.map2_foldl(pred_call_constraint(Preds, Info, ArgTVars), PredIDs,
> + Constraints, PredTVars, !TCInfo),
> + list.condense([ArgTVars | PredTVars], TVars),
> + add_type_constraint(Constraints, TVars, !TCInfo).
> +
> + % call_foreign_proc goals are implemented in a similar manner to
> predicate
> + % calls. The rest are implemented by calling expression_to_constraint on
> + % each goal within the goal
> +goal_to_constraint(Environment, hlds_goal(conj(_, Goals), _), !TCInfo) :-
> + list.foldl(goal_to_constraint(Environment), Goals, !TCInfo).
> +
> +goal_to_constraint(Environment, hlds_goal(disj(Goals), _), !TCInfo) :-
> + list.foldl(goal_to_constraint(Environment), Goals, !TCInfo).
> +
> +goal_to_constraint(Environment, hlds_goal(negation(Goal), _), !TCInfo) :-
> + goal_to_constraint(Environment, Goal, !TCInfo).
> +
> +goal_to_constraint(Environment, hlds_goal(
> + call_foreign_proc(_,PredID,_,ForeignArgs,_,_,_), Info), !TCInfo) :-
> + Context = goal_info_get_context(Info),
> + ArgVars = list.map(foreign_arg_var, ForeignArgs),
> + ArgTypes0 = list.map(foreign_arg_type, ForeignArgs),
> + predicate_table_get_preds(Environment^pred_env, Preds),
> + ( map.search(Preds, PredID, PredInfo) ->
> + pred_info_get_typevarset(PredInfo, PredTVarSet),
> + prog_data.tvarset_merge_renaming(!.TCInfo^tconstr_tvarset,
> + PredTVarSet, NewTVarSet, TVarRenaming),
> + !:TCInfo = !.TCInfo^tconstr_tvarset := NewTVarSet,
> + prog_type_subst.apply_variable_renaming_to_type_list(TVarRenaming,
> + ArgTypes0, ArgTypes),
> + list.foldl_corresponding(variable_assignment_constraint(Context),
> + ArgVars, ArgTypes, !TCInfo)
> + ;
> + ErrMsg = simple_msg(Context, [always([words("Cannot find the"),
> + words("predicate with ID"), int_fixed(pred_id_to_int(PredID)),
> + words("referenced by the call_foreign_proc")])]),
> + add_message_to_spec(ErrMsg, !TCInfo)
> + ).
> +
> +goal_to_constraint(Environment, hlds_goal(scope(_,Goal), _), !TCInfo) :-
> + goal_to_constraint(Environment, Goal, !TCInfo).
> +
> +goal_to_constraint(Environment, hlds_goal(if_then_else(_,Cond,Then,Else),
> _),
> + !TCInfo) :-
> + goal_to_constraint(Environment, Cond, !TCInfo),
> + goal_to_constraint(Environment, Then, !TCInfo),
> + goal_to_constraint(Environment, Else, !TCInfo).
> +
> +goal_to_constraint(Environment,
> + hlds_goal(generic_call(Details, Vars, _, _), Info), !TCInfo) :-
> + Context = goal_info_get_context(Info),
> + list.map_foldl(get_var_type, Vars, ArgTVars, !TCInfo),
> + ArgTypes = list.map(tvar_to_type, ArgTVars),
> + (
> + Details = higher_order(CallVar, Purity, Kind, _),
> + (
> + Kind = pf_predicate,
> + HOType = higher_order_type(ArgTypes, no, Purity, lambda_normal)
> + ;
> + Kind = pf_function,
> + svvarset.new_var(FunctionTVar, !.TCInfo^tconstr_tvarset,
> + NewTVarSet),
> + !:TCInfo = !.TCInfo^tconstr_tvarset := NewTVarSet,
> + HOType = apply_n_type(FunctionTVar, ArgTypes, kind_star)
> + ),
> + variable_assignment_constraint(Context, CallVar, HOType, !TCInfo)
> + ;
> + % Class methods are handled by looking up the method number in the
> + % class' method list.
> + Details = class_method(_, MethodNum, ClassID, _),
> + ClassID = class_id(Name, Arity),
> + ( map.search(Environment^class_env, ClassID, ClassDefn) ->
> + ( list.index0(ClassDefn^class_hlds_interface, MethodNum,
> Method) ->
> + Method = hlds_class_proc(PredID, _),
> + predicate_table_get_preds(Environment^pred_env, Preds),
> + ( pred_has_arity(Preds, list.length(Vars), PredID) ->
> + pred_call_constraint(Preds, Info, ArgTVars, PredID,
> + Constraint, PredTVars, !TCInfo),
> + list.append(ArgTVars, PredTVars, TVars),
> + add_type_constraint([Constraint], TVars, !TCInfo)
> + ;
> + ErrMsg = simple_msg(Context,
> [always([words("Incorrect"),
> + words("number of arguments provided to method"),
> + int_fixed(MethodNum), words("of typeclass"),
> + sym_name_and_arity(Name / Arity)])]),
> + add_message_to_spec(ErrMsg, !TCInfo)
> + )
> + ;
> + ErrMsg = simple_msg(Context, [always([words("The
> typeclass"),
> + sym_name_and_arity(Name / Arity),
> + words("does not have the given method.")])]),
> + add_message_to_spec(ErrMsg, !TCInfo)
> + )
> + ;
> + ErrMsg = simple_msg(Context, [always([words("The typeclass"),
> + sym_name_and_arity(Name / Arity), words("is
> undefined.")])]),
> + add_message_to_spec(ErrMsg, !TCInfo)
> + )
> + ;
> + Details = event_call(Name),
> + ( event_arg_types(Environment^event_env, Name, _ArgTypes0) ->
> + % XXX Need to get a tvarset for the event types
> + %tvarset_merge_renaming(!.TVarSet, EventTVarSet, !:TVarSet,
> + % Renaming),
> + %apply_variable_renaming_to_type_list(ArgTypes0, ArgTypes),
> + %foldl_corresponding(variable_assignment_constraint(Context),
> + % Vars, ArgTypes, !TCInfo)
> + ErrMsg = simple_msg(Context, [always([words("Event calls are"),
> + words("not supported by constraint-based
> typechecking.")])]),
> + add_message_to_spec(ErrMsg, !TCInfo)
> + ;
> + ErrMsg = simple_msg(Context, [always([words("There is not
> event"),
> + words("named"), words(Name)])]),
> + add_message_to_spec(ErrMsg, !TCInfo)
> + )
> + ;
> + % Casts do not contain any type information
> + Details = cast(_)
> + ).
> +
> +goal_to_constraint(Environment, hlds_goal(switch(_,_,Cases), _), !TCInfo) :-
> + list.map(get_case_goal, Cases, Goals),
> + list.foldl(goal_to_constraint(Environment), Goals, !TCInfo).
> +
> +goal_to_constraint(Env, hlds_goal(shorthand(bi_implication(GoalA,
> GoalB)), _),
> + !TCInfo) :-
> + goal_to_constraint(Env, GoalA, !TCInfo),
> + goal_to_constraint(Env, GoalB, !TCInfo).
> +
> + % Atomic goals are handled by forcing their inner arguments
> + % to be of type stm_atomic_type, their outer arguments to be
> + % of type stm_atomic_type or io_state_type, depending on the type
> + % of atomic goal. The transaction goals are handled by recursive
> + % calls to goal_to_constraint.
> +goal_to_constraint(Environment, hlds_goal(shorthand(atomic_goal(GoalType,
> Outer,
> + Inner, _, Main, Alternatives)), Info), !TCInfo) :-
> + Context = goal_info_get_context(Info),
> + % Inner variable handling (simple assignment)
> + Inner = atomic_interface_vars(InnerInitVar, InnerFinalVar),
> + variable_assignment_constraint(Context, InnerInitVar, stm_atomic_type,
> + !TCInfo),
> + variable_assignment_constraint(Context, InnerFinalVar, stm_atomic_type,
> + !TCInfo),
> + % Create possible constraints on outer variables
> + Outer = atomic_interface_vars(OuterInitVar, OuterFinalVar),
> + get_var_type(OuterInitVar, OuterInit, !TCInfo),
> + get_var_type(OuterFinalVar, OuterFinal, !TCInfo),
> + InitStmConstraint = ctconstr([stconstr(OuterInit, stm_atomic_type)],
> + tconstr_active, Context, no, no),
> + InitIOConstraint = ctconstr([stconstr(OuterInit, io_state_type)],
> + tconstr_active, Context, no, no),
> + FinalStmConstraint = ctconstr([stconstr(OuterFinal, stm_atomic_type)],
> + tconstr_active, Context, no, no),
> + FinalIOConstraint = ctconstr([stconstr(OuterFinal, io_state_type)],
> + tconstr_active, Context, no, no),
> + % Determine which constraints should be applied to outer variables
> + (
> + GoalType = unknown_atomic_goal_type,
> + add_type_constraint([InitStmConstraint, InitIOConstraint],
> + [OuterInit], !TCInfo),
> + add_type_constraint([FinalStmConstraint, FinalIOConstraint],
> + [OuterFinal], !TCInfo)
> + ;
> + GoalType = top_level_atomic_goal,
> + add_type_constraint([InitIOConstraint], [OuterInit], !TCInfo),
> + add_type_constraint([FinalIOConstraint], [OuterFinal], !TCInfo)
> + ;
> + GoalType = nested_atomic_goal,
> + add_type_constraint([InitStmConstraint], [OuterInit], !TCInfo),
> + add_type_constraint([FinalStmConstraint], [OuterFinal], !TCInfo)
> + ),
> + % Recursively evaluate transaction goals
> + list.foldl(goal_to_constraint(Environment), [Main|Alternatives],
> !TCInfo).
> +
> + % Creates a constraint from the information stored in a predicate
> + % definition. This may only be called if the number of arguments given
> + % is equal to the arity of the predicate
> + %
> +:- pred pred_call_constraint(pred_table::in, hlds_goal_info::in,
> + list(tvar)::in, pred_id::in, conj_type_constraint::out, list(tvar)::out,
> + type_constraint_info::in, type_constraint_info::out) is det.
> +
> +pred_call_constraint(PredTable, Info, ArgTVars, PredID,
> ctconstr(Constraints,
> + tconstr_active, Context, yes(GoalPath), yes(PredID)), TVars,
> + !TCInfo) :-
> + Context = goal_info_get_context(Info),
> + GoalPath = goal_info_get_goal_path(Info),
> + ( map.search(PredTable, PredID, PredInfo) ->
> + pred_info_get_arg_types(PredInfo, PredArgTypes0),
> + pred_info_get_typevarset(PredInfo, PredTVarSet),
> + prog_data.tvarset_merge_renaming(!.TCInfo^tconstr_tvarset,
> + PredTVarSet, NewTVarSet, TVarRenaming),
> + !:TCInfo = !.TCInfo^tconstr_tvarset := NewTVarSet,
> + prog_type_subst.apply_variable_renaming_to_type_list(TVarRenaming,
> + PredArgTypes0, PredArgTypes),
> + Constraints = list.map_corresponding(create_stconstr, ArgTVars,
> + PredArgTypes),
> + prog_type.type_vars_list(PredArgTypes, TVars)
> + ;
> + ErrMsg = simple_msg(Context, [always([words("The predicate with
> ID"),
> + int_fixed(pred_id_to_int(PredID)),
> + words("has not been defined.")])]),
> + add_message_to_spec(ErrMsg, !TCInfo),
> + TVars = [],
> + Constraints = []
> + ).
> +
> + % Creates a constraint from a higher-order unification, e.g,
> + % :- pred add(int, int, int), X = add(Y) ->
> + % X :: pred(int, int), Y :: int.
> + % Fails if the number of arguments supplied to the predicate is greater
> + % than its arity.
> +:- pred ho_pred_unif_constraint(pred_table::in, hlds_goal_info::in,
> tvar::in,
> + list(tvar)::in, pred_id::in, conj_type_constraint::out,
> + type_constraint_info::in, type_constraint_info::out) is semidet.
> +
> +ho_pred_unif_constraint(PredTable, Info, LHSTVar, ArgTVars, PredID,
> + ctconstr(Constraints, tconstr_active, Context, yes(GoalPath),
> + yes(PredID)), !TCInfo) :-
> + Context = goal_info_get_context(Info),
> + GoalPath = goal_info_get_goal_path(Info),
> + ( map.search(PredTable, PredID, PredInfo) ->
> + pred_info_get_arg_types(PredInfo, PredArgTypes0),
> + pred_info_get_typevarset(PredInfo, PredTVarSet),
> + pred_info_get_purity(PredInfo, Purity),
> + prog_data.tvarset_merge_renaming(!.TCInfo^tconstr_tvarset,
> PredTVarSet,
> + NewTVarSet, TVarRenaming),
> + !:TCInfo = !.TCInfo^tconstr_tvarset := NewTVarSet,
> + prog_type_subst.apply_variable_renaming_to_type_list(TVarRenaming,
> + PredArgTypes0, PredArgTypes),
> + list.split_list(list.length(ArgTVars), PredArgTypes, HOArgTypes,
> + LambdaTypes),
> + ArgConstraints = list.map_corresponding(create_stconstr, ArgTVars,
> + HOArgTypes),
> + LHSConstraint = stconstr(LHSTVar, higher_order_type(LambdaTypes, no,
> + Purity, lambda_normal)),
> + Constraints = [LHSConstraint|ArgConstraints]
> + ;
> + ErrMsg = simple_msg(Context, [always([words("The predicate with
> ID"),
> + int_fixed(pred_id_to_int(PredID)),
> + words("has not been defined.")])]),
> + add_message_to_spec(ErrMsg, !TCInfo),
> + Constraints = []
> + ).
> +
> + % Creates a constraint from the assignment of a type to a program
> variable
> + %
> +:- pred variable_assignment_constraint(prog_context::in, prog_var::in,
> + mer_type::in, type_constraint_info::in, type_constraint_info::out) is
> det.
> +
> +variable_assignment_constraint(Context, Var, Type, !TCInfo) :-
> + prog_type.type_vars(Type, TypeVariables),
> + get_var_type(Var, TVar, !TCInfo),
> + Constraint = ctconstr([stconstr(TVar, Type)], tconstr_active, Context,
> + no, no),
> + add_type_constraint([Constraint], [TVar|TypeVariables], !TCInfo).
> +
> + % Create a conjunction of type constraints from a functor unification
> goal.
> + % The LHS variable is constrained to be of the result type, and each RHS
> + % variable is constrained to be of the appropriate argument type.
> + %
> +:- pred functor_unif_constraint(tvar::in, list(tvar)::in,
> hlds_goal_info::in,
> + hlds_cons_defn::in, conj_type_constraint::out, type_constraint_info::in,
> + type_constraint_info::out) is det.
> +
> +functor_unif_constraint(LTVar, ArgTVars, Info, hlds_cons_defn(TypeCtor,
> + FunctorTVarSet, TypeParams0, _, _, _, FuncArgs, _), Constraints,
> + !TCInfo) :-
> + Context = goal_info_get_context(Info),
> + GoalPath = goal_info_get_goal_path(Info),
> + % Find the types of each argument and the result type, given a renaming
> + % of type variables
> + list.map(get_ctor_arg_type, FuncArgs, FuncArgTypes0),
> + prog_data.tvarset_merge_renaming(!.TCInfo^tconstr_tvarset,
> FunctorTVarSet,
> + NewTVarSet, TVarRenaming),
> + !:TCInfo = !.TCInfo^tconstr_tvarset := NewTVarSet,
> + prog_type_subst.apply_variable_renaming_to_tvar_list(TVarRenaming,
> + TypeParams0, TypeParams),
> + prog_type_subst.apply_variable_renaming_to_type_list(TVarRenaming,
> + FuncArgTypes0, FuncArgTypes),
> + Params = list.map(tvar_to_type, TypeParams),
> + prog_type.construct_type(TypeCtor, Params, ResultType),
> + LHS_Constraint = stconstr(LTVar, ResultType),
> + RHS_Constraints = list.map_corresponding(create_stconstr,
> + ArgTVars, FuncArgTypes),
> + Constraints = ctconstr([LHS_Constraint|RHS_Constraints],
> + tconstr_active, Context, yes(GoalPath), no).
> +
> +%-----------------------------------------------------------------------------%
> +% Constraint generation utility predicates
> +
> +:- pred pred_has_arity(pred_table::in, int::in, pred_id::in) is semidet.
> +
> +pred_has_arity(Preds, Arity, PredID) :-
> + map.lookup(Preds, PredID, Pred),
> + pred_info_get_arg_types(Pred, PredArgTypes),
> + list.length(PredArgTypes) = Arity.
> +
> + % Converts any builtin atomic type to a string representing that type.
> + %
> +:- pred builtin_atomic_type(cons_id::in, string::out) is semidet.
> +
> +builtin_atomic_type(int_const(_), "int").
> +builtin_atomic_type(float_const(_), "float").
> +builtin_atomic_type(string_const(_), "string").
> +builtin_atomic_type(cons(unqualified(String), 0), "character") :-
> + string.char_to_string(_, String).
> +builtin_atomic_type(implementation_defined_const(Name), Type) :-
> + (
> + ( Name = "file"
> + ; Name = "module"
> + ; Name = "pred"
> + ; Name = "grade"
> + ),
> + Type = "string"
> + ;
> + Name = "line",
> + Type = "int"
> + ).
> +
> + % Creates a new ID for a type constraint, then maps each of the given
> type
> + % variables to that constraint
> + %
> +:- pred add_type_constraint(list(conj_type_constraint)::in, list(tvar)::in,
> + type_constraint_info::in, type_constraint_info::out) is det.
> +
> +add_type_constraint(Constraints, TVars, tconstr_info(VarMap,
> + !.ConstraintCounter, !.ConstraintMap, !.VarConstraints, TVarSet,
> + Errors), tconstr_info(VarMap, !:ConstraintCounter, !:ConstraintMap,
> + !:VarConstraints, TVarSet, Errors)) :-
> + (
> + Constraints = [],
> + error("Invalid constraints")
> + ;
> + Constraints = [SingleConstraint],
> + Constraint = tconstr_conj(SingleConstraint)
> + ;
> + Constraints = [_,_|_],
> + Constraint = tconstr_disj(Constraints, no)
> + ),
> + counter.allocate(ID, !ConstraintCounter),
> + svmap.det_insert(ID, Constraint, !ConstraintMap),
> + list.foldl(map_var_to_constraint(ID), TVars, !VarConstraints).
> +
> +:- pred map_var_to_constraint(type_constraint_id::in, tvar::in,
> + var_constraint_map::in, var_constraint_map::out) is det.
> +
> +map_var_to_constraint(ID, TVar, !VarConstraints) :-
> + ( map.search(!.VarConstraints, TVar, OldIDs) ->
> + ( list.contains(OldIDs, ID) ->
> + true
> + ;
> + svmap.det_update(TVar, [ID|OldIDs], !VarConstraints)
> + )
> + ;
> + svmap.det_insert(TVar, [ID], !VarConstraints)
> + ).
> +
> + % If a program variable corresponds to a particular type variable,
> return
> + % that type variable. Otherwise, create a new type variable and map the
> + % program variable to it, then return that type variable
> + %
> +:- pred get_var_type(prog_var::in, tvar::out,
> + type_constraint_info::in, type_constraint_info::out) is det.
> +
> +get_var_type(Var, TVar, tconstr_info(!.VarMap, CC, CM, VC, !.TVarSet, Errs),
> + tconstr_info(!:VarMap, CC, CM, VC, !:TVarSet, Errs)) :-
> + ( bimap.search(!.VarMap, Var, TVar0) ->
> + TVar = TVar0
> + ;
> + svvarset.new_var(TVar, !TVarSet),
> + svbimap.det_insert(Var, TVar, !VarMap)
> + ).
> +
> +:- func create_stconstr(tvar, mer_type) = simple_type_constraint.
> +
> +create_stconstr(TVar, Type) = stconstr(TVar, Type).
> +
> +:- pred get_case_goal(case::in, hlds_goal::out) is det.
> +
> +get_case_goal(Case, Case^case_goal).
> +
> +:- pred get_ctor_arg_type(constructor_arg::in, mer_type::out) is det.
> +
> +get_ctor_arg_type(ctor_arg(_, Type, _), Type).
> +
> +:- func tvar_to_type(tvar) = mer_type.
> +
> +tvar_to_type(TVar) = type_variable(TVar, kind_star).
> +
> +%-----------------------------------------------------------------------------%
> +%-----------------------------------------------------------------------------%
> +% Constraint printing
> +
> +
> +:- pred print_guess(tvarset::in, pair(tvar, type_domain)::in, io::di,
> io::uo)
> + is det.
> +
> +print_guess(TVarSet, Guess, !IO) :-
> + io.print(" Guessing ", !IO),
> + print_type_domain(TVarSet, Guess, !IO).
> +
> + % If one or more conjunction constraints have become unsatisfiable,
> print
> + % out those constraints
> + %
> +:- pred print_constraint_change(tvarset::in, type_constraint::in,
> + type_constraint::in, io::di, io::uo) is det.
> +
> +print_constraint_change(TVarSet, Constraint0, Constraint1, !IO) :-
> + (
> + Constraint0 = tconstr_conj(ConjConstraints0),
> + Constraint1 = tconstr_conj(ConjConstraints1),
> + print_conj_constraint_change(TVarSet,
> + ConjConstraints0, ConjConstraints1, !IO)
> + ;
> + Constraint0 = tconstr_conj(_),
> + Constraint1 = tconstr_disj(_, _),
> + unexpected(this_file, "print_constraint_change: mismatch")
You might want to use $pred ++ ": mismatch" here instead (and below).
> + ;
> + Constraint0 = tconstr_disj(_, _),
> + Constraint1 = tconstr_conj(_),
> + unexpected(this_file, "print_constraint_change: mismatch")
> + ;
> + Constraint0 = tconstr_disj(DisjConstraints0, MaybeSingleton0),
> + Constraint1 = tconstr_disj(DisjConstraints1, MaybeSingleton1),
> + list.foldl_corresponding(print_conj_constraint_change(TVarSet),
> + DisjConstraints0, DisjConstraints1, !IO),
> + (
> + MaybeSingleton0 = no,
> + MaybeSingleton1 = yes(_)
> + ->
> + io.write_string(" Disjunction reduced to one disjunct\n", !IO)
> + ;
> + true
> + )
> + ).
> +
> +:- pred print_conj_constraint_change(tvarset::in, conj_type_constraint::in,
> + conj_type_constraint::in, io::di, io::uo) is det.
> +
> +print_conj_constraint_change(TVarSet, CCS @ ctconstr(_, ActivityA, _, _, _),
> + ctconstr(_, ActivityB, _, _, _), !IO) :-
> + (
> + ActivityA = tconstr_active,
> + ActivityB = tconstr_unsatisfiable
> + ->
> + conj_constraint_to_string(4, TVarSet, CCS, ConstraintString),
> + io.write_string(" Conjunction marked unsatisfiable:\n", !IO),
> + io.write_string(ConstraintString ++ "\n", !IO)
> + ;
> + true
> + ).
> +
> +:- pred print_domain_map_change(tvarset::in, type_domain_map::in,
> + pair(tvar, type_domain)::in, io::di, io::uo) is det.
> +
> +print_domain_map_change(TVarSet, OldDomainMap, (TVar - NewDomain), !IO) :-
> + ( map.search(OldDomainMap, TVar, OldDomain) ->
> + ( equal_domain(OldDomain, NewDomain) ->
> + true
> + ;
> + io.write_string(" Old domain:", !IO),
> + print_type_domain(TVarSet, pair(TVar, OldDomain), !IO),
> + io.write_string(" New domain:", !IO),
> + print_type_domain(TVarSet, pair(TVar, NewDomain), !IO)
> + )
> + ;
> + io.write_string(" New domain added:", !IO),
> + print_type_domain(TVarSet, pair(TVar, NewDomain), !IO)
> + ).
> +
> +:- pred print_constraint_solution(type_constraint_info::in,
> + prog_varset::in, type_domain_map::in, io::di, io::uo) is det.
> +
> +print_constraint_solution(TCInfo, ProgVarSet, DomainMap, !IO) :-
> + bimap.to_assoc_list(TCInfo^tconstr_var_map, VarMapAL),
> + list.map(pair.fst, VarMapAL, ProgVars),
> + list.map(pair.snd, VarMapAL, RelevantTVars),
> + list.map(find_type_domain(DomainMap), RelevantTVars, RelevantDomains),
> +
> + io.print("\n", !IO),
> + list.foldl_corresponding(print_prog_var_domain(TCInfo^tconstr_tvarset,
> + ProgVarSet), ProgVars, RelevantDomains, !IO).
> +
> +
> +:- pred print_prog_var_domain(tvarset::in, prog_varset::in, prog_var::in,
> + type_domain::in, io::di, io::uo) is det.
> +
> +print_prog_var_domain(TVarSet, ProgVarSet, ProgVar, Domain, !IO) :-
> + type_domain_to_string(TVarSet, Domain, DomainName),
> + VarName = mercury_var_to_string(ProgVarSet, no, ProgVar),
> + io.print(" " ++ VarName ++ " -> {" ++ DomainName ++ "}\n", !IO).
> +
> +:- pred print_type_domain(tvarset::in, pair(tvar, type_domain)::in,
> + io::di, io::uo) is det.
> +
> +print_type_domain(TVarSet, (TVar - Domain), !IO) :-
> + type_domain_to_string(TVarSet, Domain, DomainName),
> + TVarName = mercury_var_to_string(TVarSet, yes, TVar),
> + io.print(" " ++ TVarName ++ " -> {" ++ DomainName ++ "}\n", !IO).
> +
> +:- pred type_domain_to_string(tvarset::in, type_domain::in, string::out)
> + is det.
> +
> +type_domain_to_string(TVarSet, Domain, DomainName) :-
> + (
> + Domain = tdomain_any,
> + DomainName = "any"
> + ;
> + Domain = tdomain_singleton(Type),
> + type_to_string(TVarSet, Type, DomainName)
> + ;
> + Domain = tdomain(DomainSet),
> + list.map(type_to_string(TVarSet), set.to_sorted_list(DomainSet),
> + DomainTypeNames),
> + DomainName = string.join_list(", ", DomainTypeNames)
> + ).
> +
> +:- pred print_pred_constraint(type_constraint_info::in, prog_varset::in,
> + io::di, io::uo) is det.
> +
> +print_pred_constraint(tconstr_info(VarMap, _, ConstraintMap,
> + VarConstraints, TVarSet, _), ProgVarSet, !IO) :-
> + bimap.to_assoc_list(VarMap, VarMapAssocList),
> + list.foldl(print_var_constraints(ConstraintMap, VarConstraints,
> + TVarSet, ProgVarSet), VarMapAssocList, !IO).
> +
> +:- pred print_var_constraints(type_constraint_map::in,
> var_constraint_map::in,
> + tvarset::in, prog_varset::in, pair(prog_var, tvar)::in, io::di, io::uo)
> + is det.
> +
> +print_var_constraints(ConstraintMap, VarConstraints, TVarSet, ProgVarSet,
> + (Var - TVar), !IO) :-
> + VarName = mercury_var_to_string(ProgVarSet, yes, Var),
> + TVarName = mercury_var_to_string(TVarSet, yes, TVar),
> + io.print(VarName ++ " -> " ++ TVarName ++ "\n", !IO),
> + ( map.search(VarConstraints, TVar, ConstraintIDs0) ->
> + ConstraintIDs = ConstraintIDs0
> + ;
> + ConstraintIDs = []
> + ),
> + list.map(constraint_to_string(2, TVarSet, ConstraintMap), ConstraintIDs,
> + StringReps),
> + String = string.join_list(",\n", StringReps),
> + io.print(String ++ "\n", !IO).
> +
> +
> +:- pred constraint_to_string(int::in, tvarset::in, type_constraint_map::in,
> + type_constraint_id::in, string::out) is det.
> +
> +constraint_to_string(Indent, TVarSet, ConstraintMap, ConstraintID,
> String) :-
> + IDString = string.int_to_string(ConstraintID),
> + map.lookup(ConstraintMap, ConstraintID, Constraint),
> + IndentString = duplicate_char(' ', Indent),
> + (
> + Constraint = tconstr_conj(ConjConstraints),
> + conj_constraint_to_string(Indent, TVarSet, ConjConstraints,
> + ConjString)
> + ;
> + Constraint = tconstr_disj(Constraints, _),
> + list.map(conj_constraint_to_string(Indent+2, TVarSet),
> + Constraints, ConjStrings),
> + ConjString = IndentString ++ "(\n" ++ string.join_list(" OR\n",
> + ConjStrings) ++ "\n" ++ IndentString ++ ")"
> + ),
> + String = IndentString ++ "Constraint " ++ IDString ++ ":\n" ++
> + ConjString.
> +
> +:- pred conj_constraint_to_string(int::in, tvarset::in,
> + conj_type_constraint::in, string::out) is det.
> +
> +conj_constraint_to_string(Indent, TVarSet,
> + ctconstr(SimpleConstraints, _, Context, _, PredID), String) :-
> + IndentString = duplicate_char(' ', Indent),
> + LineNumber = string.int_to_string(term.context_line(Context)),
> + FileName = term.context_file(Context),
> + (
> + PredID = yes(ID),
> + PredString = " (calling predicate " ++
> + int_to_string(pred_id_to_int(ID)) ++ ")"
> + ;
> + PredID = no,
> + PredString = ""
> + ),
> + ContextString = IndentString ++ "[" ++ FileName ++ ": " ++ LineNumber
> + ++ PredString ++ "]\n",
> + ( SimpleConstraints = [SimpleConstraint] ->
> + simple_constraint_to_string(Indent, TVarSet, SimpleConstraint,
> + String0)
> + ;
> + list.map(simple_constraint_to_string(Indent + 2, TVarSet),
> + SimpleConstraints, SimpleStrings),
> + String0 = IndentString ++ "(\n" ++ string.join_list(" AND\n",
> + SimpleStrings) ++ "\n" ++ IndentString ++ ")"
> + ),
> + String = ContextString ++ String0.
> +
> +:- pred simple_constraint_to_string(int::in, tvarset::in,
> + simple_type_constraint::in, string::out) is det.
> +
> +simple_constraint_to_string(Indent, TVarSet, stconstr(TVar, Type),
> + String) :-
> + VarName = mercury_var_to_string(TVarSet, yes, TVar),
> + type_to_string(TVarSet, Type, TypeName),
> + String = duplicate_char(' ', Indent) ++ "( " ++ VarName ++ " :: "
> + ++ TypeName ++ ")".
> +
> +:- pred type_to_string(tvarset::in, mer_type::in, string::out) is det.
> +
> +type_to_string(TVarSet, Type, Name) :-
> + (
> + Type = type_variable(TVar,_),
> + Name = mercury_var_to_string(TVarSet, yes, TVar)
> + ;
> + Type = defined_type(SymName, Subtypes, _),
> + list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
> + SubtypeName = string.join_list(", ", SubtypeNames),
> + Name = sym_name_to_string(SymName) ++ "(" ++ SubtypeName ++ ")"
> + ;
> + Type = builtin_type(builtin_type_int),
> + Name = "int"
> + ;
> + Type = builtin_type(builtin_type_float),
> + Name = "float"
> + ;
> + Type = builtin_type(builtin_type_string),
> + Name = "string"
> + ;
> + Type = builtin_type(builtin_type_character),
> + Name = "character"
> + ;
> + Type = tuple_type(Subtypes, _),
> + list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
> + Name = "{" ++ string.join_list(", ", SubtypeNames) ++ "}"
> + ;
> + Type = higher_order_type(Subtypes, no, _, _),
> + list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
> + Name = "pred(" ++ string.join_list(", ", SubtypeNames) ++ ")"
> + ;
> + Type = higher_order_type(Subtypes, yes(ReturnType), _, _),
> + list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
> + type_to_string(TVarSet, ReturnType, ReturnTypeName),
> + Name = "func(" ++ string.join_list(", ", SubtypeNames) ++ ") = "
> + ++ ReturnTypeName
> + ;
> + Type = apply_n_type(_, Subtypes, _),
> + list.map(type_to_string(TVarSet), Subtypes, SubtypeNames),
> + Name = "func(" ++ string.join_list(", ", SubtypeNames) ++ ")"
> + ;
> + Type = kinded_type(Type0, _),
> + type_to_string(TVarSet, Type0, Name)
> + ).
> +
> +%-----------------------------------------------------------------------------%
> +% General purpose utility
> +
> +/*
> + % These should probably be added to the standard library
> + %
> +:- pred filter_map_foldl(pred(X, Y, A, A)::in(pred(in, out, in, out)
> + is semidet), list(X)::in, list(Y)::out, A::in, A::out) is det.
> +
> +filter_map_foldl(_, [], [], !A).
> +filter_map_foldl(P, [X|Xs], True, !A) :-
> + ( P(X, Y, !A) ->
> + filter_map_foldl(P, Xs, TrueTail, !A),
> + True = [Y|TrueTail]
> + ;
> + filter_map_foldl(P, Xs, True, !A)
> + ).
> +
> +:- pred unmaybe(maybe(T)::in, T::out) is semidet.
> +
> +unmaybe(yes(X), X).
> +
> + % zip_single(Elem, List, NewList):
> + %
> + % NewList is the result of adding Elem between each element
> + % in List. Like string.join_list
> +:- pred zip_single(T::in, list(T)::in, list(T)::out) is det.
> +
> +zip_single(_, [], []).
> +zip_single(_, [A], [A]).
> +zip_single(E, [A,A0|As], [A,E|Bs]) :-
> + zip_single(E, [A0|As], Bs).
> +*/
> +
> +% These aren't actually used by my program, but might be added to the
> +% standard library (just standard predicates with extra arguments)
> +%
> +/*
> +:- func map_corresponding4(func(A, B, C, D) = E, list(A), list(B), list(C),
> + list(D)) = list(E).
> +map_corresponding4(F, As, Bs, Cs, Ds) =
> + (
> + As = [A|As0],
> + Bs = [B|Bs0],
> + Cs = [C|Cs0],
> + Ds = [D|Ds0]
> + ->
> + [F(A,B,C,D) | map_corresponding4(F, As0, Bs0, Cs0, Ds0)]
Add spaces after the commas.
> + ;
> + As = [],
> + Bs = [],
> + Cs = [],
> + Ds = []
> + ->
> + []
> + ;
> + func_error("map_corresponding4: mismatched list arguments")
> + ).
> +
> +:- pred foldl5_corresponding(pred(A, B, C, C, D, D, E, E, F, F, G, G)::in(
> + pred(in, in, in, out, in, out, in, out, in, out, in, out) is det),
> + list(A)::in, list(B)::in, C::in, C::out, D::in, D::out, E::in, E::out,
> + F::in, F::out, G::in, G::out) is det.
> +foldl5_corresponding(_, [], [], !A, !B, !C, !D, !E).
> +foldl5_corresponding(_, [_|_], [], _,_,_,_,_,_,_,_,_,_) :-
> + error("foldl5_corresponding: Mismatched list arguments").
> +foldl5_corresponding(_, [], [_|_], _,_,_,_,_,_,_,_,_,_) :-
Ditto.
> + error("foldl5_corresponding: Mismatched list arguments").
> +foldl5_corresponding(P, [M|Ms], [N|Ns], !A, !B, !C, !D, !E) :-
> + P(M, N, !A, !B, !C, !D, !E),
> + foldl5_corresponding(P, Ms, Ns, !A, !B, !C, !D, !E).
> +
> +
> +:- pred map_corresponding_foldl4(pred(A,B,C,D,D,E,E,F,F,G,G)::in(
> + pred(in,in,out,in,out,in,out,in,out,in,out) is det), list(A)::in,
> + list(B)::in, list(C)::out, D::in, D::out, E::in, E::out, F::in, F::out,
> + G::in, G::out) is det.
> +map_corresponding_foldl4(_, [], [], [], !Acc1, !Acc2, !Acc3, !Acc4).
> +map_corresponding_foldl4(_, [], [_|_], [], !Acc1, !Acc2, !Acc3, !Acc4) :-
> + error("map_corresponding_foldl4: mismatched list arguments").
> +map_corresponding_foldl4(_, [_|_], [], [], !Acc1, !Acc2, !Acc3, !Acc4) :-
> + error("map_corresponding_foldl4: mismatched list arguments").
> +map_corresponding_foldl4(P, [A|As], [B|Bs], [C|Cs], !Acc1, !Acc2, !Acc3,
> + !Acc4) :-
> + P(A, B, C, !Acc1, !Acc2, !Acc3, !Acc4),
> + map_corresponding_foldl4(P, As, Bs, Cs, !Acc1, !Acc2, !Acc3, !Acc4).
> +
> +*/
> +
> +%-----------------------------------------------------------------------------%
> +
> +:- func this_file = string.
> +
> +this_file = "type_constraints.m".
Use $file instead.
> +
> +%-----------------------------------------------------------------------------%
> Index: library/list.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/library/list.m,v
> retrieving revision 1.178
> diff -u -r1.178 list.m
> --- library/list.m 30 Jan 2009 03:51:44 -0000 1.178
> +++ library/list.m 17 Feb 2009 03:00:20 -0000
> @@ -407,6 +407,13 @@
> :- pred list.zip(list(T)::in, list(T)::in, list(T)::out) is det.
> :- func list.zip(list(T), list(T)) = list(T).
>
> + % list.zip_single(A, ListB, List):
> + %
> + % List is the result of adding A in between each element of ListB.
> + %
> +:- pred zip_single(T::in, list(T)::in, list(T)::out) is det.
> +:- func zip_single(T, list(T)) = list(T).
This is a bad choice of name (
> +
> % list.duplicate(Count, Elem, List) is true iff List is a list
> % containing Count duplicate copies of Elem.
> %
> @@ -1231,6 +1238,14 @@
> in, out, in, out, in, out, in, out, in, out, in, out, in, out)
> is nondet.
>
> + % list.filter_map_foldl(Transformer, List, TrueList, Start, End)
> + % takes a predicate with one input argument, one output argument and an
> + % accumulator. It is called with each element of List. If a call
> succeeds,
> + % then the output is included in TrueList and the accumulator is
> updated.
> + %
> +:- pred list.filter_map_foldl(pred(X, Y, A, A)::in(pred(in, out, in, out)
> + is semidet), list(X)::in, list(Y)::out, A::in, A::out) is det.
> +
> % list.all_true(Pred, List) takes a closure with one input argument.
> % If Pred succeeds for every member of List, all_true succeeds.
> % If Pred fails for any member of List, all_true fails.
> @@ -1844,6 +1859,13 @@
>
> %-----------------------------------------------------------------------------%
>
> +list.zip_single(_, [], []).
> +list.zip_single(_, [A], [A]).
> +list.zip_single(E, [A,A0|As], [A,E|Bs]) :-
> + list.zip_single(E, [A0|As], Bs).
> +
> +%-----------------------------------------------------------------------------%
> +
> list.split_list(N, List, Start, End) :-
> ( N = 0 ->
> Start = [],
> @@ -2351,6 +2373,15 @@
> P(H0, H, !A, !B, !C, !D, !E, !F),
> list.map_foldl6(P, T0, T, !A, !B, !C, !D, !E, !F).
>
> +list.filter_map_foldl(_, [], [], !A).
> +list.filter_map_foldl(P, [X|Xs], True, !A) :-
> + ( P(X, Y, !A) ->
> + list.filter_map_foldl(P, Xs, TrueTail, !A),
> + True = [Y|TrueTail]
> + ;
> + list.filter_map_foldl(P, Xs, True, !A)
> + ).
> +
> list.foldr(_, [], !A).
> list.foldr(P, [H | T], !A) :-
> list.foldr(P, T, !A),
> @@ -2648,6 +2679,9 @@
> list.zip(Xs, Ys) = Zs :-
> list.zip(Xs, Ys, Zs).
>
> +list.zip_single(E, Xs) = Ys :-
> + list.zip_single(E, Xs, Ys).
> +
> list.duplicate(N, A) = Xs :-
> list.duplicate(N, A, Xs).
>
> Index: library/maybe.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/library/maybe.m,v
> retrieving revision 1.3
> diff -u -r1.3 maybe.m
> --- library/maybe.m 19 Apr 2006 05:17:53 -0000 1.3
> +++ library/maybe.m 17 Feb 2009 03:05:05 -0000
> @@ -84,6 +84,9 @@
> :- mode map_fold2_maybe(pred(in, out, in, out, di, uo) is det,
> in, out, in, out, di, uo) is det.
>
> + % remove_maybe(yes(X), X).
> +:- pred remove_maybe(maybe(T)::in, T::out) is semidet.
> +
> %-----------------------------------------------------------------------------%
> %-----------------------------------------------------------------------------%
>
> @@ -109,6 +112,8 @@
> map_fold2_maybe(P, yes(T0), yes(T), !A, !B) :-
> P(T0, T, !A, !B).
>
> +remove_maybe(yes(X), X).
> +
> %-----------------------------------------------------------------------------%
> :- end_module maybe.
> %-----------------------------------------------------------------------------%
> Index: library/set.m
> ===================================================================
> RCS file: /home/mercury/mercury1/repository/mercury/library/set.m,v
> retrieving revision 1.85
> diff -u -r1.85 set.m
> --- library/set.m 31 Jul 2008 06:34:41 -0000 1.85
> +++ library/set.m 5 Feb 2009 05:51:51 -0000
> @@ -254,6 +254,8 @@
> % set.filter_map(PF, S) =
> % list_to_set(list.filter_map(PF, to_sorted_list(S))).
> %
> +:- pred set.filter_map(pred(T1, T2), set(T1), set(T2)).
> +:- mode set.filter_map(in(pred(in, out) is semidet), in, out) is det.
> :- func set.filter_map(func(T1) = T2, set(T1)) = set(T2).
> :- mode set.filter_map(func(in) = out is semidet, in) = out is det.
>
> @@ -514,6 +516,11 @@
> set.filter_map(PF, S1) = S2 :-
> S2 = set.list_to_set(list.filter_map(PF, set.to_sorted_list(S1))).
>
> +set.filter_map(P, S1, S2) :-
> + set.to_sorted_list(S1, L1),
> + list.filter_map(P, L1, L2),
> + set.list_to_set(L2, S2).
> +
> set.fold(F, S, A) = B :-
> B = list.foldl(F, set.to_sorted_list(S), A).
Good work, thanks!
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to: mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions: mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------
More information about the reviews
mailing list