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

 Tstruct fl >

53

List.exists (fun (f, t) > occurs tvar t) fl

54

 Tarray (_, t)

55

 Tstatic (_, t)

56

 Tclock t

57

 Tlink t > occurs tvar t

58

 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > false

59


60

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

61

(* Generalize by sideeffects *)

62

let rec generalize ty =

63

match ty.tdesc with

64

 Tvar >

65

(* No scopes, always generalize *)

66

ty.tdesc < Tunivar

67

 Tarrow (t1,t2) >

68

generalize t1; generalize t2

69

 Ttuple tl >

70

List.iter generalize tl

71

 Tstruct fl >

72

List.iter (fun (f, t) > generalize t) fl

73

 Tstatic (d, t)

74

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

75

 Tclock t

76

 Tlink t >

77

generalize t

78

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

79


80

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

81

let rec instantiate inst_vars inst_dim_vars ty =

82

let ty = repr ty in

83

match ty.tdesc with

84

 Tenum _  Tconst _  Tvar  Tint  Treal  Tbool  Trat > ty

85

 Tarrow (t1,t2) >

86

{ty with tdesc =

87

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

88

 Ttuple tlist >

89

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

90

 Tstruct flist >

91

{ty with tdesc = Tstruct (List.map (fun (f, t) > (f, instantiate inst_vars inst_dim_vars t)) flist)}

92

 Tclock t >

93

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

94

 Tstatic (d, t) >

95

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

96

 Tarray (d, t) >

97

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

98

 Tlink t >

99

(* should not happen *)

100

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

101

 Tunivar >

102

try

103

List.assoc ty.tid !inst_vars

104

with Not_found >

105

let var = new_var () in

106

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

107

var

108


109

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

110

let rec type_coretype type_dim cty =

111

match (*get_repr_type*) cty with

112

 Tydec_any > new_var ()

113

 Tydec_int > Type_predef.type_int

114

 Tydec_real > Type_predef.type_real

115

 Tydec_float > Type_predef.type_real

116

 Tydec_bool > Type_predef.type_bool

117

 Tydec_clock ty > Type_predef.type_clock (type_coretype type_dim ty)

118

 Tydec_const c > Type_predef.type_const c

119

 Tydec_enum tl > Type_predef.type_enum tl

120

 Tydec_struct fl > Type_predef.type_struct (List.map (fun (f, ty) > (f, type_coretype type_dim ty)) fl)

121

 Tydec_array (d, ty) >

122

begin

123

type_dim d;

124

Type_predef.type_array d (type_coretype type_dim ty)

125

end

126


127

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

128

let rec coretype_type ty =

129

match (repr ty).tdesc with

130

 Tvar > Tydec_any

131

 Tint > Tydec_int

132

 Treal > Tydec_real

133

 Tbool > Tydec_bool

134

 Tconst c > Tydec_const c

135

 Tclock t > Tydec_clock (coretype_type t)

136

 Tenum tl > Tydec_enum tl

137

 Tstruct fl > Tydec_struct (List.map (fun (f, t) > (f, coretype_type t)) fl)

138

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

139

 Tstatic (_, t) > coretype_type t

140

 _ > assert false

141


142

let get_type_definition tname =

143

try

144

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

145

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

146


147

(* Equality on ground types only *)

148

(* Should be used between local variables which must have a ground type *)

149

let rec eq_ground t1 t2 =

150

match t1.tdesc, t2.tdesc with

151

 Tint, Tint  Tbool, Tbool  Trat, Trat  Treal, Treal > true

152

 Tenum tl, Tenum tl' when tl == tl' > true

153

 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > List.for_all2 eq_ground tl tl'

154

 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > List.for_all2 (fun (_, t) (_, t') > eq_ground t t') fl fl'

155

 (Tconst t, _) >

156

let def_t = get_type_definition t in

157

eq_ground def_t t2

158

 (_, Tconst t) >

159

let def_t = get_type_definition t in

160

eq_ground t1 def_t

161

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

162

 Tclock t1', Tclock t2' > eq_ground t1' t2'

163

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

164

 Tarray (e1, t1'), Tarray (e2, t2') > Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'

165

 _ > false

166


167

(** [unify t1 t2] unifies types [t1] and [t2]

168

using standard destructive unification.

169

Raises [Unify (t1,t2)] if the types are not unifiable.

170

[t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,

171

so in case of unification error: expected type [t1], got type [t2].

172

If [sub]typing is allowed, [t2] may be a subtype of [t1].

173

If [semi] unification is required,

174

[t1] should furthermore be an instance of [t2]

175

and constants are handled differently.*)

176

let unify ?(sub=false) ?(semi=false) t1 t2 =

177

let rec unif t1 t2 =

178

let t1 = repr t1 in

179

let t2 = repr t2 in

180

if t1==t2 then

181

()

182

else

183

match t1.tdesc,t2.tdesc with

184

(* strictly subtyping cases first *)

185

 _ , Tclock t2 when sub && (get_clock_base_type t1 = None) >

186

unif t1 t2

187

 _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) >

188

unif t1 t2

189

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

190

 Tvar, Tvar >

191

if t1.tid < t2.tid then

192

t2.tdesc < Tlink t1

193

else

194

t1.tdesc < Tlink t2

195

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

196

t1.tdesc < Tlink t2

197

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

198

t2.tdesc < Tlink t1

199

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

200

begin

201

unif t2 t2';

202

unif t1' t1

203

end

204

 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' >

205

List.iter2 unif tl tl'

206

 Ttuple [t1] , _ > unif t1 t2

207

 _ , Ttuple [t2] > unif t1 t2

208

 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' >

209

List.iter2 (fun (_, t) (_, t') > unif t t') fl fl'

210

 Tclock _, Tstatic _

211

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

212

 Tclock t1', Tclock t2' > unif t1' t2'

213

 Tint, Tint  Tbool, Tbool  Trat, Trat  Treal, Treal

214

 Tunivar, _  _, Tunivar > ()

215

 (Tconst t, _) >

216

let def_t = get_type_definition t in

217

unif def_t t2

218

 (_, Tconst t) >

219

let def_t = get_type_definition t in

220

unif t1 def_t

221

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

222

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

223

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

224

let eval_const =

225

if semi

226

then (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c))

227

else (fun c > None) in

228

begin

229

unif t1' t2';

230

Dimension.eval Basic_library.eval_env eval_const e1;

231

Dimension.eval Basic_library.eval_env eval_const e2;

232

Dimension.unify ~semi:semi e1 e2;

233

end

234

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

235

in unif t1 t2

236


237

(* Expected type ty1, got type ty2 *)

238

let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =

239

try

240

unify ~sub:sub ~semi:semi ty1 ty2

241

with

242

 Unify _ >

243

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

244

 Dimension.Unify _ >

245

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

246


247

(* ty1 is a subtype of ty2 *)

248

(*

249

let rec sub_unify sub ty1 ty2 =

250

match (repr ty1).tdesc, (repr ty2).tdesc with

251

 Ttuple tl1 , Ttuple tl2 >

252

if List.length tl1 <> List.length tl2

253

then raise (Unify (ty1, ty2))

254

else List.iter2 (sub_unify sub) tl1 tl2

255

 Ttuple [t1] , _ > sub_unify sub t1 ty2

256

 _ , Ttuple [t2] > sub_unify sub ty1 t2

257

 Tstruct tl1 , Tstruct tl2 >

258

if List.map fst tl1 <> List.map fst tl2

259

then raise (Unify (ty1, ty2))

260

else List.iter2 (fun (_, t1) (_, t2) > sub_unify sub t1 t2) tl1 tl2

261

 Tclock t1 , Tclock t2 > sub_unify sub t1 t2

262

 Tclock t1 , _ when sub > sub_unify sub t1 ty2

263

 Tstatic (d1, t1) , Tstatic (d2, t2) >

264

begin

265

sub_unify sub t1 t2;

266

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

267

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

268

Dimension.unify d1 d2

269

end

270

 Tstatic (r_d, t1) , _ when sub > sub_unify sub t1 ty2

271

 _ > unify ty1 ty2

272

*)

273


274

let rec type_struct_const_field loc (label, c) =

275

if Hashtbl.mem field_table label

276

then let tydec = Hashtbl.find field_table label in

277

let tydec_struct = get_struct_type_fields tydec in

278

let ty_label = type_coretype (fun d > ()) (List.assoc label tydec_struct) in

279

begin

280

try_unify ty_label (type_const loc c) loc;

281

type_coretype (fun d > ()) tydec

282

end

283

else raise (Error (loc, Unbound_value ("struct field " ^ label)))

284


285

and type_const loc c =

286

match c with

287

 Const_int _ > Type_predef.type_int

288

 Const_real _ > Type_predef.type_real

289

 Const_float _ > Type_predef.type_real

290

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

291

let ty = new_var () in

292

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

293

Type_predef.type_array d ty

294

 Const_tag t >

295

if Hashtbl.mem tag_table t

296

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

297

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

298

 Const_struct fl >

299

let ty_struct = new_var () in

300

begin

301

let used =

302

List.fold_left

303

(fun acc (l, c) >

304

if List.mem l acc

305

then raise (Error (loc, Already_bound ("struct field " ^ l)))

306

else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)

307

[] fl in

308

try

309

let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in

310

(* List.iter (fun l > Format.eprintf "total: %s@." l) total;

311

List.iter (fun l > Format.eprintf "used: %s@." l) used; *)

312

let undef = List.find (fun l > not (List.mem l used)) total

313

in raise (Error (loc, Unbound_value ("struct field " ^ undef)))

314

with Not_found >

315

ty_struct

316

end

317

 Const_string _ > assert false (* string should only appear in annotations *)

318


319

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

320

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

321

[env] is a pair composed of:

322

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

323

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

324

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

325

propagation policy in Lustre.

326

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

327

later discovered to be clocks during the typing process.

328

*)

329

let check_constant loc const_expected const_real =

330

if const_expected && not const_real

331

then raise (Error (loc, Not_a_constant))

332


333

let rec type_standard_args env in_main const expr_list =

334

let ty_list =

335

List.map

336

(fun e > let ty = dynamic_type (type_expr env in_main const e) in

337

match get_clock_base_type ty with

338

 None > ty

339

 Some ty > ty)

340

expr_list in

341

let ty_res = new_var () in

342

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

343

ty_res

344


345

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

346

used during node applications and assignments *)

347

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

348

let loc = real_arg.expr_loc in

349

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

350

let real_type = type_expr env in_main const real_arg in

351

let real_type =

352

if const

353

then let d =

354

if is_dimension_type real_type

355

then dimension_of_expr real_arg

356

else Dimension.mkdim_var () in

357

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

358

Dimension.eval Basic_library.eval_env eval_const d;

359

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

360

(match Types.get_static_value real_type with

361

 None > ()

362

 Some d' > try_unify real_type real_static_type loc);

363

real_static_type

364

else real_type in

365

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

366

try_unify ~sub:sub formal_type real_type loc

367


368

and type_ident env in_main loc const id =

369

type_expr env in_main const (expr_of_ident id loc)

370


371

(* typing an application implies:

372

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

373

 checking type adequation between formal and real arguments

374

An application may embed an homomorphic/internal function, in which case we need to split

375

it in many calls

376

*)

377

and type_appl env in_main loc const f args =

378

let args = expr_list_of_expr args in

379

if Basic_library.is_internal_fun f && List.exists is_tuple_expr args

380

then

381

try

382

let args = Utils.transpose_list (List.map expr_list_of_expr args) in

383

Types.type_of_type_list (List.map (type_call env in_main loc const f) args)

384

with

385

Utils.TransposeError (l, l') > raise (Error (loc, WrongMorphism (l, l')))

386

else

387

type_call env in_main loc const f args

388


389

(* type a (single) call. [args] is here a list of arguments. *)

390

and type_call env in_main loc const f args =

391

let tins, touts = new_var (), new_var () in

392

let tfun = Type_predef.type_arrow tins touts in

393

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

394

let tins = type_list_of_type tins in

395

if List.length args <> List.length tins then

396

raise (Error (loc, WrongArity (List.length tins, List.length args)))

397

else

398

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

399

touts

400


401

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

402

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

403

and type_expr env in_main const expr =

404

let resulting_ty =

405

match expr.expr_desc with

406

 Expr_const c >

407

let ty = type_const expr.expr_loc c in

408

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

409

expr.expr_type < ty;

410

ty

411

 Expr_ident v >

412

let tyv =

413

try

414

Env.lookup_value (fst env) v

415

with Not_found >

416

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

417

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

418

in

419

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

420

let ty' =

421

if const

422

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

423

else new_var () in

424

try_unify ty ty' expr.expr_loc;

425

expr.expr_type < ty;

426

ty

427

 Expr_array elist >

428

let ty_elt = type_standard_args env in_main const elist in

429

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

430

let ty = Type_predef.type_array d ty_elt in

431

expr.expr_type < ty;

432

ty

433

 Expr_access (e1, d) >

434

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

435

let ty_elt = new_var () in

436

let d = Dimension.mkdim_var () in

437

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

438

expr.expr_type < ty_elt;

439

ty_elt

440

 Expr_power (e1, d) >

441

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

442

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

443

Dimension.eval Basic_library.eval_env eval_const d;

444

let ty_elt = type_standard_args env in_main const [e1] in

445

let ty = Type_predef.type_array d ty_elt in

446

expr.expr_type < ty;

447

ty

448

 Expr_tuple elist >

449

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

450

expr.expr_type < ty;

451

ty

452

 Expr_ite (c, t, e) >

453

type_subtyping_arg env in_main const c Type_predef.type_bool;

454

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

455

expr.expr_type < ty;

456

ty

457

 Expr_appl (id, args, r) >

458

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

459

expression *)

460

(match r with

461

 None > ()

462

 Some (x, l) >

463

check_constant expr.expr_loc const false;

464

let expr_x = expr_of_ident x expr.expr_loc in

465

let typ_l =

466

Type_predef.type_clock

467

(type_const expr.expr_loc (Const_tag l)) in

468

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

469

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

470

expr.expr_type < touts;

471

touts

472

 Expr_fby (e1,e2)

473

 Expr_arrow (e1,e2) >

474

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

475

check_constant expr.expr_loc const false;

476

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

477

expr.expr_type < ty;

478

ty

479

 Expr_pre e >

480

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

481

check_constant expr.expr_loc const false;

482

let ty = type_standard_args env in_main const [e] in

483

expr.expr_type < ty;

484

ty

485

 Expr_when (e1,c,l) >

486

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

487

check_constant expr.expr_loc const false;

488

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

489

let expr_c = expr_of_ident c expr.expr_loc in

490

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

491

(*update_clock env in_main c expr.expr_loc typ_l;*)

492

let ty = type_standard_args env in_main const [e1] in

493

expr.expr_type < ty;

494

ty

495

 Expr_merge (c,hl) >

496

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

497

check_constant expr.expr_loc const false;

498

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

499

let expr_c = expr_of_ident c expr.expr_loc in

500

let typ_l = Type_predef.type_clock typ_in in

501

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

502

(*update_clock env in_main c expr.expr_loc typ_l;*)

503

expr.expr_type < typ_out;

504

typ_out

505

in

506

Log.report ~level:3 (fun fmt > Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);

507

resulting_ty

508


509

and type_branches env in_main loc const hl =

510

let typ_in = new_var () in

511

let typ_out = new_var () in

512

try

513

let used_labels =

514

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

515

unify typ_in (type_const loc (Const_tag t));

516

type_subtyping_arg env in_main const h typ_out;

517

if List.mem t accu

518

then raise (Error (loc, Already_bound t))

519

else t :: accu) [] hl in

520

let type_labels = get_enum_type_tags (coretype_type typ_in) in

521

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

522

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

523

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

524

else (typ_in, typ_out)

525

with Unify (t1, t2) >

526

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

527

(*

528

and update_clock env in_main id loc typ =

529

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

530

try

531

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

532

in vdecl.var_type < typ

533

with

534

Not_found >

535

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

536

*)

537

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

538

let type_eq env in_main undefined_vars eq =

539

(* Check undefined variables, type lhs *)

540

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

541

let ty_lhs = type_expr env in_main false expr_lhs in

542

(* Check multiple variable definitions *)

543

let define_var id uvars =

544

try

545

ignore(IMap.find id uvars);

546

IMap.remove id uvars

547

with Not_found >

548

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

549

in

550

(* check assignment of declared constant, assignment of clock *)

551

let ty_lhs =

552

type_of_type_list

553

(List.map2 (fun ty id >

554

if get_static_value ty <> None

555

then raise (Error (eq.eq_loc, Assigned_constant id)) else

556

match get_clock_base_type ty with

557

 None > ty

558

 Some ty > ty)

559

(type_list_of_type ty_lhs) eq.eq_lhs) in

560

let undefined_vars =

561

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

562

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

563

to a (always nonconstant) lhs variable *)

564

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

565

undefined_vars

566


567


568

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

569

in environment [env] *)

570

let type_coreclock env ck id loc =

571

match ck.ck_dec_desc with

572

 Ckdec_any  Ckdec_pclock (_,_) > ()

573

 Ckdec_bool cl >

574

let dummy_id_expr = expr_of_ident id loc in

575

let when_expr =

576

List.fold_left

577

(fun expr (x, l) >

578

{expr_tag = new_tag ();

579

expr_desc= Expr_when (expr,x,l);

580

expr_type = new_var ();

581

expr_clock = Clocks.new_var true;

582

expr_delay = Delay.new_var ();

583

expr_loc=loc;

584

expr_annot = None})

585

dummy_id_expr cl

586

in

587

ignore (type_expr env false false when_expr)

588


589

let rec check_type_declaration loc cty =

590

match cty with

591

 Tydec_clock ty

592

 Tydec_array (_, ty) > check_type_declaration loc ty

593

 Tydec_const tname >

594

if not (Hashtbl.mem type_table cty)

595

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

596

 _ > ()

597


598

let type_var_decl vd_env env vdecl =

599

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

600

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

601

let type_dim d =

602

begin

603

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

604

Dimension.eval Basic_library.eval_env eval_const d;

605

end in

606

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

607

let ty_status =

608

if vdecl.var_dec_const

609

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

610

else ty in

611

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

612

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

613

vdecl.var_type < ty_status;

614

new_env

615


616

let type_var_decl_list vd_env env l =

617

List.fold_left (type_var_decl vd_env) env l

618


619

let type_of_vlist vars =

620

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

621

type_of_type_list tyl

622


623

let add_vdecl vd_env vdecl =

624

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

625

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

626

else vdecl::vd_env

627


628

let check_vd_env vd_env =

629

ignore (List.fold_left add_vdecl [] vd_env)

630


631

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

632

location is used for error reports. *)

633

let type_node env nd loc =

634

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

635

let vd_env_ol = nd.node_outputs@nd.node_locals in

636

let vd_env = nd.node_inputs@vd_env_ol in

637

check_vd_env vd_env;

638

let init_env = env in

639

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

640

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

641

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

642

let new_env = Env.overwrite env delta_env in

643

let undefined_vars_init =

644

List.fold_left

645

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

646

IMap.empty vd_env_ol in

647

let undefined_vars =

648

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

649

in

650

(* Typing asserts *)

651

List.iter (fun assert_ >

652

let assert_expr = assert_.assert_expr in

653

type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool

654

) nd.node_asserts;

655


656

(* check that table is empty *)

657

if (not (IMap.is_empty undefined_vars)) then

658

raise (Error (loc, Undefined_var undefined_vars));

659

let ty_ins = type_of_vlist nd.node_inputs in

660

let ty_outs = type_of_vlist nd.node_outputs in

661

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

662

generalize ty_node;

663

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

664

nd.node_type < ty_node;

665

Env.add_value env nd.node_id ty_node

666


667

let type_imported_node env nd loc =

668

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

669

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

670

check_vd_env vd_env;

671

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

672

let ty_ins = type_of_vlist nd.nodei_inputs in

673

let ty_outs = type_of_vlist nd.nodei_outputs in

674

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

675

generalize ty_node;

676

(*

677

if (is_polymorphic ty_node) then

678

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

679

*)

680

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

681

nd.nodei_type < ty_node;

682

new_env

683


684

let type_top_consts env clist =

685

List.fold_left (fun env cdecl >

686

let ty = type_const cdecl.const_loc cdecl.const_value in

687

let d =

688

if is_dimension_type ty

689

then dimension_of_const cdecl.const_loc cdecl.const_value

690

else Dimension.mkdim_var () in

691

let ty = Type_predef.type_static d ty in

692

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

693

cdecl.const_type < ty;

694

new_env) env clist

695


696

let type_top_decl env decl =

697

match decl.top_decl_desc with

698

 Node nd > (

699

try

700

type_node env nd decl.top_decl_loc

701

with Error (loc, err) as exc > (

702

if !Options.global_inline then

703

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

704

Printers.pp_node nd

705

;

706

raise exc)

707

)

708

 ImportedNode nd >

709

type_imported_node env nd decl.top_decl_loc

710

 Consts clist >

711

type_top_consts env clist

712

 Open _ > env

713


714

let type_prog env decls =

715

try

716

List.fold_left type_top_decl env decls

717

with Failure _ as exc > raise exc

718


719

(* Once the Lustre program is fully typed,

720

we must get back to the original description of dimensions,

721

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

722


723

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

724

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

725

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

726

*)

727

let uneval_vdecl_generics vdecl =

728

if vdecl.var_dec_const

729

then

730

match get_static_value vdecl.var_type with

731

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

732

 Some d > Dimension.uneval vdecl.var_id d

733


734

let uneval_node_generics vdecls =

735

List.iter uneval_vdecl_generics vdecls

736


737

let uneval_top_generics decl =

738

match decl.top_decl_desc with

739

 Node nd >

740

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

741

 ImportedNode nd >

742

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

743

 Consts clist > ()

744

 Open _ > ()

745


746

let uneval_prog_generics prog =

747

List.iter uneval_top_generics prog

748


749

let rec get_imported_node decls id =

750

match decls with

751

 [] > assert false

752

 decl::q >

753

(match decl.top_decl_desc with

754

 ImportedNode nd when id = nd.nodei_id > decl

755

 _ > get_imported_node q id)

756


757

let check_env_compat header declared computed =

758

uneval_prog_generics header;

759

Env.iter declared (fun k decl_type_k >

760

let computed_t = instantiate (ref []) (ref [])

761

(try Env.lookup_value computed k

762

with Not_found >

763

let loc = (get_imported_node header k).top_decl_loc in

764

raise (Error (loc, Declared_but_undefined k))) in

765

(*Types.print_ty Format.std_formatter decl_type_k;

766

Types.print_ty Format.std_formatter computed_t;*)

767

try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc

768

)

769


770

(* Local Variables: *)

771

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

772

(* End: *)
