Project

General

Profile

Download (19.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 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 *)
252
  | MClearReset -> 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
      -> (
279
	(match expr.value_desc with
280
	| Fun (fun_id, vl) -> (
281
	  (* Thanks to normalization, vl shall only contain constant or
282
	     local/state vars but not calls to other functions *)
283
	  fprintf fmt "\"kind\": \"operator\",@ ";
284
	  fprintf fmt "\"lhs\": \"%a\",@ " pp_var_name lhs;
285
	  fprintf fmt "\"name\": \"%s\",@ \"args\": [@[%a@]]"
286
	    fun_id
287
	    (pp_emf_cst_or_var_list m) vl
288
	)	 
289
	| Array _ | Access _ | Power _ 
290
	| Cst _ 
291
	| Var _ -> (
292
	  fprintf fmt "\"kind\": \"local_assign\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
293
	    pp_var_name lhs
294
	    (pp_emf_cst_or_var m) expr
295
	))    )
296

    
297
    | MStateAssign(lhs, expr) (* a Pre construct Shall only be defined by a
298
				 variable or a constant, no function anymore! *)
299
      -> (
300
	fprintf fmt "\"kind\": \"pre\",@ \"lhs\": \"%a\",@ \"rhs\": %a"
301
	  pp_var_name lhs
302
	  (pp_emf_cst_or_var m) expr
303
      )
304
       
305
    | MSetReset id
306
      -> (
307
	fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"true\""
308
	  (reset_name id)
309
      )
310
    | MNoReset id           
311
      -> (
312
	fprintf fmt "\"kind\": \"reset\",@ \"lhs\": \"%s\",@ \"rhs\": \"false\""
313
	  (reset_name id)
314
      )
315
  (* TODO: handle clear_reset *)
316
  | MClearReset -> ()
317
       
318
    | MBranch (g, hl) -> (
319
      let all_outputs, outputs, inputs = branch_instr_vars m i in
320
      (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
321
      (* 	Machine_code.pp_instr i *)
322
      (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
323
      (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements outputs) *)
324
      (* 	pp_emf_vars_decl *)
325
      (* 	(VSet.elements inputs) *)
326

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

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

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

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

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

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

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

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

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