1

(* 

2

* SchedMCore  A MultiCore Scheduling Framework

3

* Copyright (C) 20092011, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE

4

*

5

* This file is part of Prelude

6

*

7

* Prelude is free software; you can redistribute it and/or

8

* modify it under the terms of the GNU Lesser General Public License

9

* as published by the Free Software Foundation ; either version 2 of

10

* the License, or (at your option) any later version.

11

*

12

* Prelude is distributed in the hope that it will be useful, but

13

* WITHOUT ANY WARRANTY ; without even the implied warranty of

14

* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU

15

* Lesser General Public License for more details.

16

*

17

* You should have received a copy of the GNU Lesser General Public

18

* License along with this program ; if not, write to the Free Software

19

* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307

20

* USA

21

* *)

22


23

(** Main typing module. Classic inference algorithm with destructive

24

unification. *)

25


26

let debug fmt args = () (* Format.eprintf "%a" *)

27

(* Though it shares similarities with the clock calculus module, no code

28

is shared. Simple environments, very limited identifier scoping, no

29

identifier redefinition allowed. *)

30


31

open Utils

32

(* Yes, opening both modules is dirty as some type names will be

33

overwritten, yet this makes notations far lighter.*)

34

open LustreSpec

35

open Corelang

36

open Types

37

open Format

38


39

let pp_typing_env fmt env =

40

Env.pp_env print_ty fmt env

41


42

(** [occurs tvar ty] returns true if the type variable [tvar] occurs in

43

type [ty]. False otherwise. *)

44

let rec occurs tvar ty =

45

let ty = repr ty in

46

match ty.tdesc with

47

 Tvar > ty=tvar

48

 Tarrow (t1, t2) >

49

(occurs tvar t1)  (occurs tvar t2)

50

 Ttuple tl >

51

List.exists (occurs tvar) tl

52

 Tstruct fl >

53

List.exists (fun (f, t) > occurs tvar t) fl

54

 Tarray (_, t)

55

 Tstatic (_, t)

56

 Tclock t

57

 Tlink t > occurs tvar t

58

 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > false

59


60

(** Promote monomorphic type variables to polymorphic type variables. *)

61

(* Generalize by sideeffects *)

62

let rec generalize ty =

63

match ty.tdesc with

64

 Tvar >

65

(* No scopes, always generalize *)

66

ty.tdesc < Tunivar

67

 Tarrow (t1,t2) >

68

generalize t1; generalize t2

69

 Ttuple tl >

70

List.iter generalize tl

71

 Tstruct fl >

72

List.iter (fun (f, t) > generalize t) fl

73

 Tstatic (d, t)

74

 Tarray (d, t) > Dimension.generalize d; generalize t

75

 Tclock t

76

 Tlink t >

77

generalize t

78

 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > ()

79


80

(** Downgrade polymorphic type variables to monomorphic type variables *)

81

let rec instantiate inst_vars inst_dim_vars ty =

82

let ty = repr ty in

83

match ty.tdesc with

84

 Tenum _  Tconst _  Tvar  Tint  Treal  Tbool  Trat > ty

85

 Tarrow (t1,t2) >

86

{ty with tdesc =

87

Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}

88

 Ttuple tlist >

89

{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)}

90

 Tstruct flist >

91

{ty with tdesc = Tstruct (List.map (fun (f, t) > (f, instantiate inst_vars inst_dim_vars t)) flist)}

92

 Tclock t >

93

{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)}

94

 Tstatic (d, t) >

95

{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}

96

 Tarray (d, t) >

97

{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)}

98

 Tlink t >

99

(* should not happen *)

100

{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)}

101

 Tunivar >

102

try

103

List.assoc ty.tid !inst_vars

104

with Not_found >

105

let var = new_var () in

106

inst_vars := (ty.tid, var)::!inst_vars;

107

var

108


109

(* [type_coretype cty] types the type declaration [cty] *)

110

let rec type_coretype type_dim cty =

111

match (*get_repr_type*) cty with

112

 Tydec_any > new_var ()

113

 Tydec_int > Type_predef.type_int

114

 Tydec_real > Type_predef.type_real

115

 Tydec_float > Type_predef.type_real

116

 Tydec_bool > Type_predef.type_bool

117

 Tydec_clock ty > Type_predef.type_clock (type_coretype type_dim ty)

118

 Tydec_const c > Type_predef.type_const c

119

 Tydec_enum tl > Type_predef.type_enum tl

120

 Tydec_struct fl > Type_predef.type_struct (List.map (fun (f, ty) > (f, type_coretype type_dim ty)) fl)

121

 Tydec_array (d, ty) >

122

begin

123

type_dim d;

124

Type_predef.type_array d (type_coretype type_dim ty)

125

end

126


127

(* [coretype_type] is the reciprocal of [type_typecore] *)

128

let rec coretype_type ty =

129

match (repr ty).tdesc with

130

 Tvar > Tydec_any

131

 Tint > Tydec_int

132

 Treal > Tydec_real

133

 Tbool > Tydec_bool

134

 Tconst c > Tydec_const c

135

 Tclock t > Tydec_clock (coretype_type t)

136

 Tenum tl > Tydec_enum tl

137

 Tstruct fl > Tydec_struct (List.map (fun (f, t) > (f, coretype_type t)) fl)

138

 Tarray (d, t) > Tydec_array (d, coretype_type t)

139

 Tstatic (_, t) > coretype_type t

140

 _ > assert false

141


142

let get_type_definition tname =

143

try

144

type_coretype (fun d > ()) (Hashtbl.find type_table (Tydec_const tname))

145

with Not_found > raise (Error (Location.dummy_loc, Unbound_type tname))

146


147

(* Equality on ground types only *)

148

(* Should be used between local variables which must have a ground type *)

149

let rec eq_ground t1 t2 =

150

match t1.tdesc, t2.tdesc with

151

 Tint, Tint  Tbool, Tbool  Trat, Trat > true

152

 Tenum tl, Tenum tl' when tl == tl' > true

153

 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > List.for_all2 eq_ground tl tl'

154

 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > List.for_all2 (fun (_, t) (_, t') > eq_ground t t') fl fl'

155

 (Tconst t, _) >

156

let def_t = get_type_definition t in

157

eq_ground def_t t2

158

 (_, Tconst t) >

159

let def_t = get_type_definition t in

160

eq_ground t1 def_t

161

 Tarrow (t1,t2), Tarrow (t1',t2') > eq_ground t1 t1' && eq_ground t2 t2'

162

 Tclock t1', _ > eq_ground t1' t2

163

 _, Tclock t2' > eq_ground t1 t2'

164

 Tstatic (e1, t1'), Tstatic (e2, t2')

165

 Tarray (e1, t1'), Tarray (e2, t2') > Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'

166

 _ > false

167


168

(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify

169

(t1,t2)] if the types are not unifiable.*)

170

(* Standard destructive unification *)

171

let rec unify t1 t2 =

172

let t1 = repr t1 in

173

let t2 = repr t2 in

174

if t1=t2 then

175

()

176

else

177

(* No type abbreviations resolution for now *)

178

match t1.tdesc,t2.tdesc with

179

(* This case is not mandory but will keep "older" types *)

180

 Tvar, Tvar >

181

if t1.tid < t2.tid then

182

t2.tdesc < Tlink t1

183

else

184

t1.tdesc < Tlink t2

185

 (Tvar, _) when (not (occurs t1 t2)) >

186

t1.tdesc < Tlink t2

187

 (_,Tvar) when (not (occurs t2 t1)) >

188

t2.tdesc < Tlink t1

189

 Tarrow (t1,t2), Tarrow (t1',t2') >

190

begin

191

unify t1 t1';

192

unify t2 t2'

193

end

194

 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' >

195

List.iter2 unify tl tl'

196

 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' >

197

List.iter2 (fun (_, t) (_, t') > unify t t') fl fl'

198

 Tclock _, Tstatic _

199

 Tstatic _, Tclock _ > raise (Unify (t1, t2))

200

 Tclock t1', _ > unify t1' t2

201

 _, Tclock t2' > unify t1 t2'

202

 Tint, Tint  Tbool, Tbool  Trat, Trat

203

 Tunivar, _  _, Tunivar > ()

204

 (Tconst t, _) >

205

let def_t = get_type_definition t in

206

unify def_t t2

207

 (_, Tconst t) >

208

let def_t = get_type_definition t in

209

unify t1 def_t

210

 Tenum tl, Tenum tl' when tl == tl' > ()

211

 Tstatic (e1, t1'), Tstatic (e2, t2')

212

 Tarray (e1, t1'), Tarray (e2, t2') >

213

begin

214

unify t1' t2';

215

Dimension.eval Basic_library.eval_env (fun c > None) e1;

216

Dimension.eval Basic_library.eval_env (fun c > None) e2;

217

Dimension.unify e1 e2;

218

end

219

 _,_ > raise (Unify (t1, t2))

220


221

(** [semi_unify t1 t2] checks whether type [t1] is an instance of type [t2]. Raises [Unify

222

(t1,t2)] if the types are not semiunifiable.*)

223

(* Standard destructive semiunification *)

224

let rec semi_unify t1 t2 =

225

let t1 = repr t1 in

226

let t2 = repr t2 in

227

if t1=t2 then

228

()

229

else

230

(* No type abbreviations resolution for now *)

231

match t1.tdesc,t2.tdesc with

232

(* This case is not mandory but will keep "older" types *)

233

 Tvar, Tvar >

234

if t1.tid < t2.tid then

235

t2.tdesc < Tlink t1

236

else

237

t1.tdesc < Tlink t2

238

 (Tvar, _) > raise (Unify (t1, t2))

239

 (_,Tvar) when (not (occurs t2 t1)) >

240

t2.tdesc < Tlink t1

241

 Tarrow (t1,t2), Tarrow (t1',t2') >

242

begin

243

semi_unify t1 t1';

244

semi_unify t2 t2'

245

end

246

 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' >

247

List.iter2 semi_unify tl tl'

248

 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' >

249

List.iter2 (fun (_, t) (_, t') > semi_unify t t') fl fl'

250

 Tclock _, Tstatic _

251

 Tstatic _, Tclock _ > raise (Unify (t1, t2))

252

 Tclock t1', _ > semi_unify t1' t2

253

 _, Tclock t2' > semi_unify t1 t2'

254

 Tint, Tint  Tbool, Tbool  Trat, Trat

255

 Tunivar, _  _, Tunivar > ()

256

 (Tconst t, _) >

257

let def_t = get_type_definition t in

258

semi_unify def_t t2

259

 (_, Tconst t) >

260

let def_t = get_type_definition t in

261

semi_unify t1 def_t

262

 Tenum tl, Tenum tl' when tl == tl' > ()

263


264

 Tstatic (e1, t1'), Tstatic (e2, t2')

265

 Tarray (e1, t1'), Tarray (e2, t2') >

266

begin

267

semi_unify t1' t2';

268

Dimension.eval Basic_library.eval_env (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) e1;

269

Dimension.eval Basic_library.eval_env (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) e2;

270

Dimension.semi_unify e1 e2;

271

end

272

 _,_ > raise (Unify (t1, t2))

273


274

(* Expected type ty1, got type ty2 *)

275

let try_unify ty1 ty2 loc =

276

try

277

unify ty1 ty2

278

with

279

 Unify _ >

280

raise (Error (loc, Type_clash (ty1,ty2)))

281

 Dimension.Unify _ >

282

raise (Error (loc, Type_clash (ty1,ty2)))

283


284

let try_semi_unify ty1 ty2 loc =

285

try

286

semi_unify ty1 ty2

287

with

288

 Unify _ >

289

raise (Error (loc, Type_clash (ty1,ty2)))

290

 Dimension.Unify _ >

291

raise (Error (loc, Type_clash (ty1,ty2)))

292


293

(* ty1 is a subtype of ty2 *)

294

let rec sub_unify sub ty1 ty2 =

295

match (repr ty1).tdesc, (repr ty2).tdesc with

296

 Ttuple tl1 , Ttuple tl2 >

297

if List.length tl1 <> List.length tl2

298

then raise (Unify (ty1, ty2))

299

else List.iter2 (sub_unify sub) tl1 tl2

300

 Ttuple [t1] , _ > sub_unify sub t1 ty2

301

 _ , Ttuple [t2] > sub_unify sub ty1 t2

302

 Tstruct tl1 , Tstruct tl2 >

303

if List.map fst tl1 <> List.map fst tl2

304

then raise (Unify (ty1, ty2))

305

else List.iter2 (fun (_, t1) (_, t2) > sub_unify sub t1 t2) tl1 tl2

306

 Tclock t1 , Tclock t2 > sub_unify sub t1 t2

307

 Tclock t1 , _ when sub > sub_unify sub t1 ty2

308

 Tstatic (d1, t1) , Tstatic (d2, t2) >

309

begin

310

sub_unify sub t1 t2;

311

Dimension.eval Basic_library.eval_env (fun c > None) d1;

312

Dimension.eval Basic_library.eval_env (fun c > None) d2;

313

Dimension.unify d1 d2

314

end

315

 Tstatic (r_d, t1) , _ when sub > sub_unify sub t1 ty2

316

 _ > unify ty1 ty2

317


318

let try_sub_unify sub ty1 ty2 loc =

319

try

320

sub_unify sub ty1 ty2

321

with

322

 Unify _ >

323

raise (Error (loc, Type_clash (ty1,ty2)))

324

 Dimension.Unify _ >

325

raise (Error (loc, Type_clash (ty1,ty2)))

326


327

let rec type_struct_const_field loc (label, c) =

328

if Hashtbl.mem field_table label

329

then let tydec = Hashtbl.find field_table label in

330

let tydec_struct = get_struct_type_fields tydec in

331

let ty_label = type_coretype (fun d > ()) (List.assoc label tydec_struct) in

332

begin

333

try_unify ty_label (type_const loc c) loc;

334

type_coretype (fun d > ()) tydec

335

end

336

else raise (Error (loc, Unbound_value ("struct field " ^ label)))

337


338

and type_const loc c =

339

match c with

340

 Const_int _ > Type_predef.type_int

341

 Const_real _ > Type_predef.type_real

342

 Const_float _ > Type_predef.type_real

343

 Const_array ca > let d = Dimension.mkdim_int loc (List.length ca) in

344

let ty = new_var () in

345

List.iter (fun e > try_unify ty (type_const loc e) loc) ca;

346

Type_predef.type_array d ty

347

 Const_tag t >

348

if Hashtbl.mem tag_table t

349

then type_coretype (fun d > ()) (Hashtbl.find tag_table t)

350

else raise (Error (loc, Unbound_value ("enum tag " ^ t)))

351

 Const_struct fl >

352

let ty_struct = new_var () in

353

begin

354

let used =

355

List.fold_left

356

(fun acc (l, c) >

357

if List.mem l acc

358

then raise (Error (loc, Already_bound ("struct field " ^ l)))

359

else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)

360

[] fl in

361

try

362

let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in

363

(* List.iter (fun l > Format.eprintf "total: %s@." l) total;

364

List.iter (fun l > Format.eprintf "used: %s@." l) used; *)

365

let undef = List.find (fun l > not (List.mem l used)) total

366

in raise (Error (loc, Unbound_value ("struct field " ^ undef)))

367

with Not_found >

368

ty_struct

369

end

370


371

(* The following typing functions take as parameter an environment [env]

372

and whether the element being typed is expected to be constant [const].

373

[env] is a pair composed of:

374

 a map from ident to type, associating to each ident, i.e.

375

variables, constants and (imported) nodes, its type including whether

376

it is constant or not. This latter information helps in checking constant

377

propagation policy in Lustre.

378

 a vdecl list, in order to modify types of declared variables that are

379

later discovered to be clocks during the typing process.

380

*)

381

let check_constant loc const_expected const_real =

382

if const_expected && not const_real

383

then raise (Error (loc, Not_a_constant))

384


385

let rec type_standard_args env in_main const expr_list =

386

let ty_list = List.map (fun e > dynamic_type (type_expr env in_main const e)) expr_list in

387

let ty_res = new_var () in

388

List.iter2 (fun e ty > try_unify ty_res ty e.expr_loc) expr_list ty_list;

389

ty_res

390


391

(* emulates a subtyping relation between types t and (d : t),

392

used during node applications and assignments *)

393

and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =

394

let loc = real_arg.expr_loc in

395

let const = const  (Types.get_static_value formal_type <> None) in

396

let real_type = type_expr env in_main const real_arg in

397

let real_type =

398

if const

399

then let d =

400

if is_dimension_type real_type

401

then dimension_of_expr real_arg

402

else Dimension.mkdim_var () in

403

let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in

404

Dimension.eval Basic_library.eval_env eval_const d;

405

let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in

406

(match Types.get_static_value real_type with

407

 None > ()

408

 Some d' > try_unify real_type real_static_type loc);

409

real_static_type

410

else real_type in

411

(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)

412

try_sub_unify sub real_type formal_type loc

413


414

and type_ident env in_main loc const id =

415

type_expr env in_main const (expr_of_ident id loc)

416


417

(* typing an application implies:

418

 checking that const formal parameters match real const (maybe symbolic) arguments

419

 checking type adequation between formal and real arguments

420

An application may embed an homomorphic/internal function, in which case we need to split

421

it in many calls

422

*)

423

and type_appl env in_main loc const f args =

424

let args = expr_list_of_expr args in

425

if Basic_library.is_internal_fun f && List.exists is_tuple_expr args

426

then

427

try

428

let args = Utils.transpose_list (List.map expr_list_of_expr args) in

429

Types.type_of_type_list (List.map (type_call env in_main loc const f) args)

430

with

431

Utils.TransposeError (l, l') > raise (Error (loc, WrongMorphism (l, l')))

432

else

433

type_call env in_main loc const f args

434


435

(* type a (single) call. [args] is here a list of arguments. *)

436

and type_call env in_main loc const f args =

437

let tfun = type_ident env in_main loc const f in

438

let tins, touts = split_arrow tfun in

439

let tins = type_list_of_type tins in

440

if List.length args <> List.length tins then

441

raise (Error (loc, WrongArity (List.length args, List.length tins)))

442

else

443

List.iter2 (type_subtyping_arg env in_main const) args tins;

444

touts

445


446

(** [type_expr env in_main expr] types expression [expr] in environment

447

[env], expecting it to be [const] or not. *)

448

and type_expr env in_main const expr =

449

let resulting_ty =

450

match expr.expr_desc with

451

 Expr_const c >

452

let ty = type_const expr.expr_loc c in

453

let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in

454

expr.expr_type < ty;

455

ty

456

 Expr_ident v >

457

let tyv =

458

try

459

Env.lookup_value (fst env) v

460

with Not_found >

461

Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;

462

raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))

463

in

464

let ty = instantiate (ref []) (ref []) tyv in

465

let ty' =

466

if const

467

then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())

468

else new_var () in

469

try_unify ty ty' expr.expr_loc;

470

expr.expr_type < ty;

471

ty

472

 Expr_array elist >

473

let ty_elt = type_standard_args env in_main const elist in

474

let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in

475

let ty = Type_predef.type_array d ty_elt in

476

expr.expr_type < ty;

477

ty

478

 Expr_access (e1, d) >

479

type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;

480

let ty_elt = new_var () in

481

let d = Dimension.mkdim_var () in

482

type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);

483

expr.expr_type < ty_elt;

484

ty_elt

485

 Expr_power (e1, d) >

486

let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in

487

type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;

488

Dimension.eval Basic_library.eval_env eval_const d;

489

let ty_elt = type_standard_args env in_main const [e1] in

490

let ty = Type_predef.type_array d ty_elt in

491

expr.expr_type < ty;

492

ty

493

 Expr_tuple elist >

494

let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in

495

expr.expr_type < ty;

496

ty

497

 Expr_ite (c, t, e) >

498

type_subtyping_arg env in_main const c Type_predef.type_bool;

499

let ty = type_standard_args env in_main const [t; e] in

500

expr.expr_type < ty;

501

ty

502

 Expr_appl (id, args, r) >

503

(* application of non internal function is not legal in a constant

504

expression *)

505

(match r with

506

 None > ()

507

 Some (x, l) >

508

check_constant expr.expr_loc const false;

509

let expr_x = expr_of_ident x expr.expr_loc in

510

let typ_l =

511

Type_predef.type_clock

512

(type_const expr.expr_loc (Const_tag l)) in

513

type_subtyping_arg env in_main ~sub:false const expr_x typ_l);

514

let touts = type_appl env in_main expr.expr_loc const id args in

515

expr.expr_type < touts;

516

touts

517

 Expr_fby (e1,e2)

518

 Expr_arrow (e1,e2) >

519

(* fby/arrow is not legal in a constant expression *)

520

check_constant expr.expr_loc const false;

521

let ty = type_standard_args env in_main const [e1; e2] in

522

expr.expr_type < ty;

523

ty

524

 Expr_pre e >

525

(* pre is not legal in a constant expression *)

526

check_constant expr.expr_loc const false;

527

let ty = type_standard_args env in_main const [e] in

528

expr.expr_type < ty;

529

ty

530

 Expr_when (e1,c,l) >

531

(* when is not legal in a constant expression *)

532

check_constant expr.expr_loc const false;

533

let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in

534

let expr_c = expr_of_ident c expr.expr_loc in

535

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

536

update_clock env in_main c expr.expr_loc typ_l;

537

let ty = type_standard_args env in_main const [e1] in

538

expr.expr_type < ty;

539

ty

540

 Expr_merge (c,hl) >

541

(* merge is not legal in a constant expression *)

542

check_constant expr.expr_loc const false;

543

let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in

544

let expr_c = expr_of_ident c expr.expr_loc in

545

let typ_l = Type_predef.type_clock typ_in in

546

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

547

update_clock env in_main c expr.expr_loc typ_l;

548

expr.expr_type < typ_out;

549

typ_out

550

 Expr_uclock (e,k)  Expr_dclock (e,k) >

551

let ty = type_expr env in_main const e in

552

expr.expr_type < ty;

553

ty

554

 Expr_phclock (e,q) >

555

let ty = type_expr env in_main const e in

556

expr.expr_type < ty;

557

ty

558

in

559

Log.report ~level:3 (fun fmt > Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);

560

resulting_ty

561


562

and type_branches env in_main loc const hl =

563

let typ_in = new_var () in

564

let typ_out = new_var () in

565

try

566

let used_labels =

567

List.fold_left (fun accu (t, h) >

568

unify typ_in (type_const loc (Const_tag t));

569

type_subtyping_arg env in_main const h typ_out;

570

if List.mem t accu

571

then raise (Error (loc, Already_bound t))

572

else t :: accu) [] hl in

573

let type_labels = get_enum_type_tags (coretype_type typ_in) in

574

if List.sort compare used_labels <> List.sort compare type_labels

575

then let unbound_tag = List.find (fun t > not (List.mem t used_labels)) type_labels in

576

raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag)))

577

else (typ_in, typ_out)

578

with Unify (t1, t2) >

579

raise (Error (loc, Type_clash (t1,t2)))

580


581

and update_clock env in_main id loc typ =

582

(*Log.report ~level:1 (fun fmt > Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)

583

try

584

let vdecl = List.find (fun v > v.var_id = id) (snd env)

585

in vdecl.var_type < typ

586

with

587

Not_found >

588

raise (Error (loc, Unbound_value ("clock " ^ id)))

589


590

(** [type_eq env eq] types equation [eq] in environment [env] *)

591

let type_eq env in_main undefined_vars eq =

592

(* Check undefined variables, type lhs *)

593

let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v > expr_of_ident v eq.eq_loc) eq.eq_lhs) in

594

let ty_lhs = type_expr env in_main false expr_lhs in

595

(* Check multiple variable definitions *)

596

let define_var id uvars =

597

try

598

ignore(IMap.find id uvars);

599

IMap.remove id uvars

600

with Not_found >

601

raise (Error (eq.eq_loc, Already_defined id))

602

in

603

let undefined_vars =

604

List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs in

605

(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned

606

to a (always nonconstant) lhs variable *)

607

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

608

undefined_vars

609


610


611

(* [type_coreclock env ck id loc] types the type clock declaration [ck]

612

in environment [env] *)

613

let type_coreclock env ck id loc =

614

match ck.ck_dec_desc with

615

 Ckdec_any  Ckdec_pclock (_,_) > ()

616

 Ckdec_bool cl >

617

let dummy_id_expr = expr_of_ident id loc in

618

let when_expr =

619

List.fold_left

620

(fun expr (x, l) >

621

{expr_tag = new_tag ();

622

expr_desc= Expr_when (expr,x,l);

623

expr_type = new_var ();

624

expr_clock = Clocks.new_var true;

625

expr_delay = Delay.new_var ();

626

expr_loc=loc;

627

expr_annot = None})

628

dummy_id_expr cl

629

in

630

ignore (type_expr env false false when_expr)

631


632

let rec check_type_declaration loc cty =

633

match cty with

634

 Tydec_clock ty

635

 Tydec_array (_, ty) > check_type_declaration loc ty

636

 Tydec_const tname >

637

if not (Hashtbl.mem type_table cty)

638

then raise (Error (loc, Unbound_type tname));

639

 _ > ()

640


641

let type_var_decl vd_env env vdecl =

642

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

643

let eval_const id = Types.get_static_value (Env.lookup_value env id) in

644

let type_dim d =

645

begin

646

type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;

647

Dimension.eval Basic_library.eval_env eval_const d;

648

end in

649

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

650

let ty_status =

651

if vdecl.var_dec_const

652

then Type_predef.type_static (Dimension.mkdim_var ()) ty

653

else ty in

654

let new_env = Env.add_value env vdecl.var_id ty_status in

655

type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;

656

vdecl.var_type < ty_status;

657

new_env

658


659

let type_var_decl_list vd_env env l =

660

List.fold_left (type_var_decl vd_env) env l

661


662

let type_of_vlist vars =

663

let tyl = List.map (fun v > v.var_type) vars in

664

type_of_type_list tyl

665


666

let add_vdecl vd_env vdecl =

667

if List.exists (fun v > v.var_id = vdecl.var_id) vd_env

668

then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))

669

else vdecl::vd_env

670


671

let check_vd_env vd_env =

672

ignore (List.fold_left add_vdecl [] vd_env)

673


674

(** [type_node env nd loc] types node [nd] in environment env. The

675

location is used for error reports. *)

676

let type_node env nd loc =

677

let is_main = nd.node_id = !Options.main_node in

678

let vd_env_ol = nd.node_outputs@nd.node_locals in

679

let vd_env = nd.node_inputs@vd_env_ol in

680

check_vd_env vd_env;

681

let init_env = env in

682

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

683

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

684

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

685

let new_env = Env.overwrite env delta_env in

686

let undefined_vars_init =

687

List.fold_left

688

(fun uvs v > IMap.add v.var_id () uvs)

689

IMap.empty vd_env_ol in

690

let undefined_vars =

691

List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs

692

in

693

(* check that table is empty *)

694

if (not (IMap.is_empty undefined_vars)) then

695

raise (Error (loc, Undefined_var undefined_vars));

696

let ty_ins = type_of_vlist nd.node_inputs in

697

let ty_outs = type_of_vlist nd.node_outputs in

698

let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in

699

generalize ty_node;

700

(* TODO ? Check that no node in the hierarchy remains polymorphic ? *)

701

nd.node_type < ty_node;

702

Env.add_value env nd.node_id ty_node

703


704

let type_imported_node env nd loc =

705

let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in

706

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

707

check_vd_env vd_env;

708

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

709

let ty_ins = type_of_vlist nd.nodei_inputs in

710

let ty_outs = type_of_vlist nd.nodei_outputs in

711

let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in

712

generalize ty_node;

713

(*

714

if (is_polymorphic ty_node) then

715

raise (Error (loc, Poly_imported_node nd.nodei_id));

716

*)

717

let new_env = Env.add_value env nd.nodei_id ty_node in

718

nd.nodei_type < ty_node;

719

new_env

720


721

let type_top_consts env clist =

722

List.fold_left (fun env cdecl >

723

let ty = type_const cdecl.const_loc cdecl.const_value in

724

let d =

725

if is_dimension_type ty

726

then dimension_of_const cdecl.const_loc cdecl.const_value

727

else Dimension.mkdim_var () in

728

let ty = Type_predef.type_static d ty in

729

let new_env = Env.add_value env cdecl.const_id ty in

730

cdecl.const_type < ty;

731

new_env) env clist

732


733

let type_top_decl env decl =

734

match decl.top_decl_desc with

735

 Node nd > (

736

try

737

type_node env nd decl.top_decl_loc

738

with Error (loc, err) as exc > (

739

if !Options.global_inline then

740

Format.eprintf "Type error: failing node@.%a@.@?"

741

Printers.pp_node nd

742

;

743

raise exc)

744

)

745

 ImportedNode nd >

746

type_imported_node env nd decl.top_decl_loc

747

 Consts clist >

748

type_top_consts env clist

749

 Open _ > env

750


751

let type_prog env decls =

752

try

753

List.fold_left type_top_decl env decls

754

with Failure _ as exc > raise exc

755


756

(* Once the Lustre program is fully typed,

757

we must get back to the original description of dimensions,

758

with constant parameters, instead of unifiable internal variables. *)

759


760

(* The following functions aims at 'unevaluating' dimension expressions occuring in array types,

761

i.e. replacing unifiable second_order variables with the original static parameters.

762

Once restored in this formulation, dimensions may be meaningfully printed.

763

*)

764

let uneval_vdecl_generics vdecl =

765

if vdecl.var_dec_const

766

then

767

match get_static_value vdecl.var_type with

768

 None > (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)

769

 Some d > Dimension.uneval vdecl.var_id d

770


771

let uneval_node_generics vdecls =

772

List.iter uneval_vdecl_generics vdecls

773


774

let uneval_top_generics decl =

775

match decl.top_decl_desc with

776

 Node nd >

777

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

778

 ImportedNode nd >

779

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

780

 Consts clist > ()

781

 Open _ > ()

782


783

let uneval_prog_generics prog =

784

List.iter uneval_top_generics prog

785


786

let rec get_imported_node decls id =

787

match decls with

788

 [] > assert false

789

 decl::q >

790

(match decl.top_decl_desc with

791

 ImportedNode nd when id = nd.nodei_id > decl

792

 _ > get_imported_node q id)

793


794

let check_env_compat header declared computed =

795

uneval_prog_generics header;

796

Env.iter declared (fun k decl_type_k >

797

let computed_t = instantiate (ref []) (ref [])

798

(try Env.lookup_value computed k

799

with Not_found >

800

let loc = (get_imported_node header k).top_decl_loc in

801

raise (Error (loc, Declared_but_undefined k))) in

802

(*Types.print_ty Format.std_formatter decl_type_k;

803

Types.print_ty Format.std_formatter computed_t;*)

804

try_semi_unify decl_type_k computed_t Location.dummy_loc

805

)

806


807

(* Local Variables: *)

808

(* compilecommand:"make C .." *)

809

(* End: *)
