Affinement de la gestion des niveaux toujours; type ETBigint

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

4 files changed, 69 insertions, 70 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index a7cfcc591e..f294f70799 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -37,49 +37,46 @@ let (grammar_state : all_grammar_command list ref) = ref []
 
 
 (**************************************************************************)
-let canonise_assoc = function
-  | None -> Gramext.LeftA (* camlp4 rule *)
-  | Some Gramext.NonA -> Gramext.RightA
-  | Some a -> a
-
 let assoc_level = function
   | Gramext.LeftA -> "L"
   | _ -> ""
 
-let constr_level assoc = function
-  | 8 -> assert (assoc <> Some Gramext.LeftA); "top"
-  | n -> (string_of_int n)^(assoc_level (canonise_assoc assoc))
+let constr_level = function
+  | 8,assoc -> assert (assoc <> Gramext.LeftA); "top"
+  | n,assoc -> (string_of_int n)^(assoc_level assoc)
 
 let constr_prod_level = function
   | 8 -> "top"
   | n -> string_of_int n
 
 let numeric_levels =
-  ref [8,Some Gramext.RightA; 1,Some Gramext.RightA; 0,Some Gramext.RightA]
+  ref [8,Gramext.RightA; 1,Gramext.RightA; 0,Gramext.RightA]
 
 (* At a same level, LeftA takes precedence over RightA and NoneA *)
 (* In case, several associativity exists for a level, we make two levels, *)
 (* first LeftA, then RightA and NoneA together *)
-exception Found of Gramext.g_assoc option
+exception Found of Gramext.g_assoc
+
+open Ppextend
 
-let eq_assoc a b = match (canonise_assoc a, canonise_assoc b) with
-  | Gramext.LeftA, Gramext.LeftA -> true
-  | Gramext.LeftA, _ -> false
-  | _, Gramext.LeftA -> false
+let admissible_assoc = function
+  | Gramext.LeftA, (Gramext.RightA | Gramext.NonA) -> false
+  | Gramext.RightA, Gramext.LeftA -> false
   | _ -> true
- 
-let find_position assoc = function
-  | None -> None, Some (canonise_assoc assoc)
+
+let find_position other assoc = function
+  | None -> None, (if other then assoc else None), None
   | Some n ->
-      if n = 8 & canonise_assoc assoc = Gramext.LeftA then 
+      let assoc = out_some assoc in
+      if n = 8 & assoc = Gramext.LeftA then 
 	error "Left associativity not allowed at level 8";
-      let after = ref (8,Some Gramext.RightA) in
+      let after = ref (8,Gramext.RightA) in
       let rec add_level q = function
         | (p,_ as pa)::l when p > n -> pa :: add_level pa l
         | (p,a as pa)::l as l' when p = n ->
-	    if eq_assoc a assoc then raise (Found a);
+	    if admissible_assoc (a,assoc) then raise (Found a);
 	    (* Maybe this was (p,Left) and p occurs a second time *)
-	    if canonise_assoc a = Gramext.LeftA then
+	    if a = Gramext.LeftA then
 	      match l with
 		| (p,a)::_ as l' when p = n -> raise (Found a)
 		| _ -> after := pa; (n,assoc)::l'
@@ -90,12 +87,14 @@ let find_position assoc = function
 	    after := q; (n,assoc)::l
       in
       try
-        numeric_levels := add_level (8,Some Gramext.RightA) !numeric_levels;
-        Some (Gramext.After (constr_level (snd !after) (fst !after))),
-	Some (canonise_assoc assoc)
+	(* Create the entry *)
+        numeric_levels := add_level (8,Gramext.RightA) !numeric_levels;
+        Some (Gramext.After (constr_level !after)),
+	Some assoc, Some (constr_level (n,assoc))
       with
-          Found a -> Some (Gramext.Level (constr_level a n)),
-	  Some (canonise_assoc a)
+          Found a ->
+	    (* Just inherit the existing associativity and name (None) *)
+	    Some (Gramext.Level (constr_level (n,a))), None, None
 
 (* Interpretation of the right hand side of grammar rules *)
 
@@ -147,6 +146,9 @@ let make_act f pil =
     | Some (p, ETIdent) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:identifier) ->
 	  make ((p,CRef (Ident (dummy_loc,v))) :: env) tl)
+    | Some (p, ETBigint) :: tl -> (* non-terminal *)
+        Gramext.action (fun (v:Bignat.bigint) ->
+	  make ((p,CNumeral (dummy_loc,v)) :: env) tl)
     | Some (p, ETPattern) :: tl -> 
 	failwith "Unexpected entry of type cases pattern" in
   make [] (List.rev pil)
@@ -160,7 +162,10 @@ let make_cases_pattern_act f pil =
     | Some (p, ETPattern) :: tl -> (* non-terminal *)
         Gramext.action (fun v -> make ((p,v) :: env) tl)
     | Some (p, ETReference) :: tl -> (* non-terminal *)
-        Gramext.action (fun v -> make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
+	Gramext.action (fun v -> make ((p,CPatAtom(dummy_loc,Some v)) :: env)
+	  tl)
+    | Some (p, ETBigint) :: tl -> (* non-terminal *)
+	Gramext.action (fun v -> make ((p,CPatNumeral(dummy_loc,v)) :: env) tl)
     | Some (p, (ETIdent | ETConstr _ | ETOther _)) :: tl ->
 	error "ident and constr entry not admitted in patterns cases syntax extensions" in
   make [] (List.rev pil)
@@ -210,17 +215,17 @@ let make_rule univ assoc etyp rule =
 
 (* Rules of a level are entered in reverse order, so that the first rules
    are applied before the last ones *)
-let extend_entry univ (te, etyp, pos, name, ass, rls) =
+let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) =
   let rules = List.rev (List.map (make_rule univ ass etyp) rls) in
-  grammar_extend te pos [(name, ass, rules)]
+  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 e,lev = get_constr_entry typ in
-  let pos,ass = find_position ass lev in
-  let name = option_app (constr_level ass) lev in
-  (e,typ,pos,name,ass,rls)
+  let other = match typ with ETOther _ -> true | _ -> false in
+  let pos,p4ass,name = find_position other ass lev in
+  (e,typ,pos,name,ass,p4ass,rls)
 
 (* Add a bunch of grammar rules. Does not check if it is well formed *)
 let extend_grammar_rules gram =
@@ -248,27 +253,24 @@ 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 pos (level,assoc) make_act pt =
+let extend_constr entry (level,assoc) make_act pt =
   let univ = get_univ "constr" in
   let pil = List.map (symbol_of_prod_item univ assoc) pt in
   let (symbs,ntl) = List.split pil in
   let act = make_act ntl in
-  grammar_extend entry pos [(level, assoc, [symbs, act])]
+  let pos,p4assoc,name = find_position false assoc level in
+  grammar_extend entry pos [(name, p4assoc, [symbs, act])]
 
 let extend_constr_notation (n,assoc,ntn,rule) =
   let mkact loc env = CNotation (loc,ntn,env) in
   let (e,level) = get_constr_entry (ETConstr (n,())) in
-  let pos,assoc = find_position assoc level in
-  extend_constr e pos (option_app (constr_level assoc) level,assoc) 
-    (make_act mkact) rule
+  extend_constr e (level,assoc) (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 (Gramext.Level "0"))
-    (None,None)
-    (make_act mkact) rule;
+  extend_constr Constr.constr (Some 0,Some Gramext.NonA) (make_act mkact) rule;
   let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr Constr.pattern None (None,None)
+  extend_constr Constr.pattern (None,None)
     (make_cases_pattern_act mkact) pat_rule
 
 (* These grammars are not a removable *)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index ae3561c1f9..c7ea8737fa 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -25,7 +25,7 @@ type production_position =
   | InternalProd
 
 type 'pos constr_entry_key =
-  | ETIdent | ETReference
+  | ETIdent | ETReference | ETBigint
   | ETConstr of (int * 'pos)
   | ETPattern
   | ETOther of string * string
@@ -158,6 +158,7 @@ let rename_command_entry nt =
 
 let explicitize_prod_entry 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)
@@ -238,18 +239,18 @@ let border = function
   | NonTerm (ProdPrimitive (ETConstr(_,BorderProd (_,a))),_) :: _ -> a
   | _ -> None
 
-let clever_assoc = function
+let clever_assoc ass = function
   | [g] when g.gr_production <> [] ->
       (match border g.gr_production, border (List.rev g.gr_production) with
-	  Some RightA, Some LeftA -> Some NonA
-	| a, b when a=b -> a
-	| Some LeftA, Some RightA -> Some LeftA (* since LR *)
-	| _ -> None)
-  | _ -> None
+	| Some LeftA, Some RightA -> ass (* Untractable; we cheat *)
+	| Some LeftA, _ -> Some LeftA
+	| _, Some RightA -> Some RightA
+	| _ -> Some NonA)
+  | _ -> ass
 
 let gram_entry univ (nt, ass, rl) =
   let l = List.map (gram_rule (univ,nt)) rl in
-  let ass = if ass = None then clever_assoc l else ass in
+  let ass = clever_assoc ass l in
   { ge_name = nt;
     gl_assoc = ass;
     gl_rules = l }
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 705fc88185..12d2ecc620 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -26,7 +26,7 @@ type production_position =
   | InternalProd
 
 type 'pos constr_entry_key =
-  | ETIdent | ETReference
+  | ETIdent | ETReference | ETBigint
   | ETConstr of (int * 'pos)
   | ETPattern
   | ETOther of string * string
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 0862c792de..e527fafd8c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -327,7 +327,7 @@ let string_of_assoc = function
   | Some(Gramext.LeftA) | None -> "LEFTA"
   | Some(Gramext.NonA) -> "NONA"
 
-let make_symbolic assoc n symbols etyps =
+let make_symbolic n symbols etyps =
   (n,List.map assoc_of_type etyps),
   (String.concat " " (List.flatten (List.map string_of_symbol symbols)))
 
@@ -446,6 +446,7 @@ let interp_syntax_modifiers =
   let rec interp assoc level etyps = function
     | [] ->
 	let n = match level with None -> 1 | Some n -> n in
+	let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
 	(assoc,n,etyps,!onlyparsing)
     | SetEntryType (s,typ) :: l ->
 	let id = id_of_string s in
@@ -486,25 +487,20 @@ let set_entry_type etyps (x,typ) =
 	  let assoc = if left then Gramext.LeftA else Gramext.RightA in
           ETConstr (n,BorderProd (left,Some assoc))
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
-      | (ETPattern | ETIdent | ETOther _ | ETReference as t), _ -> t
+      | (ETPattern | ETIdent | ETBigint | ETOther _ | ETReference as t), _ -> t
     with Not_found -> ETConstr typ
   in (x,typ)
 
-let collapse_assoc_left = function
-  | None | Some Gramext.LeftA -> Some Gramext.NonA
-  | a -> a
+let border = function
+  | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a
+  | _ -> None
 
-let collapse_assoc_right = function
-  | Some Gramext.RightA -> Some Gramext.NonA
-  | a -> a
-
-let is_border = function
-  | (_,ETConstr(_,BorderProd _)) :: _ -> true
-  | _ -> false
-
-let adjust_associativity typs assoc =
-  let assoc = if is_border typs then assoc else collapse_assoc_left assoc in
-  if is_border (List.rev typs) then assoc else collapse_assoc_right assoc 
+let recompute_assoc typs =
+  match border typs, border (List.rev typs) with
+    | Some Gramext.LeftA, Some Gramext.RightA -> assert false
+    | Some Gramext.LeftA, _ -> Some Gramext.LeftA
+    | _, Some Gramext.RightA -> Some Gramext.RightA
+    | _ -> Some Gramext.NonA
 
 let add_syntax_extension df modifiers =
   let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in
@@ -513,8 +509,8 @@ let add_syntax_extension df modifiers =
       (n,BorderProd(true,assoc)) (10,InternalProd) (n,BorderProd(false,assoc))
       [] (split df) in
   let typs = List.map (set_entry_type etyps) typs in
-  let assoc = adjust_associativity typs assoc in
-  let (prec,notation) = make_symbolic assoc n symbs typs in
+  let assoc = recompute_assoc typs in
+  let (prec,notation) = make_symbolic n symbs typs in
   let gram_rule = make_grammar_rule n assoc typs symbs notation in
   let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbs) in
   Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule))
@@ -596,9 +592,9 @@ let add_notation_in_scope df a modifiers sc toks =
   let etyps = merge_entry_types etyps' etyps in
 *)
   let typs = List.map (set_entry_type etyps) typs in
-  let assoc = adjust_associativity typs assoc in
+  let assoc = recompute_assoc typs in
   (* Declare the parsing and printing rules if not already done *)
-  let (prec,notation) = make_symbolic assoc n symbols typs in
+  let (prec,notation) = make_symbolic n symbols typs in
   let gram_rule = make_grammar_rule n assoc typs symbols notation in
   let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbols) in
   Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule));