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
Afficher les réponses par date
participants (1)
-
Stefan Monnier