Meilleure factorisation des entrées NEXT internes

Nouvelle entrée "annot" pour contourner le conflit entre ">" et les
annotations entre piquants


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

8 files changed, 89 insertions, 41 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 7603bde18..67aacdd56 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -78,13 +78,13 @@ let find_position other assoc lev =
         | (p,_ as pa)::l when p > n -> pa :: add_level pa l
         | (p,a as pa)::l as l' when p = n ->
 	    if admissible_assoc (a,assoc) then raise (Found a);
-	    (* Maybe this was (p,Left) and p occurs a second time *)
+	    (* Maybe this was (p,Right) and p occurs a second time *)
 	    if a = Gramext.LeftA then
 	      match l with
 		| (p,a)::_ as l' when p = n -> raise (Found a)
-		| _ -> after := pa; (n,create_assoc assoc)::l'
+		| _ -> after := pa; pa::(n,create_assoc assoc)::l
 	    else
-	      (* This was not (p,LeftA) hence assoc is LeftA *)
+	      (* This was not (p,LeftA) hence assoc is RightA *)
 	      (after := q; (n,create_assoc assoc)::l')
 	| l ->
 	    after := q; (n,create_assoc assoc)::l
@@ -189,16 +189,16 @@ let make_cases_pattern_act
  * annotations are added when type-checking the command, function
  * Extend.of_ast) *)
 
-let rec build_prod_item univ assoc = function
-  | ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc s)
-  | ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc s)
-  | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ assoc s)
-  | ProdPrimitive typ -> symbol_of_production assoc typ
+let rec build_prod_item univ assoc fromlevel = function
+  | ProdList0 s -> Gramext.Slist0 (build_prod_item univ assoc fromlevel s)
+  | ProdList1 s -> Gramext.Slist1 (build_prod_item univ assoc fromlevel s)
+  | ProdOpt s   -> Gramext.Sopt   (build_prod_item univ assoc fromlevel s)
+  | ProdPrimitive typ -> symbol_of_production assoc fromlevel typ
 
-let symbol_of_prod_item univ assoc = function
+let symbol_of_prod_item univ assoc from = function
   | Term tok -> (Gramext.Stoken tok, None)
   | NonTerm (nt, ovar) ->
-      let eobj = build_prod_item univ assoc nt in
+      let eobj = build_prod_item univ assoc from nt in
       (eobj, ovar)
 
 let coerce_to_id = function
@@ -278,7 +278,7 @@ let subst_constr_expr a loc subs =
   in subst a
 
 let make_rule univ assoc etyp rule =
-  let pil = List.map (symbol_of_prod_item univ assoc) rule.gr_production in
+  let pil = List.map (symbol_of_prod_item univ assoc etyp) rule.gr_production in
   let (symbs,ntl) = List.split pil in
   let act = match etyp with
     | ETPattern ->
@@ -299,8 +299,7 @@ let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) =
   grammar_extend te pos [(name, p4ass, rules)]
 
 (* Defines new entries. If the entry already exists, check its type *)
-let define_entry univ {ge_name=n; gl_assoc=ass; gl_rules=rls} =
-  let typ = explicitize_entry (fst univ) n in
+let define_entry univ {ge_name=typ; gl_assoc=ass; gl_rules=rls} =
   let e,lev,keepassoc = get_constr_entry typ in
   let pos,p4ass,name = find_position keepassoc ass lev in
   (e,typ,pos,name,ass,p4ass,rls)
@@ -331,9 +330,9 @@ let make_gen_act f pil =
         Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
   make [] (List.rev pil)
 
-let extend_constr entry (level,assoc,keepassoc) make_act pt =
+let extend_constr entry (n,level,assoc,keepassoc) make_act pt =
   let univ = get_univ "constr" in
-  let pil = List.map (symbol_of_prod_item univ assoc) pt in
+  let pil = List.map (symbol_of_prod_item univ assoc n) pt in
   let (symbs,ntl) = List.split pil in
   let act = make_act ntl in
   let pos,p4assoc,name = find_position keepassoc assoc level in
@@ -342,14 +341,14 @@ let extend_constr entry (level,assoc,keepassoc) make_act pt =
 let extend_constr_notation (n,assoc,ntn,rule) =
   let mkact loc env = CNotation (loc,ntn,List.map snd env) in
   let (e,level,keepassoc) = get_constr_entry (ETConstr (n,())) in
-  extend_constr e (level,assoc,keepassoc) (make_act mkact) rule
+  extend_constr e (ETConstr(n,()),level,assoc,keepassoc) (make_act mkact) rule
 
 let extend_constr_delimiters (sc,rule,pat_rule) =
   let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr Constr.constr (Some 0,Some Gramext.NonA,false)
+  extend_constr Constr.constr (ETConstr(0,()),Some 0,Some Gramext.NonA,false)
     (make_act mkact) rule;
   let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr Constr.pattern (None,None,false)
+  extend_constr Constr.pattern (ETPattern,None,None,false)
     (make_cases_pattern_act mkact) pat_rule
 
 (* These grammars are not a removable *)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index a49ec01b0..14a33a656 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -50,7 +50,7 @@ type grammar_rule = {
   gr_action : constr_expr }
 
 type grammar_entry = { 
-  ge_name : string;
+  ge_name : constr_entry;
   gl_assoc : Gramext.g_assoc option;
   gl_rules : grammar_rule list }
 
@@ -189,7 +189,7 @@ let explicitize_entry = explicitize_prod_entry ()
 (* We're cheating: not necessarily the same assoc on right and left *)
 let clever_explicitize_prod_entry pos univ from en =
   let t = explicitize_prod_entry pos univ en in
-  match explicitize_entry univ from with
+  match from with
     | ETConstr (from,()) ->
 	(match t with
 	  | ETConstr (n,BorderProd (left,None)) when (n=from & left) ->
@@ -255,9 +255,10 @@ let clever_assoc ass g =
   else ass
 
 let gram_entry univ (nt, ass, rl) =
-  let l = List.map (gram_rule (univ,nt)) rl in
+  let from = explicitize_entry (snd univ) nt in
+  let l = List.map (gram_rule (univ,from)) rl in
   let ass = List.fold_left clever_assoc ass l in
-  { ge_name = nt;
+  { ge_name = from;
     gl_assoc = ass;
     gl_rules = l }
 
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 7398c7903..808e50158 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -51,7 +51,7 @@ type grammar_rule = {
   gr_action : constr_expr }
 
 type grammar_entry = { 
-  ge_name : string;
+  ge_name : constr_entry;
   gl_assoc : Gramext.g_assoc option;
   gl_rules : grammar_rule list }
 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 9ef698ad1..c9f753a38 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -53,10 +53,7 @@ GEXTEND Gram
       | IDENT "Dump"; IDENT "Universes"; fopt = OPT STRING ->
 	  VernacPrint (PrintUniverses fopt)
 
-      | IDENT "Locate"; qid = global -> VernacLocate (LocateTerm qid)
-      | IDENT "Locate"; IDENT "File"; f = STRING -> VernacLocate (LocateFile f)
-      | IDENT "Locate"; IDENT "Library"; qid = global ->
-	  VernacLocate (LocateLibrary  qid)
+      | IDENT "Locate"; l = locatable -> VernacLocate l
 
       (* Managing load paths *)
       | IDENT "Add"; IDENT "LoadPath"; dir = STRING; alias = as_dirpath ->
@@ -177,6 +174,12 @@ GEXTEND Gram
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
       | IDENT "Scope"; s = IDENT -> PrintScope s ] ]
   ;
+  locatable:
+    [ [ qid = global -> LocateTerm qid
+      | IDENT "File"; f = STRING -> LocateFile f
+      | IDENT "Library"; qid = global -> LocateLibrary  qid
+      | s = STRING -> LocateNotation s ] ]
+  ;
   option_value:
     [ [ n  = integer   -> IntValue n
       | s  = STRING    -> StringValue s ] ]
@@ -263,7 +266,11 @@ GEXTEND Gram
       | IDENT "only"; IDENT "parsing" -> SetOnlyParsing ] ]
   ;
   syntax_extension_type:
-    [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference ] ]
+    [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
+      | IDENT "annot" ->
+	  if !Options.v7 <> true then Util.error "annot not allowed in new syntax";
+	  ETOther ("constr","annot")
+    ] ]
   ;
   opt_scope:
     [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ]
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 647dc0a25..62ee20cad 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -53,13 +53,13 @@ GEXTEND Gram
     [ [ leqn = LIST1 equation SEP "|" -> leqn ] ]
   ;
   constr: LEVEL "1"
-    [ [ "<"; p = lconstr; ">"; "Cases"; lc = LIST1 constr; "of";
+    [ [ "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of";
         OPT "|"; eqs = ne_eqn_list; "end" ->
 	  CCases (loc, Some p, lc, eqs)
       | "Cases"; lc = LIST1 constr; "of";
 	OPT "|"; eqs = ne_eqn_list; "end" ->
 	  CCases (loc, None, lc, eqs)
-      | "<"; p = lconstr; ">"; "Cases"; lc = LIST1 constr; "of"; "end" ->
+      | "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of"; "end" ->
 	  CCases (loc, Some p, lc, [])
       | "Cases"; lc = LIST1 constr; "of"; "end" -> 
 	  CCases (loc, None, lc, []) ] ]
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e73cc7894..a39601099 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -79,7 +79,7 @@ let test_ident_colon =
         | _ -> raise Stream.Failure)
 
 GEXTEND Gram
-  GLOBAL: constr9 lconstr constr sort global constr_pattern Constr.ident
+  GLOBAL: constr9 lconstr constr sort global constr_pattern Constr.ident annot
           (*ne_name_comma_list*);
   Constr.ident:
     [ [ id = Prim.ident -> id
@@ -108,10 +108,10 @@ GEXTEND Gram
     [ "top" RIGHTA
       [ c1 = constr; "->"; c2 = constr -> CArrow (loc, c1, c2) ]
     | "1" RIGHTA
-      [ "<"; p = lconstr; ">"; IDENT "Match"; c = constr; "with";
+      [ "<"; p = annot; ">"; IDENT "Match"; c = constr; "with";
         cl = LIST0 constr; "end" ->
 	  COrderedCase (loc, MatchStyle, Some p, c, cl)
-      | "<"; p = lconstr; ">"; IDENT "Case"; c = constr; "of";
+      | "<"; p = annot; ">"; IDENT "Case"; c = constr; "of";
         cl = LIST0 constr; "end" ->
 	  COrderedCase (loc, RegularStyle, Some p, c, cl)
       | IDENT "Case"; c = constr; "of"; cl = LIST0 constr; "end" ->
@@ -130,13 +130,13 @@ GEXTEND Gram
         IDENT "then"; c2 = constr;
         IDENT "else"; c3 = constr LEVEL "top" ->
 	  COrderedCase (loc, IfStyle, None, c1, [c2; c3])
-      | "<"; p = lconstr; ">";
+      | "<"; p = annot; ">";
         IDENT "let"; "("; b = ne_name_comma_list; ")"; "="; c = constr; 
         "in"; c1 = constr LEVEL "top" ->
           (* TODO: right loc *)
 	  COrderedCase (loc, LetStyle, Some p, c,
             [CLambdaN (loc, [b, CHole loc], c1)])
-      | "<"; p = lconstr; ">";
+      | "<"; p = annot; ">";
         IDENT "if"; c1 = constr;
         IDENT "then"; c2 = constr; 
         IDENT "else"; c3 = constr LEVEL "top" ->
@@ -199,6 +199,39 @@ GEXTEND Gram
     [ RIGHTA [ c1 = constr -> c1
       | c1 = constr; "::"; c2 = constr -> CCast (loc, c1, c2) ] ]
   ;
+  (* annot and product_annot_tail are hacks to forbid concrete syntax *)
+  (* ">" (e.g. for gt, Zgt, ...) in annotations *)
+  annot:
+    [ RIGHTA
+      [ bll = binders; c = annot -> abstract_constr loc c bll 
+      | "("; lc1 = lconstr; ":"; c = constr; (bl,body) = product_annot_tail ->
+          let id = coerce_to_name lc1 in
+	  CProdN (loc, ([id], c)::bl, body)
+      | "("; lc1 = lconstr; ","; lc2 = lconstr; ":"; c = constr;
+        (bl,body) = product_annot_tail ->
+          let id1 = coerce_to_name lc1 in
+          let id2 = coerce_to_name lc2 in
+	  CProdN (loc, ([id1; id2], c)::bl, body)
+      | "("; lc1 = lconstr; ","; lc2 = lconstr; ",";
+        idl = ne_name_comma_list; ":"; c = constr;
+	(bl,body) = product_annot_tail ->
+          let id1 = coerce_to_name lc1 in
+          let id2 = coerce_to_name lc2 in
+	  CProdN (loc, (id1::id2::idl, c)::bl, body)
+      | "("; lc1 = lconstr; ")" -> lc1
+      | c1 = annot; "->"; c2 = annot -> CArrow (loc, c1, c2)
+      | c1 = SELF; "=="; c2 = NEXT -> CNotation (loc, "_ == _", [c1;c2])
+      | c1 = SELF; "="; c2 = NEXT -> CNotation (loc, "_ = _", [c1;c2])
+      | c = constr LEVEL "4L" -> c
+      ] ]
+  ;
+  product_annot_tail:
+    [ [ ";"; idl = ne_name_comma_list; ":"; c = constr;
+        (bl,c2) = product_annot_tail -> ((idl, c)::bl, c2)
+      | ";"; idl = ne_name_comma_list; (bl,c2) = product_annot_tail ->
+          ((idl, CHole (fst (List.hd idl)))::bl, c2)
+      | ")"; c = annot -> ([], c) ] ]
+  ;
   ne_name_comma_list:
     [ [ nal = LIST1 name SEP "," -> nal ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 96b358402..33948d83b 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -351,6 +351,7 @@ module Constr =
     let global = make_gen_entry uconstr rawwit_ref "global"
     let sort = make_gen_entry uconstr rawwit_sort "sort"
     let pattern = Gram.Entry.create "constr:pattern"
+    let annot = Gram.Entry.create "constr:annot"
     let constr_pattern = gec_constr "constr_pattern"
   end
 
@@ -506,7 +507,7 @@ let camlp4_assoc = function
   | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA 
   | None | Some Gramext.LeftA -> Gramext.LeftA
 
-let adjust_level assoc = function
+let adjust_level assoc from = function
   (* If NonA on the right-hand side, set to NEXT *)
   | (n,BorderProd (false,Some Gramext.NonA)) -> Some None
   (* If NonA on the left-hand side, adopt the current assoc ?? *)
@@ -520,7 +521,10 @@ let adjust_level assoc = function
       if (left & a = Gramext.LeftA) or ((not left) & a = Gramext.RightA)
       then Some (Some n) else Some (Some (n-1))
 (*  | (8,InternalProd) -> None (* Or (Some 8) for factorization ? *)*)
-  | (n,InternalProd) -> Some (Some n)
+  | (n,InternalProd) ->
+      match from with
+	| ETConstr (p,()) when p = n+1 -> Some None
+	| _ -> Some (Some n)
 
 let compute_entry allow_create adjust = function
   | ETConstr (10,_) -> weaken_entry Constr.lconstr, None, true
@@ -530,6 +534,8 @@ let compute_entry allow_create adjust = function
   | ETBigint -> weaken_entry Prim.bigint, None, false
   | ETReference -> weaken_entry Constr.global, None, false
   | ETPattern -> weaken_entry Constr.pattern, None, false
+  | ETOther ("constr","annot") -> 
+      weaken_entry Constr.annot, None, false
   | ETOther (u,n) ->
       let u = get_univ u in
       let e =
@@ -539,15 +545,16 @@ let compute_entry allow_create adjust = function
 
 let get_constr_entry = compute_entry true (fun (n,()) -> Some n)
 
-let get_constr_production_entry ass = compute_entry false (adjust_level ass)
+let get_constr_production_entry ass from =
+  compute_entry false (adjust_level ass from)
 
 let constr_prod_level = function
   | 8 -> "top"
   | 4 -> "4L"
   | n -> string_of_int n
 
-let symbol_of_production assoc typ =
-  match get_constr_production_entry assoc typ with
+let symbol_of_production assoc from typ =
+  match get_constr_production_entry assoc from typ with
     | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
     | (eobj,Some None,_) -> Gramext.Snext
     | (eobj,Some (Some lev),_) -> 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 4ea1c4e5b..b15046c29 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -35,7 +35,7 @@ val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
 val get_constr_entry :
   constr_entry -> grammar_object Gram.Entry.e * int option * bool
 
-val symbol_of_production : Gramext.g_assoc option -> 
+val symbol_of_production : Gramext.g_assoc option -> constr_entry ->
   constr_production_entry -> Token.t Gramext.g_symbol
 
 val grammar_extend :
@@ -136,6 +136,7 @@ module Constr :
     val global : reference Gram.Entry.e
     val sort : rawsort Gram.Entry.e
     val pattern : cases_pattern_expr Gram.Entry.e
+    val annot : constr_expr Gram.Entry.e
     val constr_pattern : constr_expr Gram.Entry.e
   end