Project

General

Profile

Download (20.6 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 Lustre_types
102
open Machine_code_types
103
open Machine_code_common
104
open Format
105
open EMF_common
106

    
107
exception Unhandled of string
108

    
109
module ISet = Utils.ISet
110

    
111
let fprintf_list = Utils.fprintf_list
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" (fprintf_list ~sep:"_" pp_var_name) outs id)
174
  | _ -> ()
175
(* No name *)
176

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

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

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

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

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

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

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

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

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

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

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

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

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

    
400
and pp_emf_instrs m fmt instrs =
401
  fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
402

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

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

    
418
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
419

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

    
427
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
428

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

    
444
let pp_emf_annots cpt fmt annots =
445
  fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
446

    
447
let pp_emf_annots_list cpt fmt annots_list =
448
  fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
449

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

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

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

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

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

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

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