[Typer] residues-elab

Salut Maxim, Commentaires et questions:

In elaboration, check residues only under certain conditions.

* src/elab.ml:
In `infer_and_generalize_def`, only check for residues if the definition
contains no uninstantiated metavariables in an outer scope. Also,
restrict analysis to residues created for this particular definiton
(hence the `pre_residues` parameter).

* src/unification.ml:
Change `check_no_residues` to run on a given list instead of all current
residues, and remove residues from the list once an error has been
logged.

[ FWIW, le format que j'utilise habituellement dans Typer est celui du "GNU Coding Standard": https://www.gnu.org/prep/standards/html_node/Change-Logs.html C'était écrit à l'origine pour les fichiers ChangeLog plutot que pour les "commit message" des systèmes de contrôle de révision, donc il y a un petit peu d'ajustement à faire. ]

+let check_def_residues (e : lexp)

•                   (t : lexp)
  

•                   (scope_level : scope_level)
  

•                   (pre_residues : Unif.residue_list) =
  

• let (_, e_free_mv) = OL.fv e in
• let (_, t_free_mv) = OL.fv t in
• let (free_mv_map, _) = OL.mv_set_union e_free_mv t_free_mv in
• (* Only check residues if no metavariables appear outside of this
• • definition's scope level. *)
• if IMap.for_all

•   (fun _ (mv_scope_level, _, _, _) ->
  

•      mv_scope_level >= scope_level)
  

•   free_mv_map
  

• then
• let this_def_residues = Unif.filter_residues pre_residues in
• Unif.raise_errors_on_residues (location e) this_def_residues

Hmm... ça correspond pas tout à fait à l'idée que j'avais. Je pensais plutôt qcch comme:

for all (_, e1, e2) in !current_residues do let (_, e1_free_mv) = OL.fv e1 in let (_, e2_free_mv) = OL.fv e2 in (* Check if the reside includes vars which can still be instantiated *) if IMap.for_all (fun _ (mv_scope_level, _, _, _) -> mv_scope_level > scope_level) free_mv_map then Unif.raise_errors_on_residues ... else ; (* All good: there's still hope to resolve this later. *)

Et ma question est: si je comprends bien tu as testé que le code passe, maintenant, mais je ne vois plus de test que `current_residues` est vide "eventually". Est-on sûr qu'on ne va pas des fois accepter du code alors qu'il reste des résidus insatisfaits?

Stefan