mise en place commandes minicoq

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

3 files changed, 91 insertions, 12 deletions

diff --git a/parsing/g_minicoq.g4 b/parsing/g_minicoq.g4
index 4f8e145719..9cd01fdd0d 100644
--- a/parsing/g_minicoq.g4
+++ b/parsing/g_minicoq.g4
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Names
 open Univ
 open Generic
@@ -25,6 +26,7 @@ type command =
 let gram = Grammar.create lexer
 
 let term = Grammar.Entry.create gram "term"
+let name = Grammar.Entry.create gram "name"
 let command = Grammar.Entry.create gram "command"
 
 let new_univ =
@@ -35,9 +37,15 @@ let new_univ =
 let path_of_string s = make_path [] (id_of_string s) CCI
 
 EXTEND
+  name: [ 
+    [ id = IDENT -> Name (id_of_string id)
+    | "_" -> Anonymous
+  ] ];
   term: [ 
     [ id = IDENT -> 
 	VAR (id_of_string id) 
+    | IDENT "Rel"; n = INT ->
+	Rel (int_of_string n)
     | "Set" ->
 	DOP0 (Sort (Prop Pos))
     | "Prop" ->
@@ -52,10 +60,23 @@ EXTEND
     | IDENT "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), [||])
-    | "["; id = IDENT; ":"; t = term; "]"; c = term ->
-	DOP2 (Lambda, t, DLAM (Name (id_of_string id), c))
-    | "("; id = IDENT; ":"; t = term; ")"; c = term ->
-	DOP2 (Prod, t, DLAM (Name (id_of_string id), c))
+    | "["; na = name; ":"; t = term; "]"; c = term ->
+	DOP2 (Lambda, t, DLAM (na, c))
+    | "("; na = name; ":"; t = term; ")"; c = term ->
+	DOP2 (Prod, t, DLAM (na, c))
+    | "("; id = IDENT; cl = LIST1 term; ")" ->
+	let c = VAR (id_of_string id) in
+	DOPN (AppL, Array.of_list (c::cl))
+    | "("; cl = LIST1 term; ")" ->
+	begin match cl with
+	  | [c] -> c
+	  | _ -> DOPN (AppL, Array.of_list cl)
+	end
+    | "("; c = term; "::"; t = term; ")" ->
+	DOP2 (Cast, c, t)
+    | "<"; p = term; ">"; IDENT "Case"; c = term; "of"; 
+      bl = LIST0 term; "end" ->
+	DOPN (MutCase None, Array.of_list (p :: c :: bl))
   ] ];
   command: [ 
     [ "Definition"; id = IDENT; ":="; c = term; "." ->
@@ -72,3 +93,59 @@ EXTEND
   ] ];
 END
 
+(* Pretty-print. *)
+
+let print_univers = ref false
+let print_casts = ref false
+
+let print_type u =
+  let sp = u.u_sp and num = u.u_num in
+  [< 'sTR "Type";
+     if !print_univers then 
+       [< 'sTR "("; print_id (basename sp); 'sPC; 'iNT num >] 
+     else 
+       [< >] 
+  >]
+  
+let print_name = function
+  | Anonymous -> [< 'sTR "_" >]
+  | Name id -> print_id id
+
+let print_rel bv n = print_name (List.nth bv (pred n))
+
+let rename bv = function
+  | Anonymous -> Anonymous
+  | Name id as na -> 
+      let idl = 
+	List.fold_left 
+	  (fun l n -> match n with Name x -> x::l | _ -> l) [] bv 
+      in
+      if List.mem na bv then Name (next_ident_away id idl) else na
+
+let rec pp bv = function
+  | DOP0 (Sort (Prop Pos)) -> [< 'sTR "Set" >]
+  | DOP0 (Sort (Prop Null)) -> [< 'sTR "Prop" >]
+  | DOP0 (Sort (Type u)) -> print_type u
+  | DOP2 (Lambda, t, DLAM(na, c)) ->
+      [< 'sTR"["; print_name na; 'sTR":"; pp bv t; 'sTR"]"; pp (na::bv) c >]
+  | DOP2 (Prod, t, DLAM(na, c)) ->
+      [< 'sTR"("; print_name na; 'sTR":"; pp bv t; 'sTR")"; pp (na::bv) c >]
+  | DOP2 (Cast, c, t) ->
+      if !print_casts then 
+	[< 'sTR"("; pp bv c; 'sTR"::"; pp bv t; 'sTR")" >]
+      else
+	pp bv c
+  | DOPN (AppL, cv) ->
+      [< >]
+  | DOPN (Const sp, _) ->
+      [< 'sTR"Const "; print_id (basename sp) >]
+  | DOPN (MutInd (sp,i), _) ->
+      [< 'sTR"Ind "; print_id (basename sp); 'sTR" "; 'iNT i >]
+  | DOPN (MutConstruct ((sp,i),j), _) ->
+      [< 'sTR"Construct "; print_id (basename sp); 'sTR" "; 'iNT i; 
+	 'sTR" "; 'iNT j >]
+  | VAR id -> print_id id
+  | Rel n -> print_rel bv n
+  | _ -> [< 'sTR"<???>" >]
+
+let pr_term = pp []
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index ef47c4f894..77dbb5c712 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -1,4 +1,5 @@
 
+open Pp
 open Names
 open Term
 
@@ -15,3 +16,4 @@ type command =
 
 val command : command Grammar.Entry.e
 
+val pr_term : constr -> std_ppcmds
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 08ec04091b..181c50a77c 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -63,7 +63,7 @@ let firstchar =
 let identchar = 
   ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
 let symbolchar =
-  ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~']
+  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' '=' '?' '@' '^' '|' '~']
 let decimal_literal = ['0'-'9']+
 let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
 let oct_literal = '0' ['o' 'O'] ['0'-'7']+
@@ -77,13 +77,13 @@ rule token = parse
 	if is_keyword s then ("",s) else ("IDENT",s) }
   | decimal_literal | hex_literal | oct_literal | bin_literal
       { ("INT", Lexing.lexeme lexbuf) }
-  | ":=" { ("COLONEQUAL","") }
-  | ":"  { ("COLON","") }
-  | "."  { ("DOT","") }
+  | "(" | ")" | "[" | "]" | "{" | "}" | "<" | ">" | "." | "_" 
+      { ("", Lexing.lexeme lexbuf) }
   | symbolchar+
-      { ("SPECIAL", Lexing.lexeme lexbuf) }
+      { ("", Lexing.lexeme lexbuf) }
   | '`' [^'`']* '`'
-      { ("QUOTED", Lexing.lexeme lexbuf) }
+      { let s = Lexing.lexeme lexbuf in
+	("QUOTED", String.sub s 1 (String.length s - 2)) }
   | "\""
       { Buffer.reset string_buffer;
         let string_start = Lexing.lexeme_start lexbuf in
@@ -99,7 +99,7 @@ rule token = parse
       { ("EOI","") }
 
 and comment = parse
-    "(*"
+  | "(*"
       { comment_depth := succ !comment_depth; comment lexbuf }
   | "*)"
       { comment_depth := pred !comment_depth;
@@ -124,7 +124,7 @@ and comment = parse
       { comment lexbuf }
 
 and string = parse
-    '"'
+  | '"'
       { () }
   | '\\' ("\010" | "\013" | "\013\010") [' ' '\009'] *
       { string lexbuf }