[m-rev.] Constraint-based typechecking

[Julien Fischer]

On Tue, 17 Feb 2009, Andrew Wesley Ebert wrote:

> 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.
>
> 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.

A few things:

(1) As others have mentioned, please don't leave mystery commented-out code
     lying around.

(2) There should be some regression tests for this added to the test
     suite, e.g. the ambig_pred thing I looked at the other day.  I am
     happy for them to be added separately.

(3) Have you checked that the compiler still bootchecks?  You will need
     to do this before committing.

(4) There are a number of compile-time trace goal conditions used in
     the type_constraints module.  The comment at the head of the module
     should say what they are and what they are useful for.

(5) The type_constraints module is actually about four or five modules.
     It should be broken up IMO, but *don't* do this now

Cheers,
Julien.

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------