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 Lustre_types

26

open Corelang

27

open Format

28


29


30

module type EXPR_TYPE_HUB =

31

sig

32

type type_expr

33

val import: Types.Main.type_expr > type_expr

34

val export: type_expr > Types.Main.type_expr

35

end

36


37

module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =

38

struct

39


40

module TP = Type_predef.Make (T)

41

include TP

42


43

let pp_typing_env fmt env =

44

Env.pp_env print_ty fmt env

45


46

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

47

(* Generic functions: occurs, instantiate and generalize *)

48

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

49


50

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

51

occurs in type [ty]. False otherwise. *)

52

let rec occurs tvar ty =

53

let ty = repr ty in

54

match type_desc ty with

55

 Tvar > ty=tvar

56

 Tarrow (t1, t2) >

57

(occurs tvar t1)  (occurs tvar t2)

58

 Ttuple tl >

59

List.exists (occurs tvar) tl

60

 Tstruct fl >

61

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

62

 Tarray (_, t)

63

 Tstatic (_, t)

64

 Tclock t

65

 Tlink t > occurs tvar t

66

 Tenum _  Tconst _  Tunivar  Tbasic _ > false

67


68

(** Promote monomorphic type variables to polymorphic type

69

variables. *)

70

(* Generalize by sideeffects *)

71

let rec generalize ty =

72

match type_desc ty with

73

 Tvar >

74

(* No scopes, always generalize *)

75

ty.tdesc < Tunivar

76

 Tarrow (t1,t2) >

77

generalize t1; generalize t2

78

 Ttuple tl >

79

List.iter generalize tl

80

 Tstruct fl >

81

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

82

 Tstatic (d, t)

83

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

84

 Tclock t

85

 Tlink t >

86

generalize t

87

 Tenum _  Tconst _  Tunivar  Tbasic _ > ()

88


89

(** Downgrade polymorphic type variables to monomorphic type

90

variables *)

91

let rec instantiate inst_vars inst_dim_vars ty =

92

let ty = repr ty in

93

match ty.tdesc with

94

 Tenum _  Tconst _  Tvar  Tbasic _ > ty

95

 Tarrow (t1,t2) >

96

{ty with tdesc =

97

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

98

 Ttuple tlist >

99

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

100

 Tstruct flist >

101

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

102

 Tclock t >

103

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

104

 Tstatic (d, t) >

105

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

106

 Tarray (d, t) >

107

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

108

 Tlink t >

109

(* should not happen *)

110

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

111

 Tunivar >

112

try

113

List.assoc ty.tid !inst_vars

114

with Not_found >

115

let var = new_var () in

116

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

117

var

118


119


120


121

let basic_coretype_type t =

122

if is_real_type t then Tydec_real else

123

if is_int_type t then Tydec_int else

124

if is_bool_type t then Tydec_bool else

125

assert false

126


127

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

128

let rec type_coretype type_dim cty =

129

match (*get_repr_type*) cty with

130

 Tydec_any > new_var ()

131

 Tydec_int > type_int

132

 Tydec_real > (* Type_predef. *)type_real

133

(*  Tydec_float > Type_predef.type_real *)

134

 Tydec_bool > (* Type_predef. *)type_bool

135

 Tydec_clock ty > (* Type_predef. *)type_clock (type_coretype type_dim ty)

136

 Tydec_const c > (* Type_predef. *)type_const c

137

 Tydec_enum tl > (* Type_predef. *)type_enum tl

138

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

139

 Tydec_array (d, ty) >

140

begin

141

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

142

type_dim d;

143

(* Type_predef. *)type_array d (type_coretype type_dim ty)

144

end

145


146

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

147

let rec coretype_type ty =

148

match (repr ty).tdesc with

149

 Tvar > Tydec_any

150

 Tbasic _ > basic_coretype_type ty

151

 Tconst c > Tydec_const c

152

 Tclock t > Tydec_clock (coretype_type t)

153

 Tenum tl > Tydec_enum tl

154

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

155

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

156

 Tstatic (_, t) > coretype_type t

157

 _ > assert false

158


159

let get_coretype_definition tname =

160

try

161

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

162

match top.top_decl_desc with

163

 TypeDef tdef > tdef.tydef_desc

164

 _ > assert false

165

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

166


167

let get_type_definition tname =

168

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

169


170

(* Equality on ground types only *)

171

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

172

let rec eq_ground t1 t2 =

173

let t1 = repr t1 in

174

let t2 = repr t2 in

175

t1==t2 

176

match t1.tdesc, t2.tdesc with

177

 Tbasic t1, Tbasic t2 when t1 == t2 > true

178

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

179

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

180

 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'

181

 (Tconst t, _) >

182

let def_t = get_type_definition t in

183

eq_ground def_t t2

184

 (_, Tconst t) >

185

let def_t = get_type_definition t in

186

eq_ground t1 def_t

187

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

188

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

189

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

190

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

191

 _ > false

192


193

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

194

using standard destructive unification.

195

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

196

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

197

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

198

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

199

If [semi] unification is required,

200

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

201

and constants are handled differently.*)

202

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

203

let rec unif t1 t2 =

204

let t1 = repr t1 in

205

let t2 = repr t2 in

206

if t1==t2 then

207

()

208

else

209

match t1.tdesc,t2.tdesc with

210

(* strictly subtyping cases first *)

211

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

212

unif t1 t2

213

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

214

unif t1 t2

215

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

216

 Tvar, Tvar >

217

if t1.tid < t2.tid then

218

t2.tdesc < Tlink t1

219

else

220

t1.tdesc < Tlink t2

221

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

222

t1.tdesc < Tlink t2

223

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

224

t2.tdesc < Tlink t1

225

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

226

begin

227

unif t2 t2';

228

unif t1' t1

229

end

230

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

231

List.iter2 unif tl tl'

232

 Ttuple [t1] , _ > unif t1 t2

233

 _ , Ttuple [t2] > unif t1 t2

234

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

235

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

236

 Tclock _, Tstatic _

237

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

238

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

239

 Tbasic t1, Tbasic t2 when t1 == t2 > ()

240

 Tunivar, _  _, Tunivar > ()

241

 (Tconst t, _) >

242

let def_t = get_type_definition t in

243

unif def_t t2

244

 (_, Tconst t) >

245

let def_t = get_type_definition t in

246

unif t1 def_t

247

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

248

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

249

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

250

let eval_const =

251

if semi

252

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

253

else (fun c > None) in

254

begin

255

unif t1' t2';

256

Dimension.eval Basic_library.eval_env eval_const e1;

257

Dimension.eval Basic_library.eval_env eval_const e2;

258

Dimension.unify ~semi:semi e1 e2;

259

end

260

(* Special cases for machine_types. Rules to unify static types infered

261

for numerical constants with non static ones for variables with

262

possible machine types *)

263

 Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 > BasicT.unify bt1 bt2

264

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

265

in unif t1 t2

266


267

(* Expected type ty1, got type ty2 *)

268

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

269

try

270

unify ~sub:sub ~semi:semi ty1 ty2

271

with

272

 Unify _ >

273

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

274

 Dimension.Unify _ >

275

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

276


277


278

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

279

(* Typing function for each basic AST construct *)

280

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

281


282

let rec type_struct_const_field ?(is_annot=false) loc (label, c) =

283

if Hashtbl.mem field_table label

284

then let tydef = Hashtbl.find field_table label in

285

let tydec = (typedef_of_top tydef).tydef_desc in

286

let tydec_struct = get_struct_type_fields tydec in

287

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

288

begin

289

try_unify ty_label (type_const ~is_annot loc c) loc;

290

type_coretype (fun d > ()) tydec

291

end

292

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

293


294

and type_const ?(is_annot=false) loc c =

295

match c with

296

 Const_int _ > (* Type_predef. *)type_int

297

 Const_real _ > (* Type_predef. *)type_real

298

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

299

let ty = new_var () in

300

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

301

(* Type_predef. *)type_array d ty

302

 Const_tag t >

303

if Hashtbl.mem tag_table t

304

then

305

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

306

let tydec =

307

if is_user_type tydef.tydef_desc

308

then Tydec_const tydef.tydef_id

309

else tydef.tydef_desc in

310

type_coretype (fun d > ()) tydec

311

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

312

 Const_struct fl >

313

let ty_struct = new_var () in

314

begin

315

let used =

316

List.fold_left

317

(fun acc (l, c) >

318

if List.mem l acc

319

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

320

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

321

[] fl in

322

try

323

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

324

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

325

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

326

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

327

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

328

with Not_found >

329

ty_struct

330

end

331

 Const_string _  Const_modeid _ >

332

if is_annot then (* Type_predef. *)type_string else assert false (* string datatype should only appear in annotations *)

333


334

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

335

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

336

[env] is a pair composed of:

337

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

338

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

339

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

340

propagation policy in Lustre.

341

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

342

later discovered to be clocks during the typing process.

343

*)

344

let check_constant loc const_expected const_real =

345

if const_expected && not const_real

346

then raise (Error (loc, Not_a_constant))

347


348

let rec type_add_const env const arg targ =

349

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

350

if const

351

then let d =

352

if is_dimension_type targ

353

then dimension_of_expr arg

354

else Dimension.mkdim_var () in

355

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

356

Dimension.eval Basic_library.eval_env eval_const d;

357

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

358

(match (* Types. *)get_static_value targ with

359

 None > ()

360

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

361

real_static_type

362

else targ

363


364

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

365

used during node applications and assignments *)

366

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

367

let loc = real_arg.expr_loc in

368

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

369

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

370

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

371

try_unify ~sub:sub formal_type real_type loc

372


373

(* typing an application implies:

374

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

375

 checking type adequation between formal and real arguments

376

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

377

it in many calls

378

*)

379

and type_appl env in_main loc const f args =

380

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

381

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

382

then

383

try

384

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

385

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

386

with

387

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

388


389

else (

390

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

391

)

392


393

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

394

and type_dependent_call env in_main loc const f targs =

395

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

396

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

397

(* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)

398

let tfun = (* Type_predef. *)type_arrow tins touts in

399

(* Format.eprintf "fun=%a@." print_ty tfun; *)

400

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

401

(* Format.eprintf "type subtyping@."; *)

402

let tins = type_list_of_type tins in

403

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

404

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

405

else

406

begin

407

List.iter2 (

408

fun (a,t) ti >

409

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

410

(* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *)

411

try_unify ~sub:true ti t' a.expr_loc;

412

(* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *)

413


414

)

415

targs

416

tins;

417

touts

418

end

419


420

(* type a simple call without dependent types

421

but possible homomorphic extension.

422

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

423

and type_simple_call env in_main loc const f targs =

424

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

425

let tfun = (* Type_predef. *)type_arrow tins touts in

426

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

427

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

428

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

429

touts

430


431

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

432

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

433

and type_expr ?(is_annot=false) env in_main const expr =

434

let resulting_ty =

435

match expr.expr_desc with

436

 Expr_const c >

437

let ty = type_const ~is_annot expr.expr_loc c in

438

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

439

expr.expr_type < Expr_type_hub.export ty;

440

ty

441

 Expr_ident v >

442

let tyv =

443

try

444

Env.lookup_value (fst env) v

445

with Not_found >

446

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

447

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

448

in

449

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

450

let ty' =

451

if const

452

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

453

else new_var () in

454

try_unify ty ty' expr.expr_loc;

455

expr.expr_type < Expr_type_hub.export ty;

456

ty

457

 Expr_array elist >

458

let ty_elt = new_var () in

459

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

460

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

461

let ty = (* Type_predef. *)type_array d ty_elt in

462

expr.expr_type < Expr_type_hub.export ty;

463

ty

464

 Expr_access (e1, d) >

465

type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int;

466

let ty_elt = new_var () in

467

let d = Dimension.mkdim_var () in

468

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

469

expr.expr_type < Expr_type_hub.export ty_elt;

470

ty_elt

471

 Expr_power (e1, d) >

472

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

473

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

474

Dimension.eval Basic_library.eval_env eval_const d;

475

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

476

let ty = (* Type_predef. *)type_array d ty_elt in

477

expr.expr_type < Expr_type_hub.export ty;

478

ty

479

 Expr_tuple elist >

480

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

481

expr.expr_type < Expr_type_hub.export ty;

482

ty

483

 Expr_ite (c, t, e) >

484

type_subtyping_arg env in_main const c (* Type_predef. *)type_bool;

485

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

486

expr.expr_type < Expr_type_hub.export ty;

487

ty

488

 Expr_appl (id, args, r) >

489

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

490

expression *)

491

(match r with

492

 None > ()

493

 Some c >

494

check_constant expr.expr_loc const false;

495

type_subtyping_arg env in_main const c (* Type_predef. *)type_bool);

496

let args_list = expr_list_of_expr args in

497

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

498

let targs = new_ty (Ttuple (List.map (fun a > Expr_type_hub.import a.expr_type) args_list)) in

499

args.expr_type < Expr_type_hub.export targs;

500

expr.expr_type < Expr_type_hub.export touts;

501

touts

502

 Expr_fby (e1,e2)

503

 Expr_arrow (e1,e2) >

504

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

505

check_constant expr.expr_loc const false;

506

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

507

expr.expr_type < Expr_type_hub.export ty;

508

ty

509

 Expr_pre e >

510

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

511

check_constant expr.expr_loc const false;

512

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

513

expr.expr_type < Expr_type_hub.export ty;

514

ty

515

 Expr_when (e1,c,l) >

516

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

517

check_constant expr.expr_loc const false;

518

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

519

let expr_c = expr_of_ident c expr.expr_loc in

520

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

521

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

522

expr.expr_type < Expr_type_hub.export ty;

523

ty

524

 Expr_merge (c,hl) >

525

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

526

check_constant expr.expr_loc const false;

527

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

528

let expr_c = expr_of_ident c expr.expr_loc in

529

let typ_l = (* Type_predef. *)type_clock typ_in in

530

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

531

expr.expr_type < Expr_type_hub.export typ_out;

532

typ_out

533

in

534

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

535

resulting_ty

536


537

and type_branches ?(is_annot=false) env in_main loc const hl =

538

let typ_in = new_var () in

539

let typ_out = new_var () in

540

try

541

let used_labels =

542

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

543

unify typ_in (type_const ~is_annot loc (Const_tag t));

544

type_subtyping_arg env in_main const h typ_out;

545

if List.mem t accu

546

then raise (Error (loc, Already_bound t))

547

else t :: accu) [] hl in

548

let type_labels = get_enum_type_tags (coretype_type typ_in) in

549

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

550

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

551

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

552

else (typ_in, typ_out)

553

with Unify (t1, t2) >

554

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

555


556

(* Eexpr are always in annotations. TODO: add the quantifiers variables to the env *)

557

let type_eexpr env eexpr =

558

(type_expr

559

~is_annot:true

560

env

561

false (* not in main *)

562

false (* not a const *)

563

eexpr.eexpr_qfexpr)

564


565


566

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

567

let type_eq env in_main undefined_vars eq =

568

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

569

(* Check undefined variables, type lhs *)

570

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

571

let ty_lhs = type_expr env in_main false expr_lhs in

572

(* Check multiple variable definitions *)

573

let define_var id uvars =

574

if ISet.mem id uvars

575

then ISet.remove id uvars

576

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

577

in

578

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

579

let ty_lhs =

580

type_of_type_list

581

(List.map2 (fun ty id >

582

if get_static_value ty <> None

583

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

584

match get_clock_base_type ty with

585

 None > ty

586

 Some ty > ty)

587

(type_list_of_type ty_lhs) eq.eq_lhs) in

588

let undefined_vars =

589

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

590

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

591

to a (always nonconstant) lhs variable *)

592

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

593

undefined_vars

594


595


596

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

597

in environment [env] *)

598

let type_coreclock env ck id loc =

599

match ck.ck_dec_desc with

600

 Ckdec_any > ()

601

 Ckdec_bool cl >

602

let dummy_id_expr = expr_of_ident id loc in

603

let when_expr =

604

List.fold_left

605

(fun expr (x, l) >

606

{expr_tag = new_tag ();

607

expr_desc= Expr_when (expr,x,l);

608

expr_type = Types.Main.new_var ();

609

expr_clock = Clocks.new_var true;

610

expr_delay = Delay.new_var ();

611

expr_loc=loc;

612

expr_annot = None})

613

dummy_id_expr cl

614

in

615

ignore (type_expr env false false when_expr)

616


617

let rec check_type_declaration loc cty =

618

match cty with

619

 Tydec_clock ty

620

 Tydec_array (_, ty) > check_type_declaration loc ty

621

 Tydec_const tname >

622

(* Format.eprintf "TABLE: %a@." print_type_table (); *)

623

if not (Hashtbl.mem type_table cty)

624

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

625

 _ > ()

626


627

let type_var_decl vd_env env vdecl =

628

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

629

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

630

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

631

let type_dim d =

632

begin

633

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

634

Dimension.eval Basic_library.eval_env eval_const d;

635

end in

636

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

637


638

let ty_static =

639

if vdecl.var_dec_const

640

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

641

else ty in

642

(match vdecl.var_dec_value with

643

 None > ()

644

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

645

try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;

646

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

647

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

648

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

649

new_env

650


651

let type_var_decl_list vd_env env l =

652

List.fold_left (type_var_decl vd_env) env l

653


654

let type_of_vlist vars =

655

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

656

type_of_type_list tyl

657


658

let add_vdecl vd_env vdecl =

659

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

660

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

661

else vdecl::vd_env

662


663

let check_vd_env vd_env =

664

ignore (List.fold_left add_vdecl [] vd_env)

665


666

let type_spec env c =

667

(*TODO

668

enrich env locally with locals and consts

669

type each pre/post as a boolean expr

670

I don't know if we want to update the global env with locally typed variables.

671

For the moment, returning the provided env

672

*)

673

env

674


675

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

676

location is used for error reports. *)

677

let type_node env nd loc =

678

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

679

let vd_env_ol = nd.node_outputs@nd.node_locals in

680

let vd_env = nd.node_inputs@vd_env_ol in

681

check_vd_env vd_env;

682

let init_env = env in

683

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

684

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

685

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

686

let new_env = Env.overwrite env delta_env in

687

let undefined_vars_init =

688

List.fold_left

689

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

690

ISet.empty vd_env_ol in

691

let undefined_vars =

692

let eqs, auts = get_node_eqs nd in

693

(* TODO XXX: il faut typer les handlers de l'automate *)

694

List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs

695

in

696

(* Typing asserts *)

697

List.iter (fun assert_ >

698

let assert_expr = assert_.assert_expr in

699

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

700

) nd.node_asserts;

701

(* Typing spec/contracts *)

702

(match nd.node_spec with None > ()  Some spec > ignore (type_spec (new_env, vd_env) spec));

703

(* Typing annots *)

704

List.iter (fun annot >

705

List.iter (fun (_, eexpr) > ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots

706

) nd.node_annot;

707


708

(* check that table is empty *)

709

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

710

let undefined_vars = ISet.diff undefined_vars local_consts in

711

if (not (ISet.is_empty undefined_vars)) then

712

raise (Error (loc, Undefined_var undefined_vars));

713

let ty_ins = type_of_vlist nd.node_inputs in

714

let ty_outs = type_of_vlist nd.node_outputs in

715

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

716

generalize ty_node;

717

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

718

nd.node_type < Expr_type_hub.export ty_node;

719

Env.add_value env nd.node_id ty_node

720


721

let type_imported_node env nd loc =

722

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

723

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

724

check_vd_env vd_env;

725

ignore(type_var_decl_list vd_env new_env nd.nodei_outputs);

726

let ty_ins = type_of_vlist nd.nodei_inputs in

727

let ty_outs = type_of_vlist nd.nodei_outputs in

728

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

729

generalize ty_node;

730

(*

731

if (is_polymorphic ty_node) then

732

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

733

*)

734

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

735

nd.nodei_type < Expr_type_hub.export ty_node;

736

new_env

737


738

let type_top_const env cdecl =

739

let ty = type_const cdecl.const_loc cdecl.const_value in

740

let d =

741

if is_dimension_type ty

742

then dimension_of_const cdecl.const_loc cdecl.const_value

743

else Dimension.mkdim_var () in

744

let ty = (* Type_predef. *)type_static d ty in

745

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

746

cdecl.const_type < Expr_type_hub.export ty;

747

new_env

748


749

let type_top_consts env clist =

750

List.fold_left type_top_const env clist

751


752

let rec type_top_decl env decl =

753

match decl.top_decl_desc with

754

 Node nd > (

755

try

756

type_node env nd decl.top_decl_loc

757

with Error (loc, err) as exc > (

758

if !Options.global_inline then

759

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

760

Printers.pp_node nd

761

;

762

raise exc)

763

)

764

 ImportedNode nd >

765

type_imported_node env nd decl.top_decl_loc

766

 Const c >

767

type_top_const env c

768

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

769

 Open _ > env

770


771

let get_type_of_call decl =

772

match decl.top_decl_desc with

773

 Node nd >

774

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

775

type_list_of_type in_typ, type_list_of_type out_typ

776

 ImportedNode nd >

777

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

778

type_list_of_type in_typ, type_list_of_type out_typ

779

 _ > assert false

780


781

let type_prog env decls =

782

try

783

List.fold_left type_top_decl env decls

784

with Failure _ as exc > raise exc

785


786

(* Once the Lustre program is fully typed, we must get back to the

787

original description of dimensions, with constant parameters,

788

instead of unifiable internal variables. *)

789


790

(* The following functions aims at 'unevaluating' dimension

791

expressions occuring in array types, i.e. replacing unifiable

792

second_order variables with the original static parameters.

793

Once restored in this formulation, dimensions may be

794

meaningfully printed. *)

795

let uneval_vdecl_generics vdecl =

796

if vdecl.var_dec_const

797

then

798

match get_static_value (Expr_type_hub.import vdecl.var_type) with

799

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

800

 Some d > Dimension.uneval vdecl.var_id d

801


802

let uneval_node_generics vdecls =

803

List.iter uneval_vdecl_generics vdecls

804


805

let uneval_spec_generics spec =

806

List.iter uneval_vdecl_generics (spec.consts@spec.locals)

807


808

let uneval_top_generics decl =

809

match decl.top_decl_desc with

810

 Node nd >

811

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

812

 ImportedNode nd >

813

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

814

 Const _

815

 TypeDef _

816

 Open _

817

> ()

818


819

let uneval_prog_generics prog =

820

List.iter uneval_top_generics prog

821


822

let rec get_imported_symbol decls id =

823

match decls with

824

 [] > assert false

825

 decl::q >

826

(match decl.top_decl_desc with

827

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

828

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

829

 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id

830

 _ > get_imported_symbol q id)

831


832

let check_env_compat header declared computed =

833

uneval_prog_generics header;

834

Env.iter declared (fun k decl_type_k >

835

let loc = (get_imported_symbol header k).top_decl_loc in

836

let computed_t =

837

instantiate (ref []) (ref [])

838

(try Env.lookup_value computed k

839

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

840

(*Types.print_ty Format.std_formatter decl_type_k;

841

Types.print_ty Format.std_formatter computed_t;*)

842

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

843

)

844


845

let check_typedef_top decl =

846

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

847

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

848

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

849

match decl.top_decl_desc with

850

 TypeDef ty >

851

let owner = decl.top_decl_owner in

852

let itf = decl.top_decl_itf in

853

let decl' =

854

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

855

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

856

let owner' = decl'.top_decl_owner in

857

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

858

let itf' = decl'.top_decl_itf in

859

(match decl'.top_decl_desc with

860

 Const _  Node _  ImportedNode _ > assert false

861

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

862

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

863

 _ > ()

864


865

let check_typedef_compat header =

866

List.iter check_typedef_top header

867

end

868


869

include Make(Types.Main) (struct

870

type type_expr = Types.Main.type_expr

871

let import x = x

872

let export x = x

873

end)

874

(* Local Variables: *)

875

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

876

(* End: *)
