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.value_type) vl,

35

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

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 rec 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

 Types.Ttuple l, _ > assert (List.length l = 1); check_type_equal (List.hd l) t2

52

 _, Types.Ttuple l > assert (List.length l = 1); check_type_equal t1 (List.hd l)

53

 Types.Tstatic (_, t), _ > check_type_equal t t2

54

 _, Types.Tstatic (_, t) > check_type_equal t1 t

55

 _ > eprintf "ERROR: %a  %a" pp_type t1 pp_type t2; assert false (* TODO *)

56


57

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

58

first type can be polymorphic.

59

@param subsitution the base substitution

60

@param type_poly the type which can be polymorphic

61

@param typ the type to match type_poly with

62

**)

63

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

64

assert(not (is_Tunivar typ));

65

(* If type_poly is polymorphic *)

66

if is_Tunivar type_poly then

67

(* If a subsitution exists for it *)

68

if List.mem_assoc type_poly.tid substituion then

69

begin

70

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

71

match typ *)

72

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

73

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

74

substituion

75

end

76

(* If type_poly is not in the subsitution *)

77

else

78

(* We add it to the substituion *)

79

(type_poly.tid, typ)::substituion

80

(* iftype_poly is not polymorphic *)

81

else

82

begin

83

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

84

assert(check_type_equal type_poly typ);

85

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

86

substituion

87

end

88


89

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

90

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

91

@param calls a list of pair of list of types

92

@param return true if the two pairs are equal

93

**)

94

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

95

(List.for_all2 check_type_equal i1 i2)

96

&& (List.for_all2 check_type_equal i1 i2)

97


98

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

99

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

100

@param call a pair of list of types

101

@param calls a list of pair of list of types

102

@param return true if all the elements are equal

103

**)

104

let check_calls call calls =

105

List.for_all (check_call_equal call) calls

106


107

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

108

of all its polymorphic type instanciation for a given machine.

109

@param machine the machine which instantiate the subinstance

110

@param submachine the machine corresponding to the subinstance

111

@return the correspondance between polymorphic type id and their instantiation

112

**)

113

let get_substitution machine ident submachine =

114

eprintf "%s %s %s@." machine.mname.node_id ident submachine.mname.node_id;

115

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

116

let calls = find_submachine_step_call ident machine.mstep.step_instrs in

117

(* extract the first call *)

118

let call = match calls with

119

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

120

 [] > assert(false)

121

 h::t > h in

122

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

123

assert(check_calls call calls);

124

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

125

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

126

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

127

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

128

(* keep only the type of vars *)

129

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

130

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

131

and the call *)

132

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

133

(* Unify the two lists of types *)

134

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

135

(* Assume that our substitution match all the possible

136

polymorphic type of the node *)

137

let polymorphic_types = find_all_polymorphic_type submachine in

138

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

139

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

140

substitution

141


142

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

143

@param machine the machine

144

@param fmt the formater to print on

145

@param substitution correspondance between polymorphic type id and their instantiation

146

@param ident the identifier of the subinstance

147

@param submachine the submachine of the subinstance

148

**)

149

let pp_machine_subinstance_state_decl fmt (substitution, ident, submachine) =

150

pp_node_state_decl substitution ident fmt submachine

151


152

(** Print the state record for a machine.

153

@param fmt the formater to print on

154

@param var_list list of all state var

155

@param typed_submachines list of pairs of instantiated types and machine

156

**)

157

let pp_state_record_definition fmt (var_list, typed_submachines) =

158

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

159

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

160

typed_submachines

161

(Utils.pp_final_char_if_non_empty ";@," typed_submachines)

162

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

163

var_list

164

(Utils.pp_final_char_if_non_empty ";" var_list)

165


166

(** Print the declaration for polymorphic types.

167

@param fmt the formater to print on

168

@param polymorphic_types all the types to print

169

**)

170

let pp_generic fmt polymorphic_types =

171

let pp_polymorphic_types =

172

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

173

if polymorphic_types != [] then

174

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

175

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

176

pp_polymorphic_types

177

else

178

fprintf fmt ""

179


180

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

181

@param machines list of all machines

182

@param instance instance of a machine

183

@return the machine corresponding to hte given instance

184

**)

185

let get_machine machines instance =

186

let id = (extract_node instance).node_id in

187

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

188


189

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

190

@param fmt the formater to print on

191

@param id id of the polymorphic type

192

@param typ the new type

193

**)

194

let pp_generic_instanciation fmt (id, typ) =

195

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

196


197

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

198

@param fmt the formater to print on

199

@param substitutions the instanciation substitution

200

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

201

@param submachine the submachine to instanciate

202

**)

203

let pp_new_package fmt (substitutions, ident, submachine)=

204

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

205

(pp_package_name_with_polymorphic substitutions) submachine

206

pp_package_name submachine

207

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

208


209


210

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

211

@param fmt the formater to print on

212

@param m the machine

213

**)

214

let pp_file machines fmt m =

215

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

216

let names = List.map fst m.minstances in

217

let var_list = m.mmemory in

218

let typed_submachines = List.map2

219

(fun instance submachine >

220

let ident = (fst instance) in

221

get_substitution m ident submachine, ident, submachine)

222

m.minstances submachines in

223

let pp_record fmt =

224

pp_state_record_definition fmt (var_list, typed_submachines) in

225

let typed_submachines_filtered =

226

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

227

let polymorphic_types = find_all_polymorphic_type m in

228

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

229


230

(* Include all the subinstance*)

231

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

232

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

233


234

pp_generic polymorphic_types

235


236

(*Begin the package*)

237

(pp_begin_package false) m

238


239

(*Declare the state type*)

240

pp_private_limited_type_decl pp_state_type

241


242

(*Declare the reset procedure*)

243

(pp_reset_prototype m)

244


245

(*Declare the step procedure*)

246

(pp_step_prototype m)

247


248

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

249

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

250

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

251


252

(*Define the state type*)

253

pp_type_decl (pp_state_type, pp_record)

254


255

(*End the package*)

256

pp_end_package m

257


258

end
