diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-10 14:00:57 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-10 14:00:57 +0000 |
commit | cb985b826fc82f94186b849206504d7d328b70e5 (patch) | |
tree | 9b6794a0b80e9ed5e1315ce3733b8bd4733e4b73 /library/libobject.ml | |
parent | 852b03667133e46109d62ed27c9bff54cc72f556 (diff) |
Nouvelle approche pour le discharge modulaire
- Avant : une unique méthode discharge_function qui avait accès à l'ancien
environnement mais pas de possibilité de raisonner avec les objets
du nouvel environnement en cours de construction. C'était problématique
pour le discharge des implicites, arguments scope, etc qui étaient
finalement faits en même temps que le discharge des constantes et inductifs
mais avec pour effets de bord que les entrées dans la lib_stk arrivaient
juste avant celles des constantes et inductifs avec des problèmes pour
effacer les bonnes entrées au moment du reset
- Maintenant : deux méthodes distinctes : discharge_function qui est appliquée
pour collecter de l'ancien environnement ce qui est à garder dans la
section et rebuild_function qui reconstruit le nouvel environnement
connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche
ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant
l'extensibilité que la méthode ancienne du fichier discharge.ml ne
permettait pas)
Au passage, ajout d'un modificateur Global aux déclarations
d'implicites et d'arguments scopes pour indiquer qu'elles doivent
perdurer à la sortie de la section
Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration
aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps
discharged reste)
Au passage, nettoyage impargs.ml, suppression code mort résiduel du
traducteur etc...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libobject.ml')
-rw-r--r-- | library/libobject.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index 0a5379ee5..46cc55361 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -37,6 +37,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; + rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } let yell s = anomaly s @@ -50,6 +51,7 @@ let default_object s = { yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun (_,obj) -> Keep obj); discharge_function = (fun _ -> None); + rebuild_function = (fun x -> x); export_function = (fun _ -> None)} @@ -75,6 +77,7 @@ type dynamic_object_declaration = { dyn_subst_function : object_name * substitution * obj -> obj; dyn_classify_function : object_name * obj -> obj substitutivity; dyn_discharge_function : object_name * obj -> obj option; + dyn_rebuild_function : obj -> obj; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -112,6 +115,9 @@ let declare_object odecl = option_map infun (odecl.discharge_function (oname,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the dischargefun" + and rebuild lobj = + if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) + else anomaly "somehow we got the wrong dynamic object in the rebuildfun" and exporter lobj = if Dyn.tag lobj = na then option_map infun (odecl.export_function (outfun lobj)) @@ -125,6 +131,7 @@ let declare_object odecl = dyn_subst_function = substituter; dyn_classify_function = classifier; dyn_discharge_function = discharge; + dyn_rebuild_function = rebuild; dyn_export_function = exporter }; (infun,outfun) @@ -166,5 +173,8 @@ let classify_object ((_,lobj) as node) = let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj +let rebuild_object lobj = + apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + let export_object lobj = apply_dyn_fun None (fun d -> d.dyn_export_function lobj) lobj |