Réaffichage des Syntactic Definition (printer constr_expr).

Affinement de la gestion des niveaux de constr.
Cablage en dur du parsing et de l'affichage des délimiteurs de scopes.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 76 insertions, 54 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c813cf71d1..68bcd12357 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -26,6 +26,7 @@ open Topconstr
 open Rawterm
 open Pattern
 open Nametab
+open Symbols
 (*i*)
 
 (* Translation from rawconstr to front constr *)
@@ -285,7 +286,7 @@ and extern_numeral scopes t (sc,n) =
 
 and extern_symbol scopes t = function
   | [] -> raise No_match
-  | (sc,ntn,pat,n as rule)::rules ->
+  | (keyrule,pat,n as rule)::rules ->
       try
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args) = match t,n with
@@ -296,16 +297,21 @@ and extern_symbol scopes t = function
 	(* Try matching ... *)
 	let subst = match_aconstr t pat in
 	(* Try availability of interpretation ... *)
-	(match Symbols.availability_of_notation (sc,ntn) scopes with
-          (* Uninterpretation is not allowed in current context *)
-	  | None -> raise No_match
-          (* Uninterpretation is allowed in current context *)
-	  | Some scopt ->
-	      let scopes = option_cons scopt scopes in
-	      let l = List.map (fun (id,c) -> (id,extern scopes c)) subst in
-	      let e = insert_delimiters (CNotation (loc,ntn,l)) scopt in
-	      if args = [] then e 
-	      else explicitize [] e (List.map (extern scopes) args))
+        let e =
+          match keyrule with
+          | NotationRule (sc,ntn) ->
+	      (match Symbols.availability_of_notation (sc,ntn) scopes with
+                  (* Uninterpretation is not allowed in current context *)
+              | None -> raise No_match
+                  (* Uninterpretation is allowed in current context *)
+	      | Some scopt ->
+	          let scopes = option_cons scopt scopes in
+	          let l = list_map_assoc (extern scopes) subst in
+	          insert_delimiters (CNotation (loc,ntn,l)) scopt)
+          | SynDefRule kn ->
+              CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
+ 	if args = [] then e 
+	else explicitize [] e (List.map (extern scopes) args)
       with
 	  No_match -> extern_symbol scopes t rules
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7236335c39..e8e42a7b4b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -274,8 +274,8 @@ let rec intern_cases_pattern scopes aliases = function
   | CPatNumeral (loc, n) ->
       ([aliases],
       Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes)
-  | CPatDelimiters (_, sc, e) ->
-      intern_cases_pattern (sc::scopes) aliases e
+  | CPatDelimiters (loc, key, e) ->
+      intern_cases_pattern (find_delimiters_scope loc key::scopes) aliases e
   | CPatAtom (loc, Some head) ->
       (match maybe_constructor head with
 	 | ConstrPat c ->
@@ -396,8 +396,8 @@ let internalise sigma env allow_soapp lvar c =
 	  (Symbols.interp_notation ntn scopes)
     | CNumeral (loc, n) ->
 	Symbols.interp_numeral loc n scopes
-    | CDelimiters (loc, sc, e) ->
-	intern (ids,impls,sc::scopes) e
+    | CDelimiters (loc, key, e) ->
+	intern (ids,impls,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, ref, args) ->
         let (f,_,args_scopes) = intern_reference env lvar ref in
 	RApp (loc, f, intern_args env args_scopes args)
diff --git a/interp/symbols.ml b/interp/symbols.ml
index 87282f0467..0d949fb283 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -40,7 +40,7 @@ open Ppextend
 (* Scope of symbols *)
 
 type level = precedence * precedence list
-type delimiters = string * string
+type delimiters = string
 type scope = {
   notations: (aconstr * (level * string)) Stringmap.t;
   delimiters: delimiters option
@@ -86,19 +86,35 @@ let check_scope sc = let _ = find_scope sc in ()
 (**********************************************************************)
 (* Delimiters *)
 
-let declare_delimiters scope dlm =
-  let sc = find_scope scope in
-  if sc.delimiters <> None && Options.is_verbose () then
-    warning ("Overwriting previous delimiters in "^scope);
-  let sc = { sc with delimiters = Some dlm } in
-  scope_map := Stringmap.add scope sc !scope_map   
+let delimiters_map = ref Stringmap.empty
 
-let find_delimiters scope = (find_scope scope).delimiters
+let declare_delimiters scope key =
+  let sc = find_scope scope in
+  if sc.delimiters <> None && Options.is_verbose () then begin
+    let old = out_some sc.delimiters in
+    Options.if_verbose 
+      warning ("Overwritting previous delimiter key "^old^" in scope "^scope)
+  end;
+  let sc = { sc with delimiters = Some key } in
+  scope_map := Stringmap.add scope sc !scope_map;
+  if Stringmap.mem key !delimiters_map then begin
+    let oldsc = Stringmap.find key !delimiters_map in
+    Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+  end;
+  delimiters_map := Stringmap.add key scope !delimiters_map
+
+let find_delimiters_scope loc key = 
+  try Stringmap.find key !delimiters_map
+  with Not_found -> 
+    user_err_loc 
+    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
 
 (* Uninterpretation tables *)
 
 type interpretation = identifier list * aconstr
-type interp_rule = scope_name * notation * interpretation * int option
+type interp_rule =
+  | NotationRule of scope_name * notation
+  | SynDefRule of kernel_name
 
 (* We define keys for rawterm and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
@@ -191,21 +207,17 @@ let rec find_without_delimiters find ntn_scope = function
 
 (* The mapping between notations and their interpretation *)
 
-let declare_interpretation ntn scope pat =
+let declare_notation_interpretation ntn scope (_,pat) prec df =
   let sc = find_scope scope in
   if Stringmap.mem ntn sc.notations && Options.is_verbose () then
     warning ("Notation "^ntn^" is already used in scope "^scope);
-  let sc = { sc with notations = Stringmap.add ntn pat sc.notations } in
+  let sc =
+    { sc with notations = Stringmap.add ntn (pat,(prec,df)) sc.notations } in
   scope_map := Stringmap.add scope sc !scope_map
 
-let declare_uninterpretation ntn scope metas c =
+let declare_uninterpretation rule (metas,c as pat) =
   let (key,n) = aconstr_key c in
-  notations_key_table :=
-    Gmapl.add key (scope,ntn,(metas,c),n) !notations_key_table
-
-let declare_notation ntn scope (metas,c) prec df onlyparse =
-  declare_interpretation ntn scope (c,(prec,df));
-  if not onlyparse then declare_uninterpretation ntn scope metas c
+  notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
 
 let rec find_interpretation f = function
   | scope::scopes ->
@@ -340,7 +352,7 @@ let find_arguments_scope r =
 
 let pr_delimiters_info = function
   | None -> str "No delimiters"
-  | Some (l,r) -> str "Delimiters are " ++ str l ++ str " and " ++ str r
+  | Some key -> str "Delimiting key is " ++ str key
 
 let rec rawconstr_of_aconstr () x =
   map_aconstr_with_binders_loc dummy_loc (fun id () -> (id,())) 
@@ -383,12 +395,13 @@ let find_notation_printing_rule ntn =
 (* Synchronisation with reset *)
 
 let freeze () =
- (!scope_map, !scope_stack, !arguments_scope,
+ (!scope_map, !scope_stack, !arguments_scope, !delimiters_map,
   !notations_key_table, !printing_rules)
 
-let unfreeze (scm,scs,asc,fkm,pprules) =
+let unfreeze (scm,scs,asc,dlm,fkm,pprules) =
   scope_map := scm;
   scope_stack := scs;
+  delimiters_map := dlm;
   arguments_scope := asc;
   notations_key_table := fkm;
   printing_rules := pprules
@@ -399,6 +412,7 @@ let init () =
   scope_stack := Stringmap.empty
   arguments_scope := Refmap.empty
 *)
+  delimiters_map := Stringmap.empty;
   notations_key_table := Gmapl.empty;
   printing_rules := Stringmap.empty
 
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 466a2bb281..24a1388039 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -28,7 +28,7 @@ open Ppextend
    interpreter and printers for integers + optional delimiters *)
 
 type level = precedence * precedence list
-type delimiters = string * string
+type delimiters = string
 type scope
 type scopes = scope_name list
 
@@ -43,7 +43,7 @@ val open_scope : scope_name -> unit
 (* Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
-val find_delimiters : scope_name -> delimiters option
+val find_delimiters_scope : loc -> delimiters -> scope_name
 
 (*s Declare and uses back and forth a numeral interpretation *)
 
@@ -80,15 +80,20 @@ val availability_of_numeral : scope_name -> scopes -> scope_name option option
 type interpretation = identifier list * aconstr
 
 (* Binds a notation in a given scope to an interpretation *)
-type interp_rule = scope_name * notation * interpretation * int option
-val declare_notation : notation -> scope_name -> interpretation -> level ->
-  string -> bool -> unit
+type interp_rule =
+  | NotationRule of scope_name * notation
+  | SynDefRule of kernel_name
+val declare_notation_interpretation : notation -> scope_name ->
+      interpretation -> level -> string -> unit
+
+val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (* Returns the interpretation bound to a notation *)
 val interp_notation : notation -> scopes -> aconstr
 
 (* Returns the possible notations for a given term *)
-val uninterp_notations : rawconstr -> interp_rule list
+val uninterp_notations : rawconstr ->
+      (interp_rule * interpretation * int option) list
 
 (* Test if a notation is available in the scopes *)
 (* context [scopes] if available, the result is not None; the first *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a49352da37..eef20a7b16 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -31,23 +31,20 @@ let _ = Summary.declare_summary
 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
+  Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
+  Symbols.declare_uninterpretation (Symbols.SynDefRule kn) ([],c)
 
 let open_syntax_constant i ((sp,kn),c) =
   Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
 
+let cache_syntax_constant d =
+  load_syntax_constant 1 d
+
 let subst_syntax_constant ((sp,kn),subst,c) =
   subst_aconstr subst c
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8173d3fc45..c548d820db 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -240,7 +240,7 @@ type cases_pattern_expr =
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatNumeral of loc * Bignat.bigint
-  | CPatDelimiters of loc * scope_name * cases_pattern_expr
+  | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
   | CRef of reference
@@ -263,7 +263,7 @@ type constr_expr =
   | CNotation of loc * notation * (identifier * constr_expr) list
   | CGrammar of loc * aconstr * (identifier * constr_expr) list
   | CNumeral of loc * Bignat.bigint
-  | CDelimiters of loc * scope_name * constr_expr
+  | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr = identifier * int * constr_expr * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 85b05a4faa..272b5391b6 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -64,7 +64,7 @@ type cases_pattern_expr =
   | CPatCstr of loc * reference * cases_pattern_expr list
   | CPatAtom of loc * reference option
   | CPatNumeral of loc * Bignat.bigint
-  | CPatDelimiters of loc * scope_name * cases_pattern_expr
+  | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
   | CRef of reference
@@ -87,7 +87,7 @@ type constr_expr =
   | CNotation of loc * notation * (identifier * constr_expr) list
   | CGrammar of loc * aconstr * (identifier * constr_expr) list
   | CNumeral of loc * Bignat.bigint
-  | CDelimiters of loc * scope_name * constr_expr
+  | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr = identifier * int * constr_expr * constr_expr