Project

General

Profile

Download (19.8 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 Lustrec.Lustre_types
102
open Lustrec.Machine_code_types
103
open Lustrec.Machine_code_common
104
open Format 
105
open EMF_common
106
exception Unhandled of string
107

    
108
module ISet = Lustrec.Utils.ISet
109
let fprintf_list = Lustrec.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 Lustrec.Corelang.get_instr_desc i with
121
  | MStep ([var], 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 = Lustrec.Corelang.const_of_bool true && c2 = Lustrec.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@.@?" Lustrec.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 Lustrec.Corelang.get_instr_desc i with
167
  | MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
168
  | MReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
169
  | MBranch (g, _) -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
170
  | MStep (outs, id, _) ->
171
     print_protect fmt 
172
       (fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
173
  | _ -> () (* No name *)
174

    
175
let rec branch_block_vars m il =
176
  List.fold_left
177
    (fun (accu_all_def, accu_def, accu_read) i ->
178
      let all_defined_vars, common_def_vars, read_vars = branch_instr_vars m i in
179
      ISet.union accu_all_def all_defined_vars,
180
      ISet.union accu_def common_def_vars,
181
      VSet.union accu_read read_vars)
182
    (ISet.empty, ISet.empty, VSet.empty) il
183
  
184
and branch_instr_vars m i =
185
  (* Returns all_outputs, outputs, inputs of the instruction. It is
186
     only called on MBranch instructions but evaluate recursively
187
     instructions appearing in branches.
188

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

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

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

    
240
        def_vars are variables defined in all branches. *)
241

    
242

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

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

    
321
      (* ; *)
322
      let inputs = VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs in
323
      (* Format.eprintf "Filtering in: %a@.@." *)
324
      (* 	pp_emf_vars_decl *)
325
      (* 	(VSet.elements inputs) *)
326

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

    
354
    | MStep ([var], f, _) when is_arrow_fun m i -> (* Lustrec.Arrow case *) (
355
      fprintf fmt "\"kind\": \"arrow\",@ \"name\": \"%s\",@ \"lhs\": \"%a\",@ \"rhs\": \"%s\""
356
	f
357
	pp_var_name var
358
	(reset_name f)
359
    )
360

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

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

    
390
let pp_emf_annot cpt fmt (key, ee) =
391
  let _ =
392
    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }"
393
      !cpt
394
      (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) key
395
      pp_emf_eexpr ee
396
  in
397
  incr cpt
398

    
399
let pp_emf_spec_mode fmt m =
400
  fprintf fmt "{@[";
401
  fprintf fmt "\"mode_id\": \"%s\",@ "
402
    m.mode_id;
403
  fprintf fmt "\"ensure\": [%a],@ "
404
    pp_emf_eexprs m.ensure;
405
  fprintf fmt "\"require\": [%a]@ "
406
    pp_emf_eexprs m.require;
407
  fprintf fmt "@]}"
408
  
409
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
410

    
411
let pp_emf_spec_import fmt i =
412
  fprintf fmt "{@[";
413
  fprintf fmt "\"contract\": \"%s\",@ "
414
    i.import_nodeid;
415
  fprintf fmt "\"inputs\": [%a],@ "
416
    pp_emf_expr i.inputs;
417
  fprintf fmt "\"outputs\": [%a],@ "
418
    pp_emf_expr i.outputs;
419
  fprintf fmt "@]}"
420
  
421
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
422

    
423
let pp_emf_spec fmt spec =
424
  fprintf fmt "{ @[<hov 0>";
425
  (* fprintf fmt "\"consts\": [%a],@ "
426
   *   pp_emf_consts spec.consts;
427
   * fprintf fmt "\"locals\": [%a],@ "
428
   *   pp_emf_vars_decl spec.locals;
429
   * fprintf fmt "\"stmts\": [%a],@ "
430
   *   pp_emf_stmts spec.stmts; *)
431
  fprintf fmt "\"assume\": [%a],@ "
432
    pp_emf_eexprs spec.assume;
433
  fprintf fmt "\"guarantees\": [%a],@ "
434
    pp_emf_eexprs spec.guarantees;
435
  fprintf fmt "\"modes\": [%a]@ "
436
    pp_emf_spec_modes spec.modes;
437
  (* fprintf fmt "\"imports\": [%a]@ "
438
   *   pp_emf_spec_imports spec.imports;   *)
439
  fprintf fmt "@] }"
440
  
441
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
442
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
443

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

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

    
553
(* Local Variables: *)
554
(* compile-command: "make -C ../.." *)
555
(* End: *)
(2-2/4)