minicoq: pretty-print applications; ambiguite grammaire supprimee; Ind, Const et Construct mots cles

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

5 files changed, 21 insertions, 13 deletions

diff --git a/Makefile b/Makefile
index 850060911..e52b55118 100644
--- a/Makefile
+++ b/Makefile
@@ -96,7 +96,7 @@ parsing/lexer.cmo: parsing/lexer.ml
 
 # Default rules
 
-.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .g4
+.SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4
 
 .ml.cmo:
 	$(OCAMLC) $(BYTEFLAGS) -c $<
@@ -110,10 +110,10 @@ parsing/lexer.cmo: parsing/lexer.ml
 .mll.ml:
 	ocamllex $<
 
-.g4.cmo:
+.ml4.cmo:
 	$(OCAMLC) $(BYTEFLAGS) -I $(CAMLP4LIB) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
 
-.g4.cmx:
+.ml44.cmx:
 	$(OCAMLOPT) $(OPTFLAGS) -I $(CAMLP4LIB) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
 
 # Cleaning
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index 7b7dca0ad..b45b480dc 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 open Pp
+open Util
 open Names
 open Univ
 open Generic
@@ -9,7 +10,7 @@ open Term
 
 let lexer = {
   Token.func = Lexer.func;
-  Token.using = (fun _ -> ());
+  Token.using = (function ("",s) -> Lexer.add_keyword s | _ -> ());
   Token.removing = (fun _ -> ());
   Token.tparse = Lexer.tparse;
   Token.text = Lexer.token_text }
@@ -58,12 +59,12 @@ EXTEND
 	DOP0 (Sort (Prop Null))
     | "Type" ->
 	DOP0 (Sort (Type (new_univ())))
-    | IDENT "Const"; id = IDENT ->
+    | "Const"; id = IDENT ->
 	DOPN (Const (path_of_string id), [||])
-    | IDENT "Ind"; id = IDENT; n = INT ->
+    | "Ind"; id = IDENT; n = INT ->
 	let n = int_of_string n in
 	DOPN (MutInd (path_of_string id, n), [||])
-    | IDENT "Construct"; id = IDENT; n = INT; i = INT ->
+    | "Construct"; id = IDENT; n = INT; i = INT ->
 	let n = int_of_string n and i = int_of_string i in
 	DOPN (MutConstruct ((path_of_string id, n), i), [||])
     | "["; na = name; ":"; t = term; "]"; c = term ->
@@ -152,10 +153,13 @@ let rec pp bv = function
   | DOP2 (Cast, c, t) ->
       if !print_casts then 
 	[< 'sTR"("; pp bv c; 'sTR"::"; pp bv t; 'sTR")" >]
-      else
+      else 
 	pp bv c
-  | DOPN (AppL, cv) ->
-      [< >]
+  | DOPN (AppL, [|c|]) ->
+      pp bv c
+  | DOPN (AppL, v) ->
+      [< 'sTR"("; prvect_with_sep (fun () -> [< 'sPC >]) (pp bv) v;
+	 'sTR")" >]
   | DOPN (Const sp, _) ->
       [< 'sTR"Const "; print_id (basename sp) >]
   | DOPN (MutInd (sp,i), _) ->
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 670acaa25..0c8f7f5f9 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -1,6 +1,8 @@
 
 (* $Id$ *)
 
+val add_keyword : string -> unit
+
 val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
 
 val tparse : string * string -> (string * string) Stream.t -> string
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 181c50a77..9a417622b 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -11,7 +11,7 @@ type error =
 
 exception Error of error * int * int
 
-let is_keyword =
+let add_keyword,is_keyword =
   let table = Hashtbl.create 149 in
   List.iter (fun kw -> Hashtbl.add table kw ())
     [ "Grammar"; "Syntax"; "Quit"; "Load"; "Compile";
@@ -21,7 +21,8 @@ let is_keyword =
       "Theorem"; "Variable"; "Axiom"; "Parameter"; "Hypothesis";
       "Orelse"; "Proof"; "Qed";
       "Prop"; "Set"; "Type" ];
-  fun s -> try Hashtbl.find table s; true with Not_found -> false
+  (fun s -> Hashtbl.add table s ()),
+  (fun s -> try Hashtbl.find table s; true with Not_found -> false)
       
 let char_for_backslash =
   match Sys.os_type with
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 7255eb721..a58ce94a6 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -43,7 +43,8 @@ let rec globalize bv = function
 let check c = 
   let c = globalize [] c in
   let (j,u) = safe_machine !env c in
-  mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 (pr_term (j_type j)); 'fNL >])
+  let ty = j_type j in
+  mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 (pr_term ty); 'fNL >])
 
 let definition id ty c =
   let c = globalize [] c in