driver_parser.mly 6.46 KB
Newer Older
1 2 3
/********************************************************************/
/*                                                                  */
/*  The Why3 Verification Platform   /   The Why3 Development Team  */
4
/*  Copyright 2010-2014   --   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
  let loc () = Loc.extract (symbol_start_pos (), symbol_end_pos ())
  let loc_i i = Loc.extract (rhs_start_pos i, rhs_end_pos i)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
17 18
  let infix s = "infix " ^ s
  let prefix s = "prefix " ^ s
19
  let mixfix s = "mixfix " ^ s
20 21
%}

22 23
%token <string> INPUT /* never reaches the parser */

24
%token <int> INTEGER
25 26
%token <string> IDENT
%token <string> STRING
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
27
%token <string> OPERATOR
28
%token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
29
%token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME
30
%token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
31
%token BLACKLIST
32
%token MODULE EXCEPTION VAL CONVERTER
33
%token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN
34
%token LEFTPAR_STAR_RIGHTPAR COMMA CONSTANT
35
%token LEFTSQ RIGHTSQ LARROW
36

37 38 39
%nonassoc SYNTAX REMOVE PRELUDE
%nonassoc prec_pty

40 41
%type <Driver_ast.file> file
%start file
42 43
%type <Driver_ast.file_extract> file_extract
%start file_extract
44 45 46 47

%%

file:
48 49
| list0_global_theory EOF
    { $1 }
50 51
;

52 53 54 55 56 57
list0_global_theory:
| /* epsilon */      { { f_global = []; f_rules = [] } }
| global list0_global_theory
    { {$2 with f_global = (loc_i 1, $1) :: ($2.f_global)} }
| theory list0_global_theory
    { {$2 with f_rules = $1 :: ($2.f_rules)} }
58 59 60 61 62 63 64
;

global:
| PRELUDE STRING { Prelude $2 }
| PRINTER STRING { Printer $2 }
| VALID STRING { RegexpValid $2 }
| INVALID STRING { RegexpInvalid $2 }
65
| TIMEOUT STRING { RegexpTimeout $2 }
66
| OUTOFMEMORY STRING { RegexpOutOfMemory $2 }
67
| TIME STRING  { TimeRegexp $2 }
68 69
| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
| FAIL STRING STRING { RegexpFailure ($2, $3) }
70 71 72 73 74
| VALID INTEGER { ExitCodeValid $2 }
| INVALID INTEGER { ExitCodeInvalid $2 }
| TIMEOUT INTEGER { ExitCodeTimeout $2 }
| UNKNOWN INTEGER STRING { ExitCodeUnknown ($2, $3) }
| FAIL INTEGER STRING { ExitCodeFailure ($2, $3) }
75
| FILENAME STRING { Filename $2 }
76
| TRANSFORM STRING { Transform $2 }
77
| PLUGIN STRING STRING { Plugin ($2,$3) }
78
| BLACKLIST list1_string_list { Blacklist $2 }
79 80 81
;

theory:
82
| THEORY tqualid list0_trule END
83
    { { thr_name = $2; thr_rules = $3 } }
84 85 86 87
;

list0_trule:
| /* epsilon */     { [] }
88
| trule list0_trule { (loc_i 1, $1) :: $2 }
89 90 91
;

trule:
92 93 94 95 96 97 98 99
| PRELUDE STRING                   { Rprelude  ($2) }
| SYNTAX TYPE      qualid STRING   { Rsyntaxts ($3, $4) }
| SYNTAX CONSTANT  qualid STRING   { Rsyntaxfs ($3, $4) }
| SYNTAX FUNCTION  qualid STRING   { Rsyntaxfs ($3, $4) }
| SYNTAX PREDICATE qualid STRING   { Rsyntaxps ($3, $4) }
| REMOVE PROP qualid               { Rremovepr ($3) }
| META ident meta_args             { Rmeta     ($2, $3) }
| META STRING meta_args            { Rmeta     ($2, $3) }
100 101 102 103 104 105 106 107
;

meta_args:
| meta_arg                 { [$1] }
| meta_arg COMMA meta_args { $1 :: $3 }
;

meta_arg:
108
| TYPE primitive_type_top { PMAty $2 }
109 110 111 112 113
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
| INTEGER          { PMAint $1 }
114 115
;

116
tqualid:
117 118 119
| ident              { loc (), [$1] }
| ident DOT tqualid  { loc (), ($1 :: snd $3) }
| STRING DOT tqualid { loc (), ($1 :: snd $3) }
120 121
;

122
qualid:
123 124
| ident_rich        { loc (), [$1] }
| ident DOT qualid  { loc (), ($1 :: snd $3) }
125 126 127
;

ident:
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
| IDENT     { $1 }
| SYNTAX    { "syntax" }
| REMOVE    { "remove" }
| PRELUDE   { "prelude" }
| PRINTER   { "printer" }
| VALID     { "valid" }
| INVALID   { "invalid" }
| TIMEOUT   { "timeout" }
| UNKNOWN   { "unknown" }
| FAIL      { "fail" }
| FILENAME  { "filename" }
| TRANSFORM { "transformation" }
| PLUGIN    { "plugin" }
;

ident_rich:
144 145 146 147 148 149 150 151 152 153
| ident                     { $1 }
| LEFTPAR_STAR_RIGHTPAR     { infix "*" }
| LEFTPAR operator RIGHTPAR { $2 }
;

operator:
| OPERATOR              { infix $1 }
| OPERATOR UNDERSCORE   { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
154
| LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
155 156
;

157 158 159 160 161
list1_string_list:
| STRING                   { [$1] }
| list1_string_list STRING { $2 :: $1 }
;

162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
/* Types */

primitive_type_top:
| qualid primitive_type_args_top  { PTyapp ($1, $2) }
| primitive_type_arg_common       { $1 }
;

primitive_type_args_top:
| /* epsilon */ %prec prec_pty                { [] }
| primitive_type_arg primitive_type_args_top  { $1 :: $2 }
;

primitive_type:
| qualid primitive_type_args  { PTyapp ($1, $2) }
| primitive_type_arg          { $1 }
;

primitive_type_args:
| primitive_type_arg                      { [$1] }
| primitive_type_arg primitive_type_args  { $1 :: $2 }
;

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

primitive_type_arg_common:
| type_var                          { PTyvar $1 }
| 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 }
;

type_var:
| QUOTE ident { $2 }
;

205 206 207 208 209 210 211 212
/* WhyML */

file_extract:
| list0_global_theory_module EOF
{ $1 }
;

list0_global_theory_module:
213 214
| /* epsilon */
    { { fe_global = []; fe_th_rules = []; fe_mo_rules = [] } }
215
| global_extract list0_global_theory_module
216 217 218 219 220 221 222
    { {$2 with fe_global = (loc_i 1, $1) :: ($2.fe_global)} }
| 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)} }
;

223 224 225 226 227 228
global_extract:
| PRELUDE STRING { EPrelude $2 }
| PRINTER STRING { EPrinter $2 }
| BLACKLIST list1_string_list { EBlacklist $2 }
;

229 230 231 232 233 234 235 236 237 238 239
module_:
| MODULE tqualid list0_mrule END
    { { mor_name = $2; mor_rules = $3 } }
;

list0_mrule:
| /* epsilon */     { [] }
| mrule list0_mrule { (loc_i 1, $1) :: $2 }
;

mrule:
240 241 242
| trule                          { MRtheory $1 }
| SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) }
| SYNTAX VAL qualid STRING       { MRval ($3, $4) }
243
| SYNTAX CONVERTER qualid STRING { MRconverter ($3, $4) }
244 245
;