Project

General

Profile

Revision 0038002e src/parser_lustre.mly

View differences:

src/parser_lustre.mly
26 26
open Dimension
27 27
open Utils
28 28

  
29
let mktyp x = mktyp (Location.symbol_rloc ()) x
30
let mkclock x = mkclock (Location.symbol_rloc ()) x
31
let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x
32
let mkexpr x = mkexpr (Location.symbol_rloc ()) x
33
let mkeq x = mkeq (Location.symbol_rloc ()) x
34
let mkassert x = mkassert (Location.symbol_rloc ()) x
35
let mktop_decl x = mktop_decl (Location.symbol_rloc ()) x
36
let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x
37

  
38
let mkdim_int i = mkdim_int (Location.symbol_rloc ()) i
39
let mkdim_bool b = mkdim_bool (Location.symbol_rloc ()) b
40
let mkdim_ident id = mkdim_ident (Location.symbol_rloc ()) id
41
let mkdim_appl f args = mkdim_appl (Location.symbol_rloc ()) f args
42
let mkdim_ite i t e = mkdim_ite (Location.symbol_rloc ()) i t e
29
let get_loc () = Location.symbol_rloc ()
30
let mktyp x = mktyp (get_loc ()) x
31
let mkclock x = mkclock (get_loc ()) x
32
let mkvar_decl x = mkvar_decl (get_loc ()) x
33
let mkexpr x = mkexpr (get_loc ()) x
34
let mkeexpr x = mkeexpr (get_loc ()) x 
35
let mkeq x = mkeq (get_loc ()) x
36
let mkassert x = mkassert (get_loc ()) x
37
let mktop_decl x = mktop_decl (get_loc ()) x
38
let mkpredef_call x = mkpredef_call (get_loc ()) x
39
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
40

  
41
let mkdim_int i = mkdim_int (get_loc ()) i
42
let mkdim_bool b = mkdim_bool (get_loc ()) b
43
let mkdim_ident id = mkdim_ident (get_loc ()) id
44
let mkdim_appl f args = mkdim_appl (get_loc ()) f args
45
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
46

  
47
let mkannots annots = { annots = annots; annot_loc = get_loc () }
43 48

  
44 49
let add_node loc own msg hashtbl name value =
45 50
  try
46 51
    match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with
47 52
    | Node _        , ImportedNode _ when own   -> ()
48 53
    | ImportedNode _, _                         -> Hashtbl.add hashtbl name value
49
    | Node _        , _                         -> raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))
54
    | Node _        , _                         -> raise (Error (loc, Already_bound_symbol msg))
50 55
    | _                                         -> assert false
51 56
  with
52 57
    Not_found                                   -> Hashtbl.add hashtbl name value
......
54 59

  
55 60
let add_symbol loc msg hashtbl name value =
56 61
 if Hashtbl.mem hashtbl name
57
 then raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))
62
 then raise (Error (loc, Already_bound_symbol msg))
58 63
 else Hashtbl.add hashtbl name value
59 64

  
60 65
let check_symbol loc msg hashtbl name =
61 66
 if not (Hashtbl.mem hashtbl name)
62
 then raise (Corelang.Error (loc, Corelang.Unbound_symbol msg))
67
 then raise (Error (loc, Unbound_symbol msg))
63 68
 else ()
64 69

  
70
let check_node_symbol msg name value =
71
 if Hashtbl.mem node_table name
72
 then () (* TODO: should we check the types here ? *)
73
 else Hashtbl.add node_table name value
74

  
65 75
%}
66 76

  
67 77
%token <int> INT
68 78
%token <string> REAL
69 79
%token <float> FLOAT
80
%token <string> STRING
70 81
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
71 82
%token STATELESS ASSERT OPEN QUOTE FUNCTION
72 83
%token <string> IDENT
......
86 97
%token MULT DIV MOD
87 98
%token MINUS PLUS UMINUS
88 99
%token PRE ARROW
100
%token REQUIRES ENSURES OBSERVER
101
%token INVARIANT BEHAVIOR ASSUMES
102
%token EXISTS FORALL
89 103
%token PROTOTYPE LIB
90 104
%token EOF
91 105

  
106
%nonassoc prec_exists prec_forall
92 107
%nonassoc COMMA
93 108
%left MERGE IF
94 109
%nonassoc ELSE
......
110 125
%nonassoc LBRACKET
111 126

  
112 127
%start prog
113
%type <Corelang.top_decl list> prog
128
%type <LustreSpec.top_decl list> prog
129

  
114 130
%start header
115
%type <bool -> Corelang.top_decl list> header
131
%type <bool -> LustreSpec.top_decl list> header
132

  
133
%start lustre_annot
134
%type <LustreSpec.expr_annot> lustre_annot
135

  
136
%start lustre_spec
137
%type <LustreSpec.node_annot> lustre_spec
116 138

  
117 139
%%
118 140

  
......
157 179
			     nodei_prototype = $13;
158 180
			     nodei_in_lib = $14;})
159 181
    in
160
    (let loc = Location.symbol_rloc () in 
161
     fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) }
182
     check_node_symbol ("node " ^ $3) $3 nd; 
183
     let loc = get_loc () in
184
     (fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) }
162 185

  
163 186
prototype_opt:
164 187
 { None }
......
186 209
			     node_dec_stateless = $2;
187 210
			     node_stateless = None;
188 211
			     node_spec = $1;
189
			     node_annot = match annots with [] -> None | _ -> Some annots})
212
			     node_annot = annots})
190 213
     in
191 214
     let loc = Location.symbol_rloc () in
192 215
     add_node loc true ("node " ^ $3) node_table $3 nd; nd}
193 216

  
194 217
nodespec_list:
195 218
 { None }
196
| NODESPEC nodespec_list { (function None -> (fun s1 -> Some s1) | Some s2 -> (fun s1 -> Some (LustreSpec.merge_node_annot s1 s2))) $2 $1 }
219
| NODESPEC nodespec_list { 
220
  (function 
221
  | None    -> (fun s1 -> Some s1) 
222
  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
197 223

  
198 224
typ_def_list:
199 225
    /* empty */ {}
......
203 229
  TYPE IDENT EQ typeconst {
204 230
    try
205 231
      let loc = Location.symbol_rloc () in
206
      add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (Corelang.get_repr_type $4)
232
      add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (get_repr_type $4)
207 233
    with Not_found-> assert false }
208 234
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
209 235
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) }
......
245 271
  { [], [], [] }
246 272
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
247 273
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
248
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}
274
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
249 275
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
250 276

  
251 277
automaton:
......
281 307
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
282 308
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
283 309

  
310
lustre_spec:
311
| contract EOF { $1 }
312

  
313
contract:
314
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
315
 
316
requires:
317
{ [] }
318
| REQUIRES qexpr SCOL requires { $2::$4 }
319

  
320
ensures:
321
{ [] }
322
| ENSURES qexpr SCOL ensures { $2 :: $4 }
323
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { 
324
  mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
325
}
326

  
327
behaviors:
328
{ [] }
329
| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
330

  
331
assumes:
332
{ [] }
333
| ASSUMES qexpr SCOL assumes { $2::$4 } 
334

  
335
tuple_qexpr:
336
| qexpr COMMA qexpr {[$3;$1]}
337
| tuple_qexpr COMMA qexpr {$3::$1}
338

  
339
qexpr:
340
| expr { mkeexpr $1 }
341
  /* Quantifiers */
342
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } 
343
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
344

  
345

  
284 346
tuple_expr:
285 347
    expr COMMA expr {[$3;$1]}
286 348
| tuple_expr COMMA expr {$3::$1}
......
524 586

  
525 587
SCOL_opt:
526 588
    SCOL {} | {}
589

  
590

  
591
lustre_annot:
592
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
593

  
594
lustre_annot_list:
595
  { [] } 
596
| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
597
| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
598
| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
599
| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
600

  
601
kwd:
602
DIV { [] }
603
| DIV IDENT kwd { $2::$3}
604

  
605
%%
606
(* Local Variables: *)
607
(* compile-command:"make -C .." *)
608
(* End: *)
609

  
610

  

Also available in: Unified diff