diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 18:37:54 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 18:37:54 +0000 |
commit | e88e0b2140bdd2d194a52bc09f8338b5667d0f92 (patch) | |
tree | 67ca22f77ddb98725456e5f9a0b5ad613ae28da5 /interp/syntax_def.ml | |
parent | e4efb857fa9053c41e4c030256bd17de7e24542f (diff) |
Réforme de l'interprétation des termes :
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/syntax_def.ml')
-rw-r--r-- | interp/syntax_def.ml | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml new file mode 100644 index 000000000..a49352da3 --- /dev/null +++ b/interp/syntax_def.ml @@ -0,0 +1,72 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Util +open Pp +open Names +open Libnames +open Topconstr +open Libobject +open Lib +open Nameops + +(* Syntactic definitions. *) + +let syntax_table = ref (KNmap.empty : aconstr KNmap.t) + +let _ = Summary.declare_summary + "SYNTAXCONSTANT" + { Summary.freeze_function = (fun () -> !syntax_table); + Summary.unfreeze_function = (fun ft -> syntax_table := ft); + Summary.init_function = (fun () -> syntax_table := KNmap.empty); + Summary.survive_section = false } + +let add_syntax_constant kn c = + syntax_table := KNmap.add kn c !syntax_table + +let cache_syntax_constant ((sp,kn),c) = + if Nametab.exists_cci sp then + errorlabstrm "cache_syntax_constant" + (pr_id (basename sp) ++ str " already exists"); + add_syntax_constant kn c; + Nametab.push_syntactic_definition (Nametab.Until 1) sp kn + +let load_syntax_constant i ((sp,kn),c) = + if Nametab.exists_cci sp then + errorlabstrm "cache_syntax_constant" + (pr_id (basename sp) ++ str " already exists"); + add_syntax_constant kn c; + Nametab.push_syntactic_definition (Nametab.Until i) sp kn + +let open_syntax_constant i ((sp,kn),c) = + Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn + +let subst_syntax_constant ((sp,kn),subst,c) = + subst_aconstr subst c + +let classify_syntax_constant (_,c) = Substitute c + +let (in_syntax_constant, out_syntax_constant) = + declare_object {(default_object "SYNTAXCONSTANT") with + cache_function = cache_syntax_constant; + load_function = load_syntax_constant; + open_function = open_syntax_constant; + subst_function = subst_syntax_constant; + classify_function = classify_syntax_constant; + export_function = (fun x -> Some x) } + +let declare_syntactic_definition id c = + let _ = add_leaf id (in_syntax_constant c) in () + +let rec set_loc loc _ a = + map_aconstr_with_binders_loc loc (fun id e -> (id,e)) (set_loc loc) () a + +let search_syntactic_definition loc kn = + set_loc loc () (KNmap.find kn !syntax_table) |