1

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

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT  ISAESUPAERO *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

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

11


12

open Format

13


14

open Machine_code_types

15

open Lustre_types

16

open Corelang

17

open Machine_code_common

18


19

open Ada_backend_common

20


21

(** Functions printing the .ads file **)

22

module Main =

23

struct

24


25

(** Find a submachine step call in a list of instructions.

26

@param ident submachine instance ident

27

@param instr_list List of instruction sto search

28

@return a list of pair containing input types and output types for each step call found

29

**)

30

let rec find_submachine_step_call ident instr_list =

31

let search_instr instruction =

32

match instruction.instr_desc with

33

 MStep (il, i, vl) when String.equal i ident > [

34

(List.map (function x> x.var_type) il,

35

List.map (function x> x.value_type) vl)]

36

 MBranch (_, l) > List.flatten

37

(List.map (function x, y > find_submachine_step_call ident y) l)

38

 _ > []

39

in

40

List.flatten (List.map search_instr instr_list)

41


42

(** Check that two types are the same.

43

@param t1 a type

44

@param t2 an other type

45

@param return true if the two types are Tbasic or Tunivar and equal

46

**)

47

let check_type_equal (t1:Types.type_expr) (t2:Types.type_expr) =

48

match (Types.repr t1).Types.tdesc, (Types.repr t2).Types.tdesc with

49

 Types.Tbasic x, Types.Tbasic y > x = y

50

 Types.Tunivar, Types.Tunivar > t1.tid = t2.tid

51

 _ > assert false (* TODO *)

52


53

(** Extend a substitution to unify the two given types. Only the

54

first type can be polymorphic.

55

@param subsitution the base substitution

56

@param type_poly the type which can be polymorphic

57

@param typ the type to match type_poly with

58

**)

59

let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_expr), (typ:Types.type_expr)) =

60

assert(not (is_Tunivar typ));

61

(* If type_poly is polymorphic *)

62

if is_Tunivar type_poly then

63

(* If a subsitution exists for it *)

64

if List.mem_assoc type_poly.tid substituion then

65

begin

66

(* We check that the type corresponding to type_poly in the subsitution

67

match typ *)

68

assert(check_type_equal (List.assoc type_poly.tid substituion) typ);

69

(* We return the original substituion, it is already correct *)

70

substituion

71

end

72

(* If type_poly is not in the subsitution *)

73

else

74

(* We add it to the substituion *)

75

(type_poly.tid, typ)::substituion

76

(* iftype_poly is not polymorphic *)

77

else

78

begin

79

(* We check that type_poly and typ are the same *)

80

assert(check_type_equal type_poly typ);

81

(* We return the original substituion, it is already correct *)

82

substituion

83

end

84


85

(** Check that two calls are equal. A call is

86

a pair of list of types, the inputs and the outputs.

87

@param calls a list of pair of list of types

88

@param return true if the two pairs are equal

89

**)

90

let check_call_equal (i1, o1) (i2, o2) =

91

(List.for_all2 check_type_equal i1 i2)

92

&& (List.for_all2 check_type_equal i1 i2)

93


94

(** Check that all the elements of list of calls are equal to one.

95

A call is a pair of list of types, the inputs and the outputs.

96

@param call a pair of list of types

97

@param calls a list of pair of list of types

98

@param return true if all the elements are equal

99

**)

100

let check_calls call calls =

101

List.for_all (check_call_equal call) calls

102


103

(** Extract from a subinstance that can have polymorphic type the instantiation

104

of all its polymorphic type instanciation for a given machine.

105

@param machine the machine which instantiate the subinstance

106

@param submachine the machine corresponding to the subinstance

107

@return the correspondance between polymorphic type id and their instantiation

108

**)

109

let get_substitution machine ident submachine =

110

(* extract the calls to submachines from the machine *)

111

let calls = find_submachine_step_call ident machine.mstep.step_instrs in

112

(* extract the first call *)

113

let call = match calls with

114

(* assume that there is always one call to a subinstance *)

115

 [] > assert(false)

116

 h::t > h in

117

(* assume that all the calls to a subinstance are using the same type *)

118

assert(check_calls call calls);

119

(* make a list of all types from input and output vars *)

120

let call_types = (fst call)@(snd call) in

121

(* extract all the input and output vars from the submachine *)

122

let machine_vars = submachine.mstep.step_inputs@submachine.mstep.step_outputs in

123

(* keep only the type of vars *)

124

let machine_types = List.map (function x> x.var_type) machine_vars in

125

(* assume that there is the same numer of input and output in the submachine

126

and the call *)

127

assert (List.length machine_types = List.length call_types);

128

(* Unify the two lists of types *)

129

let substituion = List.fold_left unification [] (List.combine machine_types call_types) in

130

(* Assume that our substitution match all the possible

131

polymorphic type of the node *)

132

let polymorphic_types = find_all_polymorphic_type submachine in

133

assert (List.length polymorphic_types = List.length substituion);

134

assert (List.for_all (function x>List.mem_assoc x substituion) polymorphic_types);

135

substituion

136


137

(** Print the declaration of a state element of a subinstance of a machine.

138

@param machine the machine

139

@param fmt the formater to print on

140

@param substitution correspondance between polymorphic type id and their instantiation

141

@param ident the identifier of the subinstance

142

@param submachine the submachine of the subinstance

143

**)

144

let pp_machine_subinstance_state_decl fmt (substitution, ident, submachine) =

145

pp_node_state_decl substitution ident fmt submachine

146


147

(** Print the state record for a machine.

148

@param fmt the formater to print on

149

@param var_list list of all state var

150

@param typed_submachines list of pairs of instantiated types and machine

151

**)

152

let pp_state_record_definition fmt (var_list, typed_submachines) =

153

fprintf fmt "@, @[<v>record@, @[<v>%a%t%a%t@]@,end record@]"

154

(Utils.fprintf_list ~sep:";@;" pp_machine_subinstance_state_decl)

155

typed_submachines

156

(Utils.pp_final_char_if_non_empty ";@," typed_submachines)

157

(Utils.fprintf_list ~sep:";@;" (pp_machine_var_decl NoMode))

158

var_list

159

(Utils.pp_final_char_if_non_empty ";" var_list)

160


161

(** Print the declaration for polymorphic types.

162

@param fmt the formater to print on

163

@param polymorphic_types all the types to print

164

**)

165

let pp_generic fmt polymorphic_types =

166

let pp_polymorphic_types =

167

List.map (fun id fmt > pp_polymorphic_type fmt id) polymorphic_types in

168

if polymorphic_types != [] then

169

fprintf fmt "generic@, @[<v>%a;@]@,"

170

(Utils.fprintf_list ~sep:";@," pp_private_limited_type_decl)

171

pp_polymorphic_types

172

else

173

fprintf fmt ""

174


175

(** Extract from a machine list the one corresponding to the given instance.

176

@param machines list of all machines

177

@param instance instance of a machine

178

@return the machine corresponding to hte given instance

179

**)

180

let get_machine machines instance =

181

let id = (extract_node instance).node_id in

182

List.find (function m > m.mname.node_id=id) machines

183


184

(** Print instanciation of a generic type in a new statement.

185

@param fmt the formater to print on

186

@param id id of the polymorphic type

187

@param typ the new type

188

**)

189

let pp_generic_instanciation fmt (id, typ) =

190

fprintf fmt "%a => %a" pp_polymorphic_type id pp_type typ

191


192

(** Print a new statement instantiating a generic package.

193

@param fmt the formater to print on

194

@param substitutions the instanciation substitution

195

@param ident the name of the instance, useless in this function

196

@param submachine the submachine to instanciate

197

**)

198

let pp_new_package fmt (substitutions, ident, submachine)=

199

fprintf fmt "package %a is new %a @[<v>(%a)@]"

200

(pp_package_name_with_polymorphic substitutions) submachine

201

pp_package_name submachine

202

(Utils.fprintf_list ~sep:",@," pp_generic_instanciation) substitutions

203


204


205

(** Print the package declaration(ads) of a machine.

206

@param fmt the formater to print on

207

@param m the machine

208

**)

209

let pp_file machines fmt m =

210

let submachines = List.map (get_machine machines) m.minstances in

211

let names = List.map fst m.minstances in

212

let var_list = m.mmemory in

213

let typed_submachines = List.map2

214

(fun instance submachine >

215

let ident = (fst instance) in

216

get_substitution m ident submachine, ident, submachine)

217

m.minstances submachines in

218

let pp_record fmt =

219

pp_state_record_definition fmt (var_list, typed_submachines) in

220

let typed_submachines_filtered =

221

List.filter (function (l, _, _) > l != []) typed_submachines in

222

let polymorphic_types = find_all_polymorphic_type m in

223

fprintf fmt "@[<v>%a%t%a%a@, @[<v>@,%a;@,@,%t;@,@,%t;@,@,private@,@,%a%t%a;@,@]@,%a;@.@]"

224


225

(* Include all the subinstance*)

226

(Utils.fprintf_list ~sep:";@," pp_with_machine) submachines

227

(Utils.pp_final_char_if_non_empty ";@,@," submachines)

228


229

pp_generic polymorphic_types

230


231

(*Begin the package*)

232

(pp_begin_package false) m

233


234

(*Declare the state type*)

235

pp_private_limited_type_decl pp_state_type

236


237

(*Declare the reset procedure*)

238

(pp_reset_prototype m)

239


240

(*Declare the step procedure*)

241

(pp_step_prototype m)

242


243

(*Instantiate the polymorphic type that need to be instantiate*)

244

(Utils.fprintf_list ~sep:";@," pp_new_package) typed_submachines_filtered

245

(Utils.pp_final_char_if_non_empty ";@,@," typed_submachines_filtered)

246


247

(*Define the state type*)

248

pp_type_decl (pp_state_type, pp_record)

249


250

(*End the package*)

251

pp_end_package m

252


253

end
