CristalCaveGem » LustreC

  mstatic: var_decl list; (* static inputs only *)

  mstep: step_t;

  mspec: node_annot option;

}

let pp_step fmt s =

    node_dec_stateless = false;

    node_stateless = Some false;

    node_spec = None;

let arrow_top_decl =

  {

                                 [MLocalAssign(var_output, LocalVar var_input2)] ]

    };

    mspec = None;

  }

let new_instance =

(*                       s : step instructions           *)

let translate_ident node (m, si, j, d, s) id =

  try (* id is a node var *)

    if ISet.exists (fun v -> v.var_id = id) m

    then StateVar var_id

    else LocalVar var_id

  (*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*)

  match eq.eq_lhs, eq.eq_rhs.expr_desc with

  | [x], Expr_arrow (e1, e2)                     ->

    let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in

    let c1 = translate_expr node args e1 in

    let c2 = translate_expr node args e2 in

     Utils.IMap.add o (arrow_top_decl, []) j,

     d,

     (control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)

    (ISet.add var_x m,

     si,

     j,

     d,

     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)

    (ISet.add var_x m,

     MStateAssign (var_x, translate_expr node args e1) :: si,

     j,

     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)

  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) ->

    let el =

      match arg.expr_desc with

      | Expr_tuple el -> el

  | [x], Expr_ite   (c, t, e) 

    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)

      -> 

    (m, 

     si, 

     j, 

    )

  | [x], _                                       -> (

    (m, si, j, d, 

     control_on_clock 

       node