(debut) de grammaire minicoq

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

4 files changed, 77 insertions, 1 deletions

diff --git a/parsing/.cvsignore b/parsing/.cvsignore
index c1104f3abe..87551eece0 100644
--- a/parsing/.cvsignore
+++ b/parsing/.cvsignore
@@ -1 +1,2 @@
 lexer.ml
+*.ppo
diff --git a/parsing/g_minicoq.g4 b/parsing/g_minicoq.g4
index 8ee3d54256..4f8e145719 100644
--- a/parsing/g_minicoq.g4
+++ b/parsing/g_minicoq.g4
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 open Names
+open Univ
 open Generic
 open Term
 
@@ -12,12 +13,62 @@ let lexer = {
   Token.tparse = Lexer.tparse;
   Token.text = Lexer.token_text }
   
+type command =
+  | Definition of identifier * constr option * constr
+  | Parameter of identifier * constr
+  | Variable of identifier * constr
+  | Inductive of 
+      (identifier * constr) list *
+      (identifier * constr * (identifier * constr) list) list
+  | Check of constr
+
 let gram = Grammar.create lexer
 
 let term = Grammar.Entry.create gram "term"
 let command = Grammar.Entry.create gram "command"
 
+let new_univ =
+  let uc = ref 0 in
+  let univ = id_of_string "univ" in
+  fun () -> incr uc; { u_sp = make_path [] univ CCI; u_num = !uc }
+
+let path_of_string s = make_path [] (id_of_string s) CCI
+
 EXTEND
-  term: [ [ id = IDENT -> VAR (id_of_string id) ] ];
+  term: [ 
+    [ id = IDENT -> 
+	VAR (id_of_string id) 
+    | "Set" ->
+	DOP0 (Sort (Prop Pos))
+    | "Prop" ->
+	DOP0 (Sort (Prop Null))
+    | "Type" ->
+	DOP0 (Sort (Type (new_univ())))
+    | IDENT "Const"; id = IDENT ->
+	DOPN (Const (path_of_string id), [||])
+    | IDENT "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 ->
+	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))
+  ] ];
+  command: [ 
+    [ "Definition"; id = IDENT; ":="; c = term; "." ->
+	Definition (id_of_string id, None, c)
+    | "Definition"; id = IDENT; ":"; t = term; ":="; c = term; "." ->
+	Definition (id_of_string id, Some t, c)
+    | "Parameter"; id = IDENT; ":"; t = term; "." ->
+	Parameter (id_of_string id, t)
+    | "Variable"; id = IDENT; ":"; t = term; "." ->
+	Variable (id_of_string id, t)
+    | IDENT "Check"; c = term; "." ->
+	Check c
+    | EOI -> raise End_of_file
+  ] ];
 END
 
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index 0b2ceb1e80..ef47c4f894 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -1,4 +1,17 @@
 
+open Names
 open Term
 
 val term : constr Grammar.Entry.e
+
+type command =
+  | Definition of identifier * constr option * constr
+  | Parameter of identifier * constr
+  | Variable of identifier * constr
+  | Inductive of 
+      (identifier * constr) list *
+      (identifier * constr * (identifier * constr) list) list
+  | Check of constr
+
+val command : command Grammar.Entry.e
+
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index c0cbca3ba1..08ec04091b 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -64,6 +64,10 @@ 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']+
+let bin_literal = '0' ['b' 'B'] ['0'-'1']+
 
 rule token = parse
   | blank+ 
@@ -71,6 +75,11 @@ rule token = parse
   | firstchar identchar* 
       { let s = Lexing.lexeme lexbuf in
 	if is_keyword s then ("",s) else ("IDENT",s) }
+  | decimal_literal | hex_literal | oct_literal | bin_literal
+      { ("INT", Lexing.lexeme lexbuf) }
+  | ":=" { ("COLONEQUAL","") }
+  | ":"  { ("COLON","") }
+  | "."  { ("DOT","") }
   | symbolchar+
       { ("SPECIAL", Lexing.lexeme lexbuf) }
   | '`' [^'`']* '`'
@@ -86,6 +95,8 @@ rule token = parse
         comment_start_pos := Lexing.lexeme_start lexbuf;
         comment lexbuf;
         token lexbuf }
+  | eof 
+      { ("EOI","") }
 
 and comment = parse
     "(*"