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;

371

) targs tins;

372

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

373

touts;

374

end

375


376

(* type a simple call without dependent types

377

but possible homomorphic extension.

378

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

379

and type_simple_call env in_main loc const f targs =

380

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

381

let tfun = Type_predef.type_arrow tins touts in

382

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

383

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

384

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

385

touts

386


387

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

388

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

389

and type_expr env in_main const expr =

390

let resulting_ty =

391

match expr.expr_desc with

392

 Expr_const c >

393

let ty = type_const expr.expr_loc c in

394

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

395

expr.expr_type < ty;

396

ty

397

 Expr_ident v >

398

let tyv =

399

try

400

Env.lookup_value (fst env) v

401

with Not_found >

402

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

403

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

404

in

405

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

406

let ty' =

407

if const

408

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

409

else new_var () in

410

try_unify ty ty' expr.expr_loc;

411

expr.expr_type < ty;

412

ty

413

 Expr_array elist >

414

let ty_elt = new_var () in

415

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

416

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

417

let ty = Type_predef.type_array d ty_elt in

418

expr.expr_type < ty;

419

ty

420

 Expr_access (e1, d) >

421

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

422

let ty_elt = new_var () in

423

let d = Dimension.mkdim_var () in

424

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

425

expr.expr_type < ty_elt;

426

ty_elt

427

 Expr_power (e1, d) >

428

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

429

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

430

Dimension.eval Basic_library.eval_env eval_const d;

431

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

432

let ty = Type_predef.type_array d ty_elt in

433

expr.expr_type < ty;

434

ty

435

 Expr_tuple elist >

436

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

437

expr.expr_type < ty;

438

ty

439

 Expr_ite (c, t, e) >

440

type_subtyping_arg env in_main const c Type_predef.type_bool;

441

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

442

expr.expr_type < ty;

443

ty

444

 Expr_appl (id, args, r) >

445

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

446

expression *)

447

(match r with

448

 None > ()

449

 Some c >

450

check_constant expr.expr_loc const false;

451

type_subtyping_arg env in_main const c Type_predef.type_bool);

452

let args_list = expr_list_of_expr args in

453

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

454

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

455

expr.expr_type < touts;

456

touts

457

 Expr_fby (e1,e2)

458

 Expr_arrow (e1,e2) >

459

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

460

check_constant expr.expr_loc const false;

461

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

462

expr.expr_type < ty;

463

ty

464

 Expr_pre e >

465

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

466

check_constant expr.expr_loc const false;

467

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

468

expr.expr_type < ty;

469

ty

470

 Expr_when (e1,c,l) >

471

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

472

check_constant expr.expr_loc const false;

473

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

474

let expr_c = expr_of_ident c expr.expr_loc in

475

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

476

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

477

expr.expr_type < ty;

478

ty

479

 Expr_merge (c,hl) >

480

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

481

check_constant expr.expr_loc const false;

482

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

483

let expr_c = expr_of_ident c expr.expr_loc in

484

let typ_l = Type_predef.type_clock typ_in in

485

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

486

expr.expr_type < typ_out;

487

typ_out

488

in

489

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

490

resulting_ty

491


492

and type_branches env in_main loc const hl =

493

let typ_in = new_var () in

494

let typ_out = new_var () in

495

try

496

let used_labels =

497

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

498

unify typ_in (type_const loc (Const_tag t));

499

type_subtyping_arg env in_main const h typ_out;

500

if List.mem t accu

501

then raise (Error (loc, Already_bound t))

502

else t :: accu) [] hl in

503

let type_labels = get_enum_type_tags (coretype_type typ_in) in

504

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

505

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

506

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

507

else (typ_in, typ_out)

508

with Unify (t1, t2) >

509

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

510


511

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

512

let type_eq env in_main undefined_vars eq =

513

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

514

(* Check undefined variables, type lhs *)

515

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

516

let ty_lhs = type_expr env in_main false expr_lhs in

517

(* Check multiple variable definitions *)

518

let define_var id uvars =

519

if ISet.mem id uvars

520

then ISet.remove id uvars

521

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

522

in

523

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

524

let ty_lhs =

525

type_of_type_list

526

(List.map2 (fun ty id >

527

if get_static_value ty <> None

528

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

529

match get_clock_base_type ty with

530

 None > ty

531

 Some ty > ty)

532

(type_list_of_type ty_lhs) eq.eq_lhs) in

533

let undefined_vars =

534

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

535

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

536

to a (always nonconstant) lhs variable *)

537

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

538

undefined_vars

539


540


541

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

542

in environment [env] *)

543

let type_coreclock env ck id loc =

544

match ck.ck_dec_desc with

545

 Ckdec_any  Ckdec_pclock (_,_) > ()

546

 Ckdec_bool cl >

547

let dummy_id_expr = expr_of_ident id loc in

548

let when_expr =

549

List.fold_left

550

(fun expr (x, l) >

551

{expr_tag = new_tag ();

552

expr_desc= Expr_when (expr,x,l);

553

expr_type = new_var ();

554

expr_clock = Clocks.new_var true;

555

expr_delay = Delay.new_var ();

556

expr_loc=loc;

557

expr_annot = None})

558

dummy_id_expr cl

559

in

560

ignore (type_expr env false false when_expr)

561


562

let rec check_type_declaration loc cty =

563

match cty with

564

 Tydec_clock ty

565

 Tydec_array (_, ty) > check_type_declaration loc ty

566

 Tydec_const tname >

567

if not (Hashtbl.mem type_table cty)

568

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

569

 _ > ()

570


571

let type_var_decl vd_env env vdecl =

572

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

573

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

574

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

575

let type_dim d =

576

begin

577

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

578

Dimension.eval Basic_library.eval_env eval_const d;

579

end in

580

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

581


582

let ty_static =

583

if vdecl.var_dec_const

584

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

585

else ty in

586

(match vdecl.var_dec_value with

587

 None > ()

588

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

589

try_unify ty_static vdecl.var_type vdecl.var_loc;

590

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

591

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

592

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

593

new_env

594


595

let type_var_decl_list vd_env env l =

596

List.fold_left (type_var_decl vd_env) env l

597


598

let type_of_vlist vars =

599

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

600

type_of_type_list tyl

601


602

let add_vdecl vd_env vdecl =

603

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

604

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

605

else vdecl::vd_env

606


607

let check_vd_env vd_env =

608

ignore (List.fold_left add_vdecl [] vd_env)

609


610

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

611

location is used for error reports. *)

612

let type_node env nd loc =

613

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

614

let vd_env_ol = nd.node_outputs@nd.node_locals in

615

let vd_env = nd.node_inputs@vd_env_ol in

616

check_vd_env vd_env;

617

let init_env = env in

618

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

619

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

620

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

621

let new_env = Env.overwrite env delta_env in

622

let undefined_vars_init =

623

List.fold_left

624

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

625

ISet.empty vd_env_ol in

626

let undefined_vars =

627

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

628

in

629

(* Typing asserts *)

630

List.iter (fun assert_ >

631

let assert_expr = assert_.assert_expr in

632

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

633

) nd.node_asserts;

634


635

(* check that table is empty *)

636

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

637

let undefined_vars = ISet.diff undefined_vars local_consts in

638

if (not (ISet.is_empty undefined_vars)) then

639

raise (Error (loc, Undefined_var undefined_vars));

640

let ty_ins = type_of_vlist nd.node_inputs in

641

let ty_outs = type_of_vlist nd.node_outputs in

642

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

643

generalize ty_node;

644

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

645

nd.node_type < ty_node;

646

Env.add_value env nd.node_id ty_node

647


648

let type_imported_node env nd loc =

649

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

650

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

651

check_vd_env vd_env;

652

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

653

let ty_ins = type_of_vlist nd.nodei_inputs in

654

let ty_outs = type_of_vlist nd.nodei_outputs in

655

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

656

generalize ty_node;

657

(*

658

if (is_polymorphic ty_node) then

659

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

660

*)

661

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

662

nd.nodei_type < ty_node;

663

new_env

664


665

let type_top_const env cdecl =

666

let ty = type_const cdecl.const_loc cdecl.const_value in

667

let d =

668

if is_dimension_type ty

669

then dimension_of_const cdecl.const_loc cdecl.const_value

670

else Dimension.mkdim_var () in

671

let ty = Type_predef.type_static d ty in

672

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

673

cdecl.const_type < ty;

674

new_env

675


676

let type_top_consts env clist =

677

List.fold_left type_top_const env clist

678


679

let rec type_top_decl env decl =

680

match decl.top_decl_desc with

681

 Node nd > (

682

try

683

type_node env nd decl.top_decl_loc

684

with Error (loc, err) as exc > (

685

(*if !Options.global_inline then

686

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

687

Printers.pp_node nd

688

;*)

689

raise exc)

690

)

691

 ImportedNode nd >

692

type_imported_node env nd decl.top_decl_loc

693

 Const c >

694

type_top_const env c

695

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

696

 Open _ > env

697


698

let get_type_of_call decl =

699

match decl.top_decl_desc with

700

 Node nd >

701

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

702

type_list_of_type in_typ, type_list_of_type out_typ

703

 ImportedNode nd >

704

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

705

type_list_of_type in_typ, type_list_of_type out_typ

706

 _ > assert false

707


708

let type_prog env decls =

709

try

710

List.fold_left type_top_decl env decls

711

with Failure _ as exc > raise exc

712


713

(* Once the Lustre program is fully typed,

714

we must get back to the original description of dimensions,

715

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

716


717

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

718

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

719

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

720

*)

721

let uneval_vdecl_generics vdecl =

722

if vdecl.var_dec_const

723

then

724

match get_static_value vdecl.var_type with

725

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

726

 Some d > Dimension.uneval vdecl.var_id d

727


728

let uneval_node_generics vdecls =

729

List.iter uneval_vdecl_generics vdecls

730


731

let uneval_top_generics decl =

732

match decl.top_decl_desc with

733

 Node nd >

734

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

735

 ImportedNode nd >

736

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

737

 Const _

738

 TypeDef _

739

 Open _ > ()

740


741

let uneval_prog_generics prog =

742

List.iter uneval_top_generics prog

743


744

let rec get_imported_symbol decls id =

745

match decls with

746

 [] > assert false

747

 decl::q >

748

(match decl.top_decl_desc with

749

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

750

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

751

 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id

752

 _ > get_imported_symbol q id)

753


754

let check_env_compat header declared computed =

755

uneval_prog_generics header;

756

Env.iter declared (fun k decl_type_k >

757

let loc = (get_imported_symbol header k).top_decl_loc in

758

let computed_t =

759

instantiate (ref []) (ref [])

760

(try Env.lookup_value computed k

761

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

762

(*Types.print_ty Format.std_formatter decl_type_k;

763

Types.print_ty Format.std_formatter computed_t;*)

764

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

765

)

766


767

let check_typedef_top decl =

768

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

769

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

770

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

771

match decl.top_decl_desc with

772

 TypeDef ty >

773

let owner = decl.top_decl_owner in

774

let itf = decl.top_decl_itf in

775

let decl' =

776

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

777

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

778

let owner' = decl'.top_decl_owner in

779

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

780

let itf' = decl'.top_decl_itf in

781

(match decl'.top_decl_desc with

782

 Const _  Node _  ImportedNode _ > assert false

783

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

784

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

785

 _ > ()

786


787

let check_typedef_compat header =

788

List.iter check_typedef_top header

789


790

(* Local Variables: *)

791

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

792

(* End: *)
