From e88e0b2140bdd2d194a52bc09f8338b5667d0f92 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 14 Nov 2002 18:37:54 +0000
Subject: 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
---
 interp/syntax_def.ml | 72 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 72 insertions(+)
 create mode 100644 interp/syntax_def.ml

(limited to 'interp/syntax_def.ml')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
new file mode 100644
index 0000000000..a49352da37
--- /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)
-- 
cgit v1.2.3