CristalCaveGem » LustreC

open Format

open Corelang

open Machine_code

let pp_fun i = 

  match i with

  | "ite" -> "ite"

  | "uminus" -> "uminus"

  | "not" -> "not"

  | "=" -> "equal"

  | "&&" -> "and"

  | "||" -> "or"

  | "impl" -> "impl"

  | "xor" -> "xor"

  | "!=" -> "different"

  | "mod" -> "mod"

  | ">" -> "gt"

  | "<" -> "lt"

  | ">=" -> "gte"

  | "<=" -> "lte"

  | _ -> Printf.printf "%s\n" i;assert false

let rec print_instr_dep instances name fmt instr =

  match instr with 

  | MReset i -> ()

  | MLocalAssign (i,v) -> ()

  | MStateAssign (i,v) -> ()

  | MStep (il, i, vl) ->

      let name' = try node_name (fst (List.assoc i instances)) with Not_found -> pp_fun i in

      Format.fprintf fmt "  %s -> %s;" name name'

  | MBranch (g,hl) -> ()

let print_machine_dep fmt m =

  Format.fprintf fmt "%s [color=red];@.%a"

    m.mname.node_id

    (Utils.fprintf_list ~sep:"@." (print_instr_dep m.minstances m.mname.node_id)) m.mstep.step_instrs

(*

let rec print_instr_struct instances name fmt instr =

  match instr with 

  | MReset i -> ()

  | MLocalAssign (i,v) -> ()

  | MStateAssign (i,v) -> ()

  | MStep (il, i, vl) ->

      let name' = try node_name (fst (List.assoc i instances)) with Not_found -> pp_fun i in

      Format.fprintf fmt "  %s -> %s;@." name name'

  | MBranch (g,hl) -> ()

let rec translate_expr vars ((m, si, j, d, s) as args) expr =

 match expr.expr_desc with

 | Expr_const v                     -> Cst v

 | Expr_ident x                     -> translate_ident vars args x

 | Expr_array el                    -> Array (List.map (translate_expr vars args) el)

 | Expr_access (t, i)               -> Access (translate_expr vars args t, translate_expr vars args (expr_of_dimension i))

 | Expr_power  (e, n)               -> Power  (translate_expr vars args e, translate_expr vars args (expr_of_dimension n))

 | Expr_tuple _

 | Expr_arrow _ 

 | Expr_fby _

 | Expr_pre _                       -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)

 | Expr_when    (e1, _, _)          -> translate_expr vars args e1

 | Expr_merge   (x, _)              -> raise NormalizationError

 | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->

   let nd = node_from_name id in

   (match e.expr_desc with

   | Expr_tuple el -> Fun (node_name nd, List.map (translate_expr vars args) el)

   | _             -> Fun (node_name nd, [translate_expr vars args e]))

 | Expr_ite (g,t,e) -> (

   (* special treatment depending on the active backend. For horn backend or

      acsl spec, ite are preserved in expression. While they are removed for C

      or Java backends. *)

     Fun ("ite", [translate_expr vars args g; translate_expr vars args t; translate_expr vars args e])

 )

 | _                   -> raise NormalizationError

  let nd = match top.top_decl_desc with Node nd -> nd | _ -> assert false in

List.map (fun d -> d.Dimension.dim_loc, translate_expr (node_vars nd) init_args (expr_of_dimension d)) nd.node_checks;

*)

let print_machine_struct orig dest fmt m =

  Format.fprintf fmt "subgraph cluster_%s {@.label = \"%s\"@.}@." m.mname.node_id m.mname.node_id

(*

digraph G {

	subgraph cluster_0 {

		style=filled;

		color=lightgrey;

		node [style=filled,color=white];

		a0 -> a1 -> a2 -> a3;

		label = "process #1";

	}

	subgraph cluster_1 {

		node [style=filled];

		b0 -> b1 -> b2 -> b3;

		label = "process #2";

		color=blue

	}

	start -> a0;

	start -> b0;

	a1 -> b3;

	b2 -> a3;

	a3 -> a0;

	a3 -> end;

	b3 -> end;

	start [shape=Mdiamond];

	end [shape=Msquare];

}

*)

let translate_to_dep destname basename prog machines =

	  let source_file = destname ^ "_dep.dot" in

	  let source_out = open_out source_file in

	  let fmt = formatter_of_out_channel source_out in

    Format.fprintf fmt "digraph %s {@.%a}@." basename (Utils.fprintf_list ~sep:"@." print_machine_dep) machines

let translate_to_struct destname basename prog machines = () (*

	  let source_file = destname ^ "_struct.dot" in

	  let source_out = open_out source_file in

	  let fmt = formatter_of_out_channel source_out in

    Format.fprintf fmt "digraph %s {@.%a}@." basename (Utils.fprintf_list ~sep:"" (print_machine_struct "input" "output")) (get_nodes prog)*)

let translate destname basename prog machines =

    translate_to_dep destname basename prog machines;

    translate_to_struct destname basename prog machines

(* Local Variables: *)

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

(* End: *)