Project

General

Profile

Download (20.7 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
module ISet = Utils.ISet
110

    
111
(* XXX: UNUSED *)
112
(* exception Unhandled of string *)
113

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

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

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

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

    
161
let branch_cpt = ref 0
162

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
403
and pp_emf_instrs m fmt instrs =
404
  pp_comma_list (pp_emf_instr m) fmt instrs
405

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

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

    
421
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
422

    
423
(* XXX: UNUSED *)
424
(* let pp_emf_spec_import fmt i =
425
 *   fprintf fmt "{@[";
426
 *   fprintf fmt "\"contract\": \"%s\",@ " i.import_nodeid;
427
 *   fprintf fmt "\"inputs\": [%a],@ " pp_emf_expr i.inputs;
428
 *   fprintf fmt "\"outputs\": [%a],@ " pp_emf_expr i.outputs;
429
 *   fprintf fmt "@]}"
430
 *
431
 * let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import *)
432

    
433
let pp_emf_spec fmt spec =
434
  fprintf fmt "{ @[<hov 0>";
435
  (* fprintf fmt "\"consts\": [%a],@ "
436
   *   pp_emf_consts spec.consts;
437
   * fprintf fmt "\"locals\": [%a],@ "
438
   *   pp_emf_vars_decl spec.locals;
439
   * fprintf fmt "\"stmts\": [%a],@ "
440
   *   pp_emf_stmts spec.stmts; *)
441

    
442
  (* TODO *)
443
  (* fprintf fmt "\"assume\": [%a],@ " pp_emf_eexprs spec.assume;
444
   * fprintf fmt "\"guarantees\": [%a],@ " pp_emf_eexprs spec.guarantees;
445
   * fprintf fmt "\"modes\": [%a]@ " pp_emf_spec_modes spec.modes; *)
446

    
447
   (* fprintf fmt "\"imports\": [%a]@ "
448
   *   pp_emf_spec_imports spec.imports; *)
449
  fprintf fmt "@] }"
450

    
451
let pp_emf_annots cpt fmt annots =
452
  pp_comma_list (pp_emf_annot cpt) fmt annots.annots
453

    
454
let pp_emf_annots_list cpt fmt annots_list =
455
  pp_comma_list (pp_emf_annots cpt) fmt annots_list
456

    
457
(* let pp_emf_contract fmt nd =
458
 *   let c = Printers.node_as_contract nd in
459
 *   fprintf fmt "@[<v 2>\"%a\": {@ "
460
 *     pp_protect (fun fmt -> pp_print_string fmt nd.node_id);
461
 *   fprintf fmt "\"contract\": %a@ "
462
 *     pp_emf_spec c;
463
 *   fprintf fmt "@]@ }" *)
464

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

    
504
(*let pp_machine fmt m =                      
505
  match m.mspec with
506
  | None | Some (NodeSpec _) -> pp_machine fmt m
507
  | Some (Contract _) -> pp_emf_contract fmt m
508
 *)
509

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

    
531
(****************************************************)
532
(* Main function: iterates over node and print them *)
533
(****************************************************)
534
let pp_meta fmt basename =
535
  fprintf fmt "\"meta\": @[<v 0>{@ ";
536
  Format.pp_comma_list
537
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
538
    fmt
539
    [
540
      "compiler-name", Filename.basename Sys.executable_name;
541
      "compiler-version", Version.number;
542
      "command", String.concat " " (Array.to_list Sys.argv);
543
      "source_file", basename;
544
    ];
545
  fprintf fmt "@ @]},@ "
546

    
547
let translate fmt basename prog machines =
548
  (* record_types prog; *)
549
  fprintf fmt "@[<v 0>{@ ";
550
  pp_meta fmt basename;
551
  (* Typedef *)
552
  fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "
553
    (pp_emf_list pp_emf_typedef)
554
    (Corelang.get_typedefs prog);
555
  fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "
556
    (pp_emf_list pp_emf_top_const)
557
    (Corelang.get_consts prog);
558
  fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
559
  pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);
560
  fprintf fmt "}@],@ ";
561
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
562
  (* Previous alternative: mapping normalized lustre to EMF:
563
     pp_comma_list pp_decl fmt prog; *)
564
  pp_emf_list pp_machine fmt machines;
565
  fprintf fmt "}@]@ }";
566
  fprintf fmt "@]@ }"
567

    
568
(* Local Variables: *)
569
(* compile-command: "make -C ../.." *)
570
(* End: *)
(1-1/7)