CristalCaveGem » LustreC

(* Datastructure updated while visiting equations *)

type machine_ctx = {

  (* Memories *)

  m: VSet.t;

  (* Reset instructions *)

  t: mc_formula_t list;

}

  m = VSet.empty;

  si = [];

  j = IMap.empty;

  t = []

}

(****************************************************************)

(* Main function to translate equations into this machine context we

   are building *) 

(****************************************************************)

  mkinstr

    (MBranch (v, [l, [inst]]))

    match (Clocks.repr ck).cdesc with

    | Con (ck, cr, l) ->

      let id = Clocks.const_of_carrier cr in

      let ck_spec = mk_condition v l in

      aux (id :: ck_ids,

           v :: vs,

           },

    | _ -> acc

  in

let reset_instance env i r c =

  match r with

  | Some r ->

  | None -> []

  let translate_expr = translate_expr env in

  let translate_act = translate_act env in

  in

  let reset_instance = reset_instance env in

  let mkinstr' = mkinstr ~lustre_eq:eq True in

  (* 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 var_x = env.get_var x in

    let c1 = translate_expr e1 in

    let c2 = translate_expr e2 in

    { ctx with

      si = mkinstr True (MReset o) :: ctx.si;

    }

  | [x], Expr_pre e1 when env.is_local x    ->

    let var_x = env.get_var x in

    { ctx with

      m = VSet.add var_x ctx.m;

    }

  | [x], Expr_fby (e1, e2) when env.is_local x ->

    let var_x = env.get_var x in

    { ctx with

      m = VSet.add var_x ctx.m;

      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;

    }

  | p, Expr_appl (f, arg, r)

    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->

    let var_p = List.map (fun v -> env.get_var v) p in

        el [eq.eq_rhs.expr_clock] in

    let call_ck = Clock_calculus.compute_root_clock

        (Clock_predef.ck_tuple env_cks) in

    (*Clocks.new_var true 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;*)

           else reset_instance o r call_ck)

          @ ctx.s

    }

  | [x], _ ->

    let var_x = env.get_var x in

  | _ ->

    Format.eprintf "internal error: Machine_code.translate_eq %a@?"

      Printers.pp_node_eq eq;

    locals []

let translate_eqs env ctx eqs =

(****************************************************************)

    in

    vars, eql, assertl

  let constant_eqs = constant_equations locals in

  let env = build_env locals other_vars  in

  (* Compute constants' instructions  *)

  assert (VSet.is_empty ctx0.m);

  assert (ctx0.si = []);

  assert (IMap.is_empty ctx0.j);

  (* Compute ctx for all eqs *)

  ctx, ctx0.s

   *   VSet.pp inout_vars

   * ; *)

  (* Format.eprintf "ok4@.@?"; *)