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

let d = Dimension.copy (ref []) d in

115

type_dim d;

116

Type_predef.type_array d (type_coretype type_dim ty)

117

end

118


119

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

120

let rec coretype_type ty =

121

match (repr ty).tdesc with

122

 Tvar > Tydec_any

123

 Tint > Tydec_int

124

 Treal > Tydec_real

125

 Tbool > Tydec_bool

126

 Tconst c > Tydec_const c

127

 Tclock t > Tydec_clock (coretype_type t)

128

 Tenum tl > Tydec_enum tl

129

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

130

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

131

 Tstatic (_, t) > coretype_type t

132

 _ > assert false

133


134

let get_coretype_definition tname =

135

try

136

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

137

match top.top_decl_desc with

138

 TypeDef tdef > tdef.tydef_desc

139

 _ > assert false

140

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

141


142

let get_type_definition tname =

143

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

144


145

(* Equality on ground types only *)

146

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

147

let rec eq_ground t1 t2 =

148

let t1 = repr t1 in

149

let t2 = repr t2 in

150

t1==t2 

151

match t1.tdesc, t2.tdesc with

152

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

153

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

154

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

155

 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'

156

 (Tconst t, _) >

157

let def_t = get_type_definition t in

158

eq_ground def_t t2

159

 (_, Tconst t) >

160

let def_t = get_type_definition t in

161

eq_ground t1 def_t

162

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

163

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

164

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

165

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

166

 _ > false

167


168

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

169

using standard destructive unification.

170

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

171

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

172

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

173

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

174

If [semi] unification is required,

175

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

176

and constants are handled differently.*)

177

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

178

let rec unif t1 t2 =

179

let t1 = repr t1 in

180

let t2 = repr t2 in

181

if t1==t2 then

182

()

183

else

184

match t1.tdesc,t2.tdesc with

185

(* strictly subtyping cases first *)

186

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

187

unif t1 t2

188

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

189

unif t1 t2

190

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

191

 Tvar, Tvar >

192

if t1.tid < t2.tid then

193

t2.tdesc < Tlink t1

194

else

195

t1.tdesc < Tlink t2

196

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

197

t1.tdesc < Tlink t2

198

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

199

t2.tdesc < Tlink t1

200

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

201

begin

202

unif t2 t2';

203

unif t1' t1

204

end

205

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

206

List.iter2 unif tl tl'

207

 Ttuple [t1] , _ > unif t1 t2

208

 _ , Ttuple [t2] > unif t1 t2

209

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

210

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

211

 Tclock _, Tstatic _

212

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

213

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

214

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

215

 Tunivar, _  _, Tunivar > ()

216

 (Tconst t, _) >

217

let def_t = get_type_definition t in

218

unif def_t t2

219

 (_, Tconst t) >

220

let def_t = get_type_definition t in

221

unif t1 def_t

222

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

223

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

224

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

225

let eval_const =

226

if semi

227

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

228

else (fun c > None) in

229

begin

230

unif t1' t2';

231

Dimension.eval Basic_library.eval_env eval_const e1;

232

Dimension.eval Basic_library.eval_env eval_const e2;

233

Dimension.unify ~semi:semi e1 e2;

234

end

235

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

236

in unif t1 t2

237


238

(* Expected type ty1, got type ty2 *)

239

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

240

try

241

unify ~sub:sub ~semi:semi ty1 ty2

242

with

243

 Unify _ >

244

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

245

 Dimension.Unify _ >

246

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

247


248

let rec type_struct_const_field loc (label, c) =

249

if Hashtbl.mem field_table label

250

then let tydef = Hashtbl.find field_table label in

251

let tydec = (typedef_of_top tydef).tydef_desc in

252

let tydec_struct = get_struct_type_fields tydec in

253

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

254

begin

255

try_unify ty_label (type_const loc c) loc;

256

type_coretype (fun d > ()) tydec

257

end

258

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

259


260

and type_const loc c =

261

match c with

262

 Const_int _ > Type_predef.type_int

263

 Const_real _ > Type_predef.type_real

264

(*  Const_float _ > Type_predef.type_real *)

265

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

266

let ty = new_var () in

267

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

268

Type_predef.type_array d ty

269

 Const_tag t >

270

if Hashtbl.mem tag_table t

271

then

272

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

273

let tydec =

274

if is_user_type tydef.tydef_desc

275

then Tydec_const tydef.tydef_id

276

else tydef.tydef_desc in

277

type_coretype (fun d > ()) tydec

278

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

279

 Const_struct fl >

280

let ty_struct = new_var () in

281

begin

282

let used =

283

List.fold_left

284

(fun acc (l, c) >

285

if List.mem l acc

286

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

287

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

288

[] fl in

289

try

290

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

291

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

292

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

293

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

294

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

295

with Not_found >

296

ty_struct

297

end

298

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

299


300

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

301

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

302

[env] is a pair composed of:

303

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

304

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

305

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

306

propagation policy in Lustre.

307

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

308

later discovered to be clocks during the typing process.

309

*)

310

let check_constant loc const_expected const_real =

311

if const_expected && not const_real

312

then raise (Error (loc, Not_a_constant))

313


314

let rec type_add_const env const arg targ =

315

(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*)

316

if const

317

then let d =

318

if is_dimension_type targ

319

then dimension_of_expr arg

320

else Dimension.mkdim_var () in

321

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

322

Dimension.eval Basic_library.eval_env eval_const d;

323

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

324

(match Types.get_static_value targ with

325

 None > ()

326

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

327

real_static_type

328

else targ

329


330

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

331

used during node applications and assignments *)

332

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

333

let loc = real_arg.expr_loc in

334

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

335

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

336

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

337

try_unify ~sub:sub formal_type real_type loc

338


339

(* typing an application implies:

340

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

341

 checking type adequation between formal and real arguments

342

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

343

it in many calls

344

*)

345

and type_appl env in_main loc const f args =

346

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

347

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

348

then

349

try

350

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

351

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

352

with

353

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

354

else

355

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

356


357

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

358

and type_dependent_call env in_main loc const f targs =

359

(*Format.eprintf "Typing.type_dependent_call %s@." f;*)

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 false (* not necessary a constant *) (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 args_list = expr_list_of_expr args in

451

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

452

args.expr_type < new_ty (Ttuple (List.map (fun a > a.expr_type) args_list));

453

expr.expr_type < touts;

454

touts

455

 Expr_fby (e1,e2)

456

 Expr_arrow (e1,e2) >

457

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

458

check_constant expr.expr_loc const false;

459

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

460

expr.expr_type < ty;

461

ty

462

 Expr_pre e >

463

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

464

check_constant expr.expr_loc const false;

465

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

466

expr.expr_type < ty;

467

ty

468

 Expr_when (e1,c,l) >

469

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

470

check_constant expr.expr_loc const false;

471

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

472

let expr_c = expr_of_ident c expr.expr_loc in

473

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

474

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

475

expr.expr_type < ty;

476

ty

477

 Expr_merge (c,hl) >

478

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

479

check_constant expr.expr_loc const false;

480

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

481

let expr_c = expr_of_ident c expr.expr_loc in

482

let typ_l = Type_predef.type_clock typ_in in

483

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

484

expr.expr_type < typ_out;

485

typ_out

486

in

487

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

488

resulting_ty

489


490

and type_branches env in_main loc const hl =

491

let typ_in = new_var () in

492

let typ_out = new_var () in

493

try

494

let used_labels =

495

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

496

unify typ_in (type_const loc (Const_tag t));

497

type_subtyping_arg env in_main const h typ_out;

498

if List.mem t accu

499

then raise (Error (loc, Already_bound t))

500

else t :: accu) [] hl in

501

let type_labels = get_enum_type_tags (coretype_type typ_in) in

502

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

503

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

504

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

505

else (typ_in, typ_out)

506

with Unify (t1, t2) >

507

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

508


509

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

510

let type_eq env in_main undefined_vars eq =

511

(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)

512

(* Check undefined variables, type lhs *)

513

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

514

let ty_lhs = type_expr env in_main false expr_lhs in

515

(* Check multiple variable definitions *)

516

let define_var id uvars =

517

if ISet.mem id uvars

518

then ISet.remove id uvars

519

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

520

in

521

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

522

let ty_lhs =

523

type_of_type_list

524

(List.map2 (fun ty id >

525

if get_static_value ty <> None

526

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

527

match get_clock_base_type ty with

528

 None > ty

529

 Some ty > ty)

530

(type_list_of_type ty_lhs) eq.eq_lhs) in

531

let undefined_vars =

532

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

533

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

534

to a (always nonconstant) lhs variable *)

535

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

536

undefined_vars

537


538


539

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

540

in environment [env] *)

541

let type_coreclock env ck id loc =

542

match ck.ck_dec_desc with

543

 Ckdec_any > ()

544

 Ckdec_bool cl >

545

let dummy_id_expr = expr_of_ident id loc in

546

let when_expr =

547

List.fold_left

548

(fun expr (x, l) >

549

{expr_tag = new_tag ();

550

expr_desc= Expr_when (expr,x,l);

551

expr_type = new_var ();

552

expr_clock = Clocks.new_var true;

553

expr_delay = Delay.new_var ();

554

expr_loc=loc;

555

expr_annot = None})

556

dummy_id_expr cl

557

in

558

ignore (type_expr env false false when_expr)

559


560

let rec check_type_declaration loc cty =

561

match cty with

562

 Tydec_clock ty

563

 Tydec_array (_, ty) > check_type_declaration loc ty

564

 Tydec_const tname >

565

if not (Hashtbl.mem type_table cty)

566

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

567

 _ > ()

568


569

let type_var_decl vd_env env vdecl =

570

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

571

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

572

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

573

let type_dim d =

574

begin

575

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

576

Dimension.eval Basic_library.eval_env eval_const d;

577

end in

578

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

579


580

let ty_static =

581

if vdecl.var_dec_const

582

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

583

else ty in

584

(match vdecl.var_dec_value with

585

 None > ()

586

 Some v > type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);

587

try_unify ty_static vdecl.var_type vdecl.var_loc;

588

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

589

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

590

(*Format.eprintf "END %a@." Types.print_ty ty_static;*)

591

new_env

592


593

let type_var_decl_list vd_env env l =

594

List.fold_left (type_var_decl vd_env) env l

595


596

let type_of_vlist vars =

597

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

598

type_of_type_list tyl

599


600

let add_vdecl vd_env vdecl =

601

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

602

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

603

else vdecl::vd_env

604


605

let check_vd_env vd_env =

606

ignore (List.fold_left add_vdecl [] vd_env)

607


608

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

609

location is used for error reports. *)

610

let type_node env nd loc =

611

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

612

let vd_env_ol = nd.node_outputs@nd.node_locals in

613

let vd_env = nd.node_inputs@vd_env_ol in

614

check_vd_env vd_env;

615

let init_env = env in

616

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

617

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

618

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

619

let new_env = Env.overwrite env delta_env in

620

let undefined_vars_init =

621

List.fold_left

622

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

623

ISet.empty vd_env_ol in

624

let undefined_vars =

625

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

626

in

627

(* Typing asserts *)

628

List.iter (fun assert_ >

629

let assert_expr = assert_.assert_expr in

630

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

631

) nd.node_asserts;

632


633

(* check that table is empty *)

634

let local_consts = List.fold_left (fun res vdecl > if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in

635

let undefined_vars = ISet.diff undefined_vars local_consts in

636

if (not (ISet.is_empty undefined_vars)) then

637

raise (Error (loc, Undefined_var undefined_vars));

638

let ty_ins = type_of_vlist nd.node_inputs in

639

let ty_outs = type_of_vlist nd.node_outputs in

640

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

641

generalize ty_node;

642

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

643

nd.node_type < ty_node;

644

Env.add_value env nd.node_id ty_node

645


646

let type_imported_node env nd loc =

647

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

648

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

649

check_vd_env vd_env;

650

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

651

let ty_ins = type_of_vlist nd.nodei_inputs in

652

let ty_outs = type_of_vlist nd.nodei_outputs in

653

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

654

generalize ty_node;

655

(*

656

if (is_polymorphic ty_node) then

657

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

658

*)

659

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

660

nd.nodei_type < ty_node;

661

new_env

662


663

let type_top_const env cdecl =

664

let ty = type_const cdecl.const_loc cdecl.const_value in

665

let d =

666

if is_dimension_type ty

667

then dimension_of_const cdecl.const_loc cdecl.const_value

668

else Dimension.mkdim_var () in

669

let ty = Type_predef.type_static d ty in

670

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

671

cdecl.const_type < ty;

672

new_env

673


674

let type_top_consts env clist =

675

List.fold_left type_top_const env clist

676


677

let rec type_top_decl env decl =

678

match decl.top_decl_desc with

679

 Node nd > (

680

try

681

type_node env nd decl.top_decl_loc

682

with Error (loc, err) as exc > (

683

if !Options.global_inline then

684

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

685

Printers.pp_node nd

686

;

687

raise exc)

688

)

689

 ImportedNode nd >

690

type_imported_node env nd decl.top_decl_loc

691

 Const c >

692

type_top_const env c

693

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

694

 Open _ > env

695


696

let get_type_of_call decl =

697

match decl.top_decl_desc with

698

 Node nd >

699

let (in_typ, out_typ) = split_arrow nd.node_type in

700

type_list_of_type in_typ, type_list_of_type out_typ

701

 ImportedNode nd >

702

let (in_typ, out_typ) = split_arrow nd.nodei_type in

703

type_list_of_type in_typ, type_list_of_type out_typ

704

 _ > assert false

705


706

let type_prog env decls =

707

try

708

List.fold_left type_top_decl env decls

709

with Failure _ as exc > raise exc

710


711

(* Once the Lustre program is fully typed,

712

we must get back to the original description of dimensions,

713

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

714


715

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

716

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

717

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

718

*)

719

let uneval_vdecl_generics vdecl =

720

if vdecl.var_dec_const

721

then

722

match get_static_value vdecl.var_type with

723

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

724

 Some d > Dimension.uneval vdecl.var_id d

725


726

let uneval_node_generics vdecls =

727

List.iter uneval_vdecl_generics vdecls

728


729

let uneval_top_generics decl =

730

match decl.top_decl_desc with

731

 Node nd >

732

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

733

 ImportedNode nd >

734

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

735

 Const _

736

 TypeDef _

737

 Open _ > ()

738


739

let uneval_prog_generics prog =

740

List.iter uneval_top_generics prog

741


742

let rec get_imported_symbol decls id =

743

match decls with

744

 [] > assert false

745

 decl::q >

746

(match decl.top_decl_desc with

747

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

748

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

749

 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id

750

 _ > get_imported_symbol q id)

751


752

let check_env_compat header declared computed =

753

uneval_prog_generics header;

754

Env.iter declared (fun k decl_type_k >

755

let loc = (get_imported_symbol header k).top_decl_loc in

756

let computed_t =

757

instantiate (ref []) (ref [])

758

(try Env.lookup_value computed k

759

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

760

(*Types.print_ty Format.std_formatter decl_type_k;

761

Types.print_ty Format.std_formatter computed_t;*)

762

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

763

)

764


765

let check_typedef_top decl =

766

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

767

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

768

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

769

match decl.top_decl_desc with

770

 TypeDef ty >

771

let owner = decl.top_decl_owner in

772

let itf = decl.top_decl_itf in

773

let decl' =

774

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

775

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

776

let owner' = decl'.top_decl_owner in

777

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

778

let itf' = decl'.top_decl_itf in

779

(match decl'.top_decl_desc with

780

 Const _  Node _  ImportedNode _ > assert false

781

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

782

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

783

 _ > ()

784


785

let check_typedef_compat header =

786

List.iter check_typedef_top header

787


788

(* Local Variables: *)

789

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

790

(* End: *)
