driver_parser.mly 3.5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
/**************************************************************************/
/*                                                                        */
/*  Copyright (C) 2010-                                                   */
/*    Francois Bobot                                                      */
/*    Jean-Christophe Filliatre                                           */
/*    Johannes Kanig                                                      */
/*    Andrei Paskevich                                                    */
/*                                                                        */
/*  This software is free software; you can redistribute it and/or        */
/*  modify it under the terms of the GNU Library General Public           */
/*  License version 2.1, with the special exception on linking            */
/*  described in file LICENSE.                                            */
/*                                                                        */
/*  This software is distributed in the hope that it will be useful,      */
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  */
/*                                                                        */
/**************************************************************************/

%{
  open Driver_ast
  open Parsing
  let loc () = (symbol_start_pos (), symbol_end_pos ())
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
24
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
25 26
  let infix s = "infix " ^ s
  let prefix s = "prefix " ^ s
27 28 29 30
%}

%token <string> IDENT
%token <string> STRING
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
31
%token <string> OPERATOR
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32 33
%token THEORY END SYNTAX REMOVE TAG PRELUDE PRINTER CALL_ON_FILE CALL_ON_STDIN
%token VALID INVALID UNKNOWN FAIL
34
%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
35
%token LOGIC TYPE PROP FILENAME
36 37 38 39 40 41 42

%type <Driver_ast.file> file
%start file

%%

file:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43 44
| list0_global list0_theory EOF
    { { f_global = $1; f_rules = $2 } }
45 46
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
47 48 49 50 51 52 53 54 55 56 57 58 59 60
list0_global:
| /* epsilon */       { [] }
| global list0_global { (loc_i 1, $1) :: $2 }
;

global:
| PRELUDE STRING { Prelude $2 }
| PRINTER STRING { Printer $2 }
| CALL_ON_FILE STRING { CallFile $2 }
| CALL_ON_STDIN STRING { CallStdin $2 }
| VALID STRING { RegexpValid $2 }
| INVALID STRING { RegexpInvalid $2 }
| UNKNOWN STRING STRING { RegexpUnknown ($2, $3) }
| FAIL STRING STRING { RegexpFailure ($2, $3) }
61
| FILENAME STRING { Filename $2 }
62 63 64 65 66 67 68 69
;

list0_theory:
| /* epsilon */       { [] }
| theory list0_theory { $1 :: $2 }
;

theory:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
70
| THEORY qualid list0_trule END
71
    { { thr_name = $2; thr_rules = $3 } }
72 73 74 75 76 77 78 79
;

list0_trule:
| /* epsilon */     { [] }
| trule list0_trule { $1 :: $2 }
;

trule:
80
| PRELUDE STRING                      { Rprelude  (loc (),$2) }
81
| REMOVE cloned PROP qualid           { Rremove   ($2, $4) }
82 83
| SYNTAX TYPE qualid STRING           { Rsyntaxty ($3, $4) }
| SYNTAX LOGIC qualid STRING          { Rsyntaxls ($3, $4) }
84 85 86
| TAG cloned TYPE qualid STRING       { Rtagty    ($2, $4, $5) }
| TAG cloned LOGIC qualid STRING      { Rtagls    ($2, $4, $5) }
| TAG cloned PROP qualid STRING       { Rtagpr    ($2, $4, $5) }
87 88
;

89
cloned:
90
| /* epsilon */ { false }
91
| CLONED        { true  }
92 93 94
;

qualid:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
95 96
| ident            { loc(), [$1] }
| ident DOT qualid { loc(), ($1 :: snd $3) }
97 98 99
;

ident:
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
100
| IDENT  
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
101
    { $1 }
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
102
| STRING 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103
    { $1 }
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
104
| LEFTPAR UNDERSCORE OPERATOR UNDERSCORE RIGHTPAR 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105
    { infix $3 }
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
106
| LEFTPAR OPERATOR UNDERSCORE RIGHTPAR 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
107 108 109 110 111 112 113
    { prefix $2 }
/*
| LEFTPAR UNDERSCORE lident_op RIGHTPAR 
    { { id = postfix $3; id_loc = loc () } }
*/
| PRELUDE
    { "prelude" }
114 115
;