CristalCaveGem » LustreC

  let pp_step_definition env typed_submachines fmt (m, m_spec_opt, guarantees) =

    let transform_local_to_state_assign instr = match instr.instr_desc with

      | MLocalAssign (ident, value) -> 

      | _ -> instr

    in

    let pp_local_ghost_list, spec_instrs = match m_spec_opt with

  **)

  let pp_reset_definition env typed_submachines fmt (m, m_spec_opt) =

    let build_assign = function var ->

    in

    let env, memory = match m_spec_opt with

      | None -> env, m.mmemory

              in

              let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in

              { instr_desc = assign;

              }

            in

            let mkval_var id = {

  e

let get_instr_desc i = i.instr_desc

let update_instr_desc i id = { i with instr_desc = id }

val mktop: top_decl_desc -> top_decl

(* constructor for machine types *)

val get_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc

val update_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t

   delay

   machine_code_types

   spec_types

   scheduling_type

   log

   printers

open Lustre_types

open Machine_code_types

open Machine_code_common

open Corelang

open Clocks

open Causality

exception NormalizationError

let translate_ident env id =

  (* Format.eprintf "trnaslating ident: %s@." id; *)

    let var_id = env.get_var id in

    mk_val (Var var_id) var_id.var_type

  with Not_found ->

    let vdecl = (Corelang.var_decl_of_const

                   (const_of_top (Hashtbl.find Corelang.consts_table id)))

    in

    mk_val (Var vdecl) vdecl.var_type

  with Not_found ->

  try

    let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in

    mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)

    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;

    assert false

(* specialize predefined (polymorphic) operators wrt their instances,

   so that the C semantics is preserved *)

      [translate_act (y, t)]

      [translate_act (y, e)]

  | Expr_merge (x, hl) ->

(* Datastructure updated while visiting equations *)

type machine_ctx = {

  si: instr_t list;

  s: instr_t list;

}

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

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

   are building *) 

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

let translate_eq env ctx eq =

  let translate_expr = translate_expr env in

  let translate_act = translate_act env in

  let reset_instance = reset_instance env in

  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =

    control_on_clock ck (mkinstr' instr) in

    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in

    let c1 = translate_expr e1 in

    let c2 = translate_expr e2 in

    { ctx with

    }

  | [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) ->

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

    { ctx with

      si = if Stateless.check_node node_f

      s = (if Stateless.check_node node_f

    }

  | [x], _ ->

    let var_x = env.get_var x in

  | _ ->

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

      Printers.pp_node_eq eq;

      if vdecl.var_dec_const

      then

        { eq_lhs = [vdecl.var_id];

          eq_loc = vdecl.var_loc

        } :: eqs

      else eqs)

  let ctx0 = translate_eqs env ctx_init constant_eqs in

  assert (VSet.is_empty ctx0.m);

  assert (ctx0.si = []);

  (* Compute ctx for all eqs *)

  let ctx = translate_eqs env ctx_init sorted_eqs in

    let l = VSet.elements (VSet.diff locals ctx.m) in

    List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l

  in

  {

    mname = nd;

    mmemory = VSet.elements ctx.m;

    List.map

      (fun decl ->

         let node = node_of_top decl in

         translate_decl node sch

      ) nodes

  in

open Lustre_types

open Machine_code_types

open Corelang

let print_statelocaltag = true

let is_output m id =

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

let mk_conditional ?lustre_eq c t e =

let mk_val v t =

  { value_desc = v; 

    mmemory = [var_state];

    mcalls = [];

    minstances = [];

    mstatic = [];

    mconst = [];

    mstep = {

      step_locals = [];

      step_checks = [];

      step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)

			[MStateAssign(var_state, cst false);

			 MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])

			[MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];

      step_asserts = [];

    };

 | _                   , []                               ->

   [inst1]

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

      (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)

      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))

   :: (List.tl insts2)

val is_stateless: Machine_code_types.machine_t -> bool

val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_types.value_t

val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t

val empty_machine: Machine_code_types.machine_t

val arrow_machine: Machine_code_types.machine_t

val new_instance: Lustre_types.top_decl -> Lustre_types.tag -> Lustre_types.ident

(************ Machine code types *************)

open Lustre_types

open Spec_types

type value_t =

  {

    value_desc: value_t_desc;

  | Access of value_t * value_t

  | Power of value_t * value_t

type instr_t =

  {

    instr_desc: instr_t_desc; (* main data: the content *)

    (* lustre_expr: expr option; (* possible representation as a lustre expression *) *)

    lustre_eq: eq option;     (* possible representation as a lustre flow equation *)

  }

and instr_t_desc =

  | MLocalAssign of var_decl * value_t

type machine_spec = {

  mnode_spec: node_spec_t option;

}

type machine_t = {

  let vdecl = { vdecl with var_type = const.const_type } in

  let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in

  mkinstr

    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))

(* We do not perform this optimization on contract nodes since there

let update_machine main_node machine scopes =

  let stateassign (vdecl_mem, vdecl_orig) =

    (MStateAssign (vdecl_mem, mk_val (Var vdecl_orig) vdecl_orig.var_type))

  in

  let selection =

    mstep = { 

      machine.mstep with 

        step_instrs = machine.mstep.step_instrs

    }

  }

  | In

  | Out

  | Var of var_decl

  | Instance of state_t * ident

  | Memory of state_t * ident

type predicate_t =

  tname: node_desc;

  tlocals: var_decl list;

  toutputs: var_decl list;

}

  let equal n1 n2 = n1 = n2

end

module ISet = Set.Make(IdentModule)

module IdentDepGraph = Imperative.Digraph.ConcreteBidirectional (IdentModule)

module TopologicalDepGraph = Topological.Make(IdentDepGraph)