pseudo-parser ocamlyacc de la nouvelle syntaxe

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

1 files changed, 246 insertions, 0 deletions

diff --git a/doc/syntax.mly b/doc/syntax.mly
new file mode 100644
index 000000000..2785e7ca0
--- /dev/null
+++ b/doc/syntax.mly
@@ -0,0 +1,246 @@
+%{
+
+type constr_ast =
+  Pair of constr_ast * constr_ast
+| Prod of binder list * constr_ast
+| Lambda of binder list * constr_ast
+| Cast of constr_ast * constr_ast
+| Let of string * constr_ast * constr_ast
+| LetCase of binder list * constr_ast * constr_ast
+| IfCase of constr_ast * constr_ast * constr_ast
+| Eval of red_fun * constr_ast
+| Infix of string * constr_ast * constr_ast
+| Prefix of string * constr_ast
+| Postfix of string * constr_ast
+| Appl of constr_ast * constr_arg list
+| ApplExpl of constr_ast * constr_ast list
+| Scope of string * constr_ast
+| Qualid of string list
+| Prop | Set | Type
+| Int of string
+| Hole
+| Meta of string
+| Fixp of fix_kind *
+      (string * binder list * constr_ast * string option * constr_ast) list *
+      string
+| Match of case_item list * constr_ast option *
+           (pattern list * constr_ast) list 
+
+and redfun = Simpl
+
+and binder = string * constr_ast
+
+and constr_arg = string option * constr_ast
+
+and fix_kind = Fix | CoFix
+
+and case_item = constr_ast * (string option * constr_ast option)
+
+and pattern = 
+  PatAs of pattern * string
+| PatType of pattern * constr_ast
+| PatConstr of string * pattern list
+| PatVar of string
+%}
+
+%token <string> META
+%token <string> INT
+%token <string> IDENT
+%token <string> INFIX
+%token <string> PREFIX
+%token <string> POSTFIX
+%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF THEN ELSE EVAL AT FOR BQUOTE PROP SET TYPE WILDCARD FIX COFIX MATCH WITH ENDKW AND LBRACE RBRACE STRUCT AS SIMPL
+
+%start constr
+%type <constr_ast> constr
+
+%%
+
+paren_constr:
+          constr COMMA paren_constr  { Pair($1,$3) }
+        | constr                     { $1 }
+;
+
+constr:
+          binder_constr  { $1 }
+        | oper_constr    { $1}
+;
+
+binder_constr:
+          BANG ne_binders DOT constr                  { Prod($2, $4) }
+        | FUN ne_binders type RARROW constr
+            { Lambda($2,Cast($5,$3)) }
+        | LET IDENT binders type COLONEQ constr IN constr
+            { Let($2,$6,Lambda($3,Cast($8,4))) }
+        | LET LPAR comma_binders RPAR COLONEQ constr IN constr
+            { LetCase($3,$6,$8) }
+        | IF constr THEN constr ELSE constr           { IfCase($2,$4,$6) }
+        | fix_constr                                  { $1 }
+        | EVAL rfun IN constr                         { Eval($2,$4) }
+;
+
+comma_binders:
+          ne_comma_binders  { $1 }
+        |                   { [] }
+;
+
+ne_comma_binders:
+          binder COMMA ne_comma_binders  { $1 :: $3 }
+        | binder                         { [$1] }
+;
+
+rfun:
+          SIMPL  { Simpl }
+;
+
+
+oper_constr:
+          oper_constr INFIX oper_constr  { Infix($2,$1,$3) }
+        | PREFIX oper_constr             { Prefix($1,$2) }
+        | oper_constr POSTFIX            { Postfix($2,$1) }
+        | appl_constr                    { $1 }
+;
+
+appl_constr:
+          simple_constr ne_appl_args  { Appl($1,$2) }
+        | AT global simple_constrs    { ApplExpl($2,$3) }
+        | simple_constr               { $1 }
+;
+
+appl_arg:
+          AT INT COLONEQ simple_constr  { (Some $2,$4) }
+        | simple_constr                 { (None,$1) }
+;
+
+ne_appl_args:
+          appl_arg               { [$1] }
+        | appl_arg ne_appl_args  { $1::$2 }
+;
+
+simple_constr:
+          atomic_constr                           { $1 }
+        | match_constr                            { $1 }
+        | LPAR paren_constr RPAR                  { $2 }
+        | BQUOTE IDENT COLON paren_constr BQUOTE  { Scope($2,$4) }
+;
+
+simple_constrs:
+          simple_constr simple_constrs  { $1::$2 }
+        |                               { [] }
+;
+
+atomic_constr:
+          global    { Qualid $1 }
+        | PROP      { Prop }
+        | SET       { Set }
+        | TYPE      { Type }
+        | INT       { Int $1 }
+        | WILDCARD  { Hole }
+        | META      { Meta $1 }
+;
+
+global:
+          IDENT DOT global  { $1 :: $3 }
+        | IDENT             { [$1] }
+;
+
+fix_constr:
+          fix_kw fix_decl
+            { let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) }
+        | fix_kw fix_decl fix_decls FOR IDENT  { ($1, $2::$3, $5) }
+;
+
+fix_kw: FIX {Fix} | COFIX {CoFix}
+;
+
+fix_decl:
+          IDENT binders type annot COLONEQ constr  { ($1,$2,$3,$4,$6) }
+;
+
+fix_decls:
+          AND fix_decl fix_decls  { $2::$3 }
+        | AND fix_decl            { [$2] }
+;
+
+annot:
+          LBRACE STRUCT IDENT RBRACE  { Some $3 }
+        |                             { None }
+;
+
+match_constr:
+          MATCH case_items case_type WITH branches ENDKW  { Match($2,$3,$5) }
+;
+
+case_items:
+          case_item                   { [$1] }
+        | case_item COMMA case_items  { $1::$3 }
+;
+
+case_item:
+          constr pred_pattern { ($1,$2) }
+;
+
+case_type:
+          RARROW constr  { Some $2 }
+        |                { None }
+;
+
+pred_pattern:
+          AS IDENT COLON constr  { (Some $2, Some $4) }
+        | AS IDENT               { (Some $2, None) }
+        | COLON constr           { (None, Some $2) }
+        |                        { (None,None) }
+;
+
+branches:
+          BAR branch_list  { $2 }
+        | branch_list      { $1 }
+        |                  { [] }
+;
+
+branch_list:
+          patterns RARROW constr                  { [$1, $3] }
+        | patterns RARROW constr BAR branch_list  { ($1,$3)::$5 }
+;
+
+patterns:
+          pattern                 { [$1] }
+        | pattern COMMA patterns  { $1::$3 }
+;
+
+pattern:
+          pattern AS IDENT       { PatAs($1,$3) }
+        | pattern COLON constr   { PatType($1,$3) }
+        | IDENT simple_patterns  { PatConstr($1,$2) }
+        | simple_pattern         { $1 }
+;
+
+simple_pattern:
+          IDENT              { PatVar $1 }
+        | LPAR pattern RPAR  { $2 }
+;
+
+simple_patterns:
+          simple_pattern                  { [$1] }
+        | simple_pattern simple_patterns  { $1::$2 }
+;
+
+binder:
+          IDENT                 { ($1,Hole) }
+        | LPAR IDENT type RPAR  { ($2,$3) }
+;
+
+binders:
+          ne_binders  { $1 }
+        |             { [] }
+
+ne_binders:
+          binder             { $1 }
+        | binder ne_binders  { $1::$2 }
+;
+
+type:
+          COLON constr  { $2 }
+        |               { Hole }
+;
+