Ajout "at next level" dans Notation

Mise en place structure pour définir un objet en même temps que sa notation


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

6 files changed, 99 insertions, 62 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 076f7f026c..6a557f368c 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -24,14 +24,20 @@ type production_position =
   | BorderProd of bool * Gramext.g_assoc option  (* true=left; false=right *)
   | InternalProd
 
-type 'pos constr_entry_key =
+type production_level =
+  | NextLevel
+  | NumLevel of int
+
+type ('lev,'pos) constr_entry_key =
   | ETIdent | ETReference | ETBigint
-  | ETConstr of (int * 'pos)
+  | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
 
-type constr_production_entry = production_position constr_entry_key
-type constr_entry = unit constr_entry_key
+type constr_production_entry =
+    (production_level,production_position) constr_entry_key
+type constr_entry = (int,unit) constr_entry_key
+type simple_constr_production_entry = (production_level,unit) constr_entry_key
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
@@ -80,10 +86,10 @@ let act_of_ast vars = function
 let to_act_check_vars = act_of_ast
 
 type syntax_modifier =
-  | SetItemLevel of string list * int
+  | SetItemLevel of string list * production_level
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
-  | SetEntryType of string * constr_entry
+  | SetEntryType of string * simple_constr_production_entry
   | SetOnlyParsing
 
 type nonterm =
@@ -162,44 +168,50 @@ let rename_command_entry nt =
 
 (* This translates constr0, constr1, ... level into camlp4 levels of constr *)
 
-let explicitize_prod_entry pos univ nt =
+let explicitize_prod_entry inj pos univ nt =
   if univ = "prim" & nt = "var" then ETIdent else
   if univ = "prim" & nt = "bigint" then ETBigint else
   if univ <> "constr" then ETOther (univ,nt) else
   match nt with
-  | "constr0" -> ETConstr (0,pos)
-  | "constr1" -> ETConstr (1,pos)
-  | "constr2" -> ETConstr (2,pos)
-  | "constr3" -> ETConstr (3,pos)
-  | "lassoc_constr4" -> ETConstr (4,pos)
-  | "constr5" -> ETConstr (5,pos)
-  | "constr6" -> ETConstr (6,pos)
-  | "constr7" -> ETConstr (7,pos)
-  | "constr8" -> ETConstr (8,pos)
-  | "constr" when !Options.v7 -> ETConstr (8,pos)
-  | "constr9" -> ETConstr (9,pos)
-  | "constr10" | "lconstr" -> ETConstr (10,pos)
+  | "constr0" -> ETConstr (inj 0,pos)
+  | "constr1" -> ETConstr (inj 1,pos)
+  | "constr2" -> ETConstr (inj 2,pos)
+  | "constr3" -> ETConstr (inj 3,pos)
+  | "lassoc_constr4" -> ETConstr (inj 4,pos)
+  | "constr5" -> ETConstr (inj 5,pos)
+  | "constr6" -> ETConstr (inj 6,pos)
+  | "constr7" -> ETConstr (inj 7,pos)
+  | "constr8" -> ETConstr (inj 8,pos)
+  | "constr" when !Options.v7 -> ETConstr (inj 8,pos)
+  | "constr9" -> ETConstr (inj 9,pos)
+  | "constr10" | "lconstr" -> ETConstr (inj 10,pos)
   | "pattern" -> ETPattern
   | "ident" -> ETIdent
   | "global" -> ETReference
   | _ -> ETOther (univ,nt)
 
-let explicitize_entry = explicitize_prod_entry ()
+let explicitize_entry = explicitize_prod_entry (fun x -> x) ()
 
 (* Express border sub entries in function of the from level and an assoc *)
 (* 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
+  let t = explicitize_prod_entry (fun x -> NumLevel x) pos univ en in
   match from with
     | ETConstr (from,()) ->
 	(match t with
-	  | ETConstr (n,BorderProd (left,None)) when (n=from & left) ->
+	  | ETConstr (n,BorderProd (left,None))
+              when (n=NumLevel from & left) ->
 	      ETConstr (n,BorderProd (left,Some Gramext.LeftA))
-	  | ETConstr (n,BorderProd (left,None)) when (n=from-1 & not left) ->
-	      ETConstr (n+1,BorderProd (left,Some Gramext.LeftA))
-	  | ETConstr (n,BorderProd (left,None)) when (n=from-1 & left) ->
-	      ETConstr (n+1,BorderProd (left,Some Gramext.RightA))
-	  | ETConstr (n,BorderProd (left,None)) when (n=from & not left) ->
+	  | ETConstr (NumLevel n,BorderProd (left,None))
+              when (n=from-1 & not left) ->
+	      ETConstr
+                (NumLevel (n+1),BorderProd (left,Some Gramext.LeftA))
+	  | ETConstr (NumLevel n,BorderProd (left,None))
+              when (n=from-1 & left) ->
+	      ETConstr
+                (NumLevel (n+1),BorderProd (left,Some Gramext.RightA))
+	  | ETConstr (n,BorderProd (left,None))
+              when (n=NumLevel from & not left) ->
 	      ETConstr (n,BorderProd (left,Some Gramext.RightA))
 	  | t -> t)
     | _ -> t
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 808e50158b..ef685ffb16 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -25,14 +25,20 @@ type production_position =
   | BorderProd of bool * Gramext.g_assoc option  (* true=left; false=right *)
   | InternalProd
 
-type 'pos constr_entry_key =
+type production_level =
+  | NextLevel
+  | NumLevel of int
+
+type ('lev,'pos) constr_entry_key =
   | ETIdent | ETReference | ETBigint
-  | ETConstr of (int * 'pos)
+  | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
 
-type constr_production_entry = production_position constr_entry_key
-type constr_entry = unit constr_entry_key
+type constr_production_entry =
+    (production_level,production_position) constr_entry_key
+type constr_entry = (int,unit) constr_entry_key
+type simple_constr_production_entry = (production_level,unit) constr_entry_key
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
@@ -68,10 +74,10 @@ val set_constr_globalizer :
   (entry_context -> constr_expr -> constr_expr) -> unit
 
 type syntax_modifier =
-  | SetItemLevel of string list * int
+  | SetItemLevel of string list * production_level
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
-  | SetEntryType of string * constr_entry
+  | SetEntryType of string * simple_constr_production_entry
   | SetOnlyParsing
 
 type nonterm =
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 3db24bcd12..13d4a623bb 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -214,7 +214,7 @@ END
 (* automatic translation of levels *)
 let adapt_level n = n*10
 let map_modl = function
-  | SetItemLevel(ids,n) -> SetItemLevel(ids,adapt_level n)
+  | SetItemLevel(ids,NumLevel n) -> SetItemLevel(ids,NumLevel (adapt_level n))
   | SetLevel n -> SetLevel(adapt_level n)
   | m -> m
 	  
@@ -305,11 +305,14 @@ GEXTEND Gram
   locality:
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
+  level:
+    [ [ IDENT "level"; n = natural -> NumLevel n
+      | IDENT "next"; IDENT "level" -> NextLevel ] ]
+  ;
   syntax_modifier:
-    [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> 
-        SetItemLevel ([x],n)
-      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; IDENT "level";
-        n = natural -> SetItemLevel (x::l,n)
+    [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev)
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; lev = level ->
+          SetItemLevel (x::l,lev)
       | IDENT "at"; IDENT "level"; n = natural -> SetLevel n
       | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2d1fcdd306..5b88cee39e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -216,8 +216,9 @@ GEXTEND Gram
           (id,c,lc) ] ]
   ;
   oneind:
-    [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr; ":=";
-	lc = constructor_list -> (id,indpar,c,lc) ] ]
+    [ [ ntn = OPT [ ntn = STRING; ":=" -> (ntn,None) ];
+        id = base_ident; indpar = simple_binders_list; ":"; c = constr; ":=";
+	lc = constructor_list -> (id,ntn,indpar,c,lc) ] ]
   ;
   simple_binders_list:
     [ [ bl = ne_simple_binders_list -> bl
@@ -298,7 +299,7 @@ GEXTEND Gram
   gallina_ext:
     [ [ IDENT "Mutual"; bl = ne_simple_binders_list ; f = finite_token;
         indl = block_old_style ->
-	  let indl' = List.map (fun (id,ar,c) -> (id,bl,ar,c)) indl in
+	  let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
 	  VernacInductive (f,indl')
       | record_token; oc = opt_coercion; name = base_ident;
 	ps = simple_binders_list; ":";
@@ -316,7 +317,7 @@ GEXTEND Gram
       | IDENT "Scheme"; l = schemes -> VernacScheme l
       | f = finite_token; s = csort; id = base_ident;
 	indpar = simple_binders_list; ":="; lc = constructor_list -> 
-          VernacInductive (f,[id,indpar,s,lc]) ] ]
+          VernacInductive (f,[id,None,indpar,s,lc]) ] ]
   ;
   csort:
     [ [ s = sort -> CSort (loc,s) ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 0e9e8dabbd..4a6d3ca69d 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -103,7 +103,7 @@ GEXTEND Gram
 	  test_plurial_form bl;
 	  VernacAssumption (stre, bl)
       (* Gallina inductive declarations *)
-      | OPT[IDENT "Mutual"]; f = finite_token;
+      | (* Non port�� (?) : OPT[IDENT "Mutual"];*) f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
           VernacInductive (f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -118,9 +118,11 @@ GEXTEND Gram
 	s = lconstr; ":="; cstr = OPT base_ident; "{";
         fs = LIST0 local_decl_expr; "}" ->
 	  VernacRecord ((oc,name),ps,s,cstr,fs)
+(* Non port�� ?
       | f = finite_token; s = csort; id = base_ident;
         indpar = LIST0 simple_binder; ":="; lc = constructor_list -> 
-          VernacInductive (f,[id,indpar,s,lc])
+          VernacInductive (f,[id,None,indpar,s,lc])
+*)
     ] ]
   ;
   thm_token:
@@ -171,17 +173,20 @@ GEXTEND Gram
   ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; ":=";
-	lc = constructor_list -> (id,indpar,c,lc) ] ]
+    [ [ ntn = OPT [ ntn = STRING -> (ntn,None) ];
+        id = base_ident; indpar = LIST0 simple_binder; ":"; c = lconstr; ":=";
+	lc = constructor_list -> (id,ntn,indpar,c,lc) ] ]
   ;
   constructor_list:
     [ [ "|"; l = LIST1 constructor_binder SEP "|" -> l
       | l = LIST1 constructor_binder SEP "|" -> l
       |  -> [] ] ]
   ;
+(*
   csort:
     [ [ s = sort -> CSort (loc,s) ] ]
   ;
+*)
   opt_coercion:
     [ [ ">" -> true
       |  -> false ] ]
@@ -699,11 +704,14 @@ GEXTEND Gram
   [ [ univ = IDENT ->
         set_default_action_parser (parser_type_from_name univ); univ ] ]
   ;
+  level:
+    [ [ IDENT "level"; n = natural -> NumLevel n
+      | IDENT "next"; IDENT "level" -> NextLevel ] ]
+  ;
   syntax_modifier:
-    [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> 
-        SetItemLevel ([x],n)
-      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; IDENT "level";
-        n = natural -> SetItemLevel (x::l,n)
+    [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev)
+      | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; 
+        lev = level -> SetItemLevel (x::l,lev)
       | IDENT "at"; IDENT "level"; n = natural -> SetLevel n
       | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d160734ea1..39047e6880 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -542,22 +542,27 @@ let camlp4_assoc = function
          s.t. if [cur] is set then [n] is the same as the [from] level *)
 let adjust_level assoc from = function
 (* Associativity is None means force the level *)
-  | (n,BorderProd (_,None)) -> Some (Some (n,true))
+  | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
 (* Compute production name on the right side *)
   (* If NonA or LeftA on the right-hand side, set to NEXT *)
-  | (n,BorderProd (false,Some (Gramext.NonA|Gramext.LeftA))) -> Some None
+  | (NumLevel n,BorderProd (false,Some (Gramext.NonA|Gramext.LeftA))) ->
+      Some None
   (* If RightA on the right-hand side, set to the explicit (current) level *)
-  | (n,BorderProd (false,Some Gramext.RightA)) -> Some (Some (n,true))
+  | (NumLevel n,BorderProd (false,Some Gramext.RightA)) ->
+      Some (Some (n,true))
 (* Compute production name on the left side *)
   (* If NonA on the left-hand side, adopt the current assoc ?? *)
-  | (n,BorderProd (true,Some Gramext.NonA)) -> None
+  | (NumLevel n,BorderProd (true,Some Gramext.NonA)) -> None
   (* If the expected assoc is the current one, set to SELF *)
-  | (n,BorderProd (true,Some a)) when a = camlp4_assoc assoc -> None
+  | (NumLevel n,BorderProd (true,Some a)) when a = camlp4_assoc assoc ->
+      None
   (* Otherwise, force the level, n or n-1, according to expected assoc *)
-  | (n,BorderProd (true,Some a)) ->
+  | (NumLevel n,BorderProd (true,Some a)) ->
       if a = Gramext.LeftA then Some (Some (n,true)) else Some None
+  (* None means NEXT *)
+  | (NextLevel,_) -> Some None
 (* Compute production name elsewhere *)
-  | (n,InternalProd) ->
+  | (NumLevel n,InternalProd) ->
       match from with
 	| ETConstr (p,()) when p = n+1 -> Some None
 	| ETConstr (p,()) -> Some (Some (n,n=p))
@@ -609,7 +614,7 @@ let compute_entry allow_create adjust = function
 (* This computes the name of the level where to add a new rule *)
 let get_constr_entry en =
   match en with
-      ETConstr(200,_) when not !Options.v7 ->
+      ETConstr(200,()) when not !Options.v7 ->
         snd (get_entry (get_univ "constr") "binder_constr"),
         None,
         false
@@ -620,7 +625,7 @@ let get_constr_entry en =
 let get_constr_production_entry ass from en =
   (* first 2 cases to help factorisation *)
   match en with
-    | ETConstr (10,q) when !Options.v7 ->
+    | ETConstr (NumLevel 10,q) when !Options.v7 ->
         weaken_entry Constr.lconstr, None, false
 (*
     | ETConstr (8,q) when !Options.v7 ->
@@ -643,9 +648,9 @@ let constr_prod_level assoc cur lev =
 
 let is_self from e =
   match from, e with
-      ETConstr(n,_), ETConstr(n',
+      ETConstr(n,()), ETConstr(NumLevel n',
         BorderProd(false, _ (* Some(Gramext.NonA|Gramext.LeftA) *))) -> false
-    | ETConstr(n,_), ETConstr(n',BorderProd(true,_)) -> n=n'
+    | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(true,_)) -> n=n'
     | (ETIdent,ETIdent | ETReference, ETReference | ETBigint,ETBigint
       | ETPattern, ETPattern) -> true
     | ETOther(s1,s2), ETOther(s1',s2') -> s1=s1' & s2=s2'
@@ -653,7 +658,7 @@ let is_self from e =
 
 let is_binder_level from e =
   match from, e with
-      ETConstr(200,_), ETConstr(200,_) -> not !Options.v7
+      ETConstr(200,()), ETConstr(NumLevel 200,_) -> not !Options.v7
     | _ -> false
 
 let symbol_of_production assoc from typ =
@@ -667,3 +672,5 @@ let symbol_of_production assoc from typ =
       | (eobj,Some None,_) -> Gramext.Snext
       | (eobj,Some (Some (lev,cur)),_) -> 
           Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level assoc cur lev)
+
+