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

semi_unify t1 t1';

216

semi_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 > Some (Dimension.mkdim_ident Location.dummy_loc c)) e1;

241

Dimension.eval Basic_library.eval_env (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) 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 try_semi_unify ty1 ty2 loc =

256

try

257

semi_unify ty1 ty2

258

with

259

 Unify _ >

260

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

261

 Dimension.Unify _ >

262

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

263


264

let rec type_const loc c =

265

match c with

266

 Const_int _ > Type_predef.type_int

267

 Const_real _ > Type_predef.type_real

268

 Const_float _ > Type_predef.type_real

269

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

270

let ty = new_var () in

271

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

272

Type_predef.type_array d ty

273

 Const_tag t >

274

if Hashtbl.mem tag_table t

275

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

276

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

277


278

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

279

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

280

[env] is a pair composed of:

281

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

282

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

283

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

284

propagation policy in Lustre.

285

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

286

later discovered to be clocks during the typing process.

287

*)

288

let check_constant loc const_expected const_real =

289

if const_expected && not const_real

290

then raise (Error (loc, Not_a_constant))

291


292

let rec type_standard_args env in_main const expr_list =

293

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

294

let ty_res = new_var () in

295

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

296

ty_res

297


298

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

299

used during node applications and assignments *)

300

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

301

let loc = real_arg.expr_loc in

302

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

303

let real_type = type_expr env in_main const real_arg in

304

let real_type =

305

if const

306

then let d =

307

if is_dimension_type real_type

308

then dimension_of_expr real_arg

309

else Dimension.mkdim_var () in

310

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

311

Dimension.eval Basic_library.eval_env eval_const d;

312

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

313

(match Types.get_static_value real_type with

314

 None > ()

315

 Some d' > try_unify real_type real_static_type loc);

316

real_static_type

317

else real_type in

318

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

319

let real_types = type_list_of_type real_type in

320

let formal_types = type_list_of_type formal_type in

321

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

322

then raise (Unify (real_type, formal_type))

323

else List.iter2 (type_subtyping loc sub) real_types formal_types

324


325

and type_subtyping loc sub real_type formal_type =

326

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

327

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

328

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

329

 _ > try_unify formal_type real_type loc

330


331

and type_ident env in_main loc const id =

332

type_expr env in_main const (expr_of_ident id loc)

333


334

(* typing an application implies:

335

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

336

 checking type adequation between formal and real arguments

337

*)

338

and type_appl env in_main loc const f args =

339

let tfun = type_ident env in_main loc const f in

340

let tins, touts = split_arrow tfun in

341

let tins = type_list_of_type tins in

342

let args = expr_list_of_expr args in

343

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

344

touts

345


346

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

347

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

348

and type_expr env in_main const expr =

349

let res =

350

match expr.expr_desc with

351

 Expr_const c >

352

let ty = type_const expr.expr_loc c in

353

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

354

expr.expr_type < ty;

355

ty

356

 Expr_ident v >

357

let tyv =

358

try

359

Env.lookup_value (fst env) v

360

with Not_found >

361

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

362

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

363

in

364

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

365

let ty' =

366

if const

367

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

368

else new_var () in

369

try_unify ty ty' expr.expr_loc;

370

expr.expr_type < ty;

371

ty

372

 Expr_array elist >

373

let ty_elt = type_standard_args env in_main const elist in

374

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

375

let ty = Type_predef.type_array d ty_elt in

376

expr.expr_type < ty;

377

ty

378

 Expr_access (e1, d) >

379

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

380

let ty_elt = new_var () in

381

let d = Dimension.mkdim_var () in

382

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

383

expr.expr_type < ty_elt;

384

ty_elt

385

 Expr_power (e1, d) >

386

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

387

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

388

Dimension.eval Basic_library.eval_env eval_const d;

389

let ty_elt = type_standard_args env in_main const [e1] in

390

let ty = Type_predef.type_array d ty_elt in

391

expr.expr_type < ty;

392

ty

393

 Expr_tuple elist >

394

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

395

expr.expr_type < ty;

396

ty

397

 Expr_ite (c, t, e) >

398

type_subtyping_arg env in_main const c Type_predef.type_bool;

399

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

400

expr.expr_type < ty;

401

ty

402

 Expr_appl (id, args, r) >

403

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

404

expression *)

405

(match r with

406

 None > ()

407

 Some (x, l) >

408

check_constant expr.expr_loc const false;

409

let expr_x = expr_of_ident x expr.expr_loc in

410

let typ_l =

411

Type_predef.type_clock

412

(type_const expr.expr_loc (Const_tag l)) in

413

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

414

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

415

expr.expr_type < touts;

416

touts

417

 Expr_fby (e1,e2)

418

 Expr_arrow (e1,e2) >

419

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

420

check_constant expr.expr_loc const false;

421

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

422

expr.expr_type < ty;

423

ty

424

 Expr_pre e >

425

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

426

check_constant expr.expr_loc const false;

427

let ty = type_standard_args env in_main const [e] in

428

expr.expr_type < ty;

429

ty

430

 Expr_when (e1,c,l) >

431

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

432

check_constant expr.expr_loc const false;

433

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

434

let expr_c = expr_of_ident c expr.expr_loc in

435

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

436

update_clock env in_main c expr.expr_loc typ_l;

437

let ty = type_standard_args env in_main const [e1] in

438

expr.expr_type < ty;

439

ty

440

 Expr_merge (c,hl) >

441

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

442

check_constant expr.expr_loc const false;

443

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

444

let expr_c = expr_of_ident c expr.expr_loc in

445

let typ_l = Type_predef.type_clock typ_in in

446

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

447

update_clock env in_main c expr.expr_loc typ_l;

448

expr.expr_type < typ_out;

449

typ_out

450

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

451

let ty = type_expr env in_main const e in

452

expr.expr_type < ty;

453

ty

454

 Expr_phclock (e,q) >

455

let ty = type_expr env in_main const e in

456

expr.expr_type < ty;

457

ty

458

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

459


460

and type_branches env in_main loc const hl =

461

let typ_in = new_var () in

462

let typ_out = new_var () in

463

try

464

let used_labels =

465

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

466

unify typ_in (type_const loc (Const_tag t));

467

type_subtyping_arg env in_main const h typ_out;

468

if List.mem t accu

469

then raise (Error (loc, Already_bound t))

470

else t :: accu) [] hl in

471

let type_labels = get_enum_type_tags (coretype_type typ_in) in

472

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

473

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

474

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

475

else (typ_in, typ_out)

476

with Unify (t1, t2) >

477

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

478


479

and update_clock env in_main id loc typ =

480

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

481

try

482

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

483

in vdecl.var_type < typ

484

with

485

Not_found >

486

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

487


488

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

489

let type_eq env in_main undefined_vars eq =

490

(* Check undefined variables, type lhs *)

491

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

492

let ty_lhs = type_expr env in_main false expr_lhs in

493

(* Check multiple variable definitions *)

494

let define_var id uvars =

495

try

496

ignore(IMap.find id uvars);

497

IMap.remove id uvars

498

with Not_found >

499

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

500

in

501

let undefined_vars =

502

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

503

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

504

to a (always nonconstant) lhs variable *)

505

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

506

undefined_vars

507


508


509

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

510

in environment [env] *)

511

let type_coreclock env ck id loc =

512

match ck.ck_dec_desc with

513

 Ckdec_any  Ckdec_pclock (_,_) > ()

514

 Ckdec_bool cl >

515

let dummy_id_expr = expr_of_ident id loc in

516

let when_expr =

517

List.fold_left

518

(fun expr (x, l) >

519

{expr_tag = new_tag ();

520

expr_desc= Expr_when (expr,x,l);

521

expr_type = new_var ();

522

expr_clock = Clocks.new_var true;

523

expr_delay = Delay.new_var ();

524

expr_loc=loc;

525

expr_annot = None})

526

dummy_id_expr cl

527

in

528

ignore (type_expr env false false when_expr)

529


530

let rec check_type_declaration loc cty =

531

match cty with

532

 Tydec_clock ty

533

 Tydec_array (_, ty) > check_type_declaration loc ty

534

 Tydec_const tname >

535

if not (Hashtbl.mem type_table cty)

536

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

537

 _ > ()

538


539

let type_var_decl vd_env env vdecl =

540

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

541

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

542

let type_dim d =

543

begin

544

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

545

Dimension.eval Basic_library.eval_env eval_const d;

546

end in

547

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

548

let ty_status =

549

if vdecl.var_dec_const

550

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

551

else ty in

552

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

553

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

554

vdecl.var_type < ty_status;

555

new_env

556


557

let type_var_decl_list vd_env env l =

558

List.fold_left (type_var_decl vd_env) env l

559


560

let type_of_vlist vars =

561

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

562

type_of_type_list tyl

563


564

let add_vdecl vd_env vdecl =

565

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

566

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

567

else vdecl::vd_env

568


569

let check_vd_env vd_env =

570

ignore (List.fold_left add_vdecl [] vd_env)

571


572

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

573

location is used for error reports. *)

574

let type_node env nd loc =

575

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

576

let vd_env_ol = nd.node_outputs@nd.node_locals in

577

let vd_env = nd.node_inputs@vd_env_ol in

578

check_vd_env vd_env;

579

let init_env = env in

580

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

581

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

582

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

583

let new_env = Env.overwrite env delta_env in

584

let undefined_vars_init =

585

List.fold_left

586

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

587

IMap.empty vd_env_ol in

588

let undefined_vars =

589

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

590

in

591

(* check that table is empty *)

592

if (not (IMap.is_empty undefined_vars)) then

593

raise (Error (loc, Undefined_var undefined_vars));

594

let ty_ins = type_of_vlist nd.node_inputs in

595

let ty_outs = type_of_vlist nd.node_outputs in

596

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

597

generalize ty_node;

598

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

599

nd.node_type < ty_node;

600

Env.add_value env nd.node_id ty_node

601


602

let type_imported_node env nd loc =

603

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

604

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

605

check_vd_env vd_env;

606

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

607

let ty_ins = type_of_vlist nd.nodei_inputs in

608

let ty_outs = type_of_vlist nd.nodei_outputs in

609

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

610

generalize ty_node;

611

(*

612

if (is_polymorphic ty_node) then

613

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

614

*)

615

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

616

nd.nodei_type < ty_node;

617

new_env

618


619

let type_imported_fun env nd loc =

620

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

621

let vd_env = nd.fun_inputs@nd.fun_outputs in

622

check_vd_env vd_env;

623

ignore(type_var_decl_list vd_env new_env nd.fun_outputs);

624

let ty_ins = type_of_vlist nd.fun_inputs in

625

let ty_outs = type_of_vlist nd.fun_outputs in

626

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

627

generalize ty_node;

628

(*

629

if (is_polymorphic ty_node) then

630

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

631

*)

632

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

633

nd.fun_type < ty_node;

634

new_env

635


636

let type_top_consts env clist =

637

List.fold_left (fun env cdecl >

638

let ty = type_const cdecl.const_loc cdecl.const_value in

639

let d =

640

if is_dimension_type ty

641

then dimension_of_const cdecl.const_loc cdecl.const_value

642

else Dimension.mkdim_var () in

643

let ty = Type_predef.type_static d ty in

644

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

645

cdecl.const_type < ty;

646

new_env) env clist

647


648

let type_top_decl env decl =

649

match decl.top_decl_desc with

650

 Node nd > (

651

try

652

type_node env nd decl.top_decl_loc

653

with Error (loc, err) as exc > (

654

if !Options.global_inline then

655

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

656

Printers.pp_node nd

657

;

658

raise exc)

659

)

660

 ImportedNode nd >

661

type_imported_node env nd decl.top_decl_loc

662

 ImportedFun nd >

663

type_imported_fun env nd decl.top_decl_loc

664

 Consts clist >

665

type_top_consts env clist

666

 Open _ > env

667


668

let type_prog env decls =

669

try

670

List.fold_left type_top_decl env decls

671

with Failure _ as exc > raise exc

672


673

(* Once the Lustre program is fully typed,

674

we must get back to the original description of dimensions,

675

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

676


677

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

678

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

679

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

680

*)

681

let uneval_vdecl_generics vdecl =

682

if vdecl.var_dec_const

683

then

684

match get_static_value vdecl.var_type with

685

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

686

 Some d > Dimension.uneval vdecl.var_id d

687


688

let uneval_node_generics vdecls =

689

List.iter uneval_vdecl_generics vdecls

690


691

let uneval_top_generics decl =

692

match decl.top_decl_desc with

693

 Node nd >

694

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

695

 ImportedNode nd >

696

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

697

 ImportedFun nd >

698

()

699

 Consts clist > ()

700

 Open _ > ()

701


702

let uneval_prog_generics prog =

703

List.iter uneval_top_generics prog

704


705

let check_env_compat header declared computed =

706

uneval_prog_generics header;

707

Env.iter declared (fun k decl_type_k >

708

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

709

(*Types.print_ty Format.std_formatter decl_type_k;

710

Types.print_ty Format.std_formatter computed_t;*)

711

try_semi_unify decl_type_k computed_t Location.dummy_loc

712

)

713


714

(* Local Variables: *)

715

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

716

(* End: *)
