Project

General

Profile

Download (20.8 KB) Statistics
| Branch: | Tag: | Revision:
1 3ca27bc7 ploc
(* 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 preserved for
14
   reference.
15
*)
16
17 a6df3992 Ploc
open LustreSpec
18 f7caf067 ploc
open Machine_code
19 a6df3992 Ploc
open Format
20
open Utils
21
22 f7caf067 ploc
exception Unhandled of string
23 3ca27bc7 ploc
    
24
25
(* Basic printing functions *)
26
    
27 a6df3992 Ploc
let pp_var_string fmt v = fprintf fmt "\"%s\"" v
28
let pp_var_name fmt v = fprintf fmt "\"%a\"" Printers.pp_var_name v
29
let pp_node_args = fprintf_list ~sep:", " pp_var_name
30
31 3ca27bc7 ploc
    
32
(* Matlab starting counting from 1.
33
   simple function to extract the element id in the list. Starts from 1. *)
34 f7caf067 ploc
let rec get_idx x l =
35
  match l with
36
  | hd::tl -> if hd = x then 1 else 1+(get_idx x tl)
37
  | [] -> assert false
38 3ca27bc7 ploc
39
(**********************************************)
40
(* Old stuff: printing normalized code as EMF *)     
41
(**********************************************)
42
43
(*
44 a6df3992 Ploc
let pp_expr vars fmt expr =
45
  let rec pp_expr fmt expr =
46
    match expr.expr_desc with
47
    | Expr_const c -> Printers.pp_const fmt c
48
    | Expr_ident id ->
49
       if List.mem id vars then
50 32539b6d ploc
	 Format.fprintf fmt "u%i" (get_idx id vars)
51 a6df3992 Ploc
       else
52
	 assert false (* impossible to find element id in var list *)
53
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
54
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
55
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
56
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
57 97be8db8 Teme
    | Expr_ite (c, t, e) -> fprintf fmt "if %a; y=(%a); else y=(%a); end" pp_expr c pp_expr t pp_expr e
58 a6df3992 Ploc
    | Expr_arrow (e1, e2) ->(
59
      match e1.expr_desc, e2.expr_desc with
60
      | Expr_const c1, Expr_const c2 -> if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then fprintf fmt "STEP" else assert false (* only handle true -> false *)
61
      | _ -> assert false (* only handle true -> false *)
62
    )
63
    | Expr_fby (e1, e2) -> assert false (* not covered yet *)
64 30dee850 Teme
    | Expr_pre e -> fprintf fmt "UNITDELAY"
65 a6df3992 Ploc
    | Expr_when (e, id, l) -> assert false (* clocked based expressions are not handled yet *)
66
    | Expr_merge (id, hl) -> assert false (* clocked based expressions are not handled yet *)
67
    | Expr_appl (id, e, r) -> pp_app fmt id e r
68
69
  and pp_tuple fmt el =
70
    fprintf_list ~sep:"," pp_expr fmt el
71
72
  and pp_app fmt id e r =
73
    match r with
74
    | None -> pp_call fmt id e
75
    | Some c -> assert false (* clocked based expressions are not handled yet *)
76
77
  and pp_call fmt id e =
78
    match id, e.expr_desc with
79
    | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
80
    | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
81
    | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
82
    | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
83
    | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
84
    | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "mod (%a, %a)" pp_expr e1 pp_expr e2
85
    | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a & %a)" pp_expr e1 pp_expr e2
86
    | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a | %a)" pp_expr e1 pp_expr e2
87
    | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "xor (%a, %a)" pp_expr e1 pp_expr e2
88
    | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "((~%a) | %a)" pp_expr e1 pp_expr e2
89
    | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
90
    | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
91
    | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
92
    | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
93 97be8db8 Teme
    | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a ~= %a)" pp_expr e1 pp_expr e2
94
    | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_expr e1 pp_expr e2
95 a6df3992 Ploc
    | "not", _ -> fprintf fmt "(~%a)" pp_expr e
96
    | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
97
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
98
99
  in
100
  pp_expr fmt expr
101
102
let pp_stmt fmt stmt =
103
  match stmt with
104
  | Eq eq -> (
105
    match eq.eq_lhs with
106
      [var] -> (
107
     (* first, we extract the expression and associated variables *)
108
	let vars = Utils.ISet.elements (Corelang.get_expr_vars eq.eq_rhs) in
109 97be8db8 Teme
110 d3e837ea Ploc
	fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @]}"
111 a6df3992 Ploc
	  var
112
	  (pp_expr vars) eq.eq_rhs (* todo_pp_expr expr *)
113
	  (fprintf_list ~sep:", " pp_var_string) vars
114
      )
115
    | _ -> assert false (* should not happen for input of EMF backend (cocospec generated nodes *)
116
  )
117
  | _ -> assert false (* should not happen with EMF backend *)
118
119
let pp_node fmt nd =
120 d3e837ea Ploc
  fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ "
121 a6df3992 Ploc
    nd.node_id
122
    pp_node_args nd.node_inputs
123
    pp_node_args nd.node_outputs;
124
  fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }"
125 d3e837ea Ploc
    (fprintf_list ~sep:",@ " pp_stmt ) nd.node_stmts;
126 a6df3992 Ploc
  fprintf fmt "@]@ }"
127 30dee850 Teme
128 a6df3992 Ploc
let pp_decl fmt decl =
129
  match decl.top_decl_desc with
130
  | Node nd -> fprintf fmt "%a@ " pp_node nd
131 30dee850 Teme
  | ImportedNode _
132 a6df3992 Ploc
  | Const _
133 30dee850 Teme
  | Open _
134 a6df3992 Ploc
  | TypeDef _ -> eprintf "should not happen in EMF backend"
135 3ca27bc7 ploc
*)
136
137
138
(**********************************************)
139
(*   Printing machine code as EMF             *)
140
(**********************************************)
141 a6df3992 Ploc
142 524060b3 ploc
(* detect whether the instruction i represents an ARROW, ie an arrow with true
143
   -> false *)
144
let is_arrow_fun m i =
145
  match Corelang.get_instr_desc i with
146
  | MStep ([var], i, vl)  -> (
147
    let name = try (Machine_code.get_node_def i m).node_id with Not_found -> Format.eprintf "Impossible to find node %s@.@?" i; raise Not_found in
148
    match name, vl with
149
    | "_arrow", [v1; v2] -> (
150
	match v1.value_desc, v2.value_desc with
151
	| Cst c1, Cst c2 ->
152
	   if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then
153
	     true
154
	   else
155
	     assert false (* only handle true -> false *)
156
	| _ -> assert false
157
    )
158
    | _ -> false
159
  )
160
  | _ -> false
161
162
let pp_original_lustre_expression m fmt i =
163
  match Corelang.get_instr_desc i with
164
  | MLocalAssign _ | MStateAssign _ 
165
  | MBranch _
166
    -> ( match i.lustre_eq with None -> () | Some e -> Printers.pp_node_eq fmt e) 
167
  | MStep _ when is_arrow_fun m i -> () (* we print nothing, this is a STEP *)
168
  | MStep _ -> (match i.lustre_eq with None -> () | Some eq -> Printers.pp_node_eq fmt eq)
169
  | _ -> ()
170
171
172 145379a9 ploc
(* Print machine code values as matlab expressions. Variable identifiers are
173
   replaced by uX where X is the index of the variables in the list vars of input
174
   variables. *)
175 524060b3 ploc
let rec pp_matlab_val vars fmt v =
176 f7caf067 ploc
  match v.value_desc with
177
  | Cst c -> Printers.pp_const fmt c
178
  | LocalVar v
179
  | StateVar v ->
180
     let id = v.var_id in
181
     if List.mem id vars then
182 32539b6d ploc
       Format.fprintf fmt "u%i" (get_idx id vars)
183 f7caf067 ploc
     else
184 524060b3 ploc
       let _ = Format.eprintf "Error: looking for var %s in %a@.@?" id (Utils.fprintf_list ~sep:"," Format.pp_print_string) vars in assert false (* impossible to find element id in var list *)
185 f7caf067 ploc
  | Fun (n, vl) -> pp_fun vars n fmt vl
186
  | _ -> assert false (* not available in EMF backend *)
187
and pp_fun vars id fmt vl =
188 145379a9 ploc
  (* eprintf "print %s with %i args@.@?" id (List.length vl);*)
189 f7caf067 ploc
  match id, vl with
190 524060b3 ploc
    | "+", [v1;v2] -> fprintf fmt "(%a + %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
191
    | "uminus", [v] -> fprintf fmt "(- %a)" (pp_matlab_val vars) v
192
    | "-", [v1;v2] -> fprintf fmt "(%a - %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
193
    | "*",[v1;v2] -> fprintf fmt "(%a * %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
194
    | "/", [v1;v2] -> fprintf fmt "(%a / %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
195
    | "mod", [v1;v2] -> fprintf fmt "mod (%a, %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
196
    | "&&", [v1;v2] -> fprintf fmt "(%a & %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
197
    | "||", [v1; v2] -> fprintf fmt "(%a | %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
198
    | "xor", [v1; v2] -> fprintf fmt "xor (%a, %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
199
    | "impl", [v1; v2] -> fprintf fmt "((~%a) | %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
200
    | "<", [v1; v2] -> fprintf fmt "(%a < %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
201
    | "<=", [v1; v2] -> fprintf fmt "(%a <= %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
202
    | ">", [v1; v2] -> fprintf fmt "(%a > %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
203
    | ">=", [v1; v2] -> fprintf fmt "(%a >= %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
204
    | "!=", [v1; v2] -> fprintf fmt "(%a != %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
205
    | "=", [v1; v2] -> fprintf fmt "(%a = %a)" (pp_matlab_val vars) v1 (pp_matlab_val vars) v2
206
    | "not", [v] -> fprintf fmt "(~%a)" (pp_matlab_val vars) v
207
    | _ -> fprintf fmt "%s (%a)" id  (Utils.fprintf_list ~sep:", " (pp_matlab_val vars)) vl 
208 a6df3992 Ploc
209 3ca27bc7 ploc
     
210 1bff14ac ploc
211 145379a9 ploc
(* pp_basic_instr prints regular instruction. These do not contain MStep which
212
   should have been already filtered out. Another restriction which is supposed
213
   to be enforced is that branching statement contain a single instruction (in
214
   practice it has to be an assign) *)
215 524060b3 ploc
let pp_matlab_basic_instr m vars fmt i =
216 1bff14ac ploc
  match Corelang.get_instr_desc i with
217
  | MLocalAssign (var,v) 
218 524060b3 ploc
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_matlab_val vars) v
219 f7caf067 ploc
  | MReset _           
220 145379a9 ploc
    -> Format.eprintf "unhandled reset in EMF@.@?"; assert false
221 f7caf067 ploc
  | MNoReset _
222 145379a9 ploc
    -> Format.eprintf "unhandled noreset in EMF@.@?"; assert false
223 524060b3 ploc
  | MBranch _ (* branching instructions already handled *)
224
    -> Format.eprintf "unhandled branch statement in EMF (should have been filtered out before)@.@?";
225
      assert false
226 145379a9 ploc
  | MStep _ (* function calls already handled, including STEP *)
227
    -> Format.eprintf "unhandled function call in EMF (should have been filtered out before)@.@?";
228
      assert false
229
  | MComment _ 
230
    -> Format.eprintf "unhandled comment in EMF@.@?"; assert false
231
      (* not  available for EMF output *)
232
233 f7caf067 ploc
234 3ca27bc7 ploc
235 524060b3 ploc
let rec get_instr_lhs_var i =
236 3ca27bc7 ploc
  match Corelang.get_instr_desc i with
237 f7caf067 ploc
  | MLocalAssign (var,_) 
238
  | MStateAssign (var,_) 
239 524060b3 ploc
  | MStep ([var], _, _)  ->
240
     (* The only MStep instructions that filtered here
241
	should be arrows, ie. single var *)
242
     var
243
  | MBranch (_,(_,case1)::_)     ->
244
     get_instrs_var case1 (* assuming all cases define the same variables *)
245
  | MStep (f,name,a) -> Format.eprintf "step %s@.@?" name; assert false (* no other MStep here *)
246
  | MBranch _ -> assert false (* branch instruction should admit at least one case *)
247 f7caf067 ploc
  | MReset _           
248
  | MNoReset _
249
  | MComment _ -> assert false (* not  available for EMF output *)
250
and get_instrs_var il =
251
  match il with
252 524060b3 ploc
  | i::_ -> get_instr_lhs_var i (* looking for the first instr *)
253 f7caf067 ploc
  | _ -> assert false
254
255 3ca27bc7 ploc
  
256 f7caf067 ploc
let rec  get_val_vars v =
257
  match v.value_desc with
258
  | Cst c -> Utils.ISet.empty
259
  | LocalVar v
260
  | StateVar v -> Utils.ISet.singleton v.var_id
261
  | Fun (n, vl) -> List.fold_left (fun res v -> Utils.ISet.union (get_val_vars v) res) Utils.ISet.empty vl
262
  | _ -> assert false (* not available in EMF backend *)
263 3ca27bc7 ploc
264 524060b3 ploc
let rec get_instr_rhs_vars i =
265 3ca27bc7 ploc
  match Corelang.get_instr_desc i with
266 f7caf067 ploc
  | MLocalAssign (_,v)  
267
  | MStateAssign (_,v) -> get_val_vars v
268 145379a9 ploc
  | MStep (_, _, vl)  -> List.fold_left (fun res v -> Utils.ISet.union res (get_val_vars v)) Utils.ISet.empty vl 
269
  | MBranch (c,[(_,[case1]);(_,[case2])])     ->
270 f7caf067 ploc
     Utils.ISet.union
271
       (get_val_vars c)
272
       (
273
	 Utils.ISet.union
274 524060b3 ploc
	   (get_instr_rhs_vars case1)
275
	   (get_instr_rhs_vars case2)
276 f7caf067 ploc
       )
277 524060b3 ploc
  | MBranch (g, branches) ->
278
     List.fold_left
279
       (fun accu (_, il) -> Utils.ISet.union accu (get_instrs_vars il))
280
       (get_val_vars g)
281
       branches
282
  | MReset id           
283
  | MNoReset id -> Utils.ISet.singleton id
284
  | MComment _ -> Utils.ISet.empty
285
and get_instrs_vars il =
286
  List.fold_left (fun res i -> Utils.ISet.union res (get_instr_rhs_vars i))
287
    Utils.ISet.empty
288
    il
289 1bff14ac ploc
290
291 524060b3 ploc
     
292
let rec pp_emf_instr m fmt i =
293 145379a9 ploc
  (* Either it is a Step function non arrow, then we have a dedicated treatment,
294
     or it has to be a single variable assigment *)
295 524060b3 ploc
  let arguments_vars = Utils.ISet.elements (get_instr_rhs_vars i) in	
296 145379a9 ploc
  
297
  match Corelang.get_instr_desc i with
298 524060b3 ploc
  (* Regular node call either a statuful node or a functional one *)
299
  | MStep (outputs, f, inputs) when not (is_arrow_fun m i) -> (
300
    fprintf fmt "\"CALL\": @[<v 2>{ \"node\": \"%s\",@ \"inputs\": [%a],@ \"vars\": [%a]@ \"lhs\": [%a],@ \"original_lustre_expr\": [%a]@]}"
301
      ((Machine_code.get_node_def f m).node_id) (* Node name *)
302
      (Utils.fprintf_list ~sep:", " (fun fmt _val -> fprintf fmt "\"%a\"" (pp_matlab_val arguments_vars) _val)) inputs                  (* inputs *)
303
      (fprintf_list ~sep:", " pp_var_string) arguments_vars
304
      (fprintf_list ~sep:", " (fun fmt v -> pp_var_string fmt v.var_id)) outputs  (* outputs *)
305
      (pp_original_lustre_expression m) i         (* original lustre expr *)
306
  )
307
  | MStep _ -> (* Arrow case *) (
308
    let var = get_instr_lhs_var i in
309
    fprintf fmt "\"STEP\": @[<v 2>{ \"lhs\": \"%s\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%a]@]}"
310 145379a9 ploc
      var.var_id
311
      (fprintf_list ~sep:", " pp_var_string) arguments_vars
312
      (pp_original_lustre_expression m) i
313
  )
314 524060b3 ploc
  | MBranch (g,[(tag1,[case1]);(tag2,[case2])]) when tag1 = Corelang.tag_true || tag2 = Corelang.tag_true  ->
315
     (* Thanks to normalization with join_guards = false, branches shall contain
316
	a single expression *)
317
     let var = get_instr_lhs_var i in
318
     let then_case, else_case =
319
       if tag1 = Corelang.tag_true then
320
	 case1, case2
321
       else
322
	 case2, case1
323
     in
324
     fprintf fmt "\"ITE\": @[<v 2>{ \"lhs\": \"%s\",@ \"guard\": \"%a\",@ \"then_expr\": \"%a\",@ \"else_expr\": \"%a\",@ \"vars\": [%a],@ \"original_lustre_expr\": [%a]@]}"
325
       var.var_id
326
       (pp_matlab_val arguments_vars) g
327
       (pp_matlab_basic_instr m arguments_vars) then_case
328
       (pp_matlab_basic_instr m arguments_vars) else_case
329
       (fprintf_list ~sep:", " pp_var_string) arguments_vars
330
       (pp_original_lustre_expression m) i
331
332
  | MBranch (g, [single_tag, single_branch]) ->
333
     (* First case: it corresponds to a clocked expression: a MBranch with a
334
	single case. It shall become a subsystem with an enable port that depends on g = single_tag *)
335
     (* Thanks to normalization with join_guards = false, branches shall contain
336
	a single expression TODO REMOVE COMMENT THIS IS NOT TRUE *)
337
     let var = get_instr_lhs_var i in
338
     fprintf fmt "\"ENABLEDSUB\": @[<v 2>{ \"lhs\": \"%s\",@ \"enable_cond\": \"%a = %s\",@ \"subsystem\": {%a },@ \"vars\": [%a],@ \"original_lustre_expr\": [%a]@]}"
339
       var.var_id
340
       (pp_matlab_val arguments_vars) g
341
       single_tag
342
       (fprintf_list ~sep:",@ " (pp_emf_instr m)) single_branch
343
       (fprintf_list ~sep:", " pp_var_string) arguments_vars
344
       (pp_original_lustre_expression m) i
345
       
346
  | MBranch (g, hl) ->
347
     (* Thanks to normalization with join_guards = false, branches shall contain
348
	a single expression *)
349
     fprintf fmt "\"BRANCH\": @[<v 2>{ \"guard\": \"%a\",@ \"branches\": [@[<v 0>%a@]],@ \"vars\": [%a],@ \"original_lustre_expr\": [%a]@]}"
350
       (pp_matlab_val arguments_vars) g
351
       (fprintf_list ~sep:",@ "
352
	  (fun fmt (tag, (is_tag: instr_t list)) ->
353
	    fprintf fmt "\"%s\": [%a]"
354
	      tag
355
	      (fprintf_list ~sep:",@ " (fun fmt i_tag -> match Corelang.get_instr_desc i_tag with
356
		  | MLocalAssign (var,v) 
357
		  | MStateAssign (var,v) ->
358
		     fprintf fmt "{lhs= \"%s\", rhs= \"%a\"]" var.var_id (pp_matlab_val arguments_vars) v
359
		  | _ -> Format.eprintf "unhandled instr: %a@." Machine_code.pp_instr i_tag; assert false
360
	      )) is_tag
361
	  )) hl 
362
       (fprintf_list ~sep:", " pp_var_string) arguments_vars
363
       (pp_original_lustre_expression m) i
364
       
365
       
366
       
367
  | _ ->
368
     (* Other expressions, including "pre" *)
369
     ( 
370
       (* first, we extract the expression and associated variables *)
371
       let var = get_instr_lhs_var i in
372
       fprintf fmt "\"EXPR\": @[<v 2>{ \"lhs\": \"%s\",@ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%a]@]}"
373
	 var.var_id
374
	 (fun fmt i -> match Corelang.get_instr_desc i with
375
	 | MStep _ -> fprintf fmt "STEP"
376
	 | _ -> pp_matlab_basic_instr m arguments_vars fmt i) i
377
	 (fprintf_list ~sep:", " pp_var_string) arguments_vars
378
	 (pp_original_lustre_expression m) i
379
     )
380 1bff14ac ploc
    
381 524060b3 ploc
(* A (normalized) node becomes a JSON struct
382
   node foo (in1, in2: int) returns (out1, out2: int);
383
   var x : int;
384
   let
385
     x = bar(in1, in2); -- a stateful node
386
     out1 = x;
387
     out2 = in2;
388
   tel
389
390
   Since foo contains a stateful node, it is stateful itself. Its prototype is 
391
   extended with a reset input. When the node is reset, each of its "pre" expression
392
   is reset as well as all calls to stateful node it contains. 
393
394
   will produce the following JSON struct:
395
   "foo": {inputs:  [{name: "in1", type: "int"}, 
396
                     {name: "in2", type: "int"}, 
397
                     {name: "__reset", type: "reset"}
398
                    ],
399
           outputs: [{name: "out1", type: "int"}, {name: "out2", type: "int"}],
400
           locals:  [{name: "x", type: "int"}],
401
           instrs:  [
402
                    { def_x: { lhs: ["x"], 
403
                               rhs: {type: "statefulcall", name: "bar", 
404
                                     args: [in1, in2], reset: [ni4_reset] } 
405
                             }
406
                    }
407
                    { def_out1: { lhs: "out1", rhs: "x" } },
408
                    { def_out2: { lhs: "out2", rhs: "in2" }}
409
                    ]
410
           }
411
412
Basically we have three different definitions
413
1. classical assign of a variable to another one:
414
   { def_out1: { lhs: "out1", rhs: "x" } },
415
2. call to a stateless function, typically an operator
416
   { def_x: { lhs: ["x"], 
417
     rhs: {type: "statelesscall", name: "bar", args: [in1, in2]} 
418
   }
419
  or in the operator version 
420
   { def_x: { lhs: ["x"], 
421
     rhs: {type: "operator", name: "+", args: [in1, in2]} 
422
   }
423
424
  In Simulink this should introduce a subsystem in the first case or a 
425
  regular block in the second with card(lhs) outputs and card{args} inputs.
426
427
3. call to a stateful node. It is similar to the stateless above, 
428
   with the addition of the reset argument
429
    { def_x: { lhs: ["x"], 
430
               rhs: {type: "statefulcall", name: "bar", 
431
                     args: [in1, in2], reset: [ni4_reset] } 
432
             }
433
    }
434
  
435
  In lustrec compilation phases, a unique id is associated to this specific
436
  instance of stateful node "bar", here ni4. 
437
  Instruction such as reset(ni4) or noreset(ni4) may -- or not -- reset this 
438
  specific node. This corresponds to "every c" suffix of a node call in lustre.
439
440
  In Simulink this should introduce a subsystem that has this extra reset input.  
441
  The reset should be defined as an "OR" over (1) the input reset of the parent 
442
  node, __reset in the present example and (2) any occurence of reset(ni4) in 
443
  the instructions.
444
445
4. branching construct: (guard expr, (tag, instr list) list)
446
   { "merge_XX": { type: "branch", guard: "var_guard", 
447
                   inputs:   ["varx", "vary"],
448
                   outputs:  ["vark", "varz"],
449
                   branches: ["tag1": [liste_of_definitions (1-4)], ...] 
450
                 }
451
   }
452
453
  In Simulink, this should become one IF block to produce enable ports "var_guard == tag1", "var_guard == tag2", .... as well as one action block per branch: each of these action block shall  
454
*)     
455 f7caf067 ploc
let pp_machine fmt m =
456
  try
457
    fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ "
458
      m.mname.node_id
459
      pp_node_args m.mstep.step_inputs
460
      pp_node_args m.mstep.step_outputs;
461
    fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }"
462 524060b3 ploc
      (fprintf_list ~sep:",@ " (pp_emf_instr m)) m.mstep.step_instrs;
463 f7caf067 ploc
    fprintf fmt "@]@ }"
464
  with Unhandled msg -> (
465
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
466
      m.mname.node_id;
467
    eprintf "%s@ " msg;
468
    eprintf "node skipped - no output generated@ @]@."
469
  )
470 3ca27bc7 ploc
471
(****************************************************)
472
(* Main function: iterates over node and print them *)
473
(****************************************************)
474
let pp_meta fmt basename =
475
  fprintf fmt "\"meta\": @[<v 0>{@ ";
476
  Utils.fprintf_list ~sep:",@ "
477
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
478
    fmt
479
    ["compiler-name", (Filename.basename Sys.executable_name);
480
     "compiler-version", Version.number;
481
     "command", (String.concat " " (Array.to_list Sys.argv));
482
     "source_file", basename
483
    ]
484
  ;
485
  fprintf fmt "@ @]},@ "
486 f7caf067 ploc
    
487 3ca27bc7 ploc
let translate fmt basename prog machines =
488 a6df3992 Ploc
  fprintf fmt "@[<v 0>{@ ";
489 3ca27bc7 ploc
  pp_meta fmt basename;
490
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
491 145379a9 ploc
  (* Previous alternative: mapping normalized lustre to EMF: 
492
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
493 f7caf067 ploc
  fprintf_list ~sep:",@ " pp_machine fmt machines;
494 3ca27bc7 ploc
  fprintf fmt "@ @]}";
495 a6df3992 Ploc
  fprintf fmt "@ @]}"
496 3ca27bc7 ploc
497
(* Local Variables: *)
498
(* compile-command: "make -C ../.." *)
499
(* End: *)