1

open LustreSpec

2


3

let check_input nd value =

4

Format.eprintf "lin check input@.";

5

if not (value.eexpr_quantifiers = []) then (

6

Log.report ~level:1

7

(fun fmt > Format.fprintf fmt "Invalid linearization command for node %s. No quantifiers allowed!@." nd.node_id );

8

false

9


10

) else

11

let value_type =

12

match (Types.repr value.eexpr_type).Types.tdesc with

13

 Types.Ttuple tl > Types.Ttuple (List.map Types.dynamic_type tl)

14

 t > t

15

in

16

let vardecl_types = Types.Ttuple(List.map (fun v > Types.repr v.var_type) nd.node_inputs) in

17

if not (value_type = vardecl_types) then (

18

Log.report ~level:1

19

(fun fmt > Format.fprintf fmt "Invalid linearization command for node %s: expecting type %a, got type %a@." nd.node_id

20

Types.print_ty (Types.new_ty vardecl_types)

21

Types.print_ty (Types.repr value.eexpr_type)

22

);

23

false

24

)

25

else

26

true

27


28

(* Eliminate variables. It will change the order of the statements. Do not touch automaton *)

29


30


31

let rec elim_vars vars stmts =

32

Format.eprintf "lin elim var@.";

33


34

(* Removing memories (lhs = Pre _ or Fby _) *)

35

let memory_vars, non_memory_vars = List.partition (fun vid >

36

let v_def = List.find (fun stm > match stm with Eq e > e.eq_lhs = [vid]  _ > false) stmts in

37

match v_def with

38

Eq eq > (match eq.eq_rhs.expr_desc with

39

Expr_pre _  Expr_fby _ > true

40

 _ > false

41

)

42

 _ > false

43

) vars

44

in

45


46

(* we partition this level stmts. Local Automata are left untouched and

47

are addressed separately *)

48

let local_defs, mem_defs, aut_defs = List.fold_left

49

(fun (ll,el,al) def > (

50

match def with

51

 Aut a > (ll, el, a::al) (* we do not handle automaton now. Will be down later *)

52

 Eq eq > (

53

match eq.eq_lhs with

54

 [v] > if List.mem v non_memory_vars then

55

eq::ll, el, al

56

else

57

ll, eq::el, al

58

 _ > raise (Failure "elim eq failed, unnormalized equation"))

59

)) ([], [], []) stmts

60

in

61

Format.eprintf "lin local ok@.";

62

let mem_defs' =

63

(* let local_defs, _ = (\* local defs have to be normalized to avoid loops (fixpoints) in unrolling *\) *)

64

(* List.fold_left (fun (accu, vl) def > *)

65

(* (\* we clean def wrt accu *\) *)

66

(* Format.eprintf "lin cleaning local %a@." Printers.pp_node_eq def; *)

67

(* let def_e = Corelang.substitute_expr vl accu def.eq_rhs in *)

68

(* Format.eprintf "lin obtaining %a@." Printers.pp_expr def_e; *)

69

(* {def with eq_rhs = def_e}::accu, def.eq_lhs @ vl *)

70

(* ) ([],[]) local_defs *)

71

(* in *)

72

List.map (fun e >

73

Format.eprintf "lin cleaning %a@." Printers.pp_expr e.eq_rhs;

74

let res = {e with eq_rhs = Corelang.substitute_expr ~open_pre:true non_memory_vars local_defs e.eq_rhs } in

75

Format.eprintf "lin cleaned %a@." Printers.pp_expr res.eq_rhs;

76

Eq res

77

) mem_defs in

78

Format.eprintf "lin main def ok@.";

79

let aut_defs' = List.map (fun a > Aut {a with aut_handlers = List.map elim_handler a.aut_handlers}) aut_defs in

80

Format.eprintf "lin aut def ok@.";

81

mem_defs'@aut_defs', memory_vars

82


83

and elim_handler h =

84

Format.eprintf "lin elim handler@.";

85

let stmts, mem_vid = elim_vars (List.map (fun v > v.var_id) h.hand_locals) h.hand_stmts in

86

{ h with

87

hand_locals = (List.filter (fun v > List.mem v.var_id mem_vid) h.hand_locals);

88

hand_stmts = stmts }

89


90


91


92


93


94

(* This function returns a modified node.

95

TODO make sure there is no function call in the node (or nothing with a lhs of length > 1

96

*)

97

let node nd value =

98

(* We check that value is a tuple compatible with the input arguments of the node *)

99

Format.eprintf "lin node@.";

100

if not (check_input nd value) then

101

nd (* not applicable *)

102

else (

103

Log.report ~level:1

104

(fun fmt > Format.fprintf fmt "Linearizing node %s around point %a@."

105

nd.node_id

106

Printers.pp_eexpr value

107

);

108

(* Node is simplified. No more local non memory variables *)

109

let unrolled_stmts, mem_vid =

110

elim_vars (List.map (fun v > v.var_id) nd.node_locals) nd.node_stmts

111

in

112

(* Each expression is expressed as (expr > Pre expr) ie. normalized wrt pre *)

113

let stmts = unrolled_stmts in

114

{ nd with

115

node_locals = (List.filter (fun v > List.mem v.var_id mem_vid) nd.node_locals);

116

node_stmts = stmts

117

}

118

)

119


120

(* Local Variables: *)

121

(* compilecommand:"make C .." *)

122

(* End: *)

123

