Project

General

Profile

Download (20 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
exception Unhandled of string
107

    
108
module ISet = Utils.ISet
109
let fprintf_list = Utils.fprintf_list
110
  
111

    
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
     (
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 c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then
130
		true
131
	      else
132
		assert false (* only handle true -> false *)
133
	   | _ -> assert false
134
	 )
135
	    
136
	 | _ -> false
137
       with
138
       | Not_found -> false (* Not declared (should have been detected now, or
139
			       imported node) *)
140
     )
141
  | _ -> false
142
     
143
     
144
     
145
let is_resetable_fun lustre_eq =
146
  (* We extract the clock if it exist from the original lustre equation *)
147
  match lustre_eq with
148
  | Some eq -> (
149
    match eq.eq_rhs.expr_desc with
150
    | Expr_appl(_,_,reset) -> (
151
      match reset with None -> false | Some _ -> true
152
    )
153
    | Expr_arrow _ -> true
154
    | _ -> Format.eprintf "reseting expr %a@.@?" Printers.pp_expr eq.eq_rhs; assert false
155
  )
156
  | None -> assert false (* should have been assigned to an original lustre equation *)
157

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

    
162
     
163

    
164
let branch_cpt = ref 0
165
let get_instr_id fmt i =
166
  match Corelang.get_instr_desc i with
167
  | MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
168
  | MSetReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
169
  (* TODO: handle clear_reset *)
170
  | MClearReset -> ()
171
  | MBranch _ -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
172
  | MStep (outs, id, _) ->
173
     print_protect fmt 
174
       (fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
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 = branch_instr_vars m i in
181
      ISet.union accu_all_def all_defined_vars,
182
      ISet.union accu_def common_def_vars,
183
      VSet.union accu_read read_vars)
184
    (ISet.empty, ISet.empty, VSet.empty) il
185
  
186
and branch_instr_vars m i =
187
  (* Returns all_outputs, outputs, inputs of the instruction. It is
188
     only called on MBranch instructions but evaluate recursively
189
     instructions appearing in branches.
190

    
191
     It is used to gather the global input/output of a switch and
192
     print it at the begin of the JSON subtree.
193

    
194
     The set "All outputs" is used to filter out input variables
195
     belong to that set. *)
196

    
197
  match Corelang.get_instr_desc i with
198
  | MLocalAssign (var,expr) 
199
    | MStateAssign (var,expr) -> ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
200
  | MStep (vars, f, args)  ->
201
     let is_stateful = List.mem_assoc f m.minstances in 
202
     let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
203
     let args_vars =
204
       List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args in
205
     
206
     lhs, lhs,
207
     (
208
       if is_stateful && is_resetable_fun i.lustre_eq then
209
	 let reset_var =
210
	   let loc = Location.dummy_loc in
211
	   Corelang.mkvar_decl loc
212
	     (reset_name f,
213
	      Corelang.mktyp loc Tydec_bool, Corelang.mkclock loc Ckdec_any,
214
	      false,
215
	      None,
216
	      None) 
217
	 in
218
	 VSet.add reset_var args_vars
219
       else
220
	 args_vars
221
     )
222
  | MBranch (g,(_,hd_il)::tl)     -> (* We focus on variables defined in all branches *)
223
     let read_guard = get_expr_vars g in
224
     (* Bootstrapping with first item *) 
225
     let all_def_vars_hd, def_vars_hd, read_vars_hd = branch_block_vars m hd_il in
226
     let all_def_vars, def_vars, read_vars =
227
       List.fold_left
228
	 (fun (all_def_vars, def_vars, read_vars) (_, il) ->
229
	   (* We accumulate reads but intersect writes *)
230
	   let all_writes_il, writes_il, reads_il = branch_block_vars m il in
231
	   ISet.union all_def_vars all_writes_il,
232
	   ISet.inter def_vars writes_il,
233
	   VSet.union read_vars reads_il
234
	 )
235
	 (all_def_vars_hd, def_vars_hd, read_vars_hd)
236
	 tl
237
     in
238
     (* all_def_vars correspond to variables written or defined in one
239
        of the branch. It may happen that a variable is defined in one
240
        but not in the other, because of reset for example.  
241

    
242
        def_vars are variables defined in all branches. *)
243

    
244

    
245
     all_def_vars, def_vars, VSet.union read_guard read_vars
246
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
247
  | MSetReset ni
248
  | MNoReset ni ->
249
    let write = ISet.singleton (reset_name ni) in
250
    write, write, VSet.empty
251
  (* TODO: handle clear_reset and reset flag *)
252
  | MClearReset | MResetAssign _ -> ISet.empty, ISet.empty, VSet.empty
253
  | MSpec _ | MComment _ -> assert false (* not  available for EMF output *)
254
     
255
(* A kind of super join_guards: all MBranch are postponed and sorted by
256
   guards so they can be easier merged *)
257
let merge_branches instrs =
258
  let instrs, branches =
259
    List.fold_right (fun i (il, branches) ->
260
      match Corelang.get_instr_desc i with
261
	MBranch _ -> il, i::branches
262
      | _ -> i::il, branches
263
    ) instrs ([],[])
264
  in
265
  let sorting_branches b1 b2 =
266
    match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with
267
    | MBranch(g1, _), MBranch(g2, _) ->
268
       compare g1 g2
269
    | _ -> assert false
270
  in
271
  let sorted_branches = List.sort sorting_branches branches in
272
  instrs @ (join_guards_list sorted_branches)
273
    
274
let rec pp_emf_instr m fmt i =
275
  let pp_content fmt i =
276
    match Corelang.get_instr_desc i with
277
    | MLocalAssign(lhs, expr) ->
278
      begin match expr.value_desc with
279
        | Fun (fun_id, vl) ->
280
          (* Thanks to normalization, vl shall only contain constant or
281
             local/state vars but not calls to other functions *)
282
          fprintf fmt "\"kind\": \"operator\",@ ";
283
          fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
284
          fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
285
            fun_id
286
            (pp_emf_cst_or_var_list m) vl
287
        | Array _ | Access _ | Power _
288
        | Cst _
289
        | Var _ ->
290
          fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
291
            pp_var_name lhs
292
            (pp_emf_cst_or_var m) expr
293
        | ResetFlag ->
294
          (* TODO: handle reset flag *)
295
          assert false
296
      end
297

    
298
    | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
299
                                 variable or a constant, no function anymore! *)
300
      -> (
301
          fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
302
            pp_var_name lhs
303
            (pp_emf_cst_or_var m) expr
304
        )
305

    
306
    | MSetReset id
307
      -> (
308
          fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
309
            (reset_name id)
310
        )
311
    | MNoReset id           
312
      -> (
313
          fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
314
            (reset_name id)
315
        )
316
    (* TODO: handle clear_reset and reset flag *)
317
    | MClearReset | MResetAssign _ -> ()
318

    
319
    | MBranch (g, hl) -> (
320
        let all_outputs, outputs, inputs = branch_instr_vars m i in
321
        (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
322
        (* 	Machine_code.pp_instr i *)
323
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
324
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)
325
        (* 	pp_emf_vars_decl *)
326
        (* 	(VSet.elements inputs) *)
327

    
328
        (* ; *)
329
        let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
330
      (* Format.eprintf "Filtering in: %a@.@." *)
331
      (* 	pp_emf_vars_decl *)
332
      (* 	(VSet.elements inputs) *)
333

    
334
      (* ; *)
335
      fprintf fmt "\"kind\": \"branch\",@ ";
336
      fprintf fmt "\"guard\": %a,@ " (pp_emf_cst_or_var m) g; (* it has to be a variable or a constant *)
337
      fprintf fmt "\"outputs\": [%a],@ " (fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs);
338
      fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl
339
	(* (let guard_inputs = get_expr_vars g in
340
	   VSet.elements (VSet.diff inputs guard_inputs)) -- previous version to
341
	   remove guard's variable from inputs *)
342
	(VSet.elements inputs)
343
      ;
344
      fprintf fmt "@[<v 2>\"branches\": {@ @[<v 0>%a@]@]@ }"
345
	(fprintf_list ~sep:",@ "
346
	   (fun fmt (tag, instrs_tag) ->
347
	     let branch_all_lhs, _, branch_inputs = branch_block_vars m instrs_tag in
348
	     let branch_inputs = VSet.filter (fun v -> not (ISet.mem v.var_id branch_all_lhs)) branch_inputs in
349
	     fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt -> Format.pp_print_string fmt tag);
350
	     fprintf fmt "\"guard_value\": \"%a\",@ " pp_tag_id tag; 
351
	     fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl (VSet.elements branch_inputs); 
352
	     fprintf fmt "@[<v 2>\"instrs\": {@ ";
353
	     (pp_emf_instrs m) fmt instrs_tag;
354
	     fprintf fmt "@]@ }";
355
	     fprintf fmt "@]@ }"
356
	   )
357
	)
358
	hl
359
    )
360

    
361
    | MStep ([var], f, _) when is_arrow_fun m i -> (* Arrow case *) (
362
      fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""
363
	f
364
	pp_var_name var
365
	(reset_name f)
366
    )
367

    
368
    | MStep (outputs, f, inputs) when not (is_imported_node f m) -> (
369
      let node_f = get_node_def f m in
370
      let is_stateful = List.mem_assoc f m.minstances in 
371
      fprintf fmt "\"kind\": \"%s\",@ \"name\": \"%a\",@ \"id\": \"%s\",@ "
372
	(if is_stateful then "statefulcall" else "statelesscall")
373
	print_protect (fun fmt -> pp_print_string fmt (node_f.node_id)) 
374
	f;
375
      fprintf fmt "\"lhs\": [@[%a@]],@ \"args\": [@[%a@]]"
376
	(fprintf_list ~sep:",@ " (fun fmt v -> fprintf fmt "\"%a\"" pp_var_name v)) outputs
377
	(pp_emf_cst_or_var_list m) inputs;
378
      if is_stateful then
379
	fprintf fmt ",@ \"reset\": { \"name\": \"%s\", \"resetable\": \"%b\"}"
380
	  (reset_name f)
381
	  (is_resetable_fun i.lustre_eq)	  
382
      else fprintf fmt "@ "
383
    )
384

    
385
    | MStep(outputs, f, inputs ) -> (* This is an imported node *)
386
       EMF_library_calls.pp_call fmt m f outputs inputs
387
	 
388
    | MSpec _ | MComment _ 
389
      -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
390
  (* not  available for EMF output *)
391
  in
392
    fprintf fmt "@[ @[<v 2>\"%a\": {@ " get_instr_id i;
393
    fprintf fmt "%a" pp_content i;
394
    fprintf fmt "@]@]@ }"
395
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
396

    
397
let pp_emf_annot cpt fmt (key, ee) =
398
  let _ =
399
    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }"
400
      !cpt
401
      (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) key
402
      pp_emf_eexpr ee
403
  in
404
  incr cpt
405

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

    
418
let pp_emf_spec_import fmt i =
419
  fprintf fmt "{@[";
420
  fprintf fmt "\"contract\": \"%s\",@ "
421
    i.import_nodeid;
422
  fprintf fmt "\"inputs\": [%a],@ "
423
    pp_emf_expr i.inputs;
424
  fprintf fmt "\"outputs\": [%a],@ "
425
    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],@ "
439
    pp_emf_eexprs spec.assume;
440
  fprintf fmt "\"guarantees\": [%a],@ "
441
    pp_emf_eexprs spec.guarantees;
442
  fprintf fmt "\"modes\": [%a]@ "
443
    pp_emf_spec_modes spec.modes;
444
  (* fprintf fmt "\"imports\": [%a]@ "
445
   *   pp_emf_spec_imports spec.imports;   *)
446
  fprintf fmt "@] }"
447
  
448
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
449
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (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 = (*merge_branches*) m.mstep.step_instrs in
461
  try
462
    fprintf fmt "@[<v 2>\"%a\": {@ "
463
      print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
464
    (match m.mspec.mnode_spec with
465
     | Some (Contract _) -> fprintf fmt "\"contract\": \"true\",@ "
466
     | _ -> ());
467
    fprintf fmt "\"imported\": \"false\",@ ";
468
    fprintf fmt "\"kind\": %t,@ "
469
      (fun fmt -> if not ( snd (get_stateless_status m) )
470
	then fprintf fmt "\"stateful\""
471
	else fprintf fmt "\"stateless\"");
472
    fprintf fmt "\"inputs\": [%a],@ "
473
      pp_emf_vars_decl m.mstep.step_inputs;
474
    fprintf fmt "\"outputs\": [%a],@ "
475
      pp_emf_vars_decl m.mstep.step_outputs;
476
    fprintf fmt "\"locals\": [%a],@ "
477
      pp_emf_vars_decl m.mstep.step_locals;
478
    fprintf fmt "\"mems\": [%a],@ "
479
      pp_emf_vars_decl m.mmemory;
480
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
481
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
482
      (pp_emf_instrs m) instrs;
483
    (match m.mspec.mnode_spec with
484
     | None -> ()
485
     | Some (Contract c) -> (
486
         assert (c.locals = [] && c.consts = [] && c.stmts = [] && c.imports = []);
487
         fprintf fmt "\"spec\": %a,@ " pp_emf_spec c
488
       )
489
     | Some (NodeSpec id) -> fprintf fmt "\"contract\": \"%s\",@ " id
490
    );
491
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
492
    fprintf fmt "@]@ }"
493
  with Unhandled msg -> (
494
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
495
      m.mname.node_id;
496
    eprintf "%s@ " msg;
497
    eprintf "node skipped - no output generated@ @]@."
498
  )
499

    
500
(*let pp_machine fmt m =                      
501
  match m.mspec with
502
  | None | Some (NodeSpec _) -> pp_machine fmt m
503
  | Some (Contract _) -> pp_emf_contract fmt m
504
 *)
505
                      
506
let pp_emf_imported_node fmt top =
507
  let ind = Corelang.imported_node_of_top top in
508
  try
509
    fprintf fmt "@[<v 2>\"%a\": {@ "
510
      print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);
511
    fprintf fmt "\"imported\": \"true\",@ ";
512
    fprintf fmt "\"inputs\": [%a],@ "
513
      pp_emf_vars_decl ind.nodei_inputs;
514
    fprintf fmt "\"outputs\": [%a],@ "
515
      pp_emf_vars_decl ind.nodei_outputs;
516
    fprintf fmt "\"original_name\": \"%s\"" ind.nodei_id;
517
    (match ind.nodei_spec with None -> fprintf fmt "@ "
518
                             | Some (Contract _) -> assert false (* should have been processed *)
519
                             | Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id
520
    );
521
    fprintf fmt "@]@ }"
522
  with Unhandled msg -> (
523
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
524
      ind.nodei_id;
525
    eprintf "%s@ " msg;
526
    eprintf "node skipped - no output generated@ @]@."
527
  )
528
(****************************************************)
529
(* Main function: iterates over node and print them *)
530
(****************************************************)
531
let pp_meta fmt basename =
532
  fprintf fmt "\"meta\": @[<v 0>{@ ";
533
  Utils.fprintf_list ~sep:",@ "
534
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
535
    fmt
536
    ["compiler-name", (Filename.basename Sys.executable_name);
537
     "compiler-version", Version.number;
538
     "command", (String.concat " " (Array.to_list Sys.argv));
539
     "source_file", basename
540
    ]
541
  ;
542
  fprintf fmt "@ @]},@ "
543
    
544
let translate fmt basename prog machines =
545
  (* record_types prog; *)
546
  fprintf fmt "@[<v 0>{@ ";
547
  pp_meta fmt basename;
548
  (* Typedef *)
549
  fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "
550
    (pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog);
551
  fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "
552
    (pp_emf_list pp_emf_top_const) (Corelang.get_consts prog);
553
  fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
554
  pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);
555
  fprintf fmt "}@],@ ";
556
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
557
  (* Previous alternative: mapping normalized lustre to EMF: 
558
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
559
  pp_emf_list pp_machine fmt machines;
560
  fprintf fmt "}@]@ }";
561
  fprintf fmt "@]@ }"
562

    
563
(* Local Variables: *)
564
(* compile-command: "make -C ../.." *)
565
(* End: *)
(1-1/4)