Project

General

Profile

Revision 217837e2

View differences:

src/compiler_common.ml
35 35
      end
36 36
  end
37 37

  
38
(* Loading Lusi file and filling type tables with parsed
38
(* Loading Lus/Lusi file and filling type tables with parsed
39 39
   functions/nodes *)
40
let parse_header own filename =
40
let parse filename extension =
41 41
  Location.set_input filename;
42
  let h_in = open_in filename in
43
  let lexbuf = Lexing.from_channel h_in in
42
  let f_in = open_in filename in
43
  let lexbuf = Lexing.from_channel f_in in
44 44
  Location.init lexbuf filename;
45 45
  (* Parsing *)
46
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);
46
  let prog = 
47 47
    try
48
      let header = Parse.header Parser_lustre.header Lexer_lustre.token lexbuf in
49
      (*ignore (Modules.load_header ISet.empty header);*)
50
      close_in h_in;
51
      header
48
      match extension with
49
        ".lusi" ->
50
        Log.report ~level:1
51
          (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);
52
        Parse.header Parser_lustre.header Lexer_lustre.token lexbuf 
53
      | ".lus" ->
54
         Log.report ~level:1 
55
           (fun fmt -> fprintf fmt ".. parsing source file %s@ " filename);
56
         Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf
57
      | _ -> assert false
52 58
    with
53 59
    | (Parse.Error err) as exc -> 
54
      Parse.report_error err;
55
      raise exc
60
       Parse.report_error err;
61
       raise exc
56 62
    | Corelang.Error (loc, err) as exc -> (
57 63
      eprintf "Parsing error: %a%a@."
58
	Error.pp_error_msg err
59
	Location.pp_loc loc;
64
        Error.pp_error_msg err
65
        Location.pp_loc loc;
60 66
      raise exc
61 67
    )
62

  
63
let parse_source source_name =
64
  (* Loading the input file *)
65
  Location.set_input source_name;
66
  let s_in = open_in source_name in
67
  let lexbuf = Lexing.from_channel s_in in
68
  Location.init lexbuf source_name;
69

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

  
88 73
let expand_automata decls =
89 74
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. expanding automata@ ");
......
169 154
   (Env.initial, Env.initial)
170 155
 *)
171 156

  
172
let generate_lusic_header destname lusic_ext =	
173
  match !Options.output with
174
  | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
175
  | _ -> ()
176 157
	 
177 158

  
178 159
    
src/compiler_stages.ml
15 15
   compiled header *)
16 16
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
17 17
  let destname = !Options.dest_dir ^ "/" ^ basename in
18
  let lusic_ext = extension ^ "c" in
18
  let lusic_ext = ".lusic" in
19 19
  let header_name = destname ^ lusic_ext in
20 20
  begin
21
    if not (Sys.file_exists header_name) then
21
    if (* Generating the lusic file *)
22
      extension = ".lusi" (* because input is a lusi *)
23
      || (extension = ".lus" &&
24
            not (Sys.file_exists header_name))
25
           (* or because it is a lus but not lusic exists *)
26
      || (let lusic = Lusic.read_lusic destname lusic_ext in
27
          not lusic.Lusic.from_lusi)
28
         (* or the lusic exists but is not generated from a lusi, hence it
29
            has te be regenerated *)
30
    then
22 31
      begin
23 32
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
24
	Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
25
	if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
33
	Lusic.write_lusic
34
          (extension = ".lusi") (* is it a lusi file ? *)
35
          (if extension = ".lusi" then prog else Lusic.extract_header dirname basename prog)
36
          destname
37
          lusic_ext;
38
        let _ =
39
          match !Options.output with
40
          | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
41
          | _ -> ()
42
        in
43
        ()
44
      end
45
    else (* Lusic exists and is usable. Checking compatibility *)
46
      begin
47
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
48
        let lusic = Lusic.read_lusic destname lusic_ext in
49
        Lusic.check_obsolete lusic destname;
50
	let header = lusic.Lusic.contents in
51
	let (declared_types_env, declared_clocks_env) = Modules.get_envs_from_top_decls header in
52
	check_compatibility
53
	  (prog, computed_types_env, computed_clocks_env)
54
	  (header, declared_types_env, declared_clocks_env)
26 55
      end
27
    else
28
      let lusic = Lusic.read_lusic destname lusic_ext in
29
      if not lusic.Lusic.from_lusi then
30
	begin
31
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
32
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
33
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
34
	  if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
35
	end
36
      else
37
	begin
38
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
39
	  Lusic.check_obsolete lusic destname;
40
	  let header = lusic.Lusic.contents in
41
	  let (declared_types_env, declared_clocks_env) = Modules.get_envs_from_top_decls header in
42
	  check_compatibility
43
	    (prog, computed_types_env, computed_clocks_env)
44
	    (header, declared_types_env, declared_clocks_env)
45
	end
46 56
  end
47 57

  
48 58

  
49 59
(* From prog to prog *)
50
let stage1 params prog dirname basename =
60
let stage1 params prog dirname basename extension =
51 61
  (* Updating parent node information for variables *)
52 62
  Compiler_common.update_vdecl_parents_prog prog;
53 63

  
......
56 66
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
57 67

  
58 68
  (* Importing source *)
59
  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:false prog in
60

  
69
  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:(extension = ".lusi") prog in
70
  
61 71
  (* Registering types and clocks for future checks *)
62 72
  Global.type_env := Env.overwrite !Global.type_env typ_env;
63 73
  Global.clock_env := Env.overwrite !Global.clock_env clk_env;
......
135 145
  create_dest_dir ();
136 146

  
137 147
  (* Compatibility with Lusi *)
138
  (* Checking the existence of a lusi (Lustre Interface file) *)
139
  let extension = ".lusi" in
140
  compile_source_to_header prog !Global.type_env !Global.clock_env dirname basename extension;
141

  
148
  (* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)
149
  compile_source_to_header
150
    prog !Global.type_env !Global.clock_env dirname basename extension;
151
 
152
    
142 153
  Typing.uneval_prog_generics prog;
143 154
  Clock_calculus.uneval_prog_generics prog;
144 155

  
......
246 257

  
247 258

  
248 259
(* printing code *)
249
let stage3 prog machine_code dependencies basename =
260
let stage3 prog machine_code dependencies basename extension =
250 261
  let basename    =  Filename.basename basename in
251
  match !Options.output with
252
    "C" -> 
262
  match !Options.output, extension with
263
    "C", ".lus" -> 
264
     begin
265
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
266
       C_backend.translate_to_c
267
	 (* alloc_header_file source_lib_file source_main_file makefile_file *)
268
	 basename prog machine_code dependencies
269
     end
270
  |  "C", _ -> 
253 271
      begin
254
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
255
	C_backend.translate_to_c
256
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
257
	  basename prog machine_code dependencies
272
      	Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");
258 273
      end
259
  | "java" ->
274
  | "java", _ ->
260 275
     begin
261 276
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
262 277
     (*let source_file = basename ^ ".java" in
......
266 281
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
267 282
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
268 283
     end
269
  | "horn" ->
284
  | "horn", _ ->
270 285
     begin
271 286
       let destname = !Options.dest_dir ^ "/" ^ basename in
272 287
       let source_file = destname ^ ".smt2" in (* Could be changed *)
......
283 298
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
284 299
       )
285 300
     end
286
  | "lustre" ->
301
  | "lustre", _ ->
287 302
     begin
288 303
       let destname = !Options.dest_dir ^ "/" ^ basename in
289
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
304
       let source_file = destname ^ ".lustrec" ^ extension  in (* Could be changed *)
305
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. exporting processed file as %s@," source_file);
290 306
       let source_out = open_out source_file in
291 307
       let fmt = formatter_of_out_channel source_out in
292 308
       Printers.pp_prog fmt prog;
......
294 310
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
295 311
       ()
296 312
     end
297
  | "emf" ->
313
  | "emf", _ ->
298 314
     begin
299 315
       let destname = !Options.dest_dir ^ "/" ^ basename in
300 316
       let source_file = destname ^ ".emf" in (* Could be changed *)
src/main_lustre_compiler.ml
34 34
    close_out h_out
35 35
  end
36 36

  
37
(* compile a .lusi header file *)
38
let compile_header dirname  basename extension =
39
  let destname = !Options.dest_dir ^ "/" ^ basename in
40
  let header_name = basename ^ extension in
41
  let lusic_ext = extension ^ "c" in
42
  begin
43
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
44
    let header = parse_header true (dirname ^ "/" ^ header_name) in
45
    (* Disbaled today, should be done anyway when following the regular compilation 
46
ignore (Modules.load ~is_header:true ISet.empty header); *)
47
    ignore (check_top_decls header); (* typing/clocking with an empty env *)
48
    create_dest_dir ();
49
    Log.report ~level:1
50
      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
51
    Lusic.write_lusic true header destname lusic_ext;
52
    generate_lusic_header destname lusic_ext;
53

  
54

  
55

  
56
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@ ")
57
  end
58 37

  
59 38

  
60 39

  
61 40

  
62 41

  
63 42
(* compile a .lus source file *)
64
let rec compile_source dirname basename extension =
43
let rec compile dirname basename extension =
65 44
  let source_name = dirname ^ "/" ^ basename ^ extension in
66 45

  
67 46
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
68 47

  
69 48
  (* Parsing source *)
70
  let prog = parse_source source_name in
49
  let prog = parse source_name extension in
71 50

  
72 51
  let prog =
73
    if !Options.mpfr then
52
    if !Options.mpfr &&
53
         extension = ".lus" (* trying to avoid the injection of the module for lusi files *) 
54
    then
74 55
      Mpfr.mpfr_module::prog
75 56
    else
76 57
      prog
......
80 61
  let prog, dependencies = 
81 62
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
82 63
    try 
83
      Compiler_stages.stage1 params prog dirname basename
64
      Compiler_stages.stage1 params prog dirname basename extension
84 65
    with Compiler_stages.StopPhase1 prog -> (
85 66
      if !Options.lusi then
86 67
	begin
......
118 99
  let machine_code = Plugins.refine_machine_code prog machine_code in
119 100
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ @ ");
120 101
  
121
  Compiler_stages.stage3 prog machine_code dependencies basename;
102
  Compiler_stages.stage3 prog machine_code dependencies basename extension;
122 103
  begin
123 104
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
124 105
    (* We stop the process here *)
......
127 108

  
128 109
let compile dirname basename extension =
129 110
  match extension with
130
  | ".lusi"  -> compile_header dirname basename extension
131
  | ".lus"   -> compile_source dirname basename extension
111
  | ".lusi"  
112
  | ".lus"   -> compile dirname basename extension
132 113
  | _        -> assert false
133 114

  
134 115
let anonymous filename =
src/main_lustre_testgen.ml
44 44
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
45 45

  
46 46
  (* Parsing source *)
47
  let prog = parse_source source_name in
47
  let prog = parse source_name extension in
48 48
  let params = Backends.get_normalization_params () in
49
  let prog, dependencies = Compiler_stages.stage1 params prog dirname basename in
49
  let prog, dependencies = Compiler_stages.stage1 params prog dirname basename extension in
50 50

  
51 51
  (* Two cases
52 52
     - generation of coverage conditions
src/main_lustre_verifier.ml
48 48
  decr Options.verbose_level;
49 49

  
50 50
  (* Parsing source *)
51
  let prog = parse_source source_name in
51
  let prog = parse source_name extension in
52 52

  
53 53
  (* Checking which solver is active *)
54 54
  incr Options.verbose_level;
......
63 63
      incr Options.verbose_level;
64 64
      let params = Verifier.get_normalization_params () in
65 65
      decr Options.verbose_level;
66
      Compiler_stages.stage1 params prog dirname basename
66
      Compiler_stages.stage1 params prog dirname basename extension
67 67
    with Compiler_stages.StopPhase1 prog -> (
68 68
        assert false
69 69
    )
src/modules.ml
213 213
         )
214 214
      | Include name ->
215 215
         let basename = Options_management.name_dependency (true, name) "" in
216
         let include_src = Compiler_common.parse_source basename in
217
         load_rec ~is_header:false accu include_src
218
                         
219

  
216
         if Filename.check_suffix basename ".lus" then
217
           let include_src = Compiler_common.parse basename ".lus" in
218
           load_rec ~is_header:false accu include_src
219
         else
220
           raise (Error (decl.top_decl_loc, LoadError("include requires a lustre file")))
221
   
220 222
      | Node nd ->
221 223
         if is_header then
222 224
           raise (Error(decl.top_decl_loc,
src/parsers/parse.ml
41 41
  | Node_spec_error s       -> fprintf fmt "Impossible to parse the following node specification:@.%s@.@?" s
42 42

  
43 43
let report_error (loc, err) =
44
  eprintf "Syntax error: %a%a@."
44
  eprintf "Syntax error: %a@.%a@."
45 45
    pp_error err
46 46
    Location.pp_loc loc
47 47

  
src/parsers/parser_lustre.mly
361 361
    { merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
362 362
| CONST IDENT COL typeconst EQ expr SCOL contract
363 363
    { merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
364
| VAR IDENT EQ expr SCOL contract
365
    { merge_contracts (mk_contract_var $2 false None $4 (get_loc())) $6 }
366 364
| VAR IDENT COL typeconst EQ expr SCOL contract
367 365
    { merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
368 366
| ASSUME qexpr SCOL contract
src/printers.ml
289 289
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
290 290
    pp_expr e.eexpr_qfexpr
291 291

  
292
    
293
let pp_spec_eq fmt eq = 
294
  fprintf fmt "var %a : %a = %a;" 
295
    pp_eq_lhs eq.eq_lhs
296
    Types.print_node_ty eq.eq_rhs.expr_type
297
    pp_expr eq.eq_rhs
298
  
299
let pp_spec_stmt fmt stmt =
300
  match stmt with
301
  | Eq eq -> pp_spec_eq fmt eq
302
  | Aut aut -> assert false (* Not supported yet *)
303
             
304
  
292 305
let pp_spec fmt spec =
293
  fprintf fmt "@[<hov 2>(*@@ ";
294 306
  (* const are prefixed with const in pp_var and with nothing for regular
295 307
     variables. We adapt the call to produce the appropriate output. *)
296
  fprintf_list ~sep:"@,@@ " (fun fmt v ->
297
    fprintf fmt "%s%a = %t;"
298
      (if v.var_dec_const then "" else "var")
308
    fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->
309
    fprintf fmt "const %a = %t;"
299 310
      pp_var v
300
      (fun fmt -> match v.var_dec_value with None -> () | Some e -> pp_expr fmt e)
301
  ) fmt (spec.consts @ spec.locals);
302
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
303
  fprintf_list ~sep:"@,@@ " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
304
  fprintf_list ~sep:"@,@@ " (fun fmt mode ->
311
      (fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)
312
    ) fmt spec.consts;
313
  
314
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
315
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
316
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantees %a;" pp_eexpr r) fmt spec.guarantees;
317
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
305 318
    fprintf fmt "mode %s (@[@ %a@ %a@]);" 
306 319
      mode.mode_id
307
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
308
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
320
      (fprintf_list ~eol:"@," ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
321
      (fprintf_list ~eol:"@," ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
309 322
  ) fmt spec.modes;
310
  fprintf_list ~sep:"@,@@ " (fun fmt import ->
323
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
311 324
    fprintf fmt "import %s (%a) returns (%a);" 
312 325
      import.import_nodeid
313 326
      (fprintf_list ~sep:"@ " pp_expr) import.inputs
314 327
      (fprintf_list ~sep:"@ " pp_expr) import.outputs
315
  ) fmt spec.imports;
316
  fprintf fmt "@]*)";
317
  ()
328
  ) fmt spec.imports
318 329

  
330
let pp_spec_as_comment fmt spec =
331
  fprintf fmt "@[<hov 2>(*@@ ";
332
  pp_spec fmt spec;
333
  fprintf fmt "@]*)@ "
319 334
    
320 335
let pp_node fmt nd =
321 336
  fprintf fmt "@[<v 0>";
......
327 342
    pp_node_args nd.node_outputs;
328 343
  (* Contracts *)
329 344
  fprintf fmt "%a%t"
330
    (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
345
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) nd.node_spec
331 346
    (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ");
332 347
  (* Locals *)
333 348
  fprintf fmt "%a" (fun fmt locals ->
......
361 376
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
362 377

  
363 378
let pp_imported_node fmt ind = 
364
  fprintf fmt "@[<v>%s %s (%a) returns (%a)@]"
379
  fprintf fmt "@[<v 0>";
380
  (* Prototype *)
381
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
365 382
    (if ind.nodei_stateless then "function" else "node")
366 383
    ind.nodei_id
367 384
    pp_node_args ind.nodei_inputs
368
    pp_node_args ind.nodei_outputs
385
    pp_node_args ind.nodei_outputs;
386
  (* Contracts *)
387
  fprintf fmt "%a%t"
388
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt s | _ -> ()) ind.nodei_spec
389
    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
390
  fprintf fmt "@]@ "
391
  
369 392

  
370 393
let pp_const_decl fmt cdecl =
371 394
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
src/tools/stateflow/sf_sem.ml
82 82
     Format.fprintf auto_fmt "%a@." Printers.pp_prog prog;
83 83

  
84 84
     let params = Backends.get_normalization_params () in
85
     let prog, deps = Compiler_stages.stage1 params prog "" "" in
85
     let prog, deps = Compiler_stages.stage1 params prog "" "" ".lus" in
86 86

  
87 87

  
88 88
     Options.print_dec_types := false;
src/typing.ml
27 27
open Format
28 28

  
29 29

  
30
(* TODO general remark: expect in the add_vdelc, it seems to me that
31
   all the pairs (env, vd_env) should be replace with just env, since
32
   vd_env is never used and the env element is always extract with a
33
   fst *)
34

  
35
   
30 36
module type EXPR_TYPE_HUB =
31 37
sig
32 38
  type type_expr 
......
663 669
    let check_vd_env vd_env =
664 670
      ignore (List.fold_left add_vdecl [] vd_env)
665 671

  
666
    let type_spec env c =
672
    let type_spec env spec =
673
      let vd_env = spec.consts @ spec.locals in
674
      check_vd_env vd_env;
675
      let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in
676
      (* typing stmts *)
677
      let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) spec.stmts  in
678
      let undefined_vars_init =
679
        List.fold_left
680
          (fun uvs v -> ISet.add v.var_id uvs)
681
          ISet.empty spec.locals
682
      in
683
      let _ =
684
        List.fold_left
685
          (type_eq (env, vd_env) (false (*is_main*)))
686
          undefined_vars_init
687
          eqs
688
      in
689
      
667 690
      (*TODO 
668 691
        enrich env locally with locals and consts
669 692
        type each pre/post as a boolean expr
......
699 722
          type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
700 723
        )  nd.node_asserts;
701 724
      (* Typing spec/contracts *)
702
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec (new_env, vd_env) spec));
725
      (match nd.node_spec with None -> () | Some spec -> ignore (type_spec new_env spec));
703 726
      (* Typing annots *)
704 727
      List.iter (fun annot ->
705 728
          List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
......
719 742
      Env.add_value env nd.node_id ty_node
720 743

  
721 744
    let type_imported_node env nd loc =
722
      let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in
723 745
      let vd_env = nd.nodei_inputs@nd.nodei_outputs in
724 746
      check_vd_env vd_env;
725
      ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);
747
      let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in
748
      let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in
749
      let new_env = Env.overwrite env delta_env in
750
      (* Typing spec *)
751
      (match nd.nodei_spec with None -> () | Some spec -> ignore (type_spec new_env spec)); 
726 752
      let ty_ins = type_of_vlist nd.nodei_inputs in
727 753
      let ty_outs = type_of_vlist nd.nodei_outputs in
728 754
      let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
src/utils/utils.ml
253 253
let pp_newline_if_non_empty l =
254 254
  (fun fmt -> match l with [] -> () | _ -> Format.fprintf fmt "@,")
255 255

  
256
let rec fprintf_list ~sep:sep f fmt = function
256
let fprintf_list ?(eol:('a, formatter, unit) Pervasives.format = "") ~sep:sep f fmt l =
257
  let rec aux fmt = function
257 258
  | []   -> ()
258 259
  | [e]  -> f fmt e
259
  | x::r -> Format.fprintf fmt "%a%(%)%a" f x sep (fprintf_list ~sep f) r
260

  
260
  | x::r -> Format.fprintf fmt "%a%(%)%a" f x sep aux r
261
  in
262
  match l with
263
  | [] -> ()
264
  | _ -> (
265
    aux fmt l;
266
    Format.fprintf fmt "%(%)" eol
267
  )                 
268
   
261 269
let pp_list l pp_fun beg_str end_str sep_str =
262 270
  if (beg_str="\n") then
263 271
    print_newline ()

Also available in: Unified diff