Simplifification de vernac_expr li l'abandon du traducteur

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

4 files changed, 41 insertions, 97 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 8d4f3b83f4..24bee11e12 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -88,19 +88,15 @@ let rec make_tags lev = function
       etyp :: make_tags lev l
   | [] -> []
 
-let declare_tactic_pprule n (s,t,p) =
-  Pptactic.declare_extra_tactic_pprule true s (t,p);
-  Pptactic.declare_extra_tactic_pprule false s (t,p)
+let cache_tactic_notation (_,(pa,pp)) =
+  Egrammar.extend_grammar (Egrammar.TacticGrammar pa);
+  Pptactic.declare_extra_tactic_pprule true (pi1 pp) (pi2 pp, pi3 pp)
 
-let cache_tactic_notation (_,((n,pa),pp)) =
-  Egrammar.extend_grammar (Egrammar.TacticGrammar (n,pa));
-  List.iter (declare_tactic_pprule n) pp
+let subst_tactic_parule subst (key,n,p,(d,tac)) =
+  (key,n,p,(d,Tacinterp.subst_tactic subst tac))
 
-let subst_one_tactic_notation subst (s,p,(d,tac)) =
-  (s,p,(d,Tacinterp.subst_tactic subst tac))
-
-let subst_tactic_notation (_,subst,((n,pa),pp)) =
-  ((n,List.map (subst_one_tactic_notation subst) pa),pp)
+let subst_tactic_notation (_,subst,(pa,pp)) =
+  (subst_tactic_parule subst pa,pp)
 
 let (inTacticGrammar, outTacticGrammar) =
   declare_object {(default_object "TacticGrammar") with
@@ -123,23 +119,14 @@ let rec next_key_away key t =
   if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
   else key
 
-let make_tactic_pprule n s prods =
+let add_tactic_notation (n,prods,e) =
   let tags = make_tags n prods in
-  let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in
-  (s, tags, (n,List.map make_terminal_status prods))
-
-let make_tactic_parule s prods e =
+  let key = next_key_away (tactic_notation_key prods) tags in
+  let pprule = (key,tags,(n,List.map make_terminal_status prods)) in
   let ids = List.fold_left cons_production_parameter [] prods in
   let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in
-  (s,prods,(Lib.cwd (),tac))
-
-let locate_tactic_body n (s,prods,e) =
-  let (s',t,p as pp) = make_tactic_pprule n s prods in
-  (make_tactic_parule s' prods e, pp)
-
-let add_tactic_notation (n,g) =
-  let pa,pp = List.split (List.map (locate_tactic_body n) g) in
-  Lib.add_anonymous_leaf (inTacticGrammar ((n,pa),pp))
+  let parule = (key,n,prods,(Lib.cwd(),tac)) in
+  Lib.add_anonymous_leaf (inTacticGrammar (parule,pprule))
 
 (**********************************************************************)
 (* Printing grammar entries                                           *)
@@ -631,7 +618,7 @@ let recompute_assoc typs =
 let make_grammar_rule (n,typs,symbols,_) ntn =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
-  (n,assoc,ntn,prod,None)
+  (n,assoc,ntn,prod)
 
 let make_pp_rule (n,typs,symbols,fmt) =
   match fmt with
@@ -654,7 +641,7 @@ let pr_level ntn (from,args) =
 
 let cache_syntax_extension (_,(_,(prec,ntn,gr,pp))) =
   try 
-    let _, oldprec = Notation.level_of_notation ntn in
+    let oldprec = Notation.level_of_notation ntn in
     if prec <> oldprec then
       errorlabstrm ""
 	(str ("Notation "^ntn^" is already defined") ++ spc() ++ 
@@ -663,7 +650,7 @@ let cache_syntax_extension (_,(_,(prec,ntn,gr,pp))) =
 	 pr_level ntn prec);
   with Not_found ->
     (* Reserve the notation level *)
-    Notation.declare_notation_level ntn (None,prec);
+    Notation.declare_notation_level ntn prec;
     (* Declare the parsing rule *)
     Egrammar.extend_grammar (Egrammar.Notation (prec,gr));
     (* Declare the printing rule *)
@@ -869,10 +856,10 @@ let load_notation _ (_,(_,scope,pat,onlyparse,_)) =
 
 let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) =
   if i=1 then begin
-    let exists,_ = Notation.exists_notation_in_scope scope ntn pat in
+    let exists = Notation.exists_notation_in_scope scope ntn pat in
     (* Declare the interpretation *)
     if not exists then
-      Notation.declare_notation_interpretation ntn scope pat df false;
+      Notation.declare_notation_interpretation ntn scope pat df;
     if not exists & not onlyparse then
       Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat
   end
@@ -929,7 +916,7 @@ let level_rule (n,p) = if p = E then n else max (n-1) 0
 
 let recover_syntax ntn = 
   try 
-    let _,prec = Notation.level_of_notation ntn in
+    let prec = Notation.level_of_notation ntn in
     let pprule,_ = Notation.find_notation_printing_rule ntn in
     let gr = Egrammar.recover_notation_grammar ntn prec in
     Some (prec,ntn,gr,pprule)
@@ -1022,7 +1009,7 @@ let add_infix local (inf,modl) pr sc =
   else
     add_notation_in_scope local df a modl sc toks
 
-let standardise_locatable_notation ntn =
+let standardize_locatable_notation ntn =
   let unquote = function
     | String s -> [unquote_notation_token s]
     | _ -> [] in
@@ -1070,16 +1057,3 @@ let add_delimiters scope key =
 
 let add_class_scope scope cl = 
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
-
-
-(* Temporary compatibility *)
-
-let translate_distfix _ = failwith "No more v7 support 1"
-let add_distfix _ = failwith "No more v7 support 2"
-let add_tactic_grammar = add_tactic_notation
-let add_grammar_obj _ = failwith "No more v7 support 4"
-let add_syntax_obj _ = failwith "No more v7 support 5"
-
-let add_syntax_extension local mv _ = add_syntax_extension local (out_some mv)
-let add_notation local c x _ sc = add_notation local c (out_some x) sc
-let add_infix local x pr _ sc = add_infix local x pr sc
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 243b6345fd..869ba00d0f 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -19,38 +19,27 @@ open Notation
 open Topconstr
 (*i*)
 
-(* Adding grammar and pretty-printing objects in the environment *)
+(* Adding parsing and pretty-printing rules in the environment *)
 
-val add_syntax_obj : string -> raw_syntax_entry list -> unit
-
-val add_grammar_obj : string -> raw_grammar_entry list -> unit
 val add_token_obj : string -> unit
-val add_tactic_grammar : 
-  int * (string * grammar_production list * raw_tactic_expr) list -> unit
+
+val add_tactic_notation : 
+  int * grammar_production list * raw_tactic_expr -> unit
 
 val add_infix : locality_flag -> (string * syntax_modifier list) ->
-  reference -> (string * syntax_modifier list) option ->
-    scope_name option -> unit
-val add_distfix : locality_flag ->
-  grammar_associativity -> precedence -> string -> reference
-    -> scope_name option -> unit
-val translate_distfix : grammar_associativity -> string -> reference ->
-  Gramext.g_assoc * string * constr_expr
+  reference -> scope_name option -> unit
 
 val add_delimiters : scope_name -> string -> unit
 val add_class_scope : scope_name -> Classops.cl_typ -> unit
 
-val add_notation : locality_flag -> constr_expr
-  -> (string * syntax_modifier list) option
-  -> (string * syntax_modifier list) option
-      -> scope_name option -> unit
+val add_notation : locality_flag -> constr_expr ->
+  (string * syntax_modifier list) -> scope_name option -> unit
 
-val add_notation_interpretation : string -> Constrintern.implicits_env
-  -> constr_expr -> scope_name option -> unit
+val add_notation_interpretation : string -> Constrintern.implicits_env ->
+  constr_expr -> scope_name option -> unit
 
-val add_syntax_extension : locality_flag
-  -> (string * syntax_modifier list) option
-  -> (string * syntax_modifier list) option -> unit
+val add_syntax_extension : 
+  locality_flag -> (string * syntax_modifier list) -> unit
 
 val print_grammar : string -> string -> unit
 
@@ -60,4 +49,4 @@ val merge_modifiers : Gramext.g_assoc option -> int option ->
 val interp_infix_modifiers : syntax_modifier list ->
   Gramext.g_assoc option * precedence option * bool * string located option
 
-val standardise_locatable_notation : string -> string
+val standardize_locatable_notation : string -> string
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a93e6fd5e6..fb9bb44967 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -280,10 +280,6 @@ let print_located_module r =
 (**********)
 (* Syntax *)
 
-let vernac_syntax = Metasyntax.add_syntax_obj
-
-let vernac_grammar = Metasyntax.add_grammar_obj
-
 let vernac_syntax_extension = Metasyntax.add_syntax_extension
 
 let vernac_delimiters = Metasyntax.add_delimiters
@@ -298,8 +294,6 @@ let vernac_arguments_scope qid scl =
 
 let vernac_infix = Metasyntax.add_infix
 
-let vernac_distfix = Metasyntax.add_distfix
-
 let vernac_notation = Metasyntax.add_notation
 
 (***********)
@@ -974,7 +968,7 @@ let vernac_locate = function
   | LocateFile f -> locate_file f
   | LocateNotation ntn ->
       ppnl (Notation.locate_notation (Constrextern.without_symbols pr_rawterm)
-	(Metasyntax.standardise_locatable_notation ntn))
+	(Metasyntax.standardize_locatable_notation ntn))
 
 (********************)
 (* Proof management *)
@@ -1108,19 +1102,14 @@ let interp c = match c with
   | (VernacV7only _ | VernacV8only _) -> assert false
 
   (* Syntax *)
-  | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel
-  | VernacTacticGrammar (n,al) -> Metasyntax.add_tactic_grammar (n,al)
-  | VernacGrammar (univ,al) -> vernac_grammar univ al
-  | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8
+  | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e)
+  | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
   | VernacOpenCloseScope sc -> vernac_open_close_scope sc
   | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
-  | VernacInfix (local,mv,qid,mv8,sc) -> vernac_infix local mv qid mv8 sc
-  | VernacDistfix (local,assoc,n,inf,qid,sc) -> 
-      vernac_distfix local assoc n inf qid sc
-  | VernacNotation (local,c,infpl,mv8,sc) ->
-      vernac_notation local c infpl mv8 sc
+  | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc
+  | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
 
   (* Gallina *)
   | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e62288d16d..ab05f7d0df 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -172,25 +172,17 @@ type vernac_expr =
   | VernacVar of lident
 
   (* Syntax *) 
-  | VernacGrammar of lstring * raw_grammar_entry list
-  | VernacTacticGrammar of int *
-      (lstring * grammar_production list * raw_tactic_expr) list
-  | VernacSyntax of lstring * raw_syntax_entry list
-  | VernacSyntaxExtension of locality_flag *
-      (lstring * syntax_modifier list) option 
-      * (lstring * syntax_modifier list) option
-  | VernacDistfix of locality_flag *
-      grammar_associativity * precedence * lstring * lreference *
-      scope_name option
+  | VernacTacticNotation of int * grammar_production list * raw_tactic_expr
+  | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * lstring
   | VernacBindScope of scope_name * class_rawexpr list
   | VernacArgumentsScope of lreference * scope_name option list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
-      lreference * (lstring * syntax_modifier list) option * scope_name option
+      lreference * scope_name option
   | VernacNotation of
-      locality_flag * constr_expr * (lstring * syntax_modifier list) option *
-      (lstring * syntax_modifier list) option * scope_name option
+      locality_flag * constr_expr * (lstring * syntax_modifier list) *
+      scope_name option
 
   (* Gallina *)
   | VernacDefinition of definition_kind * lident * definition_expr *