Project

General

Profile

« Previous | Next » 

Revision 0406ab94

Added by LĂ©lio Brun 7 months ago

implement optimization on spec: IT WORKS

View differences:

src/machine_code.ml
186 186
  (* Transition spec *)
187 187
  t :
188 188
    (var_decl list
189
    (* inputs *)
190
    * var_decl list
191
    (* locals *)
192
    * var_decl list
193
    (* outputs *)
189
    (* vars *)
194 190
    * ISet.t (* memory footprint *)
195 191
    * ident IMap.t
196 192
    (* memory instances footprint *)
......
247 243
  let outputs_i = Lustre_live.inter_live_i_with id i outputs in
248 244
  let pred_mp ctx a = And [ mk_memory_pack ~i:(i - 1) id; a ] :: ctx.mp in
249 245
  let pred_t ctx a =
250
    ( inputs,
251
      locals_i,
252
      outputs_i,
246
    ( inputs @ locals_i @ outputs_i,
253 247
      ctx.m,
254 248
      IMap.map (fun (td, _) -> node_name td) ctx.j,
255 249
      Exists
256 250
        ( Lustre_live.existential_vars id i eq (locals @ outputs),
257 251
          And
258 252
            [
259
              mk_transition ~i:(i - 1) id (vdecls_to_vals inputs)
260
                (vdecls_to_vals locals_pi)
261
                (vdecls_to_vals outputs_pi);
253
              mk_transition ~i:(i - 1) id
254
                (vdecls_to_vals (inputs @ locals_pi @ outputs_pi));
262 255
              a;
263 256
            ] ) )
264 257
    :: ctx.t
......
274 267
            (if fst (get_stateless_status_node nd) then []
275 268
            else [ mk_memory_pack ~i id ])
276 269
            @ [
277
                mk_transition ~i id (vdecls_to_vals inputs)
278
                  (vdecls_to_vals locals_i) (vdecls_to_vals outputs_i);
270
                mk_transition ~i id
271
                  (vdecls_to_vals (inputs @ locals_i @ outputs_i));
279 272
              ];
280 273
        }
281 274
        :: ctx.s;
......
304 297
      ctl
305 298
        (MStep ([ var_x ], inst, [ c1; c2 ]))
306 299
        (mk_memory_pack ~inst (node_name td))
307
        (mk_transition ~inst (node_name td) [] [] [ vdecl_to_val var_x ])
300
        (mk_transition ~inst (node_name td) [ vdecl_to_val var_x ])
308 301
        { ctx with j = IMap.add inst (td, []) ctx.j }
309 302
    in
310 303
    { ctx with si = mkinstr (MSetReset inst) :: ctx.si }
......
332 325
    }
333 326
  | p, Expr_appl (f, arg, r)
334 327
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
335
    let var_p = List.map (fun v -> env.get_var v) p in
328
    let var_p = List.map env.get_var p in
336 329
    let el = expr_list_of_expr arg in
337 330
    let vl = List.map translate_expr el in
338 331
    let node_f = node_from_name f in
......
351 344
      ctl ~ck:call_ck
352 345
        (MStep (var_p, inst, vl))
353 346
        (mk_memory_pack ~inst (node_name node_f))
354
        (mk_transition ?r ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
347
        (mk_transition ?r ~inst (node_name node_f) (vl @ vdecls_to_vals var_p))
355 348
        {
356 349
          ctx with
357 350
          j = IMap.add inst call_f ctx.j;
......
472 465
  {
473 466
    tname = nd;
474 467
    tindex = Some 0;
475
    tinputs = nd.node_inputs;
476
    tlocals = [];
477
    toutputs = [];
468
    tvars = nd.node_inputs;
478 469
    tformula = True;
479 470
    tmem_footprint = ISet.empty;
480 471
    tinst_footprint = IMap.empty;
......
483 474
let transition_toplevel nd i =
484 475
  let tr =
485 476
    mk_transition nd.node_id ~i
486
      (vdecls_to_vals nd.node_inputs)
487
      []
488
      (vdecls_to_vals nd.node_outputs)
477
      (vdecls_to_vals (nd.node_inputs @ nd.node_outputs))
489 478
  in
490 479
  {
491 480
    tname = nd;
492 481
    tindex = None;
493
    tinputs = nd.node_inputs;
494
    tlocals = [];
495
    toutputs = nd.node_outputs;
482
    tvars = nd.node_inputs @ nd.node_outputs;
496 483
    tformula =
497 484
      (if fst (get_stateless_status_node nd) then tr
498 485
      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
......
564 551
    transition_0 nd
565 552
    ::
566 553
    List.mapi
567
      (fun i (tinputs, tlocals, toutputs, tmem_footprint, tinst_footprint, f) ->
554
      (fun i (tvars, tmem_footprint, tinst_footprint, f) ->
568 555
        {
569 556
          tname = nd;
570 557
          tindex = Some (i + 1);
571
          tinputs;
572
          tlocals;
573
          toutputs;
558
          tvars;
574 559
          tformula = red f;
575 560
          tmem_footprint;
576 561
          tinst_footprint;
......
583 568
      ~instr_spec:
584 569
        ((if fst (get_stateless_status_node nd) then []
585 570
         else [ mk_memory_pack ~i:0 nd.node_id ])
586
        @ [
587
            mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) [] [];
588
          ])
571
        @ [ mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) ])
589 572
      MClearReset
590 573
  in
591 574
  {

Also available in: Unified diff