Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

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

1 files changed, 77 insertions, 43 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 0e1f72536..2e4eea4b0 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -19,13 +19,17 @@ open Topconstr
 open Genarg
 
 type entry_type = argument_type
-type constr_entry_type = ETConstr | ETIdent | ETReference
+type constr_entry_type =
+  | ETIdent | ETReference
+  | ETConstr of (int * parenRelation) * int option
+  | ETPattern
+  | ETOther of string * string
 
 type nonterm_prod =
   | ProdList0 of nonterm_prod
   | ProdList1 of nonterm_prod
   | ProdOpt of nonterm_prod
-  | ProdPrimitive of (string * string)
+  | ProdPrimitive of constr_entry_type
 
 type prod_item =
   | Term of Token.pattern
@@ -38,7 +42,6 @@ type grammar_rule = {
 
 type grammar_entry = { 
   ge_name : string;
-  ge_type : constr_entry_type;
   gl_assoc : Gramext.g_assoc option;
   gl_rules : grammar_rule list }
 
@@ -56,18 +59,20 @@ type entry_context = (identifier * constr_entry_type) list
 let ast_to_rawconstr = ref (fun _ _ -> AVar (id_of_string "Z"))
 let set_ast_to_rawconstr f = ast_to_rawconstr := f
 
-let act_of_ast vars = function
-  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr vars a
-  | SimpleAction (loc,CasesPatternNode a) -> failwith "TODO:act_of_ast: cases_pattern"
+let act_of_ast env = function
+  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr env a
+  | SimpleAction (loc,CasesPatternNode a) -> 
+      failwith "TODO:act_of_ast: cases_pattern"
   | CaseAction _ -> failwith "case/let not supported"
 
 let to_act_check_vars = act_of_ast
 
 type syntax_modifier =
-  | SetItemLevel of string * int
+  | SetItemLevel of string list * int
   | SetLevel of int
   | SetAssoc of Gramext.g_assoc
   | SetEntryType of string * constr_entry_type
+  | SetOnlyParsing
 
 type nonterm =
   | NtShort of string
@@ -76,8 +81,7 @@ type grammar_production =
   | VTerm of string
   | VNonTerm of loc * nonterm * Names.identifier option
 type raw_grammar_rule = string * grammar_production list * grammar_action
-type raw_grammar_entry = 
-  string * constr_entry_type * grammar_associativity * raw_grammar_rule list
+type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
 
 let subst_grammar_rule subst gr =
   { gr with gr_action = subst_aconstr subst gr.gr_action }
@@ -141,55 +145,85 @@ let rename_command nt =
   else if nt = "lassoc_command4" then warn nt "lassoc_constr4"
   else nt
 
-let qualified_nterm current_univ = function
-  | NtQual (univ, en) -> (rename_command univ, rename_command en)
-  | NtShort en -> (current_univ, rename_command en)
-
-let entry_type_of_constr_entry_type = function
-  | ETConstr -> ConstrArgType
-  | ETIdent -> IdentArgType
-  | ETReference -> RefArgType
-
-let constr_entry_of_entry = function
-  | ConstrArgType -> ETConstr
-  | IdentArgType -> ETIdent
-  | RefArgType -> ETReference
-  | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
-
-let nterm loc (get_entry_type,univ) nont =
-  let nt = qualified_nterm univ nont in
-  try (nt,constr_entry_of_entry (get_entry_type nt))
-  with Not_found -> 
-    let (s,n) = nt in
-    user_err_loc(loc,"Externd.nterm",str("unknown grammar entry: "^s^":"^n))
+(* This translates constr0, constr1, ... level into camlp4 levels of constr *)
+
+let explicitize_entry univ nt =
+  if univ = "prim" & nt = "var" then ETIdent else
+  if univ <> "constr" then ETOther (univ,nt) else
+  match nt with
+  | "constr0" -> ETConstr ((0,E),Some 0)
+  | "constr1" -> ETConstr ((1,E),Some 1)
+  | "constr2" -> ETConstr ((2,E),Some 2)
+  | "constr3" -> ETConstr ((3,E),Some 3)
+  | "lassoc_constr4" -> ETConstr ((4,E),Some 4)
+  | "constr5" -> ETConstr ((5,E),Some 5)
+  | "constr6" -> ETConstr ((6,E),Some 6)
+  | "constr7" -> ETConstr ((7,E),Some 7)
+  | "constr8" | "constr" -> ETConstr ((8,E),Some 8)
+  | "constr9" -> ETConstr ((9,E),Some 9)
+  | "constr10" | "lconstr" -> ETConstr ((10,E),Some 10)
+  | "ident" -> ETIdent
+  | "global" -> ETReference
+  | _ -> ETOther (univ,nt)
+
+(* This determines if a reference to constr_n is a reference to the level
+   below wrt associativity (to be translated in camlp4 into "constr" without 
+   level) or to another level (to be translated into "constr LEVEL n") *)
+
+let clever_explicitize_entry univ name from assoc pos =
+  match explicitize_entry univ name, explicitize_entry "" from, pos with
+    | ETConstr ((n,_ as s),_),ETConstr ((lev,_),_),Some start
+	when n = lev - 1 & assoc <> Some Gramext.LeftA & start
+	  or n = lev & assoc = Some Gramext.LeftA & start
+	  or n = lev & assoc = Some Gramext.RightA & not start
+	  or n = lev - 1 & assoc <> Some Gramext.RightA & not start
+	-> ETConstr (s, None)
+    | x,_,_ -> x
+
+let qualified_nterm current_univ from ass pos = function
+  | NtQual (univ, en) ->
+      let univ = rename_command univ in
+      clever_explicitize_entry univ (rename_command en) from ass pos
+  | NtShort en ->
+      clever_explicitize_entry current_univ (rename_command en) from ass pos
+
+let check_entry check_entry_type = function
+  | ETOther (u,n) -> check_entry_type (u,n)
+  | _ -> ()
+
+let nterm loc (((check_entry_type,univ),lev,ass),pos) nont =
+  let typ = qualified_nterm univ lev ass pos nont in
+  check_entry check_entry_type typ;
+  typ
 
 let prod_item univ env = function
   | VTerm s -> env, Term (terminal s)
   | VNonTerm (loc, nt, Some p) ->
-     let (nont, etyp) = nterm loc univ nt in
-      ((p, etyp) :: env, NonTerm (ProdPrimitive nont, Some (p,etyp)))
+     let typ = nterm loc univ nt in
+      ((p, typ) :: env, NonTerm (ProdPrimitive typ, Some (p,typ)))
   | VNonTerm (loc, nt, None) ->
-      let (nont, etyp) = nterm loc univ nt in 
-      env, NonTerm (ProdPrimitive nont, None)
+      let typ = nterm loc univ nt in 
+      env, NonTerm (ProdPrimitive typ, None)
 
-let rec prod_item_list univ penv pil =
+let rec prod_item_list univ penv pil start =
   match pil with
     | [] -> [], penv
     | pi :: pitl ->
-	let (env, pic) = prod_item univ penv pi in
-	let (pictl, act_env) = prod_item_list univ env pitl in
+	let pos = if pitl=[] then Some false else start in
+	let (env, pic) = prod_item (univ,pos) penv pi in
+	let (pictl, act_env) = prod_item_list univ env pitl None in
         (pic :: pictl, act_env)
 
-let gram_rule univ etyp (name,pil,act) =
-  let (pilc, act_env) = prod_item_list univ [] pil in
+let gram_rule univ (name,pil,act) =
+  let (pilc, act_env) = prod_item_list univ [] pil (Some true) in
   let a = to_act_check_vars act_env act in
   { gr_name = name; gr_production = pilc; gr_action = a }
 
-let gram_entry univ (nt, etyp, ass, rl) =
-  { ge_name = rename_command nt;
-    ge_type = etyp;
+let gram_entry univ (nt, ass, rl) =
+  let name = rename_command nt in
+  { ge_name = name;
     gl_assoc = ass;
-    gl_rules = List.map (gram_rule univ etyp) rl }
+    gl_rules = List.map (gram_rule (univ,name,ass)) rl }
 
 let interp_grammar_command univ ge entryl =
   let univ = rename_command univ in