driver_parser.mly 6.25 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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

%{
  open Driver_ast
14

15 16
%}

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

32 33 34
%nonassoc SYNTAX REMOVE PRELUDE
%nonassoc prec_pty

35 36
%start <Driver_ast.file> file
%start <Driver_ast.file_extract> file_extract
37 38
%%

39
file: list0_global_theory EOF { $1 }
40

41
list0_global_theory:
42 43 44 45
| (* epsilon *)
    { { f_global = []; f_rules = [] } }
| loc(global) list0_global_theory
    { {$2 with f_global = $1 :: ($2.f_global)} }
46 47
| theory list0_global_theory
    { {$2 with f_rules = $1 :: ($2.f_rules)} }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
48 49 50 51

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

theory:
75
| THEORY loc(tqualid) list(loc(trule)) END
76
    { { thr_name = $2; thr_rules = $3 } }
77

78 79 80 81
syntax:
| OVERRIDING SYNTAX { true }
| SYNTAX            { false }

82
trule:
83 84 85 86 87 88
| 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) }
| syntax CONVERTER qualid STRING { Rconverter ($3, $4, $1) }
Clément Fumex's avatar
Clément Fumex committed
89
| syntax LITERAL   qualid STRING { Rliteral   ($3, $4, $1) }
90
| REMOVE PROP qualid             { Rremovepr  ($3) }
91
| REMOVE ALL                     { Rremoveall }
92 93
| META ident meta_args           { Rmeta      ($2, $3) }
| META STRING meta_args          { Rmeta      ($2, $3) }
94

95
meta_args: separated_nonempty_list(COMMA,meta_arg) { $1 }
96 97

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

105
tqualid:
106 107 108 109 110
| ident              { [$1] }
| ident DOT tqualid  { $1 :: $3 }
| STRING DOT tqualid { $1 :: $3 }

qualid:  loc(qualid_)  { $1 }
111

112 113 114
qualid_:
| ident_rich         { [$1] }
| ident DOT qualid_  { ($1 :: $3) }
115 116

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

ident_rich:
135 136 137 138
| ident                     { $1 }
| LEFTPAR operator RIGHTPAR { $2 }

operator:
139 140 141 142 143
| OPERATOR              { Ident.infix $1 }
| OPERATOR UNDERSCORE   { Ident.prefix $1 }
| LEFTSQ RIGHTSQ        { Ident.mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { Ident.mixfix "[<-]" }
| LEFTSQ RIGHTSQ LARROW { Ident.mixfix "[]<-" }
144

145
(* Types *)
146

147 148 149
meta_type:
| qualid meta_type_args       { PTyapp ($1, $2) }
| primitive_type_arg_common   { $1 }
150

151 152 153
meta_type_args:
| (* epsilon *) %prec prec_pty        { [] }
| primitive_type_arg meta_type_args   { $1 :: $2 }
154 155

primitive_type:
156
| qualid primitive_type_arg+  { PTyapp ($1, $2) }
157 158 159 160 161 162 163
| primitive_type_arg          { $1 }

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

primitive_type_arg_common:
164
| QUOTE ident                       { PTyvar $2 }
165 166 167 168 169 170 171 172
| 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 }

173
(* WhyML *)
174 175

file_extract:
176
| list0_global_theory_module EOF { $1 }
177 178

list0_global_theory_module:
179
| (* epsilon *)
180
    { { fe_global = []; fe_th_rules = []; fe_mo_rules = [] } }
181 182
| loc(global_extract) list0_global_theory_module
    { {$2 with fe_global = $1 :: ($2.fe_global)} }
183 184 185 186 187
| 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)} }

188
global_extract:
189 190 191
| PRELUDE STRING    { EPrelude $2 }
| PRINTER STRING    { EPrinter $2 }
| BLACKLIST STRING+ { EBlacklist $2 }
192

193
module_:
194
| MODULE loc(tqualid) list(loc(mrule)) END
195 196 197
    { { mor_name = $2; mor_rules = $3 } }

mrule:
198 199 200
| trule                          { MRtheory $1 }
| SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) }
| SYNTAX VAL qualid STRING       { MRval ($3, $4) }
201

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