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_array (d, ty) >

115

begin

116

type_dim d;

117

Type_predef.type_array d (type_coretype type_dim ty)

118

end

119


120

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

121

let rec coretype_type ty =

122

match (repr ty).tdesc with

123

 Tvar > Tydec_any

124

 Tint > Tydec_int

125

 Treal > Tydec_real

126

 Tbool > Tydec_bool

127

 Tconst c > Tydec_const c

128

 Tclock t > Tydec_clock (coretype_type t)

129

 Tenum tl > Tydec_enum tl

130

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

131

 Tstatic (_, t) > coretype_type t

132

 _ > assert false

133


134

let get_type_definition tname =

135

try

136

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

137

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

138


139

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

140

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

141

(* Standard destructive unification *)

142

let rec unify t1 t2 =

143

let t1 = repr t1 in

144

let t2 = repr t2 in

145

if t1=t2 then

146

()

147

else

148

(* No type abbreviations resolution for now *)

149

match t1.tdesc,t2.tdesc with

150

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

151

 Tvar, Tvar >

152

if t1.tid < t2.tid then

153

t2.tdesc < Tlink t1

154

else

155

t1.tdesc < Tlink t2

156

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

157

t1.tdesc < Tlink t2

158

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

159

t2.tdesc < Tlink t1

160

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

161

begin

162

unify t1 t1';

163

unify t2 t2'

164

end

165

 Ttuple tlist1, Ttuple tlist2 >

166

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

167

raise (Unify (t1, t2))

168

else

169

List.iter2 unify tlist1 tlist2

170

 Tclock _, Tstatic _

171

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

172

 Tclock t1', _ > unify t1' t2

173

 _, Tclock t2' > unify t1 t2'

174

 Tint, Tint  Tbool, Tbool  Trat, Trat

175

 Tunivar, _  _, Tunivar > ()

176

 (Tconst t, _) >

177

let def_t = get_type_definition t in

178

unify def_t t2

179

 (_, Tconst t) >

180

let def_t = get_type_definition t in

181

unify t1 def_t

182

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

183

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

184

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

185

begin

186

unify t1' t2';

187

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

188

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

189

Dimension.unify e1 e2;

190

end

191

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

192


193

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

194

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

195

(* Standard destructive semiunification *)

196

let rec semi_unify t1 t2 =

197

let t1 = repr t1 in

198

let t2 = repr t2 in

199

if t1=t2 then

200

()

201

else

202

(* No type abbreviations resolution for now *)

203

match t1.tdesc,t2.tdesc with

204

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

205

 Tvar, Tvar >

206

if t1.tid < t2.tid then

207

t2.tdesc < Tlink t1

208

else

209

t1.tdesc < Tlink t2

210

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

211

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

212

t2.tdesc < Tlink t1

213

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

214

begin

215

unify t1 t1';

216

unify t2 t2'

217

end

218

 Ttuple tlist1, Ttuple tlist2 >

219

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

220

raise (Unify (t1, t2))

221

else

222

List.iter2 semi_unify tlist1 tlist2

223

 Tclock _, Tstatic _

224

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

225

 Tclock t1', _ > semi_unify t1' t2

226

 _, Tclock t2' > semi_unify t1 t2'

227

 Tint, Tint  Tbool, Tbool  Trat, Trat

228

 Tunivar, _  _, Tunivar > ()

229

 (Tconst t, _) >

230

let def_t = get_type_definition t in

231

semi_unify def_t t2

232

 (_, Tconst t) >

233

let def_t = get_type_definition t in

234

semi_unify t1 def_t

235

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

236

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

237

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

238

begin

239

semi_unify t1' t2';

240

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

241

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

242

Dimension.semi_unify e1 e2;

243

end

244

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

245


246

let try_unify ty1 ty2 loc =

247

try

248

unify ty1 ty2

249

with

250

 Unify _ >

251

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

252

 Dimension.Unify _ >

253

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

254


255

let rec type_const loc c =

256

match c with

257

 Const_int _ > Type_predef.type_int

258

 Const_real _ > Type_predef.type_real

259

 Const_float _ > Type_predef.type_real

260

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

261

let ty = new_var () in

262

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

263

Type_predef.type_array d ty

264

 Const_tag t >

265

if Hashtbl.mem tag_table t

266

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

267

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

268


269

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

270

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

271

[env] is a pair composed of:

272

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

273

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

274

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

275

propagation policy in Lustre.

276

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

277

later discovered to be clocks during the typing process.

278

*)

279

let check_constant loc const_expected const_real =

280

if const_expected && not const_real

281

then raise (Error (loc, Not_a_constant))

282


283

let rec type_standard_args env in_main const expr_list =

284

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

285

let ty_res = new_var () in

286

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

287

ty_res

288


289

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

290

used during node applications and assignments *)

291

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

292

let loc = real_arg.expr_loc in

293

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

294

let real_type = type_expr env in_main const real_arg in

295

let real_type =

296

if const

297

then let d =

298

if is_dimension_type real_type

299

then dimension_of_expr real_arg

300

else Dimension.mkdim_var () in

301

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

302

Dimension.eval Basic_library.eval_env eval_const d;

303

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

304

(match Types.get_static_value real_type with

305

 None > ()

306

 Some d' > try_unify real_type real_static_type loc);

307

real_static_type

308

else real_type in

309

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;

310

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

311

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

312

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

313

 _ > try_unify formal_type real_type loc

314


315

and type_ident env in_main loc const id =

316

type_expr env in_main const (expr_of_ident id loc)

317


318

(* typing an application implies:

319

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

320

 checking type adequation between formal and real arguments

321

*)

322

and type_appl env in_main loc const f args =

323

let tfun = type_ident env in_main loc const f in

324

let tins, touts = split_arrow tfun in

325

let tins = type_list_of_type tins in

326

let args = expr_list_of_expr args in

327

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

328

touts

329


330

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

331

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

332

and type_expr env in_main const expr =

333

let res =

334

match expr.expr_desc with

335

 Expr_const c >

336

let ty = type_const expr.expr_loc c in

337

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

338

expr.expr_type < ty;

339

ty

340

 Expr_ident v >

341

let tyv =

342

try

343

Env.lookup_value (fst env) v

344

with Not_found >

345

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

346

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

347

in

348

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

349

let ty' =

350

if const

351

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

352

else new_var () in

353

try_unify ty ty' expr.expr_loc;

354

expr.expr_type < ty;

355

ty

356

 Expr_array elist >

357

let ty_elt = type_standard_args env in_main const elist in

358

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

359

let ty = Type_predef.type_array d ty_elt in

360

expr.expr_type < ty;

361

ty

362

 Expr_access (e1, d) >

363

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

364

let ty_elt = new_var () in

365

let d = Dimension.mkdim_var () in

366

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

367

expr.expr_type < ty_elt;

368

ty_elt

369

 Expr_power (e1, d) >

370

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

371

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

372

Dimension.eval Basic_library.eval_env eval_const d;

373

let ty_elt = type_standard_args env in_main const [e1] in

374

let ty = Type_predef.type_array d ty_elt in

375

expr.expr_type < ty;

376

ty

377

 Expr_tuple elist >

378

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

379

expr.expr_type < ty;

380

ty

381

 Expr_ite (c, t, e) >

382

type_subtyping_arg env in_main const c Type_predef.type_bool;

383

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

384

expr.expr_type < ty;

385

ty

386

 Expr_appl (id, args, r) >

387

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

388

expression *)

389

(match r with

390

 None > ()

391

 Some (x, l) >

392

check_constant expr.expr_loc const false;

393

let expr_x = expr_of_ident x expr.expr_loc in

394

let typ_l =

395

Type_predef.type_clock

396

(type_const expr.expr_loc (Const_tag l)) in

397

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

398

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

399

expr.expr_type < touts;

400

touts

401

 Expr_fby (e1,e2)

402

 Expr_arrow (e1,e2) >

403

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

404

check_constant expr.expr_loc const false;

405

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

406

expr.expr_type < ty;

407

ty

408

 Expr_pre e >

409

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

410

check_constant expr.expr_loc const false;

411

let ty = type_standard_args env in_main const [e] in

412

expr.expr_type < ty;

413

ty

414

 Expr_when (e1,c,l) >

415

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

416

check_constant expr.expr_loc const false;

417

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

418

let expr_c = expr_of_ident c expr.expr_loc in

419

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

420

update_clock env in_main c expr.expr_loc typ_l;

421

let ty = type_standard_args env in_main const [e1] in

422

expr.expr_type < ty;

423

ty

424

 Expr_merge (c,hl) >

425

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

426

check_constant expr.expr_loc const false;

427

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

428

let expr_c = expr_of_ident c expr.expr_loc in

429

let typ_l = Type_predef.type_clock typ_in in

430

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

431

update_clock env in_main c expr.expr_loc typ_l;

432

expr.expr_type < typ_out;

433

typ_out

434

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

435

let ty = type_expr env in_main const e in

436

expr.expr_type < ty;

437

ty

438

 Expr_phclock (e,q) >

439

let ty = type_expr env in_main const e in

440

expr.expr_type < ty;

441

ty

442

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

443


444

and type_branches env in_main loc const hl =

445

let typ_in = new_var () in

446

let typ_out = new_var () in

447

try

448

let used_labels =

449

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

450

unify typ_in (type_const loc (Const_tag t));

451

type_subtyping_arg env in_main const h typ_out;

452

if List.mem t accu

453

then raise (Error (loc, Already_bound t))

454

else t :: accu) [] hl in

455

let type_labels = get_enum_type_tags (coretype_type typ_in) in

456

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

457

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

458

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

459

else (typ_in, typ_out)

460

with Unify (t1, t2) >

461

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

462


463

and update_clock env in_main id loc typ =

464

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

465

try

466

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

467

in vdecl.var_type < typ

468

with

469

Not_found >

470

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

471


472

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

473

let type_eq env in_main undefined_vars eq =

474

(* Check undefined variables, type lhs *)

475

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

476

let ty_lhs = type_expr env in_main false expr_lhs in

477

(* Check multiple variable definitions *)

478

let define_var id uvars =

479

try

480

ignore(IMap.find id uvars);

481

IMap.remove id uvars

482

with Not_found >

483

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

484

in

485

let undefined_vars =

486

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

487

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

488

to a (always nonconstant) lhs variable *)

489

let tins = type_list_of_type ty_lhs in

490

let args = expr_list_of_expr eq.eq_rhs in

491

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

492

undefined_vars

493


494


495

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

496

in environment [env] *)

497

let type_coreclock env ck id loc =

498

match ck.ck_dec_desc with

499

 Ckdec_any  Ckdec_pclock (_,_) > ()

500

 Ckdec_bool cl >

501

let dummy_id_expr = expr_of_ident id loc in

502

let when_expr =

503

List.fold_left

504

(fun expr (x, l) >

505

{expr_tag = new_tag ();

506

expr_desc= Expr_when (expr,x,l);

507

expr_type = new_var ();

508

expr_clock = Clocks.new_var true;

509

expr_delay = Delay.new_var ();

510

expr_loc=loc;

511

expr_annot = None})

512

dummy_id_expr cl

513

in

514

Format.eprintf "yiihii@.";

515

ignore (type_expr env false false when_expr)

516


517

let rec check_type_declaration loc cty =

518

match cty with

519

 Tydec_clock ty

520

 Tydec_array (_, ty) > check_type_declaration loc ty

521

 Tydec_const tname >

522

if not (Hashtbl.mem type_table cty)

523

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

524

 _ > ()

525


526

let type_var_decl vd_env env vdecl =

527

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

528

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

529

let type_dim d =

530

begin

531

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

532

Dimension.eval Basic_library.eval_env eval_const d;

533

end in

534

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

535

let ty_status =

536

if vdecl.var_dec_const

537

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

538

else ty in

539

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

540

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

541

vdecl.var_type < ty_status;

542

new_env

543


544

let type_var_decl_list vd_env env l =

545

List.fold_left (type_var_decl vd_env) env l

546


547

let type_of_vlist vars =

548

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

549

type_of_type_list tyl

550


551

let add_vdecl vd_env vdecl =

552

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

553

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

554

else vdecl::vd_env

555


556

let check_vd_env vd_env =

557

ignore (List.fold_left add_vdecl [] vd_env)

558


559

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

560

location is used for error reports. *)

561

let type_node env nd loc =

562

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

563

let vd_env_ol = nd.node_outputs@nd.node_locals in

564

let vd_env = nd.node_inputs@vd_env_ol in

565

check_vd_env vd_env;

566

let init_env = env in

567

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

568

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

569

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

570

let new_env = Env.overwrite env delta_env in

571

let undefined_vars_init =

572

List.fold_left

573

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

574

IMap.empty vd_env_ol in

575

let undefined_vars =

576

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

577

in

578

(* check that table is empty *)

579

if (not (IMap.is_empty undefined_vars)) then

580

raise (Error (loc, Undefined_var undefined_vars));

581

let ty_ins = type_of_vlist nd.node_inputs in

582

let ty_outs = type_of_vlist nd.node_outputs in

583

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

584

generalize ty_node;

585

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

586

nd.node_type < ty_node;

587

Env.add_value env nd.node_id ty_node

588


589

let type_imported_node env nd loc =

590

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

591

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

592

check_vd_env vd_env;

593

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

594

let ty_ins = type_of_vlist nd.nodei_inputs in

595

let ty_outs = type_of_vlist nd.nodei_outputs in

596

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

597

generalize ty_node;

598

(*

599

if (is_polymorphic ty_node) then

600

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

601

*)

602

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

603

nd.nodei_type < ty_node;

604

new_env

605


606

let type_imported_fun env nd loc =

607

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

608

let vd_env = nd.fun_inputs@nd.fun_outputs in

609

check_vd_env vd_env;

610

ignore(type_var_decl_list vd_env new_env nd.fun_outputs);

611

let ty_ins = type_of_vlist nd.fun_inputs in

612

let ty_outs = type_of_vlist nd.fun_outputs in

613

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

614

generalize ty_node;

615

(*

616

if (is_polymorphic ty_node) then

617

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

618

*)

619

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

620

nd.fun_type < ty_node;

621

new_env

622


623

let type_top_consts env clist =

624

List.fold_left (fun env cdecl >

625

let ty = type_const cdecl.const_loc cdecl.const_value in

626

let d =

627

if is_dimension_type ty

628

then dimension_of_const cdecl.const_loc cdecl.const_value

629

else Dimension.mkdim_var () in

630

let ty = Type_predef.type_static d ty in

631

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

632

cdecl.const_type < ty;

633

new_env) env clist

634


635

let type_top_decl env decl =

636

match decl.top_decl_desc with

637

 Node nd >

638

type_node env nd decl.top_decl_loc

639

 ImportedNode nd >

640

type_imported_node env nd decl.top_decl_loc

641

 ImportedFun nd >

642

type_imported_fun env nd decl.top_decl_loc

643

 Consts clist >

644

type_top_consts env clist

645

 Open _ > env

646


647

let type_prog env decls =

648

try

649

List.fold_left type_top_decl env decls

650

with Failure _ as exc > raise exc

651


652

(* Once the Lustre program is fully typed,

653

we must get back to the original description of dimensions,

654

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

655


656

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

657

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

658

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

659

*)

660

(*

661

let uneval_vdecl_generics vdecl ty =

662

if vdecl.var_dec_const

663

then

664

match get_static_value ty with

665

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

666

 Some d > Dimension.unify d (Dimension.mkdim_ident vdecl.var_loc vdecl.var_id)

667


668

let uneval_node_generics vdecls =

669

let inst_typ_vars = ref [] in

670

let inst_dim_vars = ref [] in

671

let inst_ty_list = List.map (fun v > instantiate inst_typ_vars inst_dim_vars v.var_type) vdecls in

672

List.iter2 (fun v ty > uneval_vdecl_generics v ty) vdecls inst_ty_list;

673

List.iter2 (fun v ty > generalize ty; v.var_type < ty) vdecls inst_ty_list

674

*)

675

let uneval_vdecl_generics vdecl =

676

if vdecl.var_dec_const

677

then

678

match get_static_value vdecl.var_type with

679

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

680

 Some d > Dimension.uneval vdecl.var_id d

681


682

let uneval_node_generics vdecls =

683

List.iter uneval_vdecl_generics vdecls

684


685

let uneval_top_generics decl =

686

match decl.top_decl_desc with

687

 Node nd >

688

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

689

 ImportedNode nd >

690

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

691

 ImportedFun nd >

692

()

693

 Consts clist > ()

694

 Open _ > ()

695


696

let uneval_prog_generics prog =

697

List.iter uneval_top_generics prog

698


699

let check_env_compat declared computed =

700

Env.iter declared (fun k decl_type_k >

701

let computed_t = Env.lookup_value computed k in

702

try_unify decl_type_k computed_t Location.dummy_loc

703

)

704


705

(* Local Variables: *)

706

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

707

(* End: *)
