1

open Lustre_types

2

open Utils

3

open Seal_utils

4


5

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

6

(* Computing a slice of a node, selecting only some variables, based on *)

7

(* their COI (cone of influence) *)

8

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

9


10

(* Basic functions to search into nodes. Could be moved to corelang eventually *)

11

let is_variable nd vid = List.exists (fun v > v.var_id = vid) nd.node_locals

12


13

let find_variable nd vid = List.find (fun v > v.var_id = vid) nd.node_locals

14


15

(* Returns the vars required to compute v. Memories are specifically identified. *)

16

let coi_var deps nd v =

17

let vname = v.var_id in

18

let sliced_deps = Causality.slice_graph deps vname in

19

(* Format.eprintf "sliced graph for %a: %a@."

20

* Printers.pp_var v

21

* Causality.pp_dep_graph sliced_deps; *)

22

let vset, memset =

23

IdentDepGraph.fold_vertex

24

(fun vname (vset, memset) >

25

if Causality.ExprDep.is_read_var vname then

26

let vname' = String.sub vname 1 (1 + String.length vname) in

27

if is_variable nd vname' then

28

ISet.add vname' vset, ISet.add vname' memset

29

else vset, memset

30

else ISet.add vname vset, memset)

31

sliced_deps

32

(ISet.singleton vname, ISet.empty)

33

in

34

report ~level:3 (fun fmt >

35

Format.fprintf fmt "COI of var %s: (%a // %a)@." v.var_id

36

(fprintf_list ~sep:"," Format.pp_print_string)

37

(ISet.elements vset)

38

(fprintf_list ~sep:"," Format.pp_print_string)

39

(ISet.elements memset));

40

vset, memset

41


42

(* Computes the variables required to compute vl. Variables /seen/ do not need

43

to be computed *)

44

let rec coi_vars deps nd vl seen =

45

let coi_vars = coi_vars deps nd in

46

List.fold_left

47

(fun accu v >

48

let vset, memset = coi_var deps nd v in

49

(* We handle the new mems discovered in the coi *)

50

let memset =

51

ISet.filter

52

(fun vid > not (List.exists (fun v > v.var_id = vid) vl))

53

memset

54

in

55

let memset_vars =

56

ISet.fold (fun vid accu > find_variable nd vid :: accu) memset []

57

in

58

let vset' = coi_vars memset_vars (vl @ seen) in

59

ISet.union accu (ISet.union vset vset'))

60

ISet.empty

61

(List.filter (fun v > not (List.mem v seen)) vl)

62


63

(* compute the coi of vars_to_keeps in node nd *)

64

let compute_sliced_vars vars_to_keep deps nd =

65

ISet.elements (coi_vars deps nd vars_to_keep [])

66


67

(* If existing outputs are included in vars_to_keep, just slice the content.

68

Otherwise outputs are replaced by vars_to_keep *)

69

let slice_node vars_to_keep msch nd =

70

let coi_vars =

71

compute_sliced_vars vars_to_keep msch.Scheduling_type.dep_graph nd

72

in

73

report ~level:3 (fun fmt >

74

Format.fprintf fmt "COI Vars: %a@."

75

(Utils.fprintf_list ~sep:"," Format.pp_print_string)

76

coi_vars);

77

let outputs =

78

List.filter (fun v > List.mem v.var_id coi_vars) nd.node_outputs

79

in

80

let outputs =

81

match outputs with

82

 [] >

83

report ~level:2 (fun fmt >

84

Format.fprintf fmt

85

"No visible output variable, subtituting with provided vars@ ");

86

vars_to_keep

87

 l >

88

l

89

in

90

let locals =

91

List.filter (fun v > List.mem v.var_id coi_vars) nd.node_locals

92

in

93


94

report ~level:3 (fun fmt > Format.fprintf fmt "Scheduling node@.");

95


96

(* Split tuples while sorting eqs *)

97

let eqs, auts = Corelang.get_node_eqs nd in

98

assert (auts = []);

99

(* Automata should be expanded by now *)

100

let sorted_eqs, unused =

101

Scheduling.sort_equations_from_schedule eqs msch.Scheduling_type.schedule

102

in

103

let locals = List.filter (fun v > not (List.mem v.var_id unused)) locals in

104

report ~level:3 (fun fmt > Format.fprintf fmt "Scheduled node@.");

105


106

let stmts =

107

List.filter

108

(fun (* stmt > * match stmt with *  Aut _ > assert false *  Eq *)

109

eq >

110

match eq.eq_lhs with

111

 [ vid ] >

112

List.mem vid coi_vars

113

 _ >

114

Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq;

115

assert false

116

(* should not happen after inlining and normalization *))

117

sorted_eqs

118

in

119

{

120

nd with

121

node_outputs = outputs;

122

node_locals = locals;

123

node_stmts = List.map (fun e > Eq e) stmts;

124

}
