CristalCaveGem » LustreC

open LustreSpec

open Corelang

open Machine_code

let pp_var fmt id = Format.pp_print_string fmt id.var_id

let rec pp_c_val self pp_var fmt v =

  match v with

  | Cst c         -> C_backend_common.pp_c_const fmt c

  | Array _      

  | Access _

  | Power _  -> assert false

  | LocalVar v    -> pp_var fmt v

  | StateVar v    ->

    (* array memory vars are represented by an indirection to a local var with the right type,

       in order to avoid casting everywhere. *)

    if Types.is_array_type v.var_type

    then assert false

    else Format.fprintf fmt "%s_%a" self pp_var v

  | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl

module CSrc = C_backend_src.Main (C_backend_src.EmptyMod) 

(* let pp_assign = CSrc.pp_assign *)

let pp_assign m self pp_var fmt var_type var_name value =

  Format.fprintf fmt "%a = %a;" 

    (pp_c_val self pp_var) var_name

    (pp_c_val self pp_var) value

let check_type_restrictions m =

  (* Checking that all memories are of type real. Since everything should be

     inlined, only arrows instances would be allowed *)

  let is_real_var v = Types.is_real_type v.var_type in

  if not (List.for_all is_real_var m.mmemory) then (

    Format.eprintf "Main node contains variable with non real type: %s@.@?"

      (List.find (fun v -> not (is_real_var v)) m.mmemory).var_id ;

    assert false

  ) else

    Format.printf " - All variables are real: OK@.";

  let call_name (_, (td, _)) = node_name td in 

  let is_arrow_call c = call_name c = "_arrow" in

  if not (List.for_all is_arrow_call m.minstances) then (

    Format.eprintf "All calls are not inlined: call to node %s@.@?"

      (call_name (List.find (fun c -> not (is_arrow_call c)) m.minstances)) ;

    assert false    

  ) else

    Format.printf " - All calls inlined: OK@."

let rec pp_conditional (m: machine_t) self fmt c tl el =

  Format.fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"

    (pp_c_val self pp_var) c

    (Utils.pp_newline_if_non_empty tl)

    (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) tl

    (Utils.pp_newline_if_non_empty el)

    (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) el

and pp_machine_instr (m: machine_t) self fmt instr =

  match instr with 

  | MReset i -> assert false (* no reset allowed *)

  | MLocalAssign (i,v) -> 

    pp_assign m self pp_var fmt i.var_type (LocalVar i) v

  | MStateAssign (i,v) (* state variable are handled as local ones *)

    -> pp_assign m self pp_var fmt i.var_type (StateVar i) v

  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->

    pp_machine_instr m self fmt (MLocalAssign (i0, Fun (i, vl)))

  | MStep (il, i, vl) -> 

    assert false (* no calls *)

  | MBranch (g,hl) -> 

    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false

    then (* boolean case, needs special treatment in C because truth value is not unique *)

	 (* may disappear if we optimize code by replacing last branch test with default *)

      let tl = try List.assoc tag_true  hl with Not_found -> [] in

      let el = try List.assoc tag_false hl with Not_found -> [] in

      pp_conditional m self fmt g tl el

    else (* enum type case *)

      assert false

let rec extract_init_step m instrs = 

  let extract = extract_init_step m in

    let f instr = 

      match instr with

      | MReset i -> assert false (* no reset allowed *)

      | MLocalAssign _ 

      | MStateAssign _ -> instr, instr

      | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->

	let instr = MLocalAssign (i0, Fun (i, vl)) in

	instr, instr

      | MStep (il, i, vl) -> (

	let (n,_) = List.assoc i m.minstances in

	match node_name n, vl, il with

	| "_arrow", [i1; i2], [o] -> 

	  MLocalAssign(o, i1), MLocalAssign(o, i2) 

	| _ -> assert false (* no calls allowed *)

      )

    | MBranch (g,hl) -> 

      if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false

      then 

      let tl = try List.assoc tag_true  hl with Not_found -> [] in

      let el = try List.assoc tag_false hl with Not_found -> [] in

      let tl_init, tl_step = extract tl in

      let el_init, el_step = extract el in

	MBranch(g, [tag_true, tl_init; tag_false, el_init]),

	MBranch(g, [tag_true, el_init; tag_false, el_step])

      else (* enum type case *)

	assert false

  in

  List.fold_right 

    (fun i (init, step) -> let i_i, i_s = f i in i_i::init, i_s::step) 

    instrs

    ([], [])

let rec filter_bool_assigns instrs =

  let filter_instr instr res =

    match instr with

      | MReset i -> assert false (* no reset allowed *)

      | MLocalAssign (i,v) when not (Types.is_real_type i.var_type) -> res

      | MLocalAssign _ 

      | MStateAssign _ -> instr::res

      | MStep _ -> instr::res      

      | MBranch (g,hl) -> MBranch(g, List.map (fun (t,il) -> t, filter_bool_assigns il) hl)::res

  in

  List.fold_right filter_instr instrs []

let pp_randomized_input fmt v = 

  Format.fprintf fmt "%s = rand(-1, 1);" v.var_id

let translate fmt basename normalized_prog machines =

  (* No modular compilation: require a main node *)

  let main_node =

    match !Options.main_node with

    | "" ->  failwith "Main node required for riny backend" 

    | main_node -> (

      match Machine_code.get_machine_opt main_node machines with

      | None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; assert false

      | Some m -> m

    )

  in

  (* Verify that we have only real variables (no bool nor int) *)

  check_type_restrictions main_node;

  (* Project instrs to init and step versions *)

  let init, step = extract_init_step main_node main_node.mstep.step_instrs in

  let init = Optimize_machine.instrs_fusion init in

  let step = Optimize_machine.instrs_fusion step in

  (* Removing bool assigns that remain from _arrow *)

  let init = filter_bool_assigns init in

  let step = filter_bool_assigns step in

  (* Print the step instructions with all arrows to true *)

  Format.fprintf fmt "@[<v 0>%a@ @[<v 2>while (0. < 1.) {@ %a@ %a@]@ }@ @]@."

    (* Printing first loop body *)

    (Utils.fprintf_list ~sep:"@ "

       (pp_machine_instr main_node main_node.mname.node_id))

    init

    (* Randomized inputs *)

    (Utils.fprintf_list ~sep:"@ "

       pp_randomized_input)

       main_node.mstep.step_inputs

    (* Loop body *)

    (Utils.fprintf_list ~sep:"@ "

       (pp_machine_instr main_node main_node.mname.node_id))

    step;

  (* Print only the main node (should have been inlined) *)

  (* Each input is declared as a in = rand(min, max); *)

  ()

(* Local Variables: *)

(* compile-command:"make -C ../../.." *)

(* End: *)