1


2

open Machine_code_types

3

open Lustre_types

4

open Corelang

5

(*

6

open 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 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 = (Types.repr typ).tdesc == Types.Tunivar

50


51

(** Find all polymorphic type : 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 _, 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 (Types.repr typ).Types.tdesc with

96

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

97

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

98

 Types.Tbasic Types.Basic.Tbool > 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:Types.type_expr) (t2:Types.type_expr) =

109

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

110

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

111

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

112

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

113

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

114

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

115

 _, 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*Types.type_expr) list) ((type_poly:Types.type_expr), (typ: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, _) (i2, _) =

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::_ > 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 (Types.repr typ).Types.tdesc with

227

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

228

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

229

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

230

 Types.Tunivar > Format.fprintf fmt "POLY(%i)" typ.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

 [(_, 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 (_, 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

instr_spec = Spec_types.True

272

}

273

in

274

let mkval_var id = {

275

value_desc = Var id;

276

value_type = id.var_type;

277

value_annot = None

278

}

279

in

280

let rec find_split s1 id1 accu = function

281

 [] > [], accu, mkval_var id1

282

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

283

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

284

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

285

in

286

let gen_from_else l =

287

List.map

288

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

289

l

290

in

291

let rec gen_assigns if_assigns else_assigns =

292

let res, accu_else = match if_assigns with

293

 (s1, id1, v1)::q >

294

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

295

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

296

 [] > [], else_assigns

297

in

298

(gen_from_else accu_else)@res

299

in

300

let if_assigns = List.map get_assign instrs1_pushed in

301

let else_assigns = match instrs2 with

302

 None > []

303

 Some instrs2 >

304

let instrs2_pushed = push_if_in_expr instrs2 in

305

List.map get_assign instrs2_pushed

306

in

307

gen_assigns if_assigns else_assigns

308

 _ > [instr]

309

)@(push_if_in_expr q)

310


311


312


313

