Re-déplacement du résultat de Grammar au niveau constr_expr

(globalisation uniquement des noms - sauf cases, fix, ..., pas
d'implicites, pas d'interprétation des scopes - pas plus robuste
qu'avant...).
Diverses améliorations affichage et parsing.


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

3 files changed, 44 insertions, 12 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index c7ea8737f..64d8cc7cd 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -47,7 +47,7 @@ type prod_item =
 type grammar_rule = {
   gr_name : string; 
   gr_production : prod_item list; 
-  gr_action : aconstr }
+  gr_action : constr_expr }
 
 type grammar_entry = { 
   ge_name : string;
@@ -65,11 +65,14 @@ type grammar_associativity = Gramext.g_assoc option
 
 type entry_context = identifier list
 
-let ast_to_rawconstr = ref (fun _ _ -> AVar (id_of_string "Z"))
-let set_ast_to_rawconstr f = ast_to_rawconstr := f
+open Rawterm
+open Libnames
+
+let globalizer = ref (fun _ _ -> CHole dummy_loc)
+let set_constr_globalizer f = globalizer := f
 
 let act_of_ast vars = function
-  | SimpleAction (loc,ConstrNode a) -> !ast_to_rawconstr vars a
+  | SimpleAction (loc,ConstrNode a) -> !globalizer vars a
   | SimpleAction (loc,CasesPatternNode a) -> 
       failwith "TODO:act_of_ast: cases_pattern"
   | CaseAction _ -> failwith "case/let not supported"
@@ -92,8 +95,11 @@ type grammar_production =
 type raw_grammar_rule = string * grammar_production list * grammar_action
 type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list
 
+(* No kernel names in Grammar's *)
+let subst_constr_expr _ a = a
+
 let subst_grammar_rule subst gr =
-  { gr with gr_action = subst_aconstr subst gr.gr_action }
+  { gr with gr_action = subst_constr_expr subst gr.gr_action }
 
 let subst_grammar_entry subst ge =
   { ge with gl_rules = List.map (subst_grammar_rule subst) ge.gl_rules }
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 12d2ecc62..7398c7903 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -48,7 +48,7 @@ type prod_item =
 type grammar_rule = {
   gr_name : string; 
   gr_production : prod_item list; 
-  gr_action : aconstr }
+  gr_action : constr_expr }
 
 type grammar_entry = { 
   ge_name : string;
@@ -63,8 +63,9 @@ type grammar_associativity = Gramext.g_assoc option
 
 (* Globalisation and type-checking of Grammar actions *)
 type entry_context = identifier list
-val to_act_check_vars : entry_context -> grammar_action -> aconstr
-val set_ast_to_rawconstr : (entry_context -> constr_expr -> aconstr) -> unit
+
+val set_constr_globalizer : 
+  (entry_context -> constr_expr -> constr_expr) -> unit
 
 type syntax_modifier =
   | SetItemLevel of string list * int
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e177bb621..cea099da7 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -214,7 +214,33 @@ let rec pr_arrow pr = function
 
 let pr_annotation pr t = str "<" ++ pr ltop t ++ str ">"
 
-let pr_cases _ _ _ = str "<CASES(TODO)>"
+let rec pr_pat = function
+  | CPatAlias (_,p,x) -> pr_pat p ++ spc () ++ str "as" ++ spc () ++ pr_id x
+  | CPatCstr (_,c,[]) -> pr_reference c
+  | CPatCstr (_,c,pl) ->
+      hov 0 (
+	str "(" ++ pr_reference c ++ spc () ++ 
+	prlist_with_sep spc pr_pat pl ++ str ")")
+  | CPatAtom (_,Some c) -> pr_reference c
+  | CPatAtom (_,None) -> str "_"
+  | CPatNumeral (_,n) -> Bignat.pr_bigint n
+  | CPatDelimiters (_,key,p) -> pr_delimiters key (pr_pat p)
+
+let pr_eqn pr (_,patl,rhs) =
+  hov 0 (
+    prlist_with_sep spc pr_pat patl ++
+    str "=>" ++
+    brk (1,1) ++ pr ltop rhs)
+
+let pr_cases pr po tml eqns =
+  hov 0 (
+    pr_opt (pr_annotation pr) po ++
+    hv 0 (
+      hv 0 (
+	str "Cases" ++ brk (1,2) ++
+	prlist_with_sep spc (pr ltop) tml ++ spc() ++ str "of") ++
+      prlist_with_sep pr_bar (pr_eqn pr) eqns ++ spc () ++
+      str "end"))
 
 let rec pr inherited a =
   let (strm,prec) = match a with
@@ -239,8 +265,8 @@ let rec pr inherited a =
       hov 0 (
 	pr (latom,E) a ++ 
 	prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l), lapp
-  | CCases (_,po,c,eqns) ->
-      pr_cases po c eqns, lcases
+  | CCases (_,po,tml,eqns) ->
+      pr_cases pr po tml eqns, lcases
   | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
       (* On force les parenthèses autour d'un "if" sous-terme (même si le
 	 parsing est lui plus tolérant) *)
@@ -278,7 +304,6 @@ let rec pr inherited a =
   | CCast (_,a,b) ->
       hv 0 (pr (lcast,L) a ++ cut () ++ str "::" ++ pr (lcast,E) b), lcast
   | CNotation (_,s,env) -> pr_notation pr s env
-  | CGrammar _ -> failwith "CGrammar: TODO"
   | CNumeral (_,p) -> Bignat.pr_bigint p, latom
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr ltop a), latom
   | CDynamic _ -> str "<dynamic>", latom