Project

General

Profile

Revision a0b18d45

View differences:

src/compiler_common.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open Format 
13
open Format
14 14
open Lustre_types
15 15
open Corelang
16 16

  
......
45 45
  (* Parsing *)
46 46
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);
47 47
    try
48
      let header = Parse.header Parser_lustre.header Lexer_lustre.token lexbuf in
48
      let header = Parse.header Parser_lustre.header_main Lexer_lustre.token lexbuf in
49 49
      (*ignore (Modules.load_header ISet.empty header);*)
50 50
      close_in h_in;
51 51
      header
52 52
    with
53
    | (Parse.Error err) as exc -> 
53
    | (Parse.Error err) as exc ->
54 54
      Parse.report_error err;
55 55
      raise exc
56 56
    | Corelang.Error (loc, err) as exc -> (
......
68 68
  Location.init lexbuf source_name;
69 69

  
70 70
  (* Parsing *)
71
  Log.report ~level:1 
71
  Log.report ~level:1
72 72
    (fun fmt -> fprintf fmt ".. parsing source file %s@ " source_name);
73 73
  try
74
    let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in
74
    let prog = Parse.prog Parser_lustre.prog_main Lexer_lustre.token lexbuf in
75 75
    (*ignore (Modules.load_program ISet.empty prog);*)
76 76
    close_in s_in;
77 77
    prog
78 78
  with
79
  | (Parse.Error err) as exc -> 
79
  | (Parse.Error err) as exc ->
80 80
    Parse.report_error err;
81 81
    raise exc
82 82
  | Corelang.Error (loc, err) as exc ->
......
115 115
      Location.pp_loc loc;
116 116
    raise exc
117 117

  
118
let type_decls env decls =  
118
let type_decls env decls =
119 119
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
120
  let new_env = 
120
  let new_env =
121 121
    begin
122 122
      try
123 123
	Typing.type_prog env decls
......
126 126
	  Types.pp_error err
127 127
	  Location.pp_loc loc;
128 128
	raise exc
129
    end 
129
    end
130 130
  in
131 131
  if !Options.print_types || !Options.verbose_level > 2 then
132 132
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
133 133
  new_env
134
      
135
let clock_decls env decls = 
134

  
135
let clock_decls env decls =
136 136
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ ");
137 137
  let new_env =
138 138
    begin
......
188 188
   (Env.initial, Env.initial)
189 189
 *)
190 190

  
191
let generate_lusic_header destname lusic_ext =	
191
let generate_lusic_header destname lusic_ext =
192 192
  match !Options.output with
193 193
  | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
194 194
  | _ -> ()
195
	 
196 195

  
197
    
196

  
197

  
198 198
let check_compatibility (prog, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
199 199
  try
200 200
    (* checking defined types are compatible with declared types*)
......
228 228
let is_stateful topdecl =
229 229
  match topdecl.top_decl_desc with
230 230
  | Node nd -> (match nd.node_stateless with Some b -> not b | None -> not nd.node_dec_stateless)
231
  | ImportedNode nd -> not nd.nodei_stateless 
231
  | ImportedNode nd -> not nd.nodei_stateless
232 232
  | _ -> false
233 233

  
234 234

  
......
274 274
    | Node nd ->
275 275
       List.iter
276 276
	 (update_vdecl_parents nd.node_id)
277
	 (nd.node_inputs @ nd.node_outputs @ nd.node_locals )  
278
    | ImportedNode ind -> 
277
	 (nd.node_inputs @ nd.node_outputs @ nd.node_locals )
278
    | ImportedNode ind ->
279 279
       List.iter
280 280
	 (update_vdecl_parents ind.nodei_id)
281
	 (ind.nodei_inputs @ ind.nodei_outputs )  
281
	 (ind.nodei_inputs @ ind.nodei_outputs )
282 282
    | _ -> ()
283 283
  ) prog
src/lexerLustreSpec.mll
89 89
      {REAL (Num.num_of_string (l^r), String.length r, s)}
90 90
  | (('-'? ['0'-'9']+ as l)  '.' (['0'-'9']+ as r) ('E'|'e') (('+'|'-') ['0'-'9'] ['0'-'9']* as exp)) as s
91 91
      {REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp, s)}
92
  | '-'? ['0'-'9']+ 
92
  | '-'? ['0'-'9']+
93 93
      {INT (int_of_string (Lexing.lexeme lexbuf)) }
94 94
 (* | '/' (['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* '/')+ as s
95 95
      {IDENT s}
......
149 149
  let annot s =
150 150
    let lexbuf = Lexing.from_string s in
151 151
   try
152
     Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lexbuf
152
     Parser_lustre.lustre_annot_main(* ParserLustreSpec.lustre_annot *) token lexbuf
153 153
   with Parsing.Parse_error as _e -> (
154 154
     Format.eprintf "Lexing error at position %a:@.unexpected token %s when parsing annotation %s@.@?"
155 155
       (fun fmt p -> Format.fprintf fmt "%s l%i c%i" p.Lexing.pos_fname p.Lexing.pos_lnum p.Lexing.pos_cnum) lexbuf.Lexing.lex_curr_p
156 156
       (Lexing.lexeme lexbuf) s;
157 157
     raise (Error (Location.curr lexbuf)))
158
     
158

  
159 159

  
160 160
  let spec s =
161 161
    let lexbuf = Lexing.from_string s in
162 162
    try
163
      Parser_lustre.lustre_spec (*ParserLustreSpec.lustre_spec*) token lexbuf
163
      Parser_lustre.lustre_spec_main (*ParserLustreSpec.lustre_spec*) token lexbuf
164 164
    with Parsing.Parse_error ->
165 165
      raise (Error (Location.curr lexbuf))
166 166
}
src/parser_lustre.mly
84 84
%token EXISTS FORALL
85 85
%token PROTOTYPE LIB
86 86
%token EOF
87
%token END
87 88

  
88 89
%nonassoc prec_exists prec_forall
89 90
/* unused precedence rules*/
......
116 117
%nonassoc RBRACKET
117 118
%nonassoc LBRACKET
118 119

  
119
%start prog
120
%type <Lustre_types.top_decl list> prog
120
/* these XXX_main rules are used to avoid end-of-stream conflicts with
121
   menhir. See http://gallium.inria.fr/~fpottier/menhir/manual.html#sec43
122
*/
123
%start prog_main %type <Lustre_types.top_decl list>
124
prog_main
121 125

  
122
%start header
123
%type <Lustre_types.top_decl list> header
126
%start header_main
127
%type <Lustre_types.top_decl list> header_main
124 128

  
125
%start lustre_annot
126
%type <Lustre_types.expr_annot> lustre_annot
129
%start lustre_annot_main
130
%type <Lustre_types.expr_annot> lustre_annot_main
127 131

  
128
%start lustre_spec
129
%type <Lustre_types.contract_desc> lustre_spec
132
%start lustre_spec_main
133
%type <Lustre_types.contract_desc> lustre_spec_main
130 134

  
131
%start signed_const
132
%type <Lustre_types.constant> signed_const
135
%start signed_const_main
136
%type <Lustre_types.constant> signed_const_main
133 137

  
134
%start expr
135
%type <Lustre_types.expr> expr
138
%start expr_main
139
%type <Lustre_types.expr> expr_main
136 140

  
137
%start stmt_list
138
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list
141
%start stmt_list_main
142
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list_main
139 143

  
140
%start vdecl_list
141
%type <Lustre_types.var_decl list> vdecl_list
144
%start vdecl_list_main
145
%type <Lustre_types.var_decl list> vdecl_list_main
142 146
%%
143 147

  
144 148
module_ident:
......
168 172
type_ident:
169 173
  IDENT { $1 }
170 174

  
175
prog_main:
176
  | e = prog END { e }
177

  
171 178
prog:
172 179
 open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
173 180

  
174 181
typ_def_prog:
175 182
 typ_def_list { $1 false }
176 183

  
184
header_main:
185
  | e = header END { e }
186

  
177 187
header:
178 188
 open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) }
179 189

  
......
299 309
field_list:                           { [] }
300 310
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
301 311

  
312
stmt_list_main:
313
| e = stmt_list END { e }
314

  
302 315
stmt_list:
303 316
  { [], [], [] }
304 317
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
......
339 352
       ident_list      EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
340 353
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
341 354

  
355
lustre_spec_main:
356
  | e = lustre_spec END { e }
357

  
342 358
lustre_spec:
343
| contract EOF { $1 }
359
  | contract EOF { $1 }
344 360

  
345 361
contract:
346 362
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
......
390 406
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
391 407
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
392 408

  
409
expr_main:
410
  | e = expr END { e }
411

  
393 412
expr:
394 413
/* constants */
395 414
  INT {mkexpr (Expr_const (Const_int $1))}
......
521 540
| IDENT EQ signed_const { [ ($1, $3) ] }
522 541
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
523 542

  
543
signed_const_main:
544
  | e = signed_const END { e }
545

  
524 546
signed_const:
525 547
  INT {Const_int $1}
526 548
| REAL {let c,e,s =$1 in Const_real (c,e,s)}
......
587 609
  {[]}
588 610
| VAR local_vdecl_list SCOL {$2}
589 611

  
612
vdecl_list_main:
613
  | e = vdecl_list END { e }
614

  
590 615
vdecl_list:
591 616
  vdecl {$1}
592 617
| vdecl_list SCOL vdecl {$3 @ $1}
......
650 675
SCOL_opt:
651 676
    SCOL {} | {}
652 677

  
678
lustre_annot_main:
679
  | e = lustre_annot END { e }
653 680

  
654 681
lustre_annot:
655 682
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }

Also available in: Unified diff