← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to dev/ocamlweb-doc/syntax.mly

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
dev/ocamlweb-doc/syntax.mly
 
1
%{
 
2
open Ast
 
3
open Parse
 
4
%}
 
5
 
 
6
%token <string> META INT IDENT
 
7
%token <string> OPER
 
8
%token LPAR RPAR BAR COMMA COLON BANG FUN DOT RARROW LET COLONEQ IN IF
 
9
%token THEN ELSE EVAL AT FOR PROP SET TYPE WILDCARD FIX
 
10
%token COFIX MATCH WITH END AND LBRACE RBRACE STRUCT AS SIMPL PERCENT
 
11
%token EOF
 
12
 
 
13
%start main
 
14
%type <Ast.constr_ast> main
 
15
 
 
16
%start constr
 
17
%type <Ast.constr_ast> constr
 
18
 
 
19
%start simple_constr
 
20
%type <Ast.constr_ast> simple_constr
 
21
 
 
22
%%
 
23
 
 
24
main:
 
25
          constr EOF { $1 }
 
26
;
 
27
 
 
28
 
 
29
paren_constr:
 
30
          constr COMMA paren_constr  { Pair($1,$3) }
 
31
        | constr                     { $1 }
 
32
;
 
33
 
 
34
constr:
 
35
          binder_constr  { $1 }
 
36
        | oper_constr    { close_stack $1 }
 
37
;
 
38
 
 
39
binder_constr:
 
40
          BANG ne_binders DOT constr              { Prod($2, $4) }
 
41
        | FUN ne_binders type_cstr RARROW constr  { Lambda($2,mk_cast $5 $3) }
 
42
        | LET IDENT binders type_cstr COLONEQ constr IN constr
 
43
            { Let($2,mk_lambda $3 (mk_cast $6 $4),$8) }
 
44
        | LET LPAR comma_binders RPAR COLONEQ constr IN constr
 
45
            { LetCase($3,$6,$8) }
 
46
        | IF constr THEN constr ELSE constr       { IfCase($2,$4,$6) }
 
47
        | fix_constr                              { $1 }
 
48
        | EVAL rfun IN constr                     { Eval($2,$4) }
 
49
;
 
50
 
 
51
comma_binders:
 
52
          ne_comma_binders  { $1 }
 
53
        |                   { [] }
 
54
;
 
55
 
 
56
ne_comma_binders:
 
57
          binder COMMA ne_comma_binders  { $1 :: $3 }
 
58
        | binder                         { [$1] }
 
59
;
 
60
 
 
61
rfun:
 
62
          SIMPL  { Simpl }
 
63
;
 
64
 
 
65
 
 
66
/* 2 Conflits shift/reduce */
 
67
oper_constr:
 
68
          oper_constr oper appl_constr
 
69
            { parse_term $3 (parse_oper $2 $1) }
 
70
        | oper_constr oper binder_constr
 
71
            { parse_term $3 (parse_oper $2 $1) }
 
72
        | oper_constr oper  { parse_oper $2 $1 }
 
73
        |                   { empty }
 
74
        | appl_constr       { parse_term $1 empty }
 
75
;
 
76
 
 
77
oper:
 
78
          OPER {$1}
 
79
        | COLON {":"}
 
80
;
 
81
 
 
82
appl_constr:
 
83
          simple_constr ne_appl_args  { Appl($1,$2) }
 
84
        | AT global simple_constrs    { ApplExpl($2,$3) }
 
85
        | simple_constr               { $1 }
 
86
;
 
87
 
 
88
appl_arg:
 
89
          AT INT COLONEQ simple_constr  { (Some $2,$4) }
 
90
        | simple_constr                 { (None,$1) }
 
91
;
 
92
 
 
93
ne_appl_args:
 
94
          appl_arg               { [$1] }
 
95
        | appl_arg ne_appl_args  { $1::$2 }
 
96
;
 
97
 
 
98
simple_constr:
 
99
          atomic_constr                           { $1 }
 
100
        | match_constr                            { $1 }
 
101
        | LPAR paren_constr RPAR                  { $2 }
 
102
        | simple_constr PERCENT IDENT { Scope($3,$1) }
 
103
;
 
104
 
 
105
simple_constrs:
 
106
          simple_constr simple_constrs  { $1::$2 }
 
107
        |                               { [] }
 
108
;
 
109
 
 
110
atomic_constr:
 
111
          global    { Qualid $1 }
 
112
        | PROP      { Prop }
 
113
        | SET       { Set }
 
114
        | TYPE      { Type }
 
115
        | INT       { Int $1 }
 
116
        | WILDCARD  { Hole }
 
117
        | META      { Meta $1 }
 
118
;
 
119
 
 
120
global:
 
121
          IDENT DOT global  { $1 :: $3 }
 
122
        | IDENT             { [$1] }
 
123
;
 
124
 
 
125
/* Conflit normal */
 
126
fix_constr:
 
127
          fix_kw fix_decl
 
128
            { let (id,_,_,_,_ as fx) = $2 in Fixp($1,[fx],id) }
 
129
        | fix_kw fix_decl fix_decls FOR IDENT  { Fixp($1, $2::$3, $5) }
 
130
;
 
131
 
 
132
fix_kw: FIX {Fix} | COFIX {CoFix}
 
133
;
 
134
 
 
135
fix_decl:
 
136
          IDENT binders type_cstr annot COLONEQ constr  { ($1,$2,$3,$4,$6) }
 
137
;
 
138
 
 
139
fix_decls:
 
140
          AND fix_decl fix_decls  { $2::$3 }
 
141
        | AND fix_decl            { [$2] }
 
142
;
 
143
 
 
144
annot:
 
145
          LBRACE STRUCT IDENT RBRACE  { Some $3 }
 
146
        |                             { None }
 
147
;
 
148
 
 
149
match_constr:
 
150
          MATCH case_items case_type WITH branches END  { Match($2,$3,$5) }
 
151
;
 
152
 
 
153
case_items:
 
154
          case_item                   { [$1] }
 
155
        | case_item COMMA case_items  { $1::$3 }
 
156
;
 
157
 
 
158
case_item:
 
159
          constr pred_pattern { ($1,$2) }
 
160
;
 
161
 
 
162
case_type:
 
163
          RARROW constr  { Some $2 }
 
164
        |                { None }
 
165
;
 
166
 
 
167
pred_pattern:
 
168
          AS IDENT COLON constr  { (Some $2, Some $4) }
 
169
        | AS IDENT               { (Some $2, None) }
 
170
        | COLON constr           { (None, Some $2) }
 
171
        |                        { (None,None) }
 
172
;
 
173
 
 
174
branches:
 
175
          BAR branch_list  { $2 }
 
176
        | branch_list      { $1 }
 
177
        |                  { [] }
 
178
;
 
179
 
 
180
branch_list:
 
181
          patterns RARROW constr                  { [$1, $3] }
 
182
        | patterns RARROW constr BAR branch_list  { ($1,$3)::$5 }
 
183
;
 
184
 
 
185
patterns:
 
186
          pattern                 { [$1] }
 
187
        | pattern COMMA patterns  { $1::$3 }
 
188
;
 
189
 
 
190
pattern:
 
191
          pattern AS IDENT       { PatAs($1,$3) }
 
192
        | pattern COLON constr   { PatType($1,$3) }
 
193
        | IDENT simple_patterns  { PatConstr($1,$2) }
 
194
        | simple_pattern         { $1 }
 
195
;
 
196
 
 
197
simple_pattern:
 
198
          IDENT              { PatVar $1 }
 
199
        | LPAR pattern RPAR  { $2 }
 
200
;
 
201
 
 
202
simple_patterns:
 
203
          simple_pattern                  { [$1] }
 
204
        | simple_pattern simple_patterns  { $1::$2 }
 
205
;
 
206
 
 
207
binder:
 
208
          IDENT                 { ($1,Hole) }
 
209
        | LPAR IDENT type_cstr RPAR  { ($2,$3) }
 
210
;
 
211
 
 
212
binders:
 
213
          ne_binders  { $1 }
 
214
        |             { [] }
 
215
 
 
216
ne_binders:
 
217
          binder             { [$1] }
 
218
        | binder ne_binders  { $1::$2 }
 
219
;
 
220
 
 
221
type_cstr:
 
222
          COLON constr  { $2 }
 
223
        |               { Hole }
 
224
;