1

(********************************************************************)

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT  LIFL *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

(* This file was originally from the Prelude compiler *)

11

(* *)

12

(********************************************************************)

13


14

(** Main typing module. Classic inference algorithm with destructive

15

unification. *)

16


17

let debug fmt args = () (* Format.eprintf "%a" *)

18

(* Though it shares similarities with the clock calculus module, no code

19

is shared. Simple environments, very limited identifier scoping, no

20

identifier redefinition allowed. *)

21


22

open Utils

23

(* Yes, opening both modules is dirty as some type names will be

24

overwritten, yet this makes notations far lighter.*)

25

open LustreSpec

26

open Corelang

27

open Types

28

open Format

29


30

let pp_typing_env fmt env =

31

Env.pp_env print_ty fmt env

32


33

(** [occurs tvar ty] returns true if the type variable [tvar] occurs in

34

type [ty]. False otherwise. *)

35

let rec occurs tvar ty =

36

let ty = repr ty in

37

match ty.tdesc with

38

 Tvar > ty=tvar

39

 Tarrow (t1, t2) >

40

(occurs tvar t1)  (occurs tvar t2)

41

 Ttuple tl >

42

List.exists (occurs tvar) tl

43

 Tstruct fl >

44

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

45

 Tarray (_, t)

46

 Tstatic (_, t)

47

 Tclock t

48

 Tlink t > occurs tvar t

49

 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > false

50


51

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

52

(* Generalize by sideeffects *)

53

let rec generalize ty =

54

match ty.tdesc with

55

 Tvar >

56

(* No scopes, always generalize *)

57

ty.tdesc < Tunivar

58

 Tarrow (t1,t2) >

59

generalize t1; generalize t2

60

 Ttuple tl >

61

List.iter generalize tl

62

 Tstruct fl >

63

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

64

 Tstatic (d, t)

65

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

66

 Tclock t

67

 Tlink t >

68

generalize t

69

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

70


71

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

72

let rec instantiate inst_vars inst_dim_vars ty =

73

let ty = repr ty in

74

match ty.tdesc with

75

 Tenum _  Tconst _  Tvar  Tint  Treal  Tbool  Trat > ty

76

 Tarrow (t1,t2) >

77

{ty with tdesc =

78

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

79

 Ttuple tlist >

80

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

81

 Tstruct flist >

82

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

83

 Tclock t >

84

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

85

 Tstatic (d, t) >

86

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

87

 Tarray (d, t) >

88

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

89

 Tlink t >

90

(* should not happen *)

91

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

92

 Tunivar >

93

try

94

List.assoc ty.tid !inst_vars

95

with Not_found >

96

let var = new_var () in

97

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

98

var

99


100

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

101

let rec type_coretype type_dim cty =

102

match (*get_repr_type*) cty with

103

 Tydec_any > new_var ()

104

 Tydec_int > Type_predef.type_int

105

 Tydec_real > Type_predef.type_real

106

 Tydec_float > Type_predef.type_real

107

 Tydec_bool > Type_predef.type_bool

108

 Tydec_clock ty > Type_predef.type_clock (type_coretype type_dim ty)

109

 Tydec_const c > Type_predef.type_const c

110

 Tydec_enum tl > Type_predef.type_enum tl

111

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

112

 Tydec_array (d, ty) >

113

begin

114

type_dim d;

115

Type_predef.type_array d (type_coretype type_dim ty)

116

end

117


118

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

119

let rec coretype_type ty =

120

match (repr ty).tdesc with

121

 Tvar > Tydec_any

122

 Tint > Tydec_int

123

 Treal > Tydec_real

124

 Tbool > Tydec_bool

125

 Tconst c > Tydec_const c

126

 Tclock t > Tydec_clock (coretype_type t)

127

 Tenum tl > Tydec_enum tl

128

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

129

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

130

 Tstatic (_, t) > coretype_type t

131

 _ > assert false

132


133

let get_coretype_definition tname =

134

try

135

let top = Hashtbl.find type_table (Tydec_const tname) in

136

match top.top_decl_desc with

137

 TypeDef tdef > tdef.tydef_desc

138

 _ > assert false

139

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

140


141

let get_type_definition tname =

142

type_coretype (fun d > ()) (get_coretype_definition tname)

143


144

(* Equality on ground types only *)

145

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

146

let rec eq_ground t1 t2 =

147

let t1 = repr t1 in

148

let t2 = repr t2 in

149

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

let rec type_struct_const_field loc (label, c) =

248

if Hashtbl.mem field_table label

249

then let tydef = Hashtbl.find field_table label in

250

let tydec = (typedef_of_top tydef).tydef_desc in

251

let tydec_struct = get_struct_type_fields tydec in

252

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

253

begin

254

try_unify ty_label (type_const loc c) loc;

255

type_coretype (fun d > ()) tydec

256

end

257

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

258


259

and type_const loc c =

260

match c with

261

 Const_int _ > Type_predef.type_int

262

 Const_real _ > Type_predef.type_real

263

 Const_float _ > Type_predef.type_real

264

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

265

let ty = new_var () in

266

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

267

Type_predef.type_array d ty

268

 Const_tag t >

269

if Hashtbl.mem tag_table t

270

then

271

let tydef = typedef_of_top (Hashtbl.find tag_table t) in

272

let tydec =

273

if is_user_type tydef.tydef_desc

274

then Tydec_const tydef.tydef_id

275

else tydef.tydef_desc in

276

type_coretype (fun d > ()) tydec

277

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

278

 Const_struct fl >

279

let ty_struct = new_var () in

280

begin

281

let used =

282

List.fold_left

283

(fun acc (l, c) >

284

if List.mem l acc

285

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

286

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

287

[] fl in

288

try

289

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

290

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

291

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

292

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

293

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

294

with Not_found >

295

ty_struct

296

end

297

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

298


299

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

300

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

301

[env] is a pair composed of:

302

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

303

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

304

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

305

propagation policy in Lustre.

306

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

307

later discovered to be clocks during the typing process.

308

*)

309

let check_constant loc const_expected const_real =

310

if const_expected && not const_real

311

then raise (Error (loc, Not_a_constant))

312


313

let rec type_add_const env const arg targ =

314

if const

315

then let d =

316

if is_dimension_type targ

317

then dimension_of_expr arg

318

else Dimension.mkdim_var () in

319

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

320

Dimension.eval Basic_library.eval_env eval_const d;

321

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

322

(match Types.get_static_value targ with

323

 None > ()

324

 Some d' > try_unify targ real_static_type arg.expr_loc);

325

real_static_type

326

else targ

327


328

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

329

used during node applications and assignments *)

330

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

331

let loc = real_arg.expr_loc in

332

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

333

let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in

334

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

335

try_unify ~sub:sub formal_type real_type loc

336


337

and type_ident env in_main loc const id =

338

type_expr env in_main const (expr_of_ident id loc)

339


340

(* typing an application implies:

341

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

342

 checking type adequation between formal and real arguments

343

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

344

it in many calls

345

*)

346

and type_appl env in_main loc const f args =

347

let targs = List.map (type_expr env in_main const) args in

348

if Basic_library.is_internal_fun f && List.exists is_tuple_type targs

349

then

350

try

351

let targs = Utils.transpose_list (List.map type_list_of_type targs) in

352

Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)

353

with

354

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

355

else

356

type_dependent_call env in_main loc const f (List.combine args targs)

357


358

(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)

359

and type_dependent_call env in_main loc const f targs =

360

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

361

let tfun = Type_predef.type_arrow tins touts in

362

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

363

let tins = type_list_of_type tins in

364

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

365

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

366

else

367

begin

368

List.iter2 (fun (a,t) ti >

369

let t' = type_add_const env (const  Types.get_static_value ti <> None) a t

370

in try_unify ~sub:true ti t' a.expr_loc) targs tins;

371

touts

372

end

373


374

(* type a simple call without dependent types

375

but possible homomorphic extension.

376

[targs] is here a list of arguments' types. *)

377

and type_simple_call env in_main loc const f targs =

378

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

379

let tfun = Type_predef.type_arrow tins touts in

380

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

381

(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)

382

try_unify ~sub:true tins (type_of_type_list targs) loc;

383

touts

384


385

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

386

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

387

and type_expr env in_main const expr =

388

let resulting_ty =

389

match expr.expr_desc with

390

 Expr_const c >

391

let ty = type_const expr.expr_loc c in

392

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

393

expr.expr_type < ty;

394

ty

395

 Expr_ident v >

396

let tyv =

397

try

398

Env.lookup_value (fst env) v

399

with Not_found >

400

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

401

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

402

in

403

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

404

let ty' =

405

if const

406

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

407

else new_var () in

408

try_unify ty ty' expr.expr_loc;

409

expr.expr_type < ty;

410

ty

411

 Expr_array elist >

412

let ty_elt = new_var () in

413

List.iter (fun e > try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;

414

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

415

let ty = Type_predef.type_array d ty_elt in

416

expr.expr_type < ty;

417

ty

418

 Expr_access (e1, d) >

419

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

420

let ty_elt = new_var () in

421

let d = Dimension.mkdim_var () in

422

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

423

expr.expr_type < ty_elt;

424

ty_elt

425

 Expr_power (e1, d) >

426

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

427

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

428

Dimension.eval Basic_library.eval_env eval_const d;

429

let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in

430

let ty = Type_predef.type_array d ty_elt in

431

expr.expr_type < ty;

432

ty

433

 Expr_tuple elist >

434

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

435

expr.expr_type < ty;

436

ty

437

 Expr_ite (c, t, e) >

438

type_subtyping_arg env in_main const c Type_predef.type_bool;

439

let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in

440

expr.expr_type < ty;

441

ty

442

 Expr_appl (id, args, r) >

443

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

444

expression *)

445

(match r with

446

 None > ()

447

 Some c >

448

check_constant expr.expr_loc const false;

449

type_subtyping_arg env in_main const c Type_predef.type_bool);

450

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

451

expr.expr_type < touts;

452

touts

453

 Expr_fby (e1,e2)

454

 Expr_arrow (e1,e2) >

455

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

456

check_constant expr.expr_loc const false;

457

let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in

458

expr.expr_type < ty;

459

ty

460

 Expr_pre e >

461

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

462

check_constant expr.expr_loc const false;

463

let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in

464

expr.expr_type < ty;

465

ty

466

 Expr_when (e1,c,l) >

467

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

468

check_constant expr.expr_loc const false;

469

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

470

let expr_c = expr_of_ident c expr.expr_loc in

471

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

472

let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in

473

expr.expr_type < ty;

474

ty

475

 Expr_merge (c,hl) >

476

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

477

check_constant expr.expr_loc const false;

478

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

479

let expr_c = expr_of_ident c expr.expr_loc in

480

let typ_l = Type_predef.type_clock typ_in in

481

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

482

expr.expr_type < typ_out;

483

typ_out

484

in

485

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

486

resulting_ty

487


488

and type_branches env in_main loc const hl =

489

let typ_in = new_var () in

490

let typ_out = new_var () in

491

try

492

let used_labels =

493

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

494

unify typ_in (type_const loc (Const_tag t));

495

type_subtyping_arg env in_main const h typ_out;

496

if List.mem t accu

497

then raise (Error (loc, Already_bound t))

498

else t :: accu) [] hl in

499

let type_labels = get_enum_type_tags (coretype_type typ_in) in

500

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

501

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

502

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

503

else (typ_in, typ_out)

504

with Unify (t1, t2) >

505

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

506


507

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

508

let type_eq env in_main undefined_vars eq =

509

(* Check undefined variables, type lhs *)

510

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

511

let ty_lhs = type_expr env in_main false expr_lhs in

512

(* Check multiple variable definitions *)

513

let define_var id uvars =

514

try

515

ignore(IMap.find id uvars);

516

IMap.remove id uvars

517

with Not_found >

518

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

519

in

520

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

521

let ty_lhs =

522

type_of_type_list

523

(List.map2 (fun ty id >

524

if get_static_value ty <> None

525

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

526

match get_clock_base_type ty with

527

 None > ty

528

 Some ty > ty)

529

(type_list_of_type ty_lhs) eq.eq_lhs) in

530

let undefined_vars =

531

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

532

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

533

to a (always nonconstant) lhs variable *)

534

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

535

undefined_vars

536


537


538

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

539

in environment [env] *)

540

let type_coreclock env ck id loc =

541

match ck.ck_dec_desc with

542

 Ckdec_any  Ckdec_pclock (_,_) > ()

543

 Ckdec_bool cl >

544

let dummy_id_expr = expr_of_ident id loc in

545

let when_expr =

546

List.fold_left

547

(fun expr (x, l) >

548

{expr_tag = new_tag ();

549

expr_desc= Expr_when (expr,x,l);

550

expr_type = new_var ();

551

expr_clock = Clocks.new_var true;

552

expr_delay = Delay.new_var ();

553

expr_loc=loc;

554

expr_annot = None})

555

dummy_id_expr cl

556

in

557

ignore (type_expr env false false when_expr)

558


559

let rec check_type_declaration loc cty =

560

match cty with

561

 Tydec_clock ty

562

 Tydec_array (_, ty) > check_type_declaration loc ty

563

 Tydec_const tname >

564

if not (Hashtbl.mem type_table cty)

565

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

566

 _ > ()

567


568

let type_var_decl vd_env env vdecl =

569

(*Format.eprintf "Typing.type_var_decl START %a@." Printers.pp_var vdecl;*)

570

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

571

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

572

let type_dim d =

573

begin

574

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

575

Dimension.eval Basic_library.eval_env eval_const d;

576

end in

577

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

578

let ty_status =

579

if vdecl.var_dec_const

580

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

581

else ty in

582

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

583

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

584

vdecl.var_type < ty_status;

585

(*Format.eprintf "END@.";*)

586

new_env

587


588

let type_var_decl_list vd_env env l =

589

List.fold_left (type_var_decl vd_env) env l

590


591

let type_of_vlist vars =

592

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

593

type_of_type_list tyl

594


595

let add_vdecl vd_env vdecl =

596

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

597

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

598

else vdecl::vd_env

599


600

let check_vd_env vd_env =

601

ignore (List.fold_left add_vdecl [] vd_env)

602


603

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

604

location is used for error reports. *)

605

let type_node env nd loc =

606

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

607

let vd_env_ol = nd.node_outputs@nd.node_locals in

608

let vd_env = nd.node_inputs@vd_env_ol in

609

check_vd_env vd_env;

610

let init_env = env in

611

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

612

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

613

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

614

let new_env = Env.overwrite env delta_env in

615

let undefined_vars_init =

616

List.fold_left

617

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

618

IMap.empty vd_env_ol in

619

let undefined_vars =

620

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

621

in

622

(* Typing asserts *)

623

List.iter (fun assert_ >

624

let assert_expr = assert_.assert_expr in

625

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

626

) nd.node_asserts;

627


628

(* check that table is empty *)

629

if (not (IMap.is_empty undefined_vars)) then

630

raise (Error (loc, Undefined_var undefined_vars));

631

let ty_ins = type_of_vlist nd.node_inputs in

632

let ty_outs = type_of_vlist nd.node_outputs in

633

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

634

generalize ty_node;

635

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

636

nd.node_type < ty_node;

637

Env.add_value env nd.node_id ty_node

638


639

let type_imported_node env nd loc =

640

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

641

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

642

check_vd_env vd_env;

643

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

644

let ty_ins = type_of_vlist nd.nodei_inputs in

645

let ty_outs = type_of_vlist nd.nodei_outputs in

646

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

647

generalize ty_node;

648

(*

649

if (is_polymorphic ty_node) then

650

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

651

*)

652

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

653

nd.nodei_type < ty_node;

654

new_env

655


656

let type_top_const env cdecl =

657

let ty = type_const cdecl.const_loc cdecl.const_value in

658

let d =

659

if is_dimension_type ty

660

then dimension_of_const cdecl.const_loc cdecl.const_value

661

else Dimension.mkdim_var () in

662

let ty = Type_predef.type_static d ty in

663

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

664

cdecl.const_type < ty;

665

new_env

666


667

let type_top_consts env clist =

668

List.fold_left type_top_const env clist

669


670

let rec type_top_decl env decl =

671

match decl.top_decl_desc with

672

 Node nd > (

673

try

674

type_node env nd decl.top_decl_loc

675

with Error (loc, err) as exc > (

676

if !Options.global_inline then

677

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

678

Printers.pp_node nd

679

;

680

raise exc)

681

)

682

 ImportedNode nd >

683

type_imported_node env nd decl.top_decl_loc

684

 Const c >

685

type_top_const env c

686

 TypeDef _ > List.fold_left type_top_decl env (consts_of_enum_type decl)

687

 Open _ > env

688


689

let type_prog env decls =

690

try

691

List.fold_left type_top_decl env decls

692

with Failure _ as exc > raise exc

693


694

(* Once the Lustre program is fully typed,

695

we must get back to the original description of dimensions,

696

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

697


698

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

699

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

700

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

701

*)

702

let uneval_vdecl_generics vdecl =

703

if vdecl.var_dec_const

704

then

705

match get_static_value vdecl.var_type with

706

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

707

 Some d > Dimension.uneval vdecl.var_id d

708


709

let uneval_node_generics vdecls =

710

List.iter uneval_vdecl_generics vdecls

711


712

let uneval_top_generics decl =

713

match decl.top_decl_desc with

714

 Node nd >

715

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

716

 ImportedNode nd >

717

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

718

 Const _

719

 TypeDef _

720

 Open _ > ()

721


722

let uneval_prog_generics prog =

723

List.iter uneval_top_generics prog

724


725

let rec get_imported_symbol decls id =

726

match decls with

727

 [] > assert false

728

 decl::q >

729

(match decl.top_decl_desc with

730

 ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf > decl

731

 Const c when id = c.const_id && decl.top_decl_itf > decl

732

 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id

733

 _ > get_imported_symbol q id)

734


735

let check_env_compat header declared computed =

736

uneval_prog_generics header;

737

Env.iter declared (fun k decl_type_k >

738

let loc = (get_imported_symbol header k).top_decl_loc in

739

let computed_t =

740

instantiate (ref []) (ref [])

741

(try Env.lookup_value computed k

742

with Not_found > raise (Error (loc, Declared_but_undefined k))) in

743

(*Types.print_ty Format.std_formatter decl_type_k;

744

Types.print_ty Format.std_formatter computed_t;*)

745

try_unify ~sub:true ~semi:true decl_type_k computed_t loc

746

)

747


748

let check_typedef_top decl =

749

(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)

750

(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)

751

(*Format.eprintf "%a" Corelang.print_type_table ();*)

752

match decl.top_decl_desc with

753

 TypeDef ty >

754

let owner = decl.top_decl_owner in

755

let itf = decl.top_decl_itf in

756

let decl' =

757

try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)

758

with Not_found > raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in

759

let owner' = decl'.top_decl_owner in

760

(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)

761

let itf' = decl'.top_decl_itf in

762

(match decl'.top_decl_desc with

763

 Const _  Node _  ImportedNode _ > assert false

764

 TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') > ()

765

 _ > raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))

766

 _ > ()

767


768

let check_typedef_compat header =

769

List.iter check_typedef_top header

770


771

(* Local Variables: *)

772

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

773

(* End: *)
