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

 Tarray (_, t)

53

 Tstatic (_, t)

54

 Tclock t

55

 Tlink t > occurs tvar t

56

 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > false

57


58

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

59

(* Generalize by sideeffects *)

60

let rec generalize ty =

61

match ty.tdesc with

62

 Tvar >

63

(* No scopes, always generalize *)

64

ty.tdesc < Tunivar

65

 Tarrow (t1,t2) >

66

generalize t1; generalize t2

67

 Ttuple tlist >

68

List.iter generalize tlist

69

 Tstatic (d, t)

70

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

71

 Tclock t

72

 Tlink t >

73

generalize t

74

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

75


76

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

77

let rec instantiate inst_vars inst_dim_vars ty =

78

let ty = repr ty in

79

match ty.tdesc with

80

 Tenum _  Tconst _  Tvar  Tint  Treal  Tbool  Trat > ty

81

 Tarrow (t1,t2) >

82

{ty with tdesc =

83

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

84

 Ttuple tlist >

85

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

86

 Tclock t >

87

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

88

 Tstatic (d, t) >

89

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

90

 Tarray (d, t) >

91

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

92

 Tlink t >

93

(* should not happen *)

94

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

95

 Tunivar >

96

try

97

List.assoc ty.tid !inst_vars

98

with Not_found >

99

let var = new_var () in

100

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

101

var

102


103

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

104

let rec type_coretype type_dim cty =

105

match (*get_repr_type*) cty with

106

 Tydec_any > new_var ()

107

 Tydec_int > Type_predef.type_int

108

 Tydec_real > Type_predef.type_real

109

 Tydec_float > Type_predef.type_real

110

 Tydec_bool > Type_predef.type_bool

111

 Tydec_clock ty > Type_predef.type_clock (type_coretype type_dim ty)

112

 Tydec_const c > Type_predef.type_const c

113

 Tydec_enum tl > Type_predef.type_enum tl

114

 Tydec_struct fl > assert false (*Type_predef.type_struct fl*)

115

 Tydec_array (d, ty) >

116

begin

117

type_dim d;

118

Type_predef.type_array d (type_coretype type_dim ty)

119

end

120


121

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

122

let rec coretype_type ty =

123

match (repr ty).tdesc with

124

 Tvar > Tydec_any

125

 Tint > Tydec_int

126

 Treal > Tydec_real

127

 Tbool > Tydec_bool

128

 Tconst c > Tydec_const c

129

 Tclock t > Tydec_clock (coretype_type t)

130

 Tenum tl > Tydec_enum tl

131

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

132

 Tstatic (_, t) > coretype_type t

133

 _ > assert false

134


135

let get_type_definition tname =

136

try

137

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

138

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

139


140

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

141

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

142

(* Standard destructive unification *)

143

let rec unify t1 t2 =

144

let t1 = repr t1 in

145

let t2 = repr t2 in

146

if t1=t2 then

147

()

148

else

149

(* No type abbreviations resolution for now *)

150

match t1.tdesc,t2.tdesc with

151

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

152

 Tvar, Tvar >

153

if t1.tid < t2.tid then

154

t2.tdesc < Tlink t1

155

else

156

t1.tdesc < Tlink t2

157

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

158

t1.tdesc < Tlink t2

159

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

160

t2.tdesc < Tlink t1

161

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

162

begin

163

unify t1 t1';

164

unify t2 t2'

165

end

166

 Ttuple tlist1, Ttuple tlist2 >

167

if (List.length tlist1) <> (List.length tlist2) then

168

raise (Unify (t1, t2))

169

else

170

List.iter2 unify tlist1 tlist2

171

 Tclock _, Tstatic _

172

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

173

 Tclock t1', _ > unify t1' t2

174

 _, Tclock t2' > unify t1 t2'

175

 Tint, Tint  Tbool, Tbool  Trat, Trat

176

 Tunivar, _  _, Tunivar > ()

177

 (Tconst t, _) >

178

let def_t = get_type_definition t in

179

unify def_t t2

180

 (_, Tconst t) >

181

let def_t = get_type_definition t in

182

unify t1 def_t

183

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

184

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

185

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

186

begin

187

unify t1' t2';

188

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

189

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

190

Dimension.unify e1 e2;

191

end

192

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

193


194

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

195

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

196

(* Standard destructive semiunification *)

197

let rec semi_unify t1 t2 =

198

let t1 = repr t1 in

199

let t2 = repr t2 in

200

if t1=t2 then

201

()

202

else

203

(* No type abbreviations resolution for now *)

204

match t1.tdesc,t2.tdesc with

205

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

206

 Tvar, Tvar >

207

if t1.tid < t2.tid then

208

t2.tdesc < Tlink t1

209

else

210

t1.tdesc < Tlink t2

211

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

212

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

213

t2.tdesc < Tlink t1

214

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

215

begin

216

semi_unify t1 t1';

217

semi_unify t2 t2'

218

end

219

 Ttuple tlist1, Ttuple tlist2 >

220

if (List.length tlist1) <> (List.length tlist2) then

221

raise (Unify (t1, t2))

222

else

223

List.iter2 semi_unify tlist1 tlist2

224

 Tclock _, Tstatic _

225

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

226

 Tclock t1', _ > semi_unify t1' t2

227

 _, Tclock t2' > semi_unify t1 t2'

228

 Tint, Tint  Tbool, Tbool  Trat, Trat

229

 Tunivar, _  _, Tunivar > ()

230

 (Tconst t, _) >

231

let def_t = get_type_definition t in

232

semi_unify def_t t2

233

 (_, Tconst t) >

234

let def_t = get_type_definition t in

235

semi_unify t1 def_t

236

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

237

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

238

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

239

begin

240

semi_unify t1' t2';

241

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

242

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

243

Dimension.semi_unify e1 e2;

244

end

245

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

246


247

let try_unify ty1 ty2 loc =

248

try

249

unify ty1 ty2

250

with

251

 Unify _ >

252

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

253

 Dimension.Unify _ >

254

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

255


256

let try_semi_unify ty1 ty2 loc =

257

try

258

semi_unify ty1 ty2

259

with

260

 Unify _ >

261

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

262

 Dimension.Unify _ >

263

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

264


265

let rec type_const loc c =

266

match c with

267

 Const_int _ > Type_predef.type_int

268

 Const_real _ > Type_predef.type_real

269

 Const_float _ > Type_predef.type_real

270

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

271

let ty = new_var () in

272

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

273

Type_predef.type_array d ty

274

 Const_tag t >

275

if Hashtbl.mem tag_table t

276

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

277

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

278


279

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

280

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

281

[env] is a pair composed of:

282

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

283

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

284

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

285

propagation policy in Lustre.

286

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

287

later discovered to be clocks during the typing process.

288

*)

289

let check_constant loc const_expected const_real =

290

if const_expected && not const_real

291

then raise (Error (loc, Not_a_constant))

292


293

let rec type_standard_args env in_main const expr_list =

294

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

295

let ty_res = new_var () in

296

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

297

ty_res

298


299

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

300

used during node applications and assignments *)

301

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

302

let loc = real_arg.expr_loc in

303

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

304

let real_type = type_expr env in_main const real_arg in

305

let real_type =

306

if const

307

then let d =

308

if is_dimension_type real_type

309

then dimension_of_expr real_arg

310

else Dimension.mkdim_var () in

311

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

312

Dimension.eval Basic_library.eval_env eval_const d;

313

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

314

(match Types.get_static_value real_type with

315

 None > ()

316

 Some d' > try_unify real_type real_static_type loc);

317

real_static_type

318

else real_type in

319

(*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;*)

320

let real_types = type_list_of_type real_type in

321

let formal_types = type_list_of_type formal_type in

322

if (List.length real_types) <> (List.length formal_types)

323

then raise (Unify (real_type, formal_type))

324

else List.iter2 (type_subtyping loc sub) real_types formal_types

325


326

and type_subtyping loc sub real_type formal_type =

327

match (repr real_type).tdesc, (repr formal_type).tdesc with

328

 Tstatic _ , Tstatic _ when sub > try_unify formal_type real_type loc

329

 Tstatic (r_d, r_ty), _ when sub > try_unify formal_type r_ty loc

330

 _ > try_unify formal_type real_type loc

331


332

and type_ident env in_main loc const id =

333

type_expr env in_main const (expr_of_ident id loc)

334


335

(* typing an application implies:

336

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

337

 checking type adequation between formal and real arguments

338

*)

339

and type_appl env in_main loc const f args =

340

let tfun = type_ident env in_main loc const f in

341

let tins, touts = split_arrow tfun in

342

let tins = type_list_of_type tins in

343

let args = expr_list_of_expr args in

344

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

345

touts

346


347

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

348

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

349

and type_expr env in_main const expr =

350

let res =

351

match expr.expr_desc with

352

 Expr_const c >

353

let ty = type_const expr.expr_loc c in

354

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

355

expr.expr_type < ty;

356

ty

357

 Expr_ident v >

358

let tyv =

359

try

360

Env.lookup_value (fst env) v

361

with Not_found >

362

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

363

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

364

in

365

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

366

let ty' =

367

if const

368

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

369

else new_var () in

370

try_unify ty ty' expr.expr_loc;

371

expr.expr_type < ty;

372

ty

373

 Expr_array elist >

374

let ty_elt = type_standard_args env in_main const elist in

375

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

376

let ty = Type_predef.type_array d ty_elt in

377

expr.expr_type < ty;

378

ty

379

 Expr_access (e1, d) >

380

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

381

let ty_elt = new_var () in

382

let d = Dimension.mkdim_var () in

383

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

384

expr.expr_type < ty_elt;

385

ty_elt

386

 Expr_power (e1, d) >

387

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

388

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

389

Dimension.eval Basic_library.eval_env eval_const d;

390

let ty_elt = type_standard_args env in_main const [e1] in

391

let ty = Type_predef.type_array d ty_elt in

392

expr.expr_type < ty;

393

ty

394

 Expr_tuple elist >

395

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

396

expr.expr_type < ty;

397

ty

398

 Expr_ite (c, t, e) >

399

type_subtyping_arg env in_main const c Type_predef.type_bool;

400

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

401

expr.expr_type < ty;

402

ty

403

 Expr_appl (id, args, r) >

404

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

405

expression *)

406

(match r with

407

 None > ()

408

 Some (x, l) >

409

check_constant expr.expr_loc const false;

410

let expr_x = expr_of_ident x expr.expr_loc in

411

let typ_l =

412

Type_predef.type_clock

413

(type_const expr.expr_loc (Const_tag l)) in

414

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

415

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

416

expr.expr_type < touts;

417

touts

418

 Expr_fby (e1,e2)

419

 Expr_arrow (e1,e2) >

420

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

421

check_constant expr.expr_loc const false;

422

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

423

expr.expr_type < ty;

424

ty

425

 Expr_pre e >

426

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

427

check_constant expr.expr_loc const false;

428

let ty = type_standard_args env in_main const [e] in

429

expr.expr_type < ty;

430

ty

431

 Expr_when (e1,c,l) >

432

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

433

check_constant expr.expr_loc const false;

434

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

435

let expr_c = expr_of_ident c expr.expr_loc in

436

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

437

update_clock env in_main c expr.expr_loc typ_l;

438

let ty = type_standard_args env in_main const [e1] in

439

expr.expr_type < ty;

440

ty

441

 Expr_merge (c,hl) >

442

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

443

check_constant expr.expr_loc const false;

444

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

445

let expr_c = expr_of_ident c expr.expr_loc in

446

let typ_l = Type_predef.type_clock typ_in in

447

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

448

update_clock env in_main c expr.expr_loc typ_l;

449

expr.expr_type < typ_out;

450

typ_out

451

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

452

let ty = type_expr env in_main const e in

453

expr.expr_type < ty;

454

ty

455

 Expr_phclock (e,q) >

456

let ty = type_expr env in_main const e in

457

expr.expr_type < ty;

458

ty

459

in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res

460


461

and type_branches env in_main loc const hl =

462

let typ_in = new_var () in

463

let typ_out = new_var () in

464

try

465

let used_labels =

466

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

467

unify typ_in (type_const loc (Const_tag t));

468

type_subtyping_arg env in_main const h typ_out;

469

if List.mem t accu

470

then raise (Error (loc, Already_bound t))

471

else t :: accu) [] hl in

472

let type_labels = get_enum_type_tags (coretype_type typ_in) in

473

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

474

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

475

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

476

else (typ_in, typ_out)

477

with Unify (t1, t2) >

478

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

479


480

and update_clock env in_main id loc typ =

481

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

482

try

483

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

484

in vdecl.var_type < typ

485

with

486

Not_found >

487

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

488


489

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

490

let type_eq env in_main undefined_vars eq =

491

(* Check undefined variables, type lhs *)

492

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

493

let ty_lhs = type_expr env in_main false expr_lhs in

494

(* Check multiple variable definitions *)

495

let define_var id uvars =

496

try

497

ignore(IMap.find id uvars);

498

IMap.remove id uvars

499

with Not_found >

500

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

501

in

502

let undefined_vars =

503

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

504

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

505

to a (always nonconstant) lhs variable *)

506

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

507

undefined_vars

508


509


510

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

511

in environment [env] *)

512

let type_coreclock env ck id loc =

513

match ck.ck_dec_desc with

514

 Ckdec_any  Ckdec_pclock (_,_) > ()

515

 Ckdec_bool cl >

516

let dummy_id_expr = expr_of_ident id loc in

517

let when_expr =

518

List.fold_left

519

(fun expr (x, l) >

520

{expr_tag = new_tag ();

521

expr_desc= Expr_when (expr,x,l);

522

expr_type = new_var ();

523

expr_clock = Clocks.new_var true;

524

expr_delay = Delay.new_var ();

525

expr_loc=loc;

526

expr_annot = None})

527

dummy_id_expr cl

528

in

529

ignore (type_expr env false false when_expr)

530


531

let rec check_type_declaration loc cty =

532

match cty with

533

 Tydec_clock ty

534

 Tydec_array (_, ty) > check_type_declaration loc ty

535

 Tydec_const tname >

536

if not (Hashtbl.mem type_table cty)

537

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

538

 _ > ()

539


540

let type_var_decl vd_env env vdecl =

541

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

542

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

543

let type_dim d =

544

begin

545

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

546

Dimension.eval Basic_library.eval_env eval_const d;

547

end in

548

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

549

let ty_status =

550

if vdecl.var_dec_const

551

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

552

else ty in

553

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

554

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

555

vdecl.var_type < ty_status;

556

new_env

557


558

let type_var_decl_list vd_env env l =

559

List.fold_left (type_var_decl vd_env) env l

560


561

let type_of_vlist vars =

562

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

563

type_of_type_list tyl

564


565

let add_vdecl vd_env vdecl =

566

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

567

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

568

else vdecl::vd_env

569


570

let check_vd_env vd_env =

571

ignore (List.fold_left add_vdecl [] vd_env)

572


573

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

574

location is used for error reports. *)

575

let type_node env nd loc =

576

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

577

let vd_env_ol = nd.node_outputs@nd.node_locals in

578

let vd_env = nd.node_inputs@vd_env_ol in

579

check_vd_env vd_env;

580

let init_env = env in

581

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

582

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

583

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

584

let new_env = Env.overwrite env delta_env in

585

let undefined_vars_init =

586

List.fold_left

587

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

588

IMap.empty vd_env_ol in

589

let undefined_vars =

590

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

591

in

592

(* check that table is empty *)

593

if (not (IMap.is_empty undefined_vars)) then

594

raise (Error (loc, Undefined_var undefined_vars));

595

let ty_ins = type_of_vlist nd.node_inputs in

596

let ty_outs = type_of_vlist nd.node_outputs in

597

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

598

generalize ty_node;

599

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

600

nd.node_type < ty_node;

601

Env.add_value env nd.node_id ty_node

602


603

let type_imported_node env nd loc =

604

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

605

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

606

check_vd_env vd_env;

607

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

608

let ty_ins = type_of_vlist nd.nodei_inputs in

609

let ty_outs = type_of_vlist nd.nodei_outputs in

610

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

611

generalize ty_node;

612

(*

613

if (is_polymorphic ty_node) then

614

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

615

*)

616

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

617

nd.nodei_type < ty_node;

618

new_env

619


620

let type_imported_fun env nd loc =

621

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

622

let vd_env = nd.fun_inputs@nd.fun_outputs in

623

check_vd_env vd_env;

624

ignore(type_var_decl_list vd_env new_env nd.fun_outputs);

625

let ty_ins = type_of_vlist nd.fun_inputs in

626

let ty_outs = type_of_vlist nd.fun_outputs in

627

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

628

generalize ty_node;

629

(*

630

if (is_polymorphic ty_node) then

631

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

632

*)

633

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

634

nd.fun_type < ty_node;

635

new_env

636


637

let type_top_consts env clist =

638

List.fold_left (fun env cdecl >

639

let ty = type_const cdecl.const_loc cdecl.const_value in

640

let d =

641

if is_dimension_type ty

642

then dimension_of_const cdecl.const_loc cdecl.const_value

643

else Dimension.mkdim_var () in

644

let ty = Type_predef.type_static d ty in

645

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

646

cdecl.const_type < ty;

647

new_env) env clist

648


649

let type_top_decl env decl =

650

match decl.top_decl_desc with

651

 Node nd > (

652

try

653

type_node env nd decl.top_decl_loc

654

with Error (loc, err) as exc > (

655

if !Options.global_inline then

656

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

657

Printers.pp_node nd

658

;

659

raise exc)

660

)

661

 ImportedNode nd >

662

type_imported_node env nd decl.top_decl_loc

663

 ImportedFun nd >

664

type_imported_fun env nd decl.top_decl_loc

665

 Consts clist >

666

type_top_consts env clist

667

 Open _ > env

668


669

let type_prog env decls =

670

try

671

List.fold_left type_top_decl env decls

672

with Failure _ as exc > raise exc

673


674

(* Once the Lustre program is fully typed,

675

we must get back to the original description of dimensions,

676

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

677


678

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

679

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

680

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

681

*)

682

let uneval_vdecl_generics vdecl =

683

if vdecl.var_dec_const

684

then

685

match get_static_value vdecl.var_type with

686

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

687

 Some d > Dimension.uneval vdecl.var_id d

688


689

let uneval_node_generics vdecls =

690

List.iter uneval_vdecl_generics vdecls

691


692

let uneval_top_generics decl =

693

match decl.top_decl_desc with

694

 Node nd >

695

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

696

 ImportedNode nd >

697

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

698

 ImportedFun nd >

699

()

700

 Consts clist > ()

701

 Open _ > ()

702


703

let uneval_prog_generics prog =

704

List.iter uneval_top_generics prog

705


706

let check_env_compat header declared computed =

707

uneval_prog_generics header;

708

Env.iter declared (fun k decl_type_k >

709

let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in

710

(*Types.print_ty Format.std_formatter decl_type_k;

711

Types.print_ty Format.std_formatter computed_t;*)

712

try_semi_unify decl_type_k computed_t Location.dummy_loc

713

)

714


715

(* Local Variables: *)

716

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

717

(* End: *)
