1


2

open Lustrec.Machine_code_types

3

open Lustrec.Lustre_types

4

open Lustrec.Corelang

5

(*

6

open Lustrec.Machine_code_common

7

*)

8


9

let is_machine_statefull m = not m.mname.node_dec_stateless

10


11

(** Return true if its the arrow machine

12

@param machine the machine to test

13

*)

14

let is_arrow machine = String.equal Lustrec.Arrow.arrow_id machine.mname.node_id

15


16

(** Extract a node from an instance.

17

@param instance the instance

18

**)

19

let extract_node instance =

20

let (_, (node, _)) = instance in

21

match node.top_decl_desc with

22

 Node nd > nd

23

 _ > assert false (*TODO*)

24


25

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

26

assume that the machine is in the list.

27

@param machines list of all machines

28

@param instance instance of a machine

29

@return the machine corresponding to hte given instance

30

**)

31

let get_machine machines instance =

32

let id = (extract_node instance).node_id in

33

try

34

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

35

with

36

Not_found > assert false (*TODO*)

37


38

(** Extract all the inputs and outputs.

39

@param machine the machine

40

@return a list of all the var_decl of a macine

41

**)

42

let get_all_vars_machine m =

43

m.mmemory@m.mstep.step_inputs@m.mstep.step_outputs@m.mstatic

44


45

(** Check if a type is polymorphic.

46

@param typ the type

47

@return true if its polymorphic

48

**)

49

let is_Tunivar typ = (Lustrec.Types.repr typ).tdesc == Lustrec.Types.Tunivar

50


51

(** Find all polymorphic type : Lustrec.Types.Tunivar in a machine.

52

@param machine the machine

53

@return a list of id corresponding to polymorphic type

54

**)

55

let find_all_polymorphic_type m =

56

let vars = get_all_vars_machine m in

57

let extract id = id.var_type.tid in

58

let polymorphic_type_vars =

59

List.filter (function x> is_Tunivar x.var_type) vars in

60

List.sort_uniq () (List.map extract polymorphic_type_vars)

61


62


63

(** Check if a submachine is statefull.

64

@param submachine a submachine

65

@return true if the submachine is statefull

66

**)

67

let is_submachine_statefull submachine =

68

not (snd (snd submachine)).mname.node_dec_stateless

69


70

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

71

@param ident submachine instance ident

72

@param instr_list List of instruction sto search

73

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

74

**)

75

let rec find_submachine_step_call ident instr_list =

76

let search_instr instruction =

77

match instruction.instr_desc with

78

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

79

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

80

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

81

 MBranch (_, l) > List.flatten

82

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

83

 _ > []

84

in

85

List.flatten (List.map search_instr instr_list)

86


87

(* Replace this function by check_type_equal but be careful to the fact that

88

this function chck equality and that it is both basic type.

89

This might be a required feature when it used *)

90

(** Test if two types are the same.

91

@param typ1 the first type

92

@param typ2 the second type

93

**)

94

let pp_eq_type typ1 typ2 =

95

let get_basic typ = match (Lustrec.Types.repr typ).Lustrec.Types.tdesc with

96

 Lustrec.Types.Tbasic Lustrec.Types.Basic.Tint > Lustrec.Types.Basic.Tint

97

 Lustrec.Types.Tbasic Lustrec.Types.Basic.Treal > Lustrec.Types.Basic.Treal

98

 Lustrec.Types.Tbasic Lustrec.Types.Basic.Tbool > Lustrec.Types.Basic.Tbool

99

 _ > assert false (*TODO*)

100

in

101

get_basic typ1 = get_basic typ2

102


103

(** Check that two types are the same.

104

@param t1 a type

105

@param t2 an other type

106

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

107

**)

108

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

109

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

110

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

111

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

112

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

113

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

114

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

115

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

116

 _ > assert false

117


118

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

119

first type can be polymorphic.

120

@param subsitution the base substitution

121

@param type_poly the type which can be polymorphic

122

@param typ the type to match type_poly with

123

**)

124

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

125

assert(not (is_Tunivar typ));

126

(* If type_poly is polymorphic *)

127

if is_Tunivar type_poly then

128

(* If a subsitution exists for it *)

129

if List.mem_assoc type_poly.tid substituion then

130

begin

131

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

132

match typ *)

133

(try

134

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

135

with

136

Not_found > assert false);

137

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

138

substituion

139

end

140

(* If type_poly is not in the subsitution *)

141

else

142

(* We add it to the substituion *)

143

(type_poly.tid, typ)::substituion

144

(* iftype_poly is not polymorphic *)

145

else

146

begin

147

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

148

assert(check_type_equal type_poly typ);

149

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

150

substituion

151

end

152


153

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

154

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

155

@param calls a list of pair of list of types

156

@param return true if the two pairs are equal

157

**)

158

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

159

(List.for_all2 check_type_equal i1 i2)

160

&& (List.for_all2 check_type_equal i1 i2)

161


162

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

163

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

164

@param call a pair of list of types

165

@param calls a list of pair of list of types

166

@param return true if all the elements are equal

167

**)

168

let check_calls call calls =

169

List.for_all (check_call_equal call) calls

170


171

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

172

of all its polymorphic type instanciation for a given machine. It searches

173

the step calls and extract a substitution for all polymorphic type from

174

it.

175

@param machine the machine which instantiate the subinstance

176

@param ident the identifier of the instance which permits to find the step call

177

@param submachine the machine corresponding to the subinstance

178

@return the correspondance between polymorphic type id and their instantiation

179

**)

180

let get_substitution machine ident submachine =

181

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

182

let calls = find_submachine_step_call ident machine.mstep.step_instrs in

183

(* extract the first call *)

184

let call = match calls with

185

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

186

 [] > assert(false)

187

 h::t > h in

188

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

189

assert(check_calls call calls);

190

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

191

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

192

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

193

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

194

(* keep only the type of vars *)

195

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

196

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

197

and the call *)

198

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

199

(* Unify the two lists of types *)

200

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

201

(* Assume that our substitution match all the possible

202

polymorphic type of the node *)

203

let polymorphic_types = find_all_polymorphic_type submachine in

204

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

205

(try

206

assert (List.for_all (fun x > List.mem_assoc x substitution) polymorphic_types)

207

with

208

Not_found > assert false);

209

substitution

210


211


212

(** Extract from a machine the instance corresponding to the identifier,

213

assume that the identifier exists in the instances of the machine.

214


215

@param identifier the instance identifier

216

@param machine a machine

217

@return the instance of machine.minstances corresponding to identifier

218

**)

219

let get_instance identifier typed_submachines =

220

try

221

List.assoc identifier typed_submachines

222

with Not_found > assert false

223


224

(*Usefull for debug*)

225

let pp_type_debug fmt typ =

226

(match (Lustrec.Types.repr typ).Lustrec.Types.tdesc with

227

 Lustrec.Types.Tbasic Lustrec.Types.Basic.Tint > Format.fprintf fmt "INTEGER"

228

 Lustrec.Types.Tbasic Lustrec.Types.Basic.Treal > Format.fprintf fmt "FLOAT"

229

 Lustrec.Types.Tbasic Lustrec.Types.Basic.Tbool > Format.fprintf fmt "BOOLEAN"

230

 Lustrec.Types.Tunivar > Format.fprintf fmt "POLY(%i)" typ.Lustrec.Types.tid

231

 _ > assert false

232

)

233


234

let build_if g c1 i1 tl =

235

let neg = c1=tag_false in

236

let other = match tl with

237

 [] > None

238

 [(c2, i2)] > Some i2

239

 _ > assert false

240

in

241

match neg, other with

242

 true, Some x > (false, g, x, Some i1)

243

 _ >

244

(neg, g, i1, other)

245


246

let rec push_if_in_expr = function

247

 [] > []

248

 instr::q >

249

(

250

match get_instr_desc instr with

251

 MBranch (g, (c1, i1)::tl) when c1=tag_false  c1=tag_true >

252

let (neg, g, instrs1, instrs2) = build_if g c1 i1 tl in

253

let instrs1_pushed = push_if_in_expr instrs1 in

254

let get_assign instr = match get_instr_desc instr with

255

 MLocalAssign (id, value) > (false, id, value)

256

 MStateAssign (id, value) > (true, id, value)

257

 _ > assert false

258

in

259

let gen_eq ident state value1 value2 =

260

assert(check_type_equal ident.var_type value1.value_type);

261

assert(check_type_equal ident.var_type value2.value_type);

262

let value = {

263

value_desc = Fun ("ite", [g;value1;value2]);

264

value_type = ident.var_type;

265

value_annot = None

266

}

267

in

268

let assign = if state then MStateAssign (ident, value) else MLocalAssign (ident, value) in

269

{ instr_desc = assign;

270

lustre_eq = None

271

}

272

in

273

let mkval_var id = {

274

value_desc = Var id;

275

value_type = id.var_type;

276

value_annot = None

277

}

278

in

279

let rec find_split s1 id1 accu = function

280

 [] > [], accu, mkval_var id1

281

 (s2, id2, v2)::q when s1 = s2

282

&& id1.var_id = id2.var_id > accu, q, v2

283

 t::q > find_split s1 id1 (t::accu) q

284

in

285

let gen_from_else l =

286

List.map

287

(fun (s2, id2, v2) > gen_eq id2 s2 (mkval_var id2) v2)

288

l

289

in

290

let rec gen_assigns if_assigns else_assigns =

291

let res, accu_else = match if_assigns with

292

 (s1, id1, v1)::q >

293

let accu, remain, v2 = find_split s1 id1 [] else_assigns in

294

(gen_eq id1 s1 v1 v2)::(gen_assigns q remain), accu

295

 [] > [], else_assigns

296

in

297

(gen_from_else accu_else)@res

298

in

299

let if_assigns = List.map get_assign instrs1_pushed in

300

let else_assigns = match instrs2 with

301

 None > []

302

 Some instrs2 >

303

let instrs2_pushed = push_if_in_expr instrs2 in

304

List.map get_assign instrs2_pushed

305

in

306

gen_assigns if_assigns else_assigns

307

 x > [instr]

308

)@(push_if_in_expr q)

309


310


311


312

