CristalCaveGem » LustreC

module IdentDepGraph = Graph.Imperative.Digraph.ConcreteBidirectional (IdentModule)

(* Dependency of mem variables on mem variables is cut off 

   by duplication of some mem vars into local node vars.

   Thus, cylic dependency errors may only arise between no-mem vars.

no_mem' = combinational(no_mem, mem);

=> (mem -> no_mem' -> no_mem)

module ExprDep = struct

let instance_var_cpt = ref 0

let mk_instance_var id =

 incr instance_var_cpt; sprintf "!%s_%d" id !instance_var_cpt

let is_instance_var v = v.[0] = '!'

let eq_memory_variables mems eq =

  let rec match_mem lhs rhs mems =

    | Expr_pre _    -> List.fold_right ISet.add lhs mems

    | Expr_tuple tl -> 

      let lhs' = (transpose_list [lhs]) in

      List.fold_right2 match_mem lhs' tl mems

    | _             -> mems in

  match_mem eq.eq_lhs eq.eq_rhs mems

let node_memory_variables nd =

 List.fold_left eq_memory_variables ISet.empty nd.node_eqs

(* computes the equivalence relation relating variables 

   in the same equation lhs, under the form of a table 

(* Add dependencies from lhs to rhs in [g, g'], *)

(* no-mem/no-mem and mem/no-mem in g            *)

(* mem/mem in g'                                *)

  let add_var lhs_is_mem lhs x (g, g') =

    else (g, g') in

(* Add dependencies from [lhs] to rhs clock [ck]. *)

  let rec add_clock lhs_is_mem lhs ck g =

    | Clocks.Ccarrying (_, ck') -> add_clock lhs_is_mem lhs ck' g

    | _                         -> g 

  in

  let rec add_dep lhs_is_mem lhs rhs g =

    (* Add mashup dependencies for a user-defined node instance [lhs] = [f]([e]) *)

    (* i.e every input is connected to every output, through a ghost var *)

    let mashup_appl_dependencies f e g =

    | Expr_access (e1, _)

    | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g

    | Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g

      if List.length t <> List.length lhs then ( 

	match lhs with

	| [l] -> List.fold_right (fun r -> add_dep lhs_is_mem [l] r) t g

	    (List.length t)

	  ;

	  assert false

      else

	List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g

    | Expr_merge (c, hl) -> add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)

    | Expr_ite   (c, t, e) -> add_dep lhs_is_mem lhs c (add_dep lhs_is_mem lhs t (add_dep lhs_is_mem lhs e g))

    | Expr_dclock  (e, _)

    | Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g 

  in

(* Returns the dependence graph for node [n] *)

  instance_var_cpt := 0;

  let g = new_graph (), new_graph () in

  (* Basic dependencies *)

  g

end

  let break_cycle head cp_head g =

    let succs = IdentDepGraph.succ g head in

    IdentDepGraph.add_edge g head cp_head;

    List.iter

      (fun s ->

	IdentDepGraph.remove_edge g head s;

let global_dependency node =

  let mems = ExprDep.node_memory_variables node in

  (*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems;

  Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*)

  CycleDetection.check_cycles g_non_mems;