1

open Lustrec

2

open Lustrec.Lustre_types

3

open Lustrec.Utils

4

open Seal_utils

5


6

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

7

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

8

(* their COI (cone of influence) *)

9

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

10


11

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

12

let is_variable nd vid =

13

List.exists

14

(fun v > v.var_id = vid)

15

nd.node_locals

16


17

let find_variable nd vid =

18

List.find

19

(fun v > v.var_id = vid)

20

nd.node_locals

21


22

(* Returns the vars required to compute v.

23

Memories are specifically identified. *)

24

let coi_var deps nd v =

25

let vname = v.var_id in

26

let sliced_deps =

27

Causality.slice_graph deps vname

28

in

29

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

30

* Printers.pp_var v

31

* Causality.pp_dep_graph sliced_deps; *)

32

let vset, memset =

33

IdentDepGraph.fold_vertex

34

(fun vname (vset,memset) >

35

if Causality.ExprDep.is_read_var vname

36

then

37

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

38

if is_variable nd vname' then

39

ISet.add vname' vset,

40

ISet.add vname' memset

41

else

42

vset, memset

43

else

44

ISet.add vname vset, memset

45

)

46

sliced_deps

47

(ISet.singleton vname, ISet.empty)

48

in

49

report ~level:3

50

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

51

v.var_id

52

(fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements vset)

53

(fprintf_list ~sep:"," Format.pp_print_string) (ISet.elements memset)

54

) ;

55

vset, memset

56


57


58

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

59

to be computed *)

60

let rec coi_vars deps nd vl seen =

61

let coi_vars = coi_vars deps nd in

62

List.fold_left

63

(fun accu v >

64

let vset, memset = coi_var deps nd v in

65

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

66

let memset =

67

ISet.filter (

68

fun vid >

69

not

70

(List.exists

71

(fun v > v.var_id = vid)

72

vl

73

)

74

) memset

75

in

76

let memset_vars =

77

ISet.fold (

78

fun vid accu >

79

(find_variable nd vid)::accu

80

) memset []

81

in

82

let vset' =

83

coi_vars memset_vars (vl@seen)

84

in

85

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

86

)

87

ISet.empty

88

(List.filter

89

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

90

vl

91

)

92


93


94

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

95

let compute_sliced_vars vars_to_keep deps nd =

96

ISet.elements (coi_vars deps nd vars_to_keep [])

97


98


99


100


101


102

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

103

Otherwise outputs are replaced by vars_to_keep *)

104

let slice_node vars_to_keep msch nd =

105

let coi_vars =

106

compute_sliced_vars vars_to_keep msch.Scheduling_type.dep_graph nd

107

in

108

report ~level:3 (fun fmt > Format.fprintf fmt

109

"COI Vars: %a@."

110

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

111

coi_vars);

112

let outputs =

113

List.filter

114

(

115

fun v > List.mem v.var_id coi_vars

116

) nd.node_outputs

117

in

118

let outputs = match outputs with

119

[] > (

120

report ~level:2 (fun fmt > Format.fprintf fmt "No visible output variable, subtituting with provided vars@ ");

121

vars_to_keep

122

)

123

 l > l

124

in

125

let locals =

126

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

127

in

128


129

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

130


131

(* Split tuples while sorting eqs *)

132

let eqs, auts = Corelang.get_node_eqs nd in

133

assert (auts = []); (* Automata should be expanded by now *)

134

let sorted_eqs, unused = Scheduling.sort_equations_from_schedule

135

eqs

136

msch.Scheduling_type.schedule

137

in

138

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

139

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

140


141

let stmts =

142

List.filter (

143

fun (* stmt >

144

* match stmt with

145

*  Aut _ > assert false

146

*  Eq *) eq > (

147

match eq.eq_lhs with

148

[vid] > List.mem vid coi_vars

149

 _ > Format.eprintf "Faulty statement: %a@.@?" Printers.pp_node_eq eq; assert false

150

(* should not happen after inlining and normalization *)

151

)

152

) sorted_eqs

153

in

154

{ nd

155

with

156

node_outputs = outputs;

157

node_locals = locals;

158

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

159

}
