Project

General

Profile

Revision 63f10e14 src/machine_code.ml

View differences:

src/machine_code.ml
394 394
                   [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
395 395

  
396 396
let translate_eq node ((m, si, j, d, s) as args) eq =
397
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
397
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
398 398
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
399 399
  | [x], Expr_arrow (e1, e2)                     ->
400
    let var_x = get_node_var x node in
401
    let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in
402
    let c1 = translate_expr node args e1 in
403
    let c2 = translate_expr node args e2 in
404
    (m,
405
     MReset o :: si,
406
     Utils.IMap.add o (arrow_top_decl, []) j,
407
     d,
408
     (control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)
400
     let var_x = get_node_var x node in
401
     let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in
402
     let c1 = translate_expr node args e1 in
403
     let c2 = translate_expr node args e2 in
404
     (m,
405
      MReset o :: si,
406
      Utils.IMap.add o (arrow_top_decl, []) j,
407
      d,
408
      (control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)
409 409
  | [x], Expr_pre e1 when ISet.mem (get_node_var x node) d     ->
410
    let var_x = get_node_var x node in
411
    (ISet.add var_x m,
412
     si,
413
     j,
414
     d,
415
     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)
410
     let var_x = get_node_var x node in
411
     (ISet.add var_x m,
412
      si,
413
      j,
414
      d,
415
      control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)
416 416
  | [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->
417
    let var_x = get_node_var x node in
418
    (ISet.add var_x m,
419
     MStateAssign (var_x, translate_expr node args e1) :: si,
420
     j,
421
     d,
422
     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
417
     let var_x = get_node_var x node in
418
     (ISet.add var_x m,
419
      MStateAssign (var_x, translate_expr node args e1) :: si,
420
      j,
421
      d,
422
      control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
423 423

  
424 424
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
425
    let var_p = List.map (fun v -> get_node_var v node) p in
426
    let el = expr_list_of_expr arg in
427
    let vl = List.map (translate_expr node args) el in
428
    let node_f = node_from_name f in
429
    let call_f =
430
      node_f,
431
      NodeDep.filter_static_inputs (node_inputs node_f) el in
432
    let o = new_instance node node_f eq.eq_rhs.expr_tag in
433
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
434
    let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
435
    (*Clocks.new_var true in
436
    Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
437
    Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
438
    (m,
439
     (if Stateless.check_node node_f then si else MReset o :: si),
440
     Utils.IMap.add o call_f j,
441
     d,
442
     (if Stateless.check_node node_f
443
      then []
444
      else reset_instance node args o r call_ck) @
445
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
446
(*
447
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
448
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
449
      backends. *)
450
  | [x], Expr_ite   (c, t, e)
425
     let var_p = List.map (fun v -> get_node_var v node) p in
426
     let el = expr_list_of_expr arg in
427
     let vl = List.map (translate_expr node args) el in
428
     let node_f = node_from_name f in
429
     let call_f =
430
       node_f,
431
       NodeDep.filter_static_inputs (node_inputs node_f) el in
432
     let o = new_instance node node_f eq.eq_rhs.expr_tag in
433
     let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
434
     let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
435
     (*Clocks.new_var true in
436
       Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
437
       Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
438
     (m,
439
      (if Stateless.check_node node_f then si else MReset o :: si),
440
      Utils.IMap.add o call_f j,
441
      d,
442
      (if Stateless.check_node node_f
443
       then []
444
       else reset_instance node args o r call_ck) @
445
	(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
446
  (*
447
    (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
448
    are preserved. While they are replaced as if g then x = t else x = e in  C or Java
449
    backends. *)
450
    | [x], Expr_ite   (c, t, e)
451 451
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
452
      ->
452
    ->
453 453
    let var_x = get_node_var x node in
454 454
    (m,
455
     si,
456
     j,
457
     d,
458
     (control_on_clock node args eq.eq_rhs.expr_clock
459
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
455
    si,
456
    j,
457
    d,
458
    (control_on_clock node args eq.eq_rhs.expr_clock
459
    (MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
460 460
    )
461 461

  
462
*)
462
  *)
463 463
  | [x], _                                       -> (
464 464
    let var_x = get_node_var x node in
465 465
    (m, si, j, d,
......
471 471
    )
472 472
  )
473 473
  | _                                            ->
474
    begin
475
      Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;
476
      assert false
477
    end
474
     begin
475
       Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;
476
       assert false
477
     end
478 478

  
479 479
let find_eq xl eqs =
480 480
  let rec aux accu eqs =

Also available in: Unified diff