1

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

2

(* *)

3

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

4

(* Copyright 2012   ONERA  CNRS  INPT *)

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

type dim_expr =

15

{mutable dim_desc: dim_desc;

16

dim_loc: Location.t;

17

dim_id: int}

18


19

and dim_desc =

20

 Dbool of bool

21

 Dint of int

22

 Dident of Utils.ident

23

 Dappl of Utils.ident * dim_expr list

24

 Dite of dim_expr * dim_expr * dim_expr

25

 Dlink of dim_expr

26

 Dvar

27

 Dunivar

28


29

exception Unify of dim_expr * dim_expr

30

exception InvalidDimension

31


32

let new_id = ref (1)

33


34

let mkdim loc dim =

35

incr new_id;

36

{ dim_loc = loc;

37

dim_id = !new_id;

38

dim_desc = dim;}

39


40

let mkdim_var () =

41

incr new_id;

42

{ dim_loc = Location.dummy_loc;

43

dim_id = !new_id;

44

dim_desc = Dvar;}

45


46

let mkdim_ident loc id =

47

incr new_id;

48

{ dim_loc = loc;

49

dim_id = !new_id;

50

dim_desc = Dident id;}

51


52

let mkdim_bool loc b =

53

incr new_id;

54

{ dim_loc = loc;

55

dim_id = !new_id;

56

dim_desc = Dbool b;}

57


58

let mkdim_int loc i =

59

incr new_id;

60

{ dim_loc = loc;

61

dim_id = !new_id;

62

dim_desc = Dint i;}

63


64

let mkdim_appl loc f args =

65

incr new_id;

66

{ dim_loc = loc;

67

dim_id = !new_id;

68

dim_desc = Dappl (f, args);}

69


70

let mkdim_ite loc i t e =

71

incr new_id;

72

{ dim_loc = loc;

73

dim_id = !new_id;

74

dim_desc = Dite (i, t, e);}

75


76

let rec pp_dimension fmt dim =

77

(*fprintf fmt "<%d>" (Obj.magic dim: int);*)

78

match dim.dim_desc with

79

 Dident id >

80

fprintf fmt "%s" id

81

 Dint i >

82

fprintf fmt "%d" i

83

 Dbool b >

84

fprintf fmt "%B" b

85

 Dite (i, t, e) >

86

fprintf fmt "if %a then %a else %a"

87

pp_dimension i pp_dimension t pp_dimension e

88

 Dappl (f, [arg]) >

89

fprintf fmt "(%s%a)" f pp_dimension arg

90

 Dappl (f, [arg1; arg2]) >

91

fprintf fmt "(%a%s%a)" pp_dimension arg1 f pp_dimension arg2

92

 Dappl (_, _) > assert false

93

 Dlink dim' > fprintf fmt "%a" pp_dimension dim'

94

 Dvar > fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id)

95

 Dunivar > fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id)

96


97

let rec multi_dimension_product loc dim_list =

98

match dim_list with

99

 [] > mkdim_int loc 1

100

 [d] > d

101

 d::q > mkdim_appl loc "*" [d; multi_dimension_product loc q]

102


103

(* Builds a dimension expr representing 0<=d *)

104

let check_bound loc d =

105

mkdim_appl loc "<=" [mkdim_int loc 0; d]

106


107

(* Builds a dimension expr representing 0<=i<d *)

108

let check_access loc d i =

109

mkdim_appl loc "&&"

110

[mkdim_appl loc "<=" [mkdim_int loc 0; i];

111

mkdim_appl loc "<" [i; d]]

112


113

let rec repr dim =

114

match dim.dim_desc with

115

 Dlink dim' > repr dim'

116

 _ > dim

117


118

let rec is_eq_dimension d1 d2 =

119

let d1 = repr d1 in

120

let d2 = repr d2 in

121

d1.dim_id = d2.dim_id 

122

match d1.dim_desc, d2.dim_desc with

123

 Dappl (f1, args1), Dappl (f2, args2) >

124

f1 = f2 && List.length args1 = List.length args2 && List.for_all2 is_eq_dimension args1 args2

125

 Dite (c1, t1, e1), Dite (c2, t2, e2) >

126

is_eq_dimension c1 c2 && is_eq_dimension t1 t2 && is_eq_dimension e1 e2

127

 Dint i1 , Dint i2 > i1 = i2

128

 Dbool b1 , Dbool b2 > b1 = b2

129

 Dident id1, Dident id2 > id1 = id2

130

 _ > false

131


132

let is_dimension_const dim =

133

match (repr dim).dim_desc with

134

 Dint _

135

 Dbool _ > true

136

 _ > false

137


138

let size_const_dimension dim =

139

match (repr dim).dim_desc with

140

 Dint i > i

141

 Dbool b > if b then 1 else 0

142

 _ > (Format.eprintf "internal error: size_const_dimension %a@." pp_dimension dim; assert false)

143


144

let rec is_polymorphic dim =

145

match dim.dim_desc with

146

 Dident _

147

 Dint _

148

 Dbool _

149

 Dvar > false

150

 Dite (i, t, e) >

151

is_polymorphic i  is_polymorphic t  is_polymorphic e

152

 Dappl (_, args) > List.exists is_polymorphic args

153

 Dlink dim' > is_polymorphic dim'

154

 Dunivar > true

155


156

(* Normalizes a dimension expression, i.e. canonicalize all polynomial

157

subexpressions, where unsupported operations (eg. '/') are treated

158

as variables.

159

*)

160


161

let rec factors dim =

162

match dim.dim_desc with

163

 Dappl (f, args) when f = "*" > List.flatten (List.map factors args)

164

 _ > [dim]

165


166

let rec factors_constant fs =

167

match fs with

168

 [] > 1

169

 f::q >

170

match f.dim_desc with

171

 Dint i > i * (factors_constant q)

172

 _ > factors_constant q

173


174

let norm_factors fs =

175

let k = factors_constant fs in

176

let nk = List.filter (fun d > not (is_dimension_const d)) fs in

177

(k, List.sort Pervasives.compare nk)

178


179

let rec terms dim =

180

match dim.dim_desc with

181

 Dappl (f, args) when f = "+" > List.flatten (List.map terms args)

182

 _ > [dim]

183


184

let rec normalize dim =

185

dim

186

(*

187

let rec unnormalize loc l =

188

let l = List.sort (fun (k, l) (k', l') > compare l l') (List.map (fun (k, l) > (k, List.sort compare l)) l) in

189

match l with

190

 [] > mkdim_int loc 0

191

 t::q >

192

List.fold_left (fun res (k, l) > mkdim_appl loc "+" res (mkdim_appl loc "*" (mkdim_int loc k) l)) t q

193

*)

194

let copy copy_dim_vars dim =

195

let rec cp dim =

196

match dim.dim_desc with

197

 Dbool _

198

 Dint _ > dim

199

 Dident id > mkdim_ident dim.dim_loc id

200

 Dite (c, t, e) > mkdim_ite dim.dim_loc (cp c) (cp t) (cp e)

201

 Dappl (id, args) > mkdim_appl dim.dim_loc id (List.map cp args)

202

 Dlink dim' > cp dim'

203

 Dunivar > assert false

204

 Dvar >

205

try

206

List.assoc dim.dim_id !copy_dim_vars

207

with Not_found >

208

let var = mkdim dim.dim_loc Dvar in

209

copy_dim_vars := (dim.dim_id, var)::!copy_dim_vars;

210

var

211

in cp dim

212


213

(* Partially evaluates a 'simple' dimension expr [dim], i.e. an expr containing only int and bool

214

constructs, with conditionals. [eval_const] is a typing environment for static values. [eval_op] is an evaluation env for basic operators. The argument [dim] is modified inplace.

215

*)

216

let rec eval eval_op eval_const dim =

217

match dim.dim_desc with

218

 Dbool _

219

 Dint _ > ()

220

 Dident id >

221

(match eval_const id with

222

 Some val_dim > dim.dim_desc < Dlink val_dim

223

 None > (Format.eprintf "invalid %a@." pp_dimension dim; raise InvalidDimension))

224

 Dite (c, t, e) >

225

begin

226

eval eval_op eval_const c;

227

eval eval_op eval_const t;

228

eval eval_op eval_const e;

229

match (repr c).dim_desc with

230

 Dbool b > dim.dim_desc < Dlink (if b then t else e)

231

 _ > ()

232

end

233

 Dappl (id, args) >

234

begin

235

List.iter (eval eval_op eval_const) args;

236

if List.for_all is_dimension_const args

237

then dim.dim_desc < Env.lookup_value eval_op id (List.map (fun d > (repr d).dim_desc) args)

238

end

239

 Dlink dim' >

240

begin

241

eval eval_op eval_const dim';

242

dim.dim_desc < Dlink (repr dim')

243

end

244

 Dvar > ()

245

 Dunivar > assert false

246


247

let uneval const univar =

248

let univar = repr univar in

249

match univar.dim_desc with

250

 Dunivar > univar.dim_desc < Dident const

251

 _ > assert false

252


253

(** [occurs dvar dim] returns true if the dimension variable [dvar] occurs in

254

dimension expression [dim]. False otherwise. *)

255

let rec occurs dvar dim =

256

let dim = repr dim in

257

match dim.dim_desc with

258

 Dvar > dim.dim_id = dvar.dim_id

259

 Dident _

260

 Dint _

261

 Dbool _

262

 Dunivar > false

263

 Dite (i, t, e) >

264

occurs dvar i  occurs dvar t  occurs dvar e

265

 Dappl (_, args) > List.exists (occurs dvar) args

266

 Dlink _ > assert false

267


268

(* Promote monomorphic dimension variables to polymorphic variables.

269

Generalize by sideeffects *)

270

let rec generalize dim =

271

match dim.dim_desc with

272

 Dvar > dim.dim_desc < Dunivar

273

 Dident _

274

 Dint _

275

 Dbool _

276

 Dunivar > ()

277

 Dite (i, t, e) >

278

generalize i; generalize t; generalize e

279

 Dappl (_, args) > List.iter generalize args

280

 Dlink dim' > generalize dim'

281


282

(* Instantiate polymorphic dimension variables to monomorphic variables.

283

Also duplicates the whole term structure (but the constant subterms).

284

*)

285

let rec instantiate inst_dim_vars dim =

286

let dim = repr dim in

287

match dim.dim_desc with

288

 Dvar

289

 Dident _

290

 Dint _

291

 Dbool _ > dim

292

 Dite (i, t, e) >

293

mkdim_ite dim.dim_loc

294

(instantiate inst_dim_vars i)

295

(instantiate inst_dim_vars t)

296

(instantiate inst_dim_vars e)

297

 Dappl (f, args) > mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args)

298

 Dlink dim' > assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*)

299

 Dunivar >

300

try

301

List.assoc dim.dim_id !inst_dim_vars

302

with Not_found >

303

let var = mkdim dim.dim_loc Dvar in

304

inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars;

305

var

306


307

(** destructive unification of [dim1] and [dim2].

308

Raises [Unify (t1,t2)] if the types are not unifiable.

309

if [semi] unification is required,

310

[dim1] should furthermore be an instance of [dim2] *)

311

let unify ?(semi=false) dim1 dim2 =

312

let rec unif dim1 dim2 =

313

let dim1 = repr dim1 in

314

let dim2 = repr dim2 in

315

if dim1.dim_id = dim2.dim_id then () else

316

match dim1.dim_desc, dim2.dim_desc with

317

 Dunivar, _

318

 _ , Dunivar > assert false

319

 Dvar , Dvar >

320

if dim1.dim_id < dim2.dim_id

321

then dim2.dim_desc < Dlink dim1

322

else dim1.dim_desc < Dlink dim2

323

 Dvar , _ when (not semi) && not (occurs dim1 dim2) >

324

dim1.dim_desc < Dlink dim2

325

 _ , Dvar when not (occurs dim2 dim1) >

326

dim2.dim_desc < Dlink dim1

327

 Dite(i1, t1, e1), Dite(i2, t2, e2) >

328

begin

329

unif i1 i2;

330

unif t1 t2;

331

unif e1 e2

332

end

333

 Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 >

334

List.iter2 unif args1 args2

335

 Dbool b1, Dbool b2 when b1 = b2 > ()

336

 Dint i1 , Dint i2 when i1 = i2 > ()

337

 Dident id1, Dident id2 when id1 = id2 > ()

338

 _ > raise (Unify (dim1, dim2))

339

in unif dim1 dim2

340


341

let rec rename fnode fvar e =

342

{ e with dim_desc = expr_replace_var_desc fnode fvar e.dim_desc }

343

and expr_replace_var_desc fnode fvar e =

344

let re = rename fnode fvar in

345

match e with

346

 Dvar

347

 Dunivar

348

 Dbool _

349

 Dint _ > e

350

 Dident v > Dident (fvar v)

351

 Dappl (id, el) > Dappl (fnode id, List.map re el)

352

 Dite (g,t,e) > Dite (re g, re t, re e)

353

 Dlink e > Dlink (re e)

354


355

let rec expr_replace_expr fvar e =

356

{ e with dim_desc = expr_replace_expr_desc fvar e.dim_desc }

357

and expr_replace_expr_desc fvar e =

358

let re = expr_replace_expr fvar in

359

match e with

360

 Dvar

361

 Dunivar

362

 Dbool _

363

 Dint _ > e

364

 Dident v > (fvar v).dim_desc

365

 Dappl (id, el) > Dappl (id, List.map re el)

366

 Dite (g,t,e) > Dite (re g, re t, re e)

367

 Dlink e > Dlink (re e)
