Project

General

Profile

Download (20.5 KB) Statistics
| Branch: | Tag: | Revision:
1
(* EMF backend *)
2
(* This backup is initially motivated by the need to express Spacer computed
3
   invariants as Matlab Simulink executable evidences.
4

    
5
   Therefore the input language is more restricted. We do not expect fancy
6
   datastructure, complex function calls, etc.
7

    
8
   In case of error, use -node foo -inline to eliminate function calls that are
9
   not seriously handled yet.
10
   
11

    
12
   In terms of algorithm, the process was initially based on printing normalized
13
   code. We now rely on machine code printing. The old code is available in old
14
   commits (eg in dd71e482a9d0).
15

    
16
   
17
   A (normalized) node becomes a JSON struct
18
   node foo (in1, in2: int) returns (out1, out2: int);
19
   var x : int;
20
   let
21
   x = bar(in1, in2); -- a stateful node
22
   out1 = x;
23
   out2 = in2;
24
   tel
25

    
26
   Since foo contains a stateful node, it is stateful itself. Its prototype is 
27
   extended with a reset input. When the node is reset, each of its "pre" expression
28
   is reset as well as all calls to stateful node it contains. 
29

    
30
   will produce the following JSON struct:
31
   "foo": {"kind":  "stateful",
32
   inputs:  [{name: "in1", type: "int"}, 
33
   {name: "in2", type: "int"}, 
34
   ],
35
   outputs: [{name: "out1", type: "int"}, {name: "out2", type: "int"}],
36
   locals:  [{name: "x", type: "int"}],
37
   instrs:  {
38
   def_x: { lhs: ["x"], 
39
   rhs: {type: "statefulcall", name: "bar", 
40
   args: [in1, in2], reset: [ni4_reset] } 
41
   }
42
   
43
   def_out1: { lhs: "out1", rhs: "x" } ,
44
   def_out2: { lhs: "out2", rhs: "in2"}
45
   }
46
   }
47

    
48
   Basically we have the following different definitions
49
   1. local assign of a variable to another one:
50
   def_out1: { kind: "local_assign", lhs: "out1", rhs: "x" },
51

    
52
   2. pre construct over a variable (this is a state assign):
53
   def_pre_x: { kind: "pre", lhs: "pre_x", rhs: "x" },
54

    
55
   3. arrow constructs, while there is not specific input, it could be reset 
56
   by a specific signal. We register it as a fresh rhs var:
57
   def_arrow: { kind: "arrow", name: "ni4", lhs: "is_init", rhs: "reset_ni4"}
58

    
59
   2. call to a stateless function, typically an operator
60
   def_x: { kind: "statelesscall", lhs: ["x"], 
61
   name: "bar", rhs: [in1, in2]} 
62
   
63
   or in the operator version 
64
   def_x: { kind: "operator", lhs: ["x"], 
65
   name: "+", rhs: [in1, in2]} 
66
   
67

    
68
   In Simulink this should introduce a subsystem in the first case or a 
69
   regular block in the second with card(lhs) outputs and card{args} inputs.
70

    
71
   3. call to a stateful node. It is similar to the stateless above, 
72
   with the addition of the reset argument
73
   { def_x: { kind: "statefulcall", lhs: ["x"], 
74
   name: "bar", rhs: [in1, in2], reset: [ni4_reset] } 
75
   }
76
   
77
   In lustrec compilation phases, a unique id is associated to this specific
78
   instance of stateful node "bar", here ni4. 
79
   Instruction such as reset(ni4) or noreset(ni4) may -- or not -- reset this 
80
   specific node. This corresponds to "every c" suffix of a node call in lustre.
81

    
82
   In Simulink this should introduce a subsystem that has this extra reset input.  
83
   The reset should be defined as an "OR" over (1) the input reset of the parent 
84
   node, __reset in the present example and (2) any occurence of reset(ni4) in 
85
   the instructions.
86

    
87
   4. branching construct: (guard expr, (tag, instr list) list)
88
   "merge_XX": { type: "branch", guard: "var_guard", 
89
   inputs:   ["varx", "vary"],
90
   outputs:  ["vark", "varz"],
91
   branches: {"tag1": {liste_of_definitions (1-4)}, ...}
92
   }
93
   
94

    
95
   In Simulink, this should become one IF block to produce enable ports 
96
   "var_guard == tag1", "var_guard == tag2", .... as well as one action 
97
   block per branch: each of these action block shall  
98

    
99
*)
100

    
101
open Utils
102
open Lustre_types
103
open Corelang
104
open Machine_code_types
105
open Machine_code_common
106
open Format
107
open EMF_common
108

    
109
exception Unhandled of string
110

    
111
module ISet = Utils.ISet
112

    
113
(**********************************************)
114
(*   Utility functions: arrow and lustre expr *)
115
(**********************************************)
116

    
117
(* detect whether the instruction i represents an ARROW, ie an arrow with true
118
   -> false *)
119
let is_arrow_fun m i =
120
  match Corelang.get_instr_desc i with
121
  | MStep ([ _ ], i, vl) -> (
122
      try
123
        let name = (get_node_def i m).node_id in
124
        match name, vl with
125
        | "_arrow", [ v1; v2 ] -> (
126
            match v1.value_desc, v2.value_desc with
127
            | Cst c1, Cst c2 ->
128
                if
129
                  c1 = Corelang.const_of_bool true
130
                  && c2 = Corelang.const_of_bool false
131
                then true
132
                else assert false
133
            (* only handle true -> false *)
134
            | _ -> assert false)
135
        | _ -> false
136
      with Not_found ->
137
        false
138
        (* Not declared (should have been detected now, or
139
           imported node) *))
140
  | _ -> false
141

    
142
let is_resetable_fun lustre_eq =
143
  (* We extract the clock if it exist from the original lustre equation *)
144
  match lustre_eq with
145
  | Some eq -> (
146
      match eq.eq_rhs.expr_desc with
147
      | Expr_appl (_, _, reset) -> (
148
          match reset with None -> false | Some _ -> true)
149
      | Expr_arrow _ -> true
150
      | _ ->
151
          Format.eprintf "reseting expr %a@.@?" Printers.pp_expr eq.eq_rhs;
152
          assert false)
153
  | None -> assert false
154
(* should have been assigned to an original lustre equation *)
155

    
156
(**********************************************)
157
(*   Printing machine code as EMF             *)
158
(**********************************************)
159

    
160
let branch_cpt = ref 0
161

    
162
let get_instr_id fmt i =
163
  match Corelang.get_instr_desc i with
164
  | MLocalAssign (lhs, _) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
165
  | MSetReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
166
  (* TODO: handle clear_reset *)
167
  | MClearReset -> ()
168
  | MBranch _ ->
169
      incr branch_cpt;
170
      fprintf fmt "branch_%i" !branch_cpt
171
  | MStep (outs, id, _) ->
172
      print_protect fmt (fun fmt ->
173
        fprintf fmt "%a_%s" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "_")
174
                               pp_var_name) outs id)
175
  | _ -> ()
176
(* No name *)
177

    
178
let rec branch_block_vars m il =
179
  List.fold_left
180
    (fun (accu_all_def, accu_def, accu_read) i ->
181
      let all_defined_vars, common_def_vars, read_vars =
182
        branch_instr_vars m i
183
      in
184
      ( ISet.union accu_all_def all_defined_vars,
185
        ISet.union accu_def common_def_vars,
186
        VSet.union accu_read read_vars ))
187
    (ISet.empty, ISet.empty, VSet.empty)
188
    il
189

    
190
and branch_instr_vars m i =
191
  (* Returns all_outputs, outputs, inputs of the instruction. It is
192
     only called on MBranch instructions but evaluate recursively
193
     instructions appearing in branches.
194

    
195
     It is used to gather the global input/output of a switch and
196
     print it at the begin of the JSON subtree.
197

    
198
     The set "All outputs" is used to filter out input variables
199
     belong to that set. *)
200
  match Corelang.get_instr_desc i with
201
  | MLocalAssign (var, expr) | MStateAssign (var, expr) ->
202
      ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
203
  | MStep (vars, f, args) ->
204
      let is_stateful = List.mem_assoc f m.minstances in
205
      let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
206
      let args_vars =
207
        List.fold_left
208
          (fun accu v -> VSet.union accu (get_expr_vars v))
209
          VSet.empty args
210
      in
211

    
212
      ( lhs,
213
        lhs,
214
        if is_stateful && is_resetable_fun i.lustre_eq then
215
          let reset_var =
216
            let loc = Location.dummy in
217
            Corelang.mkvar_decl loc
218
              ( reset_name f,
219
                Corelang.mktyp loc Tydec_bool,
220
                Corelang.mkclock loc Ckdec_any,
221
                false,
222
                None,
223
                None )
224
          in
225
          VSet.add reset_var args_vars
226
        else args_vars )
227
  | MBranch (g, (_, hd_il) :: tl) ->
228
      (* We focus on variables defined in all branches *)
229
      let read_guard = get_expr_vars g in
230
      (* Bootstrapping with first item *)
231
      let all_def_vars_hd, def_vars_hd, read_vars_hd =
232
        branch_block_vars m hd_il
233
      in
234
      let all_def_vars, def_vars, read_vars =
235
        List.fold_left
236
          (fun (all_def_vars, def_vars, read_vars) (_, il) ->
237
            (* We accumulate reads but intersect writes *)
238
            let all_writes_il, writes_il, reads_il = branch_block_vars m il in
239
            ( ISet.union all_def_vars all_writes_il,
240
              ISet.inter def_vars writes_il,
241
              VSet.union read_vars reads_il ))
242
          (all_def_vars_hd, def_vars_hd, read_vars_hd)
243
          tl
244
      in
245

    
246
      (* all_def_vars correspond to variables written or defined in one
247
         of the branch. It may happen that a variable is defined in one
248
         but not in the other, because of reset for example.
249

    
250
         def_vars are variables defined in all branches. *)
251
      all_def_vars, def_vars, VSet.union read_guard read_vars
252
  | MBranch _ ->
253
      assert false (* branch instruction should admit at least one case *)
254
  | MSetReset ni | MNoReset ni ->
255
      let write = ISet.singleton (reset_name ni) in
256
      write, write, VSet.empty
257
  (* TODO: handle clear_reset and reset flag *)
258
  | MClearReset | MResetAssign _ -> ISet.empty, ISet.empty, VSet.empty
259
  | MSpec _ | MComment _ -> assert false
260
(* not  available for EMF output *)
261

    
262
(* A kind of super join_guards: all MBranch are postponed and sorted by
263
   guards so they can be easier merged *)
264
let merge_branches instrs =
265
  let instrs, branches =
266
    List.fold_right
267
      (fun i (il, branches) ->
268
        match Corelang.get_instr_desc i with
269
        | MBranch _ -> il, i :: branches
270
        | _ -> i :: il, branches)
271
      instrs ([], [])
272
  in
273
  let sorting_branches b1 b2 =
274
    match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with
275
    | MBranch (g1, _), MBranch (g2, _) -> compare g1 g2
276
    | _ -> assert false
277
  in
278
  let sorted_branches = List.sort sorting_branches branches in
279
  instrs @ join_guards_list sorted_branches
280

    
281
let rec pp_emf_instr m fmt i =
282
  let pp_content fmt i =
283
    match Corelang.get_instr_desc i with
284
    | MLocalAssign (lhs, expr) -> (
285
        match expr.value_desc with
286
        | Fun (fun_id, vl) ->
287
            (*
288
           Thanks to normalization, vl shall only contain constant or
289
           local/state vars but not calls to other functions *)
290
            fprintf fmt "\"kind\": \"operator\",@ ";
291
            fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
292
            fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]" fun_id
293
              (pp_emf_cst_or_var_list m) vl
294
        | Array _ | Access _ | Power _ | Cst _ | Var _ ->
295
            fprintf fmt
296
              "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
297
              pp_var_name lhs (pp_emf_cst_or_var m) expr
298
        | ResetFlag ->
299
            (* TODO: handle reset flag *)
300
            assert false)
301
    | MStateAssign (lhs, expr)
302
    (* a Pre construct Shall only be defined by a
303
       variable or a constant, no function anymore! *) ->
304
        fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
305
          pp_var_name lhs (pp_emf_cst_or_var m) expr
306
    | MSetReset id ->
307
        fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
308
          (reset_name id)
309
    | MNoReset id ->
310
        fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
311
          (reset_name id)
312
    (* TODO: handle clear_reset and reset flag *)
313
    | MClearReset | MResetAssign _ -> ()
314
    | MBranch (g, hl) ->
315
        let all_outputs, outputs, inputs = branch_instr_vars m i in
316

    
317
        (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
318
        (* 	Machine_code.pp_instr i *)
319
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
320
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)
321
        (* 	pp_emf_vars_decl *)
322
        (* 	(VSet.elements inputs) *)
323

    
324
        (* ; *)
325
        let inputs =
326
          VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs
327
        in
328

    
329
        (* Format.eprintf "Filtering in: %a@.@." *)
330
        (* 	pp_emf_vars_decl *)
331
        (* 	(VSet.elements inputs) *)
332

    
333
        (* ; *)
334
        fprintf fmt "\"kind\": \"branch\",@ ";
335
        fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g;
336
        (* it has to be a variable or a constant *)
337
        fprintf fmt "\"outputs\": [%a],@ "
338
          (pp_comma_list pp_var_string)
339
          (ISet.elements outputs);
340
        fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
341
          (*
342
           (let guard_inputs = get_expr_vars g in
343
           VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to
344
           remove guard's variable from inputs *)
345
          (VSet.elements inputs);
346
        fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"
347
          (pp_comma_list (fun fmt (tag, instrs_tag) ->
348
               let branch_all_lhs, _, branch_inputs =
349
                 branch_block_vars m instrs_tag
350
               in
351
               let branch_inputs =
352
                 VSet.filter
353
                   (fun v -> not (ISet.mem v.var_id branch_all_lhs))
354
                   branch_inputs
355
               in
356
               fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->
357
                   Format.pp_print_string fmt tag);
358
               fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag;
359
               fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
360
                 (VSet.elements branch_inputs);
361
               fprintf fmt "@[<v 2>\"instrs\": {@ ";
362
               (pp_emf_instrs m) fmt instrs_tag;
363
               fprintf fmt "@]@ }";
364
               fprintf fmt "@]@ }"))
365
          hl
366
    | MStep ([ var ], f, _) when is_arrow_fun m i ->
367
        (* Arrow case *)
368
        fprintf fmt
369
          "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \
370
           \"%s\""
371
          f pp_var_name var (reset_name f)
372
    | MStep (outputs, f, inputs) when not (is_imported_node f m) ->
373
        let node_f = get_node_def f m in
374
        let is_stateful = List.mem_assoc f m.minstances in
375
        fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "
376
          (if is_stateful then "statefulcall" else "statelesscall")
377
          print_protect
378
          (fun fmt -> pp_print_string fmt node_f.node_id)
379
          f;
380
        fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
381
          (pp_comma_list (fun fmt v ->
382
               fprintf fmt "\"%a\"" pp_var_name v))
383
          outputs (pp_emf_cst_or_var_list m) inputs;
384
        if is_stateful then
385
          fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"
386
            (reset_name f)
387
            (is_resetable_fun i.lustre_eq)
388
        else fprintf fmt "@ "
389
    | MStep (outputs, f, inputs) ->
390
        (* This is an imported node *)
391
        EMF_library_calls.pp_call fmt m f outputs inputs
392
    | MSpec _ | MComment _ ->
393
        Format.eprintf "unhandled comment in EMF@.@?";
394
        assert false
395
    (* not  available for EMF output *)
396
  in
397
  fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
398
  fprintf fmt "%a" pp_content i;
399
  fprintf fmt "@]@]@ }"
400

    
401
and pp_emf_instrs m fmt instrs =
402
  pp_comma_list (pp_emf_instr m) fmt instrs
403

    
404
let pp_emf_annot cpt fmt (key, ee) =
405
  let _ =
406
    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }" !cpt
407
      (pp_comma_list (fun fmt s -> fprintf fmt "\"%s\"" s))
408
      key pp_emf_eexpr ee
409
  in
410
  incr cpt
411

    
412
let pp_emf_spec_mode fmt m =
413
  fprintf fmt "{@[";
414
  fprintf fmt "\"mode_id\": \"%s\",@ " m.mode_id;
415
  fprintf fmt "\"ensure\": [%a],@ " pp_emf_eexprs m.ensure;
416
  fprintf fmt "\"require\": [%a]@ " pp_emf_eexprs m.require;
417
  fprintf fmt "@]}"
418

    
419
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
420

    
421
let pp_emf_spec_import fmt i =
422
  fprintf fmt "{@[";
423
  fprintf fmt "\"contract\": \"%s\",@ " i.import_nodeid;
424
  fprintf fmt "\"inputs\": [%a],@ " pp_emf_expr i.inputs;
425
  fprintf fmt "\"outputs\": [%a],@ " pp_emf_expr i.outputs;
426
  fprintf fmt "@]}"
427

    
428
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
429

    
430
let pp_emf_spec fmt spec =
431
  fprintf fmt "{ @[<hov 0>";
432
  (* fprintf fmt "\"consts\": [%a],@ "
433
   *   pp_emf_consts spec.consts;
434
   * fprintf fmt "\"locals\": [%a],@ "
435
   *   pp_emf_vars_decl spec.locals;
436
   * fprintf fmt "\"stmts\": [%a],@ "
437
   *   pp_emf_stmts spec.stmts; *)
438
  fprintf fmt "\"assume\": [%a],@ " pp_emf_eexprs spec.assume;
439
  fprintf fmt "\"guarantees\": [%a],@ " pp_emf_eexprs spec.guarantees;
440
  fprintf fmt "\"modes\": [%a]@ " pp_emf_spec_modes spec.modes;
441
  (* fprintf fmt "\"imports\": [%a]@ "
442
   *   pp_emf_spec_imports spec.imports; *)
443
  fprintf fmt "@] }"
444

    
445
let pp_emf_annots cpt fmt annots =
446
  pp_comma_list (pp_emf_annot cpt) fmt annots.annots
447

    
448
let pp_emf_annots_list cpt fmt annots_list =
449
  pp_comma_list (pp_emf_annots cpt) fmt annots_list
450

    
451
(* let pp_emf_contract fmt nd =
452
 *   let c = Printers.node_as_contract nd in
453
 *   fprintf fmt "@[<v 2>\"%a\": {@ "
454
 *     print_protect (fun fmt -> pp_print_string fmt nd.node_id);
455
 *   fprintf fmt "\"contract\": %a@ "
456
 *     pp_emf_spec c;
457
 *   fprintf fmt "@]@ }" *)
458

    
459
let pp_machine fmt m =
460
  let instrs =
461
    (*merge_branches*)
462
    m.mstep.step_instrs
463
  in
464
  try
465
    fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->
466
        pp_print_string fmt m.mname.node_id);
467
    (match m.mspec.mnode_spec with
468
    | Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "
469
    | _ -> ());
470
    fprintf fmt "\"imported\": \"false\",@ ";
471
    fprintf fmt "\"kind\": %t,@ " (fun fmt ->
472
        if not (snd (get_stateless_status m)) then fprintf fmt "\"stateful\""
473
        else fprintf fmt "\"stateless\"");
474
    fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_inputs;
475
    fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl m.mstep.step_outputs;
476
    fprintf fmt "\"locals\": [%a],@ " pp_emf_vars_decl m.mstep.step_locals;
477
    fprintf fmt "\"mems\": [%a],@ " pp_emf_vars_decl m.mmemory;
478
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
479
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ " (pp_emf_instrs m) instrs;
480
    (match m.mspec.mnode_spec with
481
    | None -> ()
482
    | Some (Contract c) ->
483
        assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
484
        fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
485
    | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id);
486
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }"
487
      (pp_emf_annots_list (ref 0))
488
      m.mannot;
489
    fprintf fmt "@]@ }"
490
  with Unhandled msg ->
491
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
492
      m.mname.node_id;
493
    eprintf "%s@ " msg;
494
    eprintf "node skipped - no output generated@ @]@."
495

    
496
(*let pp_machine fmt m =                      
497
  match m.mspec with
498
  | None | Some (NodeSpec _) -> pp_machine fmt m
499
  | Some (Contract _) -> pp_emf_contract fmt m
500
 *)
501

    
502
let pp_emf_imported_node fmt top =
503
  let ind = Corelang.imported_node_of_top top in
504
  try
505
    fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->
506
        pp_print_string fmt ind.nodei_id);
507
    fprintf fmt "\"imported\": \"true\",@ ";
508
    fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl ind.nodei_inputs;
509
    fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl ind.nodei_outputs;
510
    fprintf fmt "\"original_name\": \"%s\"" ind.nodei_id;
511
    (match ind.nodei_spec with
512
    | None -> fprintf fmt "@ "
513
    | Some (Contract _) -> assert false (* should have been processed *)
514
    | Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id);
515
    fprintf fmt "@]@ }"
516
  with Unhandled msg ->
517
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
518
      ind.nodei_id;
519
    eprintf "%s@ " msg;
520
    eprintf "node skipped - no output generated@ @]@."
521

    
522
(****************************************************)
523
(* Main function: iterates over node and print them *)
524
(****************************************************)
525
let pp_meta fmt basename =
526
  fprintf fmt "\"meta\": @[<v 0>{@ ";
527
  Format.pp_comma_list
528
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
529
    fmt
530
    [
531
      "compiler-name", Filename.basename Sys.executable_name;
532
      "compiler-version", Version.number;
533
      "command", String.concat " " (Array.to_list Sys.argv);
534
      "source_file", basename;
535
    ];
536
  fprintf fmt "@ @]},@ "
537

    
538
let translate fmt basename prog machines =
539
  (* record_types prog; *)
540
  fprintf fmt "@[<v 0>{@ ";
541
  pp_meta fmt basename;
542
  (* Typedef *)
543
  fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "
544
    (pp_emf_list pp_emf_typedef)
545
    (Corelang.get_typedefs prog);
546
  fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "
547
    (pp_emf_list pp_emf_top_const)
548
    (Corelang.get_consts prog);
549
  fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
550
  pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);
551
  fprintf fmt "}@],@ ";
552
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
553
  (* Previous alternative: mapping normalized lustre to EMF:
554
     pp_comma_list pp_decl fmt prog; *)
555
  pp_emf_list pp_machine fmt machines;
556
  fprintf fmt "}@]@ }";
557
  fprintf fmt "@]@ }"
558

    
559
(* Local Variables: *)
560
(* compile-command: "make -C ../.." *)
561
(* End: *)
(1-1/7)