Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/backends/EMF/EMF_backend.ml
101 101
open Lustre_types
102 102
open Machine_code_types
103 103
open Machine_code_common
104
open Format 
104
open Format
105 105
open EMF_common
106

  
106 107
exception Unhandled of string
107 108

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

  
111
let fprintf_list = Utils.fprintf_list
112 112

  
113 113
(**********************************************)
114 114
(*   Utility functions: arrow and lustre expr *)
......
118 118
   -> false *)
119 119
let is_arrow_fun m i =
120 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
     )
121
  | MStep ([ _ ], i, vl) -> (
122
      try
123
        let name = (get_node_def i m).node_id in
124
        match name, vl with
125
        | "_arrow", [ v1; v2 ] -> (
126
            match v1.value_desc, v2.value_desc with
127
            | Cst c1, Cst c2 ->
128
                if
129
                  c1 = Corelang.const_of_bool true
130
                  && c2 = Corelang.const_of_bool false
131
                then true
132
                else assert false
133
            (* only handle true -> false *)
134
            | _ -> assert false)
135
        | _ -> false
136
      with Not_found ->
137
        false
138
        (* Not declared (should have been detected now, or
139
           imported node) *))
141 140
  | _ -> false
142
     
143
     
144
     
141

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

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

  
162
     
163

  
164 160
let branch_cpt = ref 0
161

  
165 162
let get_instr_id fmt i =
166 163
  match Corelang.get_instr_desc i with
167
  | MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
164
  | MLocalAssign (lhs, _) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
168 165
  | MSetReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
169 166
  (* TODO: handle clear_reset *)
170 167
  | MClearReset -> ()
171
  | MBranch _ -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
168
  | MBranch _ ->
169
      incr branch_cpt;
170
      fprintf fmt "branch_%i" !branch_cpt
172 171
  | 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 *)
172
      print_protect fmt (fun fmt ->
173
          fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
174
  | _ -> ()
175
(* No name *)
176 176

  
177 177
let rec branch_block_vars m il =
178 178
  List.fold_left
179 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
  
180
      let all_defined_vars, common_def_vars, read_vars =
181
        branch_instr_vars m i
182
      in
183
      ( ISet.union accu_all_def all_defined_vars,
184
        ISet.union accu_def common_def_vars,
185
        VSet.union accu_read read_vars ))
186
    (ISet.empty, ISet.empty, VSet.empty)
187
    il
188

  
186 189
and branch_instr_vars m i =
187 190
  (* Returns all_outputs, outputs, inputs of the instruction. It is
188 191
     only called on MBranch instructions but evaluate recursively
......
193 196

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

  
197 199
  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
200
  | MLocalAssign (var, expr) | MStateAssign (var, expr) ->
201
      ISet.singleton var.var_id, ISet.singleton var.var_id, get_expr_vars expr
202
  | MStep (vars, f, args) ->
203
      let is_stateful = List.mem_assoc f m.minstances in
204
      let lhs = ISet.of_list (List.map (fun v -> v.var_id) vars) in
205
      let args_vars =
206
        List.fold_left
207
          (fun accu v -> VSet.union accu (get_expr_vars v))
208
          VSet.empty args
209
      in
210

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

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

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

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

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

  
319
    | MBranch (g, hl) -> (
313
    | MBranch (g, hl) ->
320 314
        let all_outputs, outputs, inputs = branch_instr_vars m i in
315

  
321 316
        (* Format.eprintf "Mbranch %a@.vars: all_out: %a, out:%a, in:%a@.@." *)
322 317
        (* 	Machine_code.pp_instr i *)
323 318
        (* 	(fprintf_list ~sep:", " pp_var_string) (ISet.elements all_outputs) *)
......
326 321
        (* 	(VSet.elements inputs) *)
327 322

  
328 323
        (* ; *)
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 *)
324
        let inputs =
325
          VSet.filter (fun v -> not (ISet.mem v.var_id all_outputs)) inputs
326
        in
327

  
328
        (* Format.eprintf "Filtering in: %a@.@." *)
329
        (* 	pp_emf_vars_decl *)
330
        (* 	(VSet.elements inputs) *)
331

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

  
400
and pp_emf_instrs m fmt instrs =
401
  fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
396 402

  
397 403
let pp_emf_annot cpt fmt (key, ee) =
398 404
  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
405
    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }" !cpt
406
      (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s))
407
      key pp_emf_eexpr ee
403 408
  in
404 409
  incr cpt
405 410

  
406 411
let pp_emf_spec_mode fmt m =
407 412
  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;
413
  fprintf fmt "\"mode_id\": \"%s\",@ " m.mode_id;
414
  fprintf fmt "\"ensure\": [%a],@ " pp_emf_eexprs m.ensure;
415
  fprintf fmt "\"require\": [%a]@ " pp_emf_eexprs m.require;
414 416
  fprintf fmt "@]}"
415
  
417

  
416 418
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
417 419

  
418 420
let pp_emf_spec_import fmt i =
419 421
  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;
422
  fprintf fmt "\"contract\": \"%s\",@ " i.import_nodeid;
423
  fprintf fmt "\"inputs\": [%a],@ " pp_emf_expr i.inputs;
424
  fprintf fmt "\"outputs\": [%a],@ " pp_emf_expr i.outputs;
426 425
  fprintf fmt "@]}"
427
  
426

  
428 427
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
429 428

  
430 429
let pp_emf_spec fmt spec =
......
435 434
   *   pp_emf_vars_decl spec.locals;
436 435
   * fprintf fmt "\"stmts\": [%a],@ "
437 436
   *   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;
437
  fprintf fmt "\"assume\": [%a],@ " pp_emf_eexprs spec.assume;
438
  fprintf fmt "\"guarantees\": [%a],@ " pp_emf_eexprs spec.guarantees;
439
  fprintf fmt "\"modes\": [%a]@ " pp_emf_spec_modes spec.modes;
444 440
  (* fprintf fmt "\"imports\": [%a]@ "
445
   *   pp_emf_spec_imports spec.imports;   *)
441
   *   pp_emf_spec_imports spec.imports; *)
446 442
  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
443

  
444
let pp_emf_annots cpt fmt annots =
445
  fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
446

  
447
let pp_emf_annots_list cpt fmt annots_list =
448
  fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
450 449

  
451 450
(* let pp_emf_contract fmt nd =
452 451
 *   let c = Printers.node_as_contract nd in
......
455 454
 *   fprintf fmt "\"contract\": %a@ "
456 455
 *     pp_emf_spec c;
457 456
 *   fprintf fmt "@]@ }" *)
458
  
457

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

  
500 495
(*let pp_machine fmt m =                      
501 496
  match m.mspec with
502 497
  | None | Some (NodeSpec _) -> pp_machine fmt m
503 498
  | Some (Contract _) -> pp_emf_contract fmt m
504 499
 *)
505
                      
500

  
506 501
let pp_emf_imported_node fmt top =
507 502
  let ind = Corelang.imported_node_of_top top in
508 503
  try
509
    fprintf fmt "@[<v 2>\"%a\": {@ "
510
      print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);
504
    fprintf fmt "@[<v 2>\"%a\": {@ " print_protect (fun fmt ->
505
        pp_print_string fmt ind.nodei_id);
511 506
    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;
507
    fprintf fmt "\"inputs\": [%a],@ " pp_emf_vars_decl ind.nodei_inputs;
508
    fprintf fmt "\"outputs\": [%a],@ " pp_emf_vars_decl ind.nodei_outputs;
516 509
    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
    );
510
    (match ind.nodei_spec with
511
    | None -> fprintf fmt "@ "
512
    | Some (Contract _) -> assert false (* should have been processed *)
513
    | Some (NodeSpec id) -> fprintf fmt ",@ \"coco_contract\": %s" id);
521 514
    fprintf fmt "@]@ }"
522
  with Unhandled msg -> (
515
  with Unhandled msg ->
523 516
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
524 517
      ind.nodei_id;
525 518
    eprintf "%s@ " msg;
526 519
    eprintf "node skipped - no output generated@ @]@."
527
  )
520

  
528 521
(****************************************************)
529 522
(* Main function: iterates over node and print them *)
530 523
(****************************************************)
......
533 526
  Utils.fprintf_list ~sep:",@ "
534 527
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
535 528
    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
  ;
529
    [
530
      "compiler-name", Filename.basename Sys.executable_name;
531
      "compiler-version", Version.number;
532
      "command", String.concat " " (Array.to_list Sys.argv);
533
      "source_file", basename;
534
    ];
542 535
  fprintf fmt "@ @]},@ "
543
    
536

  
544 537
let translate fmt basename prog machines =
545 538
  (* record_types prog; *)
546 539
  fprintf fmt "@[<v 0>{@ ";
547 540
  pp_meta fmt basename;
548 541
  (* Typedef *)
549 542
  fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "
550
    (pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog);
543
    (pp_emf_list pp_emf_typedef)
544
    (Corelang.get_typedefs prog);
551 545
  fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "
552
    (pp_emf_list pp_emf_top_const) (Corelang.get_consts prog);
546
    (pp_emf_list pp_emf_top_const)
547
    (Corelang.get_consts prog);
553 548
  fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
554 549
  pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);
555 550
  fprintf fmt "}@],@ ";
556 551
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
557
  (* Previous alternative: mapping normalized lustre to EMF: 
552
  (* Previous alternative: mapping normalized lustre to EMF:
558 553
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
559 554
  pp_emf_list pp_machine fmt machines;
560 555
  fprintf fmt "}@]@ }";

Also available in: Unified diff