Parsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


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

3 files changed, 40 insertions, 45 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 8bfa53842c..222b8277a2 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -342,13 +342,12 @@ open Termast
 
 let ast_of_cvt_bind f = function
   | (NoDep n,c) -> ope ("BINDING", [(num n); ope ("COMMAND",[(f c)])])
-  | (Dep  id,c) -> ope ("BINDING", [nvar (string_of_id id);
-                                      ope  ("COMMAND",[(f c)])]) 
+  | (Dep  id,c) -> ope ("BINDING", [nvar id; ope  ("COMMAND",[(f c)])]) 
   | (Com,c)     -> ope ("BINDING", [ope ("COMMAND",[(f c)])])
 
 let rec ast_of_cvt_intro_pattern = function
   | WildPat   -> ope ("WILDCAR",[])
-  | IdPat id  -> nvar (string_of_id id) 
+  | IdPat id  -> nvar id
   | DisjPat l -> ope ("DISJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
   | ConjPat l -> ope ("CONJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
   | ListPat l -> ope ("LISTPATTERN",  (List.map ast_of_cvt_intro_pattern l))
@@ -363,7 +362,7 @@ let last_of_cvt_flags (_,red) =
    let lqid =
      List.map
        (function
-	  | EvalVarRef id -> nvar (string_of_id id)
+	  | EvalVarRef id -> nvar id
 	  | EvalConstRef sp ->
 	      ast_of_qualid (Global.qualid_of_global (ConstRef sp)))
        lconst in
@@ -383,7 +382,7 @@ let ast_of_cvt_redexp = function
   | Unfold l ->
     ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
       [match sp with
-	| EvalVarRef id -> nvar (string_of_id id)
+	| EvalVarRef id -> nvar id
 	| EvalConstRef sp -> 					
 	    ast_of_qualid (Global.qualid_of_global (ConstRef sp))]
       @(List.map num locc))) l)
@@ -397,8 +396,8 @@ let ast_of_cvt_redexp = function
 
 (* Gives the ast corresponding to a tactic argument *)
 let ast_of_cvt_arg = function
-  | Identifier id   -> nvar (string_of_id id) 
-  | Qualid qid      -> nvar (Nametab.string_of_qualid qid) 
+  | Identifier id   -> nvar id
+  | Qualid qid      -> ast_of_qualid qid
   | Quoted_string s -> str s
   | Integer n       -> num n 
   | Command c       -> ope ("COMMAND",[c])
@@ -411,8 +410,8 @@ let ast_of_cvt_arg = function
       "Constr_context argument could not be used">]
   | Clause idl      -> 
       let transl = function
-	| InHyp id -> ope ("INHYP", [nvar (string_of_id id)])
-	| InHypType id -> ope ("INHYPTYPE", [nvar (string_of_id id)]) in
+	| InHyp id -> ope ("INHYP", [nvar id])
+	| InHypType id -> ope ("INHYPTYPE", [nvar id]) in
       ope ("CLAUSE", List.map transl idl)
   | Bindings bl     -> ope ("BINDINGS", 
 			    List.map (ast_of_cvt_bind (fun x -> x)) bl)
@@ -424,17 +423,14 @@ let ast_of_cvt_arg = function
   | Tacexp ast      -> ope ("TACTIC",[ast])
   | Tac (tac,ast) -> ast
   | Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red])
-  | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); 
-                                      (num n); 
-                                      ope ("COMMAND",[c])]) 
-  | Cofixexp (id,c) -> ope ("COFIXEXP",[(nvar (string_of_id id)); 
-                                          (ope ("COMMAND",[c]))])
+  | Fixexp (id,n,c) -> ope ("FIXEXP",[nvar id; num n; ope ("COMMAND",[c])])
+  | Cofixexp (id,c) -> ope ("COFIXEXP",[nvar id; ope ("COMMAND",[c])])
   | Intropattern p ->  ast_of_cvt_intro_pattern p
   | Letpatterns (gl_occ_opt,hyp_occ_list) ->
      let hyps_pats =
        List.map
 	 (fun (id,l) ->
-	    ope ("HYPPATTERN", nvar (string_of_id id) :: (List.map num l)))
+	    ope ("HYPPATTERN", nvar id :: (List.map num l)))
 	 hyp_occ_list in
      let all_pats =
        match gl_occ_opt with
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index ede93699af..846344210c 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -29,6 +29,7 @@ open Tactic_debug
 open Coqast
 open Ast
 open Term
+open Declare
 
 let err_msg_tactic_not_found macro_loc macro =
   user_err_loc
@@ -42,13 +43,13 @@ type value =
   | VRTactic of (goal list sigma * validation)
   | VContext of (goal sigma -> value)
   | VArg of tactic_arg
-  | VFun of (string * value) list * string option list * Coqast.t
+  | VFun of (identifier * value) list * identifier option list * Coqast.t
   | VVoid
   | VRec of value ref
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 and interp_sign =
-  enamed_declarations * Environ.env * (string * value) list *
+  enamed_declarations * Environ.env * (identifier * value) list *
     (int * constr) list * goal sigma option * debug_info
 
 (* For tactic_of_value *)
@@ -124,9 +125,9 @@ let constr_of_id id = function
 
 (* Extracted the constr list from lfun *)
 let rec constr_list goalopt = function
-  | (str,VArg(Constr c))::tl -> (id_of_string str,c)::(constr_list goalopt tl)
-  | (str,VArg(Identifier id))::tl ->
-    (try (id_of_string str,(constr_of_id id goalopt))::(constr_list goalopt tl)
+  | (id,VArg(Constr c))::tl -> (id,c)::(constr_list goalopt tl)
+  | (id0,VArg(Identifier id))::tl ->
+    (try (id0,(constr_of_id id goalopt))::(constr_list goalopt tl)
      with | Not_found -> (constr_list goalopt tl))
   | _::tl -> constr_list goalopt tl
   | [] -> []
@@ -278,12 +279,12 @@ let head_with_value (lvar,lval) =
 (* Type of patterns *)
 type match_pattern =
   | Term of constr_pattern
-  | Subterm of string option * constr_pattern
+  | Subterm of identifier option * constr_pattern
 
 (* Type of hypotheses for a Match Context rule *)
 type match_context_hyps =
   | NoHypId of match_pattern
-  | Hyp of string * match_pattern
+  | Hyp of identifier * match_pattern
 
 (* Type of a Match rule for Match Context and Match *)
 type match_rule=
@@ -503,7 +504,7 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
       (try (unrec (List.assoc s lfun))
        with | Not_found ->
          (try (vcontext_interp goalopt (lookup s))
-          with | Not_found -> VArg (Identifier (id_of_string s))))
+          with | Not_found -> VArg (Identifier s)))
     | Node(_,"QUALIDARG",[Nvar(_,s)]) ->
       (try (make_qid (unrec (List.assoc s lfun)))
        with | Not_found ->
@@ -531,9 +532,9 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
       VArg (Tac ((tac_interp lfun lmatch debug ast),ast))
 (*Remains to treat*)
     | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
-      VArg ((Fixexp (id_of_string s,n,c)))
+      VArg ((Fixexp (s,n,c)))
     | Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) ->
-      VArg ((Cofixexp (id_of_string s,c)))
+      VArg ((Cofixexp (s,c)))
 (*End of Remains to treat*)
     | Node(_,"INTROPATTERN", [ast]) ->
       VArg ((Intropattern (cvt_intro_pattern
@@ -621,19 +622,18 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
   | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
     (id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t)::
       (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
-  | Node(_,"LETCUTCLAUSE",[Nvar(_,s);com;tce])::tl ->
-    let id = id_of_string s
-    and typ =
+  | Node(_,"LETCUTCLAUSE",[Nvar(_,id);com;tce])::tl ->
+    let typ =
       constr_of_Constr (unvarg
       (val_interp (evc,env,lfun,lmatch,goalopt,debug) com))
     and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce in
     (match tac with
     | VArg (Constr csr) ->
-      (s,VArg (Constr (mkCast (csr,typ))))::
+      (id,VArg (Constr (mkCast (csr,typ))))::
       (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
     | VArg (Identifier id) ->
       (try
-         (s,VArg (Constr (mkCast (constr_of_id id goalopt,typ))))::
+         (id,VArg (Constr (mkCast (constr_of_id id goalopt,typ))))::
          (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
        with | Not_found ->
          errorlabstrm "Tacinterp.letin_interp"
@@ -645,12 +645,12 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
            (match goalopt with
            | None -> Global.named_context ()
            | Some g -> pf_hyps g) in
-         start_proof id Declare.NeverDischarge ndc typ;
+         start_proof id NeverDischarge ndc typ;
          by t;
          let (_,({const_entry_body = pft; const_entry_type = _},_)) =
            cook_proof () in
          delete_proof id;
-         (s,VArg (Constr (mkCast (pft,typ))))::
+         (id,VArg (Constr (mkCast (pft,typ))))::
          (letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
        with | NotTactic ->
          delete_proof id;
@@ -663,9 +663,8 @@ and letin_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
 (* Interprets the clauses of a LetCut *)
 and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
   | [] -> tclIDTAC
-  | Node(_,"LETCUTCLAUSE",[Nvar(_,s);com;tce])::tl ->
-    let id = id_of_string s
-    and typ =
+  | Node(_,"LETCUTCLAUSE",[Nvar(_,id);com;tce])::tl ->
+    let typ =
       constr_of_Constr (unvarg
       (val_interp (evc,env,lfun,lmatch,goalopt,debug) com))
     and tac = val_interp (evc,env,lfun,lmatch,goalopt,debug) tce
@@ -699,7 +698,7 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
     | _ ->
       (try
          let t = tactic_of_value tac in
-         start_proof id Declare.NeverDischarge ndc typ;
+         start_proof id NeverDischarge ndc typ;
          by t;
          let (_,({const_entry_body = pft; const_entry_type = _},_)) =
            cook_proof () in
@@ -1216,7 +1215,7 @@ let add_tacdef na vbody =
       errorlabstrm "Tacinterp.add_tacdef" 
       [< 'sTR
          "There is already a Meta Definition or a Tactic Definition named ";
-         'sTR na>];
-    let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
-    Options.if_verbose mSGNL [< 'sTR (na ^ " is defined") >]
+         pr_id na>];
+    let _ = Lib.add_leaf na OBJ (inMD (na,vbody)) in
+    Options.if_verbose mSGNL [< pr_id na; 'sTR " is defined" >]
   end
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 971cb88df8..f6be508697 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -25,13 +25,13 @@ type value =
   | VRTactic of (goal list sigma * validation)
   | VContext of (goal sigma -> value)
   | VArg of tactic_arg
-  | VFun of (string * value) list * string option list * Coqast.t
+  | VFun of (identifier * value) list * identifier option list * Coqast.t
   | VVoid
   | VRec of value ref
 
 (* Signature for interpretation: val\_interp and interpretation functions *)
 and interp_sign =
-  enamed_declarations * Environ.env * (string * value) list *
+  enamed_declarations * Environ.env * (identifier * value) list *
     (int * constr) list * goal sigma option * debug_info
 
 (* Gives the constr corresponding to a CONSTR [tactic_arg] *)
@@ -45,7 +45,7 @@ val tacticIn : (unit -> Coqast.t) -> Coqast.t
    initialized with dummy values *)
 val r_evc     : enamed_declarations ref
 val r_env     : Environ.env ref
-val r_lfun    : (string * value) list ref
+val r_lfun    : (identifier * value) list ref
 val r_lmatch  : (int * constr) list ref
 val r_goalopt : goal sigma option ref
 val r_debug   : debug_info ref
@@ -57,7 +57,7 @@ val set_debug : debug_info -> unit
 val get_debug : unit -> debug_info
 
 (* Adds a definition for tactics in the table *)
-val add_tacdef : string -> Coqast.t -> unit
+val add_tacdef : identifier -> Coqast.t -> unit
 
 (* Interprets any expression *)
 val val_interp : interp_sign -> Coqast.t -> value
@@ -66,8 +66,8 @@ val val_interp : interp_sign -> Coqast.t -> value
 val interp_tacarg : interp_sign -> Coqast.t -> tactic_arg
 
 (* Interprets tactic expressions *)
-val tac_interp : (string * value) list -> (int * constr) list -> debug_info ->
-                 Coqast.t -> tactic
+val tac_interp : (identifier * value) list -> (int * constr) list ->
+                 debug_info -> Coqast.t -> tactic
 
 (* Initial call for interpretation *)
 val interp : Coqast.t -> tactic