driver_parser.mly 7.01 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14 15

%{
  open Driver_ast
%}

16
%token <int> INTEGER
17 18
%token <string> IDENT
%token <string> STRING
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
19
%token <string> OPERATOR
20 21
%token <string> RIGHTSQ_QUOTE
%token <string> RIGHTPAR_QUOTE
22
%token <string> INPUT (* never reaches the parser *)
23
%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER MODEL_PARSER OVERRIDING USE
24
%token INTERFACE
25
%token VALID INVALID UNKNOWN FAIL
26
%token TIMEOUT OUTOFMEMORY STEPLIMITEXCEEDED TIME STEPS
27
%token UNDERSCORE LEFTPAR RIGHTPAR DOT DOTDOT QUOTE EOF
28
%token BLACKLIST
29
%token MODULE EXCEPTION VAL LITERAL
30
%token FUNCTION PREDICATE TYPE PROP ALL FILENAME TRANSFORM PLUGIN
31
%token COMMA CONSTANT
32
%token LEFTSQ RIGHTSQ LARROW
33
%token PREC
34

35
%nonassoc SYNTAX REMOVE PRELUDE INTERFACE
36 37
%nonassoc prec_pty

38 39
%start <Driver_ast.file> file
%start <Driver_ast.file_extract> file_extract
40 41
%%

42
file: list0_global_theory EOF { $1 }
43

44
list0_global_theory:
45 46 47 48
| (* epsilon *)
    { { f_global = []; f_rules = [] } }
| loc(global) list0_global_theory
    { {$2 with f_global = $1 :: ($2.f_global)} }
49 50
| theory list0_global_theory
    { {$2 with f_rules = $1 :: ($2.f_rules)} }
51 52 53 54

global:
| PRELUDE STRING { Prelude $2 }
| PRINTER STRING { Printer $2 }
55
| MODEL_PARSER STRING { ModelParser $2 }
56 57
| VALID STRING { RegexpValid $2 }
| INVALID STRING { RegexpInvalid $2 }
58
| TIMEOUT STRING { RegexpTimeout $2 }
59
| OUTOFMEMORY STRING { RegexpOutOfMemory $2 }
60
| STEPLIMITEXCEEDED STRING { RegexpStepLimitExceeded $2 }
61
| TIME STRING  { TimeRegexp $2 }
62
| STEPS STRING INTEGER { StepRegexp ($2, $3) }
63 64
| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
| FAIL STRING STRING { RegexpFailure ($2, $3) }
65 66 67
| VALID INTEGER { ExitCodeValid $2 }
| INVALID INTEGER { ExitCodeInvalid $2 }
| TIMEOUT INTEGER { ExitCodeTimeout $2 }
68
| STEPLIMITEXCEEDED INTEGER { ExitCodeStepLimitExceeded $2 }
69 70
| UNKNOWN INTEGER STRING { ExitCodeUnknown ($2, $3) }
| FAIL INTEGER STRING { ExitCodeFailure ($2, $3) }
71
| FILENAME STRING { Filename $2 }
72
| TRANSFORM STRING { Transform $2 }
73
| PLUGIN STRING STRING { Plugin ($2,$3) }
74 75
| BLACKLIST STRING+ { Blacklist $2 }
| INPUT { assert false }
76 77

theory:
78
| THEORY loc(tqualid) list(loc(trule)) END
79
    { { thr_name = $2; thr_rules = $3 } }
80

81 82 83 84
syntax:
| OVERRIDING SYNTAX { true }
| SYNTAX            { false }

85
trule:
86 87 88 89 90
| PRELUDE STRING                 { Rprelude   ($2) }
| syntax TYPE      qualid STRING { Rsyntaxts  ($3, $4, $1) }
| syntax CONSTANT  qualid STRING { Rsyntaxfs  ($3, $4, $1) }
| syntax FUNCTION  qualid STRING { Rsyntaxfs  ($3, $4, $1) }
| syntax PREDICATE qualid STRING { Rsyntaxps  ($3, $4, $1) }
Clément Fumex's avatar
Clément Fumex committed
91
| syntax LITERAL   qualid STRING { Rliteral   ($3, $4, $1) }
92
| REMOVE PROP qualid             { Rremovepr  ($3) }
93
| REMOVE ALL                     { Rremoveall }
94 95
| META ident meta_args           { Rmeta      ($2, $3) }
| META STRING meta_args          { Rmeta      ($2, $3) }
96
| USE qualid                     { Ruse       ($2)     }
97

98
meta_args: separated_nonempty_list(COMMA,meta_arg) { $1 }
99 100

meta_arg:
101
| TYPE   meta_type { PMAty  $2 }
102 103 104 105 106
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
| INTEGER          { PMAint $1 }
107

108
tqualid:
109 110 111 112 113
| ident              { [$1] }
| ident DOT tqualid  { $1 :: $3 }
| STRING DOT tqualid { $1 :: $3 }

qualid:  loc(qualid_)  { $1 }
114

115 116 117
qualid_:
| ident_rich         { [$1] }
| ident DOT qualid_  { ($1 :: $3) }
118 119

ident:
120 121 122 123
| IDENT        { $1 }
| SYNTAX       { "syntax" }
| REMOVE       { "remove" }
| PRELUDE      { "prelude" }
124
| INTERFACE    { "interface" }
125 126 127
| BLACKLIST    { "blacklist" }
| PRINTER      { "printer" }
| STEPS        { "steps" }
128
| MODEL_PARSER { "model_parser" }
129 130 131 132 133 134 135 136
| VALID        { "valid" }
| INVALID      { "invalid" }
| TIMEOUT      { "timeout" }
| UNKNOWN      { "unknown" }
| FAIL         { "fail" }
| FILENAME     { "filename" }
| TRANSFORM    { "transformation" }
| PLUGIN       { "plugin" }
137 138

ident_rich:
139 140 141
| ident                             { $1 }
| LEFTPAR operator RIGHTPAR         { $2 }
| LEFTPAR operator RIGHTPAR_QUOTE   { $2 ^ $3 }
142 143

operator:
144 145
| o = OPERATOR                      { if o.[0] <> '!' && o.[0] <> '?' then
                                      Ident.op_infix o else Ident.op_prefix o }
146
| OPERATOR UNDERSCORE               { Ident.op_prefix $1 }
147 148 149 150 151 152 153 154 155 156
| LEFTSQ rightsq                    { Ident.op_get $2 }
| LEFTSQ rightsq LARROW             { Ident.op_set $2 }
| LEFTSQ LARROW rightsq             { Ident.op_update $3 }
| LEFTSQ DOTDOT rightsq             { Ident.op_cut $3 }
| LEFTSQ UNDERSCORE DOTDOT rightsq  { Ident.op_rcut $4 }
| LEFTSQ DOTDOT UNDERSCORE rightsq  { Ident.op_lcut $4 }

rightsq:
| RIGHTSQ         { "" }
| RIGHTSQ_QUOTE   { $1 }
157

158
(* Types *)
159

160 161 162
meta_type:
| qualid meta_type_args       { PTyapp ($1, $2) }
| primitive_type_arg_common   { $1 }
163

164 165 166
meta_type_args:
| (* epsilon *) %prec prec_pty        { [] }
| primitive_type_arg meta_type_args   { $1 :: $2 }
167 168

primitive_type:
169
| qualid primitive_type_arg+  { PTyapp ($1, $2) }
170 171 172 173 174 175 176
| primitive_type_arg          { $1 }

primitive_type_arg:
| qualid                    { PTyapp ($1, []) }
| primitive_type_arg_common { $1 }

primitive_type_arg_common:
177
| QUOTE ident                       { PTyvar $2 }
178 179 180 181 182 183 184 185
| LEFTPAR primitive_types RIGHTPAR  { PTuple $2 }
| LEFTPAR RIGHTPAR                  { PTuple [] }
| LEFTPAR primitive_type RIGHTPAR   { $2 }

primitive_types:
| primitive_type COMMA primitive_type  { [$1; $3] }
| primitive_type COMMA primitive_types { $1 :: $3 }

186
(* WhyML *)
187 188

file_extract:
189
| list0_global_theory_module EOF { $1 }
190 191

list0_global_theory_module:
192
| (* epsilon *)
193
    { { fe_global = []; fe_th_rules = []; fe_mo_rules = [] } }
194 195
| loc(global_extract) list0_global_theory_module
    { {$2 with fe_global = $1 :: ($2.fe_global)} }
196 197 198 199 200
| theory list0_global_theory_module
    { {$2 with fe_th_rules = $1 :: ($2.fe_th_rules)} }
| module_ list0_global_theory_module
    { {$2 with fe_mo_rules = $1 :: ($2.fe_mo_rules)} }

201
global_extract:
202 203 204
| PRELUDE STRING    { EPrelude $2 }
| PRINTER STRING    { EPrinter $2 }
| BLACKLIST STRING+ { EBlacklist $2 }
205

206
module_:
207
| MODULE loc(tqualid) list(loc(mrule)) END
208 209 210
    { { mor_name = $2; mor_rules = $3 } }

mrule:
211
| trule                          { MRtheory $1 }
212
| INTERFACE STRING               { MRinterface ($2) }
213
| SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) }
214 215 216
| SYNTAX VAL qualid STRING       { MRval ($3, $4, []) }
| SYNTAX VAL qualid STRING precedence
                                 { MRval ($3, $4, $5) }
217 218

precedence:
219
| PREC list(INTEGER) { $2 }
220

221
loc(X): X { Loc.extract ($startpos,$endpos), $1 }