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

let real_types = type_list_of_type real_type in

311

let formal_types = type_list_of_type formal_type in

312

try

313

List.iter2 (type_subtyping loc sub) real_types formal_types

314

with _ > raise (Unify (real_type, formal_type))

315


316

and type_subtyping loc sub real_type formal_type =

317

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

318

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

319

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

320

 _ > try_unify formal_type real_type loc

321


322

and type_ident env in_main loc const id =

323

type_expr env in_main const (expr_of_ident id loc)

324


325

(* typing an application implies:

326

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

327

 checking type adequation between formal and real arguments

328

*)

329

and type_appl env in_main loc const f args =

330

let tfun = type_ident env in_main loc const f in

331

let tins, touts = split_arrow tfun in

332

let tins = type_list_of_type tins in

333

let args = expr_list_of_expr args in

334

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

335

touts

336


337

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

338

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

339

and type_expr env in_main const expr =

340

let res =

341

match expr.expr_desc with

342

 Expr_const c >

343

let ty = type_const expr.expr_loc c in

344

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

345

expr.expr_type < ty;

346

ty

347

 Expr_ident v >

348

let tyv =

349

try

350

Env.lookup_value (fst env) v

351

with Not_found >

352

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

353

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

354

in

355

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

356

let ty' =

357

if const

358

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

359

else new_var () in

360

try_unify ty ty' expr.expr_loc;

361

expr.expr_type < ty;

362

ty

363

 Expr_array elist >

364

let ty_elt = type_standard_args env in_main const elist in

365

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

366

let ty = Type_predef.type_array d ty_elt in

367

expr.expr_type < ty;

368

ty

369

 Expr_access (e1, d) >

370

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

371

let ty_elt = new_var () in

372

let d = Dimension.mkdim_var () in

373

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

374

expr.expr_type < ty_elt;

375

ty_elt

376

 Expr_power (e1, d) >

377

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

378

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

379

Dimension.eval Basic_library.eval_env eval_const d;

380

let ty_elt = type_standard_args env in_main const [e1] in

381

let ty = Type_predef.type_array d ty_elt in

382

expr.expr_type < ty;

383

ty

384

 Expr_tuple elist >

385

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

386

expr.expr_type < ty;

387

ty

388

 Expr_ite (c, t, e) >

389

type_subtyping_arg env in_main const c Type_predef.type_bool;

390

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

391

expr.expr_type < ty;

392

ty

393

 Expr_appl (id, args, r) >

394

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

395

expression *)

396

(match r with

397

 None > ()

398

 Some (x, l) >

399

check_constant expr.expr_loc const false;

400

let expr_x = expr_of_ident x expr.expr_loc in

401

let typ_l =

402

Type_predef.type_clock

403

(type_const expr.expr_loc (Const_tag l)) in

404

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

405

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

406

expr.expr_type < touts;

407

touts

408

 Expr_fby (e1,e2)

409

 Expr_arrow (e1,e2) >

410

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

411

check_constant expr.expr_loc const false;

412

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

413

expr.expr_type < ty;

414

ty

415

 Expr_pre e >

416

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

417

check_constant expr.expr_loc const false;

418

let ty = type_standard_args env in_main const [e] in

419

expr.expr_type < ty;

420

ty

421

 Expr_when (e1,c,l) >

422

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

423

check_constant expr.expr_loc const false;

424

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

425

let expr_c = expr_of_ident c expr.expr_loc in

426

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

427

update_clock env in_main c expr.expr_loc typ_l;

428

let ty = type_standard_args env in_main const [e1] in

429

expr.expr_type < ty;

430

ty

431

 Expr_merge (c,hl) >

432

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

433

check_constant expr.expr_loc const false;

434

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

435

let expr_c = expr_of_ident c expr.expr_loc in

436

let typ_l = Type_predef.type_clock typ_in in

437

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

438

update_clock env in_main c expr.expr_loc typ_l;

439

expr.expr_type < typ_out;

440

typ_out

441

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

442

let ty = type_expr env in_main const e in

443

expr.expr_type < ty;

444

ty

445

 Expr_phclock (e,q) >

446

let ty = type_expr env in_main const e in

447

expr.expr_type < ty;

448

ty

449

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

450


451

and type_branches env in_main loc const hl =

452

let typ_in = new_var () in

453

let typ_out = new_var () in

454

try

455

let used_labels =

456

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

457

unify typ_in (type_const loc (Const_tag t));

458

type_subtyping_arg env in_main const h typ_out;

459

if List.mem t accu

460

then raise (Error (loc, Already_bound t))

461

else t :: accu) [] hl in

462

let type_labels = get_enum_type_tags (coretype_type typ_in) in

463

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

464

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

465

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

466

else (typ_in, typ_out)

467

with Unify (t1, t2) >

468

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

469


470

and update_clock env in_main id loc typ =

471

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

472

try

473

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

474

in vdecl.var_type < typ

475

with

476

Not_found >

477

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

478


479

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

480

let type_eq env in_main undefined_vars eq =

481

(* Check undefined variables, type lhs *)

482

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

483

let ty_lhs = type_expr env in_main false expr_lhs in

484

(* Check multiple variable definitions *)

485

let define_var id uvars =

486

try

487

ignore(IMap.find id uvars);

488

IMap.remove id uvars

489

with Not_found >

490

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

491

in

492

let undefined_vars =

493

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

494

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

495

to a (always nonconstant) lhs variable *)

496

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

497

undefined_vars

498


499


500

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

501

in environment [env] *)

502

let type_coreclock env ck id loc =

503

match ck.ck_dec_desc with

504

 Ckdec_any  Ckdec_pclock (_,_) > ()

505

 Ckdec_bool cl >

506

let dummy_id_expr = expr_of_ident id loc in

507

let when_expr =

508

List.fold_left

509

(fun expr (x, l) >

510

{expr_tag = new_tag ();

511

expr_desc= Expr_when (expr,x,l);

512

expr_type = new_var ();

513

expr_clock = Clocks.new_var true;

514

expr_delay = Delay.new_var ();

515

expr_loc=loc;

516

expr_annot = None})

517

dummy_id_expr cl

518

in

519

Format.eprintf "yiihii@.";

520

ignore (type_expr env false false when_expr)

521


522

let rec check_type_declaration loc cty =

523

match cty with

524

 Tydec_clock ty

525

 Tydec_array (_, ty) > check_type_declaration loc ty

526

 Tydec_const tname >

527

if not (Hashtbl.mem type_table cty)

528

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

529

 _ > ()

530


531

let type_var_decl vd_env env vdecl =

532

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

533

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

534

let type_dim d =

535

begin

536

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

537

Dimension.eval Basic_library.eval_env eval_const d;

538

end in

539

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

540

let ty_status =

541

if vdecl.var_dec_const

542

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

543

else ty in

544

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

545

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

546

vdecl.var_type < ty_status;

547

new_env

548


549

let type_var_decl_list vd_env env l =

550

List.fold_left (type_var_decl vd_env) env l

551


552

let type_of_vlist vars =

553

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

554

type_of_type_list tyl

555


556

let add_vdecl vd_env vdecl =

557

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

558

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

559

else vdecl::vd_env

560


561

let check_vd_env vd_env =

562

ignore (List.fold_left add_vdecl [] vd_env)

563


564

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

565

location is used for error reports. *)

566

let type_node env nd loc =

567

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

568

let vd_env_ol = nd.node_outputs@nd.node_locals in

569

let vd_env = nd.node_inputs@vd_env_ol in

570

check_vd_env vd_env;

571

let init_env = env in

572

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

573

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

574

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

575

let new_env = Env.overwrite env delta_env in

576

let undefined_vars_init =

577

List.fold_left

578

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

579

IMap.empty vd_env_ol in

580

let undefined_vars =

581

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

582

in

583

(* check that table is empty *)

584

if (not (IMap.is_empty undefined_vars)) then

585

raise (Error (loc, Undefined_var undefined_vars));

586

let ty_ins = type_of_vlist nd.node_inputs in

587

let ty_outs = type_of_vlist nd.node_outputs in

588

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

589

generalize ty_node;

590

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

591

nd.node_type < ty_node;

592

Env.add_value env nd.node_id ty_node

593


594

let type_imported_node env nd loc =

595

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

596

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

597

check_vd_env vd_env;

598

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

599

let ty_ins = type_of_vlist nd.nodei_inputs in

600

let ty_outs = type_of_vlist nd.nodei_outputs in

601

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

602

generalize ty_node;

603

(*

604

if (is_polymorphic ty_node) then

605

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

606

*)

607

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

608

nd.nodei_type < ty_node;

609

new_env

610


611

let type_imported_fun env nd loc =

612

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

613

let vd_env = nd.fun_inputs@nd.fun_outputs in

614

check_vd_env vd_env;

615

ignore(type_var_decl_list vd_env new_env nd.fun_outputs);

616

let ty_ins = type_of_vlist nd.fun_inputs in

617

let ty_outs = type_of_vlist nd.fun_outputs in

618

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

619

generalize ty_node;

620

(*

621

if (is_polymorphic ty_node) then

622

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

623

*)

624

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

625

nd.fun_type < ty_node;

626

new_env

627


628

let type_top_consts env clist =

629

List.fold_left (fun env cdecl >

630

let ty = type_const cdecl.const_loc cdecl.const_value in

631

let d =

632

if is_dimension_type ty

633

then dimension_of_const cdecl.const_loc cdecl.const_value

634

else Dimension.mkdim_var () in

635

let ty = Type_predef.type_static d ty in

636

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

637

cdecl.const_type < ty;

638

new_env) env clist

639


640

let type_top_decl env decl =

641

match decl.top_decl_desc with

642

 Node nd >

643

type_node env nd decl.top_decl_loc

644

 ImportedNode nd >

645

type_imported_node env nd decl.top_decl_loc

646

 ImportedFun nd >

647

type_imported_fun env nd decl.top_decl_loc

648

 Consts clist >

649

type_top_consts env clist

650

 Open _ > env

651


652

let type_prog env decls =

653

try

654

List.fold_left type_top_decl env decls

655

with Failure _ as exc > raise exc

656


657

(* Once the Lustre program is fully typed,

658

we must get back to the original description of dimensions,

659

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

660


661

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

662

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

663

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

664

*)

665

(*

666

let uneval_vdecl_generics vdecl ty =

667

if vdecl.var_dec_const

668

then

669

match get_static_value ty with

670

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

671

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

672


673

let uneval_node_generics vdecls =

674

let inst_typ_vars = ref [] in

675

let inst_dim_vars = ref [] in

676

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

677

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

678

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

679

*)

680

let uneval_vdecl_generics vdecl =

681

if vdecl.var_dec_const

682

then

683

match get_static_value vdecl.var_type with

684

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

685

 Some d > Dimension.uneval vdecl.var_id d

686


687

let uneval_node_generics vdecls =

688

List.iter uneval_vdecl_generics vdecls

689


690

let uneval_top_generics decl =

691

match decl.top_decl_desc with

692

 Node nd >

693

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

694

 ImportedNode nd >

695

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

696

 ImportedFun nd >

697

()

698

 Consts clist > ()

699

 Open _ > ()

700


701

let uneval_prog_generics prog =

702

List.iter uneval_top_generics prog

703


704

let check_env_compat declared computed =

705

Env.iter declared (fun k decl_type_k >

706

let computed_t = Env.lookup_value computed k in

707

try_unify decl_type_k computed_t Location.dummy_loc

708

)

709


710

(* Local Variables: *)

711

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

712

(* End: *)
