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 env 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

let try_unify ty1 ty2 loc =

194

try

195

unify ty1 ty2

196

with

197

 Unify _ >

198

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

199

 Dimension.Unify _ >

200

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

201


202

let rec type_const loc c =

203

match c with

204

 Const_int _ > Type_predef.type_int

205

 Const_real _ > Type_predef.type_real

206

 Const_float _ > Type_predef.type_real

207

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

208

let ty = new_var () in

209

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

210

Type_predef.type_array d ty

211

 Const_tag t >

212

if Hashtbl.mem tag_table t

213

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

214

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

215


216

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

217

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

218

[env] is a pair composed of:

219

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

220

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

221

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

222

propagation policy in Lustre.

223

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

224

later discovered to be clocks during the typing process.

225

*)

226

let check_constant loc const_expected const_real =

227

if const_expected && not const_real

228

then raise (Error (loc, Not_a_constant))

229


230

let rec type_standard_args env in_main const expr_list =

231

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

232

let ty_res = new_var () in

233

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

234

ty_res

235


236

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

237

used during node application only *)

238

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

239

let loc = real_arg.expr_loc in

240

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

241

let real_type = type_expr env in_main const real_arg in

242

let real_type =

243

if const

244

then let d =

245

if is_dimension_type real_type

246

then dimension_of_expr real_arg

247

else Dimension.mkdim_var () in

248

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

249

Dimension.eval Basic_library.eval_env eval_const d;

250

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

251

(match Types.get_static_value real_type with

252

 None > ()

253

 Some d' > try_unify real_type real_static_type loc);

254

real_static_type

255

else real_type in

256

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

257

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

258

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

259

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

260

 _ > try_unify formal_type real_type loc

261


262

and type_ident env in_main loc const id =

263

type_expr env in_main const (expr_of_ident id loc)

264


265

(* typing an application implies:

266

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

267

 checking type adequation between formal and real arguments

268

*)

269

and type_appl env in_main loc const f args =

270

let tfun = type_ident env in_main loc const f in

271

let tins, touts = split_arrow tfun in

272

let tins = type_list_of_type tins in

273

let args = expr_list_of_expr args in

274

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

275

touts

276


277

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

278

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

279

and type_expr env in_main const expr =

280

let res =

281

match expr.expr_desc with

282

 Expr_const c >

283

let ty = type_const expr.expr_loc c in

284

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

285

expr.expr_type < ty;

286

ty

287

 Expr_ident v >

288

let tyv =

289

try

290

Env.lookup_value (fst env) v

291

with Not_found >

292

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

293

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

294

in

295

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

296

let ty' =

297

if const

298

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

299

else new_var () in

300

try_unify ty ty' expr.expr_loc;

301

expr.expr_type < ty;

302

ty

303

 Expr_array elist >

304

let ty_elt = type_standard_args env in_main const elist in

305

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

306

let ty = Type_predef.type_array d ty_elt in

307

expr.expr_type < ty;

308

ty

309

 Expr_access (e1, d) >

310

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

311

let ty_elt = new_var () in

312

let d = Dimension.mkdim_var () in

313

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

314

expr.expr_type < ty_elt;

315

ty_elt

316

 Expr_power (e1, d) >

317

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

318

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

319

Dimension.eval Basic_library.eval_env eval_const d;

320

let ty_elt = type_standard_args env in_main const [e1] in

321

let ty = Type_predef.type_array d ty_elt in

322

expr.expr_type < ty;

323

ty

324

 Expr_tuple elist >

325

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

326

expr.expr_type < ty;

327

ty

328

 Expr_ite (c, t, e) >

329

type_subtyping_arg env in_main const c Type_predef.type_bool;

330

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

331

expr.expr_type < ty;

332

ty

333

 Expr_appl (id, args, r) >

334

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

335

expression *)

336

(match r with

337

 None > ()

338

 Some (x, l) >

339

check_constant expr.expr_loc const false;

340

let expr_x = expr_of_ident x expr.expr_loc in

341

let typ_l =

342

Type_predef.type_clock

343

(type_const expr.expr_loc (Const_tag l)) in

344

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

345

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

346

expr.expr_type < touts;

347

touts

348

 Expr_fby (e1,e2)

349

 Expr_arrow (e1,e2) >

350

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

351

check_constant expr.expr_loc const false;

352

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

353

expr.expr_type < ty;

354

ty

355

 Expr_pre e >

356

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

357

check_constant expr.expr_loc const false;

358

let ty = type_standard_args env in_main const [e] in

359

expr.expr_type < ty;

360

ty

361

 Expr_when (e1,c,l) >

362

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

363

check_constant expr.expr_loc const false;

364

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

365

let expr_c = expr_of_ident c expr.expr_loc in

366

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

367

update_clock env in_main c expr.expr_loc typ_l;

368

let ty = type_standard_args env in_main const [e1] in

369

expr.expr_type < ty;

370

ty

371

 Expr_merge (c,hl) >

372

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

373

check_constant expr.expr_loc const false;

374

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

375

let expr_c = expr_of_ident c expr.expr_loc in

376

let typ_l = Type_predef.type_clock typ_in in

377

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

378

update_clock env in_main c expr.expr_loc typ_l;

379

expr.expr_type < typ_out;

380

typ_out

381

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

382

let ty = type_expr env in_main const e in

383

expr.expr_type < ty;

384

ty

385

 Expr_phclock (e,q) >

386

let ty = type_expr env in_main const e in

387

expr.expr_type < ty;

388

ty

389

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

390


391

and type_branches env in_main loc const hl =

392

let typ_in = new_var () in

393

let typ_out = new_var () in

394

try

395

let used_labels =

396

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

397

unify typ_in (type_const loc (Const_tag t));

398

type_subtyping_arg env in_main const h typ_out;

399

if List.mem t accu

400

then raise (Error (loc, Already_bound t))

401

else t :: accu) [] hl in

402

let type_labels = get_enum_type_tags (coretype_type typ_in) in

403

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

404

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

405

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

406

else (typ_in, typ_out)

407

with Unify (t1, t2) >

408

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

409


410

and update_clock env in_main id loc typ =

411

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

412

try

413

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

414

in vdecl.var_type < typ

415

with

416

Not_found >

417

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

418


419

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

420

let type_eq env in_main undefined_vars eq =

421

(* Check undefined variables, type lhs *)

422

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

423

let ty_lhs = type_expr env in_main false expr_lhs in

424

(* Check multiple variable definitions *)

425

let define_var id uvars =

426

try

427

ignore(IMap.find id uvars);

428

IMap.remove id uvars

429

with Not_found >

430

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

431

in

432

let undefined_vars =

433

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

434

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

435

to a (always nonconstant) lhs variable *)

436

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

437

undefined_vars

438


439


440

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

441

in environment [env] *)

442

let type_coreclock env ck id loc =

443

match ck.ck_dec_desc with

444

 Ckdec_any  Ckdec_pclock (_,_) > ()

445

 Ckdec_bool cl >

446

let dummy_id_expr = expr_of_ident id loc in

447

let when_expr =

448

List.fold_left

449

(fun expr (x, l) >

450

{expr_tag = new_tag ();

451

expr_desc= Expr_when (expr,x,l);

452

expr_type = new_var ();

453

expr_clock = Clocks.new_var true;

454

expr_delay = Delay.new_var ();

455

expr_loc=loc;

456

expr_annot = None})

457

dummy_id_expr cl

458

in

459

Format.eprintf "yiihii@.";

460

ignore (type_expr env false false when_expr)

461


462

let rec check_type_declaration loc cty =

463

match cty with

464

 Tydec_clock ty

465

 Tydec_array (_, ty) > check_type_declaration loc ty

466

 Tydec_const tname >

467

if not (Hashtbl.mem type_table cty)

468

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

469

 _ > ()

470


471

let type_var_decl vd_env env vdecl =

472

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

473

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

474

let type_dim d =

475

begin

476

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

477

Dimension.eval Basic_library.eval_env eval_const d;

478

end in

479

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

480

let ty_status =

481

if vdecl.var_dec_const

482

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

483

else ty in

484

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

485

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

486

vdecl.var_type < ty_status;

487

new_env

488


489

let type_var_decl_list vd_env env l =

490

List.fold_left (type_var_decl vd_env) env l

491


492

let type_of_vlist vars =

493

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

494

type_of_type_list tyl

495


496

let add_vdecl vd_env vdecl =

497

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

498

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

499

else vdecl::vd_env

500


501

let check_vd_env vd_env =

502

ignore (List.fold_left add_vdecl [] vd_env)

503


504

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

505

location is used for error reports. *)

506

let type_node env nd loc =

507

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

508

let vd_env_ol = nd.node_outputs@nd.node_locals in

509

let vd_env = nd.node_inputs@vd_env_ol in

510

check_vd_env vd_env;

511

let init_env = env in

512

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

513

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

514

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

515

let new_env = Env.overwrite env delta_env in

516

let undefined_vars_init =

517

List.fold_left

518

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

519

IMap.empty vd_env_ol in

520

let undefined_vars =

521

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

522

in

523

(* check that table is empty *)

524

if (not (IMap.is_empty undefined_vars)) then

525

raise (Error (loc, Undefined_var undefined_vars));

526

let ty_ins = type_of_vlist nd.node_inputs in

527

let ty_outs = type_of_vlist nd.node_outputs in

528

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

529

generalize ty_node;

530

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

531

nd.node_type < ty_node;

532

Env.add_value env nd.node_id ty_node

533


534

let type_imported_node env nd loc =

535

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

536

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

537

check_vd_env vd_env;

538

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

539

let ty_ins = type_of_vlist nd.nodei_inputs in

540

let ty_outs = type_of_vlist nd.nodei_outputs in

541

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

542

generalize ty_node;

543

(*

544

if (is_polymorphic ty_node) then

545

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

546

*)

547

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

548

nd.nodei_type < ty_node;

549

new_env

550


551

let type_imported_fun env nd loc =

552

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

553

let vd_env = nd.fun_inputs@nd.fun_outputs in

554

check_vd_env vd_env;

555

ignore(type_var_decl_list vd_env new_env nd.fun_outputs);

556

let ty_ins = type_of_vlist nd.fun_inputs in

557

let ty_outs = type_of_vlist nd.fun_outputs in

558

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

559

generalize ty_node;

560

(*

561

if (is_polymorphic ty_node) then

562

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

563

*)

564

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

565

nd.fun_type < ty_node;

566

new_env

567


568

let type_top_consts env clist =

569

List.fold_left (fun env cdecl >

570

let ty = type_const cdecl.const_loc cdecl.const_value in

571

let d =

572

if is_dimension_type ty

573

then dimension_of_const cdecl.const_loc cdecl.const_value

574

else Dimension.mkdim_var () in

575

let ty = Type_predef.type_static d ty in

576

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

577

cdecl.const_type < ty;

578

new_env) env clist

579


580

let type_top_decl env decl =

581

match decl.top_decl_desc with

582

 Node nd >

583

type_node env nd decl.top_decl_loc

584

 ImportedNode nd >

585

type_imported_node env nd decl.top_decl_loc

586

 ImportedFun nd >

587

type_imported_fun env nd decl.top_decl_loc

588

 Consts clist >

589

type_top_consts env clist

590

 Open _ > env

591


592

let type_prog env decls =

593

try

594

List.fold_left type_top_decl env decls

595

with Failure _ as exc > raise exc

596


597

(* Once the Lustre program is fully typed,

598

we must get back to the original description of dimensions,

599

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

600


601

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

602

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

603

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

604

*)

605

(*

606

let uneval_vdecl_generics vdecl ty =

607

if vdecl.var_dec_const

608

then

609

match get_static_value ty with

610

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

611

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

612


613

let uneval_node_generics vdecls =

614

let inst_typ_vars = ref [] in

615

let inst_dim_vars = ref [] in

616

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

617

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

618

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

619

*)

620

let uneval_vdecl_generics vdecl =

621

if vdecl.var_dec_const

622

then

623

match get_static_value vdecl.var_type with

624

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

625

 Some d > Dimension.uneval vdecl.var_id d

626


627

let uneval_node_generics vdecls =

628

List.iter uneval_vdecl_generics vdecls

629


630

let uneval_top_generics decl =

631

match decl.top_decl_desc with

632

 Node nd >

633

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

634

 ImportedNode nd >

635

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

636

 ImportedFun nd >

637

()

638

 Consts clist > ()

639

 Open _ > ()

640


641

let uneval_prog_generics prog =

642

List.iter uneval_top_generics prog

643


644

let check_env_compat declared computed =

645

Env.iter declared (fun k decl_type_k >

646

let computed_t = Env.lookup_value computed k in

647

try_unify decl_type_k computed_t Location.dummy_loc

648

)

649


650

(* Local Variables: *)

651

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

652

(* End: *)
