CristalCaveGem » LustreC

    | Fun (n, vl)   -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl

let rec pp_instr fmt i =

    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v

    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v

    | MReset i           -> Format.fprintf fmt "reset %s" i

let is_memory m id =

  List.exists (fun o -> o.var_id = id.var_id) m.mmemory

let dummy_var_decl name typ =

  {

    mmemory = [var_state];

    mcalls = [];

    minstances = [];

    mstatic = [];

    mconst = [];

    mstep = {

      step_locals = [];

      step_checks = [];

      step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool)

      step_asserts = [];

    };

    mspec = None;

 match (Clocks.repr ck).cdesc with

 | Con    (ck1, cr, l) ->

   let id  = Clocks.const_of_carrier cr in

 | _                   -> inst

let rec join_branches hl1 hl2 =

   else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2

and join_guards inst1 insts2 =

 | _                   , []                               ->

   [inst1]

 | MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 ->

 | _ -> inst1 :: insts2

let join_guards_list insts =

let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =

  match expr.expr_desc with

  | Expr_ite   (c, t, e) -> let g = translate_guard node args c in

                              [translate_act node args (y, t)]

                              [translate_act node args (y, e)]

let reset_instance node args i r c =

  match r with

  | None        -> []

  | Some r      -> let g = translate_guard node args r in

let translate_eq node ((m, si, j, d, s) as args) eq =

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

     let c1 = translate_expr node args e1 in

     let c2 = translate_expr node args e2 in

     (m,

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

      d,

  | [x], Expr_pre e1 when ISet.mem (get_node_var x node) d     ->

     let var_x = get_node_var x node in

     (ISet.add var_x m,

      si,

      j,

      d,

  | [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->

     let var_x = get_node_var x node in

     (ISet.add var_x m,

      j,

      d,

  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->

     let var_p = List.map (fun v -> get_node_var v node) p in

       Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;

       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;*)

     (m,

      Utils.IMap.add o call_f j,

      d,

      (if Stateless.check_node node_f

       then []

       else reset_instance node args o r call_ck) @

  (*

    (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)

    are preserved. While they are replaced as if g then x = t else x = e in  C or Java

let get_const_assign m id =

  try

    | MLocalAssign (_, e) -> e

    | _                   -> assert false

  with Not_found -> assert false