Project

General

Profile

Revision 59020713

View differences:

src/backends/EMF/EMF_backend.ml
375 375
      pp_emf_eexpr ee
376 376
  in
377 377
  incr cpt
378

  
379
let pp_emf_spec_mode fmt m =
380
  fprintf fmt "{@[";
381
  fprintf fmt "\"mode_id\": \"%s\",@ "
382
    m.mode_id;
383
  fprintf fmt "\"require\": [%a],@ "
384
    pp_emf_eexprs m.ensure;
385
  fprintf fmt "\"require\": [%a],@ "
386
    pp_emf_eexprs m.require;
387
  fprintf fmt "@]}"
388
  
389
let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode
390

  
391
let pp_emf_spec_import fmt i =
392
  fprintf fmt "{@[";
393
  fprintf fmt "\"contract\": \"%s\",@ "
394
    i.import_nodeid;
395
  fprintf fmt "\"inputs\": [%a],@ "
396
    pp_emf_exprs i.inputs;
397
  fprintf fmt "\"outputs\": [%a],@ "
398
    pp_emf_exprs i.outputs;
399
  fprintf fmt "@]}"
400
  
401
let pp_emf_spec_imports = pp_emf_list pp_emf_spec_import
402

  
403
let pp_emf_spec fmt spec =
404
  fprintf fmt "{ @[<hov 0>";
405
  fprintf fmt "\"consts\": [%a],@ "
406
    pp_emf_consts spec.consts;
407
  fprintf fmt "\"locals\": [%a],@ "
408
    pp_emf_vars_decl spec.locals;
409
  fprintf fmt "\"stmts\": [%a],@ "
410
    pp_emf_stmts spec.stmts;
411
  fprintf fmt "\"assume\": [%a],@ "
412
    pp_emf_eexprs spec.assume;
413
  fprintf fmt "\"guarantees\": [%a],@ "
414
    pp_emf_eexprs spec.guarantees;
415
  fprintf fmt "\"modes\": [%a],@ "
416
    pp_emf_spec_modes spec.modes;
417
  fprintf fmt "\"imports\": [%a]@ "
418
    pp_emf_spec_imports spec.imports;  
419
  fprintf fmt "@] }"
378 420
  
379 421
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
380 422
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
423

  
424
  
425
                                           
381 426
let pp_machine fmt m =
382 427
  let instrs = (*merge_branches*) m.mstep.step_instrs in
383 428
  try
384 429
    fprintf fmt "@[<v 2>\"%a\": {@ "
385
       print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
430
      print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
431
    fprintf fmt "\"imported\": \"false\",@ ";
386 432
    fprintf fmt "\"kind\": %t,@ "
387 433
      (fun fmt -> if not ( snd (get_stateless_status m) )
388 434
	then fprintf fmt "\"stateful\""
......
399 445
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
400 446
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
401 447
      (pp_emf_instrs m) instrs;
448
    (match m.mspec with None -> () | Some spec -> fprintf fmt "\"spec\": %a,@ " pp_emf_spec spec);
402 449
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
403 450
    fprintf fmt "@]@ }"
404 451
  with Unhandled msg -> (
......
408 455
    eprintf "node skipped - no output generated@ @]@."
409 456
  )
410 457

  
458
let pp_emf_imported_node fmt top =
459
  let ind = Corelang.imported_node_of_top top in
460
   try
461
    fprintf fmt "@[<v 2>\"%a\": {@ "
462
      print_protect (fun fmt -> pp_print_string fmt ind.nodei_id);
463
    fprintf fmt "\"imported\": \"true\",@ ";
464
    fprintf fmt "\"inputs\": [%a],@ "
465
      pp_emf_vars_decl ind.nodei_inputs;
466
    fprintf fmt "\"outputs\": [%a],@ "
467
      pp_emf_vars_decl ind.nodei_outputs;
468
    fprintf fmt "\"original_name\": \"%s\",@ " ind.nodei_id;
469
    (match ind.nodei_spec with None -> () | Some spec -> fprintf fmt "\"spec\": %a" pp_emf_spec spec);
470
    fprintf fmt "@]@ }"
471
  with Unhandled msg -> (
472
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
473
      ind.nodei_id;
474
    eprintf "%s@ " msg;
475
    eprintf "node skipped - no output generated@ @]@."
476
  )
411 477
(****************************************************)
412 478
(* Main function: iterates over node and print them *)
413 479
(****************************************************)
......
425 491
  fprintf fmt "@ @]},@ "
426 492
    
427 493
let translate fmt basename prog machines =
428
   (* record_types prog; *)
494
  (* record_types prog; *)
429 495
  fprintf fmt "@[<v 0>{@ ";
430 496
  pp_meta fmt basename;
497
  (* Typedef *)
498
  fprintf fmt "\"typedef\": [@[<v 0>%a@]],@ "
499
    (pp_emf_list pp_emf_typedef) (Corelang.get_typedefs prog);
500
  fprintf fmt "\"consts\": [@[<v 0>%a@]],@ "
501
    (pp_emf_list pp_emf_top_const) (Corelang.get_consts prog);
502
  fprintf fmt "\"imported_nodes\": @[<v 0>{@ ";
503
  pp_emf_list pp_emf_imported_node fmt (Corelang.get_imported_nodes prog);
504
  fprintf fmt "}@],@ ";
431 505
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
432 506
  (* Previous alternative: mapping normalized lustre to EMF: 
433 507
     fprintf_list ~sep:",@ " pp_decl fmt prog; *)
434
  fprintf_list ~sep:",@ " pp_machine fmt (List.rev machines);
508
  pp_emf_list pp_machine fmt (List.rev machines);
435 509
  fprintf fmt "}@]@ }";
436 510
  fprintf fmt "@]@ }"
437 511

  
src/backends/EMF/EMF_common.ml
76 76
*)
77 77
  
78 78
  
79
let pp_tag_type fmt typ =
80
  let rec aux tydec_desc =
81
  match tydec_desc with  
82
  | Tydec_int -> fprintf fmt "int"
83
  | Tydec_real -> fprintf fmt "real"
84
  | Tydec_bool -> fprintf fmt "bool"
85
  | Tydec_clock ty -> aux ty
86
  | Tydec_enum const_list -> (
87
    let size = List.length const_list in
88
    if size < 255 then
89
      fprintf fmt "uint8"
90
    else if size < 65535 then
91
      fprintf fmt "uint16"
92
    else
93
      assert false (* Too much states. This not reasonable *)
94
  )
95
  | Tydec_const _ | Tydec_struct _ | Tydec_array _ | Tydec_any -> eprintf "unhandled cst tag in EMF: %a@." Printers.pp_var_type_dec_desc tydec_desc; assert false
96
  in
97
  aux typ.tydef_desc
98 79

  
99
     
100
let pp_cst_type fmt c (*infered_typ*) =
101
  match c with
102
  | Const_tag t ->
103
     let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
104
     if typ.tydef_id = "bool" then
105
       fprintf fmt "bool"
106
     else
107
       pp_tag_type fmt typ
108
  | Const_int _ -> fprintf fmt "int" (*!Options.int_type*)
109
  | Const_real _ -> fprintf fmt "real" (*!Options.real_type*)
110
  | Const_string _ -> fprintf fmt "string" 
111
  | _ -> eprintf "cst: %a@." Printers.pp_const c; assert false
80
let rec pp_emf_dim fmt dim_expr =
81
  fprintf fmt "{";
82
  (let open Dimension in
83
   match dim_expr.dim_desc with
84
   | Dbool b -> fprintf fmt "\"kind\": \"bool\",@ \"value\": \"%b\"" b
85
   | Dint i -> fprintf fmt "\"kind\": \"int\",@ \"value\": \"%i\"" i
86
   | Dident s -> fprintf fmt "\"kind\": \"ident\",@ \"value\": \"%s\"" s
87
   | Dappl(f, args) -> fprintf fmt "\"kind\": \"fun\",@ \"id\": \"%s\",@ \"args\": [@[%a@]]"
88
                         f (Utils.fprintf_list ~sep:",@ " pp_emf_dim) args 
89
   | Dite(i,t,e) -> fprintf fmt "\"kind\": \"ite\",@ \"guard\": \"%a\",@ \"then\": %a,@ \"else\": %a"
90
                      pp_emf_dim i pp_emf_dim t pp_emf_dim e 
91
   | Dlink e -> pp_emf_dim fmt e
92
   | Dvar
93
   | Dunivar -> assert false (* unresolved *)
94
  );
95
  fprintf fmt "}"
112 96

  
113
let rec pp_infered_type fmt t =
114
  let open Types in
115
  if is_bool_type t  then fprintf fmt "bool" else
116
  if is_int_type t then fprintf fmt "int" else (* !Options.int_type *)
117
  if is_real_type t then fprintf fmt "real" else (* !Options.real_type *)
118
  match t.tdesc with
119
  | Tclock t ->
120
     pp_infered_type fmt t
121
  | Tstatic (_, t) ->
122
     fprintf fmt "%a" pp_infered_type t
123
  | Tconst id ->
124
    (* This is a type id for a enumerated type, eg. introduced by automata *)
125
     let typ =
126
       (Corelang.typedef_of_top (Hashtbl.find Corelang.type_table (Tydec_const id)))
127
     in
128
     pp_tag_type fmt typ
129
   | Tlink ty -> 
130
       pp_infered_type fmt ty 
131
   | _ -> eprintf "unhandled type: %a@." Types.print_node_ty t; assert false
132 97
     
98

  
99

  
100
(* First try to print the declared one *)
133 101
let rec pp_concrete_type dec_t infered_t fmt =
134 102
  match dec_t with
135
  | Tydec_int -> fprintf fmt "int" (* !Options.int_type *)
136
  | Tydec_real -> fprintf fmt "real" (* !Options.real_type *)
103
  | Tydec_any -> (* Dynamical built variable. No declared type. Shall
104
                    use the infered one. *)
105
     pp_infered_type fmt infered_t
106
  | Tydec_int -> fprintf fmt "{ \"kind\": \"int\" }" (* !Options.int_type *)
107
  | Tydec_real -> fprintf fmt "{ \"kind\": \"real\" }" (* !Options.real_type *)
137 108
  (* TODO we could add more concrete types here if they were available in
138 109
     dec_t *)
139
  | Tydec_bool -> fprintf fmt "bool"
110
  | Tydec_bool -> fprintf fmt "{ \"kind\": \"bool\" }"
140 111
  | Tydec_clock t -> pp_concrete_type t infered_t fmt
141 112
  | Tydec_const id -> (
142
    (* This is a type id for a enumerated type, eg. introduced by automata *)
113
    (* This is an alias type *)
114

  
115
    (* id for a enumerated type, eg. introduced by automata *)
143 116
    let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.type_table dec_t)) in
144
    pp_tag_type fmt typ
117
    (* Print the type name associated to this enumerated type. This is
118
       basically an integer *)
119
    pp_tag_type id typ infered_t fmt
120
  )
121
                    
122
  | Tydec_struct _ | Tydec_enum _ ->
123
     assert false (* should not happen. These type are only built when
124
                     declaring a type in the prefix of the lustre
125
                     file. They shall not be associated to variables
126
                   *)
127
    
128
  | Tydec_array (dim, e) -> (
129
    let inf_base = match infered_t.Typing.tdesc with
130
      | Typing.Tarray(_,t) -> t
131
      | _ ->   (* returing something useless, hoping that the concrete
132
                  datatype will return something usefull *)
133
         Typing.new_var ()
134
    in
135
    fprintf fmt "{ \"kind\": \"array\", \"base_type\": %t, \"dim\": %a }"
136
      (pp_concrete_type e inf_base)
137
      pp_emf_dim dim
145 138
  )
146
  | Tydec_any -> pp_infered_type fmt infered_t 
147
  | _ -> eprintf
148
     "unhandled construct in type printing for EMF backend: %a@."
149
     Printers.pp_var_type_dec_desc dec_t; raise (Failure "var")
139
                          
140
(* | _ -> eprintf
141
 *          "unhandled construct in type printing for EMF backend: %a@."
142
 *          Printers.pp_var_type_dec_desc dec_t; raise (Failure "var") *)
143
and pp_tag_type id typ inf fmt =
144
  (* We ought to represent these types as values: enum will become int, we keep the name for structs *)
145
  let rec aux tydec_desc =
146
    match tydec_desc with  
147
    | Tydec_int 
148
      | Tydec_real 
149
      | Tydec_bool
150
      | Tydec_array _ -> pp_concrete_type tydec_desc inf fmt
151
    | Tydec_const id ->
152
       (* Alias of an alias: unrolling definitions *)
153
       let typ = (Corelang.typedef_of_top
154
                    (Hashtbl.find Corelang.type_table tydec_desc))
155
       in
156
       pp_tag_type id typ inf fmt
150 157
       
158
    | Tydec_clock ty -> aux ty
159
    | Tydec_enum const_list -> ( (* enum can be mapped to int *)
160
      let size = List.length const_list in
161
      fprintf fmt "{ \"name\": \"%s\", \"kind\": \"enum\", \"size\": \"%i\" }" id size
162
    )
163
    | Tydec_struct _ ->
164
       fprintf fmt "{ \"name\": \"%s\", \"kind\": \"struct\" }" id
165
    | Tydec_any -> (* shall not happen: a declared type cannot be
166
                      bound to type any *)
167
       assert false
168
  in
169
  aux typ.tydef_desc
170
and pp_infered_type fmt t =
171
  (* Shall only be used for variable types that were not properly declared. Ie generated at compile time. *)
172
  let open Types in
173
  if is_bool_type t  then fprintf fmt "bool" else
174
    if is_int_type t then fprintf fmt "int" else (* !Options.int_type *)
175
      if is_real_type t then fprintf fmt "real" else (* !Options.real_type *)
176
        match t.tdesc with
177
        | Tclock t ->
178
           pp_infered_type fmt t
179
        | Tstatic (_, t) ->
180
           fprintf fmt "%a" pp_infered_type t
181
        | Tconst id ->
182
           (* This is a type id for a enumerated type, eg. introduced by automata *)
183
           let typ =
184
             (Corelang.typedef_of_top
185
                (Hashtbl.find Corelang.type_table (Tydec_const id)))
186
           in
187
           pp_tag_type id typ t fmt
188
        | Tlink ty -> 
189
           pp_infered_type fmt ty 
190
        | _ -> eprintf "unhandled type: %a@." Types.print_node_ty t; assert false
151 191

  
152 192
(*let pp_cst_type fmt v =
153 193
  match v.value_desc with
154 194
  | Cst c-> pp_cst_type c v.value_type fmt (* constants do not have declared type (yet) *)
155 195
  | _ -> assert false
156 196
*)
157
       
197

  
198
(* Provide both the declared type and the infered one. *)
158 199
let pp_var_type fmt v =
159 200
  try
160 201
    if Machine_types.is_specified v then
161 202
      Machine_types.pp_var_type fmt v
162 203
    else
163 204
      pp_concrete_type v.var_dec_type.ty_dec_desc v.var_type fmt
164
  with Failure _ -> eprintf "failed var: %a@." Printers.pp_var v; assert false
205
  with Failure msg -> eprintf "failed var: %a@.%s@." Printers.pp_var v msg; assert false
165 206
    
166 207
(******** Other print functions *)
167
    
208

  
209
let pp_emf_list ?(eol:('a, formatter, unit) Pervasives.format="") pp fmt l =
210
  match l with
211
    [] -> ()
212
  | _ -> fprintf fmt "@[";
213
         Utils.fprintf_list ~sep:",@ " pp fmt l;
214
         fprintf fmt "@]%(%)" eol
215
  
216
(* Print the variable declaration *)
168 217
let pp_emf_var_decl fmt v =
169 218
  fprintf fmt "@[{\"name\": \"%a\", \"datatype\":\"%a\", \"original_name\": \"%a\"}@]"
170 219
    pp_var_name v
171 220
    pp_var_type v
172 221
    Printers.pp_var_name v
173
    
174
let pp_emf_vars_decl fmt vl =
175
  fprintf fmt "@[";
176
  Utils.fprintf_list ~sep:",@ " pp_emf_var_decl fmt vl;
177
  fprintf fmt "@]"
222

  
223
let pp_emf_vars_decl = pp_emf_list pp_emf_var_decl
224

  
225
 
178 226
  
179 227
let reset_name id =
180 228
  "reset_" ^ id
......
187 235
    let const_list = match typ.tydef_desc with Tydec_enum tl -> tl | _ -> assert false in
188 236
    fprintf fmt "%i" (get_idx t const_list)
189 237

  
190
let pp_emf_cst fmt c =
238
let pp_cst_type c inf fmt (*infered_typ*) =
239
  match c with
240
  | Const_tag t ->
241
     let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
242
     if typ.tydef_id = "bool" then
243
       fprintf fmt "bool"
244
     else
245
       pp_tag_type t typ inf fmt
246
  | Const_int _ -> fprintf fmt "int" (*!Options.int_type*)
247
  | Const_real _ -> fprintf fmt "real" (*!Options.real_type*)
248
  | Const_string _ -> fprintf fmt "string" 
249
  | _ -> eprintf "cst: %a@." Printers.pp_const c; assert false
250

  
251
    
252
let pp_emf_cst c inf fmt =
253
  let pp_typ fmt =
254
    fprintf fmt "\"datatype\": \"";
255
    pp_cst_type c inf fmt;
256
    fprintf fmt "\"@ "
257
  in
191 258
  match c with
192 259
  | Const_tag t->
193 260
     let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
......
195 262
       fprintf fmt "{@[\"type\": \"constant\",@ ";
196 263
       fprintf fmt"\"value\": \"%a\",@ "
197 264
	 Printers.pp_const c;
198
       fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
265
       pp_typ fmt;
199 266
       fprintf fmt "@]}"
200 267
     )
201 268
     else (
......
203 270
	 pp_tag_id t;
204 271
       fprintf fmt "\"origin_type\": \"%s\",@ \"origin_value\": \"%s\",@ "
205 272
	 typ.tydef_id t;
206
       fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
273
       pp_typ fmt;
207 274
       fprintf fmt "@]}"
208 275
     )
209 276
  | Const_string s ->
210
    fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%s\",@ " s;
211
    fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
212
    fprintf fmt "@]}"
277
     fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%s\",@ " s;
278
     pp_typ fmt;
279
     fprintf fmt "@]}"
213 280
     
214 281
  | _ -> (
215 282
    fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%a\",@ "
216 283
      Printers.pp_const c;
217
    fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
284
    pp_typ fmt;
218 285
    fprintf fmt "@]}"
219 286
  )
220 287
  
221
  
288
(* Print a value: either a constant or a variable value *)
222 289
let pp_emf_cst_or_var m fmt v =
223 290
  match v.value_desc with
224
  | Cst c -> pp_emf_cst fmt c
291
  | Cst c -> pp_emf_cst c v.value_type fmt 
225 292
  | Var v -> (
226 293
    fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
227 294
      pp_var_name v;
......
239 306
    
240 307
let rec pp_emf_expr fmt e =
241 308
  match e.expr_desc with
242
  | Expr_const c -> pp_emf_cst fmt c
309
  | Expr_const c -> pp_emf_cst c e.expr_type fmt 
243 310
  | Expr_ident id ->
244 311
     fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
245 312
       print_protect (fun fmt -> pp_print_string fmt id);
......
254 321
  | Expr_tuple el ->
255 322
     fprintf fmt "[@[<hov 0>%a@ @]]"
256 323
       (Utils.fprintf_list ~sep:",@ " pp_emf_expr) el
324
 (* Missing these 
325
  | Expr_ite   of expr * expr * expr
326
  | Expr_arrow of expr * expr
327
  | Expr_fby of expr * expr
328
  | Expr_array of expr list
329
  | Expr_access of expr * Dimension.dim_expr
330
  | Expr_power of expr * Dimension.dim_expr
331
  | Expr_pre of expr
332
  | Expr_when of expr * ident * label
333
  | Expr_merge of ident * (label * expr) list
334
  | Expr_appl of call_t
335
  *)
257 336
  | _ -> (
258 337
    Log.report ~level:2
259 338
      (fun fmt ->
......
274 353
(* | Expr_when of expr * ident * label *)
275 354
(* | Expr_merge of ident * (label * expr) list *)
276 355
(* | Expr_appl of call_t *)
277
     
278 356

  
357
let pp_emf_exprs = pp_emf_list pp_emf_expr
358
       
359
let pp_emf_const fmt v =
360
  fprintf fmt "@[{\"name\": \"%a\", \"datatype\":\"%a\", \"original_name\": \"%a\", \"value\": \"%a\"}@]"
361
    pp_var_name v
362
    pp_var_type v
363
    Printers.pp_var_name v
364
    pp_emf_expr (match v.var_dec_value with None -> assert false | Some e -> e)
365

  
366
let pp_emf_consts = pp_emf_list pp_emf_const
367
                  
279 368
let pp_emf_eexpr fmt ee =
280 369
  fprintf fmt "{@[<hov 0>\"quantifiers\": \"%a\",@ \"qfexpr\": @[%a@]@] }"
281 370
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) ee.eexpr_quantifiers
282 371
    pp_emf_expr ee.eexpr_qfexpr
283
    
284
    
372

  
373
let pp_emf_eexprs = pp_emf_list pp_emf_eexpr
374

  
375
(*
376
                      TODO Thanksgiving
377

  
378
                      trouver un moyen de transformer en machine code les instructions de chaque spec
379
                      peut etre associer a chaque imported node une minimachine
380
                      et rajouter un champ a spec dans machine code pour stoquer memoire et instr
381
 *)                
382
                 
383
let pp_emf_stmt fmt stmt =
384
  match stmt with
385
  | Aut _ -> assert false
386
  | Eq eq -> (
387
    fprintf fmt "@[ @[<v 2>\"%a\": {@ " (Utils.fprintf_list ~sep:"_" pp_print_string) eq.eq_lhs;
388
    fprintf fmt "\"lhs\": [%a],@ " (Utils.fprintf_list ~sep:", " (fun fmt vid -> fprintf fmt "\"%s\"" vid)) eq.eq_lhs;
389
    fprintf fmt "\"rhs\": \"%a\",@ " pp_emf_expr eq.eq_rhs;
390
    fprintf fmt "@]@]@ }"
391
  )
392

  
393
let pp_emf_stmts = pp_emf_list pp_emf_stmt 
394
  
395
(* Printing the type declaration, not its use *)
396
let rec pp_emf_typ_dec fmt tydef_dec =
397
  fprintf fmt "{";
398
  (match tydef_dec with
399
   | Tydec_any -> fprintf fmt "\"kind\": \"any\""
400
   | Tydec_int -> fprintf fmt "\"kind\": \"int\""
401
   | Tydec_real -> fprintf fmt "\"kind\": \"real\""
402
   | Tydec_bool-> fprintf fmt "\"kind\": \"bool\""
403
   | Tydec_clock ck -> pp_emf_typ_dec fmt ck
404
   | Tydec_const c -> fprintf fmt "\"kind\": \"alias\",@ \"value\": \"%s\"" c
405
   | Tydec_enum el -> fprintf fmt "\"kind\": \"enum\",@ \"elements\": [%a]"
406
                        (Utils.fprintf_list ~sep:", " (fun fmt e -> fprintf fmt "\"%s\"" e)) el
407
   | Tydec_struct s -> fprintf fmt "\"kind\": \"struct\",@ \"fields\": [%a]"
408
                         (Utils.fprintf_list ~sep:", " (fun fmt (id,typ) ->
409
                              fprintf fmt "\"%s\": %a" id pp_emf_typ_dec typ)) s
410
   | Tydec_array (dim, typ) -> fprintf fmt "\"kind\": \"array\",@ \"dim\": @[%a@],@ \"base\": %a"
411
                               pp_emf_dim dim
412
                               pp_emf_typ_dec typ
413
  );
414
  fprintf fmt "}"
415
 
416
let pp_emf_typedef fmt typdef_top =
417
  let typedef = Corelang.typedef_of_top typdef_top in
418
  fprintf fmt "\"%s\": @[%a@]" typedef.tydef_id pp_emf_typ_dec typedef.tydef_desc 
419
  
420
let pp_emf_top_const fmt const_top = 
421
  let const = Corelang.const_of_top const_top in
422
  fprintf fmt "\"%s\": " const.const_id;
423
  pp_emf_cst const.const_value const.const_type fmt
424

  
285 425
(* Local Variables: *)
286 426
(* compile-command: "make -C ../.." *)
287 427
(* End: *)
src/compiler_stages.ml
188 188
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
189 189
  let prog = Normalization.normalize_prog params prog in
190 190
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
191

  
191
  
192 192
  (* Compatibility with Lusi *)
193 193
  (* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)
194 194
  compile_source_to_header
195 195
    prog !Global.type_env !Global.clock_env dirname basename extension;
196 196

  
197

  
197 198
  let prog =
198 199
    if !Options.mpfr
199 200
    then
src/corelang.ml
220 220
    eexpr_quantifiers = [];
221 221
    eexpr_type = Types.new_var ();
222 222
    eexpr_clock = Clocks.new_var true;
223
    eexpr_normalized = None;
224 223
    eexpr_loc = loc }
225 224

  
226 225
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
......
805 804
     eexpr_tag = Utils.new_tag ();
806 805
     eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
807 806
     eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;
808
     eexpr_normalized = Utils.option_map 
809
       (fun (vdecl, eqs, vdecls) ->
810
	 rename_var f_node f_var vdecl,
811
	 List.map (rename_eq f_node f_var) eqs,
812
	 rename_vars f_node f_var vdecls
813
       ) ee.eexpr_normalized;
814
     
815 807
   }
816 808
 
817 809
     
......
1035 1027
     eexpr_type = expr.expr_type;
1036 1028
     eexpr_clock = expr.expr_clock;
1037 1029
     eexpr_loc = expr.expr_loc;
1038
     eexpr_normalized = None
1039 1030
   }
1040 1031
 (* and expr_desc_to_eexpr_desc expr_desc = *)
1041 1032
 (*   let conv = expr_to_eexpr in *)
src/corelang.mli
86 86
val const_xor: constant -> constant -> constant
87 87
val const_impl: constant -> constant -> constant
88 88

  
89
val get_var: ident -> var_decl list -> var_decl
89 90
val get_node_vars: node_desc -> var_decl list
90 91
val get_node_var: ident -> node_desc -> var_decl
91 92
val get_node_eqs: node_desc -> eq list * automata_desc list
src/lustre_types.ml
118 118
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
119 119
     mutable eexpr_type: Types.type_expr;
120 120
     mutable eexpr_clock: Clocks.clock_expr;
121
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
121
     (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
122 122
     eexpr_loc: Location.t}
123 123

  
124 124
and expr_annot =
src/machine_code.ml
20 20

  
21 21

  
22 22
       
23
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)
23
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
24 24
(* the context contains  m : state aka memory variables  *)
25 25
(*                      si : initialization instructions *)
26 26
(*                       j : node aka machine instances  *)
27 27
(*                       d : local variables             *)
28 28
(*                       s : step instructions           *)
29
let translate_ident node (m, si, j, d, s) id =
29
let translate_ident vars _ (* (m, si, j, d, s) *) id =
30 30
  (* Format.eprintf "trnaslating ident: %s@." id; *)
31
  try (* id is a node var *)
32
    let var_id = get_node_var id node in
31
  try (* id is a var that shall be visible here , ie. in vars *)
32
    let var_id = get_var id vars in
33 33
    mk_val (Var var_id) var_id.var_type
34 34
  with Not_found ->
35 35
    try (* id is a constant *)
36
      let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in
36
      let vdecl = (Corelang.var_decl_of_const
37
                     (const_of_top (Hashtbl.find Corelang.consts_table id)))
38
      in
37 39
      mk_val (Var vdecl) vdecl.var_type
38 40
    with Not_found ->
39 41
      (* id is a tag *)
40
      (* DONE construire une liste des enum declarés et alors chercher dedans la liste
41
	 qui contient id *)
42
      (* DONE construire une liste des enum declarés et alors chercher
43
         dedans la liste qui contient id *)
42 44
      try
43 45
        let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
44 46
        mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
45
      with Not_found -> (Format.eprintf "internal error: Machine_code.translate_ident %s" id;
47
      with Not_found -> (Format.eprintf
48
                           "internal error: Machine_code.translate_ident %s"
49
                           id;
46 50
                         assert false)
47 51

  
48
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =
52
let rec control_on_clock vars ((m, si, j, d, s) as args) ck inst =
49 53
 match (Clocks.repr ck).cdesc with
50 54
 | Con    (ck1, cr, l) ->
51 55
   let id  = Clocks.const_of_carrier cr in
52
   control_on_clock node args ck1 (mkinstr
56
   control_on_clock vars args ck1 (mkinstr
53 57
				     (* TODO il faudrait prendre le lustre
54 58
					associé à instr et rajouter print_ck_suffix
55 59
					ck) de clocks.ml *)
56
				     (MBranch (translate_ident node args id,
60
				     (MBranch (translate_ident vars args id,
57 61
					       [l, [inst]] )))
58 62
 | _                   -> inst
59 63

  
......
79 83
  | "C" -> specialize_to_c expr
80 84
  | _   -> expr
81 85

  
82
let rec translate_expr node ((m, si, j, d, s) as args) expr =
86
let rec translate_expr vars ((m, si, j, d, s) as args) expr =
83 87
  let expr = specialize_op expr in
88
  (* all calls are using the same arguments (vars for the variable
89
     enviroment and args for computed memories). No fold constructs
90
     here. We can do partial evaluation of translate_expr *)
91
  let translate_expr = translate_expr vars args in 
84 92
  let value_desc = 
85 93
    match expr.expr_desc with
86 94
    | Expr_const v                     -> Cst v
87
    | Expr_ident x                     -> (translate_ident node args x).value_desc
88
    | Expr_array el                    -> Array (List.map (translate_expr node args) el)
89
    | Expr_access (t, i)               -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
90
    | Expr_power  (e, n)               -> Power  (translate_expr node args e, translate_expr node args (expr_of_dimension n))
95
    | Expr_ident x                     -> (translate_ident vars args x).value_desc
96
    | Expr_array el                    -> Array (List.map translate_expr el)
97
    | Expr_access (t, i)               -> Access (translate_expr t,
98
                                                  translate_expr 
99
                                                    (expr_of_dimension i))
100
    | Expr_power  (e, n)               -> Power  (translate_expr e,
101
                                                  translate_expr
102
                                                    (expr_of_dimension n))
91 103
    | Expr_tuple _
92
    | Expr_arrow _ 
93
    | Expr_fby _
94
    | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
95
    | Expr_when    (e1, _, _)          -> (translate_expr node args e1).value_desc
104
      | Expr_arrow _ 
105
      | Expr_fby _
106
      | Expr_pre _                       -> (Printers.pp_expr
107
                                               Format.err_formatter expr;
108
                                             Format.pp_print_flush
109
                                               Format.err_formatter ();
110
                                             raise NormalizationError)
111
                                          
112
    | Expr_when    (e1, _, _)          -> (translate_expr e1).value_desc
96 113
    | Expr_merge   (x, _)              -> raise NormalizationError
97 114
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
98
      let nd = node_from_name id in
99
      Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
115
       let nd = node_from_name id in
116
       Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
100 117
    | Expr_ite (g,t,e) -> (
101 118
      (* special treatment depending on the active backend. For horn backend, ite
102 119
	 are preserved in expression. While they are removed for C or Java
103 120
	 backends. *)
104 121
      match !Options.output with
105 122
      | "horn" -> 
106
	 Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
123
	 Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
107 124
      | "C" | "java" | _ -> 
108 125
	 (Format.eprintf "Normalization error for backend %s: %a@."
109 126
	    !Options.output
......
114 131
  in
115 132
  mk_val value_desc expr.expr_type
116 133

  
117
let translate_guard node args expr =
134
let translate_guard vars args expr =
118 135
  match expr.expr_desc with
119
  | Expr_ident x  -> translate_ident node args x
120
  | _ -> (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false)
136
  | Expr_ident x  -> translate_ident vars args x
137
  | _ -> (Format.eprintf "internal error: translate_guard %a@."
138
            Printers.pp_expr expr;
139
          assert false)
121 140

  
122
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
141
let rec translate_act vars ((m, si, j, d, s) as args) (y, expr) =
142
  let translate_act = translate_act vars args in
143
  let translate_guard = translate_guard vars args in
144
  let translate_ident = translate_ident vars args in
145
  let translate_expr = translate_expr vars args in
123 146
  let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
124 147
  match expr.expr_desc with
125
  | Expr_ite   (c, t, e) -> let g = translate_guard node args c in
148
  | Expr_ite   (c, t, e) -> let g = translate_guard c in
126 149
			    mk_conditional ?lustre_eq:(Some eq) g
127
                              [translate_act node args (y, t)]
128
                              [translate_act node args (y, e)]
129
  | Expr_merge (x, hl)   -> mkinstr ?lustre_eq:(Some eq) (MBranch (translate_ident node args x,
130
                                     List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl))
131
  | _                    -> mkinstr ?lustre_eq:(Some eq)  (MLocalAssign (y, translate_expr node args expr))
150
                              [translate_act (y, t)]
151
                              [translate_act (y, e)]
152
  | Expr_merge (x, hl)   -> mkinstr ?lustre_eq:(Some eq)
153
                              (MBranch (translate_ident x,
154
                                        List.map (fun (t,  h) ->
155
                                            t, [translate_act (y, h)])
156
                                          hl))
157
  | _                    -> mkinstr ?lustre_eq:(Some eq)
158
                              (MLocalAssign (y, translate_expr expr))
132 159

  
133
let reset_instance node args i r c =
160
let reset_instance vars args i r c =
134 161
  match r with
135 162
  | None        -> []
136
  | Some r      -> let g = translate_guard node args r in
137
                   [control_on_clock node args c (mk_conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])]
163
  | Some r      -> let g = translate_guard vars args r in
164
                   [control_on_clock
165
                      vars
166
                      args
167
                      c
168
                      (mk_conditional
169
                         g
170
                         [mkinstr (MReset i)]
171
                         [mkinstr (MNoReset i)])
172
                   ]
173

  
174
let translate_eq vars ((m, si, j, d, s) as args) eq =
175
  let translate_expr = translate_expr vars args in
176
  let translate_act = translate_act vars args in
177
  let control_on_clock = control_on_clock vars args in
178
  let reset_instance = reset_instance vars args in
138 179

  
139
let translate_eq node ((m, si, j, d, s) as args) eq =
140
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
180
  (* Format.eprintf "translate_eq %a with clock %a@." 
181
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
141 182
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
142 183
  | [x], Expr_arrow (e1, e2)                     ->
143
     let var_x = get_node_var x node in
144
     let o = new_instance node Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
145
     let c1 = translate_expr node args e1 in
146
     let c2 = translate_expr node args e2 in
184
     let var_x = get_var x vars in
185
     let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
186
     let c1 = translate_expr e1 in
187
     let c2 = translate_expr e2 in
147 188
     (m,
148 189
      mkinstr (MReset o) :: si,
149 190
      Utils.IMap.add o (Arrow.arrow_top_decl, []) j,
150 191
      d,
151
      (control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)
152
  | [x], Expr_pre e1 when VSet.mem (get_node_var x node) d     ->
153
     let var_x = get_node_var x node in
192
      (control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)
193
  | [x], Expr_pre e1 when VSet.mem (get_var x vars) d     ->
194
     let var_x = get_var x vars in
154 195
     (VSet.add var_x m,
155 196
      si,
156 197
      j,
157 198
      d,
158
      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1))) :: s)
159
  | [x], Expr_fby (e1, e2) when VSet.mem (get_node_var x node) d ->
160
     let var_x = get_node_var x node in
199
      control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1))) :: s)
200
  | [x], Expr_fby (e1, e2) when VSet.mem (get_var x vars) d ->
201
     let var_x = get_var x vars in
161 202
     (VSet.add var_x m,
162
      mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1)) :: si,
203
      mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1)) :: si,
163 204
      j,
164 205
      d,
165
      control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e2))) :: s)
206
      control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e2))) :: s)
166 207

  
167 208
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
168
     let var_p = List.map (fun v -> get_node_var v node) p in
209
     let var_p = List.map (fun v -> get_var v vars) p in
169 210
     let el = expr_list_of_expr arg in
170
     let vl = List.map (translate_expr node args) el in
211
     let vl = List.map translate_expr el in
171 212
     let node_f = node_from_name f in
172 213
     let call_f =
173 214
       node_f,
174 215
       NodeDep.filter_static_inputs (node_inputs node_f) el in
175
     let o = new_instance node node_f eq.eq_rhs.expr_tag in
216
     let o = new_instance node_f eq.eq_rhs.expr_tag in
176 217
     let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
177 218
     let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
178 219
     (*Clocks.new_var true in
......
184 225
      d,
185 226
      (if Stateless.check_node node_f
186 227
       then []
187
       else reset_instance node args o r call_ck) @
188
	(control_on_clock node args call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s)
228
       else reset_instance o r call_ck) @
229
	(control_on_clock call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s)
189 230
  (*
190 231
    (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
191 232
    are preserved. While they are replaced as if g then x = t else x = e in  C or Java
......
204 245

  
205 246
  *)
206 247
  | [x], _                                       -> (
207
    let var_x = get_node_var x node in
248
    let var_x = get_var x vars in
208 249
    (m, si, j, d,
209 250
     control_on_clock
210
       node
211
       args
212 251
       eq.eq_rhs.expr_clock
213
       (translate_act node args (var_x, eq.eq_rhs)) :: s
252
       (translate_act (var_x, eq.eq_rhs)) :: s
214 253
    )
215 254
  )
216 255
  | _                                            ->
......
235 274
let translate_eqs node args eqs =
236 275
  List.fold_right (fun eq args -> translate_eq node args eq) eqs args;;
237 276

  
238
let translate_decl nd sch =
239
  (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
240
  let schedule = sch.Scheduling_type.schedule in
241
  let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in
242
  let constant_eqs = constant_equations nd in
243

  
244
  (* In case of non functional backend (eg. C), additional local variables have
245
     to be declared for each assert *)
246
  let new_locals, assert_instrs, nd_node_asserts =
277
let process_asserts nd =
278
  
247 279
    let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
248 280
    if Backends.is_functional () then
249 281
      [], [], exprl  
......
267 299
	  in
268 300
	  assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); 
269 301
	  let eq = mkeq loc ([var_id], expr) in
270
	  (i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)
302
          (i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)
271 303
	) (1, [], [], []) exprl
272 304
      in
273 305
      vars, eql, assertl
274
  in
275
  let locals_list = nd.node_locals @ new_locals in
306
  
307
let translate_decl nd sch =
308
  (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
309
  let schedule = sch.Scheduling_type.schedule in
310
  let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in
311
  let constant_eqs = constant_equations nd in
276 312

  
313
  (* In case of non functional backend (eg. C), additional local variables have
314
     to be declared for each assert *)
315
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
316
  let locals_list = nd.node_locals @ new_locals in
277 317
  let nd = { nd with node_locals = locals_list } in
318
  let vars = get_node_vars nd in
319
  
278 320
  let init_args = VSet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> VSet.add l) locals_list VSet.empty, [] in
279 321
  (* memories, init instructions, node calls, local variables (including memories), step instrs *)
280
  let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in
322

  
323
  let m0, init0, j0, locals0, s0 =
324
    translate_eqs vars init_args constant_eqs
325
  in
326

  
281 327
  assert (VSet.is_empty m0);
282 328
  assert (init0 = []);
283 329
  assert (Utils.IMap.is_empty j0);
284
  let m, init, j, locals, s as context_with_asserts = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in
330

  
331
  let m, init, j, locals, s as context_with_asserts =
332
    translate_eqs
333
      vars
334
      (m0, init0, j0, locals0, [])
335
      (assert_instrs@sorted_eqs)
336
  in
285 337
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
286 338
  {
287 339
    mname = nd;
......
295 347
      step_inputs = nd.node_inputs;
296 348
      step_outputs = nd.node_outputs;
297 349
      step_locals = VSet.elements (VSet.diff locals m);
298
      step_checks = List.map (fun d -> d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks;
350
      step_checks = List.map (fun d -> d.Dimension.dim_loc,
351
                                       translate_expr vars init_args
352
                                         (expr_of_dimension d))
353
                      nd.node_checks;
299 354
      step_instrs = (
300 355
	(* special treatment depending on the active backend. For horn backend,
301 356
	   common branches are not merged while they are in C or Java
......
308 363
	else
309 364
	  s
310 365
      );
311
      step_asserts = List.map (translate_expr nd context_with_asserts) nd_node_asserts;
366
      step_asserts = List.map (translate_expr vars context_with_asserts) nd_node_asserts;
312 367
    };
313 368
    mspec = nd.node_spec;
314 369
    mannot = nd.node_annot;
src/machine_code_common.ml
216 216

  
217 217
let new_instance =
218 218
  let cpt = ref (-1) in
219
  fun caller callee tag ->
219
  fun callee tag ->
220 220
    begin
221 221
      let o =
222 222
	if Stateless.check_node callee then
......
225 225
	  Printf.sprintf "ni_%d" (incr cpt; !cpt) in
226 226
      let o =
227 227
	if !Options.ansi && is_generic_node callee
228
	then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e -> e.expr_tag = tag) caller.node_gencalls)
228
	then Printf.sprintf "%s_inst_%d"
229
               o
230
               (incr cpt; !cpt)
229 231
	else o in
230 232
      o
231 233
    end
src/machine_code_common.mli
9 9
val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t
10 10
val empty_machine: Machine_code_types.machine_t
11 11
val arrow_machine: Machine_code_types.machine_t
12
val new_instance: Lustre_types.node_desc -> Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident
12
val new_instance: Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident
13 13
val value_of_dimension: Machine_code_types.machine_t -> Dimension.dim_expr -> Machine_code_types.value_t
14 14
val dimension_of_value:Machine_code_types.value_t -> Dimension.dim_expr
15 15
val pp_instr: Machine_code_types.machine_t -> Format.formatter -> Machine_code_types.instr_t -> unit
src/machine_code_types.ml
41 41

  
42 42
type static_call = top_decl * (Dimension.dim_expr list)
43 43

  
44
                 
44 45
type machine_t = {
45 46
  mname: node_desc;
46 47
  mmemory: var_decl list;
src/normalization.ml
170 170
      then
171 171
	let new_aliases =
172 172
	  List.map2
173
	    (mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc)
173
	    (mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)
174 174
	    (Types.type_list_of_type expr.expr_type)
175 175
	    (Clocks.clock_list_of_clock expr.expr_clock) in
176 176
	let new_def =
177 177
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
178 178
	in
179 179
	(* Typing and Registering machine type *) 
180
	let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr  in
180
	let _ = if Machine_types.is_active then
181
                  Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr
182
        in
181 183
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
182 184
      else
183 185
	(defs, vars), expr
......
400 402
let normalize_eq_split norm_ctx defvars eq =
401 403
  try
402 404
    let defs, vars = normalize_eq norm_ctx defvars eq in
403
  List.fold_right (fun eq (def, vars) -> 
404
    let eq_defs = Splitting.tuple_split_eq eq in
405
    if eq_defs = [eq] then
406
      eq::def, vars 
407
    else
408
      List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
409
  ) defs ([], vars)  
410

  
411
  with _ -> (
405
    List.fold_right (fun eq (def, vars) -> 
406
        let eq_defs = Splitting.tuple_split_eq eq in
407
        if eq_defs = [eq] then
408
          eq::def, vars 
409
        else
410
          List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
411
      ) defs ([], vars)  
412
    
413
  with ex -> (
412 414
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
413
    assert false
415
    raise ex
414 416
  )
415 417

  
416
let normalize_eexpr decls norm_ctx vars ee = ee (*
417
  (* New output variable *)
418
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
419
  let output_var = 
420
    mkvar_decl 
421
      ee.eexpr_loc 
422
      (output_id, 
423
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
424
       mkclock ee.eexpr_loc Ckdec_any, 
425
       false (* not a constant *),
426
       None,
427
       None
428
      ) 
418
(* Projecting an eexpr to an eexpr associated to a single
419
   variable. Returns the updated ee, the bounded variable and the
420
   associated statement *)
421
let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
422
  assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)
423
  (* don't do anything is eexpr is just a variable *)
424
  let skip =
425
    match ee.eexpr_qfexpr.expr_desc with
426
    | Expr_ident _ | Expr_const _ -> true
427
    | _ -> false
429 428
  in
429
  if skip then
430
    ee, (def, vars)
431
  else (
432
    (* New output variable *)
433
    let output_id = "spec" ^ string_of_int ee.eexpr_tag in
434
    let output_var = 
435
      mkvar_decl 
436
        ee.eexpr_loc 
437
        (output_id, 
438
         mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)
439
         mkclock ee.eexpr_loc Ckdec_any, 
440
         false (* not a constant *),
441
         None,
442
         None
443
        ) 
444
    in
445
    let output_expr = expr_of_vdecl output_var in
446
    (* Rebuilding an eexpr with a silly expression, just a variable *)
447
    let ee' = { ee with eexpr_qfexpr = output_expr } in
448

  
449
    (* Now processing a fresh equation output_id = eexpr_qfexpr. We
450
       inline possible calls within, normalize it and type/clock the
451
       result.  *)
452
    let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
453
    (* Inlining any calls *)
454
    let nodes = get_nodes decls in
455
    let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
456
    let vars, eqs =
457
      if calls = [] && not (eq_has_arrows eq) then
458
        vars, [eq]    
459
      else
460
        assert false (* TODO *)
461
    in
462
    
463
    (* Normalizing expr and eqs *)
464
    let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) eqs in
465
(*    let todefine =
466
      List.fold_left
467
        (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
468
        (ISet.add output_id ISet.empty) vars in
469
 *)      
470

  
471
    (* Typing / Clocking *)
472
    try
473
      ignore (Typing.type_var_decl_list vars !Global.type_env vars);
474
        (*
475
    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
476
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
477
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
478
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
479
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
480
  (* check that table is empty *)
481
    if (not (ISet.is_empty undefined_vars)) then
482
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
483
    
484
    (*Format.eprintf "normalized eqs %a@.@?" 
485
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
486
         *)
487

  
488
    ee', (defs, vars)
489
    
490
  with (Types.Error (loc,err)) as exc ->
491
    eprintf "Typing error for eexpr %a: %a%a%a@."
492
      Printers.pp_eexpr ee
493
      Types.pp_error err
494
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
495
      Location.pp_loc loc
496
  
497
      
498
    ;
499
    raise exc
500
                                     
501
  )
502
    
503
   (*
430 504
  
431 505
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
432 506
  (* Calls are first inlined *)
433
  let nodes = get_nodes decls in
434
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
435
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
436
   let calls = List.map 
437
    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls 
438
  in
439
*)
507
  
440 508
  (*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls;  *)
441
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
442
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
443 509
  let (new_locals, eqs) =
444 510
    if calls = [] && not (eq_has_arrows eq) then
445 511
      (locals, [eq])     
......
485 551
    raise exc
486 552
                                                 *)    
487 553
 
488
    
489
let normalize_spec decls iovars s = s (*
490
  (* Each stmt is normalized *)
491
  let orig_vars = iovars @ s.locals in
554

  
555
(* We use node local vars to make sure we are creating fresh variables *) 
556
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =  
557
  (* Original set of variables actually visible from here: iun/out and
558
     spec locals (no node locals) *)
559
  let orig_vars = in_vars @ out_vars @ s.locals in
492 560
  let not_is_orig_var v =
493 561
    List.for_all ((!=) v) orig_vars in
494
  let defs, vars = 
495
    let eqs, auts = List.fold_right (fun (el,al) s -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
496
    if auts != [] then assert false; (* Automata should be expanded by now. *)
497
    List.fold_left (normalize_eq node) ([], orig_vars) eqs
562
  let norm_ctx = {
563
      parentid = parentid;
564
      vars = in_vars @ out_vars @ l_vars;
565
      is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);
566
    }
567
  in
568
  (* Normalizing existing stmts *)
569
  let eqs, auts = List.fold_right (fun s (el,al)  -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
570
  if auts != [] then assert false; (* Automata should be expanded by now. *)
571
  let defsvars = 
572
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs
573
  in
574
  (* Iterate through predicates and normalize them on the go, creating
575
     fresh variables for any guarantees/assumes/require/ensure *)
576
  let process_predicates l defvars =
577
    List.fold_right (fun ee (accu, defvars) ->
578
        let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in
579
        ee'::accu, defvars
580
      ) l ([], defvars)
498 581
  in
499
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
500 582

  
501
  (*
583
  
584
  let assume', defsvars = process_predicates s.assume defsvars in
585
  let guarantees', defsvars = process_predicates s.guarantees defsvars in
586
  let modes', (defs, vars) =
587
    List.fold_right (
588
        fun m (accu_m, defsvars) ->
589
        let require', defsvars = process_predicates m.require defsvars in
590
        let ensure', defsvars = process_predicates m.ensure defsvars in
591
        { m with require = require'; ensure = ensure' }:: accu_m, defsvars
592
      ) s.modes ([], defsvars)
593
  in
594
  
595
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
596
   
502 597
      
503 598
  {s with
504 599
    locals = s.locals @ new_locals;
505 600
    stmts = List.map (fun eq -> Eq eq) defs;
506
  let nee _ = () in
507
  (*normalize_eexpr decls iovars in *)
508
  List.iter nee s.assume;
509
  List.iter nee s.guarantees;
510
  List.iter (fun m -> 
511
      List.iter nee m.require;
512
    List.iter nee m.ensure
513
    ) s.modes;
514
   *)
515
  s
516
                                       *)
601
    assume = assume';
602
    guarantees = guarantees';
603
    modes = modes'
604
  }
605
(* let nee _ = () in
606
 *   (\*normalize_eexpr decls iovars in *\)
607
 *   List.iter nee s.assume;
608
 *   List.iter nee s.guarantees;
609
 *   List.iter (fun m -> 
610
 *       List.iter nee m.require;
611
 *     List.iter nee m.ensure
612
 *     ) s.modes; *)
613
   
614

  
615
                                                                     
616
  
617
  
517 618
    
518 619
(* The normalization phase introduces new local variables
519 620
   - output cannot be memories. If this happen, new local variables acting as
......
534 635
*)
535 636
let normalize_node decls node =
536 637
  reset_cpt_fresh ();
537
  let inputs_outputs = node.node_inputs@node.node_outputs in
538
  let orig_vars = inputs_outputs@node.node_locals in
638
  let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
539 639
  let not_is_orig_var v =
540 640
    List.for_all ((!=) v) orig_vars in
541 641
  let norm_ctx = {
......
636 736

  
637 737
	 Careful: we do not normalize annotations, since they can have the form
638 738
	 x = (a, b, c) *)
639
      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls inputs_outputs s) 
739
      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s) 
640 740
    end
641 741
  in
642 742
  
......
658 758
  match nd.nodei_spec with
659 759
    None -> nd
660 760
  | Some s ->
661
     let inputs_outputs = nd.nodei_inputs@nd.nodei_outputs in
662
     let s = normalize_spec decls inputs_outputs s in
761
     let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in
663 762
     { nd with nodei_spec = Some s }
664 763
  
665 764
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
src/typing.ml
27 27
open Format
28 28

  
29 29

  
30
(* TODO general remark: expect in the add_vdelc, it seems to me that
30
(* TODO general remark: except in the add_vdecl, it seems to me that
31 31
   all the pairs (env, vd_env) should be replace with just env, since
32 32
   vd_env is never used and the env element is always extract with a
33 33
   fst *)
......
686 686
          undefined_vars_init
687 687
          eqs
688 688
      in
689
      
689
      (* Typing each predicate expr *)
690
      let type_pred_ee ee : unit=
691
        type_subtyping_arg (env, vd_env) (false (* not in main *)) (false (* not a const *)) ee.eexpr_qfexpr type_bool
692
      in
693
      List.iter type_pred_ee
694
        (
695
          spec.assume 
696
          @ spec.guarantees
697
          @ List.flatten (List.map (fun m -> m.ensure @ m.require) spec.modes) 
698
        );
690 699
      (*TODO 
691 700
        enrich env locally with locals and consts
692 701
        type each pre/post as a boolean expr

Also available in: Unified diff