Préparation à la prise en compte des changements de scopes internes aux notations; bugs d'affichage (confusion key/scope dans les délimiteurs); bug de non-indépendance des règles d'affichage et parsing vis à vis du nom des variables de la notation

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

9 files changed, 74 insertions, 69 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1a398c665..9e86405cc 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -111,7 +111,7 @@ let rec extern_cases_pattern_in_scope scopes pat =
     let (sc,n) = Symbols.uninterp_cases_numeral pat in
     match Symbols.availability_of_numeral sc scopes with
     | None -> raise No_match
-    | Some scopt -> insert_pat_delimiters (CPatNumeral (loc,n)) scopt
+    | Some key -> insert_pat_delimiters (CPatNumeral (loc,n)) key
   with No_match ->
   match pat with
   | PatVar (_,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
@@ -283,7 +283,7 @@ and extern_eqn scopes (loc,ids,pl,c) =
 and extern_numeral scopes t (sc,n) =
   match Symbols.availability_of_numeral sc scopes with
     | None -> raise No_match
-    | Some scopt -> insert_delimiters (CNumeral (loc,n)) scopt
+    | Some key -> insert_delimiters (CNumeral (loc,n)) key
 
 and extern_symbol scopes t = function
   | [] -> raise No_match
@@ -305,10 +305,11 @@ and extern_symbol scopes t = function
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
-	      | Some scopt ->
+	      | Some (scopt,key) ->
 	          let scopes = option_cons scopt scopes in
-	          let l = list_map_assoc (extern scopes) subst in
-	          insert_delimiters (CNotation (loc,ntn,l)) scopt)
+	          let l =
+		    List.map (fun (c,scl) -> extern (scl@scopes) c) subst in
+	          insert_delimiters (CNotation (loc,ntn,l)) key)
           | SynDefRule kn ->
               CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
  	if args = [] then e 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3d5526d39..9e792dc74 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -334,18 +334,19 @@ let coerce_to_id = function
       user_err_loc (constr_loc c, "subst_rawconstr",
         str"This expression should be a simple identifier")
 
-let traverse_binder id (subst,(ids,impls,scopes as env)) =
-  let id = try coerce_to_id (List.assoc id subst) with Not_found -> id in
-  id,(subst,(Idset.add id ids,impls,scopes))
+let traverse_binder subst id (ids,impls,scopes as env) =
+  let id = try coerce_to_id (fst (List.assoc id subst)) with Not_found -> id in
+  id,(Idset.add id ids,impls,scopes)
 
-let rec subst_rawconstr loc interp (subst,env as senv) = function
+let rec subst_rawconstr loc interp subst (ids,impls,scopes as env) = function
   | AVar id ->
-      let a = try List.assoc id subst
-      with Not_found -> CRef (Ident (loc,id)) in
-      interp env a
+      let (a,subscopes) =
+	try List.assoc id subst
+	with Not_found -> (CRef (Ident (loc,id)),[]) in
+      interp (ids,impls,subscopes@scopes) a
   | t ->
-      map_aconstr_with_binders_loc loc traverse_binder
-      (subst_rawconstr loc interp) senv t
+      map_aconstr_with_binders_loc loc (traverse_binder subst)
+      (subst_rawconstr loc interp subst) env t
 
 (**********************************************************************)
 (* Main loop                                                          *)
@@ -395,8 +396,9 @@ let internalise sigma env allow_soapp lvar c =
 	RLetIn (loc, na, intern env c1,
           intern (name_fold Idset.add na ids,impls,scopes) c2)
     | CNotation (loc,ntn,args) ->
-	subst_rawconstr loc intern (args,env)
-	  (Symbols.interp_notation ntn scopes)
+	let (ids,c) = Symbols.interp_notation ntn scopes in
+	let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+	subst_rawconstr loc intern subst env c
     | CNumeral (loc, n) ->
 	Symbols.interp_numeral loc n scopes
     | CDelimiters (loc, key, e) ->
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index e2e60dc15..98c500c12 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -51,7 +51,7 @@ let ppcmd_of_cut = function
   | PpTbrk(n1,n2) -> tbrk(n1,n2)
 
 type unparsing = 
-  | UnpMetaVar of identifier * tolerability
+  | UnpMetaVar of int * tolerability
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing list
   | UnpCut of ppcut
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 890422de8..625c85e68 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -41,7 +41,7 @@ val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
 val ppcmd_of_cut : ppcut -> std_ppcmds
 
 type unparsing = 
-  | UnpMetaVar of identifier * tolerability
+  | UnpMetaVar of int * tolerability
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing list
   | UnpCut of ppcut
diff --git a/interp/symbols.ml b/interp/symbols.ml
index 3704decd4..6fc3c93c0 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -39,13 +39,13 @@ open Ppextend
 (**********************************************************************)
 (* Scope of symbols *)
 
+type scopes = scope_name list
 type level = precedence * precedence list
 type delimiters = string
 type scope = {
-  notations: (aconstr * (level * string)) Stringmap.t;
+  notations: (interpretation * (level * string)) Stringmap.t;
   delimiters: delimiters option
 }
-type scopes = scope_name list
 
 (* Scopes table: scope_name -> symbol_interpretation *)
 let scope_map = ref Stringmap.empty
@@ -56,13 +56,15 @@ let empty_scope = {
 }
 
 let default_scope = "core_scope"
+let type_scope = "type_scope"
 
 let _ = Stringmap.add default_scope empty_scope !scope_map
+let _ = Stringmap.add type_scope empty_scope !scope_map
 
 (**********************************************************************)
 (* The global stack of scopes                                         *)
 
-let scope_stack = ref [default_scope]
+let scope_stack = ref [default_scope;type_scope]
 
 let current_scopes () = !scope_stack
 
@@ -111,7 +113,6 @@ let find_delimiters_scope loc key =
 
 (* Uninterpretation tables *)
 
-type interpretation = identifier list * aconstr
 type interp_rule =
   | NotationRule of scope_name * notation
   | SynDefRule of kernel_name
@@ -183,14 +184,14 @@ let lookup_numeral_interpreter loc sc =
 
 let find_with_delimiters scope =
   match (Stringmap.find scope !scope_map).delimiters with
-    | Some _ -> Some (Some scope)
+    | Some key -> Some (Some scope, Some key)
     | None -> None
 
 let rec find_without_delimiters find ntn_scope = function
   | scope :: scopes -> 
       (* Is the expected ntn/numpr attached to the most recently open scope? *)
       if scope = ntn_scope then
-	Some None
+	Some (None,None)
       else
 	(* If the most recently open scope has a notation/numeral printer
     	   but not the expected one then we need delimiters *)
@@ -204,7 +205,7 @@ let rec find_without_delimiters find ntn_scope = function
 
 (* The mapping between notations and their interpretation *)
 
-let declare_notation_interpretation ntn scope (_,pat) prec df =
+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);
@@ -231,14 +232,9 @@ let uninterp_notations c =
   Gmapl.find (rawconstr_key c) !notations_key_table
 
 let availability_of_notation (ntn_scope,ntn) scopes =
-  match 
-    let f scope =
-      Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
-    find_without_delimiters f ntn_scope scopes
-  with
-    | None -> None
-    | Some None -> Some None
-    | Some (Some dlm) -> Some (Some ntn_scope)
+  let f scope =
+    Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in
+  find_without_delimiters f ntn_scope scopes
 
 let rec interp_numeral loc n = function
   | scope :: scopes ->
@@ -278,12 +274,8 @@ let uninterp_cases_numeral c =
   with Not_found -> raise No_match
 
 let availability_of_numeral printer_scope scopes =
-  match 
-    let f scope = Hashtbl.mem numeral_interpreter_tab scope in
-    find_without_delimiters f printer_scope scopes
-  with
-    | None -> None
-    | Some x -> Some x
+  let f scope = Hashtbl.mem numeral_interpreter_tab scope in
+  option_app snd (find_without_delimiters f printer_scope scopes)
 
 (* Miscellaneous *)
 
@@ -356,13 +348,14 @@ let rec rawconstr_of_aconstr () x =
     rawconstr_of_aconstr () x
 
 let pr_notation_info prraw ntn c =
-  str ntn ++ str " stands for " ++ prraw (rawconstr_of_aconstr () c)
+  str "\"" ++ str ntn ++ str "\" := " ++ prraw (rawconstr_of_aconstr () c)
 
 let pr_named_scope prraw scope sc =
   str "Scope " ++ str scope ++ fnl ()
   ++ pr_delimiters_info sc.delimiters ++ fnl ()
   ++ Stringmap.fold
-       (fun ntn (r,(_,df)) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
+       (fun ntn ((_,r),(_,df)) strm ->
+	 pr_notation_info prraw df r ++ fnl () ++ strm)
        sc.notations (mt ())
 
 let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
@@ -405,7 +398,7 @@ let unfreeze (scm,scs,asc,dlm,fkm,pprules) =
 
 let init () =
 (*
-  scope_map := Strinmap.empty;
+  scope_map := Stringmap.empty;
   scope_stack := Stringmap.empty
   arguments_scope := Refmap.empty
 *)
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 24a138803..17b99dbd4 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -73,12 +73,10 @@ val interp_numeral_as_pattern : loc -> bigint -> name -> scopes ->cases_pattern
 val uninterp_numeral : rawconstr -> scope_name * bigint
 val uninterp_cases_numeral : cases_pattern -> scope_name * bigint
 
-val availability_of_numeral : scope_name -> scopes -> scope_name option option
+val availability_of_numeral : scope_name -> scopes -> delimiters option option
 
 (*s Declare and interpret back and forth a notation *)
 
-type interpretation = identifier list * aconstr
-
 (* Binds a notation in a given scope to an interpretation *)
 type interp_rule =
   | NotationRule of scope_name * notation
@@ -89,7 +87,7 @@ val declare_notation_interpretation : notation -> scope_name ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (* Returns the interpretation bound to a notation *)
-val interp_notation : notation -> scopes -> aconstr
+val interp_notation : notation -> scopes -> interpretation
 
 (* Returns the possible notations for a given term *)
 val uninterp_notations : rawconstr ->
@@ -100,12 +98,13 @@ val uninterp_notations : rawconstr ->
 (* argument is itself not None if a delimiters is needed; the second *)
 (* argument is a numeral printer if the *)
 val availability_of_notation : scope_name * notation -> scopes -> 
-  scope_name option option
+  (scope_name option * delimiters option) option
 
 (*s** Miscellaneous *)
 
 (* Checks for already existing notations *)
-val exists_notation_in_scope : scope_name -> level -> notation -> aconstr->bool
+val exists_notation_in_scope : scope_name -> level -> notation ->
+      interpretation-> bool
 val exists_notation : level -> notation -> bool
 
 (* Declares and looks for scopes associated to arguments of a global ref *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index bce7772b4..1be41458d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -41,7 +41,7 @@ let name_app f e = function
   | Anonymous -> Anonymous, e
 
 let map_aconstr_with_binders_loc loc g f e = function
-  | AVar (id) -> RVar (loc,id)
+  | AVar id -> RVar (loc,id)
   | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args)
   | ALambda (na,ty,c) ->
       let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
@@ -225,13 +225,18 @@ and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) =
     match_ alp metas sigma rhs1 rhs2
   else raise No_match
 
-let match_aconstr c (metas,pat) = match_ [] metas [] c pat
+type scope_name = string
+
+type interpretation = (identifier * scope_name list) list * aconstr
+
+let match_aconstr c (metas_scl,pat) =
+  let subst = match_ [] (List.map fst metas_scl) [] c pat in
+  (* Reorder canonically the substitution *)
+  List.map (fun (x,scl) -> (List.assoc x subst,scl)) metas_scl
 
 (**********************************************************************)
 (*s Concrete syntax for terms *)
 
-type scope_name = string
-
 type notation = string
 
 type explicitation = int
@@ -261,7 +266,7 @@ type constr_expr =
   | CMeta of loc * int
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr
-  | CNotation of loc * notation * (identifier * constr_expr) list
+  | CNotation of loc * notation * constr_expr list
   | CNumeral of loc * Bignat.bigint
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
@@ -325,7 +330,7 @@ let rec occur_var_constr_expr id = function
   | CLambdaN (_,l,b) -> occur_var_binders id b l
   | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a]
   | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b
-  | CNotation (_,_,l) -> List.exists (fun (_,x) -> occur_var_constr_expr id x) l
+  | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l
   | CDelimiters (loc,_,a) -> occur_var_constr_expr id a
   | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ -> false
   | CCases (loc,_,_,_) 
@@ -367,7 +372,7 @@ let map_constr_expr_with_binders f g e = function
       let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
   | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
   | CCast (loc,a,b) -> CCast (loc,f e a,f e b)
-  | CNotation (loc,n,l) -> CNotation (loc,n,List.map (fun (x,t) ->(x,f e t)) l)
+  | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x
   | CCases (loc,po,a,bl) ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 38c39fc9b..35f62478e 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -48,12 +48,14 @@ val aconstr_of_rawconstr : rawconstr -> aconstr
 (* [match_aconstr metas] match a rawconstr against an aconstr with
    metavariables in [metas]; it raises [No_match] if the matching fails *)
 exception No_match
-val match_aconstr : 
-  rawconstr -> (identifier list * aconstr) -> (identifier * rawconstr) list
-
-(*s Concrete syntax for terms *)
 
 type scope_name = string
+type interpretation = (identifier * scope_name list) list * aconstr
+
+val match_aconstr : rawconstr -> interpretation ->
+      (rawconstr * scope_name list) list
+
+(*s Concrete syntax for terms *)
 
 type notation = string
 
@@ -84,7 +86,7 @@ type constr_expr =
   | CMeta of loc * int
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * constr_expr
-  | CNotation of loc * notation * (identifier * constr_expr) list
+  | CNotation of loc * notation * constr_expr list
   | CNumeral of loc * Bignat.bigint
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 265f4945d..e37d0d664 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -316,12 +316,14 @@ let make_hunks_ast symbols etyps from =
   in l
 
 let make_hunks etyps symbols =
+  let vars,typs = List.split etyps in
   let (_,l) =
   List.fold_right
     (fun it (ws,l) -> match it with
       | NonTerminal m ->
-	  let prec = precedence_of_entry_type (List.assoc m etyps) in
-	  let u = UnpMetaVar (m,prec) in
+	  let i = list_index m vars in
+	  let prec = precedence_of_entry_type (List.nth typs (i-1)) in
+	  let u = UnpMetaVar (i ,prec) in
 	  let l' = match ws with
 	    | AddBrk n -> UnpCut (PpBrk(n,1)) :: u :: l
 	    | _ -> u :: l in
@@ -561,10 +563,10 @@ let add_syntax_extension df modifiers =
 
 (* A notation comes with a grammar rule, a pretty-printing rule, an
    identifiying pattern called notation and an associated scope *)
-let load_notation _ (_,(_,prec,ntn,scope,_,pat,onlyparse,_)) =
+let load_notation _ (_,(_,prec,ntn,scope,pat,onlyparse,_)) =
   Symbols.declare_scope scope
 
-let open_notation i (_,(oldse,prec,ntn,scope,metas,pat,onlyparse,df)) =
+let open_notation i (_,(oldse,prec,ntn,scope,pat,onlyparse,df)) =
   if i=1 then begin
     let b = Symbols.exists_notation_in_scope scope prec ntn pat in
     (* Declare the old printer rule and its interpretation *)
@@ -572,21 +574,21 @@ let open_notation i (_,(oldse,prec,ntn,scope,metas,pat,onlyparse,df)) =
       Esyntax.add_ppobject {sc_univ="constr";sc_entries=out_some oldse};
     (* Declare the interpretation *)
     if not b then
-      Symbols.declare_notation_interpretation ntn scope (metas,pat) prec df;
+      Symbols.declare_notation_interpretation ntn scope pat prec df;
     if not b & not onlyparse then
-      Symbols.declare_uninterpretation (NotationRule (ntn,scope)) (metas,pat)
+      Symbols.declare_uninterpretation (NotationRule (ntn,scope)) pat
   end
 
 let cache_notation o =
   load_notation 1 o;
   open_notation 1 o
 
-let subst_notation (_,subst,(oldse,prec,ntn,scope,metas,pat,b,df)) =
+let subst_notation (_,subst,(oldse,prec,ntn,scope,(metas,pat),b,df)) =
   (option_app
     (list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst)) oldse,
    prec,ntn,
    scope,
-   metas,subst_aconstr subst pat, b, df)
+   (metas,subst_aconstr subst pat), b, df)
 
 let (inNotation, outNotation) =
   declare_object {(default_object "NOTATION") with
@@ -642,8 +644,9 @@ let add_notation_in_scope df a (assoc,n,etyps,onlyparse) sc toks =
     if onlyparse then None
     else Some (make_old_pp_rule n symbols typs r notation scope vars) in
   (* Declare the interpretation *)
+  let vars = List.map (fun id -> id,[] (* insert the right scope *)) vars in
   Lib.add_anonymous_leaf
-    (inNotation(old_pp_rule,prec,notation,scope,vars,a,onlyparse,df))
+    (inNotation(old_pp_rule,prec,notation,scope,(vars,a),onlyparse,df))
 
 let add_notation df a modifiers sc =
   let toks = split df in