Re-déplacement du résultat de Grammar au niveau constr_expr

(globalisation uniquement des noms - sauf cases, fix, ..., pas
d'implicites, pas d'interprétation des scopes - pas plus robuste
qu'avant...).
Diverses améliorations affichage et parsing.


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

6 files changed, 19 insertions, 19 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 68bcd1235..1a398c665 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -100,7 +100,7 @@ let idopt_of_name = function
 
 let extern_evar loc n = warning "No notation for Meta"; CMeta (loc,n)
 
-let extern_ref r = Qualid (dummy_loc,shortest_qualid_of_global None r)
+let extern_reference loc r = Qualid (loc,shortest_qualid_of_global None r)
 
 (**********************************************************************)
 (* conversion of terms and cases patterns                             *)
@@ -118,7 +118,7 @@ let rec extern_cases_pattern_in_scope scopes pat =
   | PatVar (_,Anonymous) -> CPatAtom (loc, None) 
   | PatCstr(_,cstrsp,args,na) ->
       let args = List.map (extern_cases_pattern_in_scope scopes) args in
-      let p = CPatCstr (loc,extern_ref (ConstructRef cstrsp),args) in
+      let p = CPatCstr (loc,extern_reference loc (ConstructRef cstrsp),args) in
       (match na with
 	| Name id -> CPatAlias (loc,p,id)
 	| Anonymous -> p)
@@ -186,7 +186,7 @@ let rec extern scopes r =
     extern_symbol scopes r (Symbols.uninterp_notations r)
   with No_match -> match r with
 
-  | RRef (_,ref) -> CRef (extern_ref ref)
+  | RRef (_,ref) -> CRef (extern_reference loc ref)
 
   | RVar (_,id) -> CRef (Ident (loc,id))
 
@@ -202,7 +202,8 @@ let rec extern scopes r =
 	 | RRef (loc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in
 	     let args = extern_args extern scopes args subscopes in
-	     extern_app (implicits_of_global ref) (extern_ref ref) args
+	     extern_app (implicits_of_global ref) (extern_reference loc ref)
+	       args
 	 | _       -> 
 	     explicitize [] (extern scopes f) (List.map (extern scopes) args))
 
@@ -333,7 +334,7 @@ let extern_constr at_top env t =
 (* Main translation function from pattern -> constr_expr *)
 
 let rec extern_pattern tenv env = function
-  | PRef ref -> CRef (extern_ref ref)
+  | PRef ref -> CRef (extern_reference loc ref)
 
   | PVar id -> CRef (Ident (loc,id))
 
@@ -359,7 +360,8 @@ let rec extern_pattern tenv env = function
       let args = List.map (extern_pattern tenv env) args in
       (match f with
 	 | PRef ref ->
-	     extern_app (implicits_of_global ref) (extern_ref ref) args
+	     extern_app (implicits_of_global ref) (extern_reference loc ref)
+	     args
 	 | _       -> explicitize [] (extern_pattern tenv env f) args)
 
   | PSoApp (n,args) ->
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 614cbfdd4..d49b2b9a7 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -33,7 +33,7 @@ val extern_pattern : env -> names_context -> constr_pattern -> constr_expr
    level of quantification clashing with the variables in [env] are renamed *)
 
 val extern_constr : bool -> env -> constr -> constr_expr
-val extern_ref    : global_reference -> reference
+val extern_reference : loc -> global_reference -> reference
 
 (* For debugging *)
 val print_implicits : bool ref
@@ -41,6 +41,7 @@ val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
 val print_universes : bool ref
+val print_no_symbol : bool ref
 
 (* This governs printing of implicit arguments. If [with_implicits] is
    on and not [with_arguments] then implicit args are printed prefixed
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e8e42a7b4..3d5526d39 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -134,7 +134,7 @@ let intern_var (env,impls,_) (vars1,vars2) loc id =
   RRef (loc, VarRef id), imps, args_scopes
 
 (* Is it a global reference or a syntactic definition? *)
-let intern_qualid env vars loc qid =
+let intern_qualid loc qid =
   try match Nametab.extended_locate qid with
   | TrueGlobal ref ->
     if !dump then add_glob loc ref;
@@ -146,14 +146,14 @@ let intern_qualid env vars loc qid =
 
 let intern_reference env lvar = function
   | Qualid (loc, qid) ->
-      intern_qualid env lvar loc qid
+      intern_qualid loc qid
   | Ident (loc, id) ->
       (* For old ast syntax compatibility *)
       if (string_of_id id).[0] = '$' then RVar (loc,id),[],[] else
       (* End old ast syntax compatibility *)
       try intern_var env lvar loc id
       with Not_found -> 
-      try intern_qualid env lvar loc (make_short_qualid id)
+      try intern_qualid loc (make_short_qualid id)
       with e ->
 	(* Extra allowance for grammars *)
 	if !interning_grammar then begin
@@ -162,6 +162,9 @@ let intern_reference env lvar = function
 	end
 	else raise e
 
+let interp_reference vars r =
+  let (r,_,_) = intern_reference (Idset.empty,[],[]) (vars,[]) r in r
+
 let apply_scope_env (ids,impls,scopes as env) = function
   | [] -> env, []
   | (Some sc)::scl -> (ids,impls,sc::scopes), scl
@@ -338,7 +341,7 @@ let traverse_binder id (subst,(ids,impls,scopes as env)) =
 let rec subst_rawconstr loc interp (subst,env as senv) = function
   | AVar id ->
       let a = try List.assoc id subst
-      with Not_found -> CRef (Ident (dummy_loc,id)) in
+      with Not_found -> CRef (Ident (loc,id)) in
       interp env a
   | t ->
       map_aconstr_with_binders_loc loc traverse_binder
@@ -426,9 +429,6 @@ let internalise sigma env allow_soapp lvar c =
     | CCast (loc, c1, c2) ->
 	RCast (loc,intern env c1,intern env c2)
 
-    | CGrammar (loc,c,subst) ->
-	subst_rawconstr loc intern (subst,env) c
-
     | CDynamic (loc,d) -> RDynamic (loc,d)
 
   and intern_eqn n (ids,impls,scopes as env) (loc,lhs,rhs) =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index ce8c6f5ee..8666db633 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -80,6 +80,8 @@ val interp_constrpattern_gen :
 val interp_constrpattern : 
   evar_map -> env -> constr_expr -> int list * constr_pattern
 
+val interp_reference : identifier list -> reference -> rawconstr
+
 (* Interprets into a abbreviatable constr *)
 val interp_aconstr : constr_expr -> aconstr
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2028d6de8..bce7772b4 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -262,7 +262,6 @@ type constr_expr =
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * 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 * string * constr_expr
   | CDynamic of loc * Dyn.t
@@ -299,7 +298,6 @@ let constr_loc = function
   | CSort (loc,_) -> loc
   | CCast (loc,_,_) -> loc
   | CNotation (loc,_,_) -> loc
-  | CGrammar (loc,_,_) -> loc
   | CNumeral (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
   | CDynamic _ -> dummy_loc
@@ -328,7 +326,6 @@ let rec occur_var_constr_expr id = function
   | 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
-  | CGrammar (loc,_,l) -> List.exists (fun (_,x) -> occur_var_constr_expr id x)l
   | CDelimiters (loc,_,a) -> occur_var_constr_expr id a
   | CHole _ | CMeta _ | CSort _ | CNumeral _ | CDynamic _ -> false
   | CCases (loc,_,_,_) 
@@ -371,7 +368,6 @@ let map_constr_expr_with_binders f g e = function
   | 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)
-  | CGrammar (loc,r,l) -> CGrammar (loc,r,List.map (fun (x,t) ->(x,f e t)) 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 272b5391b..38c39fc9b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -85,7 +85,6 @@ type constr_expr =
   | CSort of loc * rawsort
   | CCast of loc * constr_expr * 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 * string * constr_expr
   | CDynamic of loc * Dyn.t